mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
e2c5cf1d4b
Aeneas emits a *_Template.lean naming everything the extracted code needs from outside itself — the extraction's own statement of its boundary. extract.sh has always said, in prose, "after regenerating, diff the template against the hand-written file". Prose is not a gate, and the diff cannot be one: the two files legitimately differ in almost every line, holes and Aeneas comments against real definitions and modeling policy. MEASURING FIRST CHANGED WHAT THIS ITEM SHOULD BE. The TODO offered two options — enforce the diff, or pin both files — and the answer turned out to be neither. Both files were ALREADY byte-pinned by Phase 0b. And two further things stand here: the generated Funs.lean imports the model and CALLS these externals, so the Lean compiler enforces their TYPES wherever the extracted code uses them; and 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 is the tier-A/B claim the documents make in prose — the curve calls and the three curve types resolve to proven definitions rather than axioms, because gen/CurveField/Funs.lean opens `namespace curve25519_dalek` and so defines the very names Aeneas asks for. Nothing checked it. A regeneration that renamed one, or a model that quietly answered one with an axiom instead, would have left the documents claiming a proof where the repository had an assumption. Phase 0d recomputes the classification with model-correspondence.py (namespace-aware, so a definition inside a namespace counts under its full name) and requires equality with the committed MODEL-CORRESPONDENCE.txt. UNRESOLVED — the extraction asking for something nothing here provides — is a hard failure. dalek 43 MODEL 8 PROVEN 3 EXTRA anza 38 MODEL 0 PROVEN 4 EXTRA (no CurveSig crate) risc0 36 MODEL 8 PROVEN 4 EXTRA betrusted 35 MODEL 8 PROVEN 4 EXTRA selftest-correspondence.sh, five cases, negative-tested by disabling the comparison. The case that matters is 2: a PROVEN external answered by an axiom instead. No name changes anywhere, every byte pin still matches, and it compiles, because the signature is unchanged — before Phase 0d nothing in the button could tell. Trap recorded for whoever extends it: case 3 first deleted the PROVEN rows, which was VACUOUS on anza, since anza has none — it removed nothing, the table still matched, and the case passed while testing nothing. It now deletes the first row whatever its verdict AND asserts the file changed. extract.sh now points at the gate instead of asking a human to look. Certified by a full sweep: both buttons, all four forks, purged trees, machine otherwise idle. 8/8 green.
100 lines
5 KiB
Bash
Executable file
100 lines
5 KiB
Bash
Executable file
#!/usr/bin/env bash
|
|
# Regenerate the Lean model in gen/ from the Rust sources.
|
|
#
|
|
# SCOPE: field arithmetic + Edwards point arithmetic
|
|
# roots: crate::field, crate::backend::serial::u64::field,
|
|
# crate::backend::serial::curve_models, crate::edwards
|
|
# (same widening the reference solution used for its Tier-1 addition-law
|
|
# theorem; scalar-mul backends stay opaque — upstream Aeneas cannot
|
|
# translate them; they are modeled/axiomatized in
|
|
# gen/CurveField/FunsExternal.lean OUTSIDE every certificate's cone.
|
|
# decompress IS extracted since the phase-2 full lift — the source's
|
|
# step_2 uses the documented negate-then-conditional-assign rewrite).
|
|
#
|
|
# Rust --charon--> CurveField.llbc --aeneas--> gen/CurveField/*.lean
|
|
#
|
|
# The hand-written gen/CurveField/{TypesExternal,FunsExternal}.lean are NOT
|
|
# touched by regeneration (Aeneas only rewrites the *_Template variants).
|
|
# 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
|
|
|
|
source ~/aeneas-toolchain/env.sh
|
|
HERE="$(cd "$(dirname "$0")" && pwd)"
|
|
CRATE=~/GitClone/FormalVerification/sources/curve25519-dalek-source/curve25519-dalek
|
|
|
|
echo "[1/4] charon: Rust -> LLBC (field + curve_models + edwards + scalar [MERGED GEN])"
|
|
cd "$CRATE"
|
|
# Force the portable SERIAL backend (the one we verify): the SIMD dispatch
|
|
# arm is `#[cfg(curve25519_dalek_backend = "simd")]`, so pinning the cfg to
|
|
# "serial" removes it from the extraction — no vector-backend axiom leaks in.
|
|
export RUSTFLAGS='--cfg curve25519_dalek_backend="serial"'
|
|
charon cargo --preset=aeneas \
|
|
--start-from crate::field \
|
|
--start-from crate::backend::serial::u64::field \
|
|
--start-from crate::backend::serial::curve_models \
|
|
--start-from crate::edwards \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::add' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::sub' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::mul' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::square' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::montgomery_mul' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::montgomery_square' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::montgomery_reduce' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::montgomery_invert' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::as_montgomery' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::from_montgomery' \
|
|
--start-from 'crate::backend::serial::u64::scalar::_::from_bytes_wide' \
|
|
--start-from 'crate::scalar::_::from_bytes_mod_order' \
|
|
--start-from 'crate::scalar::_::from_bytes_mod_order_wide' \
|
|
--opaque 'crate::field::_::internal_invert_batch' \
|
|
--opaque 'crate::backend::serial::scalar_mul::variable_base' \
|
|
--opaque 'crate::backend::serial::scalar_mul::straus' \
|
|
--opaque 'crate::backend::serial::scalar_mul::precomputed_straus' \
|
|
--opaque 'crate::backend::serial::scalar_mul::pippenger' \
|
|
--opaque 'crate::backend::vector' \
|
|
--opaque 'crate::backend::get_selected_backend' \
|
|
--opaque 'crate::edwards::_::sum' \
|
|
--opaque 'crate::edwards::_::from_slice' \
|
|
--dest-file "$HERE/CurveField.llbc" \
|
|
-- --no-default-features
|
|
|
|
echo "[2/4] aeneas: LLBC -> Lean (split files, CurveField.* modules)"
|
|
cd "$HERE"
|
|
aeneas -backend lean -split-files -subdir CurveField -dest gen CurveField.llbc
|
|
|
|
echo "[3/4] charon: ed25519-dalek verify glue -> LLBC (SHA-512 opaque)"
|
|
SIGCRATE="$(dirname "$CRATE")/ed25519-dalek"
|
|
cd "$SIGCRATE"
|
|
charon cargo --preset=aeneas \
|
|
--start-from 'crate::verifying::verify_sha512' \
|
|
--start-from 'crate::verifying::recompute_r_sha512' \
|
|
--opaque 'crate::verifying::sha512_new' \
|
|
--opaque 'crate::verifying::sha512_update' \
|
|
--opaque 'crate::verifying::sha512_finalize_bytes' \
|
|
--opaque 'crate::signature::compressed_from_bytes' \
|
|
--opaque 'curve25519_dalek' \
|
|
--opaque 'sha2' --opaque 'digest' --opaque 'ed25519' \
|
|
--opaque 'signature' --opaque 'subtle' --opaque 'zeroize' \
|
|
--exclude 'hybrid_array' --exclude 'typenum' \
|
|
--hide-marker-traits \
|
|
--dest-file "$HERE/CurveSig.llbc"
|
|
|
|
echo "[4/4] aeneas: LLBC -> Lean (CurveSig.* modules; hand-maintained"
|
|
echo " TypesExternal.lean / FunsExternal.lean are NOT overwritten)"
|
|
cd "$HERE"
|
|
aeneas -backend lean -split-files -subdir CurveSig -dest gen CurveSig.llbc
|
|
|
|
echo "Done. Now run ./check.sh to type-check the regenerated model."
|