diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-11-02 12:48:02 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-11-02 15:48:09 -0400 |
| commit | 7f20cf022c139dac1379dd249dd9b42998d6aced (patch) | |
| tree | ec326b091999ad3a097c552a8eb0a1be9ba40153 /src/Experiments | |
| parent | 2fc3ff8afe6396c2866874980e3721dda2505839 (diff) | |
improve some fragile proofs (built on 8.4)
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 8b6e709a5..0fa27be66 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -598,8 +598,8 @@ Proof. rewrite Tuple.to_list_from_list. apply Conversion.convert_bounded. } { destruct w; - repeat match goal with p : _ * Z |- _ => destruct p end. - simpl Tuple.to_list in *. + repeat match goal with p : (_ * Z)%type |- _ => destruct p end. + cbv [Tuple.to_list Tuple.to_list'] in *. rewrite Pow2BaseProofs.bounded_iff in *. (* TODO : Is there a better way to do this? *) pose proof (H0 0). @@ -611,7 +611,7 @@ Proof. pose proof (H0 6). pose proof (H0 7). clear H0. - cbv [GF25519.wire_widths nth_default nth_error] in *. + cbv [GF25519.wire_widths nth_default nth_error value] in *. repeat rewrite combine_ZNWord by (rewrite ?Znat.Nat2Z.inj_add; simpl Z.of_nat; repeat apply lor_shiftl_bounds; omega). cbv - [ZNWord Z.lor Z.shiftl]. rewrite Z.shiftl_0_l. @@ -626,12 +626,12 @@ Lemma initial_bounds : forall x n, (Tuple.to_list (length PseudoMersenneBaseParams.limb_widths) (GF25519BoundedCommon.proj1_fe25519 x)) n < 2 ^ GF25519.int_width - - (if PeanoNat.Nat.eq_dec n 0 + (if Decidable.dec (n=0)%nat then 0 else Z.shiftr (2 ^ GF25519.int_width) (nth_default 0 PseudoMersenneBaseParams.limb_widths - (Init.Nat.pred n))))%Z. + (pred n))))%Z. Proof. intros. cbv [GF25519BoundedCommon.fe25519] in *. |