docs: Phase 2 Days 11-21 — totality tickets + Tier C audit + long-tail enumeration#84
Merged
hyperpolymath merged 1 commit intoMay 27, 2026
Conversation
… long-tail enumeration Closes out Phase 2 of the proof-debt triage. Three day-bands done in parallel via sub-agent dispatch + integration: ## Days 11-14: Tier B totality refactor tickets Filed three GitHub issues for the modules with Family 3 (covering / totality) blockers: - **proven#80** — SafePassword.Strength `windows`/`detectPatterns`/ `analyzeStrength` covering→total refactor. Includes 3 refactor options (Vect, assert_smaller, fuel param) with cost estimates. Discharges 3 OWED sites once landed. - **proven#81** — SafeJson.Access `%default covering` → per-function `total` refactor. Mutually-recursive parsePathSegments/parsePathIndex + getPath/matchesType need structural-decrease visibility. Discharges 2 OWED sites. - **proven#83** — SafeCrypto modernIsSecure/standardIsSecure tracker for Idris2 0.9.0 elaborator fix (case-rewrite eta-expansion). NOT a totality issue; will discharge once 0.9.0 lands or via workaround. Cross-references added to `docs/proof-debt-triage-tier-a.md` for the 7 sites tracked across these 3 issues. ## Days 15-18: Tier C OWED-AXIOM library/version audit **Result: 79/79 OWED-AXIOM sites in Tier A modules PASS audit.** Each doc comment names its library (Idris2 0.8.0 + specific dependencies like Data.Bits, Data.String, Argon2id, etc.), pins a version, and gives an actionable discharge condition. One minor doc-comment clarification landed: `src/Proven/SafeCSRF/Proofs.idr:79` — `constantTimeEqSym` now explicitly names `Data.Char.eqCharSym` as the awaited reflective lemma (parallel to `Boj.SafetyLemmas.charEqSym`). ## Days 19-21: Witness-only long-tail enumeration Adversarial-grep + per-module inspection surfaced **6 additional confirmed overclaim modules** beyond the 13 already enumerated in PROOF-NEEDS.md: - **SafeSupplyChain** (HIGH) — `Prevents: tampered builds, unattested artifacts, provenance forgery` with no theorem. - **SafePBKDF2** (HIGH) — `Prevents: low iteration counts, short salts, weak derived key lengths` with no theorem. - **SafeProvenance** (MEDIUM) — `Formally verified change tracking and audit trails`. - **SafePolicy** (MEDIUM) — `Formally verified policy enforcement`. - **SafeRegistry** (MEDIUM) — `formally verified parsing ... with guarantees of correctness and termination`. - **SafeSchema** (MEDIUM) — `Formally verified schema evolution` + `compatibility proofs` + `correctness guarantees`. Headers softened in this commit (same pattern as the 22 softenings in proven#76 — `formally verified` → `via Bool predicates; theorems OWED`, etc.). **2 modules re-classified as actually proven** (NOT overclaims): SafeTrust (`satisfiesMonotone` discharged at L296-303 via exhaustive pattern-match + Refl per arm) + SafeOrdering (already noted in PROOF-NEEDS.md adversarial sample). PROOF-NEEDS.md patched: 6 new entries added to §"Owed" with severity + verbatim doc claims; 3 cross-cutting batch-fix templates documented for Phase 3 mechanical processing of the residual long tail. ## Caveat: long-tail still extrapolated The Days 19-21 enumeration was partial — Bash permission boundaries on the audit sub-agent prevented full read-through of all 76 claim-bearing single-file modules. On the order of **~54 modules remain extrapolated** as overclaim candidates. PROOF-NEEDS.md now honestly tags this residual as extrapolated rather than enumerated. ## Net visible debt after Phase 2 - 280 Fork A OWED in `src/Proven/*/Proofs.idr` - 87 Fork A OWED stubs in `tests/properties/*Props.idr` - 19 enumerated overclaim modules in PROOF-NEEDS.md (was 13; +6) - ~54 long-tail single-file modules still extrapolated - 3 GitHub issues open for Phase 3 unblocking (#80, #81, #83) **Total visible, grep-discoverable debt entries: ~386** (280 + 87 + 19). ## What Phase 2 deliberately did NOT do - Did not discharge any proof (that's Phase 3). - Did not per-site-read the 29 OWED-bearing modules outside Tier A (~70 sites). These are picked up in a Phase 2-bis or rolled into Phase 3 sequencing. - Did not exhaustively enumerate the ~54 long-tail extrapolated modules. ## Stack ordering Branched from `docs/proof-debt-triage-and-header-softening` which already includes #78 (test wireup) + #79 (Tier A classification) via in-branch merges. This commit is the final Phase 2 closeout — when the base PR merges to main, all of Phase 2 lands together. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
force-pushed
the
phase2/tier-a-per-site-reads
branch
from
15aa1f0 to
e28b863
Compare
hyperpolymath
merged commit 984163f
into
docs/proof-debt-triage-and-header-softening
10 of 15 checks passed
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes out Phase 2 of the proof-debt triage. Three day-bands done in parallel via sub-agent dispatch + integration.
Days 11-14 — Tier B totality refactor tickets
Three GitHub issues filed:
%default covering→ per-functiontotal(discharges 2 OWED sites)Cross-references added to
docs/proof-debt-triage-tier-a.mdfor the 7 sites tracked.Days 15-18 — Tier C OWED-AXIOM audit
79/79 OWED-AXIOM sites in Tier A modules PASS audit. Every doc comment names library + version + actionable discharge condition. One minor clarification landed:
SafeCSRF/Proofs.idr:79now explicitly names `Data.Char.eqCharSym` as the awaited reflective lemma.Days 19-21 — Long-tail enumeration
6 additional confirmed overclaim modules beyond the 13 already enumerated:
Headers softened in this PR (same pattern as the 22 softenings in proven#76). PROOF-NEEDS.md patched with the 6 new entries plus 3 cross-cutting batch-fix templates for Phase 3.
2 modules re-classified as actually proven: SafeTrust (`satisfiesMonotone` discharged) + SafeOrdering (already in adversarial sample).
Caveat
The long-tail enumeration was partial — Bash permission boundaries on the audit sub-agent prevented full read-through of all 76 claim-bearing single-file modules. On the order of ~54 modules remain extrapolated as overclaim candidates. PROOF-NEEDS.md now honestly tags this residual as extrapolated rather than enumerated.
Net visible debt after Phase 2
What Phase 2 deliberately did NOT do
Stack ordering
Stacked on `docs/proof-debt-triage-and-header-softening` (PR #76, which already includes #78 and #79 via in-branch merges). When #76 merges to main, all Phase 2 work lands together as one squashed commit.
Test plan
🤖 Generated with Claude Code