blob: f3dc594d99e9c0b1d245fa1b13951d429f35f33f (
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
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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
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
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
;;; memory-low.lisp
;;;
;;; Uses memory-acl2 (potentially, memory-raw) to set up a model of
;;; the X86's physical address 32-bit memory system. Addresses are
;;; (assumed to be) 32-bit, values are (assumed to
;;; be) 32-bit.
;;;
;;; From work by Warren Hunt and/or Alan Dunn.
;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "../Utilities/bytes-and-words")
(include-book "../Utilities/disjoint")
(include-book "memory-acl2")
;;; uncomment to get Alan's fast and raw memory
;;;(include-book "memory-raw" :ttags (memory)) ; must be included second
(local
(include-book "arithmetic-5/top" :dir :system))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Basic definitions
(defun r08-low (addr mem)
(declare (xargs :guard t))
(read-mem-byte addr mem))
(defun w08-low (addr val mem)
(declare (xargs :guard (integerp addr)))
(write-mem-byte addr val mem))
(defun r32-low (addr mem)
;; We prove equivalence with a simpler definition below, given our
;; assumptions about addresses.
(declare (xargs :guard (integerp addr)))
(let ((byte0 (ifix (read-mem-byte addr mem)))
(byte1 (ifix (read-mem-byte (n32+ 1 addr) mem)))
(byte2 (ifix (read-mem-byte (n32+ 2 addr) mem)))
(byte3 (ifix (read-mem-byte (n32+ 3 addr) mem))))
(n32+ (ash byte3 24)
(n32+ (ash byte2 16)
(n32+ (ash byte1 8)
byte0)))))
(defun w32-low (addr val mem)
;; We prove equivalence with a simpler definition below, given our
;; assumptions about addresses and values.
(declare (xargs :guard (and (integerp addr)
(integerp val))))
(let ((byte0 (n08 val))
(byte1 (n08 (ash val -8)))
(byte2 (n08 (ash val -16)))
(byte3 (n08 (ash val -24))))
(let* ((mem (write-mem-byte addr byte0 mem))
(mem (write-mem-byte (n32+ 1 addr) byte1 mem))
(mem (write-mem-byte (n32+ 2 addr) byte2 mem))
(mem (write-mem-byte (n32+ 3 addr) byte3 mem)))
mem)))
(local
(defthm crock-1
(and (implies (and (n08p n1)
(n08p n2))
(n32p (+ n1
(* 256
n2))))
(implies (and (n08p n1)
(n08p n2)
(n08p n3))
(n32p (+ n1
(* 256
n2)
(* 65536
n3))))
(implies (and (n08p n1)
(n08p n2)
(n08p n3)
(n08p n4))
(n32p (+ n1
(* 256
n2)
(* 65536
n3)
(* 16777216
n4)))))))
(defthm r32-low-alt-def
(implies (and (n32p addr)
(n32p (+ 3 addr))
(memoryp mem))
(equal (r32-low addr mem)
(let ((byte0 (read-mem-byte addr mem))
(byte1 (read-mem-byte (+ 1 addr) mem))
(byte2 (read-mem-byte (+ 2 addr) mem))
(byte3 (read-mem-byte (+ 3 addr) mem)))
(+ (ash byte3 24)
(+ (ash byte2 16)
(+ (ash byte1 8)
byte0))))))
:rule-classes :definition)
(defthm w32-low-alt-def
(implies (and (n32p addr)
(n32p (+ 3 addr))
(memoryp mem))
(equal (w32-low addr val mem)
(let ((byte0 (n08 val))
(byte1 (n08 (ash val -8)))
(byte2 (n08 (ash val -16)))
(byte3 (n08 (ash val -24))))
(let* ((mem (write-mem-byte addr byte0 mem))
(mem (write-mem-byte (+ 1 addr) byte1 mem))
(mem (write-mem-byte (+ 2 addr) byte2 mem))
(mem (write-mem-byte (+ 3 addr) byte3 mem)))
mem))))
:rule-classes :definition)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Some theorems
(defthm r32-low-from-four-r08-low
(implies (and (n32p addr)
(n32p (+ 3 addr))
(memoryp mem)
(equal (r08-low addr mem) byte0)
(equal (r08-low (+ 1 addr) mem) byte1)
(equal (r08-low (+ 2 addr) mem) byte2)
(equal (r08-low (+ 3 addr) mem) byte3))
(equal (r32-low addr mem)
(+ (ash byte3 24)
(+ (ash byte2 16)
(+ (ash byte1 8)
byte0))))))
(in-theory (disable r32-low-from-four-r08-low))
;;; Note that I do not have any rules about reads/writes or
;;; writes/writes that intersect but do not overlap completely. What
;;; should I do about these? Perhaps this is an argument for some
;;; kind of read-bytes and write-bytes that also specify how many
;;; bytes to read or write.
(defthm |(n08p (r08-low addr mem))|
(implies (memoryp mem)
(n08p (r08-low addr mem)))
:rule-classes ((:rewrite)
(:type-prescription
:corollary
(implies (memoryp mem)
(and (integerp (r08-low addr mem))
(<= 0 (r08-low addr mem)))))))
(defthm |(n32p (r32-low addr mem))|
(implies (memoryp mem)
(n32p (r32-low addr mem)))
:rule-classes ((:rewrite)
(:type-prescription
:corollary
(implies (memoryp mem)
(and (integerp (r32-low addr mem))
(<= 0 (r32-low addr mem))))))
:hints (("Goal" :in-theory (e/d ()
(ash)
))))
(defthm |(memoryp (w08-low addr val mem))|
(implies (and (n32p addr)
(n08p val)
(memoryp mem))
(memoryp (w08-low addr val mem))))
(defthm |(memoryp (w32-low addr val mem))|
(implies (and (n32p addr)
(n32p val)
(memoryp mem))
(memoryp (w32-low addr val mem)))
:hints (("Goal" :in-theory (e/d ()
(ash)
))))
(defthm |(r08-low addr (w08-low addr val mem))|
(equal (r08-low addr (w08-low addr val mem))
val))
(defthm |(r08-low addr1 (w08-low addr2 val mem))|
(implies (disjointp (list (list addr1)
(list addr2)))
(equal (r08-low addr1 (w08-low addr2 val mem))
(r08-low addr1 mem)))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|))))
(defthm |(r08-low addr1 (w32-low addr2 val mem))|
(implies (and (n32p addr1)
(n32p addr2)
(n32p (+ 3 addr2))
(disjointp (list (list addr1)
(range addr2 0 4))))
(equal (r08-low addr1 (w32-low addr2 val mem))
(r08-low addr1 mem)))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|))))
(defthm |(w08-low addr val1 (w08-low addr val2 mem))|
(equal (w08-low addr val1 (w08-low addr val2 mem))
(w08-low addr val1 mem)))
(defthm |(w08-low addr1 val1 (w08-low addr2 val2 mem))|
(implies (and (integerp addr1)
(integerp addr2)
(disjointp (list (list addr1)
(list addr2))))
(equal (w08-low addr1 val1 (w08-low addr2 val2 mem))
(w08-low addr2 val2 (w08-low addr1 val1 mem))))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|)))
:rule-classes ((:rewrite :loop-stopper ((addr1 addr2)))))
(defthm |(r32-low addr1 (w08-low addr2 val mem))|
(implies (and (n32p addr1)
(n32p (+ 3 addr1))
(n32p addr2)
(disjointp (list (range addr1 0 4)
(list addr2))))
(equal (r32-low addr1 (w08-low addr2 val mem))
(r32-low addr1 mem)))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|))))
(encapsulate
()
(local
(defthm crock-2
(implies (n32p x)
(n08p (floor x 16777216)))))
(local
(defthm crock-3
(implies (n32p val)
(EQUAL (+ (N08 VAL)
(* 16777216 (FLOOR VAL 16777216))
(* 256 (N08 (FLOOR VAL 256)))
(* 65536 (N08 (FLOOR VAL 65536))))
VAL))
:hints (("Goal" :in-theory (enable n08)))))
(defthm |(r32-low addr (w32-low addr val mem))|
(implies (and (n32p addr)
(n32p (+ 3 addr))
(n32p val))
(equal (r32-low addr (w32-low addr val mem))
val))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|))))
)
(defthm |(r32-low addr1 (w32-low addr2 val mem))|
(implies (and (n32p addr1)
(n32p (+ 3 addr1))
(n32p addr2)
(n32p (+ 3 addr2))
(disjointp (list (range addr1 0 4)
(range addr2 0 4))))
(equal (r32-low addr1 (w32-low addr2 val mem))
(r32-low addr1 mem)))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|))))
;;; We push w32's inside w08's
;;; I think this is the proper way if we ever worry about overlapping
;;; reads and writes.
(defthm |(w32-low addr1 val1 (w08-low addr2 val2 mem))|
(implies (and (n32p addr1)
(n32p (+ 3 addr1))
(n32p addr2)
(disjointp (list (range addr1 0 4)
(list addr2))))
(equal (w32-low addr1 val1 (w08-low addr2 val2 mem))
(w08-low addr2 val2 (w32-low addr1 val1 mem))))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|))))
(defthm |(w32-low addr val1 (w32-low addr val2 mem))|
(implies (and (n32p addr)
(n32p (+ 3 addr)))
(equal (w32-low addr val1 (w32-low addr val2 mem))
(w32-low addr val1 mem))))
(defthm |(w32-low addr1 val1 (w32-low addr2 val2 mem))|
(implies (and (n32p addr1)
(n32p (+ 3 addr1))
(n32p addr2)
(n32p (+ 3 addr2))
(disjointp (list (range addr1 0 4)
(range addr2 0 4))))
(equal (w32-low addr1 val1 (w32-low addr2 val2 mem))
(w32-low addr2 val2 (w32-low addr1 val1 mem))))
:rule-classes ((:rewrite :loop-stopper ((addr1 addr2))))
:hints (("Goal" :in-theory (enable |(not (equal x y)) --- disjointp|))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-theory (disable r08-low
w08-low
r32-low
w32-low
r32-low-alt-def
w32-low-alt-def))
|
