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/Double/Proofs/LoadImmediate.v | |
parent | 3ec21c64b3682465ca8e159a187689b207c71de4 (diff) |
remove old pipeline
Diffstat (limited to 'src/LegacyArithmetic/Double/Proofs/LoadImmediate.v')
-rw-r--r-- | src/LegacyArithmetic/Double/Proofs/LoadImmediate.v | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v deleted file mode 100644 index 13847b50a..000000000 --- a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v +++ /dev/null @@ -1,32 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.InterfaceProofs. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. - -Local Open Scope Z_scope. -Local Opaque tuple_decoder. -Local Arguments Z.mul !_ !_. - -Section load_immediate. - Context {n W} - {decode : decoder n W} - {is_decode : is_decode decode} - {ldi : load_immediate W} - {is_ldi : is_load_immediate ldi}. - - Global Instance is_load_immediate_double - : is_load_immediate (ldi_double n). - Proof using Type*. - intros x H; hnf in H. - pose proof (decode_exponent_nonnegative decode (ldi x)). - assert (0 <= x mod 2^n < 2^n) by auto with zarith. - assert (x / 2^n < 2^n) - by (apply Z.div_lt_upper_bound; autorewrite with pull_Zpow zsimplify; auto with zarith). - assert (0 <= x / 2^n < 2^n) by (split; Z.zero_bounds). - unfold ldi_double, load_immediate_double; simpl. - autorewrite with simpl_tuple_decoder Zshift_to_pow; simpl; push_decode. - autorewrite with zsimplify; reflexivity. - Qed. -End load_immediate. |