diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 1756a2d..45fdfee 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -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. **Compilation of Rust to machine code** (rustc backend) is out of scope, as is side-channel behaviour (timing, speculation). The proofs are about functional correctness at the MIR/LLBC level. diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 70dce86..4cf362f 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,18 +1,21 @@ 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh -00329d644a9651bb132c5688cfd89d3616142146a2c8534c34a05e63126feb29 check.sh -7a55136cd15ab96b3ab77234ffb8a2fc7c9544cb8b36426d29e257ffb2d2ba6e extract.sh +785b290842e43f053eaaf977b190c208ed3f96a146b20783ad3c3565d9d62c01 check.sh +71244d824847311bcb3ba8ad1f1905c4b24fe8f015e3230969914019cb628b61 extract.sh c9672a28825cd1d4055fb9efbb4a1d94c921c7b5c79e4cd5d0626ba061e554c1 GEN-MODEL.sha256 e6f31b4303f5a344781d353f1dddefc185876df470e27b285c81556621e65c05 inventory-allowlist-scalar.txt 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard +fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03 model-correspondence.py +ceebf2872eac57ebe2d61d00258ea3d367d263b6c6ebfaae1eede92ef3d478a2 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 diff --git a/verification/MODEL-CORRESPONDENCE.txt b/verification/MODEL-CORRESPONDENCE.txt new file mode 100644 index 0000000..0d6cfed --- /dev/null +++ b/verification/MODEL-CORRESPONDENCE.txt @@ -0,0 +1,48 @@ +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|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|47 diff --git a/verification/check.sh b/verification/check.sh index 6b0b790..62955c6 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -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 diff --git a/verification/extract.sh b/verification/extract.sh index f30414e..0be61d3 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -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 diff --git a/verification/model-correspondence.py b/verification/model-correspondence.py new file mode 100755 index 0000000..1563013 --- /dev/null +++ b/verification/model-correspondence.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +"""Classify every external the extraction declares. + +For each gen//_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//.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])) diff --git a/verification/selftest-correspondence.sh b/verification/selftest-correspondence.sh new file mode 100755 index 0000000..7fe9813 --- /dev/null +++ b/verification/selftest-correspondence.sh @@ -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