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
|
(in-package "ACL2")
(include-book "bcv-model")
(include-book "bcv-simple-model")
(include-book "generic")
(local (encapsulate ()
(local (include-book "bcv-find-correct-witness-bcv-check-pre"))
(defthm collect-pc-merged-code-merged-code-1
(implies (and (merged-code-safe merged-code init-frame)
(case-split (not (equal init-frame 'aftergoto))))
(equal (car (collect-pc-merged-code merged-code))
(g 'pc init-frame)))
:rule-classes :linear)
;; (defthm collect-pc-merged-code-merged-code-2
;; (implies (and (merged-code-safe merged-code init-frame)
;; (wff-code1 (extract-code merged-code)
;; (g 'pc (car merged-code))))
;; (equal (car (collect-pc-merged-code merged-code))
;; (g 'pc (car merged-code))))
;; :rule-classes :linear)
;; (defthm wff-code1-uniqueness
;; (IMPLIES
;; (AND (WFF-CODE1 (EXTRACT-CODE MERGED-CODE4) any)
;; (MERGED-CODE-SAFE MERGED-CODE4 MERGED-CODE3))
;; (wff-code1 (extract-code merged-code4)
;; (g 'pc (car merged-code4))))
;; :rule-classes :forward-chaining)
(encapsulate ()
(local (include-book "bcv-find-correct-witness-bcv-check-pre"))
(defthm merged-code-safe-implies-extract-code-pc-is-same-strong-linear
(implies (merged-code-safe merged-code sig-frame)
(equal (g 'pc (car (extract-code merged-code)))
(g 'pc (car merged-code))))
:rule-classes :linear))
(defthm wff-code1-implies-pc-less
(implies (and (wff-code1 code (+ 1 pc))
(consp code))
(< pc (g 'pc (car code))))
:rule-classes :forward-chaining)
(defthm merged-code-safe-implies-pc-less-than
(implies (and (WFF-CODE1 (EXTRACT-CODE MERGED-CODE)
(+ 1 pc))
(consp (extract-code merged-code))
(merged-code-safe merged-code sig-frame))
(< pc
(g 'pc (car merged-code))))
:hints (("Goal" :do-not-induct t
:in-theory (disable wff-code1
extract-code
merged-code-safe)
:use ((:instance wff-code1-implies-pc-less
(code (extract-code merged-code))))))
:rule-classes :linear)
;;
;; not necessary!
(defthm merged-code-safe-stack-map-implies-consp-extract-code
(implies (and (merged-code-safe merged-code init-frame)
(stack-map? init-frame))
(consp (extract-code merged-code)))
:rule-classes :forward-chaining)
(encapsulate ()
(local
(defthm get-is-stack-map-sig-frame-pop-n
(equal (g 'is-stack-map (sig-frame-pop-n n sig-frame))
(g 'is-stack-map sig-frame))))
(local
(defthm get-is-inst-sig-frame-pop-n
(equal (g 'is-inst (sig-frame-pop-n n sig-frame))
(g 'is-inst sig-frame))))
(local
(defthm get-pc-sig-frame-pop-n
(equal (g 'pc (sig-frame-pop-n n sig-frame))
(g 'pc sig-frame))))
(defthm bcv-execute-step-produce-stack-map-or-aftergoto
(implies (and (stack-map? stack-map)
(bcv-check-step-pre inst stack-map)
(not (stack-map? (bcv-execute-step inst stack-map))))
(equal (bcv-execute-step inst stack-map) 'aftergoto))))
(defthm merged-code-is-safe-implies-ordered-lemma
(implies (and (merged-code-safe merged-code init-frame)
(consp (extract-code merged-code))
(wff-code1 (extract-code merged-code)
(g 'pc (car merged-code))))
(ordered (collect-pc-merged-code merged-code)))
:hints (("Goal" :in-theory (disable sig-frame-compatible
bcv-check-step-pre
bcv-execute-step
inst? stack-map?)
:do-not '(generalize fertilize))))
;----------------------------------------------------------------------
(defthm collect-pc-merged-code-merged-code-3
(implies (and (merged-code-safe merged-code init-frame)
(not (consp (extract-code merged-code))))
(equal (car (collect-pc-merged-code merged-code))
(g 'pc init-frame)))
:rule-classes :linear)
(defthm collect-pc-merged-code-merged-code-4
(implies (and (merged-code-safe merged-code init-frame)
(not (consp (extract-code merged-code))))
(ordered (collect-pc-merged-code merged-code))))
;----------------------------------------------------------------------
(defthm merged-code-is-safe-implies-ordered
(implies (and (merged-code-safe merged-code init-frame)
(wff-code1 (extract-code merged-code)
(g 'pc (car merged-code))))
(ordered (collect-pc-merged-code merged-code)))
:hints (("Goal" :in-theory (disable sig-frame-compatible
bcv-check-step-pre
bcv-execute-step
inst? stack-map?)
:do-not '(generalize fertilize)
:cases ((consp (extract-code merged-code))))))
))
;----------------------------------------------------------------------
(defthm merged-code-is-safe-implies-ordered
(implies (and (merged-code-safe merged-code init-frame)
(wff-code1 (extract-code merged-code)
(g 'pc (car merged-code))))
(ordered (collect-pc-merged-code merged-code)))
:hints (("Goal" :in-theory (disable sig-frame-compatible
bcv-check-step-pre
bcv-execute-step
inst? stack-map?)
:do-not '(generalize fertilize)
:cases ((consp (extract-code merged-code))))))
;----------------------------------------------------------------------
(defthm merged-code-safe-implies-pc-less-than
(implies (and (WFF-CODE1 (EXTRACT-CODE MERGED-CODE)
(+ 1 pc))
(consp (extract-code merged-code))
(merged-code-safe merged-code sig-frame))
(< pc
(g 'pc (car merged-code))))
:rule-classes :linear)
(defthm merged-code-safe-stack-map-implies-consp-extract-code
(implies (and (merged-code-safe merged-code init-frame)
(stack-map? init-frame))
(consp (extract-code merged-code)))
:rule-classes :forward-chaining)
|
