docs: ochrance optional checkpoint items — clade, debt, coverage, EXPLAINME (#37)

ANCHOR clade=fv; populate agent_instructions/debt.a2ml with carried debt; refresh coverage.a2ml; strip leaked /var/mnt/eclipse paths and fix Merkle path in EXPLAINME.adoc.

Author: hyperpolymath

.machine_readable/agent_instructions/coverage.a2ml

@@ -2,60 +2,30 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # coverage.a2ml — Session coverage tracking
-# Updated at the end of each AI agent session.
-# Persists what was visited, what was skipped, and what has MUSTs.
-#
-# Reference: ADR-002 in standards/agentic-a2ml/docs/
+# Updated at the end of each AI agent session: what was visited, skipped, and
+# which components have known MUSTs. Reference: ADR-002 in standards/agentic-a2ml/docs/
 
 [metadata]
-version = "1.0.0"
-last-updated = "2026-03-24"
-
-# ============================================================================
-# COVERAGE STATE
-# ============================================================================
-# Updated by agents at session end. Tracks which components have been
-# visited and which have known MUSTs that were skipped.
+version = "1.1.0"
+last-updated = "2026-06-05"
 
 [coverage]
+# The proof-campaign coverage is tracked authoritatively in docs/PROOFS.adoc
+# (Stage 0 done; Stages 1–4 open). This file tracks agent-session visits.
 total-components = 0
 visited-components = 0
 coverage-percent = 0
+authoritative-campaign-state = "docs/PROOFS.adoc"
 
-# ============================================================================
-# VISITED COMPONENTS
-# ============================================================================
-# Component → session date + ring reached
-# Agents add entries as they work through components.
-#
-# Example:
-# [coverage.visited.emergency-room]
-# date = "2026-03-23"
-# ring = 2
-# fixes = 3
-# notes = "boot-guardian built, shutdown-marshal built"
+[coverage.visited.proof-campaign-stage-0]
+date = "2026-06-05"
+ring = 0
+notes = "Parser totality + Merkle combiner generalization + manifest round-trip + progressive assurance landed (PR #32). See docs/PROOFS.adoc."
 
-# ============================================================================
-# SKIPPED COMPONENTS WITH MUSTS
-# ============================================================================
-# Components with known MUSTs that were not visited in the most recent session.
-# These become P1 inputs for the next session's Phase 0.
-#
-# Example:
-# [coverage.skipped-musts.session-sentinel]
-# priority = "P0"
-# issue = "56 SIGABRTs in 4 days, D-Bus race condition"
-# discovered = "2026-03-23"
+[coverage.visited.machine-readable-checkpoint]
+date = "2026-06-05"
+ring = 1
+fixes = 7
+notes = "Refreshed 6a2 (all six) + ANCHOR from the March .scm stubs; recorded D1/D2/D3, proven surface, honest bounds, runbooks; reconciled all open branches into one main."
 
-# ============================================================================
-# CHERRY-PICKING AUDIT
-# ============================================================================
-# At session end, agents report whether they chose easy work over hard work.
-# This is the accountability mechanism for the weighted priority system.
-#
-# [coverage.cherry-picking]
-# easy-high-completed = 3
-# hard-high-completed = 1
-# easy-low-completed = 2
-# hard-low-deferred = 4
-# assessment = "Correctly prioritised — all MUST items addressed before COULDs"
+# Skipped MUSTs / cherry-picking audit: none recorded this session.

.machine_readable/agent_instructions/debt.a2ml

@@ -2,48 +2,61 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # debt.a2ml — Meander debt list
-# Things found but not fixed. Carried between sessions.
-# Becomes the next session's Phase 0 input.
-#
+# Things found but not fixed. Carried between sessions; becomes the next
+# session's Phase 0 input. Items are consumed (removed) when fixed.
+# Each item: component, issue, effort (easy|medium|hard), impact (high|medium|low), discovered.
 # Reference: ADR-002 in standards/agentic-a2ml/docs/
 
 [metadata]
-version = "1.0.0"
-last-updated = "2026-03-24"
-
-# ============================================================================
-# DEBT ITEMS
-# ============================================================================
-# Each item has: component, issue, effort (easy|medium|hard), impact (high|medium|low),
-# priority (should|could), and discovered date.
-#
-# Items are consumed (removed) when fixed. New items are added at session end.
-# The debt list prevents the "one more wave" loop — found things are persisted,
-# not forgotten, and not used as justification for infinite meandering.
+version = "1.1.0"
+last-updated = "2026-06-05"
 
 # ============================================================================
 # SHOULD — would fix next wave
 # ============================================================================
-# These are inputs for the next session if the user says "keep going".
-#
-# Example:
-# [[debt.should]]
-# component = "system-tools/monitoring/observatory"
-# issue = "Stale duplicate of root observatory/"
-# effort = "easy"
-# impact = "medium"
-# discovered = "2026-03-23"
+
+[[debt.should]]
+component = "ochrance-core/Ochrance/FFI/Crypto.idr"
+issue = "Idris stub fallbacks (hashPairStub / blake3Stub / ed25519VerifyStub) remain in the verification flow and libochrance.so is not yet built+linked — so no cryptographic-integrity claim can be made (CLAUDE.md rule 4)."
+effort = "hard"
+impact = "high"
+discovered = "2026-06-05"
+
+[[debt.should]]
+component = "ochrance-core/Ochrance/Filesystem/Repair.idr"
+issue = "Repair idempotence is property-tested only, not proven (proof campaign Stage 3)."
+effort = "hard"
+impact = "high"
+discovered = "2026-06-05"
+
+[[debt.should]]
+component = "ochrance-core/Ochrance/FFI/Echidna.idr"
+issue = "ECHIDNA FFI is stubbed — echidnaProve returns 'FFI not yet implemented'."
+effort = "hard"
+impact = "medium"
+discovered = "2026-06-05"
 
 # ============================================================================
 # COULD — would fix eventually
 # ============================================================================
-# These are low-priority items that don't justify a session on their own.
-# They get picked up when an agent is in the area for other reasons.
-#
-# Example:
-# [[debt.could]]
-# component = "cicada"
-# issue = "RSR_OUTLINE.adoc references banned AGPL-3.0"
-# effort = "easy"
-# impact = "low"
-# discovered = "2026-03-23"
+
+[[debt.could]]
+component = ".machine_readable/"
+issue = "Behind the rsr-template scaffold: missing ai/, compliance/, configs/, policies/, scripts/, 0.1-AI-MANIFEST.a2ml, ENSAID_CONFIG.a2ml, root README.adoc, root-allow.txt. Needs template sync (Track B) — blocked on rsr-template/standards access."
+effort = "medium"
+impact = "medium"
+discovered = "2026-06-05"
+
+[[debt.could]]
+component = ".machine_readable/6a2/ (estate-wide)"
+issue = "phase vocabulary is not pinned by an enforced standard (svalinn 'crg-c-testing' vs ochrance 'implementation') — possible standards↔rsr-template divergence (Flag A); confirm against the canonical standards spec."
+effort = "medium"
+impact = "medium"
+discovered = "2026-06-05"
+
+[[debt.could]]
+component = ".github/workflows (ECHIDNA validation)"
+issue = "Dangerous-pattern scan greps literal strings including inside comments, so legitimate documentation can trip it (false positives)."
+effort = "easy"
+impact = "low"
+discovered = "2026-06-04"

.machine_readable/anchors/ANCHOR.a2ml

@@ -3,7 +3,7 @@
 
 id: "org.hyperpolymath.ochrance"
 version: "1.0.0"
-clade: "unknown"
+clade: "fv"
 status: "active"
 
 # SSG Configuration (Unified boj-server build)

EXPLAINME.adoc

@@ -16,15 +16,15 @@ Three components orchestrate this: A2ML parser/validator (parses filesystem mani
 
 === Claim 1: A2ML Lexer and Parser Are Structurally Recursive and Total
 
-**Location**: `/var/mnt/eclipse/repos/ochrance/ochrance-core/A2ML/Lexer.idr` and `/var/mnt/eclipse/repos/ochrance/ochrance-core/A2ML/Parser.idr` (Idris2 modules)
+**Location**: `ochrance-core/A2ML/Lexer.idr` and `ochrance-core/A2ML/Parser.idr` (Idris2 modules)
 
 **How verified**: Both modules use the `%default total` directive, requiring all functions to be total (no partial match, no undefined behavior). The lexer is structurally recursive: it tokenizes input by consuming characters and recursing on the remainder (proof: input size strictly decreases). The parser is similarly total: it parses tokens using sized types (`List (n : Nat)`) to guarantee termination (proof: token list shrinks). README (§Overview) claims "A2ML Parser/Validator" with compile-time structure proofs; this is verified by the Idris2 type checker itself — if either module had a partial function, `idris2 --check` would reject it with an error, not compile.
 
 **Caveat**: Idris2 totality checking is a sound approximation but not perfect. Deeply nested mutual recursion can escape detection in rare cases, though practice shows this is extremely rare.
 
 === Claim 2: Verified Merkle Tree Size Guarantees Are Compile-Time Proofs
 
-**Location**: `/var/mnt/eclipse/repos/ochrance/ochrance-core/Framework/Merkle.idr` (Idris2 Merkle tree with size-indexed types)
+**Location**: `ochrance-core/Filesystem/Merkle.idr` (Idris2 Merkle tree with size-indexed types)
 
 **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.