diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-02 19:39:26 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-02 19:39:26 -0400 |
| commit | 768714f7d959e3bc1d1288662f18c6548de05752 (patch) | |
| tree | ee254adb6ccf18b8d7e078826147df52ba7aa47a /src/Experiments | |
| parent | e12319df9a4974f661319e6c70bb33a7d2eb25bc (diff) | |
Fix broken proof
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 8a4612fcd..38b15cf57 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -844,7 +844,7 @@ Let ERepB : Erep. exists (eta4 ERepB_value). cbv [GF25519BoundedCommon.eq ModularBaseSystem.eq Pre.onCurve]. vm_decide_no_check. -Qed. +Defined. Lemma ERepB_value_correct : ERepB_value = proj1_sig (EToRep B). Proof. vm_cast_no_check (eq_refl ERepB_value). Qed. @@ -852,9 +852,8 @@ Proof. vm_cast_no_check (eq_refl ERepB_value). Qed. Let ERepB_correct : ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519) ERepB (EToRep B). pose proof ERepB_value_correct; destruct (EToRep B). cbv [proj1_sig] in *; subst. - (*vm_decide. -Qed.*) -Admitted. + vm_decide. +Qed. Lemma B_order_l : CompleteEdwardsCurveTheorems.E.eq (CompleteEdwardsCurve.E.mul (Z.to_nat l) B) |