3 commits

Author	SHA1	Message	Date
mrwulf	8e52a449dc	Double-scalar-mul enters the verified model: vartime_double_base extracted transparently ... extract.sh now opens crate::backend::serial::scalar_mul::vartime_double_base (the other scalar_mul strategies stay opaque): non_adjacent_form (with its loops), NafLookupTable5 (from/select), the curve-model helpers and vartime_double_base::mul itself land in gen/CurveField - the same namespace as the proven edwards operations, so the coming double-and-add induction can consume EdDouble/EdAddProjNiels/EdConvert directly. Zero sorries, zero external axioms (the pinned sources carry documented compat refactors: single-assignment loop helpers, param-rooted while, always-256-iterations, index-based LE load). Full check.sh pressed fresh over the regenerated model: every existing field and group-law certificate still green and axiom-clean - the scope extension is purely additive.	2026-07-04 11:48:51 +02:00
mrwulf	8ce599c4aa	group-law layer: complete twisted Edwards addition law proven ... Extraction widened to backend::serial::curve_models + edwards (own gen/, 209 defs). Adapted the reference Ed* proof suite: namespace rename + Curve25519TraitsIdentity -> Curve25519_dalekTraitsIdentity. New opaque externals (scalar_mul backends, get_selected_backend, decompress, sum, from_slice) are axioms outside both certificate cones — verified by the Phase-3 audit. All 21 proofs compile; field certificates unchanged. Not claimed (matching the reference solution's honest scope): edAdd associativity, scalar multiplication, decompress/compress, AVX2 backend. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-07-02 14:50:42 +02:00
mrwulf	b79375600f	field layer: 14 proofs pass, fieldImplementation axiom-clean ... 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. check.sh gates: source integrity, stub audit, zero axiom declarations under Proofs/, per-certificate axiom audit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-07-02 14:17:44 +02:00