Skip to content
Permalink
Browse files

Move machinecode soundness into readerProgProof

  • Loading branch information...
oskarabrahamsson committed Mar 2, 2019
1 parent 447fe67 commit 465aae4e3ae9643e44fd7bf01bdca6b14c7728fc
@@ -3,7 +3,8 @@
*)
open preamble
semanticsPropsTheory backendProofTheory x64_configProofTheory
readerProgTheory readerCompileTheory
readerProgTheory readerCompileTheory readerProofTheory
readerSoundnessTheory;

val _ = new_theory "readerProgProof";

@@ -14,10 +15,10 @@ val reader_io_events_def = new_specification (
|> SIMP_RULE bool_ss [SKOLEM_THM,GSYM RIGHT_EXISTS_IMP_THM]);

val (reader_sem, reader_output) =
reader_io_events_def |> SPEC_ALL |> UNDISCH |> CONJ_PAIR
reader_io_events_def |> SPEC_ALL |> UNDISCH |> CONJ_PAIR;

val (reader_not_fail, reader_sem_sing) =
MATCH_MP semantics_prog_Terminate_not_Fail reader_sem |> CONJ_PAIR
MATCH_MP semantics_prog_Terminate_not_Fail reader_sem |> CONJ_PAIR;

val compile_correct_applied =
MATCH_MP compile_correct reader_compiled
@@ -29,12 +30,63 @@ val compile_correct_applied =
|> 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]
|> REWRITE_RULE [AND_IMP_INTRO];

val reader_compiled_thm =
Theorem reader_compiled_thm =
CONJ compile_correct_applied reader_output
|> DISCH_ALL
|> check_thm
|> curry save_thm "reader_compiled_thm";
|> check_thm;

(*
* This makes the theorem prettier.
* Does a good alternative already exist somewhere?
*)

val installed_x64_def = Define `
installed_x64 ((code, data, cfg) :
(word8 list # word64 list # 64 lab_to_target$config))
ffi mc ms
<=>
?cbspace data_sp.
is_x64_machine_config mc /\
installed
code cbspace
data data_sp
cfg.ffi_names
ffi
(heap_regs x64_backend_config.stack_conf.reg_names) mc ms
`;

val reader_code_def = Define `
reader_code = (code, data, config)
`;

val _ = Parse.hide "mem";
val mem = ``mem:'U->'U->bool``;

Theorem machine_code_sound
`input_exists fs cl /\ wfcl cl /\ wfFS fs /\ STD_streams fs
==>
(installed_x64 reader_code (basis_ffi cl fs) mc ms
==>
machine_sem mc (basis_ffi cl fs) ms ⊆
extend_with_resource_limit
{Terminate Success (reader_io_events cl fs)}) /\
?fs_out hol_refs s.
extract_fs fs (reader_io_events cl fs) = SOME fs_out /\
(no_errors fs fs_out ==>
reader_main fs init_refs (TL cl) = (fs_out, hol_refs, SOME s) /\
hol_refs.the_context extends init_ctxt /\
fs_out = add_stdout (flush_stdin (TL cl) fs)
(msg_success s hol_refs.the_context) /\
!asl c.
MEM (Sequent asl c) s.thms /\
is_set_theory ^mem
==>
(thyof hol_refs.the_context, asl) |= c)`
(metis_tac [installed_x64_def, reader_code_def, reader_compiled_thm, PAIR,
FST, SND, reader_success_stderr, input_exists_def,
reader_sound]);

val _ = export_theory ();

@@ -1835,7 +1835,7 @@ val no_errors_def = Define `
Theorem reader_success_stderr
`input_exists fs cl /\
STD_streams fs /\
reader_main fs refs cl = (fs', refs', s) /\
reader_main fs refs (TL cl) = (fs', refs', s) /\
no_errors fs fs'
==>
?st. s = SOME st`

0 comments on commit 465aae4

Please sign in to comment.
You can’t perform that action at this time.