docs(proof-debt): adopt OWED-with-justification convention (Refs standards#158) (#65)

hyperpolymath · claude · web-flow · commit 2cb3332aa3a1 · 2026-05-20T21:14:45.000+01:00
## Summary Single doc PR documenting the OWED-with-justification convention adopted by the standards#158 Fork A campaign. Companion to the 28 module-annotation PRs (proven#37-64). ### Human-facing: PROOF-NEEDS.md - Top-of-file note flags the 2026-05-20 re-audit of the 39 "carried forward, pending Proofs.idr re-audit" directories. Result: 6 clean, 28 with bodyless decls now annotated as OWED, 5 already fully proven. - New **"OWED-with-justification convention"** section codifies the pattern: ```idris ||| OWED: <one-sentence claim> ||| Held back by <Idris2 0.8.0 blocker>. Discharge once <unblocker>. 0 declarationName : Type ``` - Blocker-family table for the five recurring categories surfaced in the audit. - Fork-A-vs-Fork-B scope note. - "Honestly proven" section updated to reflect the re-audit (was "not re-verified by this pass"). ### Machine-facing: `.machine_readable/6a2/STATE.a2ml` - `last-updated` bumped 2026-03-15 → 2026-05-20. - New `[proof-coverage]` section with module counts. - New `[trust-posture]` section pinning the zero-bypass-token state. - New `[active-campaigns]` + `[session-history]` sections. ### Machine-facing: `.machine_readable/6a2/META.a2ml` - `last-updated` date added. - New `[architecture-decisions]` section with **ADR-001** recording the OWED-with-justification convention adoption, modelled on the boj-server META.a2ml ADR format. - New `[proof-conventions]` section pinning shape + banned tokens. ## What this is NOT - No Idris2 sources touched. Doc-only. - No `postulate` keyword introduced anywhere — the convention explicitly bans it (zero existing files use it). - Not a closure of #158 — the 28 annotation PRs are still DRAFT pending estate CI clear. ## Test plan - [x] PROOF-NEEDS.md still renders; the existing "Honesty refresh 2026-05-18" framing is preserved unchanged. - [x] STATE.a2ml + META.a2ml are TOML-parseable (visual inspection). - [x] No `.idr` files touched; build status unaffected. - [ ] CI will run on this branch once the estate-wide concurrency pool clears. ## Refs Refs hyperpolymath/standards#158 (Fork A campaign tracker), hyperpolymath/standards#124 (estate proof-debt epic). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
@@ -1,9 +1,22 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # META.a2ml — Project meta-information
-# Converted from META.scm on 2026-03-15
 
 [metadata]
 project = "proven"
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
 license = "PMPL-1.0-or-later"
 standard = "RSR 2026"
+last-updated = "2026-05-20"
+
+[architecture-decisions]
+decisions = [
+  { id = "ADR-001", title = "OWED-with-justification convention for bodyless declarations in Proofs.idr files", status = "accepted", date = "2026-05-20", body = "Bodyless type signatures (implicit postulates) are made discoverable via triple-pipe doc-comment naming the claim + Idris2 0.8.0 blocker + discharge condition, plus a leading `0 ` erased-multiplicity marker, plus the original bare signature. The `postulate` keyword is NOT used (zero Proofs.idr files use it). Canonical example: src/Proven/SafeChecksum/Proofs.idr. Reference: hyperpolymath/standards#158 Fork A campaign, PROOF-NEEDS.md." },
+]
+
+[proof-conventions]
+# Reference: see PROOF-NEEDS.md "OWED-with-justification convention".
+unproven-obligation-pattern = "owed-with-justification"
+unproven-obligation-shape = "triple-pipe-doccomment + 0-erased-multiplicity + bare-signature"
+banned-tokens-in-proofs-idr = ["believe_me", "idris_crash", "postulate"]
+canonical-example = "src/Proven/SafeChecksum/Proofs.idr"
+adr-reference = "ADR-001"
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -1,14 +1,48 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # STATE.a2ml — Project state checkpoint
-# Converted from STATE.scm on 2026-03-15
 
 [metadata]
 project = "proven"
 version = "0.1.0"
-last-updated = "2026-03-15"
+last-updated = "2026-05-20"
 status = "active"
 
 [project-context]
 name = "proven"
 completion-percentage = "stable"
 phase = "stable-library"
+
+[proof-coverage]
+# Counts as of 2026-05-20 audit (standards#158 Fork A).
+safe-modules-with-proofs-idr-directory = 41
+safe-modules-clean = 6
+# Clean = zero bodyless decls. Modules: SafeChecksum, SafeBuffer, SafeBloom,
+# SafeCryptoAccel, SafeHKDF, SafeFPGA. These landed 2026-05-19/20 and set the
+# OWED convention.
+
+safe-modules-with-owed-annotation = 28
+# Annotated via PRs #37-64 under standards#158 Fork A (excl. #36 = CI bump).
+# Eight locally idris2-0.8.0-verified: #52 #54 #56 #57 #58 #60 #62 #63.
+
+bodyless-decls-total = 250
+# All annotated with ||| OWED: + 0 erased-multiplicity per the SafeChecksum
+# convention. See PROOF-NEEDS.md "OWED-with-justification convention" and
+# META.a2ml ADR-001.
+
+[trust-posture]
+believe-me-uses = 0
+idris-crash-uses = 0
+postulate-keyword-uses = 0
+# Zero proof-bypass tokens in Proofs.idr files. All unproven obligations are
+# explicit OWED declarations with named blocker + discharge condition.
+
+[active-campaigns]
+fork-a-annotation = "complete (28 DRAFT PRs filed, awaiting estate CI clear of concurrency-pool exhaustion)"
+fork-b-discharge = "triage open — quick-wins flagged in PROOF-NEEDS.md (SafeCrypto isSecure refactor; SafePath already-Refl pairs)"
+
+[session-history]
+# Most recent first.
+"2026-05-20" = "Fork A campaign complete: 250 bodyless decls across 28 of 41 modules annotated via OWED-with-justification convention (PRs #37-64, Refs standards#158); cross-prover audit confirms 0 Lean sorry / 0 Coq Admitted in first-party code (only echidnabot dogfood fixtures)"
+"2026-05-19" = "Six new modules merged with explicit OWED markers (SafeChecksum, SafeBuffer, SafeBloom, SafeCryptoAccel, SafeHKDF, SafeFPGA) — convention-setting"
+"2026-05-18" = "PROOF-NEEDS.md honesty refresh (standards#124); ~70 single-file overclaim modules surfaced separately from the Proofs.idr-directory audit"
+"2026-03-15" = "STATE.scm converted to STATE.a2ml"
diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
@@ -1,5 +1,16 @@
 # PROOF-NEEDS.md — proven
 
+> **Re-audit update 2026-05-20.** The 39 "carried forward, pending Proofs.idr
+> re-audit" directories have now been re-audited (hyperpolymath/standards#158
+> Fork A). Net finding: of those 39, **6 are clean** (no bodyless decls;
+> SafeChecksum, SafeBuffer, SafeBloom, SafeCryptoAccel, SafeHKDF, SafeFPGA —
+> these set the OWED convention), **28 carried bodyless decls** which have
+> now been annotated as `||| OWED:` + `0 ` erased-multiplicity per the
+> convention (PRs hyperpolymath/proven#37-64, all DRAFT pending estate CI
+> clear; 8 locally idris2-0.8.0-verified). Total: 250 bodyless decls
+> surfaced and made discoverable. See the new "OWED-with-justification
+> convention" section below and `.machine_readable/6a2/META.a2ml` ADR-001.
+>
 > **Honesty refresh 2026-05-18.** `proven` is the estate trust root, so this
 > ledger must not overclaim. The prior edition asserted "the most complete
 > Idris2 proof infrastructure in the ecosystem" and "~30 modules lack proof
@@ -137,16 +148,67 @@ Each line: module — verbatim doc claim — why it is owed.
 > `Prevents:|formally verified|cannot crash|guarantee|no false negative|
 > traversal|injection|attack` without a discharged theorem is OWED.
 
-## Honestly proven (carried forward, pending Proofs.idr re-audit)
+## OWED-with-justification convention (adopted 2026-05-20)
+
+Bodyless type signatures in `Proofs.idr` files are *implicit postulates* —
+Idris2 parses them as axioms with no proof body. To make the trust posture
+visible (to readers and to grep), each bodyless declaration carries:
+
+```idris
+||| OWED: <one-sentence statement of what's claimed>
+||| Held back by <specific Idris2 0.8.0 blocker>. Discharge once
+||| <what would unblock it>.
+0 declarationName : Type
+```
+
+Three parts: triple-pipe doc-comment with claim+blocker+discharge condition;
+leading `0` (Idris2 quantitative-type-theory erased-multiplicity marker —
+runtime-erased); original bare type signature.
+
+**Do NOT use the `postulate` keyword.** Zero `Proofs.idr` files in `proven`
+use it. The OWED+`0`+bare-sig pattern is chosen so that the reason each
+obligation exists is discoverable, and erasure means proof gaps cannot
+silently affect runtime behaviour.
+
+Canonical example: `src/Proven/SafeChecksum/Proofs.idr` (L24-100). Also see
+SafeBuffer, SafeBloom, SafeCryptoAccel, SafeHKDF, SafeFPGA — these landed
+2026-05-20 and set the convention.
+
+### Blocker families surfaced in the 2026-05-20 audit
+
+| Family | Typical shape | Discharge route |
+|--------|---------------|-----------------|
+| String FFI opacity | claims about `unpack`/`pack`/`ord`/`toLower`/`prim__eq_String` | Typed String/Char primitive layer, or Class-J axiom set parallel to gossamer/boj-server |
+| Numeric-literal Refl gaps | `Bits32`/`Bits64`/large-`Nat` literal equality | `Data.Bits` reflective tactic or `Integer`-backed bound |
+| Covering-not-total reduction | e.g. `gcd n 0 = n` under `Data.Nat.gcd` declared `covering` (cf. SafeMath PR#46) | Upstream Idris2 stdlib promoting to `total`, or local total reimplementation |
+| Foldl-predicate gaps | claims about `Data.List.all`/`any` on abstract lists | Cons-distribution lemmas inline (cf. proof-of-work PR#60) |
+| Structurally OWED | e.g. SafeJWT `validatedJWTFromValidation` (record type lacks provenance proof field) | Type-side widening, not just FFI seam |
+
+### Fork A scope vs. Fork B scope
+
+Fork A (this campaign) = make every bodyless decl explicit with a justified
+OWED note. Surfacing, not discharging. **Complete 2026-05-20** via PRs
+hyperpolymath/proven#37-64.
+
+Fork B (per-module discharge triage) is the next layer — selectively
+proving the dischargeable subset. Quick-win candidates surfaced in the
+audit: SafeCrypto `modernIsSecure`/`standardIsSecure` (3-line `isSecure`
+refactor), SafePath already-Refl-able pairs (already done in PR#57). Other
+modules require deeper triage.
+
+## Honestly proven (carried forward, Proofs.idr re-audited 2026-05-20)
 
 39 directories: SafeAPIKey, SafeArgs, SafeBase64, SafeCORS, SafeCSP, SafeCSRF,
 SafeCSV, SafeContentType, SafeCookie, SafeCrypto, SafeEmail, SafeEnv, SafeFile,
 SafeHSTS, SafeHTTP, SafeHeader, SafeHtml, SafeJWT, SafeJson, SafeMath,
 SafeNetwork, SafeOTP, SafePassword, SafePath, SafeRBAC, SafeRateLimiter,
 SafeRecord, SafeRedirect, SafeRegex, SafeSQL, SafeSRI, SafeSSRF, SafeSemVer,
 SafeShell, SafeString, SafeTOML, SafeUrl, SafeXML, SafeYAML — **plus**
-SafeOrdering (single-file, one discharged theorem). These are *claimed*
-proven; their `Proofs.idr` bodies are not re-verified by this pass.
+SafeOrdering (single-file, one discharged theorem). Their `Proofs.idr` bodies
+were re-audited 2026-05-20 under standards#158 Fork A: of the 39 directory-form
+modules, 6 are clean (zero bodyless decls), 28 had bodyless decls now
+annotated as explicit OWED, 5 had only fully-discharged proofs already. No
+silent postulates remain.
 
 ## Stubs — proof absence disguised as presence (CRITICAL) — *now empty*
 
