1 files changed, 19 insertions, 0 deletions
diff --git a/src/LegacyArithmetic/Pow2Base.v b/src/LegacyArithmetic/Pow2Base.v
new file mode 100644
index 000000000..62f1f742d
--- /dev/null
+++ b/src/LegacyArithmetic/Pow2Base.v
@@ -0,0 +1,19 @@
+Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ZUtil.
+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)).
+End Pow2Base.