| .. |
|
AddSpec.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
Basic.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
ConstSpecs.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
Denote.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
EdAddAffNiels.lean
|
group-law layer: complete twisted Edwards addition law proven
|
2026-07-02 14:50:42 +02:00 |
|
EdAddProjNiels.lean
|
group-law layer: complete twisted Edwards addition law proven
|
2026-07-02 14:50:42 +02:00 |
|
EdConvert.lean
|
group-law layer: complete twisted Edwards addition law proven
|
2026-07-02 14:50:42 +02:00 |
|
EdCurve.lean
|
group-law layer: complete twisted Edwards addition law proven
|
2026-07-02 14:50:42 +02:00 |
|
EdDenote.lean
|
group-law layer: complete twisted Edwards addition law proven
|
2026-07-02 14:50:42 +02:00 |
|
EdDouble.lean
|
group-law layer: complete twisted Edwards addition law proven
|
2026-07-02 14:50:42 +02:00 |
|
EdMain.lean
|
group-law layer: complete twisted Edwards addition law proven
|
2026-07-02 14:50:42 +02:00 |
|
FeQ.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
Field.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
FieldMain.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
InvertSpec.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
MulSpec.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
P25519.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
ReduceSpec.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
ScalarAddSpec.lean
|
Signature layer, first bricks: canonicity closure + hash-to-scalar foundation
|
2026-07-03 23:18:29 +02:00 |
|
ScalarBytesSpec.lean
|
Signature layer: the 64-byte unpack certificates (8x8 loops proven)
|
2026-07-04 03:00:42 +02:00 |
|
ScalarDenote.lean
|
scalar layer: clean Scalar52 extraction + denotation foundation
|
2026-07-02 21:13:43 +02:00 |
|
ScalarFullMulSpec.lean
|
Signature layer, first bricks: canonicity closure + hash-to-scalar foundation
|
2026-07-03 23:18:29 +02:00 |
|
ScalarLoop.lean
|
scalar: generic loop-combinator lemmas (loop_step, range_next_lt/ge_spec)
|
2026-07-02 21:47:47 +02:00 |
|
ScalarMain.lean
|
Signature layer, first bricks: canonicity closure + hash-to-scalar foundation
|
2026-07-03 23:18:29 +02:00 |
|
ScalarMontSpec.lean
|
Signature layer, first bricks: canonicity closure + hash-to-scalar foundation
|
2026-07-03 23:18:29 +02:00 |
|
ScalarMulSpec.lean
|
scalar layer: mul_internal proven — Montgomery frontier phase A down
|
2026-07-03 18:56:04 +02:00 |
|
ScalarReduceSpec.lean
|
Signature layer, first bricks: canonicity closure + hash-to-scalar foundation
|
2026-07-03 23:18:29 +02:00 |
|
ScalarSubSpec.lean
|
Signature layer, first bricks: canonicity closure + hash-to-scalar foundation
|
2026-07-03 23:18:29 +02:00 |
|
ScalarUnpackSpec.lean
|
Signature layer: the 64-byte unpack certificates (8x8 loops proven)
|
2026-07-04 03:00:42 +02:00 |
|
ScalarWideSpec.lean
|
Signature layer, first bricks: canonicity closure + hash-to-scalar foundation
|
2026-07-03 23:18:29 +02:00 |
|
Square2Spec.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
SquareSpec.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
|
SubNegSpec.lean
|
field layer: 14 proofs pass, fieldImplementation axiom-clean
|
2026-07-02 14:17:44 +02:00 |
