1 | include "common/ByteValues.ma". |
---|
2 | |
---|
3 | (* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps |
---|
4 | not further back in the translation chain. *) |
---|
5 | inductive OpAccs: Type[0] ≝ |
---|
6 | Mul: OpAccs |
---|
7 | | DivuModu: OpAccs. |
---|
8 | |
---|
9 | inductive Op1: Type[0] ≝ |
---|
10 | Cmpl: Op1 |
---|
11 | | Inc: Op1 |
---|
12 | | Rl: Op1. (* TODO: implement left rotation *) |
---|
13 | |
---|
14 | inductive Op2: Type[0] ≝ |
---|
15 | Add: Op2 |
---|
16 | | Addc: Op2 |
---|
17 | | Sub: Op2 |
---|
18 | | And: Op2 |
---|
19 | | Or: Op2 |
---|
20 | | Xor: Op2. |
---|
21 | |
---|
22 | record Eval : Type[0] ≝ |
---|
23 | { |
---|
24 | opaccs: OpAccs → Byte → Byte → Byte × Byte; |
---|
25 | op1: Op1 → Byte → Byte; |
---|
26 | op2: Bit → Op2 → Byte → Byte → (Byte × Bit) |
---|
27 | }. |
---|
28 | |
---|
29 | axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte. |
---|
30 | axiom op1_implementation: Op1 → Byte → Byte. |
---|
31 | axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit). |
---|
32 | |
---|
33 | definition eval : Eval ≝ |
---|
34 | mk_Eval opaccs_implementation |
---|
35 | op1_implementation |
---|
36 | op2_implementation. |
---|
37 | |
---|
38 | axiom UnsupportedOp : String. |
---|
39 | |
---|
40 | definition be_opaccs : OpAccs → beval → beval → res (beval × beval) ≝ |
---|
41 | λop,a,b. |
---|
42 | ! a' ← Byte_of_val UnsupportedOp a ; |
---|
43 | ! b' ← Byte_of_val UnsupportedOp b ; |
---|
44 | let 〈a'',b''〉 ≝ opaccs eval op a' b' in |
---|
45 | return 〈BVByte a'', BVByte b''〉. |
---|
46 | |
---|
47 | definition be_op1 : Op1 → beval → res beval ≝ |
---|
48 | λop,a. |
---|
49 | ! a' ← Byte_of_val UnsupportedOp a ; |
---|
50 | return BVByte (op1 eval op a'). |
---|
51 | |
---|
52 | definition op2_bytes : Op2 → ∀n.Bit → Vector Byte n → Vector Byte n → (Vector Byte n) × Bit ≝ |
---|
53 | λop,n,carry. |
---|
54 | let f ≝ λn,b1,b2.λpr : (Vector Byte n) × Bit. |
---|
55 | let 〈res_tl, carry〉 ≝ pr in |
---|
56 | let 〈res_hd,carry'〉 ≝ op2 eval carry op b1 b2 in |
---|
57 | 〈res_hd ::: res_tl, carry'〉 in |
---|
58 | fold_right2_i … f 〈[[ ]],carry〉 n. |
---|
59 | |
---|
60 | definition be_add_sub_byte : bool → bebit → beval → Byte → res (beval × bebit) ≝ |
---|
61 | λis_add,carry,a1,b2. |
---|
62 | let op ≝ if is_add then Addc else Sub in |
---|
63 | match a1 with |
---|
64 | [ BVByte b1 ⇒ |
---|
65 | ! carry' ← Bit_of_val UnsupportedOp carry ; |
---|
66 | let 〈rslt, carry''〉 ≝ op2 eval carry' op b1 b2 in |
---|
67 | return 〈BVByte rslt, BBbit carry''〉 |
---|
68 | | BVptr ptr p ⇒ |
---|
69 | match ptype ptr with |
---|
70 | [ Code ⇒ Error … [MSG UnsupportedOp] |
---|
71 | | XData ⇒ |
---|
72 | match p with |
---|
73 | [ O ⇒ |
---|
74 | ! carry' ← Bit_of_val UnsupportedOp carry ; |
---|
75 | if carry' then Error … [MSG UnsupportedOp] |
---|
76 | else |
---|
77 | let o1o0 : Byte × Byte ≝ vsplit ? 8 8 (offv (poff ptr)) in |
---|
78 | let 〈rslt,carry〉 ≝ op2 eval false op b2 (\snd o1o0) in |
---|
79 | let p0 ≝ mk_part 0 (le_S … (le_n …)) in |
---|
80 | let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (\fst o1o0 @@ rslt)) in |
---|
81 | return 〈BVptr ptr' p, BBptrcarry is_add ptr p0 b2〉 |
---|
82 | | _ ⇒ (* it is 1. To generalize, many casts ⌈…⌉ needs to be added *) |
---|
83 | match carry with |
---|
84 | [ BBptrcarry is_add' ptr' p' by' ⇒ |
---|
85 | if eq_b is_add is_add' ∧ eq_block (pblock ptr) (pblock ptr') ∧ |
---|
86 | eq_bv_suffix 8 8 8 (offv (poff ptr)) (offv (poff ptr')) |
---|
87 | then If eqb p' 0 then with prf do |
---|
88 | let by' : Byte ≝ by' ⌈? ↦ Byte⌉ in |
---|
89 | let o1o0 ≝ vsplit ? 8 8 (offv (poff ptr)) in |
---|
90 | let o1o0 ≝ [[\fst o1o0 ; \snd o1o0]] in |
---|
91 | let 〈rslt,ignore〉 ≝ op2_bytes op ? false o1o0 [[b2 ; by']] in |
---|
92 | let part1 ≝ mk_part 1 (le_n …) in |
---|
93 | let ptr' ≝ mk_pointer (pblock ptr) (mk_offset (vflatten … rslt)) in |
---|
94 | OK … 〈BVptr ptr' part1, |
---|
95 | BBptrcarry is_add ptr' part1 (b2 @@ by')〉 |
---|
96 | else Error … [MSG UnsupportedOp] |
---|
97 | else Error … [MSG UnsupportedOp] |
---|
98 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
99 | ] |
---|
100 | ] |
---|
101 | ] |
---|
102 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
103 | ]. |
---|
104 | @hide_prf |
---|
105 | lapply prf @(eqb_elim p') #H * >H % |
---|
106 | qed. |
---|
107 | |
---|
108 | definition byte_at : ∀n.BitVector (8*n) → ∀p.p < n → Byte ≝ |
---|
109 | λn,v,p,H. |
---|
110 | let suffix : BitVector (8 + 8*p) ≝ |
---|
111 | \snd (vsplit … (v⌈BitVector ?↦BitVector (8*(n - S p) + (8 + 8*p))⌉)) in |
---|
112 | \fst (vsplit … suffix). |
---|
113 | >(commutative_times_fast ? p) |
---|
114 | change with (? = BitVector (? + S p*8)) |
---|
115 | >(commutative_times_fast (S p)) |
---|
116 | <distributive_times_plus_fast |
---|
117 | <(plus_minus_m_m … H) % |
---|
118 | qed. |
---|
119 | |
---|
120 | definition eq_opt : ∀A.(A → A → bool) → option A → option A → bool ≝ |
---|
121 | λA,eq,m,n. |
---|
122 | match m with |
---|
123 | [ Some a ⇒ |
---|
124 | match n with |
---|
125 | [ Some b ⇒ eq a b |
---|
126 | | _ ⇒ false |
---|
127 | ] |
---|
128 | | _ ⇒ |
---|
129 | match m with |
---|
130 | [ None ⇒ true |
---|
131 | | _ ⇒ false |
---|
132 | ] |
---|
133 | ]. |
---|
134 | |
---|
135 | (* This tables shows what binary ops may be defined on bevals depending on |
---|
136 | the arguments (columns marked by 1st argument, rows by 2nd). Further |
---|
137 | checks for definedness are done for pointer parts taking into account |
---|
138 | blocks, parts and the carry value. |
---|
139 | Neither BVundef nor BVpc allow any operations |
---|
140 | arg2\arg1 | BVByte | BVptr (D) | BVptr (C) | BVnull | BVXor | BVnonzero | |
---|
141 | ----------+-----------+----------------+-----------+--------+-------+-----------+ |
---|
142 | BVByte | all | Add, Addc, Sub | -- | -- | -- | Or | |
---|
143 | ----------+-----------+----------------+-----------+--------+-------+-----------+ |
---|
144 | BVptr (D) | Add, Addc | Sub, Xor | Xor | Xor | -- | -- | |
---|
145 | ----------+-----------+----------------+-----------+--------+-------+-----------+ |
---|
146 | BVptr (C) | -- | Xor | Xor | Xor | -- | -- | |
---|
147 | ----------+-----------+----------------+-----------+--------+-------+-----------+ |
---|
148 | BVnull | -- | Xor | Xor | Xor | -- | -- | |
---|
149 | ----------+-----------+----------------+-----------+--------+-------+-----------+ |
---|
150 | BVXor | -- | -- | -- | -- | Or | Or | |
---|
151 | ----------+-----------+----------------+-----------+--------+-------+-----------+ |
---|
152 | BVnonzero | Or | -- | -- | -- | Or | -- | |
---|
153 | ----------+-----------+----------------+-----------+--------+-------+-----------+ |
---|
154 | *) |
---|
155 | definition be_op2 : bebit → Op2 → beval → beval → res (beval × bebit) ≝ |
---|
156 | λcarry,op,a1,a2. |
---|
157 | match a1 with |
---|
158 | [ BVByte b1 ⇒ |
---|
159 | (* if match op with [ Or ⇒ true | _ ⇒ false ] ∧ eq_bv … (zero …) b1 then |
---|
160 | return 〈a2, carry〉 |
---|
161 | else *) (* maybe it will be needed, need to see actual translations *) |
---|
162 | match a2 with |
---|
163 | [ BVByte b2 ⇒ |
---|
164 | ! carry ← Bit_of_val UnsupportedOp carry ; |
---|
165 | let 〈result, carry〉 ≝ op2 eval carry op b1 b2 in |
---|
166 | return 〈BVByte result, BBbit carry〉 |
---|
167 | | BVptr _ _ ⇒ |
---|
168 | match op with |
---|
169 | [ Add ⇒ be_add_sub_byte true (BBbit false) a2 b1 |
---|
170 | | Addc ⇒ be_add_sub_byte true carry a2 b1 |
---|
171 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
172 | ] |
---|
173 | | BVnonzero ⇒ |
---|
174 | match op with |
---|
175 | [ Or ⇒ return 〈BVnonzero, carry〉 |
---|
176 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
177 | ] |
---|
178 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
179 | ] |
---|
180 | | BVptr ptr1 p1 ⇒ |
---|
181 | match a2 with |
---|
182 | [ BVByte b2 ⇒ |
---|
183 | match op with |
---|
184 | [ Add ⇒ be_add_sub_byte true (BBbit false) a1 b2 |
---|
185 | | Addc ⇒ be_add_sub_byte true carry a1 b2 |
---|
186 | | Sub ⇒ be_add_sub_byte false carry a1 b2 |
---|
187 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
188 | ] |
---|
189 | | BVptr ptr2 p2 ⇒ |
---|
190 | match op with |
---|
191 | [ Sub ⇒ |
---|
192 | match ptype ptr1 with |
---|
193 | [ Code ⇒ Error … [MSG UnsupportedOp] |
---|
194 | | XData ⇒ |
---|
195 | if eq_block (pblock ptr1) (pblock ptr2) ∧ |
---|
196 | eqb p1 p2 |
---|
197 | then |
---|
198 | ! carry ← Bit_of_val UnsupportedOp carry ; |
---|
199 | let by1 ≝ byte_at ? (offv (poff ptr1)) … (part_no_ok p1) in |
---|
200 | let by2 ≝ byte_at ? (offv (poff ptr2)) … (part_no_ok p1) in |
---|
201 | let 〈result, carry〉 ≝ op2 eval carry Sub by1 by2 in |
---|
202 | return 〈BVByte result, BBbit carry〉 |
---|
203 | else Error … [MSG UnsupportedOp] |
---|
204 | ] |
---|
205 | | Xor ⇒ |
---|
206 | if eqb p1 p2 then |
---|
207 | return 〈BVXor (Some ? ptr1) (Some ? ptr2) p1, carry〉 |
---|
208 | else Error … [MSG UnsupportedOp] |
---|
209 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
210 | ] |
---|
211 | | BVnull p2 ⇒ |
---|
212 | match op with |
---|
213 | [ Xor ⇒ |
---|
214 | if eqb p1 p2 then |
---|
215 | return 〈BVXor (Some ? ptr1) (None ?) p1, carry〉 |
---|
216 | else |
---|
217 | Error … [MSG UnsupportedOp] |
---|
218 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
219 | ] |
---|
220 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
221 | ] |
---|
222 | | BVnull p1 ⇒ |
---|
223 | match op with |
---|
224 | [ Xor ⇒ |
---|
225 | match a2 with |
---|
226 | [ BVptr ptr2 p2 ⇒ |
---|
227 | if eqb p1 p2 then |
---|
228 | return 〈BVXor (None ?) (Some ? ptr2) p1, carry〉 |
---|
229 | else |
---|
230 | Error … [MSG UnsupportedOp] |
---|
231 | | BVnull p2 ⇒ |
---|
232 | if eqb p1 p2 then |
---|
233 | return 〈BVXor (None ?) (None ?) p1, carry〉 |
---|
234 | else |
---|
235 | Error … [MSG UnsupportedOp] |
---|
236 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
237 | ] |
---|
238 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
239 | ] |
---|
240 | | BVXor ptr1_opt ptr1_opt' p1 ⇒ |
---|
241 | match op with |
---|
242 | [ Or ⇒ |
---|
243 | match a2 with |
---|
244 | [ BVByte b2 ⇒ |
---|
245 | if eq_bv … (bv_zero …) b2 then return 〈a1, carry〉 |
---|
246 | else Error … [MSG UnsupportedOp] |
---|
247 | | BVnonzero ⇒ return 〈BVnonzero, carry〉 |
---|
248 | | BVXor ptr2_opt ptr2_opt' p2 ⇒ |
---|
249 | if ((eqb p1 0 ∧ eqb p2 1) ∨ (eqb p1 1 ∧ eqb p2 0)) then |
---|
250 | let eq_at ≝ λp,ptr1,ptr2. |
---|
251 | eq_block (pblock ptr1) (pblock ptr2) ∧ |
---|
252 | eq_bv … (byte_at ? (offv (poff ptr1)) … (part_no_ok p)) |
---|
253 | (byte_at ? (offv (poff ptr2)) … (part_no_ok p)) in |
---|
254 | if eq_opt ? (eq_at p1) ptr1_opt ptr1_opt' ∧ |
---|
255 | eq_opt ? (eq_at p2) ptr2_opt ptr2_opt' |
---|
256 | then return 〈BVByte (bv_zero …), carry〉 |
---|
257 | else return 〈BVnonzero, carry〉 |
---|
258 | else Error … [MSG UnsupportedOp] |
---|
259 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
260 | ] |
---|
261 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
262 | ] |
---|
263 | | BVnonzero ⇒ |
---|
264 | match op with |
---|
265 | [ Or ⇒ |
---|
266 | match a2 with |
---|
267 | [ BVByte _ ⇒ return 〈BVnonzero, carry〉 |
---|
268 | | BVnonzero ⇒ return 〈BVnonzero, carry〉 |
---|
269 | | BVXor _ _ _ ⇒ return 〈BVnonzero, carry〉 |
---|
270 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
271 | ] |
---|
272 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
273 | ] |
---|
274 | | _ ⇒ Error … [MSG UnsupportedOp] |
---|
275 | ]. |
---|