Add MulSplitUnfolder

5 files changed, 89 insertions, 2 deletions

diff --git a/_CoqProject b/_CoqProject
index 4543997ba..91ca74ade 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -37,6 +37,7 @@ src/Arithmetic/Saturated/Freeze.v
 src/Arithmetic/Saturated/FreezeUnfolder.v
 src/Arithmetic/Saturated/MontgomeryAPI.v
 src/Arithmetic/Saturated/MulSplit.v
+src/Arithmetic/Saturated/MulSplitUnfolder.v
 src/Arithmetic/Saturated/UniformWeight.v
 src/Arithmetic/Saturated/UniformWeightInstances.v
 src/Arithmetic/Saturated/Wrappers.v
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index cf774be57..68f5afd20 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -1034,6 +1034,44 @@ Ltac apply_patterned t1 :=
             (@Z.add_get_carry)
             (@Z.zselect)).
 
+Ltac pattern_strip_full t :=
+  let t := (eval pattern
+                 Z,
+            (@Let_In Z (fun _ => Z)),
+            @runtime_mul, @runtime_add, @runtime_opp, @runtime_shr, @runtime_and, @runtime_lor,
+            (@id_with_alt Z),
+            @Z.add_get_carry, @Z.zselect, @Z.mul_split_at_bitwidth,
+            Z.mul, Z.add, Z.opp, Z.shiftr, Z.shiftl, Z.land, Z.lor,
+            Z.modulo, Z.div, Z.log2, Z.pow, Z.ones,
+            Z.eq_dec, Z.eqb,
+            (@ModularArithmetic.F.to_Z), (@ModularArithmetic.F.of_Z),
+            2%Z, 1%Z, 0%Z
+             in t) in
+  let t := match t with ?t _
+                         _
+                         _ _ _ _ _ _
+                         _
+                         _ _ _
+                         _ _ _ _ _ _ _
+                         _ _ _ _ _
+                         _ _
+                         _ _
+                         _ _ _ => t end in
+  t.
+
+Ltac apply_patterned_full t1 :=
+  constr:(t1
+            Z
+            (@Let_In Z (fun _ => Z))
+            (@runtime_mul) (@runtime_add) (@runtime_opp) (@runtime_shr) (@runtime_and) (@runtime_lor)
+            (@id_with_alt Z)
+            (@Z.add_get_carry) (@Z.zselect) (@Z.mul_split_at_bitwidth)
+            Z.mul Z.add Z.opp Z.shiftr Z.shiftl Z.land Z.lor
+            Z.modulo Z.div Z.log2 Z.pow Z.ones
+            Z.eq_dec Z.eqb
+            (@ModularArithmetic.F.to_Z) (@ModularArithmetic.F.of_Z)
+            2%Z 1%Z 0%Z).
+
 Ltac basesystem_partial_evaluation_RHS_gen unfold_tac :=
   let t := match goal with |- _ _ ?t => t end in
   let t := unfold_tac t in
diff --git a/src/Arithmetic/CoreUnfolder.v b/src/Arithmetic/CoreUnfolder.v
index 372a873b8..3692ff65d 100644
--- a/src/Arithmetic/CoreUnfolder.v
+++ b/src/Arithmetic/CoreUnfolder.v
@@ -6,8 +6,10 @@ Require Import Crypto.Util.Tactics.VM.
 Ltac make_parameterized_sig t :=
   refine (_ : { v : _ | v = t });
   eexists; cbv delta [t
+                        B.limb ListUtil.sum ListUtil.sum_firstn
+                        Decidable.dec Decidable.dec_eq_Z
                         id_tuple_with_alt id_tuple'_with_alt
-                        Z.add_get_carry_full];
+                        Z.add_get_carry_full Z.mul_split];
   repeat autorewrite with pattern_runtime;
   reflexivity.
 
@@ -39,7 +41,7 @@ for i in eval multerm mul_cps mul split_cps split reduce_cps reduce negate_snd_c
 done
 echo "  End Associational."
 echo "  Module Positional."
-for i in to_associational_cps to_associational eval zeros add_to_nth_cps add_to_nth place_cps place from_associational_cps from_associational carry_cps carry chained_carries_cps chained_carries add_cps mul_cps reduce_cps carry_reduce_cps negate_snd_cps split_cps scmul_cps unbalanced_sub_cps sub_cps sub opp_cps Fencode Fdecode eval_from select_cps select; do
+for i in to_associational_cps to_associational eval zeros add_to_nth_cps add_to_nth place_cps place from_associational_cps from_associational carry_cps carry chained_carries_cps chained_carries encode add_cps mul_cps reduce_cps carry_reduce_cps negate_snd_cps split_cps scmul_cps unbalanced_sub_cps sub_cps sub opp_cps Fencode Fdecode eval_from select_cps select; do
   echo "    Definition ${i}_sig := parameterize_sig (@Core.B.Positional.${i}).";
   echo "    Definition ${i} := parameterize_from_sig ${i}_sig.";
   echo "    Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
@@ -196,6 +198,11 @@ done
     Definition chained_carries_eq := parameterize_eq chained_carries chained_carries_sig.
     Hint Rewrite <- chained_carries_eq : pattern_runtime.
 
+    Definition encode_sig := parameterize_sig (@Core.B.Positional.encode).
+    Definition encode := parameterize_from_sig encode_sig.
+    Definition encode_eq := parameterize_eq encode encode_sig.
+    Hint Rewrite <- encode_eq : pattern_runtime.
+
     Definition add_cps_sig := parameterize_sig (@Core.B.Positional.add_cps).
     Definition add_cps := parameterize_from_sig add_cps_sig.
     Definition add_cps_eq := parameterize_eq add_cps add_cps_sig.
diff --git a/src/Arithmetic/Saturated/MulSplitUnfolder.v b/src/Arithmetic/Saturated/MulSplitUnfolder.v
new file mode 100644
index 000000000..d74051e46
--- /dev/null
+++ b/src/Arithmetic/Saturated/MulSplitUnfolder.v
@@ -0,0 +1,40 @@
+Require Import Crypto.Arithmetic.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.MulSplit.
+
+Module B.
+  Module Associational.
+(**
+<<
+#!/bin/bash
+for i in sat_multerm_cps sat_multerm sat_mul_cps sat_mul; do
+    echo "    Definition ${i}_sig := parameterize_sig (@MulSplit.B.Associational.${i}).";
+    echo "    Definition ${i} := parameterize_from_sig ${i}_sig.";
+    echo "    Definition ${i}_eq := parameterize_eq ${i} ${i}_sig.";
+    echo "    Hint Rewrite <- ${i}_eq : pattern_runtime."; echo "";
+done
+echo "  End Associational."
+echo "End B."
+>> *)
+    Definition sat_multerm_cps_sig := parameterize_sig (@MulSplit.B.Associational.sat_multerm_cps).
+    Definition sat_multerm_cps := parameterize_from_sig sat_multerm_cps_sig.
+    Definition sat_multerm_cps_eq := parameterize_eq sat_multerm_cps sat_multerm_cps_sig.
+    Hint Rewrite <- sat_multerm_cps_eq : pattern_runtime.
+
+    Definition sat_multerm_sig := parameterize_sig (@MulSplit.B.Associational.sat_multerm).
+    Definition sat_multerm := parameterize_from_sig sat_multerm_sig.
+    Definition sat_multerm_eq := parameterize_eq sat_multerm sat_multerm_sig.
+    Hint Rewrite <- sat_multerm_eq : pattern_runtime.
+
+    Definition sat_mul_cps_sig := parameterize_sig (@MulSplit.B.Associational.sat_mul_cps).
+    Definition sat_mul_cps := parameterize_from_sig sat_mul_cps_sig.
+    Definition sat_mul_cps_eq := parameterize_eq sat_mul_cps sat_mul_cps_sig.
+    Hint Rewrite <- sat_mul_cps_eq : pattern_runtime.
+
+    Definition sat_mul_sig := parameterize_sig (@MulSplit.B.Associational.sat_mul).
+    Definition sat_mul := parameterize_from_sig sat_mul_sig.
+    Definition sat_mul_eq := parameterize_eq sat_mul sat_mul_sig.
+    Hint Rewrite <- sat_mul_eq : pattern_runtime.
+
+  End Associational.
+End B.
diff --git a/src/Arithmetic/Saturated/WrappersUnfolder.v b/src/Arithmetic/Saturated/WrappersUnfolder.v
index 20df67b58..52006a702 100644
--- a/src/Arithmetic/Saturated/WrappersUnfolder.v
+++ b/src/Arithmetic/Saturated/WrappersUnfolder.v
@@ -1,5 +1,6 @@
 Require Import Crypto.Arithmetic.CoreUnfolder.
 Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
+Require Import Crypto.Arithmetic.Saturated.MulSplitUnfolder.
 Require Import Crypto.Arithmetic.Saturated.Wrappers.
 
 Module Columns.