From 3ca227f1137e6a3b65bc33f5689e1c230d591595 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 8 Jan 2019 04:21:38 -0500 Subject: remove old pipeline --- src/Arithmetic/Core.v | 1431 ------------------------------------------------- 1 file changed, 1431 deletions(-) delete mode 100644 src/Arithmetic/Core.v (limited to 'src/Arithmetic/Core.v') diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v deleted file mode 100644 index 48046d7e3..000000000 --- a/src/Arithmetic/Core.v +++ /dev/null @@ -1,1431 +0,0 @@ -(***** - -This file provides a generalized version of arithmetic with "mixed -radix" numerical systems. Later, parameters are entered into the -general functions, and they are partially evaluated until only runtime -basic arithmetic operations remain. - -CPS ---- - -Fuctions are written in continuation passing style (CPS). This means -that each operation is passed a "continuation" function, which it is -expected to call on its own output (like a callback). See the end of -this comment for a motivating example explaining why we do CPS, -despite a fair amount of resulting boilerplate code for each -operation. The code block for an operation called A would look like -this: - -``` -Definition A_cps x y {T} f : T := ... - -Definition A x y := A_cps x y id. -Lemma A_cps_id x y : forall {T} f, @A_cps x y T f = f (A x y). -Hint Opaque A : uncps. -Hint Rewrite A_cps_id : uncps. - -Lemma eval_A x y : eval (A x y) = ... -Hint Rewrite eval_A : push_basesystem_eval. -``` - -`A_cps` is the main, CPS-style definition of the operation (`f` is the -continuation function). `A` is the non-CPS version of `A_cps`, simply -defined by passing an identity function to `A_cps`. `A_cps_id` states -that we can replace the CPS version with the non-cps version. `eval_A` -is the actual correctness lemma for the operation, stating that it has -the correct arithmetic properties. In general, the middle block -containing `A` and `A_cps_id` is boring boilerplate and can be safely -ignored. - -HintDbs -------- - -+ `uncps` : Converts CPS operations to their non-CPS versions. -+ `push_basesystem_eval` : Contains all the correctness lemmas for - operations in this file, which are in terms of the `eval` function. - -Positional/Associational ------------------------- - -We represent mixed-radix numbers in a few different ways: - -+ "Positional" : a tuple of numbers and a weight function (nat->Z), -which is evaluated by multiplying the `i`th element of the tuple by -`weight i`, and then summing the products. -+ "Associational" : a list of pairs of numbers--the first is the -weight, the second is the runtime value. Evaluated by multiplying each -pair and summing the products. - -The associational representation is good for basic operations like -addition and multiplication; for addition, one can simply just append -two associational lists. But the end-result code should use the -positional representation (with each digit representing a machine -word). Since converting to and fro can be easily compiled away once -the weight function is known, we use associational to write most of -the operations and liberally convert back and forth to ensure correct -output. In particular, it is important to convert before carrying. - -Runtime Operations ------------------- - -Since some instances of e.g. Z.add or Z.mul operate on (compile-time) -weights, and some operate on runtime values, we need a way to -differentiate these cases before partial evaluation. We define a -runtime_scope to mark certain additions/multiplications as runtime -values, so they will not be unfolded during partial evaluation. For -instance, if we have: - -``` -Definition f (x y : Z * Z) := (fst x + fst y, (snd x + snd y)%RT). -``` - -then when we are partially evaluating `f`, we can easily exclude the -runtime operations (`cbv - [runtime_add]`) and prevent Coq from trying -to simplify the second addition. - - -Why CPS? --------- - -Let's suppose we want to add corresponding elements of two `list Z`s -(so on inputs `[1,2,3]` and `[2,3,1]`, we get `[3,5,4]`). We might -write our function like this : - -``` -Fixpoint add_lists (p q : list Z) := - match p, q with - | p0 :: p', q0 :: q' => - dlet sum := p0 + q0 in - sum :: add_lists p' q' - | _, _ => nil - end. -``` - -(Note : `dlet` is a notation for `Let_In`, which is just a dumb -wrapper for `let`. This allows us to `cbv - [Let_In]` if we want to -not simplify certain `let`s.) - -A CPS equivalent of `add_lists` would look like this: - -``` -Fixpoint add_lists_cps (p q : list Z) {T} (f:list Z->T) := - match p, q with - | p0 :: p', q0 :: q' => - dlet sum := p0 + q0 in - add_lists_cps p' q' (fun r => f (sum :: r)) - | _, _ => f nil - end. -``` - -Now let's try some partial evaluation. The expression we'll evaluate is: - -``` -Definition x := - (fun a0 a1 a2 b0 b1 b2 => - let r := add_lists [a0;a1;a2] [b0;b1;b2] in - let rr := add_lists r r in - add_lists rr rr). -``` - -Or, using `add_lists_cps`: - -``` -Definition y := - (fun a0 a1 a2 b0 b1 b2 => - add_lists_cps [a0;a1;a2] [b0;b1;b2] - (fun r => add_lists_cps r r - (fun rr => add_lists_cps rr rr id))). -``` - -If we run `Eval cbv -[Z.add] in x` and `Eval cbv -[Z.add] in y`, we get -identical output: - -``` -fun a0 a1 a2 b0 b1 b2 : Z => - [a0 + b0 + (a0 + b0) + (a0 + b0 + (a0 + b0)); - a1 + b1 + (a1 + b1) + (a1 + b1 + (a1 + b1)); - a2 + b2 + (a2 + b2) + (a2 + b2 + (a2 + b2))] -``` - -However, there are a lot of common subexpressions here--this is what -the `dlet` we put into the functions should help us avoid. Let's try -`Eval cbv -[Let_In Z.add] in x`: - -``` -fun a0 a1 a2 b0 b1 b2 : Z => - (fix add_lists (p q : list Z) {struct p} : - list Z := - match p with - | [] => [] - | p0 :: p' => - match q with - | [] => [] - | q0 :: q' => - dlet sum := p0 + q0 in - sum :: add_lists p' q' - end - end) - ((fix add_lists (p q : list Z) {struct p} : - list Z := - match p with - | [] => [] - | p0 :: p' => - match q with - | [] => [] - | q0 :: q' => - dlet sum := p0 + q0 in - sum :: add_lists p' q' - end - end) - (dlet sum := a0 + b0 in - sum - :: (dlet sum0 := a1 + b1 in - sum0 :: (dlet sum1 := a2 + b2 in - [sum1]))) - (dlet sum := a0 + b0 in - sum - :: (dlet sum0 := a1 + b1 in - sum0 :: (dlet sum1 := a2 + b2 in - [sum1])))) - ((fix add_lists (p q : list Z) {struct p} : - list Z := - match p with - | [] => [] - | p0 :: p' => - match q with - | [] => [] - | q0 :: q' => - dlet sum := p0 + q0 in - sum :: add_lists p' q' - end - end) - (dlet sum := a0 + b0 in - sum - :: (dlet sum0 := a1 + b1 in - sum0 :: (dlet sum1 := a2 + b2 in - [sum1]))) - (dlet sum := a0 + b0 in - sum - :: (dlet sum0 := a1 + b1 in - sum0 :: (dlet sum1 := a2 + b2 in - [sum1])))) -``` - -Not so great. Because the `dlet`s are stuck in the inner terms, we -can't simplify the expression very nicely. Let's try that on the CPS -version (`Eval cbv -[Let_In Z.add] in y`): - -``` -fun a0 a1 a2 b0 b1 b2 : Z => - dlet sum := a0 + b0 in - dlet sum0 := a1 + b1 in - dlet sum1 := a2 + b2 in - dlet sum2 := sum + sum in - dlet sum3 := sum0 + sum0 in - dlet sum4 := sum1 + sum1 in - dlet sum5 := sum2 + sum2 in - dlet sum6 := sum3 + sum3 in - dlet sum7 := sum4 + sum4 in - [sum5; sum6; sum7] -``` - -Isn't that lovely? Since we can push continuation functions "under" -the `dlet`s, we can end up with a nice, concise, simplified -expression. - -One might suggest that we could just inline the `dlet`s and do common -subexpression elimination. But some of our terms have so many `dlet`s -that inlining them all would make a term too huge to process in -reasonable time, so this is not really an option. - -*****) - -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.omega.Omega. -Require Import Coq.ZArith.BinIntDef. -Local Open Scope Z_scope. - -Require Import Crypto.Algebra.Nsatz. -Require Import Crypto.Util.Decidable Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Crypto.Util.Sigma. -Require Import Crypto.Util.CPSUtil Crypto.Util.Prod. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Zselect. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.CPS. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.UniquePose. -Require Import Crypto.Util.Tactics.VM. -Require Import Crypto.Util.IdfunWithAlt. -Require Import Crypto.Util.Notations. - -Require Import Coq.Lists.List. Import ListNotations. -Require Crypto.Util.Tuple. Local Notation tuple := Tuple.tuple. - -Local Ltac prove_id := - repeat match goal with - | _ => progress intros - | _ => progress simpl - | _ => progress cbv [Let_In] - | _ => progress (autorewrite with uncps push_id in * ) - | _ => break_innermost_match_step - | _ => contradiction - | _ => reflexivity - | _ => nsatz - | _ => solve [auto] - end. - -Create HintDb push_basesystem_eval discriminated. -Local Ltac prove_eval := - repeat match goal with - | _ => progress intros - | _ => progress simpl - | _ => progress cbv [Let_In] - | _ => progress Z.ltb_to_lt - | _ => progress (autorewrite with push_basesystem_eval uncps push_id cancel_pair in * ) - | _ => break_innermost_match_step - | _ => split - | H : _ /\ _ |- _ => destruct H - | H : Some _ = Some _ |- _ => progress (inversion H; subst) - | _ => discriminate - | _ => reflexivity - | _ => nsatz - end. - -Definition mod_eq (m:positive) a b := a mod m = b mod m. -Global Instance mod_eq_equiv m : RelationClasses.Equivalence (mod_eq m). -Proof. constructor; congruence. Qed. -Definition mod_eq_dec m a b : {mod_eq m a b} + {~ mod_eq m a b} - := Z.eq_dec _ _. -Lemma mod_eq_Z2F_iff m a b : - mod_eq m a b <-> Logic.eq (F.of_Z m a) (F.of_Z m b). -Proof. rewrite <-F.eq_of_Z_iff; reflexivity. Qed. - -Delimit Scope runtime_scope with RT. - -Definition runtime_mul := Z.mul. -Global Notation "a * b" := (runtime_mul a%RT b%RT) : runtime_scope. -Definition runtime_add := Z.add. -Global Notation "a + b" := (runtime_add a%RT b%RT) : runtime_scope. -Definition runtime_opp := Z.opp. -Global Notation "- a" := (runtime_opp a%RT) : runtime_scope. -Definition runtime_and := Z.land. -Global Notation "a &' b" := (runtime_and a%RT b%RT) : runtime_scope. -Definition runtime_shr := Z.shiftr. -Global Notation "a >> b" := (runtime_shr a%RT b%RT) : runtime_scope. -Definition runtime_lor := Z.lor. -Global Arguments runtime_lor (_ _)%RT. - -Ltac cbv_runtime := cbv beta delta [runtime_add runtime_and runtime_lor runtime_mul runtime_opp runtime_shr]. - -Module B. - Definition limb := (Z*Z)%type. (* position coefficient and run-time value *) - Module Associational. - Definition eval (p:list limb) : Z := - List.fold_right Z.add 0%Z (List.map (fun t => fst t * snd t) p). - - Lemma eval_nil : eval nil = 0. Proof. reflexivity. Qed. - Lemma eval_cons p q : eval (p::q) = (fst p) * (snd p) + eval q. Proof. reflexivity. Qed. - Lemma eval_app p q: eval (p++q) = eval p + eval q. - Proof. induction p; simpl eval; rewrite ?eval_nil, ?eval_cons; nsatz. Qed. - Hint Rewrite eval_nil eval_cons eval_app : push_basesystem_eval. - - Definition multerm (t t' : limb) : limb := - (fst t * fst t', (snd t * snd t')%RT). - Lemma eval_map_multerm (a:limb) (q:list limb) - : eval (List.map (multerm a) q) = fst a * snd a * eval q. - Proof. - induction q; cbv [multerm]; simpl List.map; - autorewrite with push_basesystem_eval cancel_pair; nsatz. - Qed. Hint Rewrite eval_map_multerm : push_basesystem_eval. - - Definition mul_cps (p q:list limb) {T} (f : list limb->T) := - flat_map_cps (fun t => @map_cps _ _ (multerm t) q) p f. - - Definition mul (p q:list limb) := mul_cps p q id. - Lemma mul_cps_id p q: forall {T} f, @mul_cps p q T f = f (mul p q). - Proof. cbv [mul_cps mul]; prove_id. Qed. - Hint Opaque mul : uncps. - Hint Rewrite mul_cps_id : uncps. - - Lemma eval_mul p q: eval (mul p q) = eval p * eval q. - Proof. cbv [mul mul_cps]; induction p; prove_eval. Qed. - Hint Rewrite eval_mul : push_basesystem_eval. - - Section split_cps. - Context (s:Z) {T : Type}. - - Fixpoint split_cps (xs:list limb) - (f :list limb*list limb->T) := - match xs with - | nil => f (nil, nil) - | cons x xs' => - split_cps xs' - (fun sxs' => - Z.eqb_cps (fst x mod s) 0 - (fun b => - if b - then f (fst sxs', cons (fst x / s, snd x) (snd sxs')) - else f (cons x (fst sxs'), snd sxs'))) - end. - End split_cps. - - Definition split s xs := split_cps s xs id. - Lemma split_cps_id s p: forall {T} f, - @split_cps s T p f = f (split s p). - Proof. - induction p as [|?? IHp]; - repeat match goal with - | _ => rewrite IHp - | _ => progress (cbv [split]; prove_id) - end. - Qed. - Hint Opaque split : uncps. - Hint Rewrite split_cps_id : uncps. - - Lemma eval_split s p (s_nonzero:s<>0): - eval (fst (split s p)) + s*eval (snd (split s p)) = eval p. - Proof. - cbv [split]; induction p; prove_eval. - match goal with - H:_ |- _ => - unique pose proof (Z_div_exact_full_2 _ _ s_nonzero H) - end; nsatz. - Qed. Hint Rewrite @eval_split using auto : push_basesystem_eval. - - Definition reduce_cps (s:Z) (c:list limb) (p:list limb) - {T} (f : list limb->T) := - split_cps s p - (fun ab => mul_cps c (snd ab) - (fun rr =>f (fst ab ++ rr))). - - Definition reduce s c p := reduce_cps s c p id. - Lemma reduce_cps_id s c p {T} f: - @reduce_cps s c p T f = f (reduce s c p). - Proof. cbv [reduce_cps reduce]; prove_id. Qed. - Hint Opaque reduce : uncps. - Hint Rewrite reduce_cps_id : uncps. - - Lemma reduction_rule a b s c m (m_eq:Z.pos m = s - c): - (a + s * b) mod m = (a + c * b) mod m. - Proof. - rewrite m_eq. pose proof (Pos2Z.is_pos m). - replace (a + s * b) with ((a + c*b) + b*(s-c)) by ring. - rewrite Z.add_mod, Z_mod_mult, Z.add_0_r, Z.mod_mod by omega. - trivial. - Qed. - Lemma eval_reduce s c p (s_nonzero:s<>0) m (m_eq : Z.pos m = s - eval c) : - mod_eq m (eval (reduce s c p)) (eval p). - Proof. - cbv [reduce reduce_cps mod_eq]; prove_eval. - erewrite <-reduction_rule by eauto; prove_eval. - Qed. - Hint Rewrite eval_reduce using (omega || assumption) : push_basesystem_eval. - (* Why TF does this hint get picked up outside the section (while other eval_ hints do not?) *) - - - Definition negate_snd_cps (p:list limb) {T} (f:list limb ->T) := - map_cps (fun cx => (fst cx, (-snd cx)%RT)) p f. - - Definition negate_snd p := negate_snd_cps p id. - Lemma negate_snd_id p {T} f : @negate_snd_cps p T f = f (negate_snd p). - Proof. cbv [negate_snd_cps negate_snd]; prove_id. Qed. - Hint Opaque negate_snd : uncps. - Hint Rewrite negate_snd_id : uncps. - - Lemma eval_negate_snd p : eval (negate_snd p) = - eval p. - Proof. - cbv [negate_snd_cps negate_snd]; induction p; prove_eval. - Qed. Hint Rewrite eval_negate_snd : push_basesystem_eval. - - Section Carries. - Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}. - Let modulo x y := modulo_cps _ x y id. - Let div x y := div_cps _ x y id. - Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)} - {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}. - Context {div_mod : forall a b:Z, b <> 0 -> - a = b * (div a b) + modulo a b}. - Hint Rewrite modulo_cps_id div_cps_id : uncps. - - Definition carryterm_cps (w fw:Z) (t:limb) {T} (f:list limb->T) := - Z.eqb_cps (fst t) w (fun eqb => - if eqb - then dlet t2 := snd t in - div_cps _ t2 fw (fun d2 => - modulo_cps _ t2 fw (fun m2 => - dlet d2 := d2 in - dlet m2 := m2 in - f ((w*fw, d2) :: (w, m2) :: @nil limb))) - else f [t]). - - Definition carryterm w fw t := carryterm_cps w fw t id. - Lemma carryterm_cps_id w fw t {T} f : - @carryterm_cps w fw t T f - = f (@carryterm w fw t). - Proof using div_cps_id modulo_cps_id. - cbv [carryterm_cps carryterm Let_In]; prove_id. - Qed. - Hint Opaque carryterm : uncps. - Hint Rewrite carryterm_cps_id : uncps. - - - Lemma eval_carryterm w fw (t:limb) (fw_nonzero:fw<>0): - eval (carryterm w fw t) = eval [t]. - Proof using Type*. - cbv [carryterm_cps carryterm Let_In]; prove_eval. - specialize (div_mod (snd t) fw fw_nonzero). - nsatz. - Qed. Hint Rewrite eval_carryterm using auto : push_basesystem_eval. - - Definition carry_cps (w fw:Z) (p:list limb) {T} (f:list limb->T) := - flat_map_cps (carryterm_cps w fw) p f. - - Definition carry w fw p := carry_cps w fw p id. - Lemma carry_cps_id w fw p {T} f: - @carry_cps w fw p T f = f (carry w fw p). - Proof using div_cps_id modulo_cps_id. - cbv [carry_cps carry]; prove_id. - Qed. - Hint Opaque carry : uncps. - Hint Rewrite carry_cps_id : uncps. - - Lemma eval_carry w fw p (fw_nonzero:fw<>0): - eval (carry w fw p) = eval p. - Proof using Type*. cbv [carry_cps carry]; induction p; prove_eval. Qed. - Hint Rewrite eval_carry using auto : push_basesystem_eval. - End Carries. - - End Associational. - - Ltac div_mod_cps_t := - intros; autorewrite with uncps push_id; try reflexivity. - - Hint Rewrite - @Associational.reduce_cps_id - @Associational.split_cps_id - @Associational.mul_cps_id : uncps. - Hint Rewrite - @Associational.carry_cps_id - @Associational.carryterm_cps_id - using div_mod_cps_t : uncps. - - - Module Positional. - Section Positional. - Import Associational. - Context (weight : nat -> Z) (* [weight i] is the weight of position [i] *) - (weight_0 : weight 0%nat = 1%Z) - (weight_nonzero : forall i, weight i <> 0). - - (** Converting from positional to associational *) - Definition to_associational_cps {n:nat} (xs:tuple Z n) - {T} (f:list limb->T) := - map_cps weight (seq 0 n) - (fun r => - to_list_cps n xs (fun rr => combine_cps r rr f)). - - Definition to_associational {n} xs := - @to_associational_cps n xs _ id. - Lemma to_associational_cps_id {n} x {T} f: - @to_associational_cps n x T f = f (to_associational x). - Proof using Type. cbv [to_associational_cps to_associational]; prove_id. Qed. - Hint Opaque to_associational : uncps. - Hint Rewrite @to_associational_cps_id : uncps. - - Definition eval {n} x := - @to_associational_cps n x _ Associational.eval. - - Lemma eval_single (x:Z) : eval (n:=1) x = weight 0%nat * x. - Proof. cbv - [Z.mul Z.add]. ring. Qed. - - Lemma eval_unit : eval (n:=0) tt = 0. - Proof. reflexivity. Qed. - Hint Rewrite eval_unit eval_single : push_basesystem_eval. - - Lemma eval_to_associational {n} x : - Associational.eval (@to_associational n x) = eval x. - Proof using Type. - cbv [to_associational_cps eval to_associational]; prove_eval. - Qed. Hint Rewrite @eval_to_associational : push_basesystem_eval. - - (** (modular) equality that tolerates redundancy **) - Definition eq {sz} m (a b : tuple Z sz) : Prop := - mod_eq m (eval a) (eval b). - - (** Converting from associational to positional *) - - Definition zeros n : tuple Z n := Tuple.repeat 0 n. - Lemma eval_zeros n : eval (zeros n) = 0. - Proof using Type. - cbv [eval Associational.eval to_associational_cps zeros]. - pose proof (seq_length n 0). generalize dependent (seq 0 n). - intro xs; revert n; induction xs as [|?? IHxs]; intros n H; - [autorewrite with uncps; reflexivity|]. - destruct n as [|n]; [distr_length|]. - specialize (IHxs n). autorewrite with uncps in *. - rewrite !@Tuple.to_list_repeat in *. - simpl List.repeat. rewrite map_cons, combine_cons, map_cons. - simpl fold_right. rewrite IHxs by distr_length. ring. - Qed. Hint Rewrite eval_zeros : push_basesystem_eval. - - Definition add_to_nth_cps {n} i x t {T} (f:tuple Z n->T) := - @on_tuple_cps _ _ 0 (update_nth_cps i (runtime_add x)) n n t _ f. - - Definition add_to_nth {n} i x t := @add_to_nth_cps n i x t _ id. - Lemma add_to_nth_cps_id {n} i x xs {T} f: - @add_to_nth_cps n i x xs T f = f (add_to_nth i x xs). - Proof using weight. - cbv [add_to_nth_cps add_to_nth]; erewrite !on_tuple_cps_correct - by (intros; autorewrite with uncps; reflexivity); prove_id. - Unshelve. - intros; subst. autorewrite with uncps push_id. distr_length. - Qed. - Hint Opaque add_to_nth : uncps. - Hint Rewrite @add_to_nth_cps_id : uncps. - - Lemma eval_add_to_nth {n} (i:nat) (x:Z) (H:(i progress (apply Zminus_eq; ring_simplify) - | _ => progress autorewrite with push_basesystem_eval cancel_pair distr_length - | _ => progress rewrite <-?ListUtil.map_nth_default_always, ?map_fst_combine, ?List.firstn_all2, ?ListUtil.map_nth_default_always, ?nth_default_seq_inbouns, ?plus_O_n - end; trivial; lia. - Unshelve. - intros; subst. autorewrite with uncps push_id. distr_length. - Qed. Hint Rewrite @eval_add_to_nth using omega : push_basesystem_eval. - - Section place_cps. - Context {T : Type}. - - Fixpoint place_cps (t:limb) (i:nat) (f:nat * Z->T) := - Z.eqb_cps (fst t mod weight i) 0 (fun eqb => - if eqb - then f (i, let c := fst t / weight i in (c * snd t)%RT) - else match i with S i' => place_cps t i' f | O => f (O, fst t * snd t)%RT end). - End place_cps. - - Definition place t i := place_cps t i id. - Lemma place_cps_id t i {T} f : - @place_cps T t i f = f (place t i). - Proof using Type. cbv [place]; induction i; prove_id. Qed. - Hint Opaque place : uncps. - Hint Rewrite place_cps_id : uncps. - - Lemma place_cps_in_range (t:limb) (n:nat) - : (fst (place_cps t n id) < S n)%nat. - Proof using Type. induction n; simpl; cbv [Z.eqb_cps]; break_match; simpl; omega. Qed. - Lemma weight_place_cps t i - : weight (fst (place_cps t i id)) * snd (place_cps t i id) - = fst t * snd t. - Proof using Type*. - induction i; cbv [id]; simpl place_cps; cbv [Z.eqb_cps]; break_match; - Z.ltb_to_lt; - autorewrite with cancel_pair; - try match goal with [H:_|-_] => apply Z_div_exact_full_2 in H end; - nsatz || auto. - Qed. - - Definition from_associational_cps n (p:list limb) - {T} (f:tuple Z n->T):= - fold_right_cps2 - (fun t st T' f' => - place_cps t (pred n) - (fun p=> add_to_nth_cps (fst p) (snd p) st f')) - (zeros n) p f. - - Definition from_associational n p := from_associational_cps n p id. - Lemma from_associational_cps_id {n} p {T} f: - @from_associational_cps n p T f = f (from_associational n p). - Proof using Type. - cbv [from_associational_cps from_associational]; prove_id. - Qed. - Hint Opaque from_associational : uncps. - Hint Rewrite @from_associational_cps_id : uncps. - - Lemma eval_from_associational {n} p (n_nonzero:n<>O): - eval (from_associational n p) = Associational.eval p. - Proof using Type*. - cbv [from_associational_cps from_associational]; induction p; - [|pose proof (place_cps_in_range a (pred n))]; prove_eval. - cbv [place]; rewrite weight_place_cps. nsatz. - Qed. - Hint Rewrite @eval_from_associational using omega - : push_basesystem_eval. - - - Section Wrappers. - (* Simple wrappers for Associational definitions; convert to - associational, do the operation, convert back. *) - - Definition add_cps {n} (p q : tuple Z n) {T} (f:tuple Z n->T) := - to_associational_cps p - (fun P => to_associational_cps q - (fun Q => from_associational_cps n (P++Q) f)). - - Definition mul_cps {n m} (p q : tuple Z n) {T} (f:tuple Z m->T) := - to_associational_cps p - (fun P => to_associational_cps q - (fun Q => Associational.mul_cps P Q - (fun PQ => from_associational_cps m PQ f))). - - Definition reduce_cps {m n} (s:Z) (c:list B.limb) (p : tuple Z m) - {T} (f:tuple Z n->T) := - to_associational_cps p - (fun P => Associational.reduce_cps s c P - (fun R => from_associational_cps n R f)). - - Definition negate_snd_cps {n} (p : tuple Z n) - {T} (f:tuple Z n->T) := - to_associational_cps p - (fun P => Associational.negate_snd_cps P - (fun R => from_associational_cps n R f)). - - Definition split_cps {n m1 m2} (s:Z) (p : tuple Z n) - {T} (f:(tuple Z m1 * tuple Z m2) -> T) := - to_associational_cps p - (fun P => Associational.split_cps s P - (fun split_P => - from_associational_cps m1 (fst split_P) - (fun m1_P => - from_associational_cps m2 (snd split_P) - (fun m2_P => - f (m1_P, m2_P))))). - - Definition scmul_cps {n} (x : Z) (p: tuple Z n) - {T} (f:tuple Z n->T) := - to_associational_cps p - (fun P => Associational.mul_cps P [(1, x)] - (fun R => from_associational_cps n R f)). - - (* This version of sub does not add balance; bounds must be - carefully handled. *) - Definition unbalanced_sub_cps {n} (p q: tuple Z n) - {T} (f:tuple Z n->T) := - to_associational_cps p - (fun P => to_associational_cps q - (fun Q => Associational.negate_snd_cps Q - (fun negQ => from_associational_cps n (P ++ negQ) f))). - - End Wrappers. - Hint Unfold - Positional.add_cps - Positional.mul_cps - Positional.reduce_cps - Positional.negate_snd_cps - Positional.split_cps - Positional.scmul_cps - Positional.unbalanced_sub_cps - . - - Section Carries. - Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}. - Let modulo x y := modulo_cps _ x y id. - Let div x y := div_cps _ x y id. - Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)} - {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}. - Context {div_mod : forall a b:Z, b <> 0 -> - a = b * (div a b) + modulo a b}. - Hint Rewrite modulo_cps_id div_cps_id : uncps. - - Definition carry_cps {n m} (index:nat) (p:tuple Z n) - {T} (f:tuple Z m->T) := - to_associational_cps p - (fun P => @Associational.carry_cps - modulo_cps div_cps - (weight index) - (weight (S index) / weight index) - P T - (fun R => from_associational_cps m R f)). - - Definition carry {n m} i p := @carry_cps n m i p _ id. - Lemma carry_cps_id {n m} i p {T} f: - @carry_cps n m i p T f = f (carry i p). - Proof. - cbv [carry_cps carry]; prove_id; rewrite carry_cps_id; reflexivity. - Qed. - Hint Opaque carry : uncps. Hint Rewrite @carry_cps_id : uncps. - - Lemma eval_carry {n m} i p: (n <> 0%nat) -> (m <> 0%nat) -> - weight (S i) / weight i <> 0 -> - eval (carry (n:=n) (m:=m) i p) = eval p. - Proof. - cbv [carry_cps carry]; intros. prove_eval. - rewrite @eval_carry by eauto. - apply eval_to_associational. - Qed. - Hint Rewrite @eval_carry : push_basesystem_eval. - - Definition carry_reduce_cps {n} - (s:Z) (c:list limb) (p : tuple Z n) - {T} (f: tuple Z n ->T) := - carry_cps (n:=n) (m:=S n) (pred n) p - (fun r => reduce_cps (m:=S n) (n:=n) s c r f). - Hint Unfold carry_reduce_cps. - - (* N.B. It is important to reverse [idxs] here. Like - [fold_right], [fold_right_cps2] is written such that the first - terms in the list are actually used last in the computation. For - example, running: - - `Eval cbv - [Z.add] in (fun a b c d => fold_right Z.add d [a;b;c]).` - - will produce [fun a b c d => (a + (b + (c + d)))].*) - Definition chained_carries_cps {n} (p:tuple Z n) (idxs : list nat) - {T} (f:tuple Z n->T) := - fold_right_cps2 carry_cps p (rev idxs) f. - - Definition chained_carries {n} p idxs := @chained_carries_cps n p idxs _ id. - Lemma chained_carries_id {n} p idxs : forall {T} f, - @chained_carries_cps n p idxs T f = f (chained_carries p idxs). - Proof using modulo_cps_id div_cps_id. - cbv [chained_carries_cps chained_carries]; prove_id. - Qed. - Hint Opaque chained_carries : uncps. - Hint Rewrite @chained_carries_id : uncps. - - Lemma eval_chained_carries {n} (p:tuple Z n) idxs : - (forall i, In i idxs -> weight (S i) / weight i <> 0) -> - eval (chained_carries p idxs) = eval p. - Proof using Type*. - cbv [chained_carries chained_carries_cps]; intros; - autorewrite with uncps push_id. - apply fold_right_invariant; [|intro; rewrite <-in_rev]; - destruct n; prove_eval; auto. - Qed. Hint Rewrite @eval_chained_carries : push_basesystem_eval. - - Definition chained_carries_reduce_cps_step {n} (s:Z) (c:list limb) {T} - (chained_carries_reduce_cps : forall (p:tuple Z n) (carry_chains : list (list nat)) (f : tuple Z n -> T), T) - (p : tuple Z n) (carry_chains : list (list nat)) - (f : tuple Z n -> T) - : T - := match carry_chains with - | nil => f p - | carry_chain :: nil - => chained_carries_cps - (n:=n) p carry_chain f - | carry_chain :: carry_chains - => chained_carries_cps - (n:=n) p carry_chain - (fun r => carry_reduce_cps (n:=n) s c r - (fun r' => chained_carries_reduce_cps r' carry_chains f)) - end. - Section chained_carries_reduce_cps. - Context {n:nat} (s:Z) (c:list limb) {T:Type}. - - Fixpoint chained_carries_reduce_cps - (p : tuple Z n) (carry_chains : list (list nat)) - (f : tuple Z n -> T) - : T - := @chained_carries_reduce_cps_step - n s c T - chained_carries_reduce_cps p carry_chains f. - End chained_carries_reduce_cps. - - Lemma step_chained_carries_reduce_cps {n} (s:Z) (c:list limb) {T} p carry_chain carry_chains (f : tuple Z n -> T) - : chained_carries_reduce_cps s c p (carry_chain :: carry_chains) f - = match length carry_chains with - | O => chained_carries_cps - (n:=n) p carry_chain f - | S _ - => chained_carries_cps - (n:=n) p carry_chain - (fun r => carry_reduce_cps (n:=n) s c r - (fun r' => chained_carries_reduce_cps s c r' carry_chains f)) - end. - Proof. - destruct carry_chains; reflexivity. - Qed. - - Definition chained_carries_reduce {n} (s:Z) (c:list limb) (p:tuple Z n) (carry_chains : list (list nat)) - : tuple Z n - := chained_carries_reduce_cps s c p carry_chains id. - - Lemma chained_carries_reduce_id {n} s c {T} p carry_chains f - : @chained_carries_reduce_cps n s c T p carry_chains f - = f (@chained_carries_reduce n s c p carry_chains). - Proof. - destruct carry_chains as [|carry_chain carry_chains]; [ reflexivity | ]. - cbv [chained_carries_reduce]. - revert p carry_chain; induction carry_chains as [|? carry_chains IHcarry_chains]; intros. - { simpl; repeat autounfold; autorewrite with uncps. reflexivity. } - { rewrite !step_chained_carries_reduce_cps. - simpl @length; cbv iota beta. - repeat autounfold; autorewrite with uncps. - rewrite !IHcarry_chains. - reflexivity. } - Qed. - Hint Opaque chained_carries_reduce : uncps. - Hint Rewrite @chained_carries_reduce_id : uncps. - - Lemma eval_chained_carries_reduce {n} (s:Z) (c:list limb) (p:tuple Z n) carry_chains - (Hn : n <> 0%nat) - (s_nonzero:s<>0) m (m_eq : Z.pos m = s - Associational.eval c) - (Hwt : weight (S (Init.Nat.pred n)) / weight (Init.Nat.pred n) <> 0) - : (List.fold_right - and - True - (List.map - (fun idxs - => forall i, In i idxs -> weight (S i) / weight i <> 0) - carry_chains)) -> - mod_eq m (eval (chained_carries_reduce s c p carry_chains)) (eval p). - Proof using Type*. - destruct carry_chains as [|carry_chain carry_chains]; [ reflexivity | ]. - cbv [chained_carries_reduce]. - revert p carry_chain; induction carry_chains as [|? carry_chains IHcarry_chains]; intros. - { cbn in *; prove_eval; auto. } - { rewrite !step_chained_carries_reduce_cps. - simpl @length; cbv iota beta. - repeat autounfold; autorewrite with uncps push_id push_basesystem_eval. - cbv [chained_carries_reduce]. - rewrite !IHcarry_chains by (cbn in *; tauto); clear IHcarry_chains. - cbn in * |- . - prove_eval; auto. } - Qed. - Hint Rewrite @eval_chained_carries_reduce using (omega || assumption) : push_basesystem_eval. - - (* Reverse of [eval]; translate from Z to basesystem by putting - everything in first digit and then carrying. This function, like - [eval], is not defined using CPS. *) - Definition encode {n} (x : Z) : tuple Z n := - chained_carries (from_associational n [(1,x)]) (seq 0 n). - Lemma eval_encode {n} x : (n <> 0%nat) -> - (forall i, In i (seq 0 n) -> weight (S i) / weight i <> 0) -> - eval (@encode n x) = x. - Proof using Type*. cbv [encode]; intros; prove_eval; auto. Qed. - Hint Rewrite @eval_encode : push_basesystem_eval. - - End Carries. - Hint Unfold carry_reduce_cps. - - Section Subtraction. - Context {m n} {coef : tuple Z n} - {coef_mod : mod_eq m (eval coef) 0}. - - Definition sub_cps (p q : tuple Z n) {T} (f:tuple Z n->T):= - add_cps coef p - (fun cp => negate_snd_cps q - (fun _q => add_cps cp _q f)). - - Definition sub p q := sub_cps p q id. - Lemma sub_id p q {T} f : @sub_cps p q T f = f (sub p q). - Proof using Type. cbv [sub_cps sub]; autounfold; prove_id. Qed. - Hint Opaque sub : uncps. - Hint Rewrite sub_id : uncps. - - Lemma eval_sub p q : mod_eq m (eval (sub p q)) (eval p - eval q). - Proof using Type*. - cbv [sub sub_cps]; autounfold; destruct n; prove_eval. - transitivity (eval coef + (eval p - eval q)). - { apply f_equal2; ring. } - { cbv [mod_eq] in *; rewrite Z.add_mod_full, coef_mod, Z.add_0_l, Zmod_mod. reflexivity. } - Qed. - - Definition opp_cps (p : tuple Z n) {T} (f:tuple Z n->T):= - sub_cps (zeros n) p f. - End Subtraction. - - (* Lemmas about converting to/from F. Will be useful in proving - that basesystem is isomorphic to F.commutative_ring_modulo.*) - Section F. - Context {sz:nat} {sz_nonzero : sz<>0%nat} {m :positive}. - Context (weight_divides : forall i : nat, weight (S i) / weight i <> 0). - Context {modulo_cps div_cps:forall {R},Z->Z->(Z->R)->R}. - Let modulo x y := modulo_cps _ x y id. - Let div x y := div_cps _ x y id. - Context {modulo_cps_id : forall R x y f, modulo_cps R x y f = f (modulo x y)} - {div_cps_id : forall R x y f, div_cps R x y f = f (div x y)}. - Context {div_mod : forall a b:Z, b <> 0 -> - a = b * (div a b) + modulo a b}. - Hint Rewrite modulo_cps_id div_cps_id : uncps. - - Definition Fencode (x : F m) : tuple Z sz := - encode (div_cps:=div_cps) (modulo_cps:=modulo_cps) (F.to_Z x). - - Definition Fdecode (x : tuple Z sz) : F m := F.of_Z m (eval x). - - Lemma Fdecode_Fencode_id x : Fdecode (Fencode x) = x. - Proof using div_mod sz_nonzero weight_0 weight_divides weight_nonzero div_cps_id modulo_cps_id. - cbv [Fdecode Fencode]; rewrite @eval_encode by eauto. - apply F.of_Z_to_Z. - Qed. - - Lemma eq_Feq_iff a b : - Logic.eq (Fdecode a) (Fdecode b) <-> eq m a b. - Proof using Type. cbv [Fdecode]; rewrite <-F.eq_of_Z_iff; reflexivity. Qed. - End F. - - - End Positional. - Hint Rewrite eval_unit eval_single : push_basesystem_eval. - - (* Helper lemmas and definitions for [eval] that to be in a - separate section so the weight function can change. *) - Section EvalHelpers. - Lemma eval_step {n} (x:tuple Z n) : forall wt z, - eval wt (Tuple.append z x) = wt 0%nat * z + eval (fun i => wt (S i)) x. - Proof. - destruct n; [reflexivity|]. - intros; cbv [eval to_associational_cps]. - autorewrite with uncps. rewrite map_S_seq. reflexivity. - Qed. - - Lemma eval_left_append {n} : forall wt x xs, - eval wt (Tuple.left_append (n:=n) x xs) - = wt n * x + eval wt xs. - Proof. - induction n as [|n IHn]; intros wt x xs; try destruct xs; - unfold Tuple.left_append; fold @Tuple.left_append; - autorewrite with push_basesystem_eval; [ring|]. - rewrite (Tuple.subst_append xs), Tuple.hd_append, Tuple.tl_append. - rewrite !eval_step, IHn. ring. - Qed. - Hint Rewrite @eval_left_append : push_basesystem_eval. - - Lemma eval_wt_equiv {n} :forall wta wtb (x:tuple Z n), - (forall i, wta i = wtb i) -> eval wta x = eval wtb x. - Proof. - destruct n as [|n]; [reflexivity|]. - induction n as [|n IHn]; intros wta wtb x H; [rewrite !eval_single, H; reflexivity|]. - simpl tuple in *; destruct x. - change (t, z) with (Tuple.append (n:=S n) z t). - rewrite !eval_step. rewrite (H 0%nat). apply Group.cancel_left. - apply IHn; auto. - Qed. - - Definition eval_from {n} weight (offset:nat) (x : tuple Z n) : Z := - eval (fun i => weight (i+offset)%nat) x. - - Lemma eval_from_0 {n} wt x : @eval_from n wt 0 x = eval wt x. - Proof. cbv [eval_from]. auto using eval_wt_equiv. Qed. - End EvalHelpers. - - Section Select. - Context {weight : nat -> Z}. - - Definition select_cps {n} (mask cond:Z) (p:tuple Z n) - {T} (f:tuple Z n->T) := - dlet t := Z.zselect cond 0 mask in Tuple.map_cps (runtime_and t) p f. - - Definition select {n} mask cond p := @select_cps n mask cond p _ id. - Lemma select_id {n} mask cond p T f : - @select_cps n mask cond p T f = f (select mask cond p). - Proof. - cbv [select select_cps Let_In]; autorewrite with uncps push_id; - reflexivity. - Qed. - Hint Opaque select : uncps. - - Lemma map_and_0 {n} (p:tuple Z n) : Tuple.map (Z.land 0) p = zeros n. - Proof. - induction n as [|n IHn]; [destruct p; reflexivity | ]. - rewrite (Tuple.subst_append p), Tuple.map_append, Z.land_0_l, IHn. - reflexivity. - Qed. - - Lemma eval_select {n} mask cond x (H:Tuple.map (Z.land mask) x = x) : - B.Positional.eval weight (@select n mask cond x) = - if dec (cond = 0) then 0 else B.Positional.eval weight x. - Proof. - cbv [select select_cps Let_In]. - autorewrite with uncps push_id. - rewrite Z.zselect_correct; break_match. - { rewrite map_and_0. apply B.Positional.eval_zeros. } - { change runtime_and with Z.land. rewrite H; reflexivity. } - Qed. - - End Select. - - End Positional. - - Hint Unfold - Positional.add_cps - Positional.mul_cps - Positional.reduce_cps - Positional.carry_reduce_cps - Positional.negate_snd_cps - Positional.split_cps - Positional.scmul_cps - Positional.unbalanced_sub_cps - Positional.opp_cps - . - Hint Rewrite - @Associational.reduce_cps_id - @Associational.split_cps_id - @Associational.mul_cps_id - @Positional.from_associational_cps_id - @Positional.place_cps_id - @Positional.add_to_nth_cps_id - @Positional.to_associational_cps_id - @Positional.sub_id - @Positional.select_id - : uncps. - Hint Rewrite - @Associational.carry_cps_id - @Associational.carryterm_cps_id - @Positional.carry_cps_id - @Positional.chained_carries_id - @Positional.chained_carries_reduce_id - using div_mod_cps_t : uncps. - Hint Rewrite - @Associational.eval_mul - @Positional.eval_single - @Positional.eval_unit - @Positional.eval_to_associational - @Positional.eval_left_append - @Associational.eval_carry - @Associational.eval_carryterm - @Associational.eval_reduce - @Associational.eval_split - @Positional.eval_zeros - @Positional.eval_carry - @Positional.eval_from_associational - @Positional.eval_add_to_nth - @Positional.eval_chained_carries - @Positional.eval_chained_carries_reduce - @Positional.eval_sub - @Positional.eval_select - using (assumption || (div_mod_cps_t; auto) || vm_decide) : push_basesystem_eval. -End B. - -(* Modulo and div that do shifts if possible, otherwise normal mod/div *) -Section DivMod. - Definition modulo_cps {T} (a b : Z) (f : Z -> T) : T := - Z.eqb_cps (2 ^ (Z.log2 b)) b (fun eqb => - if eqb - then let x := (Z.ones (Z.log2 b)) in f (a &' x)%RT - else f (Z.modulo a b)). - - Definition div_cps {T} (a b : Z) (f : Z -> T) : T := - Z.eqb_cps (2 ^ (Z.log2 b)) b (fun eqb => - if eqb - then let x := Z.log2 b in f ((a >> x)%RT) - else f (Z.div a b)). - - Definition modulo (a b : Z) : Z := modulo_cps a b id. - Definition div (a b : Z) : Z := div_cps a b id. - - Lemma modulo_id {T} a b f - : @modulo_cps T a b f = f (modulo a b). - Proof. cbv [modulo_cps modulo]; autorewrite with uncps; break_match; reflexivity. Qed. - Hint Opaque modulo : uncps. - Hint Rewrite @modulo_id : uncps. - - Lemma div_id {T} a b f - : @div_cps T a b f = f (div a b). - Proof. cbv [div_cps div]; autorewrite with uncps; break_match; reflexivity. Qed. - Hint Opaque div : uncps. - Hint Rewrite @div_id : uncps. - - Lemma div_cps_correct {T} a b f : @div_cps T a b f = f (Z.div a b). - Proof. - cbv [div_cps Z.eqb_cps]; intros. break_match; try reflexivity. - rewrite Z.shiftr_div_pow2 by apply Z.log2_nonneg. - Z.ltb_to_lt; congruence. - Qed. - - Lemma modulo_cps_correct {T} a b f : @modulo_cps T a b f = f (Z.modulo a b). - Proof. - cbv [modulo_cps Z.eqb_cps]; intros. break_match; try reflexivity. - rewrite Z.land_ones by apply Z.log2_nonneg. - Z.ltb_to_lt; congruence. - Qed. - - Definition div_correct a b : div a b = Z.div a b := div_cps_correct a b id. - Definition modulo_correct a b : modulo a b = Z.modulo a b := modulo_cps_correct a b id. - - Lemma div_mod a b (H:b <> 0) : a = b * div a b + modulo a b. - Proof. - rewrite div_correct, modulo_correct; auto using Z.div_mod. - Qed. -End DivMod. - -Hint Opaque div modulo : uncps. -Hint Rewrite @div_id @modulo_id : uncps. - -Import B. - -Create HintDb basesystem_partial_evaluation_unfolder. - -Hint Unfold - id - Associational.eval - Associational.multerm - Associational.mul_cps - Associational.mul - Associational.split_cps - Associational.split - Associational.reduce_cps - Associational.reduce - Associational.negate_snd_cps - Associational.negate_snd - Associational.carryterm_cps - Associational.carryterm - Associational.carry_cps - Associational.carry - Positional.to_associational_cps - Positional.to_associational - Positional.eval - Positional.zeros - Positional.add_to_nth_cps - Positional.add_to_nth - Positional.place_cps - Positional.place - Positional.from_associational_cps - Positional.from_associational - Positional.carry_cps - Positional.carry - Positional.chained_carries_cps - Positional.chained_carries - Positional.chained_carries_reduce_cps_step - Positional.chained_carries_reduce_cps - Positional.chained_carries_reduce - Positional.encode - Positional.add_cps - Positional.mul_cps - Positional.reduce_cps - Positional.carry_reduce_cps - Positional.negate_snd_cps - Positional.split_cps - Positional.scmul_cps - Positional.unbalanced_sub_cps - Positional.sub_cps - Positional.sub - Positional.opp_cps - Positional.Fencode - Positional.Fdecode - Positional.eval_from - Positional.select_cps - Positional.select - modulo div modulo_cps div_cps - id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' - Z.add_get_carry_full Z.add_get_carry_full_cps - : basesystem_partial_evaluation_unfolder. - -Hint Unfold - B.limb ListUtil.sum ListUtil.sum_firstn - CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2 - Decidable.dec Decidable.dec_eq_Z - id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' - Z.add_get_carry_full Z.add_get_carry_full_cps Z.mul_split Z.mul_split_cps Z.mul_split_cps' - : basesystem_partial_evaluation_unfolder. - - -Ltac basesystem_partial_evaluation_unfolder t := - eval - cbv - delta [ - (* this list must contain all definitions referenced by t that reference [Let_In], [runtime_add], [runtime_opp], [runtime_mul], [runtime_shr], or [runtime_and] *) - id - Positional.to_associational_cps Positional.to_associational - Positional.eval Positional.zeros Positional.add_to_nth_cps - Positional.add_to_nth Positional.place_cps Positional.place - Positional.from_associational_cps Positional.from_associational - Positional.carry_cps Positional.carry - Positional.chained_carries_cps Positional.chained_carries - Positional.chained_carries_reduce_cps - Positional.chained_carries_reduce - Positional.chained_carries_reduce_cps_step - Positional.sub_cps Positional.sub Positional.split_cps - Positional.scmul_cps Positional.unbalanced_sub_cps - Positional.negate_snd_cps Positional.add_cps Positional.opp_cps - Associational.eval Associational.multerm Associational.mul_cps - Associational.mul Associational.split_cps Associational.split - Associational.reduce_cps Associational.reduce - Associational.carryterm_cps Associational.carryterm - Associational.carry_cps Associational.carry - Associational.negate_snd_cps Associational.negate_snd div modulo - id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' - Z.add_get_carry_full Z.add_get_carry_full_cps - ] in t. - -Ltac pattern_strip t := - let t := (eval pattern @Let_In, - @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor, - @id_with_alt, - @Z.add_get_carry, @Z.zselect - in t) in - let t := match t with ?t _ _ _ _ _ _ _ _ _ _ => t end in - t. - -Ltac apply_patterned t1 := - constr:(t1 - (@Let_In) - (@runtime_mul) - (@runtime_add) - (@runtime_opp) - (@runtime_shr) - (@runtime_and) - (@runtime_lor) - (@id_with_alt) - (@Z.add_get_carry) - (@Z.zselect)). - -Ltac pattern_strip_full t := - let t := (eval pattern - (@Let_In Z (fun _ => Z)), - @Z.add_get_carry_cps, @Z.mul_split_at_bitwidth_cps, - (@Z.eq_dec_cps), (@Z.eqb_cps), - @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor, - (@id_with_alt Z), - @Z.add_get_carry, @Z.zselect, @Z.mul_split_at_bitwidth, - Z.mul, Z.add, Z.opp, Z.shiftr, Z.shiftl, Z.land, Z.lor, - Z.modulo, Z.div, Z.log2, Z.pow, Z.ones, - Z.eq_dec, Z.eqb, - (@ModularArithmetic.F.to_Z), (@ModularArithmetic.F.of_Z), - 2%Z, 1%Z, 0%Z - in t) in - let t := match t with ?t - _ - _ _ - _ _ - _ _ _ _ _ _ - _ - _ _ _ - _ _ _ _ _ _ _ - _ _ _ _ _ - _ _ - _ _ - _ _ _ => t end in - let t := (eval pattern Z, (@Let_In), (@id_with_alt) in t) in - let t := match t with ?t _ _ _ => t end in - t. - -Ltac apply_patterned_full t1 := - constr:(t1 - Z - (@Let_In) (@id_with_alt) - (@Let_In Z (fun _ => Z)) - (@Z.add_get_carry_cps) (@Z.mul_split_at_bitwidth_cps) - (@Z.eq_dec_cps) (@Z.eqb_cps) - (@runtime_mul) (@runtime_add) (@runtime_opp) (@runtime_shr) (@runtime_and) (@runtime_lor) - (@id_with_alt Z) - (@Z.add_get_carry) (@Z.zselect) (@Z.mul_split_at_bitwidth) - Z.mul Z.add Z.opp Z.shiftr Z.shiftl Z.land Z.lor - Z.modulo Z.div Z.log2 Z.pow Z.ones - Z.eq_dec Z.eqb - (@ModularArithmetic.F.to_Z) (@ModularArithmetic.F.of_Z) - 2%Z 1%Z 0%Z). - -Ltac basesystem_partial_evaluation_gen unfold_tac t t1 := - let t := unfold_tac t in - let t := pattern_strip t in - let dummy := match goal with _ => pose t as t1 end in - let t1' := apply_patterned t1 in - t1'. - -Ltac basesystem_partial_evaluation_RHS_gen unfold_tac := - let t := match goal with |- _ _ ?t => t end in - let t1 := fresh "t1" in - let t1' := basesystem_partial_evaluation_gen unfold_tac t t1 in - transitivity t1'; - [replace_with_vm_compute t1; clear t1|reflexivity]. - -Ltac basesystem_partial_evaluation_default_unfolder t := - basesystem_partial_evaluation_unfolder t. - -Ltac basesystem_partial_evaluation_RHS := - basesystem_partial_evaluation_RHS_gen basesystem_partial_evaluation_default_unfolder. -Ltac basesystem_partial_evaluation := - basesystem_partial_evaluation_gen basesystem_partial_evaluation_default_unfolder. - - -(** This block of tactic code works around bug #5434 - (https://coq.inria.fr/bugs/show_bug.cgi?id=5434), that - [vm_compute] breaks an invariant in pretyping/constr_matching.ml. - So we refresh all of the names in match statements in the goal by - crawling it. - - In particular, [replace_with_vm_compute] creates a [vm_compute]d - term which has anonymous binders where pretyping expects there to - be named binders. This shows up when you try to match on the - function (the branch statement of the match) with an Ltac pattern - like [(fun x : ?T => ?C)] rather than [(fun x : ?T => @?C x)]; we - use the former in reification to save the cost of many extra - invocations of [cbv beta]. Luckily, patterns like [(fun x : ?T => - @?C x)] don't trigger this anomaly, so we can walk the term, - fixing all match statements whose branches are functions whose - binder names were eaten by [vm_compute] (note that in a match, - every branch where the corresponding constructor takes arguments - is represented internally as a function (lambda term)). We fix - the match statements by pulling out the branch with the [@?] - pattern that doesn't trigger the anomaly, and then recreating the - match with a destructuring [let] that hasn't been through - [vm_compute], and therefore has name information that - constr_matching is happy with. *) -Ltac replace_match_with_destructuring_match T := - match T with - | ?F ?X - => let F' := replace_match_with_destructuring_match F in - let X' := replace_match_with_destructuring_match X in - constr:(F' X') - (* we must use [@?f a b] here and not [?f], or else we get an anomaly *) - | match ?d with pair a b => @?f a b end - => let d' := replace_match_with_destructuring_match d in - let T' := fresh in - constr:(let '(a, b) := d' in - match f a b with - | T' => ltac:(let v := (eval cbv beta delta [T'] in T') in - let v := replace_match_with_destructuring_match v in - exact v) - end) - | (fun a : ?A => @?f a) - => let T' := fresh in - let T' := fresh T' in - let T' := fresh T' in - constr:(fun a : A - => match f a with - | T' => ltac:(let v := (eval cbv beta delta [T'] in T') in - let v := replace_match_with_destructuring_match v in - exact v) - end) - | ?x => x - end. -Ltac do_replace_match_with_destructuring_match_in_goal := - let G := get_goal in - let G' := replace_match_with_destructuring_match G in - change G'. - -(* TODO : move *) -Lemma F_of_Z_opp {m} x : F.of_Z m (- x) = F.opp (F.of_Z m x). -Proof. - cbv [F.opp]; intros. rewrite F.to_Z_of_Z, <-Z.sub_0_l. - etransitivity; rewrite F.of_Z_mod; - [rewrite Z.opp_mod_mod|]; reflexivity. -Qed. - -Hint Rewrite <-@F.of_Z_add : pull_FofZ. -Hint Rewrite <-@F.of_Z_mul : pull_FofZ. -Hint Rewrite <-@F.of_Z_sub : pull_FofZ. -Hint Rewrite <-@F_of_Z_opp : pull_FofZ. - -Ltac F_mod_eq := - cbv [Positional.Fdecode]; autorewrite with pull_FofZ; - apply mod_eq_Z2F_iff. - -Ltac presolve_op_mod_eq wt x := - transitivity (Positional.eval wt x); repeat autounfold; - [ cbv [mod_eq]; apply f_equal2; [|reflexivity]; - apply f_equal - | autorewrite with uncps push_id push_basesystem_eval ]. - -Ltac solve_op_mod_eq wt x := - presolve_op_mod_eq wt x; - [ basesystem_partial_evaluation_RHS; - do_replace_match_with_destructuring_match_in_goal - | reflexivity ]. - -Ltac solve_op_F wt x := F_mod_eq; solve_op_mod_eq wt x. -Ltac presolve_op_F wt x := F_mod_eq; presolve_op_mod_eq wt x. -- cgit v1.2.3