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
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
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
384
385
386
387
388
389
|
(in-package "ACL2")
(include-book "lofat-syscalls")
(include-book "centaur/getopt/top" :dir :system)
(defoptions mkdir-opts
:parents (demo2)
:tag :demo2
((parents "no error if existing, make parent directories as needed"
booleanp
:rule-classes :type-prescription
:alias #\p)))
(defun mkdir-list (fs name-list exit-status)
(b*
(((when (atom name-list))
(mv fs exit-status))
(fat32-path
(path-to-fat32-path (coerce (car name-list) 'list)))
;; It doesn't really matter for these purposes what the errno is. We're
;; not trying to match this program for its stderr output.
((mv fs retval &)
(hifat-mkdir fs fat32-path))
(exit-status (if (equal retval 0) exit-status 1)))
(mkdir-list fs (cdr name-list) exit-status)))
(defoptions rm-opts
:parents (demo2)
:tag :demo2
((recursive "Recursively delete a directory"
booleanp
:rule-classes :type-prescription
:alias #\r)))
(defun
rm-list (fat32$c name-list exit-status)
(declare (xargs :stobjs fat32$c
:guard (and (lofat-fs-p fat32$c)
(string-listp name-list))))
(b* (((when (atom name-list))
(mv fat32$c exit-status))
(fat32-path (path-to-fat32-path
(coerce (car name-list) 'list)))
((mv fat32$c retval &)
(if (not (fat32-filename-list-p fat32-path))
(mv fat32$c 1 *enoent*)
(lofat-unlink fat32$c fat32-path)))
(exit-status (if (equal retval 0) exit-status 1)))
(rm-list fat32$c (cdr name-list) exit-status)))
(defthm
lofat-fs-p-of-rm-list
(implies
(and (lofat-fs-p fat32$c))
(lofat-fs-p (mv-nth 0
(rm-list fat32$c
name-list exit-status)))))
(defund
rm-1
(fat32$c disk-image-string rm-paths)
(declare (xargs :guard (and (lofat-fs-p fat32$c)
(string-listp rm-paths)
(stringp disk-image-string)
(>= (length disk-image-string) *initialbytcnt*))
:stobjs fat32$c))
(b* (((mv fat32$c error-code)
(string-to-lofat fat32$c disk-image-string))
((unless (equal error-code 0))
(mv fat32$c disk-image-string 1))
((mv fat32$c exit-status)
(rm-list fat32$c rm-paths 0))
(disk-image-string (lofat-to-string fat32$c)))
(mv fat32$c disk-image-string exit-status)))
(defthm
rm-2-guard-lemma-1
(implies
(not (equal (mv-nth 1 (rm-list fs name-list exit-status))
exit-status))
(equal (mv-nth 1 (rm-list fs name-list exit-status))
1)))
(defun rm-2 (fat32$c state disk-path output-path rm-paths)
(declare (xargs :stobjs (state fat32$c)
:guard (and (fat32$c-p fat32$c)
(string-listp rm-paths)
(stringp disk-path)
(stringp output-path)
(state-p state))
:guard-hints (("Goal" :in-theory (e/d (rm-1)
(read-file-into-string2))))))
(mbe :logic
(b*
((disk-image-string (read-file-into-string disk-path))
((mv fat32$c disk-image-string exit-status)
(rm-1 fat32$c disk-image-string rm-paths))
((unless (equal exit-status 0)) (mv fat32$c state 1))
((mv channel state)
(open-output-channel output-path
:character state))
((when (null channel)) (mv fat32$c state 1))
(state
(princ$ disk-image-string channel state))
(state (close-output-channel channel state)))
(mv fat32$c state exit-status))
:exec
(b*
(((mv fat32$c error-code)
(disk-image-to-lofat
fat32$c disk-path state))
((unless (equal error-code 0))
(mv fat32$c state 1))
((mv fat32$c exit-status)
(rm-list fat32$c rm-paths 0))
((unless (equal exit-status 0)) (mv fat32$c state 1))
((mv state error-code)
(lofat-to-disk-image
fat32$c output-path state))
(exit-status (if (equal error-code 0) exit-status 1)))
(mv fat32$c state exit-status))))
(defoptions rmdir-opts
:parents (demo2)
:tag :demo2
((parents "no error if existing, make parent directories as needed"
booleanp
:rule-classes :type-prescription
:alias #\p)))
(defun rmdir-list (fs name-list exit-status)
(b*
(((when (atom name-list))
(mv fs exit-status))
(fat32-path
(path-to-fat32-path (coerce (car name-list) 'list)))
;; It doesn't really matter for these purposes what the errno is. We're
;; not trying to match this program for its stderr output.
((mv fs retval &)
(hifat-rmdir fs fat32-path))
(exit-status (if (equal retval 0) exit-status 1)))
(rmdir-list fs (cdr name-list) exit-status)))
(defoptions wc-opts
:parents (demo2)
:tag :demo2
((bytes "Count bytes"
booleanp
:rule-classes :type-prescription
:alias #\c)
(lines "Count lines"
booleanp
:rule-classes :type-prescription
:alias #\l)
(words "Count words"
booleanp
:rule-classes :type-prescription
:alias #\w)))
(defun
wc-helper
(text nl nw nc beginning-of-word-p pos)
(declare (xargs :measure (nfix (- (length text) pos))
:guard (and (stringp text)
(natp pos)
(natp nc)
(natp nw)
(natp nl)
(<= pos (length text)))))
(if (zp (- (length text) pos))
(mv nl nw nc)
(b* ((c (char text pos))
(nc (+ nc 1))
(nl (if (equal c #\newline) (+ nl 1) nl))
((mv beginning-of-word-p nw)
(if (or (equal c #\space)
(equal c #\newline)
(equal c #\tab))
(mv t nw)
(if beginning-of-word-p (mv nil (+ nw 1))
(mv beginning-of-word-p nw)))))
(wc-helper text nl
nw nc beginning-of-word-p (+ pos 1)))))
(defthm
wc-helper-correctness-1
(implies (and (integerp pos)
(<= pos (length text))
(integerp nc))
(equal (mv-nth 2
(wc-helper text nl nw nc beginning-of-word-p pos))
(+ nc (length text) (- pos)))))
(defund wc-1 (fat32$c path)
(declare
(xargs
:stobjs fat32$c
:guard (and (stringp path)
(lofat-fs-p fat32$c))
:guard-hints
(("goal" :in-theory
(enable lofat-open lofat-lstat hifat-open)))))
(b*
((fat32-path (path-to-fat32-path (coerce path 'list)))
;; It would be nice to eliminate this check by proving a theorem, but
;; it's not at all simple to ensure that a string given to us is free of
;; filenames indicating deleted files and such which are not allowed in
;; a path satisfying fat32-filename-list-p.
((unless (fat32-filename-list-p fat32-path))
(mv 0 0 0 1))
((mv val error-code &)
(lofat-lstat fat32$c fat32-path))
((unless (equal error-code 0))
(mv 0 0 0 error-code))
(file-length (struct-stat->st_size val))
((mv fd-table file-table fd &)
(lofat-open fat32-path nil nil))
((mv file-text file-read-length &)
(lofat-pread
fd file-length 0 fat32$c fd-table file-table))
((unless (equal file-read-length file-length))
(mv 0 0 0 1))
((mv nl nw nc)
(wc-helper file-text 0 0 0 t 0)))
(mv nl nw nc 0)))
(defoptions ls-opts
:parents (demo2)
:tag :demo2
((directory "Recursively delete a directory"
booleanp
:rule-classes :type-prescription
:alias #\d)))
(defun ls-list (fat32$c name-list exit-status)
(declare (xargs :stobjs fat32$c
:guard (and
(lofat-fs-p fat32$c) (string-listp name-list))))
(b*
(((when (atom name-list)) (mv nil exit-status))
(fat32-path
(path-to-fat32-path (coerce (car name-list) 'list)))
;; It doesn't really matter for these purposes what the errno is. We're
;; not trying to match this program for its stderr output.
((unless
(fat32-filename-list-p fat32-path))
(ls-list fat32$c (cdr name-list) 2))
((mv & retval &)
(lofat-lstat fat32$c fat32-path))
((unless (equal retval 0))
(ls-list fat32$c (cdr name-list) 2))
((mv tail-list exit-status) (ls-list fat32$c (cdr name-list) exit-status)))
(mv (cons (car name-list) tail-list) exit-status)))
(defund
ls-1
(fat32$c ls-paths disk-image-string)
(declare (xargs :guard (and (lofat-fs-p fat32$c)
(string-listp ls-paths)
(stringp disk-image-string)
(>= (length disk-image-string)
*initialbytcnt*))
:stobjs fat32$c))
(b* (((mv fat32$c error-code)
(string-to-lofat fat32$c disk-image-string))
((unless (equal error-code 0))
(mv fat32$c nil 2))
((mv ls-list exit-status)
(ls-list fat32$c ls-paths 0)))
(mv fat32$c ls-list exit-status)))
(defun
ls-2
(fat32$c state ls-paths disk-path)
(declare
(xargs :stobjs (state fat32$c)
:guard (and (fat32$c-p fat32$c)
(state-p state)
(string-listp ls-paths)
(stringp disk-path))
:guard-hints
(("goal" :in-theory (e/d (ls-1)
(read-file-into-string2))))))
(mbe
:logic
(b* ((disk-image-string (read-file-into-string disk-path))
((mv fat32$c ls-list exit-status)
(ls-1 fat32$c
ls-paths disk-image-string)))
(mv fat32$c ls-list exit-status))
:exec
(b* (((mv fat32$c error-code)
(disk-image-to-lofat fat32$c disk-path state))
((unless (equal error-code 0))
(mv fat32$c nil 2))
((mv ls-list exit-status)
(ls-list fat32$c ls-paths 0)))
(mv fat32$c ls-list exit-status))))
(defoptions truncate-opts
:parents (demo2)
:tag :demo2
((size "set or adjust the file size by SIZE bytes"
natp
:rule-classes :type-prescription
:alias #\s
:default 0)))
(defun
truncate-list (fat32$c name-list size exit-status)
(declare (xargs :stobjs fat32$c
:guard (and (lofat-fs-p fat32$c)
(string-listp name-list)
(natp size))))
(b* (((when (atom name-list))
(mv fat32$c exit-status))
(fat32-path (path-to-fat32-path
(coerce (car name-list) 'list)))
((mv fat32$c retval &)
(if (not (fat32-filename-list-p fat32-path))
(mv fat32$c 1 *enoent*)
(lofat-truncate fat32$c fat32-path size)))
(exit-status (if (equal retval 0) exit-status 1)))
(truncate-list fat32$c (cdr name-list) size exit-status)))
(defun compare-disks (image-path1 image-path2 fat32$c state)
(declare (xargs :stobjs (fat32$c state)
:guard (and (fat32$c-p fat32$c)
(stringp image-path1)
(stringp image-path2))
:guard-hints (("Goal" :in-theory (disable
read-file-into-string2)))))
(b*
(((mv fat32$c error-code1)
(disk-image-to-lofat
fat32$c image-path1 state))
((mv fs-ref error-code2)
(if
(not (equal error-code1 0))
(mv nil *EIO*)
(lofat-to-hifat fat32$c)))
((mv fat32$c error-code3)
(disk-image-to-lofat
fat32$c image-path2 state))
((mv fs error-code4)
(if
(or (not (equal error-code1 0)) (not (equal error-code3 0)))
(mv nil *EIO*)
(lofat-to-hifat fat32$c)))
((unless (or (equal error-code1 0) (equal error-code3 0)))
(mv t fat32$c))
((unless (and (equal error-code1 0) (equal error-code3 0)))
(mv nil fat32$c))
((unless (or (equal error-code2 0) (equal error-code4 0)))
(mv t fat32$c))
((unless (and (equal error-code2 0) (equal error-code4 0)))
(mv nil fat32$c))
((unless (hifat-equiv fs-ref fs))
(mv nil fat32$c)))
(mv t fat32$c)))
(defthm
compare-disks-correctness-1-lemma-1
(implies
(not (stringp str))
(not (equal (mv-nth 1 (string-to-lofat-nx str))
0)))
:hints (("goal" :in-theory (enable string-to-lofat string-to-lofat-nx))))
(defthm
compare-disks-correctness-1
(let*
((str1 (read-file-into-string image-path1))
(str2 (read-file-into-string image-path2)))
(implies
(fat32$c-p fat32$c)
(equal
(mv-nth 0
(compare-disks image-path1
image-path2 fat32$c state))
(eqfat str1 str2))))
:hints
(("goal"
:in-theory
(e/d (eqfat string-to-lofat-ignore-lemma-14
lofat-equiv)
(read-file-into-string2 (:e string-to-lofat-nx)))
:expand (hide (string-to-lofat-nx nil)))))
|
