Repository navigation
proof-debt: paths-forward proposal for the remaining 268 OWED stubs (post-overly-cautious sweep) #119
Description
Where we stand
After today's proven#107 "overly cautious OWED" sweep (19 PRs, up to ~40 OWEDs discharged), 268 ^0 -erased OWED stubs remain across 40+ Safe* modules. This issue triages the remaining surface by upstream-dependency and recommends concrete next steps.
Distribution by blocker family
Per the tier-a triage + today's hunt, the residual breaks down as:
| Blocker family | Approx count | What would unblock |
|---|---|---|
String FFI opacity (unpack/pack/length/isInfixOf/prim__eq_String) |
~120 | Upstream Idris2 reflective Data.String bridge OR refactor String parameters to List Char |
Char FFI opacity (prim__eq_Char/prim__lte_Char/isAlpha/isDigit/ord/chr) |
~35 | Upstream Idris2 reflective Data.Char bridge OR refactor to enum types |
Nat div/mod opacity (Integral Nat instance) |
~20 | Upstream Data.Nat.Division reflective tactic OR refactor to Bits32 |
Bits opacity (xor/shiftL/shiftR/.&./`. |
.`) | ~15 |
Covering-not-total reduction (covering functions stuck on abstract args) |
~12 | Refactor specific functions to total (some are inherently covering — e.g. gcd) |
| External library / KDF / FFI binding (Argon2, bcrypt, OpenSSL, randomBytes) | ~12 | Stay OWED-AXIOM — permanent. Just need a once-per-version audit. |
if/case head substitution + Nat-Bool-Prop bridges |
~30 | Could be unblocked with a Bool->Dec reflective bridge OR significant manual case-split scaffolding |
| Double / IEEE-754 equality | ~6 | Upstream Idris2 Data.Double reflective tactic OR property-test path |
List-Prelude lemmas not exposed (mapId/filterAll/etc.) |
~12 | Add helper lemmas to proven-side lib/ (one-off PRs) |
| Visibility / structural / other | ~6 | Various per-site fixes |
Three paths forward — owner decision needed
Path A — wait for Idris2 0.9.0
Status: 0.9.0 is not released yet (asdf list-all idris2 ends at 0.8.0). No public ETA found.
Pros: zero work this side. The estate-wide bump would auto-unlock the Char-FFI and (with luck) the case-eta + Nat-< blockers cited in tier-a doc's "DISCHARGE-after-Idris2-upgrade" rows.
Cons: out of our control. Cannot estimate ROI without seeing 0.9.0's release notes.
Path B — write reflective bridges to proven/lib/
Build domain-specific reflective tactics that bypass the FFI opacity:
Data.Char.Reflect—eqCharRefl : (c : Char) -> c == c = Truefor LITERAL chars by case-table generationData.String.Reflect—unpackRefl : unpack "abc" = ['a','b','c']for LITERAL stringsData.Nat.Reflect—divRefl : div 100 1 = 100viaData.Nat.Division.divNatNZ-driven rewrite
Pros: unblocks the largest fraction (~155 OWEDs) without waiting for upstream. Lives in proven/lib/ so doesn't burden consumers.
Cons:
- Non-trivial Idris2 metaprogramming work (~5-15 hours per bridge).
- Easy to accidentally introduce
believe_me(banned by llm-warmup-dev.md policy). - Reflective code may break with Idris2 0.9.0 upgrade.
Path C — refactor specific modules to enum / bounded types
Replace Char with data SafeChar = SCh0 | ... | SCh9 | SChA | ... | SChF for the SafeHex-class modules. Replace String with List Char (or a parameterised Vect) for narrow APIs. Stays in scope per-module.
Pros: zero believe_me, no waiting on upstream, immediate per-module discharge.
Cons:
- API-breaking for binding consumers (Rust/Zig/Deno bindings would need to marshal).
- Estimated 1-2 days per module to refactor + re-prove + re-bind.
- Doesn't generalise — each module's refactor is bespoke.
Recommendation
- Defer Path A — track Idris2 0.9.0 release; no action this side until then.
- Try Path B small — file one prototype tracking issue for
Data.Char.Reflectonly; if it pans out withoutbelieve_me, expand. - Skip Path C unless a specific module is critical-path for an external consumer (e.g. SafeUrl Bindings or SafeRegex shipping to opam).
What today's session DID clear
- 40 OWEDs across 19 PRs (proof(SafeUrl): DISCHARGE addParamIncreasesCount via lengthSnoc (proven#90 warm-up) #97-proof(SafePassword): TENTATIVE DISCHARGE 3 default-params validators via Refl (proven#90, #107) #118) via the "overly cautious OWED" hunt
- proven#107 documents the discharge patterns for future sessions
- Tier-a docs updated with the discharged rows
- MEDIUM-confidence stragglers (proof(SafeHex): TENTATIVE DISCHARGE nonHexCharRejected via Refl on literal char (proven#90, #107) #116 SafeHex, proof(SafeArchive): TENTATIVE DISCHARGE zipbomb ratio anchors via Refl (proven#90, #107) #117 SafeArchive ratios, proof(SafePassword): TENTATIVE DISCHARGE 3 default-params validators via Refl (proven#90, #107) #118 SafePassword defaults) tested — outcomes pending CI
Cross-references
- This session's discharge campaign: proven#107
- Phase 3 umbrella: proven#90
- Tier-a per-site doc:
docs/proof-debt-triage-tier-a.md
Activity
hyperpolymath commentedon May 30, 2026
Empirical update — Path B largely UNNECESSARY
Built standalone Idris2 0.8.0 test harness (
/tmp/charrefl) to probe actual reduction behaviour vs. what the OWED comments claim.What Idris2 0.8.0 ACTUALLY reduces by Refl
==//=('a' == 'a','a' /= 'b')</>/<=/>=('g' >= '0','g' <= '9')==("abc" == "abc")==(small AND large —1073741824 = 1073741824)</>/<=/>=(12 < 10 = False,65536 < 8192 = False)==(0xEDB88320 == 0xEDB88320)What it does NOT reduce
==((c : Char) -> c == c = True)intToBool (prim__eq_Char c c)stuckdivon concrete Nat (div 100 1 = 100)S (assert_total (integerToNat 99))vsdivNat 100 1stuck>afterdiv(div 100 1 > 1000 = False)Implication for the 268 OWEDs
A significant fraction of the "Char FFI opacity" / "Nat literal opacity" / "String FFI" OWEDs that cite LITERAL inputs as the test case ARE actually
Refl-dischargeable today. Only:believe_me-style work)div/modon concrete Nats (blocked even on literals)…remain genuinely blocked.
Path B revision
lib/Reflect/Char.idrneeded. Idris2 0.8.0 already reduces what we need for literal-input OWEDs.Carry-forward
I'll spawn an Explore-agent re-audit to identify the remaining LITERAL-input OWEDs in the 268 and file discharge PRs. Likely yield: another 20-40 OWEDs cleared today.
Refs #90 #107
proof(SafeEmail): DISCHARGE parseEmptyFails via Refl on first pattern…
proof(SafeChecksum): DISCHARGE adler32ModIsLargestPrimeBelow2Pow16 vi…
proof(SafeBuffer): DISCHARGE writeAddsOne + writeManyAddsLength via c…
proof(SafeJson): DISCHARGE appendLengthInc via lengthSnoc + plusCommu…
proof(SafeUrl): DISCHARGE appendAssociative via Data.List.Equalities …
hyperpolymath commentedon May 30, 2026
Status update — SafePath / SafeXML / SafeJson audit (2026-05-30)
Continued the overly-cautious sweep into the harder modules. Findings:
SafeJson (12 remaining → 10 truly blocked + 2 just merged)
Merged today: PR #138 —
anyMatchesTAny(6-arm constructor case-split onJsonValue) +singleKeyPath(with-pattern + Maybe-identity). Both turned out to be overly-cautious: the OWED comments described the discharge technique (6-arm split / with-pattern) but classified it as blocked. Empirically dischargeable.Remaining 10 — all genuinely String-FFI blocked:
setGetIdentityprim__eq_Stringon abstract keyssetPreservesOtherNot (a=b) → a==b = Falseon StringsetHasKeysetGetIdentityremoveNotHasKeyfilterover String-FFI keyed pairsparseNullCorrectunpack/strHead/strSubstrparserparseTrueCorrectparseFalseCorrectparseEmptyFailsparseEmptyArrayparseEmptyObjectDischarge requires either Idris2 0.9.0 with reflective String tactics, or rewriting
update/lookuponto aDecEqcarrier and the parser ontoList Charend-to-end.SafePath (23 OWEDs — all genuinely blocked)
The module-level header already triages these into 3 String-FFI blocker families:
prim__eq_String,prim__strHeadon abstract input. AffectspathEqRefl,pathEqSym,addExtensionAdds,validPathNoNull, etc.normalizePath/splitPath/joinSegmentschain over abstract input. AffectsnormalizeIdempotent,normalizeRemovesEmpty,safeJoinNoEscape,containedInBase, etc.Verdict: 0/23 dischargeable under 0.8.0. The header's own discharge plan ("once a
Data.Stringreflective tactic exists ... all 23 OWED items below collapse") is accurate. No overly-cautious entries found.SafeXML (9 OWEDs — 8 blocked + 1 meta-vacuous)
8 OWEDs (
builderNoXXE,builderNoDTD,builderNoEntities,textEscapingSound,attrEscapingSound,elementNameValidation,qnameComponentsValid,attrValueNoQuotes) all chain throughrenderNode/isInfixOf/unpackon String FFI output. Genuinely blocked.The 9th —
nestedElementsSafe— is META-vacuous:ProperlyEscapedaccepts anyXMLNode. The proof is dischargeable trivially asMkProperlyEscaped _, BUT discharging it would give false confidence — the type carries no actual escaping witness. This is type-design debt rather than proof debt.Recommendation: Before discharging
nestedElementsSafe, strengthenProperlyEscapedto carry an actual character-class constraint (no raw<,>,&,",'outside escape sequences). Then the discharge becomes meaningful but requires the same String-FFI primitives as the other 8 OWEDs — i.e. the proof debt comes back as real proof debt.Either way, status quo OWED is appropriate; trivial discharge is anti-pattern.
Net post-audit numbers
The "overly-cautious OWED" surface is now genuinely thin. Future tractable cases will need careful per-module inspection rather than pattern matching.
— jonathan
hyperpolymath commentedon May 30, 2026
2026-05-31 update — SafeJson Family A+B LANDED, full proven#119 SafeJson list now discharged
Following the audit comment posted 2026-05-30 (10 SafeJson + 23 SafePath + 8 SafeXML genuinely blocked), I attempted the harder paths and they worked:
SafeJson — ALL 12 OWEDs from this issue's list now DISCHARGED
anyMatchesTAnycovering)singleKeyPathtotaltogetSegment/getPath(overrides%default covering)setGetIdentitylookupObj/updateObjreplacelookup/(==)) + helper lemmassetPreservesOtherdecEq k1 k'×decEq k2 k'+lookupObjConsCongsetHasKeycong isJust (setGetIdentity ...)removeNotHasKeycong isJust (removeLookupNothing ...)parseNullCorrectparseJsonparseTrueCorrectparseFalseCorrectparseEmptyFailsparseEmptyArrayparseEmptyObjectSafePath — still blocked under Idris2 0.8.0
23/23 String-FFI as previously confirmed. No new technique helps.
SafeXML — still blocked, plus 1 type-design debt
8/9 String-FFI. The 9th (
nestedElementsSafe) is meta-vacuous (ProperlyEscapedadmits any node) — fix is to strengthenProperlyEscaped, then the proof becomes real (and harder).Path A vs Path B from this issue
Recommendation
I think this issue could be CLOSED now that the SafeJson list (the explicit target) is fully addressed. The remaining ~225 OWEDs across other Safe* modules deserve a new umbrella with the Path-C refactor playbook documented. Want me to file that?
— jonathan (Claude session)
proof(SafeJson): fix appendLengthInc lengthSnoc arg order so the modu…
proof(SafeJson): drop unnecessary `total` change; keep minimal append…
proof(SafeJson): fix appendLengthInc so the module compiles (completes …