forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
wordfreqProofScript.sml
79 lines (66 loc) · 2.92 KB
/
wordfreqProofScript.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
(*
Constructs the end-to-end correctness theorem for wordfreq example
by composing the application-specific correctness theorem, the
compiler evaluation theorem and the compiler correctness theorem.
*)
open preamble
semanticsPropsTheory backendProofTheory x64_configProofTheory
wordfreqProgTheory wordfreqCompileTheory
val _ = new_theory"wordfreqProof";
val wordfreq_io_events_def = new_specification("wordfreq_io_events_def",["wordfreq_io_events"],
wordfreq_semantics |> Q.GENL[`fs`,`pname`,`fname`]
|> SIMP_RULE bool_ss [SKOLEM_THM,Once(GSYM RIGHT_EXISTS_IMP_THM),RIGHT_EXISTS_AND_THM]);
val (wordfreq_sem,wordfreq_output) = wordfreq_io_events_def |> SPEC_ALL |> UNDISCH |> CONJ_PAIR
val (wordfreq_not_fail,wordfreq_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail wordfreq_sem |> CONJ_PAIR
val compile_correct_applied =
MATCH_MP compile_correct wordfreq_compiled
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO]
|> C MATCH_MP wordfreq_not_fail
|> C MATCH_MP x64_backend_config_ok
|> REWRITE_RULE[wordfreq_sem_sing,AND_IMP_INTRO]
|> REWRITE_RULE[Once (GSYM AND_IMP_INTRO)]
|> C MATCH_MP (CONJ(UNDISCH x64_machine_config_ok)(UNDISCH x64_init_ok))
|> DISCH(#1(dest_imp(concl x64_init_ok)))
|> REWRITE_RULE[AND_IMP_INTRO]
val wordfreq_compiled_lemma =
CONJ compile_correct_applied wordfreq_output
|> SIMP_RULE std_ss [AND_IMP_INTRO,GSYM CONJ_ASSOC]
|> DISCH_ALL;
val compiler_output_def = Define `
compiler_output = (code,data,config)`;
(* TODO: move *)
val get_file_contents_def = Define `
get_file_contents fs fname =
if inFS_fname fs fname then
case ALOOKUP fs.files fname of
| NONE => NONE
| SOME ino =>
case ALOOKUP fs.inode_tbl (File ino) of
| NONE => NONE
| SOME s => SOME (implode s)
else NONE`
val wfFS_def = Define `
wfFS fs <=> fsFFIProps$wfFS fs ∧ STD_streams fs`;
val x64_installed_def = Define `
x64_installed (c,d,conf) cbspace data_sp mc ms <=>
is_x64_machine_config mc ∧
targetSem$installed c cbspace d data_sp conf.lab_conf.ffi_names
(heap_regs x64_backend_config.stack_conf.reg_names) mc conf.lab_conf.shmem_extra ms`
(* -- *)
Theorem wordfreq_compiled_thm:
wfcl [pname; fname] ∧ wfFS fs ∧ hasFreeFD fs ∧
(get_file_contents fs fname = SOME file_contents) ∧
x64_installed compiler_output cbspace data_sp mc ms ⇒
∃io_events ascii_output.
machine_sem mc (basis_ffi [pname; fname] fs) ms ⊆
extend_with_resource_limit {Terminate Success io_events} ∧
(extract_fs fs io_events = SOME (add_stdout fs ascii_output)) ∧
valid_wordfreq_output file_contents ascii_output
Proof
strip_tac
\\ assume_tac wordfreq_compiled_lemma
\\ rfs [get_file_contents_def,wfFS_def,compiler_output_def,x64_installed_def]
\\ asm_exists_tac \\ fs [option_case_eq]
\\ metis_tac [wordfreqProgTheory.wordfreq_output_spec_def]
QED
val _ = export_theory();