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
|
(in-package "ACL2")
(include-book "jvm-model")
(include-book "bcv-simple-model")
;; (defun pc-in-range (frame method-table)
;; (let* ((method-name (g 'method-name frame))
;; (method (binding method-name method-table))
;; (pc (g 'pc frame))
;; (code (g 'code method)))
;; (and (integerp pc)
;; (<= 0 pc)
;; (< pc (len code)))))
(local (in-theory (disable bcv-simple-method bcv-simple-inst
BCV-CHECK-STEP-PRE
ALL-NEXT-STATE-SAFE
bcv-simple-execute-step)))
(local (include-book "arithmetic/top-with-meta" :dir :system))
(local
(defthm bcv-simple-method1-implies-inst-verified
(implies (and (bcv-simple-method1 i code sig-vector)
(integerp i)
(integerp pc)
(<= 0 (- pc i))
(< (- pc i) (len code)))
(bcv-simple-inst pc
(nth (- pc i) code)
sig-vector))
:hints (("Goal" :in-theory (enable bcv-simple-inst bcv-simple-method1)
:do-not '(generalize)))))
(defthm bcv-simple-method-implies-next-inst-verified
(implies (and (bcv-simple-method method method-table)
(integerp pc)
(<= 0 pc)
(< pc (len (g 'code method))))
(bcv-simple-inst pc
(nth pc (g 'code method))
(g 'sig-vector method)))
:hints (("Goal" :in-theory (e/d (bcv-simple-method)
(bcv-simple-method1))
:do-not '(generalize)
:use ((:instance bcv-simple-method1-implies-inst-verified
(code (g 'code method))
(i 0)
(sig-vector (g 'sig-vector method)))))))
;; (defthm bcv-simple-method-implies-next-inst-verified-version-2
;; (implies (and (bcv-simple-method
;; (s 'sig-vector (collect-witness-bcv-method
;; method
;; method method-table)
;; (integerp pc)
;; (<= 0 pc)
;; (< pc (len (g 'code method))))
;; (bcv-simple-inst pc
;; (nth pc (g 'code method))
;; (g 'sig-vector method)))
;; :hints (("Goal" :in-theory (e/d (bcv-simple-method)
;; (bcv-simple-method1))
;; :do-not '(generalize)
;; :use ((:instance bcv-simple-method1-implies-inst-verified
;; (code (g 'code method))
;; (i 0)
;; (sig-vector (g 'sig-vector method)))))))
;----------------------------------------------------------------------
;; bcv-simple-inst implies
;; (bcv-simple-check-step-pre inst sframe))
;; and
;; (all-next-state-safe (bcv-simple-execute-step inst sframe))
;----------------------------------------------------------------------
;; (i-am-here) ;; Fri Nov 11 14:55:12 2005
(defthm bcv-simple-check-step-pre-if-sig-frame-compatible
(implies (and (sig-frame-compatible sframe gframe)
(bcv-simple-check-step-pre inst gframe))
(bcv-simple-check-step-pre inst sframe))
:hints (("Goal" :in-theory (enable bcv-simple-check-step-pre))))
(local
(defthm pc-no-change-pop-n
(equal (g 'pc (sig-frame-pop-n n sig-frame))
(g 'pc sig-frame))))
(local
(defthm equal-opstack-pop-n-still-equal
(implies (and (syntaxp (and (symbolp sframe)
(equal sframe 'sframe)))
(equal (g 'op-stack sframe)
(g 'op-stack gframe)))
(equal (g 'op-stack (sig-frame-pop-n n sframe))
(g 'op-stack
(sig-frame-pop-n n gframe))))))
(local
(defthm equal-max-stack-pop-n-still-equal
(equal (g 'max-stack (sig-frame-pop-n n sframe))
(g 'max-stack sframe))))
(local
(defthm equal-method-table-pop-n-still-equal
(equal (g 'method-table (sig-frame-pop-n n sframe))
(g 'method-table sframe))))
(local
(defthm equal-method-name-pop-n-still-equal
(equal (g 'method-name (sig-frame-pop-n n sframe))
(g 'method-name sframe))))
(defthm bcv-check-step-post-if-sig-frame-compatible
(implies (and (sig-frame-compatible sframe gframe)
(all-next-state-safe (bcv-simple-execute-step inst gframe) vector))
(all-next-state-safe (bcv-simple-execute-step inst sframe) vector))
:hints (("Goal" :in-theory (enable bcv-simple-execute-step all-next-state-safe))))
;----------------------------------------------------------------------
;; (defthm bcv-simple-method-implies-next-inst-verified-specific
;; (implies (and (bcv-simple-method method)
;; (integerp pc)
;; (<= 0 pc)
;; (< pc (len (g 'code method))))
;; (bcv-simple-inst pc
;; (nth pc (g 'code method))
;; (g 'sig-vector method)))
;; :hints (("Goal" :in-theory (e/d (bcv-simple-method)
;; (bcv-simple-method1))
;; :do-not '(generalize)
;; :use ((:instance bcv-simple-method1-implies-inst-verified
;; (code (g 'code method))
;; (i 0)
;; (sig-vector (g 'sig-vector method)))))))
|
