Factored out some proofs that rely only on base being powers of two, and defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util.

1 files changed, 43 insertions, 0 deletions

diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v
new file mode 100644
index 000000000..847967f52
--- /dev/null
+++ b/src/ModularArithmetic/Pow2Base.v
@@ -0,0 +1,43 @@
+Require Import Zpower ZArith.
+Require Import Crypto.Util.ListUtil.
+Require Import Coq.Lists.List.
+
+Local Open Scope Z_scope.
+
+Section Pow2Base.
+  Context (limb_widths : list Z).
+  Local Notation "w[ i ]" := (nth_default 0 limb_widths i).
+
+  Fixpoint base_from_limb_widths limb_widths :=
+    match limb_widths with
+    | nil => nil
+    | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw)
+    end.
+
+  Local Notation "{base}" := (base_from_limb_widths limb_widths).
+
+
+  Definition bounded us := forall i, 0 <= nth_default 0 us i < 2 ^ w[i].
+
+  Definition upper_bound := 2 ^ (sum_firstn limb_widths (length limb_widths)).
+
+  Fixpoint decode_bitwise' us i acc := 
+    match i with
+    | O => acc
+    | S i' => decode_bitwise' us i' (Z.lor (nth_default 0 us i') (Z.shiftl acc w[i']))
+    end.
+
+  Definition decode_bitwise us := decode_bitwise' us (length us) 0.
+
+  (* i is current index, counts down *)
+  Fixpoint encode' z i :=
+    match i with
+    | O => nil
+    | S i' => let lw := sum_firstn limb_widths in
+       encode' z i' ++ (Z.shiftr (Z.land z (Z.ones (lw i))) (lw i')) :: nil
+    end.
+
+  (* max must be greater than input; this is used to truncate last digit *)
+  Definition encodeZ x:= encode' x (length limb_widths).
+
+End Pow2Base.
\ No newline at end of file