From 168aae776b0d27704671c757a1bb16735eedf40f Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Fri, 16 Jun 2017 17:21:34 +1000 Subject: [PATCH] Add Compile and Proof theories for wordcount and wordfreq --- tutorial/Holmakefile | 3 ++- tutorial/wordcountCompileScript.sml | 17 +++++++++++++++++ tutorial/wordcountProofScript.sml | 24 ++++++++++++++++++++++++ tutorial/wordfreqProofScript.sml | 24 ++++++++++++++++++++++++ 4 files changed, 67 insertions(+), 1 deletion(-) create mode 100644 tutorial/wordcountCompileScript.sml create mode 100644 tutorial/wordcountProofScript.sml create mode 100644 tutorial/wordfreqProofScript.sml diff --git a/tutorial/Holmakefile b/tutorial/Holmakefile index 82faf17abc..91b9a2e550 100644 --- a/tutorial/Holmakefile +++ b/tutorial/Holmakefile @@ -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 diff --git a/tutorial/wordcountCompileScript.sml b/tutorial/wordcountCompileScript.sml new file mode 100644 index 0000000000..210963feb4 --- /dev/null +++ b/tutorial/wordcountCompileScript.sml @@ -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(); diff --git a/tutorial/wordcountProofScript.sml b/tutorial/wordcountProofScript.sml new file mode 100644 index 0000000000..f0d5f7325e --- /dev/null +++ b/tutorial/wordcountProofScript.sml @@ -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(); diff --git a/tutorial/wordfreqProofScript.sml b/tutorial/wordfreqProofScript.sml new file mode 100644 index 0000000000..6474f8c6a2 --- /dev/null +++ b/tutorial/wordfreqProofScript.sml @@ -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();