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
|
(in-package "ACL2")
; generate-index-list.lisp Mihir Mehta
;; If one's going to append some blocks at the end of the disk, one needs to
;; generate the indices for those blocks - that's what this function does.
(defun
generate-index-list
(disk-length block-list-length)
(declare (xargs :guard (and (natp disk-length)
(natp block-list-length))))
(if (zp block-list-length)
nil
(cons (nfix disk-length)
(generate-index-list (1+ disk-length)
(1- block-list-length)))))
(defthm
generate-index-list-correctness-1
(nat-listp
(generate-index-list disk-length block-list-length)))
(defthm
generate-index-list-correctness-2
(equal
(len (generate-index-list disk-length block-list-length))
(nfix block-list-length)))
(defthm
member-of-generate-index-list
(iff (member-equal
x
(generate-index-list disk-length block-list-length))
(or (and (equal x 0)
(zp disk-length)
(not (zp block-list-length)))
(and (integerp x)
(>= x (nfix disk-length))
(< x
(nfix (+ disk-length
(nfix block-list-length))))))))
(defthm remove-when-absent
(implies (not (member-equal x l))
(equal (remove-equal x l)
(true-list-fix l))))
(defthm len-of-true-list-fix
(equal (len (true-list-fix x)) (len x)))
(defthm
generate-index-list-correctness-4
(implies
(and (integerp x)
(natp disk-length)
(>= x disk-length)
(< x
(+ disk-length (nfix block-list-length))))
(equal
(len
(remove-equal
x
(generate-index-list disk-length block-list-length)))
(- (nfix block-list-length) 1))))
|
