forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
wordcountProofScript.sml
38 lines (31 loc) · 1.5 KB
/
wordcountProofScript.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
(*
Constructs the end-to-end correctness theorem for wordcount example
by composing the application-specific correctness theorem, the
compiler evaluation theorem and the compiler correctness theorem.
*)
open preamble
semanticsPropsTheory backendProofTheory x64_configProofTheory
wordcountProgTheory wordcountCompileTheory
val _ = new_theory"wordcountProof";
val _ = temp_clear_overloads_on"STRCAT"; (* " *)
val wordcount_io_events_def = new_specification("wordcount_io_events_def",["wordcount_io_events"],
wordcount_semantics |> Q.GENL[`cl`,`fs`,`contents`,`fs'`]
|> SIMP_RULE bool_ss [SKOLEM_THM,Once(GSYM RIGHT_EXISTS_IMP_THM)]);
val (wordcount_sem,wordcount_output) = wordcount_io_events_def |> SPEC_ALL |> UNDISCH |> CONJ_PAIR
val (wordcount_not_fail,wordcount_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail wordcount_sem |> CONJ_PAIR
val compile_correct_applied =
MATCH_MP compile_correct wordcount_compiled
|> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO]
|> C MATCH_MP wordcount_not_fail
|> C MATCH_MP x64_backend_config_ok
|> REWRITE_RULE[wordcount_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 wordcount_compiled_thm =
CONJ compile_correct_applied wordcount_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "wordcount_compiled_thm";
val _ = export_theory();