[umbrella] Phase 3 — proof discharge campaign (SafeUrl warm-up → SafeRegex)

[hyperpolymath]

Campaign overview

Phase 3 of the proof-debt remediation arc kicks off the actual discharge work — converting OWED annotations into proven theorems. This is a multi-quarter campaign; this issue is the umbrella + sequencing tracker.

Phases 1 + 2 (Days 1-10) closed via PRs #76 + #77 (2026-05-27). Phase 2 Days 11-21 partially done — see Phase 2 tail status below.

Aggregate disposition (Tier A, ~209 sites)

Disposition	Sites	%	Effort
DISCHARGE	~59	28%	~30h
DISCHARGE-after-totality	~7	3%	gated on #80, #81
PROPERTY-TEST	~66	31%	~22h
OWED-AXIOM (permanent or until Idris2 upgrade)	~79	38%	tracked separately

DISCHARGE backlog concentration: SafeRegex (20) + SafeBase64 (10) + SafeEmail (10) = ~70% of total discharge work.

Recommended sequencing

1. SafeUrl warm-up — 16 OWED sites in src/Proven/SafeUrl/Proofs.idr. Lower-risk; mixed family. Use as gauge for Idris2 0.8.0 reducibility constraints.
   • Tractable today: addParamIncreasesCount (needs lengthSnoc : (xs : List a) -> (x : a) -> length (xs ++ [x]) = S (length xs) lemma + rewrite).
   • Blocked on Idris2 0.9.0: emptyBuilderEmpty (joinWith reduction), setGetIdentity (String equality).
2. SafeRegex (20 sites) — largest single concentration. Discharge via Brzozowski derivative formalism (or property-test path if formal blocked).
3. SafeBase64 (10 sites) — well-understood (fixed alphabet); high yield.
4. SafeEmail (10 sites) — depends on SafeRegex landing.

Phase 2 tail (still NOT done)

• Days 11–14: Tier B totality-refactor — tracked at Totality refactor: SafePassword.Strength.{detectPatterns, analyzeStrength, ...} (covering → total) #80 (SafePassword.Strength), Totality refactor: SafeJson.Access (%default covering → per-function total) #81 (SafeJson.Access)
• Days 15–18: Tier C OWED-AXIOM library/version doc audit (Argon2, bcrypt, OpenSSL versions + permanent-axiom rationale)
• Days 19–21: Witness-only long-tail enumeration of ~55 modules in PROOF-NEEDS.md

Phase 3 work proceeds in parallel with Phase 2 tail (only DISCHARGE-after-totality slice is gated).

Discharge convention

Per Fork A convention (.machine_readable/6a2/META.a2ml ADR-001):

• ||| OWED: → ||| DISCHARGED: once theorem closes, OR
• ||| OWED-AXIOM: for permanent obligations (external KDF, FFI opacity not in Idris2 reach)

Each discharge PR should:

• Convert ONE OWED → DISCHARGED (single-purpose, reviewable)
• Update PROOF-NEEDS.md if relevant
• Include a tests/properties/ smoke test where the theorem composes with existing checks
• GPG-sign + auto-merge per estate convention

Cross-references

• Phase 1 framework: docs/proof-debt-triage.md
• Tier A classification: docs/proof-debt-triage-tier-a.md
• Honest ledger: PROOF-NEEDS.md
• Phase 2 in-flight tickets: Totality refactor: SafePassword.Strength.{detectPatterns, analyzeStrength, ...} (covering → total) #80, Totality refactor: SafeJson.Access (%default covering → per-function total) #81, Idris2 0.9.0 dependency: SafeCrypto.modernIsSecure / standardIsSecure (case-rewrite eta-expansion) #83
• Memory: project_proven_proof_debt_triage.md

Disambiguation

proven proof-debt is DISTINCT from:

• ephapax formal/ (single judgment, Coq) — see ephapax CLAUDE.md
• typed-wasm post-A10 (L1-L15 lattice) — see project_typed_wasm_proof_debt_post_a10

No cross-references; fixes do not transfer.