diff options
Diffstat (limited to 'src/Specific/ArithmeticSynthesisTest130.v')
| -rw-r--r-- | src/Specific/ArithmeticSynthesisTest130.v | 224 |
1 files changed, 0 insertions, 224 deletions
diff --git a/src/Specific/ArithmeticSynthesisTest130.v b/src/Specific/ArithmeticSynthesisTest130.v deleted file mode 100644 index e9e40df19..000000000 --- a/src/Specific/ArithmeticSynthesisTest130.v +++ /dev/null @@ -1,224 +0,0 @@ -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.Decidable. -Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. -Require Import Crypto.Util.Tactics.BreakMatch. -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. - Definition a24 := 121665%Z. (* XXX TODO(andreser) FIXME? Is this right for this curve? *) - - (* 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. - - Local Ltac solve_constant_sig := - lazymatch goal with - | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ] - => let t := (eval vm_compute in - (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in - (exists t; vm_decide) - end. - - Definition zero_sig : - { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}. - Proof. - solve_constant_sig. - Defined. - - Definition one_sig : - { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}. - Proof. - solve_constant_sig. - Defined. - - Definition a24_sig : - { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }. - Proof. - solve_constant_sig. - 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 a b. - 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 a b. - 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 a. - 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 a b. - 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 a. - 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. |