mrwulf 090410c54b PHASE-2 HALF-LIFT on the betrusted fork: verify_accepts_iff_point, button-enforced ... Verbatim port of the risc0 fork's phase-2 files (identical v4 shape: as_bytes serializers, inlined affine conversion, single sha512_hash3 oracle bind) - every proof compiled unchanged. verify_accepts_iff_point: accept IFF the signature's R bytes are the canonical encoding of the recomputed [k](-A) + [s]B over the certified model. Five new standard certificates; Phase 3b enforces the hash3 + wire-format boundary on both apex and half-lift. Full button green fresh. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>		2026-07-05 16:57:57 +02:00
..
AddSpec.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
CompressSpec.lean	PHASE-2 HALF-LIFT on the betrusted fork: verify_accepts_iff_point, button-enforced	2026-07-05 16:57:57 +02:00
ConstSpecs.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
Denote.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
DsmLoopSpec.lean	Double-scalar-mul proof campaign, bricks 1-3: table, digit step, loop	2026-07-04 15:07:59 +02:00
DsmMulSpec.lean	NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex	2026-07-04 16:52:10 +02:00
DsmNafLoadSpec.lean	NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex	2026-07-04 16:52:10 +02:00
DsmNafLoopSpec.lean	NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex	2026-07-04 16:52:10 +02:00
DsmNafMath.lean	NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex	2026-07-04 16:52:10 +02:00
DsmNafSpec.lean	NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex	2026-07-04 16:52:10 +02:00
DsmStepSpec.lean	Double-scalar-mul proof campaign, bricks 1-3: table, digit step, loop	2026-07-04 15:07:59 +02:00
DsmTableSpec.lean	Double-scalar-mul proof campaign, bricks 1-3: table, digit step, loop	2026-07-04 15:07:59 +02:00
EdAddAffNiels.lean	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
EdAddProjNiels.lean	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
EdConvert.lean	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
EdCurve.lean	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
EdDenote.lean	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
EdDouble.lean	group-law layer: complete twisted Edwards addition law proven	2026-07-02 17:11:28 +02:00
EdMain.lean	lean-guard: disable core dumps (no more apport popups on capped aborts)	2026-07-02 16:23:31 +02:00
FeQ.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
Field.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
FieldMain.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
InvertSpec.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
MulSpec.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
P25519.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
PointLiftSpec.lean	PHASE-2 HALF-LIFT on the betrusted fork: verify_accepts_iff_point, button-enforced	2026-07-05 16:57:57 +02:00
ReduceSpec.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
ScalarAddSpec.lean	Signature layer, first bricks: canonicity closure + hash-to-scalar foundation	2026-07-03 23:18:34 +02:00
ScalarBytesSpec.lean	Hash-to-scalar PROVEN: from_bytes_wide_spec - Scalar::from_hash's reduction is exact mod l	2026-07-04 11:00:52 +02:00
ScalarDenote.lean	Merge scalar into CurveField: one type universe, serial-only backend	2026-07-04 22:20:26 +02:00
ScalarFromBytesSpec.lean	Hash-to-scalar PROVEN: from_bytes_wide_spec - Scalar::from_hash's reduction is exact mod l	2026-07-04 11:00:52 +02:00
ScalarFullMulSpec.lean	Signature layer, first bricks: canonicity closure + hash-to-scalar foundation	2026-07-03 23:18:34 +02:00
ScalarLoop.lean	scalar layer: add+sub fully proven mod l against THIS fork's v4 extraction	2026-07-03 18:45:17 +02:00
ScalarMain.lean	Signature layer, first bricks: canonicity closure + hash-to-scalar foundation	2026-07-03 23:18:34 +02:00
ScalarMontSpec.lean	Signature layer, first bricks: canonicity closure + hash-to-scalar foundation	2026-07-03 23:18:34 +02:00
ScalarMulSpec.lean	Scalar layer complete: Montgomery reduction + full mul ported, scalarImplementation aggregate	2026-07-03 21:46:57 +02:00
ScalarPackSpec.lean	PHASE-2 HALF-LIFT on the betrusted fork: verify_accepts_iff_point, button-enforced	2026-07-05 16:57:57 +02:00
ScalarReduceSpec.lean	Signature layer, first bricks: canonicity closure + hash-to-scalar foundation	2026-07-03 23:18:34 +02:00
ScalarSubSpec.lean	Signature layer, first bricks: canonicity closure + hash-to-scalar foundation	2026-07-03 23:18:34 +02:00
ScalarUnpackSpec.lean	Hash-to-scalar PROVEN: from_bytes_wide_spec - Scalar::from_hash's reduction is exact mod l	2026-07-04 11:00:52 +02:00
ScalarWideSpec.lean	Signature layer, first bricks: canonicity closure + hash-to-scalar foundation	2026-07-03 23:18:34 +02:00
SigApexSpec.lean	THE SIGNATURE APEX on the betrusted fork: verify_accepts_iff, button-enforced	2026-07-04 22:49:19 +02:00
Square2Spec.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
SquareSpec.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
SubNegSpec.lean	field layer: proofs pass, fieldImplementation axiom-clean	2026-07-02 14:38:53 +02:00
ToBytesMath.lean	PHASE-2 HALF-LIFT on the betrusted fork: verify_accepts_iff_point, button-enforced	2026-07-05 16:57:57 +02:00
ToBytesSpec.lean	PHASE-2 HALF-LIFT on the betrusted fork: verify_accepts_iff_point, button-enforced	2026-07-05 16:57:57 +02:00