diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 720cc49..6077218 100644 --- a/TRUSTED-BASE.md +++ b/TRUSTED-BASE.md @@ -34,6 +34,16 @@ running Rust code. Everything else is machine-checked. implementation itself is NOT verified. Zero curve, scalar, or backend axioms are in any of the four cones. The constructive decompress theorem underneath the full lift (`decompress_of_canonical`) carries the standard three axioms ONLY. + That two-tier separation is enforced, not merely observed. Phase 3 + requires every arithmetic certificate's cone to be exactly the three + kernel axioms, and every apex cone to equal the documented set above + exactly. `selftest-tiers.sh` attacks it from both sides: it injects one + of the axioms above into an arithmetic certificate's *proof*, leaving the + statement untouched so that only the cone moves, and it shifts the + documented apex boundary by one name in each direction. All three must be + 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". 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 diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index fbd2230..eb5383a 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -16,3 +16,4 @@ eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgat 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh 2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f selftest-statements.sh +df2389909839c5c2275097044b112bd254e48aa21b4b8f6c1430847c0a0c7cc6 selftest-tiers.sh diff --git a/verification/selftest-tiers.sh b/verification/selftest-tiers.sh new file mode 100755 index 0000000..5921546 --- /dev/null +++ b/verification/selftest-tiers.sh @@ -0,0 +1,237 @@ +#!/usr/bin/env bash +# ───────────────────────────────────────────────────────────────────────────── +# selftest-tiers.sh — adversarial self-test for the TWO-TIER axiom boundary. +# +# This repository has two tiers and the distinction is the most valuable +# property it has: +# +# · the ARITHMETIC tier — field, curve, scalar and encoding certificates — +# must rest on Lean's three kernel axioms and NOTHING else. No hash oracle, +# no wire-format opacity. That is what makes "the curve arithmetic is +# proven" a claim about mathematics rather than about assumptions; +# · the APEX tier — the four signature certificates — legitimately carries +# this fork's SHA-512 and wire-format axioms, because a signature scheme +# cannot be verified without a hash. +# +# Collapsing the two, by widening the arithmetic tier to accept oracles, would +# destroy that property while every button stayed green — and it is exactly +# what a single careless edit to a shared lemma does. Until 2026-07-30 nothing +# tested it. These cases do. +# +# 0 control: untouched tree passes +# 1 AN APEX ORACLE LEAKED INTO AN ARITHMETIC CERTIFICATE. A hash axiom is +# introduced into the proof of an arithmetic certificate — statement +# unchanged, so only the cone moves. Phase 3 must name that certificate. +# 2 the apex boundary WIDENED by one name -> apex cones no longer match +# 3 the apex boundary NARROWED by one name -> same, from the other side +# +# Case 1 recompiles one module and is the slow one (~2 min). Cases 2 and 3 need +# no Lean at all. Run after a green check.sh. +# ───────────────────────────────────────────────────────────────────────────── +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}" +FAILURES=0 +SAFE_EXIT=0 +STASH="$(mktemp -d)" + +# The audit phases write a temporary driver (.audit-XXXX.lean / .apex-XXXX.lean) +# and delete it on the way out — but a phase that exits 1 never reaches its own +# rm. This test provokes four such exits on purpose, so it is this test's job to +# clear the residue. Record what was here first and remove only what we caused; +# litter that predates the run is somebody else's finding, not ours to hide. +shopt -s nullglob +LITTER_BEFORE="$(printf '%s\n' "$HERE"/.audit-*.lean "$HERE"/.apex-*.lean | sort)" +shopt -u nullglob + +VICTIM_MOD=PointEqSpec +VICTIM_CERT=CurveFieldProofs.enc_point_inj + +# Which apex axiom to smuggle downward is a per-fork question, so derive it +# rather than hard-code it: take this repo's own documented apex boundary, drop +# the three kernel axioms, and keep the names that are actually declared inside +# the victim module's import closure — an axiom the victim cannot see cannot be +# injected into it. Prefer a hash oracle when one is reachable (dalek reaches +# verifying.sha512_new); the three forks that route SHA-512 through a single +# apex-only module reach only the wire-format axioms, which serve equally well: +# the property under test is that NO apex axiom may appear in this tier. +import_closure() { # every .lean file the victim module transitively imports + local -A seen=(); local -a q=("$VICTIM_MOD"); local m f i + while [ ${#q[@]} -gt 0 ]; do + m="${q[0]}"; q=("${q[@]:1}") + [ -n "${seen[$m]:-}" ] && continue + seen[$m]=1 + for f in "$HERE/Proofs/$m.lean" "$HERE/gen/${m//.//}.lean"; do + [ -f "$f" ] || continue + echo "$f" + while read -r i; do q+=("$i"); done \ + < <(grep '^import ' "$f" | awk '{print $2}' | sed 's/^Proofs\.//') + done + done +} +oracle_for_this_fork() { + local allowed closure m + allowed=$(grep -h "ALLOWED='" "$HERE/check.sh" | sed "s/.*ALLOWED='\[//;s/\].*//" \ + | tr ',' '\n' | sed 's/^ *//;s/ *$//' \ + | grep -v '^propext$\|^Classical.choice$\|^Quot.sound$') + closure=$(import_closure) + for m in $(echo "$allowed" | grep 'sha512\|sha2') $allowed; do + if grep -qE "^axiom ${m//./\\.}( |:)" $closure 2>/dev/null; then echo "$m"; return; fi + done +} +ORACLE="$(oracle_for_this_fork)" +if [ -z "$ORACLE" ]; then + echo "FATAL: this fork's apex boundary lists no axiom this test can inject."; exit 1 +fi + +cleanup() { + [ -f "$STASH/victim" ] && cp "$STASH/victim" "$HERE/Proofs/$VICTIM_MOD.lean" + [ -f "$STASH/check" ] && cp "$STASH/check" "$HERE/check.sh" + [ -f "$STASH/pins" ] && cp "$STASH/pins" "$HERE/HARNESS.sha256" + # If we are dying mid-case the victim's .olean may still hold the injected + # oracle while its source no longer shows it. That artifact is worse than no + # artifact: it is a poisoned object with a clean source. Remove it. Phase 3's + # vacuous-scan guard then fails loudly, and any full run rebuilds it anyway. + # On the normal path the run has already restored and rebuilt the module, so + # deleting it there would leave the tree worse than we found it — an + # --audit-only run afterwards would fail on a missing artifact we removed. + [ "$SAFE_EXIT" -eq 1 ] || rm -f "$HERE/Proofs/$VICTIM_MOD.olean" "$HERE/Proofs/$VICTIM_MOD.ilean" + local f + shopt -s nullglob + for f in "$HERE"/.audit-*.lean "$HERE"/.apex-*.lean; do + grep -qxF "$f" <<<"$LITTER_BEFORE" || rm -f "$f" "${f%.lean}.olean" + done + shopt -u nullglob + rm -rf "$STASH" +} +trap cleanup EXIT INT TERM +cp "$HERE/Proofs/$VICTIM_MOD.lean" "$STASH/victim" +cp "$HERE/check.sh" "$STASH/check" +cp "$HERE/HARNESS.sha256" "$STASH/pins" + +# The axiom audit, lifted from the shipping button so the tested logic is the +# shipping logic. BOTH tiers live under the one "Phase 3" marker — the +# per-certificate arithmetic audit and, below it, the apex boundary check. An +# earlier draft of this file lifted them as two markers, got an empty driver for +# the second, and the driver still cleared a line-count sanity check because the +# CERTS array padded it. So the guard below looks for the two diagnostics we +# intend to provoke, not for a number of lines. +lift() { + # set -euo pipefail, verbatim from the button. The -e is load-bearing and was + # missing from an earlier draft: the phase's Lean work happens in a subshell + # and the phase ends with a bare `echo ""`, so without -e a subshell that + # exits 1 is masked by the echo's success and the driver reports green while + # printing APEX AUDIT FAILED. The button gets this right at check.sh:32; a + # lift that does not copy it tests something the button never runs. + { echo 'set -euo pipefail' + echo 'source ~/aeneas-toolchain/env.sh' + echo "HERE=\"$HERE\"" + echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"' + echo "TIMEOUT=$TIMEOUT" + sed -n '/^EXPECTED=/p;/^AUDIT_IMPORTS=(/,/^)/p;/^CERTS=(/,/^)/p' "$HERE/check.sh" + awk '/^# ── Phase 3: axiom audit/{f=1} f&&/^# ── (Phase 3c|Phases end)/{exit} f{print}' "$HERE/check.sh" + } > "$STASH/p3.sh" + for want in 'AXIOM AUDIT FAILED' 'APEX AUDIT FAILED' 'CERTS=(' 'AUDIT_IMPORTS=(' 'EXPECTED='; do + if ! grep -qF "$want" "$STASH/p3.sh"; then + echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved." + exit 1 + fi + done +} +lift + +recompile() { + ( 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 '$HERE/lean-guard' Proofs/$VICTIM_MOD.lean + " ) >/dev/null 2>&1 +} + +expect() { # expect