From 9f7e0ee59475d15362fa71809f5e8a7142f40dfc Mon Sep 17 00:00:00 2001 From: mrwulf Date: Fri, 31 Jul 2026 02:39:34 +0200 Subject: [PATCH] P2-a: attack the arithmetic/apex tier boundary itself selftest-tiers.sh tests the property this repository exists to assert and that nothing had tested: the arithmetic tier rests on the three kernel axioms and NOTHING else. Five cases, all green. control both tiers pass on the untouched tree case 1 an apex axiom injected into an ARITHMETIC certificate's proof, statement untouched so only the cone moves -> Phase 3 rejects case 2 apex boundary widened by one name -> Phase 3 rejects case 3 apex boundary narrowed by one name -> Phase 3 rejects restored both tiers pass again Which axiom to inject is derived per fork from this repo's own documented boundary intersected with the victim module's import closure; no name is hard-coded, so the same script ships unchanged in all four forks. Two defects in the test were found and fixed before it was trusted. The lifted driver first omitted `set -euo pipefail`: the phase's Lean work runs in a subshell and the phase ends in a bare `echo ""`, so without -e the subshell's exit 1 was masked and the driver reported GREEN while printing APEX AUDIT FAILED. And a line-count sanity check passed an empty driver because the CERTS array padded it; the guard now looks for the diagnostics it means to provoke. Both are recorded in the script's comments. The test restores what it touches and rebuilds the module it edits, so it leaves the tree exactly as it found it. New executable is pinned in HARNESS.sha256 (Phase 0c fails closed on an unpinned one). Certified by a full sweep: both buttons, all four forks, from purged trees, machine otherwise idle. 8/8 green, 0 errors. --- TRUSTED-BASE.md | 10 ++ verification/HARNESS.sha256 | 1 + verification/selftest-tiers.sh | 237 +++++++++++++++++++++++++++++++++ 3 files changed, 248 insertions(+) create mode 100755 verification/selftest-tiers.sh diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 7e3dc1f..78374fb 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. **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 cecf39d..cdc44a0 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