blob: f44b1b7f757569003a7ba7bfd9129e925abf7097 (
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
(** * Strip CF for Interface for bounded arithmetic *)
Require Import Coq.ZArith.ZArith.
Require Import Crypto.BoundedArithmetic.Interface.
Local Open Scope type_scope.
Local Open Scope Z_scope.
Section strip_CF.
Context (n : Z) (* bit-width of width of [W] *)
{W : Type} (* bounded type, [W] for word *)
(Wdecoder : decoder n W).
Local Notation imm := Z (only parsing). (* immediate (compile-time) argument *)
Global Instance shift_right_doubleword_immediate_strip_CF
{shrdf : shift_right_doubleword_immediate_with_CF W}
: shift_right_doubleword_immediate W
:= { shrd x y z := snd (shrdf x y z) }.
Global Instance is_shift_right_doubleword_immediate_strip_CF
{shrdf : shift_right_doubleword_immediate_with_CF W}
{shift_right_doubleword_immediate_with_CF : is_shift_right_doubleword_immediate_with_CF shrdf}
: is_shift_right_doubleword_immediate shift_right_doubleword_immediate_strip_CF
:= shift_right_doubleword_immediate_with_CF.
Global Instance shift_left_immediate_strip_CF
{shlf : shift_left_immediate_with_CF W}
: shift_left_immediate W
:= { shl x y := snd (shlf x y) }.
Global Instance is_shift_left_immediate_strip_CF
{shlf : shift_left_immediate_with_CF W}
{shift_left_immediate_with_CF : is_shift_left_immediate_with_CF shlf}
: is_shift_left_immediate shift_left_immediate_strip_CF
:= shift_left_immediate_with_CF.
Global Instance shift_right_immediate_strip_CF
{shrf : shift_right_immediate_with_CF W}
: shift_right_immediate W
:= { shr x y := snd (shrf x y) }.
Global Instance is_shift_right_immediate_strip_CF
{shrf : shift_right_immediate_with_CF W}
{shift_right_immediate_with_CF : is_shift_right_immediate_with_CF shrf}
: is_shift_right_immediate shift_right_immediate_strip_CF
:= shift_right_immediate_with_CF.
Global Instance bitwise_and_strip_CF
{andf : bitwise_and_with_CF W}
: bitwise_and W
:= { and x y := snd (andf x y) }.
Global Instance is_bitwise_and_strip_CF
{andf : bitwise_and_with_CF W}
{bitwise_and_with_CF : is_bitwise_and_with_CF andf}
: is_bitwise_and bitwise_and_strip_CF
:= { decode_bitwise_and := @decode_snd_bitwise_and_with_CF _ _ _ _ bitwise_and_with_CF }.
Global Instance bitwise_or_strip_CF
{orf : bitwise_or_with_CF W}
: bitwise_or W
:= { or x y := snd (orf x y) }.
Global Instance is_bitwise_or_strip_CF
{orf : bitwise_or_with_CF W}
{bitwise_or_with_CF : is_bitwise_or_with_CF orf}
: is_bitwise_or bitwise_or_strip_CF
:= { decode_bitwise_or := @decode_snd_bitwise_or_with_CF _ _ _ _ bitwise_or_with_CF }.
Global Instance multiply_double_strip_CF
{muldwf : multiply_double_with_CF W}
: multiply_double W
:= { muldw x y := snd (muldwf x y) }.
Global Instance is_mul_double_strip_CF
{muldwf : multiply_double_with_CF W}
{multiply_double_with_CF : is_mul_double_with_CF muldwf}
: is_mul_double multiply_double_strip_CF
:= { decode_fst_mul_double := @decode_fst_mul_double_with_CF _ _ _ _ multiply_double_with_CF;
decode_snd_mul_double := @decode_snd_mul_double_with_CF _ _ _ _ multiply_double_with_CF}.
End strip_CF.
|
