mirror of
https://github.com/saymrwulf/ltl-accumulator-verified.git
synced 2026-09-03 19:53:48 +00:00
Review round 4: F1* absorbed (lied-size boundary), acceptCons_sound, kit reproducibility
Round-3 verdicts: GPT-5.6 conditionally approves (blockers closed, one portability finding); the Claude reviewer's Socratic addendum produced F1*, the strongest finding of the series — deployed verify_consistency and mechanized ConsRec are NOT extensionally equal. Reproduced exactly (witness verify_consistency(1,3,R2,R3,P(2→3))=True vs ConsRec reject; 3,405 divergences n<60; strictly one-sided; power-of-two seeding mechanism confirmed in source). - KNOWN-GAPS gap 14: witness, mechanism, one-sidedness, and the pinned-pair side condition under which Theorem 3 transfers to the deployed verifier (pacta's pin-store flow supplies it by construction). No pacta code change; deployed behavior matches upstream RFC 9162 implementations. - fidelity: lied-size family — 73,573 boundary cases, 3,867 expected divergences PINNED, one-sided direction asserted per case. Banner rescoped: agreement over pinned families, not extensional equality. - Theorem3.lean: acceptCons_sound (F2) — soundness over the named acceptCons predicate, n₀=0 discharged from the non-prefix premise, size bound derived from acceptance via new consRec_some_le. Cones read from #print axioms; CONES/AxiomCheck/allowlist updated (218 → 222 constants, diff = the two theorems + two generated auxiliaries). - F3/GPT§7: verification/lean-toolchain pin + run_bare.sh (reviewer's standalone runner, plain public lean — verified green: 61 cones, 222 constants, gate green) + AENEAS_ENV override in check.sh and selftest_audit.sh. - F4: awk field-equality replaces regex-with-dots in Phase 3b. - F5: git-tracked .pyc removed (worse than reported — it was in the repo, not just the kit); __pycache__ gitignored; round-4 kit ships a corpus MANIFEST.sha256 + pinned commit (also GPT's governance condition). check.sh exit 0, ATTESTATION GREEN; selftest exit 0, 9/9 + control. Live LTL untouched (12 leaves, bcd15f9d…); attestation still gated on ePrint decision + author review + explicit operator order. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
parent
9972ab4198
commit
2da0a79981
14 changed files with 416 additions and 236 deletions
3
.gitignore
vendored
3
.gitignore
vendored
|
|
@ -1,2 +1,5 @@
|
|||
*.olean
|
||||
.lake/
|
||||
__pycache__/
|
||||
*.pyc
|
||||
bare-*.out
|
||||
|
|
|
|||
|
|
@ -77,3 +77,30 @@ list is COMPLETE, not merely that the items are acceptable.
|
|||
from the kit). Round 3 ships the complete stdlib-only import closure
|
||||
of `pacta.transparency`, content-addressed against pacta commit
|
||||
`3d81d53`, plus the clean-extraction transcript with exit code.
|
||||
14. **Deployed `verify_consistency` accepts strictly more than the
|
||||
mechanized `ConsRec` on lied-size inputs** (round-3 Claude addendum
|
||||
F1*, reproduced by the operator against deployed pacta). Witness:
|
||||
for the honest proof P between sizes 2→3, `verify_consistency(1, 3,
|
||||
R2, R3, P)` returns True — a semantically false claim ("R2 is the
|
||||
root of a size-1 prefix") — while `ConsRec` rejects; 3,405 such
|
||||
divergences exist for n < 60, ALL one-sided (the mechanized model
|
||||
never accepts anything the deployed verifier rejects; inclusion
|
||||
shows zero divergences under identical abuse). Mechanism: when the
|
||||
claimed old size is a power of two, the deployed RFC 9162 iterative
|
||||
algorithm seeds the walk with the old root and uses the sizes only
|
||||
as bit-navigation state, so several size claims navigate one proof
|
||||
identically. Consequences: (a) fidelity between the two consistency
|
||||
verifiers is agreement over the pinned case families, NOT
|
||||
extensional equality — the harness's lied-size family pins the
|
||||
boundary (73,573 cases, 3,867 expected divergences, direction
|
||||
asserted one-sided); (b) Theorem 3 / `acceptCons_sound` cover the
|
||||
MECHANIZED accept set, and their soundness transfers to the deployed
|
||||
verifier only under the side condition that the consumer's
|
||||
`(n₀, r₀)` is an authentic pinned pair and `n₁` is the authentic
|
||||
size of the tree behind `r₁` — which pacta's pin-store flow supplies
|
||||
by construction (`n₀` comes from the consumer's own pin, never from
|
||||
the peer; `(n₁, r₁)` arrive together in one signed head). No
|
||||
exploitability against that flow is claimed or ruled out here;
|
||||
assessing it requires the signature/STH layer (gap 4). No pacta code
|
||||
change is made (deployed behavior matches upstream RFC 9162
|
||||
implementations; the consumer flow enforces the side condition).
|
||||
|
|
|
|||
|
|
@ -40,6 +40,10 @@ separate, explicitly-authorized operator decision.
|
|||
- `verification/check.sh` is THE button: compiles every file through
|
||||
`lean-guard` (memory cap, core pinning, timeout, single-flight lock)
|
||||
and axiom-audits every certificate against its documented exact cone.
|
||||
- Reviewers without the operator toolchain: `verification/run_bare.sh`
|
||||
compiles, axiom-audits, and inventory-gates the corpus with a plain
|
||||
public `lean` (version pinned in `verification/lean-toolchain`); the
|
||||
operator path is overridable via `AENEAS_ENV`.
|
||||
- Expected boundary: `propext, Classical.choice, Quot.sound` plus
|
||||
`LTLAcc.sha256` for hash-touching certificates — documented per
|
||||
certificate in `check.sh`, audited both directions.
|
||||
|
|
|
|||
|
|
@ -1,136 +1,119 @@
|
|||
# Response to reviewers — round 3
|
||||
# Response to reviewers — round 4
|
||||
|
||||
Corpus: `ltl-accumulator-verified`. Round-2 reviews received against the
|
||||
round-2 freeze `260ad64` (GPT-5.6 second adversarial review; second
|
||||
Claude round-2 findings). Every finding was independently re-verified
|
||||
against the corpus before any change; all confirmed findings are fixed
|
||||
in this freeze. No theorem statement changed except the one interface
|
||||
tightening both reviewers requested (L1/NEW-2).
|
||||
Corpus: `ltl-accumulator-verified`. Round-3 reviews received against the
|
||||
round-3 freeze `9972ab4`: GPT-5.6 (conditional approval, one portability
|
||||
finding) and the round-3 Claude reviewer's Socratic addendum (one new
|
||||
confirmed finding, four reinstated ones). Every claim was independently
|
||||
re-verified by the operator before any change. This round contains ONE
|
||||
new theorem, one harness family, and packaging/scoping fixes. No
|
||||
existing theorem statement or proof changed.
|
||||
|
||||
## Disposition of round-2 findings
|
||||
## The headline: F1* (Claude addendum) — CONFIRMED and absorbed
|
||||
|
||||
### GPT H1 / Claude NEW-1 — coverage gate evadable (CONFIRMED, fixed structurally)
|
||||
The addendum demonstrated that the deployed `verify_consistency` and
|
||||
the mechanized `ConsRec` acceptance are **not extensionally equal**:
|
||||
the deployed RFC 9162 iterative verifier accepts honest proofs under
|
||||
lied size claims (witness: `verify_consistency(1, 3, R2, R3, P(2→3)) =
|
||||
True`; ConsRec rejects). Reproduced exactly on the operator machine
|
||||
against deployed pacta: same witness, same 3,405 divergences for
|
||||
n < 60, same strictly one-sided direction (the mechanized model is the
|
||||
stricter; inclusion diverges nowhere under identical abuse), same
|
||||
power-of-two seeding mechanism in the deployed source.
|
||||
|
||||
Both reviewers were right, and GPT's namespace-collision attack
|
||||
(`LTLAcc.Hidden.MTH` classified against `CONES[LTLAcc.MTH]`) showed that
|
||||
regex hardening (Claude's proposed fix) would not have closed the class.
|
||||
We adopted GPT's required correction in full — the inventory is now
|
||||
derived from the Lean environment, not from source:
|
||||
Absorbed as follows:
|
||||
|
||||
- **`Proofs/Inventory.lean`** imports every corpus module and emits
|
||||
EVERY constant whose originating module is a corpus module: fully
|
||||
qualified name, declaration kind, and axiom cone. There is **no
|
||||
filtering** — compiler-generated auxiliaries and `_private.*` mangles
|
||||
are emitted and pinned too, so there is no name shape that can hide.
|
||||
A corpus module missing from the import list is an elaboration error.
|
||||
- The axiom cone is computed by our own walker AND cross-checked
|
||||
in-process against core `collectAxioms` (the machinery `#print axioms`
|
||||
uses) for every constant — divergence is a hard error. (This caught a
|
||||
real toolchain subtlety during development: `ConstantInfo.value?`
|
||||
returns `none` for theorems on 4.30.0-rc2, which would have silently
|
||||
truncated cones; the direct constructor match avoids it, and the
|
||||
cross-check would have refused to ship it.)
|
||||
- **`verification/inventory-allowlist.txt`** pins all 218 constants;
|
||||
**`inventory_gate.sh`** diffs environment vs allowlist fail-closed in
|
||||
BOTH directions (UNCLASSIFIED / STALE), requires the INV-COUNT
|
||||
trailer (a truncated Lean run cannot pass as an empty diff), and
|
||||
asserts the whole corpus contains exactly one axiom-kind constant:
|
||||
`LTLAcc.sha256`.
|
||||
- check.sh Phase 3b additionally verifies: the inventory's module list
|
||||
== the compile manifest (both directions), every CONES entry appears
|
||||
in the allowlist **with an identical cone** (two independent cone
|
||||
computations must agree), and every CONES entry is queried by
|
||||
AxiomCheck.
|
||||
- **GPT release condition 2 (adversarial tests) is met by
|
||||
`verification/selftest_audit.sh`**, which attacks the exact production
|
||||
gate: attributed, indented, private, and instance declarations, the
|
||||
nested-namespace basename collision, a smuggled axiom, a deleted
|
||||
declaration (STALE direction), and unmanifested `Proofs/` and `gen/`
|
||||
modules through the full check.sh — plus a positive control so the
|
||||
self-test cannot pass vacuously. Transcript in the kit
|
||||
(`selftest-transcript.txt`).
|
||||
- **KNOWN-GAPS gap 14**: full statement — witness, mechanism,
|
||||
one-sidedness, and the soundness-transfer side condition (the
|
||||
consumer's `(n₀, r₀)` is an authentic pinned pair and `n₁` is the
|
||||
authentic size behind `r₁`), which pacta's pin-store flow supplies by
|
||||
construction. No exploitability against that flow is claimed or ruled
|
||||
out; that assessment belongs to the signature/STH layer (gap 4).
|
||||
- **Harness**: new lied-size family — 73,573 boundary cases (lied old
|
||||
size exhaustive for n < 60, lied new size sampled), 3,867 expected
|
||||
divergences PINNED, and the one-sided direction asserted on every
|
||||
case: a single `lean=True / deployed=False` instance fails the run.
|
||||
These families would have caught F1* in round 1; now they guard it
|
||||
forever.
|
||||
- **Banner**: `FIDELITY GREEN` now reads "agreement over the pinned
|
||||
case families (not extensional equality; KNOWN-GAPS gap 14)". The
|
||||
STATEMENT-MAP fidelity row and Theorem-3 row carry the same scoping.
|
||||
- **No pacta code change.** The deployed behavior matches upstream
|
||||
RFC 9162 implementations; the consumer flow enforces the side
|
||||
condition (`n₀` comes from the consumer's own pin, never from the
|
||||
peer; `(n₁, r₁)` arrive together in one signed head). pacta also
|
||||
remains change-frozen during paper processing.
|
||||
|
||||
### GPT H2 — fidelity target could not run (CONFIRMED, fixed)
|
||||
## F2 — `acceptCons` routed through zero theorems (CONFIRMED, fixed)
|
||||
|
||||
Reproduced exactly (`ModuleNotFoundError: pacta.postquantum`). The
|
||||
round-3 `pacta-fidelity-target` ships the complete **load-time import
|
||||
closure** of `pacta.transparency` (`__init__`, `transparency`,
|
||||
`postquantum`, `signing`, `yamlio`) — all stdlib-only, so a bare
|
||||
Python 3 runs it with no pip installs — content-addressed in
|
||||
`MANIFEST.sha256` against pacta commit `3d81d538…` with verification
|
||||
instructions (`TARGET-PROVENANCE.md`). The kit includes the complete
|
||||
terminal transcript AND exit code of `run_fidelity.py` executed from a
|
||||
clean extraction: exit 0, `230,271 + 230,016`, zero mismatches
|
||||
(`fidelity-clean-run-transcript.txt`), plus the full green `check.sh`
|
||||
transcript ending in `ATTESTATION GREEN` with fidelity not skipped
|
||||
(`check-transcript.txt`) — GPT release conditions 3 and 5.
|
||||
New theorem `acceptCons_sound` (Theorem3.lean): soundness stated over
|
||||
the named `acceptCons` predicate the harness tests — the consistency
|
||||
twin of round-2's `acceptIncl_sound`. The `n₀ = 0` disjunct is
|
||||
discharged from the non-prefix premise; the size bound `n₀ ≤ n₁` is
|
||||
derived from ConsRec acceptance itself via the new lemma
|
||||
`consRec_some_le` (the `n₀ > n` branch returns `none`), so the caller
|
||||
owes nothing beyond acceptance + wrong-prefix. Cones (read from
|
||||
`#print axioms`, as always): `consRec_some_le` = [propext,
|
||||
LTLAcc.sha256, Quot.sound]; `acceptCons_sound` = [propext,
|
||||
Classical.choice, LTLAcc.sha256, Quot.sound]. Both are in CONES,
|
||||
AxiomCheck, and the inventory allowlist (218 → 222 constants; the diff
|
||||
is exactly the two theorems plus their two generated auxiliaries).
|
||||
|
||||
### GPT M1 — audit narrower outside Proofs/ (CONFIRMED, fixed)
|
||||
## F3 — Lean-side kit reproducibility (CONFIRMED, fixed)
|
||||
|
||||
- Orphan-olean guard is now recursive over the whole tree (it caught a
|
||||
stray development artifact on its first run).
|
||||
- gen/ has the same unmanifested-source ("dead file") check as Proofs/.
|
||||
- The axiom surface is pinned corpus-wide twice: textually (exactly one
|
||||
`axiom` line under gen/, none under Proofs/) and semantically (the
|
||||
inventory admits exactly one axiom-kind constant anywhere).
|
||||
- Declaration discovery under gen/ now goes through the environment
|
||||
inventory like everything else.
|
||||
`verification/lean-toolchain` now pins `leanprover/lean4:v4.30.0-rc2`,
|
||||
and `verification/run_bare.sh` is the reviewer's standalone runner:
|
||||
plain public `lean`, no lake, no Aeneas checkout — compile all modules,
|
||||
print all cones, run the inventory gate. Verified green on this machine
|
||||
(under the operator's memory-cap discipline): 61 cone lines, 222
|
||||
constants, gate green. check.sh remains the operator's button.
|
||||
|
||||
### GPT M2 — stale fidelity counts in STATEMENT-MAP (CONFIRMED, fixed)
|
||||
## F4 — regex metacharacters in Phase 3b (CONFIRMED, fixed)
|
||||
|
||||
The row now reads 230,271 + 230,016 with the expanded families named.
|
||||
Process note: the round-2 Claude review certified this row as already
|
||||
fixed; it was not. Consistent with this project's experience, "verified"
|
||||
claims by reviewers are themselves re-verified now.
|
||||
The `PINNED BUT NOT INVENTORIED` check now uses awk field equality
|
||||
instead of a regex containing the constant name; the module-manifest
|
||||
greps were already `-F`. Dots no longer act as wildcards anywhere in
|
||||
the gate.
|
||||
|
||||
### GPT M3 — "not choice-dischargeable" overclaims (CONFIRMED, fixed)
|
||||
## F5 — kit hygiene (CONFIRMED, fixed; one sharpening)
|
||||
|
||||
STATEMENT-MAP now uses (essentially) GPT's safer wording: the guards
|
||||
show each named extractor returns a non-collision on at least one
|
||||
canonical honest input, ruling out the globally-inhabited-existential
|
||||
degeneration; they do NOT establish logical dependence on every
|
||||
hypothesis, nor exclude other classical arguments on restricted domains.
|
||||
The stray `.pyc` was worse than reported: it was **git-tracked**, which
|
||||
is why `git archive` shipped it. Untracked; `__pycache__/`/`*.pyc`
|
||||
gitignored. The round-4 kit gives the corpus tarball the same treatment
|
||||
as the pacta target: `MANIFEST.sha256` over every file in the archive
|
||||
plus the pinned public commit and repo URL — this also implements
|
||||
GPT's governance condition (publish hashes of the audit-critical
|
||||
files; they are all in the archive the manifest covers).
|
||||
|
||||
### GPT L1 / Claude NEW-2 — redundant `hm` in `acceptIncl_sound` (CONFIRMED, fixed)
|
||||
## GPT §7 — hard-coded toolchain bootstrap (CONFIRMED, fixed)
|
||||
|
||||
The hypothesis is gone; the range fact is derived from `hacc.1`, so the
|
||||
theorem is stated purely in terms of acceptance + wrong-leaf premise.
|
||||
Cone unchanged (`propext, Classical.choice, LTLAcc.sha256, Quot.sound`),
|
||||
re-verified by `#print axioms` and the inventory.
|
||||
`AENEAS_ENV` override with a clear FATAL message in both check.sh and
|
||||
selftest_audit.sh, exactly as recommended; default unchanged for the
|
||||
operator. Together with F3 this closes the "reviewer-friendly
|
||||
push-button" gap: reviewers get `run_bare.sh`, operators keep the
|
||||
guarded button.
|
||||
|
||||
### GPT ledger additions (adopted, as history)
|
||||
## GPT §9 — paper-language conditions
|
||||
|
||||
KNOWN-GAPS gains gap 12 (audit-gate lineage: the round-2 gate was
|
||||
evadable, what replaced it, and the residual limits of an
|
||||
environment-derived inventory — it cannot see never-compiled source,
|
||||
which the dead-file checks cover, nor defeat a hostile toolchain) and
|
||||
gap 13 (the round-2 kit's fidelity target was not self-contained).
|
||||
Adopted into the paper-cycle queue verbatim (they overlap the queue
|
||||
built across rounds 1–3), plus F1*'s two additions: the fidelity
|
||||
sentence must say "finite differential testing over pinned families,
|
||||
extensional equality is false for consistency (one-sided)", and
|
||||
Theorem 3's deployment claim must carry the pinned-pair side condition.
|
||||
The paper is edited in its own cycle, not in this corpus.
|
||||
|
||||
## Found in round-3 self-review (neither reviewer caught)
|
||||
## Reviewer-process note (kept, per this project's candor convention)
|
||||
|
||||
- **README layer table was still stale at `260ad64`**: L4 carried
|
||||
"queued for S4 restoration" and the pin-store row said "pending",
|
||||
despite round-1 F2 being certified as fixed by the round-2 Claude
|
||||
review. The table now matches the frozen state (all layers done,
|
||||
L4 explicitly "done as specializations" per gap 3).
|
||||
- KNOWN-GAPS gap 2 still cited the old 164,224 count; updated.
|
||||
|
||||
## Round-2 Claude review, remaining notes
|
||||
|
||||
NEW-1 was correct in direction; we implemented the stronger
|
||||
environment-based fix rather than the proposed regex broadening, since
|
||||
the namespace collision defeats any basename-keyed source scan. The
|
||||
round-2 Claude claim that the fidelity harness was "confirmed green
|
||||
against the real pacta code" was obtained by hand-stubbing the missing
|
||||
modules — with the round-3 self-contained target, that result is now
|
||||
reproducible by anyone from the kit alone.
|
||||
The round-3 Claude reviewer's self-analysis (Q1–Q7) found its own
|
||||
"confirmed/verified" inflations and then did what the drill demands:
|
||||
applied constructive-witness standards to its own strongest doubt and
|
||||
produced F1*. Its round-3.5 addendum is the strongest single review
|
||||
artifact this corpus has received. The operator re-verified every claim
|
||||
in it anyway — trust nothing, including good news.
|
||||
|
||||
## What did NOT change
|
||||
|
||||
All theorem statements and proofs except the `acceptIncl_sound`
|
||||
signature tightening; the axiom boundary (single opaque `sha256`); the
|
||||
pinned CONES table (59 entries, all cones byte-identical to round 2);
|
||||
the fidelity counts. The live transparency log remains frozen at
|
||||
12 leaves (root `bcd15f9d…`) and is untouched by this round;
|
||||
attestation remains blocked pending the ePrint decision, author
|
||||
review, and an explicit operator order.
|
||||
All pre-existing theorem statements and proofs; the axiom boundary
|
||||
(single opaque `sha256`); the 230,271/230,016 family pins; the live
|
||||
transparency log (12 leaves, root `bcd15f9d…`); deployed pacta.
|
||||
Attestation remains blocked pending the ePrint decision, the author's
|
||||
read, and an explicit operator order.
|
||||
|
|
|
|||
|
|
@ -21,11 +21,11 @@ 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`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged) | Theorem3 | sha256 (+choice) |
|
||||
| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged); `acceptCons_sound` routes it through the named `acceptCons` predicate (size bound derived from acceptance via `consRec_some_le`). Covers the MECHANIZED accept set; transfer to the deployed verifier is conditional on the pinned-pair side condition of gap 14 | 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 230,271 inclusion + 230,016 consistency (paper's case set + out-of-range families m≥n, n₀>n₁, n₀=0; round-2 M2 fixed the stale pre-expansion counts here) | fidelity | (testing) |
|
||||
| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency over the pinned case families — **not extensional equality**: the lied-size family (73,573 cases) pins the known one-sided divergence of gap 14 (3,867 expected, deployed-accepts-only, direction asserted) | 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
|
||||
|
|
|
|||
|
|
@ -68,3 +68,5 @@ import Proofs.PinStore
|
|||
#print axioms LTLAcc.acceptIncl_sound
|
||||
#print axioms LTLAcc.extractCons_correct_paper
|
||||
#print axioms LTLAcc.Hash
|
||||
#print axioms LTLAcc.consRec_some_le
|
||||
#print axioms LTLAcc.acceptCons_sound
|
||||
|
|
|
|||
|
|
@ -78,4 +78,41 @@ theorem extractCons_correct_paper (n₀ : Nat) (C : List Hash) (D₀ D₁ : List
|
|||
rw [hD0, h0]; simp
|
||||
· exact extractCons_correct n₀ C D₀ D₁ hlen0 hpos hle hne hacc
|
||||
|
||||
/-- `ConsRec` acceptance implies the size bound: the `n₀ > n` branch
|
||||
returns `none`, so a `some` forces `n₀ ≤ n`. Lets `acceptCons_sound`
|
||||
owe no separate range hypothesis (mirrors `acceptIncl_sound`
|
||||
deriving `m < n` from `hacc.1` — review round 3, F2). -/
|
||||
theorem consRec_some_le {n₀ n : Nat} {C : List Hash} {b : Bool} {r : Hash}
|
||||
{p : Hash × Hash} (h : ConsRec n₀ n C b r = some p) : n₀ ≤ n := by
|
||||
rcases Nat.lt_or_ge n n₀ with hgt | hge
|
||||
· rw [ConsRec, if_neg (by omega : ¬ n₀ = n),
|
||||
if_pos (Or.inl hgt : n₀ > n ∨ n₀ = 0 ∨ n ≤ 1)] at h
|
||||
simp at h
|
||||
· exact hge
|
||||
|
||||
/-- Consistency soundness through the named acceptance predicate
|
||||
(review round 3, F2 — the consistency twin of `acceptIncl_sound`):
|
||||
if `acceptCons` holds between the pinned head of `D₀` and the head
|
||||
of `D₁` but `D₀` is not the real prefix, `extractCons` outputs a
|
||||
collision. The `n₀ = 0` disjunct of `acceptCons` is impossible under
|
||||
`hne` (`D₀ = [] = D₁.take 0`); the size bound comes from acceptance
|
||||
itself (`consRec_some_le`).
|
||||
|
||||
SCOPE (gap 14): this covers the MECHANIZED accept predicate. The
|
||||
deployed `verify_consistency` accepts strictly more on inputs whose
|
||||
claimed sizes are not the authentic sizes of the trees behind the
|
||||
roots; soundness transfers to deployment only under the pinned-pair
|
||||
side condition documented in KNOWN-GAPS gap 14. -/
|
||||
theorem acceptCons_sound (n₀ : Nat) (C : List Hash) (D₀ D₁ : List Bytes)
|
||||
(hlen0 : D₀.length = n₀)
|
||||
(hne : D₀ ≠ D₁.take n₀)
|
||||
(hacc : acceptCons n₀ D₁.length (MTH D₀) (MTH D₁) C) :
|
||||
IsCollision (extractCons n₀ C D₀ D₁).1 (extractCons n₀ C D₀ D₁).2 := by
|
||||
rcases hacc with h0 | hcons
|
||||
· exfalso; apply hne
|
||||
have hD0 : D₀ = [] := List.length_eq_zero_iff.mp (by omega)
|
||||
rw [hD0, h0]; simp
|
||||
· exact extractCons_correct_paper n₀ C D₀ D₁ hlen0
|
||||
(consRec_some_le hcons) hne hcons
|
||||
|
||||
end LTLAcc
|
||||
|
|
|
|||
|
|
@ -9,7 +9,11 @@
|
|||
# 2 compile manifest · 3 boundary-exact axiom audit
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -euo pipefail
|
||||
source ~/aeneas-toolchain/env.sh
|
||||
# Toolchain bootstrap is overridable for reviewers with their own install
|
||||
# (review round 3, GPT §7); the operator default stays pinned.
|
||||
AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
|
||||
[ -f "$AENEAS_ENV" ] || { echo "FATAL: Aeneas environment not found: $AENEAS_ENV (set AENEAS_ENV; or use run_bare.sh with a plain lean per lean-toolchain)"; exit 1; }
|
||||
source "$AENEAS_ENV"
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
||||
TIMEOUT="${LEAN_TIMEOUT:-600}"
|
||||
|
|
@ -86,6 +90,8 @@ declare -A CONES=(
|
|||
[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"
|
||||
[LTLAcc.consRec_some_le]="propext, LTLAcc.sha256, Quot.sound"
|
||||
[LTLAcc.acceptCons_sound]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
|
||||
)
|
||||
|
||||
# (The former EXCLUDE table is gone: since Phase 3b reads the environment,
|
||||
|
|
@ -225,8 +231,11 @@ while IFS='|' read -r _ name _ cone; do
|
|||
echo " CONE CROSS-CHECK FAILED: $name CONES=[$want] inventory=[$got]"; COVFAIL=1; }
|
||||
fi
|
||||
done < <(grep '^INV|' "$HERE/inventory-allowlist.txt")
|
||||
# (field-equality, not regex — dots in names must not act as wildcards;
|
||||
# review round 3, F4)
|
||||
for cert in "${!CONES[@]}"; do
|
||||
grep -q "^INV|$cert|" "$HERE/inventory-allowlist.txt" || {
|
||||
awk -F'|' -v n="$cert" '$1=="INV" && $2==n {found=1} END {exit !found}' \
|
||||
"$HERE/inventory-allowlist.txt" || {
|
||||
echo " PINNED BUT NOT INVENTORIED: $cert (in CONES, not in allowlist)"; COVFAIL=1; }
|
||||
done
|
||||
rm -f "$INVLOG"
|
||||
|
|
|
|||
Binary file not shown.
|
|
@ -9,8 +9,12 @@ 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).
|
||||
a proof of extensional equality over all inputs — and extensional
|
||||
equality is in fact FALSE for consistency: the lied-size family below
|
||||
pins the known one-sided divergence (deployed accepts claimed sizes an
|
||||
honest proof was never generated for; the mechanized ConsRec rejects —
|
||||
KNOWN-GAPS gap 14). 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.
|
||||
|
|
@ -34,6 +38,11 @@ from pacta.transparency import ( # noqa: E402
|
|||
import lean_defs as L # noqa: E402
|
||||
|
||||
NMAX = int(os.environ.get("FIDELITY_NMAX", "256"))
|
||||
# lied-size family pins (gap 14; valid for the default FIDELITY_LIED_NMAX=60):
|
||||
# 73,573 boundary cases, 3,867 expected one-sided divergences
|
||||
# (3,405 lied-old-size + 462 lied-new-size), smallest witness (n=3, m=2 claimed 1)
|
||||
LIED_PIN_TOTAL = 73_573
|
||||
LIED_PIN_DIV = 3_867
|
||||
|
||||
|
||||
def _h(b):
|
||||
|
|
@ -100,17 +109,74 @@ def consistency():
|
|||
return total
|
||||
|
||||
|
||||
def lied_sizes():
|
||||
"""Lied-size boundary family (round-3 review, Claude F1* / gap 14).
|
||||
|
||||
The deployed RFC 9162 iterative verify_consistency accepts honest
|
||||
proofs under CLAIMED sizes the proof was never generated for (when
|
||||
the claimed old size is a power of two it seeds the walk with the
|
||||
old root and uses the sizes only as bit-navigation state); the
|
||||
mechanized ConsRec binds the split geometry to the sizes and
|
||||
rejects. Divergences in this family are therefore EXPECTED and
|
||||
documented — what this pins is:
|
||||
(a) the DIRECTION: every divergence must be deployed=True /
|
||||
lean=False (the mechanized model is the stricter one; a
|
||||
lean=True/deployed=False case would break soundness transfer
|
||||
and fails the run immediately), and
|
||||
(b) the exact divergence COUNT, so any drift in either verifier
|
||||
shows up as a pin failure.
|
||||
Inclusion showed zero divergences under identical abuse (round-3
|
||||
addendum); the inclusion side is covered by the m>=n families above.
|
||||
"""
|
||||
lied_nmax = int(os.environ.get("FIDELITY_LIED_NMAX", "60"))
|
||||
total = 0
|
||||
div = 0
|
||||
for n in range(2, lied_nmax):
|
||||
data = [bytes([i % 251]) for i in range(n)]
|
||||
r1 = merkle_root(data)
|
||||
for m_true in range(1, n):
|
||||
P = consistency_proof(data, m_true)
|
||||
r0 = merkle_root(data[:m_true])
|
||||
for m_lie in range(0, n + 1): # lied OLD size
|
||||
if m_lie == m_true:
|
||||
continue
|
||||
total += 1
|
||||
dep = verify_consistency(m_lie, n, r0, r1, P)
|
||||
lean = L.accept_cons(m_lie, n, r0, r1, P)
|
||||
if dep != lean:
|
||||
div += 1
|
||||
assert dep and not lean, (
|
||||
"ONE-SIDEDNESS BROKEN: lean accepts, deployed rejects",
|
||||
n, m_true, m_lie)
|
||||
for n_lie in (n - 1, n + 1, n + 7): # lied NEW size
|
||||
if n_lie < m_true or n_lie == n or n_lie < 1:
|
||||
continue
|
||||
total += 1
|
||||
dep = verify_consistency(m_true, n_lie, r0, r1, P)
|
||||
lean = L.accept_cons(m_true, n_lie, r0, r1, P)
|
||||
if dep != lean:
|
||||
div += 1
|
||||
assert dep and not lean, (
|
||||
"ONE-SIDEDNESS BROKEN: lean accepts, deployed rejects",
|
||||
n, m_true, "n_lie", n_lie)
|
||||
return total, div
|
||||
|
||||
|
||||
def main():
|
||||
print(f"S7 fidelity: Lean defs vs deployed pacta, NMAX={NMAX}")
|
||||
ti, rc, pc = inclusion()
|
||||
print(f" inclusion: {ti} verifier cases, {rc} MTH==merkle_root, {pc} Path==inclusion_proof — all agree")
|
||||
tc = consistency()
|
||||
print(f" consistency: {tc} verifier cases (incl. honest), MTH checks — all agree")
|
||||
tl, dl = lied_sizes()
|
||||
print(f" lied-sizes: {tl} boundary cases, {dl} EXPECTED divergences, all deployed-accepts-only (gap 14)")
|
||||
# pinned counts (identical generation to the paper's harness)
|
||||
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 ===")
|
||||
assert (tl, dl) == (LIED_PIN_TOTAL, LIED_PIN_DIV), (tl, dl)
|
||||
print(f" PINNED: inclusion={ti} (230,271) consistency={tc} (230,016) lied-sizes={tl}/{dl}")
|
||||
print("=== FIDELITY GREEN: agreement over the pinned case families "
|
||||
"(not extensional equality; KNOWN-GAPS gap 14) ===")
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
|
|
|
|||
|
|
@ -15,20 +15,59 @@
|
|||
#
|
||||
# Invariant checked by check.sh on top of the diff:
|
||||
# exactly ONE axiom line in this file, and it is LTLAcc.sha256.
|
||||
INV|LTLAcc.Bytes|def|
|
||||
INV|LTLAcc.ConsRec._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.match_1|def|
|
||||
INV|LTLAcc.ConsRec|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Hash|def|
|
||||
INV|LTLAcc.IsCollision|def|LTLAcc.sha256
|
||||
INV|LTLAcc.MTH._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH_single|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH_split._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH_split._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH_split|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary.induct|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path.induct|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root.match_1|def|
|
||||
INV|LTLAcc.Root_left._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root_left._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root_left|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_one_cons|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_one|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_right._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root_right._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root_right|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.acceptCons_sound._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.acceptCons_sound|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.acceptCons|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.acceptIncl|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.acceptIncl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.acceptIncl_sound|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Bytes|def|
|
||||
INV|LTLAcc.ConsRec|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.consRec_base_false_eq|theorem|Classical.choice,Quot.sound,propext
|
||||
INV|LTLAcc.consRec_base_false_eq.match_1|def|propext
|
||||
INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_1|def|propext
|
||||
INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_2|def|propext
|
||||
INV|LTLAcc.consRec_base_true_eq|theorem|propext
|
||||
INV|LTLAcc.consRec_base_true_eq.match_1|def|propext
|
||||
INV|LTLAcc.consRecBinding|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.consRecBinding.match_1|def|
|
||||
INV|LTLAcc.acceptIncl|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.consRecBinding._proof_1_10|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.consRecBinding._proof_1_11|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.consRecBinding._proof_1_12|theorem|Quot.sound,propext
|
||||
|
|
@ -41,38 +80,44 @@ INV|LTLAcc.consRecBinding._proof_1_5|theorem|Quot.sound,propext
|
|||
INV|LTLAcc.consRecBinding._proof_1_6|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.consRecBinding._proof_1_7|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.consRecBinding._proof_1_8|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec.match_1|def|
|
||||
INV|LTLAcc.ConsRec._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.ConsRec._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.consRecBinding.match_1|def|
|
||||
INV|LTLAcc.consRecBinding|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_1|def|propext
|
||||
INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_2|def|propext
|
||||
INV|LTLAcc.consRec_base_false_eq.match_1|def|propext
|
||||
INV|LTLAcc.consRec_base_false_eq|theorem|Classical.choice,Quot.sound,propext
|
||||
INV|LTLAcc.consRec_base_true_eq.match_1|def|propext
|
||||
INV|LTLAcc.consRec_base_true_eq|theorem|propext
|
||||
INV|LTLAcc.consRec_some_le._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.consRec_some_le|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.domsep|theorem|
|
||||
INV|LTLAcc.eq_dropLast_append_of_getLast?|theorem|propext
|
||||
INV|LTLAcc.exists_singleton_of_length_one|theorem|Classical.choice,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct_paper|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct_paper._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractCons.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons.match_1|def|
|
||||
INV|LTLAcc.extractConsNode|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode.match_1|def|
|
||||
INV|LTLAcc.extractConsNode._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractConsNode|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct_paper._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct_paper|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_nonvacuous._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractCons|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl.match_1|def|
|
||||
INV|LTLAcc.extractIncl_correct._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_correct._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_correct._proof_1_4|theorem|Quot.sound,propext
|
||||
|
|
@ -81,17 +126,18 @@ INV|LTLAcc.extractIncl_correct._proof_1_6|theorem|Quot.sound,propext
|
|||
INV|LTLAcc.extractIncl_correct._proof_1_7|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_correct._proof_1_8|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_correct._proof_1_9|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl.match_1|def|
|
||||
INV|LTLAcc.extractIncl_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_nonvacuous._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractIncl|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_correct._proof_1_10|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_correct._proof_1_4|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_correct._proof_1_5|theorem|Quot.sound,propext
|
||||
|
|
@ -99,114 +145,72 @@ INV|LTLAcc.extractMTH_correct._proof_1_6|theorem|Quot.sound,propext
|
|||
INV|LTLAcc.extractMTH_correct._proof_1_7|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_correct._proof_1_8|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_correct._proof_1_9|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_nonvacuous._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.extractMTH|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.fork_distinct|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.getD_drop|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.getD_drop._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.getD_take|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.getD_drop|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.getD_take._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.getD_take._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Hash|def|
|
||||
INV|LTLAcc.getD_take|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.hleaf|def|LTLAcc.sha256
|
||||
INV|LTLAcc.hnode|def|LTLAcc.sha256
|
||||
INV|LTLAcc.hnode_preimage_inj|theorem|propext
|
||||
INV|LTLAcc.incl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.hnode|def|LTLAcc.sha256
|
||||
INV|LTLAcc.incl_complete._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.incl_complete._proof_1_5|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.incl_complete._proof_1_6|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.incl_complete._proof_1_7|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.incl_complete._proof_1_8|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.incl_complete._proof_1_9|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.instDecidableEqHash|def|
|
||||
INV|LTLAcc.incl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.instDecidableEqHash._proof_1|theorem|
|
||||
INV|LTLAcc.instInhabitedHash|def|propext
|
||||
INV|LTLAcc.instDecidableEqHash|def|
|
||||
INV|LTLAcc.instInhabitedHash._proof_1|theorem|propext
|
||||
INV|LTLAcc.IsCollision|def|LTLAcc.sha256
|
||||
INV|LTLAcc.kbelow|def|Quot.sound,propext
|
||||
INV|LTLAcc.instInhabitedHash|def|propext
|
||||
INV|LTLAcc.kbelow._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow._unsafe_rec|def|
|
||||
INV|LTLAcc.kbelow.eq_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow.eq_def|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_eq_of_pow2_between|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow.induct|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_4|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow.induct|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_lt|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_eq_of_pow2_between|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_lt._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_lt._proof_1_4|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_lt._proof_1_5|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_lt|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_pos|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_pow2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_prefix_eq|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_prefix_eq._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow._unsafe_rec|def|
|
||||
INV|LTLAcc.le_two_kbelow|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow_prefix_eq|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.kbelow|def|Quot.sound,propext
|
||||
INV|LTLAcc.le_two_kbelow._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.le_two_kbelow._proof_1_4|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH_single|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH_split|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.MTH_split._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.MTH_split._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path.induct|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary.induct|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Path._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pinAccept|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pinAccept_monotone|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.le_two_kbelow|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pinAccept_monotone._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pinAccept_monotone._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pinExtract|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pinAccept_monotone|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pinAccept|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pinExtract.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pin_prefix_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pinExtract|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pin_prefix_correct._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pin_prefix_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pin_prefix_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pin_prefix_nonvacuous._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pow2_exp_unique|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pin_prefix_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.pow2_exp_unique._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pow2_exp_unique._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pow2_exp_unique._proof_1_3|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_left|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_left._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root_left._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root.match_1|def|
|
||||
INV|LTLAcc.Root_one|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_one_cons|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_right|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root_right._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root_right._proof_1_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary|def|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary._proof_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.Root._unary._proof_2|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.pow2_exp_unique|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.sha256|axiom|LTLAcc.sha256
|
||||
INV|LTLAcc.take_all|theorem|propext
|
||||
INV|LTLAcc.take_append_drop|theorem|
|
||||
INV|LTLAcc.take_drop_prefix|theorem|Classical.choice,Quot.sound,propext
|
||||
INV|LTLAcc.take_take_le|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.take_take_le._proof_1_1|theorem|Quot.sound,propext
|
||||
INV|LTLAcc.take_take_le|theorem|Quot.sound,propext
|
||||
INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.eq_1|theorem|
|
||||
INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.eq_2|theorem|
|
||||
INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.splitter|def|
|
||||
|
|
@ -214,15 +218,15 @@ INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.eq_1|theorem|
|
|||
INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.eq_2|theorem|
|
||||
INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.splitter|def|
|
||||
INV|_private.Proofs.Basic.0.PSigma.casesOn._arg_pusher|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_1|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_2|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.splitter|def|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.eq_1|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.eq_2|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.splitter|def|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.eq_1|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.eq_2|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.splitter|def|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_1|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_2|theorem|
|
||||
INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.splitter|def|
|
||||
INV|_private.Proofs.Completeness.0.PSigma.casesOn._arg_pusher|theorem|
|
||||
INV|_private.Proofs.Consistency.0.LTLAcc.extractConsNode.match_1.eq_1|theorem|
|
||||
INV|_private.Proofs.Consistency.0.LTLAcc.extractConsNode.match_1.eq_2|theorem|
|
||||
|
|
|
|||
1
verification/lean-toolchain
Normal file
1
verification/lean-toolchain
Normal file
|
|
@ -0,0 +1 @@
|
|||
leanprover/lean4:v4.30.0-rc2
|
||||
42
verification/run_bare.sh
Executable file
42
verification/run_bare.sh
Executable file
|
|
@ -0,0 +1,42 @@
|
|||
#!/usr/bin/env bash
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
# run_bare.sh — REVIEWER's standalone runner (review round 3, Claude F3).
|
||||
#
|
||||
# Compiles, axiom-audits, and inventory-gates the corpus with a plain
|
||||
# public `lean` binary — no lake, no Aeneas checkout, no operator
|
||||
# environment. The corpus is Mathlib-free and needs only the toolchain
|
||||
# pinned in ./lean-toolchain (elan users: `elan default $(cat lean-toolchain)`
|
||||
# or run inside this directory and let elan pick it up).
|
||||
#
|
||||
# This runner exists so a reviewer can go from "trust the transcripts"
|
||||
# to "run the button" on any machine. It is NOT the operator's button:
|
||||
# check.sh remains the release gate (memory-guarded lean-guard, cone
|
||||
# table, fidelity phase, ATTESTATION marker). This script covers the
|
||||
# kernel-facing phases only: compile, #print-axioms audit, inventory
|
||||
# gate.
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -euo pipefail
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
command -v lean >/dev/null || { echo "FATAL: no 'lean' on PATH (want $(cat "$HERE/lean-toolchain"))"; exit 1; }
|
||||
echo "toolchain: $(lean --version)"
|
||||
echo "pinned: $(cat "$HERE/lean-toolchain")"
|
||||
|
||||
export LEAN_PATH="${LEAN_PATH:+$LEAN_PATH:}$HERE/gen:$HERE"
|
||||
|
||||
echo "=== compile (gen + 9 proof modules) ==="
|
||||
( cd "$HERE/gen" && lean -o LTLAcc/HashExternal.olean LTLAcc/HashExternal.lean )
|
||||
cd "$HERE"
|
||||
for m in Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore; do
|
||||
echo " · Proofs/$m"
|
||||
lean -o "Proofs/$m.olean" "Proofs/$m.lean"
|
||||
done
|
||||
|
||||
echo "=== axiom audit (#print axioms, compare against check.sh CONES yourself) ==="
|
||||
lean Proofs/AxiomCheck.lean | tee bare-axcheck.out | grep -c "depends on axioms\|does not depend" \
|
||||
| xargs -I{} echo " {} cone lines printed (full output: bare-axcheck.out)"
|
||||
|
||||
echo "=== inventory gate (environment == allowlist) ==="
|
||||
lean Proofs/Inventory.lean > bare-inventory.out
|
||||
"$HERE/inventory_gate.sh" bare-inventory.out "$HERE/inventory-allowlist.txt"
|
||||
|
||||
echo "=== BARE RUN GREEN (compile + axiom print + inventory gate) ==="
|
||||
|
|
@ -27,7 +27,9 @@
|
|||
# All Lean work goes through lean-guard (memory-capped, single-flight).
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -euo pipefail
|
||||
source ~/aeneas-toolchain/env.sh
|
||||
AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
|
||||
[ -f "$AENEAS_ENV" ] || { echo "FATAL: Aeneas environment not found: $AENEAS_ENV"; exit 1; }
|
||||
source "$AENEAS_ENV"
|
||||
SRC="$(cd "$(dirname "$0")" && pwd)"
|
||||
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
||||
CORES="${LEAN_MAX_CORES:-0-3}"
|
||||
|
|
|
|||
Loading…
Reference in a new issue