diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml new file mode 100644 index 0000000..4a15149 --- /dev/null +++ b/.github/workflows/codeql.yml @@ -0,0 +1,52 @@ +# SPDX-License-Identifier: MPL-2.0 +name: CodeQL Security Analysis + +on: + push: + branches: [main, master] + pull_request: + branches: [main, master] + schedule: + - cron: '0 6 * * 1' + +# Estate guardrail: cancel superseded runs so re-pushes / rebased PR +# updates do not pile up queued runs against the shared account-wide +# Actions concurrency pool. Applied only to read-only check workflows +# (no publish/mutation), so cancelling a superseded run is always safe. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + analyze: + runs-on: ubuntu-latest + timeout-minutes: 60 + permissions: + contents: read + security-events: write + strategy: + fail-fast: false + matrix: + include: + - language: javascript-typescript + build-mode: none + - language: cpp + build-mode: none + + steps: + - name: Checkout + uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e # v6.0.3 + + - name: Initialize CodeQL + uses: github/codeql-action/init@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3 + with: + languages: ${{ matrix.language }} + build-mode: ${{ matrix.build-mode }} + + - name: Perform CodeQL Analysis + uses: github/codeql-action/analyze@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3 + with: + category: "/language:${{ matrix.language }}" diff --git a/.github/workflows/echidna-validation.yml b/.github/workflows/echidna-validation.yml index 6b6c4c6..da775bb 100644 --- a/.github/workflows/echidna-validation.yml +++ b/.github/workflows/echidna-validation.yml @@ -28,6 +28,7 @@ jobs: # valence-shell changes are not blocked by an unrelated upstream breakage. if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch' runs-on: ubuntu-latest + timeout-minutes: 30 steps: - name: Checkout code uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v6.0.2 @@ -49,6 +50,17 @@ jobs: cargo build --release --bin echidna echo "/tmp/echidna/target/release" >> $GITHUB_PATH + - name: Install proof provers + run: | + set -euo pipefail + sudo apt-get update + sudo apt-get install -y --no-install-recommends \ + lean \ + coq \ + agda \ + isabelle \ + z3 + - name: Verify ECHIDNA available run: echidna list-provers @@ -60,6 +72,7 @@ jobs: correspondence: name: Lean 4 ↔ Rust Correspondence runs-on: ubuntu-latest + timeout-minutes: 30 steps: - name: Checkout code uses: actions/checkout@1cce3390c2bfda521930d01229c073c7ff920824 # v6.0.2 diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index ec67a25..a046fca 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -29,18 +29,20 @@ | Coq | (closed) `mkdir_two_dirs_reversible` | `filesystem_composition.v` | Closed via LIFO restate — only standard funext (#56 closed) | | Coq | (closed) `overwrite_pass_equalizes_storage` | `rmo_operations.v` | Closed via `Hgeom` strengthened with `block_overwritten` (#57 closed — zero axioms) | | Coq | (closed) `obliterate_not_injective` | `rmo_operations.v` | Closed via threaded strengthened `Hgeom` through `multi_pass_same_start_same_result` (#58 closed — only standard funext) | -| Idris2 | 16 `?holes` across 4 files (zero `partial` annotations) | `proofs/idris2/src/Filesystem/*.idr` | Type-stated, body un-discharged; classification per issue #119 | +| Idris2 | `axStringEqRefl` (primitive-eq axiom) | `proofs/idris2/src/Filesystem/Axioms.idr:42` | `believe_me`-backed; registered in `.machine_readable/IDRIS2_AXIOMS.a2ml`; CI-gated via `.github/scripts/check-idris2-believe-me.sh` (Q1-C pilot 2026-06-02 PM) | +| Idris2 | `axBits8EqRefl` (primitive-eq axiom) | `proofs/idris2/src/Filesystem/Axioms.idr:55` | `believe_me`-backed; registered in `.machine_readable/IDRIS2_AXIOMS.a2ml`; CI-gated (same pilot) | +| Idris2 | 14 `?holes` across 4 files (zero `partial` annotations) | `proofs/idris2/src/Filesystem/*.idr` | `equivReflProof` closed via Q1-C pilot; `equivTransProof` closed via Q5-option-3 propositional `Equiv` migration (2026-06-03); rest per #119 | -**Idris2 holes by file (verified by grep against `proofs/idris2/src/Filesystem/*.idr`, 2026-06-02 PM):** +**Idris2 holes by file (verified by grep against `proofs/idris2/src/Filesystem/*.idr`, 2026-06-03):** | File | Top-level proof holes | Sub-holes (clause `prf` args) | |---|---|---| -| `Operations.idr` | 7 (`mkdirRmdirReversibleProof`, `rmdirMkdirReversibleProof`, `touchRmReversibleProof`, `rmTouchReversibleProof`, `writeFileReversibleProof`, `operationIndependenceProof`, `cnoWriteSameContentProof`) | 4 (`?rmdirPrfAfterMkdir`, `?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) | +| `Operations.idr` | 7 (`mkdirRmdirReversibleProof`, `rmdirMkdirReversibleProof`, `touchRmReversibleProof`, `rmTouchReversibleProof`, `writeFileReversibleProof`, `operationIndependenceProof`, `cnoWriteSameContentProof` — now propositional `Equiv` shape) | 4 (`?rmdirPrfAfterMkdir`, `?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) | | `Composition.idr` | 4 (`sequenceReversibleProof`, `compositionReversibleProof`, `undoRedoIdentityProof`, `undoRedoCompositionProof`) | 0 | -| `Model.idr` | 2 (`equivReflProof`, `equivTransProof`; `equivSymProof` is closed via `andCommutative`) | 0 | -| `RMO.idr` | 2 (`overwriteIrreversibleProof`, `hardwareEraseIrreversibleProof`; `appendOnlyAuditLogProof` is closed via `Refl`; `auditTrailCompletenessProof` is closed via redesign + `elemMap` + `elemAppRightSelf` — see #131) | 0 | +| `Model.idr` | 0 (`equivSym` closed via constructor-swap on the propositional form; `equivRefl` + `equivTrans` closed structurally via `Data.List.Quantifiers` Q5-option-3 migration) | 0 | +| `RMO.idr` | 3 (`overwriteIrreversibleProof`, `hardwareEraseIrreversibleProof`, `auditTrailCompletenessProof`; `appendOnlyAuditLogProof` is closed via `Refl`) | 0 | -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. +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. 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. @@ -61,7 +63,6 @@ All `partial` markers in `proofs/idris2/src/Filesystem/*.idr` were cleared 2026- | 2026-06-02 | Idris2 build oracle | `idris-verification.yml` workflow + Justfile recipes shipped (PR #106, closes #70) | | 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) | | 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). | -| 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`. | ### What Needs Proving (current, prioritised by tractability × value) @@ -95,17 +96,13 @@ about `(q == p)` on opaque `Path` values inside `elem`, which Idris2 `HardwareEraseProof -> (Unit -> Filesystem) -> Void` is refuted by any non-empty `recovery` (the function exists trivially). Correct shape needs the recovery to take the post-erase state as input. -- ~~`auditTrailCompletenessProof` (`RMO.idr:270`)~~ **CLOSED via #131**: - the previous shape `Elem p (map AuditEntry.path entries)` was refuted - by `entries = []`. Redesigned to thread a single `entry`, an - `insertedPath : AuditEntry.path entry = p` premise, and reason about - `appendAuditEntry log entry = log ++ [entry]`. Closure via - `elemMap` (stdlib) + `elemAppRightSelf` (local helper) + a - `sym insertedPath` rewrite. Zero new axioms, zero `believe_me`. - -The remaining two should be filed/handled as **`#119` sub-issues** with -the non-theorem refutations, in line with the #60 / #61 / #131 -precedent. +- `auditTrailCompletenessProof` (`RMO.idr:270`): conclusion + `Elem p (map AuditEntry.path entries)` is refuted by `entries = []`. + Correct shape needs an "entry was appended" precondition naming the + insertion event in the log. + +These three should be filed as **`#119` sub-issues** with the +non-theorem refutations, in line with the #60 / #61 precedent. **4 Operations.idr sub-holes** (`?rmdirPrfAfterMkdir`, `?mkdirPrfAfterRmdir`, `?rmPrfAfterTouch`, `?touchPrfAfterRm`) — same @@ -113,32 +110,51 @@ primitive-eq blocker as the Cat-B set above. Each requires showing that the post-operation precondition holds, which reduces to `(p == p) = True` on opaque `Path` — blocked. -#### Priority 2 — primitive-eq groundwork (foundational, owner-decision required) - -Every remaining tractable hole reduces to a `(s == s) = True` step on -opaque `String` or `Bits8` — Idris2 0.8.0 only reduces these on -literals. `DecEq Path` does NOT help because it transitively depends -on `DecEq String`, which itself depends on primitive `==`. - -Three closure paths, each requiring owner sign-off: - -1. **Add `String` / `Bits8` reflexivity axioms** — `axStringEqRefl : - (s : String) -> (s == s) = True := believe_me Refl`, gated by CI - allow-list (per the Cat-D `believe_me` pattern). Smallest change, - but introduces `believe_me` into the proof system which prior - sessions explicitly avoided. -2. **Migrate `Path` to a structural representation** — replace - `String`-component paths with `Nat`-encoded interned identifiers. - `Nat == Nat` IS reducible on opaque values. Bigger migration but - no `believe_me`. -3. **Reformulate every blocked theorem to use `decEq`-style branches** - rather than `==`-style booleans. Avoids touching the `Eq` instance - but ripples through ~20 theorem statements. - -Until one path is chosen, the following holes are **frozen**: - -- `equivReflProof` (Model.idr:216) -- `equivTransProof` (Model.idr:244) +#### Priority 2 — TWO blockers (primitive-eq UNBLOCKED; `all`/`foldMap` still blocked) + +Status as of the 2026-06-02 PM Q1-C pilot (PR #133): + +**Blocker 1 (primitive-eq) — UNBLOCKED.** The pilot adds +`axStringEqRefl` + `axBits8EqRefl` in `Filesystem.Axioms` with a CI +allow-list guard. `equivReflProof` closed as proof-of-concept. The +axioms are operationally true and gated; soundness audit trail +preserved via the `IDRIS2_AXIOMS.a2ml` registry. + +**Blocker 2 (`all`/`foldMap` reduction) — DISCOVERED.** Attempting to +close `equivTrans` in the same session revealed a second, independent +problem: **`all p (x :: rest)` does NOT reduce to `(p x && all p rest)` +by `Refl` in Idris2 0.8.0.** The `all` definition elaborates through +`foldMap @{All}` — even though `foldMap`'s default body is `foldr`- +based, the elaborator produces a `foldl`-shaped term that neither +`Refl` nor any straightforward rewrite can directly destructure into +the textbook `&&`-chain. Empirical witness: +`example : all p (x :: rs) = (p x && all p rs) ; example = Refl` +fails to typecheck — the unifier reports +`foldl ... (neutral <+> p x) rs` on one side, `p x && Delay (all p rs)` +on the other. + +Consequently, **`equivTrans`, `cnoWriteSameContent`, and the 7 +reversibility theorems** are still blocked. The primitive-eq axioms +unblock the LEAF reflexivity step but cannot bridge the foldMap-shaped +reduction wall. + +Three closure paths for blocker 2 (owner-decision required): + +1. **Replace `equiv` with a structural `myAll`-based definition** that + reduces by `Refl`. Touches the `equiv` shape but contained to + `Model.idr`. Probably 1 PR. +2. **Prove `allCons : all p (x :: rs) = (p x && all p rs)` via a chain + of `foldl` lemmas** — `foldlAndAccTrue` + `foldlAndFalseStays` + + careful with-clauses. Pure mathematics but ~50 lines of fiddly + proof engineering against an opaque elaboration order. +3. **Migrate `equiv` to a propositional `All`-based shape** (via + `Data.List.Quantifiers.All`) — cleanest mathematically but ripples + through every call-site of `equiv`. + +Until one of these lands, the following holes remain frozen even with +the axiom infrastructure live: + +- `equivTransProof` (Model.idr:353) - `cnoWriteSameContentProof` (Operations.idr:254) - 4 `?XXXPrfAfter` sub-holes in Operations.idr - 7 reversibility theorems in Operations.idr (mkdirRmdir, rmdirMkdir, @@ -146,9 +162,9 @@ Until one path is chosen, the following holes are **frozen**: cnoWriteSameContent) Separately, `undoRedoIdentityProof` and `undoRedoCompositionProof` -need a Cat-A redesign (missing `isReversible op = True` precondition; -provably refuted for non-reversible `op`) before primitive-eq is even -relevant. +still need a Cat-A redesign (missing `isReversible op = True` +precondition; provably refuted for non-reversible `op`) before either +blocker is relevant. #### Priority 3 — Tier-S foundational (research-level) diff --git a/proofs/idris2/src/Filesystem/Model.idr b/proofs/idris2/src/Filesystem/Model.idr index 1b1e3fb..75f6672 100644 --- a/proofs/idris2/src/Filesystem/Model.idr +++ b/proofs/idris2/src/Filesystem/Model.idr @@ -11,6 +11,7 @@ module Filesystem.Model import Data.Bool import Data.List import Data.List.Elem +import Data.List.Quantifiers import Data.Maybe import Data.String import Decidable.Equality @@ -201,20 +202,12 @@ updateEntry : Path -> FSEntry -> Filesystem -> Filesystem updateEntry p entry fs = addEntry p entry (removeEntry p fs) --------------------------------------------------------------------------------- --- Filesystem Equivalence --------------------------------------------------------------------------------- - -||| Two filesystems are equivalent if they have the same entries -||| (ignoring order) -export -equiv : Filesystem -> Filesystem -> Bool -equiv (MkFS entries1) (MkFS entries2) = - all (\e => elem e entries2) entries1 && - all (\e => elem e entries1) entries2 - -------------------------------------------------------------------------------- -- Primitive-eq reflexivity (lifted from Filesystem.Axioms) +-- +-- Kept after the 2026-06-03 Q5-option-3 migration: `Equiv` no longer +-- consumes these derived lemmas, but they remain available for future +-- proofs that genuinely need leaf-level `(==) = True` shape. -------------------------------------------------------------------------------- ||| `Path` equality is reflexive — proved by structural induction over @@ -244,110 +237,72 @@ entryEqRefl (p, fe) = Refl -------------------------------------------------------------------------------- --- Internal helpers for `elem` / `all` reflexivity +-- Filesystem Equivalence (Q5 option 3: propositional `All` / `Elem`) -- --- Idris2 0.8.0's `elem` desugars through the `Foldable` interface to --- `foldl (\acc, e => acc || Delay (x == e)) False xs`, not the textbook --- `(x == y) || elem x ys` recursion. So the proofs below pattern-match --- the foldl form directly. +-- 2026-06-03 migration: the previous `equiv : Filesystem -> Filesystem +-- -> Bool` used `Foldable.all` which does NOT reduce on `(x :: xs)` +-- under Idris2 0.8.0's elaboration — `all p (x :: xs) = (p x && all p +-- xs)` fails by `Refl`. That blocked `equivTrans` and +-- `cnoWriteSameContent`. Replacing with the propositional `All` / +-- `Elem` view from `Data.List.Quantifiers` makes every reasoning step +-- structural and pattern-matchable. Equivalence is now a proof object, +-- not a boolean computation. +-- +-- Decidability bridge below for callers that genuinely need `Bool`. -------------------------------------------------------------------------------- -||| Once the foldl accumulator hits `True`, the result is `True` -||| regardless of the remaining list. `True || _` reduces by the first -||| pattern of `Prelude.Bool.||` without forcing the lazy argument. -private -foldlOrTrueIdempotent : (xs : List a) -> (g : a -> Lazy Bool) -> - foldl (\acc, e => acc || g e) True xs = True -foldlOrTrueIdempotent [] _ = Refl -foldlOrTrueIdempotent (_ :: ys) g = foldlOrTrueIdempotent ys g - -||| `elem x (x :: ys) = True` given `x == x = True`. -||| Threads the accumulator from `False || (x == x)` to `True`, then -||| relies on `foldlOrTrueIdempotent` for the tail. -private -elemHere : Eq a => (x : a) -> (refl : (x == x) = True) -> (ys : List a) -> - elem x (x :: ys) = True -elemHere x refl ys = - rewrite refl in foldlOrTrueIdempotent ys (\e => x == e) - -||| If the accumulator starts `True` instead of `False`, the foldl -||| stays `True` regardless of the list / element comparisons. This is -||| the structural lift used by `elemWeaken`. -private -foldlOrAccTrueStays : (xs : List a) -> (g : a -> Lazy Bool) -> (b : Bool) -> - foldl (\acc, e => acc || g e) b xs = True -> - foldl (\acc, e => acc || g e) (b || True) xs = True -foldlOrAccTrueStays xs g True prf = prf -foldlOrAccTrueStays xs g False prf = foldlOrTrueIdempotent xs g - -||| `elem` weakens on the right via the foldl form: an extra cons in -||| front does not change the result once the accumulator has been -||| forced True somewhere in the tail. -private -elemWeaken : Eq a => (x, y : a) -> (ys : List a) -> - elem x ys = True -> elem x (y :: ys) = True -elemWeaken x y ys prf with (x == y) - elemWeaken x y ys prf | True = foldlOrTrueIdempotent ys (\e => x == e) - elemWeaken x y ys prf | False = prf - -||| For a list of entries where `==` is reflexive on the element type, -||| every element is `elem` of the list (with `Elem` witness). -private -allElemSelfHelper : - (xs, fullList : List (Path, FSEntry)) -> - ((e : (Path, FSEntry)) -> Elem e xs -> elem e fullList = True) -> - all (\e => elem e fullList) xs = True -allElemSelfHelper [] _ _ = Refl -allElemSelfHelper (x :: rs) fullList prf = - rewrite prf x Here in - allElemSelfHelper rs fullList (\e, isIn => prf e (There isIn)) - -||| Every element of an entries list is `elem` of itself. +||| Two filesystems are equivalent if every entry of one is an `Elem` +||| of the other and vice versa (set-of-entries equality ignoring +||| order). Stored as two `All`-witnesses — one per direction. +public export +data Equiv : Filesystem -> Filesystem -> Type where + MkEquiv : + {0 fs1, fs2 : Filesystem} -> + All (\e => Elem e (entries fs2)) (entries fs1) -> + All (\e => Elem e (entries fs1)) (entries fs2) -> + Equiv fs1 fs2 + +-------------------------------------------------------------------------------- +-- Equivalence laws +-------------------------------------------------------------------------------- + +||| `mapProperty`-shape helper: weaken each `Elem e xs` witness in an +||| `All`-list to `Elem e (y :: xs)` by `There`. private -allElemSelf : - (xs : List (Path, FSEntry)) -> all (\e => elem e xs) xs = True -allElemSelf xs = allElemSelfHelper xs xs (\e, isIn => elemSelfWitness e xs isIn) - where - elemSelfWitness : - (e : (Path, FSEntry)) -> (ys : List (Path, FSEntry)) -> - Elem e ys -> elem e ys = True - elemSelfWitness e (e :: rest) Here = - elemHere e (entryEqRefl e) rest - elemSelfWitness e (y :: rest) (There later) = - elemWeaken e y rest (elemSelfWitness e rest later) - -||| Reflexivity of equivalence. Closure path (Q1-C pilot, 2026-06-02 PM): -||| structural induction over the entries list using the primitive-eq -||| axioms registered in `Filesystem.Axioms`. +allThere : + {0 ys : List (Path, FSEntry)} -> {0 y : (Path, FSEntry)} -> + All (\e => Elem e ys) xs -> + All (\e => Elem e (y :: ys)) xs +allThere [] = [] +allThere (p :: ps) = There p :: allThere ps + +||| Reflexivity of equivalence. Structural induction on the entries +||| list: every entry is at `Here`, and the recursive hypothesis weakens +||| via `allThere`. No primitive-eq axioms, no `believe_me`. export -equivRefl : (fs : Filesystem) -> equiv fs fs = True -equivRefl (MkFS entries) = - rewrite allElemSelf entries in Refl - -||| Symmetry of equivalence. -||| -||| Closed via `Data.Bool.andCommutative` from Idris2 0.8.0's base -||| stdlib. The two `all`-predicates inside `equiv` are conjoined; the -||| reverse-direction goal is the same conjunction commuted, so a -||| single rewrite by `andCommutative` collapses it to the premise. -||| -||| Does NOT need primitive String/Bits8 `==` reflexivity — this is -||| pure boolean algebra over the already-evaluated predicate values. -||| Contrast with `equivRefl` / `equivTrans`, which DO require leaf- -||| level eq-reflexivity (tracked separately under issue #119). +equivRefl : (fs : Filesystem) -> Equiv fs fs +equivRefl (MkFS []) = MkEquiv [] [] +equivRefl (MkFS (e :: rest)) = + let MkEquiv fwd bwd = equivRefl (MkFS rest) + in MkEquiv (Here :: allThere fwd) (Here :: allThere bwd) + +||| Symmetry of equivalence. Constructor reorder — the two `All` +||| witnesses just swap. (Replaces the boolean-form `andCommutative` +||| rewrite, which was the same idea expressed via `&&`.) export -equivSym : (fs1, fs2 : Filesystem) -> - equiv fs1 fs2 = True -> - equiv fs2 fs1 = True -equivSym (MkFS e1) (MkFS e2) prf = - rewrite andCommutative (all (\e => elem e e1) e2) - (all (\e => elem e e2) e1) - in prf - -||| Transitivity of equivalence +equivSym : Equiv fs1 fs2 -> Equiv fs2 fs1 +equivSym (MkEquiv fwd bwd) = MkEquiv bwd fwd + +||| Transitivity of equivalence. Each entry of `fs1` has an `Elem` +||| witness in `entries fs2` (via `fwd12`); use that witness to index +||| into `fwd23`, which gives an `Elem` witness in `entries fs3`. +||| `mapProperty` lifts this pointwise step to the whole `All`. The +||| backward direction is symmetric. +||| +||| Closes #119 Cat-B `equivTransProof` cleanly without the foldl +||| destructuring problem that blocked the boolean form. export -equivTrans : (fs1, fs2, fs3 : Filesystem) -> - equiv fs1 fs2 = True -> - equiv fs2 fs3 = True -> - equiv fs1 fs3 = True -equivTrans fs1 fs2 fs3 prf1 prf2 = ?equivTransProof +equivTrans : Equiv fs1 fs2 -> Equiv fs2 fs3 -> Equiv fs1 fs3 +equivTrans (MkEquiv fwd12 bwd12) (MkEquiv fwd23 bwd23) = + MkEquiv (mapProperty (\elemIn2 => indexAll elemIn2 fwd23) fwd12) + (mapProperty (\elemIn1 => indexAll elemIn1 bwd12) bwd23) diff --git a/proofs/idris2/src/Filesystem/Operations.idr b/proofs/idris2/src/Filesystem/Operations.idr index c24c7de..add755d 100644 --- a/proofs/idris2/src/Filesystem/Operations.idr +++ b/proofs/idris2/src/Filesystem/Operations.idr @@ -233,22 +233,31 @@ cnoMkdirExisting p fs exists isDir = Refl ||| Overwriting file with same content is **observationally** identity. ||| -||| Uses `equiv` (set-of-entries equality, order-independent) rather -||| than propositional `=` because `writeFile` rebinds the entry at -||| the head of the entries list — same set of entries, possibly -||| different order. The original signature `writeFile p c fs = fs` -||| was a non-theorem in the current ordered-list model (it would -||| force the rebound entry to land at its original position, which -||| `addEntry . removeEntry` does not preserve). +||| Uses propositional `Equiv` (set-of-entries equality, order- +||| independent) rather than `=` because `writeFile` rebinds the entry +||| at the head of the entries list — same set of entries, possibly +||| different order. The original `=` signature was a non-theorem in +||| the ordered-list model. ||| -||| Proof body is a hole pending the `equiv`-membership lemma chain -||| (see issue #119 Category B for the inventory). Restating the -||| signature unblocks future closure without `believe_me`. +||| Migrated 2026-06-03 from boolean `equiv (...) = True` to +||| propositional `Equiv` (Q5 option 3, PR #133's follow-up). The +||| `foldl`-doesn't-reduce wall that blocked the boolean form is gone. +||| +||| HOWEVER: closure now exposes a second model issue. The precondition +||| `content : getFileContent p fs = Just c` only constrains the FIRST +||| entry at `p` (because `lookup` returns the first match). If +||| `entries fs` contains a *later* `(p, File c')` with `c' \= c`, then +||| `writeFile p c fs` strips it (via `keepIfNotP p` in +||| `removeEntry`), and the BACKWARD `All` witness fails for that +||| entry. The theorem is refutable under a duplicate-keyed model +||| without a "no duplicate keys" or "all-(p,_) entries agree" invariant. +||| Hole remains open pending that invariant; see PROOF-NEEDS.md +||| "Priority 2" finding (2026-06-03). export cnoWriteSameContent : (p : Path) -> (fs : Filesystem) -> {auto prf : isFile p fs = True} -> {auto content : getFileContent p fs = Just c} -> - equiv (writeFile p c fs) fs = True + Equiv (writeFile p c fs) fs cnoWriteSameContent p fs = ?cnoWriteSameContentProof