docs(machine_readable): ochrance checkpoint — refresh 6a2 + ANCHOR (#35)

Refresh all six 6a2 files + ANCHOR from the March .scm-converted stubs to current content: proven surface, proof-campaign milestones, decisions D1/D2/D3, combiner generalization, honest proof bounds, build/verify runbooks, and a realignment record for the 2026-06-05 convergence.

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -3,10 +3,9 @@
 #
 # AGENTIC.a2ml — AI agent constraints and capabilities
 # Defines what AI agents can and cannot do in this repository.
-
 [metadata]
 version = "0.1.0"
-last-updated = "2026-03-16"
+last-updated = "2026-06-05"
 
 [agent-permissions]
 can-edit-source = true
@@ -17,8 +16,16 @@ can-create-files = true
 
 [agent-constraints]
 # What AI agents must NOT do:
-# - Never use banned language patterns (believe_me, unsafeCoerce, etc.)
+# - Never use banned proof escapes (believe_me, assert_total, postulate, unsafePerformIO, holes) on proof symbols
+# - Never weaken %default total, nor introduce `covering` / `partial` on verification code
 # - Never commit secrets or credentials
 # - Never use banned languages (TypeScript, Python, Go, etc.)
-# - Never place state files in repository root (must be in .machine_readable/)
-# - Never use AGPL license (use MPL-2.0)
+# - Never place state/meta files in repository root (must live under .machine_readable/)
+# - Never use AGPL (license is MPL-2.0)
+
+[agent-workflow]
+# How AI agents should work here:
+proof-campaign = "resume from docs/PROOFS.adoc — the authoritative, dependency-sorted plan; it survives context compaction"
+post-migration = "on return from the svalinn → Ephapax track, follow docs/AFTER-MIGRATION.adoc before resuming"
+verification-gate = "idris2 --build ochrance.ipkg must stay clean and fully total"
+model-guidance = "Opus for proof discovery / structural walls; Sonnet for mechanisation, refactors, tests; Haiku for grunt sweeps"

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -1,10 +1,28 @@
 # SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
 # ECOSYSTEM.a2ml — Ecosystem position
-# Converted from ECOSYSTEM.scm on 2026-03-15
-
 [metadata]
 project = "ochrance"
 ecosystem = "hyperpolymath"
+last-updated = "2026-06-05"
 
 [position]
 type = "component"
+role = """Neurosymbolic filesystem-integrity verifier — the receipt/attestation layer for accountable state transitions."""
+
+[related-projects]
+projects = [
+  "echidna — Rust/Julia neurosymbolic prover (provides libechidna.so); Ochránce adds Idris2 as a backend",
+  "idris2-echidna — Idris2 prover abstraction layer",
+  "proven — Idris2 formally verified library",
+  "ochrance-framework — architecture + docs; its duplicate core is retired (D1)",
+  "svalinn — estate sibling, edge verification gateway; migrating ReScript → Ephapax (D3)",
+  "valence-shell — consumes Ochránce receipts for accountable state transitions (see integrations/valence-shell-bridge.a2ml)",
+  "echo-types — semantics of the residue/loss those transitions expose",
+  "boj-server — SSG/build host (casket engine); ANCHOR parent (see anchors/ANCHOR.a2ml)",
+]
+
+[integrations]
+# detail in .machine_readable/integrations/*.a2ml
+declared = [ "proven", "valence-shell-bridge", "verisimdb", "vexometer", "feedback-o-tron" ]

.machine_readable/6a2/META.a2ml

@@ -1,9 +1,33 @@
 # SPDX-License-Identifier: MPL-2.0
-# META.a2ml — Project meta-information
-# Converted from META.scm on 2026-03-15
-
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# META.a2ml — Architecture decisions & development practices
 [metadata]
 project = "ochrance"
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
 license = "MPL-2.0"
 standard = "RSR 2026"
+last-updated = "2026-06-05"
+
+[architecture]
+summary = """6-layer trust pyramid (L0 hardware root → L5 TUI/telemetry). Framework-first: a VerifiedSubsystem interface with pluggable modules; the filesystem is the reference subsystem. A2ML is the attestation/audit markup. A verified Merkle tree carries a combiner-generic soundness theorem. Crypto is provided by a thin Zig FFI over std.crypto."""
+core = "ochrance-core (Idris2) — single source of proof truth"
+ffi = "ffi/zig (BLAKE3 / SHA-256 / SHA3-256 / Ed25519); thin C NVMe syscall shims (L1)"
+languages = "Idris2 (proofs), Zig (FFI), C (syscall shims), Rust + Julia (ECHIDNA, future)"
+
+[decisions]
+# architecture decisions on record (proof-side rationale in docs/PROOFS.adoc)
+records = [
+  "D1 — single core: ochrance-core is the source of truth; ochrance-framework's duplicate core is retired, its mode-indexed VerifiedSubsystem Interface harvested.",
+  "D2 — crypto binding as a typed interface: collision resistance modelled as an Idris hypothesis (CollisionResistant h); the binding theorem is discharged against it, not left as prose.",
+  "D3 — svalinn migrates ReScript → Ephapax before proof (migrate-then-prove).",
+  "Combiner generalization: Merkle construction/verification/soundness are parameterised over the hash combiner; XOR and BLAKE3 are instances of one universally-quantified theorem; cryptographic binding is the separate trust assumption.",
+]
+
+[practices]
+totality = "every module carries %default total; structural recursion only; no believe_me / assert_* / postulate / unsafePerformIO / holes on proof symbols"
+idris = "Idris2 0.8.0+"
+progressive-strictness = "verification supports Lax / Checked / Attested modes"
+error-taxonomy = "q/ query · p/ proof · z/ zone"
+ci = "type-check + totality gate, A2ML/property/integration/e2e suites, Zig FFI build+test, CodeQL, secret scans, RSR antipattern / SPDX / workflow linters"
+docs = "AsciiDoc (.adoc) except GitHub-required files; the proof campaign is tracked in docs/PROOFS.adoc"

.machine_readable/6a2/NEUROSYM.a2ml

@@ -3,12 +3,35 @@
 #
 # NEUROSYM.a2ml — Neurosymbolic integration metadata
 # Configuration for Hypatia scanning and symbolic reasoning.
-
 [metadata]
 version = "0.1.0"
-last-updated = "2026-03-16"
+last-updated = "2026-06-05"
 
 [hypatia-config]
 scan-enabled = true
 scan-depth = "standard"
 report-format = "logtalk"
+
+[symbolic]
+prover = "Idris2 (dependent types)"
+neural-backend = "ECHIDNA (Rust/Julia) — FFI stubbed, integration pending"
+abstraction = "idris2-echidna prover layer (planned 13th ECHIDNA backend)"
+
+[proof-obligations]
+# discharged — machine-checked, axiom-free
+discharged = [
+  "merkleCorrectWith — combiner-generic inclusion soundness",
+  "verifyProofReconstructsWith — verify ≡ root == reconstruct",
+  "roundtripManifest — grammar invertibility over the reference token codec",
+  "progressive assurance (SatisfiesMinimum / attestedSatisfiesLax)",
+]
+# open — see docs/PROOFS.adoc Stages 1–4
+open = [
+  "buildMerkleTree correctness + IO↔pure bridge to the production crypto path",
+  "CollisionResistant h + merkleBinding (D2)",
+  "Verify / Validator soundness; repair correctness (L3 linear); Merkle completeness",
+]
+
+[honest-bounds]
+# boundaries by design — documented, never faked
+notes = """The production parse∘lex∘serialize round-trip rests on primitive String operations (pack/unpack/parseInteger) with no equational theory; the honest guarantee is roundtripManifest over a reference token codec, complemented by a runtime round-trip property. The residual root==root Bool step in merkleCorrect is propositional digest equality — the strongest honest statement without an unsafe reflexivity axiom."""

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -2,22 +2,27 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # PLAYBOOK.a2ml — Operational playbook
-# Runbooks, incident response, deployment procedures.
-
+# Runbooks, build/verify procedures, incident response.
 [metadata]
 version = "0.1.0"
-last-updated = "2026-03-16"
+last-updated = "2026-06-05"
 
-[deployment]
-# method = "gitops"
-# target = "container"
+[build-and-verify]
+typecheck = "idris2 --build ochrance.ipkg   # must be clean and fully total"
+single-file = "idris2 --check ochrance-core/Ochrance/A2ML/Lexer.idr"
+ffi = "cd ffi/zig && zig build && zig build test   # BLAKE3 / SHA-256 / SHA3-256 / Ed25519 KATs (Zig 0.11.0)"
+suites = "A2ML parser, property, integration, and tests/e2e_test.sh"
 
 [incident-response]
-# 1. Check .machine_readable/STATE.a2ml for current status
-# 2. Review recent commits and CI results
-# 3. Run just validate to check compliance
+steps = [
+  "Check .machine_readable/6a2/STATE.a2ml for current status, blockers, and next actions",
+  "Review recent commits and CI results on main",
+  "Re-run the proof build (idris2 --build ochrance.ipkg) and the affected suite",
+]
 
 [release-process]
-# 1. Update version in STATE.a2ml, META.a2ml
-# 2. Run just quality (format, lint, test)
-# 3. Tag and push
+steps = [
+  "Update version + last-updated in STATE.a2ml and META.a2ml",
+  "Ensure CI is green (totality gate, suites, Zig FFI build+test, CodeQL, RSR linters)",
+  "Tag and push",
+]

.machine_readable/6a2/STATE.a2ml

@@ -1,14 +1,74 @@
 # SPDX-License-Identifier: MPL-2.0
-# STATE.a2ml — Project state checkpoint
-# Converted from STATE.scm on 2026-03-15
-
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# STATE.a2ml — Ochránce project state checkpoint
 [metadata]
 project = "ochrance"
 version = "0.1.0"
-last-updated = "2026-03-15"
+last-updated = "2026-06-05"
 status = "active"
+session = "machine-readable checkpoint — 2026-06-05"
 
 [project-context]
-name = "ochrance"
-completion-percentage = 0
-phase = "In development"
+name = "Ochránce"
+purpose = """Neurosymbolic filesystem verification framework in Idris2 dependent types: a pluggable VerifiedSubsystem interface, A2ML attestation/audit markup, a verified Merkle tree with a combiner-generic soundness theorem, and ECHIDNA integration."""
+completion-percentage = 40
+
+[position]
+phase = "implementation"   # design | implementation | testing | maintenance | archived
+maturity = "experimental"  # experimental | alpha | beta | production | lts
+
+[proven-surface]
+# machine-checked, axiom-free (no believe_me / assert_* / postulate / holes on proof symbols)
+theorems = [
+  "merkleCorrect / merkleCorrectWith — inclusion-proof soundness, generic over the hash combiner (XOR & BLAKE3 are instances)",
+  "verifyProofReconstructs(With) — verify ≡ (root == reconstruct leaf prf)",
+  "roundtripManifest (+ algoRT/modeRT/refsRT/mpolRT codecs) — decodeManifest (encodeManifest m) = Just m",
+  "SatisfiesMinimum / attestedSatisfiesLax — progressive-assurance threshold witness",
+  "ABI Handle / createHandle — So (ptr /= 0) non-null invariant",
+  "supporting lemmas: reconstructAppendWith, powerTwoSucc, justInj",
+]
+
+[route-to-mvp]
+# the proof campaign — docs/PROOFS.adoc is the authoritative, dependency-sorted plan
+milestones = [
+  "Stage 1 — Merkle closure (buildMerkleTree correctness, IO↔pure bridge) + crypto-binding interface (CollisionResistant)",
+  "Stage 2 — Verify + Validator soundness; hex codec round-trip",
+  "Stage 3 — Repair correctness (L3 linear types); harvest framework's mode-indexed Interface",
+  "Stage 4 — Merkle completeness, binding discharge, progressive monotonicity, write-up",
+]
+
+[blockers-and-issues]
+issues = [
+  "No cryptographic-integrity claim yet: Idris stub fallbacks (hashPairStub / blake3Stub / ed25519VerifyStub in FFI/Crypto.idr) remain in the verification flow; libochrance.so not yet built + linked in",
+  "Repair (L3) idempotence is property-tested only, not yet proven",
+  "ECHIDNA FFI is stubbed (echidnaProve returns 'FFI not yet implemented')",
+  "Production round-trip (parse∘lex∘serialize) is honestly bounded by primitive String ops — see docs/PROOFS.adoc",
+]
+
+[critical-next-actions]
+actions = [
+  "Stage 1 (Opus): buildMerkleTree index/root-fold laws; bridge verifyProofIO/rootHashBytesIO to the …With spec",
+  "Introduce CollisionResistant h + merkleBinding interface (D2)",
+  "Remove Idris-side crypto stubs and build + link libochrance.so into the flow (unblocks the crypto-integrity claim)",
+  "Sync .machine_readable scaffold to rsr-template (ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST, ENSAID_CONFIG, root README, root-allow) — pending template access",
+]
+
+[recent-history]
+# 2026-06-05 reconciliation: main is now the single trunk
+merged = [
+  "#31 — Zig crypto FFI (BLAKE3/SHA-256/SHA3-256/Ed25519) + zig-ffi.yml CI + Valence-Shell bridge docs",
+  "#32 — A2ML parser totality + correctness, Merkle combiner generalization, proof ledger, post-migration re-entry runbook",
+  "#33 — nixpkgs flake.lock bump",
+  "#34 — CodeQL cron weekly→monthly",
+]
+decisions = [
+  "D1 — converge on ochrance-core (ochrance-framework duplicate core retired; mode-indexed VerifiedSubsystem Interface harvested)",
+  "D2 — crypto binding modelled as a typed CollisionResistant hypothesis, discharged not asserted",
+  "D3 — svalinn migrates ReScript → Ephapax (migrate-then-prove)",
+]
+
+[maintenance-status]
+last-run-utc = "2026-06-05T14:08:00Z"
+last-result = "pass"  # unknown | pass | warn | fail
+notes = "CI green on main; core builds fully total. A2ML parser 16/16, property 47/47, e2e 22/22; integration suite and Zig FFI build+test green."

.machine_readable/anchors/ANCHOR.a2ml

@@ -16,3 +16,16 @@ ssg:
 # Relationships
 parents:
   - "org.hyperpolymath.boj-server"
+
+# Realignments — significant repository realignments on record
+realignments:
+  - date: "2026-06-05"
+    kind: "convergence + proof-campaign"
+    summary: >
+      Converged on ochrance-core as the single source of proof truth (D1);
+      retired the ochrance-framework duplicate core and harvested its
+      mode-indexed VerifiedSubsystem interface. Generalised Merkle
+      construction / verification / soundness over the hash combiner
+      (XOR and BLAKE3 as instances of one theorem). Implemented the Zig
+      crypto FFI. Reconciled all open branches into a single main.
+    authority: "docs/PROOFS.adoc"