diff options
Diffstat (limited to 'src/LegacyArithmetic/Double/Proofs/LoadImmediate.v')
-rw-r--r-- | src/LegacyArithmetic/Double/Proofs/LoadImmediate.v | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v new file mode 100644 index 000000000..2c7f87dd7 --- /dev/null +++ b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v @@ -0,0 +1,32 @@ +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. + +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. |