diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-12 13:43:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-12 13:43:24 -0400 |
| commit | 24363e3c6e317514858205119f77e7849d7cfb94 (patch) | |
| tree | c77ee3b38ecc32a0161a3330056483edb30222e5 /src | |
| parent | 040cffe6c076ff3c20d9bbb7a577fbd4be8e3e16 (diff) | |
Add Ed25519 to _CoqProject
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/Ed25519.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index c09ee445e..8b75b4502 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -70,7 +70,7 @@ Proof. reflexivity. Defined. -Definition extended_to_coord (P : Erep) : (GF25519.fe25519 * GF25519.fe25519) := +Fail Definition extended_to_coord (P : Erep) : (GF25519.fe25519 * GF25519.fe25519) := CompleteEdwardsCurve.E.coordinates (ExtendedCoordinates.Extended.to_twisted P). Lemma encode_eq_iff : forall x y : ModularArithmetic.F.F GF25519.modulus, @@ -96,7 +96,7 @@ Let EToRep := PointEncoding.point_phi Let ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x). -Definition feEnc (x : GF25519.fe25519) : Word.word 255 := +Definition feEnc (x : GF25519.fe25519) : Word.word 255 := let '(x0, x1, x2, x3, x4, x5, x6, x7) := (GF25519.pack x) in Word.combine (ZNWord 32 x0) @@ -105,12 +105,12 @@ Definition feEnc (x : GF25519.fe25519) : Word.word 255 := (Word.combine (ZNWord 32 x3) (Word.combine (ZNWord 32 x4) (Word.combine (ZNWord 32 x5) - (Word.combine (ZNWord 32 x6) (ZNWord 31 x7))))))). + (Word.combine (ZNWord 32 x6) (ZNWord 31 x7))))))). -Let ERepEnc := +Fail Let ERepEnc := (PointEncoding.Kencode_point (Ksign := feSign) - (Kenc := feEnc) + (Kenc := feEnc) (Kpoint := Erep) (Kpoint_to_coord := fun P => CompleteEdwardsCurve.E.coordinates (ExtendedCoordinates.Extended.to_twisted P)) @@ -122,11 +122,11 @@ Let S2Rep := fun (x : ModularArithmetic.F.F l) => (Pow2Base.encodeZ (List.repeat (BinInt.Z.of_nat 32) 8) (ModularArithmetic.F.to_Z x))). - -Check @sign_correct + +Fail Check @sign_correct (* E := *) E (* Eeq := *) CompleteEdwardsCurveTheorems.E.eq (* Eadd := *) CompleteEdwardsCurve.E.add @@ -183,4 +183,4 @@ Check @sign_correct . -Check verify_correct.
\ No newline at end of file +Check verify_correct. |