A2ML parser totality + correctness, Merkle combiner generalization, proof ledger (#32)

Parser made total by structural recursion (zero covering), inverted-unless and end-of-input bugs fixed; Merkle construction/verification/soundness generalized over the hash combiner (merkleCorrectWith); repo hygiene (untrack build artifacts); proof-campaign ledger (PROOFS.adoc) and post-migration re-entry runbook (AFTER-MIGRATION.adoc). FFI/e2e reconciled to main's #31 implementations.

Author: hyperpolymath

.github/workflows/echidna-validation.yml

@@ -31,17 +31,26 @@ jobs:
 
       - name: Dangerous pattern scan (Idris2)
         run: |
-          echo "=== Idris2 Dangerous Pattern Scan ==="
+          echo "=== Idris2 Dangerous Pattern Scan (code only; comments excluded) ==="
           ISSUES=0
           for pattern in "believe_me" "assert_total" "assert_smaller" "unsafePerformIO"; do
-            FOUND=$(grep -rn "$pattern" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null | wc -l || echo 0)
-            if [ "$FOUND" -gt 0 ]; then
-              echo "CRITICAL: Found $FOUND instances of '$pattern'"
-              grep -rn "$pattern" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null
-              ISSUES=$((ISSUES + FOUND))
+            # Strip doc comments (||| ...) and line comments (-- ...) before
+            # matching, so documentation that merely names a pattern is not
+            # flagged: only genuine uses in code count. Without this, a doc
+            # string like "this proof needs no assert_smaller" would fail the gate.
+            MATCHES=""
+            for f in $(find ochrance-core/ src/abi/ -name "*.idr" 2>/dev/null); do
+              M=$(sed -e 's/|||.*$//' -e 's/--.*$//' "$f" | grep -n "$pattern" | sed "s|^|$f:|" || true)
+              [ -n "$M" ] && MATCHES="${MATCHES}${M}"$'\n'
+            done
+            N=$(printf '%s' "$MATCHES" | grep -c . || true)
+            if [ "$N" -gt 0 ]; then
+              echo "CRITICAL: Found $N use(s) of '$pattern' in code:"
+              printf '%s\n' "$MATCHES"
+              ISSUES=$((ISSUES + N))
             fi
           done
-          echo "Total dangerous patterns: $ISSUES"
+          echo "Total dangerous patterns (in code): $ISSUES"
           echo "dangerous_count=$ISSUES" >> $GITHUB_OUTPUT
 
           if [ "$ISSUES" -gt 0 ]; then
@@ -53,7 +62,7 @@ jobs:
         run: |
           echo "=== Totality Enforcement ==="
           MISSING=0
-          for f in $(find ochrance-core/ modules/ src/abi/ -name "*.idr" 2>/dev/null); do
+          for f in $(find ochrance-core/ src/abi/ -name "*.idr" 2>/dev/null); do
             if ! grep -q "%default total" "$f"; then
               echo "WARNING: $f missing '%default total'"
               MISSING=$((MISSING + 1))
@@ -67,11 +76,11 @@ jobs:
       - name: Partial function check
         run: |
           echo "=== Partial Function Check ==="
-          PARTIAL=$(grep -rn "^partial" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null | wc -l || echo 0)
+          PARTIAL=$(grep -rn "^partial" ochrance-core/ src/abi/ --include="*.idr" 2>/dev/null | wc -l || echo 0)
           echo "Explicitly partial functions: $PARTIAL"
           if [ "$PARTIAL" -gt 0 ]; then
             echo "Review required:"
-            grep -rn "^partial" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null
+            grep -rn "^partial" ochrance-core/ src/abi/ --include="*.idr" 2>/dev/null
           fi
 
       - name: FFI stub status
@@ -100,7 +109,7 @@ jobs:
         run: |
           echo "## ECHIDNA Validation Results" >> $GITHUB_STEP_SUMMARY
           echo "" >> $GITHUB_STEP_SUMMARY
-          echo "- Scanned: ochrance-core/, modules/, src/abi/, ffi/zig/" >> $GITHUB_STEP_SUMMARY
+          echo "- Scanned: ochrance-core/, src/abi/, ffi/zig/" >> $GITHUB_STEP_SUMMARY
           echo "- Checks: dangerous patterns (believe_me etc), totality enforcement, partial functions, FFI stub status, Zig safety" >> $GITHUB_STEP_SUMMARY
           echo "" >> $GITHUB_STEP_SUMMARY
           echo "*Powered by ECHIDNA neurosymbolic verification*" >> $GITHUB_STEP_SUMMARY

.gitignore

@@ -80,6 +80,7 @@ htmlcov/
 
 # Zig
 **/zig-out/
+**/zig-cache/
 **/.zig-cache/
 **/zig-cache/
 

ABI-FFI-README.md

@@ -185,9 +185,8 @@ zig build test                    # Run Zig unit tests
 # Ensure libochrance.so is on LD_LIBRARY_PATH
 export LD_LIBRARY_PATH="$PWD/ffi/zig/zig-out/lib:$LD_LIBRARY_PATH"
 
-# Type-check and build
+# Type-check and build (the core package includes the filesystem subsystem)
 idris2 --build ochrance.ipkg
-idris2 --build ochrance-fs.ipkg
 ```
 
 ### Cross-Compile

CLAUDE.md

@@ -21,30 +21,26 @@ ochrance/
 │   │   ├── Interface.idr    # VerifiedSubsystem interface
 │   │   ├── Proof.idr        # Proof witnesses
 │   │   └── Error.idr        # q/p/z error taxonomy
+│   ├── Filesystem/          # Reference VerifiedSubsystem
+│   │   ├── Types.idr        # FSState, Block, FSSnapshot
+│   │   ├── Merkle.idr       # Verified Merkle tree + merkleCorrect theorem
+│   │   ├── Verify.idr       # Verification logic
+│   │   └── Repair.idr       # Linear type repair
 │   └── FFI/
+│       ├── Crypto.idr       # FFI to libochrance.so (BLAKE3/SHA-256/Ed25519)
 │       └── Echidna.idr      # FFI to libechidna.so
-├── modules/
-│   └── filesystem/          # Reference VerifiedSubsystem
-│       ├── Types.idr        # FSState, Block, FSSnapshot
-│       ├── Merkle.idr       # Verified Merkle tree
-│       ├── Verify.idr       # Verification logic
-│       └── Repair.idr       # Linear type repair
 ├── tests/                   # Test suite
-├── ochrance.ipkg            # Core package
-└── ochrance-fs.ipkg         # Filesystem module package
+└── ochrance.ipkg            # Core package (includes the filesystem subsystem)
 ```
 
 ## Build Commands
 
 ```bash
-# Type-check core
+# Type-check core (includes the filesystem subsystem)
 idris2 --build ochrance.ipkg
 
-# Type-check filesystem module
-idris2 --build ochrance-fs.ipkg
-
 # Check single file
-idris2 --check ochrance-core/A2ML/Lexer.idr
+idris2 --check ochrance-core/Ochrance/A2ML/Lexer.idr
 
 # REPL
 idris2 --repl ochrance.ipkg

EXPLAINME.adoc

@@ -50,12 +50,11 @@ Also integrates with ECHIDNA for neural proof synthesis — FFI calls to libechi
 | `ochrance-core/Framework/Proof.idr` | Proof witness types; generic proof structure for all subsystems
 | `ochrance-core/Framework/Error.idr` | Error taxonomy: q/* (query), p/* (proof), z/* (zone/system)
 | `ochrance-core/Framework/FFI/Echidna.idr` | FFI to ECHIDNA neural prover (via Zig C ABI)
-| `modules/filesystem/Types.idr` | Filesystem types: FSState, Block, FSSnapshot with dependent proofs
-| `modules/filesystem/Merkle.idr` | Verified Merkle tree: size-indexed with compile-time structure proofs (placeholder XOR hashes)
-| `modules/filesystem/Verify.idr` | Verification logic: block hashes, tree integrity, attestation signatures
-| `modules/filesystem/Repair.idr` | Linear type repair: repair operations consume old state (Quantity 1)
-| `ochrance.ipkg` | Package definition for core library
-| `ochrance-fs.ipkg` | Package definition for filesystem module
+| `ochrance-core/Ochrance/Filesystem/Types.idr` | Filesystem types: FSState, Block, FSSnapshot with dependent proofs
+| `ochrance-core/Ochrance/Filesystem/Merkle.idr` | Verified Merkle tree: height-indexed with compile-time structure proofs and the `merkleCorrect` inclusion-soundness theorem (placeholder XOR hashes for the pure path)
+| `ochrance-core/Ochrance/Filesystem/Verify.idr` | Verification logic: block hashes, tree integrity, attestation signatures
+| `ochrance-core/Ochrance/Filesystem/Repair.idr` | Linear type repair: repair operations consume old state (Quantity 1)
+| `ochrance.ipkg` | Package definition for the core library (includes the filesystem subsystem)
 |===
 
 == Testing Critical Paths

Justfile

@@ -24,10 +24,6 @@ check-versions:
 build-core:
     idris2 --build ochrance.ipkg
 
-# Build filesystem module
-build-fs:
-    idris2 --build ochrance-fs.ipkg
-
 # Build ABI layer
 build-abi:
     idris2 --build ochrance-abi.ipkg
@@ -37,12 +33,11 @@ build-ffi:
     cd ffi/zig && zig build
 
 # Build all components
-build: build-core build-fs build-abi build-ffi
+build: build-core build-abi build-ffi
 
 # Run all tests (builds core, installs, then runs test suites)
 test: build-core
     idris2 --install ochrance.ipkg
-    idris2 --install ochrance-fs.ipkg
     idris2 --build tests/A2ML/tests.ipkg
     tests/A2ML/build/exec/a2ml-tests
     idris2 --build tests/property/tests.ipkg
@@ -59,7 +54,6 @@ test-a2ml: build-core
 # Run integration tests only
 test-integration: build-core
     idris2 --install ochrance.ipkg
-    idris2 --install ochrance-fs.ipkg
     idris2 --build tests/integration/tests.ipkg
     tests/integration/build/exec/integration-tests
 
@@ -89,18 +83,13 @@ check FILE:
 repl:
     idris2 --repl ochrance.ipkg
 
-# Open REPL for filesystem module
-repl-fs:
-    idris2 --repl ochrance-fs.ipkg
-
 # Find type at position in file
 type-at FILE LINE COL:
     idris2 --find-type-at {{FILE}}:{{LINE}}:{{COL}}
 
 # Install packages
 install:
     idris2 --install ochrance.ipkg
-    idris2 --install ochrance-fs.ipkg
     idris2 --install ochrance-abi.ipkg
 
 # Install OSTree hooks
@@ -126,11 +115,11 @@ format:
 stats:
     @echo "=== Ochránce Statistics ==="
     @echo "Idris2 modules:"
-    @find ochrance-core modules -name "*.idr" | wc -l
+    @find ochrance-core -name "*.idr" | wc -l
     @echo "Total lines of code:"
-    @find ochrance-core modules -name "*.idr" -exec cat {} \; | wc -l
+    @find ochrance-core -name "*.idr" -exec cat {} \; | wc -l
     @echo "Functions marked total:"
-    @grep -r 'total' ochrance-core modules | grep -v '%default' | wc -l
+    @grep -r 'total' ochrance-core | grep -v '%default' | wc -l
 
 # Run panic-attacker pre-commit scan
 assail:

docs/AFTER-MIGRATION.adoc

@@ -0,0 +1,83 @@
+= Ochránce — Re-entry After the svalinn → Ephapax Migration
+:toc: macro
+:sectnums:
+
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+
+This is the *round-trip closure* for the svalinn migration that was disposed from
+the proof campaign (`docs/PROOFS.adoc`, Decision *D3*; outbound charter at
+`svalinn/docs/ephapax-migration/HANDOFF.adoc`). Read it when the migration
+excursion *returns*, before resuming the proof program. It exists so the loop
+"delegate → migrate → come back" closes cleanly even after this thread is gone.
+
+toc::[]
+
+== The loop
+
+----
+proof thread (here)
+  └─ dispose svalinn migration  →  HANDOFF.adoc  →  [svalinn + ephapax session]
+        runs the spike, then the map, then the port (its own draft PRs)
+  ←─ return here  →  read THIS doc  →  reconcile  →  resume PROOFS.adoc
+----
+
+You are at the *return* step.
+
+== Reachability first (so you don't hit a 404)
+
+The migration's outputs live in the *svalinn* repo, not here. To do the
+reconciliation below you need *either* `hyperpolymath/svalinn` in this session's
+scope, *or* the delegated session to paste you its spike verdict. The proof
+campaign itself only needs `ochrance`.
+
+== Step 1 — Read the spike verdict (the gate)
+
+The migration was *gated* on a readiness spike (can Ephapax host an HTTP gateway
+today?). Its result is the capability matrix in
+`svalinn/docs/ephapax-migration/BLOCKER-LINEAGE.adoc`. Branch on it:
+
+[cols="1,4",options="header"]
+|===
+| Verdict | What it means / what you do
+
+| *GREEN* — Ephapax viable
+| The migration proceeded. Go to Step 2.
+
+| *RED* — a MUST-have absent, *D3 invalidated*
+| svalinn's language decision is *reopened*. Do *not* resume svalinn proofs.
+  Update `PROOFS.adoc` D3 with the new decision (stay ReScript + prove /
+  AffineScript / wait on Ephapax), then treat svalinn as a fresh disposed track.
+|===
+
+== Step 2 — Reconcile (green path)
+
+Fold the migration's results back into the campaign. Checklist:
+
+* [ ] `BLOCKER-LINEAGE.adoc` exists and its ring-0 critical chain was executed.
+* [ ] *Zero* `Obj.magic` in svalinn `src/` (the 20+ casts are gone
+  *structurally*, not patched).
+* [ ] JWT/JTI revocation is true-by-construction → svalinn *issue #13* is
+  dischargeable: verify and close it.
+* [ ] The *Ephapax* test suite runs *green* in CI (the pre-existing ReScript red
+  is gone because the ReScript is gone — not because it was fixed).
+* [ ] svalinn *PR #32* (the AffineScript language-policy PR) was reconciled to
+  Ephapax or closed; the `.claude/CLAUDE.md` language table was updated.
+* [ ] `PROOFS.adoc` updated: tick the svalinn disposed track; *promote* its
+  post-migration specs (Appendix E of the charter) into the proof program — now
+  the language is final, they are provable.
+
+== Step 3 — Resume the proof campaign
+
+Return to `docs/PROOFS.adoc` and continue at the stage you left (Stage 1 on Opus
+if you came straight back). The svalinn specs become a *sibling track* once
+Ephapax is the language; prove them via the route the spike established —
+Ephapax's own linear types, the Idris ABI layer (`svalinn/src/abi/*.idr`), or
+SPARK (`svalinn/docs/cerro-torre-integration.adoc` §6.2).
+
+== Cross-references
+
+* `docs/PROOFS.adoc` — the proof-campaign ledger (Decision D3, disposed tracks).
+* `svalinn/docs/ephapax-migration/HANDOFF.adoc` — the outbound charter.
+* `svalinn/docs/ephapax-migration/BLOCKER-LINEAGE.adoc` — the migration's own
+  output (spike verdict + critical chain), produced by the delegated session.