diff options
author | Andres Erbsen <andreser@mit.edu> | 2019-01-08 04:21:38 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2019-01-09 22:49:02 -0500 |
commit | 3ca227f1137e6a3b65bc33f5689e1c230d591595 (patch) | |
tree | e1e5a2dd2a2f34f239d3276227ddbdc69eeeb667 /src/LegacyArithmetic/Pow2Base.v | |
parent | 3ec21c64b3682465ca8e159a187689b207c71de4 (diff) |
remove old pipeline
Diffstat (limited to 'src/LegacyArithmetic/Pow2Base.v')
-rw-r--r-- | src/LegacyArithmetic/Pow2Base.v | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/src/LegacyArithmetic/Pow2Base.v b/src/LegacyArithmetic/Pow2Base.v deleted file mode 100644 index c5c69e684..000000000 --- a/src/LegacyArithmetic/Pow2Base.v +++ /dev/null @@ -1,18 +0,0 @@ -Require Import Coq.ZArith.Zpower Coq.ZArith.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)). -End Pow2Base. |