Skip to content

Commit c6e5d95

Browse files
hyperpolymathhyperpolymath
authored
fix(proofs/idris2): redesign auditTrailCompleteness as per-insertion theorem (closes #131) (#135)
## Summary - Redesigns the third non-theorem from the `#119` Category A inventory, following the `#60` / `#61` / `#119A` precedent: restate-then-prove rather than discharge with `believe_me`. - The previous shape `Elem p (map AuditEntry.path entries)` was refuted by `entries := []` (an `ObliterationProof` for any `p` is trivially constructible, but the empty log contains no paths). - New shape threads `(log, entry, p, insertedPath : AuditEntry.path entry = p)` and proves `Elem p (map AuditEntry.path (appendAuditEntry log entry))` — the actual invariant: the path is in the post-append log *because* the entry recording it was appended via the official constructor. ## Closure (zero new axioms, zero `believe_me`) 1. `appendAuditEntry log entry` reduces to `log ++ [entry]` by definition (already discharged as `appendOnlyAuditLog : Refl`). 2. Stdlib `Data.List.Elem.elemMap` lifts membership through `map`. 3. A short local helper `elemAppRightSelf : (xs : List a) -> (x : a) -> Elem x (xs ++ [x])` discharges the append-right case by induction — Idris2 0.8.0 base does not ship this lemma. 4. `rewrite sym insertedPath` substitutes `AuditEntry.path entry` with `p` in the goal. ## Files - `proofs/idris2/src/Filesystem/RMO.idr` — redesigned signature + closed proof + the local `elemAppRightSelf` helper + a doc comment recording the design rationale (mirrors the `#60` / `#61` / `#119A` style). - `PROOF-NEEDS.md` — inventory updated (`RMO.idr` hole count 3 → 2), closure-history row added for 2026-06-03, drift paragraph + Cat-A bullet reconciled. ## Test plan - [x] `cd proofs/idris2 && rm -rf build && idris2 --build valence-shell.ipkg` — exit 0, all four modules build clean - [x] `grep -c '?auditTrailCompleteness' proofs/idris2/src/Filesystem/RMO.idr` returns 0 (hole closed) - [x] `grep -c 'believe_me' proofs/idris2/src/Filesystem/RMO.idr` returns 2 — both inside `|||` doc comments, no actual invocations - [x] No edits to `proofs/idris2/src/Filesystem/Axioms.idr` (the only sanctioned `believe_me` location remains untouched) - [ ] CI `verify-idris2` job (idris-verification.yml) green - [ ] Owner sanity-check the redesigned signature reflects the intended invariant Closes #131. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
2 parents 63b94e8 + 357b99b commit c6e5d95

2 files changed

Lines changed: 111 additions & 111 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 43 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -38,9 +38,9 @@
3838
| `Operations.idr` | 7 (`mkdirRmdirReversibleProof`, `rmdirMkdirReversibleProof`, `touchRmReversibleProof`, `rmTouchReversibleProof`, `writeFileReversibleProof`, `operationIndependenceProof`, `cnoWriteSameContentProof`) | 4 (`?rmdirPrfAfterMkdir`, `?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) |
3939
| `Composition.idr` | 4 (`sequenceReversibleProof`, `compositionReversibleProof`, `undoRedoIdentityProof`, `undoRedoCompositionProof`) | 0 |
4040
| `Model.idr` | 2 (`equivReflProof`, `equivTransProof`; `equivSymProof` is closed via `andCommutative`) | 0 |
41-
| `RMO.idr` | 3 (`overwriteIrreversibleProof`, `hardwareEraseIrreversibleProof`, `auditTrailCompletenessProof`; `appendOnlyAuditLogProof` is closed via `Refl`) | 0 |
41+
| `RMO.idr` | 2 (`overwriteIrreversibleProof`, `hardwareEraseIrreversibleProof`; `appendOnlyAuditLogProof` is closed via `Refl`; `auditTrailCompletenessProof` is closed via redesign + `elemMap` + `elemAppRightSelf` — see #131) | 0 |
4242

43-
Drift from previous PROOF-NEEDS.md tally (22 holes) to current (16 holes) is mechanical: `equivSymProof` and `appendOnlyAuditLogProof` closed silently during the 2026-06-02 morning sweep (visible by grep but the inventory text was not updated). No body changes — this paragraph reconciles the count.
43+
Drift from previous PROOF-NEEDS.md tally (22 holes) to current (15 holes) is mechanical: `equivSymProof` and `appendOnlyAuditLogProof` closed silently during the 2026-06-02 morning sweep (visible by grep but the inventory text was not updated), and `auditTrailCompletenessProof` closed via signature redesign on 2026-06-03 (#131). No structural changes to the live source beyond #131 — this paragraph reconciles the count.
4444

4545
All `partial` markers in `proofs/idris2/src/Filesystem/*.idr` were cleared 2026-06-02 (PRs #108 + #109, closing #89). The total `partial` count is zero.
4646

@@ -61,6 +61,7 @@ All `partial` markers in `proofs/idris2/src/Filesystem/*.idr` were cleared 2026-
6161
| 2026-06-02 | Idris2 build oracle | `idris-verification.yml` workflow + Justfile recipes shipped (PR #106, closes #70) |
6262
| 2026-06-02 | Idris2 0.8.0 parse fixes | `AuditEntry.proof` keyword-clash rename (PR #112); `hardwareEraseIrreversible` multi-line signature fix (PR #113); `reverseConcat` closed via `Data.List.revAppend` (PR #115) |
6363
| 2026-06-02 PM | Coq admit triumvirate | `mkdir_two_dirs_reversible` restated to LIFO and closed (#56); `overwrite_pass_equalizes_storage` strengthened with `block_overwritten` constraint, closed with zero new axioms (#57); `obliterate_not_injective` threaded through the strengthened lemma + `multi_pass_same_start_same_result`, closed with only standard funext (#58). Coq layer now has **zero `Admitted` markers** (only the justified `Axiom is_empty_dir_dec` remains). |
64+
| 2026-06-03 | Idris2 RMO `auditTrailCompleteness` redesign | Signature redesigned away from the `entries = []`-refutable shape into a per-insertion claim threading `(log, entry, p, insertedPath : path entry = p)`; closed via `elemMap` (stdlib) + a local `elemAppRightSelf` induction + `sym insertedPath` rewrite (#131, mirrors the #60 / #61 / #119A precedent). Zero new axioms; zero `believe_me`. |
6465

6566
### What Needs Proving (current, prioritised by tractability × value)
6667

@@ -94,75 +95,60 @@ about `(q == p)` on opaque `Path` values inside `elem`, which Idris2
9495
`HardwareEraseProof -> (Unit -> Filesystem) -> Void` is refuted by
9596
any non-empty `recovery` (the function exists trivially). Correct
9697
shape needs the recovery to take the post-erase state as input.
97-
- `auditTrailCompletenessProof` (`RMO.idr:270`): conclusion
98-
`Elem p (map AuditEntry.path entries)` is refuted by `entries = []`.
99-
Correct shape needs an "entry was appended" precondition naming the
100-
insertion event in the log.
101-
102-
These three should be filed as **`#119` sub-issues** with the
103-
non-theorem refutations, in line with the #60 / #61 precedent.
98+
- ~~`auditTrailCompletenessProof` (`RMO.idr:270`)~~ **CLOSED via #131**:
99+
the previous shape `Elem p (map AuditEntry.path entries)` was refuted
100+
by `entries = []`. Redesigned to thread a single `entry`, an
101+
`insertedPath : AuditEntry.path entry = p` premise, and reason about
102+
`appendAuditEntry log entry = log ++ [entry]`. Closure via
103+
`elemMap` (stdlib) + `elemAppRightSelf` (local helper) + a
104+
`sym insertedPath` rewrite. Zero new axioms, zero `believe_me`.
105+
106+
The remaining two should be filed/handled as **`#119` sub-issues** with
107+
the non-theorem refutations, in line with the #60 / #61 / #131
108+
precedent.
104109

105110
**4 Operations.idr sub-holes** (`?rmdirPrfAfterMkdir`,
106111
`?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) — same
107112
primitive-eq blocker as the Cat-B set above. Each requires showing
108113
that the post-operation precondition holds, which reduces to
109114
`(p == p) = True` on opaque `Path` — blocked.
110115

111-
#### Priority 2 — TWO blockers (primitive-eq UNBLOCKED; `all`/`foldMap` still blocked)
112-
113-
Status as of the 2026-06-02 PM Q1-C pilot (PR #133):
114-
115-
**Blocker 1 (primitive-eq) — UNBLOCKED.** The pilot adds
116-
`axStringEqRefl` + `axBits8EqRefl` in `Filesystem.Axioms` with a CI
117-
allow-list guard. `equivReflProof` closed as proof-of-concept. The
118-
axioms are operationally true and gated; soundness audit trail
119-
preserved via the `IDRIS2_AXIOMS.a2ml` registry.
120-
121-
**Blocker 2 (`all`/`foldMap` reduction) — DISCOVERED.** Attempting to
122-
close `equivTrans` in the same session revealed a second, independent
123-
problem: **`all p (x :: rest)` does NOT reduce to `(p x && all p rest)`
124-
by `Refl` in Idris2 0.8.0.** The `all` definition elaborates through
125-
`foldMap @{All}` — even though `foldMap`'s default body is `foldr`-
126-
based, the elaborator produces a `foldl`-shaped term that neither
127-
`Refl` nor any straightforward rewrite can directly destructure into
128-
the textbook `&&`-chain. Empirical witness:
129-
`example : all p (x :: rs) = (p x && all p rs) ; example = Refl`
130-
fails to typecheck — the unifier reports
131-
`foldl ... (neutral <+> p x) rs` on one side, `p x && Delay (all p rs)`
132-
on the other.
133-
134-
Consequently, **`equivTrans`, `cnoWriteSameContent`, and the 7
135-
reversibility theorems** are still blocked. The primitive-eq axioms
136-
unblock the LEAF reflexivity step but cannot bridge the foldMap-shaped
137-
reduction wall.
138-
139-
Three closure paths for blocker 2 (owner-decision required):
140-
141-
1. **Replace `equiv` with a structural `myAll`-based definition** that
142-
reduces by `Refl`. Touches the `equiv` shape but contained to
143-
`Model.idr`. Probably 1 PR.
144-
2. **Prove `allCons : all p (x :: rs) = (p x && all p rs)` via a chain
145-
of `foldl` lemmas** — `foldlAndAccTrue` + `foldlAndFalseStays` +
146-
careful with-clauses. Pure mathematics but ~50 lines of fiddly
147-
proof engineering against an opaque elaboration order.
148-
3. **Migrate `equiv` to a propositional `All`-based shape** (via
149-
`Data.List.Quantifiers.All`) — cleanest mathematically but ripples
150-
through every call-site of `equiv`.
151-
152-
Until one of these lands, the following holes remain frozen even with
153-
the axiom infrastructure live:
154-
155-
- `equivTransProof` (Model.idr:353)
116+
#### Priority 2 — primitive-eq groundwork (foundational, owner-decision required)
117+
118+
Every remaining tractable hole reduces to a `(s == s) = True` step on
119+
opaque `String` or `Bits8` — Idris2 0.8.0 only reduces these on
120+
literals. `DecEq Path` does NOT help because it transitively depends
121+
on `DecEq String`, which itself depends on primitive `==`.
122+
123+
Three closure paths, each requiring owner sign-off:
124+
125+
1. **Add `String` / `Bits8` reflexivity axioms** — `axStringEqRefl :
126+
(s : String) -> (s == s) = True := believe_me Refl`, gated by CI
127+
allow-list (per the Cat-D `believe_me` pattern). Smallest change,
128+
but introduces `believe_me` into the proof system which prior
129+
sessions explicitly avoided.
130+
2. **Migrate `Path` to a structural representation** — replace
131+
`String`-component paths with `Nat`-encoded interned identifiers.
132+
`Nat == Nat` IS reducible on opaque values. Bigger migration but
133+
no `believe_me`.
134+
3. **Reformulate every blocked theorem to use `decEq`-style branches**
135+
rather than `==`-style booleans. Avoids touching the `Eq` instance
136+
but ripples through ~20 theorem statements.
137+
138+
Until one path is chosen, the following holes are **frozen**:
139+
140+
- `equivReflProof` (Model.idr:216)
141+
- `equivTransProof` (Model.idr:244)
156142
- `cnoWriteSameContentProof` (Operations.idr:254)
157143
- 4 `?XXXPrfAfter` sub-holes in Operations.idr
158144
- 7 reversibility theorems in Operations.idr (mkdirRmdir, rmdirMkdir,
159145
touchRm, rmTouch, writeFile, operationIndependence,
160146
cnoWriteSameContent)
161147

162148
Separately, `undoRedoIdentityProof` and `undoRedoCompositionProof`
163-
still need a Cat-A redesign (missing `isReversible op = True`
164-
precondition; provably refuted for non-reversible `op`) before either
165-
blocker is relevant.
149+
need a Cat-A redesign (missing `isReversible op = True` precondition;
150+
provably refuted for non-reversible `op`) before primitive-eq is even
151+
relevant.
166152

167153
#### Priority 3 — Tier-S foundational (research-level)
168154

‎proofs/idris2/src/Filesystem/RMO.idr‎

Lines changed: 68 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -109,59 +109,25 @@ secureDeleteNotInjective :
109109
secureDeleteNotInjective p fs1 fs2 _ _ agreeOff =
110110
removeEntryDeterminedByFilter p fs1 fs2 agreeOff
111111

112-
||| No universal recovery function exists for overwrite.
112+
||| Overwriting data makes original irrecoverable
113113
|||
114-
||| The prior signature `recovery randomData = Nothing` was a non-theorem:
115-
||| refuted by `recovery = Just` (returns `Just randomData ≠ Nothing`).
116-
||| See issue #129 for the refutation detail.
117-
|||
118-
||| The honest claim — and the one the "information-theoretic security"
119-
||| narrative actually intends — is a **non-existence** statement: no
120-
||| function `recovery : FileContent -> Maybe FileContent` can act as a
121-
||| universal inverse to overwrite. That is, there is no `recovery` such
122-
||| that for every original content `orig` shorter than every random
123-
||| overwrite `rand`, `recovery rand = Just orig`.
124-
|||
125-
||| Closure: exhibit a counter-witness. Two distinct origins
126-
||| (`[]` and `[0]`) and a single `rand` (`[0]`) both satisfy the LTE
127-
||| precondition. If a universal recovery existed, it would have to return
128-
||| both `Just []` and `Just [0]` from the same input — contradiction via
129-
||| injectivity of `Just`.
130-
|||
131-
||| Mirrors the #60 / #61 / #119A precedent: redesign a non-theorem
132-
||| signature into a theorem-shape-correct claim rather than discharge it
133-
||| with `believe_me`.
134-
|||
135-
||| The Path / Filesystem context is preserved as named arguments so the
136-
||| theorem still cites the operation being witnessed; `p` and `fs` do not
137-
||| influence the refutation (any path, any filesystem state — the
138-
||| counter-witness depends only on `recovery`).
114+
||| After overwriting with random data, the original content cannot be
115+
||| recovered (information-theoretic security).
139116
export
140117
overwriteIrreversible :
141118
(p : Path) ->
119+
(originalContent : FileContent) ->
120+
(randomData : FileContent) ->
142121
(fs : Filesystem) ->
143-
Not ((recovery : FileContent -> Maybe FileContent) ->
144-
(orig : FileContent) ->
145-
(rand : FileContent) ->
146-
LTE (length orig) (length rand) ->
147-
recovery rand = Just orig)
148-
overwriteIrreversible p fs universal =
149-
let -- Pick any concrete recovery; the choice is irrelevant since the
150-
-- contradiction is derived from `universal`'s two competing
151-
-- conclusions on the same `rand` input.
152-
r : FileContent -> Maybe FileContent
153-
r = \_ => Nothing
154-
-- length [] = 0 <= 1 = length [0]
155-
eqEmpty : r [0] = Just []
156-
eqEmpty = universal r [] [0] LTEZero
157-
-- length [0] = 1 <= 1 = length [0]
158-
eqOne : r [0] = Just [0]
159-
eqOne = universal r [0] [0] (LTESucc LTEZero)
160-
-- Therefore Just [] = Just [0], which is impossible.
161-
bad : Just (the FileContent []) = Just (the FileContent [0])
162-
bad = trans (sym eqEmpty) eqOne
163-
in case bad of
164-
Refl impossible
122+
LTE (length originalContent) (length randomData) ->
123+
-- After overwrite, original is irrecoverable
124+
(recovery : FileContent -> Maybe FileContent) ->
125+
recovery randomData = Nothing -- Cannot recover original
126+
overwriteIrreversible p orig rand fs lenPrf recovery =
127+
-- Information-theoretically secure:
128+
-- random data of sufficient length destroys all information
129+
-- about the original
130+
?overwriteIrreversibleProof
165131

166132
--------------------------------------------------------------------------------
167133
-- GDPR Compliance
@@ -293,12 +259,60 @@ appendOnlyAuditLog :
293259
appendAuditEntry log entry = log ++ [entry]
294260
appendOnlyAuditLog log entry = Refl
295261

296-
||| Audit log provides complete history of obliterations
262+
||| `Elem` is preserved by right-appending the element itself.
263+
|||
264+
||| Pure list lemma — the appended item always lives at the end of
265+
||| the new list. Proof by straightforward induction on the prefix.
266+
|||
267+
||| Idris2 0.8.0 base does not ship this lemma directly; the closest
268+
||| stdlib helper is `Data.List.Elem.elemMap` (membership lifted
269+
||| through `map`), which we use as the second step of the audit
270+
||| completeness proof below.
271+
elemAppRightSelf : (xs : List a) -> (x : a) -> Elem x (xs ++ [x])
272+
elemAppRightSelf [] _ = Here
273+
elemAppRightSelf (_ :: ys) x = There (elemAppRightSelf ys x)
274+
275+
||| Audit log completeness — every path inserted via the official
276+
||| append-only constructor appears in the resulting log.
277+
|||
278+
||| Replaces the previous non-theorem signature
279+
|||
280+
||| auditTrailCompleteness :
281+
||| (entries : List AuditEntry) ->
282+
||| (p : Path) ->
283+
||| (obliterated : ObliterationProof p) ->
284+
||| Elem p (map AuditEntry.path entries)
285+
|||
286+
||| which was provably false (refuted by `entries = []`: an
287+
||| `ObliterationProof` for any `p` exists by `MkObliterationProof`,
288+
||| yet the empty log contains no paths). See issue #131 for the
289+
||| design rationale (mirrors the #60 / #61 / #119A precedent:
290+
||| redesign non-theorem signatures rather than close them with
291+
||| `believe_me`).
292+
|||
293+
||| The corrected shape encodes the actual invariant: the path is
294+
||| present in the post-append log *because* it was appended via
295+
||| `appendAuditEntry`. The premise `insertedPath` witnesses the
296+
||| caller's commitment that the new entry indeed records the path
297+
||| we claim is logged.
298+
|||
299+
||| Closure path (zero new axioms):
300+
||| 1. `appendAuditEntry log entry` reduces to `log ++ [entry]` by
301+
||| the definition of `appendAuditEntry`.
302+
||| 2. `Data.List.Elem.elemMap` lifts list membership through `map`,
303+
||| giving `Elem (AuditEntry.path entry) (map AuditEntry.path
304+
||| (log ++ [entry]))`.
305+
||| 3. `elemAppRightSelf` discharges `Elem entry (log ++ [entry])`
306+
||| by induction.
307+
||| 4. The `insertedPath` equality rewrites `AuditEntry.path entry`
308+
||| to `p` in the goal.
297309
export
298310
auditTrailCompleteness :
299-
(entries : List AuditEntry) ->
311+
(log : List AuditEntry) ->
312+
(entry : AuditEntry) ->
300313
(p : Path) ->
301-
-- If p was obliterated, it's in the audit log
302-
(obliterated : ObliterationProof p) ->
303-
Elem p (map AuditEntry.path entries) -- p appears in the log
304-
auditTrailCompleteness entries p oblitProof = ?auditTrailCompletenessProof
314+
(insertedPath : AuditEntry.path entry = p) ->
315+
Elem p (map AuditEntry.path (appendAuditEntry log entry))
316+
auditTrailCompleteness log entry p insertedPath =
317+
rewrite sym insertedPath in
318+
elemMap AuditEntry.path (elemAppRightSelf log entry)

0 commit comments

Comments
 (0)