-
Notifications
You must be signed in to change notification settings - Fork 83
/
eval_exampleProgScript.sml
237 lines (208 loc) · 6.79 KB
/
eval_exampleProgScript.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
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
(*
Defines abstract syntax for a simple program that calls eval.
The call is made to machine code read from a file.
*)
open preamble ml_translatorLib ml_progLib
basisProgTheory basisFunctionsLib
val _ = new_theory "eval_exampleProg";
val _ = translation_extends "basisProg";
(* We assume the machine code is in two files:
- eval_words.txt
- exactly one integer (decimal numeral) per line
- in the range [0, 2**64)
- each line represents one compiler-generated
bitmap (64-bit word)
- eval_bytes.txt
- exactly one integer (decimal numeral) per line
- in the range [0, 2**8)
- each line represents one compiler-generated byte
of machine code *)
Definition trimr_def:
trimr s = substring s 0 (strlen s - 1)
End
val res = translate trimr_def;
(* TODO changed but this file is broken *)
val fname_to_words = process_topdecs`
fun fname_to_words from_int fname =
List.map
(from_int o
Option.valOf o Int.fromNatString o
trimr)
(Option.valOf (TextIO.b_inputLinesFrom #"\n" fname))
handle _ => (print "Error reading data to eval.\n";
Runtime.exit 1; [])`;
val res = append_prog fname_to_words;
val ml_prog_state = get_ml_prog_state()
val s2 = get_state ml_prog_state
val locn_thm = EVAL``LENGTH ^s2.refs``
Theorem ref_eval_thm:
!l. eval_rel
^s2
^(get_env ml_prog_state)
(App Opref [Lit l])
(^s2 with refs := ^s2.refs ++ [Refv (Litv l)])
(Loc ^(rconc locn_thm))
Proof
rw[ml_progTheory.eval_rel_alt]
\\ rw[evaluateTheory.evaluate_def]
\\ rw[semanticPrimitivesTheory.do_app_def]
\\ rw[semanticPrimitivesTheory.store_alloc_def]
\\ rw[semanticPrimitivesTheory.state_component_equality]
\\ rw[locn_thm]
QED
val () = ml_prog_update (
ml_progLib.add_Dlet
(Q.SPEC `StrLit "initial string\n"` ref_eval_thm)
"the_string_ref")
open evaluatePropsTheory evaluateTheory ml_progTheory
semanticPrimitivesTheory
Theorem evaluate_eval_state_NONE:
(∀s:'ffi state env exps s' res.
evaluate s env exps = (s', res) ⇒
(s.eval_state = NONE ⇔ s'.eval_state = NONE)) ∧
(∀s:'ffi state env x pes err_x s' res.
evaluate_match s env x pes err_x = (s', res) ⇒
(s.eval_state = NONE ⇔ s'.eval_state = NONE)) ∧
(∀s:'ffi state env decs s' res.
evaluate_decs s env decs = (s', res) ⇒
(s.eval_state = NONE ⇔ s'.eval_state = NONE))
Proof
ho_match_mp_tac full_evaluate_ind
\\ rw[evaluate_def, evaluate_decs_def,
CaseEqs["prod","result","option","match_result",
"error_result","bool","exp_or_val"]]
\\ gs[dec_clock_def]
\\ gvs[do_eval_res_def,CaseEqs["option","prod"]]
\\ gvs[declare_env_def,CaseEqs["option"]]
\\ gvs[do_eval_def,CaseEqs[
"prod","option","eval_state","list","v"]]
\\ gvs[reset_env_generation_def,
CaseEqs["prod","option","eval_state"]]
QED
Theorem Decls_eval_state_NONE:
Decls env st decls res_env res_st ==>
(res_st.eval_state = NONE <=> st.eval_state = NONE)
Proof
rw[Decls_def]
\\ drule (CONJUNCT2 (CONJUNCT2 evaluate_eval_state_NONE))
\\ simp[]
QED
Theorem Decls_add_eval_state:
Decls env st decls res_env res_st ∧
st.eval_state = NONE
⇒
Decls env (st with eval_state := es) decls res_env
(res_st with eval_state := es)
Proof
rw[Decls_def]
\\ drule(CONJUNCT2(CONJUNCT2 eval_no_eval_simulation))
\\ simp[]
\\ disch_then(qspec_then`es`mp_tac) \\ rw[]
\\ metis_tac[]
QED
Theorem ML_code_eval_state_NONE_EVERY:
!env bls st.
ML_code env bls st /\
(bls <> [] ==> (FST(SND(HD bls))).eval_state = NONE)
==> EVERY (\bl. (FST(SND bl)).eval_state = NONE) bls
Proof
ho_match_mp_tac ML_code_ind
\\ rw[ML_code_def] \\ fs[]
\\ Cases_on`bls` \\ gs[]
\\ PairCases_on`h` \\ fs[]
\\ fs[ML_code_def]
\\ imp_res_tac Decls_eval_state_NONE
\\ gvs[]
QED
Theorem ML_code_env_eq:
!env bls1 bls2.
LIST_REL (λbl1 bl2. SND(SND(SND bl1)) = SND(SND(SND bl2))) bls1 bls2 ==>
ML_code_env env bls1 = ML_code_env env bls2
Proof
ho_match_mp_tac ML_code_env_ind
\\ rw[ML_code_env_def]
\\ PairCases_on`bl2`
\\ rw[ML_code_env_def]
\\ AP_TERM_TAC
\\ first_x_assum irule
\\ simp[]
QED
Theorem ML_code_add_eval_state:
ML_code env0 bls s2 ==>
(bls <> [] ==> (FST(SND(HD bls))).eval_state = NONE) ==>
ML_code env0
(MAP (λ(comm,st,decls,env).
(comm,st with eval_state := es,decls,env)) bls)
(s2 with eval_state := es)
Proof
ntac 2 strip_tac
\\ drule ML_code_eval_state_NONE_EVERY
\\ impl_tac >- rw[]
\\ pop_assum kall_tac
\\ pop_assum mp_tac
\\ map_every qid_spec_tac [`s2`,`bls`,`env0`]
\\ ho_match_mp_tac ML_code_ind
\\ rw[ML_code_def]
\\ irule Decls_add_eval_state \\ gvs[]
\\ qmatch_goalsub_abbrev_tac`Decls env2`
\\ `env2 = ML_code_env env0 bls` suffices_by rw[]
\\ simp[Abbr`env2`]
\\ irule ML_code_env_eq
\\ simp[LIST_REL_MAP1]
\\ irule EVERY2_refl
\\ simp[FORALL_PROD]
QED
val ml_prog_state = get_ml_prog_state()
val s2 = get_state ml_prog_state
val env = get_env ml_prog_state
Triviality declare_env_thm:
declare_env_rel ^s2 ^env ^s2
(Env ^env (0,0))
Proof
rw[ml_progTheory.declare_env_rel_def]
\\ qmatch_goalsub_abbrev_tac`declare_env es env`
\\ `declare_env es env = SOME (Env env (0,0), NONE)`
by cheat (* TODO: redesign to cope with eval state NONE *)
\\ rw[semanticPrimitivesTheory.state_component_equality]
\\ rw[Abbr`es`] \\ EVAL_TAC
QED
val () = ml_prog_update (
ml_progLib.add_Denv declare_env_thm "env1");
(* These decs cannot go through ml_progLib
because it only supports declaring functions *)
val read_code_decs = process_topdecs`
val the_bytes =
fname_to_words Word8.fromInt "eval_bytes.txt"
val the_words =
fname_to_words Word64.fromInt "eval_words.txt"`;
(* These decs cannot go through ml_progLib
because it does not support eval.
To make the effect of the eval'd code visible, we
put a string ref in its scope and print the
string after eval'ing. *)
val call_eval_decs = ``
[Dlet unknown_loc Pany
(App Opapp [Var (Short "print");
App Opderef [Var (Short "the_string_ref")]]);
Dlet unknown_loc (Pvar "env2")
(App Eval [Var (Short "env1");
Lit (StrLit "dummy_input_state");
Lit (StrLit "dummy_decs");
Lit (StrLit "dummy_output_state");
Var (Short "the_bytes");
Var (Short "the_words")]);
Dlet unknown_loc Pany
(App Opapp [Var (Short "print");
App Opderef [Var (Short "the_string_ref")]]) ]``;
val decls_thm = get_Decls_thm (get_ml_prog_state())
val init_decls =
decls_thm |> concl |> strip_comb |> #2 |> el 3
val all_decls =
listSyntax.mk_append(init_decls,
listSyntax.mk_append(read_code_decs, call_eval_decs))
|> PURE_REWRITE_CONV [listTheory.APPEND]
|> rconc
Definition eval_example_prog_def:
eval_example_prog = ^all_decls
End
val _ = export_theory();