From b1a3c63c77cd0be5679ce0e949863325a6348e7b Mon Sep 17 00:00:00 2001 From: jadep Date: Sat, 1 Apr 2017 13:53:51 -0400 Subject: insert a reduce step in the correct place of the carry chain --- src/NewBaseSystem.v | 26 +++++++++++++++++--------- src/Specific/NewBaseSystemTest.v | 31 +++++++++++++++++++++---------- 2 files changed, 38 insertions(+), 19 deletions(-) (limited to 'src') diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 6b80a99c9..44f6a7fe6 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -614,27 +614,27 @@ Module B. Context {modulo div : Z->Z->Z}. Context {div_mod : forall a b:Z, b <> 0 -> a = b * (div a b) + modulo a b}. - Definition carry_cps {n} (index:nat) (p:tuple Z n) - {T} (f:tuple Z n->T) := + 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 div (weight index) (weight (S index) / weight index) P T - (fun R => from_associational_cps n R f)). + (fun R => from_associational_cps m R f)). - Definition carry {n} i p := @carry_cps n i p _ id. - Lemma carry_cps_id {n} i p {T} f: - @carry_cps n i p T f = f (carry i p). + 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} i p: (n <> 0%nat) -> + Lemma eval_carry {n m} i p: (n <> 0%nat) -> (m <> 0%nat) -> weight (S i) / weight i <> 0 -> - eval (carry (n := n) i p) = eval p. + eval (carry (n:=n) (m:=m) i p) = eval p. Proof. cbv [carry_cps carry]; intros. prove_eval. rewrite @eval_carry by eauto. @@ -705,6 +705,12 @@ Module B. (fun P => Associational.reduce_cps s c P (fun R => from_associational_cps n R f)). + Definition carry_reduce_cps {n div modulo} + (s:Z) (c:list limb) (p : tuple Z n) + {T} (f: tuple Z n ->T) := + carry_cps (div:=div) (modulo:=modulo) (n:=n) (m:=S n) (pred n) p + (fun r => reduce_cps (m:=S n) (n:=n) s c r f). + Definition negate_snd_cps {n} (p : tuple Z n) {T} (f:tuple Z n->T) := to_associational_cps p @@ -716,6 +722,7 @@ Module B. Positional.add_cps Positional.mul_cps Positional.reduce_cps + Positional.carry_reduce_cps Positional.negate_snd_cps . @@ -811,6 +818,7 @@ Module B. Positional.add_cps Positional.mul_cps Positional.reduce_cps + Positional.carry_reduce_cps Positional.negate_snd_cps Positional.opp_cps . @@ -913,7 +921,7 @@ Ltac F_mod_eq := apply mod_eq_Z2F_iff. Ltac solve_op_mod_eq wt x := - transitivity (Positional.eval wt x); autounfold; + transitivity (Positional.eval wt x); repeat autounfold; [|autorewrite with uncps push_id push_basesystem_eval; reflexivity]; cbv [mod_eq]; apply f_equal2; [|reflexivity]; diff --git a/src/Specific/NewBaseSystemTest.v b/src/Specific/NewBaseSystemTest.v index 595e4baea..2271db4e4 100644 --- a/src/Specific/NewBaseSystemTest.v +++ b/src/Specific/NewBaseSystemTest.v @@ -24,7 +24,8 @@ Section Ops25p5. Definition s : Z := 2^255. Definition c : list B.limb := [(1, 19)]. Definition coef_div_modulus := 2. (* add 2*modulus before subtracting *) - Definition carry_chain := Eval vm_compute in (seq 0 sz) ++ ([0;1])%nat. + 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 *) @@ -35,9 +36,15 @@ Section Ops25p5. Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed. Lemma wt_nonzero i : wt i <> 0. Proof. apply Z.pow_nonzero; zero_bounds. Qed. - Lemma wt_divides i (H:In i carry_chain) : wt (S i) / wt i <> 0. + Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0. Proof. - cbv [In carry_chain] in H. + 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. @@ -76,7 +83,7 @@ Section Ops25p5. eval (add a b) = (eval a + eval b)%F }. Proof. eexists; cbv beta zeta; intros. - pose proof wt_nonzero. pose proof wt_divides. + pose proof wt_nonzero. let x := constr:( Positional.add_cps (n := sz) wt a b id) in solve_op_F wt x. reflexivity. @@ -89,7 +96,7 @@ Section Ops25p5. eval (sub a b) = (eval a - eval b)%F}. Proof. eexists; cbv beta zeta; intros. - pose proof wt_nonzero. pose proof wt_divides. + 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. @@ -102,7 +109,7 @@ Section Ops25p5. eval (opp a) = F.opp (eval a)}. Proof. eexists; cbv beta zeta; intros. - pose proof wt_nonzero. pose proof wt_divides. + pose proof wt_nonzero. let x := constr:( Positional.opp_cps (n:=sz) (coef := coef) wt a id) in solve_op_F wt x. reflexivity. @@ -115,7 +122,7 @@ Section Ops25p5. eval (mul a b) = (eval a * eval b)%F}. Proof. eexists; cbv beta zeta; intros. - pose proof wt_nonzero. pose proof wt_divides. + 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 @@ -137,9 +144,13 @@ Section Ops25p5. eval (carry a) = eval a}. Proof. eexists; cbv beta zeta; intros. - pose proof wt_nonzero. pose proof wt_divides. pose proof div_mod. + 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_chain id) in + 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. @@ -176,4 +187,4 @@ Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig). Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig). *) -End Ops25p5. +End Ops25p5. \ No newline at end of file -- cgit v1.2.3