blob: 13847b50addfccbc3f47e9c44289dfa6dc23ea6a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
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.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.
|
