Add 130-bit 3-register synthesis

This one has fewer operations, and so will be faster to play with

3 files changed, 350 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 0ecbfc92f..ee8537d44 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -191,8 +191,10 @@ src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
 src/Spec/Test/X25519.v
 src/Specific/ArithmeticSynthesisTest.v
+src/Specific/ArithmeticSynthesisTest130.v
 src/Specific/IntegrationTestDisplayCommon.v
 src/Specific/IntegrationTestLadderstep.v
+src/Specific/IntegrationTestLadderstep130.v
 src/Specific/IntegrationTestLadderstepDisplay.v
 src/Specific/IntegrationTestMul.v
 src/Specific/IntegrationTestMulDisplay.v
diff --git a/src/Specific/ArithmeticSynthesisTest130.v b/src/Specific/ArithmeticSynthesisTest130.v
new file mode 100644
index 000000000..e2fcebfae
--- /dev/null
+++ b/src/Specific/ArithmeticSynthesisTest130.v
@@ -0,0 +1,212 @@
+Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
+Require Import Coq.Lists.List. Import ListNotations.
+Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable.
+Require Import Crypto.Util.LetIn Crypto.Util.ZUtil Crypto.Util.Tactics.
+Require Crypto.Util.Tuple.
+Local Notation tuple := Tuple.tuple.
+Local Open Scope list_scope.
+Local Open Scope Z_scope.
+Local Coercion Z.of_nat : nat >-> Z.
+
+(***
+Modulus : 2^255-5
+Base: 130
+***)
+Section Ops51.
+  Local Infix "^" := tuple : type_scope.
+
+  (* These definitions will need to be passed as Ltac arguments (or
+  cleverly inferred) when things are eventually automated *)
+  Definition sz := 3%nat.
+  Definition s : Z := 2^255.
+  Definition c : list B.limb := [(1, 5)].
+  Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *)
+  Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)).
+  Definition carry_chain2 := ([0;1])%nat.
+
+  (* These definitions are inferred from those above *)
+  Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *)
+  Definition wt := fun i : nat =>
+                     let si := Z.log2 s * i in
+                     2 ^ ((si/sz) + (if dec ((si/sz)*sz=si) then 0 else 1)).
+  Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat.
+  Definition coef := (* subtraction coefficient *)
+    Eval vm_compute in
+      ( let p := Positional.encode
+                   (modulo:=modulo) (div:=div) (n:=sz)
+                   wt (s-Associational.eval c) in
+        (fix addp (acc: Z^sz) (ctr : nat) : Z^sz :=
+         match ctr with
+         | O => acc
+         | S n => addp (Positional.add_cps wt acc p id) n
+        end) (Positional.zeros sz) coef_div_modulus).
+  Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl.
+
+  Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed.
+  Lemma wt_nonzero i : wt i <> 0.
+  Proof.
+    apply Z.pow_nonzero; zero_bounds; try break_match; vm_decide.
+  Qed.
+
+  Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0.
+  Proof.
+    cbv [In carry_chain1] in H.
+    repeat match goal with H : _ \/ _ |- _ => destruct H end;
+      try (exfalso; assumption); subst; try vm_decide.
+  Qed.
+  Lemma wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0.
+  Proof.
+    cbv [In carry_chain2] in H.
+    repeat match goal with H : _ \/ _ |- _ => destruct H end;
+      try (exfalso; assumption); subst; try vm_decide.
+  Qed.
+  Lemma wt_divides_full i : wt (S i) / wt i <> 0.
+  Proof.
+    cbv [wt].
+    match goal with |- _ ^ ?x / _ ^ ?y <> _ => assert (0 <= y <= x) end.
+    { rewrite Nat2Z.inj_succ.
+      split; try break_match; ring_simplify;
+      repeat match goal with
+             | _ => apply Z.div_le_mono; try vm_decide; [ ]
+             | _ => apply Z.mul_le_mono_nonneg_l; try vm_decide; [ ]
+             | _ => apply Z.add_le_mono; try vm_decide; [ ]
+             | |- ?x <= ?y + 1 => assert (x <= y); [|omega]
+             | |- ?x + 1 <= ?y => rewrite <- Z.div_add by vm_decide
+             | _ => progress zero_bounds
+             | _ => progress ring_simplify
+             | _ => vm_decide
+             end. }
+    break_match; rewrite <-Z.pow_sub_r by omega;
+      apply Z.pow_nonzero; omega.
+  Qed.
+
+  Definition zero_sig :
+    { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}.
+  Proof.
+    let t := eval vm_compute in
+    (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt 0) in
+        exists t; vm_decide.
+  Defined.
+
+  Definition one_sig :
+    { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}.
+  Proof.
+    let t := eval vm_compute in
+    (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt 1) in
+        exists t; vm_decide.
+  Defined.
+
+  Definition add_sig :
+    { add : (Z^sz -> Z^sz -> Z^sz)%type |
+               forall a b : Z^sz,
+                 let eval := Positional.Fdecode (m:=m) wt in
+                 eval (add a b) = (eval a  + eval b)%F }.
+  Proof.
+    eexists; cbv beta zeta; intros.
+    pose proof wt_nonzero.
+    let x := constr:(
+        Positional.add_cps (n := sz) wt a b id) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Definition sub_sig :
+    {sub : (Z^sz -> Z^sz -> Z^sz)%type |
+               forall a b : Z^sz,
+                 let eval := Positional.Fdecode (m:=m) wt in
+                 eval (sub a b) = (eval a - eval b)%F}.
+  Proof.
+    eexists; cbv beta zeta; intros.
+    pose proof wt_nonzero.
+    let x := constr:(
+         Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Definition opp_sig :
+    {opp : (Z^sz -> Z^sz)%type |
+               forall a : Z^sz,
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (opp a) = F.opp (eval a)}.
+  Proof.
+    eexists; cbv beta zeta; intros.
+    pose proof wt_nonzero.
+    let x := constr:(
+         Positional.opp_cps (n:=sz) (coef := coef) wt a id) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Definition mul_sig :
+    {mul : (Z^sz -> Z^sz -> Z^sz)%type |
+               forall a b : Z^sz,
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (mul a b) = (eval a  * eval b)%F}.
+  Proof.
+    eexists; cbv beta zeta; intros.
+    pose proof wt_nonzero.
+    let x := constr:(
+         Positional.mul_cps (n:=sz) (m:=sz2) wt a b
+           (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in
+    solve_op_F wt x. reflexivity.
+
+    (* rough breakdown of synthesis time *)
+    (* 1.2s for side conditions -- should improve significantly when [chained_carries] gets a correctness lemma *)
+    (* basesystem_partial_evaluation_RHS (primarily vm_compute): 1.8s, which gets re-computed during defined *)
+
+    (* doing [cbv -[Let_In runtime_add runtime_mul]] took 37s *)
+
+  Defined. (* 3s *)
+
+  (* Performs a full carry loop (as specified by carry_chain) *)
+  Definition carry_sig :
+    {carry : (Z^sz -> Z^sz)%type |
+               forall a : Z^sz,
+                 let eval := Positional.Fdecode (m := m) wt in
+                 eval (carry a) = eval a}.
+  Proof.
+    eexists; cbv beta zeta; intros.
+    pose proof wt_nonzero. pose proof wt_divides_chain1.
+    pose proof div_mod. pose proof wt_divides_chain2.
+    let x := constr:(
+               Positional.chained_carries_cps (n:=sz) (div:=div)(modulo:=modulo) wt a carry_chain1
+                  (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
+                  (fun rrr => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt rrr carry_chain2 id
+             ))) in
+    solve_op_F wt x. reflexivity.
+  Defined.
+
+  Definition ring_51 :=
+    (Ring.ring_by_isomorphism
+         (F := F m)
+         (H := Z^sz)
+         (phi := Positional.Fencode wt)
+         (phi' := Positional.Fdecode wt)
+         (zero := proj1_sig zero_sig)
+         (one := proj1_sig one_sig)
+         (opp := proj1_sig opp_sig)
+         (add := proj1_sig add_sig)
+         (sub := proj1_sig sub_sig)
+         (mul := proj1_sig mul_sig)
+         (phi'_zero := proj2_sig zero_sig)
+         (phi'_one := proj2_sig one_sig)
+         (phi'_opp := proj2_sig opp_sig)
+         (Positional.Fdecode_Fencode_id
+            (sz_nonzero := sz_nonzero)
+            (div_mod := div_mod)
+            wt eq_refl wt_nonzero wt_divides_full)
+         (Positional.eq_Feq_iff wt)
+         (proj2_sig add_sig)
+         (proj2_sig sub_sig)
+         (proj2_sig mul_sig)
+      ).
+
+(*
+Eval cbv [proj1_sig add_sig] in (proj1_sig add_sig).
+Eval cbv [proj1_sig sub_sig] in (proj1_sig sub_sig).
+Eval cbv [proj1_sig opp_sig] in (proj1_sig opp_sig).
+Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig).
+Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig).
+*)
+
+End Ops51.
diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v
new file mode 100644
index 000000000..cc2853636
--- /dev/null
+++ b/src/Specific/IntegrationTestLadderstep130.v
@@ -0,0 +1,136 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
+Require Import Coq.Classes.Morphisms.
+Local Open Scope Z_scope.
+
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Crypto.Specific.ArithmeticSynthesisTest130.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.MoveLetIn.
+Require Import Crypto.Util.Tactics.SetEvars.
+Require Import Crypto.Util.Tactics.SubstEvars.
+Require Import Crypto.Curves.Montgomery.XZ.
+Import ListNotations.
+
+Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon.
+
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.
+
+Section BoundedField25p5.
+  Local Coercion Z.of_nat : nat >-> Z.
+
+  Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)).
+  Let length_lw := Eval compute in List.length limb_widths.
+
+  Local Notation b_of exp := {| lower := 0 ; upper := 2^exp + 2^(exp-3) |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *)
+  (* The definition [bounds_exp] is a tuple-version of the
+     limb-widths, which are the [exp] argument in [b_of] above, i.e.,
+     the approximate base-2 exponent of the bounds on the limb in that
+     position. *)
+  Let bounds_exp : Tuple.tuple Z length_lw
+    := Eval compute in
+        Tuple.from_list length_lw limb_widths eq_refl.
+  Let bounds : Tuple.tuple zrange length_lw
+    := Eval compute in
+        Tuple.map (fun e => b_of e) bounds_exp.
+
+  Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))).
+  Let bitwidth := Eval compute in (2^lgbitwidth)%nat.
+  Let feZ : Type := tuple Z sz.
+  Let feW : Type := tuple (wordT lgbitwidth) sz.
+  Let feBW : Type := BoundedWord sz bitwidth bounds.
+  Let phi : feBW -> F m :=
+    fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x).
+
+  (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
+  Definition FMxzladderstep := @M.xzladderstep (F m) F.add F.sub F.mul.
+
+  (** TODO(jadep,andreser): Move to NewBaseSystemTest? *)
+  Definition Mxzladderstep_sig
+    : { xzladderstep : tuple Z sz -> tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz * (tuple Z sz * tuple Z sz)
+      | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }.
+  Proof.
+    exists (@M.xzladderstep _ (proj1_sig add_sig) (proj1_sig sub_sig) (fun x y => proj1_sig carry_sig (proj1_sig mul_sig x y))).
+    intros.
+    cbv [FMxzladderstep M.xzladderstep].
+    destruct Q, Q'; cbv [map map' fst snd Let_In eval].
+    repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig).
+    reflexivity.
+  Defined.
+
+  (* TODO : change this to field once field isomorphism happens *)
+  Definition xzladderstep :
+    { xzladderstep : feBW -> feBW -> feBW * feBW -> feBW * feBW -> feBW * feBW * (feBW * feBW)
+    | forall a24 x1 Q Q', Tuple.map (n:=2) (Tuple.map (n:=2) phi) (xzladderstep a24 x1 Q Q') = FMxzladderstep (phi a24) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }.
+  Proof.
+    lazymatch goal with
+    | [ |- { f | forall a b c d, ?phi (f a b c d) = @?rhs a b c d } ]
+      => apply lift4_sig with (P:=fun a b c d f => phi f = rhs a b c d)
+    end.
+    intros.
+    eexists_sig_etransitivity. all:cbv [phi].
+    rewrite <- !(Tuple.map_map (B.Positional.Fdecode wt) (BoundedWordToZ sz bitwidth bounds)).
+    rewrite <- (proj2_sig Mxzladderstep_sig).
+    apply f_equal.
+    cbv [proj1_sig]; cbv [Mxzladderstep_sig].
+    context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _).
+    set (k := @M.xzladderstep _ _ _ _); context_to_dlet_in_rhs k; subst k.
+    cbv [M.xzladderstep].
+    lazymatch goal with
+    | [ |- context[@proj1_sig ?a ?b carry_sig] ]
+      => context_to_dlet_in_rhs (@proj1_sig a b carry_sig)
+    end.
+    lazymatch goal with
+    | [ |- context[@proj1_sig ?a ?b mul_sig] ]
+      => context_to_dlet_in_rhs (@proj1_sig a b mul_sig)
+    end.
+    lazymatch goal with
+    | [ |- context[@proj1_sig ?a ?b add_sig] ]
+      => context_to_dlet_in_rhs (@proj1_sig a b add_sig)
+    end.
+    lazymatch goal with
+    | [ |- context[@proj1_sig ?a ?b sub_sig] ]
+      => context_to_dlet_in_rhs (@proj1_sig a b sub_sig)
+    end.
+    cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz].
+    reflexivity.
+    eexists_sig_etransitivity_for_rewrite_fun.
+    { intro; cbv beta.
+      subst feBW.
+      set_evars.
+      do 2 lazymatch goal with
+           | [ |- context[Tuple.map (n:=?n) (fun x => ?f (?g x))] ]
+             => rewrite <- (Tuple.map_map (n:=n) f g : pointwise_relation _ eq _ _)
+           end.
+      subst_evars.
+      reflexivity. }
+    cbv beta.
+    apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)).
+    apply adjust_tuple2_tuple2_sig.
+    (* jgross start here! *)
+    Set Ltac Profiling.
+    (*
+    Time Glue.refine_to_reflective_glue.
+    Time ReflectiveTactics.refine_with_pipeline_correct.
+    { Time ReflectiveTactics.do_reify. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. }
+    { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. }
+    { Time SubstLet.subst_let; clear; abstract vm_cast_no_check (eq_refl true). }
+    { Time SubstLet.subst_let; clear; vm_compute; reflexivity. }
+    { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. }
+    { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. }
+    { Time abstract ReflectiveTactics.handle_bounds_from_hyps. }
+     *)
+    Time refine_reflectively.
+    Show Ltac Profile.
+  Time Defined.
+
+Time End BoundedField25p5.