From 7acd4ec7c6a515096d32136a5cc0d422525e3e4b Mon Sep 17 00:00:00 2001 From: mrwulf Date: Wed, 22 Jul 2026 23:02:05 +0200 Subject: [PATCH] audit pass: refresh extract.sh phase-1 wording (post-flip drill) Full re-verification of the phase-1 window from primary sources, per the standing drill after a model flip. Results: - diff surface since snapshot 5dca0db: 414 additive lines only; every generic algorithm file byte-untouched - mechanical normalized diff: all 6 mono functions byte-identical to their origins under ONLY the documented transforms (oracle renames, call renames, single-slice M', is_err idiom) - oracle wiring == deployed 128s HASHERS instance incl. the t_len: t_l alias; constants == lib.rs 128s module; exactly 5 oracles in the cone - FULL upstream suite in release WITH the patches: 13 lib + 3 ACVP KAT integration + 12 py_vectors + 37 doc-tests, zero failures (stronger regression evidence than the original window collected) - extraction reproducible: regen byte-identical to committed gen/ - check.sh re-run green; commit-message numerics re-verified (62 defs, 0 sorry, 5+13 axioms, apex 63/30); remote heads match local - hand externals proven to be header + template body exactly One catch, fixed here: extract.sh still carried the pre-phase-1 'expect non-green' wording. Co-Authored-By: Claude Fable 5 --- verification/extract.sh | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/verification/extract.sh b/verification/extract.sh index ff934c8..8f474a7 100755 --- a/verification/extract.sh +++ b/verification/extract.sh @@ -9,14 +9,13 @@ # # Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean # -# PHASE-1 PRECONDITION (gate-0 finding, 2026-07-22): upstream models the -# hash family as `crate::hashers::Hashers`, a struct of plain function -# pointers, which Aeneas cannot translate (3 unique errors, the only -# obstruction in the whole cone). Until the Aeneas-compat patch in -# fips205-source replaces that struct with named opaque free functions -# on the verify path (the curve25519-dalek-source sha512-shim pattern), -# this script produces a PARTIAL model. Do not build proofs on a partial -# model; check.sh stays non-green until extraction is clean. +# HISTORY (gate-0 finding, resolved 2026-07-22): upstream models the hash +# family as `crate::hashers::Hashers`, a struct of plain function pointers, +# which Aeneas cannot translate. The compat patch in fips205-source +# (>= 2d89ee3) provides the additive monomorphic verify_mono module whose +# hash suite is reached through named free functions — this script roots +# there, and charon + aeneas both exit 0. Regeneration is byte-identical +# (verified against the committed gen/ during the 2026-07-22 audit). # # Usage: ./extract.sh set -euo pipefail @@ -46,4 +45,4 @@ echo " NOT overwritten once they exist)" cd "$HERE" aeneas -backend lean -split-files -subdir SlhVerify -dest gen SlhVerify.llbc -echo "Done. Now run ./check.sh (expect non-green until phase 1 lands)." +echo "Done. Now run ./check.sh (Phase 1: the regenerated model must type-check)."