Saner checking for freeze and ladderstep

1 files changed, 36 insertions, 14 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
index 200ad593a..5b43277cc 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v
@@ -7,25 +7,45 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := Mxzladderstep_sig.
+  Inductive tags := a24_sig | Mxzladderstep_sig.
 End TAG.
 
+Ltac add_a24_sig pkg :=
+  if_ladderstep
+    pkg
+    ltac:(fun _ => Tag.update_by_tac_if_not_exists
+                       pkg
+                       TAG.a24_sig
+                       ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                                      let m := Tag.get pkg TAG.m in
+                                      let wt := Tag.get pkg TAG.wt in
+                                      let a24 := Tag.get pkg TAG.a24 in
+                                      let a24_sig := fresh "a24_sig" in
+                                      let a24_sig := pose_a24_sig sz m wt a24 a24_sig in
+                                      constr:(a24_sig)))
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_Mxzladderstep_sig pkg :=
-  Tag.update_by_tac_if_not_exists
+  if_ladderstep
     pkg
-    TAG.Mxzladderstep_sig
-    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
-                   let wt := Tag.get pkg TAG.wt in
-                   let m := Tag.get pkg TAG.m in
-                   let add_sig := Tag.get pkg TAG.add_sig in
-                   let sub_sig := Tag.get pkg TAG.sub_sig in
-                   let mul_sig := Tag.get pkg TAG.mul_sig in
-                   let square_sig := Tag.get pkg TAG.square_sig in
-                   let carry_sig := Tag.get pkg TAG.carry_sig in
-                   let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
-                   let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in
-                   constr:(Mxzladderstep_sig)).
+    ltac:(fun _ => Tag.update_by_tac_if_not_exists
+                       pkg
+                       TAG.Mxzladderstep_sig
+                       ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                                      let wt := Tag.get pkg TAG.wt in
+                                      let m := Tag.get pkg TAG.m in
+                                      let add_sig := Tag.get pkg TAG.add_sig in
+                                      let sub_sig := Tag.get pkg TAG.sub_sig in
+                                      let mul_sig := Tag.get pkg TAG.mul_sig in
+                                      let square_sig := Tag.get pkg TAG.square_sig in
+                                      let carry_sig := Tag.get pkg TAG.carry_sig in
+                                      let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
+                                      let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in
+                                      constr:(Mxzladderstep_sig)))
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_Ladderstep_package pkg :=
+  let pkg := add_a24_sig pkg in
   let pkg := add_Mxzladderstep_sig pkg in
   Tag.strip_subst_local pkg.
 
@@ -33,6 +53,8 @@ Ltac add_Ladderstep_package pkg :=
 Module MakeLadderstepPackage (PKG : PrePackage).
   Module Import MakeLadderstepPackageInternal := MakePackageBase PKG.
 
+  Ltac get_a24_sig _ := get TAG.a24_sig.
+  Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing).
   Ltac get_Mxzladderstep_sig _ := get TAG.Mxzladderstep_sig.
   Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing).
 End MakeLadderstepPackage.