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
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
/* default Order dec */
val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
/* sneaky deref with no effect necessary for bitfield writes */
val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
/* this is here because if we don't have it before including vector_dec
we get infinite loops caused by interaction with bool/bit casts */
/* val eq_bit2 = "eq_bit" : (bit, bit) -> bool */
/* overload operator == = {eq_bit2} */
$include <smt.sail>
$include <flow.sail>
$include <arith.sail>
$include <option.sail>
$include <vector_dec.sail>
infix 7 >>
infix 7 <<
infix 7 ^^
val shift_bits_left = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
val shift_bits_right = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
val shift_left = "shiftl" : forall 'm. (bits('m), int) -> bits('m)
val shift_right = "shiftr" : forall 'm. (bits('m), int) -> bits('m)
overload operator << = {shift_bits_left, shift_left}
overload operator >> = {shift_bits_right, shift_right}
val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
val operator ^^ = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
infix 4 <_s
infix 4 >=_s
infix 4 <_u
infix 4 >=_u
infix 4 <=_u
val operator <_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
val operator <_u : forall 'n. (bits('n), bits('n)) -> bool
val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
function operator <_s (x, y) = signed(x) < signed(y)
function operator >=_s (x, y) = signed(x) >= signed(y)
function operator <_u (x, y) = unsigned(x) < unsigned(y)
function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
val pow2_atom = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
val pow2_int = "pow2" : int -> int
overload pow2 = {pow2_atom, pow2_int}
val cast cast_bool_bit : bool -> bit
function cast_bool_bit(b) =
match b {
true => bitzero,
false => bitone
}
val cast cast_bit_bool : bit -> bool
function cast_bit_bool (b) =
match b {
bitzero => false,
bitone => true
}
val and_bits = {c:"and_bits", _: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
overload operator & = {and_bool, and_bits}
val or_bits = {c:"or_bits", _: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
overload operator | = {or_bool, or_bits}
val not_vec = {c:"not_bits", _:"not_vec"} : forall 'n. bits('n) -> bits('n)
overload ~ = {not_bool, not_vec}
val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
overload operator == = {eq_anything}
val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
function neq_vec (x, y) = not_bool(eq_bits(x, y))
val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
function neq_anything (x, y) = not_bool(x == y)
overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
/* val reg_index : reg_size -> reg_index */
/* function reg_index x = unsigned(x) */
val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
overload quot = {quotient_nat, quotient}
val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w)
val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n)
function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
val to_bits : forall 'l, 'l >= 0.(implicit('l), int) -> bits('l)
function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
overload operator ^ = {xor_vec, int_power, concat_str}
val mask : forall 'l 'm, 'l >= 0 & 'm >= 0. (implicit('l), bits('m)) -> bits('l)
/* put this val spec into Sail lib for "%" */
val mod = {
smt: "mod",
ocaml: "modulus",
lem: "integerMod",
c: "tmod_int",
coq: "Z.rem"
} : forall 'M 'N. (atom('M), atom('N)) -> {'O, 0 <= 'O & 'O < N . atom('O)}
/* overload operator % = {mod_int} */
|
