mrwulf 50b1e2e8ee Merge scalar into CurveField: one type universe, serial-only backend ... Replicates dalek's gen merge: extract.sh co-extracts the Scalar52 backend and scalar::from_bytes_mod_order[_wide] into the CurveField model (with this fork's sub::black_box opaqued, its identity model ported to the merged FunsExternal), pins RUSTFLAGS --cfg curve25519_dalek_backend="serial" so the SIMD dispatch arm compiles out (get_selected_backend becomes a real definition), and upgrades unwrap_u8 to the documented Choice-model definition. ScalarDenote repoints by one import line; both buttons green over the merged gen (scalar chain + field/group/dsm chain, all certificates axiom-clean). Prepares the verify-glue integration (CurveSig) on this fork. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>		2026-07-04 21:58:33 +02:00
..
Funs.lean	Merge scalar into CurveField: one type universe, serial-only backend	2026-07-04 21:58:33 +02:00
FunsExternal.lean	Merge scalar into CurveField: one type universe, serial-only backend	2026-07-04 21:58:33 +02:00
FunsExternal_Template.lean	Merge scalar into CurveField: one type universe, serial-only backend	2026-07-04 21:58:33 +02:00
Types.lean	Merge scalar into CurveField: one type universe, serial-only backend	2026-07-04 21:58:33 +02:00
TypesExternal.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:52 +02:00
TypesExternal_Template.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:52 +02:00