From 803286b824f63a2c9185db92ca53767b84c1e7d7 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 19:34:18 +0100 Subject: [PATCH] docs(proof-debt): adopt OWED-with-justification convention (Refs standards#158) PROOF-NEEDS.md: - Top-of-file update flags the 2026-05-20 re-audit of the 39 "carried forward" directory-form modules under the #158 Fork A campaign. - New "OWED-with-justification convention" section codifies the pattern set by SafeChecksum/SafeBuffer/SafeBloom/SafeCryptoAccel/SafeHKDF/SafeFPGA (2026-05-19/20): triple-pipe `||| OWED:` doc-comment with claim + Idris2 0.8.0 blocker + discharge condition; leading `0 ` erased-multiplicity; original bare signature. The `postulate` keyword is NOT used (zero Proofs.idr files use it). - Blocker-family table documents the five recurring categories surfaced in the 2026-05-20 audit (String FFI opacity, numeric-literal Refl gaps, covering-not-total reduction, foldl-predicate gaps, structurally OWED). - "Honestly proven" section updated: 39 directories' Proofs.idr bodies have now been re-audited (6 clean, 28 OWED-annotated, 5 fully proven). .machine_readable/6a2/STATE.a2ml: - last-updated bumped 2026-03-15 -> 2026-05-20. - New [proof-coverage] section: module counts + Fork A campaign status. - New [trust-posture] section: 0 believe_me / idris_crash / postulate uses. - New [active-campaigns] section. - New [session-history] section with three recent dates. .machine_readable/6a2/META.a2ml: - last-updated date added. - New [architecture-decisions] section with ADR-001 recording the OWED-with-justification convention. - New [proof-conventions] section pinning the shape and banned tokens. Doc-only change; no Idris2 sources touched. Refs hyperpolymath/standards#158. Co-Authored-By: Claude Opus 4.7 (1M context) --- .machine_readable/6a2/META.a2ml | 15 ++++++- .machine_readable/6a2/STATE.a2ml | 38 +++++++++++++++++- PROOF-NEEDS.md | 68 ++++++++++++++++++++++++++++++-- 3 files changed, 115 insertions(+), 6 deletions(-) diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index 5ca2ce98..935e486d 100644 --- 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 " 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 index d13dbb9b..a603c5ca 100644 --- 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 index d9f4e4d1..f7c840fb 100644 --- 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,7 +148,55 @@ 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: +||| Held back by . Discharge once +||| . +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, @@ -145,8 +204,11 @@ 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*