hyperpolymath · Jul 2, 2026 · Jul 2, 2026
@@ -218,7 +218,9 @@ signature rejection.
 ### Idris2 Integration Tests
 
 ```bash
-idris2 --build tests/integration.ipkg
+idris2 --install ochrance.ipkg
+idris2 --build tests/integration/tests.ipkg
+./tests/integration/build/exec/integration-tests
 ```
 
 ## Contributing

@@ -29,7 +29,7 @@ Three components orchestrate this: A2ML parser/validator (parses filesystem mani
 
 **How verified**: The Merkle tree is defined as a size-indexed binary tree: `MerkleTree : (size : Nat) → Type`. At compile time, Idris2 verifies that all leaf nodes are at depth `log2(size)`. The tree operations (leaf insertion, hash computation, proof generation) take dependent proofs that structure is maintained. README (§Architecture) claims "Verified Merkle trees — Size-indexed binary trees with compile-time structure proofs." This is proven by the type signature itself: if you try to construct a tree of size 8 with only 7 leaves, the type checker rejects it because the dependent type `MerkleTree 8` requires exactly 8 leaves.
 
-**Caveat**: The size-indexed *structure* proofs are independent of hash strength. Real hashing now exists — the Zig FFI implements BLAKE3/SHA-256/SHA3-256 (`ffi/zig/src/main.zig`, with known-answer-vector tests) and the IO Merkle path calls `hashPairBlake3` — but a pure XOR combiner (`hashPairStub`) remains for totality/offline testing, and `libochrance.so` must be built and linked for the cryptographic path to be live. Until the stub paths are removed and the FFI is wired into the verification flow, the structure proofs hold but cryptographic integrity is not yet claimed.
+**Caveat**: The size-indexed *structure* proofs are independent of hash strength. The cryptographic path is live: the Zig FFI implements BLAKE3/SHA-256/SHA3-256 (`ffi/zig/src/main.zig`, known-answer-vector tested), `build.zig` emits `libochrance.so`, and the IO Merkle path calls `hashPairBlake3` across `%foreign` — confirmed end to end by `tests/ffi/CryptoFFITest.idr` (the production root is the BLAKE3 fold, not the XOR spec root) and CI-gated in the `Idris2` and `Zig FFI` workflows. The pure XOR combiner (`xorCombiner`) is the totality-friendly *spec instance* of the combiner-generic theorems, not a fallback. The irreducible crypto assumption is `CollisionResistant`, isolated in `Filesystem.MerkleAssumption`.
 
 == Dogfooded Across The Account
 
@@ -60,12 +60,12 @@ Also integrates with ECHIDNA for neural proof synthesis — FFI calls to libechi
 
 == Testing Critical Paths
 
-* **Lexer totality**: `idris2 --check ochrance-core/A2ML/Lexer.idr` — Idris2 type checker verifies structurally recursive, no partial functions
-* **Parser totality**: `idris2 --check ochrance-core/A2ML/Parser.idr` — sized types ensure termination proof
-* **Validator**: `tests/validator_test.idr` — roundtrip A2ML → AST → A2ML preserves structure
-* **Merkle tree**: `tests/merkle_test.idr` — size-indexed tree construction and hash verification
-* **Repair linearity**: `tests/repair_test.idr` — linear type system prevents use-after-repair bugs (compile-time error if violated)
-* **ECHIDNA FFI**: `tests/echidna_ffi_test.idr` — call libechidna.so via Zig FFI, verify proof synthesis works
+* **Lexer/Parser totality**: `idris2 --build ochrance.ipkg` (opts `--total`) — every core module, including the lexer's structural recursion and the parser's sized-type termination, type-checks under the totality checker; CI-gated by the `Idris2` workflow
+* **Parser/roundtrip**: `tests/A2ML/ParserTests.idr` — lex/parse/serialize roundtrip and error handling (fail-capable, CI-gated)
+* **Properties**: `tests/property/PropertyTests.idr` — 47 property checks across hex roundtrip, Merkle, repair idempotence, and validation (incl. policy rejection cases)
+* **Integration**: `tests/integration/IntegrationTests.idr` — manifest generation → validation → verification → repair scenarios
+* **Crypto FFI runtime**: `tests/ffi/CryptoFFITest.idr` (via `tests/ffi/run_ffi_test.sh`) — real BLAKE3/SHA-256/SHA3-256 across `%foreign` into `libochrance.so`; proves the production Merkle root ≠ XOR spec root
+* **ECHIDNA FFI**: not yet testable — `Ochrance.FFI.Echidna` is a design stub (`Left "FFI not yet implemented"`); see ROADMAP Phase 2
 
 == Known Limitations & TODOs
 

@@ -22,11 +22,16 @@ v0.1.0, 2026-02-06
 
 Formal verification is **in progress** — see link:docs/PROOFS.adoc[`docs/PROOFS.adoc`]
 for the authoritative, dependency-sorted plan and the currently-proven surface
-(combiner-generic Merkle soundness, A2ML parser totality, manifest round-trip,
-progressive assurance). *Cryptographic integrity is not yet claimed*: the real
-BLAKE3 / SHA-256 / SHA3-256 / Ed25519 lives in the Zig FFI, but the Idris-side
-stub fallbacks must be removed and `libochrance.so` linked into the verification
-flow first (issue #39).
+(combiner-generic Merkle soundness + binding, verify/validator soundness with
+policy enforcement, repair correctness, A2ML parser totality, manifest
+round-trip, progressive assurance). The real BLAKE3 / SHA-256 / SHA3-256 /
+Ed25519 lives in the Zig FFI (`libochrance.so`), is wired into the Idris
+production path via `%foreign`, and is CI-verified end to end: the `Idris2`
+workflow builds every proof module under `--total` and runs the Idris→Zig
+runtime test on each PR. Named residual boundaries, not hidden: the
+`CollisionResistant` hypothesis (isolated in `Filesystem.MerkleAssumption`),
+the ABI-layer `blake3Hash` placeholder (`src/abi/`, issue #39), and the
+attestation trust-root / key-management story.
 
 == Architecture
 

@@ -8,44 +8,51 @@ v0.1.0, 2026-02-07
 
 == Current Status
 
-**Phase 1: Ochránce Core** (54% complete - In Progress)
-
-The A2ML parsing pipeline is fully functional with total lexer and covering parser. Type-safe framework with q/p/z error taxonomy is complete. Current focus: completing validator, serializer, and Merkle tree implementation.
+**Phase 1: Ochránce Core** — 10/11 components complete (updated 2026-07-02)
+
+The proof program's Stages 1–3 are machine-checked and CI-enforced: the
+`Idris2` workflow builds every core module under `--total` on each PR, and
+the Idris→Zig FFI runtime test proves the production Merkle path computes
+real BLAKE3 across the `%foreign` boundary. The validator enforces policy
+(require_sig, max_age freshness) with soundness theorems. Ledger of record:
+`docs/PROOFS.adoc`. Remaining engineering: filling in the placeholder
+integration scenarios, canonical signing serialization, and the Stage 4
+proofs (Merkle completeness, progressive monotonicity, VerifiedSubsystem
+law).
 
 == Development Phases
 
 === Phase 1: Ochránce Core (v0.1.0) - **In Progress**
 
 Target: Complete core verification framework with full A2ML support
 
-**Completion: 54%**
+**Completion: 10/11 components**
 
 Components:
 
 * [x] A2ML Lexer (total, tested)
 * [x] A2ML Parser (total, tested)
-* [ ] A2ML Validator (comprehensive signature verification)
-* [ ] A2ML Serializer (roundtrip: Manifest ↔ String)
+* [x] A2ML Validator (structural + policy enforcement proven sound; Ed25519 signature verification via FFI; residual: canonical signing serialization, positive-path signature KAT, trust-root story)
+* [x] A2ML Serializer (roundtrip proven for the reference token codec; production pipeline runtime-checked — the String-primitive wall, see PROOFS.adoc)
 * [x] Framework Interface (VerifiedSubsystem)
 * [x] Proof Witnesses (Lax/Checked/Attested modes)
 * [x] Error Taxonomy (q/p/z classification)
-* [ ] Merkle Tree Implementation (size-indexed; BLAKE3 FFI now implemented in Zig — build/link wiring still pending)
-* [ ] Filesystem Verification (VerifiedSubsystem instance)
-* [ ] Linear Type Repair (consume-old-state semantics)
-* [ ] Integration Tests (50+ scenarios)
+* [x] Merkle Tree Implementation (size-indexed; real BLAKE3 via libochrance.so, CI-gated end to end; residual assumption: CollisionResistant, isolated)
+* [x] Filesystem Verification (verify soundness proven — Stages 2.2/2.4; residual: proof-token constructor visibility)
+* [x] Linear Type Repair (repair correctness proven — Stages 3.1/3.2; impl models hashes only, no block I/O; full linearity deferred, see PROOFS.adoc)
+* [ ] Integration Tests (10 real scenarios green + fail-capable and CI-gated; 45 remaining placeholders to fill)
 
 **Critical Next Actions:**
 
-1. Complete A2ML Validator (signature verification via FFI)
-2. Implement A2ML Serializer (roundtrip verification)
-3. Wire the implemented Zig BLAKE3 FFI into Merkle and remove the XOR stub combiner
-4. Implement Filesystem.Verify module
-5. Implement Filesystem.Repair with linear types (Quantity 1)
+1. Canonical signing serialization (delimited, all-fields-bound) + positive-path Ed25519 known-answer test through validateManifestIO
+2. Stage 4 proofs: Merkle completeness (4.1), remaining SatisfiesMinimum monotonicity cases (4.3), VerifiedSubsystem law stated + proven for FSState
+3. Fill in the 45 placeholder integration scenarios
+4. Make real BLAKE3 reachable from a root-verify entry point (IO path via the proven IO↔pure bridge; VerifyRoot currently requires a pure Combiner)
+5. Require the Idris2 / Zig FFI checks in the repo ruleset (currently no required status checks — auto-merge lands before CI finishes)
 
 **Blockers:**
 
-* Idris2 0.8.0+ compiler required
-* `libochrance.so` (Zig crypto FFI) must be built and linked into the Idris2 verification flow; the primitives themselves (BLAKE3/SHA-256/SHA3-256/Ed25519) are now implemented and tested
+* None for the components above. Named boundaries: CollisionResistant hypothesis (isolated); ABI-layer blake3Hash placeholder + ECHIDNA FFI stub (issue #39, Phase 2 scope); attestation trust-root / key management (design decision needed)
 
 === Phase 2: ECHIDNA Integration (v0.2.0) - **Planned**
 

@@ -3,7 +3,7 @@ SPDX-License-Identifier: CC-BY-SA-4.0
 Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 <!-- TOPOLOGY.md — Project architecture map and completion dashboard -->
-<!-- Last updated: 2026-06-17 -->
+<!-- Last updated: 2026-07-02 -->
 
 # Ochránce — Project Topology
 
@@ -65,25 +65,42 @@ COMPONENT                            STATUS         NOTES (proof / verification
 ───────────────────────────────────  ──────────────  ────────────────────────────────────────────
 CORE VERIFICATION (IDRIS2)
   Merkle soundness + round-trip       ███████░░░ 70%  merkleCorrect(With) + buildGetLeaf proven
-  Merkle completeness + binding       ░░░░░░░░░░  0%  converse + CollisionResistant (Stage 1.4/4)
+  Merkle completeness + binding       █████░░░░░ 50%  binding DONE (merkleBinding; CR isolated in
+                                                      MerkleAssumption); completeness converse open (4.1)
   A2ML parser + reference round-trip  ███████░░░ 70%  total; ref-codec proven; prod pipeline runtime-only
-  Verify soundness                    ░░░░░░░░░░  0%  verify success ⇏ a proof yet (Stage 2)
-  Linear-type Repair                  ██░░░░░░░░ 20%  IMPL IS A STUB (no block I/O); unproven (Stage 3)
-  VerifiedSubsystem law               █████░░░░░ 50%  interface + FSState instance; law unproven (Stage 3)
-  Progressive assurance               ███████░░░ 70%  attestedSatisfiesLax proven; monotonicity (Stage 4)
+  Verify soundness                    ████████░░ 80%  Stages 2.1–2.4 proven (verifyRefsSound,
+                                                      merkleRootVerifyHashSound mod CR+DecodeInjective);
+                                                      residual: proof-token constructor visibility
+  Validator + policy enforcement      ████████░░ 80%  validateManifestSound (4-tuple incl. policy);
+                                                      require_sig/max_age proven enforced; residual:
+                                                      canonical signing serialization + positive KAT
+  Linear-type Repair                  ██████░░░░ 60%  Stages 3.1/3.2 proven (mod GoodRefs+hashRefl);
+                                                      impl hash-map-only, no block I/O; linearity deferred
+  VerifiedSubsystem law               █████░░░░░ 50%  interface + FSState instance; law not yet STATED
+                                                      in Interface.idr (repairThenVerify proven at
+                                                      pure-core level, not lifted)
+  Progressive assurance               ███████░░░ 70%  attestedSatisfiesLax proven; monotonicity (Stage 4.3)
 
 SYSTEM & EXTERNAL
-  Zig crypto (BLAKE3/SHA/Ed25519)     ███████░░░ 70%  implemented + known-answer-vector tested in Zig
-  Crypto linked into verify flow      ██░░░░░░░░ 20%  NOT linked; Idris-side stubs still live (#39)
+  Zig crypto (BLAKE3/SHA/Ed25519)     █████████░ 90%  implemented + KAT-tested; Zig 0.15.2; 24 tests
+                                                      (unit + linked C-ABI integration) CI-gated
+  Crypto linked into verify flow      ███████░░░ 70%  libochrance.so built+linked+CI-gated end to end
+                                                      (Idris2 workflow runs run_ffi_test.sh per PR);
+                                                      residual: root-verify entry needs pure Combiner
+                                                      (IO path open), ABI blake3Hash placeholder (#39)
   ECHIDNA integration                 █░░░░░░░░░ 10%  design types only; FFI entirely stubbed
 
 REPO INFRASTRUCTURE
   Justfile automation                 ██████████ 100% build / verify tasks
-  .machine_readable/                  ██████████ 100% STATE tracking active
-  Idris2 .ipkg / totality gate        ██████████ 100% 19 core modules; --total build green
+  .machine_readable/                  ██████████ 100% STATE tracking active; descriptiles (post-6a2)
+  Idris2 .ipkg / totality gate        ██████████ 100% 29 core modules; --total build green
+  CI proof gate (Idris2 workflow)     ██████████ 100% every PR: full --total build + 3 fail-capable
+                                                      suites + Idris→Zig FFI runtime test
 
 ────────────────────────────────────────────────────────────────────────────────────────────────
-OVERALL (proof axis):                 ████░░░░░░ ~40% Stage 1.1 done; 1.2–4 open. See docs/PROOFS.adoc.
+OVERALL (proof axis):                 ███████░░░ ~70% Stages 1–3 done (mod named hypotheses);
+                                                      Stage 4 open: Merkle completeness, monotonicity
+                                                      cases, VerifiedSubsystem law. See docs/PROOFS.adoc.
 ```
 
 ## Key Dependencies

@@ -4,6 +4,7 @@
 
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 This is the authoritative, dependency-sorted plan for driving the formal
 verification of the Ochránce estate to completion. It is the durable source of
@@ -213,6 +214,32 @@ only `map id y` (functor-identity *law*, not definitional) — so invert by casi
 on the head outcome *and* the tail fold, keeping each step definitional; (ii) `with`
 abstracts only a hypothesis's WHNF, so case on `validateRef ref` (exposed there),
 not the nested `isValidHexString`.
++
+EXTENDED (2026-07-02): policy enforcement is now part of the proven surface.
+`validatePolicy` — previously dead code in the production path (a manifest with
+`require_sig = true` and no attestation *passed*) — is wired into
+`validateManifest`, and `validateManifestSound` is a 4-tuple: acceptance also
+forces `validatePolicy m = Right ()`. New theorems, all machine-checked,
+axiom-free: `requireSigNoAttestationRejected` (the gate is provably wired in);
+`staleManifestRejected` (end-to-end: `validatePolicyAt` rejects a manifest
+older than `max_age` — proved by rewriting the goal along the
+`parseTimestamp ts = Just issued` hypothesis, which unblocks both stuck case
+scrutinees at once; the `with`-abstraction route fails here because `with`
+cannot rewrite an already-fixed hypothesis); `checkFreshnessRejectsStale` /
+`checkFreshnessAcceptsFresh`; `hexAcceptSound` (strengthened check: exactly 64
+hex chars AND hex-only content — the old check accepted `'.'`, empty and
+any-length strings) + `hexWrongLengthRejected` + `hexEmptyRejected`; and
+known-answer proofs for the total ISO-8601-subset `parseTimestamp` (epoch = 0,
+modern date cross-checked, garbage and month-13 rejected). Freshness is
+clock-free in the pure layer (`validatePolicyAt` takes `now`;
+`validateManifestIO` fetches `System.time`) — IO↔pure-bridge style.
++
+CI-ENFORCED (2026-07-01): the entire ledger is now gated per PR — the `Idris2`
+workflow builds every core module under `--total` (a broken proof is a red
+check) and runs the Idris→Zig FFI runtime test (`tests/ffi/run_ffi_test.sh`),
+so the production-Merkle-root-is-real-BLAKE3 fact is re-verified on every
+change. The three Idris test suites are fail-capable (exit 1) as of the same
+change.
 
 . *[DONE — 2.2 (inversion); merkle-wiring deferred]* `verify` soundness. Lifted
   `verifyRefsHelper` / `parseBlockIdx` out of the instance `where` to top-level

@@ -69,5 +69,5 @@ main = do
   putStrLn "  • A2ML (Types/Lexer/Validator):  ✓"
   putStrLn "  • Framework (Interface/Proofs):  ✓"  
   putStrLn "  • Filesystem (Types/Merkle):     ✓"
-  putStrLn "  • FFI Crypto (stubbed):          ✓"
+  putStrLn "  • FFI Crypto (real, via libochrance): ✓"
   putStrLn ""