diff --git a/compiler/backend/backendComputeLib.sml b/compiler/backend/backendComputeLib.sml index 9d5d0fc62b..269e841955 100644 --- a/compiler/backend/backendComputeLib.sml +++ b/compiler/backend/backendComputeLib.sml @@ -631,6 +631,7 @@ val add_backend_compset = computeLib.extend_compset (* ---- wordLang inst_select and inst flattening ---- *) ,word_instTheory.three_to_two_reg_def ,word_instTheory.pull_exp_def + ,word_instTheory.is_Lookup_CurrHeap_def ,word_instTheory.inst_select_def ,word_instTheory.inst_select_exp_def ,word_instTheory.flatten_exp_def diff --git a/compiler/backend/data_to_wordScript.sml b/compiler/backend/data_to_wordScript.sml index e69f189be2..db07aa382c 100644 --- a/compiler/backend/data_to_wordScript.sml +++ b/compiler/backend/data_to_wordScript.sml @@ -110,13 +110,13 @@ val ptr_bits_def = Define ` val real_addr_def = Define ` (real_addr (conf:data_to_word$config) r): 'a wordLang$exp = let k = shift (:'a) in - if k <= conf.pad_bits + 1 then - Op Add [Lookup CurrHeap; - Shift Lsr (Var r) (shift_length conf - k)] + let l = shift_length conf in + if k = l ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0 then + Op Add [Lookup CurrHeap; Op Sub [Var r; Const 1w]] + else if k <= conf.pad_bits + 1 then + Op Add [Lookup CurrHeap; Shift Lsr (Var r) (l - k)] else - Op Add [Lookup CurrHeap; - Shift Lsl (Shift Lsr (Var r) - (shift_length conf)) k]` + Op Add [Lookup CurrHeap; Shift Lsl (Shift Lsr (Var r) l) k]` val real_offset_def = Define ` (real_offset (conf:data_to_word$config) r): 'a wordLang$exp = diff --git a/compiler/backend/presLangScript.sml b/compiler/backend/presLangScript.sml index 05264c5849..9ea179ad51 100644 --- a/compiler/backend/presLangScript.sml +++ b/compiler/backend/presLangScript.sml @@ -631,6 +631,8 @@ val stack_prog_to_display_def = Define` store_name_to_display sn] | Set sn n => Item NONE «Set» [store_name_to_display sn; num_to_display n] + | OpCurrHeap b n1 n2 => Item NONE «OpCurrHeap» + [asm_binop_to_display b; num_to_display n1; num_to_display n2] | Call rh tgt eh => Item NONE «Call» [(case rh of | NONE => empty_item «Tail» @@ -762,6 +764,8 @@ val word_prog_to_display_def = tDefine "word_prog_to_display" ` [word_prog_to_display_ret a; option_to_display num_to_display b; list_to_display num_to_display c; word_prog_to_display_handler d]) /\ + (word_prog_to_display (OpCurrHeap b n1 n2) = Item NONE «OpCurrHeap» + [asm_binop_to_display b; num_to_display n1; num_to_display n2]) /\ (word_prog_to_display (Seq prog1 prog2) = Item NONE (strlit "Seq") [word_prog_to_display prog1; word_prog_to_display prog2]) /\ (word_prog_to_display (If cmp n reg p1 p2) = Item NONE (strlit "If") diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml index d335115ed8..8cd56c64ab 100644 --- a/compiler/backend/proofs/data_to_word_assignProofScript.sml +++ b/compiler/backend/proofs/data_to_word_assignProofScript.sml @@ -8474,7 +8474,7 @@ Theorem word_exp_insert: word_exp t (real_addr c m))) Proof fs [wordSemTheory.word_exp_def,real_addr_def] - \\ IF_CASES_TAC \\ fs [] + \\ rpt (IF_CASES_TAC \\ fs []) \\ fs [wordSemTheory.word_exp_def,real_addr_def] \\ fs [lookup_insert] QED diff --git a/compiler/backend/proofs/data_to_word_memoryProofScript.sml b/compiler/backend/proofs/data_to_word_memoryProofScript.sml index 2dd148053c..470a19ddf7 100644 --- a/compiler/backend/proofs/data_to_word_memoryProofScript.sml +++ b/compiler/backend/proofs/data_to_word_memoryProofScript.sml @@ -4609,9 +4609,12 @@ val get_real_addr_def = Define ` let k = shift (:α) in case FLOOKUP st CurrHeap of | SOME (Word curr) => - if k <= conf.pad_bits + 1 - then SOME (curr + (w >>> (shift_length conf - k))) - else SOME (curr + (w >>> (shift_length conf) << k)) + if k = shift_length conf ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0 + then SOME (curr + w - 1w) + else + if k <= conf.pad_bits + 1 + then SOME (curr + (w >>> (shift_length conf - k))) + else SOME (curr + (w >>> (shift_length conf) << k)) | _ => NONE` val get_real_offset_def = Define ` @@ -4619,6 +4622,15 @@ val get_real_offset_def = Define ` if dimindex (:'a) = 32 then SOME (w + bytes_in_word) else SOME (w << 1 + bytes_in_word)` +Triviality or_1: + ∀w. (0 -- 0) w ‖ 1w = 1w :'a word +Proof + fs [fcpTheory.CART_EQ,word_or_def,fcpTheory.FCP_BETA,word_lsl_def, + word_0,word_bits_def] + \\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs [] + \\ rw [] \\ eq_tac \\ rw [] +QED + Theorem get_real_addr_get_addr: heap_length heap <= dimword (:'a) DIV 2 ** shift_length c /\ heap_lookup n heap = SOME anything /\ @@ -4635,6 +4647,23 @@ Proof \\ match_mp_tac LESS_LESS_EQ_TRANS \\ once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs []) + \\ IF_CASES_TAC + THEN1 + (Cases_on ‘w’ + \\ fs [get_lowerbits_def,small_shift_length_def,or_1] + \\ ‘0w = n2w n ≪ shift_length c && 1w’ by + (fs [fcpTheory.CART_EQ,word_and_def,fcpTheory.FCP_BETA,word_lsl_def,word_0] + \\ rewrite_tac [word_1comp_def] + \\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs [] + \\ gvs [good_dimindex_def,shift_def]) + \\ drule (GSYM WORD_ADD_OR) + \\ pop_assum kall_tac + \\ fs [] + \\ gvs [WORD_MUL_LSL,bytes_in_word_def,word_mul_n2w,good_dimindex_def, + dimword_def,shift_def] + \\ qpat_x_assum ‘_ = shift_length _’ (assume_tac o GSYM) + \\ fs []) + \\ pop_assum kall_tac \\ reverse IF_CASES_TAC THEN1 (drule lsl_lsr \\ fs [get_lowerbits_LSL_shift_length] \\ fs [] \\ rw [] diff --git a/compiler/backend/proofs/stack_allocProofScript.sml b/compiler/backend/proofs/stack_allocProofScript.sml index 3b65cde177..10e8dfe62e 100644 --- a/compiler/backend/proofs/stack_allocProofScript.sml +++ b/compiler/backend/proofs/stack_allocProofScript.sml @@ -5215,6 +5215,19 @@ Proof \\ BasicProvers.TOP_CASE_TAC \\ fs[] \\ rw[] \\ imp_res_tac FLOOKUP_SUBMAP \\ fs[] \\ full_simp_tac(srw_ss())[state_component_equality] ) + \\ conj_tac (* OpCurrHeap *) >- ( + fs[Once comp_def,evaluate_def,get_var_def,word_exp_def] + \\ fs [AllCaseEqs(),set_var_def] + \\ full_simp_tac(srw_ss())[state_component_equality] + \\ rw [] \\ fs [PULL_EXISTS] + \\ gs [optionTheory.IS_SOME_EXISTS,AllCaseEqs()] + \\ qpat_x_assum`_ = t.regs`(assume_tac o SYM) \\ fs[] + \\ rename [‘FLOOKUP s.regs src = SOME (Word x7)’] + \\ ‘FLOOKUP regs src = SOME (Word x7)’ by fs [FLOOKUP_DEF,SUBMAP_DEF] + \\ fs [] + \\ match_mp_tac SUBMAP_mono_FUPDATE + \\ rw[GSYM SUBMAP_DOMSUB_gen] + \\ metis_tac[SUBMAP_TRANS,SUBMAP_DOMSUB] ) \\ conj_tac (* Tick *) >- ( rpt strip_tac \\ qexists_tac `0` \\ full_simp_tac(srw_ss())[Once comp_def,evaluate_def,dec_clock_def] diff --git a/compiler/backend/proofs/stack_namesProofScript.sml b/compiler/backend/proofs/stack_namesProofScript.sml index 3a6a16ca32..63149c6118 100644 --- a/compiler/backend/proofs/stack_namesProofScript.sml +++ b/compiler/backend/proofs/stack_namesProofScript.sml @@ -208,7 +208,6 @@ val comp_correct = Q.prove( s.compile = (λcfg. c cfg o (stack_names$compile f)) ==> evaluate (comp f p, rename_state c f s) = (r, rename_state c f t)`, - recInduct evaluate_ind \\ rpt strip_tac THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac) THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac \\ CASE_TAC \\ fs [] @@ -219,6 +218,7 @@ val comp_correct = Q.prove( imp_res_tac inst_rename >> fs[]) THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[]) THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[]) + THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[]) THEN1 (fs [evaluate_def,comp_def,rename_state_def] \\ rw [] \\ fs [] \\ rw [] \\ fs [empty_env_def,dec_clock_def]) THEN1 diff --git a/compiler/backend/proofs/stack_rawcallProofScript.sml b/compiler/backend/proofs/stack_rawcallProofScript.sml index b2f2b57c0b..2f86827b6b 100644 --- a/compiler/backend/proofs/stack_rawcallProofScript.sml +++ b/compiler/backend/proofs/stack_rawcallProofScript.sml @@ -158,6 +158,8 @@ Proof (rename [`Get`] \\ simple_case) THEN1 (rename [`Set`] \\ simple_case) + THEN1 + (rename [`OpCurrHeap`] \\ simple_case) THEN1 (rename [`Tick`] \\ simple_case) THEN1 @@ -941,26 +943,4 @@ Proof \\ simp [stack_get_handler_labels_def] QED -(* -Theorem get_code_labels_comp: - !i p. - get_code_labels (comp i p) = get_code_labels p /\ - get_code_labels (comp_top i p) = get_code_labels p -Proof - recInduct comp_ind \\ rpt gen_tac \\ strip_tac - \\ Cases_on `p` \\ fs [] \\ simp [comp_top_def] - \\ simp [Once comp_def] - \\ TRY (fs [get_code_labels_def] \\ NO_TAC) - THEN1 (every_case_tac \\ fs [get_code_labels_def]) - \\ reverse conj_asm2_tac THEN1 fs [get_code_labels_def] - \\ rename [`comp_seq p1 p2`] - \\ Cases_on `comp_seq p1 p2 i (Seq (comp i p1) (comp i p2)) = - Seq (comp i p1) (comp i p2)` \\ simp [] - \\ drule comp_seq_neq_IMP \\ strip_tac \\ rveq \\ fs [] - \\ fs [comp_seq_def,dest_case_def,CaseEq"option",CaseEq"bool"] - \\ Cases_on `lookup dest i` \\ fs [] \\ rw [] - \\ simp [get_code_labels_def] -QED -*) - val _ = export_theory(); diff --git a/compiler/backend/proofs/stack_removeProofScript.sml b/compiler/backend/proofs/stack_removeProofScript.sml index cd8c62f38a..5478332631 100644 --- a/compiler/backend/proofs/stack_removeProofScript.sml +++ b/compiler/backend/proofs/stack_removeProofScript.sml @@ -9,7 +9,7 @@ open preamble set_sepTheory semanticsPropsTheory helperLib -local open dep_rewrite blastLib in end +local open dep_rewrite blastLib labPropsTheory in end val _ = new_theory"stack_removeProof"; @@ -597,6 +597,7 @@ Theorem state_rel_word_exp: word_exp t e = SOME w Proof ho_match_mp_tac word_exp_ind + \\ rpt conj_tac \\ simp[word_exp_def] \\ rw[] \\ imp_res_tac state_rel_mem_load_imp @@ -990,7 +991,7 @@ val name_cases = prove( (* Significantly faster than SEP_R_TAC *) val mem_load_lemma = Q.prove(` MEM name store_list ∧ - FLOOKUP (s:('a,'c,'b)state).store name = SOME x ∧ + FLOOKUP (s:('a,'c,'b)stackSem$state).store name = SOME x ∧ (memory s.memory s.mdomain * word_list (the_SOME_Word (FLOOKUP s.store BitmapBase) ≪ word_shift (:α)) @@ -1001,7 +1002,7 @@ val mem_load_lemma = Q.prove(` bytes_in_word * n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps)) s.data_buffer.space_left * word_store c s.store * - word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒ + word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒ mem_load (c+store_offset name) t1 = SOME x`, strip_tac >> drule fun2set_STAR_IMP>> @@ -1041,7 +1042,7 @@ val mem_load_lemma2 = Q.prove(` bytes_in_word * n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps)) s.data_buffer.space_left * word_store c s.store * - word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒ + word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒ c+store_offset name ∈ t1.mdomain`, strip_tac >> drule fun2set_STAR_IMP>> @@ -1142,28 +1143,31 @@ Proof srw_tac[][FUN_EQ_THM,prog_comp_def,FORALL_PROD,LAMBDA_PROD] QED -val comp_correct = Q.prove( - `!p s1 r s2 t1 k off jump. +Theorem comp_correct[local]: + !p s1 r s2 t1 k off jump. evaluate (p,s1) = (r,s2) /\ r <> SOME Error /\ state_rel jump off k s1 t1 /\ reg_bound p k ==> ?ck t2. evaluate (comp jump off k p,t1 with clock := ck + t1.clock) = (r,t2) /\ (case r of - | SOME (Halt _) => t2.ffi = s2.ffi - | SOME TimeOut => t2.ffi = s2.ffi - | SOME (FinalFFI _) => t2.ffi = s2.ffi - | _ => (state_rel jump off k s2 t2))`, + | SOME (Halt _) => t2.ffi = s2.ffi + | SOME TimeOut => t2.ffi = s2.ffi + | SOME (FinalFFI _) => t2.ffi = s2.ffi + | _ => (state_rel jump off k s2 t2)) +Proof recInduct evaluate_ind \\ rpt strip_tac - THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[]) - THEN1 + THEN1 (* Skip *) + (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[]) + THEN1 (* Halt *) (full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def] \\ imp_res_tac state_rel_get_var \\ full_simp_tac(srw_ss())[] \\ qexists_tac`0` \\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[] \\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[] \\ full_simp_tac(srw_ss())[state_rel_def]) - THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def]) - THEN1 ( - full_simp_tac(srw_ss())[comp_def,evaluate_def] + THEN1 (* Alloc *) + (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def]) + THEN1 (* Inst *) + (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ last_x_assum mp_tac \\ BasicProvers.TOP_CASE_TAC \\ full_simp_tac(srw_ss())[] \\ strip_tac \\ rveq @@ -1224,6 +1228,19 @@ val comp_correct = Q.prove( \\ Q.ABBREV_TAC `d = t1.mdomain` \\ drule name_cases \\ metis_tac[store_write_lemma]) + THEN1 (* OpCurrHeap *) + (qexists_tac`0` + \\ `s.use_store` by full_simp_tac(srw_ss())[state_rel_def] + \\ full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def] + \\ gvs [AllCaseEqs(),word_exp_def] + \\ every_case_tac \\ full_simp_tac(srw_ss())[] \\ srw_tac[][] + \\ fs [inst_def,assign_def,word_exp_def] + \\ gvs [AllCaseEqs(),word_exp_def,PULL_EXISTS] + \\ rename [‘FLOOKUP s.regs src = SOME (Word c1)’] + \\ rename [‘FLOOKUP s.store CurrHeap = SOME (Word c2)’] + \\ qsuff_tac ‘FLOOKUP t1.regs src = SOME (Word c1) ∧ + FLOOKUP t1.regs (k + 2) = SOME (Word c2)’ THEN1 fs [] + \\ fs [state_rel_def]) THEN1 (* Tick *) (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ `s.clock = t1.clock` by full_simp_tac(srw_ss())[state_rel_def] \\ full_simp_tac(srw_ss())[] @@ -1516,7 +1533,7 @@ val comp_correct = Q.prove( \\ disch_then(qspec_then`ck2`mp_tac) \\ simp[] \\ ntac 2 strip_tac \\ qexists_tac`ck' + ck2` \\ simp[] ) - THEN1 ( (* Install *) + THEN1 ( (* Install *) rw[comp_def] \\ fs[evaluate_def] \\ fs[reg_bound_def] @@ -1968,7 +1985,8 @@ val comp_correct = Q.prove( \\ full_simp_tac(srw_ss())[mem_load_def] \\ SEP_R_TAC \\ full_simp_tac(srw_ss())[]) \\ `good_dimindex(:'a)` by full_simp_tac(srw_ss())[state_rel_def] \\ full_simp_tac(srw_ss())[labPropsTheory.good_dimindex_def,word_shift_def,FLOOKUP_UPDATE] - \\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def])); + \\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def]) +QED Theorem compile_semantics: state_rel jump off k s1 s2 /\ semantics start s1 <> Fail ==> @@ -3442,8 +3460,8 @@ Proof QED Theorem stack_remove_lab_pres: - ∀jump off k p. - extract_labels p = extract_labels (comp jump off k p) + ∀jump off k p. + extract_labels p = extract_labels (comp jump off k p) Proof ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>> once_rewrite_tac [comp_def]>>fs[extract_labels_def]>> @@ -3474,25 +3492,26 @@ Proof QED Theorem stack_remove_comp_stack_asm_name: - ∀jump off k p. - stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧ - addr_offset_ok c 0w ∧ - good_dimindex (:'a) ∧ - (∀n. n ≤ max_stack_alloc ⇒ - c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧ - c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧ - (* Needed to implement the global store *) - (∀s. addr_offset_ok c (store_offset s)) ∧ - reg_name (k+2) c ∧ - reg_name (k+1) c ∧ - reg_name k c ∧ - off = c.addr_offset ⇒ - stack_asm_name c (comp jump off k p) + ∀jump off k p. + stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧ + addr_offset_ok c 0w ∧ + good_dimindex (:'a) ∧ + (∀n. n ≤ max_stack_alloc ⇒ + c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧ + c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧ + (* Needed to implement the global store *) + (∀s. addr_offset_ok c (store_offset s)) ∧ + reg_name (k+2) c ∧ + reg_name (k+1) c ∧ + reg_name k c ∧ + off = c.addr_offset ⇒ + stack_asm_name c (comp jump off k p) Proof ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>> simp[Once comp_def]>> rw[]>> - fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def,arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def] + fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def, + arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def] >- (every_case_tac>>fs[]) >- diff --git a/compiler/backend/proofs/stack_to_labProofScript.sml b/compiler/backend/proofs/stack_to_labProofScript.sml index 7d84ea03e2..6d37a6f0ed 100644 --- a/compiler/backend/proofs/stack_to_labProofScript.sml +++ b/compiler/backend/proofs/stack_to_labProofScript.sml @@ -1167,6 +1167,10 @@ Proof rename [`Set`] >> srw_tac[][stackSemTheory.evaluate_def,flatten_def] >> full_simp_tac(srw_ss())[state_rel_def] ) >> + conj_tac >- ( + rename [`OpCurrHeap`] >> + srw_tac[][stackSemTheory.evaluate_def,flatten_def] >> + full_simp_tac(srw_ss())[state_rel_def] ) >> conj_tac >- ( rename [`Tick`] >> simp[stackSemTheory.evaluate_def,flatten_def] >> diff --git a/compiler/backend/proofs/word_allocProofScript.sml b/compiler/backend/proofs/word_allocProofScript.sml index 0c580c1803..fa17a0af4d 100644 --- a/compiler/backend/proofs/word_allocProofScript.sml +++ b/compiler/backend/proofs/word_allocProofScript.sml @@ -1197,7 +1197,7 @@ Proof impl_tac>- (unabbrev_all_tac>>full_simp_tac(srw_ss())[state_component_equality])>> srw_tac[][]>>full_simp_tac(srw_ss())[]>>NO_TAC) - >- (*Seq*) + >- (*Seq*) (srw_tac[][]>>fs[evaluate_def,colouring_ok_def,LET_THM,get_live_def]>> last_assum(qspecl_then[`p`,`st`,`cst`,`f`,`get_live p0 live`] mp_tac)>> @@ -1347,7 +1347,20 @@ Proof TOP_CASE_TAC>>full_simp_tac(srw_ss())[]) >- (* Tick *) (exists_tac>>IF_CASES_TAC>>full_simp_tac(srw_ss())[call_env_def, flush_state_def,dec_clock_def]) - >- (*LocValue*) + >- (* OpCurrHeap *) + (exists_tac>> + full_simp_tac(srw_ss())[evaluate_def,LET_THM,word_state_eq_rel_def, + get_live_def,colouring_ok_def,word_exp_def,the_words_def] >> + Cases_on ‘lookup n0 st.locals’ THEN1 fs [] >> + ‘lookup (f n0) cst.locals = lookup n0 st.locals’ by fs [strong_locals_rel_def] >> + fs [] >> Cases_on ‘x’ >> fs [] >> + Cases_on ‘FLOOKUP st.store CurrHeap’ >> fs [] >> Cases_on ‘x’ >> fs []>> + EVERY_CASE_TAC>>fs [set_var_def]>> + match_mp_tac strong_locals_rel_insert >> + fs [get_writes_def,domain_union] >> + metis_tac[INSERT_SING_UNION,strong_locals_rel_subset,SUBSET_OF_INSERT + ,strong_locals_rel_insert,SUBSET_UNION]) + >- (* LocValue *) (exists_tac>>fs[set_var_def,strong_locals_rel_def]>>rw[]>> fs[lookup_insert]>> Cases_on`n'=n`>>fs[]>> @@ -1359,7 +1372,7 @@ Proof rpt (pop_assum kall_tac)>> simp[])>> fs[]) - >- + >- (* Install *) (exists_tac>> pairarg_tac>>fs[case_eq_thms]>> pop_assum mp_tac>>pairarg_tac>>strip_tac>>rfs[case_eq_thms]>>rw[]>> @@ -1389,14 +1402,14 @@ Proof match_mp_tac (GEN_ALL strong_locals_rel_subset|>SIMP_RULE std_ss[Once CONJ_COMM])>> asm_exists_tac>> fs[SUBSET_DEF]) - >- (*DBW*) + >- (* DBW *) (exists_tac>>pairarg_tac>>fs[case_eq_thms]>> imp_res_tac strong_locals_rel_get_var>>fs[list_insert_def]>> rw[]>>fs[]>> match_mp_tac (GEN_ALL strong_locals_rel_subset|>SIMP_RULE std_ss[Once CONJ_COMM])>> asm_exists_tac>> fs[SUBSET_DEF]) - >> (* FFI *) + >> (* FFI *) (exists_tac>>Cases_on`get_var n st`>>Cases_on`get_var n0 st`>> Cases_on`get_var n1 st`>>Cases_on`get_var n2 st`>> full_simp_tac(srw_ss())[get_writes_def,LET_THM,get_var_perm]>> @@ -1448,11 +1461,12 @@ val get_clash_sets_hd = Q.prove( full_simp_tac(srw_ss())[get_live_def,LET_THM]>>metis_tac[]); (*The liveset passed in at the back is always satisfied*) -val get_clash_sets_tl = Q.prove( -`∀prog live f. +Theorem get_clash_sets_tl[local]: + ∀prog live f. let (hd,ls) = get_clash_sets prog live in EVERY (λs. INJ f (domain s) UNIV) ls ⇒ - INJ f (domain live) UNIV`, + INJ f (domain live) UNIV +Proof completeInduct_on`prog_size (K 0) prog`>> full_simp_tac(srw_ss())[PULL_FORALL]>> rpt strip_tac>> @@ -1479,8 +1493,8 @@ val get_clash_sets_tl = Q.prove( TRY(first_x_assum(qspecl_then[`p0`,`live`,`f`]mp_tac)>> impl_tac>-size_tac>>srw_tac[][]>> full_simp_tac(srw_ss())[UNCURRY]) - >- metis_tac[INJ_UNION,domain_union,INJ_SUBSET,SUBSET_UNION] - >- metis_tac[INJ_UNION,domain_union,INJ_SUBSET,SUBSET_UNION]); + >> metis_tac[INJ_UNION,domain_union,INJ_SUBSET,SUBSET_UNION] +QED Theorem colouring_ok_alt_thm: ∀f prog live. @@ -1921,6 +1935,13 @@ val subset_tac = HINT_EXISTS_TAC>>fs[domain_numset_list_insert_eq_union,SUBSET_DEF]>> simp[domain_union]; +Theorem IMAGE_DIFF: + INJ f (s UNION t) UNIV ⇒ + IMAGE f (s DIFF t) = IMAGE f s DIFF IMAGE f t +Proof + fs [EXTENSION,INJ_DEF] \\ rw [] \\ metis_tac [] +QED + Theorem clash_tree_colouring_ok: ∀prog f live flive livein flivein. wf_cutsets prog ∧ @@ -2172,7 +2193,7 @@ Proof drule check_partial_col_INJ>> rpt (disch_then drule)>> rw[hide_def,numset_list_insert_def,list_insert_def]>> fs[domain_insert]) - >- + >- (* FFI *) (EVERY_CASE_TAC>>fs[]>> imp_res_tac check_col_INJ>> fs[numset_list_delete_def]>> @@ -2180,31 +2201,43 @@ Proof rpt (qpat_x_assum `!P. Q` kall_tac)>> rfs[AND_IMP_INTRO]>> fs[hide_def,numset_list_insert_def,wf_cutsets_def]) - >- + >- (* Raise *) (start_tac>> fs[numset_list_delete_def,numset_list_insert_def]>> metis_tac[INSERT_SING_UNION,UNION_COMM]) - >- + >- (* Return *) (start_tac>> fs[numset_list_delete_def,numset_list_insert_def]>> `domain live ∪ {num1;num2} = num1 INSERT num2 INSERT domain live` by (fs[EXTENSION]>>metis_tac[])>> fs[]) - >- + >- (* Tick *) (start_tac>> fs[numset_list_delete_def,numset_list_insert_def]) - >- + >- (* LocValue *) (start_tac>> fs[numset_list_delete_def,numset_list_insert_def,domain_union,DELETE_DEF,UNION_COMM]>> CONJ_TAC>- subset_tac>> fs[INJ_IMP_IMAGE_DIFF_single]) - >- + >- (* Set *) (start_tac>> fs[numset_list_delete_def,numset_list_insert_def,domain_union,DELETE_DEF,UNION_COMM,get_reads_exp_get_live_exp]>> match_mp_tac numset_list_insert_eq_UNION>> fs[wf_get_live_exp,get_reads_exp_get_live_exp]) - >- - (*Call*) + >- (* OpCurrHeap *) + (start_tac>> + fs[numset_list_delete_def,numset_list_insert_def,domain_union,DELETE_DEF, + UNION_COMM,get_reads_exp_get_live_exp]>> + ‘INJ f (domain live DIFF {dst}) 𝕌(:num)’ by + (qpat_x_assum ‘INJ f (domain live ∪ {dst}) 𝕌(:num)’ mp_tac + \\ rpt (pop_assum kall_tac) + \\ rewrite_tac [INJ_DEF,IN_DIFF,IN_UNION,NOT_IN_EMPTY,IN_UNIV,IN_INSERT] + \\ metis_tac []) + \\ gvs [IMAGE_DIFF] \\ rw [] + \\ rpt (pop_assum mp_tac) + \\ rewrite_tac [INJ_DEF,IN_UNION,IN_INSERT] + \\ metis_tac []) + >- (*Call*) (Cases_on`ret`>>fs[] >- (fs[check_clash_tree_def,hide_def,wf_cutsets_def,colouring_ok_def,get_live_def,get_writes_def]>> @@ -2685,6 +2718,12 @@ Proof rm_tac >- (* get *) rm_tac + >- (* OpCurrHeap *) + (rm_tac \\ fs[evaluate_def,state_component_equality,set_var_def,word_exp_def, + the_words_def,AllCaseEqs(),PULL_EXISTS,get_live_exp_def,big_union_def]>> + first_x_assum (qspecl_then [‘t’,‘delete num live’] mp_tac) >> + impl_tac >- (fs [domain_delete] \\ metis_tac []) >> + strip_tac \\ fs [] \\ rw [lookup_insert]) >- (* loc value *) rm_tac >- (* seq *) @@ -2706,8 +2745,7 @@ Proof rpt var_eq_tac>>fs[evaluate_def]>> first_x_assum (qspecl_then [`st with <|clock := MustTerminate_limit (:'a) ; termdep := st.termdep -1|>` ] mp_tac)>> fs[]>>disch_then drule>>rw[]>>fs[state_component_equality]) - >- - (* if *) + >- (* if *) (rpt (pairarg_tac>>fs[])>> qpat_x_assum`A=(res,rst)` mp_tac>> ntac 4 (TOP_CASE_TAC>>fs[])>> @@ -2722,10 +2760,6 @@ Proof TRY(first_assum match_mp_tac>>fs[strong_locals_rel_def,domain_union]>> NO_TAC)>> last_assum match_mp_tac>>fs[strong_locals_rel_def,domain_union]) - - - - >- (*call*) (qpat_x_assum`A=(res,rst)` mp_tac>> ntac 7 (TOP_CASE_TAC>>fs[])>> @@ -2863,7 +2897,9 @@ Proof pop_assum(qspecl_then[`t`,`domain v40`] mp_tac)>> impl_tac>- (fs[strong_locals_rel_def]>>metis_tac[]))>> rw[state_component_equality]>> - fs[strong_locals_rel_def]) + fs[strong_locals_rel_def] >> + fs [PULL_EXISTS,get_var_def] >> + metis_tac []) >- (* CBW *) (fs[case_eq_thms,list_insert_def]>> imp_res_tac strong_locals_rel_I_get_var>> @@ -4048,7 +4084,7 @@ val ssa_map_ok_inter = Q.prove(` (*Prove the properties that hold of ssa_cc_trans independent of semantics*) -val ssa_cc_trans_props = Q.prove(` +Theorem ssa_cc_trans_props[local]: ∀prog ssa na prog' ssa' na'. ssa_cc_trans prog ssa na = (prog',ssa',na') ∧ ssa_map_ok na ssa ∧ @@ -4056,7 +4092,8 @@ val ssa_cc_trans_props = Q.prove(` ⇒ na ≤ na' ∧ is_alloc_var na' ∧ - ssa_map_ok na' ssa'`, + ssa_map_ok na' ssa' +Proof ho_match_mp_tac ssa_cc_trans_ind>> full_simp_tac(srw_ss())[ssa_cc_trans_def]>> strip_tac >- @@ -4107,6 +4144,8 @@ val ssa_cc_trans_props = Q.prove(` exp_tac>> strip_tac >- exp_tac>> + strip_tac >- + exp_tac>> strip_tac >- (* Install *) (rpt gen_tac>> strip_tac>> @@ -4226,7 +4265,8 @@ val ssa_cc_trans_props = Q.prove(` full_simp_tac(srw_ss())[next_var_rename_def]>> DECIDE_TAC)>> imp_res_tac fix_inconsistencies_props>> - DECIDE_TAC); + DECIDE_TAC +QED val PAIR_ZIP_MEM = Q.prove(` LENGTH c = LENGTH d ∧ @@ -5905,6 +5945,16 @@ Proof >- (* Tick *) (exists_tac>> EVERY_CASE_TAC>>full_simp_tac(srw_ss())[call_env_def, flush_state_def,dec_clock_def]) + >- (* OpCurrHeap *) + (last_x_assum kall_tac>> + exists_tac>> + EVERY_CASE_TAC>>full_simp_tac(srw_ss())[next_var_rename_def]>> + imp_res_tac ssa_locals_rel_get_var>> + imp_res_tac ssa_cc_trans_exp_correct>>full_simp_tac(srw_ss())[word_state_eq_rel_def]>> + rev_full_simp_tac(srw_ss())[word_exp_perm,evaluate_def]>> + fs[set_var_def,set_store_def,ssa_cc_trans_exp_def]>> + match_mp_tac ssa_locals_rel_set_var>> + full_simp_tac(srw_ss())[every_var_def]) >- exp_tac >- (* Install *) @@ -6729,12 +6779,13 @@ val fake_moves_distinct_tar_reg = Q.prove(` unabbrev_all_tac>> metis_tac[fake_move_def,every_inst_def,distinct_tar_reg_def]); -val ssa_cc_trans_distinct_tar_reg = Q.prove(` +Theorem ssa_cc_trans_distinct_tar_reg: ∀prog ssa na. - is_alloc_var na ∧ - every_var (λx. x < na) prog ∧ - ssa_map_ok na ssa ⇒ - every_inst distinct_tar_reg (FST (ssa_cc_trans prog ssa na))`, + is_alloc_var na ∧ + every_var (λx. x < na) prog ∧ + ssa_map_ok na ssa ⇒ + every_inst distinct_tar_reg (FST (ssa_cc_trans prog ssa na)) +Proof ho_match_mp_tac ssa_cc_trans_ind>>full_simp_tac(srw_ss())[ssa_cc_trans_def]>>srw_tac[][]>> unabbrev_all_tac>> full_simp_tac(srw_ss())[every_inst_def]>>imp_res_tac ssa_cc_trans_props>>full_simp_tac(srw_ss())[] @@ -6769,6 +6820,14 @@ val ssa_cc_trans_distinct_tar_reg = Q.prove(` >> TRY (full_simp_tac(srw_ss())[list_next_var_rename_move_def]>>rpt (pop_assum mp_tac)>> LET_ELIM_TAC>>full_simp_tac(srw_ss())[every_inst_def,EQ_SYM_EQ]>>NO_TAC) + >- + (rename [‘OpCurrHeap’]>> + full_simp_tac(srw_ss())[ssa_cc_trans_inst_def,LET_THM,next_var_rename_def]>> + every_case_tac>> rw[]>> + fs[every_var_def,every_var_inst_def,every_var_imm_def,every_inst_def]>> + full_simp_tac(srw_ss())[distinct_tar_reg_def,ssa_map_ok_def,option_lookup_def]>> + EVERY_CASE_TAC>>srw_tac[][]>>res_tac>>full_simp_tac(srw_ss())[]>> + fs[is_alloc_var_def]>>CCONTR_TAC>>fs[]) >> FULL_CASE_TAC>>full_simp_tac(srw_ss())[every_var_def,every_inst_def] >- @@ -6834,11 +6893,12 @@ val ssa_cc_trans_distinct_tar_reg = Q.prove(` full_simp_tac(srw_ss())[list_next_var_rename_move_def]>> rpt(qpat_x_assum`A=(B,C,D)` mp_tac)>> LET_ELIM_TAC>>full_simp_tac(srw_ss())[EQ_SYM_EQ,every_inst_def]>> - metis_tac[fake_moves_distinct_tar_reg]); + metis_tac[fake_moves_distinct_tar_reg] +QED Theorem full_ssa_cc_trans_distinct_tar_reg: - ∀n prog. - every_inst distinct_tar_reg (full_ssa_cc_trans n prog) + ∀n prog. + every_inst distinct_tar_reg (full_ssa_cc_trans n prog) Proof srw_tac[][]>> full_simp_tac(srw_ss())[full_ssa_cc_trans_def]>> @@ -6862,7 +6922,7 @@ Proof full_simp_tac(srw_ss())[] QED -val fake_moves_conventions2 = Q.prove(` +Theorem fake_moves_conventions2[local]: ∀ls ssal ssar na l r a b c conf. fake_moves ls ssal ssar na = (l,r,a,b,c) ⇒ flat_exp_conventions l ∧ @@ -6870,12 +6930,14 @@ val fake_moves_conventions2 = Q.prove(` full_inst_ok_less conf l ∧ full_inst_ok_less conf r ∧ every_inst distinct_tar_reg l ∧ - every_inst distinct_tar_reg r`, + every_inst distinct_tar_reg r +Proof Induct>>full_simp_tac(srw_ss())[fake_moves_def]>>srw_tac[][]>>full_simp_tac(srw_ss())[flat_exp_conventions_def,full_inst_ok_less_def,every_inst_def]>> pop_assum mp_tac>> LET_ELIM_TAC>> EVERY_CASE_TAC>> full_simp_tac(srw_ss())[LET_THM]>> unabbrev_all_tac>> rveq>>fs[flat_exp_conventions_def,fake_move_def,full_inst_ok_less_def,inst_ok_less_def,every_inst_def,distinct_tar_reg_def]>> - metis_tac[]); + metis_tac[] +QED val ssa_cc_trans_flat_exp_conventions = Q.prove(` ∀prog ssa na. @@ -6928,13 +6990,14 @@ QED val _ = diminish_srw_ss ["NORMEQ_ss"]; -val ssa_cc_trans_full_inst_ok_less = Q.prove(` +Theorem ssa_cc_trans_full_inst_ok_less[local]: ∀prog ssa na c. - every_var (λx. x < na) prog ∧ - is_alloc_var na ∧ - ssa_map_ok na ssa ∧ - full_inst_ok_less c prog ⇒ - full_inst_ok_less c (FST (ssa_cc_trans prog ssa na))`, + every_var (λx. x < na) prog ∧ + is_alloc_var na ∧ + ssa_map_ok na ssa ∧ + full_inst_ok_less c prog ⇒ + full_inst_ok_less c (FST (ssa_cc_trans prog ssa na)) +Proof ho_match_mp_tac ssa_cc_trans_ind>>full_simp_tac(srw_ss())[ssa_cc_trans_def]>>srw_tac[][]>> unabbrev_all_tac>> full_simp_tac(srw_ss())[full_inst_ok_less_def] @@ -7041,7 +7104,8 @@ val ssa_cc_trans_full_inst_ok_less = Q.prove(` (match_mp_tac (GEN_ALL ssa_map_ok_more)>> qexists_tac`n'`>>fs[])>> metis_tac[convention_partitions]) - >- metis_tac[fake_moves_conventions2,full_inst_ok_less_def]); + >- metis_tac[fake_moves_conventions2,full_inst_ok_less_def] +QED Theorem full_ssa_cc_trans_full_inst_ok_less: ∀prog n c. @@ -7317,16 +7381,19 @@ Proof QED (*word_alloc preserves syntactic conventions*) -val word_alloc_two_reg_inst_lem = Q.prove(` +Theorem word_alloc_two_reg_inst_lem[local]: ∀f prog. every_inst two_reg_inst prog ⇒ - every_inst two_reg_inst (apply_colour f prog)`, + every_inst two_reg_inst (apply_colour f prog) +Proof ho_match_mp_tac apply_colour_ind>>full_simp_tac(srw_ss())[every_inst_def]>>srw_tac[][] >- (Cases_on`i`>>TRY(Cases_on`a`)>>TRY(Cases_on`m`)>>TRY(Cases_on`f'`)>> full_simp_tac(srw_ss())[apply_colour_inst_def,two_reg_inst_def]) >> - EVERY_CASE_TAC>>unabbrev_all_tac>>full_simp_tac(srw_ss())[every_inst_def]); + EVERY_CASE_TAC>>unabbrev_all_tac>>full_simp_tac(srw_ss())[every_inst_def]>> + full_simp_tac(srw_ss())[apply_colour_inst_def,two_reg_inst_def] +QED Theorem word_alloc_two_reg_inst: ∀fc c alg k prog col_opt. @@ -7451,14 +7518,16 @@ Proof fs[] QED -val apply_colour_lab_pres = Q.prove(` +Theorem apply_colour_lab_pres[local]: ∀col prog. - extract_labels prog = extract_labels (apply_colour col prog)`, + extract_labels prog = extract_labels (apply_colour col prog) +Proof ho_match_mp_tac apply_colour_ind>>fs[extract_labels_def]>>rw[]>> - EVERY_CASE_TAC>>fs[]); + EVERY_CASE_TAC>>fs[] +QED Theorem word_alloc_lab_pres: - extract_labels prog = extract_labels (word_alloc fc c alg k prog col_opt) + extract_labels prog = extract_labels (word_alloc fc c alg k prog col_opt) Proof fs[word_alloc_def,oracle_colour_ok_def]>> EVERY_CASE_TAC>>fs[]>> @@ -7471,14 +7540,14 @@ QED val convs = [flat_exp_conventions_def,full_inst_ok_less_def,every_inst_def,pre_alloc_conventions_def,call_arg_convention_def,every_stack_var_def,every_var_def,extract_labels_def,wf_cutsets_def]; Theorem remove_dead_conventions: - ∀p live c k. - let comp = FST (remove_dead p live) in - (flat_exp_conventions p ⇒ flat_exp_conventions comp) ∧ - (full_inst_ok_less c p ⇒ full_inst_ok_less c comp) ∧ - (pre_alloc_conventions p ⇒ pre_alloc_conventions comp) ∧ - (every_inst distinct_tar_reg p ⇒ every_inst distinct_tar_reg comp) ∧ - (wf_cutsets p ⇒ wf_cutsets comp) ∧ - (extract_labels p = extract_labels comp) + ∀p live c k. + let comp = FST (remove_dead p live) in + (flat_exp_conventions p ⇒ flat_exp_conventions comp) ∧ + (full_inst_ok_less c p ⇒ full_inst_ok_less c comp) ∧ + (pre_alloc_conventions p ⇒ pre_alloc_conventions comp) ∧ + (every_inst distinct_tar_reg p ⇒ every_inst distinct_tar_reg comp) ∧ + (wf_cutsets p ⇒ wf_cutsets comp) ∧ + (extract_labels p = extract_labels comp) Proof ho_match_mp_tac remove_dead_ind>>rw[]>> fs[remove_dead_def]>> diff --git a/compiler/backend/proofs/word_depthProofScript.sml b/compiler/backend/proofs/word_depthProofScript.sml index 215e0f3b59..4996269068 100644 --- a/compiler/backend/proofs/word_depthProofScript.sml +++ b/compiler/backend/proofs/word_depthProofScript.sml @@ -275,6 +275,10 @@ Proof (fs [wordSemTheory.evaluate_def] \\ rveq \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs [] \\ fs []) + THEN1 (* OpCurrHeap *) + (fs [wordSemTheory.evaluate_def] \\ rveq + \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs [] + \\ fs []) THEN1 (* Store *) (fs [wordSemTheory.evaluate_def,mem_store_def] \\ rveq \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs [] diff --git a/compiler/backend/proofs/word_elimProofScript.sml b/compiler/backend/proofs/word_elimProofScript.sml index d852a2c5a2..b74b427f7e 100644 --- a/compiler/backend/proofs/word_elimProofScript.sml +++ b/compiler/backend/proofs/word_elimProofScript.sml @@ -141,6 +141,7 @@ Proof >- (EVERY_CASE_TAC >> fs[set_var_def] >> rw[] >> fs[]) >- (EVERY_CASE_TAC >> fs[set_var_def] >> rw[] >> fs[]) >- (EVERY_CASE_TAC >> fs[set_store_def] >> rw[] >> fs[]) + >- (EVERY_CASE_TAC >> fs[set_var_def] >> rw[] >> fs[]) >- (EVERY_CASE_TAC >> fs[mem_store_def] >> rw[] >> fs[]) >- (EVERY_CASE_TAC >> fs[call_env_def, flush_state_def, dec_clock_def] >> rw[] >> fs[]) >- (EVERY_CASE_TAC >> fs[] >> rename1 `evaluate (p, st)` >> @@ -1559,6 +1560,14 @@ Proof fs[SUBSET_DEF]) >> fs[SUBSET_DEF] >> metis_tac[] ) + >- ( (* OpCurrHeap *) + simp[wordSemTheory.evaluate_def,word_exp_def,the_words_def] + \\ simp [AllCaseEqs(),PULL_EXISTS] \\ rpt gen_tac \\ strip_tac + \\ gvs [dest_result_loc_def,set_var_def] + \\ fs[word_state_rel_def, domain_find_loc_state, dest_result_loc_def] + \\ qspecl_then [`dst`, `Word z`, `s.locals`] mp_tac get_locals_insert + \\ fs[dest_word_loc_def] \\ metis_tac[SUBSET_TRANS] + ) >- ( (* Set *) simp[wordSemTheory.evaluate_def] >> Cases_on `v = Handler ∨ v = BitmapBase` >> fs[] >> diff --git a/compiler/backend/proofs/word_instProofScript.sml b/compiler/backend/proofs/word_instProofScript.sml index cd51bd61d3..f0f59e2278 100644 --- a/compiler/backend/proofs/word_instProofScript.sml +++ b/compiler/backend/proofs/word_instProofScript.sml @@ -17,10 +17,12 @@ val _ = set_grammar_ancestry ["wordLang", "wordProps", "word_inst", "wordSem"]; Type result[pp] = “:'a wordSem$result” (* TODO: Move, but some of these are specific instantiations *) -val PERM_SWAP_SIMP = Q.prove(` - PERM (A ++ (B::C)) (B::(A++C))`, +Theorem PERM_SWAP_SIMP[local]: + PERM (A ++ (B::C)) (B::(A++C)) +Proof match_mp_tac APPEND_PERM_SYM>>full_simp_tac(srw_ss())[]>> - metis_tac[PERM_APPEND]); + metis_tac[PERM_APPEND] +QED val EL_FILTER = Q.prove(` ∀ls x. x < LENGTH (FILTER P ls) ⇒ P (EL x (FILTER P ls))`, @@ -367,16 +369,18 @@ val flatten_exp_binary_branch_exp = Q.prove(` binary_branch_exp (flatten_exp exp)`, ho_match_mp_tac flatten_exp_ind>>full_simp_tac(srw_ss())[op_consts_def,flatten_exp_def,binary_branch_exp_def,EVERY_MEM,EVERY_MAP]); -val flatten_exp_every_var_exp = Q.prove(` +Theorem flatten_exp_every_var_exp[local]: ∀exp. every_var_exp P exp ⇒ - every_var_exp P (flatten_exp exp)`, - ho_match_mp_tac flatten_exp_ind>>full_simp_tac(srw_ss())[op_consts_def,flatten_exp_def,every_var_exp_def,EVERY_MEM,EVERY_MAP]); + every_var_exp P (flatten_exp exp) +Proof + ho_match_mp_tac flatten_exp_ind>>full_simp_tac(srw_ss())[op_consts_def,flatten_exp_def,every_var_exp_def,EVERY_MEM,EVERY_MAP] +QED (* inst_select correctness Main difficulty: Dealing with multiple choice of optimizations, depending on whether we are allowed to use them w.r.t. to the asm configuration *) -val inst_select_exp_thm = Q.prove(` +Theorem inst_select_exp_thm[local]: ∀c tar temp exp s w loc. binary_branch_exp exp ∧ every_var_exp (λx. x < temp) exp ∧ @@ -388,29 +392,33 @@ val inst_select_exp_thm = Q.prove(` ∀x. if x = tar then lookup x loc' = SOME w else if x < temp then lookup x loc' = lookup x s.locals - else T`, + else T +Proof completeInduct_on`exp_size (K 0) exp`>> rpt strip_tac>> Cases_on`exp`>> full_simp_tac(srw_ss())[evaluate_def,binary_branch_exp_def,every_var_exp_def] >- - (simp[inst_select_exp_def]>> + (rename [‘Const’]>> + simp[inst_select_exp_def]>> full_simp_tac(srw_ss())[LET_THM,evaluate_def,inst_def,mem_load_def,assign_def,word_exp_def,set_var_def,mem_load_def,word_op_def]>> simp[state_component_equality,locals_rel_def,lookup_insert]>> full_simp_tac(srw_ss())[locals_rel_def]) >- - (simp[inst_select_exp_def]>> + (rename [‘Var’] >> + simp[inst_select_exp_def]>> full_simp_tac(srw_ss())[LET_THM,evaluate_def,inst_def,mem_load_def,assign_def,word_exp_def,set_var_def,mem_load_def,word_op_def,get_vars_def,set_vars_def,get_var_def]>> full_simp_tac(srw_ss())[locals_rel_def]>> res_tac>>fs[alist_insert_def]>> simp[state_component_equality,lookup_insert]) >- - (simp[inst_select_exp_def]>> + (rename [‘Lookup’]>> + simp[inst_select_exp_def]>> full_simp_tac(srw_ss())[LET_THM,evaluate_def,inst_def,mem_load_def,assign_def,word_exp_def,set_var_def,mem_load_def,word_op_def,get_vars_def,set_vars_def,get_var_def]>> fs[locals_rel_def,state_component_equality,lookup_insert]) >- - (*Load*) - (Cases_on`∃exp' w'. e = Op Add[exp';Const w']` >>full_simp_tac(srw_ss())[] + (rename [‘Load’]>> + Cases_on`∃exp' w'. e = Op Add[exp';Const w']` >>full_simp_tac(srw_ss())[] >- (simp[Once inst_select_exp_def]>>IF_CASES_TAC >- @@ -453,10 +461,47 @@ val inst_select_exp_thm = Q.prove(` srw_tac[][]>>DISJ2_TAC>>strip_tac>> `x ≠ temp` by DECIDE_TAC>>metis_tac[]) >- - (*Op*) - (Cases_on`∃e1 e2. l = [e1;e2]`>>full_simp_tac(srw_ss())[inst_select_exp_def] + (rename [‘Op’]>> + Cases_on`∃e1 e2. l = [e1;e2]`>>full_simp_tac(srw_ss())[inst_select_exp_def] >- - (`binary_branch_exp e1` by + (IF_CASES_TAC THEN1 + (gvs[PULL_FORALL] >> + first_x_assum (qspec_then ‘e1’ mp_tac) >> + fs [exp_size_def,binary_branch_exp_def] >> + ‘binary_branch_exp e1’ by + (Cases_on ‘b’ \\ fs [binary_branch_exp_def]) >> fs [] >> + disch_then drule >> + gvs [word_exp_def,AllCaseEqs(),the_words_def,GSYM PULL_FORALL] >> + disch_then (qspecl_then [‘c’,‘temp’] strip_assume_tac) >> + pop_assum drule >> fs [] >> strip_tac >> + gvs [evaluate_def,word_exp_def,the_words_def] >> + first_assum (qspec_then ‘temp’ assume_tac) >> fs [] >> + Cases_on ‘e2’ >> fs [is_Lookup_CurrHeap_def] >> + rename [‘Lookup ss’] \\ Cases_on ‘ss’ >> fs [is_Lookup_CurrHeap_def] >> + gvs [word_exp_def,set_var_def,state_component_equality,lookup_insert] >> + rw [] >> metis_tac [prim_recTheory.LESS_REFL]) >> + pop_assum mp_tac >> + IF_CASES_TAC THEN1 + (gvs[PULL_FORALL] >> + first_x_assum (qspec_then ‘e2’ mp_tac) >> + fs [exp_size_def,binary_branch_exp_def] >> + ‘binary_branch_exp e2’ by + (Cases_on ‘b’ \\ fs [binary_branch_exp_def]) >> fs [] >> + disch_then drule >> + gvs [word_exp_def,AllCaseEqs(),the_words_def,GSYM PULL_FORALL] >> + disch_then (qspecl_then [‘c’,‘temp’] strip_assume_tac) >> + pop_assum drule >> fs [] >> strip_tac >> + gvs [evaluate_def,word_exp_def,the_words_def] >> + first_assum (qspec_then ‘temp’ assume_tac) >> fs [] >> + Cases_on ‘e1’ >> fs [is_Lookup_CurrHeap_def] >> + rename [‘Lookup ss’] \\ Cases_on ‘ss’ >> fs [is_Lookup_CurrHeap_def] >> + rename [‘word_op b [x1; x2] = SOME x3’] >> + ‘word_op b [x2; x1] = SOME x3’ by + (Cases_on ‘b’ \\ fs [word_op_def,AllCaseEqs()]) >> + gvs [word_exp_def,set_var_def,state_component_equality,lookup_insert] >> + rw [] >> metis_tac [prim_recTheory.LESS_REFL]) >> + pop_assum mp_tac>> + `binary_branch_exp e1` by (Cases_on`b`>>full_simp_tac(srw_ss())[binary_branch_exp_def])>> full_simp_tac(srw_ss())[word_exp_def,the_words_def,IS_SOME_EXISTS]>> last_x_assum mp_tac>>simp[Once PULL_FORALL]>> @@ -469,7 +514,8 @@ val inst_select_exp_thm = Q.prove(` pop_assum(qspecl_then[`temp`,`c`] assume_tac)>>full_simp_tac(srw_ss())[]>> Cases_on`∃w. e2 = Const w` >- - (full_simp_tac(srw_ss())[]>>IF_CASES_TAC + (rpt (disch_then kall_tac) >> + full_simp_tac(srw_ss())[]>>IF_CASES_TAC >- (full_simp_tac(srw_ss())[evaluate_def]>> simp[LET_THM,inst_def,mem_load_def,word_exp_def,assign_def,the_words_def]>> @@ -496,15 +542,25 @@ val inst_select_exp_thm = Q.prove(` DISJ2_TAC>>strip_tac>-`F` by DECIDE_TAC>> `x ≠ temp` by DECIDE_TAC>> `¬ (temp+1 < temp)` by DECIDE_TAC>> - metis_tac[])) + metis_tac[])) >> + ntac 2 (disch_then assume_tac) >> `inst_select_exp c tar temp (Op b [e1;e2]) = let p1 = inst_select_exp c temp temp e1 in let p2 = inst_select_exp c (temp+1) (temp+1) e2 in - Seq p1 (Seq p2 (Inst (Arith (Binop b tar temp (Reg (temp+1))))))` by - (full_simp_tac(srw_ss())[inst_select_exp_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[])>> + Seq p1 (Seq p2 (Inst (Arith (Binop b tar temp (Reg (temp+1))))))` by + (full_simp_tac(srw_ss())[inst_select_exp_def,LET_THM]>> + EVERY_CASE_TAC>>full_simp_tac(srw_ss())[])>> + pop_assum mp_tac >> + pop_assum mp_tac >> + pop_assum mp_tac >> full_simp_tac(srw_ss())[inst_select_exp_def,LET_THM]>>pop_assum kall_tac>> + ntac 2 (disch_then assume_tac) >> + IF_CASES_TAC THEN1 fs [] >> + rpt (qpat_x_assum ‘~(_:bool)’ kall_tac) >> + rpt (qpat_x_assum ‘_ ∨ _’ kall_tac) >> full_simp_tac(srw_ss())[evaluate_def,LET_THM]>> + disch_then kall_tac >> first_x_assum(qspecl_then[`e2`] mp_tac)>> simp[exp_size_def]>> disch_then(qspecl_then [`c`,`temp+1`,`temp+1`,`s with locals:=loc''`,`Word c''`,`loc''`] mp_tac)>> @@ -544,8 +600,8 @@ val inst_select_exp_thm = Q.prove(` Cases_on`t'`>>fs[the_words_def]>> EVERY_CASE_TAC>>fs[])) >- - (*Shift*) - (simp[inst_select_exp_def]>>last_x_assum mp_tac>>simp[Once PULL_FORALL]>>disch_then (qspec_then`e`mp_tac)>>impl_tac>-(full_simp_tac(srw_ss())[exp_size_def]>>DECIDE_TAC)>> + (rename [‘Shift’]>> + simp[inst_select_exp_def]>>last_x_assum mp_tac>>simp[Once PULL_FORALL]>>disch_then (qspec_then`e`mp_tac)>>impl_tac>-(full_simp_tac(srw_ss())[exp_size_def]>>DECIDE_TAC)>> full_simp_tac(srw_ss())[LET_THM,word_exp_def]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[] >- (`word_sh s' c' n = SOME c'` by @@ -571,7 +627,8 @@ val inst_select_exp_thm = Q.prove(` metis_tac[]) >- (`n ≥ dimindex(:'a)` by DECIDE_TAC>> - full_simp_tac(srw_ss())[word_sh_def]))); + full_simp_tac(srw_ss())[word_sh_def])) +QED val locals_rm = Q.prove(` D with locals := D.locals = D`, @@ -595,7 +652,7 @@ Theorem inst_select_thm: Proof ho_match_mp_tac inst_select_ind>>srw_tac[][]>> full_simp_tac(srw_ss())[inst_select_def,locals_rel_evaluate_thm] - >- + >- (* Assign *) (full_simp_tac(srw_ss())[evaluate_def]>>last_x_assum mp_tac>>FULL_CASE_TAC>>srw_tac[][]>> full_simp_tac(srw_ss())[every_var_def]>> imp_res_tac pull_exp_every_var_exp>> @@ -611,7 +668,7 @@ Proof srw_tac[][]>>full_simp_tac(srw_ss())[lookup_insert]>> IF_CASES_TAC>>fs[]>> metis_tac[]) - >- + >- (* Set *) (full_simp_tac(srw_ss())[evaluate_def]>>last_x_assum mp_tac>> ntac 2 FULL_CASE_TAC>>full_simp_tac(srw_ss())[]>>strip_tac>> full_simp_tac(srw_ss())[every_var_def]>> @@ -824,8 +881,8 @@ val inst_select_exp_flat_exp_conventions = Q.prove(` EVERY_CASE_TAC>>full_simp_tac(srw_ss())[flat_exp_conventions_def,inst_select_exp_def,LET_THM]); Theorem inst_select_flat_exp_conventions: - ∀c temp prog. - flat_exp_conventions (inst_select c temp prog) + ∀c temp prog. + flat_exp_conventions (inst_select c temp prog) Proof ho_match_mp_tac inst_select_ind >>srw_tac[][]>> full_simp_tac(srw_ss())[flat_exp_conventions_def,inst_select_def,LET_THM]>> @@ -845,11 +902,11 @@ val inst_select_exp_full_inst_ok_less = Q.prove(` ); Theorem inst_select_full_inst_ok_less: - ∀c temp prog. - addr_offset_ok c 0w ∧ - every_inst (inst_ok_less c) prog - ⇒ - full_inst_ok_less c (inst_select c temp prog) + ∀c temp prog. + addr_offset_ok c 0w ∧ + every_inst (inst_ok_less c) prog + ⇒ + full_inst_ok_less c (inst_select c temp prog) Proof ho_match_mp_tac inst_select_ind>> rw[inst_select_def,full_inst_ok_less_def,every_inst_def]>> @@ -862,11 +919,11 @@ QED (*Semantics preservation*) Theorem three_to_two_reg_correct: - ∀prog s res s'. - every_inst distinct_tar_reg prog ∧ - evaluate (prog,s) = (res,s') ∧ res ≠ SOME Error - ⇒ - evaluate(three_to_two_reg prog,s) = (res,s') + ∀prog s res s'. + every_inst distinct_tar_reg prog ∧ + evaluate (prog,s) = (res,s') ∧ res ≠ SOME Error + ⇒ + evaluate(three_to_two_reg prog,s) = (res,s') Proof ho_match_mp_tac three_to_two_reg_ind>> srw_tac[][]>>full_simp_tac(srw_ss())[three_to_two_reg_def,evaluate_def,state_component_equality]>> @@ -908,20 +965,20 @@ QED (* Syntactic three_to_two_reg *) Theorem three_to_two_reg_two_reg_inst: - ∀prog. every_inst two_reg_inst (three_to_two_reg prog) + ∀prog. every_inst two_reg_inst (three_to_two_reg prog) Proof ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>>full_simp_tac(srw_ss())[every_inst_def,two_reg_inst_def,three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[] QED Theorem three_to_two_reg_wf_cutsets: - ∀prog. wf_cutsets prog ⇒ wf_cutsets (three_to_two_reg prog) + ∀prog. wf_cutsets prog ⇒ wf_cutsets (three_to_two_reg prog) Proof ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>> full_simp_tac(srw_ss())[wf_cutsets_def,three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[] QED Theorem three_to_two_reg_pre_alloc_conventions: - ∀prog. pre_alloc_conventions prog ⇒ pre_alloc_conventions (three_to_two_reg prog) + ∀prog. pre_alloc_conventions prog ⇒ pre_alloc_conventions (three_to_two_reg prog) Proof ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>> full_simp_tac(srw_ss())[pre_alloc_conventions_def,every_stack_var_def,three_to_two_reg_def,LET_THM,call_arg_convention_def,inst_arg_convention_def]>> @@ -932,15 +989,15 @@ Proof QED Theorem three_to_two_reg_flat_exp_conventions: - ∀prog. flat_exp_conventions prog ⇒ flat_exp_conventions (three_to_two_reg prog) + ∀prog. flat_exp_conventions prog ⇒ flat_exp_conventions (three_to_two_reg prog) Proof ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>> full_simp_tac(srw_ss())[flat_exp_conventions_def,three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[] QED Theorem three_to_two_reg_full_inst_ok_less: - ∀prog. full_inst_ok_less c prog ⇒ - full_inst_ok_less c (three_to_two_reg prog) + ∀prog. full_inst_ok_less c prog ⇒ + full_inst_ok_less c (three_to_two_reg prog) Proof ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>> full_simp_tac(srw_ss())[three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>fs[full_inst_ok_less_def] @@ -960,8 +1017,8 @@ val inst_select_exp_no_lab = Q.prove(` rpt(TOP_CASE_TAC>>fs[extract_labels_def,inst_select_exp_def])) Theorem inst_select_lab_pres: - ∀c temp prog. - extract_labels prog = extract_labels (inst_select c temp prog) + ∀c temp prog. + extract_labels prog = extract_labels (inst_select c temp prog) Proof ho_match_mp_tac inst_select_ind>>rw[inst_select_def,extract_labels_def]>> TRY(metis_tac[inst_select_exp_no_lab])>> @@ -970,8 +1027,8 @@ Proof QED Theorem three_to_two_reg_lab_pres: - ∀prog. - extract_labels prog = extract_labels (three_to_two_reg prog) + ∀prog. + extract_labels prog = extract_labels (three_to_two_reg prog) Proof ho_match_mp_tac three_to_two_reg_ind>>rw[three_to_two_reg_def,extract_labels_def]>>EVERY_CASE_TAC>>fs[] QED diff --git a/compiler/backend/proofs/word_simpProofScript.sml b/compiler/backend/proofs/word_simpProofScript.sml index 06a857093e..ab6cda6bc0 100644 --- a/compiler/backend/proofs/word_simpProofScript.sml +++ b/compiler/backend/proofs/word_simpProofScript.sml @@ -968,6 +968,10 @@ Proof (fs [const_fp_loop_def] \\ rw [evaluate_def] \\ every_case_tac \\ fs [] \\ metis_tac [cs_delete_if_set]) + >- (** OpCurrHeap **) + (fs [const_fp_loop_def] \\ rw [evaluate_def] \\ + every_case_tac \\ fs [] \\ metis_tac [cs_delete_if_set]) + >- (** MustTerminate **) (rpt (rpt gen_tac \\ DISCH_TAC) \\ fs [const_fp_loop_def] \\ pairarg_tac \\ fs [] \\ qpat_x_assum `_ = p'` (assume_tac o GSYM) \\ fs [evaluate_def] \\ @@ -998,6 +1002,7 @@ Proof \\ (* Otherwise *) (rpt (pairarg_tac \\ fs []) \\ every_case_tac \\ rw [evaluate_def] \\ res_tac \\ fs [lookup_inter_eq] \\ every_case_tac \\ rw [])) + >- (** Call **) (rpt (rpt gen_tac \\ DISCH_TAC) \\ fs [const_fp_loop_def, evaluate_def] \\ qpat_x_assum `_ = (res, s')` mp_tac \\ @@ -1038,6 +1043,7 @@ Proof >- (imp_res_tac evaluate_consts \\ imp_res_tac pop_env_gc_fun \\ fs [set_var_def, push_env_gc_fun]) >- rw[]) + >- (** FFI **) (fs [const_fp_loop_def] \\ rw [evaluate_def] \\ every_case_tac \\ fs [] \\ @@ -1195,9 +1201,9 @@ val Seq_assoc_no_inst = Q.prove(` every_case_tac>>fs[]) Theorem compile_exp_no_inst: - ∀prog. - every_inst (inst_ok_less ac) prog ⇒ - every_inst (inst_ok_less ac) (compile_exp prog) + ∀prog. + every_inst (inst_ok_less ac) prog ⇒ + every_inst (inst_ok_less ac) (compile_exp prog) Proof fs[compile_exp_def]>> metis_tac[simp_if_no_inst,Seq_assoc_no_inst,every_inst_def, diff --git a/compiler/backend/proofs/word_to_stackProofScript.sml b/compiler/backend/proofs/word_to_stackProofScript.sml index bbecf594b6..86694661cc 100644 --- a/compiler/backend/proofs/word_to_stackProofScript.sml +++ b/compiler/backend/proofs/word_to_stackProofScript.sml @@ -5711,6 +5711,54 @@ Proof \\ metis_tac[state_rel_set_store] QED +Theorem comp_OpCurrHeap_correct: + ^(get_goal "OpCurrHeap") +Proof + REPEAT STRIP_TAC \\ fs[get_labels_def] + \\ fs[flat_exp_conventions_def] + \\ fs[comp_def,LET_THM] + \\ pairarg_tac \\ fs[] + \\ fs[wordSemTheory.evaluate_def,wordSemTheory.word_exp_def,the_words_def,AllCaseEqs()] + \\ gvs [] \\ qexists_tac`0` \\ simp[] + \\ CONV_TAC SWAP_EXISTS_CONV + \\ qexists_tac`NONE` \\ simp[] + \\ CONV_TAC (PATH_CONV "ralrlrrlrr" (UNBETA_CONV “src_r:num”)) + \\ match_mp_tac (GEN_ALL wStackLoad_thm1_weak) + \\ gvs[convs_def,reg_allocTheory.is_phy_var_def,GSYM EVEN_MOD2,EVEN_EXISTS] + \\ asm_exists_tac \\ fs [] + \\ fs [get_var_def] + \\ asm_exists_tac \\ fs [] \\ rw [] + \\ ‘t.use_store’ by fs [state_rel_def] + THEN1 + (qmatch_goalsub_abbrev_tac `wRegWrite1 kont (2 * m)` + \\ qmatch_goalsub_abbrev_tac `state_rel _ _ _ (set_var _ v _)` + \\ drule_then(qspecl_then [`v`,`m`,`kont`] mp_tac) (GEN_ALL wRegWrite1_thm1) + \\ unabbrev_all_tac + \\ fs[wordLangTheory.max_var_def,GSYM LEFT_ADD_DISTRIB] + \\ reverse impl_tac >- metis_tac[] + \\ rw [] \\ fs [stackSemTheory.evaluate_def,stackSemTheory.word_exp_def] + \\ fs [AllCaseEqs()] + \\ ‘FLOOKUP t.store CurrHeap = FLOOKUP s.store CurrHeap’ by + fs [state_rel_def,DOMSUB_FLOOKUP_THM] \\ fs [] + \\ ‘get_var (2 * m') s = SOME (Word x)’ by fs [get_var_def] + \\ imp_res_tac state_rel_get_var_imp \\ fs []) + \\ qmatch_goalsub_abbrev_tac `wRegWrite1 kont (2 * m)` + \\ qmatch_goalsub_abbrev_tac `state_rel _ _ _ (set_var _ v _)` + \\ qmatch_goalsub_abbrev_tac ‘_,set_var _ kval _’ + \\ ‘state_rel k f f' s (set_var k kval t) lens’ by fs [] + \\ drule_then(qspecl_then [`v`,`m`,`kont`] mp_tac) (GEN_ALL wRegWrite1_thm1) + \\ unabbrev_all_tac + \\ fs[wordLangTheory.max_var_def,GSYM LEFT_ADD_DISTRIB] + \\ reverse impl_tac >- metis_tac[] + \\ rw [] \\ fs [stackSemTheory.evaluate_def,stackSemTheory.word_exp_def] + \\ fs [AllCaseEqs()] + \\ ‘FLOOKUP t.store CurrHeap = FLOOKUP s.store CurrHeap’ by + fs [state_rel_def,DOMSUB_FLOOKUP_THM] \\ fs [] + \\ ‘get_var (2 * m') s = SOME (Word x)’ by fs [get_var_def] + \\ imp_res_tac state_rel_get_var_imp2 \\ fs [] + \\ fs [stackSemTheory.set_var_def,FLOOKUP_UPDATE] +QED + Theorem comp_Store_correct: ^(get_goal "Store") Proof @@ -8278,7 +8326,7 @@ Proof comp_Get_correct,comp_Set_correct,comp_Store_correct,comp_Tick_correct,comp_MustTerminate_correct, comp_Seq_correct,comp_Return_correct,comp_Raise_correct,comp_If_correct,comp_LocValue_correct, comp_Install_correct,comp_CodeBufferWrite_correct,comp_DataBufferWrite_correct, - comp_FFI_correct,comp_Call_correct + comp_FFI_correct,comp_OpCurrHeap_correct,comp_Call_correct ] QED @@ -8944,6 +8992,7 @@ Proof TRY(Cases_on`b`>>Cases_on`r`)>>EVAL_TAC>> EVERY_CASE_TAC>>EVAL_TAC) >- rpt (EVERY_CASE_TAC>>EVAL_TAC) + >- rpt (EVERY_CASE_TAC>>EVAL_TAC) >- (rpt(pairarg_tac>>fs[])>>EVAL_TAC) >- (Cases_on`ri`>>fs[wRegImm2_def,wReg2_def]>>EVERY_CASE_TAC>> @@ -9113,6 +9162,14 @@ Proof (PairCases_on`kf'`>> ntac 3 (EVAL_TAC>>rw[])>> rpt(EVAL_TAC>>rw[])) + >- + (PairCases_on`kf` \\ EVAL_TAC + \\ rw [] \\ EVAL_TAC + \\ fs[inst_ok_less_def,inst_arg_convention_def,every_inst_def, + two_reg_inst_def,wordLangTheory.every_var_inst_def,full_inst_ok_less_def, + reg_allocTheory.is_phy_var_def,asmTheory.fp_reg_ok_def] + \\ rw [] \\ EVAL_TAC \\ fs [] \\ gvs [] + \\ CCONTR_TAC \\ gvs []) >- (fs wconvs>> ntac 4 (pop_assum mp_tac)>> @@ -9212,6 +9269,9 @@ Proof >- (PairCases_on`kf'`>> rpt(EVAL_TAC>>rw[])) + >- + (PairCases_on`kf`>> + rpt(EVAL_TAC>>rw[])) >- (rpt(pairarg_tac>>fs[])>> EVAL_TAC>>fs[]) @@ -9289,16 +9349,16 @@ Proof QED Theorem stack_move_alloc_arg: - ∀n st off i p. - alloc_arg p ⇒ - alloc_arg (stack_move n st off i p) + ∀n st off i p. + alloc_arg p ⇒ + alloc_arg (stack_move n st off i p) Proof Induct>>rw[stack_move_def,alloc_arg_def] QED Theorem word_to_stack_alloc_arg: - ∀p n args. - alloc_arg (FST(word_to_stack$comp p n args)) + ∀p n args. + alloc_arg (FST(word_to_stack$comp p n args)) Proof recInduct comp_ind >> fs[comp_def,alloc_arg_def,FORALL_PROD,wRegWrite1_def,wLive_def]>> @@ -9315,7 +9375,12 @@ Proof fs[wInst_def,wRegWrite1_def,wReg1_def,wReg2_def,wRegWrite2_def]>> BasicProvers.EVERY_CASE_TAC>> fs[wStackLoad_def,alloc_arg_def]) - >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[alloc_arg_def,wStackLoad_def]) + >- + (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>> + fs[alloc_arg_def,wStackLoad_def]) + >- + (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>> + fs[alloc_arg_def,wStackLoad_def]) >- rpt (pairarg_tac>>fs[alloc_arg_def]) >- (rpt (pairarg_tac>>fs[alloc_arg_def])>> Cases_on`ri`>>fs[wReg1_def,wRegImm2_def,wReg2_def]>>BasicProvers.EVERY_CASE_TAC>>fs[]>>rveq>>fs[wStackLoad_def,alloc_arg_def]) @@ -9343,19 +9408,19 @@ Proof QED Theorem stack_move_reg_bound: - ∀n st off i p k. - i < k ∧ - reg_bound p k ⇒ - reg_bound (stack_move n st off i p) k + ∀n st off i p k. + i < k ∧ + reg_bound p k ⇒ + reg_bound (stack_move n st off i p) k Proof Induct>>rw[stack_move_def,reg_bound_def] QED Theorem word_to_stack_reg_bound: - ∀p n args. - post_alloc_conventions (FST args) p ∧ - 4 ≤ FST args ⇒ - reg_bound (FST(word_to_stack$comp p n args)) (FST args+2) + ∀p n args. + post_alloc_conventions (FST args) p ∧ + 4 ≤ FST args ⇒ + reg_bound (FST(word_to_stack$comp p n args)) (FST args+2) Proof recInduct comp_ind >>fs[comp_def,reg_bound_def,FORALL_PROD,wRegWrite1_def,wLive_def]>>rw[]>> fs[reg_bound_def,convs_def] @@ -9374,7 +9439,12 @@ Proof fs[wInst_def,wRegWrite1_def,wReg1_def,wReg2_def,wRegWrite2_def]>> BasicProvers.EVERY_CASE_TAC>> fs[wStackLoad_def,reg_bound_def]>>fs [reg_bound_def,convs_def,inst_arg_convention_def]) - >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[reg_bound_def,wStackLoad_def]) + >- + (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>> + fs[reg_bound_def,wStackLoad_def]) + >- + (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>> + fs[reg_bound_def,wStackLoad_def]) >- rpt (pairarg_tac>>fs [reg_bound_def]) >- (rpt (pairarg_tac>>fs [reg_bound_def])>> Cases_on`ri`>>fs[wReg1_def,wRegImm2_def,wReg2_def]>>BasicProvers.EVERY_CASE_TAC>>fs[]>>rveq>>fs[wStackLoad_def,reg_bound_def]) @@ -9403,17 +9473,17 @@ Proof QED Theorem stack_move_call_args: - ∀n st off i p. - call_args p 1 2 3 4 0 ⇒ - call_args (stack_move n st off i p) 1 2 3 4 0 + ∀n st off i p. + call_args p 1 2 3 4 0 ⇒ + call_args (stack_move n st off i p) 1 2 3 4 0 Proof Induct>>rw[stack_move_def,call_args_def] QED Theorem word_to_stack_call_args: - ∀p n args. - post_alloc_conventions (FST args) p ⇒ - call_args (FST(word_to_stack$comp p n args)) 1 2 3 4 0 + ∀p n args. + post_alloc_conventions (FST args) p ⇒ + call_args (FST(word_to_stack$comp p n args)) 1 2 3 4 0 Proof ho_match_mp_tac comp_ind >> fs[comp_def,call_args_def,FORALL_PROD,wRegWrite1_def,wLive_def,convs_def]>>rw[]>> @@ -9433,6 +9503,7 @@ Proof BasicProvers.EVERY_CASE_TAC>> fs[wStackLoad_def,convs_def]>>fs [call_args_def]) >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[call_args_def,wStackLoad_def]) + >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[call_args_def,wStackLoad_def]) >- rpt (pairarg_tac>>fs [call_args_def,convs_def]) >- (rpt (pairarg_tac>>fs [call_args_def])>> Cases_on`ri`>>fs[wReg1_def,wRegImm2_def,wReg2_def]>>BasicProvers.EVERY_CASE_TAC>>fs[]>>rveq>>fs[wStackLoad_def,call_args_def]) @@ -9463,10 +9534,10 @@ val reg_bound_def = stackPropsTheory.reg_bound_def val reg_bound_inst_def = stackPropsTheory.reg_bound_inst_def Theorem reg_bound_mono: - ∀p k k'. - reg_bound p k ∧ - k ≤ k' ⇒ - reg_bound p k' + ∀p k k'. + reg_bound p k ∧ + k ≤ k' ⇒ + reg_bound p k' Proof ho_match_mp_tac reg_bound_ind>>rw[reg_bound_def]>> rpt(TOP_CASE_TAC>>fs[])>> @@ -9534,7 +9605,7 @@ Proof QED Theorem compile_word_to_stack_convs: - ∀p bm q bm'. + ∀p bm q bm'. compile_word_to_stack k p bm = (q,bm') ∧ EVERY (λ(n,m,p). full_inst_ok_less c p ∧ @@ -9596,9 +9667,10 @@ val stack_move_code_labels = Q.prove(` Theorem word_to_stack_comp_code_labels: ∀prog bs kf n. - good_handlers n prog ⇒ - get_code_labels (FST (comp prog bs kf)) ⊆ - (raise_stub_location,0n) INSERT ((IMAGE (λn.(n,0)) (get_code_labels prog)) ∪ stack_get_handler_labels n (FST (comp prog bs kf))) + good_handlers n prog ⇒ + get_code_labels (FST (comp prog bs kf)) ⊆ + (raise_stub_location,0n) INSERT ((IMAGE (λn.(n,0)) (get_code_labels prog)) ∪ + stack_get_handler_labels n (FST (comp prog bs kf))) Proof ho_match_mp_tac word_to_stackTheory.comp_ind>> rw[word_to_stackTheory.comp_def]>> @@ -9623,6 +9695,7 @@ Proof >> rpt(first_x_assum drule)>>rw[]>> TRY(fs[SUBSET_DEF]>>metis_tac[]) + >- (rw [wRegWrite1_def]) >- (TOP_CASE_TAC>>fs[]>>pairarg_tac>>fs[get_code_handler_labels_wStackLoad]) >- @@ -9670,7 +9743,7 @@ Proof >> fs[SUBSET_DEF]>> metis_tac[] -QED; +QED Theorem word_to_stack_good_code_labels: compile asm_conf progs = (bs,fs,prog') ∧ @@ -9696,7 +9769,7 @@ Proof metis_tac[]) >> fs[SUBSET_DEF] -QED; +QED Theorem word_to_stack_good_code_labels_incr: raise_stub_location ∈ elabs ∧ @@ -9718,7 +9791,7 @@ Proof metis_tac[]) >> fs[SUBSET_DEF] -QED; +QED Triviality sub_union_lemma: x SUBSET y ==> x SUBSET y UNION z @@ -9750,7 +9823,7 @@ Proof (simp[backendPropsTheory.restrict_nonzero_def,Abbr`xxx`,EXTENSION,MEM_MAP]>> metis_tac[SND])>> simp[] -QED; +QED Theorem word_to_stack_good_handler_labels_incr: EVERY (λ(n,m,pp). good_handlers n pp) prog ⇒ @@ -9774,6 +9847,6 @@ Proof (simp[backendPropsTheory.restrict_nonzero_def,Abbr`xxx`,EXTENSION,MEM_MAP]>> metis_tac[SND])>> simp[] -QED; +QED val _ = export_theory(); diff --git a/compiler/backend/proofs/word_to_wordProofScript.sml b/compiler/backend/proofs/word_to_wordProofScript.sml index 3b819a4880..5370e93829 100644 --- a/compiler/backend/proofs/word_to_wordProofScript.sml +++ b/compiler/backend/proofs/word_to_wordProofScript.sml @@ -175,7 +175,7 @@ val code_rel_union_fromAList = Q.prove(` first_x_assum drule>>rw[]>> simp[]>>metis_tac[]); -val compile_single_correct = Q.prove(` +Theorem compile_single_correct[local]: ∀prog (st:('a,'c,'ffi) wordSem$state) l coracle cc. code_rel st.code l /\ (domain st.code = domain l) ∧ @@ -196,8 +196,8 @@ val compile_single_correct = Q.prove(` rst1 = rst with <| code:=rst1.code ; compile_oracle := (I ## MAP (λp. compile_single tt kk aa co (p,NONE))) o rst.compile_oracle; - compile:=cc |>`, (* todo: rst1.perm? *) - + compile:=cc |> (* todo: rst1.perm? *) +Proof (*recInduct doesn't seem to give a nice induction thm*) completeInduct_on`((st:('a,'c,'ffi)wordSem$state).termdep)`>> completeInduct_on`((st:('a,'c,'ffi)wordSem$state).clock)`>> @@ -234,8 +234,6 @@ val compile_single_correct = Q.prove(` rw[] >> rw[]>> fs[state_component_equality]) - - >- (*Call -- the hard case*) (fs[evaluate_def]>> TOP_CASE_TAC>> fs [] >> @@ -547,7 +545,7 @@ val compile_single_correct = Q.prove(` rw[]>>fs[]>> pairarg_tac>>fs[]>> qpat_x_assum`rst1 = _` SUBST_ALL_TAC>>fs[]) - >- + >- (* If *) (simp[evaluate_def,get_var_def,get_var_imm_def]>> ntac 2 (TOP_CASE_TAC>>full_simp_tac(srw_ss())[])>> Cases_on`r`>>full_simp_tac(srw_ss())[get_var_imm_def,get_var_def]>> @@ -556,7 +554,7 @@ val compile_single_correct = Q.prove(` TRY(qpat_abbrev_tac`prog = p0`)>> first_x_assum(qspecl_then[`prog`,`st`,`l`,`cc`] mp_tac)>> (impl_tac>-size_tac>>srw_tac[][])) - >- + >- (* Alloc *) (qexists_tac`st.permute`>>fs[rm_perm]>> fs[evaluate_def,get_var_def]>> ntac 2 (TOP_CASE_TAC>>fs[])>> @@ -571,10 +569,11 @@ val compile_single_correct = Q.prove(` Cases_on`x'`>>fs[]>>Cases_on`h`>>fs[]>> EVERY_CASE_TAC>>fs[has_space_def]>> rfs[call_env_def,flush_state_def]) - >- tac - >- tac - >- tac - >- (tac \\ fs[domain_lookup] \\ metis_tac[] ) + >- (rename [‘Raise’] \\ tac) + >- (rename [‘Return’] \\ tac) + >- (rename [‘Tick’] \\ tac) + >- (rename [‘OpCurrHeap’] \\ tac) + >- (rename [‘LocValue’] \\ tac \\ fs[domain_lookup] \\ metis_tac[]) >- (* Install *) (qexists_tac`st.permute`>>fs[rm_perm]>> ntac 3 (last_x_assum kall_tac)>> @@ -596,11 +595,10 @@ val compile_single_correct = Q.prove(` simp[domain_fromAList]>>AP_TERM_TAC>> simp[EXTENSION,MAP_MAP_o,compile_single_def,MEM_MAP,EXISTS_PROD])>> simp[state_component_equality,o_DEF]) - >- (*CBW*) tac - >- (*DBW*) tac - >- (*FFI*) - (tac>> - Cases_on`call_FFI st.ffi s x'' x'`>>simp[])); + >- (rename [‘CodeBufferWrite’] \\ tac) + >- (rename [‘DataBufferWrite’] \\ tac) + >- (rename [‘FFI’] \\ tac \\ Cases_on`call_FFI st.ffi s x'' x'` \\ simp[]) +QED Theorem compile_word_to_word_thm: code_rel (st:('a,'c,'ffi) wordSem$state).code l ∧ diff --git a/compiler/backend/semantics/stackPropsScript.sml b/compiler/backend/semantics/stackPropsScript.sml index a419025e56..68bd1f9436 100644 --- a/compiler/backend/semantics/stackPropsScript.sml +++ b/compiler/backend/semantics/stackPropsScript.sml @@ -751,6 +751,8 @@ val inst_name_def = Define` val stack_asm_name_def = Define` (stack_asm_name c ((Inst i):'a stackLang$prog) ⇔ inst_name c i) ∧ + (stack_asm_name c (OpCurrHeap b r1 r2) ⇔ + (c.two_reg_arith ⇒ r1 = r2) ∧ reg_name r1 c ∧ reg_name r2 c) ∧ (stack_asm_name c (CodeBufferWrite r1 r2) ⇔ reg_name r1 c ∧ reg_name r2 c) ∧ (stack_asm_name c (DataBufferWrite r1 r2) ⇔ reg_name r1 c ∧ reg_name r2 c) ∧ (stack_asm_name c (Seq p1 p2) ⇔ stack_asm_name c p1 ∧ stack_asm_name c p2) ∧ @@ -777,6 +779,7 @@ val fixed_names_def = Define` val stack_asm_remove_def = Define` (stack_asm_remove c ((Get n s):'a stackLang$prog) ⇔ reg_name n c) ∧ + (stack_asm_remove c (OpCurrHeap binop v src) ⇔ reg_name v c ∧ reg_name src c) ∧ (stack_asm_remove c (Set s n) ⇔ reg_name n c) ∧ (stack_asm_remove c (StackStore n n0) ⇔ reg_name n c) ∧ (stack_asm_remove c (StackStoreAny n n0) ⇔ reg_name n c ∧ reg_name n0 c) ∧ @@ -859,6 +862,8 @@ val reg_bound_def = Define ` v1 < k) /\ (reg_bound (Get v1 n) k <=> v1 < k) /\ + (reg_bound (OpCurrHeap op v1 v2) k <=> + v1 < k ∧ v2 < k) /\ (reg_bound (Set n v1) k <=> v1 < k /\ n <> BitmapBase) /\ (reg_bound (LocValue v1 l1 l2) k <=> diff --git a/compiler/backend/semantics/stackSemScript.sml b/compiler/backend/semantics/stackSemScript.sml index 10703c4537..2b4c3ee800 100644 --- a/compiler/backend/semantics/stackSemScript.sml +++ b/compiler/backend/semantics/stackSemScript.sml @@ -142,7 +142,7 @@ val word_exp_def = tDefine "word_exp" ` (WF_REL_TAC `measure (exp_size ARB o SND)` \\ REPEAT STRIP_TAC \\ IMP_RES_TAC wordLangTheory.MEM_IMP_exp_size \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`)) - \\ DECIDE_TAC) + \\ DECIDE_TAC); val get_var_def = Define ` get_var v (s:('a,'c,'ffi) stackSem$state) = FLOOKUP s.regs v`; @@ -545,6 +545,11 @@ val evaluate_def = tDefine "evaluate" ` case get_var v s of | SOME w => (NONE, set_store name w s) | NONE => (SOME Error, s)) /\ + (evaluate (OpCurrHeap binop v src,s) = + if ¬s.use_store then (SOME Error,s) else + case word_exp s (Op binop [Var src; Lookup CurrHeap]) of + | SOME w => (NONE, set_var v (Word w) s) + | _ => (SOME Error, s)) /\ (evaluate (Tick,s) = if s.clock = 0 then (SOME TimeOut,empty_env s) else (NONE,dec_clock s)) /\ diff --git a/compiler/backend/semantics/wordPropsScript.sml b/compiler/backend/semantics/wordPropsScript.sml index 33cac47243..f44a79d67b 100644 --- a/compiler/backend/semantics/wordPropsScript.sml +++ b/compiler/backend/semantics/wordPropsScript.sml @@ -675,6 +675,7 @@ Proof >- tac >- tac >- tac + >- tac >- (tac>>imp_res_tac mem_store_const>>full_simp_tac(srw_ss())[]) >- DECIDE_TAC >- `F`by DECIDE_TAC @@ -1484,6 +1485,13 @@ Proof rpt strip_tac>> HINT_EXISTS_TAC>> full_simp_tac(srw_ss())[GEN_ALL(SYM(SPEC_ALL word_exp_stack_swap)),s_key_eq_refl]) + >-(*OpCurrHeap*) + (fs[evaluate_def]>>every_case_tac>> + fs[set_var_def,s_key_eq_refl]>> + full_simp_tac(srw_ss())[set_store_def,s_key_eq_refl]>> + rpt strip_tac>> + HINT_EXISTS_TAC>> + full_simp_tac(srw_ss())[GEN_ALL(SYM(SPEC_ALL word_exp_stack_swap)),s_key_eq_refl]) >-(*Store*) (full_simp_tac(srw_ss())[evaluate_def]>>every_case_tac>> full_simp_tac(srw_ss())[mem_store_def,state_component_equality,s_key_eq_refl]>> @@ -2199,6 +2207,8 @@ Proof (every_case_tac>>fs[state_component_equality]) >- (fs[]>>every_case_tac>>fs[set_store_def,state_component_equality]) + >- + (fs[]>>every_case_tac>>fs[set_store_def,state_component_equality]) >- (fs[]>>every_case_tac>>fs[set_store_def,state_component_equality,mem_store_perm]) >- @@ -2477,11 +2487,11 @@ Proof QED Theorem locals_rel_word_exp: - ∀s exp w. - every_var_exp (λx. x < temp) exp ∧ - word_exp s exp = SOME w ∧ - locals_rel temp s.locals loc ⇒ - word_exp (s with locals:=loc) exp = SOME w + ∀s exp w. + every_var_exp (λx. x < temp) exp ∧ + word_exp s exp = SOME w ∧ + locals_rel temp s.locals loc ⇒ + word_exp (s with locals:=loc) exp = SOME w Proof ho_match_mp_tac word_exp_ind>>srw_tac[][]>> full_simp_tac(srw_ss())[word_exp_def,every_var_exp_def,locals_rel_def] @@ -2573,19 +2583,19 @@ val locals_rel_cut_env = Q.prove(` (*Extra temporaries not mentioned in program do not affect evaluation*) -val srestac = qpat_x_assum`A=res`sym_sub_tac>>full_simp_tac(srw_ss())[] +val srestac = qpat_x_assum`A=res`sym_sub_tac>>full_simp_tac(srw_ss())[]; Theorem locals_rel_evaluate_thm: - ∀prog st res rst loc temp. - evaluate (prog,st) = (res,rst) ∧ - res ≠ SOME Error ∧ - every_var (λx.x < temp) prog ∧ - locals_rel temp st.locals loc ⇒ - ∃loc'. - evaluate (prog,st with locals:=loc) = (res,rst with locals:=loc') ∧ - case res of - NONE => locals_rel temp rst.locals loc' - | SOME _ => rst.locals = loc' + ∀prog st res rst loc temp. + evaluate (prog,st) = (res,rst) ∧ + res ≠ SOME Error ∧ + every_var (λx.x < temp) prog ∧ + locals_rel temp st.locals loc ⇒ + ∃loc'. + evaluate (prog,st with locals:=loc) = (res,rst with locals:=loc') ∧ + case res of + | NONE => locals_rel temp rst.locals loc' + | SOME _ => rst.locals = loc' Proof completeInduct_on`prog_size (K 0) prog`>> rpt strip_tac>> @@ -2760,6 +2770,12 @@ Proof >- (IF_CASES_TAC>>full_simp_tac(srw_ss())[call_env_def,flush_state_def,state_component_equality,dec_clock_def]>> srestac>>full_simp_tac(srw_ss())[]>>metis_tac[]) + >- + (gvs[every_var_def,word_exp_def,AllCaseEqs(),the_words_def]>> + fs [PULL_EXISTS,state_component_equality,set_var_def] >> + imp_res_tac locals_rel_get_var>> + fs [get_var_def] \\ res_tac \\ fs [] >> + fs [locals_rel_def,lookup_insert]) >- (rw[]>>fs[set_var_def,state_component_equality]>>rveq>>fs[]>> qpat_x_assum`A=rst.locals` sym_sub_tac>> @@ -2913,10 +2929,11 @@ val two_reg_inst_def = Define` (two_reg_inst _ ⇔ T)` (* Recursor over instructions *) -val every_inst_def = Define` +Definition every_inst_def: (every_inst P (Inst i) ⇔ P i) ∧ (every_inst P (Seq p1 p2) ⇔ (every_inst P p1 ∧ every_inst P p2)) ∧ (every_inst P (If cmp r1 ri c1 c2) ⇔ every_inst P c1 ∧ every_inst P c2) ∧ + (every_inst P (OpCurrHeap bop r1 r2) ⇔ P (Arith (Binop bop r1 r2 (Reg r2)))) ∧ (every_inst P (MustTerminate p) ⇔ every_inst P p) ∧ (every_inst P (Call ret dest args handler) ⇔ (case ret of @@ -2925,7 +2942,8 @@ val every_inst_def = Define` (case handler of NONE => T | SOME (n,h,l1,l2) => every_inst P h))) ∧ - (every_inst P prog ⇔ T)` + (every_inst P prog ⇔ T) +End (* Every instruction is well-formed, including the jump hidden in If *) val full_inst_ok_less_def = Define` @@ -3375,6 +3393,8 @@ Proof every_case_tac >> fs [set_vars_def] >> rveq >> fs [state_fn_updates]) >- ( every_case_tac >> fs [set_store_def] >> rveq >> fs [state_fn_updates]) + >- ( + every_case_tac >> fs [set_store_def] >> rveq >> fs [state_fn_updates]) >- ( every_case_tac >> fs [mem_store_def] >> rveq >> fs [state_fn_updates]) >- ( @@ -3928,6 +3948,10 @@ Proof (fs [wordSemTheory.evaluate_def] \\ rveq \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs [] \\ fs [set_var_def]) + THEN1 (* OpCurrHeap *) + (fs [wordSemTheory.evaluate_def] \\ rveq + \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs [] + \\ fs [set_var_def]) THEN1 (* Store *) (fs [wordSemTheory.evaluate_def,mem_store_def] \\ rveq \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs [] diff --git a/compiler/backend/semantics/wordSemScript.sml b/compiler/backend/semantics/wordSemScript.sml index 3eb836bd62..fecc45091e 100644 --- a/compiler/backend/semantics/wordSemScript.sml +++ b/compiler/backend/semantics/wordSemScript.sml @@ -194,7 +194,7 @@ val word_exp_def = tDefine "word_exp" ` (WF_REL_TAC `measure (exp_size ARB o SND)` \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_IMP_exp_size \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`)) - \\ DECIDE_TAC) + \\ DECIDE_TAC); val get_var_def = Define ` get_var v ^s = sptree$lookup v s.locals`; @@ -699,6 +699,10 @@ val evaluate_def = tDefine "evaluate" ` case word_exp s exp of | NONE => (SOME Error, s) | SOME w => (NONE, set_store v w s)) /\ + (evaluate (OpCurrHeap b dst src,s) = + case word_exp s (Op b [Var src; Lookup CurrHeap]) of + | NONE => (SOME Error, s) + | SOME w => (NONE, set_var dst w s)) /\ (evaluate (Store exp v,s) = case (word_exp s exp, get_var v s) of | (SOME (Word a), SOME w) => diff --git a/compiler/backend/stackLangScript.sml b/compiler/backend/stackLangScript.sml index 007f0fd3d0..893de68c97 100644 --- a/compiler/backend/stackLangScript.sml +++ b/compiler/backend/stackLangScript.sml @@ -26,6 +26,7 @@ val _ = Datatype ` | Inst ('a inst) | Get num store_name | Set store_name num + | OpCurrHeap binop num num | Call ((stackLang$prog # num # num # num) option) (* return-handler code, link reg, labels l1,l2*) (num + num) (* target of call *) diff --git a/compiler/backend/stack_removeScript.sml b/compiler/backend/stack_removeScript.sml index 7e56adf7bd..f80ea05841 100644 --- a/compiler/backend/stack_removeScript.sml +++ b/compiler/backend/stack_removeScript.sml @@ -125,6 +125,8 @@ val comp_def = Define ` | Set name r => if name = CurrHeap then move (k+2) r else Inst (Mem Store r (Addr (k+1) (store_offset name))) + | OpCurrHeap op r n => + Inst (Arith (Binop op r n (Reg (k+2)))) (* remove stack operations *) | StackFree n => stack_free k n | StackAlloc n => stack_alloc jump k n diff --git a/compiler/backend/wordLangScript.sml b/compiler/backend/wordLangScript.sml index f4aace5feb..0c8e24b0d7 100644 --- a/compiler/backend/wordLangScript.sml +++ b/compiler/backend/wordLangScript.sml @@ -46,6 +46,7 @@ val _ = Datatype ` | Raise num | Return num num | Tick + | OpCurrHeap binop num num (* special case compiled well in stackLang *) | LocValue num num (* assign v1 := Loc v2 0 *) | Install num num num num num_set (* code buffer start, length of new code, data buffer start, length of new data, cut-set *) @@ -141,6 +142,7 @@ val every_var_def = Define ` (P num ∧ every_name P numset)) ∧ (every_var P (Raise num) = P num) ∧ (every_var P (Return num1 num2) = (P num1 ∧ P num2)) ∧ + (every_var P (OpCurrHeap _ num1 num2) = (P num1 ∧ P num2)) ∧ (every_var P Tick = T) ∧ (every_var P (Set n exp) = every_var_exp P exp) ∧ (every_var P p = T)` @@ -245,6 +247,7 @@ val max_var_def = Define ` (max_var (FFI ffi_index ptr1 len1 ptr2 len2 numset) = list_max (ptr1::len1::ptr2::len2::MAP FST (toAList numset))) ∧ (max_var (Raise num) = num) ∧ + (max_var (OpCurrHeap _ num1 num2) = MAX num1 num2) ∧ (max_var (Return num1 num2) = MAX num1 num2) ∧ (max_var Tick = 0) ∧ (max_var (LocValue r l1) = r) ∧ diff --git a/compiler/backend/word_allocScript.sml b/compiler/backend/word_allocScript.sml index 442603de37..f4688845ea 100644 --- a/compiler/backend/word_allocScript.sml +++ b/compiler/backend/word_allocScript.sml @@ -298,6 +298,10 @@ val ssa_cc_trans_def = Define` let num' = option_lookup ssa num in let mov = Move 0 [(2,num')] in (Seq mov (Raise 2),ssa,na)) ∧ + (ssa_cc_trans (OpCurrHeap b dst src) ssa na= + let src' = option_lookup ssa src in + let (dst',ssa',na') = next_var_rename dst ssa na in + (OpCurrHeap b dst' src',ssa',na')) ∧ (ssa_cc_trans (Return num1 num2) ssa na= let num1' = option_lookup ssa num1 in let num2' = option_lookup ssa num2 in @@ -483,6 +487,7 @@ val apply_colour_def = Define ` (apply_colour f (Return num1 num2) = Return (f num1) (f num2)) ∧ (apply_colour f Tick = Tick) ∧ (apply_colour f (Set n exp) = Set n (apply_colour_exp f exp)) ∧ + (apply_colour f (OpCurrHeap b n1 n2) = OpCurrHeap b (f n1) (f n2)) ∧ (apply_colour f p = p )` val _ = export_rewrites ["apply_nummap_key_def","apply_colour_exp_def" @@ -622,6 +627,7 @@ val get_live_def = Define` (get_live Tick live = live) ∧ (get_live (LocValue r l1) live = delete r live) ∧ (get_live (Set n exp) live = union (get_live_exp exp) live) ∧ + (get_live (OpCurrHeap b n1 n2) live = insert n2 () (delete n1 live)) ∧ (*Cut-set must be live, args input must be live For tail calls, there shouldn't be a liveset since control flow will never return into the same instance @@ -680,6 +686,10 @@ val remove_dead_def = Define` if lookup num live = NONE then (Skip,live) else (Get num store,delete num live)) ∧ + (remove_dead (OpCurrHeap b num src) live = + if lookup num live = NONE then + (Skip,live) + else (OpCurrHeap b num src,insert src () (delete num live))) ∧ (remove_dead (LocValue r l1) live = if lookup r live = NONE then (Skip,live) @@ -733,6 +743,7 @@ val get_writes_def = Define` (get_writes (Get num store) = insert num () LN) ∧ (get_writes (LocValue r l1) = insert r () LN) ∧ (get_writes (Install r1 _ _ _ _) = insert r1 () LN) ∧ + (get_writes (OpCurrHeap b r1 _) = insert r1 () LN) ∧ (get_writes prog = LN)` Theorem get_writes_pmatch: @@ -745,6 +756,7 @@ Theorem get_writes_pmatch: | Get num store => insert num () LN | LocValue r l1 => insert r () LN | Install r1 _ _ _ _ => insert r1 () LN + | OpCurrHeap b r1 _ => insert r1 () LN | prog => LN Proof rpt strip_tac @@ -863,6 +875,7 @@ val get_clash_tree_def = Define` (get_clash_tree Tick = Delta [] []) ∧ (get_clash_tree (LocValue r l1) = Delta [r] []) ∧ (get_clash_tree (Set n exp) = Delta [] (get_reads_exp exp)) ∧ + (get_clash_tree (OpCurrHeap b dst src) = Delta [dst] [src]) ∧ (get_clash_tree (Call ret dest args h) = let args_set = numset_list_insert args LN in dtcase ret of @@ -1072,6 +1085,8 @@ val get_heu_def = Define ` (dtcase exp of (Var r) => (add1_rhs_mem r lr,calls) | _ => (lr,calls))) ∧ (* General Set exp ignored *) + (get_heu fc (OpCurrHeap b dst src) (lr,calls) = + (add1_lhs_reg dst (add1_rhs_reg src lr),calls)) ∧ (get_heu fc (LocValue r l1) (lr,calls) = (add1_lhs_reg r lr,calls)) ∧ (get_heu fc (Seq s1 s2) lr = get_heu fc s2 (get_heu fc s1 lr)) ∧ diff --git a/compiler/backend/word_instScript.sml b/compiler/backend/word_instScript.sml index ca30f8715d..62dccffd52 100644 --- a/compiler/backend/word_instScript.sml +++ b/compiler/backend/word_instScript.sml @@ -175,6 +175,20 @@ val test = EVAL ``flatten_exp (pull_exp (Op Sub [Const 1w; Op Sub[Const 2w;Const Op Add [Const 4w; Const 5w; Op Add[Const 6w; Const 7w];Op Xor[Const 1w;Var y;Var x]] ; Const (8w:8 word)]))`` *) +Definition is_Lookup_CurrHeap_def: + is_Lookup_CurrHeap (Lookup CurrHeap) = T ∧ + is_Lookup_CurrHeap _ = F +End + +Theorem is_Lookup_CurrHeap_pmatch: + is_Lookup_CurrHeap e = + (case e of Lookup CurrHeap => T | _ => F) +Proof + rpt(CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV) >> every_case_tac >> + PURE_ONCE_REWRITE_TAC[LET_DEF] >> BETA_TAC) >> + fs [is_Lookup_CurrHeap_def] +QED + (* Maximal Munch instruction selection on (binary) expressions c is an asm_config to check validity of imms (TODO: assume 0w is accepted?) @@ -208,6 +222,13 @@ val inst_select_exp_def = tDefine "inst_select_exp" ` Get tar store_name) ∧ (*All ops are binary branching*) (inst_select_exp c tar temp (Op op [e1;e2]) = + if is_Lookup_CurrHeap e2 then + (let p1 = inst_select_exp c temp temp e1 in + Seq p1 (OpCurrHeap op tar temp)) + else if is_Lookup_CurrHeap e1 ∧ op ≠ Sub then + (let p2 = inst_select_exp c temp temp e2 in + Seq p2 (OpCurrHeap op tar temp)) + else let p1 = inst_select_exp c temp temp e1 in dtcase e2 of | Const w => @@ -262,7 +283,14 @@ Theorem inst_select_exp_pmatch: Get tar store_name (*All ops are binary branching*) | Op op [e1;e2] => - (case e2 of + (if is_Lookup_CurrHeap e2 then + (let p1 = inst_select_exp c temp temp e1 in + Seq p1 (OpCurrHeap op tar temp)) + else if is_Lookup_CurrHeap e1 ∧ op ≠ Sub then + (let p2 = inst_select_exp c temp temp e2 in + Seq p2 (OpCurrHeap op tar temp)) + else + case e2 of Const w => (*t = r op const*) if c.valid_imm (INL op) w then @@ -426,6 +454,8 @@ val three_to_two_reg_def = Define` Seq (Move 0 [r1,r2]) (Inst (Arith (AddOverflow r1 r1 r3 r4)))) ∧ (three_to_two_reg (Inst (Arith (SubOverflow r1 r2 r3 r4))) = Seq (Move 0 [r1,r2]) (Inst (Arith (SubOverflow r1 r1 r3 r4)))) ∧ + (three_to_two_reg (OpCurrHeap bop r1 r2) = + Seq (Move 0 [r1,r2]) (OpCurrHeap bop r1 r1)) ∧ (three_to_two_reg (Seq p1 p2) = Seq (three_to_two_reg p1) (three_to_two_reg p2)) ∧ (three_to_two_reg (MustTerminate p1) = @@ -459,6 +489,8 @@ Theorem three_to_two_reg_pmatch: Seq (Move 0 [r1,r2]) (Inst (Arith (AddOverflow r1 r1 r3 r4))) | (Inst (Arith (SubOverflow r1 r2 r3 r4))) => Seq (Move 0 [r1,r2]) (Inst (Arith (SubOverflow r1 r1 r3 r4))) + | (OpCurrHeap bop r1 r2) => + Seq (Move 0 [r1,r2]) (OpCurrHeap bop r1 r1) | (Seq p1 p2) => Seq (three_to_two_reg p1) (three_to_two_reg p2) | (MustTerminate p1) => diff --git a/compiler/backend/word_simpScript.sml b/compiler/backend/word_simpScript.sml index cd0e2497a3..f282204efe 100644 --- a/compiler/backend/word_simpScript.sml +++ b/compiler/backend/word_simpScript.sml @@ -322,6 +322,7 @@ val const_fp_loop_def = Define ` | Const c => (Assign v const_fp_e, insert v c cs) | _ => (Assign v const_fp_e, delete v cs)) /\ (const_fp_loop (Get v name) cs = (Get v name, delete v cs)) /\ + (const_fp_loop (OpCurrHeap b v w) cs = (OpCurrHeap b v w, delete v cs)) /\ (const_fp_loop (MustTerminate p) cs = let (p', cs') = const_fp_loop p cs in (MustTerminate p', cs')) /\ @@ -363,6 +364,7 @@ Theorem const_fp_loop_pmatch: | Const c => (Assign v (Const c), insert v c cs) | const_fp_e => (Assign v const_fp_e, delete v cs)) | (Get v name) => (Get v name, delete v cs) + | (OpCurrHeap b v w) => (OpCurrHeap b v w, delete v cs) | (MustTerminate p) => (let (p', cs') = const_fp_loop p cs in (MustTerminate p', cs')) @@ -403,6 +405,7 @@ Proof >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY] >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY] >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY] + >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY] >- (CONV_TAC(RAND_CONV(patternMatchesLib.PMATCH_ELIM_CONV)) >> every_case_tac >> fs[Once const_fp_loop_def]) >- (CONV_TAC(RAND_CONV(patternMatchesLib.PMATCH_ELIM_CONV)) diff --git a/compiler/backend/word_to_stackScript.sml b/compiler/backend/word_to_stackScript.sml index ef304cbe21..b0ec8866eb 100644 --- a/compiler/backend/word_to_stackScript.sml +++ b/compiler/backend/word_to_stackScript.sml @@ -252,6 +252,9 @@ val comp_def = Define ` let (xs,x) = wReg1 v1 kf in (wStackLoad xs (SeqStackFree (FST (SND kf)) (Return x 1)),bs)) /\ (comp (Raise v) bs kf = (Call NONE (INL raise_stub_location) NONE,bs)) /\ + (comp (OpCurrHeap b dst src) bs kf = + let (xs,src_r) = wReg1 src kf in + (wStackLoad xs (wRegWrite1 (\dst_r. OpCurrHeap b dst_r src_r) dst kf),bs)) /\ (comp (Tick) bs kf = (Tick,bs)) /\ (comp (MustTerminate p1) gs kf = comp p1 gs kf) /\ (comp (Seq p1 p2) bs kf = diff --git a/compiler/bootstrap/translation/to_word32ProgScript.sml b/compiler/bootstrap/translation/to_word32ProgScript.sml index 4f0a39353d..af4ed85bc6 100644 --- a/compiler/bootstrap/translation/to_word32ProgScript.sml +++ b/compiler/bootstrap/translation/to_word32ProgScript.sml @@ -251,6 +251,7 @@ val _ = translate (spec32 wordLangTheory.max_var_def) val _ = translate (conv32_RHS integer_wordTheory.WORD_LEi) val _ = translate (asmTheory.offset_ok_def |> SIMP_RULE std_ss [alignmentTheory.aligned_bitwise_and] |> conv32) +val _ = translate (is_Lookup_CurrHeap_pmatch |> conv32) val res = translate_no_ind (inst_select_exp_pmatch |> conv32 |> SIMP_RULE std_ss [word_mul_def,word_2comp_def] |> conv32) val ind_lemma = Q.prove( diff --git a/compiler/bootstrap/translation/to_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml index a2a15cad12..e10b1a6d05 100644 --- a/compiler/bootstrap/translation/to_word64ProgScript.sml +++ b/compiler/bootstrap/translation/to_word64ProgScript.sml @@ -250,6 +250,7 @@ val _ = translate (spec64 wordLangTheory.max_var_def) val _ = translate (conv64_RHS integer_wordTheory.WORD_LEi) val _ = translate (asmTheory.offset_ok_def |> SIMP_RULE std_ss [alignmentTheory.aligned_bitwise_and] |> conv64) +val _ = translate (is_Lookup_CurrHeap_pmatch |> conv64) val res = translate_no_ind (inst_select_exp_pmatch |> conv64 |> SIMP_RULE std_ss [word_mul_def,word_2comp_def] |> conv64) val ind_lemma = Q.prove( diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml index 301b725abb..d6003510cd 100644 --- a/translator/ml_translatorScript.sml +++ b/translator/ml_translatorScript.sml @@ -101,6 +101,27 @@ val PreImpEval_def = Define` (* Theorems *) +Theorem AppReturns_thm: + AppReturns P cl Q ⇔ + ∀v. P v ⇒ + ∃env exp. + do_opapp [cl;v] = SOME (env,exp) ∧ + ∀refs. + ∃refs' u. + eval_rel (empty_state with refs := refs) env exp + (empty_state with refs := refs++refs') u ∧ + Q u +Proof + fs [AppReturns_def] \\ eq_tac \\ rw [] + \\ first_x_assum drule + \\ Cases_on ‘cl’ \\ fs [do_opapp_def,AllCaseEqs()] + \\ rename [‘find_recfun x1 x2’] + \\ Cases_on ‘find_recfun x1 x2’ \\ fs [] + \\ PairCases_on ‘x’ \\ fs [] + \\ rename [‘ALL_DISTINCT xx’] + \\ Cases_on ‘ALL_DISTINCT xx’ \\ fs [] +QED + local val Eval_lemma = prove( ``∀env exp P.