diff options
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemList.v | 15 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListProofs.v | 25 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemListZOperations.v | 12 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 1 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 2 |
6 files changed, 32 insertions, 24 deletions
diff --git a/_CoqProject b/_CoqProject index e347697f2..a5ded72c0 100644 --- a/_CoqProject +++ b/_CoqProject @@ -73,6 +73,7 @@ src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemList.v src/ModularArithmetic/ModularBaseSystemListProofs.v +src/ModularArithmetic/ModularBaseSystemListZOperations.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v src/ModularArithmetic/Pow2Base.v diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v index 847df592b..8cce5481c 100644 --- a/src/ModularArithmetic/ModularBaseSystemList.v +++ b/src/ModularArithmetic/ModularBaseSystemList.v @@ -7,6 +7,7 @@ Require Import Crypto.BaseSystem. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. @@ -52,9 +53,6 @@ Section Defs. Definition modulus_digits := encodeZ limb_widths modulus. - Definition cmovl (x y r1 r2 : Z) := if Z.leb x y then r1 else r2. - Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2. - (* Constant-time comparison with modulus; only works if all digits of [us] are less than 2 ^ their respective limb width. *) Fixpoint ge_modulus' {A} (f : Z -> A) us (result : Z) i := @@ -68,11 +66,6 @@ Section Defs. Definition ge_modulus us := ge_modulus' id us 1 (length limb_widths - 1)%nat. - (* analagous to NEG assembly instruction on an integer that is 0 or 1: - neg 1 = 2^64 - 1 (on 64-bit; 2^32-1 on 32-bit, etc.) - neg 0 = 0 *) - Definition neg (int_width : Z) (b : Z) := if b =? 1 then Z.ones int_width else 0. - Definition conditional_subtract_modulus int_width (us : digits) (cond : Z) := (* [and_term] is all ones if us' is full, so the subtractions subtract q overall. Otherwise, it's all zeroes, and the subtractions do nothing. *) @@ -85,7 +78,7 @@ Section Defs. Context {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) (bits_eq : sum_firstn limb_widths (length limb_widths) = sum_firstn target_widths (length target_widths)). - + Definition pack := @convert limb_widths limb_widths_nonneg target_widths target_widths_nonneg (Z.eq_le_incl _ _ bits_eq). @@ -93,5 +86,5 @@ Section Defs. Definition unpack := @convert target_widths target_widths_nonneg limb_widths limb_widths_nonneg (Z.eq_le_incl _ _ (Z.eq_sym bits_eq)). - -End Defs.
\ No newline at end of file + +End Defs. diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v index 3a6ffbeac..9cb65bd19 100644 --- a/src/ModularArithmetic/ModularBaseSystemListProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v @@ -16,6 +16,7 @@ Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Notations. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.ModularArithmetic.ModularBaseSystemList. Local Open Scope Z_scope. @@ -189,7 +190,7 @@ Section ModulusDigitsProofs. | |- _ => unique pose proof modulus_pos | |- _ => unique assert (modulus = 2 ^ k - c) by (cbv [c]; ring) | |- _ => break_if - | |- _ => rewrite decode_modulus_digits + | |- _ => rewrite decode_modulus_digits | |- _ => rewrite Z.testbit_pow2_mod by eauto using nth_default_limb_widths_nonneg | |- _ => rewrite Z.ones_spec by eauto using nth_default_limb_widths_nonneg @@ -204,7 +205,7 @@ Section ModulusDigitsProofs. | |- Z.testbit modulus ?i = true => transitivity (Z.testbit (2 ^ k - c) i) | |- _ => congruence end. - + replace (c - 1) with ((c - 1) mod 2 ^ nth_default 0 limb_widths 0) by (apply Z.mod_small; omega). rewrite Z.mod_pow2_bits_high; auto. pose proof (sum_firstn_prefix_le limb_widths 1 i). @@ -244,7 +245,7 @@ Section ModulusComparisonProofs. (* Lexicographically compare two vectors of equal length, starting from the END of the list (in our context, this is the most significant end). NOT constant time. *) Definition compare us vs := compare' us vs (length us). - + Lemma decode_firstn_compare' : forall us vs i, (i <= length limb_widths)%nat -> length us = length limb_widths -> bounded limb_widths us -> @@ -258,8 +259,8 @@ Section ModulusComparisonProofs. | |- _ => progress (simpl compare') | |- _ => progress specialize_by (assumption || omega) | |- _ => rewrite sum_firstn_0 - | |- _ => rewrite set_higher - | |- _ => rewrite nth_default_base by eauto + | |- _ => rewrite set_higher + | |- _ => rewrite nth_default_base by eauto | |- _ => rewrite firstn_length, Min.min_l by omega | |- _ => rewrite firstn_O | |- _ => rewrite firstn_succ with (d := 0) by omega @@ -270,7 +271,7 @@ Section ModulusComparisonProofs. (rewrite (Z.mul_comm (2 ^ x)); apply Z.shiftl_mul_pow2; eauto) | |- _ => tauto | |- _ => split - | |- _ => break_if + | |- _ => break_if end. Qed. @@ -321,7 +322,7 @@ Section ModulusComparisonProofs. | |- _ =>erewrite (ge_modulus'_0 (@id Z)) in * | H : (?x <= 0)%nat |- _ => progress replace x with 0%nat in * by omega | |- _ => break_if - | |- _ => discriminate + | |- _ => discriminate | |- _ => solve [rewrite ?Z.leb_le, ?Z.eqb_eq in *; omega] end. destruct (le_dec j i). @@ -440,7 +441,7 @@ Section ConditionalSubtractModulusProofs. Proof. induction us; boring. Qed. - + Hint Rewrite @length_modulus_digits @length_zeros : distr_length. Lemma conditional_subtract_modulus_spec : forall u cond (cond_01 : cond = 0 \/ cond = 1), @@ -456,10 +457,10 @@ Section ConditionalSubtractModulusProofs. | |- _ => rewrite map_land_zero | |- _ => rewrite map2_sub_eq by distr_length | |- _ => rewrite sub_rep by auto - | |- _ => rewrite zeros_rep + | |- _ => rewrite zeros_rep | |- _ => rewrite decode_modulus_digits by auto | |- _ => f_equal; ring - | |- _ => discriminate + | |- _ => discriminate end. Qed. @@ -475,7 +476,7 @@ Section ConditionalSubtractModulusProofs. | |- _ => rewrite map_land_zero | |- _ => rewrite length_modulus_digits in * | |- _ => rewrite length_zeros in * - | |- _ => rewrite Min.min_l in * by omega + | |- _ => rewrite Min.min_l in * by omega | |- _ => rewrite nth_default_zeros | |- _ => rewrite nth_default_map2 with (d1 := 0) (d2 := 0) | |- _ => break_if @@ -540,4 +541,4 @@ Section ConditionalSubtractModulusProofs. + pose proof (bounded_mul2_modulus u); specialize_by auto. omega. Qed. -End ConditionalSubtractModulusProofs.
\ No newline at end of file +End ConditionalSubtractModulusProofs. diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v new file mode 100644 index 000000000..1d863abbd --- /dev/null +++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v @@ -0,0 +1,12 @@ +(** * Definitions of some basic operations on ℤ used in ModularBaseSystemList *) +(** We separate these out so that we can depend on them in other files + without waiting for ModularBaseSystemList to build. *) +Require Import Coq.ZArith.ZArith. + +Definition cmovl (x y r1 r2 : Z) := if Z.leb x y then r1 else r2. +Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2. + +(* analagous to NEG assembly instruction on an integer that is 0 or 1: + neg 1 = 2^64 - 1 (on 64-bit; 2^32-1 on 32-bit, etc.) + neg 0 = 0 *) +Definition neg (int_width : Z) (b : Z) := if Z.eqb b 1 then Z.ones int_width else 0%Z. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index d2c73b57a..f7f6efad7 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -6,6 +6,7 @@ Require Import Crypto.ModularArithmetic.Conversion. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.ModularArithmetic.ModularBaseSystemList. Require Import Crypto.ModularArithmetic.ModularBaseSystemListProofs. Require Import Crypto.ModularArithmetic.ModularBaseSystem. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index fc207c7e0..5000cec83 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -129,7 +129,7 @@ Definition zero_subst : zero = zero_ := eq_refl zero_. Definition modulus_digits_ := Eval compute in ModularBaseSystemList.modulus_digits. Definition modulus_digits_subst : ModularBaseSystemList.modulus_digits = modulus_digits_ := eq_refl modulus_digits_. -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemList.neg ModularBaseSystemList.cmovl ModularBaseSystemList.cmovne. +Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemListZOperations.neg ModularBaseSystemListZOperations.cmovl ModularBaseSystemListZOperations.cmovne. Definition app_7 {T} (f : wire_digits) (P : wire_digits -> T) : T. Proof. |