From cdd5ffb086eb647eabe640c81de9d8af7cd0a1dd Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 17 Jan 2019 15:07:47 -0500 Subject: Split up PushButtonSynthesis.v Closes #497 --- _CoqProject | 15 +- src/Arithmetic.v | 589 ++++ src/CLI.v | 4 +- src/Fancy/Barrett256.v | 8 +- src/Fancy/Montgomery256.v | 7 +- src/PushButtonSynthesis.v | 3196 -------------------- src/PushButtonSynthesis/BarrettReduction.v | 133 + .../BarrettReductionReificationCache.v | 30 + src/PushButtonSynthesis/InvertHighLow.v | 39 + src/PushButtonSynthesis/LegacySynthesisTactics.v | 112 + src/PushButtonSynthesis/MontgomeryReduction.v | 124 + .../MontgomeryReductionReificationCache.v | 23 + src/PushButtonSynthesis/Primitives.v | 383 +++ src/PushButtonSynthesis/ReificationCache.v | 11 +- src/PushButtonSynthesis/SaturatedSolinas.v | 184 ++ .../SaturatedSolinasReificationCache.v | 28 + src/PushButtonSynthesis/SmallExamples.v | 95 + src/PushButtonSynthesis/UnsaturatedSolinas.v | 602 ++++ .../UnsaturatedSolinasReificationCache.v | 168 + src/PushButtonSynthesis/WordByWordMontgomery.v | 762 +++++ .../WordByWordMontgomeryReificationCache.v | 247 ++ src/SlowPrimeSynthesisExamples.v | 2 +- src/StandaloneHaskellMain.v | 1 - src/StandaloneOCamlMain.v | 1 - 24 files changed, 3552 insertions(+), 3212 deletions(-) delete mode 100644 src/PushButtonSynthesis.v create mode 100644 src/PushButtonSynthesis/BarrettReduction.v create mode 100644 src/PushButtonSynthesis/BarrettReductionReificationCache.v create mode 100644 src/PushButtonSynthesis/InvertHighLow.v create mode 100644 src/PushButtonSynthesis/LegacySynthesisTactics.v create mode 100644 src/PushButtonSynthesis/MontgomeryReduction.v create mode 100644 src/PushButtonSynthesis/MontgomeryReductionReificationCache.v create mode 100644 src/PushButtonSynthesis/Primitives.v create mode 100644 src/PushButtonSynthesis/SaturatedSolinas.v create mode 100644 src/PushButtonSynthesis/SaturatedSolinasReificationCache.v create mode 100644 src/PushButtonSynthesis/SmallExamples.v create mode 100644 src/PushButtonSynthesis/UnsaturatedSolinas.v create mode 100644 src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v create mode 100644 src/PushButtonSynthesis/WordByWordMontgomery.v create mode 100644 src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v diff --git a/_CoqProject b/_CoqProject index 80ff80d44..23bccf874 100644 --- a/_CoqProject +++ b/_CoqProject @@ -34,7 +34,6 @@ src/LanguageInversion.v src/LanguageWf.v src/MiscCompilerPasses.v src/MiscCompilerPassesProofs.v -src/PushButtonSynthesis.v src/Rewriter.v src/RewriterInterpProofs1.v src/RewriterProofs.v @@ -92,7 +91,21 @@ src/Fancy/Prod.v src/Fancy/Spec.v src/Primitives/EdDSARepChange.v src/Primitives/MxDHRepChange.v +src/PushButtonSynthesis/BarrettReduction.v +src/PushButtonSynthesis/BarrettReductionReificationCache.v +src/PushButtonSynthesis/InvertHighLow.v +src/PushButtonSynthesis/LegacySynthesisTactics.v +src/PushButtonSynthesis/MontgomeryReduction.v +src/PushButtonSynthesis/MontgomeryReductionReificationCache.v +src/PushButtonSynthesis/Primitives.v src/PushButtonSynthesis/ReificationCache.v +src/PushButtonSynthesis/SaturatedSolinas.v +src/PushButtonSynthesis/SaturatedSolinasReificationCache.v +src/PushButtonSynthesis/SmallExamples.v +src/PushButtonSynthesis/UnsaturatedSolinas.v +src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v +src/PushButtonSynthesis/WordByWordMontgomery.v +src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v src/Spec/CompleteEdwardsCurve.v src/Spec/Ed25519.v src/Spec/EdDSA.v diff --git a/src/Arithmetic.v b/src/Arithmetic.v index 5af73875b..4436bdf0e 100644 --- a/src/Arithmetic.v +++ b/src/Arithmetic.v @@ -4,6 +4,8 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. Require Import Coq.Sorting.Permutation. Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) +Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. @@ -4775,3 +4777,590 @@ Module WordByWordMontgomery. Proof. apply to_bytesmod_correct. Qed. End modops. End WordByWordMontgomery. + +Module BarrettReduction. + (* TODO : generalize to multi-word and operate on (list Z) instead of T; maybe stop taking ops as context variables *) + Section Generic. + Context {T} (rep : T -> Z -> Prop) + (k : Z) (k_pos : 0 < k) + (low : T -> Z) + (low_correct : forall a x, rep a x -> low a = x mod 2 ^ k) + (shiftr : T -> Z -> T) + (shiftr_correct : forall a x n, + rep a x -> + 0 <= n <= k -> + rep (shiftr a n) (x / 2 ^ n)) + (mul_high : T -> T -> Z -> T) + (mul_high_correct : forall a b x y x0y1, + rep a x -> + rep b y -> + 2 ^ k <= x < 2^(k+1) -> + 0 <= y < 2^(k+1) -> + x0y1 = x mod 2 ^ k * (y / 2 ^ k) -> + rep (mul_high a b x0y1) (x * y / 2 ^ k)) + (mul : Z -> Z -> T) + (mul_correct : forall x y, + 0 <= x < 2^k -> + 0 <= y < 2^k -> + rep (mul x y) (x * y)) + (sub : T -> T -> T) + (sub_correct : forall a b x y, + rep a x -> + rep b y -> + 0 <= x - y < 2^k * 2^k -> + rep (sub a b) (x - y)) + (cond_sub1 : T -> Z -> Z) + (cond_sub1_correct : forall a x y, + rep a x -> + 0 <= x < 2 * y -> + 0 <= y < 2 ^ k -> + cond_sub1 a y = if (x Z -> Z) + (cond_sub2_correct : forall x y, cond_sub2 x y = if (x + 0 <= x < 2 * M -> + cond_sub2 (cond_sub1 a M) M = cond_sub2 (cond_sub2 x M) M. + Proof. + intros. + erewrite !cond_sub2_correct, !cond_sub1_correct by (eassumption || omega). + break_match; Z.ltb_to_lt; try lia; discriminate. + Qed. + + Lemma r_bounds : 0 <= x - q * M < 2 * M. + Proof. + pose proof looser_bound. pose proof q_bounds. pose proof x_mod_small. + subst q mu; split. + { Z.zero_bounds. apply qn_small; omega. } + { apply r_small_strong; rewrite ?Z.pow_1_r; auto; omega. } + Qed. + + Lemma reduce_correct : reduce = x mod M. + Proof. + pose proof looser_bound. pose proof r_bounds. pose proof q_bounds. + assert (2 * M < 2^k * 2^k) by nia. + rewrite barrett_reduction_small with (k:=k) (m:=mu) (offset:=1) (b:=2) by (auto; omega). + cbv [reduce Let_In]. + erewrite low_correct by eauto. Z.rewrite_mod_small. + erewrite two_conditional_subtracts by solve_rep. + rewrite !cond_sub2_correct. + subst q; reflexivity. + Qed. + End Generic. + + Section BarrettReduction. + Context (k : Z) (k_bound : 2 <= k). + Context (M muLow : Z). + Context (M_pos : 0 < M) + (muLow_eq : muLow + 2^k = 2^(2*k) / M) + (muLow_bounds : 0 <= muLow < 2^k) + (M_bound1 : 2 ^ (k - 1) < M < 2^k) + (M_bound2: 2 * (2 ^ (2 * k) mod M) <= 2 ^ (k + 1) - (muLow + 2^k)). + + Context (n:nat) (Hn_nz: n <> 0%nat) (n_le_k : Z.of_nat n <= k). + Context (nout : nat) (Hnout : nout = 2%nat). + Let w := weight k 1. + Local Lemma k_range : 0 < 1 <= k. Proof. omega. Qed. + Let props : @weight_properties w := wprops k 1 k_range. + + Hint Rewrite Positional.eval_nil Positional.eval_snoc : push_eval. + + Definition low (t : list Z) : Z := nth_default 0 t 0. + Definition high (t : list Z) : Z := nth_default 0 t 1. + Definition represents (t : list Z) (x : Z) := + t = [x mod 2^k; x / 2^k] /\ 0 <= x < 2^k * 2^k. + + Lemma represents_eq t x : + represents t x -> t = [x mod 2^k; x / 2^k]. + Proof. cbv [represents]; tauto. Qed. + + Lemma represents_length t x : represents t x -> length t = 2%nat. + Proof. cbv [represents]; intuition. subst t; reflexivity. Qed. + + Lemma represents_low t x : + represents t x -> low t = x mod 2^k. + Proof. cbv [represents]; intros; rewrite (represents_eq t x) by auto; reflexivity. Qed. + + Lemma represents_high t x : + represents t x -> high t = x / 2^k. + Proof. cbv [represents]; intros; rewrite (represents_eq t x) by auto; reflexivity. Qed. + + Lemma represents_low_range t x : + represents t x -> 0 <= x mod 2^k < 2^k. + Proof. auto with zarith. Qed. + + Lemma represents_high_range t x : + represents t x -> 0 <= x / 2^k < 2^k. + Proof. + destruct 1 as [? [? ?] ]; intros. + auto using Z.div_lt_upper_bound with zarith. + Qed. + Hint Resolve represents_length represents_low_range represents_high_range. + + Lemma represents_range t x : + represents t x -> 0 <= x < 2^k*2^k. + Proof. cbv [represents]; tauto. Qed. + + Lemma represents_id x : + 0 <= x < 2^k * 2^k -> + represents [x mod 2^k; x / 2^k] x. + Proof. + intros; cbv [represents]; autorewrite with cancel_pair. + Z.rewrite_mod_small; tauto. + Qed. + + Local Ltac push_rep := + repeat match goal with + | H : represents ?t ?x |- _ => unique pose proof (represents_low_range _ _ H) + | H : represents ?t ?x |- _ => unique pose proof (represents_high_range _ _ H) + | H : represents ?t ?x |- _ => rewrite (represents_low t x) in * by assumption + | H : represents ?t ?x |- _ => rewrite (represents_high t x) in * by assumption + end. + + Definition shiftr (t : list Z) (n : Z) : list Z := + [Z.rshi (2^k) (high t) (low t) n; Z.rshi (2^k) 0 (high t) n]. + + Lemma shiftr_represents a i x : + represents a x -> + 0 <= i <= k -> + represents (shiftr a i) (x / 2 ^ i). + Proof. + cbv [shiftr]; intros; push_rep. + match goal with H : _ |- _ => pose proof (represents_range _ _ H) end. + assert (0 < 2 ^ i) by auto with zarith. + assert (x < 2 ^ i * 2 ^ k * 2 ^ k) by nia. + assert (0 <= x / 2 ^ k / 2 ^ i < 2 ^ k) by + (split; Z.zero_bounds; auto using Z.div_lt_upper_bound with zarith). + repeat match goal with + | _ => rewrite Z.rshi_correct by auto with zarith + | _ => rewrite <-Z.div_mod''' by auto with zarith + | _ => progress autorewrite with zsimplify_fast + | _ => progress Z.rewrite_mod_small + | |- context [represents [(?a / ?c) mod ?b; ?a / ?b / ?c] ] => + rewrite (Z.div_div_comm a b c) by auto with zarith + | _ => solve [auto using represents_id, Z.div_lt_upper_bound with zarith lia] + end. + Qed. + + Context (Hw : forall i, w i = (2 ^ k) ^ Z.of_nat i). + Ltac change_weight := rewrite !Hw, ?Z.pow_0_r, ?Z.pow_1_r, ?Z.pow_2_r. + + Definition wideadd t1 t2 := fst (Rows.add w 2 t1 t2). + (* TODO: use this definition once issue #352 is resolved *) + (* Definition widesub t1 t2 := fst (Rows.sub w 2 t1 t2). *) + Definition widesub (t1 t2 : list Z) := + let t1_0 := hd 0 t1 in + let t1_1 := hd 0 (tl t1) in + let t2_0 := hd 0 t2 in + let t2_1 := hd 0 (tl t2) in + dlet_nd x0 := Z.sub_get_borrow_full (2^k) t1_0 t2_0 in + dlet_nd x1 := Z.sub_with_get_borrow_full (2^k) (snd x0) t1_1 t2_1 in + [fst x0; fst x1]. + Definition widemul := BaseConversion.widemul_inlined k n nout. + + Lemma partition_represents x : + 0 <= x < 2^k*2^k -> + represents (Partition.partition w 2 x) x. + Proof. + intros; cbn. change_weight. + Z.rewrite_mod_small. + autorewrite with zsimplify_fast. + auto using represents_id. + Qed. + + Lemma eval_represents t x : + represents t x -> Positional.eval w 2 t = x. + Proof. + intros; rewrite (represents_eq t x) by assumption. + cbn. change_weight; push_rep. + autorewrite with zsimplify. reflexivity. + Qed. + + Ltac wide_op partitions_pf := + repeat match goal with + | _ => rewrite partitions_pf by eauto + | _ => rewrite partitions_pf by auto with zarith + | _ => erewrite eval_represents by eauto + | _ => solve [auto using partition_represents, represents_id] + end. + + Lemma wideadd_represents t1 t2 x y : + represents t1 x -> + represents t2 y -> + 0 <= x + y < 2^k*2^k -> + represents (wideadd t1 t2) (x + y). + Proof. intros; cbv [wideadd]. wide_op Rows.add_partitions. Qed. + + Lemma widesub_represents t1 t2 x y : + represents t1 x -> + represents t2 y -> + 0 <= x - y < 2^k*2^k -> + represents (widesub t1 t2) (x - y). + Proof. + intros; cbv [widesub Let_In]. + rewrite (represents_eq t1 x) by assumption. + rewrite (represents_eq t2 y) by assumption. + cbn [hd tl]. + autorewrite with to_div_mod. + pull_Zmod. + match goal with |- represents [?m; ?d] ?x => + replace d with (x / 2 ^ k); [solve [auto using represents_id] |] end. + rewrite <-(Z.mod_small ((x - y) / 2^k) (2^k)) by (split; try apply Z.div_lt_upper_bound; Z.zero_bounds). + f_equal. + transitivity ((x mod 2^k - y mod 2^k + 2^k * (x / 2 ^ k) - 2^k * (y / 2^k)) / 2^k). { + rewrite (Z.div_mod x (2^k)) at 1 by auto using Z.pow_nonzero with omega. + rewrite (Z.div_mod y (2^k)) at 1 by auto using Z.pow_nonzero with omega. + f_equal. ring. } + autorewrite with zsimplify. + ring. + Qed. + (* Works with Rows.sub-based widesub definition + Proof. intros; cbv [widesub]. wide_op Rows.sub_partitions. Qed. + *) + + (* TODO: MOVE Equivlalent Keys decl to Arithmetic? *) + Declare Equivalent Keys BaseConversion.widemul BaseConversion.widemul_inlined. + Lemma widemul_represents x y : + 0 <= x < 2^k -> + 0 <= y < 2^k -> + represents (widemul x y) (x * y). + Proof. + intros; cbv [widemul]. + assert (0 <= x * y < 2^k*2^k) by auto with zarith. + wide_op BaseConversion.widemul_correct. + Qed. + + Definition mul_high (a b : list Z) a0b1 : list Z := + dlet_nd a0b0 := widemul (low a) (low b) in + dlet_nd ab := wideadd [high a0b0; high b] [low b; 0] in + wideadd ab [a0b1; 0]. + + Lemma mul_high_idea d a b a0 a1 b0 b1 : + d <> 0 -> + a = d * a1 + a0 -> + b = d * b1 + b0 -> + (a * b) / d = a0 * b0 / d + d * a1 * b1 + a1 * b0 + a0 * b1. + Proof. + intros. subst a b. autorewrite with push_Zmul. + ring_simplify_subterms. rewrite Z.pow_2_r. + rewrite Z.div_add_exact by (push_Zmod; autorewrite with zsimplify; omega). + repeat match goal with + | |- context [d * ?a * ?b * ?c] => + replace (d * a * b * c) with (a * b * c * d) by ring + | |- context [d * ?a * ?b] => + replace (d * a * b) with (a * b * d) by ring + end. + rewrite !Z.div_add by omega. + autorewrite with zsimplify. + rewrite (Z.mul_comm a0 b0). + ring_simplify. ring. + Qed. + + Lemma represents_trans t x y: + represents t y -> y = x -> + represents t x. + Proof. congruence. Qed. + + Lemma represents_add x y : + 0 <= x < 2 ^ k -> + 0 <= y < 2 ^ k -> + represents [x;y] (x + 2^k*y). + Proof. + intros; cbv [represents]; autorewrite with zsimplify. + repeat split; (reflexivity || nia). + Qed. + + Lemma represents_small x : + 0 <= x < 2^k -> + represents [x; 0] x. + Proof. + intros. + eapply represents_trans. + { eauto using represents_add with zarith. } + { ring. } + Qed. + + Lemma mul_high_represents a b x y a0b1 : + represents a x -> + represents b y -> + 2^k <= x < 2^(k+1) -> + 0 <= y < 2^(k+1) -> + a0b1 = x mod 2^k * (y / 2^k) -> + represents (mul_high a b a0b1) ((x * y) / 2^k). + Proof. + cbv [mul_high Let_In]; rewrite Z.pow_add_r, Z.pow_1_r by omega; intros. + assert (4 <= 2 ^ k) by (transitivity (Z.pow 2 2); auto with zarith). + assert (0 <= x * y / 2^k < 2^k*2^k) by (Z.div_mod_to_quot_rem_in_goal; nia). + + rewrite mul_high_idea with (a:=x) (b:=y) (a0 := low a) (a1 := high a) (b0 := low b) (b1 := high b) in * + by (push_rep; Z.div_mod_to_quot_rem_in_goal; lia). + + push_rep. subst a0b1. + assert (y / 2 ^ k < 2) by (apply Z.div_lt_upper_bound; omega). + replace (x / 2 ^ k) with 1 in * by (rewrite Z.div_between_1; lia). + autorewrite with zsimplify_fast in *. + + eapply represents_trans. + { repeat (apply wideadd_represents; + [ | apply represents_small; Z.div_mod_to_quot_rem_in_goal; nia| ]). + erewrite represents_high; [ | apply widemul_represents; solve [ auto with zarith ] ]. + { apply represents_add; try reflexivity; solve [auto with zarith]. } + { match goal with H : 0 <= ?x + ?y < ?z |- 0 <= ?x < ?z => + split; [ solve [Z.zero_bounds] | ]; + eapply Z.le_lt_trans with (m:= x + y); nia + end. } + { omega. } } + { ring. } + Qed. + + Definition cond_sub1 (a : list Z) y : Z := + dlet_nd maybe_y := Z.zselect (Z.cc_l (high a)) 0 y in + dlet_nd diff := Z.sub_get_borrow_full (2^k) (low a) maybe_y in + fst diff. + + Lemma cc_l_only_bit : forall x s, 0 <= x < 2 * s -> Z.cc_l (x / s) = 0 <-> x < s. + Proof. + cbv [Z.cc_l]; intros. + rewrite Z.div_between_0_if by omega. + break_match; Z.ltb_to_lt; Z.rewrite_mod_small; omega. + Qed. + + Lemma cond_sub1_correct a x y : + represents a x -> + 0 <= x < 2 * y -> + 0 <= y < 2 ^ k -> + cond_sub1 a y = if (x 0) by auto with zarith. + assert (2 < 2 ^ k) by (eapply Z.le_lt_trans with (m:=2 ^ 1); auto with zarith). + + cbv [muSelect]. rewrite <-muLow_eq. + rewrite Z.zselect_correct, Z.cc_m_eq by auto with zarith. + replace xHigh with (x / 2^k) by (subst x; autorewrite with zsimplify; lia). + autorewrite with pull_Zdiv push_Zpow. + rewrite (Z.mul_comm (2 ^ k / 2)). + break_match; [ ring | ]. + match goal with H : 0 <= ?x < 2, H' : ?x <> 0 |- _ => replace x with 1 by omega end. + autorewrite with zsimplify; reflexivity. + Qed. + + Lemma mu_rep : represents [muLow; 1] (2 ^ (2 * k) / M). + Proof. rewrite <-muLow_eq. eapply represents_trans; auto with zarith. Qed. + + Derive barrett_reduce + SuchThat (barrett_reduce = x mod M) + As barrett_reduce_correct. + Proof. + erewrite <-reduce_correct with (rep:=represents) (muSelect:=muSelect) (k0:=k) (mut:=[muLow;1]) (xt0:=xt) + by (auto using x_bounds, muSelect_correct, x_rep, mu_rep; omega). + subst barrett_reduce. reflexivity. + Qed. + End Defn. + End BarrettReduction. +End BarrettReduction. + +Module MontgomeryReduction. + Local Coercion Z.of_nat : nat >-> Z. + Section MontRed'. + Context (N R N' R' : Z). + Context (HN_range : 0 <= N < R) (HN'_range : 0 <= N' < R) (HN_nz : N <> 0) (R_gt_1 : R > 1) + (N'_good : Z.equiv_modulo R (N*N') (-1)) (R'_good: Z.equiv_modulo N (R*R') 1). + + Context (Zlog2R : Z) . + Let w : nat -> Z := weight Zlog2R 1. + Context (n:nat) (Hn_nz: n <> 0%nat) (n_good : Zlog2R mod Z.of_nat n = 0). + Context (R_big_enough : n <= Zlog2R) + (R_two_pow : 2^Zlog2R = R). + Let w_mul : nat -> Z := weight (Zlog2R / n) 1. + Context (nout : nat) (Hnout : nout = 2%nat). + + Definition montred' (lo hi : Z) := + dlet_nd y := nth_default 0 (BaseConversion.widemul_inlined Zlog2R n nout lo N') 0 in + dlet_nd t1_t2 := (BaseConversion.widemul_inlined_reverse Zlog2R n nout N y) in + dlet_nd sum_carry := Rows.add (weight Zlog2R 1) 2 [lo;hi] t1_t2 in + dlet_nd y' := Z.zselect (snd sum_carry) 0 N in + dlet_nd lo''_carry := Z.sub_get_borrow_full R (nth_default 0 (fst sum_carry) 1) y' in + Z.add_modulo (fst lo''_carry) 0 N. + + Local Lemma Hw : forall i, w i = R ^ Z.of_nat i. + Proof. + clear -R_big_enough R_two_pow; cbv [w weight]; intro. + autorewrite with zsimplify. + rewrite Z.pow_mul_r, R_two_pow by omega; reflexivity. + Qed. + + Declare Equivalent Keys weight w. + Local Ltac change_weight := rewrite !Hw, ?Z.pow_0_r, ?Z.pow_1_r, ?Z.pow_2_r, ?Z.pow_1_l in *. + Local Ltac solve_range := + repeat match goal with + | _ => progress change_weight + | |- context [?a mod ?b] => unique pose proof (Z.mod_pos_bound a b ltac:(omega)) + | |- 0 <= _ => progress Z.zero_bounds + | |- 0 <= _ * _ < _ * _ => + split; [ solve [Z.zero_bounds] | apply Z.mul_lt_mono_nonneg; omega ] + | _ => solve [auto] + | _ => omega + end. + + Local Lemma eval2 x y : Positional.eval w 2 [x;y] = x + R * y. + Proof. cbn. change_weight. ring. Qed. + + Hint Rewrite BaseConversion.widemul_inlined_reverse_correct BaseConversion.widemul_inlined_correct + using (autorewrite with widemul push_nth_default; solve [solve_range]) : widemul. + + Lemma montred'_eq lo hi T (HT_range: 0 <= T < R * N) + (Hlo: lo = T mod R) (Hhi: hi = T / R): + montred' lo hi = reduce_via_partial N R N' T. + Proof. + rewrite <-reduce_via_partial_alt_eq by nia. + cbv [montred' partial_reduce_alt reduce_via_partial_alt prereduce Let_In]. + rewrite Hlo, Hhi. + assert (0 <= (T mod R) * N' < w 2) by (solve_range). + + autorewrite with widemul. + rewrite Rows.add_partitions, Rows.add_div by (distr_length; apply wprops; omega). + rewrite R_two_pow. + cbv [Partition.partition seq]. rewrite !eval2. + autorewrite with push_nth_default push_map. + autorewrite with to_div_mod. rewrite ?Z.zselect_correct, ?Z.add_modulo_correct. + change_weight. + + (* pull out value before last modular reduction *) + match goal with |- (if (?n <=? ?x)%Z then ?x - ?n else ?x) = (if (?n <=? ?y) then ?y - ?n else ?y)%Z => + let P := fresh "H" in assert (x = y) as P; [|rewrite P; reflexivity] end. + + autorewrite with zsimplify. + rewrite (Z.mul_comm (((T mod R) * N') mod R) N) in *. + break_match; try reflexivity; Z.ltb_to_lt; rewrite Z.div_small_iff in * by omega; + repeat match goal with + | _ => progress autorewrite with zsimplify_fast + | |- context [?x mod (R * R)] => + unique pose proof (Z.mod_pos_bound x (R * R)); + try rewrite (Z.mod_small x (R * R)) in * by Z.rewrite_mod_small_solver + | _ => omega + | _ => progress Z.rewrite_mod_small + end. + Qed. + + Lemma montred'_correct lo hi T (HT_range: 0 <= T < R * N) + (Hlo: lo = T mod R) (Hhi: hi = T / R): montred' lo hi = (T * R') mod N. + Proof. + erewrite montred'_eq by eauto. + apply Z.equiv_modulo_mod_small; auto using reduce_via_partial_correct. + replace 0 with (Z.min 0 (R-N)) by (apply Z.min_l; omega). + apply reduce_via_partial_in_range; omega. + Qed. + End MontRed'. +End MontgomeryReduction. diff --git a/src/CLI.v b/src/CLI.v index 289e66c4f..3975b0845 100644 --- a/src/CLI.v +++ b/src/CLI.v @@ -9,7 +9,9 @@ Require Import Crypto.Util.Strings.HexString. Require Import Crypto.Util.Strings.ParseArithmetic. Require Import Crypto.Util.Option. Require Import Crypto.Util.Strings.Show. -Require Import Crypto.PushButtonSynthesis. +Require Crypto.PushButtonSynthesis.SaturatedSolinas. +Require Crypto.PushButtonSynthesis.UnsaturatedSolinas. +Require Crypto.PushButtonSynthesis.WordByWordMontgomery. Require Import Crypto.CStringification. Require Import Crypto.BoundsPipeline. Import ListNotations. Local Open Scope Z_scope. Local Open Scope string_scope. diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v index 2ee19e6e6..46e8f6f52 100644 --- a/src/Fancy/Barrett256.v +++ b/src/Fancy/Barrett256.v @@ -8,7 +8,7 @@ Require Import Crypto.Fancy.Prod. Require Import Crypto.Fancy.Spec. Require Import Crypto.Language. Import Language.Compilers. Require Import Crypto.LanguageWf. -Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.PushButtonSynthesis.BarrettReduction. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -144,7 +144,7 @@ Module Barrett256. { cbn. repeat match goal with | _ => apply Compilers.expr.WfLetIn - | _ => progress wf_subgoal + | _ => progress wf_subgoal | _ => econstructor end. } { cbn. cbv [muLow M]. @@ -299,7 +299,7 @@ Module Barrett256. repeat match goal with H : context [start_context] |- _ => rewrite <-H end. - + cbv [barrett_red256_alloc barrett_red256_fancy]. repeat step. reflexivity. @@ -399,4 +399,4 @@ Eval cbv beta iota delta [Barrett256.barrett_red256_alloc] in Barrett256.barrett Check Barrett256.prod_barrett_red256_correct. Print Assumptions Barrett256.prod_barrett_red256_correct. (* The equivalence with generated code is admitted as barrett_red256_alloc_equivalent. *) -*) \ No newline at end of file +*) diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v index e5f9c5072..19415ad03 100644 --- a/src/Fancy/Montgomery256.v +++ b/src/Fancy/Montgomery256.v @@ -7,7 +7,8 @@ Require Import Crypto.Fancy.Prod. Require Import Crypto.Fancy.Spec. Require Import Crypto.Language. Import Language.Compilers. Require Import Crypto.LanguageWf. -Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.Arithmetic. (* For the MontgomeryReduction Module *) +Require Import Crypto.PushButtonSynthesis.MontgomeryReduction. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -140,7 +141,7 @@ Module Montgomery256. { cbn. repeat match goal with | _ => apply Compilers.expr.WfLetIn - | _ => progress wf_subgoal + | _ => progress wf_subgoal | _ => econstructor end. } { cbn. cbv [N' N]. @@ -317,4 +318,4 @@ preconditions. *) (* Check Montgomery256.prod_montred256_correct. Print Assumptions Montgomery256.prod_montred256_correct. -*) \ No newline at end of file +*) diff --git a/src/PushButtonSynthesis.v b/src/PushButtonSynthesis.v deleted file mode 100644 index e3dee09c7..000000000 --- a/src/PushButtonSynthesis.v +++ /dev/null @@ -1,3196 +0,0 @@ -(** * Push-Button Synthesis of Saturated Solinas *) -Require Import Coq.Strings.String. -Require Import Coq.micromega.Lia. -Require Import Coq.ZArith.ZArith. -Require Import Coq.MSets.MSetPositive. -Require Import Coq.Lists.List. -Require Import Coq.QArith.QArith_base Coq.QArith.Qround. -Require Import Coq.Program.Tactics. (* For WBW Montgomery proofs *) -Require Import Coq.derive.Derive. -Require Import Crypto.Util.ErrorT. -Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.ListUtil.FoldBool. -Require Import Crypto.Util.Strings.Decimal. -Require Import Crypto.Util.Strings.Equality. -Require Import Crypto.Util.ZRange. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Zselect. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.ModInv. (* Only needed for WBW Montgomery *) -Require Import Crypto.Util.ZUtil.Modulo. (* Only needed for WBW Montgomery proofs *) -Require Import Crypto.Util.ZUtil.Le. (* Only needed for WBW Montgomery proofs *) -Require Import Crypto.Util.Prod. (* For WBW Montgomery proofs *) -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. (* For WBW montgomery proofs *) -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. (* For WBW montgomery proofs *) -Require Import Crypto.Util.ZUtil.Div. (* For WBW Montgomery proofs *) -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. (* For WBW Montgomery proofs *) -Require Import Crypto.Util.ZUtil.Ones. (* For WBW montgomery proofs *) -Require Import Crypto.Util.ZUtil.Shift. (* For WBW montgomery proofs *) -Require Import Crypto.Util.LetIn. (* For Barrett *) -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. (* For Barrett *) -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. (* For Barrett *) -Require Import Crypto.Util.Tactics.UniquePose. (* For Barrett *) -Require Import Crypto.Util.ZUtil.Rshi. (* For Barrett *) -Require Import Crypto.Algebra.Ring. (* For Barrett *) -Require Import Crypto.Util.ZUtil.AddModulo. (* For Barrett *) -Require Import Crypto.Util.ZUtil.Zselect. (* For Barrett *) -Require Import Crypto.Util.ZUtil.CC. (* For Barrett *) -Require Import Crypto.Util.ZUtil.EquivModulo. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.HasBody. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.LanguageWf. -Require Import Crypto.Language. -Require Import Crypto.AbstractInterpretation. -Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. -Require Import Crypto.BoundsPipeline. -Require Import Crypto.COperationSpecifications. -Require Import Crypto.PushButtonSynthesis.ReificationCache. -Import ListNotations. -Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. - -Import - LanguageWf.Compilers - Language.Compilers - AbstractInterpretation.Compilers - CStringification.Compilers. -Import Compilers.defaults. - -Import COperationSpecifications.Primitives. -Import COperationSpecifications.Solinas. - -Import Associational Positional. - -Local Coercion Z.of_nat : nat >-> Z. -Local Coercion QArith_base.inject_Z : Z >-> Q. -Local Coercion Z.pos : positive >-> Z. - -Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) - -Module Export Primitives. - (** -<< -#!/usr/bin/env python - -indent = ' ' - -print((indent + '(' + r'''** -<< -%s ->> -*''' + ')\n') % open(__file__, 'r').read()) - -for (op, opmod) in (('id', '(@id (list Z))'), ('selectznz', 'Positional.select'), ('mulx', 'mulx'), ('addcarryx', 'addcarryx'), ('subborrowx', 'subborrowx'), ('cmovznz', 'cmovznz')): - print((r'''%sDerive reified_%s_gen - SuchThat (is_reification_of reified_%s_gen %s) - As reified_%s_gen_correct. -Proof. Time cache_reify (). Time Qed. -Hint Extern 1 (_ = _) => apply_cached_reification %s (proj1 reified_%s_gen_correct) : reify_cache_gen. -Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. -Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. -Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, op, op, opmod, op, opmod, op, op, op, op)).replace('\n', '\n%s' % indent) + '\n') - ->> -*) - - Derive reified_id_gen - SuchThat (is_reification_of reified_id_gen (@id (list Z))) - As reified_id_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification (@id (list Z)) (proj1 reified_id_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_id_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_id_gen_correct) : interp_gen_cache. - Local Opaque reified_id_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_selectznz_gen - SuchThat (is_reification_of reified_selectznz_gen Positional.select) - As reified_selectznz_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification Positional.select (proj1 reified_selectznz_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_selectznz_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_selectznz_gen_correct) : interp_gen_cache. - Local Opaque reified_selectznz_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_mulx_gen - SuchThat (is_reification_of reified_mulx_gen mulx) - As reified_mulx_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification mulx (proj1 reified_mulx_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_mulx_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_mulx_gen_correct) : interp_gen_cache. - Local Opaque reified_mulx_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_addcarryx_gen - SuchThat (is_reification_of reified_addcarryx_gen addcarryx) - As reified_addcarryx_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification addcarryx (proj1 reified_addcarryx_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_addcarryx_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_addcarryx_gen_correct) : interp_gen_cache. - Local Opaque reified_addcarryx_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_subborrowx_gen - SuchThat (is_reification_of reified_subborrowx_gen subborrowx) - As reified_subborrowx_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification subborrowx (proj1 reified_subborrowx_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_subborrowx_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_subborrowx_gen_correct) : interp_gen_cache. - Local Opaque reified_subborrowx_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_cmovznz_gen - SuchThat (is_reification_of reified_cmovznz_gen cmovznz) - As reified_cmovznz_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification cmovznz (proj1 reified_cmovznz_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_cmovznz_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_cmovznz_gen_correct) : interp_gen_cache. - Local Opaque reified_cmovznz_gen. (* needed for making [autorewrite] not take a very long time *) - - (* needed for making [autorewrite] with [Set Keyed Unification] fast *) - Local Opaque expr.Interp. - - Local Notation arg_bounds_of_pipeline result - := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl) - (only parsing). - Local Notation out_bounds_of_pipeline result - := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl) - (only parsing). - - Notation FromPipelineToString prefix name result - := (((prefix ++ name)%string, - match result with - | Success E' - => let E := ToString.C.ToFunctionLines - true true (* static *) prefix (prefix ++ name)%string [] E' None - (arg_bounds_of_pipeline result) - (out_bounds_of_pipeline result) in - match E with - | inl E => Success E - | inr err => Error (Pipeline.Stringification_failed E' err) - end - | Error err => Error err - end)). - - Ltac prove_correctness use_curve_good := - let Hres := match goal with H : _ = Success _ |- _ => H end in - let H := fresh in - pose proof use_curve_good as H; - (* I want to just use [clear -H Hres], but then I can't use any lemmas in the section because of COQBUG(https://github.com/coq/coq/issues/8153) *) - repeat match goal with - | [ H' : _ |- _ ] - => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres ] - then fail - else clear H' - end; - cbv zeta in *; - destruct_head'_and; - let f := match type of Hres with ?f = _ => head f end in - try cbv [f] in *; - hnf; - PipelineTactics.do_unfolding; - try (let m := match goal with m := _ - Associational.eval _ |- _ => m end in - cbv [m] in * ); - intros; - try split; PipelineTactics.use_compilers_correctness Hres; - [ pose_proof_length_list_Z_bounded_by; - repeat first [ reflexivity - | progress autorewrite with interp interp_gen_cache push_eval - | progress autounfold with push_eval - | progress autorewrite with distr_length in * ] - | .. ]. - - Section __. - Context (n : nat) - (machine_wordsize : Z). - - Definition saturated_bounds_list : list (option zrange) - := List.repeat (Some r[0 ~> 2^machine_wordsize-1]%zrange) n. - Definition saturated_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) - := Some saturated_bounds_list. - - (* We include [0], so that even after bounds relaxation, we can - notice where the constant 0s are, and remove them. *) - Definition possible_values_of_machine_wordsize - := [0; machine_wordsize; 2 * machine_wordsize]%Z. - - Definition possible_values_of_machine_wordsize_with_bytes - := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. - - Let possible_values := possible_values_of_machine_wordsize. - Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. - - Lemma length_saturated_bounds_list : List.length saturated_bounds_list = n. - Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. - Hint Rewrite length_saturated_bounds_list : distr_length. - - Definition selectznz - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - reified_selectznz_gen - (Some r[0~>1], (saturated_bounds, (saturated_bounds, tt)))%zrange - saturated_bounds. - - Definition sselectznz (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "selectznz" selectznz. - - Definition mulx (s : Z) - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_mulx_gen - @ GallinaReify.Reify s) - (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt))%zrange - (Some r[0~>2^s-1], Some r[0~>2^s-1])%zrange. - - Definition smulx (prefix : string) (s : Z) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s). - - Definition addcarryx (s : Z) - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_addcarryx_gen - @ GallinaReify.Reify s) - (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange - (Some r[0~>2^s-1], Some r[0~>1])%zrange. - - Definition saddcarryx (prefix : string) (s : Z) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s). - - Definition subborrowx (s : Z) - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_subborrowx_gen - @ GallinaReify.Reify s) - (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange - (Some r[0~>2^s-1], Some r[0~>1])%zrange. - - Definition ssubborrowx (prefix : string) (s : Z) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s). - - Definition cmovznz (s : Z) - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_cmovznz_gen - @ GallinaReify.Reify s) - (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange - (Some r[0~>2^s-1])%zrange. - - Definition scmovznz (prefix : string) (s : Z) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s). - - Local Ltac solve_extra_bounds_side_conditions := - cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. - - Hint Rewrite - eval_select - Arithmetic.mulx_correct - Arithmetic.addcarryx_correct - Arithmetic.subborrowx_correct - Arithmetic.cmovznz_correct - Z.zselect_correct - using solve [ auto | congruence | solve_extra_bounds_side_conditions ] : push_eval. - - Strategy -1000 [mulx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma mulx_correct s' res - (Hres : mulx s' = Success res) - : mulx_correct s' (Interp res). - Proof using Type. prove_correctness I. Qed. - - Strategy -1000 [addcarryx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma addcarryx_correct s' res - (Hres : addcarryx s' = Success res) - : addcarryx_correct s' (Interp res). - Proof using Type. prove_correctness I. Qed. - - Strategy -1000 [subborrowx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma subborrowx_correct s' res - (Hres : subborrowx s' = Success res) - : subborrowx_correct s' (Interp res). - Proof using Type. prove_correctness I. Qed. - - Strategy -1000 [cmovznz]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma cmovznz_correct s' res - (Hres : cmovznz s' = Success res) - : cmovznz_correct s' (Interp res). - Proof using Type. prove_correctness I. Qed. - - Lemma selectznz_correct limbwidth res - (Hres : selectznz = Success res) - : selectznz_correct (weight (Qnum limbwidth) (QDen limbwidth)) n saturated_bounds_list (Interp res). - Proof using Type. prove_correctness I. Qed. - - Section for_stringification. - Context (valid_names : string) - (known_functions : list (string - * (string - -> string * - Pipeline.ErrorT (list string * ToString.C.ident_infos)))) - (extra_special_synthesis : string -> - list - (option - (string * - Pipeline.ErrorT - (list string * ToString.C.ident_infos)))). - - Definition aggregate_infos {A B C} (ls : list (A * ErrorT B (C * ToString.C.ident_infos))) : ToString.C.ident_infos - := fold_right - ToString.C.ident_info_union - ToString.C.ident_info_empty - (List.map - (fun '(_, res) => match res with - | Success (_, infos) => infos - | Error _ => ToString.C.ident_info_empty - end) - ls). - - Definition extra_synthesis (function_name_prefix : string) (infos : ToString.C.ident_infos) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t - := let ls_addcarryx := List.flat_map - (fun lg_split:positive => [saddcarryx function_name_prefix lg_split; ssubborrowx function_name_prefix lg_split]) - (PositiveSet.elements (ToString.C.addcarryx_lg_splits infos)) in - let ls_mulx := List.map - (fun lg_split:positive => smulx function_name_prefix lg_split) - (PositiveSet.elements (ToString.C.mulx_lg_splits infos)) in - let ls_cmov := List.map - (fun bitwidth:positive => scmovznz function_name_prefix bitwidth) - (PositiveSet.elements (ToString.C.cmovznz_bitwidths infos)) in - let ls := ls_addcarryx ++ ls_mulx ++ ls_cmov in - let infos := aggregate_infos ls in - (List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, - ToString.C.bitwidths_used infos). - - - Definition synthesize_of_name (function_name_prefix : string) (name : string) - : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos) - := fold_right - (fun v default - => match v with - | Some res => res - | None => default - end) - ((name, - Error - (Pipeline.Invalid_argument - ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ ".")))) - ((map - (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None) - known_functions) - ++ extra_special_synthesis name). - - (** Note: If you change the name or type signature of this - function, you will need to update the code in CLI.v *) - Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) - := let ls := match requests with - | nil => List.map (fun '(_, sr) => sr function_name_prefix) known_functions - | requests => List.map (synthesize_of_name function_name_prefix) requests - end in - let infos := aggregate_infos ls in - let '(extra_ls, extra_bit_widths) := extra_synthesis function_name_prefix infos in - (extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, - PositiveSet.union extra_bit_widths (ToString.C.bitwidths_used infos)). - End for_stringification. - End __. -End Primitives. - -Module UnsaturatedSolinas. - Definition zeromod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 0. - Definition onemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 1. - Definition primemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n (s - Associational.eval c). - - (** -<< -#!/usr/bin/env python - -indent = ' ' - -print((indent + '(' + r'''** -<< -%s ->> -*''' + ')\n') % open(__file__, 'r').read()) - -for i in ('carry_mul', 'carry_square', 'carry_scmul', 'carry', 'encode', 'add', 'sub', 'opp', 'zero', 'one', 'prime'): - print((r'''%sDerive reified_%s_gen - SuchThat (is_reification_of reified_%s_gen %smod) - As reified_%s_gen_correct. -Proof. Time cache_reify (). Time Qed. -Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. -Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. -Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. -Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') - -for (op, opmod) in (('to_bytes', 'freeze_to_bytesmod'), ('from_bytes', 'from_bytesmod')): - print((r'''%sDerive reified_%s_gen - SuchThat (is_reification_of reified_%s_gen %s) - As reified_%s_gen_correct. -Proof. Time cache_reify (). Time Qed. -Hint Extern 1 (_ = _) => apply_cached_reification %s (proj1 reified_%s_gen_correct) : reify_cache_gen. -Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. -Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. -Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, op, op, opmod, op, opmod, op, op, op, op)).replace('\n', '\n%s' % indent) + '\n') - ->> -*) - - Derive reified_carry_mul_gen - SuchThat (is_reification_of reified_carry_mul_gen carry_mulmod) - As reified_carry_mul_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification carry_mulmod (proj1 reified_carry_mul_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_carry_mul_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_carry_mul_gen_correct) : interp_gen_cache. - Local Opaque reified_carry_mul_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_carry_square_gen - SuchThat (is_reification_of reified_carry_square_gen carry_squaremod) - As reified_carry_square_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification carry_squaremod (proj1 reified_carry_square_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_carry_square_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_carry_square_gen_correct) : interp_gen_cache. - Local Opaque reified_carry_square_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_carry_scmul_gen - SuchThat (is_reification_of reified_carry_scmul_gen carry_scmulmod) - As reified_carry_scmul_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification carry_scmulmod (proj1 reified_carry_scmul_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_carry_scmul_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_carry_scmul_gen_correct) : interp_gen_cache. - Local Opaque reified_carry_scmul_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_carry_gen - SuchThat (is_reification_of reified_carry_gen carrymod) - As reified_carry_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification carrymod (proj1 reified_carry_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_carry_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_carry_gen_correct) : interp_gen_cache. - Local Opaque reified_carry_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_encode_gen - SuchThat (is_reification_of reified_encode_gen encodemod) - As reified_encode_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification encodemod (proj1 reified_encode_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_encode_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_encode_gen_correct) : interp_gen_cache. - Local Opaque reified_encode_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_add_gen - SuchThat (is_reification_of reified_add_gen addmod) - As reified_add_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification addmod (proj1 reified_add_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_add_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_add_gen_correct) : interp_gen_cache. - Local Opaque reified_add_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_sub_gen - SuchThat (is_reification_of reified_sub_gen submod) - As reified_sub_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification submod (proj1 reified_sub_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_sub_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_sub_gen_correct) : interp_gen_cache. - Local Opaque reified_sub_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_opp_gen - SuchThat (is_reification_of reified_opp_gen oppmod) - As reified_opp_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification oppmod (proj1 reified_opp_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_opp_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_opp_gen_correct) : interp_gen_cache. - Local Opaque reified_opp_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_zero_gen - SuchThat (is_reification_of reified_zero_gen zeromod) - As reified_zero_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification zeromod (proj1 reified_zero_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_zero_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_zero_gen_correct) : interp_gen_cache. - Local Opaque reified_zero_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_one_gen - SuchThat (is_reification_of reified_one_gen onemod) - As reified_one_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification onemod (proj1 reified_one_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_one_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_one_gen_correct) : interp_gen_cache. - Local Opaque reified_one_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_prime_gen - SuchThat (is_reification_of reified_prime_gen primemod) - As reified_prime_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification primemod (proj1 reified_prime_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_prime_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_prime_gen_correct) : interp_gen_cache. - Local Opaque reified_prime_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_to_bytes_gen - SuchThat (is_reification_of reified_to_bytes_gen freeze_to_bytesmod) - As reified_to_bytes_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification freeze_to_bytesmod (proj1 reified_to_bytes_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_to_bytes_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_to_bytes_gen_correct) : interp_gen_cache. - Local Opaque reified_to_bytes_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_from_bytes_gen - SuchThat (is_reification_of reified_from_bytes_gen from_bytesmod) - As reified_from_bytes_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification from_bytesmod (proj1 reified_from_bytes_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_from_bytes_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_from_bytes_gen_correct) : interp_gen_cache. - Local Opaque reified_from_bytes_gen. (* needed for making [autorewrite] not take a very long time *) - - (* needed for making [autorewrite] with [Set Keyed Unification] fast *) - Local Opaque expr.Interp. - - Section __. - Context (n : nat) - (s : Z) - (c : list (Z * Z)) - (machine_wordsize : Z). - - Let limbwidth := (Z.log2_up (s - Associational.eval c) / Z.of_nat n)%Q. - Let idxs := (List.seq 0 n ++ [0; 1])%list%nat. - Let coef := 2. - Let n_bytes := bytes_n (Qnum limbwidth) (Qden limbwidth) n. - Let prime_upperbound_list : list Z - := encode_no_reduce (weight (Qnum limbwidth) (Qden limbwidth)) n (s-1). - Let prime_bytes_upperbound_list : list Z - := encode_no_reduce (weight 8 1) n_bytes (s-1). - Let tight_upperbounds : list Z - := List.map - (fun v : Z => Qceiling (11/10 * v)) - prime_upperbound_list. - Definition prime_bound : ZRange.type.option.interp (base.type.Z) - := Some r[0~>(s - Associational.eval c - 1)]%zrange. - Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) - := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). - Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) - := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list). - Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize). - Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). - - Let m : Z := s - Associational.eval c. - Definition m_enc : list Z - := encode (weight (Qnum limbwidth) (Qden limbwidth)) n s c m. - - (* We include [0], so that even after bounds relaxation, we can - notice where the constant 0s are, and remove them. *) - Definition possible_values_of_machine_wordsize - := [0; machine_wordsize; 2 * machine_wordsize]%Z. - - Definition possible_values_of_machine_wordsize_with_bytes - := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. - - Let possible_values := possible_values_of_machine_wordsize. - Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. - Definition tight_bounds : list (ZRange.type.option.interp base.type.Z) - := List.map (fun u => Some r[0~>u]%zrange) tight_upperbounds. - Definition loose_bounds : list (ZRange.type.option.interp base.type.Z) - := List.map (fun u => Some r[0 ~> 3*u]%zrange) tight_upperbounds. - - Lemma length_prime_upperbound_list : List.length prime_upperbound_list = n. - Proof using Type. cbv [prime_upperbound_list]; now autorewrite with distr_length. Qed. - Hint Rewrite length_prime_upperbound_list : distr_length. - Lemma length_tight_upperbounds : List.length tight_upperbounds = n. - Proof using Type. cbv [tight_upperbounds]; now autorewrite with distr_length. Qed. - Hint Rewrite length_tight_upperbounds : distr_length. - Lemma length_tight_bounds : List.length tight_bounds = n. - Proof using Type. cbv [tight_bounds]; now autorewrite with distr_length. Qed. - Hint Rewrite length_tight_bounds : distr_length. - Lemma length_loose_bounds : List.length loose_bounds = n. - Proof using Type. cbv [loose_bounds]; now autorewrite with distr_length. Qed. - Hint Rewrite length_loose_bounds : distr_length. - Lemma length_prime_bytes_upperbound_list : List.length prime_bytes_upperbound_list = bytes_n (Qnum limbwidth) (Qden limbwidth) n. - Proof using Type. cbv [prime_bytes_upperbound_list]; now autorewrite with distr_length. Qed. - Hint Rewrite length_prime_bytes_upperbound_list : distr_length. - Lemma length_saturated_bounds_list : List.length saturated_bounds_list = n. - Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. - Hint Rewrite length_saturated_bounds_list : distr_length. - - (** Note: If you change the name or type signature of this - function, you will need to update the code in CLI.v *) - Definition check_args {T} (res : Pipeline.ErrorT T) - : Pipeline.ErrorT T - := fold_right - (fun '(b, e) k => if b:bool then Error e else k) - res - [(negb (Qle_bool 1 limbwidth)%Q, Pipeline.Value_not_leQ "limbwidth < 1" 1%Q limbwidth); - ((negb (0 0 - /\ s <> 0 - /\ 0 < machine_wordsize - /\ n <> 0%nat - /\ List.length tight_bounds = n - /\ List.length loose_bounds = n - /\ List.length prime_bytes_upperbound_list = n_bytes - /\ List.length saturated_bounds_list = n - /\ 0 < Qden limbwidth <= Qnum limbwidth - /\ s = weight (Qnum limbwidth) (QDen limbwidth) n - /\ map (Z.land (Z.ones machine_wordsize)) m_enc = m_enc - /\ eval m_enc = s - Associational.eval c - /\ Datatypes.length m_enc = n - /\ 0 < Associational.eval c < s - /\ eval tight_upperbounds < 2 * eval m_enc - /\ 0 < m. - Proof using curve_good. - clear -curve_good. - cbv [check_args fold_right] in curve_good. - cbv [tight_bounds loose_bounds prime_bound m_enc] in *. - break_innermost_match_hyps; try discriminate. - rewrite negb_false_iff in *. - Z.ltb_to_lt. - rewrite Qle_bool_iff in *. - rewrite NPeano.Nat.eqb_neq in *. - intros. - cbv [Qnum Qden limbwidth Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *. - rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. - specialize_by lia. - repeat match goal with H := _ |- _ => subst H end. - repeat match goal with - | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] - end. - repeat apply conj. - { destruct (s - Associational.eval c) eqn:?; cbn; lia. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - Qed. - - Definition carry_mul - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values - (reified_carry_mul_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) - (Some loose_bounds, (Some loose_bounds, tt)) - (Some tight_bounds). - - Definition scarry_mul (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry_mul" carry_mul. - - Definition carry_square - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values - (reified_carry_square_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) - (Some loose_bounds, tt) - (Some tight_bounds). - - Definition scarry_square (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry_square" carry_square. - - Definition carry_scmul_const (x : Z) - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values - (reified_carry_scmul_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs @ GallinaReify.Reify x) - (Some loose_bounds, tt) - (Some tight_bounds). - - Definition scarry_scmul_const (prefix : string) (x : Z) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x). - - Definition carry - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_carry_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) - (Some loose_bounds, tt) - (Some tight_bounds). - - Definition scarry (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "carry" carry. - - Definition add - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_add_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n) - (Some tight_bounds, (Some tight_bounds, tt)) - (Some loose_bounds). - - Definition sadd (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "add" add. - - Definition sub - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_sub_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify coef) - (Some tight_bounds, (Some tight_bounds, tt)) - (Some loose_bounds). - - Definition ssub (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "sub" sub. - - Definition opp - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_opp_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify coef) - (Some tight_bounds, tt) - (Some loose_bounds). - - Definition sopp (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "opp" opp. - - Definition to_bytes - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_to_bytes_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify m_enc) - (Some tight_bounds, tt) - prime_bytes_bounds. - - Definition sto_bytes (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. - - Definition from_bytes - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_from_bytes_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n) - (prime_bytes_bounds, tt) - (Some tight_bounds). - - Definition sfrom_bytes (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. - - Definition encode - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_encode_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) - (prime_bound, tt) - (Some tight_bounds). - - Definition sencode (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "encode" encode. - - Definition zero - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_zero_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) - tt - (Some tight_bounds). - - Definition szero (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "zero" zero. - - Definition one - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_one_gen - @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) - tt - (Some tight_bounds). - - Definition sone (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "one" one. - - Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. - Definition sselectznz (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Primitives.sselectznz n machine_wordsize prefix. - - Local Ltac solve_extra_bounds_side_conditions := - cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. - - Hint Rewrite - eval_carry_mulmod - eval_carry_squaremod - eval_carry_scmulmod - eval_addmod - eval_submod - eval_oppmod - eval_carrymod - freeze_to_bytesmod_partitions - eval_to_bytesmod - eval_from_bytesmod - eval_encodemod - using solve [ auto | congruence | solve_extra_bounds_side_conditions ] : push_eval. - Hint Unfold zeromod onemod : push_eval. - - Local Ltac prove_correctness _ := - Primitives.prove_correctness use_curve_good; - try solve [ auto | congruence | solve_extra_bounds_side_conditions ]. - - Lemma carry_mul_correct res - (Hres : carry_mul = Success res) - : carry_mul_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Lemma carry_square_correct res - (Hres : carry_square = Success res) - : carry_square_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Lemma carry_scmul_const_correct a res - (Hres : carry_scmul_const a = Success res) - : carry_scmul_const_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds a (Interp res). - Proof using curve_good. - prove_correctness (). - erewrite eval_carry_scmulmod by (auto || congruence); reflexivity. - Qed. - - Lemma carry_correct res - (Hres : carry = Success res) - : carry_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Lemma add_correct res - (Hres : add = Success res) - : add_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Lemma sub_correct res - (Hres : sub = Success res) - : sub_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Lemma opp_correct res - (Hres : opp = Success res) - : opp_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Lemma from_bytes_correct res - (Hres : from_bytes = Success res) - : from_bytes_correct (weight (Qnum limbwidth) (QDen limbwidth)) n n_bytes m s tight_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Lemma relax_correct - : forall x, list_Z_bounded_by tight_bounds x -> list_Z_bounded_by loose_bounds x. - Proof using Type. - cbv [tight_bounds loose_bounds list_Z_bounded_by]. - intro. - rewrite !fold_andb_map_map1, !fold_andb_map_iff; cbn [upper lower]. - setoid_rewrite Bool.andb_true_iff. - intro H. - repeat first [ let H' := fresh in destruct H as [H' H]; split; [ assumption | ] - | let x := fresh in intro x; specialize (H x) ]. - Z.ltb_to_lt; lia. - Qed. - - Lemma to_bytes_correct res - (Hres : to_bytes = Success res) - : to_bytes_correct (weight (Qnum limbwidth) (QDen limbwidth)) n n_bytes m tight_bounds (Interp res). - Proof using curve_good. - prove_correctness (); []. - erewrite freeze_to_bytesmod_partitions; [ reflexivity | .. ]. - all: repeat apply conj; autorewrite with distr_length; (congruence || auto). - all: cbv [tight_bounds] in *. - all: lazymatch goal with - | [ H1 : list_Z_bounded_by (List.map (fun x => Some (@?f x)) ?b) ?x, H2 : eval ?wt ?n ?b < _ - |- context[eval ?wt ?n ?x] ] - => unshelve epose proof (eval_list_Z_bounded_by wt n (List.map (fun x => Some (f x)) b) (List.map f b) x H1 _ _ (fun A B => Z.lt_le_incl _ _ (weight_positive _ _))); clear H1 - end. - all: congruence || auto. - all: repeat first [ reflexivity - | apply wprops - | progress rewrite ?map_map in * - | progress rewrite ?map_id in * - | progress cbn [upper lower] in * - | lia - | match goal with - | [ H : context[List.map (fun _ => 0) _] |- _ ] => erewrite <- zeros_ext_map, ?eval_zeros in H by reflexivity - end - | progress autorewrite with distr_length push_eval in * - | progress cbv [tight_upperbounds] in * ]. - Qed. - - Strategy -1000 [encode]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma encode_correct res - (Hres : encode = Success res) - : encode_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Strategy -1000 [zero]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma zero_correct res - (Hres : zero = Success res) - : zero_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Strategy -1000 [one]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma one_correct res - (Hres : one = Success res) - : one_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Section ring. - Context carry_mul_res (Hcarry_mul : carry_mul = Success carry_mul_res) - add_res (Hadd : add = Success add_res) - sub_res (Hsub : sub = Success sub_res) - opp_res (Hopp : opp = Success opp_res) - carry_res (Hcarry : carry = Success carry_res) - encode_res (Hencode : encode = Success encode_res) - zero_res (Hzero : zero = Success zero_res) - one_res (Hone : one = Success one_res). - - Definition GoodT : Prop - := GoodT - (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds - (Interp carry_mul_res) - (Interp add_res) - (Interp sub_res) - (Interp opp_res) - (Interp carry_res) - (Interp encode_res) - (Interp zero_res) - (Interp one_res). - - Theorem Good : GoodT. - Proof using curve_good Hcarry_mul Hadd Hsub Hopp Hcarry Hencode Hzero Hone. - pose proof use_curve_good; cbv zeta in *; destruct_head'_and. - eapply Good. - all: repeat first [ assumption - | apply carry_mul_correct - | apply add_correct - | apply sub_correct - | apply opp_correct - | apply carry_correct - | apply encode_correct - | apply zero_correct - | apply one_correct - | apply relax_correct ]. - Qed. - End ring. - - Section for_stringification. - Local Open Scope string_scope. - Local Open Scope list_scope. - - Definition known_functions - := [("carry_mul", scarry_mul); - ("carry_square", scarry_square); - ("carry", scarry); - ("add", sadd); - ("sub", ssub); - ("opp", sopp); - ("selectznz", sselectznz); - ("to_bytes", sto_bytes); - ("from_bytes", sfrom_bytes)]. - - Definition valid_names : string - := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions) ++ ", or 'carry_scmul' followed by a decimal literal". - - Definition extra_special_synthesis (function_name_prefix : string) (name : string) - : list (option (string * Pipeline.ErrorT (list string * ToString.C.ident_infos))) - := [if prefix "carry_scmul" name - then let sc := substring (String.length "carry_scmul") (String.length name) name in - let scZ := Z_of_decimal_string sc in - if string_beq sc (decimal_string_of_Z scZ) - then Some (scarry_scmul_const function_name_prefix scZ) - else None - else None]. - - (** Note: If you change the name or type signature of this - function, you will need to update the code in CLI.v *) - Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) - := Primitives.Synthesize - machine_wordsize valid_names known_functions (extra_special_synthesis function_name_prefix) - function_name_prefix requests. - End for_stringification. - End __. -End UnsaturatedSolinas. - -Module SaturatedSolinas. - Import COperationSpecifications.SaturatedSolinas. - - Definition mulmod - (s : Z) - (c : list (Z * Z)) - (log2base : Z) - (n nreductions : nat) - := @Rows.mulmod (weight log2base 1) (2^log2base) s c n nreductions. - - Derive reified_mul_gen - SuchThat (is_reification_of reified_mul_gen mulmod) - As reified_mul_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification mulmod (proj1 reified_mul_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_mul_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_mul_gen_correct) : interp_gen_cache. - Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) - - (* needed for making [autorewrite] with [Set Keyed Unification] fast *) - Local Opaque expr.Interp. - - Section __. - Context (s : Z) - (c : list (Z * Z)) - (machine_wordsize : Z). - - (* We include [0], so that even after bounds relaxation, we can - notice where the constant 0s are, and remove them. *) - Definition possible_values_of_machine_wordsize - := [0; 1; machine_wordsize]%Z. - - Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). - Let m := s - Associational.eval c. - (* Number of reductions is calculated as follows : - Let i be the highest limb index of c. Then, each reduction - decreases the number of extra limbs by (n-i). So, to go from - the n extra limbs we have post-multiplication down to 0, we - need ceil (n / (n - i)) reductions. *) - Let nreductions : nat := - let i := fold_right Z.max 0 (map (fun t => Z.log2 (fst t) / machine_wordsize) c) in - Z.to_nat (Qceiling (Z.of_nat n / (Z.of_nat n - i))). - Let possible_values := possible_values_of_machine_wordsize. - Let bound := Some r[0 ~> (2^machine_wordsize - 1)]%zrange. - Let boundsn : list (ZRange.type.option.interp base.type.Z) - := repeat bound n. - - (** Note: If you change the name or type signature of this - function, you will need to update the code in CLI.v *) - Definition check_args {T} (res : Pipeline.ErrorT T) - : Pipeline.ErrorT T - := fold_right - (fun '(b, e) k => if b:bool then Error e else k) - res - [((negb (0 0 - /\ s <> 0 - /\ 0 < machine_wordsize - /\ n <> 0%nat. - Proof using curve_good. - clear -curve_good. - cbv [check_args fold_right] in curve_good. - break_innermost_match_hyps; try discriminate. - rewrite negb_false_iff in *. - Z.ltb_to_lt. - rewrite NPeano.Nat.eqb_neq in *. - intros. - rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. - specialize_by lia. - repeat match goal with H := _ |- _ => subst H end. - repeat match goal with - | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] - end. - repeat apply conj. - { destruct (s - Associational.eval c) eqn:?; cbn; lia. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - Qed. - - Definition mul - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values - (reified_mul_gen - @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify nreductions) - (Some boundsn, (Some boundsn, tt)) - (Some boundsn, None (* Should be: Some r[0~>0]%zrange, but bounds analysis is not good enough *) ). - - Definition smul (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "mul" mul. - - Local Ltac solve_extra_bounds_side_conditions := - cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. - - Hint Rewrite - (fun pf => @Rows.eval_mulmod (weight machine_wordsize 1) (@wprops _ _ pf)) - using solve [ auto with zarith | congruence | solve_extra_bounds_side_conditions ] : push_eval. - Hint Unfold mulmod : push_eval. - - Local Ltac prove_correctness _ := Primitives.prove_correctness use_curve_good. - - Lemma mul_correct res - (Hres : mul = Success res) - : mul_correct (weight machine_wordsize 1) n m boundsn (Interp res). - Proof using curve_good. prove_correctness (). Qed. - - Section for_stringification. - Local Open Scope string_scope. - Local Open Scope list_scope. - - Definition known_functions - := [("mul", smul)]. - - Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). - - (** Note: If you change the name or type signature of this - function, you will need to update the code in CLI.v *) - Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) - := Primitives.Synthesize - machine_wordsize valid_names known_functions (fun _ => nil) - function_name_prefix requests. - End for_stringification. - End __. -End SaturatedSolinas. - -Module WordByWordMontgomery. - Import Arithmetic.WordByWordMontgomery. - Import COperationSpecifications.WordByWordMontgomery. - - Definition zeromod bitwidth n m m' := encodemod bitwidth n m m' 0. - Definition onemod bitwidth n m m' := encodemod bitwidth n m m' 1. - - (* we would do something faster, but it generally breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) - Local Ltac precache_reify_faster _ := - split; - [ let marker := fresh "marker" in - pose I as marker; - intros; - let LHS := lazymatch goal with |- ?LHS = _ => LHS end in - let reified_op_gen := lazymatch LHS with context[expr.Interp _ ?reified_op_gen] => reified_op_gen end in - subst reified_op_gen; - etransitivity; - [ - | let opmod := match goal with |- _ = ?RHS => head RHS end in - cbv [opmod]; solve [ eauto with reify_cache_gen nocore ] ]; - repeat lazymatch goal with - | [ H : _ |- _ ] => tryif constr_eq H marker then fail else revert H - end; - clear marker - | ]. - Local Ltac cache_reify_faster_2arg _ := - precache_reify_faster (); - [ lazymatch goal with - | [ |- forall bw n m m' v, ?interp ?ev bw n m m' v = ?interp' ?reified_mul_gen bw n m m' (@?A bw n m m' v) (@?B bw n m m' v) ] - => let rv := constr:(fun F bw n m m' v => (F bw n m m' (A bw n m m' v) (B bw n m m' v)):list Z) in - intros; - instantiate (1:=ltac:(let r := Reify rv in - refine (r @ reified_mul_gen)%Expr)) - end; - reflexivity - | prove_Wf () ]. - Local Ltac cache_reify_faster_1arg _ := - precache_reify_faster (); - [ lazymatch goal with - | [ |- forall bw n m m', ?interp ?ev bw n m m' = ?interp' ?reified_op_gen bw n m m' (@?A bw n m m') ] - => let rv := constr:(fun F bw n m m' => (F bw n m m' (A bw n m m')):list Z) in - intros; - instantiate (1:=ltac:(let r := Reify rv in - refine (r @ reified_op_gen)%Expr)) - end; - reflexivity - | prove_Wf () ]. - - (** -<< -#!/usr/bin/env python - -indent = ' ' - -print((indent + '(' + r'''** -<< -%s ->> -*''' + ')\n') % open(__file__, 'r').read()) - -for i in ('mul', 'add', 'sub', 'opp', 'to_bytes', 'from_bytes', 'nonzero'): - print((r'''%sDerive reified_%s_gen - SuchThat (is_reification_of reified_%s_gen %smod) - As reified_%s_gen_correct. -Proof. Time cache_reify (). Time Qed. -Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. -Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. -Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. -Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') - -for i in ('square', 'encode', 'from_montgomery'): - print((r'''%sDerive reified_%s_gen - SuchThat (is_reification_of reified_%s_gen %smod) - As reified_%s_gen_correct. -Proof. - Time cache_reify (). - (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) - (* Time cache_reify_faster_2arg (). *) -Time Qed. -Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. -Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. -Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. -Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') - - -for i in ('zero', 'one'): - print((r'''%sDerive reified_%s_gen - SuchThat (is_reification_of reified_%s_gen %smod) - As reified_%s_gen_correct. -Proof. - (* Time cache_reify (). *) - (* we do something faster *) - Time cache_reify_faster_1arg (). -Time Qed. -Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. -Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. -Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. -Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') - ->> -*) - - Derive reified_mul_gen - SuchThat (is_reification_of reified_mul_gen mulmod) - As reified_mul_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification mulmod (proj1 reified_mul_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_mul_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_mul_gen_correct) : interp_gen_cache. - Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_add_gen - SuchThat (is_reification_of reified_add_gen addmod) - As reified_add_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification addmod (proj1 reified_add_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_add_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_add_gen_correct) : interp_gen_cache. - Local Opaque reified_add_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_sub_gen - SuchThat (is_reification_of reified_sub_gen submod) - As reified_sub_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification submod (proj1 reified_sub_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_sub_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_sub_gen_correct) : interp_gen_cache. - Local Opaque reified_sub_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_opp_gen - SuchThat (is_reification_of reified_opp_gen oppmod) - As reified_opp_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification oppmod (proj1 reified_opp_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_opp_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_opp_gen_correct) : interp_gen_cache. - Local Opaque reified_opp_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_to_bytes_gen - SuchThat (is_reification_of reified_to_bytes_gen to_bytesmod) - As reified_to_bytes_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification to_bytesmod (proj1 reified_to_bytes_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_to_bytes_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_to_bytes_gen_correct) : interp_gen_cache. - Local Opaque reified_to_bytes_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_from_bytes_gen - SuchThat (is_reification_of reified_from_bytes_gen from_bytesmod) - As reified_from_bytes_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification from_bytesmod (proj1 reified_from_bytes_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_from_bytes_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_from_bytes_gen_correct) : interp_gen_cache. - Local Opaque reified_from_bytes_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_nonzero_gen - SuchThat (is_reification_of reified_nonzero_gen nonzeromod) - As reified_nonzero_gen_correct. - Proof. Time cache_reify (). Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification nonzeromod (proj1 reified_nonzero_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_nonzero_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_nonzero_gen_correct) : interp_gen_cache. - Local Opaque reified_nonzero_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_square_gen - SuchThat (is_reification_of reified_square_gen squaremod) - As reified_square_gen_correct. - Proof. - Time cache_reify (). - (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) - (* Time cache_reify_faster_2arg (). *) - Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification squaremod (proj1 reified_square_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_square_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_square_gen_correct) : interp_gen_cache. - Local Opaque reified_square_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_encode_gen - SuchThat (is_reification_of reified_encode_gen encodemod) - As reified_encode_gen_correct. - Proof. - Time cache_reify (). - (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) - (* Time cache_reify_faster_2arg (). *) - Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification encodemod (proj1 reified_encode_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_encode_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_encode_gen_correct) : interp_gen_cache. - Local Opaque reified_encode_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_from_montgomery_gen - SuchThat (is_reification_of reified_from_montgomery_gen from_montgomerymod) - As reified_from_montgomery_gen_correct. - Proof. - Time cache_reify (). - (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) - (* Time cache_reify_faster_2arg (). *) - Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification from_montgomerymod (proj1 reified_from_montgomery_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_from_montgomery_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_from_montgomery_gen_correct) : interp_gen_cache. - Local Opaque reified_from_montgomery_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_zero_gen - SuchThat (is_reification_of reified_zero_gen zeromod) - As reified_zero_gen_correct. - Proof. - (* Time cache_reify (). *) - (* we do something faster *) - Time cache_reify_faster_1arg (). - Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification zeromod (proj1 reified_zero_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_zero_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_zero_gen_correct) : interp_gen_cache. - Local Opaque reified_zero_gen. (* needed for making [autorewrite] not take a very long time *) - - Derive reified_one_gen - SuchThat (is_reification_of reified_one_gen onemod) - As reified_one_gen_correct. - Proof. - (* Time cache_reify (). *) - (* we do something faster *) - Time cache_reify_faster_1arg (). - Time Qed. - Hint Extern 1 (_ = _) => apply_cached_reification onemod (proj1 reified_one_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_one_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_one_gen_correct) : interp_gen_cache. - Local Opaque reified_one_gen. (* needed for making [autorewrite] not take a very long time *) - - (* needed for making [autorewrite] with [Set Keyed Unification] fast *) - Local Opaque expr.Interp. - - Section __. - Context (m : Z) - (machine_wordsize : Z). - - Let s := 2^Z.log2_up m. - Let c := s - m. - Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). - Let r := 2^machine_wordsize. - Let r' := match Z.modinv r m with - | Some r' => r' - | None => 0 - end. - Let m' := match Z.modinv (-m) r with - | Some m' => m' - | None => 0 - end. - Let n_bytes := bytes_n machine_wordsize 1 n. - Let prime_upperbound_list : list Z - := Partition.partition (UniformWeight.uweight machine_wordsize) n (s-1). - Let prime_bytes_upperbound_list : list Z - := Partition.partition (weight 8 1) n_bytes (s-1). - Let upperbounds : list Z := prime_upperbound_list. - Definition prime_bound : ZRange.type.option.interp (base.type.Z) - := Some r[0~>m-1]%zrange. - Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) - := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). - Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) - := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list). - Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize). - Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). - - (* We include [0], so that even after bounds relaxation, we can - notice where the constant 0s are, and remove them. *) - Definition possible_values_of_machine_wordsize - := [0; 1; machine_wordsize; 2 * machine_wordsize]%Z. - - Definition possible_values_of_machine_wordsize_with_bytes - := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. - - Let possible_values := possible_values_of_machine_wordsize. - Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. - Definition bounds : list (ZRange.type.option.interp base.type.Z) - := Option.invert_Some saturated_bounds (*List.map (fun u => Some r[0~>u]%zrange) upperbounds*). - - (** Note: If you change the name or type signature of this - function, you will need to update the code in CLI.v *) - Definition check_args {T} (res : Pipeline.ErrorT T) - : Pipeline.ErrorT T - := fold_right - (fun '(b, e) k => if b:bool then Error e else k) - res - [(negb (1 0 - /\ s - c <> 0 - /\ 0 < s - /\ s <> 0 - /\ 0 < machine_wordsize - /\ n <> 0%nat - /\ List.length bounds = n - /\ 0 < 1 <= machine_wordsize - /\ 0 < c < s - /\ (r * r') mod m = 1 - /\ (m * m') mod r = (-1) mod r - /\ 0 < machine_wordsize - /\ 1 < m - /\ m < r^n - /\ s = 2^Z.log2 s - /\ s <= UniformWeight.uweight machine_wordsize n - /\ s <= UniformWeight.uweight 8 n_bytes - /\ UniformWeight.uweight machine_wordsize n = UniformWeight.uweight 8 n_bytes. - Proof. - clear -curve_good. - cbv [check_args fold_right] in curve_good. - cbv [bounds prime_bound prime_bounds saturated_bounds] in *. - break_innermost_match_hyps; try discriminate. - rewrite negb_false_iff in *. - Z.ltb_to_lt. - rewrite NPeano.Nat.eqb_neq in *. - intros. - cbv [Qnum Qden Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *. - rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. - specialize_by lia. - repeat match goal with H := _ |- _ => subst H end. - repeat match goal with - | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] - end. - repeat apply conj. - { destruct m eqn:?; cbn; lia. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - { use_curve_good_t. } - Qed. - - - Definition mul - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values - (reified_mul_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') - (Some bounds, (Some bounds, tt)) - (Some bounds). - - Definition smul (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "mul" mul. - - Definition square - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values - (reified_square_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') - (Some bounds, tt) - (Some bounds). - - Definition ssquare (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "square" square. - - Definition add - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_add_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) - (Some bounds, (Some bounds, tt)) - (Some bounds). - - Definition sadd (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "add" add. - - Definition sub - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_sub_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) - (Some bounds, (Some bounds, tt)) - (Some bounds). - - Definition ssub (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "sub" sub. - - Definition opp - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_opp_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) - (Some bounds, tt) - (Some bounds). - - Definition sopp (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "opp" opp. - - Definition from_montgomery - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_from_montgomery_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') - (Some bounds, tt) - (Some bounds). - - Definition sfrom_montgomery (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_montgomery" from_montgomery. - - Definition nonzero - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - reified_nonzero_gen - (Some bounds, tt) - (Some r[0~>r-1]%zrange). - - Definition snonzero (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "nonzero" nonzero. - - Definition to_bytes - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_to_bytes_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n) - (prime_bounds, tt) - prime_bytes_bounds. - - Definition sto_bytes (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. - - Definition from_bytes - := Pipeline.BoundsPipeline - false (* subst01 *) - None (* fancy *) - possible_values_with_bytes - (reified_from_bytes_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify 1 @ GallinaReify.Reify n) - (prime_bytes_bounds, tt) - prime_bounds. - - Definition sfrom_bytes (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. - - Definition encode - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_encode_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') - (prime_bound, tt) - (Some bounds). - - Definition sencode (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "encode" encode. - - Definition zero - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_zero_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') - tt - (Some bounds). - - Definition szero (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "zero" zero. - - Definition one - := Pipeline.BoundsPipeline - true (* subst01 *) - None (* fancy *) - possible_values - (reified_one_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') - tt - (Some bounds). - - Definition sone (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "one" one. - - Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. - Definition sselectznz (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Primitives.sselectznz n machine_wordsize prefix. - - Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). - Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). - - Lemma bounded_by_of_valid x - (H : valid x) - : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some bounds) x = true. - Proof using curve_good. - pose proof use_curve_good as use_curve_good. - clear -H use_curve_good curve_good. - destruct H as [H _]; destruct_head'_and. - cbv [small] in H. - cbv [ZRange.type.base.option.is_bounded_by bounds saturated_bounds saturated_bounds_list Option.invert_Some]. - replace n with (List.length x) by now rewrite H, Partition.length_partition. - rewrite <- map_const, fold_andb_map_map1, fold_andb_map_iff. - cbv [ZRange.type.base.is_bounded_by is_bounded_by_bool lower upper]. - split; [ reflexivity | ]. - intros *; rewrite combine_same, in_map_iff, Bool.andb_true_iff, !Z.leb_le. - intros; destruct_head'_ex; destruct_head'_and; subst *; cbn [fst snd]. - match goal with - | [ H : In ?v x |- _ ] => revert v H - end. - rewrite H. - generalize (eval (n:=n) machine_wordsize x). - cbn [base.interp base.base_interp]. - generalize n. - intro n'. - induction n' as [|n' IHn']. - { cbv [Partition.partition seq map In]; tauto. } - { intros *; rewrite Partition.partition_step, in_app_iff; cbn [List.In]. - intros; destruct_head'_or; subst *; eauto; try tauto; []. - rewrite UniformWeight.uweight_S by lia. - assert (0 < UniformWeight.uweight machine_wordsize n') by now apply UniformWeight.uwprops. - assert (0 < 2 ^ machine_wordsize) by auto with zarith. - assert (0 < 2 ^ machine_wordsize * UniformWeight.uweight machine_wordsize n') by nia. - rewrite <- Z.mod_pull_div by lia. - rewrite Z.le_sub_1_iff. - auto with zarith. } - Qed. - - (* XXX FIXME *) - Lemma bounded_by_prime_bounds_of_valid_gen lgr n' x - (Hlgr : 0 < lgr) - (Hs : s = 2^Z.log2 s) - (Hs' : s <= UniformWeight.uweight lgr n') - (H : WordByWordMontgomery.valid lgr n' m x) - : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some (List.map (fun v => Some r[0~>v]%zrange) (Partition.partition (UniformWeight.uweight lgr) n' (s-1)))) x = true. - Proof using curve_good. - pose proof use_curve_good as use_curve_good. - clear -H use_curve_good curve_good Hlgr Hs Hs'. - destruct H as [H ?]; destruct_head'_and. - cbv [small] in H. - cbv [ZRange.type.base.option.is_bounded_by]. - replace n' with (List.length x) by now rewrite H, Partition.length_partition. - rewrite fold_andb_map_map1, fold_andb_map_iff. - split; [ now autorewrite with distr_length | ]. - cbv [ZRange.type.base.is_bounded_by is_bounded_by_bool lower upper]. - rewrite H; autorewrite with distr_length. - intros [v1 v0]; cbn [fst snd]. - rename x into x'. - generalize dependent (eval (n:=n') lgr x'). - replace m with (s - c) in * by easy. - intro x; intros ??? H; subst x'. - eapply In_nth_error in H; destruct H as [i H]. - rewrite nth_error_combine in H. - break_match_hyps; try discriminate; []; Option.inversion_option; Prod.inversion_prod; subst. - cbv [Partition.partition] in *. - apply nth_error_map in Heqo; apply nth_error_map in Heqo0; destruct Heqo as (?&?&?), Heqo0 as (?&?&?). - rewrite nth_error_seq in *. - break_match_hyps; try discriminate; Option.inversion_option; Prod.inversion_prod; subst. - rewrite ?Nat.add_0_l. - assert (0 <= x < s) by lia. - replace s with (2^Z.log2 s) by easy. - assert (1 < s) by lia. - assert (0 < Z.log2 s) by now apply Z.log2_pos. - assert (1 < 2^Z.log2 s) by auto with zarith. - generalize dependent (Z.log2 s); intro lgs; intros. - - edestruct (UniformWeight.uwprops lgr); try lia. - assert (forall i : nat, 0 <= UniformWeight.uweight lgr i) by (intro z; specialize (weight_positive z); lia). - apply Bool.andb_true_intro; split; apply OrdersEx.Z_as_OT.leb_le; - [apply Z.div_nonneg | apply Z.div_le_mono_nonneg]; trivial. - apply Z.mod_pos_bound; trivial. - - cbv [UniformWeight.uweight]. - cbv [weight]. - rewrite Z.div_1_r. - rewrite Z.opp_involutive. - rewrite <-2Z.land_ones by nia. - rewrite Z.sub_1_r, <-Z.ones_equiv. - rewrite Z.land_ones_ones. - destruct ((lgs H end in - let H := fresh in - pose proof use_curve_good as H; - (* I want to just use [clear -H Hres], but then I can't use any lemmas in the section because of COQBUG(https://github.com/coq/coq/issues/8153) *) - repeat match goal with - | [ H' : _ |- _ ] - => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres | dont_clear H' ] - then fail - else clear H' - end; - cbv zeta in *; - destruct_head'_and; - let f := match type of Hres with ?f = _ => head f end in - try cbv [f] in *; - hnf; - PipelineTactics.do_unfolding; - try (let m := match goal with m := _ - Associational.eval _ |- _ => m end in - cbv [m] in * ); - intros; - lazymatch goal with - | [ |- _ <-> _ ] => idtac - | [ |- _ = _ ] => idtac - | _ => split; [ | try split ]; - cbv [small] - end; - PipelineTactics.use_compilers_correctness Hres; - repeat first [ reflexivity - | now apply bounded_by_of_valid - | now apply bounded_by_prime_bounds_of_valid - | now apply bounded_by_prime_bytes_bounds_of_bytes_valid - | now apply weight_bounded_of_bytes_valid - | solve [ eapply op_correct; try eassumption; solve_extra_bounds_side_conditions ] - | progress autorewrite with interp interp_gen_cache push_eval - | progress autounfold with push_eval - | progress autorewrite with distr_length in * - | solve [ cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto ] ]. - - (** TODO: DESIGN DECISION: - - The correctness lemmas for most of the montgomery things are - parameterized over a `from_montgomery`. When filling this in - for, e.g., mul-correctness, should I use `from_montgomery` - from arithmetic, or should I use `Interp - reified_from_montgomery` (the post-pipeline version), and take - in success of the pipeline on `from_montgomery` as well? *) - - Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). - - Lemma mul_correct res - (Hres : mul = Success res) - : mul_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness mulmod_correct. Qed. - - Lemma square_correct res - (Hres : square = Success res) - : square_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness squaremod_correct. Qed. - - Lemma add_correct res - (Hres : add = Success res) - : add_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness addmod_correct. Qed. - - Lemma sub_correct res - (Hres : sub = Success res) - : sub_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness submod_correct. Qed. - - Lemma opp_correct res - (Hres : opp = Success res) - : opp_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness oppmod_correct. Qed. - - Lemma from_montgomery_correct res - (Hres : from_montgomery = Success res) - : from_montgomery_correct machine_wordsize n m r' valid (Interp res). - Proof using curve_good. prove_correctness from_montgomerymod_correct. Qed. - - Lemma nonzero_correct res - (Hres : nonzero = Success res) - : nonzero_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness nonzeromod_correct. Qed. - - Lemma to_bytes_correct res - (Hres : to_bytes = Success res) - : to_bytes_correct machine_wordsize n n_bytes m valid (Interp res). - Proof using curve_good. prove_correctness to_bytesmod_correct. Qed. - - Lemma from_bytes_correct res - (Hres : from_bytes = Success res) - : from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid (Interp res). - Proof using curve_good. prove_correctness eval_from_bytesmod_and_partitions. Qed. - - Strategy -1000 [encode]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma encode_correct res - (Hres : encode = Success res) - : encode_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness encodemod_correct. Qed. - - Strategy -1000 [zero]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma zero_correct res - (Hres : zero = Success res) - : zero_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness encodemod_correct. Qed. - - Strategy -1000 [one]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) - Lemma one_correct res - (Hres : one = Success res) - : one_correct machine_wordsize n m valid from_montgomery_res (Interp res). - Proof using curve_good. prove_correctness encodemod_correct. Qed. - - Local Opaque Pipeline.BoundsPipeline. (* need this or else [eapply Pipeline.BoundsPipeline_correct in Hres] takes forever *) - Lemma selectznz_correct res - (Hres : selectznz = Success res) - : selectznz_correct machine_wordsize n saturated_bounds_list (Interp res). - Proof using curve_good. Primitives.prove_correctness use_curve_good. Qed. - - Section ring. - Context from_montgomery_res (Hfrom_montgomery : from_montgomery = Success from_montgomery_res) - mul_res (Hmul : mul = Success mul_res) - add_res (Hadd : add = Success add_res) - sub_res (Hsub : sub = Success sub_res) - opp_res (Hopp : opp = Success opp_res) - encode_res (Hencode : encode = Success encode_res) - zero_res (Hzero : zero = Success zero_res) - one_res (Hone : one = Success one_res). - - Definition GoodT : Prop - := GoodT - machine_wordsize n m valid - (Interp from_montgomery_res) - (Interp mul_res) - (Interp add_res) - (Interp sub_res) - (Interp opp_res) - (Interp encode_res) - (Interp zero_res) - (Interp one_res). - - Theorem Good : GoodT. - Proof using curve_good Hfrom_montgomery Hmul Hadd Hsub Hopp Hencode Hzero Hone. - pose proof use_curve_good; cbv zeta in *; destruct_head'_and. - eapply Good. - all: repeat first [ assumption - | apply from_montgomery_correct - | lia ]. - all: hnf; intros. - all: push_Zmod; erewrite !(fun v Hv => proj1 (from_montgomery_correct _ Hfrom_montgomery v Hv)), <- !eval_from_montgomerymod; try eassumption; pull_Zmod. - all: repeat first [ assumption - | lazymatch goal with - | [ |- context[mul_res] ] => apply mul_correct - | [ |- context[add_res] ] => apply add_correct - | [ |- context[sub_res] ] => apply sub_correct - | [ |- context[opp_res] ] => apply opp_correct - | [ |- context[encode_res] ] => apply encode_correct - | [ |- context[zero_res] ] => apply zero_correct - | [ |- context[one_res] ] => apply one_correct - end ]. - Qed. - End ring. - - Section for_stringification. - Local Open Scope string_scope. - Local Open Scope list_scope. - - Definition known_functions - := [("mul", smul); - ("square", ssquare); - ("add", sadd); - ("sub", ssub); - ("opp", sopp); - ("from_montgomery", sfrom_montgomery); - ("nonzero", snonzero); - ("selectznz", sselectznz); - ("to_bytes", sto_bytes); - ("from_bytes", sfrom_bytes)]. - - Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). - - (** Note: If you change the name or type signature of this - function, you will need to update the code in CLI.v *) - Definition Synthesize (function_name_prefix : string) (requests : list string) - : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) - := Primitives.Synthesize - machine_wordsize valid_names known_functions (fun _ => nil) - function_name_prefix requests. - End for_stringification. - End __. -End WordByWordMontgomery. - -Module Import InvertHighLow. - Section with_wordmax. - Context (log2wordmax : Z) (consts : list Z). - Let wordmax := 2 ^ log2wordmax. - Let half_bits := log2wordmax / 2. - Let wordmax_half_bits := 2 ^ half_bits. - - Inductive kind_of_constant := upper_half (c : BinInt.Z) | lower_half (c : BinInt.Z). - - Definition constant_to_scalar_single (const x : BinInt.Z) : option kind_of_constant := - if x =? (BinInt.Z.shiftr const half_bits) - then Some (upper_half const) - else if x =? (BinInt.Z.land const (wordmax_half_bits - 1)) - then Some (lower_half const) - else None. - - Definition constant_to_scalar (x : BinInt.Z) - : option kind_of_constant := - fold_right (fun c res => match res with - | Some s => Some s - | None => constant_to_scalar_single c x - end) None consts. - - Definition invert_low (v : BinInt.Z) : option BinInt.Z - := match constant_to_scalar v with - | Some (lower_half v) => Some v - | _ => None - end. - - Definition invert_high (v : BinInt.Z) : option BinInt.Z - := match constant_to_scalar v with - | Some (upper_half v) => Some v - | _ => None - end. - End with_wordmax. -End InvertHighLow. - -(** TODO: Port Barrett and Montgomery to the new glue style, and remove these tactics. These tactics are only needed for the old-glue-style derivations. *) -Require Import Crypto.Util.Equality. (* fg_equal_rel *) -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Tactics.GetGoal. -Ltac peel_interp_app _ := - lazymatch goal with - | [ |- ?R' (?InterpE ?arg) (?f ?arg) ] - => apply fg_equal_rel; [ | reflexivity ]; - try peel_interp_app () - | [ |- ?R' (Interp ?ev) (?f ?x) ] - => let sv := type of x in - let fx := constr:(f x) in - let dv := type of fx in - let rs := reify_type sv in - let rd := reify_type dv in - etransitivity; - [ apply @expr.Interp_APP_rel_reflexive with (s:=rs) (d:=rd) (R:=R'); - typeclasses eauto - | apply fg_equal_rel; - [ try peel_interp_app () - | try lazymatch goal with - | [ |- ?R (Interp ?ev) (Interp _) ] - => reflexivity - | [ |- ?R (Interp ?ev) ?c ] - => let rc := constr:(GallinaReify.Reify c) in - unify ev rc; vm_compute; reflexivity - end ] ] - end. -Ltac pre_cache_reify _ := - let H' := fresh in - lazymatch goal with - | [ |- ?P /\ Wf ?e ] - => let P' := fresh in - evar (P' : Prop); - assert (H' : P' /\ Wf e); subst P' - end; - [ - | split; [ destruct H' as [H' _] | destruct H' as [_ H']; exact H' ]; - cbv [type.app_curried]; - let arg := fresh "arg" in - let arg2 := fresh in - intros arg arg2; - cbn [type.and_for_each_lhs_of_arrow type.eqv]; - let H := fresh in - intro H; - repeat match type of H with - | and _ _ => let H' := fresh in - destruct H as [H' H]; - rewrite <- H' - end; - clear dependent arg2; clear H; - intros _; - peel_interp_app (); - [ lazymatch goal with - | [ |- ?R (Interp ?ev) _ ] - => (tryif is_evar ev - then let ev' := fresh "ev" in set (ev' := ev) - else idtac) - end; - cbv [pointwise_relation]; - repeat lazymatch goal with - | [ H : _ |- _ ] => first [ constr_eq H H'; fail 1 - | revert H ] - end; - eexact H' - | .. ] ]; - [ intros; clear | .. ]. -Ltac do_inline_cache_reify do_if_not_cached := - pre_cache_reify (); - [ try solve [ - cbv beta zeta; - repeat match goal with H := ?e |- _ => is_evar e; subst H end; - try solve [ split; [ solve [ eauto with nocore reify_gen_cache ] | solve [ eauto with wf_gen_cache; prove_Wf () ] ] ]; - do_if_not_cached () - ]; - cache_reify () - | .. ]. - -(* TODO: MOVE ME *) -Ltac vm_compute_lhs_reflexivity := - lazymatch goal with - | [ |- ?LHS = ?RHS ] - => let x := (eval vm_compute in LHS) in - (* we cannot use the unify tactic, which just gives "not - unifiable" as the error message, because we want to see the - terms that were not unifable. See also - COQBUG(https://github.com/coq/coq/issues/7291) *) - let _unify := constr:(ltac:(reflexivity) : RHS = x) in - vm_cast_no_check (eq_refl x) - end. - -Ltac solve_rop' rop_correct do_if_not_cached machine_wordsizev := - eapply rop_correct with (machine_wordsize:=machine_wordsizev); - [ do_inline_cache_reify do_if_not_cached - | subst_evars; vm_compute_lhs_reflexivity (* lazy; reflexivity *) ]. -Ltac solve_rop_nocache rop_correct := - solve_rop' rop_correct ltac:(fun _ => idtac). -Ltac solve_rop rop_correct := - solve_rop' - rop_correct - ltac:(fun _ => let G := get_goal in fail 2 "Could not find a solution in reify_gen_cache for" G). - -Module BarrettReduction. - (* TODO : generalize to multi-word and operate on (list Z) instead of T; maybe stop taking ops as context variables *) - Section Generic. - Context {T} (rep : T -> Z -> Prop) - (k : Z) (k_pos : 0 < k) - (low : T -> Z) - (low_correct : forall a x, rep a x -> low a = x mod 2 ^ k) - (shiftr : T -> Z -> T) - (shiftr_correct : forall a x n, - rep a x -> - 0 <= n <= k -> - rep (shiftr a n) (x / 2 ^ n)) - (mul_high : T -> T -> Z -> T) - (mul_high_correct : forall a b x y x0y1, - rep a x -> - rep b y -> - 2 ^ k <= x < 2^(k+1) -> - 0 <= y < 2^(k+1) -> - x0y1 = x mod 2 ^ k * (y / 2 ^ k) -> - rep (mul_high a b x0y1) (x * y / 2 ^ k)) - (mul : Z -> Z -> T) - (mul_correct : forall x y, - 0 <= x < 2^k -> - 0 <= y < 2^k -> - rep (mul x y) (x * y)) - (sub : T -> T -> T) - (sub_correct : forall a b x y, - rep a x -> - rep b y -> - 0 <= x - y < 2^k * 2^k -> - rep (sub a b) (x - y)) - (cond_sub1 : T -> Z -> Z) - (cond_sub1_correct : forall a x y, - rep a x -> - 0 <= x < 2 * y -> - 0 <= y < 2 ^ k -> - cond_sub1 a y = if (x Z -> Z) - (cond_sub2_correct : forall x y, cond_sub2 x y = if (x - 0 <= x < 2 * M -> - cond_sub2 (cond_sub1 a M) M = cond_sub2 (cond_sub2 x M) M. - Proof. - intros. - erewrite !cond_sub2_correct, !cond_sub1_correct by (eassumption || omega). - break_match; Z.ltb_to_lt; try lia; discriminate. - Qed. - - Lemma r_bounds : 0 <= x - q * M < 2 * M. - Proof. - pose proof looser_bound. pose proof q_bounds. pose proof x_mod_small. - subst q mu; split. - { Z.zero_bounds. apply qn_small; omega. } - { apply r_small_strong; rewrite ?Z.pow_1_r; auto; omega. } - Qed. - - Lemma reduce_correct : reduce = x mod M. - Proof. - pose proof looser_bound. pose proof r_bounds. pose proof q_bounds. - assert (2 * M < 2^k * 2^k) by nia. - rewrite barrett_reduction_small with (k:=k) (m:=mu) (offset:=1) (b:=2) by (auto; omega). - cbv [reduce Let_In]. - erewrite low_correct by eauto. Z.rewrite_mod_small. - erewrite two_conditional_subtracts by solve_rep. - rewrite !cond_sub2_correct. - subst q; reflexivity. - Qed. - End Generic. - - Section BarrettReduction. - Context (k : Z) (k_bound : 2 <= k). - Context (M muLow : Z). - Context (M_pos : 0 < M) - (muLow_eq : muLow + 2^k = 2^(2*k) / M) - (muLow_bounds : 0 <= muLow < 2^k) - (M_bound1 : 2 ^ (k - 1) < M < 2^k) - (M_bound2: 2 * (2 ^ (2 * k) mod M) <= 2 ^ (k + 1) - (muLow + 2^k)). - - Context (n:nat) (Hn_nz: n <> 0%nat) (n_le_k : Z.of_nat n <= k). - Context (nout : nat) (Hnout : nout = 2%nat). - Let w := weight k 1. - Local Lemma k_range : 0 < 1 <= k. Proof. omega. Qed. - Let props : @weight_properties w := wprops k 1 k_range. - - Hint Rewrite Positional.eval_nil Positional.eval_snoc : push_eval. - - Definition low (t : list Z) : Z := nth_default 0 t 0. - Definition high (t : list Z) : Z := nth_default 0 t 1. - Definition represents (t : list Z) (x : Z) := - t = [x mod 2^k; x / 2^k] /\ 0 <= x < 2^k * 2^k. - - Lemma represents_eq t x : - represents t x -> t = [x mod 2^k; x / 2^k]. - Proof. cbv [represents]; tauto. Qed. - - Lemma represents_length t x : represents t x -> length t = 2%nat. - Proof. cbv [represents]; intuition. subst t; reflexivity. Qed. - - Lemma represents_low t x : - represents t x -> low t = x mod 2^k. - Proof. cbv [represents]; intros; rewrite (represents_eq t x) by auto; reflexivity. Qed. - - Lemma represents_high t x : - represents t x -> high t = x / 2^k. - Proof. cbv [represents]; intros; rewrite (represents_eq t x) by auto; reflexivity. Qed. - - Lemma represents_low_range t x : - represents t x -> 0 <= x mod 2^k < 2^k. - Proof. auto with zarith. Qed. - - Lemma represents_high_range t x : - represents t x -> 0 <= x / 2^k < 2^k. - Proof. - destruct 1 as [? [? ?] ]; intros. - auto using Z.div_lt_upper_bound with zarith. - Qed. - Hint Resolve represents_length represents_low_range represents_high_range. - - Lemma represents_range t x : - represents t x -> 0 <= x < 2^k*2^k. - Proof. cbv [represents]; tauto. Qed. - - Lemma represents_id x : - 0 <= x < 2^k * 2^k -> - represents [x mod 2^k; x / 2^k] x. - Proof. - intros; cbv [represents]; autorewrite with cancel_pair. - Z.rewrite_mod_small; tauto. - Qed. - - Local Ltac push_rep := - repeat match goal with - | H : represents ?t ?x |- _ => unique pose proof (represents_low_range _ _ H) - | H : represents ?t ?x |- _ => unique pose proof (represents_high_range _ _ H) - | H : represents ?t ?x |- _ => rewrite (represents_low t x) in * by assumption - | H : represents ?t ?x |- _ => rewrite (represents_high t x) in * by assumption - end. - - Definition shiftr (t : list Z) (n : Z) : list Z := - [Z.rshi (2^k) (high t) (low t) n; Z.rshi (2^k) 0 (high t) n]. - - Lemma shiftr_represents a i x : - represents a x -> - 0 <= i <= k -> - represents (shiftr a i) (x / 2 ^ i). - Proof. - cbv [shiftr]; intros; push_rep. - match goal with H : _ |- _ => pose proof (represents_range _ _ H) end. - assert (0 < 2 ^ i) by auto with zarith. - assert (x < 2 ^ i * 2 ^ k * 2 ^ k) by nia. - assert (0 <= x / 2 ^ k / 2 ^ i < 2 ^ k) by - (split; Z.zero_bounds; auto using Z.div_lt_upper_bound with zarith). - repeat match goal with - | _ => rewrite Z.rshi_correct by auto with zarith - | _ => rewrite <-Z.div_mod''' by auto with zarith - | _ => progress autorewrite with zsimplify_fast - | _ => progress Z.rewrite_mod_small - | |- context [represents [(?a / ?c) mod ?b; ?a / ?b / ?c] ] => - rewrite (Z.div_div_comm a b c) by auto with zarith - | _ => solve [auto using represents_id, Z.div_lt_upper_bound with zarith lia] - end. - Qed. - - Context (Hw : forall i, w i = (2 ^ k) ^ Z.of_nat i). - Ltac change_weight := rewrite !Hw, ?Z.pow_0_r, ?Z.pow_1_r, ?Z.pow_2_r. - - Definition wideadd t1 t2 := fst (Rows.add w 2 t1 t2). - (* TODO: use this definition once issue #352 is resolved *) - (* Definition widesub t1 t2 := fst (Rows.sub w 2 t1 t2). *) - Definition widesub (t1 t2 : list Z) := - let t1_0 := hd 0 t1 in - let t1_1 := hd 0 (tl t1) in - let t2_0 := hd 0 t2 in - let t2_1 := hd 0 (tl t2) in - dlet_nd x0 := Z.sub_get_borrow_full (2^k) t1_0 t2_0 in - dlet_nd x1 := Z.sub_with_get_borrow_full (2^k) (snd x0) t1_1 t2_1 in - [fst x0; fst x1]. - Definition widemul := BaseConversion.widemul_inlined k n nout. - - Lemma partition_represents x : - 0 <= x < 2^k*2^k -> - represents (Partition.partition w 2 x) x. - Proof. - intros; cbn. change_weight. - Z.rewrite_mod_small. - autorewrite with zsimplify_fast. - auto using represents_id. - Qed. - - Lemma eval_represents t x : - represents t x -> eval w 2 t = x. - Proof. - intros; rewrite (represents_eq t x) by assumption. - cbn. change_weight; push_rep. - autorewrite with zsimplify. reflexivity. - Qed. - - Ltac wide_op partitions_pf := - repeat match goal with - | _ => rewrite partitions_pf by eauto - | _ => rewrite partitions_pf by auto with zarith - | _ => erewrite eval_represents by eauto - | _ => solve [auto using partition_represents, represents_id] - end. - - Lemma wideadd_represents t1 t2 x y : - represents t1 x -> - represents t2 y -> - 0 <= x + y < 2^k*2^k -> - represents (wideadd t1 t2) (x + y). - Proof. intros; cbv [wideadd]. wide_op Rows.add_partitions. Qed. - - Lemma widesub_represents t1 t2 x y : - represents t1 x -> - represents t2 y -> - 0 <= x - y < 2^k*2^k -> - represents (widesub t1 t2) (x - y). - Proof. - intros; cbv [widesub Let_In]. - rewrite (represents_eq t1 x) by assumption. - rewrite (represents_eq t2 y) by assumption. - cbn [hd tl]. - autorewrite with to_div_mod. - pull_Zmod. - match goal with |- represents [?m; ?d] ?x => - replace d with (x / 2 ^ k); [solve [auto using represents_id] |] end. - rewrite <-(Z.mod_small ((x - y) / 2^k) (2^k)) by (split; try apply Z.div_lt_upper_bound; Z.zero_bounds). - f_equal. - transitivity ((x mod 2^k - y mod 2^k + 2^k * (x / 2 ^ k) - 2^k * (y / 2^k)) / 2^k). { - rewrite (Z.div_mod x (2^k)) at 1 by auto using Z.pow_nonzero with omega. - rewrite (Z.div_mod y (2^k)) at 1 by auto using Z.pow_nonzero with omega. - f_equal. ring. } - autorewrite with zsimplify. - ring. - Qed. - (* Works with Rows.sub-based widesub definition - Proof. intros; cbv [widesub]. wide_op Rows.sub_partitions. Qed. - *) - - (* TODO: MOVE Equivlalent Keys decl to Arithmetic? *) - Declare Equivalent Keys BaseConversion.widemul BaseConversion.widemul_inlined. - Lemma widemul_represents x y : - 0 <= x < 2^k -> - 0 <= y < 2^k -> - represents (widemul x y) (x * y). - Proof. - intros; cbv [widemul]. - assert (0 <= x * y < 2^k*2^k) by auto with zarith. - wide_op BaseConversion.widemul_correct. - Qed. - - Definition mul_high (a b : list Z) a0b1 : list Z := - dlet_nd a0b0 := widemul (low a) (low b) in - dlet_nd ab := wideadd [high a0b0; high b] [low b; 0] in - wideadd ab [a0b1; 0]. - - Lemma mul_high_idea d a b a0 a1 b0 b1 : - d <> 0 -> - a = d * a1 + a0 -> - b = d * b1 + b0 -> - (a * b) / d = a0 * b0 / d + d * a1 * b1 + a1 * b0 + a0 * b1. - Proof. - intros. subst a b. autorewrite with push_Zmul. - ring_simplify_subterms. rewrite Z.pow_2_r. - rewrite Z.div_add_exact by (push_Zmod; autorewrite with zsimplify; omega). - repeat match goal with - | |- context [d * ?a * ?b * ?c] => - replace (d * a * b * c) with (a * b * c * d) by ring - | |- context [d * ?a * ?b] => - replace (d * a * b) with (a * b * d) by ring - end. - rewrite !Z.div_add by omega. - autorewrite with zsimplify. - rewrite (Z.mul_comm a0 b0). - ring_simplify. ring. - Qed. - - Lemma represents_trans t x y: - represents t y -> y = x -> - represents t x. - Proof. congruence. Qed. - - Lemma represents_add x y : - 0 <= x < 2 ^ k -> - 0 <= y < 2 ^ k -> - represents [x;y] (x + 2^k*y). - Proof. - intros; cbv [represents]; autorewrite with zsimplify. - repeat split; (reflexivity || nia). - Qed. - - Lemma represents_small x : - 0 <= x < 2^k -> - represents [x; 0] x. - Proof. - intros. - eapply represents_trans. - { eauto using represents_add with zarith. } - { ring. } - Qed. - - Lemma mul_high_represents a b x y a0b1 : - represents a x -> - represents b y -> - 2^k <= x < 2^(k+1) -> - 0 <= y < 2^(k+1) -> - a0b1 = x mod 2^k * (y / 2^k) -> - represents (mul_high a b a0b1) ((x * y) / 2^k). - Proof. - cbv [mul_high Let_In]; rewrite Z.pow_add_r, Z.pow_1_r by omega; intros. - assert (4 <= 2 ^ k) by (transitivity (Z.pow 2 2); auto with zarith). - assert (0 <= x * y / 2^k < 2^k*2^k) by (Z.div_mod_to_quot_rem_in_goal; nia). - - rewrite mul_high_idea with (a:=x) (b:=y) (a0 := low a) (a1 := high a) (b0 := low b) (b1 := high b) in * - by (push_rep; Z.div_mod_to_quot_rem_in_goal; lia). - - push_rep. subst a0b1. - assert (y / 2 ^ k < 2) by (apply Z.div_lt_upper_bound; omega). - replace (x / 2 ^ k) with 1 in * by (rewrite Z.div_between_1; lia). - autorewrite with zsimplify_fast in *. - - eapply represents_trans. - { repeat (apply wideadd_represents; - [ | apply represents_small; Z.div_mod_to_quot_rem_in_goal; nia| ]). - erewrite represents_high; [ | apply widemul_represents; solve [ auto with zarith ] ]. - { apply represents_add; try reflexivity; solve [auto with zarith]. } - { match goal with H : 0 <= ?x + ?y < ?z |- 0 <= ?x < ?z => - split; [ solve [Z.zero_bounds] | ]; - eapply Z.le_lt_trans with (m:= x + y); nia - end. } - { omega. } } - { ring. } - Qed. - - Definition cond_sub1 (a : list Z) y : Z := - dlet_nd maybe_y := Z.zselect (Z.cc_l (high a)) 0 y in - dlet_nd diff := Z.sub_get_borrow_full (2^k) (low a) maybe_y in - fst diff. - - Lemma cc_l_only_bit : forall x s, 0 <= x < 2 * s -> Z.cc_l (x / s) = 0 <-> x < s. - Proof. - cbv [Z.cc_l]; intros. - rewrite Z.div_between_0_if by omega. - break_match; Z.ltb_to_lt; Z.rewrite_mod_small; omega. - Qed. - - Lemma cond_sub1_correct a x y : - represents a x -> - 0 <= x < 2 * y -> - 0 <= y < 2 ^ k -> - cond_sub1 a y = if (x 0) by auto with zarith. - assert (2 < 2 ^ k) by (eapply Z.le_lt_trans with (m:=2 ^ 1); auto with zarith). - - cbv [muSelect]. rewrite <-muLow_eq. - rewrite Z.zselect_correct, Z.cc_m_eq by auto with zarith. - replace xHigh with (x / 2^k) by (subst x; autorewrite with zsimplify; lia). - autorewrite with pull_Zdiv push_Zpow. - rewrite (Z.mul_comm (2 ^ k / 2)). - break_match; [ ring | ]. - match goal with H : 0 <= ?x < 2, H' : ?x <> 0 |- _ => replace x with 1 by omega end. - autorewrite with zsimplify; reflexivity. - Qed. - - Lemma mu_rep : represents [muLow; 1] (2 ^ (2 * k) / M). - Proof. rewrite <-muLow_eq. eapply represents_trans; auto with zarith. Qed. - - Derive barrett_reduce - SuchThat (barrett_reduce = x mod M) - As barrett_reduce_correct. - Proof. - erewrite <-reduce_correct with (rep:=represents) (muSelect:=muSelect) (k0:=k) (mut:=[muLow;1]) (xt0:=xt) - by (auto using x_bounds, muSelect_correct, x_rep, mu_rep; omega). - subst barrett_reduce. reflexivity. - Qed. - End Defn. - End BarrettReduction. - - (* all the list operations from for_reification.ident *) - Strategy 100 [length seq repeat combine map flat_map partition app rev fold_right update_nth nth_default ]. - Strategy -10 [barrett_reduce reduce]. - - Derive reified_barrett_red_gen - SuchThat (is_reification_of reified_barrett_red_gen barrett_reduce) - As reified_barrett_red_gen_correct. - Proof. Time cache_reify (). Time Qed. - - Module Export ReifyHints. - Hint Extern 1 (_ = _) => apply_cached_reification barrett_reduce (proj1 reified_barrett_red_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_barrett_red_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_barrett_red_gen_correct) : interp_gen_cache. - End ReifyHints. - Local Opaque reified_barrett_red_gen. (* needed for making [autorewrite] not take a very long time *) - - Section rbarrett_red. - Context (M : Z) - (machine_wordsize : Z). - - Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange. - Let flag_range := r[0 ~> 1]%zrange. - Let bound := Some value_range. - Let mu := (2 ^ (2 * machine_wordsize)) / M. - Let muLow := mu mod (2 ^ machine_wordsize). - Let consts_list := [M; muLow]. - - Definition possible_values_of_machine_wordsize - := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. - Let possible_values := possible_values_of_machine_wordsize. - - Definition check_args {T} (res : Pipeline.ErrorT T) - : Pipeline.ErrorT T - := fold_right - (fun '(b, e) k => if b:bool then Error e else k) - res - [((mu / (2 ^ machine_wordsize) =? 0), Pipeline.Values_not_provably_distinctZ "mu / 2 ^ k ≠ 0" (mu / 2 ^ machine_wordsize) 0); - ((machine_wordsize (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) - /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) - | None => True - end. - Proof. - cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; - split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. - Qed. - - Definition barrett_red - := Pipeline.BoundsPipeline - false (* subst01 *) - fancy_args (* fancy *) - possible_values - (reified_barrett_red_gen - @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify M @ GallinaReify.Reify muLow @ GallinaReify.Reify 2%nat @ GallinaReify.Reify 2%nat) - (bound, (bound, tt)) - bound. - - Definition sbarrett_red (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "barrett_red" barrett_red. - - (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like -<< -Lemma barrett_red_correct res - (Hres : barrett_red = Success res) - : barrett_red_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. ->> *) - - Notation BoundsPipeline_correct in_bounds out_bounds op - := (fun rv (rop : Expr (reify_type_of op)) Hrop - => @Pipeline.BoundsPipeline_correct_trans - false (* subst01 *) - fancy_args - fancy_args_good - possible_values - _ - rop - in_bounds - out_bounds - _ - op - Hrop rv) - (only parsing). - - Definition rbarrett_red_correct - := BoundsPipeline_correct - (bound, (bound, tt)) - bound - (barrett_reduce machine_wordsize M muLow 2 2). - - Notation type_of_strip_3arrow := ((fun (d : Prop) (_ : forall A B C, d) => d) _). - Definition rbarrett_red_correctT rv : Prop - := type_of_strip_3arrow (@rbarrett_red_correct rv). - End rbarrett_red. -End BarrettReduction. - -(* TODO: After moving to new-glue-style, remove these tactics *) -Ltac solve_rbarrett_red := solve_rop BarrettReduction.rbarrett_red_correct. -Ltac solve_rbarrett_red_nocache := solve_rop_nocache BarrettReduction.rbarrett_red_correct. - -Module MontgomeryReduction. - Section MontRed'. - Context (N R N' R' : Z). - Context (HN_range : 0 <= N < R) (HN'_range : 0 <= N' < R) (HN_nz : N <> 0) (R_gt_1 : R > 1) - (N'_good : Z.equiv_modulo R (N*N') (-1)) (R'_good: Z.equiv_modulo N (R*R') 1). - - Context (Zlog2R : Z) . - Let w : nat -> Z := weight Zlog2R 1. - Context (n:nat) (Hn_nz: n <> 0%nat) (n_good : Zlog2R mod Z.of_nat n = 0). - Context (R_big_enough : n <= Zlog2R) - (R_two_pow : 2^Zlog2R = R). - Let w_mul : nat -> Z := weight (Zlog2R / n) 1. - Context (nout : nat) (Hnout : nout = 2%nat). - - Definition montred' (lo hi : Z) := - dlet_nd y := nth_default 0 (BaseConversion.widemul_inlined Zlog2R n nout lo N') 0 in - dlet_nd t1_t2 := (BaseConversion.widemul_inlined_reverse Zlog2R n nout N y) in - dlet_nd sum_carry := Rows.add (weight Zlog2R 1) 2 [lo;hi] t1_t2 in - dlet_nd y' := Z.zselect (snd sum_carry) 0 N in - dlet_nd lo''_carry := Z.sub_get_borrow_full R (nth_default 0 (fst sum_carry) 1) y' in - Z.add_modulo (fst lo''_carry) 0 N. - - Local Lemma Hw : forall i, w i = R ^ Z.of_nat i. - Proof. - clear -R_big_enough R_two_pow; cbv [w weight]; intro. - autorewrite with zsimplify. - rewrite Z.pow_mul_r, R_two_pow by omega; reflexivity. - Qed. - - Declare Equivalent Keys weight w. - Local Ltac change_weight := rewrite !Hw, ?Z.pow_0_r, ?Z.pow_1_r, ?Z.pow_2_r, ?Z.pow_1_l in *. - Local Ltac solve_range := - repeat match goal with - | _ => progress change_weight - | |- context [?a mod ?b] => unique pose proof (Z.mod_pos_bound a b ltac:(omega)) - | |- 0 <= _ => progress Z.zero_bounds - | |- 0 <= _ * _ < _ * _ => - split; [ solve [Z.zero_bounds] | apply Z.mul_lt_mono_nonneg; omega ] - | _ => solve [auto] - | _ => omega - end. - - Local Lemma eval2 x y : eval w 2 [x;y] = x + R * y. - Proof. cbn. change_weight. ring. Qed. - - Hint Rewrite BaseConversion.widemul_inlined_reverse_correct BaseConversion.widemul_inlined_correct - using (autorewrite with widemul push_nth_default; solve [solve_range]) : widemul. - - Lemma montred'_eq lo hi T (HT_range: 0 <= T < R * N) - (Hlo: lo = T mod R) (Hhi: hi = T / R): - montred' lo hi = reduce_via_partial N R N' T. - Proof. - rewrite <-reduce_via_partial_alt_eq by nia. - cbv [montred' partial_reduce_alt reduce_via_partial_alt prereduce Let_In]. - rewrite Hlo, Hhi. - assert (0 <= (T mod R) * N' < w 2) by (solve_range). - - autorewrite with widemul. - rewrite Rows.add_partitions, Rows.add_div by (distr_length; apply wprops; omega). - rewrite R_two_pow. - cbv [Partition.partition seq]. rewrite !eval2. - autorewrite with push_nth_default push_map. - autorewrite with to_div_mod. rewrite ?Z.zselect_correct, ?Z.add_modulo_correct. - change_weight. - - (* pull out value before last modular reduction *) - match goal with |- (if (?n <=? ?x)%Z then ?x - ?n else ?x) = (if (?n <=? ?y) then ?y - ?n else ?y)%Z => - let P := fresh "H" in assert (x = y) as P; [|rewrite P; reflexivity] end. - - autorewrite with zsimplify. - rewrite (Z.mul_comm (((T mod R) * N') mod R) N) in *. - break_match; try reflexivity; Z.ltb_to_lt; rewrite Z.div_small_iff in * by omega; - repeat match goal with - | _ => progress autorewrite with zsimplify_fast - | |- context [?x mod (R * R)] => - unique pose proof (Z.mod_pos_bound x (R * R)); - try rewrite (Z.mod_small x (R * R)) in * by Z.rewrite_mod_small_solver - | _ => omega - | _ => progress Z.rewrite_mod_small - end. - Qed. - - Lemma montred'_correct lo hi T (HT_range: 0 <= T < R * N) - (Hlo: lo = T mod R) (Hhi: hi = T / R): montred' lo hi = (T * R') mod N. - Proof. - erewrite montred'_eq by eauto. - apply Z.equiv_modulo_mod_small; auto using reduce_via_partial_correct. - replace 0 with (Z.min 0 (R-N)) by (apply Z.min_l; omega). - apply reduce_via_partial_in_range; omega. - Qed. - End MontRed'. - - Derive reified_montred_gen - SuchThat (is_reification_of reified_montred_gen montred') - As reified_montred_gen_correct. - Proof. Time cache_reify (). Time Qed. - Module Export ReifyHints. - Hint Extern 1 (_ = _) => apply_cached_reification montred' (proj1 reified_montred_gen_correct) : reify_cache_gen. - Hint Immediate (proj2 reified_montred_gen_correct) : wf_gen_cache. - Hint Rewrite (proj1 reified_montred_gen_correct) : interp_gen_cache. - End ReifyHints. - Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *) - - Section rmontred. - Context (N R N' : Z) - (machine_wordsize : Z). - - Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange. - Let flag_range := r[0 ~> 1]%zrange. - Let bound := Some value_range. - Let consts_list := [N; N']. - - Definition possible_values_of_machine_wordsize - := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. - Local Arguments possible_values_of_machine_wordsize / . - - Let possible_values := possible_values_of_machine_wordsize. - - Definition check_args {T} (res : Pipeline.ErrorT T) - : Pipeline.ErrorT T - := res. (* TODO: this should actually check stuff that corresponds with preconditions of montred'_correct *) - - Let fancy_args - := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list; - Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list; - Pipeline.value_range := value_range; - Pipeline.flag_range := flag_range |}). - - Lemma fancy_args_good - : match fancy_args with - | Some {| Pipeline.invert_low := il ; Pipeline.invert_high := ih |} - => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) - /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) - | None => True - end. - Proof. - cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; - split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. - Qed. - - Print montred'. - Definition montred - := Pipeline.BoundsPipeline - false (* subst01 *) - fancy_args (* fancy *) - possible_values - (reified_montred_gen - @ GallinaReify.Reify N @ GallinaReify.Reify R @ GallinaReify.Reify N' @ GallinaReify.Reify (Z.log2 R) @ GallinaReify.Reify 2%nat @ GallinaReify.Reify 2%nat) - (bound, (bound, tt)) - bound. - - Definition smontred (prefix : string) - : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) - := Eval cbv beta in FromPipelineToString prefix "montred" montred. - - (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like -<< -Lemma montred_correct res - (Hres : montred = Success res) - : montred_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). - Proof using curve_good. prove_correctness (). Qed. ->> *) - - Notation BoundsPipeline_correct in_bounds out_bounds op - := (fun rv (rop : Expr (reify_type_of op)) Hrop - => @Pipeline.BoundsPipeline_correct_trans - false (* subst01 *) - fancy_args - fancy_args_good - possible_values - _ - rop - in_bounds - out_bounds - _ - op - Hrop rv) - (only parsing). - - Definition rmontred_correct - := BoundsPipeline_correct - (bound, (bound, tt)) - bound - (montred' N R N' (Z.log2 R) 2 2). - - Notation type_of_strip_3arrow := ((fun (d : Prop) (_ : forall A B C, d) => d) _). - Definition rmontred_correctT rv : Prop - := type_of_strip_3arrow (@rmontred_correct rv). - End rmontred. -End MontgomeryReduction. - -(* TODO: After moving to new-glue-style, remove these tactics *) -Ltac solve_rmontred := solve_rop MontgomeryReduction.rmontred_correct. -Ltac solve_rmontred_nocache := solve_rop_nocache MontgomeryReduction.rmontred_correct. - - -Time Compute - (Pipeline.BoundsPipeline - true None [64; 128] - ltac:(let r := Reify (to_associational (weight 51 1) 5) in - exact r) - (Some (repeat (@None _) 5), tt) - ZRange.type.base.option.None). - -Time Compute - (Pipeline.BoundsPipeline - true None [64; 128] - ltac:(let r := Reify (scmul (weight 51 1) 5) in - exact r) - (None, (Some (repeat (@None _) 5), tt)) - ZRange.type.base.option.None). - -Compute - (Pipeline.BoundsPipeline - true None [64; 128] - ltac:(let r := Reify (fun f => carry_mulmod 51 1 (2^255) [(1,19)] 5 (seq 0 5 ++ [0; 1])%list%nat f f) in - exact r) - (Some (repeat (@None _) 5), tt) - ZRange.type.base.option.None). - -Compute - (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_mulx_u64" [] - true None [64; 128] - ltac:(let r := Reify (Arithmetic.mulx 64) in - exact r) - (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange - (Some r[0~>2^64-1], Some r[0~>2^64-1])%zrange). - -Compute - (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u64" [] - true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.addcarryx 64) in - exact r) - (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange - (Some r[0~>2^64-1], Some r[0~>1])%zrange). - -Compute - (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_addcarryx_u51" [] - true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.addcarryx 51) in - exact r) - (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange - (Some r[0~>2^51-1], Some r[0~>1])%zrange). - -Compute - (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u64" [] - true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.subborrowx 64) in - exact r) - (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange - (Some r[0~>2^64-1], Some r[0~>1])%zrange). -Compute - (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_subborrowx_u51" [] - true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.subborrowx 51) in - exact r) - (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange - (Some r[0~>2^51-1], Some r[0~>1])%zrange). - -Compute - (Pipeline.BoundsPipelineToString - true "fiat_" "fiat_cmovznz64" [] - true None [1; 64; 128] - ltac:(let r := Reify (Arithmetic.cmovznz 64) in - exact r) - (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange - (Some r[0~>2^64-1])%zrange). diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v new file mode 100644 index 000000000..3e3e4e105 --- /dev/null +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -0,0 +1,133 @@ +(** * Push-Button Synthesis of Barrett Reduction *) +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.BarrettReductionReificationCache. +Require Import Crypto.PushButtonSynthesis.InvertHighLow. +Require Import Crypto.PushButtonSynthesis.LegacySynthesisTactics. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. + +Import Associational Positional Arithmetic.BarrettReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Local Opaque reified_barrett_red_gen. (* needed for making [autorewrite] not take a very long time *) + +Section rbarrett_red. + Context (M : Z) + (machine_wordsize : Z). + + Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange. + Let flag_range := r[0 ~> 1]%zrange. + Let bound := Some value_range. + Let mu := (2 ^ (2 * machine_wordsize)) / M. + Let muLow := mu mod (2 ^ machine_wordsize). + Let consts_list := [M; muLow]. + + Definition possible_values_of_machine_wordsize + := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. + Let possible_values := possible_values_of_machine_wordsize. + + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [((mu / (2 ^ machine_wordsize) =? 0), Pipeline.Values_not_provably_distinctZ "mu / 2 ^ k ≠ 0" (mu / 2 ^ machine_wordsize) 0); + ((machine_wordsize (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end. + Proof. + cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; + split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. + Qed. + + Definition barrett_red + := Pipeline.BoundsPipeline + false (* subst01 *) + fancy_args (* fancy *) + possible_values + (reified_barrett_red_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify M @ GallinaReify.Reify muLow @ GallinaReify.Reify 2%nat @ GallinaReify.Reify 2%nat) + (bound, (bound, tt)) + bound. + + Definition sbarrett_red (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "barrett_red" barrett_red. + + (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like +<< +Lemma barrett_red_correct res + (Hres : barrett_red = Success res) + : barrett_red_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. +>> *) + + Notation BoundsPipeline_correct in_bounds out_bounds op + := (fun rv (rop : Expr (reify_type_of op)) Hrop + => @Pipeline.BoundsPipeline_correct_trans + false (* subst01 *) + fancy_args + fancy_args_good + possible_values + _ + rop + in_bounds + out_bounds + _ + op + Hrop rv) + (only parsing). + + Definition rbarrett_red_correct + := BoundsPipeline_correct + (bound, (bound, tt)) + bound + (barrett_reduce machine_wordsize M muLow 2 2). + + Notation type_of_strip_3arrow := ((fun (d : Prop) (_ : forall A B C, d) => d) _). + Definition rbarrett_red_correctT rv : Prop + := type_of_strip_3arrow (@rbarrett_red_correct rv). +End rbarrett_red. + +(* TODO: After moving to new-glue-style, remove these tactics *) +Ltac solve_rbarrett_red := solve_rop rbarrett_red_correct. +Ltac solve_rbarrett_red_nocache := solve_rop_nocache rbarrett_red_correct. diff --git a/src/PushButtonSynthesis/BarrettReductionReificationCache.v b/src/PushButtonSynthesis/BarrettReductionReificationCache.v new file mode 100644 index 000000000..4c538087e --- /dev/null +++ b/src/PushButtonSynthesis/BarrettReductionReificationCache.v @@ -0,0 +1,30 @@ +(** * Push-Button Synthesis of Barrett Reduction: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional Arithmetic.BarrettReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export BarrettReduction. + (* all the list operations from for_reification.ident *) + Strategy 100 [length seq repeat combine map flat_map partition app rev fold_right update_nth nth_default ]. + Strategy -10 [barrett_reduce reduce]. + + Derive reified_barrett_red_gen + SuchThat (is_reification_of reified_barrett_red_gen barrett_reduce) + As reified_barrett_red_gen_correct. + Proof. Time cache_reify (). Time Qed. + + Module Export ReifyHints. + Hint Extern 1 (_ = _) => apply_cached_reification barrett_reduce (proj1 reified_barrett_red_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_barrett_red_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_barrett_red_gen_correct) : interp_gen_cache. + End ReifyHints. + Local Opaque reified_barrett_red_gen. (* needed for making [autorewrite] not take a very long time *) +End BarrettReduction. diff --git a/src/PushButtonSynthesis/InvertHighLow.v b/src/PushButtonSynthesis/InvertHighLow.v new file mode 100644 index 000000000..f7deb4145 --- /dev/null +++ b/src/PushButtonSynthesis/InvertHighLow.v @@ -0,0 +1,39 @@ +(** * Push-Button Synthesis fancy argument definitions *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Local Open Scope Z_scope. + +Section with_wordmax. + Context (log2wordmax : Z) (consts : list Z). + Let wordmax := 2 ^ log2wordmax. + Let half_bits := log2wordmax / 2. + Let wordmax_half_bits := 2 ^ half_bits. + + Inductive kind_of_constant := upper_half (c : BinInt.Z) | lower_half (c : BinInt.Z). + + Definition constant_to_scalar_single (const x : BinInt.Z) : option kind_of_constant := + if x =? (BinInt.Z.shiftr const half_bits) + then Some (upper_half const) + else if x =? (BinInt.Z.land const (wordmax_half_bits - 1)) + then Some (lower_half const) + else None. + + Definition constant_to_scalar (x : BinInt.Z) + : option kind_of_constant := + fold_right (fun c res => match res with + | Some s => Some s + | None => constant_to_scalar_single c x + end) None consts. + + Definition invert_low (v : BinInt.Z) : option BinInt.Z + := match constant_to_scalar v with + | Some (lower_half v) => Some v + | _ => None + end. + + Definition invert_high (v : BinInt.Z) : option BinInt.Z + := match constant_to_scalar v with + | Some (upper_half v) => Some v + | _ => None + end. +End with_wordmax. diff --git a/src/PushButtonSynthesis/LegacySynthesisTactics.v b/src/PushButtonSynthesis/LegacySynthesisTactics.v new file mode 100644 index 000000000..c2ae24f7c --- /dev/null +++ b/src/PushButtonSynthesis/LegacySynthesisTactics.v @@ -0,0 +1,112 @@ +(** * Push-Button Synthesis: Legacy Synthesis Tactics *) +Require Import Coq.Classes.Morphisms. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.Util.Equality. (* fg_equal_rel *) +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.Tactics.GetGoal. + +Import + LanguageWf.Compilers + Language.Compilers. +Import Compilers.defaults. + +(** TODO: Port Barrett and Montgomery to the new glue style, and remove these tactics. These tactics are only needed for the old-glue-style derivations. *) +Ltac peel_interp_app _ := + lazymatch goal with + | [ |- ?R' (?InterpE ?arg) (?f ?arg) ] + => apply fg_equal_rel; [ | reflexivity ]; + try peel_interp_app () + | [ |- ?R' (Interp ?ev) (?f ?x) ] + => let sv := type of x in + let fx := constr:(f x) in + let dv := type of fx in + let rs := reify_type sv in + let rd := reify_type dv in + etransitivity; + [ apply @expr.Interp_APP_rel_reflexive with (s:=rs) (d:=rd) (R:=R'); + typeclasses eauto + | apply fg_equal_rel; + [ try peel_interp_app () + | try lazymatch goal with + | [ |- ?R (Interp ?ev) (Interp _) ] + => reflexivity + | [ |- ?R (Interp ?ev) ?c ] + => let rc := constr:(GallinaReify.Reify c) in + unify ev rc; vm_compute; reflexivity + end ] ] + end. +Ltac pre_cache_reify _ := + let H' := fresh in + lazymatch goal with + | [ |- ?P /\ Wf ?e ] + => let P' := fresh in + evar (P' : Prop); + assert (H' : P' /\ Wf e); subst P' + end; + [ + | split; [ destruct H' as [H' _] | destruct H' as [_ H']; exact H' ]; + cbv [type.app_curried]; + let arg := fresh "arg" in + let arg2 := fresh in + intros arg arg2; + cbn [type.and_for_each_lhs_of_arrow type.eqv]; + let H := fresh in + intro H; + repeat match type of H with + | and _ _ => let H' := fresh in + destruct H as [H' H]; + rewrite <- H' + end; + clear dependent arg2; clear H; + intros _; + peel_interp_app (); + [ lazymatch goal with + | [ |- ?R (Interp ?ev) _ ] + => (tryif is_evar ev + then let ev' := fresh "ev" in set (ev' := ev) + else idtac) + end; + cbv [pointwise_relation]; + repeat lazymatch goal with + | [ H : _ |- _ ] => first [ constr_eq H H'; fail 1 + | revert H ] + end; + eexact H' + | .. ] ]; + [ intros; clear | .. ]. +Ltac do_inline_cache_reify do_if_not_cached := + pre_cache_reify (); + [ try solve [ + cbv beta zeta; + repeat match goal with H := ?e |- _ => is_evar e; subst H end; + try solve [ split; [ solve [ eauto with nocore reify_gen_cache ] | solve [ eauto with wf_gen_cache; prove_Wf () ] ] ]; + do_if_not_cached () + ]; + cache_reify () + | .. ]. + +(* TODO: MOVE ME *) +Ltac vm_compute_lhs_reflexivity := + lazymatch goal with + | [ |- ?LHS = ?RHS ] + => let x := (eval vm_compute in LHS) in + (* we cannot use the unify tactic, which just gives "not + unifiable" as the error message, because we want to see the + terms that were not unifable. See also + COQBUG(https://github.com/coq/coq/issues/7291) *) + let _unify := constr:(ltac:(reflexivity) : RHS = x) in + vm_cast_no_check (eq_refl x) + end. + +Ltac solve_rop' rop_correct do_if_not_cached machine_wordsizev := + eapply rop_correct with (machine_wordsize:=machine_wordsizev); + [ do_inline_cache_reify do_if_not_cached + | subst_evars; vm_compute_lhs_reflexivity (* lazy; reflexivity *) ]. +Ltac solve_rop_nocache rop_correct := + solve_rop' rop_correct ltac:(fun _ => idtac). +Ltac solve_rop rop_correct := + solve_rop' + rop_correct + ltac:(fun _ => let G := get_goal in fail 2 "Could not find a solution in reify_gen_cache for" G). diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v new file mode 100644 index 000000000..2b7841ac0 --- /dev/null +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -0,0 +1,124 @@ +(** * Push-Button Synthesis of Montgomery Reduction *) +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.MontgomeryReductionReificationCache. +Require Import Crypto.PushButtonSynthesis.InvertHighLow. +Require Import Crypto.PushButtonSynthesis.LegacySynthesisTactics. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. + +Import Associational Positional Arithmetic.MontgomeryReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *) + +Section rmontred. + Context (N R N' : Z) + (machine_wordsize : Z). + + Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange. + Let flag_range := r[0 ~> 1]%zrange. + Let bound := Some value_range. + Let consts_list := [N; N']. + + Definition possible_values_of_machine_wordsize + := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z. + Local Arguments possible_values_of_machine_wordsize / . + + Let possible_values := possible_values_of_machine_wordsize. + + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := res. (* TODO: this should actually check stuff that corresponds with preconditions of montred'_correct *) + + Let fancy_args + := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list; + Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list; + Pipeline.value_range := value_range; + Pipeline.flag_range := flag_range |}). + + Lemma fancy_args_good + : match fancy_args with + | Some {| Pipeline.invert_low := il ; Pipeline.invert_high := ih |} + => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1)) + /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2)) + | None => True + end. + Proof. + cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right]; + split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence. + Qed. + + Definition montred + := Pipeline.BoundsPipeline + false (* subst01 *) + fancy_args (* fancy *) + possible_values + (reified_montred_gen + @ GallinaReify.Reify N @ GallinaReify.Reify R @ GallinaReify.Reify N' @ GallinaReify.Reify (Z.log2 R) @ GallinaReify.Reify 2%nat @ GallinaReify.Reify 2%nat) + (bound, (bound, tt)) + bound. + + Definition smontred (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "montred" montred. + + (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like +<< +Lemma montred_correct res + (Hres : montred = Success res) + : montred_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. +>> *) + + Notation BoundsPipeline_correct in_bounds out_bounds op + := (fun rv (rop : Expr (reify_type_of op)) Hrop + => @Pipeline.BoundsPipeline_correct_trans + false (* subst01 *) + fancy_args + fancy_args_good + possible_values + _ + rop + in_bounds + out_bounds + _ + op + Hrop rv) + (only parsing). + + Definition rmontred_correct + := BoundsPipeline_correct + (bound, (bound, tt)) + bound + (montred' N R N' (Z.log2 R) 2 2). + + Notation type_of_strip_3arrow := ((fun (d : Prop) (_ : forall A B C, d) => d) _). + Definition rmontred_correctT rv : Prop + := type_of_strip_3arrow (@rmontred_correct rv). +End rmontred. + +(* TODO: After moving to new-glue-style, remove these tactics *) +Ltac solve_rmontred := solve_rop rmontred_correct. +Ltac solve_rmontred_nocache := solve_rop_nocache rmontred_correct. diff --git a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v new file mode 100644 index 000000000..f787063a4 --- /dev/null +++ b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v @@ -0,0 +1,23 @@ +(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional Arithmetic.MontgomeryReduction. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export MontgomeryReduction. + Derive reified_montred_gen + SuchThat (is_reification_of reified_montred_gen montred') + As reified_montred_gen_correct. + Proof. Time cache_reify (). Time Qed. + Module Export ReifyHints. + Hint Extern 1 (_ = _) => apply_cached_reification montred' (proj1 reified_montred_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_montred_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_montred_gen_correct) : interp_gen_cache. + End ReifyHints. + Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *) +End MontgomeryReduction. diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v new file mode 100644 index 000000000..4afa64433 --- /dev/null +++ b/src/PushButtonSynthesis/Primitives.v @@ -0,0 +1,383 @@ +(** * Push-Button Synthesis of Primitives *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. (* for selectznz *) + +Import Associational Positional. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +(** +<< +#!/usr/bin/env python + +indent = '' + +print((indent + '(' + r'''** +<< +%s +>> +*''' + ')\n') % open(__file__, 'r').read()) + +for (op, opmod) in (('id', '(@id (list Z))'), ('selectznz', 'Positional.select'), ('mulx', 'mulx'), ('addcarryx', 'addcarryx'), ('subborrowx', 'subborrowx'), ('cmovznz', 'cmovznz')): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %s) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %s (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, op, op, opmod, op, opmod, op, op, op, op)).replace('\n', '\n%s' % indent) + '\n') + +>> +*) + +Derive reified_id_gen + SuchThat (is_reification_of reified_id_gen (@id (list Z))) + As reified_id_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification (@id (list Z)) (proj1 reified_id_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_id_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_id_gen_correct) : interp_gen_cache. +Local Opaque reified_id_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_selectznz_gen + SuchThat (is_reification_of reified_selectznz_gen Positional.select) + As reified_selectznz_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification Positional.select (proj1 reified_selectznz_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_selectznz_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_selectznz_gen_correct) : interp_gen_cache. +Local Opaque reified_selectznz_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_mulx_gen + SuchThat (is_reification_of reified_mulx_gen mulx) + As reified_mulx_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification mulx (proj1 reified_mulx_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_mulx_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_mulx_gen_correct) : interp_gen_cache. +Local Opaque reified_mulx_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_addcarryx_gen + SuchThat (is_reification_of reified_addcarryx_gen addcarryx) + As reified_addcarryx_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification addcarryx (proj1 reified_addcarryx_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_addcarryx_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_addcarryx_gen_correct) : interp_gen_cache. +Local Opaque reified_addcarryx_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_subborrowx_gen + SuchThat (is_reification_of reified_subborrowx_gen subborrowx) + As reified_subborrowx_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification subborrowx (proj1 reified_subborrowx_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_subborrowx_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_subborrowx_gen_correct) : interp_gen_cache. +Local Opaque reified_subborrowx_gen. (* needed for making [autorewrite] not take a very long time *) + +Derive reified_cmovznz_gen + SuchThat (is_reification_of reified_cmovznz_gen cmovznz) + As reified_cmovznz_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification cmovznz (proj1 reified_cmovznz_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_cmovznz_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_cmovznz_gen_correct) : interp_gen_cache. +Local Opaque reified_cmovznz_gen. (* needed for making [autorewrite] not take a very long time *) + +(* needed for making [autorewrite] with [Set Keyed Unification] fast *) +Local Opaque expr.Interp. + +Local Notation arg_bounds_of_pipeline result + := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => arg_bounds) _ _ _ _ _ _ _ result eq_refl) + (only parsing). +Local Notation out_bounds_of_pipeline result + := ((fun a b c d e arg_bounds out_bounds result' (H : @Pipeline.BoundsPipeline a b c d e arg_bounds out_bounds = result') => out_bounds) _ _ _ _ _ _ _ result eq_refl) + (only parsing). + +Notation FromPipelineToString prefix name result + := (((prefix ++ name)%string, + match result with + | Success E' + => let E := ToString.C.ToFunctionLines + true true (* static *) prefix (prefix ++ name)%string [] E' None + (arg_bounds_of_pipeline result) + (out_bounds_of_pipeline result) in + match E with + | inl E => Success E + | inr err => Error (Pipeline.Stringification_failed E' err) + end + | Error err => Error err + end)). + +Ltac prove_correctness use_curve_good := + let Hres := match goal with H : _ = Success _ |- _ => H end in + let H := fresh in + pose proof use_curve_good as H; + (* I want to just use [clear -H Hres], but then I can't use any lemmas in the section because of COQBUG(https://github.com/coq/coq/issues/8153) *) + repeat match goal with + | [ H' : _ |- _ ] + => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres ] + then fail + else clear H' + end; + cbv zeta in *; + destruct_head'_and; + let f := match type of Hres with ?f = _ => head f end in + try cbv [f] in *; + hnf; + PipelineTactics.do_unfolding; + try (let m := match goal with m := _ - Associational.eval _ |- _ => m end in + cbv [m] in * ); + intros; + try split; PipelineTactics.use_compilers_correctness Hres; + [ pose_proof_length_list_Z_bounded_by; + repeat first [ reflexivity + | progress autorewrite with interp interp_gen_cache push_eval + | progress autounfold with push_eval + | progress autorewrite with distr_length in * ] + | .. ]. + +Section __. + Context (n : nat) + (machine_wordsize : Z). + + Definition saturated_bounds_list : list (option zrange) + := List.repeat (Some r[0 ~> 2^machine_wordsize-1]%zrange) n. + Definition saturated_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some saturated_bounds_list. + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; machine_wordsize; 2 * machine_wordsize]%Z. + + Definition possible_values_of_machine_wordsize_with_bytes + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. + + Lemma length_saturated_bounds_list : List.length saturated_bounds_list = n. + Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_saturated_bounds_list : distr_length. + + Definition selectznz + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + reified_selectznz_gen + (Some r[0~>1], (saturated_bounds, (saturated_bounds, tt)))%zrange + saturated_bounds. + + Definition sselectznz (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "selectznz" selectznz. + + Definition mulx (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_mulx_gen + @ GallinaReify.Reify s) + (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt))%zrange + (Some r[0~>2^s-1], Some r[0~>2^s-1])%zrange. + + Definition smulx (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("mulx_u" ++ decimal_string_of_Z s) (mulx s). + + Definition addcarryx (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_addcarryx_gen + @ GallinaReify.Reify s) + (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange + (Some r[0~>2^s-1], Some r[0~>1])%zrange. + + Definition saddcarryx (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("addcarryx_u" ++ decimal_string_of_Z s) (addcarryx s). + + Definition subborrowx (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_subborrowx_gen + @ GallinaReify.Reify s) + (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange + (Some r[0~>2^s-1], Some r[0~>1])%zrange. + + Definition ssubborrowx (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("subborrowx_u" ++ decimal_string_of_Z s) (subborrowx s). + + Definition cmovznz (s : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_cmovznz_gen + @ GallinaReify.Reify s) + (Some r[0~>1], (Some r[0~>2^s-1], (Some r[0~>2^s-1], tt)))%zrange + (Some r[0~>2^s-1])%zrange. + + Definition scmovznz (prefix : string) (s : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("cmovznz_u" ++ decimal_string_of_Z s) (cmovznz s). + + Local Ltac solve_extra_bounds_side_conditions := + cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. + + Hint Rewrite + eval_select + Arithmetic.mulx_correct + Arithmetic.addcarryx_correct + Arithmetic.subborrowx_correct + Arithmetic.cmovznz_correct + Z.zselect_correct + using solve [ auto | congruence | solve_extra_bounds_side_conditions ] : push_eval. + + Strategy -1000 [mulx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma mulx_correct s' res + (Hres : mulx s' = Success res) + : mulx_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Strategy -1000 [addcarryx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma addcarryx_correct s' res + (Hres : addcarryx s' = Success res) + : addcarryx_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Strategy -1000 [subborrowx]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma subborrowx_correct s' res + (Hres : subborrowx s' = Success res) + : subborrowx_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Strategy -1000 [cmovznz]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma cmovznz_correct s' res + (Hres : cmovznz s' = Success res) + : cmovznz_correct s' (Interp res). + Proof using Type. prove_correctness I. Qed. + + Lemma selectznz_correct limbwidth res + (Hres : selectznz = Success res) + : selectznz_correct (weight (Qnum limbwidth) (QDen limbwidth)) n saturated_bounds_list (Interp res). + Proof using Type. prove_correctness I. Qed. + + Section for_stringification. + Context (valid_names : string) + (known_functions : list (string + * (string + -> string * + Pipeline.ErrorT (list string * ToString.C.ident_infos)))) + (extra_special_synthesis : string -> + list + (option + (string * + Pipeline.ErrorT + (list string * ToString.C.ident_infos)))). + + Definition aggregate_infos {A B C} (ls : list (A * ErrorT B (C * ToString.C.ident_infos))) : ToString.C.ident_infos + := fold_right + ToString.C.ident_info_union + ToString.C.ident_info_empty + (List.map + (fun '(_, res) => match res with + | Success (_, infos) => infos + | Error _ => ToString.C.ident_info_empty + end) + ls). + + Definition extra_synthesis (function_name_prefix : string) (infos : ToString.C.ident_infos) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t + := let ls_addcarryx := List.flat_map + (fun lg_split:positive => [saddcarryx function_name_prefix lg_split; ssubborrowx function_name_prefix lg_split]) + (PositiveSet.elements (ToString.C.addcarryx_lg_splits infos)) in + let ls_mulx := List.map + (fun lg_split:positive => smulx function_name_prefix lg_split) + (PositiveSet.elements (ToString.C.mulx_lg_splits infos)) in + let ls_cmov := List.map + (fun bitwidth:positive => scmovznz function_name_prefix bitwidth) + (PositiveSet.elements (ToString.C.cmovznz_bitwidths infos)) in + let ls := ls_addcarryx ++ ls_mulx ++ ls_cmov in + let infos := aggregate_infos ls in + (List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, + ToString.C.bitwidths_used infos). + + + Definition synthesize_of_name (function_name_prefix : string) (name : string) + : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos) + := fold_right + (fun v default + => match v with + | Some res => res + | None => default + end) + ((name, + Error + (Pipeline.Invalid_argument + ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ ".")))) + ((map + (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None) + known_functions) + ++ extra_special_synthesis name). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := let ls := match requests with + | nil => List.map (fun '(_, sr) => sr function_name_prefix) known_functions + | requests => List.map (synthesize_of_name function_name_prefix) requests + end in + let infos := aggregate_infos ls in + let '(extra_ls, extra_bit_widths) := extra_synthesis function_name_prefix infos in + (extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls, + PositiveSet.union extra_bit_widths (ToString.C.bitwidths_used infos)). + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/ReificationCache.v b/src/PushButtonSynthesis/ReificationCache.v index ba8488820..148cac049 100644 --- a/src/PushButtonSynthesis/ReificationCache.v +++ b/src/PushButtonSynthesis/ReificationCache.v @@ -26,10 +26,13 @@ Definition is_reification_of' {t} (e : Expr t) (v : type.interp base.interp t) : := pointwise_equal (Interp e) v /\ Wf e. Notation is_reification_of rop op - := (ltac:(let T := constr:(@is_reification_of' (reify_type_of op) rop op) in - let T := (eval cbv [pointwise_equal is_reification_of'] in T) in - let T := (eval cbn [type.interp base.interp base.base_interp] in T) in - exact T)) + := (match @is_reification_of' (reify_type_of op) rop op with + | T + => ltac:( + let T := (eval cbv [pointwise_equal is_reification_of' T] in T) in + let T := (eval cbn [type.interp base.interp base.base_interp] in T) in + exact T) + end) (only parsing). Ltac cache_reify _ := diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v new file mode 100644 index 000000000..bcb93c4a1 --- /dev/null +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -0,0 +1,184 @@ +(** * Push-Button Synthesis of Saturated Solinas *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.SaturatedSolinasReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + AbstractInterpretation.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. +Import COperationSpecifications.SaturatedSolinas. + +Import Associational Positional. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) +(* needed for making [autorewrite] with [Set Keyed Unification] fast *) +Local Opaque expr.Interp. + +Section __. + Context (s : Z) + (c : list (Z * Z)) + (machine_wordsize : Z). + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; 1; machine_wordsize]%Z. + + Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). + Let m := s - Associational.eval c. + (* Number of reductions is calculated as follows : + Let i be the highest limb index of c. Then, each reduction + decreases the number of extra limbs by (n-i). So, to go from + the n extra limbs we have post-multiplication down to 0, we + need ceil (n / (n - i)) reductions. *) + Let nreductions : nat := + let i := fold_right Z.max 0 (map (fun t => Z.log2 (fst t) / machine_wordsize) c) in + Z.to_nat (Qceiling (Z.of_nat n / (Z.of_nat n - i))). + Let possible_values := possible_values_of_machine_wordsize. + Let bound := Some r[0 ~> (2^machine_wordsize - 1)]%zrange. + Let boundsn : list (ZRange.type.option.interp base.type.Z) + := repeat bound n. + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [((negb (0 0 + /\ s <> 0 + /\ 0 < machine_wordsize + /\ n <> 0%nat. + Proof using curve_good. + clear -curve_good. + cbv [check_args fold_right] in curve_good. + break_innermost_match_hyps; try discriminate. + rewrite negb_false_iff in *. + Z.ltb_to_lt. + rewrite NPeano.Nat.eqb_neq in *. + intros. + rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. + specialize_by lia. + repeat match goal with H := _ |- _ => subst H end. + repeat match goal with + | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] + end. + repeat apply conj. + { destruct (s - Associational.eval c) eqn:?; cbn; lia. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + Qed. + + Definition mul + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_mul_gen + @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify nreductions) + (Some boundsn, (Some boundsn, tt)) + (Some boundsn, None (* Should be: Some r[0~>0]%zrange, but bounds analysis is not good enough *) ). + + Definition smul (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "mul" mul. + + Local Ltac solve_extra_bounds_side_conditions := + cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. + + Hint Rewrite + (fun pf => @Rows.eval_mulmod (weight machine_wordsize 1) (@wprops _ _ pf)) + using solve [ auto with zarith | congruence | solve_extra_bounds_side_conditions ] : push_eval. + Hint Unfold mulmod : push_eval. + + Local Ltac prove_correctness _ := Primitives.prove_correctness use_curve_good. + + Lemma mul_correct res + (Hres : mul = Success res) + : mul_correct (weight machine_wordsize 1) n m boundsn (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Section for_stringification. + Local Open Scope string_scope. + Local Open Scope list_scope. + + Definition known_functions + := [("mul", smul)]. + + Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := Primitives.Synthesize + machine_wordsize valid_names known_functions (fun _ => nil) + function_name_prefix requests. + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v new file mode 100644 index 000000000..ccc48e2cd --- /dev/null +++ b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v @@ -0,0 +1,28 @@ +(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export SaturatedSolinas. + Definition mulmod + (s : Z) + (c : list (Z * Z)) + (log2base : Z) + (n nreductions : nat) + := @Rows.mulmod (weight log2base 1) (2^log2base) s c n nreductions. + + Derive reified_mul_gen + SuchThat (is_reification_of reified_mul_gen mulmod) + As reified_mul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification mulmod (proj1 reified_mul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_mul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_mul_gen_correct) : interp_gen_cache. + Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) +End SaturatedSolinas. diff --git a/src/PushButtonSynthesis/SmallExamples.v b/src/PushButtonSynthesis/SmallExamples.v new file mode 100644 index 000000000..09f361356 --- /dev/null +++ b/src/PushButtonSynthesis/SmallExamples.v @@ -0,0 +1,95 @@ +(** * Push-Button Synthesis Examples *) +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Language. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. + +Import + Language.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import Associational Positional. + +Time Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (to_associational (weight 51 1) 5) in + exact r) + (Some (repeat (@None _) 5), tt) + ZRange.type.base.option.None). + +Time Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (scmul (weight 51 1) 5) in + exact r) + (None, (Some (repeat (@None _) 5), tt)) + ZRange.type.base.option.None). + +Compute + (Pipeline.BoundsPipeline + true None [64; 128] + ltac:(let r := Reify (fun f => carry_mulmod 51 1 (2^255) [(1,19)] 5 (seq 0 5 ++ [0; 1])%list%nat f f) in + exact r) + (Some (repeat (@None _) 5), tt) + ZRange.type.base.option.None). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_mulx_u64" [] + true None [64; 128] + ltac:(let r := Reify (Arithmetic.mulx 64) in + exact r) + (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt))%zrange + (Some r[0~>2^64-1], Some r[0~>2^64-1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_addcarryx_u64" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.addcarryx 64) in + exact r) + (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange + (Some r[0~>2^64-1], Some r[0~>1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_addcarryx_u51" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.addcarryx 51) in + exact r) + (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange + (Some r[0~>2^51-1], Some r[0~>1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_subborrowx_u64" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.subborrowx 64) in + exact r) + (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange + (Some r[0~>2^64-1], Some r[0~>1])%zrange). +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_subborrowx_u51" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.subborrowx 51) in + exact r) + (Some r[0~>1], (Some r[0~>2^51-1], (Some r[0~>2^51-1], tt)))%zrange + (Some r[0~>2^51-1], Some r[0~>1])%zrange). + +Compute + (Pipeline.BoundsPipelineToString + true "fiat_" "fiat_cmovznz64" [] + true None [1; 64; 128] + ltac:(let r := Reify (Arithmetic.cmovznz 64) in + exact r) + (Some r[0~>1], (Some r[0~>2^64-1], (Some r[0~>2^64-1], tt)))%zrange + (Some r[0~>2^64-1])%zrange). diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v new file mode 100644 index 000000000..4f22070c5 --- /dev/null +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -0,0 +1,602 @@ +(** * Push-Button Synthesis of Unsaturated Solinas *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.UnsaturatedSolinasReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + AbstractInterpretation.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. + +Import Associational Positional. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +(* needed for making [autorewrite] not take a very long time *) +Local Opaque + reified_carry_square_gen + reified_carry_scmul_gen + reified_carry_gen + reified_encode_gen + reified_add_gen + reified_sub_gen + reified_opp_gen + reified_zero_gen + reified_one_gen + reified_prime_gen + reified_to_bytes_gen + reified_from_bytes_gen + expr.Interp. + +Section __. + Context (n : nat) + (s : Z) + (c : list (Z * Z)) + (machine_wordsize : Z). + + Let limbwidth := (Z.log2_up (s - Associational.eval c) / Z.of_nat n)%Q. + Let idxs := (List.seq 0 n ++ [0; 1])%list%nat. + Let coef := 2. + Let n_bytes := bytes_n (Qnum limbwidth) (Qden limbwidth) n. + Let prime_upperbound_list : list Z + := encode_no_reduce (weight (Qnum limbwidth) (Qden limbwidth)) n (s-1). + Let prime_bytes_upperbound_list : list Z + := encode_no_reduce (weight 8 1) n_bytes (s-1). + Let tight_upperbounds : list Z + := List.map + (fun v : Z => Qceiling (11/10 * v)) + prime_upperbound_list. + Definition prime_bound : ZRange.type.option.interp (base.type.Z) + := Some r[0~>(s - Associational.eval c - 1)]%zrange. + Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). + Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list). + Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize). + Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). + + Let m : Z := s - Associational.eval c. + Definition m_enc : list Z + := encode (weight (Qnum limbwidth) (Qden limbwidth)) n s c m. + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; machine_wordsize; 2 * machine_wordsize]%Z. + + Definition possible_values_of_machine_wordsize_with_bytes + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. + Definition tight_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0~>u]%zrange) tight_upperbounds. + Definition loose_bounds : list (ZRange.type.option.interp base.type.Z) + := List.map (fun u => Some r[0 ~> 3*u]%zrange) tight_upperbounds. + + Lemma length_prime_upperbound_list : List.length prime_upperbound_list = n. + Proof using Type. cbv [prime_upperbound_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_prime_upperbound_list : distr_length. + Lemma length_tight_upperbounds : List.length tight_upperbounds = n. + Proof using Type. cbv [tight_upperbounds]; now autorewrite with distr_length. Qed. + Hint Rewrite length_tight_upperbounds : distr_length. + Lemma length_tight_bounds : List.length tight_bounds = n. + Proof using Type. cbv [tight_bounds]; now autorewrite with distr_length. Qed. + Hint Rewrite length_tight_bounds : distr_length. + Lemma length_loose_bounds : List.length loose_bounds = n. + Proof using Type. cbv [loose_bounds]; now autorewrite with distr_length. Qed. + Hint Rewrite length_loose_bounds : distr_length. + Lemma length_prime_bytes_upperbound_list : List.length prime_bytes_upperbound_list = bytes_n (Qnum limbwidth) (Qden limbwidth) n. + Proof using Type. cbv [prime_bytes_upperbound_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_prime_bytes_upperbound_list : distr_length. + Lemma length_saturated_bounds_list : List.length saturated_bounds_list = n. + Proof using Type. cbv [saturated_bounds_list]; now autorewrite with distr_length. Qed. + Hint Rewrite length_saturated_bounds_list : distr_length. + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [(negb (Qle_bool 1 limbwidth)%Q, Pipeline.Value_not_leQ "limbwidth < 1" 1%Q limbwidth); + ((negb (0 0 + /\ s <> 0 + /\ 0 < machine_wordsize + /\ n <> 0%nat + /\ List.length tight_bounds = n + /\ List.length loose_bounds = n + /\ List.length prime_bytes_upperbound_list = n_bytes + /\ List.length saturated_bounds_list = n + /\ 0 < Qden limbwidth <= Qnum limbwidth + /\ s = weight (Qnum limbwidth) (QDen limbwidth) n + /\ map (Z.land (Z.ones machine_wordsize)) m_enc = m_enc + /\ eval m_enc = s - Associational.eval c + /\ Datatypes.length m_enc = n + /\ 0 < Associational.eval c < s + /\ eval tight_upperbounds < 2 * eval m_enc + /\ 0 < m. + Proof using curve_good. + clear -curve_good. + cbv [check_args fold_right] in curve_good. + cbv [tight_bounds loose_bounds prime_bound m_enc] in *. + break_innermost_match_hyps; try discriminate. + rewrite negb_false_iff in *. + Z.ltb_to_lt. + rewrite Qle_bool_iff in *. + rewrite NPeano.Nat.eqb_neq in *. + intros. + cbv [Qnum Qden limbwidth Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *. + rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. + specialize_by lia. + repeat match goal with H := _ |- _ => subst H end. + repeat match goal with + | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] + end. + repeat apply conj. + { destruct (s - Associational.eval c) eqn:?; cbn; lia. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + Qed. + + Definition carry_mul + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_mul_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) + (Some loose_bounds, (Some loose_bounds, tt)) + (Some tight_bounds). + + Definition scarry_mul (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "carry_mul" carry_mul. + + Definition carry_square + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_square_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) + (Some loose_bounds, tt) + (Some tight_bounds). + + Definition scarry_square (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "carry_square" carry_square. + + Definition carry_scmul_const (x : Z) + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_scmul_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs @ GallinaReify.Reify x) + (Some loose_bounds, tt) + (Some tight_bounds). + + Definition scarry_scmul_const (prefix : string) (x : Z) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix ("carry_scmul_" ++ decimal_string_of_Z x) (carry_scmul_const x). + + Definition carry + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_carry_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) + (Some loose_bounds, tt) + (Some tight_bounds). + + Definition scarry (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "carry" carry. + + Definition add + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_add_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n) + (Some tight_bounds, (Some tight_bounds, tt)) + (Some loose_bounds). + + Definition sadd (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "add" add. + + Definition sub + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_sub_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify coef) + (Some tight_bounds, (Some tight_bounds, tt)) + (Some loose_bounds). + + Definition ssub (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "sub" sub. + + Definition opp + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_opp_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify coef) + (Some tight_bounds, tt) + (Some loose_bounds). + + Definition sopp (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "opp" opp. + + Definition to_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_to_bytes_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify m_enc) + (Some tight_bounds, tt) + prime_bytes_bounds. + + Definition sto_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + + Definition from_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_from_bytes_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify n) + (prime_bytes_bounds, tt) + (Some tight_bounds). + + Definition sfrom_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + + Definition encode + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_encode_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) + (prime_bound, tt) + (Some tight_bounds). + + Definition sencode (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "encode" encode. + + Definition zero + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_zero_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) + tt + (Some tight_bounds). + + Definition szero (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "zero" zero. + + Definition one + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_one_gen + @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n) + tt + (Some tight_bounds). + + Definition sone (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "one" one. + + Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. + Definition sselectznz (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Primitives.sselectznz n machine_wordsize prefix. + + Local Ltac solve_extra_bounds_side_conditions := + cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia. + + Hint Rewrite + eval_carry_mulmod + eval_carry_squaremod + eval_carry_scmulmod + eval_addmod + eval_submod + eval_oppmod + eval_carrymod + freeze_to_bytesmod_partitions + eval_to_bytesmod + eval_from_bytesmod + eval_encodemod + using solve [ auto | congruence | solve_extra_bounds_side_conditions ] : push_eval. + Hint Unfold zeromod onemod : push_eval. + + Local Ltac prove_correctness _ := + Primitives.prove_correctness use_curve_good; + try solve [ auto | congruence | solve_extra_bounds_side_conditions ]. + + Lemma carry_mul_correct res + (Hres : carry_mul = Success res) + : carry_mul_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma carry_square_correct res + (Hres : carry_square = Success res) + : carry_square_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma carry_scmul_const_correct a res + (Hres : carry_scmul_const a = Success res) + : carry_scmul_const_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds a (Interp res). + Proof using curve_good. + prove_correctness (). + erewrite eval_carry_scmulmod by (auto || congruence); reflexivity. + Qed. + + Lemma carry_correct res + (Hres : carry = Success res) + : carry_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma add_correct res + (Hres : add = Success res) + : add_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma sub_correct res + (Hres : sub = Success res) + : sub_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma opp_correct res + (Hres : opp = Success res) + : opp_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds loose_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma from_bytes_correct res + (Hres : from_bytes = Success res) + : from_bytes_correct (weight (Qnum limbwidth) (QDen limbwidth)) n n_bytes m s tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Lemma relax_correct + : forall x, list_Z_bounded_by tight_bounds x -> list_Z_bounded_by loose_bounds x. + Proof using Type. + cbv [tight_bounds loose_bounds list_Z_bounded_by]. + intro. + rewrite !fold_andb_map_map1, !fold_andb_map_iff; cbn [upper lower]. + setoid_rewrite Bool.andb_true_iff. + intro H. + repeat first [ let H' := fresh in destruct H as [H' H]; split; [ assumption | ] + | let x := fresh in intro x; specialize (H x) ]. + Z.ltb_to_lt; lia. + Qed. + + Lemma to_bytes_correct res + (Hres : to_bytes = Success res) + : to_bytes_correct (weight (Qnum limbwidth) (QDen limbwidth)) n n_bytes m tight_bounds (Interp res). + Proof using curve_good. + prove_correctness (); []. + erewrite freeze_to_bytesmod_partitions; [ reflexivity | .. ]. + all: repeat apply conj; autorewrite with distr_length; (congruence || auto). + all: cbv [tight_bounds] in *. + all: lazymatch goal with + | [ H1 : list_Z_bounded_by (List.map (fun x => Some (@?f x)) ?b) ?x, H2 : eval ?wt ?n ?b < _ + |- context[eval ?wt ?n ?x] ] + => unshelve epose proof (eval_list_Z_bounded_by wt n (List.map (fun x => Some (f x)) b) (List.map f b) x H1 _ _ (fun A B => Z.lt_le_incl _ _ (weight_positive _ _))); clear H1 + end. + all: congruence || auto. + all: repeat first [ reflexivity + | apply wprops + | progress rewrite ?map_map in * + | progress rewrite ?map_id in * + | progress cbn [upper lower] in * + | lia + | match goal with + | [ H : context[List.map (fun _ => 0) _] |- _ ] => erewrite <- zeros_ext_map, ?eval_zeros in H by reflexivity + end + | progress autorewrite with distr_length push_eval in * + | progress cbv [tight_upperbounds] in * ]. + Qed. + + Strategy -1000 [encode]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma encode_correct res + (Hres : encode = Success res) + : encode_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Strategy -1000 [zero]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma zero_correct res + (Hres : zero = Success res) + : zero_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Strategy -1000 [one]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma one_correct res + (Hres : one = Success res) + : one_correct (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds (Interp res). + Proof using curve_good. prove_correctness (). Qed. + + Section ring. + Context carry_mul_res (Hcarry_mul : carry_mul = Success carry_mul_res) + add_res (Hadd : add = Success add_res) + sub_res (Hsub : sub = Success sub_res) + opp_res (Hopp : opp = Success opp_res) + carry_res (Hcarry : carry = Success carry_res) + encode_res (Hencode : encode = Success encode_res) + zero_res (Hzero : zero = Success zero_res) + one_res (Hone : one = Success one_res). + + Definition GoodT : Prop + := GoodT + (weight (Qnum limbwidth) (QDen limbwidth)) n m tight_bounds + (Interp carry_mul_res) + (Interp add_res) + (Interp sub_res) + (Interp opp_res) + (Interp carry_res) + (Interp encode_res) + (Interp zero_res) + (Interp one_res). + + Theorem Good : GoodT. + Proof using curve_good Hcarry_mul Hadd Hsub Hopp Hcarry Hencode Hzero Hone. + pose proof use_curve_good; cbv zeta in *; destruct_head'_and. + eapply Good. + all: repeat first [ assumption + | apply carry_mul_correct + | apply add_correct + | apply sub_correct + | apply opp_correct + | apply carry_correct + | apply encode_correct + | apply zero_correct + | apply one_correct + | apply relax_correct ]. + Qed. + End ring. + + Section for_stringification. + Local Open Scope string_scope. + Local Open Scope list_scope. + + Definition known_functions + := [("carry_mul", scarry_mul); + ("carry_square", scarry_square); + ("carry", scarry); + ("add", sadd); + ("sub", ssub); + ("opp", sopp); + ("selectznz", sselectznz); + ("to_bytes", sto_bytes); + ("from_bytes", sfrom_bytes)]. + + Definition valid_names : string + := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions) ++ ", or 'carry_scmul' followed by a decimal literal". + + Definition extra_special_synthesis (function_name_prefix : string) (name : string) + : list (option (string * Pipeline.ErrorT (list string * ToString.C.ident_infos))) + := [if prefix "carry_scmul" name + then let sc := substring (String.length "carry_scmul") (String.length name) name in + let scZ := Z_of_decimal_string sc in + if string_beq sc (decimal_string_of_Z scZ) + then Some (scarry_scmul_const function_name_prefix scZ) + else None + else None]. + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := Primitives.Synthesize + machine_wordsize valid_names known_functions (extra_special_synthesis function_name_prefix) + function_name_prefix requests. + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v new file mode 100644 index 000000000..3cee63c4e --- /dev/null +++ b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v @@ -0,0 +1,168 @@ +(** * Push-Button Synthesis of Unsaturated Solinas: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Arithmetic. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import Associational Positional. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export UnsaturatedSolinas. + Definition zeromod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 0. + Definition onemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n 1. + Definition primemod limbwidth_num limbwidth_den s c n := encodemod limbwidth_num limbwidth_den s c n (s - Associational.eval c). + + (** +<< +#!/usr/bin/env python + +indent = ' ' + +print((indent + '(' + r'''** +<< +%s +>> +*''' + ')\n') % open(__file__, 'r').read()) + +for i in ('carry_mul', 'carry_square', 'carry_scmul', 'carry', 'encode', 'add', 'sub', 'opp', 'zero', 'one', 'prime'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + +for (op, opmod) in (('to_bytes', 'freeze_to_bytesmod'), ('from_bytes', 'from_bytesmod')): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %s) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %s (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, op, op, opmod, op, opmod, op, op, op, op)).replace('\n', '\n%s' % indent) + '\n') + +>> +*) + + Derive reified_carry_mul_gen + SuchThat (is_reification_of reified_carry_mul_gen carry_mulmod) + As reified_carry_mul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carry_mulmod (proj1 reified_carry_mul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_mul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_mul_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_mul_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_carry_square_gen + SuchThat (is_reification_of reified_carry_square_gen carry_squaremod) + As reified_carry_square_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carry_squaremod (proj1 reified_carry_square_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_square_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_square_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_square_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_carry_scmul_gen + SuchThat (is_reification_of reified_carry_scmul_gen carry_scmulmod) + As reified_carry_scmul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carry_scmulmod (proj1 reified_carry_scmul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_scmul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_scmul_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_scmul_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_carry_gen + SuchThat (is_reification_of reified_carry_gen carrymod) + As reified_carry_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification carrymod (proj1 reified_carry_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_carry_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_carry_gen_correct) : interp_gen_cache. + Local Opaque reified_carry_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_encode_gen + SuchThat (is_reification_of reified_encode_gen encodemod) + As reified_encode_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification encodemod (proj1 reified_encode_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_encode_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_encode_gen_correct) : interp_gen_cache. + Local Opaque reified_encode_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_add_gen + SuchThat (is_reification_of reified_add_gen addmod) + As reified_add_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification addmod (proj1 reified_add_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_add_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_add_gen_correct) : interp_gen_cache. + Local Opaque reified_add_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_sub_gen + SuchThat (is_reification_of reified_sub_gen submod) + As reified_sub_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification submod (proj1 reified_sub_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_sub_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_sub_gen_correct) : interp_gen_cache. + Local Opaque reified_sub_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_opp_gen + SuchThat (is_reification_of reified_opp_gen oppmod) + As reified_opp_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification oppmod (proj1 reified_opp_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_opp_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_opp_gen_correct) : interp_gen_cache. + Local Opaque reified_opp_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_zero_gen + SuchThat (is_reification_of reified_zero_gen zeromod) + As reified_zero_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification zeromod (proj1 reified_zero_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_zero_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_zero_gen_correct) : interp_gen_cache. + Local Opaque reified_zero_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_one_gen + SuchThat (is_reification_of reified_one_gen onemod) + As reified_one_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification onemod (proj1 reified_one_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_one_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_one_gen_correct) : interp_gen_cache. + Local Opaque reified_one_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_prime_gen + SuchThat (is_reification_of reified_prime_gen primemod) + As reified_prime_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification primemod (proj1 reified_prime_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_prime_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_prime_gen_correct) : interp_gen_cache. + Local Opaque reified_prime_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_to_bytes_gen + SuchThat (is_reification_of reified_to_bytes_gen freeze_to_bytesmod) + As reified_to_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification freeze_to_bytesmod (proj1 reified_to_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_to_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_to_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_to_bytes_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_from_bytes_gen + SuchThat (is_reification_of reified_from_bytes_gen from_bytesmod) + As reified_from_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification from_bytesmod (proj1 reified_from_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_from_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_from_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_from_bytes_gen. (* needed for making [autorewrite] not take a very long time *) +End UnsaturatedSolinas. diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v new file mode 100644 index 000000000..3b28329c5 --- /dev/null +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -0,0 +1,762 @@ +(** * Push-Button Synthesis of Word-By-Word Montgomery *) +Require Import Coq.Strings.String. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.MSets.MSetPositive. +Require Import Coq.Lists.List. +Require Import Coq.QArith.QArith_base Coq.QArith.Qround. +Require Import Coq.Program.Tactics. (* For WBW Montgomery proofs *) +Require Import Coq.derive.Derive. +Require Import Crypto.Util.ErrorT. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil.FoldBool. +Require Import Crypto.Util.Strings.Decimal. +Require Import Crypto.Util.Strings.Equality. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.ModInv. (* Only needed for WBW Montgomery *) +Require Import Crypto.Util.ZUtil.Modulo. (* Only needed for WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Le. (* Only needed for WBW Montgomery proofs *) +Require Import Crypto.Util.Prod. (* For WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. (* For WBW montgomery proofs *) +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. (* For WBW montgomery proofs *) +Require Import Crypto.Util.ZUtil.Div. (* For WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. (* For WBW Montgomery proofs *) +Require Import Crypto.Util.ZUtil.Ones. (* For WBW montgomery proofs *) +Require Import Crypto.Util.ZUtil.Shift. (* For WBW montgomery proofs *) +Require Import Crypto.Util.Tactics.HasBody. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.LanguageWf. +Require Import Crypto.Language. +Require Import Crypto.AbstractInterpretation. +Require Import Crypto.CStringification. +Require Import Crypto.Arithmetic. +Require Import Crypto.BoundsPipeline. +Require Import Crypto.COperationSpecifications. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Require Import Crypto.PushButtonSynthesis.Primitives. +Require Import Crypto.PushButtonSynthesis.WordByWordMontgomeryReificationCache. +Import ListNotations. +Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope. + +Import + LanguageWf.Compilers + Language.Compilers + AbstractInterpretation.Compilers + CStringification.Compilers. +Import Compilers.defaults. + +Import COperationSpecifications.Primitives. +Import COperationSpecifications.Solinas. +Import COperationSpecifications.WordByWordMontgomery. + +Import Associational Positional. +Import Arithmetic.WordByWordMontgomery. + +Import WordByWordMontgomeryReificationCache.WordByWordMontgomery. + +Local Coercion Z.of_nat : nat >-> Z. +Local Coercion QArith_base.inject_Z : Z >-> Q. +Local Coercion Z.pos : positive >-> Z. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +(* needed for making [autorewrite] not take a very long time *) +Local Opaque + reified_mul_gen + reified_add_gen + reified_sub_gen + reified_opp_gen + reified_to_bytes_gen + reified_from_bytes_gen + reified_nonzero_gen + reified_square_gen + reified_encode_gen + reified_from_montgomery_gen + reified_zero_gen + reified_one_gen + expr.Interp. + +Section __. + Context (m : Z) + (machine_wordsize : Z). + + Let s := 2^Z.log2_up m. + Let c := s - m. + Let n : nat := Z.to_nat (Qceiling (Z.log2_up s / machine_wordsize)). + Let r := 2^machine_wordsize. + Let r' := match Z.modinv r m with + | Some r' => r' + | None => 0 + end. + Let m' := match Z.modinv (-m) r with + | Some m' => m' + | None => 0 + end. + Let n_bytes := bytes_n machine_wordsize 1 n. + Let prime_upperbound_list : list Z + := Partition.partition (UniformWeight.uweight machine_wordsize) n (s-1). + Let prime_bytes_upperbound_list : list Z + := Partition.partition (weight 8 1) n_bytes (s-1). + Let upperbounds : list Z := prime_upperbound_list. + Definition prime_bound : ZRange.type.option.interp (base.type.Z) + := Some r[0~>m-1]%zrange. + Definition prime_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_upperbound_list). + Definition prime_bytes_bounds : ZRange.type.option.interp (base.type.list (base.type.Z)) + := Some (List.map (fun v => Some r[0 ~> v]%zrange) prime_bytes_upperbound_list). + Local Notation saturated_bounds_list := (saturated_bounds_list n machine_wordsize). + Local Notation saturated_bounds := (saturated_bounds n machine_wordsize). + + (* We include [0], so that even after bounds relaxation, we can + notice where the constant 0s are, and remove them. *) + Definition possible_values_of_machine_wordsize + := [0; 1; machine_wordsize; 2 * machine_wordsize]%Z. + + Definition possible_values_of_machine_wordsize_with_bytes + := [0; 1; 8; machine_wordsize; 2 * machine_wordsize]%Z. + + Let possible_values := possible_values_of_machine_wordsize. + Let possible_values_with_bytes := possible_values_of_machine_wordsize_with_bytes. + Definition bounds : list (ZRange.type.option.interp base.type.Z) + := Option.invert_Some saturated_bounds (*List.map (fun u => Some r[0~>u]%zrange) upperbounds*). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition check_args {T} (res : Pipeline.ErrorT T) + : Pipeline.ErrorT T + := fold_right + (fun '(b, e) k => if b:bool then Error e else k) + res + [(negb (1 0 + /\ s - c <> 0 + /\ 0 < s + /\ s <> 0 + /\ 0 < machine_wordsize + /\ n <> 0%nat + /\ List.length bounds = n + /\ 0 < 1 <= machine_wordsize + /\ 0 < c < s + /\ (r * r') mod m = 1 + /\ (m * m') mod r = (-1) mod r + /\ 0 < machine_wordsize + /\ 1 < m + /\ m < r^n + /\ s = 2^Z.log2 s + /\ s <= UniformWeight.uweight machine_wordsize n + /\ s <= UniformWeight.uweight 8 n_bytes + /\ UniformWeight.uweight machine_wordsize n = UniformWeight.uweight 8 n_bytes. + Proof. + clear -curve_good. + cbv [check_args fold_right] in curve_good. + cbv [bounds prime_bound prime_bounds saturated_bounds] in *. + break_innermost_match_hyps; try discriminate. + rewrite negb_false_iff in *. + Z.ltb_to_lt. + rewrite NPeano.Nat.eqb_neq in *. + intros. + cbv [Qnum Qden Qceiling Qfloor Qopp Qdiv Qplus inject_Z Qmult Qinv] in *. + rewrite ?map_length, ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *. + specialize_by lia. + repeat match goal with H := _ |- _ => subst H end. + repeat match goal with + | [ H : list_beq _ _ _ _ = true |- _ ] => apply internal_list_dec_bl in H; [ | intros; Z.ltb_to_lt; omega.. ] + end. + repeat apply conj. + { destruct m eqn:?; cbn; lia. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + { use_curve_good_t. } + Qed. + + + Definition mul + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_mul_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (Some bounds, (Some bounds, tt)) + (Some bounds). + + Definition smul (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "mul" mul. + + Definition square + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values + (reified_square_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (Some bounds, tt) + (Some bounds). + + Definition ssquare (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "square" square. + + Definition add + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_add_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) + (Some bounds, (Some bounds, tt)) + (Some bounds). + + Definition sadd (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "add" add. + + Definition sub + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_sub_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) + (Some bounds, (Some bounds, tt)) + (Some bounds). + + Definition ssub (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "sub" sub. + + Definition opp + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_opp_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m) + (Some bounds, tt) + (Some bounds). + + Definition sopp (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "opp" opp. + + Definition from_montgomery + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_from_montgomery_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (Some bounds, tt) + (Some bounds). + + Definition sfrom_montgomery (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "from_montgomery" from_montgomery. + + Definition nonzero + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + reified_nonzero_gen + (Some bounds, tt) + (Some r[0~>r-1]%zrange). + + Definition snonzero (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "nonzero" nonzero. + + Definition to_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_to_bytes_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n) + (prime_bounds, tt) + prime_bytes_bounds. + + Definition sto_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "to_bytes" to_bytes. + + Definition from_bytes + := Pipeline.BoundsPipeline + false (* subst01 *) + None (* fancy *) + possible_values_with_bytes + (reified_from_bytes_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify 1 @ GallinaReify.Reify n) + (prime_bytes_bounds, tt) + prime_bounds. + + Definition sfrom_bytes (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "from_bytes" from_bytes. + + Definition encode + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_encode_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + (prime_bound, tt) + (Some bounds). + + Definition sencode (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "encode" encode. + + Definition zero + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_zero_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + tt + (Some bounds). + + Definition szero (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "zero" zero. + + Definition one + := Pipeline.BoundsPipeline + true (* subst01 *) + None (* fancy *) + possible_values + (reified_one_gen + @ GallinaReify.Reify machine_wordsize @ GallinaReify.Reify n @ GallinaReify.Reify m @ GallinaReify.Reify m') + tt + (Some bounds). + + Definition sone (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Eval cbv beta in FromPipelineToString prefix "one" one. + + Definition selectznz : Pipeline.ErrorT _ := Primitives.selectznz n machine_wordsize. + Definition sselectznz (prefix : string) + : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos)) + := Primitives.sselectznz n machine_wordsize prefix. + + Local Notation valid := (Arithmetic.WordByWordMontgomery.valid machine_wordsize n m). + Local Notation bytes_valid := (Arithmetic.WordByWordMontgomery.valid 8 n_bytes m). + + Lemma bounded_by_of_valid x + (H : valid x) + : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some bounds) x = true. + Proof using curve_good. + pose proof use_curve_good as use_curve_good. + clear -H use_curve_good curve_good. + destruct H as [H _]; destruct_head'_and. + cbv [small] in H. + cbv [ZRange.type.base.option.is_bounded_by bounds saturated_bounds saturated_bounds_list Option.invert_Some]. + replace n with (List.length x) by now rewrite H, Partition.length_partition. + rewrite <- map_const, fold_andb_map_map1, fold_andb_map_iff. + cbv [ZRange.type.base.is_bounded_by is_bounded_by_bool lower upper]. + split; [ reflexivity | ]. + intros *; rewrite combine_same, in_map_iff, Bool.andb_true_iff, !Z.leb_le. + intros; destruct_head'_ex; destruct_head'_and; subst *; cbn [fst snd]. + match goal with + | [ H : In ?v x |- _ ] => revert v H + end. + rewrite H. + generalize (eval (n:=n) machine_wordsize x). + cbn [base.interp base.base_interp]. + generalize n. + intro n'. + induction n' as [|n' IHn']. + { cbv [Partition.partition seq map In]; tauto. } + { intros *; rewrite Partition.partition_step, in_app_iff; cbn [List.In]. + intros; destruct_head'_or; subst *; eauto; try tauto; []. + rewrite UniformWeight.uweight_S by lia. + assert (0 < UniformWeight.uweight machine_wordsize n') by now apply UniformWeight.uwprops. + assert (0 < 2 ^ machine_wordsize) by auto with zarith. + assert (0 < 2 ^ machine_wordsize * UniformWeight.uweight machine_wordsize n') by nia. + rewrite <- Z.mod_pull_div by lia. + rewrite Z.le_sub_1_iff. + auto with zarith. } + Qed. + + (* XXX FIXME *) + Lemma bounded_by_prime_bounds_of_valid_gen lgr n' x + (Hlgr : 0 < lgr) + (Hs : s = 2^Z.log2 s) + (Hs' : s <= UniformWeight.uweight lgr n') + (H : WordByWordMontgomery.valid lgr n' m x) + : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some (List.map (fun v => Some r[0~>v]%zrange) (Partition.partition (UniformWeight.uweight lgr) n' (s-1)))) x = true. + Proof using curve_good. + pose proof use_curve_good as use_curve_good. + clear -H use_curve_good curve_good Hlgr Hs Hs'. + destruct H as [H ?]; destruct_head'_and. + cbv [small] in H. + cbv [ZRange.type.base.option.is_bounded_by]. + replace n' with (List.length x) by now rewrite H, Partition.length_partition. + rewrite fold_andb_map_map1, fold_andb_map_iff. + split; [ now autorewrite with distr_length | ]. + cbv [ZRange.type.base.is_bounded_by is_bounded_by_bool lower upper]. + rewrite H; autorewrite with distr_length. + intros [v1 v0]; cbn [fst snd]. + rename x into x'. + generalize dependent (eval (n:=n') lgr x'). + replace m with (s - c) in * by easy. + intro x; intros ??? H; subst x'. + eapply In_nth_error in H; destruct H as [i H]. + rewrite nth_error_combine in H. + break_match_hyps; try discriminate; []; Option.inversion_option; Prod.inversion_prod; subst. + cbv [Partition.partition] in *. + apply nth_error_map in Heqo; apply nth_error_map in Heqo0; destruct Heqo as (?&?&?), Heqo0 as (?&?&?). + rewrite nth_error_seq in *. + break_match_hyps; try discriminate; Option.inversion_option; Prod.inversion_prod; subst. + rewrite ?Nat.add_0_l. + assert (0 <= x < s) by lia. + replace s with (2^Z.log2 s) by easy. + assert (1 < s) by lia. + assert (0 < Z.log2 s) by now apply Z.log2_pos. + assert (1 < 2^Z.log2 s) by auto with zarith. + generalize dependent (Z.log2 s); intro lgs; intros. + + edestruct (UniformWeight.uwprops lgr); try lia. + assert (forall i : nat, 0 <= UniformWeight.uweight lgr i) by (intro z; specialize (weight_positive z); lia). + apply Bool.andb_true_intro; split; apply OrdersEx.Z_as_OT.leb_le; + [apply Z.div_nonneg | apply Z.div_le_mono_nonneg]; trivial. + apply Z.mod_pos_bound; trivial. + + cbv [UniformWeight.uweight]. + cbv [weight]. + rewrite Z.div_1_r. + rewrite Z.opp_involutive. + rewrite <-2Z.land_ones by nia. + rewrite Z.sub_1_r, <-Z.ones_equiv. + rewrite Z.land_ones_ones. + destruct ((lgs H end in + let H := fresh in + pose proof use_curve_good as H; + (* I want to just use [clear -H Hres], but then I can't use any lemmas in the section because of COQBUG(https://github.com/coq/coq/issues/8153) *) + repeat match goal with + | [ H' : _ |- _ ] + => tryif first [ has_body H' | constr_eq H' H | constr_eq H' Hres | dont_clear H' ] + then fail + else clear H' + end; + cbv zeta in *; + destruct_head'_and; + let f := match type of Hres with ?f = _ => head f end in + try cbv [f] in *; + hnf; + PipelineTactics.do_unfolding; + try (let m := match goal with m := _ - Associational.eval _ |- _ => m end in + cbv [m] in * ); + intros; + lazymatch goal with + | [ |- _ <-> _ ] => idtac + | [ |- _ = _ ] => idtac + | _ => split; [ | try split ]; + cbv [small] + end; + PipelineTactics.use_compilers_correctness Hres; + repeat first [ reflexivity + | now apply bounded_by_of_valid + | now apply bounded_by_prime_bounds_of_valid + | now apply bounded_by_prime_bytes_bounds_of_bytes_valid + | now apply weight_bounded_of_bytes_valid + | solve [ eapply op_correct; try eassumption; solve_extra_bounds_side_conditions ] + | progress autorewrite with interp interp_gen_cache push_eval + | progress autounfold with push_eval + | progress autorewrite with distr_length in * + | solve [ cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto ] ]. + + (** TODO: DESIGN DECISION: + + The correctness lemmas for most of the montgomery things are + parameterized over a `from_montgomery`. When filling this in + for, e.g., mul-correctness, should I use `from_montgomery` + from arithmetic, or should I use `Interp + reified_from_montgomery` (the post-pipeline version), and take + in success of the pipeline on `from_montgomery` as well? *) + + Local Notation from_montgomery_res := (from_montgomerymod machine_wordsize n m m'). + + Lemma mul_correct res + (Hres : mul = Success res) + : mul_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness mulmod_correct. Qed. + + Lemma square_correct res + (Hres : square = Success res) + : square_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness squaremod_correct. Qed. + + Lemma add_correct res + (Hres : add = Success res) + : add_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness addmod_correct. Qed. + + Lemma sub_correct res + (Hres : sub = Success res) + : sub_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness submod_correct. Qed. + + Lemma opp_correct res + (Hres : opp = Success res) + : opp_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness oppmod_correct. Qed. + + Lemma from_montgomery_correct res + (Hres : from_montgomery = Success res) + : from_montgomery_correct machine_wordsize n m r' valid (Interp res). + Proof using curve_good. prove_correctness from_montgomerymod_correct. Qed. + + Lemma nonzero_correct res + (Hres : nonzero = Success res) + : nonzero_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness nonzeromod_correct. Qed. + + Lemma to_bytes_correct res + (Hres : to_bytes = Success res) + : to_bytes_correct machine_wordsize n n_bytes m valid (Interp res). + Proof using curve_good. prove_correctness to_bytesmod_correct. Qed. + + Lemma from_bytes_correct res + (Hres : from_bytes = Success res) + : from_bytes_correct machine_wordsize n n_bytes m valid bytes_valid (Interp res). + Proof using curve_good. prove_correctness eval_from_bytesmod_and_partitions. Qed. + + Strategy -1000 [encode]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma encode_correct res + (Hres : encode = Success res) + : encode_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness encodemod_correct. Qed. + + Strategy -1000 [zero]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma zero_correct res + (Hres : zero = Success res) + : zero_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness encodemod_correct. Qed. + + Strategy -1000 [one]. (* if we don't tell the kernel to unfold this early, then [Qed] seems to run off into the weeds *) + Lemma one_correct res + (Hres : one = Success res) + : one_correct machine_wordsize n m valid from_montgomery_res (Interp res). + Proof using curve_good. prove_correctness encodemod_correct. Qed. + + Local Opaque Pipeline.BoundsPipeline. (* need this or else [eapply Pipeline.BoundsPipeline_correct in Hres] takes forever *) + Lemma selectznz_correct res + (Hres : selectznz = Success res) + : selectznz_correct machine_wordsize n saturated_bounds_list (Interp res). + Proof using curve_good. Primitives.prove_correctness use_curve_good. Qed. + + Section ring. + Context from_montgomery_res (Hfrom_montgomery : from_montgomery = Success from_montgomery_res) + mul_res (Hmul : mul = Success mul_res) + add_res (Hadd : add = Success add_res) + sub_res (Hsub : sub = Success sub_res) + opp_res (Hopp : opp = Success opp_res) + encode_res (Hencode : encode = Success encode_res) + zero_res (Hzero : zero = Success zero_res) + one_res (Hone : one = Success one_res). + + Definition GoodT : Prop + := GoodT + machine_wordsize n m valid + (Interp from_montgomery_res) + (Interp mul_res) + (Interp add_res) + (Interp sub_res) + (Interp opp_res) + (Interp encode_res) + (Interp zero_res) + (Interp one_res). + + Theorem Good : GoodT. + Proof using curve_good Hfrom_montgomery Hmul Hadd Hsub Hopp Hencode Hzero Hone. + pose proof use_curve_good; cbv zeta in *; destruct_head'_and. + eapply Good. + all: repeat first [ assumption + | apply from_montgomery_correct + | lia ]. + all: hnf; intros. + all: push_Zmod; erewrite !(fun v Hv => proj1 (from_montgomery_correct _ Hfrom_montgomery v Hv)), <- !eval_from_montgomerymod; try eassumption; pull_Zmod. + all: repeat first [ assumption + | lazymatch goal with + | [ |- context[mul_res] ] => apply mul_correct + | [ |- context[add_res] ] => apply add_correct + | [ |- context[sub_res] ] => apply sub_correct + | [ |- context[opp_res] ] => apply opp_correct + | [ |- context[encode_res] ] => apply encode_correct + | [ |- context[zero_res] ] => apply zero_correct + | [ |- context[one_res] ] => apply one_correct + end ]. + Qed. + End ring. + + Section for_stringification. + Local Open Scope string_scope. + Local Open Scope list_scope. + + Definition known_functions + := [("mul", smul); + ("square", ssquare); + ("add", sadd); + ("sub", ssub); + ("opp", sopp); + ("from_montgomery", sfrom_montgomery); + ("nonzero", snonzero); + ("selectznz", sselectznz); + ("to_bytes", sto_bytes); + ("from_bytes", sfrom_bytes)]. + + Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions). + + (** Note: If you change the name or type signature of this + function, you will need to update the code in CLI.v *) + Definition Synthesize (function_name_prefix : string) (requests : list string) + : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *) + := Primitives.Synthesize + machine_wordsize valid_names known_functions (fun _ => nil) + function_name_prefix requests. + End for_stringification. +End __. diff --git a/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v new file mode 100644 index 000000000..ac429cdb5 --- /dev/null +++ b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v @@ -0,0 +1,247 @@ +(** * Push-Button Synthesis of Word-By-Word Montgomery: Reification Cache *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.derive.Derive. +Require Import Crypto.Util.Tactics.Head. +Require Import Crypto.Arithmetic. +Require Import Crypto.Language. +Require Import Crypto.PushButtonSynthesis.ReificationCache. +Local Open Scope Z_scope. + +Import + LanguageWf.Compilers + Language.Compilers. +Import Compilers.defaults. + +Import Associational Positional. + +Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) + +Module Export WordByWordMontgomery. + Import Arithmetic.WordByWordMontgomery. + + Definition zeromod bitwidth n m m' := encodemod bitwidth n m m' 0. + Definition onemod bitwidth n m m' := encodemod bitwidth n m m' 1. + + (* we would do something faster, but it generally breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + Local Ltac precache_reify_faster _ := + split; + [ let marker := fresh "marker" in + pose I as marker; + intros; + let LHS := lazymatch goal with |- ?LHS = _ => LHS end in + let reified_op_gen := lazymatch LHS with context[expr.Interp _ ?reified_op_gen] => reified_op_gen end in + subst reified_op_gen; + etransitivity; + [ + | let opmod := match goal with |- _ = ?RHS => head RHS end in + cbv [opmod]; solve [ eauto with reify_cache_gen nocore ] ]; + repeat lazymatch goal with + | [ H : _ |- _ ] => tryif constr_eq H marker then fail else revert H + end; + clear marker + | ]. + Local Ltac cache_reify_faster_2arg _ := + precache_reify_faster (); + [ lazymatch goal with + | [ |- forall bw n m m' v, ?interp ?ev bw n m m' v = ?interp' ?reified_mul_gen bw n m m' (@?A bw n m m' v) (@?B bw n m m' v) ] + => let rv := constr:(fun F bw n m m' v => (F bw n m m' (A bw n m m' v) (B bw n m m' v)):list Z) in + intros; + instantiate (1:=ltac:(let r := Reify rv in + refine (r @ reified_mul_gen)%Expr)) + end; + reflexivity + | prove_Wf () ]. + Local Ltac cache_reify_faster_1arg _ := + precache_reify_faster (); + [ lazymatch goal with + | [ |- forall bw n m m', ?interp ?ev bw n m m' = ?interp' ?reified_op_gen bw n m m' (@?A bw n m m') ] + => let rv := constr:(fun F bw n m m' => (F bw n m m' (A bw n m m')):list Z) in + intros; + instantiate (1:=ltac:(let r := Reify rv in + refine (r @ reified_op_gen)%Expr)) + end; + reflexivity + | prove_Wf () ]. + + (** +<< +#!/usr/bin/env python + +indent = ' ' + +print((indent + '(' + r'''** +<< +%s +>> +*''' + ')\n') % open(__file__, 'r').read()) + +for i in ('mul', 'add', 'sub', 'opp', 'to_bytes', 'from_bytes', 'nonzero'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. Time cache_reify (). Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + +for i in ('square', 'encode', 'from_montgomery'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) +Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + + +for i in ('zero', 'one'): + print((r'''%sDerive reified_%s_gen + SuchThat (is_reification_of reified_%s_gen %smod) + As reified_%s_gen_correct. +Proof. + (* Time cache_reify (). *) + (* we do something faster *) + Time cache_reify_faster_1arg (). +Time Qed. +Hint Extern 1 (_ = _) => apply_cached_reification %smod (proj1 reified_%s_gen_correct) : reify_cache_gen. +Hint Immediate (proj2 reified_%s_gen_correct) : wf_gen_cache. +Hint Rewrite (proj1 reified_%s_gen_correct) : interp_gen_cache. +Local Opaque reified_%s_gen. (* needed for making [autorewrite] not take a very long time *)''' % (indent, i, i, i, i, i, i, i, i, i)).replace('\n', '\n%s' % indent) + '\n') + +>> +*) + + Derive reified_mul_gen + SuchThat (is_reification_of reified_mul_gen mulmod) + As reified_mul_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification mulmod (proj1 reified_mul_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_mul_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_mul_gen_correct) : interp_gen_cache. + Local Opaque reified_mul_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_add_gen + SuchThat (is_reification_of reified_add_gen addmod) + As reified_add_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification addmod (proj1 reified_add_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_add_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_add_gen_correct) : interp_gen_cache. + Local Opaque reified_add_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_sub_gen + SuchThat (is_reification_of reified_sub_gen submod) + As reified_sub_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification submod (proj1 reified_sub_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_sub_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_sub_gen_correct) : interp_gen_cache. + Local Opaque reified_sub_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_opp_gen + SuchThat (is_reification_of reified_opp_gen oppmod) + As reified_opp_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification oppmod (proj1 reified_opp_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_opp_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_opp_gen_correct) : interp_gen_cache. + Local Opaque reified_opp_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_to_bytes_gen + SuchThat (is_reification_of reified_to_bytes_gen to_bytesmod) + As reified_to_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification to_bytesmod (proj1 reified_to_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_to_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_to_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_to_bytes_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_from_bytes_gen + SuchThat (is_reification_of reified_from_bytes_gen from_bytesmod) + As reified_from_bytes_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification from_bytesmod (proj1 reified_from_bytes_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_from_bytes_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_from_bytes_gen_correct) : interp_gen_cache. + Local Opaque reified_from_bytes_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_nonzero_gen + SuchThat (is_reification_of reified_nonzero_gen nonzeromod) + As reified_nonzero_gen_correct. + Proof. Time cache_reify (). Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification nonzeromod (proj1 reified_nonzero_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_nonzero_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_nonzero_gen_correct) : interp_gen_cache. + Local Opaque reified_nonzero_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_square_gen + SuchThat (is_reification_of reified_square_gen squaremod) + As reified_square_gen_correct. + Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification squaremod (proj1 reified_square_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_square_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_square_gen_correct) : interp_gen_cache. + Local Opaque reified_square_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_encode_gen + SuchThat (is_reification_of reified_encode_gen encodemod) + As reified_encode_gen_correct. + Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification encodemod (proj1 reified_encode_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_encode_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_encode_gen_correct) : interp_gen_cache. + Local Opaque reified_encode_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_from_montgomery_gen + SuchThat (is_reification_of reified_from_montgomery_gen from_montgomerymod) + As reified_from_montgomery_gen_correct. + Proof. + Time cache_reify (). + (* we would do something faster, but it breaks extraction COQBUG(https://github.com/coq/coq/issues/7954) *) + (* Time cache_reify_faster_2arg (). *) + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification from_montgomerymod (proj1 reified_from_montgomery_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_from_montgomery_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_from_montgomery_gen_correct) : interp_gen_cache. + Local Opaque reified_from_montgomery_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_zero_gen + SuchThat (is_reification_of reified_zero_gen zeromod) + As reified_zero_gen_correct. + Proof. + (* Time cache_reify (). *) + (* we do something faster *) + Time cache_reify_faster_1arg (). + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification zeromod (proj1 reified_zero_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_zero_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_zero_gen_correct) : interp_gen_cache. + Local Opaque reified_zero_gen. (* needed for making [autorewrite] not take a very long time *) + + Derive reified_one_gen + SuchThat (is_reification_of reified_one_gen onemod) + As reified_one_gen_correct. + Proof. + (* Time cache_reify (). *) + (* we do something faster *) + Time cache_reify_faster_1arg (). + Time Qed. + Hint Extern 1 (_ = _) => apply_cached_reification onemod (proj1 reified_one_gen_correct) : reify_cache_gen. + Hint Immediate (proj2 reified_one_gen_correct) : wf_gen_cache. + Hint Rewrite (proj1 reified_one_gen_correct) : interp_gen_cache. + Local Opaque reified_one_gen. (* needed for making [autorewrite] not take a very long time *) +End WordByWordMontgomery. diff --git a/src/SlowPrimeSynthesisExamples.v b/src/SlowPrimeSynthesisExamples.v index 8da9e8776..74feb7b40 100644 --- a/src/SlowPrimeSynthesisExamples.v +++ b/src/SlowPrimeSynthesisExamples.v @@ -3,7 +3,7 @@ Require Import Coq.Strings.String. Require Import Coq.derive.Derive. Require Import Coq.Lists.List. Require Import Crypto.Arithmetic. -Require Import Crypto.PushButtonSynthesis. +Require Import Crypto.PushButtonSynthesis.UnsaturatedSolinas. Require Import Crypto.CStringification. Require Import Crypto.Util.Notations. diff --git a/src/StandaloneHaskellMain.v b/src/StandaloneHaskellMain.v index 1a07b827f..229b3237b 100644 --- a/src/StandaloneHaskellMain.v +++ b/src/StandaloneHaskellMain.v @@ -6,7 +6,6 @@ Require Import Coq.Strings.String. Require Crypto.Util.Strings.String. Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.HexString. -Require Import Crypto.PushButtonSynthesis. Require Import Crypto.CLI. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope string_scope. diff --git a/src/StandaloneOCamlMain.v b/src/StandaloneOCamlMain.v index cb2a20904..08038730d 100644 --- a/src/StandaloneOCamlMain.v +++ b/src/StandaloneOCamlMain.v @@ -7,7 +7,6 @@ Require Import Coq.Strings.String. Require Crypto.Util.Strings.String. Require Import Crypto.Util.Strings.Decimal. Require Import Crypto.Util.Strings.HexString. -Require Import Crypto.PushButtonSynthesis. Require Import Crypto.CLI. Require Import Crypto.Util.Notations. Import ListNotations. Local Open Scope string_scope. -- cgit v1.2.3