Only require half_sz_nonzero in karatsuba (it fails for sz=1)

4 files changed, 22 insertions, 16 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
index 9e4cd8b0a..a3ed3dfef 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Base.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -171,12 +171,6 @@ Ltac pose_half_sz sz half_sz :=
   let v := (eval compute in (half_sz' sz)) in
   cache_term v half_sz.
 
-Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
-  cache_proof_with_type_by
-    (half_sz <> 0%nat)
-    ltac:(cbv; congruence)
-           half_sz_nonzero.
-
 Ltac pose_s_nonzero s s_nonzero :=
   cache_proof_with_type_by
     (s <> 0)
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index 84b13c256..18b0bcda0 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
@@ -5,7 +5,7 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | s_nonzero | sz_le_log2_m | base_pos | m_correct | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples | c_small | base_le_bitwidth | m_enc_bounded.
+  Inductive tags := r | m | wt | sz2 | half_sz | s_nonzero | sz_le_log2_m | base_pos | m_correct | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples | c_small | base_le_bitwidth | m_enc_bounded.
 End TAG.
 
 Ltac add_r pkg :=
@@ -39,12 +39,6 @@ Ltac add_half_sz pkg :=
   let half_sz := pose_half_sz sz half_sz in
   Tag.update pkg TAG.half_sz half_sz.
 
-Ltac add_half_sz_nonzero pkg :=
-  let half_sz := Tag.get pkg TAG.half_sz in
-  let half_sz_nonzero := fresh "half_sz_nonzero" in
-  let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in
-  Tag.update pkg TAG.half_sz_nonzero half_sz_nonzero.
-
 Ltac add_s_nonzero pkg :=
   let s := Tag.get pkg TAG.s in
   let s_nonzero := fresh "s_nonzero" in
@@ -180,7 +174,6 @@ Ltac add_Base_package pkg :=
   let pkg := add_wt pkg in
   let pkg := add_sz2 pkg in
   let pkg := add_half_sz pkg in
-  let pkg := add_half_sz_nonzero pkg in
   let pkg := add_s_nonzero pkg in
   let pkg := add_sz_le_log2_m pkg in
   let pkg := add_base_pos pkg in
@@ -215,8 +208,6 @@ Module MakeBasePackage (PKG : PrePackage).
   Notation sz2 := (ltac:(let v := get_sz2 () in exact v)) (only parsing).
   Ltac get_half_sz _ := get TAG.half_sz.
   Notation half_sz := (ltac:(let v := get_half_sz () in exact v)) (only parsing).
-  Ltac get_half_sz_nonzero _ := get TAG.half_sz_nonzero.
-  Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing).
   Ltac get_s_nonzero _ := get TAG.s_nonzero.
   Notation s_nonzero := (ltac:(let v := get_s_nonzero () in exact v)) (only parsing).
   Ltac get_sz_le_log2_m _ := get TAG.sz_le_log2_m.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v
index 4dc83ce1a..454a27329 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v
@@ -80,6 +80,12 @@ Section gen.
   Defined.
 End gen.
 
+Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
+  cache_proof_with_type_by
+    (half_sz <> 0%nat)
+    ltac:(cbv; congruence)
+           half_sz_nonzero.
+
 Ltac pose_mul_sig wt m base sz s c half_sz mul_sig :=
   let sqrt_s := fresh "sqrt_s" in
   let sqrt_s := internal_pose_sqrt_s s sqrt_s in
diff --git a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
index 2e7d98c1e..197c9431b 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v
@@ -6,7 +6,19 @@ Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Karatsuba.
 Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
+Module TAG.
+  Inductive tags := half_sz_nonzero.
+End TAG.
 
+Ltac add_half_sz_nonzero pkg :=
+  if_goldilocks
+    pkg
+    ltac:(fun _ => let half_sz := Tag.get pkg TAG.half_sz in
+                   let half_sz_nonzero := fresh "half_sz_nonzero" in
+                   let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in
+                   Tag.update pkg TAG.half_sz_nonzero half_sz_nonzero)
+    ltac:(fun _ => pkg)
+    ().
 Ltac add_mul_sig pkg :=
   if_goldilocks
     pkg
@@ -35,6 +47,7 @@ Ltac add_square_sig pkg :=
     ltac:(fun _ => pkg)
     ().
 Ltac add_Karatsuba_package pkg :=
+  let pkg := add_half_sz_nonzero pkg in
   let pkg := add_mul_sig pkg in
   let pkg := add_square_sig pkg in
   Tag.strip_subst_local pkg.
@@ -43,4 +56,6 @@ Ltac add_Karatsuba_package pkg :=
 Module MakeKaratsubaPackage (PKG : PrePackage).
   Module Import MakeKaratsubaPackageInternal := MakePackageBase PKG.
 
+  Ltac get_half_sz_nonzero _ := get TAG.half_sz_nonzero.
+  Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing).
 End MakeKaratsubaPackage.