diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..a01f31d --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +*.olean +.lake/ diff --git a/KNOWN-GAPS.md b/KNOWN-GAPS.md index f327129..2d4da14 100644 --- a/KNOWN-GAPS.md +++ b/KNOWN-GAPS.md @@ -10,10 +10,18 @@ list is COMPLETE, not merely that the items are acceptable. Matches the paper (its Theorem 1 is inclusion-only); honest consistency behavior is covered by the fidelity harness's honest cases (164,224-case agreement with the deployed verifier). -3. **Lemma 2, path instance not restored** — receipt-uniqueness for - `Root` (an accepting `(v,P)` is the honest receipt) was removed with - the vacuous `root_binding` and not re-proven in extractor form. - Optional: unused by Theorems 2–3 as assembled. +3. **Lemma 2 is mechanized as specializations, not as one general + theorem.** The paper's Lemma 2 is a single statement quantified over + an abstract hash-fold `F` and a connected subtree `S`. The corpus has + no hash-fold datatype/predicate; it proves the needed instances + directly — whole-tree (`extractMTH_correct`), ConsRec + (`consRecBinding`), inclusion (`extractIncl_correct`), and the width + fact (`hnode_preimage_inj`). These suffice for Theorems 2–3. Two + consequences: (a) the abstract lemma itself is not a mechanized + object; (b) the path-instance receipt-uniqueness for `Root` (removed + with the vacuous `root_binding`) is not restored — optional, unused. + Any paper claim that "Lemma 2 is mechanized" must read "its + specializations sufficient for Theorems 2–3 are mechanized." 4. **Signature layer abstract** — Ed25519 EUF-CMA, the poison/evidence retention state, and transferability of fork evidence (paper Prop 1(2)) are not modeled; `fork_distinct` is the Merkle-layer share only. @@ -33,3 +41,20 @@ list is COMPLETE, not merely that the items are acceptable. code. No theorem was affected (kernel-checked throughout); pins were corrected, the audit surface defined, and the standing rule is now: exit code + ALL GREEN, cones read from #print axioms only. + +9. **Asymptotic cost not mechanized.** Paper Theorems 2 and 3 assert the + extractors run in `O(n)` / `O(n₁)` hash evaluations. The mechanization + proves functional correctness of the named extractors only — no cost + semantics, recurrence, or computability-after-hash-instantiation. (The + extractors are `noncomputable` over the opaque `sha256`.) +10. **Pin-store initialization from the empty pin not modeled**, and + `pin_prefix_correct` assumes `0 < n`. Trust-on-first-use / the size-0 + initial state is a separate operation; the theorems cover transitions + from a positive-size pin. (Related to gap 7's per-step scoping.) +11. **acceptIncl now named (was review F1).** The consumer's inclusion + acceptance `m < n ∧ Root … = some r` is now the Lean object + `acceptIncl`, with `acceptIncl_complete`/`acceptIncl_sound` routing + completeness/soundness through it, and the fidelity harness exercises + the out-of-range families (`m ≥ n`). `Root` alone still accepts + out-of-range `m`; that is by design (it is the reconstruction, not the + accept predicate). diff --git a/README.md b/README.md index 34d7cac..b910657 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,9 @@ the same discipline as the four `*-ed25519-verified` subject corpora. All paper-§10 mechanization targets are kernel-checked; the audit surface is defined and green (`verification/check.sh`, exit 0). See [STATEMENT-MAP.md](STATEMENT-MAP.md) for the paper↔Lean review surface and -[KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger. No changes +[KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger. Revised after review round 1 (GPT-5.6 + second Claude): audit surface +now fail-closed enforced, acceptIncl named, fidelity families extended +(230,271 / 230,016), docs reconciled. No changes until the external review round (second model instance + GPT + author) completes. The finished certificates' attestation into the LTL is a separate, explicitly-authorized operator decision. @@ -24,7 +26,7 @@ separate, explicitly-authorized operator decision. | L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) **done, non-vacuous** | | L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, WHOLE-TREE instance) **done, non-vacuous** | | — | Lemma 2, PATH instance (receipt-uniqueness of `Root`): deleted with the vacuous `root_binding` in S3.5 and **not yet restored**; optional, not needed for Theorem 3 | -| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED (faithful to ConsRec by inspection — NOT yet machine-checked); **consRecBinding PROVEN** (Theorem 3 steps 1-2, kernel-checked, no sorry); extractCons assembly (step 3 join) = S5.4 | +| L6b | **Theorem 3 (consistency soundness) DONE** — consRecBinding (steps 1-2) is the kernel-checked link between ConsRec acceptance and extractConsNode's output; extractCons/extractCons_correct (assembly, joins extractMTH); non-vacuity pinned | | L6 | pin-store state machine safety (Proposition 1) | pending | ## Discipline (identical to the subject corpora) diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md index dce195b..c1809a0 100644 --- a/STATEMENT-MAP.md +++ b/STATEMENT-MAP.md @@ -12,6 +12,8 @@ mechanization to items i–v). | §5.3 MTH | `MTH` | Basic | sha256 | | §5.3 Path | `Path` | Completeness | sha256 | | §5.3 Root (App. B) | `Root` (Option = rejection) | Basic | sha256 | +| §5.3 inclusion accept | `acceptIncl` (= `m < n ∧ Root … = some r`); `acceptIncl_complete`, `acceptIncl_sound` route Thm 1/2 through it | Basic, Completeness, Extract | sha256 (+choice) | +| Lemma 2 (general abstract form) | **not mechanized as one theorem** — proved as specializations (see KNOWN-GAPS gap 3); the row below and the Lemma-2 rows are those instances | — | — | | §5.3 ConsRec | `ConsRec` (+ machine-checked base-refactor equivalences `consRec_base_true_eq/false_eq`) | Basic, Refactor | sha256 | | Lemma 1 (domain separation) | `domsep` | Basic | **axiom-free** | | Theorem 1 (inclusion completeness) | `incl_complete` | Completeness | sha256 (+choice) | @@ -19,12 +21,18 @@ mechanization to items i–v). | Lemma 2, whole-tree instance | `extractMTH` + `extractMTH_correct` | Descent | sha256 (+choice) | | Lemma 2, ConsRec instance (Thm 3 steps 1–2) | `consRecBinding` | Binding3 | sha256 (+choice) | | Theorem 2 (inclusion soundness, explicit 𝓔) | `extractIncl` + `extractIncl_correct` | Extract | sha256 (+choice) | -| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct` | Theorem3 | sha256 (+choice) | +| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged) | Theorem3 | sha256 (+choice) | | Prop 1(1) (pin monotonicity + prefix) | `pinAccept`, `pinAccept_monotone`, `pin_prefix_correct` | PinStore | sha256 (+choice) | | Prop 1(2), Merkle share | `fork_distinct` (different roots ⇒ different content); transferability = signature layer, out of scope | PinStore | sha256 | | non-vacuity guards (anti-pigeonhole) | `extractIncl_nonvacuous`, `extractMTH_nonvacuous`, `extractCons_nonvacuous`, `pin_prefix_nonvacuous` | Extract/Descent/Theorem3/PinStore | sha256 | | definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 164,479 + 164,224 (paper's exact case set) | fidelity | (testing) | +Note on "assumption-free" (paper §10(i)): `incl_complete`'s cone lists +`LTLAcc.sha256`, but the theorem assumes **no property** of it — it +merely *mentions* the opaque constant. Constant-dependence is not +property-assumption; the soundness theorems likewise carry `sha256` +without assuming collision resistance. + Design invariant of every soundness statement: the collision is the output of a **named extractor function** and correctness is a claim about that output. A bare `∃ x y, x ≠ y ∧ sha256 x = sha256 y` is provable by diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean index c33ab76..2a35d50 100644 --- a/verification/Proofs/AxiomCheck.lean +++ b/verification/Proofs/AxiomCheck.lean @@ -63,3 +63,8 @@ import Proofs.PinStore #print axioms LTLAcc.take_append_drop #print axioms LTLAcc.instInhabitedHash #print axioms LTLAcc.instDecidableEqHash +#print axioms LTLAcc.acceptIncl +#print axioms LTLAcc.acceptIncl_complete +#print axioms LTLAcc.acceptIncl_sound +#print axioms LTLAcc.extractCons_correct_paper +#print axioms LTLAcc.Hash diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean deleted file mode 100644 index bb38c86..0000000 Binary files a/verification/Proofs/AxiomCheck.olean and /dev/null differ diff --git a/verification/Proofs/Basic.lean b/verification/Proofs/Basic.lean index 454e244..783be5e 100644 --- a/verification/Proofs/Basic.lean +++ b/verification/Proofs/Basic.lean @@ -168,4 +168,11 @@ decreasing_by def acceptCons (n₀ n₁ : Nat) (r₀ r₁ : Hash) (C : List Hash) : Prop := n₀ = 0 ∨ ConsRec n₀ n₁ C true r₀ = some (r₀, r₁) +/-- The consumer's INCLUSION acceptance predicate (paper §5.3 / Appendix B): + the `m < n` range guard is part of accept, not just a theorem hypothesis + (review F1). `Root` alone would accept out-of-range `m` at `n = 1`; this + is the object the fidelity harness's `accept_incl` mirrors. -/ +def acceptIncl (d : Bytes) (m n : Nat) (P : List Hash) (r : Hash) : Prop := + m < n ∧ Root (hleaf d) m n P = some r + end LTLAcc diff --git a/verification/Proofs/Basic.olean b/verification/Proofs/Basic.olean deleted file mode 100644 index 3825ce9..0000000 Binary files a/verification/Proofs/Basic.olean and /dev/null differ diff --git a/verification/Proofs/Binding.olean b/verification/Proofs/Binding.olean deleted file mode 100644 index fc0eade..0000000 Binary files a/verification/Proofs/Binding.olean and /dev/null differ diff --git a/verification/Proofs/Binding3.olean b/verification/Proofs/Binding3.olean deleted file mode 100644 index 290ee39..0000000 Binary files a/verification/Proofs/Binding3.olean and /dev/null differ diff --git a/verification/Proofs/Completeness.lean b/verification/Proofs/Completeness.lean index e310ac0..9a118b4 100644 --- a/verification/Proofs/Completeness.lean +++ b/verification/Proofs/Completeness.lean @@ -181,4 +181,10 @@ theorem eq_dropLast_append_of_getLast? (l : List Hash) (s : Hash) _ = a :: ((b :: u).dropLast ++ [s]) := by rw [← this] _ = (a :: b :: u).dropLast ++ [s] := by simp +/-- Completeness through the named acceptance predicate (review F1): the + honest receipt satisfies `acceptIncl`. -/ +theorem acceptIncl_complete (m : Nat) (D : List Bytes) (hm : m < D.length) : + acceptIncl (D.getD m []) m D.length (Path m D) (MTH D) := + ⟨hm, incl_complete m D hm⟩ + end LTLAcc diff --git a/verification/Proofs/Completeness.olean b/verification/Proofs/Completeness.olean deleted file mode 100644 index 753fecc..0000000 Binary files a/verification/Proofs/Completeness.olean and /dev/null differ diff --git a/verification/Proofs/Consistency.olean b/verification/Proofs/Consistency.olean deleted file mode 100644 index c8ff9c7..0000000 Binary files a/verification/Proofs/Consistency.olean and /dev/null differ diff --git a/verification/Proofs/Descent.olean b/verification/Proofs/Descent.olean deleted file mode 100644 index b44eaef..0000000 Binary files a/verification/Proofs/Descent.olean and /dev/null differ diff --git a/verification/Proofs/Extract.lean b/verification/Proofs/Extract.lean index abbf289..6764d78 100644 --- a/verification/Proofs/Extract.lean +++ b/verification/Proofs/Extract.lean @@ -208,4 +208,13 @@ theorem extractIncl_nonvacuous : intro hcol exact hcol.1 rfl +/-- Inclusion soundness through the named acceptance predicate (review F1): + if `acceptIncl` holds for a wrong leaf, `extractIncl` outputs a + collision. Ties the object the harness tests to the security theorem. -/ +theorem acceptIncl_sound (m : Nat) (D : List Bytes) (hm : m < D.length) + (d : Bytes) (P : List Hash) (hd : d ≠ D.getD m []) + (hacc : acceptIncl d m D.length P (MTH D)) : + IsCollision (extractIncl m D d P).1 (extractIncl m D d P).2 := + extractIncl_correct m D d P hm hd hacc.2 + end LTLAcc diff --git a/verification/Proofs/Extract.olean b/verification/Proofs/Extract.olean deleted file mode 100644 index 7ffd33c..0000000 Binary files a/verification/Proofs/Extract.olean and /dev/null differ diff --git a/verification/Proofs/PinStore.olean b/verification/Proofs/PinStore.olean deleted file mode 100644 index 338b462..0000000 Binary files a/verification/Proofs/PinStore.olean and /dev/null differ diff --git a/verification/Proofs/Probe.olean b/verification/Proofs/Probe.olean deleted file mode 100644 index b3d2e0b..0000000 Binary files a/verification/Proofs/Probe.olean and /dev/null differ diff --git a/verification/Proofs/ProbeAx.olean b/verification/Proofs/ProbeAx.olean deleted file mode 100644 index 4a6414b..0000000 Binary files a/verification/Proofs/ProbeAx.olean and /dev/null differ diff --git a/verification/Proofs/ProbeInduct.olean b/verification/Proofs/ProbeInduct.olean deleted file mode 100644 index f451aee..0000000 Binary files a/verification/Proofs/ProbeInduct.olean and /dev/null differ diff --git a/verification/Proofs/ProbeRefactor.olean b/verification/Proofs/ProbeRefactor.olean deleted file mode 100644 index 2ad15d2..0000000 Binary files a/verification/Proofs/ProbeRefactor.olean and /dev/null differ diff --git a/verification/Proofs/Refactor.olean b/verification/Proofs/Refactor.olean deleted file mode 100644 index c7ca473..0000000 Binary files a/verification/Proofs/Refactor.olean and /dev/null differ diff --git a/verification/Proofs/Theorem3.lean b/verification/Proofs/Theorem3.lean index 61d78ac..c403a75 100644 --- a/verification/Proofs/Theorem3.lean +++ b/verification/Proofs/Theorem3.lean @@ -64,4 +64,18 @@ theorem extractCons_nonvacuous : intro hcol exact hcol.1 rfl +/-- Theorem 3 at the paper's exact quantifiers (review M4): `n₀ ≤ n₁` + without a separate `0 < n₀`. The `n₀ = 0` case is discharged: `D₀` + has length 0 so `D₀ = [] = D₁.take 0`, contradicting `hne`. -/ +theorem extractCons_correct_paper (n₀ : Nat) (C : List Hash) (D₀ D₁ : List Bytes) + (hlen0 : D₀.length = n₀) (hle : n₀ ≤ D₁.length) + (hne : D₀ ≠ D₁.take n₀) + (hacc : ConsRec n₀ D₁.length C true (MTH D₀) = some (MTH D₀, MTH D₁)) : + IsCollision (extractCons n₀ C D₀ D₁).1 (extractCons n₀ C D₀ D₁).2 := by + rcases Nat.eq_zero_or_pos n₀ with h0 | hpos + · exfalso; apply hne + have hD0 : D₀ = [] := List.length_eq_zero_iff.mp (by omega) + rw [hD0, h0]; simp + · exact extractCons_correct n₀ C D₀ D₁ hlen0 hpos hle hne hacc + end LTLAcc diff --git a/verification/Proofs/Theorem3.olean b/verification/Proofs/Theorem3.olean deleted file mode 100644 index 01527c4..0000000 Binary files a/verification/Proofs/Theorem3.olean and /dev/null differ diff --git a/verification/check.sh b/verification/check.sh index 8d53d0d..500f7bc 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -80,8 +80,18 @@ declare -A CONES=( [LTLAcc.eq_dropLast_append_of_getLast?]="propext" [LTLAcc.instInhabitedHash]="propext" [LTLAcc.instDecidableEqHash]="" + [LTLAcc.Hash]="" + [LTLAcc.acceptIncl]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.acceptIncl_complete]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" + [LTLAcc.acceptIncl_sound]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" + [LTLAcc.extractCons_correct_paper]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" ) +# Sanctioned exclusions from the cone audit (documented, not silent): +# sha256 = THE boundary axiom (it IS the assumption) +# Bytes = bare type alias (abbrev), no cone content +declare -A EXCLUDE=( [sha256]=1 [Bytes]=1 ) + free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}' echo "=== Phase 0: source integrity ===" for f in "$HERE"/gen/LTLAcc/*.lean "$HERE"/Proofs/*.lean; do @@ -91,6 +101,10 @@ for f in "$HERE"/gen/LTLAcc/*.lean "$HERE"/Proofs/*.lean; do fi done echo " all sources valid" +for o in "$HERE"/Proofs/*.olean; do + [ -f "$o" ] || continue + [ -f "${o%.olean}.lean" ] || { echo "ORPHAN OLEAN: $o has no sibling .lean (stale artifact)"; exit 1; } +done echo "=== Phase 1: stub + axiom-smuggling audit ===" if grep -rn 'by trivial' "$HERE"/Proofs/*.lean 2>/dev/null; then @@ -152,16 +166,50 @@ for cert in "${!CONES[@]}"; do fi done rm -f "$AUD" + +# -- Phase 3b: audit-surface COVERAGE (fail-closed; review H1) -------------- +echo "=== Phase 3b: audit-surface coverage ===" +COVFAIL=0 +DECLS=$(grep -hoE "^(theorem|noncomputable def|def|abbrev) [A-Za-z0-9_?]+" \ + "$HERE"/Proofs/*.lean "$HERE"/gen/LTLAcc/*.lean | awk '{print $NF}' | sort -u) +for d in $DECLS; do + if [ -n "${CONES[LTLAcc.$d]+x}" ] || [ -n "${EXCLUDE[$d]+x}" ]; then :; else + echo " UNCLASSIFIED DECLARATION: $d (not in CONES, not a sanctioned exclusion)"; COVFAIL=1 + fi +done +# anonymous instances live only in gen/ (a controlled file); pin their count +GENINST=$(grep -cE "^instance" "$HERE"/gen/LTLAcc/*.lean) +CONEINST=$(printf '%s\n' "${!CONES[@]}" | grep -cE "LTLAcc\.inst") +if [ "$GENINST" != "$CONEINST" ]; then + echo " INSTANCE COUNT DRIFT: gen has $GENINST instances, CONES pins $CONEINST"; COVFAIL=1 +fi +# every pinned cert must actually be queried by AxiomCheck (no pin-but-never-check) +for cert in "${!CONES[@]}"; do + grep -qF "#print axioms $cert" "$HERE/Proofs/AxiomCheck.lean" || { + echo " PINNED BUT NOT QUERIED: $cert (in CONES, absent from AxiomCheck.lean)"; COVFAIL=1; } +done +[ "$COVFAIL" = 0 ] && echo " coverage complete: every declaration classified (audited or sanctioned-excluded)" +[ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; FAIL=1; } [ "$FAIL" = 0 ] || exit 1 # -- Phase 4: definition fidelity (Lean defs vs deployed pacta verifiers) -- echo "=== Phase 4: definition fidelity ===" PACTA_SRC="${PACTA_SRC:-$HERE/../../proof-aware-crypto-tooling-agent/src}" +FIDELITY_RAN=0 if [ "${SKIP_FIDELITY:-0}" = "1" ]; then echo " skipped (SKIP_FIDELITY=1)" elif [ -d "$PACTA_SRC/pacta" ]; then PACTA_SRC="$PACTA_SRC" python3 "$HERE/fidelity/run_fidelity.py" || { echo "FIDELITY FAILED"; exit 1; } + FIDELITY_RAN=1 else echo " SKIPPED: pacta repo not found at $PACTA_SRC (set PACTA_SRC to run)" fi -echo "=== ALL GREEN ===" +# Fail-closed markers (review H2): the Lean corpus is green either way, but +# only the strong marker — required by the attestation gate — is emitted +# when fidelity actually ran. Never conflate the two. +echo "=== LEAN GREEN ===" +if [ "$FIDELITY_RAN" = 1 ]; then + echo "=== ATTESTATION GREEN (Lean + fidelity) ===" +else + echo "=== FIDELITY NOT RUN — NOT attestation-ready (run with pacta present) ===" +fi diff --git a/verification/fidelity/run_fidelity.py b/verification/fidelity/run_fidelity.py index 901e3c5..97d6cc3 100644 --- a/verification/fidelity/run_fidelity.py +++ b/verification/fidelity/run_fidelity.py @@ -4,9 +4,13 @@ Differential-tests the LEAN definitions (transliterated in lean_defs.py: MTH / Path / Root / ConsRec, post-refactor decidable-if base) against the DEPLOYED pacta verifiers, over the EXACT case generation of the paper's -tests/test_paper_verifiers.py — so the pinned counts (164,479 / 164,224) -carry over and this run establishes, by exhaustive testing, that the -mechanized objects agree with the deployed RFC 9162 code. +tests/test_paper_verifiers.py — this run establishes agreement between the mechanized objects and the +deployed RFC 9162 code EXHAUSTIVELY OVER all size/index (and old/new +size) pairs through 256 FOR the two fixed generated datasets and the +listed mutation classes (honest, wrong-leaf, wrong-index, wrong-root, +truncated/padded proof, and out-of-range m≥n / n0>n1 / n0=0). It is not +a proof of extensional equality over all inputs; the Lean-to-Python +bridge remains trusted quoted-source inspection (see KNOWN-GAPS). Requires the pacta repo on PYTHONPATH (its src/). Bound NMAX matches the paper. @@ -56,6 +60,8 @@ def inclusion(): (data[m] + b"!", m, n, P, root), (data[m], (m + 1) % n, n, P, root), (data[m], m, n, P, _h(b"q")), + (data[m], n, n, P, root), # out-of-range m = n (review F1) + (data[m], n + 3, n, P, root), # out-of-range m > n (review F1) ] if P: cases.append((data[m], m, n, P[:-1], root)) @@ -81,6 +87,8 @@ def consistency(): (m, n, _h(b"x"), r1, P), (m, n, r0, _h(b"y"), P), (m, n, r0, r1, P + [_h(b"z")]), + (n + 1, n, r1, r0, P), # n0 > n1 (review F1) + (0, n, r0, r1, P), # n0 = 0 escape (review F1) ] if P: cases.append((m, n, r0, r1, P[:-1])) @@ -99,9 +107,9 @@ def main(): tc = consistency() print(f" consistency: {tc} verifier cases (incl. honest), MTH checks — all agree") # pinned counts (identical generation to the paper's harness) - assert ti == 164_479, ti - assert tc == 164_224, tc - print(f" PINNED: inclusion={ti} (164,479) consistency={tc} (164,224)") + assert ti == 230_271, ti # re-pinned after adding out-of-range families (F1) + assert tc == 230_016, tc + print(f" PINNED: inclusion={ti} (230,271) consistency={tc} (230,016)") print("=== FIDELITY GREEN: mechanized defs agree with deployed verifier ===") diff --git a/verification/gen/LTLAcc/HashExternal.olean b/verification/gen/LTLAcc/HashExternal.olean deleted file mode 100644 index 3453a43..0000000 Binary files a/verification/gen/LTLAcc/HashExternal.olean and /dev/null differ