proof-debt: paths-forward proposal for the remaining 268 OWED stubs (post-overly-cautious sweep)

[hyperpolymath]

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 = True for LITERAL chars by case-table generation
• Data.String.Reflect — unpackRefl : unpack "abc" = ['a','b','c'] for LITERAL strings
• Data.Nat.Reflect — divRefl : div 100 1 = 100 via Data.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.Reflect only; if it pans out without believe_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

Refs #90 #107

[hyperpolymath]

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

Operation	Reduces?
Char literal == / /= ('a' == 'a', 'a' /= 'b')	✅ YES
Char literal < / > / <= / >= ('g' >= '0', 'g' <= '9')	✅ YES
String literal == ("abc" == "abc")	✅ YES
Nat literal == (small AND large — 1073741824 = 1073741824)	✅ YES
Nat literal < / > / <= / >= (12 < 10 = False, 65536 < 8192 = False)	✅ YES
Bits32 literal == (0xEDB88320 == 0xEDB88320)	✅ YES

What it does NOT reduce

Operation	Reduces?	Notes
Abstract Char == ((c : Char) -> c == c = True)	❌ NO	intToBool (prim__eq_Char c c) stuck
div on concrete Nat (div 100 1 = 100)	❌ NO	S (assert_total (integerToNat 99)) vs divNat 100 1 stuck
> after div (div 100 1 > 1000 = False)	❌ NO	Same blocker

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:

• Abstract-argument OWEDs (require believe_me-style work)
• div/mod on concrete Nats (blocked even on literals)
• Genuine pack/unpack composition (mostly real)

…remain genuinely blocked.

Path B revision

• No new lib/Reflect/Char.idr needed. Idris2 0.8.0 already reduces what we need for literal-input OWEDs.
• The "reflective bridge" Path B was a strawman — the real fix is a follow-up audit that re-classifies OWEDs by literal vs. abstract input rather than by primitive family. The literal-input ones discharge today; the abstract-input ones stay until 0.9.0 or upstream.

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

[hyperpolymath]

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 on JsonValue) + 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:

OWED	Blocker
setGetIdentity	prim__eq_String on abstract keys
setPreservesOther	Not (a=b) → a==b = False on String
setHasKey	derives from setGetIdentity
removeNotHasKey	filter over String-FFI keyed pairs
parseNullCorrect	unpack/strHead/strSubstr parser
parseTrueCorrect	same
parseFalseCorrect	same
parseEmptyFails	same
parseEmptyArray	same
parseEmptyObject	same

Discharge requires either Idris2 0.9.0 with reflective String tactics, or rewriting update/lookup onto a DecEq carrier and the parser onto List Char end-to-end.

SafePath (23 OWEDs — all genuinely blocked)

The module-level header already triages these into 3 String-FFI blocker families:

1. String FFI opacity — prim__eq_String, prim__strHead on abstract input. Affects pathEqRefl, pathEqSym, addExtensionAdds, validPathNoNull, etc.
2. List-of-components Refl gaps for canonicalisation — normalizePath / splitPath / joinSegments chain over abstract input. Affects normalizeIdempotent, normalizeRemovesEmpty, safeJoinNoEscape, containedInBase, etc.
3. Predicate-fold gaps over path segments — extension-handling lemmas thread through several String + List eliminations.

Verdict: 0/23 dischargeable under 0.8.0. The header's own discharge plan ("once a Data.String reflective 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 through renderNode/isInfixOf/unpack on String FFI output. Genuinely blocked.

The 9th — nestedElementsSafe — is META-vacuous:

data ProperlyEscaped : XMLNode -> Type where
  MkProperlyEscaped : (node : XMLNode) -> ProperlyEscaped node

ProperlyEscaped accepts any XMLNode. The proof is dischargeable trivially as MkProperlyEscaped _, 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, strengthen ProperlyEscaped to 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

• Cleared today: SafeFile proof(SafeFile): DISCHARGE readTrackingMonotonic + writeTrackingMonotonic #136 (2), SafeCSV proof(SafeCSV): DISCHARGE filterTrueIdentity + mapFieldsIdentity, fix 3 broken proofs, wire into CI #137 (2 + 3 broken→OWED, 3 ctor-form witnesses), SafeJson proof(SafeJson): DISCHARGE anyMatchesTAny (6-arm split) + singleKeyPath (with-pattern) #138 (2)
• Confirmed-blocked under 0.8.0: 10 (SafeJson) + 23 (SafePath) + 8 (SafeXML proof debt) + 1 (SafeXML type-design debt)
• Approximate total remaining: ~225-230 OWEDs, ~95% are real String-FFI blockers, ~5% may unlock via constructor-form or covering-detection techniques as more modules are audited.

The "overly-cautious OWED" surface is now genuinely thin. Future tractable cases will need careful per-module inspection rather than pattern matching.

— jonathan