avrmodel.mlw 35.3 KB
Newer Older
Marc Schoolderman's avatar
Marc Schoolderman committed
1
2
3
4
5
module AVRint

use import int.Int
use import int.EuclideanDivision
use import ref.Ref
Marc Schoolderman's avatar
Marc Schoolderman committed
6
use import map.Map
Marc Schoolderman's avatar
Marc Schoolderman committed
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
use import bv.Pow2int

(***** FORMAL MODEL OF AVR ******)

type register = int

constant r0: register = 0
constant r1: register = 1
constant r2: register = 2
constant r3: register = 3
constant r4: register = 4
constant r5: register = 5
constant r6: register = 6
constant r7: register = 7
constant r8: register = 8
constant r9: register = 9
constant r10: register = 10
constant r11: register = 11
constant r12: register = 12
constant r13: register = 13
constant r14: register = 14
constant r15: register = 15
constant r16: register = 16
constant r17: register = 17
constant r18: register = 18
constant r19: register = 19
constant r20: register = 20
constant r21: register = 21
constant r22: register = 22
constant r23: register = 23
constant r24: register = 24
constant r25: register = 25
constant r26: register = 26
constant r27: register = 27
constant r28: register = 28
constant r29: register = 29
constant r30: register = 30
constant r31: register = 31

Marc Schoolderman's avatar
Marc Schoolderman committed
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
type cpu_flag = { mutable value: bool }

function (?) (x: cpu_flag): int = if x.value then 1 else 0

let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0

val cf: cpu_flag

type address_space = { mutable data: map int int }
  invariant { forall i. 0 <= self.data[i] < 256 }

function ([]) (r: address_space) (i: register): int = Map.get r.data i
function ([<-]) (r: address_space) (i: register) (v: int): address_space
  = { data = Map.set r.data i v }

function get_uint_term (rlo: (address_space, int)) (i: int): int
  = let (reg, lo) = rlo in pow2 (8*i) * reg[lo+i]

clone sum.Sum as B with type container = (address_space, int), function f = get_uint_term

function uint (w: int) (reg: address_space) (lo: register): int
  = B.sum (reg,lo) 0 w

val reg: address_space

let mov (dst src: register): unit
  writes { reg }
  ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- Map.set reg.data dst (Map.get reg.data src)

Marc Schoolderman's avatar
Marc Schoolderman committed
76
77
78
79
80
81
let ldi (dst: register) (imm: int): unit
  writes { reg }
  requires { 0 <= imm < 256 }
  ensures { reg = old reg[dst<-imm] }
= reg.data <- Map.set reg.data dst imm

Marc Schoolderman's avatar
Marc Schoolderman committed
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
let mul (dst src: register): unit
  writes { cf }
  writes { reg }
  ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- mod p 256][1 <- div p 256] }
  ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) }
  (* ensures { reg[1] < 255 } *)
= let prod = Map.get reg.data dst*Map.get reg.data src in
  reg.data <- Map.set (Map.set reg.data 0 (mod prod 256)) 1 (div prod 256);
  cf.value <- (div prod (pow2 15) <> 0);
  ()

let add (dst src: register): unit
  writes { cf }
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src])) 256] }
  ensures { ?cf = div (old (reg[dst] + reg[src])) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst in
  let r1 = (Map.get reg.data dst) in
  let r2 = (Map.get reg.data src) in
  reg.data <- Map.set reg.data dst (mod sum 256);
  let res = (Map.get reg.data dst) in
103
104
105
106
107
108
109
  if r1 >= 128 && r2 >= 128 ||
     r1 >= 128 && res < 128  ||
     r2 >= 128 && res < 128
  then
     cf.value <- True
  else
     cf.value <- False
Marc Schoolderman's avatar
Marc Schoolderman committed
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

let adc (dst src: register): unit
  writes { cf }
  reads { cf }
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] + reg[src] + ?cf)) 256] }
  ensures { ?cf = div (old (reg[dst] + reg[src] + ?cf)) 256 }
= let sum = Map.get reg.data src + Map.get reg.data dst + ?cf in
  reg.data <- Map.set reg.data dst (mod sum 256);
  cf.value <- (div sum 256 <> 0);
  ()

let sub (dst src: register): unit
  writes { cf }
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src])) 256] }
  ensures { ?cf = -div (old (reg[dst] - reg[src])) 256 }
= let sum = Map.get reg.data dst - Map.get reg.data src in
  reg.data <- Map.set reg.data dst (mod sum 256);
  assert { -255 <= sum <= 255 };
  cf.value <- (-div sum 256 <> 0);
  ()

let sbc (dst src: register): unit
  writes { cf }
  reads { cf }
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src] - ?cf)) 256] }
  ensures { ?cf = -div (old (reg[dst] - reg[src] - ?cf)) 256 }
= let sum = Map.get reg.data dst - Map.get reg.data src - ?cf in
  reg.data <- Map.set reg.data dst (mod sum 256);
  cf.value <- (-div sum 256 <> 0);
  ()

144
145
146
147
148
149
150
151
152
153
154
155
156
157
let neg (dst: register): unit
  writes { cf }
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (-reg[dst])) 256] }
(* TODO: which one is useful?
  ensures { ?cf = if reg[dst] = 0 then 0 else 1 }
  ensures { ?cf = -div (old (-reg[dst])) 256 }
*)
= let sum = - Map.get reg.data dst in
  reg.data <- Map.set reg.data dst (mod sum 256);
  assert { -255 <= sum <= 255 };
  cf.value <- (-div sum 256 <> 0);
  ()

158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
(* immediate versions *)
let subi (dst: register) (k: int): unit
  requires { 0 <= k <= 255 }
  writes { cf }
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] - k)) 256] }
  ensures { ?cf = -div (old (reg[dst] - k)) 256 }
= let sum = Map.get reg.data dst - k in
  reg.data <- Map.set reg.data dst (mod sum 256);
  cf.value <- (-div sum 256 <> 0);
  ()

let sbci (dst: register) (k: int): unit
  requires { 0 <= k <= 255 }
  writes { cf }
  reads { cf }
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] - k - ?cf)) 256] }
  ensures { ?cf = -div (old (reg[dst] - k - ?cf)) 256 }
= let sum = Map.get reg.data dst - k - ?cf in
  reg.data <- Map.set reg.data dst (mod sum 256);
  cf.value <- (-div sum 256 <> 0);
  ()

182
183
184
185
186
187
188
189
190
191
192
193
194
(* these instructions do not modify the carry flag *)
let inc (dst: register): unit
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] + 1)) 256] }
= let sum = Map.get reg.data dst + 1 in
  reg.data <- Map.set reg.data dst (mod sum 256)

let dec (dst: register): unit
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] - 1)) 256] }
= let sum = Map.get reg.data dst - 1 in
  reg.data <- Map.set reg.data dst (mod sum 256)

Marc Schoolderman's avatar
Marc Schoolderman committed
195
196
197
198
199
200
201
202
203
constant rX: register = 26
constant rY: register = 28
constant rZ: register = 30

val mem: address_space

let ld_inc (dst src: register): unit
  writes { reg }
  reads { mem }
204
  requires { 32 <= uint 2 reg src < pow2 16-1 }
205
(* TODO unnecessary
206
  requires { dst <> src /\ dst <> src+1 }
207
*)
208
209
210
  ensures { let cur = uint 2 (old reg) src in
            let inc = cur+1 in
            reg = (old reg)[dst <- mem[cur]][src <- mod inc 256][src+1 <- div inc 256] }
211
  ensures { uint 2 reg src = old(uint 2 reg src)+1 }
212
213
214
215
216
217
218
219
220
221
222
223
224
= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
  let nxt = mod (cur+1) (pow2 16) in
  reg.data <- Map.set (Map.set (Map.set reg.data dst (Map.get mem.data cur)) src (mod nxt 256)) (src+1) (div nxt 256)

let ldd (dst src ofs: register): unit
  writes { reg }
  reads { mem }
  requires { 32 <= uint 2 reg src + ofs < pow2 16 }
  ensures { let cur = uint 2 (old reg) src in
            reg = (old reg)[dst <- mem[cur+ofs]] }
= let cur = Map.get reg.data src + 256*Map.get reg.data (src+1) in
  reg.data <- Map.set reg.data dst (Map.get mem.data (cur+ofs))

Marc Schoolderman's avatar
Marc Schoolderman committed
225
226
227
let st_inc (dst src: register): unit
  writes { reg }
  writes { mem }
228
229
  requires { 32 <= uint 2 reg dst < pow2 16-1 }
  ensures { let cur = uint 2 (old reg) dst in
Marc Schoolderman's avatar
Marc Schoolderman committed
230
            let inc = cur+1 in
231
232
            reg = (old reg)[dst <- mod inc 256][dst+1 <- div inc 256] }
  ensures { let cur = uint 2 (old reg) dst in
Marc Schoolderman's avatar
Marc Schoolderman committed
233
            mem = (old mem)[cur <- reg[src]] }
234
235
  ensures { uint 2 reg dst = old(uint 2 reg dst)+1 }
= let cur = Map.get reg.data dst + 256*Map.get reg.data (dst+1) in
Marc Schoolderman's avatar
Marc Schoolderman committed
236
  let nxt = mod (cur+1) (pow2 16) in
237
  reg.data <- Map.set (Map.set reg.data dst (mod nxt 256)) (dst+1) (div nxt 256);
Marc Schoolderman's avatar
Marc Schoolderman committed
238
239
  mem.data <- Map.set mem.data cur (Map.get reg.data src)

240
241
242
243
244
245
246
247
248
let std (dst ofs src: register): unit
  writes { mem }
  reads { reg }
  requires { 32 <= uint 2 reg dst + ofs < pow2 16 }
  ensures { let cur = uint 2 (old reg) dst in
            mem = (old mem)[cur+ofs <- reg[src]] }
= let cur = Map.get reg.data dst + 256*Map.get reg.data (dst+1) in
  mem.data <- Map.set mem.data (cur+ofs) (Map.get reg.data src)

249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
(* stack operations *)

constant stack_limit: int
val stack_pointer: ref int
val stack: address_space

let push (src: register): unit
  writes { stack, stack_pointer }
  reads { reg }
  ensures { stack = old(stack[!stack_pointer <- reg[src]]) }
  ensures { !stack_pointer = old !stack_pointer - 1 }
= stack.data <- Map.set stack.data (!stack_pointer) (Map.get reg.data src);
  stack_pointer := !stack_pointer - 1

let pop (dst: register): unit
  writes { reg, stack_pointer }
  reads { stack }
  ensures { reg = (old reg)[dst <- stack[!stack_pointer]] }
  ensures { !stack_pointer = old !stack_pointer + 1 }
= stack_pointer := !stack_pointer + 1;
  reg.data <- Map.set reg.data dst (Map.get stack.data !stack_pointer)

271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
let nop (): unit
= ()

(****** REASONING ABOUT MACHINE STATE *)

predicate eq (w: int) (reg reg': address_space) (lo: int)
  = forall i. lo <= i < lo+w -> reg[i] = reg'[i]

goal eq_narrow:
  forall reg reg', lo lo' w w'. lo <= lo' -> lo'+w' <= lo+w -> eq w reg reg' lo -> eq w' reg reg' lo'
goal eq_combine:
  forall reg reg', lo lo' w w'. eq w reg reg' lo -> eq w' reg reg' lo' -> lo' = lo+w -> eq (w+w') reg reg' lo
goal eq_uint:
  forall reg reg', lo w. eq w reg reg' lo -> uint w reg lo = uint w reg' lo

286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
lemma uint_0:
  forall reg, lo. B.sum (reg,lo) 0 0 = 0
lemma uint_1:
  forall reg, lo. B.sum (reg,lo) 0 1 = reg[lo]
meta rewrite prop uint_1
lemma uint_2:
  forall reg, lo. B.sum (reg,lo) 0 2 = reg[lo] + pow2 8*reg[lo+1]
meta rewrite prop uint_2
lemma uint_3:
  forall reg, lo. B.sum (reg,lo) 0 3 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2]
meta rewrite prop uint_3
lemma uint_4:
  forall reg, lo. B.sum (reg,lo) 0 4 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3]
meta rewrite prop uint_4
lemma uint_5:
  forall reg, lo. B.sum (reg,lo) 0 5 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4]
meta rewrite prop uint_5
lemma uint_6:
  forall reg, lo. B.sum (reg,lo) 0 6 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5]
meta rewrite prop uint_6
lemma uint_7:
  forall reg, lo. B.sum (reg,lo) 0 7 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6]
meta rewrite prop uint_7
lemma uint_8:
  forall reg, lo. B.sum (reg,lo) 0 8 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7]
meta rewrite prop uint_8
lemma uint_9:
  forall reg, lo. B.sum (reg,lo) 0 9 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8]
meta rewrite prop uint_9
lemma uint_10:
  forall reg, lo. B.sum (reg,lo) 0 10 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9]
meta rewrite prop uint_10
lemma uint_11:
  forall reg, lo. B.sum (reg,lo) 0 11 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10]
meta rewrite prop uint_11
lemma uint_12:
  forall reg, lo. B.sum (reg,lo) 0 12 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11]
meta rewrite prop uint_12
lemma uint_13:
  forall reg, lo. B.sum (reg,lo) 0 13 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12]
meta rewrite prop uint_13
lemma uint_14:
  forall reg, lo. B.sum (reg,lo) 0 14 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13]
meta rewrite prop uint_14
lemma uint_15:
  forall reg, lo. B.sum (reg,lo) 0 15 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14]
meta rewrite prop uint_15
lemma uint_16:
  forall reg, lo. B.sum (reg,lo) 0 16 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15]
meta rewrite prop uint_16
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
lemma uint_17:
  forall reg, lo. B.sum (reg,lo) 0 17 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16]
meta rewrite prop uint_17
lemma uint_18:
  forall reg, lo. B.sum (reg,lo) 0 18 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17]
meta rewrite prop uint_18
lemma uint_19:
  forall reg, lo. B.sum (reg,lo) 0 19 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18]
meta rewrite prop uint_19
lemma uint_20:
  forall reg, lo. B.sum (reg,lo) 0 20 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19]
meta rewrite prop uint_20
lemma uint_21:
  forall reg, lo. B.sum (reg,lo) 0 21 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20]
meta rewrite prop uint_21
lemma uint_22:
  forall reg, lo. B.sum (reg,lo) 0 22 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21]
meta rewrite prop uint_22
lemma uint_23:
  forall reg, lo. B.sum (reg,lo) 0 23 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22]
meta rewrite prop uint_23
lemma uint_24:
  forall reg, lo. B.sum (reg,lo) 0 24 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23]
meta rewrite prop uint_24
lemma uint_25:
  forall reg, lo. B.sum (reg,lo) 0 25 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24]
meta rewrite prop uint_25
lemma uint_26:
  forall reg, lo. B.sum (reg,lo) 0 26 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25]
meta rewrite prop uint_26
lemma uint_27:
  forall reg, lo. B.sum (reg,lo) 0 27 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26]
meta rewrite prop uint_27
lemma uint_28:
  forall reg, lo. B.sum (reg,lo) 0 28 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27]
meta rewrite prop uint_28
lemma uint_29:
  forall reg, lo. B.sum (reg,lo) 0 29 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28]
meta rewrite prop uint_29
lemma uint_30:
  forall reg, lo. B.sum (reg,lo) 0 30 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29]
meta rewrite prop uint_30
lemma uint_31:
  forall reg, lo. B.sum (reg,lo) 0 31 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29] + pow2 240*reg[lo+30]
meta rewrite prop uint_31
lemma uint_32:
  forall reg, lo. B.sum (reg,lo) 0 32 = reg[lo] + pow2 8*reg[lo+1] + pow2 16*reg[lo+2] + pow2 24*reg[lo+3] + pow2 32*reg[lo+4] + pow2 40*reg[lo+5] + pow2 48*reg[lo+6] + pow2 56*reg[lo+7] + pow2 64*reg[lo+8] + pow2 72*reg[lo+9] + pow2 80*reg[lo+10] + pow2 88*reg[lo+11] + pow2 96*reg[lo+12] + pow2 104*reg[lo+13] + pow2 112*reg[lo+14] + pow2 120*reg[lo+15] + pow2 128*reg[lo+16] + pow2 136*reg[lo+17] + pow2 144*reg[lo+18] + pow2 152*reg[lo+19] + pow2 160*reg[lo+20] + pow2 168*reg[lo+21] + pow2 176*reg[lo+22] + pow2 184*reg[lo+23] + pow2 192*reg[lo+24] + pow2 200*reg[lo+25] + pow2 208*reg[lo+26] + pow2 216*reg[lo+27] + pow2 224*reg[lo+28] + pow2 232*reg[lo+29] + pow2 240*reg[lo+30] + pow2 248*reg[lo+31]
meta rewrite prop uint_32
384
385
meta compute_max_steps 0x1000000

386
387
388
(* word operations *)
let movw (dst src: register): unit
(* TODO unnecessary
389
  requires { mod dst 2 = 0 /\ mod src 2 = 0 }
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
*)
  writes { reg }
  ensures { reg = old reg[dst<-reg[src]][dst+1<-reg[src+1]] }
= reg.data <- Map.set (Map.set reg.data dst (Map.get reg.data src)) (dst+1) (Map.get reg.data (src+1))

let adiw (dst: register) (k: int): unit
  requires { 0 <= k < 64 }
(* TODO unnecessary
  requires { dst = 24 \/ dst = 26 \/ dst = 28 \/ dst = 30 }
*)
  writes { reg }
  writes { cf }
  ensures { reg = old reg[dst   <- mod (old (reg[dst] + k)) 256]
                         [dst+1 <- mod (old (reg[dst+1] + div (reg[dst] + k) 256)) 256] }
  ensures { ?cf = div (old (uint 2 reg dst + k)) 65536 }
  ensures { ?cf*pow2 16 + uint 2 reg dst = old (uint 2 reg dst + k) }
= let sum = Map.get reg.data dst + 256*Map.get reg.data (dst+1) +k in
  reg.data <- Map.set reg.data dst (mod sum 256);
  reg.data <- Map.set reg.data (dst+1) (mod (div sum 256) 256);
  cf.value <- (sum > 65535)
410

411
412
413
414
415
416
417
418
419
420
421
422
423
424
425

let sbiw (dst: register) (k: int): unit
  requires { 0 <= k < 64 }
(* TODO unnecessary
  requires { dst = 24 \/ dst = 26 \/ dst = 28 \/ dst = 30 }
*)
  writes { reg }
  writes { cf }
  ensures { reg = old reg[dst   <- mod (old (reg[dst] - k)) 256]
                         [dst+1 <- mod (old (reg[dst+1] + div (reg[dst] - k) 256)) 256] }
  ensures { ?cf = -div (old (uint 2 reg dst - k)) 65536 }
  ensures { uint 2 reg dst = ?cf*pow2 16 + old (uint 2 reg dst - k) }
= subi dst k;
  sbci (dst+1) 0

426
427
428
429
430
431
432
433
434
435
436
(*************** BITVECTOR IMPORTS ********************)

use bv.BV8

let add_ (dst src: register): unit
  writes { reg, cf }
  ensures { reg = old (reg[dst <- mod (reg[dst] + reg[src]) 256]) }
  ensures { ?cf = old (div (reg[dst] + reg[src]) 256) }
= let rd  = BV8.of_int (Map.get reg.data dst) in
  let rr  = BV8.of_int (Map.get reg.data src) in
  let rd' = BV8.add rd rr in
437
  reg.data <- Map.set reg.data dst (BV8.t'int rd');
Marc Schoolderman's avatar
Marc Schoolderman committed
438
  cf.value <- (BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rd 7 && not BV8.nth rd' 7 || not BV8.nth rd' 7 && BV8.nth rr 7)
439

440
441
442
443
444
445
446
447
448
449
let sub_ (dst src: register): unit
  writes { reg, cf }
  ensures { reg = old reg[dst <- mod (old (reg[dst] - reg[src])) 256] }
  ensures { ?cf = -div (old (reg[dst] - reg[src])) 256 }
= let rd  = BV8.of_int (Map.get reg.data dst) in
  let rr  = BV8.of_int (Map.get reg.data src) in
  let rd' = BV8.sub rd rr in
  reg.data <- Map.set reg.data dst (BV8.t'int rd');
  cf.value <- (not BV8.nth rd 7 && BV8.nth rr 7 || BV8.nth rr 7 && BV8.nth rd' 7 || BV8.nth rd' 7 && not BV8.nth rd 7)

450
451
452
453
454
let inc_ (dst: register): unit
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] + 1)) 256] }
= let rd  = BV8.of_int (Map.get reg.data dst) in
  let rd' = BV8.add rd (BV8.of_int 1) in
455
  reg.data <- Map.set reg.data dst (BV8.t'int rd')
456
457
458
459
460
461
462

let dec_ (dst: register): unit
  writes { reg }
  ensures { reg = old reg[dst <- mod (old (reg[dst] - 1)) 256] }
= let sum = Map.get reg.data dst - 1 in
  reg.data <- Map.set reg.data dst (mod sum 256)

463
464
let eor (dst src: register): unit
  writes { reg }
465
466
  ensures { reg = old reg[dst <- BV8.t'int (BV8.bw_xor (BV8.of_int reg[dst]) (BV8.of_int reg[src])) ] }
= let tmp = BV8.t'int (BV8.bw_xor (BV8.of_int (Map.get reg.data dst)) (BV8.of_int (Map.get reg.data src))) in
467
468
469
470
471
472
473
474
475
  reg.data <- Map.set reg.data dst tmp

let clr (dst: register): unit
  writes { reg }
  ensures { reg = old reg[dst<-0] }
= eor dst dst

let com (dst: register): unit
  writes { reg }
476
477
  ensures { reg = old reg[dst<- BV8.t'int (BV8.bw_not (BV8.of_int reg[dst]))] }
= let tmp = BV8.t'int (BV8.bw_not (BV8.of_int (Map.get reg.data dst))) in
478
479
480
481
  reg.data <- Map.set reg.data dst tmp

let asr (dst: register): unit
  writes { reg, cf }
482
  ensures { reg = old reg[dst<- BV8.t'int (BV8.asr (BV8.of_int reg[dst]) 1)] }
483
  ensures { ?cf = mod (old reg[dst]) 2 }
484
  ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 0 }
485
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
486
  reg.data <- Map.set reg.data dst (BV8.t'int (BV8.asr (BV8.of_int (Map.get reg.data dst)) 1))
487

488
489
490
491
492
493
494
495
let lsr (dst: register): unit
  writes { reg, cf }
  ensures { reg = old reg[dst<- BV8.t'int (BV8.lsr (BV8.of_int reg[dst]) 1)] }
  ensures { ?cf = mod (old reg[dst]) 2 }
  ensures { cf.value = BV8.nth (BV8.of_int (old reg[dst])) 0 }
= cf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) 0;
  reg.data <- Map.set reg.data dst (BV8.t'int (BV8.lsr (BV8.of_int (Map.get reg.data dst)) 1))

496
(* this instruction doesn't physically exist on the AVR, but just maps to 'add rd, rd' *)
497
498
let lsl (dst: register): unit
  writes { reg, cf }
499
500
501
502
503
504
505
506
507
508
  ensures { reg = old reg[dst <- mod (old (2*reg[dst])) 256] }
  ensures { ?cf = div (old (2*reg[dst])) 256 }
= add dst dst

(* this instruction doesn't physically exist on the AVR, but just maps to 'adc rd, rd' *)
let rol (dst: register): unit
  writes { reg, cf }
  ensures { reg = old reg[dst <- mod (old (?cf+2*reg[dst])) 256] }
  ensures { ?cf = div (old (?cf+2*reg[dst])) 256 }
= adc dst dst
509

510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
(* t flag operations *)
val tf: cpu_flag

let bst (dst: register) (bit: int): unit
  writes { tf }
  requires { 0 <= bit < 8 }
  ensures { tf.value = BV8.nth (BV8.of_int reg[dst]) bit }
= tf.value <- BV8.nth (BV8.of_int (Map.get reg.data dst)) bit

function bitset (w: BV8.t) (b: int) (v: bool): BV8.t =
  let mask = BV8.lsl (BV8.of_int 1) b in
  if v then
    BV8.bw_or w mask
  else
    BV8.bw_and w (BV8.bw_not mask)

function bitset' (w: BV8.t) (b: int) (v: bool): BV8.t =
  let v'  = BV8.of_int (if v then 1 else 0) in
  let one = BV8.of_int 1 in
  BV8.bw_or (BV8.bw_and w (BV8.bw_not (BV8.lsl one b))) (BV8.lsl v' b)

function bitsetx (w: BV8.t) (b: int) (v: bool): BV8.t =
  let mask = BV8.lsl (BV8.of_int 1) b in
  if BV8.nth w b = v then
    w
  else
    BV8.bw_xor w mask

538
539
540
541
lemma one_def:
  BV8.nth (BV8.of_int 1) 0 /\ forall b. 0 < b < 8 -> not BV8.nth (BV8.of_int 1) b

goal bitset_correct1:
542
  forall w, b, v. 0 <= b < 8 ->
543
544
545
    BV8.nth (bitset w b v) b = v

goal bitset_correct2:
546
  forall w, b i, v. 0 <= b < 8 -> 0 <= i < 8 -> i <> b ->
547
548
549
550
551
552
553
554
    BV8.nth (bitset w b v) i = BV8.nth w i

goal bitset_equiv_def:
  forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitset' w b v)

goal bitsetx_equiv_def:
  forall w, b, v. 0 <= b < 8 -> BV8.eq (bitset w b v) (bitsetx w b v)

555
556
557
let bld (dst: register) (bit: int): unit
  writes { reg }
  requires { 0 <= bit < 8 }
558
  ensures { reg = (old reg)[dst <- BV8.t'int (bitset (BV8.of_int (old reg)[dst]) bit tf.value)] }
559
560
561
= let rd = BV8.of_int (Map.get reg.data dst) in
  let mask = BV8.lsl (BV8.of_int 1) bit in
  if ?tf = 0 then
562
    reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
563
  else
564
    reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
565

566
(*
567
568
569
let bld' (dst: register) (bit: int): unit
  writes { reg }
  requires { 0 <= bit < 8 }
570
  ensures { reg = (old reg)[dst <- BV8.t'int (bitset' (BV8.of_int (old reg)[dst]) bit tf.value)] }
571
572
573
= let rd = BV8.of_int (Map.get reg.data dst) in
  let mask = BV8.lsl (BV8.of_int 1) bit in
  if ?tf = 0 then
574
    reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
575
  else
576
    reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
577
578
579
580

let bld'' (dst: register) (bit: int): unit
  writes { reg }
  requires { 0 <= bit < 8 }
581
  ensures { reg = (old reg)[dst <- BV8.t'int (bitsetx (BV8.of_int (old reg)[dst]) bit tf.value)] }
582
583
584
= let rd = BV8.of_int (Map.get reg.data dst) in
  let mask = BV8.lsl (BV8.of_int 1) bit in
  if ?tf = 0 then
585
    reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_and rd (BV8.bw_not mask)))
586
  else
587
    reg.data <- Map.set reg.data dst (BV8.t'int (BV8.bw_or rd mask))
588
589
*)

590
591
592
593
594
595
596
597
let rec ghost uint_recursion (reg: address_space) (lo w: int): unit
  requires { w >= 0 }
  ensures { B.sum (reg,lo) 1 w = 256*B.sum (reg,lo+1) 0 (w-1) }
  variant { w }
= assert { forall k. 0 <= k < w-1 -> get_uint_term (reg,lo) (k+1) = 256*get_uint_term (reg,lo+1) k };
  if w > 0 then begin
    uint_recursion reg lo (w-1)
  end
598

599
600
601
602
603
604
605
606
let rec ghost uint_bound (reg: address_space) (lo w: int): unit
  requires { w >= 0 }
  ensures { 0 <= B.sum (reg,lo) 0 w < pow2 (8*w) }
  variant { w }
= if w > 0 then begin
    uint_recursion reg lo w;
    assert { B.sum (reg,lo) 0 w = reg[lo] + 256*B.sum (reg,lo+1) 0 (w-1) };
    uint_bound reg (lo+1) (w-1);
607
608
    (* otherwise Z3 is needed *)
    assert { 256*pow2 (8*(w-1)) = pow2 (8*w) };
609
  end
610

611
612
end

613
module Shadow
614
615
616

use import int.Int
use import ref.Ref
617
618
use import AVRint as AVR
use map.Map
619

620
type shadow_registers = {
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
	ghost r0: ref int;
	ghost r1: ref int;
	ghost r2: ref int;
	ghost r3: ref int;
	ghost r4: ref int;
	ghost r5: ref int;
	ghost r6: ref int;
	ghost r7: ref int;
	ghost r8: ref int;
	ghost r9: ref int;
	ghost r10: ref int;
	ghost r11: ref int;
	ghost r12: ref int;
	ghost r13: ref int;
	ghost r14: ref int;
	ghost r15: ref int;
	ghost r16: ref int;
	ghost r17: ref int;
	ghost r18: ref int;
	ghost r19: ref int;
	ghost r20: ref int;
	ghost r21: ref int;
	ghost r22: ref int;
	ghost r23: ref int;
	ghost r24: ref int;
	ghost r25: ref int;
	ghost r26: ref int;
	ghost r27: ref int;
	ghost r28: ref int;
	ghost r29: ref int;
	ghost r30: ref int;
	ghost r31: ref int
}
654

655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
predicate synchronized (self: shadow_registers) (avr: address_space) =
	avr[0] = !(self.r0) /\
	avr[1] = !(self.r1) /\
	avr[2] = !(self.r2) /\
	avr[3] = !(self.r3) /\
	avr[4] = !(self.r4) /\
	avr[5] = !(self.r5) /\
	avr[6] = !(self.r6) /\
	avr[7] = !(self.r7) /\
	avr[8] = !(self.r8) /\
	avr[9] = !(self.r9) /\
	avr[10] = !(self.r10) /\
	avr[11] = !(self.r11) /\
	avr[12] = !(self.r12) /\
	avr[13] = !(self.r13) /\
	avr[14] = !(self.r14) /\
	avr[15] = !(self.r15) /\
	avr[16] = !(self.r16) /\
	avr[17] = !(self.r17) /\
	avr[18] = !(self.r18) /\
	avr[19] = !(self.r19) /\
	avr[20] = !(self.r20) /\
	avr[21] = !(self.r21) /\
	avr[22] = !(self.r22) /\
	avr[23] = !(self.r23) /\
	avr[24] = !(self.r24) /\
	avr[25] = !(self.r25) /\
	avr[26] = !(self.r26) /\
	avr[27] = !(self.r27) /\
	avr[28] = !(self.r28) /\
	avr[29] = !(self.r29) /\
	avr[30] = !(self.r30) /\
687
	avr[31] = !(self.r31)
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759

val shadow: shadow_registers

let ghost modify_r0 () ensures { !(shadow.r0) = reg[0] } = shadow.r0 := Map.get reg.data 0
let ghost modify_r1 () ensures { !(shadow.r1) = reg[1] } = shadow.r1 := Map.get reg.data 1; ()
let ghost modify_r2 () ensures { !(shadow.r2) = reg[2] } = shadow.r2 := Map.get reg.data 2
let ghost modify_r3 () ensures { !(shadow.r3) = reg[3] } = shadow.r3 := Map.get reg.data 3
let ghost modify_r4 () ensures { !(shadow.r4) = reg[4] } = shadow.r4 := Map.get reg.data 4
let ghost modify_r5 () ensures { !(shadow.r5) = reg[5] } = shadow.r5 := Map.get reg.data 5
let ghost modify_r6 () ensures { !(shadow.r6) = reg[6] } = shadow.r6 := Map.get reg.data 6
let ghost modify_r7 () ensures { !(shadow.r7) = reg[7] } = shadow.r7 := Map.get reg.data 7
let ghost modify_r8 () ensures { !(shadow.r8) = reg[8] } = shadow.r8 := Map.get reg.data 8
let ghost modify_r9 () ensures { !(shadow.r9) = reg[9] } = shadow.r9 := Map.get reg.data 9
let ghost modify_r10 () ensures { !(shadow.r10) = reg[10] } = shadow.r10 := Map.get reg.data 10
let ghost modify_r11 () ensures { !(shadow.r11) = reg[11] } = shadow.r11 := Map.get reg.data 11
let ghost modify_r12 () ensures { !(shadow.r12) = reg[12] } = shadow.r12 := Map.get reg.data 12
let ghost modify_r13 () ensures { !(shadow.r13) = reg[13] } = shadow.r13 := Map.get reg.data 13
let ghost modify_r14 () ensures { !(shadow.r14) = reg[14] } = shadow.r14 := Map.get reg.data 14
let ghost modify_r15 () ensures { !(shadow.r15) = reg[15] } = shadow.r15 := Map.get reg.data 15
let ghost modify_r16 () ensures { !(shadow.r16) = reg[16] } = shadow.r16 := Map.get reg.data 16
let ghost modify_r17 () ensures { !(shadow.r17) = reg[17] } = shadow.r17 := Map.get reg.data 17
let ghost modify_r18 () ensures { !(shadow.r18) = reg[18] } = shadow.r18 := Map.get reg.data 18
let ghost modify_r19 () ensures { !(shadow.r19) = reg[19] } = shadow.r19 := Map.get reg.data 19
let ghost modify_r20 () ensures { !(shadow.r20) = reg[20] } = shadow.r20 := Map.get reg.data 20
let ghost modify_r21 () ensures { !(shadow.r21) = reg[21] } = shadow.r21 := Map.get reg.data 21
let ghost modify_r22 () ensures { !(shadow.r22) = reg[22] } = shadow.r22 := Map.get reg.data 22
let ghost modify_r23 () ensures { !(shadow.r23) = reg[23] } = shadow.r23 := Map.get reg.data 23
let ghost modify_r24 () ensures { !(shadow.r24) = reg[24] } = shadow.r24 := Map.get reg.data 24
let ghost modify_r25 () ensures { !(shadow.r25) = reg[25] } = shadow.r25 := Map.get reg.data 25
let ghost modify_r26 () ensures { !(shadow.r26) = reg[26] } = shadow.r26 := Map.get reg.data 26
let ghost modify_r27 () ensures { !(shadow.r27) = reg[27] } = shadow.r27 := Map.get reg.data 27
let ghost modify_r28 () ensures { !(shadow.r28) = reg[28] } = shadow.r28 := Map.get reg.data 28
let ghost modify_r29 () ensures { !(shadow.r29) = reg[29] } = shadow.r29 := Map.get reg.data 29
let ghost modify_r30 () ensures { !(shadow.r30) = reg[30] } = shadow.r30 := Map.get reg.data 30
let ghost modify_r31 () ensures { !(shadow.r31) = reg[31] } = shadow.r31 := Map.get reg.data 31

let ghost init() ensures { synchronized shadow reg } =
  modify_r0 ();
  modify_r1 ();
  modify_r2 ();
  modify_r3 ();
  modify_r4 ();
  modify_r5 ();
  modify_r6 ();
  modify_r7 ();
  modify_r8 ();
  modify_r9 ();
  modify_r10 ();
  modify_r11 ();
  modify_r12 ();
  modify_r13 ();
  modify_r14 ();
  modify_r15 ();
  modify_r16 ();
  modify_r17 ();
  modify_r18 ();
  modify_r19 ();
  modify_r20 ();
  modify_r21 ();
  modify_r22 ();
  modify_r23 ();
  modify_r24 ();
  modify_r25 ();
  modify_r26 ();
  modify_r27 ();
  modify_r28 ();
  modify_r29 ();
  modify_r30 ();
  modify_r31 ();
  ()

end