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
|
(in-package "BCV")
(include-book "typechecker")
(include-book "typechecker-ext")
(include-book "typechecker-simple")
(include-book "bcv-base")
(encapsulate ()
(local (include-book "bcv-searchStackFrame-reduce-support"))
(defthm searchStackFrame-is-if-stack-map
(implies (and (isStackMap (car mergedcode))
(equal (forward-to-next-inst mergedcode)
(forward-to-next-inst x))
(is-suffix mergedcode all-merged-code)
(PC-WFF-MERGEDCODE1 PC ALL-MERGED-CODE)
(mergedcodeistypesafe env all-merged-code init-frame))
(EQUAL
(SEARCHSTACKFRAME
(INSTROFFSET (CAR (FORWARD-TO-NEXT-INST x)))
(STACK-MAP-WRAP (COLLECT-SIG-FRAME-VECTOR ENV all-merged-code
INIT-FRAME)))
(NEXT-STACKFRAME mergedcode)))))
;; (skip-proofs
;; (defthm searchStackFrame-is-if-stack-map-specific
;; (implies (and (is-suffix (list* mergedcode3 mergedcode5 mergedcode6)
;; all-merged-code)
;; (isStackMap mergedcode3)
;; (isInstruction mergedcode6)
;; (PC-WFF-MERGEDCODE1 PC ALL-MERGED-CODE)
;; (mergedcodeistypesafe env all-merged-code init-frame))
;; (EQUAL
;; (SEARCHSTACKFRAME
;; (INSTROFFSET mergedcode5)
;; (STACK-MAP-WRAP (COLLECT-SIG-FRAME-VECTOR ENV all-merged-code
;; INIT-FRAME)))
;; (mapFrame (getMap mergedcode3))))))
(encapsulate ()
(local (include-book "bcv-searchStackFrame-reduce-support-2"))
(defthm mergecodeIsTypeSafe-implies-collect-sig-vector-compatible-1
(implies (and (mergedcodeIsTypeSafe env mergecode stackframe)
(member inst mergecode)
(isInstruction inst)
(isInstruction (next-inst inst mergecode))
(pc-wff-mergedcode1 (next-pc mergecode) mergecode))
(equal (car (sig-do-inst inst
env
(searchStackFrame (instroffset inst)
(stack-map-wrap
(collect-sig-frame-vector
env mergecode
stackframe)))))
(searchStackFrame (instroffset (next-inst inst mergecode))
(stack-map-wrap (collect-sig-frame-vector
env mergecode
stackframe)))))))
;; (encapsulate ()
;; (local (include-book "bcv-searchStackFrame-reduce-support-2"))
;; (defthm mergecodeIsTypeSafe-implies-collect-sig-vector-compatible-2
;; (implies (and (mergedcodeIsTypeSafe env mergecode stackframe)
;; (member inst mergecode)
;; (member (next-inst inst mergecode) mergecode)
;; (isInstruction inst)
;; (isStackMap (next-inst inst mergecode))
;; (pc-wff-mergedcode1 pc mergecode))
;; (equal (car (sig-do-inst inst
;; env
;; (searchStackFrame (instroffset inst)
;; (stack-map-wrap(collect-sig-frame-vector
;; env mergecode
;; stackframe)))))
|
