diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-12 22:50:29 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-12 22:50:29 -0500 |
| commit | c85f7283994da084a837b88d612a6b937ff2fbd5 (patch) | |
| tree | b460eff65681e122fab15feabffa6fcd5e48606c /src/Specific | |
| parent | 06a7e0e095cba1b1e70691e6db0aab64040dac5b (diff) | |
| parent | 6c993ee91855ee8c19c292cd164ab24a7c1012f8 (diff) | |
Merge branch 'spec' of github.mit.edu:plv/fiat-crypto
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/EdDSA25519.v | 3 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 1 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v index 6ae501a28..d037339b4 100644 --- a/src/Specific/EdDSA25519.v +++ b/src/Specific/EdDSA25519.v @@ -594,7 +594,8 @@ Module EdDSA25519_Params <: EdDSAParams. I have so far not managed to unify them. *) Lemma point_eq_copy : forall x1 x2 y1 y2, x1 = x2 -> y1 = y2 -> forall p1 p2, mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2. - Admitted. + apply Facts.point_eq. + Qed. Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p. Proof. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 732779a1a..7ef2f0aaf 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -289,7 +289,6 @@ Proof. cbv [cap Base25Point5_10limbs.base]. intros. rewrite map_length in *. - About map_nth_default. erewrite map_nth_default; [|assumption]. instantiate (2 := 0%Z). (** For the division of maps of (2 ^ _) over lists, replace it with 2 ^ (_ - _) *) |