Permalink
Browse files

Add Compile and Proof theories for wordcount and wordfreq

  • Loading branch information...
xrchz committed Jun 16, 2017
1 parent 461e7a4 commit 168aae776b0d27704671c757a1bb16735eedf40f
@@ -1 +1,2 @@
INCLUDES = $(HOLDIR)/examples/balanced_bst .. ../translator ../basis/pure ../basis ../characteristic ../compiler
INCLUDES = $(HOLDIR)/examples/balanced_bst .. ../translator ../basis/pure ../basis ../characteristic ../compiler\
../semantics/proofs ../compiler/backend/proofs ../compiler/backend/x64/proofs
@@ -0,0 +1,17 @@
(*
Compile the wordcount program to machine code by evaluation of the compiler
in the logic.
*)

open preamble wordcountProgTheory compilationLib

val _ = new_theory"wordcountCompile";

val wordcount_compiled = save_thm("wordcount_compiled",
compile_x64
1000 (* stack size in MB *)
1000 (* heap size in MB *)
"wordcount"
wordcount_prog_def);

val _ = export_theory();
@@ -0,0 +1,24 @@
open preamble
semanticsPropsTheory backendProofTheory x64_configProofTheory
wordcountProgTheory wordcountCompileTheory

val _ = new_theory"wordcountProof";

val wordcount_io_events_def = new_specification("wordcount_io_events_def",["wordcount_io_events"],
wordcount_semantics |> Q.GENL(List.rev[`inp`,`cls`,`files`]) |> SIMP_RULE bool_ss [SKOLEM_THM]);

val (wordcount_sem,wordcount_output) = wordcount_io_events_def |> SPEC_ALL |> 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 x64_conf_ok
|> C MATCH_MP wordcount_not_fail
|> REWRITE_RULE[wordcount_sem_sing]

val wordcount_compiled_thm =
CONJ compile_correct_applied wordcount_output
|> curry save_thm "wordcount_compiled_thm";

val _ = export_theory();
@@ -0,0 +1,24 @@
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(List.rev[`inp`,`cls`,`files`]) |> SIMP_RULE bool_ss [SKOLEM_THM]);

val (wordfreq_sem,wordfreq_output) = wordfreq_io_events_def |> SPEC_ALL |> 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 x64_conf_ok
|> C MATCH_MP wordfreq_not_fail
|> REWRITE_RULE[wordfreq_sem_sing]

val wordfreq_compiled_thm =
CONJ compile_correct_applied wordfreq_output
|> curry save_thm "wordfreq_compiled_thm";

val _ = export_theory();

0 comments on commit 168aae7

Please sign in to comment.