forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpureLoopProofScript.sml
199 lines (185 loc) · 6.11 KB
/
pureLoopProofScript.sml
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
(*
Prove that pureLoop never exits prematurely.
*)
open preamble basis compilationLib;
open backendProofTheory backendPropsTheory;
open costLib costPropsTheory;
open dataSemTheory data_monadTheory dataLangTheory;
open pureLoopProgTheory;
val _ = new_theory "pureLoopProof"
val _ = temp_delsimps ["NORMEQ_CONV"]
val _ = diminish_srw_ss ["ABBREV"]
val _ = set_trace "BasicProvers.var_eq_old" 1
Overload monad_unitbind[local] = ``data_monad$bind``
Overload return[local] = ``data_monad$return``
val _ = monadsyntax.temp_add_monadsyntax()
val pureLoop = pureLoop_ast_def |> concl |> rand
val _ = install_naming_overloads "pureLoopProg";
val _ = write_to_file pureLoop_data_prog_def;
val body = ``lookup_pureLoop (fromAList pureLoop_data_prog)``
|> (REWRITE_CONV [pureLoop_data_code_def] THENC EVAL)
|> concl |> rhs |> rand |> rand
Theorem data_safe_pureLoop_code[local]:
∀s sstack smax.
s.safe_for_space ∧
(s.stack_frame_sizes = pureLoop_config.word_conf.stack_frame_size) ∧
(s.stack_max = SOME smax) ∧
(size_of_stack s.stack = SOME sstack) ∧
(sstack < s.limits.stack_limit) ∧
(smax < s.limits.stack_limit) ∧
(∃x. lookup 0 s.locals = SOME x) ∧
(lookup_pureLoop s.code = SOME (1,^body))
⇒ data_safe (evaluate (^body, s))
Proof
measureInduct_on `^s.clock`
\\ rw [ evaluate_def,get_var_def
, lookup_fromAList,get_vars_def
, find_code_def,call_env_def,data_safe_def
, flush_state_def ]
\\ rw [lookup_fromList,dec_clock_def,lookup_fromAList,data_safe_def]
\\ qmatch_goalsub_abbrev_tac `evaluate (_,s')`
\\ `s'.clock < s.clock` by rw [Abbr `s'`]
\\ first_x_assum (drule_then
(qspecl_then [`THE (size_of_stack s'.stack)`
,`THE s'.stack_max`] mp_tac))
\\ impl_tac
>- (rw [Abbr `s'`,lookup_fromList,pureLoop_config_def,lookup_def]
\\ fs [lookup_def,libTheory.the_def,MAX_DEF])
\\ rw []
\\ qmatch_asmsub_abbrev_tac `evaluate (_,s'')`
\\ `s' = s''`
by (UNABBREV_ALL_TAC
\\ rw [state_component_equality]
\\ EVAL_TAC)
\\ fs [] \\ EVERY_CASE_TAC \\ fs [data_safe_def]
QED
Theorem data_safe_pureLoop_code_shallow[local] =
data_safe_pureLoop_code |> simp_rule [to_shallow_thm,to_shallow_def]
Theorem data_safe_pureLoop_code_timeout[local]:
∀s. (∃x. lookup 0 s.locals = SOME x) ∧
(lookup_pureLoop s.code = SOME (1,^body))
⇒ ∃s'. evaluate (^body, s) =
(SOME (Rerr(Rabort Rtimeout_error)),s')
Proof
measureInduct_on `^s.clock`
\\ rw [ evaluate_def,get_var_def
, lookup_fromAList,get_vars_def
, find_code_def,call_env_def,data_safe_def]
\\ rw [lookup_fromList,dec_clock_def,lookup_fromAList,data_safe_def]
\\ qmatch_goalsub_abbrev_tac `evaluate (_,s')`
\\ `s'.clock < s.clock` by rw [Abbr `s'`]
\\ first_x_assum drule
\\ impl_tac
>- rw [Abbr `s'`,lookup_fromList]
\\ rw [] \\ rw []
QED
Theorem data_safe_pureLoop_code_timeout_shallow[local] =
data_safe_pureLoop_code_timeout |> simp_rule [to_shallow_thm,to_shallow_def]
Theorem data_safe_pureLoop:
∀ffi.
backend_config_ok (^((rand o rator o lhs o concl) pureLoop_thm))
⇒ is_safe_for_space ffi
(^((rand o rator o lhs o concl) pureLoop_thm))
^pureLoop
(1000,1000)
Proof
let
val code_lookup = mk_code_lookup
`fromAList pureLoop_data_prog`
pureLoop_data_code_def
val frame_lookup = mk_frame_lookup
`pureLoop_config.word_conf.stack_frame_size`
pureLoop_config_def
val strip_assign = mk_strip_assign code_lookup frame_lookup
val open_call = mk_open_call code_lookup frame_lookup
val make_call = mk_make_call open_call
val strip_call = mk_strip_call open_call
val open_tailcall = mk_open_tailcall code_lookup frame_lookup
val make_tailcall = mk_make_tailcall open_tailcall
in
strip_tac \\ strip_tac
\\ irule IMP_is_safe_for_space_alt \\ fs []
\\ conj_tac >- EVAL_TAC
\\ assume_tac pureLoop_thm
\\ asm_exists_tac \\ fs []
\\ assume_tac pureLoop_to_data_updated_thm
\\ fs [data_lang_safe_for_space_def]
\\ strip_tac
\\ qmatch_goalsub_abbrev_tac `_ v0`
\\ `data_safe v0` suffices_by
(Cases_on `v0` \\ fs [data_safe_def])
\\ UNABBREV_ALL_TAC
\\ qmatch_goalsub_abbrev_tac `is_64_bits c0`
\\ `is_64_bits c0` by (UNABBREV_ALL_TAC \\ EVAL_TAC)
\\ fs []
\\ rpt (pop_assum kall_tac)
(* Some tactics *)
\\ REWRITE_TAC [ to_shallow_thm
, to_shallow_def
, initial_state_def
, bvl_to_bviTheory.InitGlobals_location_eq]
\\ rpt strip_tac
(* Make first call *)
\\ make_tailcall
(* Bootcode *)
\\ ntac 7 strip_assign
(* Another call *)
\\ ho_match_mp_tac data_safe_bind_return
(* Yet another call *)
\\ make_call
\\ strip_call
\\ ntac 9 strip_assign
\\ make_if
\\ UNABBREV_ALL_TAC
(* Continues after call *)
\\ strip_makespace
\\ ntac 47 strip_assign
(* Another tailcall *)
\\ make_tailcall
\\ strip_call
\\ ntac 9 strip_assign
\\ make_if
\\ UNABBREV_ALL_TAC
\\ strip_call
\\ ntac 9 strip_assign
\\ make_if
\\ ntac 6 strip_assign
\\ open_tailcall
\\ ntac 4 strip_assign
\\ make_if
\\ ntac 2 strip_assign
\\ open_tailcall
\\ ntac 4 strip_assign
\\ make_if
\\ ntac 2 strip_assign
\\ open_tailcall
\\ ntac 4 strip_assign
\\ make_if
\\ UNABBREV_ALL_TAC
\\ strip_assign
\\ make_tailcall
\\ strip_makespace
\\ ntac 3 strip_assign
\\ make_tailcall
\\ strip_makespace
\\ ntac 4 strip_assign
\\ make_tailcall
\\ strip_assign
(* Finally we reach our function call *)
\\ ho_match_mp_tac data_safe_bind_error
\\ open_call
\\ qmatch_goalsub_abbrev_tac `f (state_locals_fupd _ _)`
\\ qmatch_goalsub_abbrev_tac `f s`
\\ `∃s'. f s = (SOME (Rerr(Rabort Rtimeout_error)),s')`
by (unabbrev_all_tac
\\ ho_match_mp_tac data_safe_pureLoop_code_timeout_shallow
\\ rw [lookup_def,lookup_fromList,code_lookup])
\\ `data_safe (f s)` suffices_by (rw [] \\ rfs [])
\\ unabbrev_all_tac
\\ ho_match_mp_tac data_safe_pureLoop_code_shallow
\\ rw [lookup_def,lookup_fromList,code_lookup,size_of_stack_def
,size_of_stack_frame_def]
end
QED
val _ = check_thm data_safe_pureLoop;
val _ = export_theory();