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
|
(in-package "ACL2")
(include-book "bcv-simple-model")
(include-book "djvm-model")
;;;
;;; note the following is not true!!
;;;
(local
(in-theory (disable bcv-simple-check-INVOKE
bcv-simple-check-POP
bcv-simple-check-PUSH
bcv-simple-check-RETURN
bcv-simple-check-IFEQ
djvm-check-INVOKE
djvm-check-POP
djvm-check-PUSH
djvm-check-RETURN
djvm-check-IFEQ)))
(local
(in-theory (disable consistent-state next-inst
extract-sig-frame)))
;; (defthm bcv-simple-check-implies-djvm-check-lemma
;; (implies (and (consistent-state djvm-s)
;; (equal (car (g 'call-stack st)) sig-frame)
;; (bcv-simple-check-step-pre
;; inst (extract-sig-frame sig-frame
;; method-table))
;; (djvm-check-step-g inst djvm-s)))
(encapsulate ()
(local (include-book "INVOKE"))
(defthm bcv-simple-check-invoke-implies-djvm-check
(IMPLIES (AND (CONSISTENT-STATE DJVM-S)
(equal (op-code (next-inst djvm-s)) 'INVOKE)
(BCV-SIMPLE-CHECK-INVOKE (next-inst djvm-s)
(EXTRACT-SIG-FRAME (CAR (G 'CALL-STACK DJVM-S))
(G 'METHOD-TABLE DJVM-S))))
(DJVM-CHECK-INVOKE (next-inst djvm-s) djvm-s))))
(encapsulate ()
(local (include-book "PUSH"))
(defthm bcv-simple-check-push-implies-djvm-check
(IMPLIES (AND (CONSISTENT-STATE DJVM-S)
(equal (op-code (next-inst djvm-s)) 'PUSH)
(BCV-SIMPLE-CHECK-PUSH (next-inst djvm-s)
(EXTRACT-SIG-FRAME (CAR (G 'CALL-STACK DJVM-S))
(G 'METHOD-TABLE DJVM-S))))
(DJVM-CHECK-PUSH (next-inst djvm-s) djvm-s))))
(encapsulate ()
(local (include-book "POP"))
(defthm bcv-simple-check-pop-implies-djvm-check
(IMPLIES (AND (CONSISTENT-STATE DJVM-S)
(equal (op-code (next-inst djvm-s)) 'POP)
(BCV-SIMPLE-CHECK-POP (next-inst djvm-s)
(EXTRACT-SIG-FRAME (CAR (G 'CALL-STACK DJVM-S))
(G 'METHOD-TABLE DJVM-S))))
(DJVM-CHECK-POP (next-inst djvm-s) djvm-s))))
(encapsulate ()
(local (include-book "IFEQ"))
(defthm bcv-simple-check-ifeq-implies-djvm-check
(IMPLIES (AND (CONSISTENT-STATE DJVM-S)
(equal (op-code (next-inst djvm-s)) 'IFEQ)
(BCV-SIMPLE-CHECK-IFEQ (next-inst djvm-s)
(EXTRACT-SIG-FRAME (CAR (G 'CALL-STACK DJVM-S))
(G 'METHOD-TABLE DJVM-S))))
(DJVM-CHECK-IFEQ (next-inst djvm-s) djvm-s))))
(encapsulate ()
(local (include-book "RETURN"))
(defthm bcv-simple-check-return-implies-djvm-check
(IMPLIES (AND (CONSISTENT-STATE DJVM-S)
(equal (op-code (next-inst djvm-s)) 'RETURN)
(BCV-SIMPLE-CHECK-RETURN (next-inst djvm-s)
(EXTRACT-SIG-FRAME (CAR (G 'CALL-STACK DJVM-S))
(G 'METHOD-TABLE DJVM-S))))
(DJVM-CHECK-RETURN (next-inst djvm-s) djvm-s))))
(encapsulate ()
(local (include-book "HALT"))
(defthm consistent-state-preserved-by-HALT
(implies (and (consistent-state st)
(equal (next-inst st) inst)
(equal (op-code inst) 'HALT))
(consistent-state
(execute-HALT inst st)))))
(defthm bcv-simple-check-implies-djvm-check
(implies (and (consistent-state djvm-s)
(bcv-simple-check-step-pre (next-inst djvm-s)
(extract-sig-frame
(TOPX (G 'CALL-STACK DJVM-S))
(G 'METHOD-TABLE DJVM-S))))
(djvm-check-step djvm-s)))
|
