From f5c02e54ff19dd9c1f1add7fc3096d343d654ad8 Mon Sep 17 00:00:00 2001 From: Yong Kiam Date: Wed, 16 Aug 2023 04:36:23 +0200 Subject: [PATCH 1/4] add ARM8 version --- .../lpr_checker/array/compilation/Holmakefile | 15 +- .../lpr_checker/array/compilation/README.md | 7 + .../lpr_arrayCompileARM8Script.sml | 11 + .../compilation/lpr_arrayCompileScript.sml | 2 +- .../lpr_arrayRamseyCompileScript.sml | 2 +- .../array/compilation/proofsARM8/Holmakefile | 15 + .../array/compilation/proofsARM8/README.md | 7 + .../proofsARM8/lpr_arrayProofARM8Script.sml | 599 ++++++++++++++++++ .../array/compilation/proofsARM8/readmePrefix | 2 + 9 files changed, 647 insertions(+), 13 deletions(-) create mode 100644 examples/lpr_checker/array/compilation/lpr_arrayCompileARM8Script.sml create mode 100644 examples/lpr_checker/array/compilation/proofsARM8/Holmakefile create mode 100644 examples/lpr_checker/array/compilation/proofsARM8/README.md create mode 100644 examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml create mode 100644 examples/lpr_checker/array/compilation/proofsARM8/readmePrefix diff --git a/examples/lpr_checker/array/compilation/Holmakefile b/examples/lpr_checker/array/compilation/Holmakefile index 496ce841c4..161f74b3d3 100644 --- a/examples/lpr_checker/array/compilation/Holmakefile +++ b/examples/lpr_checker/array/compilation/Holmakefile @@ -1,7 +1,7 @@ INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/basis $(CAKEMLDIR)/compiler .. CLINE_OPTIONS = -all: $(DEFAULT_TARGETS) README.md exec +all: $(DEFAULT_TARGETS) README.md .PHONY: all README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) @@ -9,13 +9,6 @@ DIRS = $(wildcard */) README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES) $(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES) -ifndef CC -CC=gcc -endif -lpr_array.S: *lpr_arrayCompileScript.sml -lpr_ramsey.S: *lpr_arrayRamseyCompileScript.sml -cake_lpr_array: lpr_array.S $(CAKEMLDIR)/basis/basis_ffi.o - $(CC) $< $(protect $(CAKEMLDIR)/basis/basis_ffi.o) $(GCCFLAGS) -o $@ - -exec: cake_lpr_array -.PHONY: exec +cake_lpr.S: *lpr_arrayCompileScript.sml +cake_lpr_arm8.S: *lpr_arrayRamseyCompileScript.sml +cake_lpr_ramsey.S: *lpr_arrayRamseyCompileScript.sml diff --git a/examples/lpr_checker/array/compilation/README.md b/examples/lpr_checker/array/compilation/README.md index c0b01e6a88..dd27eee706 100644 --- a/examples/lpr_checker/array/compilation/README.md +++ b/examples/lpr_checker/array/compilation/README.md @@ -1,5 +1,8 @@ An LRAT checker built on CakeML with arrays +[lpr_arrayCompileARM8Script.sml](lpr_arrayCompileARM8Script.sml): +Compiles the lpr example by evaluation inside the logic of HOL + [lpr_arrayCompileScript.sml](lpr_arrayCompileScript.sml): Compiles the lpr example by evaluation inside the logic of HOL @@ -11,3 +14,7 @@ Compiles the lpr example by evaluation inside the logic of HOL [proofs](proofs): Prove end-to-end correctness theorem for LPR checker with arrays + +[proofsARM8](proofsARM8): +Prove end-to-end correctness theorem for LPR checker with arrays +against ARM8 model diff --git a/examples/lpr_checker/array/compilation/lpr_arrayCompileARM8Script.sml b/examples/lpr_checker/array/compilation/lpr_arrayCompileARM8Script.sml new file mode 100644 index 0000000000..7fef52b730 --- /dev/null +++ b/examples/lpr_checker/array/compilation/lpr_arrayCompileARM8Script.sml @@ -0,0 +1,11 @@ +(* + Compiles the lpr example by evaluation inside the logic of HOL +*) +open preamble compilationLib lpr_arrayFullProgTheory + +val _ = new_theory "lpr_arrayCompileARM8" + +val lpr_array_compiled = save_thm("lpr_array_compiled", + compile_arm8 "cake_lpr_arm8" check_unsat_prog_def); + +val _ = export_theory (); diff --git a/examples/lpr_checker/array/compilation/lpr_arrayCompileScript.sml b/examples/lpr_checker/array/compilation/lpr_arrayCompileScript.sml index 2f59004eba..e8918b2031 100644 --- a/examples/lpr_checker/array/compilation/lpr_arrayCompileScript.sml +++ b/examples/lpr_checker/array/compilation/lpr_arrayCompileScript.sml @@ -6,6 +6,6 @@ open preamble compilationLib lpr_arrayFullProgTheory val _ = new_theory "lpr_arrayCompile" val lpr_array_compiled = save_thm("lpr_array_compiled", - compile_x64 "lpr_array" check_unsat_prog_def); + compile_x64 "cake_lpr" check_unsat_prog_def); val _ = export_theory (); diff --git a/examples/lpr_checker/array/compilation/lpr_arrayRamseyCompileScript.sml b/examples/lpr_checker/array/compilation/lpr_arrayRamseyCompileScript.sml index f35335bce4..ebcd4b0e4c 100644 --- a/examples/lpr_checker/array/compilation/lpr_arrayRamseyCompileScript.sml +++ b/examples/lpr_checker/array/compilation/lpr_arrayRamseyCompileScript.sml @@ -6,6 +6,6 @@ open preamble compilationLib lpr_arrayRamseyProgTheory val _ = new_theory "lpr_arrayRamseyCompile" val lpr_array_compiled = save_thm("lpr_ramsey_compiled", - compile_x64 "lpr_ramsey" check_unsat_prog_def); + compile_x64 "cake_lpr_ramsey" check_unsat_prog_def); val _ = export_theory (); diff --git a/examples/lpr_checker/array/compilation/proofsARM8/Holmakefile b/examples/lpr_checker/array/compilation/proofsARM8/Holmakefile new file mode 100644 index 0000000000..4ad9d618ea --- /dev/null +++ b/examples/lpr_checker/array/compilation/proofsARM8/Holmakefile @@ -0,0 +1,15 @@ +INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics/proofs\ + $(CAKEMLDIR)/compiler/backend/proofs\ + $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv \ + $(CAKEMLDIR)/compiler/encoders/arm8_asl \ + $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs\ + $(CAKEMLDIR)/compiler/backend/arm8_asl \ + .. ../.. + +all: $(DEFAULT_TARGETS) README.md +.PHONY: all + +README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml) +DIRS = $(wildcard */) +README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES) + $(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES) diff --git a/examples/lpr_checker/array/compilation/proofsARM8/README.md b/examples/lpr_checker/array/compilation/proofsARM8/README.md new file mode 100644 index 0000000000..2b2b1fce8f --- /dev/null +++ b/examples/lpr_checker/array/compilation/proofsARM8/README.md @@ -0,0 +1,7 @@ +Prove end-to-end correctness theorem for LPR checker with arrays +against ARM8 model + +[lpr_arrayProofARM8Script.sml](lpr_arrayProofARM8Script.sml): +Compose the semantics theorem and the compiler correctness +theorem with the compiler evaluation theorem to produce end-to-end +correctness theorem that reaches final machine code. diff --git a/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml b/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml new file mode 100644 index 0000000000..a497e028bd --- /dev/null +++ b/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml @@ -0,0 +1,599 @@ +(* + Compose the semantics theorem and the compiler correctness + theorem with the compiler evaluation theorem to produce end-to-end + correctness theorem that reaches final machine code. +*) +open preamble + semanticsPropsTheory backendProofTheory + arm8_asl_configProofTheory + TextIOProofTheory + satSemTheory lprTheory lpr_listTheory lpr_arrayFullProgTheory + lpr_parsingTheory lpr_arrayCompileARM8Theory lpr_composeProgTheory; + +val _ = new_theory"lpr_arrayProofARM8"; + +val check_unsat_io_events_def = new_specification("check_unsat_io_events_def",["check_unsat_io_events"], + check_unsat_semantics |> Q.GENL[`cl`,`fs`] + |> SIMP_RULE bool_ss [SKOLEM_THM,Once(GSYM RIGHT_EXISTS_IMP_THM)]); + +val (check_unsat_sem,check_unsat_output) = check_unsat_io_events_def |> SPEC_ALL |> UNDISCH |> SIMP_RULE std_ss [GSYM PULL_EXISTS]|> CONJ_PAIR +val (check_unsat_not_fail,check_unsat_sem_sing) = MATCH_MP semantics_prog_Terminate_not_Fail check_unsat_sem |> CONJ_PAIR + +val compile_correct_applied = + MATCH_MP compile_correct lpr_array_compiled + |> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO] + |> C MATCH_MP check_unsat_not_fail + |> C MATCH_MP x64_backend_config_ok + |> REWRITE_RULE[check_unsat_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 check_unsat_compiled_thm = + CONJ compile_correct_applied check_unsat_output + |> DISCH_ALL + (* |> check_thm *) + |> curry save_thm "check_unsat_compiled_thm"; + +(* Prettifying the standard parts of all the theorems *) +val installed_x64_def = Define ` + installed_x64 ((code, data, cfg) : + (word8 list # word64 list # 64 backend$config)) + mc ms + <=> + ?cbspace data_sp. + is_x64_machine_config mc /\ + installed + code cbspace + data data_sp + cfg.lab_conf.ffi_names + (heap_regs x64_backend_config.stack_conf.reg_names) mc ms + `; + +val check_unsat_code_def = Define ` + check_unsat_code = (code, data, config) + `; + +(* A standard run of cake_lpr satisfying all the default assumptions *) +val cake_lpr_run_def = Define` + cake_lpr_run cl fs mc ms ⇔ + wfcl cl ∧ wfFS fs ∧ STD_streams fs ∧ hasFreeFD fs ∧ + installed_x64 check_unsat_code mc ms` + +Theorem concat_success_str: + ∀a b c. concat [strlit "s VERIFIED INTERVALS COVER 0-"; toString (d:num); strlit "\n"] ≠ success_str a b c +Proof + rw[]>> + simp[success_str_def,expected_prefix_def]>> + simp[mlstringTheory.concat_def]>> + qmatch_goalsub_abbrev_tac`STRING #"I" (STRING #"N" lss)`>> + qmatch_goalsub_abbrev_tac`STRING #"R" (STRING #"A" lsss)`>> + EVAL_TAC +QED + +Theorem check_lines_success_str: + check_lines a b c d = INR y ⇒ + y = concat [strlit "s VERIFIED INTERVALS COVER 0-"; toString d; strlit "\n"] ∧ + ∀a b c. y ≠ success_str a b c +Proof + simp[check_lines_def]>> + every_case_tac>>rw[]>> + metis_tac[concat_success_str] +QED + +Theorem machine_code_sound: + cake_lpr_run cl fs mc ms ⇒ + machine_sem mc (basis_ffi cl fs) ms ⊆ + extend_with_resource_limit + {Terminate Success (check_unsat_io_events cl fs)} ∧ + ∃out err. + extract_fs fs (check_unsat_io_events cl fs) = + SOME (add_stdout (add_stderr fs err) out) ∧ + if LENGTH cl = 2 then + if inFS_fname fs (EL 1 cl) + then + case parse_dimacs (all_lines fs (EL 1 cl)) of + NONE => out = strlit "" + | SOME fml => out = concat (print_dimacs fml) + else out = strlit "" + else if LENGTH cl = 3 then + if out = strlit "s VERIFIED UNSAT\n" then + inFS_fname fs (EL 1 cl) ∧ + ∃fml. + parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml ∧ + unsatisfiable (interp fml) + else out = strlit "" + else if LENGTH cl = 4 then + if out = strlit "s VERIFIED TRANSFORMATION\n" then + inFS_fname fs (EL 1 cl) ∧ inFS_fname fs (EL 3 cl) ∧ + ∃fml fml2. + parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml ∧ + parse_dimacs (all_lines fs (EL 3 cl)) = SOME fml2 ∧ + (satisfiable (interp fml) ⇒ satisfiable (interp fml2)) + else out = strlit "" + else if LENGTH cl = 5 then + if ∃cnf_md5 proof_md5 rng. out = success_str cnf_md5 proof_md5 rng then + inFS_fname fs (EL 1 cl) ∧ inFS_fname fs (EL 2 cl) ∧ + inFS_fname fs (EL 4 cl) ∧ + ∃i j fml pf. + out = success_str + (implode (md5 (THE (file_content fs (EL 1 cl))))) + (implode (md5 (THE (file_content fs (EL 2 cl))))) + (print_rng i j) ∧ + parse_rng (EL 3 cl) = SOME (i,j) ∧ + parse_dimacs (all_lines fs (EL 1 cl)) = SOME fml ∧ + parse_proof (all_lines fs (EL 2 cl)) = SOME pf ∧ + i ≤ j ∧ j ≤ LENGTH pf ∧ + (satisfiable (interp (run_proof fml (TAKE i pf))) ⇒ + satisfiable (interp (run_proof fml (TAKE j pf)))) + else if ?n:num. out = concat [strlit "s VERIFIED INTERVALS COVER 0-"; toString n; strlit "\n"] then + inFS_fname fs (EL 1 cl) ∧ inFS_fname fs (EL 2 cl) ∧ inFS_fname fs (EL 4 cl) ∧ + EL 3 cl = strlit "-check" ∧ + check_lines (implode (md5 (THE (file_content fs (EL 1 cl))))) + (implode (md5 (THE (file_content fs (EL 2 cl))))) + (all_lines fs (EL 4 cl)) (LENGTH (all_lines fs (EL 2 cl))) = INR out + else out = strlit "" + else + out = strlit "" +Proof + strip_tac>> + fs[installed_x64_def,check_unsat_code_def,cake_lpr_run_def]>> + drule check_unsat_compiled_thm>> + simp[AND_IMP_INTRO]>> + disch_then drule>> + disch_then (qspecl_then [`ms`,`mc`,`data_sp`,`cbspace`] mp_tac)>> + simp[]>> strip_tac>> + fs[check_unsat_sem_def]>> + Cases_on`cl`>>fs[] + >- ( + (* 0 arg *) + fs[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC >> fs[] >- ( + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC + >- ( + (* 1 arg *) + fs[check_unsat_1_sem_def]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + qexists_tac`strlit ""` >> + simp[STD_streams_stderr,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + (* 2 arg *) + fs[check_unsat_2_sem_def]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + PairCases_on`x`>>fs[]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + qexists_tac`strlit "s VERIFIED UNSAT\n"` >> + qexists_tac`strlit ""`>> simp[]>> + CONJ_TAC >- + metis_tac[STD_streams_stderr,add_stdo_nil]>> + simp[parse_dimacs_def]>> + match_mp_tac (GEN_ALL lpr_arrayProgTheory.check_lpr_unsat_list_sound)>> + asm_exists_tac>>simp[]>> + CONJ_TAC >- ( + match_mp_tac (GEN_ALL parse_dimacs_wf)>>simp[parse_dimacs_def]>> + qexists_tac`all_lines fs h'`>>fs[])>> + metis_tac[parse_lpr_wf])>> + TOP_CASE_TAC>>fs[] + >- ( + (* 3 arg *) + fs[check_unsat_3_sem_def]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + PairCases_on`x`>>fs[]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + PairCases_on`x`>>fs[]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + qexists_tac`strlit "s VERIFIED TRANSFORMATION\n"` >> + qexists_tac`strlit ""`>> simp[]>> + CONJ_TAC >- + metis_tac[STD_streams_stderr,add_stdo_nil]>> + fs[parse_dimacs_def]>> + match_mp_tac (GEN_ALL check_lpr_sat_equiv_list_sound)>> + asm_exists_tac>>simp[]>> + CONJ_TAC >- ( + match_mp_tac (GEN_ALL parse_dimacs_wf)>>simp[parse_dimacs_def]>> + qexists_tac`all_lines fs h'`>>fs[])>> + metis_tac[parse_lpr_wf])>> + TOP_CASE_TAC>>fs[] + >- ( + (* 4 arg *) + `∀a b c. success_str a b c ≠ strlit ""` by (rw[]>>EVAL_TAC)>> + `∀n:num. concat [strlit "s VERIFIED INTERVALS COVER 0-" ; toString n; strlit"\n"] ≠ strlit ""` by + (rw[]>> + qmatch_goalsub_abbrev_tac`_ :: lss`>> + EVAL_TAC)>> + fs[check_unsat_4_sem_def]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`err`>>rw[] >> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + PairCases_on`x`>>fs[]>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit""`>>qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + (* -check option*) + >- ( + reverse IF_CASES_TAC + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + qexists_tac`y`>>qexists_tac`strlit ""`>>simp[]>> + CONJ_TAC >- + metis_tac[STD_streams_stderr,add_stdo_nil]>> + drule check_lines_success_str>> + simp[]>> rw[] + >- metis_tac[] + >- (fs[parse_rng_or_check_def]>> + qpat_x_assum`_=SOME (INL _)` mp_tac>>IF_CASES_TAC>>fs[])>> + drule parse_proof_toks_LENGTH>> + rw[]>> + metis_tac[])>> + TOP_CASE_TAC>>fs[]>> + reverse IF_CASES_TAC + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + TOP_CASE_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + reverse IF_CASES_TAC>>fs[] + >- ( + qexists_tac`strlit ""`>>simp[]>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil])>> + qmatch_goalsub_abbrev_tac`success_str a b c`>> + qexists_tac`success_str a b c`>> + qexists_tac`strlit ""`>> simp[]>> + CONJ_TAC >- + metis_tac[STD_streams_stderr,add_stdo_nil]>> + reverse IF_CASES_TAC>- ( + rw[]>> + metis_tac[])>> + fs[parse_dimacs_def,parse_proof_def]>> + rw[]>>fs[]>> + fs[parse_rng_or_check_def]>> + qpat_x_assum`_ = SOME (INR _)` mp_tac>> + IF_CASES_TAC>>fs[]>> + strip_tac>> + match_mp_tac (GEN_ALL check_lpr_range_list_sound)>> + `x1 + 1 = LENGTH x2 +1 ` by ( + fs[parse_dimacs_toks_def]>> + qpat_x_assum `_ = SOME (x0,x1,x2)` mp_tac>> + rpt (pop_assum kall_tac)>> + every_case_tac>>fs[]>> + drule LENGTH_parse_dimacs_body>> + rw[]>> simp[])>> + pop_assum SUBST_ALL_TAC>> + asm_exists_tac>>simp[]>> + fs[GSYM parse_proof_def]>> + drule parse_proof_wf_proof>> + drule parse_lpr_wf>> + simp[]>> + `parse_dimacs (all_lines fs h') = SOME x2` by + fs[parse_dimacs_def]>> + drule parse_dimacs_wf>>simp[])>> + qexists_tac`err`>>rw[]>> + metis_tac[STD_streams_add_stderr, STD_streams_stdout,add_stdo_nil] +QED + +Theorem run_proof_empty: + run_proof fml [] = fml +Proof + EVAL_TAC +QED + +Theorem par_check_sound: + EVERY (λ(cl,fs,mc,ms,i,j). + cake_lpr_run cl fs mc ms ∧ + LENGTH cl = 5 ∧ + inFS_fname fs (EL 1 cl) ∧ inFS_fname fs (EL 2 cl) ∧ + file_content fs (EL 1 cl) = SOME fmlstr ∧ + file_content fs (EL 2 cl) = SOME pfstr ∧ + parse_rng (EL 3 cl) = SOME(i,j) + ) nodes ∧ + parse_dimacs (lines_of (strlit fmlstr)) = SOME fml ∧ + parse_proof (lines_of (strlit pfstr)) = SOME pf ∧ + interval_cover 0 (LENGTH pf) (MAP (λ(cl,fs,mc,ms,i,j). (i,j)) nodes) + ⇒ + EVERY (λ(cl,fs,mc,ms,i,j). + machine_sem mc (basis_ffi cl fs) ms ⊆ + extend_with_resource_limit + {Terminate Success (check_unsat_io_events cl fs)}) nodes ∧ + ( + EVERY (λ(cl,fs,mc,ms,i,j). + extract_fs fs (check_unsat_io_events cl fs) = + SOME (add_stdout fs + (success_str (implode (md5 fmlstr)) (implode (md5 pfstr)) (print_rng i j))) + ) nodes ⇒ + (satisfiable (interp fml) ⇒ + satisfiable (interp (run_proof fml pf))) + ) +Proof + strip_tac>> + `EVERY (λ(cl,fs,mc,ms,i,j). + machine_sem mc (basis_ffi cl fs) ms ⊆ + extend_with_resource_limit + {Terminate Success (check_unsat_io_events cl fs)} ∧ + ∃out err. + extract_fs fs (check_unsat_io_events cl fs) = + SOME (add_stdout (add_stderr fs err) out) ∧ + (out = success_str (implode (md5 fmlstr)) (implode (md5 pfstr)) (print_rng i j) ⇒ + i ≤ j ∧ j ≤ LENGTH pf ∧ + (satisfiable (interp (run_proof fml (TAKE i pf))) ⇒ + satisfiable (interp (run_proof fml (TAKE j pf)))))) nodes` by ( + fs[EVERY_MEM,FORALL_PROD]>> + rw[]>>first_x_assum drule>> + strip_tac>> + drule machine_code_sound>> rpt(disch_then drule)>> + simp[]>> rpt(disch_then drule)>> + rw[]>> + asm_exists_tac>>simp[]>> + pop_assum mp_tac>> + reverse IF_CASES_TAC + >- metis_tac[]>> + strip_tac>> strip_tac>> + imp_res_tac all_lines_lines_of>> + gs[])>> + CONJ_TAC >- ( + pop_assum mp_tac>>match_mp_tac MONO_EVERY>> + simp[FORALL_PROD]>> + metis_tac[])>> + rw[]>> + drule interval_cover_satisfiable>> + disch_then(qspecl_then[`pf`,`fml`] mp_tac)>> + impl_tac>-( + fs[EVERY_MEM,FORALL_PROD,MEM_MAP,EXISTS_PROD,PULL_EXISTS,run_proof_empty]>> + rw[]>>rpt (first_x_assum drule)>> + rw[]>> + gs[SOME_11]>> + fs[cake_lpr_run_def]>> + drule STD_streams_stdout>>rw[]>> + drule add_stdout_inj>> + metis_tac[stdout_add_stderr])>> + simp[] +QED + +val check_successful_def = Define` + check_successful fmlstr pfstr (i:num,j:num) = + ∃cl fs mc ms err. + cake_lpr_run cl fs mc ms ∧ + LENGTH cl = 5 ∧ + inFS_fname fs (EL 1 cl) ∧ inFS_fname fs (EL 2 cl) ∧ + file_content fs (EL 1 cl) = SOME fmlstr ∧ + file_content fs (EL 2 cl) = SOME pfstr ∧ + parse_rng (EL 3 cl) = SOME (i,j) ∧ + extract_fs fs (check_unsat_io_events cl fs) = + SOME (add_stdout (add_stderr fs err) + (success_str (implode (md5 fmlstr)) (implode (md5 pfstr)) (print_rng i j)))` + +Theorem par_check_sound_2: + parse_dimacs (lines_of (strlit fmlstr)) = SOME fml ∧ + parse_proof (lines_of (strlit pfstr)) = SOME pf ∧ + interval_cover 0 (LENGTH pf) ranges ∧ + EVERY (check_successful fmlstr pfstr) ranges ⇒ + (satisfiable (interp fml) ⇒ satisfiable (interp (run_proof fml pf))) +Proof + rw[]>> + drule interval_cover_satisfiable>> + disch_then(qspecl_then[`pf`,`fml`] mp_tac)>> + impl_tac>-( + fs[EVERY_MEM,FORALL_PROD,MEM_MAP,EXISTS_PROD,PULL_EXISTS,run_proof_empty]>> + rw[]>>first_x_assum drule>> + simp[check_successful_def]>>rw[]>> + drule machine_code_sound>> rpt(disch_then drule)>> + simp[]>> rpt(disch_then drule)>> + rw[]>> + pop_assum mp_tac>> + TOP_CASE_TAC>>fs[] + >- ( + imp_res_tac all_lines_lines_of>> + gs[])>> + fs[cake_lpr_run_def]>> + drule STD_streams_stdout>>rw[]>> + drule add_stdout_inj>> + disch_then(qspec_then`out'` mp_tac)>> + metis_tac[stdout_add_stderr])>> + simp[] +QED + +Theorem parse_proof_LENGTH: + parse_proof ls = SOME pf ⇒ + LENGTH pf = LENGTH ls +Proof + simp[parse_proof_def]>> + rw[]>> + drule parse_proof_toks_LENGTH>> + simp[] +QED + +Theorem success_str_inj: + success_str a b c = success_str a b d ⇒ c = d +Proof + rw[success_str_def,expected_prefix_def]>> + pop_assum mp_tac>> + EVAL_TAC>> + rw[]>>simp[]>> + every_case_tac>>fs[] +QED + +val check_successful_par_def = Define` + check_successful_par fmlstr pfstr = + ∃outstr. + (∀out. MEM out outstr ⇒ + (∃cl fs mc ms err. + cake_lpr_run cl fs mc ms ∧ + LENGTH cl = 5 ∧ + inFS_fname fs (EL 1 cl) ∧ inFS_fname fs (EL 2 cl) ∧ + file_content fs (EL 1 cl) = SOME fmlstr ∧ + file_content fs (EL 2 cl) = SOME pfstr ∧ + extract_fs fs (check_unsat_io_events cl fs) = + SOME (add_stdout (add_stderr fs err) out))) ∧ + (∃cl fs mc ms. + cake_lpr_run cl fs mc ms ∧ + LENGTH cl = 5 ∧ + inFS_fname fs (EL 1 cl) ∧ inFS_fname fs (EL 2 cl) ∧ + file_content fs (EL 1 cl) = SOME fmlstr ∧ + file_content fs (EL 2 cl) = SOME pfstr ∧ + all_lines fs (EL 4 cl) = outstr ∧ + extract_fs fs (check_unsat_io_events cl fs) = + SOME (add_stdout fs + (concat [«s VERIFIED INTERVALS COVER 0-» ; toString (LENGTH (lines_of (strlit pfstr))); «\n»])))` + +Theorem par_check_sound_3: + parse_dimacs (lines_of (strlit fmlstr)) = SOME fml ∧ + parse_proof (lines_of (strlit pfstr)) = SOME pf ∧ + check_successful_par fmlstr pfstr ⇒ + (satisfiable (interp fml) ⇒ satisfiable (interp (run_proof fml pf))) +Proof + rw[check_successful_par_def]>> + (* The run with -check *) + drule machine_code_sound>> rpt(disch_then drule)>> + simp[]>> rpt(disch_then drule)>> + rw[]>> + `STD_streams fs` by fs[cake_lpr_run_def]>> + drule STD_streams_stdout>>rw[]>> + drule add_stdout_inj>> + disch_then drule>> + simp[stdout_add_stderr]>> + rw[]>>fs[concat_success_str]>> + qpat_x_assum`if _ then _ else _` mp_tac>> + reverse IF_CASES_TAC>>fs[] + >- + metis_tac[]>> + rw[]>> + drule lpr_composeProgTheory.check_lines_correct>> + rw[]>> + qpat_x_assum`satisfiable _` mp_tac>> + match_mp_tac (GEN_ALL par_check_sound_2)>> + asm_exists_tac>> simp[]>> + asm_exists_tac>> simp[]>> + drule parse_proof_LENGTH>> + imp_res_tac all_lines_lines_of>> + rw[]>> + gs[]>> + asm_exists_tac>> simp[]>> + simp[EVERY_MEM,FORALL_PROD]>> + rw[]>> + fs[SUBSET_DEF]>>first_x_assum drule>> + strip_tac>> + drule MEM_get_ranges>> + disch_then drule>> + simp[GSYM success_str_def]>> + strip_tac>> + (* The run with a given range *) + first_x_assum drule>> + strip_tac >> + simp[check_successful_def]>> + rpt(asm_exists_tac>>simp[])>> + drule machine_code_sound>> + rpt(disch_then drule)>>simp[]>> + strip_tac>>fs[]>> + qmatch_asmsub_abbrev_tac`add_stdout (add_stderr fs' _) ss`>> + `ss = out''` by ( + fs[cake_lpr_run_def]>> + drule STD_streams_stdout>>rw[]>> + drule add_stdout_inj>> + disch_then match_mp_tac>> + metis_tac[stdout_add_stderr])>> + unabbrev_all_tac>>fs[]>> + pop_assum sym_sub_tac>> + pop_assum mp_tac>> + reverse IF_CASES_TAC >- metis_tac[]>> + fs[]>>strip_tac>> + `out = print_rng i j` by + metis_tac[success_str_inj]>> + rveq>> + fs[parse_rng_print_rng]>> + metis_tac[stdout_add_stderr] +QED + +val _ = export_theory(); diff --git a/examples/lpr_checker/array/compilation/proofsARM8/readmePrefix b/examples/lpr_checker/array/compilation/proofsARM8/readmePrefix new file mode 100644 index 0000000000..e2701fbbe3 --- /dev/null +++ b/examples/lpr_checker/array/compilation/proofsARM8/readmePrefix @@ -0,0 +1,2 @@ +Prove end-to-end correctness theorem for LPR checker with arrays +against ARM8 model From 31014f68d62b892584c8fa2211335d72dff7fd95 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Wed, 16 Aug 2023 10:47:03 +0800 Subject: [PATCH 2/4] update build-sequence --- developers/build-sequence | 1 + 1 file changed, 1 insertion(+) diff --git a/developers/build-sequence b/developers/build-sequence index a56493ba97..ffb01b77ca 100644 --- a/developers/build-sequence +++ b/developers/build-sequence @@ -108,6 +108,7 @@ examples/lpr_checker examples/lpr_checker/array examples/lpr_checker/array/compilation examples/lpr_checker/array/compilation/proofs +examples/lpr_checker/array/compilation/proofsARM8 examples/opentheory examples/opentheory examples/opentheory/compilation From 2016f1789d050ab9078397cc340505865f4f51e0 Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Wed, 16 Aug 2023 10:48:50 +0800 Subject: [PATCH 3/4] correct ARM8 proof file --- .../proofsARM8/lpr_arrayProofARM8Script.sml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml b/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml index a497e028bd..9060fe8952 100644 --- a/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml +++ b/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml @@ -23,11 +23,11 @@ val compile_correct_applied = MATCH_MP compile_correct lpr_array_compiled |> SIMP_RULE(srw_ss())[LET_THM,ml_progTheory.init_state_env_thm,GSYM AND_IMP_INTRO] |> C MATCH_MP check_unsat_not_fail - |> C MATCH_MP x64_backend_config_ok + |> C MATCH_MP arm8_configProofTheory.arm8_backend_config_ok |> REWRITE_RULE[check_unsat_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))) + |> C MATCH_MP (CONJ(UNDISCH arm8_asl_machine_config_ok)(UNDISCH arm8_asl_init_ok)) + |> DISCH(#1(dest_imp(concl arm8_asl_init_ok))) |> REWRITE_RULE[AND_IMP_INTRO] val check_unsat_compiled_thm = @@ -37,18 +37,18 @@ val check_unsat_compiled_thm = |> curry save_thm "check_unsat_compiled_thm"; (* Prettifying the standard parts of all the theorems *) -val installed_x64_def = Define ` - installed_x64 ((code, data, cfg) : +val installed_arm8_asl_def = Define ` + installed_arm8_asl ((code, data, cfg) : (word8 list # word64 list # 64 backend$config)) mc ms <=> ?cbspace data_sp. - is_x64_machine_config mc /\ + is_arm8_asl_machine_config mc /\ installed code cbspace data data_sp cfg.lab_conf.ffi_names - (heap_regs x64_backend_config.stack_conf.reg_names) mc ms + (heap_regs arm8_backend_config.stack_conf.reg_names) mc ms `; val check_unsat_code_def = Define ` @@ -59,7 +59,7 @@ val check_unsat_code_def = Define ` val cake_lpr_run_def = Define` cake_lpr_run cl fs mc ms ⇔ wfcl cl ∧ wfFS fs ∧ STD_streams fs ∧ hasFreeFD fs ∧ - installed_x64 check_unsat_code mc ms` + installed_arm8_asl check_unsat_code mc ms` Theorem concat_success_str: ∀a b c. concat [strlit "s VERIFIED INTERVALS COVER 0-"; toString (d:num); strlit "\n"] ≠ success_str a b c @@ -138,7 +138,7 @@ Theorem machine_code_sound: out = strlit "" Proof strip_tac>> - fs[installed_x64_def,check_unsat_code_def,cake_lpr_run_def]>> + fs[installed_arm8_asl_def,check_unsat_code_def,cake_lpr_run_def]>> drule check_unsat_compiled_thm>> simp[AND_IMP_INTRO]>> disch_then drule>> From 70c9116352cfd04905fbfb3bd8726ca1aaec0f1d Mon Sep 17 00:00:00 2001 From: tanyongkiam Date: Wed, 16 Aug 2023 10:50:12 +0800 Subject: [PATCH 4/4] fix Holmakefile --- examples/lpr_checker/array/compilation/Holmakefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/lpr_checker/array/compilation/Holmakefile b/examples/lpr_checker/array/compilation/Holmakefile index 161f74b3d3..8e7cea16c9 100644 --- a/examples/lpr_checker/array/compilation/Holmakefile +++ b/examples/lpr_checker/array/compilation/Holmakefile @@ -10,5 +10,5 @@ README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmeP $(protect $(CAKEMLDIR)/developers/readme_gen) $(README_SOURCES) cake_lpr.S: *lpr_arrayCompileScript.sml -cake_lpr_arm8.S: *lpr_arrayRamseyCompileScript.sml +cake_lpr_arm8.S: *lpr_arrayCompileARM8Script.sml cake_lpr_ramsey.S: *lpr_arrayRamseyCompileScript.sml