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
|
(in-package "ACL2")
; cluster-listp.lisp Mihir Mehta
; Here we define some utility functions and related lemmas for a string
; representation of FAT32 clusters.
(local (include-book "../file-system-lemmas"))
(include-book "kestrel/utilities/strings/top" :dir :system)
(local (in-theory (disable make-list-ac-removal)))
;; These books were suggested by proof-by-arith.
(local (include-book "arithmetic-5/top" :dir :system))
(set-default-hints '((nonlinearp-default-hint++
id
stable-under-simplificationp hist nil)))
(defund cluster-p (cluster cluster-size)
(declare (xargs :guard t))
(and (stringp cluster)
(equal (length cluster) cluster-size)))
(defthm cluster-p-of-implode
(iff (cluster-p (implode x) cluster-size)
(equal (len x) cluster-size))
:hints (("goal" :in-theory (enable cluster-p))))
(defthm
cluster-p-correctness-1
(implies (not (stringp v))
(not (cluster-p v cluster-size)))
:hints (("goal" :in-theory (enable cluster-p))))
(defun cluster-listp (l cluster-size)
(declare (xargs :guard t))
(if
(atom l)
(equal l nil)
(and (cluster-p (car l) cluster-size)
(cluster-listp (cdr l) cluster-size))))
(defthm
cluster-listp-of-update-nth
(implies (cluster-listp l cluster-size)
(equal (cluster-listp (update-nth key val l)
cluster-size)
(and (<= (nfix key) (len l))
(cluster-p val cluster-size))))
:hints (("goal" :induct (mv (update-nth key val l)
(cluster-listp l cluster-size))
:in-theory (enable cluster-p update-nth))))
(defthm cluster-p-of-nth
(implies (cluster-listp l cluster-size)
(iff (cluster-p (nth n l) cluster-size)
(< (nfix n) (len l))))
:hints (("goal" :induct (nth n l)
:in-theory (enable cluster-p nth))))
(defthm cluster-listp-of-append
(equal (cluster-listp (append x y)
cluster-size)
(and (cluster-listp (true-list-fix x)
cluster-size)
(cluster-listp y cluster-size))))
(defthm
cluster-listp-of-resize-list
(implies (and (cluster-listp lst cluster-size)
(<= (nfix n) (len lst)))
(cluster-listp (resize-list lst n default-value)
cluster-size)))
(defund
make-clusters (text cluster-size)
(declare
(xargs :guard (and (stringp text) (natp cluster-size))
:measure (length text)))
(if
(or (zp (length text))
(zp cluster-size))
nil
(list*
(concatenate
'string
(subseq text 0 (min cluster-size (length text)))
(coerce (make-list (nfix (- cluster-size (length text)))
:initial-element (code-char 0))
'string))
(make-clusters
(subseq text (min cluster-size (length text))
nil)
cluster-size))))
(defthmd
make-clusters-correctness-1
(iff (consp (make-clusters text cluster-size))
(and (not (zp (length text)))
(not (zp cluster-size))))
:hints (("goal" :in-theory (enable make-clusters)))
:rule-classes
(:rewrite
(:rewrite
:corollary
(iff (equal (len (make-clusters text cluster-size))
0)
(or (zp (length text)) (zp cluster-size)))
:hints
(("goal"
:expand (len (make-clusters text cluster-size)))))))
(in-theory (enable (:rewrite make-clusters-correctness-1 . 2)))
(defthm
cluster-listp-of-make-clusters
(implies (stringp text)
(cluster-listp (make-clusters text cluster-size)
cluster-size))
:hints
(("goal"
:in-theory (enable cluster-listp
make-clusters make-list-ac-removal)))
:rule-classes
(:rewrite
(:rewrite
:corollary
(implies
(stringp text)
(let ((l (make-clusters text cluster-size)))
(implies (consp l)
(and (cluster-p (car l) cluster-size)
(cluster-listp (cdr l)
cluster-size))))))))
(defthm
make-clusters-correctness-2
(implies (not (zp cluster-size))
(and (>= (* cluster-size
(len (make-clusters text cluster-size)))
(length text))
(< (* cluster-size
(len (make-clusters text cluster-size)))
(+ cluster-size (length text)))))
:rule-classes :linear
:hints (("goal" :in-theory (enable make-clusters))))
(defthmd
len-of-make-clusters
(implies (not (zp cluster-size))
(equal (len (make-clusters text cluster-size))
(ceiling (length text) cluster-size)))
:hints (("goal" :in-theory (enable make-clusters))))
(defthm
make-clusters-correctness-3
(implies (and (stringp text)
(not (zp cluster-size))
(<= (length text) max-length)
(equal (mod max-length cluster-size) 0))
(<= (* cluster-size
(len (make-clusters text cluster-size)))
max-length))
:rule-classes :linear
:hints (("goal" :in-theory (disable make-clusters-correctness-2)
:use len-of-make-clusters)))
(defthm make-clusters-of-nil
(implies (and (atom text) (not (stringp text)))
(equal (make-clusters text cluster-size)
nil))
:hints (("goal" :in-theory (enable make-clusters)))
:rule-classes :type-prescription)
|
