/
readerProgProofScript.sml
269 lines (251 loc) · 10 KB
/
readerProgProofScript.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
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
(*
End-to-end correctness theorem for the OpenTheory article
checker. The theorem reaches the next-state function of the
verified hardware platform called Silver.
*)
open preamble
semanticsPropsTheory backendProofTheory ag32_configProofTheory
ag32_memoryTheory ag32_memoryProofTheory ag32_ffi_codeProofTheory
ag32_machine_configTheory ag32_basis_ffiProofTheory
readerProgTheory readerCompileTheory
holSoundnessTheory
val _ = new_theory "readerProgProof";
val reader_io_events_def =
new_specification ("reader_io_events_def", ["reader_io_events"],
reader_semantics |> Q.GENL [`cl`,`fs`]
|> SIMP_RULE std_ss [GSYM RIGHT_EXISTS_IMP_THM]
|> SIMP_RULE std_ss [SKOLEM_THM]);
val (reader_sem,reader_output) = reader_io_events_def |> SPEC_ALL |> UNDISCH |> CONJ_PAIR
val (reader_not_fail,reader_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail reader_sem |> CONJ_PAIR
val ffi_names =
``config.lab_conf.ffi_names``
|> (REWRITE_CONV[readerCompileTheory.config_def] THENC EVAL)
val LENGTH_code =
``LENGTH code``
|> (REWRITE_CONV[readerCompileTheory.code_def] THENC listLib.LENGTH_CONV)
val LENGTH_data =
``LENGTH data``
|> (REWRITE_CONV[readerCompileTheory.data_def] THENC listLib.LENGTH_CONV)
Overload reader_machine_config =
``ag32_machine_config (extcalls config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
Theorem target_state_rel_reader_start_asm_state:
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
LENGTH inp ≤ stdin_size ∧
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms ⇒
∃n. target_state_rel ag32_target (init_asm_state code data (extcalls config.lab_conf.ffi_names) (cl,inp)) (FUNPOW Next n ms) ∧
((FUNPOW Next n ms).io_events = ms.io_events) ∧
(∀x. x ∉ (ag32_startup_addresses) ⇒
((FUNPOW Next n ms).MEM x = ms.MEM x))
Proof
strip_tac
\\ drule (GEN_ALL init_asm_state_RTC_asm_step)
\\ disch_then drule
\\ simp_tac std_ss []
\\ disch_then(qspecl_then[`code`,`data`,`extcalls config.lab_conf.ffi_names`]mp_tac)
\\ impl_tac >- ( EVAL_TAC>> fs[ffi_names,LENGTH_data,LENGTH_code,extcalls_def])
\\ strip_tac
\\ drule (GEN_ALL target_state_rel_ag32_init)
\\ rveq
\\ qmatch_goalsub_abbrev_tac`_ ∉ md`
\\ disch_then(qspec_then`md`assume_tac)
\\ drule (GEN_ALL RTC_asm_step_ag32_target_state_rel_io_events)
\\ simp[EVAL``(ag32_init_asm_state m md).mem_domain``]
QED
val reader_startup_clock_def =
new_specification("reader_startup_clock_def",["reader_startup_clock"],
GEN_ALL (Q.SPEC`ms0`(Q.GEN`ms`target_state_rel_reader_start_asm_state))
|> SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM,SKOLEM_THM]);
val compile_correct_applied =
MATCH_MP compile_correct reader_compiled
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO]
|> C MATCH_MP reader_not_fail
|> C MATCH_MP ag32_backend_config_ok
|> REWRITE_RULE[reader_sem_sing,AND_IMP_INTRO]
|> REWRITE_RULE[Once (GSYM AND_IMP_INTRO)]
|> C MATCH_MP (CONJ(UNDISCH ag32_machine_config_ok)(UNDISCH ag32_init_ok))
|> DISCH(#1(dest_imp(concl ag32_init_ok)))
|> C MATCH_MP is_ag32_machine_config_ag32_machine_config
|> Q.GEN`cbspace` |> Q.SPEC`0`
|> Q.GEN`data_sp` |> Q.SPEC`0`
Triviality to_MAP_ExtCall:
[ExtCall n] = MAP ExtCall [n] ∧
(ExtCall n::MAP ExtCall ns) = MAP ExtCall (n::ns)
Proof
fs []
QED
Theorem reader_installed:
SUM (MAP strlen cl) + LENGTH cl ≤ cline_size ∧
LENGTH inp ≤ stdin_size ∧
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0 ⇒
installed code 0 data 0 config.lab_conf.ffi_names
(heap_regs ag32_backend_config.stack_conf.reg_names)
(reader_machine_config) (FUNPOW Next (reader_startup_clock ms0 inp cl) ms0)
Proof
rewrite_tac[ffi_names, extcalls_def]
\\ strip_tac
\\ rewrite_tac [to_MAP_ExtCall]
\\ irule ag32_installed
\\ drule reader_startup_clock_def
\\ disch_then drule
\\ rewrite_tac[ffi_names, extcalls_def]
\\ disch_then drule
\\ strip_tac
\\ simp[]
\\ conj_tac >- (simp[LENGTH_code] \\ EVAL_TAC)
\\ conj_tac >- (simp[LENGTH_code, LENGTH_data] \\ EVAL_TAC)
\\ conj_tac >- (EVAL_TAC)
\\ rpt $ goal_assum $ drule_at Any
\\ simp[]
\\ fs[ffi_names]
QED
val reader_machine_sem =
compile_correct_applied
|> C MATCH_MP (UNDISCH reader_installed)
|> DISCH_ALL
|> curry save_thm "reader_machine_sem";
val _ = Parse.hide "mem";
val mem = ``mem:'U->'U-> bool``;
Overload reader[local] = ``\inp r. readLines init_state inp r``
val all_lines_stdin_fs = Q.prove (
`all_lines_inode (stdin_fs inp) (UStream «stdin»)
=
lines_of (implode inp)`,
EVAL_TAC);
Theorem reader_extract_writes:
wfcl cl ∧
LENGTH cl = 1 ⇒
let events = MAP get_output_io_event (reader_io_events cl (stdin_fs inp));
out = extract_writes 1 events;
err = extract_writes 2 events;
refs = SND (init_reader () init_refs) in
case reader (MAP (tokenize o str_prefix) (lines_of (implode inp))) refs of
(M_failure (Failure e), refs) =>
(out = "") ∧
(err = explode e)
| (M_success (s, _), refs) =>
(is_set_theory ^mem ==>
(∀asl c.
MEM (Sequent asl c) s.thms ⇒
(thyof refs.the_context, asl) |= c)) ∧
refs.the_context extends init_ctxt ∧
(out = explode (concat (append (msg_success s refs.the_context)))) ∧
(err = "")
| _ => F
Proof
strip_tac \\ fs []
\\ mp_tac (GEN_ALL (DISCH_ALL reader_output))
\\ disch_then (qspecl_then [`stdin_fs inp`, `cl`] mp_tac)
\\ fs [wfFS_stdin_fs, STD_streams_stdin_fs, LENGTH_EQ_NUM_compute]
\\ impl_tac
>- (qexists_tac `inp` \\ EVAL_TAC)
\\ strip_tac
\\ Cases_on `init_reader () init_refs`
\\ drule readerProofTheory.init_reader_ok
\\ strip_tac \\ rveq \\ fs []
\\ PURE_TOP_CASE_TAC \\ fs []
\\ reverse PURE_TOP_CASE_TAC \\ fs []
>-
(PURE_CASE_TAC \\ fs []
\\ conj_tac
\\ irule extract_fs_extract_writes
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ simp [RIGHT_EXISTS_AND_THM]
\\ simp [readerProofTheory.reader_main_def,
readerProofTheory.read_stdin_def]
\\ qpat_x_assum ‘_ = init_reader _ _’ (assume_tac o SYM)
\\ simp [all_lines_stdin_fs]
\\ (conj_tac >- simp [fsFFIPropsTheory.inFS_fname_def, stdin_fs_def])
\\ (conj_tac >- simp [stdin_fs_def])
\\ conj_tac
\\ simp [stdin_fs_def, fsFFIPropsTheory.fastForwardFD_def,
libTheory.the_def, TextIOProofTheory.add_stdo_def,
TextIOProofTheory.up_stdo_def, TextIOProofTheory.stdo_def,
fsFFITheory.fsupdate_def, AFUPDKEY_ALOOKUP]
\\ SELECT_ELIM_TAC
\\ (conj_asm1_tac >- (qexists_tac ‘«»’ \\ simp []))
\\ fs []
\\ rw [OPTREL_def]
\\ fs [AllCaseEqs (), PULL_EXISTS]
\\ rw [] \\ fs []
\\ CCONTR_TAC \\ fs [] \\ rw [] \\ fs [])
\\ CASE_TAC \\ fs []
\\ once_rewrite_tac [CONJ_ASSOC]
\\ conj_tac
>-
(rw []
\\ assume_tac readerProofTheory.READER_STATE_init_state
\\ drule_all readerProofTheory.readLines_thm \\ rw []
\\ DEP_REWRITE_TAC [proves_sound] \\ simp []
\\ fs [readerProofTheory.READER_STATE_def, EVERY_MEM]
\\ first_x_assum (assume_tac o REWRITE_RULE [holKernelProofTheory.THM_def] o
Q.GENL [`a`,`b`] o Q.SPEC `Sequent a b`)
\\ fs [holKernelProofTheory.STATE_def, holKernelProofTheory.CONTEXT_def]
\\ rveq
\\ qpat_x_assum ‘ds ++ _ = _’ (assume_tac o SYM) \\ fs[])
\\ conj_tac
\\ irule extract_fs_extract_writes
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ simp [RIGHT_EXISTS_AND_THM]
\\ simp [readerProofTheory.reader_main_def,
readerProofTheory.read_stdin_def]
\\ qpat_x_assum ‘_ = init_reader _ _’ (assume_tac o SYM)
\\ simp [all_lines_stdin_fs]
\\ (conj_tac >- simp [fsFFIPropsTheory.inFS_fname_def, stdin_fs_def])
\\ (conj_tac >- simp [stdin_fs_def])
\\ conj_tac
\\ simp [stdin_fs_def, fsFFIPropsTheory.fastForwardFD_def,
libTheory.the_def, TextIOProofTheory.add_stdo_def,
TextIOProofTheory.up_stdo_def, TextIOProofTheory.stdo_def,
fsFFITheory.fsupdate_def, AFUPDKEY_ALOOKUP]
\\ SELECT_ELIM_TAC
\\ (conj_asm1_tac >- (qexists_tac ‘«»’ \\ simp []))
\\ fs []
\\ rw [OPTREL_def]
\\ fs [AllCaseEqs (), PULL_EXISTS]
\\ rw [] \\ fs []
\\ CCONTR_TAC \\ fs [] \\ rw [] \\ fs []
QED
Theorem reader_ag32_next:
SUM (MAP strlen cl) + LENGTH cl <= cline_size /\
LENGTH inp <= stdin_size /\
wfcl cl /\
(LENGTH cl = 1) /\
is_ag32_init_state (init_memory code data (extcalls config.lab_conf.ffi_names) (cl,inp)) ms0
==>
?k1. !k. k1 <= k ==>
let ms = FUNPOW Next k ms0 in
let outs = MAP (get_ag32_io_event) ms.io_events in
(ms.PC = (reader_machine_config).halt_pc) /\
(get_mem_word ms.MEM ms.PC = Encode (Jump (fAdd,0w,Imm 0w))) /\
outs ≼ MAP get_output_io_event (reader_io_events cl (stdin_fs inp)) /\
((ms.R (n2w (reader_machine_config).ptr_reg) = 0w) ==>
(outs = MAP get_output_io_event (reader_io_events cl (stdin_fs inp))))
Proof
strip_tac
\\ mp_tac (GEN_ALL reader_machine_sem)
\\ disch_then (mp_tac o CONV_RULE (RESORT_FORALL_CONV rev))
\\ disch_then (qspec_then `cl` mp_tac)
\\ disch_then (qspecl_then [`stdin_fs inp`, `inp`, `ms0`] mp_tac)
\\ impl_tac
>-
(
fs [STD_streams_stdin_fs, wfFS_stdin_fs, LENGTH_EQ_NUM_compute]
\\ qexists_tac `inp`
\\ simp [stdin_fs_def, TextIOProofTheory.stdin_def])
\\ strip_tac
\\ irule ag32_next
\\ conj_tac >- simp [ffi_names, extcalls_def]
\\ conj_tac >- (simp [ffi_names, extcalls_def, LENGTH_code, LENGTH_data] \\ EVAL_TAC)
\\ conj_tac >- (simp [ffi_names, extcalls_def] \\ EVAL_TAC)
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ drule reader_startup_clock_def
\\ rpt (disch_then drule)
\\ strip_tac
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ goal_assum (first_assum o mp_then Any mp_tac)
\\ metis_tac []
QED
val _ = export_theory();