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
|
(in-package "BCV")
(include-book "typechecker")
(include-book "typechecker-ext")
(include-book "typechecker-simple")
(include-book "bcv-base")
;; (encapsulate ()
;; (local (include-book "bcv-instructionIsTypeSafe-if-verified"))
;; (defthm mergedcodeIsTypesafe-implies-instructionIsTypeSafe
;; (implies (and (mergedcodeIsTypesafe env mergedcode stackframe)
;; (pc-wff-mergedcode1 0 (allinstructions env))
;; (is-suffix mergedcode (allinstructions env))
;; (member inst (extract-code mergedcode)))
;; (instructionIsTypeSafe
;; inst
;; env
;; (searchStackFrame (instrOffset inst)
;; (stack-map-wrap
;; (collect-sig-frame-vector env
;; mergedcode
;;
(local
(defun collect-frames (stack-maps)
(if (endp stack-maps) nil
(cons (mapFrame (car stack-maps))
(collect-frames (cdr stack-maps))))))
(local
(defthm not-member-aftergoto-collect-sig-frame-vector
(not (member 'aftergoto (collect-frames
(collect-sig-frame-vector env code init-frame))))
:hints (("Goal" :in-theory (disable instructionIsTypeSafe
instructionSatisfiesHandlers
instrOffset
sig-do-inst
allinstructions
isEnd
;;mapFrame
getMap mapOffset
frameIsAssignable
isInstruction
isStackMap)
:do-not '(generalize)))))
(local
(defthm not-member-aftergoto-then-not-found
(implies (not (member 'aftergoto (collect-frames stack-maps)))
(not (equal (searchStackFrame any (stack-map-wrap stack-maps))
'aftergoto)))))
(defthm collect-sig-frame-vector-never-aftergoto
(not (equal (searchstackframe
any
(stack-map-wrap (collect-sig-frame-vector any-env any-code
any-init-frame)))
'aftergoto))
:hints (("Goal" :in-theory (disable instructionIsTypeSafe
instructionSatisfiesHandlers
instrOffset
sig-do-inst
allinstructions
isEnd
;;mapFrame
getMap mapOffset
frameIsAssignable
isInstruction
isStackMap)
:do-not '(generalize))))
|
