Add MontgomeryAPI.encode and two lemmas about it

One of them is Admitted.

1 files changed, 22 insertions, 0 deletions

diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
index 01672c61c..5b5ec1748 100644
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ b/src/Arithmetic/Saturated/MontgomeryAPI.v
@@ -160,6 +160,9 @@ Section API.
     Definition eval {n} (p : T n) : Z :=
       B.Positional.eval (uweight bound) p.
 
+    Definition encode n (z : Z) : T n :=
+      B.Positional.encode (uweight bound) (modulo_cps:=@modulo_cps) (div_cps:=@div_cps) z.
+
     Lemma eval_small n (p : T n) (Hsmall : small p) :
       0 <= eval p < uweight bound n.
     Proof.
@@ -191,6 +194,23 @@ Section API.
         { apply Z.mul_le_mono_nonneg; omega. }
     Qed.
 
+    Lemma small_encode n (v : Z) (Hsmall : 0 <= v < uweight bound n)
+      : small (encode n v).
+    Proof.
+    Admitted. (* TODO(jadep): prove me *)
+
+    Lemma eval_encode n (v : Z) (Hsmall : 0 <= v < uweight bound n)
+      : eval (encode n v) = v.
+    Proof.
+      destruct n as [|n].
+      { cbv -[Z.le Z.lt Z.gt] in *; omega. }
+      { cbv [eval encode].
+        pose proof (@uweight_divides _ bound_pos) as Hdiv.
+        apply B.Positional.eval_encode; try reflexivity;
+          eauto using modulo_id, div_id, div_mod, uweight_nonzero.
+        { intros i ?; specialize (Hdiv i); omega. } }
+    Qed.
+
     Lemma eval_zero n : eval (@zero n) = 0.
     Proof.
       cbv [eval zero].
@@ -633,6 +653,7 @@ Hint Unfold
      conditional_sub_cps
      conditional_sub
      eval
+     encode
   : basesystem_partial_evaluation_unfolder.
 
 Ltac basesystem_partial_evaluation_unfolder t :=
@@ -652,6 +673,7 @@ Ltac basesystem_partial_evaluation_unfolder t :=
                      conditional_sub_cps
                      conditional_sub
                      eval
+                     encode
                  ] in t) in
   let t := Saturated.AddSub.basesystem_partial_evaluation_unfolder t in
   let t := Saturated.Wrappers.basesystem_partial_evaluation_unfolder t in