Transpile the Scalar52 limb backend (backend::serial::u64::scalar
add/sub/mul/square/montgomery_*) from Rust to Lean via Charon/Aeneas,
scoped at the function level to the iterator-free arithmetic core.
- verification/extract-scalar.sh: function-level Charon/Aeneas extraction
- verification/gen/CurveScalar/{Types,Funs}.lean: transpiled model (27 defs).
This fork (v4.1.2) implements Scalar52::sub's constant-time conditional add
with a pure arithmetic mask (constants::L[i] & underflow_mask), so the
extraction pulls in NO external functions or types (unlike v5 dalek, which
routes sub through subtle, and v4.1.3, which uses a local black_box).
- verification/gen/CurveScalar/{TypesExternal,FunsExternal}.lean: decl-free
stub modules kept so the check manifest is uniform across forks.
- verification/Proofs/ScalarDenote.lean: semantic foundation — Scalar52
denotation into ℤ/ℓℤ, limb-bound invariant, and L_val (the transpiled
constants::L denotes exactly the group order ℓ, kernel-checked).
- verification/check-scalar.sh: guarded compile of the gen modules plus the
denotation foundation.
check-scalar.sh passes: gen compiles; denotation + L = ℓ proven.
add/sub/mul remain in progress.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Extraction widened to backend::serial::curve_models + edwards (v4 Aeneas).
Ed* proof suite shared with the risc0 twin EXCEPT proj_double_spec: upstream
reordered ProjectivePoint::double's instructions between v4.1.2 (this fork)
and v4.1.3 (risc0), so the step sequence was resequenced to match THIS
fork's generated body — the proofs track each fork's actual code, not a
template. All 20 proofs pass under lean-guard; both certificates axiom-clean.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Ported from the locally verified Hermes working copy; FeQ and Square2Spec
(dead files in the published replica) now compile and are in the check
manifest. Basic.lean (never compiled under v4 Aeneas) removed rather than
shipped dead.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
