diff options
author | Jason Gross <jgross@mit.edu> | 2017-05-14 19:44:36 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-05-14 19:48:44 -0400 |
commit | cb50e3f370588e02d1726363d5b64bd00ef49f5b (patch) | |
tree | a92b54fa9f2569af6b4382f037f3220bffebe813 /src | |
parent | 1c8c702b7ee5b1f62496e6fdf9070332a344f4f7 (diff) |
Use specialized square in ladderstep
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/IntegrationTestLadderstep.v | 40 | ||||
-rw-r--r-- | src/Specific/IntegrationTestSquare.v | 4 |
2 files changed, 35 insertions, 9 deletions
diff --git a/src/Specific/IntegrationTestLadderstep.v b/src/Specific/IntegrationTestLadderstep.v index 3e944b7c6..6b92b51b9 100644 --- a/src/Specific/IntegrationTestLadderstep.v +++ b/src/Specific/IntegrationTestLadderstep.v @@ -52,16 +52,42 @@ Section BoundedField25p5. (** TODO(jadep,andreser): Move to NewBaseSystemTest? *) Definition FMxzladderstep := @M.xzladderstep (F m) F.add F.sub F.mul. + Section with_notations. + Local Infix "+" := (proj1_sig add_sig). + Local Notation "a * b" := (proj1_sig carry_sig (proj1_sig mul_sig a b)). + Local Notation "x ^ 2" := (proj1_sig carry_sig (proj1_sig square_sig x)). + Local Infix "-" := (proj1_sig sub_sig). + Definition Mxzladderstep a24 x1 Q Q' + := match Q, Q' with + | (x, z), (x', z') + => dlet A := x+z in + dlet B := x-z in + dlet AA := A^2 in + dlet BB := B^2 in + dlet x2 := AA*BB in + dlet E := AA-BB in + dlet z2 := E*(AA + a24*E) in + dlet C := x'+z' in + dlet D := x'-z' in + dlet CB := C*B in + dlet DA := D*A in + dlet x3 := (DA+CB)^2 in + dlet z3 := x1*(DA-CB)^2 in + ((x2, z2), (x3, z3))%core + end. + End with_notations. + + (** 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))). + exists Mxzladderstep. intros. - cbv [FMxzladderstep M.xzladderstep]. + cbv [Mxzladderstep 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). + repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig square_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig). reflexivity. Defined. @@ -101,13 +127,13 @@ Section BoundedField25p5. rewrite <- (proj2_sig Mxzladderstep_sig). apply f_equal. cbv [proj1_sig]; cbv [Mxzladderstep_sig]. - context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _). - cbv [M.xzladderstep a24_sig]. - do 4 lazymatch goal with + context_to_dlet_in_rhs (@Mxzladderstep _). + cbv [Mxzladderstep M.xzladderstep a24_sig]. + do 5 lazymatch goal with | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] => context_to_dlet_in_rhs (@proj1_sig a b f_sig) end. - cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd]. + cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig square_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd]. refine (proj2 FINAL). } subst feW feW_bounded; cbv beta. (* jgross start here! *) diff --git a/src/Specific/IntegrationTestSquare.v b/src/Specific/IntegrationTestSquare.v index b0b5e5b5a..eb91a13ff 100644 --- a/src/Specific/IntegrationTestSquare.v +++ b/src/Specific/IntegrationTestSquare.v @@ -54,8 +54,8 @@ Section BoundedField25p5. eexists_sig_etransitivity. all:cbv [phi]. rewrite <- (proj2_sig square_sig). symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a a)). - change (proj1_sig carry_sig (proj1_sig square_sig ?a ?a)) with (carry_squareZ a). + set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a)). + change (proj1_sig carry_sig (proj1_sig square_sig ?a)) with (carry_squareZ a). context_to_dlet_in_rhs carry_squareZ. cbv beta iota delta [carry_squareZ proj1_sig square_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. reflexivity. |