Permalink
Browse files

Merge pull request #612 from CakeML/cleanup

Cleanup
  • Loading branch information...
xrchz committed Jan 28, 2019
2 parents a8381c3 + d424ed8 commit be8c718bd26f8f7df6310ab4c48d33c300c1d23a
Showing with 622 additions and 953 deletions.
  1. +3 −3 basis/TextIOProofScript.sml
  2. +1 −1 basis/pure/mlstringScript.sml
  3. +2 −2 basis/pure/mlvectorScript.sml
  4. +0 −9 compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml
  5. +9 −8 compiler/backend/bvl_to_bviScript.sml
  6. +5 −3 compiler/backend/clos_annotateScript.sml
  7. +4 −4 compiler/backend/proofs/backendProofScript.sml
  8. +7 −7 compiler/backend/proofs/bvl_inlineProofScript.sml
  9. +2 −2 compiler/backend/proofs/bvl_to_bviProofScript.sml
  10. +13 −10 compiler/backend/proofs/clos_annotateProofScript.sml
  11. +18 −11 compiler/backend/proofs/clos_callProofScript.sml
  12. +8 −8 compiler/backend/proofs/clos_knownProofScript.sml
  13. +2 −1 compiler/backend/proofs/clos_labelsProofScript.sml
  14. +24 −29 compiler/backend/proofs/clos_letopProofScript.sml
  15. +2 −1 compiler/backend/proofs/clos_ticksProofScript.sml
  16. +76 −72 compiler/backend/proofs/clos_to_bvlProofScript.sml
  17. +2 −27 compiler/backend/proofs/data_to_word_memoryProofScript.sml
  18. +70 −61 compiler/backend/proofs/flat_exh_matchProofScript.sml
  19. +5 −5 compiler/backend/proofs/lab_to_targetProofScript.sml
  20. +1 −1 compiler/backend/proofs/pat_to_closProofScript.sml
  21. +7 −7 compiler/backend/proofs/source_to_flatProofScript.sml
  22. +3 −2 compiler/backend/proofs/stack_allocProofScript.sml
  23. +1 −1 compiler/backend/reg_alloc/parmoveScript.sml
  24. +1 −1 compiler/backend/semantics/bviPropsScript.sml
  25. +1 −1 compiler/backend/semantics/bvlPropsScript.sml
  26. +8 −17 compiler/backend/semantics/labPropsScript.sml
  27. +9 −9 compiler/backend/stack_allocScript.sml
  28. +4 −4 compiler/backend/stack_namesScript.sml
  29. +5 −5 compiler/backend/stack_to_labScript.sml
  30. +4 −4 compiler/inference/inferScript.sml
  31. +52 −46 compiler/inference/proofs/inferCompleteScript.sml
  32. +3 −0 misc/README.md
  33. +3 −2 misc/basicComputeLib.sml
  34. +236 −0 misc/byteScript.sml
  35. +13 −573 misc/miscScript.sml
  36. +6 −5 misc/preamble.sml
  37. +10 −9 semantics/proofs/evaluatePropsScript.sml
  38. +2 −2 semantics/proofs/semanticPrimitivesPropsScript.sml
@@ -1368,7 +1368,7 @@ Theorem read_byte_spec
fs[EndOfFile_exn_def,eof_def,get_file_content_def,liveFS_bumpFD] >> xsimpl) >>
xapp >> xsimpl >>
`nr = 1` by fs[] >> fs[] >> xsimpl >>
fs[take1_drop,eof_def,get_file_content_def] >> pairarg_tac >> fs[liveFS_bumpFD]);
fs[TAKE1_DROP,eof_def,get_file_content_def] >> pairarg_tac >> fs[liveFS_bumpFD]);

Theorem read_byte_STDIO_spec
` FD fd fdv ∧ fd ≠ 1 ∧ fd ≠ 2
@@ -1889,7 +1889,7 @@ Theorem inputLine_spec
\\ `x = pp - pos` by fs[]
\\ rw[] )
\\ unabbrev_all_tac \\ simp[DROP_DROP]
\\ simp[take1_drop,CHAR_EQ_THM] \\ xsimpl )
\\ simp[TAKE1_DROP,CHAR_EQ_THM] \\ xsimpl )
\\ fs[forwardFD_o,STDIO_numchars]
\\ xsimpl
\\ conj_asm1_tac
@@ -1921,7 +1921,7 @@ Theorem inputLine_spec
\\ pop_assum SUBST_ALL_TAC
\\ rewrite_tac[TAKE_SUM]
\\ simp[]
\\ simp[take1_drop,EL_DROP,CHAR_EQ_THM]
\\ simp[TAKE1_DROP,EL_DROP,CHAR_EQ_THM]
\\ unabbrev_all_tac \\ xsimpl)
\\ xlet_auto >- xsimpl
\\ xlet_auto >- xsimpl
@@ -601,7 +601,7 @@ val compare_aux_spec = Q.prove (
Cases_on `s2` >>
fs [] >>
full_simp_tac (srw_ss()) [TAKE_SUM, DECIDE ``!n. SUC n = 1 + n``] >>
fs [take1_drop, DROP_DROP_T, char_lt_def] >>
fs [TAKE1_DROP, DROP_DROP_T, char_lt_def] >>
fs [string_lt_def] >>
simp [] >>
rw [] >>
@@ -157,7 +157,7 @@ val foldri_aux_thm = Q.prove (
(foldri_aux f e vec len = FOLDRi f e (TAKE len (toList vec)))`,
Induct_on `len` \\ rw[foldri_aux_def] \\
Cases_on `vec` \\ fs[length_def, toList_thm, sub_def] \\
rw [ADD1, TAKE_SUM, take1_drop, FOLDRi_APPEND]
rw [ADD1, TAKE_SUM, TAKE1_DROP, FOLDRi_APPEND]
);

Theorem foldri_thm
@@ -180,7 +180,7 @@ val foldr_aux_thm = Q.prove (
(foldr_aux f e vec len = FOLDR f e (TAKE len (toList vec)))`,
Induct_on `len` \\ rw[foldr_aux_def] \\
Cases_on `vec` \\ fs[length_def, toList_thm, sub_def] \\
rw [ADD1, TAKE_SUM, take1_drop, FOLDR_APPEND]
rw [ADD1, TAKE_SUM, TAKE1_DROP, FOLDR_APPEND]
);

Theorem foldr_thm
@@ -451,15 +451,6 @@ Theorem align_eq_0_imp
\\ fs[MULT]
*)

Theorem words_of_bytes_append_word
`0 < LENGTH l1 ∧ (LENGTH l1 = w2n (bytes_in_word:'a word)) ⇒
(words_of_bytes be (l1 ++ l2) = word_of_bytes be (0w:'a word) l1 :: words_of_bytes be l2)`
(rw[]
\\ Cases_on`l1` \\ rw[words_of_bytes_def] \\ fs[]
\\ fs[MAX_DEF]
\\ first_x_assum(assume_tac o SYM) \\ fs[ADD1]
\\ rw[TAKE_APPEND,DROP_APPEND,DROP_LENGTH_NIL] \\ fs[]);

Theorem asm_step_target_configured
`asm_step c s1 i s2 ∧ target_configured s1 mc ⇒
target_configured s2 mc`
@@ -239,15 +239,16 @@ local val compile_op_quotation = `
| Label l => Op (Label (bvl_num_stubs + bvl_to_bvi_namespaces * l)) c1
| _ => Op op c1`
in
val compile_op_def = Define compile_op_quotation

Theorem compile_op_pmatch (`∀op c1.` @
(compile_op_quotation |>
map (fn QUOTE s => Portable.replace_string {from="dtcase",to="case"} s |> QUOTE
| aq => aq)))
(rpt strip_tac
val compile_op_def = Define compile_op_quotation;

Theorem compile_op_pmatch (Q.prove(
`∀op c1.` @
(compile_op_quotation |>
map (fn QUOTE s => Portable.replace_string {from="dtcase",to="case"} s |> QUOTE
| aq => aq)),
rpt strip_tac
>> rpt(CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV) >> every_case_tac)
>> fs[compile_op_def])
>> fs[compile_op_def]));
end

val _ = temp_overload_on("++",``SmartAppend``);
@@ -207,9 +207,11 @@ Theorem shift_CONS
(HD c1 :: c2:closLang$exp list)`
(Cases_on `xs` \\ fs [shift_def,LET_DEF,SING_HD,shift_LENGTH_LEMMA]);

Theorem HD_shift[simp]
`[HD (shift [x] m l i)] = shift [x] m l i`
(STRIP_ASSUME_TAC shift_SING \\ fs []);
Theorem HD_shift[simp]:
LENGTH (shift [x] m l i) = 1
[HD (shift [x] m l i)] = shift [x] m l i
Proof STRIP_ASSUME_TAC shift_SING \\ fs []
QED

(* main functions *)

@@ -516,7 +516,7 @@ Theorem compile_correct
\\ qid_spec_tac`x`
\\ simp[GSYM EVERY_MEM]
\\ irule flat_to_patProofTheory.compile_esgc_free
\\ simp[EVERY_o]
\\ simp[GSYM ALL_EL_MAP]
\\ irule source_to_flatProofTheory.compile_esgc_free
\\ asm_exists_tac \\ rw[]
\\ EVAL_TAC
@@ -571,7 +571,7 @@ Theorem compile_correct
\\ impl_tac >- (
EVAL_TAC \\ Cases \\ simp[namespaceTheory.nsLookup_def] )
\\ rw[]
\\ simp[bag_of_list_ALL_DISTINCT]
\\ simp[LIST_TO_BAG_DISTINCT]
\\ irule ALL_DISTINCT_MAP_INJ
\\ simp[]
\\ simp[all_distinct_count_list])
@@ -1665,7 +1665,7 @@ Theorem compile_correct
\\ EVAL_TAC \\ simp[])
\\ simp[Q.SPEC`P o FST`(INST_TYPE[alpha|->``:'a # 'b``]EVERY_CONJ)
|> Q.SPEC`Q o SND` |> SIMP_RULE (srw_ss()) [LAMBDA_PROD]]
\\ simp[EVERY_o, GSYM CONJ_ASSOC]
\\ simp[GSYM ALL_EL_MAP, GSYM CONJ_ASSOC]
\\ simp[MAP_MAP_o, o_DEF]
\\ qpat_x_assum`Abbrev(bmk = _)`mp_tac
\\ simp[PAIR_MAP]
@@ -1718,7 +1718,7 @@ Theorem compile_correct
\\ simp[EVERY_MAP]
\\ simp[word_to_wordTheory.full_compile_single_def, UNCURRY]
\\ simp[Once(GSYM o_DEF)]
\\ simp[EVERY_o]
\\ simp[GSYM ALL_EL_MAP]
\\ qpat_assum`∀n. EVERY ($<= _) _`mp_tac
\\ disch_then(qspec_then`n`strip_assume_tac)
\\ conj_tac
@@ -680,7 +680,7 @@ Theorem tick_compile_prog_res_range
\\ reverse conj_tac THEN1 metis_tac []
\\ fs [subspt_alt,lookup_insert] \\ rw []
\\ fs [lookup_union,lookup_insert,lookup_def,case_eq_thms]
\\ metis_tac [not_in_domain])
\\ metis_tac [lookup_NONE_domain])
\\ fs [GSYM union_assoc]
\\ match_mp_tac subspt_union_lemma
\\ fs [lookup_union,lookup_insert,lookup_def,fromAList_def]
@@ -791,12 +791,12 @@ val tick_compile_prog_IMP_exp_rel = prove(
\\ fs [lookup_insert,case_eq_thms] \\ rveq
THEN1
(rename1 `must_inline k2 _ _`
\\ fs [lookup_union,case_eq_thms,not_in_domain]
\\ fs [lookup_union,case_eq_thms,GSYM lookup_NONE_domain]
\\ match_mp_tac subspt_exp_rel
\\ qexists_tac `src_code`
\\ conj_tac THEN1 fs [subspt_alt,lookup_union]
\\ match_mp_tac exp_rel_tick_inline \\ metis_tac [])
\\ fs [lookup_union,case_eq_thms,not_in_domain,lookup_insert,lookup_def]
\\ fs [lookup_union,case_eq_thms,GSYM lookup_NONE_domain,lookup_insert,lookup_def]
\\ pop_assum (assume_tac o GSYM)
\\ first_x_assum drule \\ strip_tac \\ fs []
\\ match_mp_tac (subspt_exp_rel |> ONCE_REWRITE_RULE [CONJ_COMM])
@@ -1053,7 +1053,7 @@ val lookup_tick_inline_all = prove(
\\ IF_CASES_TAC \\ rw []
THEN1 (match_mp_tac exp_rel_tick_inline
\\ fs [lookup_insert,lookup_union]
\\ rw [] \\ fs [not_in_domain]
\\ rw [] \\ fs [GSYM lookup_NONE_domain]
\\ first_x_assum drule \\ fs [] \\ strip_tac \\ fs [])
\\ fs [] \\ rveq
\\ qmatch_goalsub_abbrev_tac `tick_inline_all _ cs1`
@@ -1072,16 +1072,16 @@ val lookup_tick_inline_all = prove(
\\ imp_res_tac ALOOKUP_MEM \\ fs [MEM_MAP,FORALL_PROD] \\ rfs [])
\\ match_mp_tac exp_rel_tick_inline
\\ rw [] \\ first_x_assum drule
\\ IF_CASES_TAC THEN1 fs [not_in_domain]
\\ IF_CASES_TAC THEN1 fs [GSYM lookup_NONE_domain]
\\ fs [case_eq_thms] \\ strip_tac
\\ fs [lookup_union,lookup_insert,lookup_fromAList]
\\ rfs [exp_rel_rw])
\\ rpt strip_tac \\ first_x_assum drule
\\ fs [lookup_union,lookup_insert]
\\ fs [not_in_domain] \\ fs [exp_rel_rw])
\\ fs [GSYM lookup_NONE_domain] \\ fs [exp_rel_rw])
\\ rpt strip_tac \\ first_x_assum drule
\\ fs [lookup_union,lookup_insert]
\\ IF_CASES_TAC \\ fs [not_in_domain] \\ fs [exp_rel_rw]);
\\ IF_CASES_TAC \\ fs [GSYM lookup_NONE_domain] \\ fs [exp_rel_rw]);

val subspt_tick_inline = prove(
``!prog cs aux.
@@ -3878,7 +3878,7 @@ Theorem compile_semantics
\\ imp_res_tac bvl_inlineProofTheory.compile_prog_names
\\ drule bvi_tailrecProofTheory.compile_prog_next_mono
\\ strip_tac \\ fs [])
\\ fs [bvi_tailrecProofTheory.input_condition_def,EVERY_o]
\\ fs [bvi_tailrecProofTheory.input_condition_def,GSYM ALL_EL_MAP]
\\ fs [GSYM in_ns_def,EVAL ``in_ns 2 2``]
\\ conj_asm1_tac
>- (
@@ -4059,7 +4059,7 @@ Theorem ALL_DISTINCT_MAP_FST_SND_full_co
\\ simp[bvl_inlineProofTheory.MAP_FST_tick_inline_all] )
\\ rw[]
\\ drule (GEN_ALL compile_inc_next_range)
\\ simp[MEM_MAP, PULL_EXISTS, EVERY_o, EVERY_MEM, EXISTS_PROD]
\\ simp[MEM_MAP, PULL_EXISTS, GSYM ALL_EL_MAP, EVERY_MEM, EXISTS_PROD]
\\ rpt strip_tac
\\ first_x_assum drule
\\ simp[bvi_tailrecProofTheory.free_names_def]
@@ -1,6 +1,7 @@
(*
Correctness proof for clos_annotate
*)

open preamble
db_varsTheory
closSemTheory closPropsTheory
@@ -373,14 +374,15 @@ Theorem v_to_words
\\ fs[LIST_EQ_REWRITE,EL_MAP,LIST_REL_EL_EQN] \\ rfs[EL_MAP]
\\ METIS_TAC[EL_MAP,o_DEF]);

Theorem do_install_thm
`state_rel s1 t1 /\ LIST_REL v_rel xs ys /\
do_install xs s1 = (res1,s2) /\
do_install ys t1 = (res2,t2)
==>
result_rel (λe1 e2. e2 = (annotate 0 e1)) (=) res1 res2 /\
state_rel s2 t2`
(fs[do_install_def]
Theorem do_install_thm:
state_rel s1 t1 /\ LIST_REL v_rel xs ys /\
do_install xs s1 = (res1,s2) /\
do_install ys t1 = (res2,t2)
==>
result_rel (λe1 e2. e2 = (annotate 0 e1)) (=) res1 res2 /\
state_rel s2 t2
Proof
fs[do_install_def]
\\ simp[CaseEq"list",CaseEq"prod",CaseEq"option"]
\\ strip_tac \\ rveq \\ fs[]
\\ imp_res_tac v_to_words
@@ -403,7 +405,7 @@ Theorem do_install_thm
\\ `annotate 0 es = [] ⇔ es = []` by (
simp[annotate_def]
\\ rewrite_tac[GSYM LENGTH_NIL]
\\ rewrite_tac[shift_LENGTH_LEMMA, LENGTH_FST_alt_free] )
\\ rewrite_tac[shift_LENGTH_LEMMA, LENGTH_FST_alt_free])
\\ fs[]
\\ fs[CaseEq"bool"] \\ rveq \\ fs[] \\ rw[]
THEN (
@@ -414,7 +416,8 @@ Theorem do_install_thm
\\ TOP_CASE_TAC \\ fs[]
\\ simp[annotate_def]
\\ Cases_on`alt_free [c]`
\\ imp_res_tac alt_free_SING \\ fs[]));
\\ imp_res_tac alt_free_SING \\ fs[])
QED

(* compiler correctness *)

@@ -1,10 +1,10 @@
(*
Correctness proof for clos_call
*)
open preamble backendPropsTheory match_goal dep_rewrite

open preamble backendPropsTheory match_goal
closSemTheory closPropsTheory
clos_callTheory
db_varsTheory;
clos_callTheory db_varsTheory

val _ = new_theory"clos_callProof";

@@ -307,7 +307,7 @@ val wfv_ind = theorem"wfv_ind";

val wfv_state_def = Define`
wfv_state g l code s ⇔
EVERY (OPTION_EVERY (wfv g l code)) s.globals ∧
EVERY (OPTION_ALL (wfv g l code)) s.globals ∧
FEVERY (every_refv (wfv g l code) o SND) s.refs ∧
s.code = FEMPTY`;

@@ -1485,7 +1485,7 @@ Theorem wfv_state_SUBMAP
wfv_state g1 l1 code s /\ code SUBMAP code1 ==>
wfv_state g1 l1 code1 s`
(rw[wfv_state_def, EVERY_MEM, FEVERY_ALL_FLOOKUP]
\\ metis_tac[OPTION_EVERY_mono, wfv_SUBMAP, every_refv_def,
\\ metis_tac[OPTION_ALL_MONO, wfv_SUBMAP, every_refv_def,
MONO_EVERY, ref_nchotomy]);

Theorem v_rel_SUBMAP
@@ -2049,8 +2049,8 @@ max_print_depth := 800
fun say0 pfx s g = (print (pfx ^ ": " ^ s ^ "\n"); ALL_TAC g)
val say = say0 "calls_correct";

Theorem calls_correct
`(∀tmp xs env1 s0 g0 g env2 ^t0 ys res s l l1 g1.
Theorem calls_correct:
(∀tmp xs env1 s0 g0 g env2 ^t0 ys res s l l1 g1.
tmp = (xs,env1,s0) ∧
evaluate (xs,env1,s0) = (res,s) ∧
res ≠ Rerr (Rabort Rtype_error) ∧
@@ -2093,8 +2093,9 @@ Theorem calls_correct
state_rel g l s t ∧
code_inv (SOME g) s.code s.compile s.compile_oracle
t.code t.compile t.compile_oracle ∧
result_rel (LIST_REL (v_rel g l t.code)) (v_rel g l t.code) res res')`
(ho_match_mp_tac evaluate_ind
result_rel (LIST_REL (v_rel g l t.code)) (v_rel g l t.code) res res')
Proof
ho_match_mp_tac evaluate_ind
\\ conj_tac >- (
rw[]
\\ qexists_tac`0`
@@ -2512,6 +2513,8 @@ Theorem calls_correct
\\ IF_CASES_TAC \\ fs [] \\ ntac 2 strip_tac
\\ first_x_assum match_mp_tac
\\ pop_assum mp_tac \\ EVAL_TAC)
\\ `[HD e1] = e1` by (imp_res_tac calls_sing \\ fs [])
\\ pop_assum SUBST_ALL_TAC
\\ Cases_on `q` \\ fs [] \\ rveq \\ fs []
\\ imp_res_tac evaluate_SING \\ rveq \\ fs []
\\ strip_tac \\ fs []
@@ -3565,13 +3568,16 @@ Theorem calls_correct
\\ imp_res_tac calls_sing \\ fs [])
\\ strip_tac \\ fs []
\\ fs [PUSH_EXISTS_IMP,GSYM PULL_EXISTS] \\ rw [] \\ fs []
\\ `[HD e1] = e1` by (imp_res_tac calls_sing \\ fs []) \\ fs []
\\ `[HD e1] = e1` by (imp_res_tac calls_sing \\ fs [])
\\ pop_assum SUBST_ALL_TAC
\\ `t0.clock = s.clock` by fs [state_rel_def]
\\ fs [evaluate_def]
\\ qexists_tac `ck` \\ fs [dec_clock_def]
\\ `ck + s.clock − 1 = ck + (s.clock − 1)` by decide_tac
\\ qpat_x_assum `_ = (_,_)` mp_tac
\\ pop_assum (fn th => simp_tac std_ss [th])
\\ `[HD e1] = e1` by (imp_res_tac calls_sing \\ fs [])
\\ pop_assum SUBST_ALL_TAC
\\ fs [])
(* Call *)
\\ conj_tac >- (
@@ -3984,7 +3990,8 @@ Theorem calls_correct
\\ qmatch_assum_abbrev_tac `closSem$evaluate (_,_,(_ with clock := ck11)) = _`
\\ qmatch_goalsub_abbrev_tac `_ with clock := ck22`
\\ qsuff_tac `ck11 = ck22` \\ rw [] \\ fs []
\\ unabbrev_all_tac \\ fs []);
\\ unabbrev_all_tac \\ fs []
QED

val code_locs_calls_list = Q.prove(`
∀ls n tr i. code_locs (MAP SND (calls_list tr i n ls)) = []`,
Oops, something went wrong.

0 comments on commit be8c718

Please sign in to comment.