Skip to content

Commit 2d66b50

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof-debt: enumerate 32 partial-marker sites in PROOF-NEEDS.md per standards#203 (#75)
`bash scripts/check-trusted-base.sh .` reported 32 of 34 escape hatches as undocumented. The symbolic-postulate breakdown in §"What Remains Postulated" classifies these by name, but the script needs file:line entries for its per-site documentation check. This PR adds a "## Escape-Hatch Enumeration (2026-05-27)" section listing every reported site with file:line + classification: - AXIOM-STUB (8): genuine trusted-base entries (verifyEd25519, sha256, ed25519Correctness, sha256CollisionResistant, signatureNonReplayable, signatureNonMalleable, tamperEvidence, replayPrevention). - AXIOM-TRANSITIVE (21): partial inherited from spec-stub references; proof terms themselves are total (Refl, (), sym, rewrite, structural induction). Adds nothing new to trusted base. - DISCHARGE-PENDING (3): normalizedIsSafe, absolutePathRejection, ociLayoutEnforcement — tractable proofs already documented in §"Path to eliminating remaining String postulates". The remaining 2 of 34 (the two assert_total spec-crash stubs) were already documented in §"assert_total Usage (2) — ACCEPTABLE". After this PR `bash scripts/check-trusted-base.sh .` reports green: [OK] All 34 escape hatch(es) are documented No code changes; only PROOF-NEEDS.md is touched. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 468cba4 commit 2d66b50

1 file changed

Lines changed: 81 additions & 0 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,3 +140,84 @@ Both in `CryptoProofs.idr`, used as crash stubs for spec-only functions. Runtime
140140
## Dangerous Patterns
141141

142142
- Zero `believe_me`, zero `cast Refl`, zero `unsafePerformIO` in proof code.
143+
144+
## Escape-Hatch Enumeration (2026-05-27 — `check-trusted-base.sh` site list)
145+
146+
Per [standards#203](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc),
147+
each `partial` site reported by `bash scripts/check-trusted-base.sh .` is
148+
enumerated below with classification. Sites are listed with full
149+
file:line so the script's per-site documentation check passes. The
150+
symbolic-postulate breakdown in §"What Remains Postulated (12 total)"
151+
above remains the substantive narrative; this section is the
152+
mechanical CI-gate index.
153+
154+
Classification taxonomy:
155+
156+
- **AXIOM-STUB** — spec-stub `partial`+`idris_crash` that IS the trusted-base
157+
entry. Runtime impl lives elsewhere (e.g., `CryptoFFI.*IO`). Type-level use only.
158+
- **AXIOM-TRANSITIVE** — proof term itself is total (`Refl`, `()`, `sym`, `rewrite`,
159+
structural induction); `partial` inherited only because the type signature
160+
references a partial spec stub. Adds nothing new to trusted base.
161+
- **DISCHARGE-PENDING** — currently `idris_crash` postulate, but a tractable
162+
proof path is documented in §"Path to eliminating remaining String postulates"
163+
above. Targeted for future elimination.
164+
165+
### CryptoProofs.idr (7)
166+
167+
| File:line | Symbol | Class | Notes |
168+
|---|---|---|---|
169+
| `container-stack/cerro-torre/verification/idris/CryptoProofs.idr:71` | `verifyEd25519` | AXIOM-STUB | Opaque spec; runtime = `CryptoFFI.verifyEd25519IO` |
170+
| `container-stack/cerro-torre/verification/idris/CryptoProofs.idr:81` | `sha256` | AXIOM-STUB | Opaque spec; runtime = `CryptoFFI.sha256IO` |
171+
| `container-stack/cerro-torre/verification/idris/CryptoProofs.idr:95` | `sha256Deterministic` | AXIOM-TRANSITIVE | Proof = `Refl` |
172+
| `container-stack/cerro-torre/verification/idris/CryptoProofs.idr:102` | `sha256Pure` | AXIOM-TRANSITIVE | Proof = `Refl` |
173+
| `container-stack/cerro-torre/verification/idris/CryptoProofs.idr:109` | `ed25519Deterministic` | AXIOM-TRANSITIVE | Proof = `Refl` |
174+
| `container-stack/cerro-torre/verification/idris/CryptoProofs.idr:151` | `ed25519Correctness` | AXIOM-STUB | RFC 8032 §5.1.7 Edwards curve correctness |
175+
| `container-stack/cerro-torre/verification/idris/CryptoProofs.idr:174` | `sha256CollisionResistant` | AXIOM-STUB | NIST SP 800-107 collision resistance |
176+
177+
### SignatureProofs.idr (9)
178+
179+
| File:line | Symbol | Class | Notes |
180+
|---|---|---|---|
181+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:60` | `signatureNonReplayable` | AXIOM-STUB | Ed25519 EUF-CMA (reduces to DL on Curve25519) |
182+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:80` | `signatureNonMalleable` | AXIOM-STUB | RFC 8032 §8 cofactored verification |
183+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:114` | `verifyPair` | AXIOM-TRANSITIVE | Calls `verifyEd25519` |
184+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:137` | `verifyChain` | AXIOM-TRANSITIVE | Calls `verifyPair` |
185+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:153` | `chainHeadValid` | AXIOM-TRANSITIVE | Proof = with-block case-split (total) |
186+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:167` | `chainTailValid` | AXIOM-TRANSITIVE | Proof = with-block case-split (total) |
187+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:218` | `chainImpliesIndividual` | AXIOM-TRANSITIVE | Proof = induction on `IsElem` (total) |
188+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:245` | `chainExtension` | AXIOM-TRANSITIVE | Proof = `rewrite validSig in validChain` (total) |
189+
| `container-stack/cerro-torre/verification/idris/SignatureProofs.idr:272` | `chainCommutative` | AXIOM-TRANSITIVE | Proof = `boolCommTrue` 4-case Bool lemma (total, see 2026-05-18 regression resolution above) |
190+
191+
### ImporterProofs.idr (6)
192+
193+
| File:line | Symbol | Class | Notes |
194+
|---|---|---|---|
195+
| `container-stack/cerro-torre/verification/idris/ImporterProofs.idr:137` | `normalizedIsSafe` | DISCHARGE-PENDING | Needs `isInfixOf` bridge + `dotDotNotInfix` lemma |
196+
| `container-stack/cerro-torre/verification/idris/ImporterProofs.idr:158` | `extractionSafety` | AXIOM-TRANSITIVE | Proof = `isPrefixOfBridge` + `unpackAppend` + `charsPrefixOfAppend` (total via StringLemmas) |
197+
| `container-stack/cerro-torre/verification/idris/ImporterProofs.idr:176` | `symlinkSafety` | AXIOM-TRANSITIVE | Same proof pattern as `extractionSafety` |
198+
| `container-stack/cerro-torre/verification/idris/ImporterProofs.idr:208` | `absolutePathRejection` | DISCHARGE-PENDING | Needs `SafePath` semantics over `List Char` |
199+
| `container-stack/cerro-torre/verification/idris/ImporterProofs.idr:242` | `ociLayoutEnforcement` | DISCHARGE-PENDING | Needs `DecEq` on `TarEntry` paths |
200+
| `container-stack/cerro-torre/verification/idris/ImporterProofs.idr:282` | `zipSlipPrevention` | AXIOM-TRANSITIVE | Same proof pattern as `extractionSafety` |
201+
202+
### Theorems.idr (10)
203+
204+
| File:line | Symbol | Class | Notes |
205+
|---|---|---|---|
206+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:42` | `computeBundleHash` | AXIOM-TRANSITIVE | Calls `sha256` spec |
207+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:50` | `WellFormed` | AXIOM-TRANSITIVE | Type references `computeBundleHash` |
208+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:57` | `ProperlySigned` | AXIOM-TRANSITIVE | Type references `verifyChain` |
209+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:76` | `bundleIntegrity` | AXIOM-TRANSITIVE | Proof = `sym wellFormed` (total) |
210+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:93` | `signatureChainSoundness` | AXIOM-TRANSITIVE | Delegates to `chainImpliesIndividual` |
211+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:123` | `supplyChainIntegrity` | AXIOM-TRANSITIVE | Proof = two `rewrite` + `wf1` (total) |
212+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:161` | `tamperEvidence` | AXIOM-STUB | Composition of `sha256CollisionResistant` + `signatureNonReplayable` |
213+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:186` | `thresholdSatisfaction` | AXIOM-TRANSITIVE | Proof = `()` (trivial; security in premises) |
214+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:206` | `replayPrevention` | AXIOM-STUB | Direct consequence of `signatureNonReplayable` |
215+
| `container-stack/cerro-torre/verification/idris/Theorems.idr:230` | `nonRepudiation` | AXIOM-TRANSITIVE | Proof = `()` (trivial; security in premises) |
216+
217+
### Summary
218+
219+
- **AXIOM-STUB** (8): `verifyEd25519`, `sha256`, `ed25519Correctness`, `sha256CollisionResistant`, `signatureNonReplayable`, `signatureNonMalleable`, `tamperEvidence`, `replayPrevention`. These are the genuine trusted-base entries.
220+
- **AXIOM-TRANSITIVE** (21): Type-signature partiality inherited from AXIOM-STUB references. Every proof term is total; the only reason these are `partial` is Idris2 0.8's lack of a `postulate` keyword forcing partiality propagation through any caller of a spec stub.
221+
- **DISCHARGE-PENDING** (3): `normalizedIsSafe`, `absolutePathRejection`, `ociLayoutEnforcement` — tractable proofs documented in §"Path to eliminating remaining String postulates" above.
222+
223+
Total: 32 sites enumerated. The remaining 2 of 34 markers reported by the script are the two `assert_total` documented in §"assert_total Usage (2) — ACCEPTABLE" above.

0 commit comments

Comments
 (0)