Better error messages on m_enc_bounded

Also only require m_correct_wt for freeze

4 files changed, 23 insertions, 24 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
index 541069d94..8c1d976ae 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Base.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -277,11 +277,5 @@ Ltac pose_c_small c wt sz c_small :=
 Ltac pose_m_enc_bounded sz bitwidth m_enc m_enc_bounded :=
   cache_proof_with_type_by
     (Tuple.map (n:=sz) (BinInt.Z.land (Z.ones bitwidth)) m_enc = m_enc)
-    ltac:(vm_decide_no_check)
+    ltac:(vm_compute; reflexivity)
            m_enc_bounded.
-
-Ltac pose_m_correct_wt m c sz wt m_correct_wt :=
-  cache_proof_with_type_by
-    (Z.pos m = wt sz - Associational.eval c)
-    ltac:(vm_decide_no_check)
-           m_correct_wt.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index 80e032fb8..82053a6b2 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 | m_enc_bounded | m_correct_wt.
+  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 | m_enc_bounded.
 End TAG.
 
 Ltac add_r pkg :=
@@ -167,15 +167,6 @@ Ltac add_m_enc_bounded pkg :=
   let m_enc_bounded := pose_m_enc_bounded sz bitwidth m_enc m_enc_bounded in
   Tag.update pkg TAG.m_enc_bounded m_enc_bounded.
 
-Ltac add_m_correct_wt pkg :=
-  let m := Tag.get pkg TAG.m in
-  let c := Tag.get pkg TAG.c in
-  let sz := Tag.get pkg TAG.sz in
-  let wt := Tag.get pkg TAG.wt in
-  let m_correct_wt := fresh "m_correct_wt" in
-  let m_correct_wt := pose_m_correct_wt m c sz wt m_correct_wt in
-  Tag.update pkg TAG.m_correct_wt m_correct_wt.
-
 Ltac add_Base_package pkg :=
   let pkg := add_r pkg in
   let pkg := add_m pkg in
@@ -200,7 +191,6 @@ Ltac add_Base_package pkg :=
   let pkg := add_wt_multiples pkg in
   let pkg := add_c_small pkg in
   let pkg := add_m_enc_bounded pkg in
-  let pkg := add_m_correct_wt pkg in
   Tag.strip_subst_local pkg.
 
 
@@ -253,6 +243,4 @@ Module MakeBasePackage (PKG : PrePackage).
   Notation c_small := (ltac:(let v := get_c_small () in exact v)) (only parsing).
   Ltac get_m_enc_bounded _ := get TAG.m_enc_bounded.
   Notation m_enc_bounded := (ltac:(let v := get_m_enc_bounded () in exact v)) (only parsing).
-  Ltac get_m_correct_wt _ := get TAG.m_correct_wt.
-  Notation m_correct_wt := (ltac:(let v := get_m_correct_wt () in exact v)) (only parsing).
 End MakeBasePackage.
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
index 44d284d8e..7fd723cb8 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v
@@ -22,9 +22,6 @@ End Exports.
 Local Open Scope Z_scope.
 Local Infix "^" := Tuple.tuple : type_scope.
 
-Ltac freeze_preunfold :=
-  cbv [freeze freeze_cps Wrappers.Columns.unbalanced_sub_cps Wrappers.Columns.conditional_add_cps Core.Columns.from_associational_cps Core.Columns.nils Core.Columns.cons_to_nth_cps Core.Columns.compact_cps Wrappers.Columns.add_cps Core.Columns.compact_step_cps Core.Columns.compact_digit_cps].
-
 Section gen.
   Context (m : positive)
           (base : Q)
@@ -66,6 +63,12 @@ Section gen.
   Defined.
 End gen.
 
+Ltac pose_m_correct_wt m c sz wt m_correct_wt :=
+  cache_proof_with_type_by
+    (Z.pos m = wt sz - Associational.eval c)
+    ltac:(vm_decide_no_check)
+           m_correct_wt.
+
 Ltac pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig :=
   cache_sig_with_type_by_existing_sig_helper
     ltac:(fun _ => cbv [freeze_sig'])
diff --git a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
index 1a4b405b6..5cda57da2 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v
@@ -6,9 +6,20 @@ Require Import Crypto.Specific.Framework.Packages.
 Require Import Crypto.Util.TagList.
 
 Module TAG.
-  Inductive tags := freeze_sig.
+  Inductive tags := m_correct_wt | freeze_sig.
 End TAG.
 
+Ltac add_m_correct_wt pkg :=
+  Tag.update_by_tac_if_not_exists
+    pkg
+    TAG.m_correct_wt
+    ltac:(fun _ => let m := Tag.get pkg TAG.m in
+                   let c := Tag.get pkg TAG.c in
+                   let sz := Tag.get pkg TAG.sz in
+                   let wt := Tag.get pkg TAG.wt in
+                   let m_correct_wt := fresh "m_correct_wt" in
+                   let m_correct_wt := pose_m_correct_wt m c sz wt m_correct_wt in
+                   constr:(m_correct_wt)).
 Ltac add_freeze_sig pkg :=
   Tag.update_by_tac_if_not_exists
     pkg
@@ -26,6 +37,7 @@ Ltac add_freeze_sig pkg :=
                    let freeze_sig := pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig in
                    constr:(freeze_sig)).
 Ltac add_Freeze_package pkg :=
+  let pkg := add_m_correct_wt pkg in
   let pkg := add_freeze_sig pkg in
   Tag.strip_subst_local pkg.
 
@@ -33,6 +45,8 @@ Ltac add_Freeze_package pkg :=
 Module MakeFreezePackage (PKG : PrePackage).
   Module Import MakeFreezePackageInternal := MakePackageBase PKG.
 
+  Ltac get_m_correct_wt _ := get TAG.m_correct_wt.
+  Notation m_correct_wt := (ltac:(let v := get_m_correct_wt () in exact v)) (only parsing).
   Ltac get_freeze_sig _ := get TAG.freeze_sig.
   Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing).
 End MakeFreezePackage.