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
|
(in-package "DJVM")
(include-book "consistent-state")
(include-book "djvm-frame-manipulation-primitives")
(in-theory (disable consistent-state consistent-thread-entry))
(include-book "INST/base-bind-free")
(defthm consistent-state-imlies-thread-by-id
(implies (consistent-state s)
(thread-by-id (current-thread s)
(thread-table s)))
:hints (("Goal" :in-theory (enable consistent-state thread-exists?))))
(defthm consistent-state-implies-consistent-thread-entries
(implies (and (consistent-state s)
(equal (instance-class-table s) cl)
(equal (heap s) hp))
(consistent-thread-entries (thread-table s) cl hp))
:hints (("Goal" :in-theory (enable consistent-state))))
(defthm consistent-thread-entries-implies-consistent-thread
(implies (and (thread-by-id id tt)
(consistent-thread-entries tt cl hp))
(consistent-thread-entry (thread-by-id id tt)
cl hp))
:hints (("Goal" :in-theory (enable thread-by-id))))
(defthm consistent-thread-entry-implies-consp-thread-call-stack
(implies (and (syntaxp (acl2::found-symbol2 's thread))
(bind-free (acl2::default-bind-free 's 's (acl2::pkg-witness "DJVM")))
(consistent-thread-entry thread
(instance-class-table s)
(heap s)))
(consp (thread-call-stack thread)))
:hints (("Goal" :in-theory (enable consistent-thread-entry))))
;----------------------------------------------------------------------
;;(i-am-here)
(encapsulate ()
(local (include-book "consistent-state-properties"))
(local
(defthm consistent-state-topstack-consistent-value-x
(implies (and (topStack-guard-strong s)
(consistent-state s))
(consistent-value-x (safe-topStack s)
(instance-class-table s)
(heap s)))
:rule-classes :forward-chaining))
(defthm consistent-value-x-implies-wff-tagged-value
(implies (consistent-value-x v cl hp)
(wff-tagged-value v))
:rule-classes :forward-chaining)
(local
(defthm safe-topStack-is-topStack
(equal (safe-topStack s)
(topStack s))
:hints (("Goal" :in-theory (enable safe-topStack topStack
current-frame)))))
(defthm consistent-state-topstack-consistent-value-x-2
(implies (and (topStack-guard-strong s)
(consistent-state s))
(consistent-value-x (topStack s)
(instance-class-table s)
(heap s)))
:hints (("Goal" :in-theory (disable safe-topStack
topStack consistent-value-x)
:use ((:instance consistent-state-topstack-consistent-value-x))))
:rule-classes :forward-chaining))
(in-theory (disable topStack safe-topStack consistent-value-x
topStack-guard-strong))
|
