Add some more helper lemmas to synthesis

2 files changed, 49 insertions, 1 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v
index dfad9e602..7c80b238d 100644
--- a/src/Specific/Framework/ArithmeticSynthesis/Base.v
+++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v
@@ -49,6 +49,24 @@ Ltac pose_half_sz_nonzero half_sz half_sz_nonzero :=
     ltac:(cbv; congruence)
            half_sz_nonzero.
 
+Ltac pose_s_nonzero s s_nonzero :=
+  cache_proof_with_type_by
+    (s <> 0)
+    ltac:(vm_decide_no_check)
+           s_nonzero.
+
+Ltac pose_sz_le_log2_m sz m sz_le_log2_m :=
+  cache_proof_with_type_by
+    (Z.of_nat sz <= Z.log2_up (Z.pos m))
+    ltac:(vm_decide_no_check)
+           sz_le_log2_m.
+
+Ltac pose_m_correct m s c m_correct :=
+  cache_proof_with_type_by
+    (Z.pos m = s - Associational.eval c)
+    ltac:(vm_decide_no_check)
+           m_correct.
+
 Ltac pose_m_enc sz s c wt m_enc :=
   let v := (eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c))) in
   let v := (eval compute in v) in (* compute away the type arguments *)
diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v
index f5602272c..791762975 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 | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples.
+  Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | s_nonzero | sz_le_log2_m | m_correct | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples.
 End TAG.
 
 Ltac add_r pkg :=
@@ -46,6 +46,27 @@ Ltac add_half_sz_nonzero pkg :=
   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
+  let s_nonzero := pose_s_nonzero s s_nonzero in
+  Tag.update pkg TAG.s_nonzero s_nonzero.
+
+Ltac add_sz_le_log2_m pkg :=
+  let sz := Tag.get pkg TAG.sz in
+  let m := Tag.get pkg TAG.m in
+  let sz_le_log2_m := fresh "sz_le_log2_m" in
+  let sz_le_log2_m := pose_sz_le_log2_m sz m sz_le_log2_m in
+  Tag.update pkg TAG.sz_le_log2_m sz_le_log2_m.
+
+Ltac add_m_correct pkg :=
+  let m := Tag.get pkg TAG.m in
+  let s := Tag.get pkg TAG.s in
+  let c := Tag.get pkg TAG.c in
+  let m_correct := fresh "m_correct" in
+  let m_correct := pose_m_correct m s c m_correct in
+  Tag.update pkg TAG.m_correct m_correct.
+
 Ltac add_m_enc pkg :=
   let sz := Tag.get pkg TAG.sz in
   let s := Tag.get pkg TAG.s in
@@ -130,6 +151,9 @@ Ltac add_Base_package pkg :=
   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_m_correct pkg in
   let pkg := add_m_enc pkg in
   let pkg := add_coef pkg in
   let pkg := add_coef_mod pkg in
@@ -159,6 +183,12 @@ Module MakeBasePackage (PKG : PrePackage).
   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.
+  Notation sz_le_log2_m := (ltac:(let v := get_sz_le_log2_m () in exact v)) (only parsing).
+  Ltac get_m_correct _ := get TAG.m_correct.
+  Notation m_correct := (ltac:(let v := get_m_correct () in exact v)) (only parsing).
   Ltac get_m_enc _ := get TAG.m_enc.
   Notation m_enc := (ltac:(let v := get_m_enc () in exact v)) (only parsing).
   Ltac get_coef _ := get TAG.coef.