mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-03 20:13:47 +00:00
Compare commits
No commits in common. "a69a08cde6cbaadc41752bd683a40c1d5bbd6047" and "b55391bd29631930a9130a99ddd38aaa9434dad1" have entirely different histories.
a69a08cde6
...
b55391bd29
15 changed files with 30 additions and 5959 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
|
@ -1,4 +1,3 @@
|
|||
*.olean
|
||||
.lake/
|
||||
lake-manifest.json
|
||||
.audit-basis
|
||||
|
|
|
|||
|
|
@ -109,99 +109,3 @@ running Rust code. Everything else is machine-checked.
|
|||
consumer's protection is, and has always been, *review at the pinned
|
||||
commit* rather than the button's own verdict. A green button says "this is
|
||||
the apparatus that was reviewed", never "this apparatus is trustworthy".
|
||||
|
||||
10. **The whole declaration surface is pinned, not just the certificates.**
|
||||
`check.sh` Phase 2c reads the compiled environment and records, for EVERY
|
||||
constant originating in an audited module — roughly three thousand of them,
|
||||
compiler-generated auxiliaries included — its originating module, fully
|
||||
qualified name, declaration kind and complete axiom cone. The observed set
|
||||
must equal `inventory-allowlist.txt` exactly, in BOTH directions: a
|
||||
declaration present but not allowlisted (`UNCLASSIFIED`) and an allowlist
|
||||
entry with no declaration (`STALE`) are both build failures, and a count
|
||||
trailer disagreeing with the lines received is a third.
|
||||
|
||||
The gap this closes: Phase 2b asks the kernel only whether an AXIOM is
|
||||
declared, and Phase 3 pins the cones of the named certificates. Between
|
||||
them sat every helper lemma in the corpus. One of those quietly acquiring
|
||||
a hash oracle in its cone moved nothing either phase looked at.
|
||||
|
||||
**Two limits, stated because a reader would otherwise assume neither.**
|
||||
|
||||
· *No independent cone walker here.* The companion accumulator runs a
|
||||
hand-written closure walker alongside the kernel's `collectAxioms` and
|
||||
requires the two to agree on every constant, so each checks the other.
|
||||
Ported to this corpus on 2026-07-29 that walker was wrong in BOTH
|
||||
directions on mathlib's inductive shapes — it reported no axioms for
|
||||
`CurveFieldProofs.EdPoint` where the kernel reported three, and after
|
||||
being extended it reported three for `CurveFieldProofs.ProjPoint` where
|
||||
the kernel reported none. Two implementations disagreeing both ways are
|
||||
not a cross-check; they are a second wrong answer. The cone figures here
|
||||
therefore rest on `collectAxioms` alone. The accumulator keeps its
|
||||
cross-check, its corpus being mathlib-free.
|
||||
|
||||
· *The scalar layer is outside this phase.* Thirteen `Proofs/Scalar*`
|
||||
modules belong to `check-scalar.sh` and are inventoried by nothing. That
|
||||
is the two-button seam, still open. Phase 2c prints every uncovered
|
||||
module by name on every run, so the omission is visible rather than
|
||||
inferred.
|
||||
|
||||
11. **Both buttons, and the seam between them.** This repository is checked by
|
||||
two scripts: `check.sh` covers the field, curve and signature layers,
|
||||
`check-scalar.sh` the scalar layer. Until 2026-07-30 neither asserted
|
||||
anything about the other's scope and the main one simply SKIPPED anything
|
||||
named `Scalar*`, so a new `Proofs/ScalarX.lean` was gated by nothing at all
|
||||
— absent from one manifest by exemption, from the other by omission,
|
||||
compiled by neither, inventoried by neither. Each button now reads the
|
||||
other's manifest and requires every shipped proof source to belong to
|
||||
EXACTLY ONE of them, both directions: neither orphaned nor double-claimed.
|
||||
|
||||
The scalar button was also brought to the main one's standard, having been
|
||||
left behind by every hardening round: it now checks source integrity,
|
||||
verifies the harness pins (so running it alone is protected too), asks the
|
||||
KERNEL about axiom declarations instead of grepping source text, inventories
|
||||
its ~1,880 declarations against its own allowlist, and asserts each of its
|
||||
13 certificates by name rather than counting how many lines of output
|
||||
matched. A count cannot say WHICH certificate is clean, and passes just as
|
||||
happily if one cone is reported twice.
|
||||
|
||||
**What this cost, recorded because the lesson generalises.** Three separate
|
||||
gates in this work reasoned about how a thing is SPELLED rather than what it
|
||||
BELONGS TO, and the corpus punished each one: `Proofs/ScalarPackSpec.lean`
|
||||
is named like the scalar layer and owned by the main button. A dead-file
|
||||
gate globbing `Scalar*` demanded it be scalar-owned; an axiom gate scanning
|
||||
`Scalar*.olean` swept in an artifact this button does not compile, which on
|
||||
a fresh tree is absent and would have failed the run for a false reason; and
|
||||
the inventory driver discovery globbing `Inventory*.lean` claimed the other
|
||||
button's driver. All three now test membership in a manifest. This is the
|
||||
same family as the source-text axiom grep that began this campaign:
|
||||
reasoning about names instead of about the thing itself.
|
||||
|
||||
12. **`--audit-only`, and why a green transcript from it is not evidence.**
|
||||
`check.sh --audit-only` runs every gate but skips recompilation, against the
|
||||
`.olean` files a previous full run left behind: about 60 seconds against
|
||||
about 1280. It exists because gate work dominates this estate's wall-clock,
|
||||
and it is safe only because it refuses.
|
||||
|
||||
It refuses unless every shipped `.lean` is BYTE-IDENTICAL to a basis
|
||||
recorded by a previous full run — not mtimes, which `touch` defeats, and a
|
||||
stale-artifact check that fails open would be worse than no shortcut at all:
|
||||
a green button would then describe a corpus that is no longer on disk. The
|
||||
basis is gitignored build state, so a fresh clone cannot inherit permission
|
||||
to skip compiling, and the closing banner says in words that the run is not
|
||||
evidence.
|
||||
|
||||
**The kernel re-elaborates nothing in such a run.** What it establishes is
|
||||
that the gates accept artifacts produced earlier — useful while developing a
|
||||
gate, worthless as a record. `formal-verification-control/tools/record-run.py`
|
||||
enforces that: it refuses to archive any transcript bearing the audit-only
|
||||
markers, and also any transcript without a terminal success banner, any
|
||||
containing `error:`, and any repository whose tree is dirty at record time.
|
||||
A banner is a request; that tool is the gate.
|
||||
|
||||
Also worth knowing when reading a red run: `lean-guard` clamps Lean's memory
|
||||
budget to what the machine can spare, and under load that clamp can be too
|
||||
small to elaborate a large module. It surfaces as `FAIL: Proofs/<module>`,
|
||||
which reads exactly like a broken proof and is not one — it is a resource
|
||||
condition, and the cap is what protects this machine from the global OOM
|
||||
that killed a session on 2026-07-02. Check the transcript for a `clamping`
|
||||
line before concluding anything about the mathematics.
|
||||
|
|
|
|||
|
|
@ -1,18 +1,10 @@
|
|||
6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt
|
||||
d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh
|
||||
a8f560f1d46560ee8b90f90ffeeb63b1eccf0afdf1d6652a37a2047786945434 check.sh
|
||||
b88f4bc16d3188f4830f8333201fc7826d46acf829c37f7da398d6ae9bfca15e check-scalar.sh
|
||||
813c31664484adddd1752ea3bb30da826ad1050fd378604c242bcafb105fb4a3 check.sh
|
||||
7a55136cd15ab96b3ab77234ffb8a2fc7c9544cb8b36426d29e257ffb2d2ba6e extract.sh
|
||||
c9672a28825cd1d4055fb9efbb4a1d94c921c7b5c79e4cd5d0626ba061e554c1 GEN-MODEL.sha256
|
||||
e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05 inventory-allowlist-scalar.txt
|
||||
86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt
|
||||
0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh
|
||||
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
||||
772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean
|
||||
84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean
|
||||
4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc Proofs/Inventory.lean
|
||||
6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean
|
||||
bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh
|
||||
eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh
|
||||
79611f9689ba714fb8d3f57aee86ad9655509303445beaad766bf8b049de8c44 selftest-axgate.sh
|
||||
3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh
|
||||
1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh
|
||||
2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f selftest-statements.sh
|
||||
a14acaafe914aabb9df44fcd05fd50d475804280fab9e332fdb5ea0b0d35f164 selftest-statements.sh
|
||||
|
|
|
|||
|
|
@ -1,70 +0,0 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────
|
||||
Proofs/Inventory.lean — environment-derived declaration inventory (main chain).
|
||||
|
||||
Audit INFRASTRUCTURE, not corpus: excluded from check.sh's compile manifest
|
||||
and from its own inventory (its constants live in modules the corpus list
|
||||
below does not name). It proves nothing and is imported by nothing.
|
||||
|
||||
Covers every module check.sh compiles except any listed as needing a
|
||||
separate driver (see Proofs/InventoryBasic.lean if present). Whether
|
||||
a split is needed was determined by compiling a probe, per repo.
|
||||
────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.InventoryCore
|
||||
import Proofs.Denote
|
||||
import Proofs.P25519
|
||||
import Proofs.ReduceSpec
|
||||
import Proofs.SubNegSpec
|
||||
import Proofs.ConstSpecs
|
||||
import Proofs.AddSpec
|
||||
import Proofs.MulSpec
|
||||
import Proofs.SquareSpec
|
||||
import Proofs.Square2Spec
|
||||
import Proofs.Field
|
||||
import Proofs.InvertSpec
|
||||
import Proofs.FieldMain
|
||||
import Proofs.FeQ
|
||||
import Proofs.EdCurve
|
||||
import Proofs.EdDenote
|
||||
import Proofs.EdDouble
|
||||
import Proofs.EdAddProjNiels
|
||||
import Proofs.EdAddAffNiels
|
||||
import Proofs.EdConvert
|
||||
import Proofs.EdMain
|
||||
import Proofs.DsmTableSpec
|
||||
import Proofs.DsmStepSpec
|
||||
import Proofs.DsmLoopSpec
|
||||
import Proofs.DsmNafLoadSpec
|
||||
import Proofs.DsmNafMath
|
||||
import Proofs.DsmNafLoopSpec
|
||||
import Proofs.DsmNafSpec
|
||||
import Proofs.DsmMulSpec
|
||||
import Proofs.ToBytesMath
|
||||
import Proofs.ToBytesSpec
|
||||
import Proofs.ScalarPackSpec
|
||||
import Proofs.CompressSpec
|
||||
import Proofs.SigApexSpec
|
||||
import Proofs.PointLiftSpec
|
||||
import Proofs.PointEqSpec
|
||||
import Proofs.DecompressSpec
|
||||
import Proofs.FromBytesSpec
|
||||
import Proofs.DecompressMain
|
||||
open Lean Ed25519Inventory
|
||||
|
||||
/-- Exactly the modules this driver covers. check.sh verifies, in BOTH
|
||||
directions, that the union of the two drivers' lists is its PROOFS
|
||||
manifest minus the audit infrastructure. -/
|
||||
def corpus : Array Name :=
|
||||
#[`Proofs.Denote, `Proofs.P25519, `Proofs.ReduceSpec, `Proofs.SubNegSpec,
|
||||
`Proofs.ConstSpecs, `Proofs.AddSpec, `Proofs.MulSpec,
|
||||
`Proofs.SquareSpec, `Proofs.Square2Spec, `Proofs.Field,
|
||||
`Proofs.InvertSpec, `Proofs.FieldMain, `Proofs.FeQ, `Proofs.EdCurve,
|
||||
`Proofs.EdDenote, `Proofs.EdDouble, `Proofs.EdAddProjNiels,
|
||||
`Proofs.EdAddAffNiels, `Proofs.EdConvert, `Proofs.EdMain,
|
||||
`Proofs.DsmTableSpec, `Proofs.DsmStepSpec, `Proofs.DsmLoopSpec,
|
||||
`Proofs.DsmNafLoadSpec, `Proofs.DsmNafMath, `Proofs.DsmNafLoopSpec,
|
||||
`Proofs.DsmNafSpec, `Proofs.DsmMulSpec, `Proofs.ToBytesMath,
|
||||
`Proofs.ToBytesSpec, `Proofs.ScalarPackSpec, `Proofs.CompressSpec,
|
||||
`Proofs.SigApexSpec, `Proofs.PointLiftSpec, `Proofs.PointEqSpec,
|
||||
`Proofs.DecompressSpec, `Proofs.FromBytesSpec, `Proofs.DecompressMain]
|
||||
|
||||
#eval show MetaM Unit from emitInventory corpus
|
||||
|
|
@ -1,110 +0,0 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────
|
||||
Proofs/InventoryCore.lean — shared machinery for the declaration inventory.
|
||||
|
||||
PORTED, NOT REINVENTED. This is the ltl-accumulator-verified design
|
||||
(Proofs/Inventory.lean there), which survived a nine-attack self-test that
|
||||
defeated a source-regex enumerator: attributed, private, indented and
|
||||
`instance` declarations were all invisible to the regex, and a nested
|
||||
`namespace Hidden theorem MTH` collided with the basename of an audited
|
||||
declaration. Reading the compiled ENVIRONMENT sees exactly what the kernel
|
||||
saw, and there is no name shape that can hide from it.
|
||||
|
||||
WHY TWO DRIVERS IMPORT THIS. Unlike the accumulator, this corpus cannot be
|
||||
imported as one environment: `Proofs.Basic` and `Proofs.ConstSpecs` both
|
||||
declare `CurveFieldProofs.zero_spec`. That is deliberate and documented —
|
||||
Basic.lean is compiled by check.sh but imported by nothing, so the reuse is
|
||||
harmless — but it makes a single whole-corpus import impossible. The corpus
|
||||
therefore splits into the main chain and Basic, one driver each, and
|
||||
check.sh concatenates their output before gating. The split is asserted in
|
||||
check.sh against the compile manifest, so a module cannot fall between the
|
||||
two drivers unnoticed.
|
||||
|
||||
The corpus module list lives in each DRIVER, not here, and is checked
|
||||
textually against check.sh's manifest in both directions. A listed module
|
||||
that is not actually imported is an elaboration error, not a silent skip.
|
||||
────────────────────────────────────────────────────────────────────────── -/
|
||||
import Lean
|
||||
|
||||
open Lean
|
||||
|
||||
namespace Ed25519Inventory
|
||||
|
||||
def kindOf : ConstantInfo → String
|
||||
| .axiomInfo _ => "axiom"
|
||||
| .defnInfo _ => "def"
|
||||
| .thmInfo _ => "theorem"
|
||||
| .opaqueInfo _ => "opaque"
|
||||
| .quotInfo _ => "quot"
|
||||
| .inductInfo _ => "inductive"
|
||||
| .ctorInfo _ => "ctor"
|
||||
| .recInfo _ => "recursor"
|
||||
|
||||
/-- Axiom cone of `n`, from the kernel's own collector — the same machinery
|
||||
`#print axioms` uses.
|
||||
|
||||
NO INDEPENDENT SECOND WALKER HERE, and that is a deliberate REDUCTION in
|
||||
strength against the ltl-accumulator design this is ported from. There, a
|
||||
hand-written closure walker runs alongside `collectAxioms` and every
|
||||
constant must get the same answer from both, so the two implementations
|
||||
check each other. Porting that walker to this corpus was tried on
|
||||
2026-07-29 and abandoned on evidence:
|
||||
|
||||
· without traversing inductive families it UNDER-approximated —
|
||||
`CurveFieldProofs.EdPoint`: walker [] vs kernel [Classical.choice,
|
||||
Quot.sound, propext];
|
||||
· adding constructors, recursor rules and `all` groups made it
|
||||
OVER-approximate — `CurveFieldProofs.ProjPoint`: walker
|
||||
[Classical.choice, Quot.sound, propext] vs kernel [].
|
||||
|
||||
Disagreeing in BOTH directions means the second implementation is not an
|
||||
independent check, it is a second wrong answer. Matching the kernel's
|
||||
traversal exactly over mathlib's inductive shapes is a Lean-internals
|
||||
project, not a gate, and shipping a walker that is wrong in two directions
|
||||
would be worse than shipping none: it would fail builds for reasons that
|
||||
are the checker's fault and teach everyone to ignore it.
|
||||
|
||||
CONSEQUENCE, stated so nobody assumes otherwise: on this corpus the cone
|
||||
figures rest on `collectAxioms` alone. The accumulator's corpus is
|
||||
mathlib-free, its walker agrees there, and it KEEPS the cross-check. This
|
||||
is recorded in TRUSTED-BASE.md. -/
|
||||
def axiomCone (n : Name) : MetaM (Array Name) := do
|
||||
let cone ← collectAxioms n
|
||||
return cone.qsort (fun a b => a.toString < b.toString)
|
||||
|
||||
/-- Emit `INV|name|kind|cone` for every constant originating in `corpus`.
|
||||
EVERY constant is emitted — fully qualified, NO filtering. Compiler-
|
||||
generated auxiliaries (equation lemmas, match/eq/induct helpers, private
|
||||
manglings) are emitted too and pinned in the allowlist, so anything new,
|
||||
renamed, removed, or with a changed cone shows up as a diff. -/
|
||||
def emitInventory (corpus : Array Name) : MetaM Unit := do
|
||||
let env ← getEnv
|
||||
let mut idxs : Array Nat := #[]
|
||||
for m in corpus do
|
||||
match env.getModuleIdx? m with
|
||||
| some i => idxs := idxs.push i
|
||||
| none => throwError "INVENTORY ERROR: corpus module {m} is not imported"
|
||||
let mut lines : Array String := #[]
|
||||
for (n, ci) in env.constants.toList do
|
||||
if let some i := env.getModuleIdxFor? n then
|
||||
if idxs.contains i then
|
||||
let cone ← axiomCone n
|
||||
let coneStr := ",".intercalate (cone.toList.map (·.toString))
|
||||
-- The ORIGINATING MODULE is part of the record, unlike the accumulator's
|
||||
-- format. It has to be: this corpus contains two distinct declarations
|
||||
-- both named `CurveFieldProofs.zero_spec` (Proofs.Basic and
|
||||
-- Proofs.ConstSpecs), inventoried by different drivers. Keyed on name
|
||||
-- alone their records were byte-identical, so the merged allowlist held
|
||||
-- 3021 entries for 3022 declarations and one real declaration was
|
||||
-- covered by an entry describing a different one. The count trailer
|
||||
-- caught it; the module field is what fixes it.
|
||||
let mdl := env.header.moduleNames[i]!
|
||||
lines := lines.push s!"INV|{mdl}|{n}|{kindOf ci}|{coneStr}"
|
||||
let sorted := lines.qsort (· < ·)
|
||||
for l in sorted do
|
||||
IO.println l
|
||||
-- Output-integrity trailer: a truncated or crashed run must never pass as an
|
||||
-- empty diff. inventory_gate.sh compares this against the lines it actually
|
||||
-- received, in both directions.
|
||||
IO.println s!"INV-COUNT|{sorted.size}"
|
||||
|
||||
end Ed25519Inventory
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────
|
||||
Proofs/InventoryScalar.lean — declaration inventory for the scalar layer.
|
||||
|
||||
Audit INFRASTRUCTURE, not corpus. Compiled by check-scalar.sh Phase 2c,
|
||||
which is where these modules' compiled artifacts exist: check.sh does not
|
||||
compile the scalar layer, so its own inventory could not cover them and
|
||||
named them as uncovered on every run instead. This closes that.
|
||||
────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.InventoryCore
|
||||
import Proofs.ScalarDenote
|
||||
import Proofs.ScalarLoop
|
||||
import Proofs.ScalarSubSpec
|
||||
import Proofs.ScalarAddSpec
|
||||
import Proofs.ScalarMulSpec
|
||||
import Proofs.ScalarMontSpec
|
||||
import Proofs.ScalarReduceSpec
|
||||
import Proofs.ScalarFullMulSpec
|
||||
import Proofs.ScalarMain
|
||||
import Proofs.ScalarWideSpec
|
||||
import Proofs.ScalarBytesSpec
|
||||
import Proofs.ScalarUnpackSpec
|
||||
import Proofs.ScalarFromBytesSpec
|
||||
open Lean Ed25519Inventory
|
||||
|
||||
/-- Exactly check-scalar.sh's PROOFS manifest; that script asserts the
|
||||
correspondence in both directions. -/
|
||||
def corpus : Array Name :=
|
||||
#[`Proofs.ScalarDenote, `Proofs.ScalarLoop, `Proofs.ScalarSubSpec, `Proofs.ScalarAddSpec, `Proofs.ScalarMulSpec, `Proofs.ScalarMontSpec, `Proofs.ScalarReduceSpec, `Proofs.ScalarFullMulSpec, `Proofs.ScalarMain, `Proofs.ScalarWideSpec, `Proofs.ScalarBytesSpec, `Proofs.ScalarUnpackSpec, `Proofs.ScalarFromBytesSpec]
|
||||
|
||||
#eval show MetaM Unit from emitInventory corpus
|
||||
|
|
@ -1,232 +1,45 @@
|
|||
#!/usr/bin/env bash
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
# check-scalar.sh — THE SECOND BUTTON (Scalar52 arithmetic mod ℓ).
|
||||
#
|
||||
# Scalar-layer check (Scalar52 arithmetic mod ℓ) — the layer is COMPLETE:
|
||||
# add, sub, Montgomery mul, and the byte-parsing chain, all kernel-audited.
|
||||
# Runs against the merged gen/CurveField universe (the scalar module lives
|
||||
# there since the merge; see extract.sh). Guarded compiles throughout.
|
||||
#
|
||||
# Brought to the same standard as check.sh on 2026-07-30 (P0-b). Before that
|
||||
# it was the weakest link in the estate, and increasingly so as the main button
|
||||
# was hardened: no source-integrity check, no harness pin, no dead-file gate,
|
||||
# no declaration inventory, an EVADABLE source-text grep for axioms where the
|
||||
# main button asks the kernel, and a count of matching output lines where the
|
||||
# main button asserts each certificate's cone individually.
|
||||
#
|
||||
# Phases:
|
||||
# 0 source integrity + harness pin (so running this button alone is also
|
||||
# protected, not only running it after check.sh)
|
||||
# 1 the two-button seam: every shipped proof source belongs to exactly one
|
||||
# of the two manifests, asserted against check.sh's, both directions
|
||||
# 2 compile the scalar layer, with a dead-file gate over Scalar*
|
||||
# 2b kernel-side axiom-declaration gate over the compiled artifacts
|
||||
# 2c environment-derived declaration inventory, diffed both directions
|
||||
# 3 per-certificate exact-cone audit
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -uo pipefail
|
||||
source ~/aeneas-toolchain/env.sh
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
||||
TIMEOUT="${LEAN_TIMEOUT:-300}"
|
||||
CORES="${LEAN_MAX_CORES:-0-3}"
|
||||
GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs)
|
||||
GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs) # MERGED GEN: scalar module now lives in CurveField
|
||||
PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec)
|
||||
# Fully-qualified scalar certificates. Each must report EXACTLY the standard
|
||||
# three axioms — asserted per certificate, not by counting how many lines of
|
||||
# output happened to match. A count cannot tell you WHICH certificate is clean.
|
||||
CERTS=(
|
||||
ScalarProofs.L_val
|
||||
ScalarProofs.sub_loop_spec
|
||||
ScalarProofs.sub_loop1_one_spec
|
||||
ScalarProofs.sub_val_spec
|
||||
ScalarProofs.add_val_spec
|
||||
ScalarProofs.mul_internal_spec
|
||||
ScalarProofs.part1_spec
|
||||
ScalarProofs.montgomery_reduce_spec
|
||||
ScalarProofs.mul_spec
|
||||
ScalarProofs.scalarImplementation
|
||||
ScalarProofs.montgomery_mul_spec
|
||||
ScalarProofs.bytes_unpack_spec
|
||||
ScalarProofs.from_bytes_wide_spec
|
||||
)
|
||||
EXPECTED="[propext, Classical.choice, Quot.sound]"
|
||||
|
||||
# ── Phase 0: source integrity + harness pin ─────────────────────────────────
|
||||
echo "=== Phase 0: source integrity + harness pin ==="
|
||||
free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}' || exit 1
|
||||
for f in "$HERE"/Proofs/Scalar*.lean; do
|
||||
[ -f "$f" ] || continue
|
||||
if ! grep -qE '^(/-|import |namespace |theorem |def |open |set_option |--)' "$f"; then
|
||||
echo "CORRUPTED: $f is not Lean source (olean clobber?). Restore: git checkout HEAD -- $f"
|
||||
exit 1
|
||||
fi
|
||||
done
|
||||
# The pin file and its policy live with check.sh; this button verifies the same
|
||||
# pins so that running it ALONE is protected too. If check.sh is absent the
|
||||
# harness is not pinned and that is a hard stop, not a warning.
|
||||
if [ ! -s "$HERE/HARNESS.sha256" ]; then
|
||||
echo "FATAL: HARNESS.sha256 is missing or empty — the harness is unpinned."; exit 1
|
||||
fi
|
||||
if ! ( cd "$HERE" && sha256sum -c --quiet HARNESS.sha256 ) ; then
|
||||
echo "FATAL: a harness file does not match its pin. The button you are running"
|
||||
echo "is not the button that was reviewed."; exit 1
|
||||
fi
|
||||
echo " sources valid; $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins"
|
||||
|
||||
# ── Phase 1: the two-button seam ────────────────────────────────────────────
|
||||
# The mirror of check.sh's Phase 1b. Each button reads the other's manifest, so
|
||||
# a new Proofs/ScalarX.lean cannot be absent from one by exemption and from the
|
||||
# other by omission — which is exactly what it was until today.
|
||||
echo "=== Phase 1: two-button seam ==="
|
||||
SEAMFAIL=0
|
||||
MAIN_SH="$HERE/check.sh"
|
||||
if [ ! -f "$MAIN_SH" ]; then
|
||||
echo " FATAL: check.sh is absent — most of the corpus would go unchecked."; exit 1
|
||||
fi
|
||||
MAIN_MANIFEST=$(sed -n '/^PROOFS=(/,/^)/p' "$MAIN_SH" | grep -oE '^ [A-Za-z][A-Za-z0-9]*' | tr -d ' ' | sort -u)
|
||||
if [ -z "$MAIN_MANIFEST" ]; then
|
||||
echo " FATAL: could not read check.sh's manifest; refusing to guess its scope."; exit 1
|
||||
fi
|
||||
SCALAR_MANIFEST=$(printf '%s\n' "${PROOFS[@]}" | sort -u)
|
||||
for f in "$HERE"/Proofs/*.lean; do
|
||||
b=$(basename "$f" .lean)
|
||||
case "$b" in AxiomCheck|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
|
||||
inm=0; ins=0
|
||||
grep -qx "$b" <<<"$MAIN_MANIFEST" && inm=1
|
||||
grep -qx "$b" <<<"$SCALAR_MANIFEST" && ins=1
|
||||
if [ $((inm + ins)) -eq 0 ]; then
|
||||
echo " ORPHAN: Proofs/$b.lean is in NEITHER manifest — compiled and audited by no button"; SEAMFAIL=1
|
||||
elif [ $((inm + ins)) -eq 2 ]; then
|
||||
echo " DOUBLE-CLAIMED: Proofs/$b.lean is in BOTH manifests"; SEAMFAIL=1
|
||||
fi
|
||||
done
|
||||
[ "$SEAMFAIL" = 0 ] && echo " every proof source belongs to exactly one button"
|
||||
[ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; }
|
||||
|
||||
# ── Phase 2: compile ────────────────────────────────────────────────────────
|
||||
echo "=== Phase 2: compile (guarded) ==="
|
||||
echo "=== stub/axiom audit ==="
|
||||
grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; }
|
||||
echo " clean"
|
||||
echo "=== compile (guarded) ==="
|
||||
cd "$AENEAS_LEAN"
|
||||
lake env bash -c "
|
||||
set -uo pipefail
|
||||
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||
for m in ${GEN[*]}; do echo \" · gen \$m\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done
|
||||
for m in ${GEN[*]}; do echo \" · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done
|
||||
cd '$HERE'
|
||||
for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
|
||||
# NO NAME-PREFIX DEAD-FILE GATE HERE. A Scalar* NAME does not imply this
|
||||
# button owns the file: Proofs/ScalarPackSpec.lean is in check.sh's manifest,
|
||||
# and a prefix gate demanded it be in this one. Phase 1 above is the correct
|
||||
# test and strictly stronger — it requires every proof source to be in
|
||||
# EXACTLY ONE of the two manifests, by membership rather than by spelling.
|
||||
for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
|
||||
" || { echo FAIL; exit 1; }
|
||||
|
||||
# ── Phase 2b: kernel-side axiom-declaration gate ────────────────────────────
|
||||
# The source-text grep this button used until today is evadable four ways on
|
||||
# Lean v4.30.0-rc2 (indented, @[simp], unsafe, and name-on-the-next-line — all
|
||||
# compile, none match an anchored pattern). Ask the kernel instead, reading the
|
||||
# compiled artifacts, exactly as check.sh Phase 2b does.
|
||||
echo "=== Phase 2b: kernel-side axiom-declaration gate ==="
|
||||
# The scanned set is this button's MANIFEST, not everything spelled Scalar*.
|
||||
# Proofs/ScalarPackSpec.lean is compiled by check.sh, so a glob swept in an
|
||||
# artifact this button does not own — and on a tree where check.sh had not run,
|
||||
# that olean is absent and the coverage count would fail for a false reason.
|
||||
SCALAR_OLEANS=$(printf '"%s.olean", ' "${PROOFS[@]}" | sed 's/, $//')
|
||||
GATE=$(mktemp "$HERE/.axgate-scalar-XXXX.lean")
|
||||
{
|
||||
echo "import Lean"
|
||||
echo "open Lean"
|
||||
echo "def expected : List String := [$SCALAR_OLEANS]"
|
||||
cat <<'LEANGATE'
|
||||
|
||||
run_cmd do
|
||||
let dir : System.FilePath := "Proofs"
|
||||
let mut errs : Array String := #[]
|
||||
let mut nMod := 0
|
||||
for name in expected do
|
||||
let p := dir / name
|
||||
-- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes
|
||||
-- this gate vacuous for that module, which must be an error, not a skip.
|
||||
unless (← p.pathExists) do
|
||||
throwError "COVERAGE: {name} is in the manifest but its compiled artifact is absent"
|
||||
nMod := nMod + 1
|
||||
let (mod, _) ← readModuleData p
|
||||
for ci in mod.constants do
|
||||
if ci matches .axiomInfo _ then
|
||||
errs := errs.push s!" {name}: {ci.name}"
|
||||
unless errs.isEmpty do
|
||||
throwError "AXIOM DECLARED in the scalar layer:\n{String.intercalate "\n" errs.toList}"
|
||||
logInfo s!" kernel confirms: {nMod} compiled scalar modules (the manifest, by membership), none declares an axiom"
|
||||
LEANGATE
|
||||
} > "$GATE"
|
||||
cd "$AENEAS_LEAN"
|
||||
GATE_RC=0
|
||||
lake env bash -c "
|
||||
set -uo pipefail
|
||||
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||
cd '$HERE'
|
||||
LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$GATE'
|
||||
" || GATE_RC=$?
|
||||
rm -f "$GATE" "${GATE%.lean}.olean"
|
||||
[ "$GATE_RC" -eq 0 ] || { echo "SCALAR AXIOM GATE FAILED"; exit 1; }
|
||||
|
||||
# ── Phase 2c: declaration inventory ─────────────────────────────────────────
|
||||
# Until today these 13 modules were the only part of the proof corpus with no
|
||||
# declaration inventory: check.sh Phase 2c covers the main chain and named them
|
||||
# as uncovered on every run. This closes that.
|
||||
echo "=== Phase 2c: scalar declaration inventory ==="
|
||||
INVFAIL=0
|
||||
INVLOG=$(mktemp /tmp/check-scalar-inv-XXXX.log)
|
||||
echo "=== Phase 3: axiom audit (kernel-level) ==="
|
||||
cd "$AENEAS_LEAN"
|
||||
lake env bash -c "
|
||||
set -uo pipefail
|
||||
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||
cd '$HERE'
|
||||
LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=8192 '$HERE/lean-guard' Proofs/InventoryScalar.lean
|
||||
" > "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "SCALAR INVENTORY COMPILE FAILED"; rm -f "$INVLOG"; exit 1; }
|
||||
OBS=$(mktemp /tmp/check-scalar-obs-XXXX.log)
|
||||
grep -E '^INV\|' "$INVLOG" > "$OBS"
|
||||
grep '^INV-COUNT|' "$INVLOG" | tail -1 >> "$OBS"
|
||||
"$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist-scalar.txt" || INVFAIL=1
|
||||
rm -f "$INVLOG" "$OBS"
|
||||
# The driver's corpus list must BE this script's manifest, both directions.
|
||||
COVERED=$(grep -oE '`Proofs\.[A-Za-z0-9]+' "$HERE/Proofs/InventoryScalar.lean" | sed 's/`Proofs\.//' | sort -u)
|
||||
for m in "${PROOFS[@]}"; do
|
||||
grep -qx "$m" <<<"$COVERED" || { echo " UNINVENTORIED: $m is compiled here but the driver does not cover it"; INVFAIL=1; }
|
||||
done
|
||||
while read -r m; do
|
||||
[ -z "$m" ] && continue
|
||||
case " ${PROOFS[*]} " in (*" $m "*) ;; (*) echo " PHANTOM: driver claims $m, not in this manifest"; INVFAIL=1;; esac
|
||||
done <<<"$COVERED"
|
||||
[ "$INVFAIL" = 0 ] || { echo "SCALAR INVENTORY FAILED"; exit 1; }
|
||||
|
||||
# ── Phase 3: per-certificate exact-cone audit ───────────────────────────────
|
||||
# Was: count the lines of #print axioms output that matched the clean cone and
|
||||
# compare against 13. A count cannot say WHICH certificate is clean, and it
|
||||
# passes just as happily if one certificate's cone is reported twice. Each
|
||||
# certificate is now asserted by name.
|
||||
echo "=== Phase 3: per-certificate exact-cone audit ==="
|
||||
cd "$AENEAS_LEAN"
|
||||
AUD_OUT=$(lake env bash -c "
|
||||
set -uo pipefail
|
||||
export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
|
||||
cd '$HERE'
|
||||
AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean')
|
||||
{ echo 'import Proofs.ScalarFromBytesSpec'; echo 'import Proofs.ScalarMain'; echo 'import Proofs.ScalarUnpackSpec'; echo 'import Proofs.ScalarWideSpec'
|
||||
for c in ${CERTS[*]}; do echo \"#print axioms \$c\"; done; } > \"\$AUD\"
|
||||
OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
|
||||
rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
|
||||
{ echo 'import Proofs.ScalarMain'; echo 'import Proofs.ScalarWideSpec'; echo 'import Proofs.ScalarUnpackSpec'; echo 'import Proofs.ScalarFromBytesSpec'; echo '#print axioms ScalarProofs.L_val'
|
||||
echo '#print axioms ScalarProofs.sub_loop_spec'
|
||||
echo '#print axioms ScalarProofs.sub_loop1_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; echo '#print axioms ScalarProofs.mul_internal_spec'
|
||||
echo '#print axioms ScalarProofs.part1_spec'; echo '#print axioms ScalarProofs.montgomery_reduce_spec'; echo '#print axioms ScalarProofs.mul_spec'; echo '#print axioms ScalarProofs.scalarImplementation'; echo '#print axioms ScalarProofs.montgomery_mul_spec'; echo '#print axioms ScalarProofs.bytes_unpack_spec'; echo '#print axioms ScalarProofs.from_bytes_wide_spec'; } > \"\$AUD\"
|
||||
OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
|
||||
echo \"\$OUT\"
|
||||
") || { echo "$AUD_OUT"; echo "SCALAR AUDIT COMPILE FAILED"; exit 1; }
|
||||
FLAT=$(tr '\n' ' ' <<<"$AUD_OUT" | tr -s ' ')
|
||||
AUDFAIL=0
|
||||
for c in "${CERTS[@]}"; do
|
||||
grep -qF "'$c' depends on axioms: $EXPECTED" <<<"$FLAT" \
|
||||
|| { echo " NOT CLEAN or NOT FOUND: $c"; AUDFAIL=1; }
|
||||
done
|
||||
if [ "$AUDFAIL" != 0 ]; then
|
||||
echo "SCALAR AXIOM AUDIT FAILED"; echo "$AUD_OUT" | tail -20 | sed 's/^/ /'; exit 1
|
||||
fi
|
||||
echo " ${#CERTS[@]}/${#CERTS[@]} scalar certificates report exactly $EXPECTED"
|
||||
rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
|
||||
N=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || true)
|
||||
[ \"\$N\" -eq 13 ] || { echo \"AXIOM AUDIT FAILED: \$N/13 clean\"; exit 1; }
|
||||
" || { echo FAIL; exit 1; }
|
||||
echo " L_val axiom-clean"
|
||||
|
||||
echo ""
|
||||
echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round"
|
||||
echo "through RR) proven mod ℓ; aggregate certificate scalarImplementation"
|
||||
echo "kernel-audited; declaration surface inventoried; harness pinned."
|
||||
echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round through RR) proven mod ℓ; aggregate certificate scalarImplementation kernel-audited."
|
||||
|
|
|
|||
|
|
@ -37,41 +37,6 @@ TIMEOUT="${LEAN_TIMEOUT:-300}"
|
|||
export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}" # 8192: ReduceSpec exceeds 6144 (coherence pass 2)
|
||||
CORES="${LEAN_MAX_CORES:-0-3}"
|
||||
|
||||
# ── Mode selection ──────────────────────────────────────────────────────────
|
||||
# --audit-only runs every gate EXCEPT the compile, against the .olean files a
|
||||
# previous full run left behind. It exists because gate work dominates this
|
||||
# estate's wall-clock: on 2026-07-29, 3.9 hours of a session went to Lean
|
||||
# re-elaborating proofs nobody had edited, while the audit phases themselves
|
||||
# take about fifteen seconds.
|
||||
#
|
||||
# IT MUST BE IMPOSSIBLE TO MISUSE, so:
|
||||
# · it refuses to run unless a previous FULL run recorded a basis of source
|
||||
# hashes AND every source still matches it byte-for-byte. Not mtimes —
|
||||
# `touch` defeats those, and a stale-artifact check that fails open is
|
||||
# worse than no shortcut at all, because a green button would then
|
||||
# describe a corpus that is no longer on disk;
|
||||
# · the basis file is build state, never committed, so a fresh clone cannot
|
||||
# inherit permission to skip compiling;
|
||||
# · the final banner DIFFERS, and says in words that the run is not evidence.
|
||||
# A transcript must never be mistakable for a full one.
|
||||
AUDIT_ONLY=0
|
||||
for arg in "$@"; do
|
||||
case "$arg" in
|
||||
--audit-only) AUDIT_ONLY=1 ;;
|
||||
--help|-h) echo "usage: check.sh [--audit-only]"; exit 0 ;;
|
||||
*) echo "unknown argument: $arg (see --help)"; exit 1 ;;
|
||||
esac
|
||||
done
|
||||
BASIS="$HERE/.audit-basis" # gitignored build state, written by full runs
|
||||
|
||||
# Every .lean this repository ships, with its hash: the exact set whose
|
||||
# recompilation --audit-only proposes to skip.
|
||||
source_basis() {
|
||||
{ find "$HERE/Proofs" -name '*.lean' -type f -printf '%P\n' | sed 's|^|Proofs/|'
|
||||
find "$HERE/gen" -name '*.lean' -type f -printf '%P\n' | sed 's|^|gen/|'; } \
|
||||
| LC_ALL=C sort | while read -r f; do printf '%s %s\n' "$(sha256sum "$HERE/$f" | cut -d' ' -f1)" "$f"; done
|
||||
}
|
||||
|
||||
# Layer manifests (extended as the pyramid grows; ORDER = import order).
|
||||
GEN_MODULES=(
|
||||
CurveField/TypesExternal
|
||||
|
|
@ -240,14 +205,9 @@ echo " $(wc -l < "$HERE/GEN-MODEL.sha256") extracted-model files match their pi
|
|||
# the audit driver, the committed manifests, the policy tables — cannot be
|
||||
# discovered that way and are listed explicitly.
|
||||
HARNESS_EXTRA=(
|
||||
AUDIT-MANIFEST.txt # the statement block Phase 3c's digest is taken over
|
||||
GEN-MODEL.sha256 # the extracted-model pins Phase 0b enforces
|
||||
inventory-allowlist.txt # the audit surface Phase 2c diffs against
|
||||
inventory-allowlist-scalar.txt # the scalar layer's audit surface (second button)
|
||||
Proofs/Audit.lean # the audit driver: it computes the digest it is judged by
|
||||
Proofs/InventoryCore.lean # inventory machinery
|
||||
Proofs/InventoryScalar.lean # inventory driver: the scalar layer
|
||||
Proofs/Inventory.lean # inventory driver: main chain
|
||||
AUDIT-MANIFEST.txt # the statement block Phase 3c's digest is taken over
|
||||
GEN-MODEL.sha256 # the extracted-model pins Phase 0b enforces
|
||||
Proofs/Audit.lean # the audit driver: it computes the digest it is judged by
|
||||
)
|
||||
echo "=== Phase 0c: harness integrity ==="
|
||||
if [ ! -s "$HERE/HARNESS.sha256" ]; then
|
||||
|
|
@ -288,80 +248,7 @@ if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lea
|
|||
fi
|
||||
echo " clean: no trivial stubs, no True targets, no axioms outside gen/"
|
||||
|
||||
# ── Phase 1b: the two-button seam ───────────────────────────────────────────
|
||||
# WHY. This repository is checked by TWO buttons: this script covers the field,
|
||||
# curve and signature layers, and check-scalar.sh covers the scalar layer.
|
||||
# Until 2026-07-30 neither asserted anything about the other's scope, and this
|
||||
# script's dead-file gate simply SKIPPED anything named Scalar*. A new
|
||||
# Proofs/ScalarX.lean was therefore gated by nothing at all: absent from this
|
||||
# manifest by exemption, absent from the other by omission, compiled by
|
||||
# neither, inventoried by neither.
|
||||
#
|
||||
# The fix is mutual: each button reads the OTHER's manifest and asserts that
|
||||
# every shipped proof source belongs to exactly one of them. Both directions,
|
||||
# so a file can neither fall between the two nor be claimed by both.
|
||||
echo "=== Phase 1b: two-button seam ==="
|
||||
SEAMFAIL=0
|
||||
SCALAR_SH="$HERE/check-scalar.sh"
|
||||
if [ ! -f "$SCALAR_SH" ]; then
|
||||
echo " FATAL: check-scalar.sh is absent — half the corpus would go unchecked."
|
||||
exit 1
|
||||
fi
|
||||
SCALAR_MANIFEST=$(grep -m1 '^PROOFS=(' "$SCALAR_SH" | sed 's/^PROOFS=(//; s/).*$//' | tr ' ' '\n' | sed '/^$/d' | sort -u)
|
||||
if [ -z "$SCALAR_MANIFEST" ]; then
|
||||
echo " FATAL: could not read check-scalar.sh's manifest; refusing to guess its scope."
|
||||
exit 1
|
||||
fi
|
||||
MAIN_MANIFEST=$(printf '%s\n' "${PROOFS[@]}" | sort -u)
|
||||
# 1. Every shipped proof source belongs to exactly one manifest.
|
||||
for f in "$HERE"/Proofs/*.lean; do
|
||||
b=$(basename "$f" .lean)
|
||||
case "$b" in AxiomCheck|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
|
||||
inm=0; ins=0
|
||||
grep -qx "$b" <<<"$MAIN_MANIFEST" && inm=1
|
||||
grep -qx "$b" <<<"$SCALAR_MANIFEST" && ins=1
|
||||
if [ $((inm + ins)) -eq 0 ]; then
|
||||
echo " ORPHAN: Proofs/$b.lean is in NEITHER manifest — compiled and audited by no button"; SEAMFAIL=1
|
||||
elif [ $((inm + ins)) -eq 2 ]; then
|
||||
echo " DOUBLE-CLAIMED: Proofs/$b.lean is in BOTH manifests — the buttons disagree about scope"; SEAMFAIL=1
|
||||
fi
|
||||
done
|
||||
# 2. Neither manifest may name a file that does not exist.
|
||||
while read -r m; do
|
||||
[ -z "$m" ] && continue
|
||||
[ -f "$HERE/Proofs/$m.lean" ] || { echo " PHANTOM: check-scalar.sh lists $m, which does not exist"; SEAMFAIL=1; }
|
||||
done <<<"$SCALAR_MANIFEST"
|
||||
[ "$SEAMFAIL" = 0 ] && echo " every proof source belongs to exactly one button ($(grep -c . <<<"$MAIN_MANIFEST") here, $(grep -c . <<<"$SCALAR_MANIFEST") scalar)"
|
||||
[ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; }
|
||||
# ── Phase 2: compile everything shipped ─────────────────────────────────────
|
||||
if [ "$AUDIT_ONLY" = 1 ]; then
|
||||
echo "=== Phase 2: SKIPPED (--audit-only) ==="
|
||||
if [ ! -s "$BASIS" ]; then
|
||||
echo "REFUSING: no basis from a previous full run ($BASIS absent)."
|
||||
echo " --audit-only may only follow a full green run in this working tree."
|
||||
echo " Run ./check.sh with no arguments first."
|
||||
exit 1
|
||||
fi
|
||||
if ! diff -q <(source_basis) "$BASIS" >/dev/null 2>&1; then
|
||||
echo "REFUSING: the sources no longer match the basis of the last full run."
|
||||
echo " The .olean files on disk describe a corpus that has changed, so every"
|
||||
echo " audit below would be judging artifacts that no source produces."
|
||||
echo " Differences (< basis, > now):"
|
||||
diff <(source_basis) "$BASIS" | head -20 | sed 's/^/ /'
|
||||
echo " Run ./check.sh with no arguments."
|
||||
exit 1
|
||||
fi
|
||||
# Fail closed on absence too: a source with no artifact cannot be audited.
|
||||
MISSING=0
|
||||
for m in "${PROOFS[@]}"; do
|
||||
[ -f "$HERE/Proofs/$m.olean" ] || { echo " MISSING ARTIFACT: Proofs/$m.olean"; MISSING=1; }
|
||||
done
|
||||
for m in "${GEN_MODULES[@]}"; do
|
||||
[ -f "$HERE/gen/$m.olean" ] || { echo " MISSING ARTIFACT: gen/$m.olean"; MISSING=1; }
|
||||
done
|
||||
[ "$MISSING" = 0 ] || { echo "REFUSING: run ./check.sh with no arguments."; exit 1; }
|
||||
echo " sources byte-identical to the last full run's basis; $(grep -c . "$BASIS") files"
|
||||
else
|
||||
echo "=== Phase 2: compile ==="
|
||||
LOG=$(mktemp /tmp/check-compile-XXXX.log)
|
||||
cd "$AENEAS_LEAN"
|
||||
|
|
@ -382,11 +269,6 @@ lake env bash -c "
|
|||
for f in Proofs/*.lean; do
|
||||
b=\$(basename \"\$f\" .lean)
|
||||
[ \"\$b\" = AxiomCheck ] && continue
|
||||
# Inventory drivers are compiled by Phase 2c, not here: they must elaborate
|
||||
# with the corpus already in the environment, and the two of them cannot be
|
||||
# imported together. They are NOT unchecked — Phase 2b reads their compiled
|
||||
# .olean like every other module, and Phase 0c pins their sources.
|
||||
case \"\$b\" in Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
|
||||
case \"\$b\" in Scalar*) continue;; esac # scalar layer: checked by check-scalar.sh (coherence pass 2)
|
||||
case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f not in check manifest\"; exit 1;; esac
|
||||
done
|
||||
|
|
@ -394,7 +276,6 @@ lake env bash -c "
|
|||
if grep -q "uses 'sorry'" "$LOG"; then
|
||||
echo "STUB DETECTED: a compiled declaration uses 'sorry'"; exit 1; fi
|
||||
rm -f "$LOG"
|
||||
fi
|
||||
|
||||
# ── Phase 2b: kernel-side axiom-declaration gate ────────────────────────────
|
||||
# WHY THIS EXISTS. Phase 1's anti-smuggling check reads SOURCE TEXT, and a
|
||||
|
|
@ -473,88 +354,6 @@ if [ "$GATE_RC" -ne 0 ]; then
|
|||
exit 1
|
||||
fi
|
||||
|
||||
# ── Phase 2c: environment-derived declaration inventory ─────────────────────
|
||||
# WHAT THIS ADDS over Phase 2b. Phase 2b asks the kernel whether any AXIOM is
|
||||
# declared under Proofs/. It says nothing about the ~3000 other declarations:
|
||||
# a `def` or `theorem` whose cone quietly acquired an oracle, a declaration
|
||||
# renamed, added or removed, or a compiler-generated auxiliary that changed
|
||||
# shape, all pass 2b unremarked.
|
||||
#
|
||||
# This phase pins the whole surface. Every constant originating in an audited
|
||||
# module contributes NAME, MODULE, KIND and full AXIOM CONE, and the observed
|
||||
# set must equal inventory-allowlist.txt EXACTLY, both directions:
|
||||
# UNCLASSIFIED (in the environment, not allowlisted) and STALE (allowlisted,
|
||||
# not in the environment) are both build failures.
|
||||
#
|
||||
# PORTED from ltl-accumulator-verified, where a nine-attack self-test proved a
|
||||
# source-regex enumerator evadable by attributed, private, indented and
|
||||
# `instance` declarations and by a nested-namespace basename collision.
|
||||
#
|
||||
# TWO DRIVERS, because this corpus cannot be imported as one environment:
|
||||
# Proofs.Basic and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec.
|
||||
# The records carry their originating module precisely so those two remain
|
||||
# distinct entries — keyed on name alone they were byte-identical, and the
|
||||
# merged allowlist covered 3022 declarations with 3021 entries.
|
||||
echo "=== Phase 2c: environment-derived declaration inventory ==="
|
||||
INVFAIL=0
|
||||
INVLOG=$(mktemp /tmp/check-inv-XXXX.log)
|
||||
cd "$AENEAS_LEAN"
|
||||
# The DRIVERS are discovered, not listed: whether this corpus needs one or two
|
||||
# is a per-repo fact (dalek and anza cannot import Proofs.Basic together with
|
||||
# Proofs.ConstSpecs; risc0 and betrusted have no Proofs.Basic at all). A
|
||||
# hardcoded pair would silently look for a file that does not exist here.
|
||||
DRIVERS=$(ls "$HERE"/Proofs/Inventory*.lean 2>/dev/null | xargs -r -n1 basename \
|
||||
| sed 's/\.lean$//' | grep -vE '^(InventoryCore|InventoryScalar)$' | sort)
|
||||
# InventoryScalar belongs to check-scalar.sh, which compiles the modules it
|
||||
# covers. Globbing Inventory*.lean swept it in here, after which this phase
|
||||
# correctly complained that its own manifest lacks the scalar modules.
|
||||
if [ -z "$DRIVERS" ]; then
|
||||
echo " NO INVENTORY DRIVER FOUND — the audit surface would go unchecked."; exit 1
|
||||
fi
|
||||
N_DRIVERS=$(printf '%s\n' "$DRIVERS" | grep -c .)
|
||||
for drv in $DRIVERS; do
|
||||
lake env bash -c "
|
||||
set -uo pipefail
|
||||
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
|
||||
cd '$HERE'
|
||||
LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=8192 '$HERE/lean-guard' Proofs/$drv.lean
|
||||
" >> "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "INVENTORY COMPILE FAILED ($drv)"; rm -f "$INVLOG"; exit 1; }
|
||||
done
|
||||
# Reconcile the two trailers into one. Summing them and comparing against the
|
||||
# lines actually collected preserves the integrity property in the presence of
|
||||
# the split: truncation in EITHER driver shows up as a mismatch.
|
||||
N_TRAILERS=$(grep -c '^INV-COUNT|' "$INVLOG")
|
||||
if [ "$N_TRAILERS" -ne "$N_DRIVERS" ]; then
|
||||
echo " INVENTORY INCOMPLETE: expected a count trailer from each of the $N_DRIVERS driver(s), saw $N_TRAILERS"
|
||||
INVFAIL=1
|
||||
fi
|
||||
SUM=$(grep '^INV-COUNT|' "$INVLOG" | cut -d'|' -f2 | paste -sd+ - | bc)
|
||||
OBS=$(mktemp /tmp/check-inv-obs-XXXX.log)
|
||||
grep '^INV|' "$INVLOG" > "$OBS"
|
||||
echo "INV-COUNT|${SUM:-0}" >> "$OBS"
|
||||
"$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist.txt" || INVFAIL=1
|
||||
rm -f "$INVLOG" "$OBS"
|
||||
|
||||
# The drivers' corpus lists must together BE the compile manifest, minus the
|
||||
# audit infrastructure and the scalar layer. Checked in both directions so a
|
||||
# module cannot fall between the two drivers, and NO SILENT TRUNCATION: what
|
||||
# this phase does not cover is named on stdout every run.
|
||||
COVERED=$(for d in $DRIVERS; do grep -ohE '`Proofs\.[A-Za-z0-9]+' "$HERE/Proofs/$d.lean"; done \
|
||||
| sed 's/`Proofs\.//' | sort -u)
|
||||
for m in "${PROOFS[@]}"; do
|
||||
case "$m" in Audit|Inventory|InventoryBasic|InventoryCore) continue;; esac
|
||||
grep -qx "$m" <<<"$COVERED" || { echo " UNINVENTORIED: $m is compiled by this script but no driver covers it"; INVFAIL=1; }
|
||||
done
|
||||
while read -r m; do
|
||||
[ -z "$m" ] && continue
|
||||
case " ${PROOFS[*]} " in (*" $m "*) ;; (*) echo " PHANTOM: driver claims $m, which this script does not compile"; INVFAIL=1;; esac
|
||||
done <<<"$COVERED"
|
||||
for f in "$HERE"/Proofs/*.lean; do
|
||||
b=$(basename "$f" .lean)
|
||||
case "$b" in Audit|Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
|
||||
grep -qx "$b" <<<"$COVERED" || echo " NOT INVENTORIED HERE (separate button): Proofs/$b.lean"
|
||||
done
|
||||
[ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; }
|
||||
# ── Phase 3: axiom audit of every certificate ───────────────────────────────
|
||||
echo "=== Phase 3: axiom audit ==="
|
||||
EXPECTED="[propext, Classical.choice, Quot.sound]"
|
||||
|
|
@ -701,22 +500,6 @@ fi
|
|||
grep -o 'statement audit PASSED:.*' <<<"$AUD_OUT" | sed 's/^/ /'
|
||||
echo " audit-manifest sha256 = $GOT_SHA (matches the committed block byte-for-byte)"
|
||||
|
||||
# ── Phases end ──────────────────────────────────────────────────────────────
|
||||
# Sentinel. Self-tests lift a phase by scanning from its header to the NEXT
|
||||
# marker; without this the final phase's lift ran to end-of-file and picked up
|
||||
# everything appended afterwards. Do not remove: anything added below this line
|
||||
# would otherwise silently become part of the last phase from a lifter's point
|
||||
# of view.
|
||||
|
||||
echo ""
|
||||
if [ "$AUDIT_ONLY" = 1 ]; then
|
||||
echo "AUDIT-ONLY RUN — GATES PASSED, PROOFS NOT RECOMPILED."
|
||||
echo "This is NOT evidence: the kernel did not re-elaborate a single proof in"
|
||||
echo "this run. It says the gates accept the artifacts a previous full run"
|
||||
echo "left behind. For a recorded result, run ./check.sh with no arguments."
|
||||
exit 0
|
||||
fi
|
||||
# Only a full run earns the right to let a later --audit-only skip compiling.
|
||||
source_basis > "$BASIS"
|
||||
echo "ALL PROOFS PASS. ALL CERTIFICATES AXIOM-CLEAN. NO DEAD FILES."
|
||||
echo "STATEMENTS AND SPECIFICATIONS BOUND TO THE COMMITTED AUDIT MANIFEST."
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load diff
File diff suppressed because it is too large
Load diff
|
|
@ -1,64 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
# inventory_gate.sh — diff an observed environment inventory against the
|
||||
# pinned allowlist. PORTED VERBATIM from ltl-accumulator-verified apart from
|
||||
# the axiom-surface assertion, which is repo-specific: there the corpus admits
|
||||
# exactly one sanctioned axiom, here it admits none.
|
||||
#
|
||||
# This is THE production coverage gate: check.sh Phase 2c calls it, and the
|
||||
# self-test exercises this exact script — the tested logic IS the shipping
|
||||
# logic.
|
||||
#
|
||||
# Usage: inventory_gate.sh <observed-lean-output> <allowlist-file>
|
||||
#
|
||||
# Fail-closed in BOTH directions:
|
||||
# UNCLASSIFIED — constant in the environment, absent from the allowlist
|
||||
# (new/renamed decl, changed kind, or changed axiom cone)
|
||||
# STALE — allowlist entry absent from the environment
|
||||
# plus an output-integrity check: the INV-COUNT trailer emitted by
|
||||
# Proofs/Inventory.lean must equal the number of INV lines actually seen,
|
||||
# so a truncated or crashed run can never pass as an empty diff.
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -uo pipefail
|
||||
export LC_ALL=C # byte-order collation: sort/comm must agree with Lean's String order
|
||||
obs_file="$1"; allow_file="$2"
|
||||
|
||||
OBS=$(grep '^INV|' "$obs_file" | sort -u)
|
||||
N_OBS=$(printf '%s' "$OBS" | grep -c '^INV|' || true)
|
||||
TRAILER=$(grep '^INV-COUNT|' "$obs_file" | tail -1 | cut -d'|' -f2)
|
||||
if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_OBS" ]; then
|
||||
echo " INVENTORY TRUNCATED: trailer=${TRAILER:-absent}, observed $N_OBS lines"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
ALLOW=$(grep '^INV|' "$allow_file" | sort -u)
|
||||
FAILGATE=0
|
||||
UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
|
||||
STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
|
||||
if [ -n "$UNCLASS" ]; then
|
||||
printf '%s\n' "$UNCLASS" | sed 's/^/ UNCLASSIFIED (in environment, not allowlisted): /'
|
||||
FAILGATE=1
|
||||
fi
|
||||
if [ -n "$STALE" ]; then
|
||||
printf '%s\n' "$STALE" | sed 's/^/ STALE (allowlisted, not in environment): /'
|
||||
FAILGATE=1
|
||||
fi
|
||||
|
||||
# The audited corpus admits NO axiom declarations at all: the sanctioned
|
||||
# external models live in gen/, outside every module these drivers cover, and
|
||||
# are byte-pinned by Phase 0b. An axiom appearing here would be a declaration
|
||||
# smuggled into the proof corpus, which Phase 2b also catches kernel-side —
|
||||
# two independent gates on the same property, deliberately.
|
||||
AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true)
|
||||
if [ -n "$AXLINES" ]; then
|
||||
echo " AXIOM SURFACE DRIFT: the audited corpus must declare no axioms; observed:"
|
||||
printf '%s\n' "$AXLINES" | sed 's/^/ /'
|
||||
FAILGATE=1
|
||||
fi
|
||||
|
||||
# The message must describe what was actually checked. It said "single
|
||||
# sanctioned axiom" when ported, which is the accumulator's policy; here the
|
||||
# audited corpus permits NONE, and a success line describing a different rule
|
||||
# is how an assertion quietly stops meaning anything.
|
||||
[ "$FAILGATE" = 0 ] && echo " inventory gate: $N_OBS constants, environment == allowlist, zero axioms declared in the audited corpus"
|
||||
exit "$FAILGATE"
|
||||
|
|
@ -1,112 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
# selftest-auditonly.sh — adversarial self-test for check.sh --audit-only.
|
||||
#
|
||||
# --audit-only skips recompilation, which makes it the most dangerous thing in
|
||||
# this repository: if it ever accepted a tree whose sources had changed, a green
|
||||
# transcript would describe a corpus that is not on disk. Its whole safety rests
|
||||
# on refusing, so refusal is what this tests.
|
||||
#
|
||||
# Cases, each asserting a SPECIFIC diagnostic:
|
||||
# 0 no basis recorded -> REFUSING, may only follow a full run
|
||||
# 1 a proof source edited by one comment -> REFUSING, sources no longer match
|
||||
# 2 a proof source DELETED -> REFUSING (the basis lists it)
|
||||
# 3 a NEW proof source added -> ORPHAN, from the seam check,
|
||||
# which runs BEFORE the mode gate and catches it first
|
||||
# 4 an artifact deleted, sources intact -> MISSING ARTIFACT
|
||||
# 5 the basis file truncated -> REFUSING (mismatch, not a pass)
|
||||
# 6 mtimes touched but bytes unchanged -> PASSES, because bytes are the
|
||||
# test and mtimes are not: `touch` must neither grant nor deny permission
|
||||
#
|
||||
# Requires a prior full green run in this tree (that is what writes the basis).
|
||||
# No Lean runs here; the whole thing takes seconds.
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -uo pipefail
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
FAILURES=0
|
||||
STASH="$(mktemp -d)"
|
||||
BASIS="$HERE/.audit-basis"
|
||||
VICTIM_SRC="Proofs/FeQ.lean"
|
||||
VICTIM_ART="Proofs/FeQ.olean"
|
||||
NEWSRC="$HERE/Proofs/ZZAuditOnlyProbe.lean"
|
||||
|
||||
cleanup() {
|
||||
[ -f "$STASH/basis" ] && cp "$STASH/basis" "$BASIS"
|
||||
[ -f "$STASH/src" ] && cp "$STASH/src" "$HERE/$VICTIM_SRC"
|
||||
[ -f "$STASH/art" ] && cp "$STASH/art" "$HERE/$VICTIM_ART"
|
||||
rm -f "$NEWSRC" "${NEWSRC%.lean}.olean"
|
||||
rm -rf "$STASH"
|
||||
}
|
||||
trap cleanup EXIT INT TERM
|
||||
|
||||
if [ ! -s "$BASIS" ]; then
|
||||
echo "FATAL: no basis in this tree. Run ./check.sh with no arguments first;"
|
||||
echo "this self-test exercises --audit-only, which requires one."
|
||||
exit 1
|
||||
fi
|
||||
cp "$BASIS" "$STASH/basis"
|
||||
cp "$HERE/$VICTIM_SRC" "$STASH/src"
|
||||
cp "$HERE/$VICTIM_ART" "$STASH/art"
|
||||
|
||||
expect() { # expect <label> <want-rc> <want-substring>
|
||||
local label="$1" want_rc="$2" want_txt="$3" out rc
|
||||
out=$( cd "$HERE" && ./check.sh --audit-only 2>&1 ); rc=$?
|
||||
if [ "$rc" -ne "$want_rc" ]; then
|
||||
echo " ✗ $label: exit $rc, expected $want_rc"; tail -6 <<<"$out" | sed 's/^/ /'
|
||||
FAILURES=$((FAILURES+1)); return
|
||||
fi
|
||||
if ! grep -qF "$want_txt" <<<"$out"; then
|
||||
echo " ✗ $label: exit code right, diagnostic wrong (refused for the wrong reason)"
|
||||
echo " wanted: $want_txt"; tail -6 <<<"$out" | sed 's/^/ /'
|
||||
FAILURES=$((FAILURES+1)); return
|
||||
fi
|
||||
echo " ✓ $label"
|
||||
}
|
||||
|
||||
echo "=== selftest-auditonly: attacking check.sh --audit-only ==="
|
||||
|
||||
expect "control: unchanged tree passes" 0 "sources byte-identical to the last full run"
|
||||
|
||||
rm -f "$BASIS"
|
||||
expect "case 0: no basis recorded" 1 "may only follow a full green run"
|
||||
cp "$STASH/basis" "$BASIS"
|
||||
|
||||
printf '\n-- selftest\n' >> "$HERE/$VICTIM_SRC"
|
||||
expect "case 1: a proof source edited by one comment" 1 "no longer match the basis"
|
||||
cp "$STASH/src" "$HERE/$VICTIM_SRC"
|
||||
|
||||
mv "$HERE/$VICTIM_SRC" "$STASH/moved"
|
||||
expect "case 2: a proof source deleted" 1 "no longer match the basis"
|
||||
mv "$STASH/moved" "$HERE/$VICTIM_SRC"
|
||||
|
||||
# A new source is refused EARLIER than the basis comparison: the seam check
|
||||
# (Phase 1b) runs first and reports it as belonging to no manifest. Asserting
|
||||
# the seam's diagnostic rather than the basis's is not a weaker test — it is the
|
||||
# true one, and demanding the basis message here would go red the day the seam
|
||||
# check does its job.
|
||||
printf 'namespace ZZProbe\ntheorem t : 1 = 1 := rfl\nend ZZProbe\n' > "$NEWSRC"
|
||||
expect "case 3: a new proof source added -> caught by the seam check first" 1 "is in NEITHER manifest"
|
||||
rm -f "$NEWSRC"
|
||||
|
||||
mv "$HERE/$VICTIM_ART" "$STASH/movedart"
|
||||
expect "case 4: an artifact deleted, sources intact" 1 "MISSING ARTIFACT"
|
||||
mv "$STASH/movedart" "$HERE/$VICTIM_ART"
|
||||
|
||||
head -3 "$STASH/basis" > "$BASIS"
|
||||
expect "case 5: the basis truncated" 1 "no longer match the basis"
|
||||
cp "$STASH/basis" "$BASIS"
|
||||
|
||||
# BYTES, NOT MTIMES. Touching every source must change nothing: a check keyed on
|
||||
# timestamps would both deny this legitimate run and, worse, ACCEPT a modified
|
||||
# file whose mtime had been reset. Asserting the pass is what pins that choice.
|
||||
find "$HERE/Proofs" "$HERE/gen" -name '*.lean' -exec touch {} +
|
||||
expect "case 6: mtimes touched, bytes unchanged -> still passes" 0 "sources byte-identical to the last full run"
|
||||
|
||||
echo ""
|
||||
if [ "$FAILURES" -eq 0 ]; then
|
||||
echo "SELFTEST PASSED — --audit-only refuses every stale tree it was shown, and"
|
||||
echo "accepts only one whose sources are byte-identical to the recorded basis."
|
||||
exit 0
|
||||
fi
|
||||
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
|
||||
exit 1
|
||||
|
|
@ -43,24 +43,13 @@ DRIVER="$STASH/phase2b.sh"
|
|||
echo "HERE=\"$HERE\""
|
||||
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
|
||||
echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
|
||||
# Stop at the NEXT phase marker, whatever it is called. A hardcoded
|
||||
# terminator ("...to Phase 3") silently widens the moment a phase is
|
||||
# inserted between the two: adding Phase 2c made this driver swallow 2c as
|
||||
# well and die on variables that phase expects check.sh to have defined,
|
||||
# which surfaced as the BASELINE failing — a self-test blaming a gate for
|
||||
# its own extraction bug.
|
||||
awk '/^# ── Phase 2b/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 2b/{exit} f{print}' "$HERE/check.sh"
|
||||
sed -n '/^# ── Phase 2b/,/^# ── Phase 3/p' "$HERE/check.sh" | sed '$d'
|
||||
} > "$DRIVER"
|
||||
if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then
|
||||
echo "FATAL: could not lift Phase 2b out of check.sh — the phase markers moved."
|
||||
echo "This self-test must attack the shipping gate; refusing to run against nothing."
|
||||
exit 1
|
||||
fi
|
||||
if [ "$(grep -c '^# ── Phase ' "$DRIVER")" -ne 1 ]; then
|
||||
echo "FATAL: the lifted block spans more than one phase; the extraction is wrong."
|
||||
grep '^# ── Phase ' "$DRIVER" | sed 's/^/ /'
|
||||
exit 1
|
||||
fi
|
||||
|
||||
expect() { # expect <name> <expected-rc> <required-substring>
|
||||
local name="$1" want_rc="$2" want_txt="$3"
|
||||
|
|
|
|||
|
|
@ -1,108 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
# selftest-inventory.sh — adversarial self-test for check.sh Phase 2c.
|
||||
#
|
||||
# WHAT PHASE 2c IS FOR. Phase 2b asks the kernel whether any AXIOM is declared
|
||||
# under Proofs/. It says nothing about the ~3000 other declarations. Phase 3
|
||||
# pins the cones of the 31 named certificates. Between them sits everything
|
||||
# else: a helper lemma that quietly acquired an oracle in its cone, a
|
||||
# declaration added, removed or renamed, a compiler-generated auxiliary that
|
||||
# changed shape. Phase 2c pins that whole surface and diffs it both ways.
|
||||
#
|
||||
# Cases, each asserting a SPECIFIC diagnostic:
|
||||
# 0 positive control: the untouched tree passes
|
||||
# 1 an allowlist row deleted -> UNCLASSIFIED (in env, not allowlisted)
|
||||
# 2 an allowlist row invented -> STALE (allowlisted, not in env)
|
||||
# 3 a cone silently widened -> BOTH, because the record changed
|
||||
# 4 an axiom row appears -> AXIOM SURFACE DRIFT
|
||||
# 5 the count trailer disagrees -> INVENTORY TRUNCATED (no vacuous pass)
|
||||
#
|
||||
# It runs the SHIPPING inventory_gate.sh against a recorded observation, so no
|
||||
# Lean is needed and the whole thing takes a second. The observation itself is
|
||||
# produced by check.sh Phase 2c; this test attacks the gate that judges it.
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -uo pipefail
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
FAILURES=0
|
||||
STASH="$(mktemp -d)"
|
||||
trap 'rm -rf "$STASH"' EXIT INT TERM
|
||||
|
||||
ALLOW="$HERE/inventory-allowlist.txt"
|
||||
[ -s "$ALLOW" ] || { echo "FATAL: inventory-allowlist.txt missing or empty"; exit 1; }
|
||||
|
||||
# The observation a green run would produce: the allowlist itself plus a
|
||||
# trailer. Deriving it from the allowlist is exactly right for this test — the
|
||||
# question is whether the GATE reacts correctly to differences, and each case
|
||||
# below introduces one.
|
||||
mkobs() { # mkobs <file> [extra-line...]
|
||||
local out="$1"; shift
|
||||
grep '^INV|' "$ALLOW" > "$out"
|
||||
for l in "$@"; do printf '%s\n' "$l" >> "$out"; done
|
||||
LC_ALL=C sort -o "$out" "$out"
|
||||
echo "INV-COUNT|$(grep -c '^INV|' "$out")" >> "$out"
|
||||
}
|
||||
|
||||
expect() { # expect <label> <obs> <allow> <want-rc> <want-substring>
|
||||
local label="$1" obs="$2" allow="$3" want_rc="$4" want_txt="$5" out rc
|
||||
out=$("$HERE/inventory_gate.sh" "$obs" "$allow" 2>&1); rc=$?
|
||||
if [ "$rc" -ne "$want_rc" ]; then
|
||||
echo " ✗ $label: exit $rc, expected $want_rc"; echo "$out" | sed 's/^/ /'
|
||||
FAILURES=$((FAILURES+1)); return
|
||||
fi
|
||||
if ! grep -qF "$want_txt" <<<"$out"; then
|
||||
echo " ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
|
||||
echo " wanted: $want_txt"; echo "$out" | sed 's/^/ /'
|
||||
FAILURES=$((FAILURES+1)); return
|
||||
fi
|
||||
echo " ✓ $label"
|
||||
}
|
||||
|
||||
echo "=== selftest-inventory: attacking check.sh Phase 2c's gate ==="
|
||||
|
||||
# ── 0. positive control ────────────────────────────────────────────────────
|
||||
mkobs "$STASH/obs.txt"
|
||||
expect "case 0 control: a faithful observation passes" "$STASH/obs.txt" "$ALLOW" 0 "environment == allowlist"
|
||||
|
||||
# ── 1. a row deleted from the allowlist: the declaration is still there, so
|
||||
# the gate must report it as unclassified rather than shrug.
|
||||
VICTIM=$(grep '^INV|' "$ALLOW" | grep '|theorem|' | head -1)
|
||||
grep -vxF "$VICTIM" "$ALLOW" > "$STASH/allow-short.txt"
|
||||
expect "case 1: allowlist row deleted -> UNCLASSIFIED" "$STASH/obs.txt" "$STASH/allow-short.txt" 1 "UNCLASSIFIED"
|
||||
|
||||
# ── 2. a row invented in the allowlist: nothing in the environment matches it.
|
||||
cp "$ALLOW" "$STASH/allow-extra.txt"
|
||||
echo "INV|Proofs.Ghost|CurveFieldProofs.ghost_lemma|theorem|Classical.choice" >> "$STASH/allow-extra.txt"
|
||||
expect "case 2: allowlist row with no declaration -> STALE" "$STASH/obs.txt" "$STASH/allow-extra.txt" 1 "STALE"
|
||||
|
||||
# ── 3. THE ONE THAT MATTERS: a cone silently widened. Same module, same name,
|
||||
# same kind — only the axiom cone grew. Phases 2b and 3 both pass this:
|
||||
# 2b only looks for axiom DECLARATIONS, and 3 only pins the 31 named
|
||||
# certificates. If the victim is not one of those, nothing else sees it.
|
||||
WIDENED=$(sed 's/$/,sha2.Sha512/' <<<"$VICTIM")
|
||||
mkobs "$STASH/obs-wide.txt"
|
||||
grep -vxF "$VICTIM" "$STASH/obs-wide.txt" > "$STASH/t" && mv "$STASH/t" "$STASH/obs-wide.txt"
|
||||
printf '%s\n' "$WIDENED" >> "$STASH/obs-wide.txt"
|
||||
LC_ALL=C sort -o "$STASH/obs-wide.txt" "$STASH/obs-wide.txt"
|
||||
echo "INV-COUNT|$(grep -c '^INV|' "$STASH/obs-wide.txt")" >> "$STASH/obs-wide.txt"
|
||||
expect "case 3: a cone widened by one oracle -> UNCLASSIFIED" "$STASH/obs-wide.txt" "$ALLOW" 1 "UNCLASSIFIED"
|
||||
|
||||
# ── 4. an axiom appears in the audited corpus. The sanctioned external models
|
||||
# live in gen/, outside every module the drivers cover, so any axiom here
|
||||
# is a declaration smuggled into the proof corpus.
|
||||
mkobs "$STASH/obs-ax.txt" "INV|Proofs.FeQ|CurveFieldProofs.rogue|axiom|"
|
||||
expect "case 4: an axiom in the corpus -> AXIOM SURFACE DRIFT" "$STASH/obs-ax.txt" "$ALLOW" 1 "AXIOM SURFACE DRIFT"
|
||||
|
||||
# ── 5. truncation. "Nothing found" and "nothing wrong" must not share a path:
|
||||
# a crashed or cut-short run has to fail, not pass as an empty diff.
|
||||
grep '^INV|' "$ALLOW" | head -100 > "$STASH/obs-trunc.txt"
|
||||
echo "INV-COUNT|$(grep -c '^INV|' "$ALLOW")" >> "$STASH/obs-trunc.txt"
|
||||
expect "case 5: trailer disagrees with the lines -> INVENTORY TRUNCATED" "$STASH/obs-trunc.txt" "$ALLOW" 1 "INVENTORY TRUNCATED"
|
||||
|
||||
echo ""
|
||||
if [ "$FAILURES" -eq 0 ]; then
|
||||
echo "SELFTEST PASSED — Phase 2c's gate rejects surface drift in both directions,"
|
||||
echo "for the stated reason in each case."
|
||||
exit 0
|
||||
fi
|
||||
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
|
||||
exit 1
|
||||
|
|
@ -68,9 +68,7 @@ build_driver() {
|
|||
sed -n '/^CERTS=(/,/^)/p' "$HERE/check.sh"
|
||||
# `$0` inside Phase 3c must resolve to the shipping check.sh, not to this
|
||||
# driver, or the apex-name recovery would read the wrong file.
|
||||
# Stop at the next phase marker, not at a blank echo: a terminator that is
|
||||
# not itself a phase boundary breaks the moment the phase's body changes.
|
||||
awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' "$HERE/check.sh" \
|
||||
sed -n '/^# ── Phase 3c/,/^echo ""$/p' "$HERE/check.sh" | sed '$d' \
|
||||
| sed "s|\"\$0\"|\"$HERE/check.sh\"|g"
|
||||
} > "$DRIVER"
|
||||
if [ "$(wc -l < "$DRIVER")" -lt 60 ]; then
|
||||
|
|
|
|||
Loading…
Reference in a new issue