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
|
(in-package "BCV")
(include-book "../DJVM/consistent-state-strong")
(include-book "../DJVM/consistent-state-to-sig-state")
(include-book "../BCV/typechecker")
(include-book "../BCV/typechecker-ext")
(include-book "../BCV/typechecker-simple")
(include-book "../BCV/bcv-functions")
(encapsulate
(((good-scl-strong *) => *)
((good-static-frame * *) => *)
((icl-witness-x *) => *))
(local
(defun good-scl-strong (scl)
(declare (ignore scl))
nil))
(local
(defun icl-witness-x (scl)
(declare (ignore scl))
nil))
(local
(defun good-static-frame (frame scl)
(declare (ignore frame scl))
nil))
(defthm good-scl-strong-icl-witness-x
(implies (good-scl-strong scl)
(good-icl (icl-witness-x scl))))
(defthm if-scl-icl-scl-compatible
(implies (good-scl-strong scl)
(icl-scl-compatible (icl-witness-x scl)
(scl-jvm2bcv scl))))
(defthm consistent-sig-stack-if-good-static-frame
(implies (and (good-scl-strong scl)
(good-static-frame frame scl))
(consistent-sig-stack
(frameStack frame)
(icl-witness-x scl))))
(defthm consistent-state-strong-implies-good-static-frame
(implies (and (djvm::consistent-state-strong s)
(good-scl-strong (djvm::env-class-table (djvm::env s))))
(good-static-frame
(djvm::frame-sig (djvm::current-frame s)
(djvm::instance-class-table s)
(djvm::heap s)
(djvm::heap-init-map (djvm::aux s)))
(djvm::env-class-table (djvm::env s)))))
(defthm consistent-state-strong-implies-good-static-frame-2
(implies (and (djvm::consistent-state-strong s)
(good-scl-strong (djvm::env-class-table (djvm::env s)))
(car (jvm::class-by-name-s classname
(SCL-JVM2BCV
(djvm::env-class-table (djvm::env s)))))
(car (jvm::method-by-name-s
method-name
args
returntype (jvm::methods-s (mv-nth 1 (jvm::class-by-name-s
classname
(scl-jvm2bcv (djvm::env-class-table
(djvm::env s))))))))
(bcv-simple-method
(mv-nth 1
(jvm::class-by-name-s
classname
(scl-jvm2bcv (djvm::env-class-table (djvm::env
s)))))
(mv-nth 1 (jvm::method-by-name-s
method-name
args
returntype (methods-s (mv-nth 1 (jvm::class-by-name-s
classname
(scl-jvm2bcv (djvm::env-class-table
(djvm::env s))))))))
stack-maps
(scl-jvm2bcv (djvm::env-class-table (djvm::env s))))
(searchStackFrame pc (stack-map-wrap stack-maps)))
(good-static-frame
(searchStackFrame pc (stack-map-wrap stack-maps))
(scl-jvm2bcv (djvm::env-class-table (djvm::env s)))))))
|
