Add sanity check of base_le_bitwidth

2 files changed, 18 insertions, 1 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
index 8c1d976ae..9e4cd8b0a 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Base.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -274,6 +274,13 @@ Ltac pose_c_small c wt sz c_small :=
     ltac:(vm_decide_no_check)
            c_small.
 
+Ltac pose_base_le_bitwidth base bitwidth base_le_bitwidth := (* this is purely a sanity check *)
+  cache_proof_with_type_by
+    (base <= inject_Z bitwidth)%Q
+    ltac:(cbv -[Z.le]; vm_decide_no_check)
+           base_le_bitwidth.
+
+
 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)
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index 82053a6b2..84b13c256 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.
+  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.
 End TAG.
 
 Ltac add_r pkg :=
@@ -159,6 +159,13 @@ Ltac add_c_small pkg :=
   let c_small := pose_c_small c wt sz c_small in
   Tag.update pkg TAG.c_small c_small.
 
+Ltac add_base_le_bitwidth pkg :=
+  let base := Tag.get pkg TAG.base in
+  let bitwidth := Tag.get pkg TAG.bitwidth in
+  let base_le_bitwidth := fresh "base_le_bitwidth" in
+  let base_le_bitwidth := pose_base_le_bitwidth base bitwidth base_le_bitwidth in
+  Tag.update pkg TAG.base_le_bitwidth base_le_bitwidth.
+
 Ltac add_m_enc_bounded pkg :=
   let sz := Tag.get pkg TAG.sz in
   let bitwidth := Tag.get pkg TAG.bitwidth in
@@ -190,6 +197,7 @@ Ltac add_Base_package pkg :=
   let pkg := add_wt_pos pkg in
   let pkg := add_wt_multiples pkg in
   let pkg := add_c_small pkg in
+  let pkg := add_base_le_bitwidth pkg in
   let pkg := add_m_enc_bounded pkg in
   Tag.strip_subst_local pkg.
 
@@ -241,6 +249,8 @@ Module MakeBasePackage (PKG : PrePackage).
   Notation wt_multiples := (ltac:(let v := get_wt_multiples () in exact v)) (only parsing).
   Ltac get_c_small _ := get TAG.c_small.
   Notation c_small := (ltac:(let v := get_c_small () in exact v)) (only parsing).
+  Ltac get_base_le_bitwidth _ := get TAG.base_le_bitwidth.
+  Notation base_le_bitwidth := (ltac:(let v := get_base_le_bitwidth () 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).
 End MakeBasePackage.