diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-18 18:11:24 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-18 18:11:46 -0400 |
| commit | 6e3e29e86345ad447e8d493796956a9a3cd684bf (patch) | |
| tree | 6a237f26fd5c3f72470522c0102e0e6e1c967cb4 /src/Experiments | |
| parent | aad7ad2084db3c8401bb9c9e783dfe3c0cf511ac (diff) | |
Work around out of memory error in 8.5, 8.5pl1
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/Ed25519.v | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 2afba20e0..2193958a3 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -286,20 +286,22 @@ Check @sign_correct Definition Fsqrt_minus1 := Eval vm_compute in ModularBaseSystem.decode (GF25519.sqrt_m1). Definition Fsqrt := PrimeFieldTheorems.F.sqrt_5mod8 Fsqrt_minus1. -Lemma bound_check255 : BinInt.Z.to_nat GF25519.modulus < 2^255. +Lemma bound_check_255_helper x y : (0 <= x)%Z -> BinInt.Z.to_nat x < 2^y <-> (x < 2^(Z.of_nat y))%Z. Proof. - cbv [GF25519.modulus]. + intros. rewrite <-(Znat.Nat2Z.id 2) at 1. rewrite ZUtil.Z.pow_Z2N_Zpow by omega. - apply Znat.Z2Nat.inj_lt; cbv; congruence. + rewrite <- Znat.Z2Nat.inj_lt by auto with zarith. + reflexivity. +Qed. +Lemma bound_check255 : BinInt.Z.to_nat GF25519.modulus < 2^255. +Proof. + apply bound_check_255_helper; vm_compute; intuition congruence. Qed. Lemma bound_check256 : BinInt.Z.to_nat GF25519.modulus < 2^256. Proof. - cbv [GF25519.modulus]. - rewrite <-(Znat.Nat2Z.id 2) at 1. - rewrite ZUtil.Z.pow_Z2N_Zpow by omega. - apply Znat.Z2Nat.inj_lt; cbv; congruence. + apply bound_check_255_helper; vm_compute; intuition congruence. Qed. Let Edec := (@PointEncodingPre.point_dec |