From e82f495c3fcdd037e85708b23c11abc37de5d918 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 7 Nov 2017 00:43:37 -0500 Subject: Use div_cps and modulo_cps in more places After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------- 10m04.41s | Total | 10m03.68s || +0m00.73s | +0.12% -------------------------------------------------------------------------------------------------------- 3m04.06s | Specific/X25519/C64/ladderstep | 3m04.00s || +0m00.06s | +0.03% 1m48.23s | Specific/NISTP256/AMD64/femul | 1m48.30s || -0m00.07s | -0.06% 0m38.59s | Arithmetic/Karatsuba | 0m38.51s || +0m00.08s | +0.20% 0m22.50s | Specific/X25519/C64/femul | 0m23.15s || -0m00.64s | -2.80% 0m21.79s | Specific/NISTP256/AMD64/fesub | 0m21.76s || +0m00.02s | +0.13% 0m19.78s | Specific/NISTP256/AMD64/feadd | 0m19.94s || -0m00.16s | -0.80% 0m18.57s | Specific/X25519/C64/freeze | 0m18.57s || +0m00.00s | +0.00% 0m17.96s | Specific/X25519/C64/fesquare | 0m18.36s || -0m00.39s | -2.17% 0m16.54s | Specific/NISTP256/AMD64/feopp | 0m16.18s || +0m00.35s | +2.22% 0m14.58s | Specific/X25519/C64/fecarry | 0m14.76s || -0m00.17s | -1.21% 0m13.80s | Specific/NISTP256/AMD64/fenz | 0m13.84s || -0m00.03s | -0.28% 0m13.34s | Specific/X25519/C64/fesub | 0m13.57s || -0m00.23s | -1.69% 0m12.72s | Arithmetic/Saturated/AddSub | 0m12.74s || -0m00.01s | -0.15% 0m12.19s | Specific/X25519/C64/feadd | 0m12.48s || -0m00.29s | -2.32% 0m10.57s | Arithmetic/Saturated/MontgomeryAPI | 0m10.36s || +0m00.21s | +2.02% 0m10.17s | Arithmetic/Saturated/Core | 0m09.92s || +0m00.25s | +2.52% 0m06.47s | Specific/NISTP256/AMD64/Synthesis | 0m06.65s || -0m00.18s | -2.70% 0m06.02s | Arithmetic/Saturated/MulSplit | 0m05.87s || +0m00.14s | +2.55% 0m05.27s | Specific/X25519/C64/Synthesis | 0m05.45s || -0m00.18s | -3.30% 0m03.70s | Arithmetic/MontgomeryReduction/WordByWord/Proofs | 0m03.65s || +0m00.05s | +1.36% 0m03.66s | Specific/Framework/ArithmeticSynthesis/Montgomery | 0m03.70s || -0m00.04s | -1.08% 0m02.93s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m02.60s || +0m00.33s | +12.69% 0m02.42s | Arithmetic/Saturated/Freeze | 0m02.45s || -0m00.03s | -1.22% 0m01.57s | Arithmetic/CoreUnfolder | 0m01.52s || +0m00.05s | +3.28% 0m01.44s | Specific/Framework/ArithmeticSynthesis/HelperTactics | 0m01.11s || +0m00.32s | +29.72% 0m01.29s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m01.21s || +0m00.08s | +6.61% 0m01.19s | Specific/Framework/ArithmeticSynthesis/Base | 0m01.00s || +0m00.18s | +18.99% 0m01.04s | Arithmetic/Saturated/CoreUnfolder | 0m01.13s || -0m00.08s | -7.96% 0m01.00s | Arithmetic/Saturated/UniformWeight | 0m00.95s || +0m00.05s | +5.26% 0m00.92s | Arithmetic/Saturated/WrappersUnfolder | 0m00.96s || -0m00.03s | -4.16% 0m00.89s | Specific/Framework/SynthesisFramework | 0m01.00s || -0m00.10s | -10.99% 0m00.87s | Specific/Framework/ReificationTypes | 0m01.00s || -0m00.13s | -13.00% 0m00.84s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.82s || +0m00.02s | +2.43% 0m00.81s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.72s || +0m00.09s | +12.50% 0m00.80s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.86s || -0m00.05s | -6.97% 0m00.78s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.76s || +0m00.02s | +2.63% 0m00.77s | Specific/Framework/MontgomeryReificationTypes | 0m00.80s || -0m00.03s | -3.75% 0m00.76s | Arithmetic/Saturated/MulSplitUnfolder | 0m00.80s || -0m00.04s | -5.00% 0m00.76s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.70s || +0m00.06s | +8.57% 0m00.75s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.64s || +0m00.10s | +17.18% 0m00.75s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.71s || +0m00.04s | +5.63% 0m00.74s | Arithmetic/Saturated/Wrappers | 0m00.78s || -0m00.04s | -5.12% 0m00.73s | Arithmetic/Saturated/FreezeUnfolder | 0m00.77s || -0m00.04s | -5.19% 0m00.72s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.72s || +0m00.00s | +0.00% 0m00.72s | Specific/Framework/ReificationTypesPackage | 0m00.84s || -0m00.12s | -14.28% 0m00.71s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.69s || +0m00.02s | +2.89% 0m00.70s | Specific/Framework/ArithmeticSynthesis/Ladderstep | 0m00.67s || +0m00.02s | +4.47% 0m00.69s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m01.03s || -0m00.34s | -33.00% 0m00.66s | Arithmetic/Saturated/UniformWeightInstances | 0m00.67s || -0m00.01s | -1.49% 0m15.65s | Arithmetic/Core | 0m14.01s || +0m01.64s | +11.70% --- src/Arithmetic/Core.v | 81 ++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 57 insertions(+), 24 deletions(-) (limited to 'src/Arithmetic') diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 929aa2260..a33bd394d 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -438,23 +438,32 @@ Module B. Qed. Hint Rewrite eval_negate_snd : push_basesystem_eval. Section Carries. - Context {modulo div:Z->Z->Z}. + 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) := if dec (fst t = w) then dlet t2 := snd t in - dlet d2 := div t2 fw in - dlet m2 := modulo t2 fw in - f ((w*fw, d2) :: (w, m2) :: @nil limb) + 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 Type. cbv [carryterm_cps carryterm Let_In]; prove_id. Qed. + 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. @@ -473,7 +482,9 @@ Module B. 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 Type. cbv [carry_cps carry]; prove_id. Qed. + 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. @@ -484,12 +495,19 @@ Module B. End Carries. End Associational. + + Ltac div_mod_cps_t := + intros; autorewrite with uncps push_id; try reflexivity. + Hint Rewrite - @Associational.carry_cps_id - @Associational.carryterm_cps_id @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. @@ -644,14 +662,20 @@ Module B. : push_basesystem_eval. Section Carries. - Context {modulo div : Z->Z->Z}. + 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}. + 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 div + modulo_cps div_cps (weight index) (weight (S index) / weight index) P T @@ -690,7 +714,9 @@ Module B. 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 Type. cbv [chained_carries_cps chained_carries]; prove_id. Qed. + 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. @@ -738,10 +764,10 @@ 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} + Definition carry_reduce_cps {n div_cps modulo_cps} (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 + carry_cps (div_cps:=div_cps) (modulo_cps:=modulo_cps) (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) @@ -820,18 +846,23 @@ Module B. 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 div:Z->Z->Z} - {div_mod : forall a b:Z, b <> 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:=div) (modulo:=modulo) (F.to_Z x). + 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. - cbv [Fdecode Fencode]; rewrite @eval_encode by auto. + 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. @@ -935,20 +966,22 @@ Module B. Positional.opp_cps . Hint Rewrite - @Associational.carry_cps_id - @Associational.carryterm_cps_id @Associational.reduce_cps_id @Associational.split_cps_id @Associational.mul_cps_id - @Positional.carry_cps_id @Positional.from_associational_cps_id @Positional.place_cps_id @Positional.add_to_nth_cps_id @Positional.to_associational_cps_id - @Positional.chained_carries_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 + using div_mod_cps_t : uncps. Hint Rewrite @Associational.eval_mul @Positional.eval_single @@ -966,7 +999,7 @@ Module B. @Positional.eval_chained_carries @Positional.eval_sub @Positional.eval_select - using (assumption || vm_decide) : push_basesystem_eval. + 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 *) -- cgit v1.2.3