Skip to content
Permalink
Browse files

Merge pull request #619 from CakeML/reader-jlamp

Adjust top-level correctness for the OpenTheory reader
  • Loading branch information...
xrchz committed Mar 5, 2019
2 parents 46f86cc + 465aae4 commit 2d7716e211a3e687d5ba9f237de202f78cbc253b
@@ -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 ();

@@ -526,25 +526,24 @@ val _ = (append_prog o process_topdecs) `
end`;

Theorem reader_main_spec
`(!r s. init_reader () refs = (r, s) ==> r = Success ()) /\
(case TL cl of [] => ?inp. stdin fs inp 0 | _ => hasFreeFD fs)
`(?s. init_reader () refs = (Success (), s)) /\
input_exists fs cl
==>
app (p:'ffi ffi_proj) ^(fetch_v "reader_main" (get_ml_prog_state()))
[Conv NONE []]
(COMMANDLINE cl * STDIO fs * HOL_STORE refs)
(POSTv u.
&UNIT_TYPE () u *
STDIO (FST (reader_main fs refs (TL cl))))`
(xcf "reader_main" (get_ml_prog_state())
(xcf "reader_main" (get_ml_prog_state())
\\ reverse (Cases_on `STD_streams fs`)
>- (fs [STDIO_def] \\ xpull)
\\ reverse (Cases_on `wfcl cl`)
>- (fs [COMMANDLINE_def] \\ xpull)
\\ simp [reader_main_def]
\\ Cases_on `init_reader () refs` \\ rw []
\\ xlet_auto
>- (xcon \\ xsimpl)
\\ xlet `POSTv u. STDIO fs * HOL_STORE r * &UNIT_TYPE () u * COMMANDLINE cl`
\\ xlet `POSTv u. STDIO fs * HOL_STORE s * &UNIT_TYPE () u * COMMANDLINE cl`
\\ xsimpl
>-
(xapp
@@ -565,7 +564,7 @@ Theorem reader_main_spec
\\ xsimpl
\\ instantiate
\\ CONV_TAC SWAP_EXISTS_CONV
\\ qexists_tac `r`
\\ qexists_tac `s`
\\ xsimpl \\ fs [])
\\ reverse CASE_TAC \\ fs [LIST_TYPE_def]
>-
@@ -586,15 +585,15 @@ Theorem reader_main_spec
\\ asm_exists_tac \\ fs []
\\ xsimpl
\\ CONV_TAC SWAP_EXISTS_CONV
\\ qexists_tac `r`
\\ qexists_tac `s`
\\ xsimpl \\ fs []);

(* ------------------------------------------------------------------------- *)
(* whole_prog_spec *)
(* ------------------------------------------------------------------------- *)

Theorem reader_whole_prog_spec
`(case TL cl of [] => ?inp. stdin fs inp 0 | _ => hasFreeFD fs)
`input_exists fs cl
==>
whole_prog_spec ^(fetch_v "reader_main" (get_ml_prog_state()))
cl fs (SOME (HOL_STORE init_refs))
@@ -605,17 +604,18 @@ Theorem reader_whole_prog_spec
\\ reverse conj_tac
>-
(fs [reader_main_def, read_file_def, read_stdin_def]
\\ every_case_tac
\\ rpt (PURE_CASE_TAC \\ fs [])
\\ fs [GSYM add_stdo_with_numchars, with_same_numchars]
\\ AP_THM_TAC
\\ AP_TERM_TAC
\\ metis_tac [fastForwardFD_with_numchars, with_same_numchars])
\\ irule
(DISCH_ALL ((MP_CANON (MATCH_MP app_wgframe (UNDISCH reader_main_spec)))))
\\ irule (reader_main_spec
|> UNDISCH |> MATCH_MP app_wgframe
|> MP_CANON |> DISCH_ALL
|> SIMP_RULE (srw_ss()) [])
\\ xsimpl \\ instantiate
\\ xsimpl
\\ CONV_TAC (RESORT_EXISTS_CONV rev)
\\ CONV_TAC SWAP_EXISTS_CONV
\\ qexists_tac `init_refs` \\ xsimpl
\\ Cases_on `init_reader () init_refs`
\\ fs [init_reader_success]);

val _ = add_user_heap_thm HOL_STORE_init_precond;
@@ -7,6 +7,7 @@ open preamble ml_monadBaseTheory
holKernelTheory holKernelProofTheory
holSyntaxTheory holSyntaxExtraTheory
readerTheory reader_initTheory
TextIOProgTheory

val _ = new_theory"readerProof";

@@ -1769,15 +1770,23 @@ Theorem process_line_inv
\\ drule (GEN_ALL readLine_thm)
\\ rpt (disch_then drule) \\ rw []);

val flush_stdin_def = Define `
flush_stdin cl fs =
case cl of
[] => fastForwardFD fs 0
| _ => fs
`;

val _ = export_rewrites ["flush_stdin_def"];

Theorem reader_proves
`reader_main fs init_refs cl = (outp,refs,SOME s)
==>
(!asl c.
MEM (Sequent asl c) s.thms
==>
(thyof refs.the_context, asl) |- c) /\
let fs' = case cl of [] => fastForwardFD fs 0 | _ => fs in
outp = add_stdout fs' (msg_success s refs.the_context) /\
outp = add_stdout (flush_stdin cl fs) (msg_success s refs.the_context) /\
refs.the_context extends init_ctxt`
(rw [reader_main_def, case_eq_thms, read_file_def, read_stdin_def,
bool_case_eq, PULL_EXISTS]
@@ -1792,4 +1801,59 @@ Theorem reader_proves
\\ fs [STATE_def, CONTEXT_def] \\ rveq
\\ fs [EQ_SYM_EQ]);

(* ------------------------------------------------------------------------- *)
(* Some things useful for the top-level soundness theorem, for instance: *)
(* if there was no output on stderr, then reader_main processed all commands *)
(* in the article without errors. *)
(* ------------------------------------------------------------------------- *)

val input_exists_def = Define `
input_exists fs cl =
case TL cl of
[] => ?inp. stdin fs inp 0
| _ => hasFreeFD fs
`;

val _ = export_rewrites ["input_exists_def"];

Theorem readLines_Fail_not_empty
`!ls st refs err refs'.
readLines ls st refs = (Failure (Fail err), refs')
==>
err <> strlit""`
(recInduct readLines_ind
\\ Cases >- rw [Once readLines_def, st_ex_return_def]
\\ rw []
\\ simp [Once readLines_def]
\\ rw [st_ex_return_def, st_ex_bind_def, handle_Fail_def, raise_Fail_def,
case_eq_thms, line_Fail_def, mlstringTheory.concat_def]);

val no_errors_def = Define `
no_errors fs fs' <=>
get_file_content fs 2 = get_file_content fs' 2`;

Theorem reader_success_stderr
`input_exists fs cl /\
STD_streams fs /\
reader_main fs refs (TL cl) = (fs', refs', s) /\
no_errors fs fs'
==>
?st. s = SOME st`
(rw [reader_main_def, read_stdin_def, read_file_def, case_eq_thms,
no_errors_def, msg_bad_name_def, msg_usage_def]
\\ pop_assum mp_tac
\\ fs [case_eq_thms, bool_case_eq] \\ rw [] \\ fs []
\\ imp_res_tac TextIOProofTheory.STD_streams_stderr
\\ fs [TextIOProofTheory.add_stdo_def, TextIOProofTheory.stdo_def,
TextIOProofTheory.up_stdo_def, fsFFITheory.fsupdate_def,
fsFFITheory.get_file_content_def,
fsFFIPropsTheory.fastForwardFD_def, TextIOProofTheory.stdin_def]
\\ fs [libTheory.the_def, UNCURRY, ALIST_FUPDKEY_ALOOKUP, case_eq_thms,
bool_case_eq]
\\ fs [mlstringTheory.concat_thm, msg_bad_name_def]
\\ SELECT_ELIM_TAC \\ fs []
\\ imp_res_tac readLines_Fail_not_empty
\\ Cases_on `e` \\ fs []);

val _ = export_theory();

@@ -7,30 +7,20 @@ open preamble readerProofTheory holSoundnessTheory
val _ = new_theory "readerSoundness";

val _ = Parse.hide "mem";

val mem = ``mem:'U->'U-> bool``;

Theorem reader_sound
`(* assumption about a strong enough set theory (see candle proofs) *)
is_set_theory ^mem ==>
(* if the reader completes a successful run (executes all commands *)
(* in the article file) when started from the initial candle state *)
reader_main fs init_refs cl = (outp,refs,SOME s)
`reader_main fs init_refs cl = (outp,refs,SOME s)
==>
(* anything on the reader theorem stack in the final state s is a *)
(* theorem in the prover context refs.the_context, and ... *)
(!asl c.
MEM (Sequent asl c) s.thms ==> (thyof refs.the_context, asl) |= c) /\
(* the context is the result of a series of legal updates to *)
(* the initial context. *)
refs.the_context extends init_ctxt /\
(* the output consists of a message displaying the context and *)
(* the contents of the theorem stack. *)
let fs' = case cl of [] => fastForwardFD fs 0 | _ => fs in
outp = add_stdout fs' (msg_success s refs.the_context)`
(rpt strip_tac
outp = add_stdout (flush_stdin cl fs) (msg_success s refs.the_context) /\
!asl c.
MEM (Sequent asl c) s.thms /\
is_set_theory ^mem
==>
(thyof refs.the_context, asl) |= c`
(strip_tac
\\ drule (GEN_ALL reader_proves) \\ rw []
\\ rw []
\\ irule proves_sound \\ fs []);

val _ = export_theory ();

0 comments on commit 2d7716e

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