File: bcv-verified-implies-method-name-method-table-fixed.lisp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (186 lines) | stat: -rw-r--r-- 7,787 bytes parent folder | download | duplicates (2)
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
(in-package "ACL2")
(include-book "bcv-model")
(include-book "generic")

(defthm bcv-execute-step-change-no-method-name
  (implies (and (bcv-check-step-pre inst sig-frame)
                (case-split (not (member (bcv-op-code inst)
                                         '(HALT RETURN)))))
           (equal (G 'METHOD-NAME
                     (BCV-EXECUTE-STEP inst
                                       SIG-FRAME))
                  (g 'method-name sig-frame))))



(defthm bcv-execute-step-change-no-method-table
  (implies (and (bcv-check-step-pre inst sig-frame)
                (case-split (not (member (bcv-op-code inst)
                                         '(HALT RETURN)))))
           (equal (G 'METHOD-table
                     (BCV-EXECUTE-STEP inst
                                       SIG-FRAME))
                  (g 'method-table sig-frame))))


;;;
;;; the following fact is not straightforward as people would have thought. 
;;; because we don't know what's the stack-map that exist in the merged-code!
;;; 
;;; After a HALT, we will depend o nthe new stack-map to continue the checking
;;;
;;; we better be able to say that methot-name and method-table registered does
;;; not change!!! 
;;; 
;;; Fri Nov 11 09:55:03 2005


;; (defthm verified-implies-method-name-no-change
;;   (implies (and (merged-code-safe merged-code sig-frame)
;;                 (stack-map? sig-frame)
;;                 (bound? pc (collect-witness-merged-code-safe merged-code sig-frame)))
;;            (equal (G 'METHOD-NAME
;;                      (CDR (ASSOC-EQUAL pc
;;                                        (COLLECT-WITNESS-MERGED-CODE-SAFE
;;                                         MERGED-CODE SIG-FRAME))))
;;                   (g 'method-name sig-frame)))
;;   :hints (("Goal" :in-theory (e/d () (bcv-execute-step
;;                                       sig-frame-compatible)))))

;;; We need to characterize it. Introducing the concept to

(defthm bcv-execute-step-produce-AFTERGOTO
  (implies (and (bcv-check-step-pre inst sig-frame)
                (case-split (member (bcv-op-code inst) '(RETURN HALT))))
           (equal (bcv-execute-step inst sig-frame) 'AFTERGOTO)))


(local 
 (defthm equal-stac-frame-pop-n-still-equal
  (equal (g 'is-stack-map (sig-frame-pop-n n sframe))
         (g 'is-stack-map sframe))))


(local 
 (defthm equal-is-inst-pop-n-still-equal
  (equal (g 'is-inst (sig-frame-pop-n n sframe))
         (g 'is-inst sframe))))



(defthm bcv-execute-step-produce-STACK-MAPS
  (implies (and (bcv-check-step-pre inst sig-frame)
                (stack-map? sig-frame)
                (case-split (not (member (bcv-op-code inst) '(RETURN HALT)))))
           (stack-map? (bcv-execute-step inst sig-frame))))
  

(encapsulate ()
   (local (include-book "bcv-find-correct-witness-bcv-check-pre"))
   (defthm merge-code-safe-implies-bcv-check-step-pre-lemma
     (implies (and (merged-code-safe merged-code sig-frame)
                   (member inst merged-code)
                   (wff-code1 (extract-code merged-code)
                              (g 'pc (car merged-code)))
                   (inst? inst)
                   (equal pc (g 'pc inst)))
              (bcv-check-step-pre inst 
                                  (cdr (assoc-equal pc 
                                                    (collect-witness-merged-code-safe 
                                                     merged-code sig-frame)))))))





(DEFTHM verified-implies-method-name-no-change-lemma
  (implies (and (merged-code-safe merged-code sig-frame)
                (wff-maps-consistent (extract-maps merged-code) init-frame)
                (stack-map? init-frame)
                (or (equal sig-frame 'aftergoto)
                    (and (stack-map? sig-frame)
                         (equal (g 'method-name sig-frame) 
                                (g 'method-name init-frame))
                         (equal (g 'method-table sig-frame)
                                (g 'method-table init-frame))))
                (bound? pc (collect-witness-merged-code-safe merged-code sig-frame)))
           (equal (G 'METHOD-NAME
                     (CDR (ASSOC-EQUAL pc
                                       (COLLECT-WITNESS-MERGED-CODE-SAFE
                                        MERGED-CODE SIG-FRAME))))
                  (g 'method-name init-frame)))
  :hints (("Goal" :in-theory (e/d () (bcv-execute-step
                                      bcv-check-step-pre
                                      bcv-execute-step
                                      stack-map? inst?
                                      sig-frame-compatible))
           :do-not '(generalize fertilize))))







(DEFTHM verified-implies-method-name-no-change
  (implies (and (merged-code-safe merged-code init-frame)
                (wff-maps-consistent (extract-maps merged-code) init-frame)
                (stack-map? init-frame)
                (bound? pc (collect-witness-merged-code-safe merged-code init-frame)))
           (equal (G 'METHOD-NAME
                     (CDR (ASSOC-EQUAL pc
                                       (COLLECT-WITNESS-MERGED-CODE-SAFE
                                        MERGED-CODE init-FRAME))))
                  (g 'method-name init-frame)))
  :hints (("Goal" :in-theory (e/d () (bcv-execute-step
                                      bcv-check-step-pre
                                      bcv-execute-step
                                      stack-map? inst?
                                      sig-frame-compatible))
           :do-not '(generalize fertilize))))




(defthm verified-implies-method-table-no-change-lemma
   (implies (and (merged-code-safe merged-code sig-frame)
                 (wff-maps-consistent (extract-maps merged-code) init-frame)
                 (stack-map? init-frame)
                 (or (equal sig-frame 'aftergoto)
                     (and (stack-map? sig-frame)
                          (equal (g 'method-name sig-frame) 
                                 (g 'method-name init-frame))
                          (equal (g 'method-table sig-frame)
                                 (g 'method-table init-frame))))
                 (bound? pc (collect-witness-merged-code-safe merged-code sig-frame)))
           (equal (G 'method-table
                     (CDR (ASSOC-EQUAL pc
                                       (COLLECT-WITNESS-MERGED-CODE-SAFE
                                        MERGED-CODE SIG-FRAME))))
                  (g 'method-table init-frame)))
  :hints (("Goal" :in-theory (e/d () (bcv-execute-step
                                      bcv-check-step-pre
                                      bcv-execute-step
                                      stack-map? inst?
                                      sig-frame-compatible))
           :do-not '(generalize fertilize))))




(defthm verified-implies-method-table-no-change
   (implies (and (merged-code-safe merged-code init-frame)
                 (wff-maps-consistent (extract-maps merged-code) init-frame)
                 (stack-map? init-frame)
                 (bound? pc (collect-witness-merged-code-safe merged-code init-frame)))
           (equal (G 'method-table
                     (CDR (ASSOC-EQUAL pc
                                       (COLLECT-WITNESS-MERGED-CODE-SAFE
                                        MERGED-CODE INIT-FRAME))))
                  (g 'method-table init-frame)))
  :hints (("Goal" :in-theory (e/d () (bcv-execute-step
                                      bcv-check-step-pre
                                      bcv-execute-step
                                      stack-map? inst?
                                      sig-frame-compatible))
           :do-not '(generalize fertilize))))