Foundational layer: A2ML v1.1 (profiles + base vocab + citations + hashing) and K9-SVC 1.0 hardening (#358)

## Foundational layer: A2ML + K9-SVC

The substrate between attestation (A2ML) and validation (K9). A2ML and
K9-SVC are
**independent foundations that name no consumer**; CodeCite/ProofTrace
stay as
standalone consumers in their own repos. **All 13 tasks landed.**

### Owner decision captured
- **K9 Hunt leash** requires **all five** preconditions, **always**
(signature +
policy + sandbox + dry-run + capability grant) — no configurable subset.

### A2ML (`a2ml/`)
1. ✅ **Lineage cleanup** — prior specs frozen under `archive/` (v0
draft, v1.0.0)
with NOT-NORMATIVE banners; `SPEC.adoc` is the single normative spec
(**v1.1.0**);
`VERSIONS.adoc` is the lineage SSOT; README reconciled "Draft v0.6.0" →
   "Stable v1.1.0". Licence prose untouched (flag-only).
2. ✅ **Profile mechanism** — `@profile`/`@profile-def`, offline
deterministic
   resolution, SSOT + hash-pinned registry (SPEC §8/§11).
3. ✅ **Base record vocabulary** `@record` — the anti-desync primitive
(SPEC §7).
4. ✅ **Citation primitives** — inert without a citation profile (SPEC
§10).
5. ✅ **Canonical hash form** (sha256); signing reserved & inert (SPEC
§9).
6. ✅ **Idris2 core** — `BaseVocab.idr` + `Profiles.idr`, decidable
checks, `%default total`.

### 6a2 (`.machine_readable/`)
7. ✅ Seven profile definitions `a2ml/state … a2ml/anchor` + verifiable
`REGISTRY.a2ml`.
8. ✅ `@profile` on all seven 6a2 files; hypatia rule **HYP-S006
profile-drift-detector** (FLAG-ONLY).

### K9-SVC (`k9-svc/`) — finishes alpha → **1.0.0 STABLE**
9. ✅ **Capability model** (`capabilities.ncl`): closed core enum +
reserved `x-` namespace; default-deny.
10. ✅ **Leash modes normative** (`leash.ncl`): Kennel/Yard/Hunt;
`authorize_hunt` = all five, always.
11. ✅ **Pedigree restructure** (`pedigree.ncl`): 7 sections incl. new
`recovery_recipe` + `docs_rationale`.
12. ✅ **Receipt schema** (`receipt/`): canonical `a2ml/k9-receipt`
profile + lossless JSON projection + worked example.
13. ✅ **Soft A2ML cross-ref** (`docs_rationale.a2ml_ref`);
must/just/nickel vs must/trust/dust/intend kept distinct.

### CI notes (for reviewers)
- **governance / Trusted-base** failure was mine (a `partial`); fixed by
making
`sectionTitlesOf` total — eliminated the escape hatch (verified locally,
gate exits 0).
- **Idris2 a2ml/AVOW** failures were **pre-existing shared infra** in
  `echidna-verify.yml` (deprecated `actions/cache` pin + an interactive
idris2-pack bootstrap that hit EOF + wrong PATH). Both fail identically
on AVOW
(which this PR never touches). Fixed: bumped the cache pin to a SHA
already
trusted in-repo, fed the pack prompt its default, corrected PATH. This
also
  wires the new v1.1 a2ml core into the type-check.
- **Hypatia security scan** (222 findings) are all `workflow_audit`
items
(`unpinned_action`, `missing_timeout_minutes`) on workflow files this PR
does
  not modify — pre-existing/estate-wide, not introduced here.

### Note on SPDX
New files match their directory's existing SPDX convention
(`AGPL-3.0-or-later`).
Pre-existing licence drift in `a2ml/` prose (README/spec say
`PMPL-1.0-or-later`
while headers say `AGPL-3.0-or-later`) is **flagged, not touched**, per
the
manual-only licence policy.

🤖 Draft.

https://claude.ai/code/session_01XZhw6Fq27eoeyEB4LR3a2c

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/echidna-verify.yml

@@ -93,7 +93,7 @@ jobs:
           submodules: recursive
 
       - name: Cache pack
-        uses: actions/cache@0c45773b623bea8c8e75f6c82b208c3cf94ea4f9 # v4.0.2
+        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
         with:
           path: |
             ~/.pack
@@ -116,17 +116,31 @@ jobs:
           git clone --depth 1 https://github.com/stefan-hoeck/idris2-pack.git "$HOME/idris2-pack"
           cd "$HOME/idris2-pack"
           # Use the bootstrap script in non-interactive mode
-          bash install.bash </dev/null || echo "::warning::pack install had warnings"
+          # pack's install.bash prompts for the scheme binary; feeding newlines
+          # makes the prompt take its detected default (chezscheme) instead of
+          # hitting EOF (which aborts the bootstrap and leaves pack uninstalled).
+          yes '' | bash install.bash || echo "::warning::pack install had warnings"
+          # pack installs its launcher into ~/.local/bin (newer layout) and/or
+          # ~/.pack/bin (older); add both so `pack` resolves on PATH.
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
           echo "$HOME/.pack/bin" >> "$GITHUB_PATH"
-          export PATH="$HOME/.pack/bin:$PATH"
-          pack install-api idris2
+          export PATH="$HOME/.local/bin:$HOME/.pack/bin:$PATH"
+          # `install-api` is not a pack subcommand; `install-app idris2`
+          # installs the idris2 executable into the pack bin dir so the
+          # subsequent `idris2 --check` resolves. The base library (Prelude,
+          # base, contrib) ships with idris2, so no .ipkg is needed for a
+          # standalone --check.
+          pack install-app idris2
           idris2 --version
 
-      - name: Type-check A2ML.Proofs
+      - name: Type-check A2ML core (Proofs + v1.1 profiles/base-vocab)
         run: |
           export PATH="$HOME/.pack/bin:$PATH"
           cd a2ml
           idris2 --check src/A2ML/Proofs.idr 2>&1 | tee ../idris2-a2ml.log
+          # v1.1 additive core: checking Profiles.idr transitively type-checks
+          # BaseVocab.idr and TypedCore.idr (its imports).
+          idris2 --check src/A2ML/Profiles.idr 2>&1 | tee -a ../idris2-a2ml.log
 
       - name: Upload log
         if: always()
@@ -147,7 +161,7 @@ jobs:
           submodules: recursive
 
       - name: Cache pack
-        uses: actions/cache@0c45773b623bea8c8e75f6c82b208c3cf94ea4f9 # v4.0.2
+        uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # v4
         with:
           path: |
             ~/.pack
@@ -167,10 +181,21 @@ jobs:
           sudo apt-get install -y build-essential libgmp-dev chezscheme
           git clone --depth 1 https://github.com/stefan-hoeck/idris2-pack.git "$HOME/idris2-pack"
           cd "$HOME/idris2-pack"
-          bash install.bash </dev/null || echo "::warning::pack install had warnings"
+          # pack's install.bash prompts for the scheme binary; feeding newlines
+          # makes the prompt take its detected default (chezscheme) instead of
+          # hitting EOF (which aborts the bootstrap and leaves pack uninstalled).
+          yes '' | bash install.bash || echo "::warning::pack install had warnings"
+          # pack installs its launcher into ~/.local/bin (newer layout) and/or
+          # ~/.pack/bin (older); add both so `pack` resolves on PATH.
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
           echo "$HOME/.pack/bin" >> "$GITHUB_PATH"
-          export PATH="$HOME/.pack/bin:$PATH"
-          pack install-api idris2
+          export PATH="$HOME/.local/bin:$HOME/.pack/bin:$PATH"
+          # `install-api` is not a pack subcommand; `install-app idris2`
+          # installs the idris2 executable into the pack bin dir so the
+          # subsequent `idris2 --check` resolves. The base library (Prelude,
+          # base, contrib) ships with idris2, so no .ipkg is needed for a
+          # standalone --check.
+          pack install-app idris2
           idris2 --version
 
       - name: Type-check AVOW proofs

.machine_readable/6a2/AGENTIC.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # AGENTIC.a2ml — AI agent constraints and capabilities
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-agentic/.
+@profile(id=a2ml/agentic)
+
 [metadata]
 version = "0.1.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # ECOSYSTEM.a2ml — Standards ecosystem position
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-ecosystem/.
+@profile(id=a2ml/ecosystem)
+
 [metadata]
 version = "1.0.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/META.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # META.a2ml — Standards meta-level information
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-meta/.
+@profile(id=a2ml/meta)
+
 [metadata]
 version = "1.0.0"
 last-updated = "2026-05-15"

.machine_readable/6a2/NEUROSYM.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # NEUROSYM.a2ml — Neurosymbolic integration metadata
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-neurosym/.
+@profile(id=a2ml/neurosym)
+
 [metadata]
 version = "0.1.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # PLAYBOOK.a2ml — Operational playbook
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-playbook/.
+@profile(id=a2ml/playbook)
+
 [metadata]
 version = "0.1.0"
 last-updated = "2026-04-11"

.machine_readable/6a2/STATE.a2ml

@@ -2,6 +2,11 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # STATE.a2ml — Standards project state
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-state/.
+@profile(id=a2ml/state)
+
 [metadata]
 project = "standards"
 version = "0.2.0"

.machine_readable/REGISTRY.a2ml

@@ -32,7 +32,7 @@ name = "A2ML — Attested Markup Language"
 stream = "foundation"
 home = "a2ml/"
 canonical_doc = "a2ml/README.adoc"
-source_hash = "sha256:b34ffe4d51c1715c4f2e51183d7a510865dc03e962fbeae121e3868fd88a718a"
+source_hash = "sha256:ffda43ed07bed095c7623d3c6a1d38c8f17a6b9e4eebaebe3bfde5aff62bcfb0"
 route = "the typed/verified machine-readable document format"
 
 [[spec]]
@@ -41,7 +41,7 @@ name = "K9 Self-Validating Components"
 stream = "foundation"
 home = "k9-svc/"
 canonical_doc = "k9-svc/README.adoc"
-source_hash = "sha256:eae3b6a0f4e2da1afcfddfecf7a5c173d6c0ac090923c63fe9c14806b5a3b11b"
+source_hash = "sha256:6a9c2065fc29abdaaeef08c3e551f21c7408afd3c9a7cee4ed3e73460db443ab"
 route = "self-validating components with embedded contracts + deploy logic"
 
 [[spec]]
@@ -266,7 +266,7 @@ name = "Standards Hypatia Rules"
 stream = "integration"
 home = "hypatia-rules/"
 canonical_doc = "hypatia-rules/README.adoc"
-source_hash = "sha256:707852684795e8474bc764473c36bc4d56fa139014ab3abbc0f550319637138c"
+source_hash = "sha256:a63e95c5e43ced2ee13c58014175da156c71ab731f01449e3a61b3e2f33bbe52"
 route = "the dogfooding rules that scan THIS repo (incl. drift detection)"
 
 [[spec]]

.machine_readable/anchors/ANCHOR.a2ml

@@ -1,5 +1,9 @@
 # ⚓ ANCHOR: standards
 # This is the canonical authority for the standards repository.
+#
+# A2ML profile declaration (SPEC.adoc Section 8.1): validates this record
+# through the profile mechanism. Definition: a2ml/profiles/a2ml-anchor/.
+@profile(id=a2ml/anchor)
 
 id: "org.hyperpolymath.standards"
 version: "1.0.0"

a2ml/README.adoc

@@ -50,7 +50,9 @@ A2ML is a typed, attested markup format. It verifies structure and references.
 
 == Documents
 
-* link:SPEC.adoc[Spec: Surface Grammar + Typed Core]
+* link:SPEC.adoc[Spec (current normative, v1.1.0): Surface Grammar + Typed Core + Profiles]
+* link:VERSIONS.adoc[Specification Lineage (versions + era)]
+* link:archive/[Archived (frozen) prior specs]
 * link:docs/QUICKSTART.adoc[Module 0 Quickstart + FAQ]
 * link:docs/MODULES.adoc[Syntax Modules (Opt-in)]
 * link:docs/GRAMMAR.adoc[Grammar Appendix]
@@ -101,6 +103,8 @@ A2ML is a typed, attested markup format. It verifies structure and references.
 * link:RELEASE-NOTES-v0.1.0.adoc[v0.1.0 Release Notes]
 * link:RELEASE-NOTES-v0.5.0.adoc[v0.5.0 Release Notes]
 * link:RELEASE-NOTES-v0.6.0.adoc[v0.6.0 Release Notes]
+* link:RELEASE-NOTES-v1.0.0.adoc[v1.0.0 Release Notes]
+* link:RELEASE-NOTES-v1.1.0.adoc[v1.1.0 Release Notes]
 
 == Announcement
 
@@ -110,9 +114,13 @@ A2ML is a typed, attested markup format. It verifies structure and references.
 
 == Status
 
-* Draft specification, v0.6.0
-* Prototype parser + CLI + demo page available
-* Typed core stubs + core tests passing (prototype)
+* *Stable specification, v1.1.0* (era v1). See link:VERSIONS.adoc[VERSIONS.adoc]
+  for the lineage; prior drafts (v0) and the frozen v1.0.0 release are under
+  link:archive/[archive/].
+* v1.1.0 is additive over v1.0.0: profile mechanism, base record vocabulary,
+  citation primitives, and canonical hashing — all inert under the base modes.
+* Prototype parser + CLI + demo page available.
+* Typed core + core tests passing (prototype).
 
 == License