mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-04 20:03:41 +00:00
audit: bind the scalar statements, and make the accounting identity mean audit
Closes four round-7/8 findings. Certified by the round-12 sweep: five repositories, both buttons and every self-test, 48/48 GREEN. ── `scalar-statements-unbound` (gpt, round 7, CRITICAL) ──────────────────── The main button bound its 31 certificates' elaborated statements and reachable specification bodies. This button bound NONE of its thirteen, while TRUSTED-BASE item 8 said the audit covers "every certificate" — false across the 44-certificate surface. The finding was raised in round 7, lost from the round-8 work list by an F-number collision between two reviewers, and re-raised in round 8. Proofs/ScalarAudit.lean is generated from each fork's OWN Audit.lean, so the canonicalisation is provably the same code: pp.all rendering, whitespace normalisation, transitive specification closure. check-scalar.sh Phase 3c pins the block's digest, requires the committed copy to match byte-for-byte so a mismatch can be DIFFED, and cross-checks the auditor's certificate set against the button's CERTS array. dalek ecf3a3f8 · anza 0d942e47 · risc0 4b550a61 · betrusted 4b550a61 risc0 and betrusted share a digest and that is correct, not a collision: their ScalarSubSpec.lean differs only in doc prose and in `black_box` entries inside `simp only [...]` lists AFTER `:= by`. Proof scripts. They bind the same statements over the same specifications, which is the documented scope. selftest-scalar-statements.sh ships the two attacks the reviewer asked for: ok gutted statement caught (cone unchanged) ok rewritten specification body caught (name and cone unchanged) The second rewrites a reachable reference body to `id (…)` — DEFINITIONALLY EQUAL, so the corpus compiles and every proof typechecks and the cone is byte-identical. Every earlier phase is blind to it. ── `drv-surface-no-cones` + `accounting-certifies-enumeration` (claude) ──── The round-7 accounting identity proved every kernel constant was ENUMERATED. The reviewer showed enumeration is not audit: their planted claim WAS enumerated, as DRV|LTLAccAudit.bait.smuggled|theorem with a real cone, and nothing examined it — rows had no cone, no allowlist covered them, the statement digest does not reach instruments, and Phase 2b gates DECLARED AXIOMS, a different question. "Progress of one step, not two." DRV rows now carry their axiom cone and are pinned in driver-allowlist.txt by inventory_gate.sh with a DRV tag — the same implementation that pins the corpus, in both directions, because a second copy of a coverage gate is a second thing to drift. The axiom policy is per-surface and enforced per surface: the corpus admits exactly the sanctioned boundary, the instruments admit none, and an instrument axiom fails EVEN WHEN ALLOWLISTED. Verified with the reviewer's own payload, both placements: before the walk -> UNCLASSIFIED: DRV|…|bait.smuggled|theorem|Classical.choice,Quot.sound,propext after the walk -> ACCOUNTING FAILED names it (kernel-side) ── `drv-naming-heuristic` (claude, round 7) ──────────────────────────────── Retired as load-bearing rather than patched. The rule admits a theorem whose name extends a constant declared alongside it, and "breaks in one line" — declare `def bait`, then `theorem bait.smuggled` walks through. It stays as a fast readable first check; membership in a committed allowlist is what now carries the weight, and a new row fails closed whatever it is called. ── what round 11 caught, which was mine ─────────────────────────────────── DRV rows first shipped WITHOUT their originating driver. dalek and anza run two drivers, each declaring its own `corpus`; keyed on name alone those two distinct declarations produced one byte-identical row, `sort -u` collapsed them, and the trailers summed to 37 against 36. The estate had already learned this on the corpus walk — INV rows carry their module because two modules both declare CurveFieldProofs.zero_spec — and I rebuilt the record without it. Rows now carry their driver, and the gate FAILS CLOSED ON DUPLICATE RECORDS naming the collision: two declarations sharing one entry means one is covered by the other's, which is exactly how a real declaration hides. The trailer now checks what the drivers EMITTED, not what survives de-duplication — conflating "the run was truncated" with "two rows were identical" is what let a record-format defect present itself as an arithmetic complaint. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
parent
9c6c3b16a3
commit
fa9da37f11
11 changed files with 685 additions and 20 deletions
|
|
@ -1,24 +1,28 @@
|
|||
6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt
|
||||
d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh
|
||||
9b0fa638179282b4dd74a6aad3d140ad1299b4e092d1f19dc337832c172947e3 check.sh
|
||||
6fd6275ba35ceb1c6ff38239a8377c0c1cb54dd5ecff83e77edc18f690b9bab4 check-scalar.sh
|
||||
fb92e967d81982ede31c0deeb5c02bacaf3380ee94d2c9af3dd2634e3d73c6ad check.sh
|
||||
e782d1c9eef71e97f3c8b97463c16abc6321cc7192dd08a877d8c42473259f84 driver-allowlist.txt
|
||||
9b24f501b1e92b8ae41db0729ae9fbdbf10438ae89764ed29aa07efc2c3d6dd6 extract.sh
|
||||
ed3e80ff9eeba730772242bcfb6d6f073623d4ffb86a8587c39e11b81eb6c37a GEN-MODEL.sha256
|
||||
e95982c15c7d754f0c9bcffef95d4c9d4c63589ac51ecdd40870133f377a005c inventory-allowlist-scalar.txt
|
||||
a0fb8a1a99bc991870b493796bf7bfe09463413298d83c6ae73a269712f96b55 inventory-allowlist-scalar.txt
|
||||
86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt
|
||||
0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh
|
||||
3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh
|
||||
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
||||
b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh
|
||||
1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py
|
||||
855134c50bc2ce374eb935058f808264ea6de5ee328ef766956e7e54366f75fe MODEL-CORRESPONDENCE.txt
|
||||
772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean
|
||||
859dcb7fcef13e8b49a8b36a496f46e9fc56448410d3bde16c78361215f4bc19 Proofs/InventoryCore.lean
|
||||
5274b1881579e24030b1aed608511640b8ba39f7e6cdb8962ce23bece655c10b Proofs/InventoryCore.lean
|
||||
660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b Proofs/Inventory.lean
|
||||
6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean
|
||||
f921d028149e41016c75db2d316f26450768c614eb8b8b9764c49da84bbf6fc8 Proofs/InventoryScalar.lean
|
||||
907616a9386727ec6d030f9ed1c9122d5ccfe4c011b23b781ff728dbb99a2582 Proofs/ScalarAudit.lean
|
||||
4b550a618b4d4e14be9e7646ae9d515d784d231b34fee39415002a25e370e9b7 SCALAR-AUDIT-MANIFEST.txt
|
||||
bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh
|
||||
6de61b2b08ab6e05c7d38377ea8f70178da4a105bb1df21c6ba6bc05a647090d selftest-axgate.sh
|
||||
7822c007d12d7be70003ea9de234102a2c4165cfab65a108e2960e51b87bee82 selftest-correspondence.sh
|
||||
41d16df48b15b99512d10a805bb811db301e9d9c8b00e5e3e0186f0110d3b71a selftest-harness.sh
|
||||
1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh
|
||||
acfa40b0f45bf7969dd6e2a26ea72e9eaf824cedb695e498f863360772fd7c06 selftest-scalar-statements.sh
|
||||
fc6d2905871500f2ee9c3f308fd8300cfcd1a7fa854d399d13812f7e2282f1fd selftest-shapes.sh
|
||||
eb7367a1494f5203f0cbeace78c9522608d51825fdcbb7ae40962d2380a7bc79 selftest-statements.sh
|
||||
7603b82c9c29a27f6659b8878d1a2e2365afb6541c3c5b2698ab2fee21bb2bde selftest-tiers.sh
|
||||
|
|
|
|||
|
|
@ -159,7 +159,37 @@ def emitDrivers (drivers : Array Name) : MetaM Unit := do
|
|||
the audit infrastructure. An instrument may declare definitions \
|
||||
and whatever the elaborator generates for them — never a claim \
|
||||
of its own."
|
||||
lines := lines.push s!"DRV|{n}|{k}"
|
||||
-- THE CONE, and it is the second half of the accounting identity.
|
||||
--
|
||||
-- Round-8 review (Claude, register keys `drv-surface-no-cones` and
|
||||
-- `accounting-certifies-enumeration`). These rows carried name and kind
|
||||
-- only. The round-7 accounting identity then proved every kernel constant
|
||||
-- was ENUMERATED by one of the two walks — and the reviewer demonstrated
|
||||
-- that enumeration is not audit: a claim planted in an instrument WAS
|
||||
-- enumerated, as `DRV|…bait.smuggled|theorem`, with a real cone of
|
||||
-- [propext, Classical.choice, Quot.sound], and then nothing looked at it.
|
||||
-- No allowlist row covered the instrument surface, the statement digest
|
||||
-- does not reach instruments, and Phase 2b gates DECLARED AXIOMS, which is
|
||||
-- a different question from cones. Their summary: the identity "converted
|
||||
-- 36 declarations nobody enumerated into 36 declarations nobody examined.
|
||||
-- That is progress of one step, not two."
|
||||
--
|
||||
-- With the cone emitted here and the rows pinned in driver-allowlist.txt
|
||||
-- by the same gate the corpus uses, the identity and the audit coincide:
|
||||
-- a planted claim is a new row, and a new row fails closed. The
|
||||
-- name-prefix rule above is kept as a fast first line of defence but is no
|
||||
-- longer load-bearing — the reviewer showed it breaks in one line.
|
||||
let cone ← axiomCone n
|
||||
let coneStr := ",".intercalate (cone.toList.map (·.toString))
|
||||
-- THE ORIGINATING DRIVER is part of the record, for the same reason the
|
||||
-- INV rows carry their module: dalek and anza run TWO drivers, each
|
||||
-- declaring its own `corpus`, and keyed on name alone those two distinct
|
||||
-- declarations produced one byte-identical row. `sort -u` then collapsed
|
||||
-- them, the trailers summed to 37 against 36 unique rows, and the gate
|
||||
-- reported the surface truncated. Two declarations must never share a
|
||||
-- record — that is what let a real declaration hide behind another one's
|
||||
-- entry when this mistake was made on the corpus walk.
|
||||
lines := lines.push s!"DRV|{env.mainModule}|{n}|{k}|{coneStr}"
|
||||
let sorted := lines.qsort (· < ·)
|
||||
for l in sorted do
|
||||
IO.println l
|
||||
|
|
|
|||
|
|
@ -20,11 +20,14 @@ import Proofs.ScalarWideSpec
|
|||
import Proofs.ScalarBytesSpec
|
||||
import Proofs.ScalarUnpackSpec
|
||||
import Proofs.ScalarFromBytesSpec
|
||||
-- The scalar audit driver is in this button's compile manifest, exactly as
|
||||
-- Proofs.Audit is in the main button's, so the inventory must cover it too.
|
||||
import Proofs.ScalarAudit
|
||||
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]
|
||||
#[`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, `Proofs.ScalarAudit]
|
||||
|
||||
#eval show MetaM Unit from emitInventory corpus
|
||||
|
|
|
|||
171
verification/Proofs/ScalarAudit.lean
Normal file
171
verification/Proofs/ScalarAudit.lean
Normal file
|
|
@ -0,0 +1,171 @@
|
|||
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
|
||||
import Lean
|
||||
open Lean Elab Command
|
||||
|
||||
namespace Ed25519ScalarAudit
|
||||
|
||||
/-- Lean's three kernel axioms. -/
|
||||
def kernel3 : List Name := [`propext, `Classical.choice, `Quot.sound]
|
||||
|
||||
/-- This fork's apex boundary: the hash oracle and wire-format symbols the
|
||||
signature-level certificates are permitted to rest on, and nothing else.
|
||||
POLICY CONSTANT — folded into the digest, so widening it moves the hash
|
||||
and fails the build. -/
|
||||
def apexExtra : List Name := [] -- the scalar layer has NO apex tier
|
||||
|
||||
def apexBoundary : List Name := kernel3 ++ apexExtra
|
||||
|
||||
/-- A constant counts as SPECIFICATION if it was declared in a `Proofs.`
|
||||
module — i.e. hand-written by us, as opposed to the extracted model in
|
||||
`gen/` (pinned separately by Phase 0). Derived from the environment, not
|
||||
from a list, so a new specification module cannot appear unnoticed. -/
|
||||
def specPrefix : String := "Proofs."
|
||||
|
||||
/-- Per-certificate expected cone. Arithmetic tier first, apex tier last. -/
|
||||
def manifest : List (Name × List Name) :=
|
||||
[ (`ScalarProofs.L_val, kernel3)
|
||||
, (`ScalarProofs.sub_loop_spec, kernel3)
|
||||
, (`ScalarProofs.sub_loop1_one_spec, kernel3)
|
||||
, (`ScalarProofs.sub_val_spec, kernel3)
|
||||
, (`ScalarProofs.add_val_spec, kernel3)
|
||||
, (`ScalarProofs.mul_internal_spec, kernel3)
|
||||
, (`ScalarProofs.part1_spec, kernel3)
|
||||
, (`ScalarProofs.montgomery_reduce_spec, kernel3)
|
||||
, (`ScalarProofs.mul_spec, kernel3)
|
||||
, (`ScalarProofs.scalarImplementation, kernel3)
|
||||
, (`ScalarProofs.montgomery_mul_spec, kernel3)
|
||||
, (`ScalarProofs.bytes_unpack_spec, kernel3)
|
||||
, (`ScalarProofs.from_bytes_wide_spec, kernel3)
|
||||
]
|
||||
|
||||
/-- Deterministic name ordering for the canonical serialization. -/
|
||||
def sortNames (l : List Name) : List Name :=
|
||||
((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName)
|
||||
|
||||
/-- Whitespace-canonical: every whitespace run collapses to one space, so the
|
||||
pretty-printer's line wrapping cannot perturb the digest. -/
|
||||
def normWs (s : String) : String :=
|
||||
(s.foldl (fun (acc : String × Bool) c =>
|
||||
let c := if c.isWhitespace then ' ' else c
|
||||
if c == ' ' then (if acc.2 then acc else (acc.1.push ' ', true))
|
||||
else (acc.1.push c, false))
|
||||
("", true)).1
|
||||
|
||||
/-- Was `n` hand-written by us, in a `Proofs.` module? -/
|
||||
def isSpecConst (env : Environment) (n : Name) : Bool :=
|
||||
match env.getModuleIdxFor? n with
|
||||
| some idx => (toString env.header.moduleNames[idx.toNat]!).startsWith specPrefix
|
||||
| none => false
|
||||
|
||||
/-- Transitive closure over specification constants, starting from a
|
||||
certificate's STATEMENT and following DEFINITION bodies (a theorem
|
||||
contributes its statement only). This discovers the reference definitions —
|
||||
and any future one — automatically, so a new specification cannot be
|
||||
introduced, or an existing one redefined, without moving the digest. -/
|
||||
partial def closureOf (env : Environment) (seen : NameSet) (work : List Name) : NameSet :=
|
||||
match work with
|
||||
| [] => seen
|
||||
| n :: rest =>
|
||||
if seen.contains n || !isSpecConst env n then closureOf env seen rest
|
||||
else
|
||||
let seen := seen.insert n
|
||||
let more := match env.find? n with
|
||||
| some (.defnInfo v) => v.value.getUsedConstants.toList ++ v.type.getUsedConstants.toList
|
||||
| some ci => ci.type.getUsedConstants.toList
|
||||
| none => []
|
||||
closureOf env seen (more ++ rest)
|
||||
|
||||
/-- Fully-explicit (`pp.all`) rendering, whitespace-canonicalized. Implicit
|
||||
arguments, instances and universe levels are all made visible, so two
|
||||
statements that merely LOOK alike cannot share a rendering. -/
|
||||
def ppAll (e : Expr) : CommandElabM String := do
|
||||
let s ← Command.liftCoreM <| Meta.MetaM.run' <|
|
||||
withOptions (fun o => o.setBool `pp.all true) do
|
||||
return (← Meta.ppExpr e).pretty
|
||||
return normWs s
|
||||
|
||||
elab "auditScalarStatements" : command => do
|
||||
let env ← getEnv
|
||||
let mut errs : Array String := #[]
|
||||
|
||||
-- (0) The manifest may not permit an axiom outside the two declared tiers.
|
||||
-- Without this, widening a cone in the manifest would be invisible.
|
||||
for (cert, cone) in manifest do
|
||||
for a in cone do
|
||||
unless apexBoundary.contains a do
|
||||
errs := errs.push s!"manifest permits {a} for {cert}, which is outside every declared tier"
|
||||
|
||||
-- (1) Each certificate must EXIST, be a THEOREM, and have EXACTLY its cone.
|
||||
-- Exact, not subset: a certificate that stopped depending on the hash
|
||||
-- oracle is as wrong as one that acquired a new axiom.
|
||||
for (cert, expected) in manifest do
|
||||
match env.find? cert with
|
||||
| none => errs := errs.push s!"{cert}: NOT FOUND (renamed or deleted?)"
|
||||
| some (.thmInfo _) =>
|
||||
let got := (← collectAxioms cert).toList
|
||||
let extras := got.filter (fun a => !expected.contains a)
|
||||
let missing := expected.filter (fun a => !got.contains a)
|
||||
unless extras.isEmpty && missing.isEmpty do
|
||||
errs := errs.push s!"{cert}: cone extra={extras} missing={missing}"
|
||||
| some (.axiomInfo _) => errs := errs.push s!"{cert}: is an AXIOM, not a proven theorem"
|
||||
| some (.opaqueInfo _) => errs := errs.push s!"{cert}: is OPAQUE, not a proven theorem"
|
||||
| some _ => errs := errs.push s!"{cert}: is not a theorem"
|
||||
|
||||
unless errs.isEmpty do
|
||||
throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"
|
||||
|
||||
-- (2) CANONICAL BLOCK: policy, then statements, then specification bodies.
|
||||
let mut lines : Array String := #[]
|
||||
lines := lines.push
|
||||
s!"policy|kernel3={String.intercalate "," ((sortNames kernel3).map toString)}|apexExtra={String.intercalate "," ((sortNames apexExtra).map toString)}|specPrefix={specPrefix}"
|
||||
let mut specs : NameSet := {}
|
||||
for (cert, cone) in manifest do
|
||||
let ci := (env.find? cert).get!
|
||||
specs := (closureOf env {} ci.type.getUsedConstants.toList).toList.foldl (·.insert ·) specs
|
||||
lines := lines.push
|
||||
s!"cert|{cert}|cone={String.intercalate "," ((sortNames cone).map toString)}|type={← ppAll ci.type}"
|
||||
for nm in sortNames specs.toList do
|
||||
match env.find? nm with
|
||||
| none => errs := errs.push s!"specification constant vanished mid-audit: {nm}"
|
||||
| some ci =>
|
||||
let isProp ← Command.liftCoreM <| Meta.MetaM.run' <| Meta.isProp ci.type
|
||||
-- Proof irrelevance: a Prop-valued constant contributes its STATEMENT; a
|
||||
-- data definition contributes its BODY, which is where fidelity lives.
|
||||
if isProp then
|
||||
lines := lines.push s!"spec|{nm}|prop|type={← ppAll ci.type}"
|
||||
else
|
||||
match ci with
|
||||
| .defnInfo v => lines := lines.push s!"spec|{nm}|def|value={← ppAll v.value}"
|
||||
| _ => lines := lines.push s!"spec|{nm}|other|type={← ppAll ci.type}"
|
||||
|
||||
unless errs.isEmpty do
|
||||
throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"
|
||||
|
||||
-- FAIL CLOSED ON ABSENCE: a manifest that somehow produced no specification
|
||||
-- constants would emit a block that binds statements only. That is a weaker
|
||||
-- claim than this file advertises, so it is an error, not a quiet pass.
|
||||
if specs.toList.isEmpty then
|
||||
throwError "AUDIT FAILED: statements reached ZERO specification constants — the closure is not doing its job"
|
||||
|
||||
logInfo ("SCALAR-AUDIT-MANIFEST-BEGIN\n" ++ String.intercalate "\n" lines.toList ++ "\nSCALAR-AUDIT-MANIFEST-END")
|
||||
-- check.sh cross-checks its own CERTS array against THIS line, so the two
|
||||
-- cannot drift apart without the build noticing.
|
||||
logInfo s!"AUDITED-SCALAR-CERTIFICATES: {String.intercalate " " ((manifest.map (·.1)).map toString)}"
|
||||
logInfo s!"statement audit PASSED: {manifest.length} certificates (exact cones + elaborated statements), {specs.toList.length} specification constants pinned"
|
||||
|
||||
end Ed25519ScalarAudit
|
||||
|
||||
open Ed25519ScalarAudit in
|
||||
auditScalarStatements
|
||||
23
verification/SCALAR-AUDIT-MANIFEST.txt
Normal file
23
verification/SCALAR-AUDIT-MANIFEST.txt
Normal file
File diff suppressed because one or more lines are too long
|
|
@ -29,7 +29,7 @@ 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)
|
||||
PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec)
|
||||
PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec ScalarAudit )
|
||||
# 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.
|
||||
|
|
@ -226,6 +226,97 @@ if [ "$AUDFAIL" != 0 ]; then
|
|||
fi
|
||||
echo " ${#CERTS[@]}/${#CERTS[@]} scalar certificates report exactly $EXPECTED"
|
||||
|
||||
# ── Phase 3c: statement + specification binding ─────────────────────────────
|
||||
# WHAT PHASE 3 DOES NOT ESTABLISH — and why this repository claimed something
|
||||
# false for four rounds. Round-7 review (GPT-5.6, register key
|
||||
# `scalar-statements-unbound`, CRITICAL): the main button bound its 31
|
||||
# certificates' elaborated statements and reachable specification bodies; this
|
||||
# button bound NONE of its thirteen. Meanwhile TRUSTED-BASE item 8 said the
|
||||
# audit covers "every certificate" and each README said check.sh audits every
|
||||
# certificate. Both were false across the 44-certificate repository surface.
|
||||
#
|
||||
# The finding was raised in round 7, was lost from the round-8 work list by an
|
||||
# F-number collision between two reviewers, and was re-raised in round 8. It is
|
||||
# closed here.
|
||||
#
|
||||
# Phase 3 proves each scalar certificate rests on exactly the standard three
|
||||
# axioms. It does not say WHAT THE THEOREM SAYS. A certificate gutted to a
|
||||
# tautology of the same cone passes it, and so does one whose reference
|
||||
# definition has been redefined to BE the extracted code — at which point the
|
||||
# theorem reads `loop = loop` and the cone is byte-identical.
|
||||
#
|
||||
# Proofs/ScalarAudit.lean emits a canonical block holding the policy constants,
|
||||
# every scalar certificate's fully-elaborated statement (`pp.all`, so implicit
|
||||
# arguments, instances and universes are all visible), and the body of every
|
||||
# specification constant transitively reachable from those statements. This
|
||||
# phase binds its SHA-256, and the block's INPUT is committed too, so a
|
||||
# mismatch can be DIFFED rather than merely reported.
|
||||
#
|
||||
# To rotate deliberately: run this button, take the printed OBSERVED digest,
|
||||
# and update the constant below AND SCALAR-AUDIT-MANIFEST.txt in the same
|
||||
# reviewable commit. An author who edits a statement and refreshes the digest
|
||||
# together is caught by reading the diff, not by this script.
|
||||
EXPECTED_SCALAR_AUDIT_SHA256="4b550a618b4d4e14be9e7646ae9d515d784d231b34fee39415002a25e370e9b7"
|
||||
echo "=== Phase 3c: scalar statement + specification binding ==="
|
||||
cd "$AENEAS_LEAN"
|
||||
# The compiler's own exit code is the primary signal; the transcript is only
|
||||
# corroboration. A timeout or a memory clamp exits non-zero WITHOUT printing
|
||||
# "error:", so grepping the text alone would let it through.
|
||||
SAUD_RC=0
|
||||
SAUD_OUT=$(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/ScalarAudit.lean 2>&1
|
||||
" ) || SAUD_RC=$?
|
||||
if [ "$SAUD_RC" -ne 0 ]; then
|
||||
echo "SCALAR AUDIT FAILED — Proofs/ScalarAudit.lean exited $SAUD_RC:"
|
||||
tail -20 <<<"$SAUD_OUT" | sed 's/^/ /'
|
||||
exit 1
|
||||
fi
|
||||
if grep -q 'error:' <<<"$SAUD_OUT"; then
|
||||
echo "SCALAR AUDIT FAILED — Proofs/ScalarAudit.lean did not elaborate cleanly:"
|
||||
grep 'error:' <<<"$SAUD_OUT" | head -20 | sed 's/^/ /'
|
||||
exit 1
|
||||
fi
|
||||
SBLOCK=$(awk '/SCALAR-AUDIT-MANIFEST-BEGIN/{f=1;next} /SCALAR-AUDIT-MANIFEST-END/{f=0} f' <<<"$SAUD_OUT")
|
||||
# FAIL CLOSED ON ABSENCE: no block and a matching block must not share a path.
|
||||
if [ -z "$SBLOCK" ]; then
|
||||
echo "SCALAR AUDIT FAILED — no SCALAR-AUDIT-MANIFEST block was emitted (fail-closed)."; exit 1
|
||||
fi
|
||||
SGOT_SHA=$(printf '%s\n' "$SBLOCK" | sha256sum | cut -d' ' -f1)
|
||||
if [ "$SGOT_SHA" != "$EXPECTED_SCALAR_AUDIT_SHA256" ]; then
|
||||
printf '%s\n' "$SBLOCK" > "$HERE/.scalar-audit-manifest.observed"
|
||||
echo "SCALAR AUDIT FAILED — audit-manifest digest mismatch."
|
||||
echo " expected: $EXPECTED_SCALAR_AUDIT_SHA256"
|
||||
echo " observed: $SGOT_SHA"
|
||||
echo " A statement, a specification body, or a policy constant changed."
|
||||
echo " First differences against the committed block:"
|
||||
diff -u "$HERE/SCALAR-AUDIT-MANIFEST.txt" "$HERE/.scalar-audit-manifest.observed" 2>/dev/null \
|
||||
| head -30 | sed 's/^/ /' || echo " (SCALAR-AUDIT-MANIFEST.txt absent — cannot diff)"
|
||||
rm -f "$HERE/.scalar-audit-manifest.observed"
|
||||
exit 1
|
||||
fi
|
||||
# The digest's INPUT must be committed and current, or the diff above would
|
||||
# compare against a stale reference and quietly mislead the next reader.
|
||||
if ! printf '%s\n' "$SBLOCK" | cmp -s - "$HERE/SCALAR-AUDIT-MANIFEST.txt"; then
|
||||
echo "SCALAR AUDIT FAILED — the committed SCALAR-AUDIT-MANIFEST.txt does not match the emitted block."
|
||||
echo " (the digest matched, so the committed copy is stale — refresh it)"; exit 1
|
||||
fi
|
||||
# CROSS-CHECK the certificate list against the CERTS array Phase 3 audits, so a
|
||||
# certificate cannot be dropped from the auditor's manifest unnoticed.
|
||||
SAUD_CERTS=$(grep -o 'AUDITED-SCALAR-CERTIFICATES:.*' <<<"$SAUD_OUT" \
|
||||
| sed 's/AUDITED-SCALAR-CERTIFICATES: //' | tr ' ' '\n' | sort -u | sed '/^$/d')
|
||||
SBASH_CERTS=$(printf '%s\n' "${CERTS[@]}" | sort -u)
|
||||
if [ "$SAUD_CERTS" != "$SBASH_CERTS" ]; then
|
||||
echo "SCALAR AUDIT FAILED — the auditor's certificate set differs from this button's CERTS array:"
|
||||
diff <(echo "$SBASH_CERTS") <(echo "$SAUD_CERTS") | sed 's/^/ /'
|
||||
exit 1
|
||||
fi
|
||||
echo " ${#CERTS[@]} scalar statements + reachable specification bodies bound, sha256 = $SGOT_SHA"
|
||||
cd "$HERE"
|
||||
|
||||
|
||||
echo ""
|
||||
echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round"
|
||||
echo "through RR) proven mod ℓ; aggregate certificate scalarImplementation"
|
||||
|
|
|
|||
|
|
@ -324,6 +324,13 @@ HARNESS_EXTRA=(
|
|||
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
|
||||
driver-allowlist.txt # the INSTRUMENTS' own declaration surface, with cones.
|
||||
# Not executable, so it would otherwise sit outside the
|
||||
# harness set — and an allowlist an attacker may rewrite
|
||||
# pins nothing.
|
||||
Proofs/ScalarAudit.lean # the scalar audit driver, likewise
|
||||
SCALAR-AUDIT-MANIFEST.txt # the block the scalar digest is taken over, committed
|
||||
# so a mismatch can be DIFFED and not merely reported
|
||||
Proofs/InventoryCore.lean # inventory machinery
|
||||
Proofs/InventoryScalar.lean # inventory driver: the scalar layer
|
||||
Proofs/Inventory.lean # inventory driver: main chain
|
||||
|
|
@ -760,6 +767,19 @@ done
|
|||
# fails closed: a declaration missing from both walks leaves the sum short, and
|
||||
# one counted twice leaves it long. A future mismatch must be explained — as
|
||||
# this one finally was — never absorbed into a constant.
|
||||
# PIN THE INSTRUMENTS' OWN SURFACE, in both directions, with the SAME gate the
|
||||
# corpus uses (round-8 review, Claude, register keys `drv-surface-no-cones`,
|
||||
# `accounting-certifies-enumeration`, and it retires `drv-naming-heuristic` as
|
||||
# load-bearing).
|
||||
#
|
||||
# The accounting identity below proves every kernel constant is ENUMERATED by
|
||||
# one of the two walks. The reviewer demonstrated that enumeration is not
|
||||
# audit: their planted claim WAS enumerated, carried a real axiom cone, and
|
||||
# nothing examined it — DRV rows had no cone and no allowlist covered them.
|
||||
# They now carry the cone, and this gate pins them exactly as the corpus is, so
|
||||
# a claim smuggled into an instrument is a NEW ROW and a new row fails closed
|
||||
# whatever it is called.
|
||||
"$HERE/inventory_gate.sh" "$INVLOG" "$HERE/driver-allowlist.txt" DRV || ACCTFAIL=1
|
||||
N_DRV=$(grep -c '^DRV|' "$INVLOG" || true)
|
||||
DRV_TRAILERS=$(grep -c '^DRV-COUNT|' "$INVLOG" || true)
|
||||
DRV_SUM=$(grep '^DRV-COUNT|' "$INVLOG" | cut -d'|' -f2 | paste -sd+ - | bc)
|
||||
|
|
@ -767,7 +787,7 @@ KERN_NAMES=$(mktemp /tmp/check-kernnames-XXXX.txt)
|
|||
ACCT_NAMES=$(mktemp /tmp/check-acctnames-XXXX.txt)
|
||||
LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f2 | LC_ALL=C sort -u > "$KERN_NAMES"
|
||||
{ LC_ALL=C awk -F'|' '/^INV\|/{print $3}' "$HERE/inventory-allowlist.txt"
|
||||
LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f2
|
||||
LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f3
|
||||
} | LC_ALL=C sort -u > "$ACCT_NAMES"
|
||||
UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN_NAMES" "$ACCT_NAMES")
|
||||
if [ "$DRV_TRAILERS" -ne "$N_DRIVERS" ]; then
|
||||
|
|
|
|||
50
verification/driver-allowlist.txt
Normal file
50
verification/driver-allowlist.txt
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
# driver-allowlist.txt — THE AUDIT INSTRUMENTS' OWN DECLARATION SURFACE,
|
||||
# pinned with axiom cones, gated by inventory_gate.sh with the DRV tag:
|
||||
# the same implementation that pins the corpus, in both directions.
|
||||
#
|
||||
# Round-8 review (Claude, register keys drv-surface-no-cones and
|
||||
# accounting-certifies-enumeration). The accounting identity proved every
|
||||
# kernel constant was ENUMERATED. It did not prove any of them was
|
||||
# EXAMINED: a claim planted in an instrument was enumerated, carried a
|
||||
# real cone, and nothing looked at it. These rows close that gap.
|
||||
#
|
||||
# Regenerate deliberately, never by hand:
|
||||
# scratchpad/gen-driver-allowlists.sh
|
||||
# and read the diff — a new row is a declaration that appeared in an
|
||||
# instrument, which is exactly the event this file exists to surface.
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1._sparseCasesOn_3|def|propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_10|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_12|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_1|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_3|def|propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_6|def|propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_8|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.apexBoundary|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit.apexExtra|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit.closureOf._sparseCasesOn_1|def|propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.closureOf._unsafe_rec|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.closureOf.match_1|def|propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.closureOf.match_4|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit.closureOf|opaque|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.commandAuditStatements|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit.isSpecConst.match_1|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit.isSpecConst|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.kernel3|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit.manifest|def|
|
||||
DRV|Proofs.Inventory|Ed25519Audit.normWs|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.ppAll|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.sortNames|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Audit.specPrefix|def|
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.axiomCone|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.emitDrivers.match_1|def|Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.emitDrivers|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory._sparseCasesOn_3|def|propext
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory.match_1|def|
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory.match_3|def|propext
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory.match_6|def|
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory|def|Classical.choice,Quot.sound,propext
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.kindOf.match_1|def|
|
||||
DRV|Proofs.Inventory|Ed25519Inventory.kindOf|def|
|
||||
DRV|Proofs.Inventory|corpus|def|
|
||||
DRV|Proofs.Inventory|drivers|def|
|
||||
|
|
@ -1893,3 +1893,27 @@ INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_7|theorem|Cl
|
|||
INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_9|theorem|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec|theorem|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.apexBoundary|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.apexExtra|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1|def|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_1|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_10|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_12|def|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_3|def|propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_6|def|propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_8|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1._sparseCasesOn_3|def|propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf|opaque|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf.match_1|def|propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf.match_4|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf._sparseCasesOn_1|def|propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf._unsafe_rec|def|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.commandAuditScalarStatements|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.isSpecConst|def|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.isSpecConst.match_1|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.kernel3|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.manifest|def|
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.normWs|def|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.ppAll|def|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.sortNames|def|Classical.choice,Quot.sound,propext
|
||||
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.specPrefix|def|
|
||||
|
|
|
|||
|
|
@ -9,7 +9,35 @@
|
|||
# self-test exercises this exact script — the tested logic IS the shipping
|
||||
# logic.
|
||||
#
|
||||
# Usage: inventory_gate.sh <observed-lean-output> <allowlist-file>
|
||||
# Usage: inventory_gate.sh <observed-lean-output> <allowlist-file> [<tag>]
|
||||
#
|
||||
# <tag> defaults to INV — the CORPUS walk. Pass DRV to gate the INSTRUMENTS'
|
||||
# OWN SURFACE with this same implementation.
|
||||
#
|
||||
# WHY THE TAG EXISTS — round-8 review (Claude, register keys
|
||||
# `drv-surface-no-cones`, `accounting-certifies-enumeration`).
|
||||
#
|
||||
# The accounting identity added in round 7 proved every constant the kernel
|
||||
# sees is ENUMERATED by one of the two walks. The reviewer showed that
|
||||
# enumeration is not audit: a claim planted in an instrument WAS enumerated —
|
||||
# `DRV|LTLAccAudit.bait.smuggled|theorem` — and then nothing looked at it,
|
||||
# because DRV rows carried name and kind and NO CONE, and no allowlist covered
|
||||
# them. In their words, the identity "converted 36 declarations nobody
|
||||
# enumerated into 36 declarations nobody examined. That is progress of one
|
||||
# step, not two."
|
||||
#
|
||||
# The second step is here: DRV rows now carry their axiom cone and are pinned
|
||||
# in a committed allowlist, by THIS gate, in both directions — exactly as the
|
||||
# corpus is. One implementation, not two, because a second copy of a coverage
|
||||
# gate is a second thing to drift.
|
||||
#
|
||||
# It also retires a heuristic. The driver-surface rule permits a theorem whose
|
||||
# name extends a constant declared alongside it, since that is what the
|
||||
# elaborator generates for a definition; the reviewer showed it "breaks in one
|
||||
# line" — declare `def bait`, then `theorem bait.smuggled` passes. That rule is
|
||||
# kept as a fast, readable first line of defence, but it is NO LONGER
|
||||
# LOAD-BEARING: a planted claim now has to appear in the pinned allowlist, and
|
||||
# a new row fails closed whatever it is named.
|
||||
#
|
||||
# Fail-closed in BOTH directions:
|
||||
# UNCLASSIFIED — constant in the environment, absent from the allowlist
|
||||
|
|
@ -21,17 +49,41 @@
|
|||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
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_file="$1"; allow_file="$2"; TAG="${3:-INV}"
|
||||
case "$TAG" in
|
||||
INV) WHAT="the audited corpus"; TRAILER_TAG="INV-COUNT"; LABEL="inventory gate"; TRUNCLABEL="INVENTORY TRUNCATED" ;;
|
||||
DRV) WHAT="the audit instruments"; TRAILER_TAG="DRV-COUNT"; LABEL="driver-surface gate"; TRUNCLABEL="DRIVER SURFACE TRUNCATED" ;;
|
||||
*) echo " GATE MISUSE: unknown tag '$TAG' (expected INV or DRV)"; exit 1 ;;
|
||||
esac
|
||||
|
||||
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"
|
||||
# The trailer is an OUTPUT-INTEGRITY check: it must equal the number of rows
|
||||
# the driver(s) actually emitted, BEFORE de-duplication. Comparing it to the
|
||||
# de-duplicated count conflates "a run was truncated" with "two rows were
|
||||
# identical", and the second is a record-format defect that must be fixed at
|
||||
# the source, not absorbed here. (It was: DRV rows now carry their driver.)
|
||||
N_RAW=$(grep -c "^$TAG|" "$obs_file" || true)
|
||||
OBS=$(grep "^$TAG|" "$obs_file" | sort -u)
|
||||
N_OBS=$(printf '%s' "$OBS" | grep -c "^$TAG|" || true)
|
||||
if [ "$N_RAW" -ne "$N_OBS" ]; then
|
||||
echo " DUPLICATE $TAG RECORDS: $N_RAW rows collapse to $N_OBS distinct ones."
|
||||
echo " Two declarations share a record, so one is covered by the other's entry:"
|
||||
grep "^$TAG|" "$obs_file" | sort | uniq -d | head -5 | sed 's/^/ /'
|
||||
exit 1
|
||||
fi
|
||||
# Each driver emits its own trailer, so DRV trailers are SUMMED; the corpus
|
||||
# walk emits one and the last is taken. Either way a truncated or crashed run
|
||||
# must never pass as an empty diff.
|
||||
if [ "$TAG" = DRV ]; then
|
||||
TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | cut -d'|' -f2 | paste -sd+ - | bc)
|
||||
else
|
||||
TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | tail -1 | cut -d'|' -f2)
|
||||
fi
|
||||
if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_RAW" ]; then
|
||||
echo " $TRUNCLABEL: trailer=${TRAILER:-absent}, observed $N_RAW lines"
|
||||
exit 1
|
||||
fi
|
||||
|
||||
ALLOW=$(grep '^INV|' "$allow_file" | sort -u)
|
||||
ALLOW=$(grep "^$TAG|" "$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"))
|
||||
|
|
@ -51,7 +103,7 @@ fi
|
|||
# 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:"
|
||||
echo " AXIOM SURFACE DRIFT: $WHAT must declare no axioms; observed:"
|
||||
printf '%s\n' "$AXLINES" | sed 's/^/ /'
|
||||
FAILGATE=1
|
||||
fi
|
||||
|
|
@ -60,5 +112,5 @@ fi
|
|||
# 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"
|
||||
[ "$FAILGATE" = 0 ] && echo " $LABEL: $N_OBS constants, environment == allowlist, zero axioms declared in $WHAT"
|
||||
exit "$FAILGATE"
|
||||
|
|
|
|||
197
verification/selftest-scalar-statements.sh
Executable file
197
verification/selftest-scalar-statements.sh
Executable file
|
|
@ -0,0 +1,197 @@
|
|||
#!/usr/bin/env bash
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
# selftest-scalar-statements.sh — adversarial self-test for check-scalar.sh
|
||||
# Phase 3c, the scalar statement + specification binding.
|
||||
#
|
||||
# WHY THIS EXISTS. Round-7 review (GPT-5.6, register key
|
||||
# `scalar-statements-unbound`, CRITICAL): the main button bound its 31
|
||||
# certificates' elaborated statements and reachable specification bodies; this
|
||||
# repository's scalar button bound NONE of its thirteen, while TRUSTED-BASE
|
||||
# item 8 said the audit covers "every certificate". The binding was added in
|
||||
# the same commit as this file. The reviewer asked for exactly two shipping
|
||||
# attacks, and this file is those two:
|
||||
#
|
||||
# 1. same-cone theorem statement gutting;
|
||||
# 2. a reachable reference body rewritten while name and cone remain fixed.
|
||||
#
|
||||
# Both are invisible to every earlier phase by construction. Phase 2b sees no
|
||||
# new axiom; Phase 3's exact-cone audit sees the same three axioms; only the
|
||||
# statement binding sees them.
|
||||
#
|
||||
# It extracts Phase 3c out of check-scalar.sh at run time, so it attacks THE
|
||||
# SHIPPING GATE rather than a copy that can drift away from it.
|
||||
#
|
||||
# Requires a prior green scalar build. Recompiling the corpus is the expensive
|
||||
# part; SKIP_SLOW=1 runs only the fast cases and SAYS SO rather than passing
|
||||
# quietly over the two that matter.
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -uo pipefail
|
||||
source ~/aeneas-toolchain/env.sh
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
|
||||
TIMEOUT="${LEAN_TIMEOUT:-900}"
|
||||
export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"
|
||||
CORES="${LEAN_MAX_CORES:-0-3}"
|
||||
SKIP_SLOW="${SKIP_SLOW:-0}"
|
||||
|
||||
STASH="$(mktemp -d)"
|
||||
FAILURES=0
|
||||
TREE_AT_START="$(cd "$HERE/.." && git status --porcelain)"
|
||||
|
||||
cleanup() {
|
||||
[ -f "$STASH/gut.lean" ] && cp "$STASH/gut.lean" "$HERE/Proofs/ScalarMain.lean"
|
||||
[ -f "$STASH/den.lean" ] && cp "$STASH/den.lean" "$HERE/Proofs/ScalarDenote.lean"
|
||||
rm -rf "$STASH"
|
||||
rm -f "$HERE"/.scalar-audit-manifest.observed
|
||||
}
|
||||
trap cleanup EXIT INT TERM
|
||||
|
||||
DRIVER="$STASH/phase3c.sh"
|
||||
PAYLOAD="$STASH/payload.sh"
|
||||
build_driver() {
|
||||
awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' \
|
||||
"$HERE/check-scalar.sh" > "$PAYLOAD"
|
||||
{ echo 'set -uo pipefail'
|
||||
echo 'source ~/aeneas-toolchain/env.sh'
|
||||
echo "HERE=\"$HERE\""
|
||||
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
|
||||
echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
|
||||
# CERTS is referenced by the cross-check inside Phase 3c. Lifted VERBATIM
|
||||
# rather than re-derived, so this test cannot drift from the button's set.
|
||||
sed -n '/^CERTS=(/,/^)/p' "$HERE/check-scalar.sh"
|
||||
cat "$PAYLOAD"
|
||||
} > "$DRIVER"
|
||||
if [ "$(wc -l < "$PAYLOAD")" -lt 40 ]; then
|
||||
echo "FATAL: could not lift Phase 3c out of check-scalar.sh — the markers moved."
|
||||
exit 1
|
||||
fi
|
||||
grep -qF 'SCALAR-AUDIT-MANIFEST-BEGIN' "$PAYLOAD" || {
|
||||
echo "FATAL: the lifted payload does not read the scalar audit block."; exit 1; }
|
||||
"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check-scalar.sh Phase 3c" || exit 1
|
||||
}
|
||||
|
||||
recompile() { # recompile <module>
|
||||
( 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_MAX_CORES=$CORES '$HERE/lean-guard' Proofs/$1.lean
|
||||
" ) >/dev/null 2>&1
|
||||
}
|
||||
|
||||
expect() { # expect <name> <expected-rc> <required-substring>
|
||||
local name="$1" want_rc="$2" want_txt="$3" out rc
|
||||
out=$(bash "$DRIVER" 2>&1); rc=$?
|
||||
if [ "$rc" -ne "$want_rc" ]; then
|
||||
echo " FAIL $name: exit $rc, expected $want_rc"
|
||||
tail -6 <<<"$out" | sed 's/^/ /'; FAILURES=$((FAILURES+1)); return
|
||||
fi
|
||||
if ! grep -qF "$want_txt" <<<"$out"; then
|
||||
echo " FAIL $name: exit code right but diagnostic wrong (rejected for the wrong reason)"
|
||||
echo " wanted substring: $want_txt"
|
||||
echo " got: $(tr '\n' '|' <<<"$out" | cut -c1-260)"
|
||||
FAILURES=$((FAILURES+1)); return
|
||||
fi
|
||||
echo " ok $name"
|
||||
}
|
||||
|
||||
echo "=== selftest-scalar-statements: attacking check-scalar.sh Phase 3c ==="
|
||||
build_driver
|
||||
|
||||
# ── 1. Baseline: the untouched repository passes and reports what it bound.
|
||||
expect "baseline green, statements bound" 0 "statements + reachable specification bodies bound"
|
||||
|
||||
# ── 2. HAND-EDIT THE COMMITTED BLOCK. The digest still matches what Lean
|
||||
# emits, so only the committed-copy comparison can see this.
|
||||
cp "$HERE/SCALAR-AUDIT-MANIFEST.txt" "$STASH/manifest.bak"
|
||||
sed -i '2s/$/ TAMPERED/' "$HERE/SCALAR-AUDIT-MANIFEST.txt"
|
||||
expect "hand-edited committed block caught" 1 "does not match the emitted block"
|
||||
cp "$STASH/manifest.bak" "$HERE/SCALAR-AUDIT-MANIFEST.txt"
|
||||
|
||||
if [ "$SKIP_SLOW" = "1" ]; then
|
||||
echo " SKIPPED (SKIP_SLOW=1): the two attacks this file exists for — gutted"
|
||||
echo " statement and rewritten specification body — were NOT run. The fast"
|
||||
echo " case above does not cover either of them."
|
||||
else
|
||||
# ── 3. ATTACK ONE: gut a certificate's STATEMENT, preserving its axiom cone.
|
||||
# ScalarProofs.scalarImplementation is the aggregate and is TERMINAL —
|
||||
# nothing outside its own module consumes it. Gutting a load-bearing
|
||||
# certificate would simply break its consumers, which demonstrates the
|
||||
# compiler working, not this gate.
|
||||
cp "$HERE/Proofs/ScalarMain.lean" "$STASH/gut.lean"
|
||||
python3 - "$HERE/Proofs/ScalarMain.lean" <<'PY'
|
||||
import sys, re
|
||||
f = sys.argv[1]
|
||||
s = open(f).read()
|
||||
m = re.search(r'^theorem scalarImplementation\b', s, re.M)
|
||||
assert m, "scalarImplementation not found"
|
||||
i = m.start()
|
||||
nxt = re.search(r'^(theorem|lemma|def|noncomputable def|end|/--|@\[)', s[i+10:], re.M)
|
||||
assert nxt, "no following declaration"
|
||||
j = i + 10 + nxt.start()
|
||||
# Same cone (Classical.em pulls in Classical.choice/propext), utterly different
|
||||
# claim. Every earlier phase is satisfied; only the statement binding is not.
|
||||
gut = "theorem scalarImplementation : (∀ p : Prop, p ∨ ¬p) := Classical.em\n\n"
|
||||
open(f, "w").write(s[:i] + gut + s[j:])
|
||||
PY
|
||||
recompile ScalarMain || { echo " FAIL setup: the gutted module did not compile"; FAILURES=$((FAILURES+1)); }
|
||||
recompile ScalarAudit
|
||||
expect "gutted statement caught (cone unchanged)" 1 "audit-manifest digest mismatch"
|
||||
cp "$STASH/gut.lean" "$HERE/Proofs/ScalarMain.lean"; rm -f "$STASH/gut.lean"
|
||||
recompile ScalarMain; recompile ScalarAudit
|
||||
|
||||
# ── 4. ATTACK TWO: rewrite a REACHABLE SPECIFICATION BODY while the
|
||||
# certificate's name and cone stay fixed. This is the attack the whole
|
||||
# block exists for: if a reference definition can be edited without
|
||||
# notice, a certificate can be made to say `loop = loop` and every cone
|
||||
# stays byte-identical.
|
||||
#
|
||||
# scDenote is reachable from the scalar statements and its body is
|
||||
# rewritten here to `id (…)`, which is DEFINITIONALLY EQUAL — so the
|
||||
# corpus still compiles and every proof still typechecks. That is the
|
||||
# point: the binding must be sensitive to the body AS WRITTEN, not
|
||||
# merely to what it evaluates to. If the setup fails to compile this
|
||||
# case reports FAIL rather than passing quietly.
|
||||
cp "$HERE/Proofs/ScalarDenote.lean" "$STASH/den.lean"
|
||||
python3 - "$HERE/Proofs/ScalarDenote.lean" <<'PY'
|
||||
import sys
|
||||
f = sys.argv[1]
|
||||
s = open(f).read()
|
||||
old = "def scDenote (a : Sc) : ZMod Ell := (scVal a : ZMod Ell)"
|
||||
assert old in s, "scDenote body not in the expected form"
|
||||
new = "def scDenote (a : Sc) : ZMod Ell := id (scVal a : ZMod Ell)"
|
||||
open(f, "w").write(s.replace(old, new, 1))
|
||||
PY
|
||||
if recompile ScalarDenote; then
|
||||
recompile ScalarAudit
|
||||
expect "rewritten specification body caught (name and cone unchanged)" 1 \
|
||||
"audit-manifest digest mismatch"
|
||||
else
|
||||
echo " FAIL setup: the rewritten specification body did not compile —"
|
||||
echo " this attack did NOT exercise the gate. Do not read the"
|
||||
echo " surrounding passes as covering it."
|
||||
FAILURES=$((FAILURES+1))
|
||||
fi
|
||||
cp "$STASH/den.lean" "$HERE/Proofs/ScalarDenote.lean"; rm -f "$STASH/den.lean"
|
||||
recompile ScalarDenote; recompile ScalarAudit
|
||||
fi
|
||||
|
||||
# ── 5. Restored: green again, and the working tree is as we found it.
|
||||
expect "restored to green" 0 "statements + reachable specification bodies bound"
|
||||
TREE_NOW="$(cd "$HERE/.." && git status --porcelain)"
|
||||
if [ "$TREE_AT_START" != "$TREE_NOW" ]; then
|
||||
echo " FAIL restore: the working tree differs from how this test found it:"
|
||||
diff <(printf '%s\n' "$TREE_AT_START") <(printf '%s\n' "$TREE_NOW") | sed 's/^/ /'
|
||||
FAILURES=$((FAILURES+1))
|
||||
else
|
||||
echo " ok working tree restored to its starting state"
|
||||
fi
|
||||
|
||||
echo ""
|
||||
if [ "$FAILURES" -eq 0 ]; then
|
||||
echo "SELFTEST PASSED — scalar Phase 3c rejects statement- and specification-"
|
||||
echo "level tampering that moves no axiom cone, for the stated reason."
|
||||
exit 0
|
||||
fi
|
||||
echo "SELFTEST FAILED: $FAILURES check(s) did not behave as claimed."
|
||||
exit 1
|
||||
Loading…
Reference in a new issue