diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 0c8d476..f2c2e3c 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -45,6 +45,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 0c7d192..7b66cab 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -1,12 +1,14 @@ c0cfe800f41ce6c12420afb97ad40330b14a2aaad232077e7579e376c48e2ae4 AUDIT-MANIFEST.txt 6b25b7e261633f4fa703de0be1dfd3c263d043107e3b3225d4c5079a93b6a64d check-scalar.sh -ad5d0b6a552c73a6c6650394df0a9e70a807bc30ea8ae21a300b3ce6be62560f check.sh -c0fd4ba1fdec8a6f37b28b5fbe3fc7e93a54f1365443d365ca44c48c117c56b7 extract.sh +b3405d760d352249536f58bb4fcabef7d3329e49cd728ae90786717bd03663f4 check.sh +5e582e44dfd210cb5b8e56f6c31907162fc8e1adf7dac7caf3afb435bbaccb53 extract.sh d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4 GEN-MODEL.sha256 9acc69d66d0c35a88da6d6d020027e5b66ce992763cef3af8de653319abfbb8c inventory-allowlist-scalar.txt 8e2950712ce39ace9cffd3bb58a13984832ff7f3f43ba7b68aa2b1eaa2bc2116 inventory-allowlist.txt 0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard +fde2e987a9f69cb9f39b18ab8b405d73db4d9abee9f714f8be993a40ef617c03 model-correspondence.py +2281dfc465954b026ebc3ac20c12d8dbadf307b4e1fecfc2dab11376a825634f MODEL-CORRESPONDENCE.txt 79a001107928713a22e679e4c4028549df76d0733455bb9937a4f438a0c315c8 Proofs/Audit.lean 4f23dc814f02d3d0355327fd01ab9092dae8b87c76cc296058693428f75e9c7e Proofs/InventoryBasic.lean 84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean @@ -14,6 +16,7 @@ d93d7b77831b7db7acc2f88c395526db850219389a967a0873f3d59ee1f64dd4 GEN-MODEL.sha2 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..b28db44 --- /dev/null +++ b/verification/MODEL-CORRESPONDENCE.txt @@ -0,0 +1,55 @@ +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.array.from_fn|MODEL +CurveField/FunsExternal|core.fmt.Formatter.debug_struct_field2_finish|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.Insts.CoreCmpEq.assert_fields_are_eq|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|edwards.affine.AffinePoint.Insts.CoreCmpEq.assert_fields_are_eq|MODEL +CurveField/FunsExternal|field.FieldElement51.internal_invert_batch|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.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_finalize_bytes|MODEL +CurveSig/FunsExternal|verifying.sha512_new|MODEL +CurveSig/FunsExternal|verifying.sha512_update|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|sha2.Sha512|MODEL +CurveSig/TypesExternal|signature.error.Error|MODEL +CORRESPONDENCE-COUNT|54 diff --git a/verification/check.sh b/verification/check.sh index 7208876..8212dde 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -324,6 +324,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 @@ -357,6 +358,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 6bd1605..e3a233f 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