diff options
-rw-r--r-- | src/Arithmetic/Core.v | 6 | ||||
-rw-r--r-- | src/Arithmetic/CoreUnfolder.v | 3 | ||||
-rw-r--r-- | src/Arithmetic/Karatsuba.v | 11 |
3 files changed, 11 insertions, 9 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 4293561fa..929aa2260 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1076,7 +1076,7 @@ Hint Unfold Positional.select_cps Positional.select modulo div modulo_cps div_cps - id_tuple_with_alt id_tuple'_with_alt + id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' Z.add_get_carry_full Z.add_get_carry_full_cps : basesystem_partial_evaluation_unfolder. @@ -1084,7 +1084,7 @@ Hint Unfold B.limb ListUtil.sum ListUtil.sum_firstn CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2 Decidable.dec Decidable.dec_eq_Z - id_tuple_with_alt id_tuple'_with_alt + id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' Z.add_get_carry_full Z.add_get_carry_full_cps Z.mul_split Z.mul_split_cps Z.mul_split_cps' : basesystem_partial_evaluation_unfolder. @@ -1110,7 +1110,7 @@ Ltac basesystem_partial_evaluation_unfolder t := Associational.carryterm_cps Associational.carryterm Associational.carry_cps Associational.carry Associational.negate_snd_cps Associational.negate_snd div modulo - id_tuple_with_alt id_tuple'_with_alt + id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' Z.add_get_carry_full Z.add_get_carry_full_cps ] in t. diff --git a/src/Arithmetic/CoreUnfolder.v b/src/Arithmetic/CoreUnfolder.v index a7a7286d1..cad4f6e7c 100644 --- a/src/Arithmetic/CoreUnfolder.v +++ b/src/Arithmetic/CoreUnfolder.v @@ -3,6 +3,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.CPS. Require Import Crypto.Util.IdfunWithAlt. +Require Import Crypto.Util.CPSUtil. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Util.Tactics.VM. @@ -16,7 +17,7 @@ Ltac make_parameterized_sig t := B.limb ListUtil.sum ListUtil.sum_firstn CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2 Decidable.dec Decidable.dec_eq_Z - id_tuple_with_alt id_tuple'_with_alt + id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps' Z.add_get_carry_full Z.mul_split Z.add_get_carry_full_cps Z.mul_split_cps Z.mul_split_cps' Z.add_get_carry_cps]; diff --git a/src/Arithmetic/Karatsuba.v b/src/Arithmetic/Karatsuba.v index d7b988e17..5176f16b0 100644 --- a/src/Arithmetic/Karatsuba.v +++ b/src/Arithmetic/Karatsuba.v @@ -78,7 +78,7 @@ Context (weight : nat -> Z) actually run and a version to bounds-check, along with a proof that they are exactly equal. This works around cases where the bounds proof requires high-level reasoning. *) - Local Notation id_with_alt_bounds := id_tuple_with_alt. + Local Notation id_with_alt_bounds_cps := id_tuple_with_alt_cps'. (* If: @@ -134,7 +134,8 @@ Context (weight : nat -> Z) (fun sum_y => mul_cps weight sum_x sum_y (fun mul_sumxy => - dlet z1 := id_with_alt_bounds (unbalanced_sub_cps weight mul_sumxy z0 id) ( + id_with_alt_bounds_cps (fun f => + (unbalanced_sub_cps weight mul_sumxy z0 f)) (fun f => (mul_cps weight (fst x0_x1) (snd y0_y1) (fun x0_y1 => mul_cps weight (snd x0_x1) (fst y0_y1) @@ -142,19 +143,19 @@ Context (weight : nat -> Z) (fun z0 => mul_cps weight (snd x0_x1) (snd y0_y1) (fun z2 => add_cps weight z0 z2 (fun sum_z => add_cps weight x0_y1 x1_y0 - (fun z1' => add_cps weight z1' z2 id)))))))) in + (fun z1' => add_cps weight z1' z2 f)))))))) (fun z1 => Positional.to_associational_cps weight z1 (fun z1 => Associational.mul_cps (pair s 1::nil) z1 (fun sz1 => Positional.to_associational_cps weight sum_z (fun sum_z => Positional.from_associational_cps weight _ (sum_z++sz1) f - ))))))))))). + )))))))))))). Definition goldilocks_mul s xs ys := goldilocks_mul_cps s xs ys id. Lemma goldilocks_mul_id s xs ys R f : @goldilocks_mul_cps s xs ys R f = f (goldilocks_mul s xs ys). Proof. - cbv [goldilocks_mul goldilocks_mul_cps id_with_alt_bounds Let_In]. + cbv [goldilocks_mul goldilocks_mul_cps Let_In]. repeat autounfold. autorewrite with uncps push_id. reflexivity. Qed. |