mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-03 19:53:45 +00:00
P2-c: classify and pin the extraction boundary
Aeneas emits a *_Template.lean naming everything the extracted code needs from outside itself — the extraction's own statement of its boundary. extract.sh has always said, in prose, "after regenerating, diff the template against the hand-written file". Prose is not a gate, and the diff cannot be one: the two files legitimately differ in almost every line, holes and Aeneas comments against real definitions and modeling policy. MEASURING FIRST CHANGED WHAT THIS ITEM SHOULD BE. The TODO offered two options — enforce the diff, or pin both files — and the answer turned out to be neither. Both files were ALREADY byte-pinned by Phase 0b. And two further things stand here: the generated Funs.lean imports the model and CALLS these externals, so the Lean compiler enforces their TYPES wherever the extracted code uses them; and the per-certificate exact cones catch any external that becomes, or stops being, an assumption anything depends on. What none of those three sees is the CLASSIFICATION: for each name the extraction asks for, whether this repository answers with an ASSUMPTION or with a PROOF. That is the tier-A/B claim the documents make in prose — the curve calls and the three curve types resolve to proven definitions rather than axioms, because gen/CurveField/Funs.lean opens `namespace curve25519_dalek` and so defines the very names Aeneas asks for. Nothing checked it. A regeneration that renamed one, or a model that quietly answered one with an axiom instead, would have left the documents claiming a proof where the repository had an assumption. Phase 0d recomputes the classification with model-correspondence.py (namespace-aware, so a definition inside a namespace counts under its full name) and requires equality with the committed MODEL-CORRESPONDENCE.txt. UNRESOLVED — the extraction asking for something nothing here provides — is a hard failure. dalek 43 MODEL 8 PROVEN 3 EXTRA anza 38 MODEL 0 PROVEN 4 EXTRA (no CurveSig crate) risc0 36 MODEL 8 PROVEN 4 EXTRA betrusted 35 MODEL 8 PROVEN 4 EXTRA selftest-correspondence.sh, five cases, negative-tested by disabling the comparison. The case that matters is 2: a PROVEN external answered by an axiom instead. No name changes anywhere, every byte pin still matches, and it compiles, because the signature is unchanged — before Phase 0d nothing in the button could tell. Trap recorded for whoever extends it: case 3 first deleted the PROVEN rows, which was VACUOUS on anza, since anza has none — it removed nothing, the table still matched, and the case passed while testing nothing. It now deletes the first row whatever its verdict AND asserts the file changed. extract.sh now points at the gate instead of asking a human to look. Certified by a full sweep: both buttons, all four forks, purged trees, machine otherwise idle. 8/8 green.
This commit is contained in:
parent
96765ea721
commit
92f3229761
7 changed files with 336 additions and 2 deletions
|
|
@ -44,6 +44,20 @@ running Rust code. Everything else is machine-checked.
|
|||
rejected, and are. Before those cases existed nothing in the harness
|
||||
distinguished "this tier needs no hash oracle" from "this tier happens
|
||||
not to use one today".
|
||||
**What answers each external, and whether it is a proof or an assumption.**
|
||||
Aeneas emits a `*_Template.lean` naming everything the extracted code needs
|
||||
from outside itself — the extraction's own statement of its boundary. Phase
|
||||
0d requires every one of those names to be answered either by the
|
||||
hand-written model beside it (an assumption, then governed by the axiom gate
|
||||
and the cones) or by a real definition already in the extracted corpus, and
|
||||
requires the classification to equal the committed
|
||||
`MODEL-CORRESPONDENCE.txt` exactly. That second class is the tier-A/B claim
|
||||
this document makes above — the curve calls and curve types resolving to
|
||||
proven definitions rather than to axioms — and until 2026-07-31 it was prose
|
||||
that nothing checked. `selftest-correspondence.sh` attacks it, including the
|
||||
case that matters most: a PROVEN external answered by an axiom instead,
|
||||
which changes no name anywhere, leaves every byte pin matching, and compiles
|
||||
cleanly because the signature is unchanged.
|
||||
6. **`Scalar52::sub::black_box` (scalar layer)**: this fork's v4.1.3 code
|
||||
implements the constant-time conditional via a local `black_box` =
|
||||
`unsafe { core::ptr::read_volatile(&value) }`. The volatile read is an
|
||||
|
|
|
|||
|
|
@ -1,18 +1,21 @@
|
|||
6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt
|
||||
d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh
|
||||
00329d644a9651bb132c5688cfd89d3616142146a2c8534c34a05e63126feb29 check.sh
|
||||
afa13c814ba9757de8d59777524e496653351112a1a7037a56f1b0b436b28cf9 extract.sh
|
||||
785b290842e43f053eaaf977b190c208ed3f96a146b20783ad3c3565d9d62c01 check.sh
|
||||
9b24f501b1e92b8ae41db0729ae9fbdbf10438ae89764ed29aa07efc2c3d6dd6 extract.sh
|
||||
0ea20d74cd359da404ee3be116058374cbb9fd992ed170e5f6c64f8d7a6b2733 GEN-MODEL.sha256
|
||||
e95982c15c7d754f0c9bcffef95d4c9d4c63589ac51ecdd40870133f377a005c inventory-allowlist-scalar.txt
|
||||
86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt
|
||||
0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh
|
||||
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
||||
fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03 model-correspondence.py
|
||||
b14a4a6f349971f56f7528b93fe5c8dcbfc3b7516c8593361262f5a29aefec08 MODEL-CORRESPONDENCE.txt
|
||||
772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean
|
||||
84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean
|
||||
4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc Proofs/Inventory.lean
|
||||
6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean
|
||||
bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh
|
||||
eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh
|
||||
73d629325b667e715c7e6a633332950ace019e18e6d143ec5cb25846b8ddeb80 selftest-correspondence.sh
|
||||
3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh
|
||||
1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh
|
||||
26f10a749e03cecd7ad173d0d621498386444d8e347f606a99a2fadb06738d86 selftest-shapes.sh
|
||||
|
|
|
|||
49
verification/MODEL-CORRESPONDENCE.txt
Normal file
49
verification/MODEL-CORRESPONDENCE.txt
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
CurveField/FunsExternal|Array.Insts.CoreHashHash.hash|MODEL
|
||||
CurveField/FunsExternal|Bool.Insts.CoreConvertFromChoice.from|MODEL
|
||||
CurveField/FunsExternal|Slice.Insts.CoreFmtDebug.fmt|MODEL
|
||||
CurveField/FunsExternal|Slice.Insts.SubtleConstantTimeEq.ct_eq|MODEL
|
||||
CurveField/FunsExternal|U32.Insts.CoreIterRangeStep.backward_checked|MODEL
|
||||
CurveField/FunsExternal|U32.Insts.CoreIterRangeStep.forward_checked|MODEL
|
||||
CurveField/FunsExternal|U32.Insts.CoreIterRangeStep.steps_between|MODEL
|
||||
CurveField/FunsExternal|U64.Insts.SubtleConditionallySelectable.conditional_assign|MODEL
|
||||
CurveField/FunsExternal|U64.Insts.SubtleConditionallySelectable.conditional_select|MODEL
|
||||
CurveField/FunsExternal|U64.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
|
||||
CurveField/FunsExternal|U8.Insts.CoreHashHash.hash|MODEL
|
||||
CurveField/FunsExternal|U8.Insts.SubtleConstantTimeEq.ct_eq|MODEL
|
||||
CurveField/FunsExternal|backend.get_selected_backend|MODEL
|
||||
CurveField/FunsExternal|backend.serial.scalar_mul.variable_base.mul|MODEL
|
||||
CurveField/FunsExternal|backend.serial.u64.scalar.Scalar52.sub.black_box|MODEL
|
||||
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get|MODEL
|
||||
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_mut|MODEL
|
||||
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index|MODEL
|
||||
CurveField/FunsExternal|edwards.CompressedEdwardsY.from_slice|MODEL
|
||||
CurveField/FunsExternal|edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq|MODEL
|
||||
CurveField/FunsExternal|edwards.EdwardsPoint.Insts.CoreIterTraitsAccumSum.sum|MODEL
|
||||
CurveField/FunsExternal|edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
|
||||
CurveField/FunsExternal|subtle.Choice.Insts.CoreConvertFromU8.from|MODEL
|
||||
CurveField/FunsExternal|subtle.Choice.Insts.CoreOpsBitBitAndChoiceChoice.bitand|MODEL
|
||||
CurveField/FunsExternal|subtle.Choice.Insts.CoreOpsBitBitOrChoiceChoice.bitor|MODEL
|
||||
CurveField/FunsExternal|subtle.Choice.unwrap_u8|MODEL
|
||||
CurveField/FunsExternal|subtle.ConditionallySelectable.conditional_assign.default|MODEL
|
||||
CurveField/FunsExternal|subtle.ConditionallySelectable.conditional_swap.default|MODEL
|
||||
CurveField/FunsExternal|backend.vector.scalar_mul.variable_base.spec_avx2.mul|EXTRA
|
||||
CurveField/FunsExternal|backend.vector.scalar_mul.variable_base.spec_avx512ifma_avx512vl.mul|EXTRA
|
||||
CurveField/FunsExternal|backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul|EXTRA
|
||||
CurveField/TypesExternal|subtle.Choice|MODEL
|
||||
CurveSig/FunsExternal|core.result.Result.Insts.CoreOpsTry_traitTry.branch|MODEL
|
||||
CurveSig/FunsExternal|curve25519_dalek.edwards.CompressedEdwardsY.as_bytes|PROVEN
|
||||
CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.compress|PROVEN
|
||||
CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint|PROVEN
|
||||
CurveSig/FunsExternal|curve25519_dalek.scalar.Scalar.from_bytes_mod_order|PROVEN
|
||||
CurveSig/FunsExternal|curve25519_dalek.scalar.Scalar.from_bytes_mod_order_wide|PROVEN
|
||||
CurveSig/FunsExternal|ed25519.Signature.to_bytes|MODEL
|
||||
CurveSig/FunsExternal|signature.compressed_from_bytes|MODEL
|
||||
CurveSig/FunsExternal|signature.error.Error.new|MODEL
|
||||
CurveSig/FunsExternal|verifying.sha512_hash3|MODEL
|
||||
CurveSig/FunsExternal|core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual|EXTRA
|
||||
CurveSig/TypesExternal|curve25519_dalek.edwards.CompressedEdwardsY|PROVEN
|
||||
CurveSig/TypesExternal|curve25519_dalek.edwards.EdwardsPoint|PROVEN
|
||||
CurveSig/TypesExternal|curve25519_dalek.scalar.Scalar|PROVEN
|
||||
CurveSig/TypesExternal|ed25519.Signature|MODEL
|
||||
CurveSig/TypesExternal|signature.error.Error|MODEL
|
||||
CORRESPONDENCE-COUNT|48
|
||||
|
|
@ -320,6 +320,7 @@ echo " $(wc -l < "$HERE/GEN-MODEL.sha256") extracted-model files match their pi
|
|||
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
|
||||
MODEL-CORRESPONDENCE.txt # the extraction boundary Phase 0d recomputes
|
||||
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
|
||||
|
|
@ -352,6 +353,63 @@ if ! ( cd "$HERE" && sha256sum -c --quiet HARNESS.sha256 ) ; then
|
|||
exit 1
|
||||
fi
|
||||
echo " $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins"
|
||||
# ── Phase 0d: template/model correspondence ─────────────────────────────────
|
||||
# WHAT AENEAS'S TEMPLATE IS. When Aeneas extracts the Rust it also emits, for
|
||||
# each crate, a *_Template.lean naming everything the extracted code needs from
|
||||
# OUTSIDE itself. That template is the extraction's own statement of its
|
||||
# boundary. The hand-written *External.lean beside it is our answer to that
|
||||
# statement, and `extract.sh` has always said, in prose, "after regenerating,
|
||||
# diff the template against the hand-written file". Prose is not a gate.
|
||||
#
|
||||
# WHAT THIS ADDS, given that three other things already stand here. Phase 0b
|
||||
# byte-pins both files, so neither can drift from its pin unnoticed. The
|
||||
# generated Funs.lean imports the model and CALLS these externals, so the Lean
|
||||
# compiler already enforces their types wherever the extracted code uses them.
|
||||
# The per-certificate exact cones catch any external that becomes — or stops
|
||||
# being — an assumption anything depends on. What none of those three sees is
|
||||
# the CLASSIFICATION: for each name the extraction asks for, whether this
|
||||
# repository answers with an assumption or with a proof.
|
||||
#
|
||||
# That distinction is the tier-A/B claim, and it was prose until 2026-07-31.
|
||||
# The docs say the curve calls (compress, as_bytes,
|
||||
# vartime_double_scalar_mul_basepoint, from_bytes_mod_order{,_wide}) and the
|
||||
# three curve TYPES resolve to the PROVEN model's own definitions rather than
|
||||
# to axioms — because gen/CurveField/Funs.lean opens `namespace
|
||||
# curve25519_dalek`, so the names Aeneas asks for are the names it defines.
|
||||
# Nothing checked it. A regeneration that renamed one of those, or a model that
|
||||
# quietly answered one with an axiom instead, would have left the documents
|
||||
# claiming a proof where the repository now had an assumption.
|
||||
#
|
||||
# model-correspondence.py recomputes the classification from the files —
|
||||
# namespace-aware, so a definition inside `namespace curve25519_dalek` counts
|
||||
# under its full name — and the result must equal the committed table exactly.
|
||||
# UNRESOLVED is a hard failure in the tool itself: the extraction asking for
|
||||
# something this repository does not provide at all.
|
||||
echo "=== Phase 0d: template/model correspondence ==="
|
||||
CORR_FILE="$HERE/MODEL-CORRESPONDENCE.txt"
|
||||
if [ ! -s "$CORR_FILE" ]; then
|
||||
echo "FATAL: MODEL-CORRESPONDENCE.txt is missing or empty — the extraction boundary is unpinned."
|
||||
exit 1
|
||||
fi
|
||||
CORR_OBSERVED=$(cd "$HERE" && python3 model-correspondence.py .) || {
|
||||
echo "$CORR_OBSERVED" | grep UNRESOLVED | sed 's/^/ /'
|
||||
echo "MODEL CORRESPONDENCE FAILED: the extraction declares an external that neither"
|
||||
echo "the hand-written model nor the proven corpus provides."
|
||||
exit 1
|
||||
}
|
||||
if ! diff -u "$CORR_FILE" <(printf '%s\n' "$CORR_OBSERVED") > /tmp/corr-diff.$$ 2>&1; then
|
||||
echo " MODEL CORRESPONDENCE DRIFT (< committed, > observed):"
|
||||
sed -n '4,24p' /tmp/corr-diff.$$ | sed 's/^/ /'
|
||||
rm -f /tmp/corr-diff.$$
|
||||
echo "MODEL CORRESPONDENCE FAILED: an external changed how it is answered."
|
||||
exit 1
|
||||
fi
|
||||
rm -f /tmp/corr-diff.$$
|
||||
echo " $(grep -c '|MODEL$' "$CORR_FILE") externals answered by the hand-written model (assumptions)"
|
||||
echo " $(grep -c '|PROVEN$' "$CORR_FILE") answered by PROVEN definitions in the extracted corpus"
|
||||
echo " $(grep -c '|EXTRA$' "$CORR_FILE") model declarations beyond what the extraction asks for"
|
||||
echo ""
|
||||
|
||||
# ── Phase 1: stub + axiom-smuggling audit ───────────────────────────────────
|
||||
echo "=== Phase 1: stub audit ==="
|
||||
if grep -rn 'by trivial' "$HERE"/Proofs/*Spec*.lean 2>/dev/null; then
|
||||
|
|
|
|||
|
|
@ -18,6 +18,16 @@
|
|||
# After regenerating, diff the templates against the hand-written files:
|
||||
# diff gen/CurveField/FunsExternal_Template.lean gen/CurveField/FunsExternal.lean
|
||||
#
|
||||
# That diff is a READING aid, not a gate — the two files legitimately differ in
|
||||
# almost every line (the template holds holes and Aeneas's own comments; the
|
||||
# model holds real definitions and the modeling policy). What IS enforced, by
|
||||
# check.sh Phase 0d, is the classification: every name the template declares
|
||||
# must be answered either by the hand-written model or by a real definition in
|
||||
# the proven corpus, and which of the two must match MODEL-CORRESPONDENCE.txt.
|
||||
# Regenerate that table with `python3 model-correspondence.py .` and commit the
|
||||
# change deliberately — a proof silently becoming an assumption is exactly what
|
||||
# the phase exists to stop.
|
||||
#
|
||||
# Usage: ./extract.sh
|
||||
set -euo pipefail
|
||||
|
||||
|
|
|
|||
74
verification/model-correspondence.py
Executable file
74
verification/model-correspondence.py
Executable file
|
|
@ -0,0 +1,74 @@
|
|||
#!/usr/bin/env python3
|
||||
"""Classify every external the extraction declares.
|
||||
|
||||
For each gen/<dir>/<X>_Template.lean, Aeneas states what the extracted Rust
|
||||
needs from outside. Each such name must be provided by exactly one of:
|
||||
|
||||
MODEL — declared in the hand-written sibling gen/<dir>/<X>.lean: an
|
||||
assumption, which the axiom gate and the per-certificate cones
|
||||
then govern;
|
||||
PROVEN — resolved to a real definition in the proven corpus, because a
|
||||
module of this repository declares it (namespace-aware). This is
|
||||
the valuable case and the one the docs claim for the tier-A/B
|
||||
curve calls; nothing has ever checked it.
|
||||
|
||||
Anything else is drift: the extraction asks for something this repository does
|
||||
not provide.
|
||||
"""
|
||||
import re, sys, os, glob
|
||||
|
||||
DECL = re.compile(
|
||||
r'^[ \t]*(?:@\[[^\]]*\]\s*)?(?:private |protected |noncomputable |unsafe )*'
|
||||
r'(axiom|def|abbrev|opaque|structure|inductive)[ \t]+([A-Za-z_][A-Za-z0-9_.\'!?]*)')
|
||||
NS = re.compile(r'^[ \t]*(namespace|end)[ \t]+([A-Za-z_][A-Za-z0-9_.\']*)')
|
||||
|
||||
def declared(path):
|
||||
"""Fully-qualified names declared in one file, honouring namespaces."""
|
||||
names, stack = set(), []
|
||||
for line in open(path, encoding='utf-8', errors='replace'):
|
||||
m = NS.match(line)
|
||||
if m:
|
||||
if m.group(1) == 'namespace':
|
||||
stack.append(m.group(2))
|
||||
elif stack and stack[-1] == m.group(2):
|
||||
stack.pop()
|
||||
continue
|
||||
d = DECL.match(line)
|
||||
if d:
|
||||
names.add('.'.join(stack + [d.group(2)]) if stack else d.group(2))
|
||||
return names
|
||||
|
||||
def main(root):
|
||||
gen = os.path.join(root, 'gen')
|
||||
templates = sorted(glob.glob(os.path.join(gen, '*', '*_Template.lean')))
|
||||
# The proven corpus: every generated module that is neither a template nor
|
||||
# a hand-written model. These are the files Aeneas produced from Rust.
|
||||
models = {t.replace('_Template', '') for t in templates}
|
||||
corpus = set()
|
||||
for f in sorted(glob.glob(os.path.join(gen, '*', '*.lean'))):
|
||||
if f in models or f.endswith('_Template.lean'):
|
||||
continue
|
||||
corpus |= declared(f)
|
||||
|
||||
rows, unresolved = [], []
|
||||
for t in templates:
|
||||
model = t.replace('_Template', '')
|
||||
rel = os.path.relpath(t, gen).replace('_Template.lean', '')
|
||||
tnames = declared(t)
|
||||
mnames = declared(model) if os.path.exists(model) else set()
|
||||
for n in sorted(tnames):
|
||||
if n in mnames:
|
||||
rows.append(f'{rel}|{n}|MODEL')
|
||||
elif n in corpus:
|
||||
rows.append(f'{rel}|{n}|PROVEN')
|
||||
else:
|
||||
rows.append(f'{rel}|{n}|UNRESOLVED')
|
||||
unresolved.append(f'{rel}|{n}')
|
||||
for n in sorted(mnames - tnames):
|
||||
rows.append(f'{rel}|{n}|EXTRA')
|
||||
print('\n'.join(rows))
|
||||
print(f'CORRESPONDENCE-COUNT|{len(rows)}')
|
||||
return 1 if unresolved else 0
|
||||
|
||||
if __name__ == '__main__':
|
||||
sys.exit(main(sys.argv[1]))
|
||||
126
verification/selftest-correspondence.sh
Executable file
126
verification/selftest-correspondence.sh
Executable file
|
|
@ -0,0 +1,126 @@
|
|||
#!/usr/bin/env bash
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
# selftest-correspondence.sh — attacks check.sh Phase 0d.
|
||||
#
|
||||
# Phase 0d asserts HOW each external the extraction asks for is answered: with
|
||||
# an assumption in the hand-written model, or with a proof already in the
|
||||
# extracted corpus. The second class is the one the documents make a claim
|
||||
# about — the curve calls and curve types are said to resolve to the proven
|
||||
# model's own definitions rather than to axioms — and that claim was prose
|
||||
# until this phase existed.
|
||||
#
|
||||
# 0 control: the committed table matches the files
|
||||
# 1 the extraction asks for something NOTHING provides -> UNRESOLVED
|
||||
# 2 a PROVEN external answered by an axiom in the model instead. This is the
|
||||
# attack that matters: a proof silently downgraded to an assumption, in a
|
||||
# name whose spelling does not change anywhere else.
|
||||
# 3 a row deleted from the committed table -> drift
|
||||
# 4 a row's verdict edited in the committed table -> drift
|
||||
#
|
||||
# No Lean: Phase 0d is pure text over gen/. Seconds, not minutes.
|
||||
# ─────────────────────────────────────────────────────────────────────────────
|
||||
set -uo pipefail
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
FAILURES=0
|
||||
STASH="$(mktemp -d)"
|
||||
|
||||
cleanup() {
|
||||
[ -f "$STASH/corr" ] && cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
|
||||
[ -f "$STASH/model" ] && cp "$STASH/model" "$HERE/$MODEL_REL"
|
||||
[ -f "$STASH/tmpl" ] && cp "$STASH/tmpl" "$HERE/$TMPL_REL"
|
||||
rm -rf "$STASH"
|
||||
}
|
||||
|
||||
# Derive the victims from this repo rather than naming them: the forks do not
|
||||
# share a gen/ layout (anza has no CurveSig crate at all, so it has no PROVEN
|
||||
# rows and case 2 does not apply there).
|
||||
TMPL_REL=$(cd "$HERE" && ls gen/*/FunsExternal_Template.lean | head -1)
|
||||
MODEL_REL="${TMPL_REL/_Template/}"
|
||||
PROVEN_ROW=$(grep -m1 '|PROVEN$' "$HERE/MODEL-CORRESPONDENCE.txt" || true)
|
||||
|
||||
trap cleanup EXIT INT TERM
|
||||
cp "$HERE/MODEL-CORRESPONDENCE.txt" "$STASH/corr"
|
||||
cp "$HERE/$MODEL_REL" "$STASH/model"
|
||||
cp "$HERE/$TMPL_REL" "$STASH/tmpl"
|
||||
|
||||
# Phase 0d lifted from the shipping button.
|
||||
{ echo 'set -euo pipefail'
|
||||
echo "HERE=\"$HERE\""
|
||||
awk '/^# ── Phase 0d/{f=1} f&&/^# ── (Phase 1|Phases end)/{exit} f{print}' "$HERE/check.sh"
|
||||
} > "$STASH/p0d.sh"
|
||||
for want in 'Phase 0d' 'MODEL CORRESPONDENCE' 'model-correspondence.py'; do
|
||||
grep -qF "$want" "$STASH/p0d.sh" || {
|
||||
echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved."; exit 1; }
|
||||
done
|
||||
|
||||
expect() { # expect <label> <want-rc> <want-substring>
|
||||
local label="$1" want_rc="$2" want_txt="$3" out rc
|
||||
out=$(bash "$STASH/p0d.sh" 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 (rejected for the wrong reason)"
|
||||
echo " wanted: $want_txt"; tail -6 <<<"$out" | sed 's/^/ /'
|
||||
FAILURES=$((FAILURES+1)); return
|
||||
fi
|
||||
echo " ✓ $label"
|
||||
}
|
||||
|
||||
echo "=== selftest-correspondence: attacking check.sh Phase 0d ==="
|
||||
echo " template: $TMPL_REL"
|
||||
|
||||
expect "control: the committed table matches the files" 0 "answered by PROVEN definitions"
|
||||
|
||||
# ── 1. the extraction asks for something nothing provides ──────────────────
|
||||
printf '\naxiom selftest_unprovided_external : Nat\n' >> "$HERE/$TMPL_REL"
|
||||
expect "case 1: an external nothing provides" 1 "MODEL CORRESPONDENCE FAILED"
|
||||
cp "$STASH/tmpl" "$HERE/$TMPL_REL"
|
||||
|
||||
# ── 2. a proof silently downgraded to an assumption ────────────────────────
|
||||
# Answer a PROVEN external with an axiom in the model. The name does not change
|
||||
# anywhere; only the way it is answered does. Nothing else in the button sees
|
||||
# this: the byte pins still match their files, the compiler is content because
|
||||
# the signature is unchanged, and no certificate's cone moves unless something
|
||||
# happens to depend on it.
|
||||
if [ -n "$PROVEN_ROW" ]; then
|
||||
PROVEN_NAME=$(cut -d'|' -f2 <<<"$PROVEN_ROW")
|
||||
PROVEN_TMPL=$(cut -d'|' -f1 <<<"$PROVEN_ROW")
|
||||
VICTIM_MODEL="gen/${PROVEN_TMPL}.lean"
|
||||
cp "$HERE/$VICTIM_MODEL" "$STASH/model2"
|
||||
printf '\naxiom %s : Nat\n' "$PROVEN_NAME" >> "$HERE/$VICTIM_MODEL"
|
||||
expect "case 2: a PROVEN external downgraded to an assumption" 1 "MODEL CORRESPONDENCE DRIFT"
|
||||
cp "$STASH/model2" "$HERE/$VICTIM_MODEL"
|
||||
else
|
||||
echo " · case 2 skipped: this fork's extraction has no PROVEN externals"
|
||||
fi
|
||||
|
||||
# ── 3/4. the committed table itself ────────────────────────────────────────
|
||||
# Delete the FIRST row, whatever its verdict. An earlier draft deleted the
|
||||
# PROVEN rows, which was vacuous on anza — that fork's extraction has none, so
|
||||
# nothing was removed, the table still matched, and the case passed by testing
|
||||
# nothing. Pick a row every fork is guaranteed to have.
|
||||
sed '0,/|/{/|/d}' "$STASH/corr" > "$HERE/MODEL-CORRESPONDENCE.txt"
|
||||
if ! diff -q "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt" >/dev/null; then
|
||||
expect "case 3: a row deleted from the committed table" 1 "MODEL CORRESPONDENCE DRIFT"
|
||||
else
|
||||
echo " ✗ case 3: the table was not actually modified — the case is vacuous"
|
||||
FAILURES=$((FAILURES+1))
|
||||
fi
|
||||
cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
|
||||
|
||||
sed -i '0,/|MODEL$/s/|MODEL$/|PROVEN/' "$HERE/MODEL-CORRESPONDENCE.txt"
|
||||
expect "case 4: a verdict edited in the committed table" 1 "MODEL CORRESPONDENCE DRIFT"
|
||||
cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
|
||||
|
||||
expect "restored: the table matches again" 0 "answered by PROVEN definitions"
|
||||
|
||||
echo ""
|
||||
if [ "$FAILURES" -eq 0 ]; then
|
||||
echo "SELFTEST PASSED — an external cannot change how it is answered, and a"
|
||||
echo "proof cannot be downgraded to an assumption, without failing the button."
|
||||
exit 0
|
||||
fi
|
||||
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
|
||||
exit 1
|
||||
Loading…
Reference in a new issue