open HolKernel boolLib bossLib Parse open intLib bitLib wordsLib integer_wordLib open optionLib combinLib finite_mapLib bitstringLib open state_monadTheory state_monad_lemmasTheory open sail_valuesAuxiliaryTheory stateAuxiliaryTheory open cheriTheory hoareTheory val _ = new_theory "test_raw_add"; val _ = Globals.max_print_depth := 10; (* MIPS register names ftp://www.linux-mips.org/pub/linux/mips/doc/ABI/MIPS-N32-ABI-Handbook.pdf *) val gpr_names_def = Define` gpr_names = [ "zero"; "at"; "v0"; "v1"; "a0"; "a1"; "a2"; "a3"; "a4"; "a5"; "a6"; "a7"; "t4"; "t5"; "t6"; "t7"; "s0"; "s1"; "s2"; "s3"; "s4"; "s5"; "s6"; "s7"; "t8"; "t9"; "kt0"; "kt1"; "gp"; "sp"; "s8"; "ra"]`; val PrePost_write_regS = Q.store_thm("PrePost_write_regS", `PrePost (λs. P (Value ()) (s with regstate := reg.write_to v s.regstate)) (write_regS reg v) P`, rw[write_regS_def,PrePost_updateS]); val PrePost_assert_expS_T = Q.store_thm("PrePost_assert_expS_T", `exp ⇒ PrePost (P (Value ())) (assert_expS exp msg) P`, rw[assert_expS_def,PrePost_returnS]); val PrePost_maybe_failS_SOME = Q.store_thm("PrePost_maybe_failS_SOME", `PrePost (P (Value x)) (maybe_failS msg (SOME x)) P`, rw[maybe_failS_def,PrePost_returnS]); (* val PrePost_MEMw_wrapper = Q.store_thm("PrePost_MEMw_wrapper", `PrePost P (MEMw_wrapper addr size data) Q`, MEMw_wrapper_def |> SIMP_RULE(srw_ss()++boolSimps.LET_ss)[] |> CONV_RULE(STRIP_QUANT_CONV(RAND_CONV(RATOR_CONV(RATOR_CONV(RAND_CONV(RAND_CONV(EVAL))))))) *) val PrePost_init_cp0_state = Q.store_thm("PrePost_init_cp0_state", `PrePost (λs. P (Value ()) (s with regstate := s.regstate with CP0Status := Mk_StatusReg (update_subrange_vec_dec (get_StatusReg s.regstate.CP0Status) 22 22 (cast_unit_vec0 B1)))) (init_cp0_state()) P`, EVAL_TAC \\ rw[]); (* val PrePost_init_cp2_state = Q.store_thm("PrePost_init_cp2_state", `PrePost P (init_cp2_state ()) Q`, rw[init_cp2_state_def] PrePost_def f"foreach" hyp stateTheory.foreachS_def \\ match_mp_tac PrePost_seqS \\ qexists_tac`P1` \\ conj_tac >- ( match_mp_tac PrePost_seqS \\ qexists_tac`P2` \\ conj_tac >- ( match_mp_tac PrePost_seqS \\ qexists_tac`P3` \\ conj_tac PrePost_strengthen_pre PrePost_write_regS ``init_cp2_state () s`` |> EVAL init_cp2_state_def |> SIMP_RULE (srw_ss()++boolSimps.LET_ss) [] f"init_cp2_state" |> *) val install_code_def = Define` install_code initialPC (code:word32 list) = iteriS (λi c. MEMw_wrapper (initialPC + 4w*(i2w i)) 4 c) code`; val clocked_whileS_def = Define` clocked_whileS clock vars cond body s = if 0n < clock then bindS (cond vars) (λcond_val s'. if cond_val then bindS (body vars) (λvars' s''. clocked_whileS (clock-1) vars' cond body s'') s' else returnS vars s') s else failS "timeout" s`; val install_and_run_def = Define` install_and_run code clock = seqS (seqS (install_code 0x40000000w code) (init_registers 0x9000000040000000w)) (clocked_whileS clock () (λunit_var. fetch_and_execute ()) (λunit_var. returnS ()))`; val PrePost_clocked_whileS_unit_T = Q.store_thm("PrePost_clocked_whileS_unit_T", `0 < k ∧ PrePostE P (cond ()) (λb s. b ∧ R s) (K (K F)) ∧ PrePost R (seqS (body ()) (clocked_whileS (k-1) () cond body)) Q ⇒ PrePost P (clocked_whileS k () cond body) Q`, rw[PrePost_def,PrePostE_def] \\ fs[Once clocked_whileS_def] \\ rfs[] \\ fs[bindS_def] \\ last_x_assum(qspec_then`s`mp_tac) \\ simp[] \\ disch_then(qspec_then`x`mp_tac) \\ simp[] \\ CASE_TAC \\ simp[] \\ BasicProvers.FULL_CASE_TAC \\ fs[] \\ strip_tac \\ rpt BasicProvers.VAR_EQ_TAC \\ fs[] \\ first_x_assum drule \\ simp[seqS_def, bindS_def,PULL_EXISTS] \\ disch_then match_mp_tac \\ BasicProvers.VAR_EQ_TAC \\ metis_tac[]); (* obtained from objdump -d test_raw_add.elf (with the cheri mips binutils version of objdump) test_raw_add.elf: file format elf64-bigmips Disassembly of section .text: 9000000040000000 : 9000000040000000: 24130001 li s3,1 9000000040000004: 24140002 li s4,2 9000000040000008: 02742020 add a0,s3,s4 900000004000000c: 240c0001 li t0,1 9000000040000010: 24050002 li a1,2 9000000040000014: 00ac2820 add a1,a1,t0 9000000040000018: 240c0001 li t0,1 900000004000001c: 24060002 li a2,2 9000000040000020: 01863020 add a2,t0,a2 9000000040000024: 24070001 li a3,1 9000000040000028: 00e73820 add a3,a3,a3 900000004000002c: 240c0001 li t0,1 9000000040000030: 240d0002 li t1,2 9000000040000034: 240e0003 li t2,3 9000000040000038: 018d7820 add t3,t0,t1 900000004000003c: 01ee4020 add a4,t3,t2 9000000040000040: 240c0001 li t0,1 9000000040000044: 240dffff li t1,-1 9000000040000048: 018d4820 add a5,t0,t1 900000004000004c: 240cffff li t0,-1 9000000040000050: 240dffff li t1,-1 9000000040000054: 018d5020 add a6,t0,t1 9000000040000058: 240cffff li t0,-1 900000004000005c: 240d0002 li t1,2 9000000040000060: 018d5820 add a7,t0,t1 9000000040000064: 240c0001 li t0,1 9000000040000068: 240dfffe li t1,-2 900000004000006c: 018d8020 add s0,t0,t1 9000000040000070: 4082d000 mtc0 v0,$26 ... 900000004000007c: 4082b800 mtc0 v0,$23 9000000040000080 : 9000000040000080: 1000ffff b 9000000040000080 9000000040000084: 00000000 nop *) val test_raw_add_insts_def = Define`test_raw_add_insts = [0x24130001w:word32 ;0x24140002w ;0x02742020w ;0x240c0001w ;0x24050002w ;0x00ac2820w ;0x240c0001w ;0x24060002w ;0x01863020w ;0x24070001w ;0x00e73820w ;0x240c0001w ;0x240d0002w ;0x240e0003w ;0x018d7820w ;0x01ee4020w ;0x240c0001w ;0x240dffffw ;0x018d4820w ;0x240cffffw ;0x240dffffw ;0x018d5020w ;0x240cffffw ;0x240d0002w ;0x018d5820w ;0x240c0001w ;0x240dfffew ;0x018d8020w ;0x4082d000w]`; fun check_name n = EVAL ``EL ^(numSyntax.term_of_int n) gpr_names``; val test_raw_add_post_def = Define` test_raw_add_post s = ( bindS (rGPR 19w) (λs3. (* check_name 19 *) seqS (assert_expS (s3 = 1w) "add modified first input") ( bindS (rGPR 20w) (λs4. (* check_name 20 *) seqS (assert_expS (s4 = 2w) "add modified second input") ( bindS (rGPR 04w) (λa0. (* check_name 04 *) seqS (assert_expS (a0 = 3w) "add failed") ( bindS (rGPR 05w) (λa1. (* check_name 05 *) seqS (assert_expS (a1 = 3w) "add into first input failed") ( bindS (rGPR 06w) (λa2. (* check_name 06 *) seqS (assert_expS (a2 = 3w) "add into second input failed") ( bindS (rGPR 07w) (λa3. (* check_name 07 *) seqS (assert_expS (a3 = 2w) "add into both inputs failed") ( bindS (rGPR 08w) (λa4. (* check_name 08 *) seqS (assert_expS (a4 = 6w) "add-to-add pipeline failed") ( bindS (rGPR 09w) (λa5. (* check_name 09 *) seqS (assert_expS (a5 = 0w) "positive plus negative to zero failed") ( bindS (rGPR 10w) (λa6. (* check_name 10 *) seqS (assert_expS (a6 = 0xfffffffffffffffew) "negative plus negative to negative failed") ( bindS (rGPR 11w) (λa7. (* check_name 11 *) seqS (assert_expS (a7 = 1w) "negative plus positive to positive failed") ( bindS (rGPR 16w) (λs0. (* check_name 16 *) (assert_expS (s0 = 0xffffffffffffffffw) "positive plus negative to negative failed")))))))))))))))))))))) s = {(Value (),s)})`; (* EVAL ``(LENGTH s.regstate.GPR = 32) ⇒ (bindS (rGPR 19w) (λs3. assert_expS (s3 = 1w) "fail") s = {(Value (),s)})`` |> SIMP_RULE (srw_ss())[] *) (* not true - m could produce lots of values that f collapses val bindS_eq_sing_Value = Q.store_thm("bindS_eq_sing_Value", `(bindS m f s = {(Value x,s')}) ⇔ ∃y s''. (m s = {(Value y,s'')}) ∧ (f y s'' = {(Value x,s')})`, rw[bindS_def] \\ reverse EQ_TAC >- ( rw[] \\ rw[] ) \\ rw[] \\ Cases_on `m s` \\ fs[] \\ Cases_on`t` \\ fs[] >- ( BasicProvers.EVERY_CASE_TAC \\ fs[] ) \\ CONV_TAC(LAND_CONV(REWR_CONV pred_setTheory.EXTENSION)) \\ rw[pairTheory.pair_case_eq, pairTheory.FORALL_PROD, state_monadTheory.result_case_eq,PULL_EXISTS] \\ metis_tac[pairTheory.PAIR_EQ] *) (* annoying because it depends on LENGTH s.regstate.GPR EVAL ``rGPR 19w s`` val test_raw_add_post_eq = ``test_raw_add_post s`` |> SIMP_CONV (srw_ss()) [test_raw_add_post_def] *) (* val decoded_insts1 = listLib.MAP_CONV EVAL ``MAP decode ^(rhs(concl test_raw_add_insts_def))`` val (SOME_is, oty) = decoded_insts1 |> concl |> rhs |> listSyntax.dest_list val asts = map rand SOME_is val ls2 = listLib.MAP_CONV EVAL ``MAP SOME ^(listSyntax.mk_list(asts,optionSyntax.dest_option oty))``; val test_raw_add_asts_def = Define` test_raw_add_asts = ^(rand(lhs(concl ls2)))`; val decoded_insts = TRANS decoded_insts1 (SYM ls2) |> ONCE_REWRITE_RULE[GSYM test_raw_add_insts_def, GSYM test_raw_add_asts_def] *) (* This is currently a non-starter, but something like it should be possible and better than a manual PrePost proof! Perhaps with the right curated compset? update: now it works! see compset below EVAL ``install_code 0x9000000040000000w test_raw_add_insts s`` *) fun mk_record_thms def = let val tm = lhs(concl (SPEC_ALL def)) val rty = type_of tm val tyop = #1 (dest_type rty) val fields = TypeBase.fields_of rty fun mktm (fieldname,_) = Term[QUOTE(tyop^"_"^fieldname^" "), ANTIQUOTE tm] val thms = map (SIMP_CONV (srw_ss()) [def] o mktm) fields in LIST_CONJ thms end val capRegToCapStruct_thms = mk_record_thms cheriTheory.capRegToCapStruct_def val instance_Sail_values_Bitvector_Machine_word_mword_dict_thms = mk_record_thms sail_valuesTheory.instance_Sail_values_Bitvector_Machine_word_mword_dict_def val default_cap_thms = mk_record_thms cheriTheory.default_cap_def val nextPC_ref_thms = mk_record_thms cheri_typesTheory.nextPC_ref_def val delayedPCC_ref_thms = mk_record_thms cheri_typesTheory.delayedPCC_ref_def val delayedPC_ref_thms = mk_record_thms cheri_typesTheory.delayedPC_ref_def val PCC_ref_thms = mk_record_thms cheri_typesTheory.PCC_ref_def val PC_ref_thms = mk_record_thms cheri_typesTheory.PC_ref_def val GPR_ref_thms = mk_record_thms cheri_typesTheory.GPR_ref_def val nextPCC_ref_thms = mk_record_thms cheri_typesTheory.nextPCC_ref_def val C_ref_thms = let fun get_def n = fetch"cheri_types"("C"^(StringCvt.padLeft#"0" 2(Int.toString n))^"_ref_def") in List.tabulate(32, mk_record_thms o get_def) end val TLBEntry_ref_thms = let fun get_def n = fetch"cheri_types"("TLBEntry"^(StringCvt.padLeft#"0" 2(Int.toString n))^"_ref_def") in List.tabulate(64, mk_record_thms o get_def) end val CP0Count_ref_thms = mk_record_thms cheri_typesTheory.CP0Count_ref_def val CP0Compare_ref_thms = mk_record_thms cheri_typesTheory.CP0Compare_ref_def val CP0Status_ref_thms = mk_record_thms cheri_typesTheory.CP0Status_ref_def val CP0BadVAddr_ref_thms = mk_record_thms cheri_typesTheory.CP0BadVAddr_ref_def val CP0EPC_ref_thms = mk_record_thms cheri_typesTheory.CP0EPC_ref_def val CP0Cause_ref_thms = mk_record_thms cheri_typesTheory.CP0Cause_ref_def val UART_WRITTEN_ref_thms = mk_record_thms cheri_typesTheory.UART_WRITTEN_ref_def val UART_WDATA_ref_thms = mk_record_thms cheri_typesTheory.UART_WDATA_ref_def val inCCallDelay_ref_thms = mk_record_thms cheri_typesTheory.inCCallDelay_ref_def val TLBRandom_ref_thms = mk_record_thms cheri_typesTheory.TLBRandom_ref_def val TLBWired_ref_thms = mk_record_thms cheri_typesTheory.TLBWired_ref_def val TLBContext_ref_thms = mk_record_thms cheri_typesTheory.TLBContext_ref_def val TLBXContext_ref_thms = mk_record_thms cheri_typesTheory.TLBXContext_ref_def val TLBEntryHi_ref_thms = mk_record_thms cheri_typesTheory.TLBEntryHi_ref_def val cap_addr_mask_thm = CONV_RULE(RAND_CONV EVAL) cheriTheory.cap_addr_mask_def val branchPending_ref_thms = mk_record_thms cheri_typesTheory.branchPending_ref_def val inBranchDelay_ref_thms = mk_record_thms cheri_typesTheory.inBranchDelay_ref_def val instCount_ref_thms = mk_record_thms cheri_typesTheory.instCount_ref_def val seqS_returnS = Q.store_thm("seqS_returnS", `seqS (returnS x) f = f`, rw[FUN_EQ_THM] \\ EVAL_TAC \\ rw[IN_DEF]); val seqS_returnS_s = Q.store_thm("seqS_returnS_s", `seqS (λs. returnS x (f s)) g = (λs. g (f s))`, rw[FUN_EQ_THM] \\ EVAL_TAC \\ rw[IN_DEF]); val bindS_returnS_s = Q.store_thm("bindS_returnS_s", `bindS (λs. returnS v (f s)) g = (λs. g v (f s))`, rw[FUN_EQ_THM] \\ EVAL_TAC \\ rw[IN_DEF]); val bindS_returnS_1 = Q.store_thm("bindS_returnS_1", `bindS (returnS v) f = f v`, rw[FUN_EQ_THM] \\ EVAL_TAC \\ rw[IN_DEF]); val bindS_readS = Q.store_thm("bindS_readS", `bindS (readS f) m = (λs. m (f s) s)`, rw[FUN_EQ_THM] \\ EVAL_TAC \\ rw[IN_DEF]); (* val cstest = wordsLib.words_compset(); val () = computeLib.extend_compset [ computeLib.Convs [ (``bindS``, 2, HO_REWR_CONV bindS_returnS_s) ], computeLib.Defs [ state_monadTheory.readS_def ] ] cstest; computeLib.CBV_CONV cstest ``bindS (λs. returnS x s) g`` *) val LENGTH_CapRegs = save_thm("LENGTH_CapRegs", EVAL ``LENGTH CapRegs``); val LENGTH_TLBEntries = save_thm("LENGTH_TLBEntries", EVAL ``LENGTH TLBEntries``); val cs0 = listLib.list_compset(); val () = computeLib.extend_compset [ computeLib.Defs [ CapRegs_def, TLBEntries_def ] ] cs0; val EL_CapRegs = save_thm("EL_CapRegs", let fun f n = computeLib.CBV_CONV cs0 ``EL ^(numSyntax.term_of_int n) CapRegs`` in LIST_CONJ ( List.tabulate(LENGTH_CapRegs |> concl |> rhs |> numSyntax.int_of_term, f) ) end); val HD_CapRegs = computeLib.CBV_CONV cs0 ``HD CapRegs``; val EL_TLBEntries = save_thm("EL_TLBEntries", let fun f n = computeLib.CBV_CONV cs0 ``EL ^(numSyntax.term_of_int n) TLBEntries`` in LIST_CONJ ( List.tabulate(LENGTH_TLBEntries |> concl |> rhs |> numSyntax.int_of_term, f) ) end); val HD_TLBEntries = computeLib.CBV_CONV cs0 ``HD TLBEntries``; val bcs = computeLib.bool_compset(); val () = computeLib.extend_compset [ computeLib.Tys [``:regstate``], computeLib.Defs (map #2 (ThmSetData.theory_data {settype = "compute", thy = "cheri_types" })), (* these should come out of regstate but seem not to... *) computeLib.Defs [ cheri_typesTheory.regstate_brss__0_accfupds, cheri_typesTheory.regstate_brss__1_accfupds, cheri_typesTheory.regstate_brss__2_accfupds, cheri_typesTheory.regstate_brss__3_accfupds, cheri_typesTheory.regstate_brss__4_accfupds, cheri_typesTheory.regstate_brss__5_accfupds, cheri_typesTheory.regstate_brss__6_accfupds ], computeLib.Extenders [ combinLib.add_combin_compset ] ] bcs; fun mk_regstate_record_thms def = let val tm = lhs(concl (SPEC_ALL def)) val rty = type_of tm val tyop = #1 (dest_type rty) val fields = TypeBase.fields_of rty fun mktm (fieldname,_) = Term[QUOTE(tyop^"_"^fieldname^" "), ANTIQUOTE tm] val tms = map mktm fields fun expand tm = let val tm = SIMP_CONV (srw_ss()) [] tm |> concl |> rand in (PURE_ONCE_REWRITE_CONV[def] THENC (computeLib.CBV_CONV bcs)) tm end fun expand2 tm = (RAND_CONV(REWR_CONV def) THENC (computeLib.CBV_CONV bcs)) tm val thms = map expand tms val thms2 = map expand2 tms in LIST_CONJ (thms@thms2) end val initial_regstate_thms = mk_regstate_record_thms cheriTheory.initial_regstate_def val init_state_thms = mk_record_thms state_monadTheory.init_state_def val cs = wordsLib.words_compset(); val eval = computeLib.CBV_CONV cs; val () = computeLib.extend_compset [ computeLib.Extenders [ optionLib.OPTION_rws, pairLib.add_pair_compset, combinLib.add_combin_compset, listLib.list_rws, listLib.add_rich_list_compset, pred_setLib.add_pred_set_compset, finite_mapLib.add_finite_map_compset, intReduce.add_int_compset, integer_wordLib.add_integer_word_compset, bitstringLib.add_bitstring_compset ], (* sail stuff *) (* computeLib.Defs (map #2 (ThmSetData.theory_data {settype = "compute", thy = "sail_values"})), *) computeLib.Defs [ listTheory.LUPDATE_compute, (* TODO: add better compset for LUPDATE! *) (* listTheory.EL_LUPDATE, *) pred_setTheory.UNION_EMPTY, lemTheory.w2ui_def, lem_listTheory.list_combine_def, lem_machine_wordTheory.size_itself_def, sail_instr_kindsTheory.read_is_exclusive_def |> SIMP_RULE std_ss [FUN_EQ_THM], sail_valuesTheory.update_list_dec_def, sail_valuesTheory.update_list_inc_def, sail_valuesTheory.pow2_def, sail_valuesTheory.pow0_def, sail_valuesTheory.make_the_value_def, sail_valuesTheory.nat_of_int_def, sail_valuesTheory.bool_of_bitU_def, sail_valuesTheory.bitU_of_bool_def, sail_valuesTheory.of_bits_failwith_def, sail_valuesTheory.size_itself_int_def, sail_valuesTheory.subrange_list_def, sail_valuesTheory.subrange_list_dec_def, sail_valuesTheory.subrange_list_inc_def, sail_valuesTheory.bools_of_int_def, sail_valuesTheory.bools_of_nat_def, sail_valuesTheory.take_list_def, sail_valuesTheory.drop_list_def, sail_valuesTheory.mem_bytes_of_bits_def, sail_valuesTheory.bytes_of_bits_def, sail_valuesTheory.bits_of_mem_bytes_def, sail_valuesTheory.bits_of_bytes_def, sail_valuesTheory.byte_chunks_def, sail_valuesTheory.access_bv_dec_def, sail_valuesTheory.access_list_def, sail_valuesTheory.access_list_inc_def, sail_valuesAuxiliaryTheory.bools_of_nat_aux_rw, sail_valuesAuxiliaryTheory.reverse_endianness_list_rw, sail_valuesAuxiliaryTheory.index_list_rw, sail_valuesAuxiliaryTheory.repeat_rw, sail_valuesAuxiliaryTheory.pad_list_rw, (* sail_valuesTheory.instance_Sail_values_Bitvector_Machine_word_mword_dict_def, *) instance_Sail_values_Bitvector_Machine_word_mword_dict_thms, sail_valuesTheory.just_list_def, sail_valuesTheory.maybe_failwith_def, sail_valuesTheory.int_of_mword_def, sail_valuesTheory.make_the_value_def, sail_valuesTheory.access_list_dec_def, sail_valuesTheory.access_list_inc_def, sail_valuesTheory.exts_bv_def, sail_valuesTheory.exts_bits_def, sail_valuesTheory.ext_list_def, sail_operatorsTheory.arith_op_bv_int_def, sail_operators_mwordsTheory.concat_vec_def, sail_operators_mwordsTheory.access_vec_dec_def, sail_operators_mwordsTheory.replicate_bits_def, sail_operators_mwordsTheory.and_vec_def, sail_operators_mwordsTheory.add_vec_def, sail_operators_mwordsTheory.add_vec_int_def, sail_operators_mwordsTheory.update_subrange_vec_dec_def, sail_operators_mwordsTheory.subrange_vec_dec_def, sail_operators_mwordsTheory.vec_of_bits_def, sail_operators_mwordsTheory.sub_vec_int_def, sail_operators_mwordsTheory.reverse_endianness_def ], computeLib.Tys [ ``:bitU``, ``:'a bits Bitvector_class``, ``:'a sequential_state``, ``:regstate``, ``:CapStruct``, ``:AccessLevel``, ``:MemAccessType``, ``:Exception``, ``:CauseReg``, ``:StatusReg``, ``:exception``, ``:read_kind``, ``:ast``, ``:'a ex``, ``:('a,'b,'c) register_ref``, ``:('a,'b) result`` ], (* these should come out of regstate but seem not to... *) computeLib.Defs [ cheri_typesTheory.regstate_brss__0_accfupds, cheri_typesTheory.regstate_brss__1_accfupds, cheri_typesTheory.regstate_brss__2_accfupds, cheri_typesTheory.regstate_brss__3_accfupds, cheri_typesTheory.regstate_brss__4_accfupds, cheri_typesTheory.regstate_brss__5_accfupds, cheri_typesTheory.regstate_brss__6_accfupds ], (* state monad *) computeLib.Defs [ stateTheory.iteriS_def, stateTheory.or_boolS_def, stateAuxiliaryTheory.iterS_aux_rw, stateAuxiliaryTheory.foreachS_rw, state_monadTheory.assert_expS_def, state_monadTheory.write_mem_eaS_def, state_monadTheory.write_mem_valS_def, state_monadTheory.write_tagS_def, state_monadTheory.write_mem_bytesS_def, state_monadTheory.updateS_def, state_monadTheory.maybe_failS_def, state_monadTheory.read_regS_def, state_monadTheory.write_regS_def, (* delete the following two in interactive proof *) state_monadTheory.read_memS_def, state_monadTheory.read_mem_bytesS_def, (* seqS_returnS, bindS_returnS_1, bindS_readS, *) liftRS_def, early_returnS_def, catch_early_returnS_def, throwS_def, bindS_def, returnS_def, seqS_def, readS_def, try_catchS_def ], (* computeLib.Convs [ (``bindS``, 2, RAND_CONV eval THENC (RATOR_CONV(RAND_CONV eval)) THENC HO_REWR_CONV bindS_returnS_s), (``seqS``, 2, RAND_CONV eval THENC (RATOR_CONV(RAND_CONV eval)) THENC HO_REWR_CONV seqS_returnS_s) ], *) (* cheri/mips model *) computeLib.Defs [ initial_regstate_thms, init_state_thms, decode_def, MEMw_wrapper_def, MEMr_wrapper_def, sign_extend1_def, (* delete this one in interactive proof *) mips_extrasTheory.sign_extend0_def, cap_addr_mask_thm, init_registers_def, init_cp0_state_def, init_cp2_state_def, cp2_next_pc_def, writeCapReg_def, LENGTH_TLBEntries, EL_TLBEntries, HD_TLBEntries, LENGTH_CapRegs, EL_CapRegs, HD_CapRegs, default_cap_thms, nextPC_ref_thms, delayedPCC_ref_thms, delayedPC_ref_thms, nextPCC_ref_thms, PCC_ref_thms, PC_ref_thms, GPR_ref_thms, branchPending_ref_thms, inBranchDelay_ref_thms, instCount_ref_thms, CP0Count_ref_thms, CP0Compare_ref_thms, CP0Status_ref_thms, CP0BadVAddr_ref_thms, CP0EPC_ref_thms, CP0Cause_ref_thms, LIST_CONJ TLBEntry_ref_thms, LIST_CONJ C_ref_thms, UART_WRITTEN_ref_thms, UART_WDATA_ref_thms, inCCallDelay_ref_thms, TLBRandom_ref_thms, TLBWired_ref_thms, TLBContext_ref_thms, TLBXContext_ref_thms, TLBEntryHi_ref_thms, TLBIndexMax_def, capStructToCapReg_def, capRegToCapStruct_thms, capStructToMemBits256_def, get_TLBEntry_valid_def, get_StatusReg_def, get_StatusReg_EXL_def, get_StatusReg_ERL_def, get_StatusReg_KSU_def, get_StatusReg_IE_def, get_CauseReg_IP_def, get_CauseReg_def, grantsAccess_def, int_of_AccessLevel_def, getCapBase_def, getCapTop_def, getCapPerms_def, cast_unit_vec0_def, set_StatusReg_BEV_def, set_StatusReg_EXL_def, fetch_and_execute_def, execute_def, execute_ADDIU_def, (* delete for interactive proof? execute_ADD_def |> SIMP_RULE std_ss [sign_extend1_def], *) execute_ADD_def, TranslatePC_def, TLBTranslate_def, TLBTranslate2_def, tlbSearch_def, tlbEntryMatch_def, SignalExceptionTLB_def, SignalException_def, SignalExceptionMIPS_def, ExceptionCode_def, TLBTranslateC_def, (* delete this one in interactive proof *) setCapOffset_def, set_CauseReg_BD_def, set_CauseReg_ExcCode_def, set_ContextReg_BadVPN2_def, set_XContextReg_XBadVPN2_def, set_XContextReg_XR_def, get_TLBEntryHiReg_def, set_TLBEntryHiReg_R_def, set_TLBEntryHiReg_VPN2_def, getAccessLevel_def, incrementCP0Count_def, mips_extrasTheory.skip_def, mips_extrasTheory.MEMea_def, mips_extrasTheory.MEMval_def, mips_extrasTheory.get_slice_int0_def, mips_extrasTheory.get_slice_int_bl_def, mips_extrasTheory.write_tag_bool_def, mips_extrasTheory.MEMr_def, zeros0_def, ones_def, bool_to_bits_def, bits_to_bool_def, bit_to_bool_def, to_bits_def, neq_bool_def, NotWordVal_def, MAX_PA_def, MAX_VA_def, MAX0_def, rGPR_def, wGPR_def ], (* (* delete these for interactive... or always...*) computeLib.Defs (map #2 (ThmSetData.theory_data {settype = "compute", thy = "cheri" })), computeLib.Defs (map #2 (ThmSetData.theory_data {settype = "compute", thy = "cheri_types" })), computeLib.Defs (map #2 (ThmSetData.theory_data {settype = "compute", thy = "mips_extras" })), *) (* test_raw_add *) computeLib.Defs [ test_raw_add_insts_def, install_code_def, install_and_run_def, clocked_whileS_def ] ] cs; val empty_state = ``init_state initial_regstate``; val init_registers_result = ``init_registers vinitPC s`` |> computeLib.CBV_CONV cs (* (computeLib.CBV_CONV cs (*THENC SIMP_CONV (srw_ss()) [seqS_returnS_s, bindS_returnS_s]*)) ``MEMw_wrapper (0x9000000040000000w + 4w * i2w 1) 4 (0x24140002w:word32) s`` computeLib.CBV_CONV cs `` OPTION_MAP v2w (just_list [SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME F; SOME T; SOME T; SOME T; SOME T; SOME T; SOME T; SOME T; SOME F ])`` *) val install_code_result = computeLib.CBV_CONV cs ``install_code 0x40000000w test_raw_add_insts s`` (* install_code_result |> concl |> rhs |> rator |> rand |> pairSyntax.dest_pair |> #2 |> dest_comb *) (* maybe better to say something about looking up the code, and ignore the other effects..? val code_installed_def = Define` code_installed initPC code s s' = let addrs = index_list (w2i initPC) (w2i initPC + 4 * (&LENGTH code)) 1 in s' = s with <| memstate := s.memstate |++ list_combine addrs (FLAT (MAP (REVERSE o THE o byte_chunks o MAP bitU_of_bool o w2v o reverse_endianness) code)) ; tagstate := s.tagstate |++ MAP (λaddr. (w2i(cap_addr_mask && i2w addr), B0)) addrs ; write_ea := SOME (Write_plain, w2i initPC + 4 * (&LENGTH code) - 4, 4i) |>`; *) val code_installed_def = Define` code_installed initPC code s = ∀k i. (k = w2ui initPC + 4 * &i) ∧ i < LENGTH code ⇒ case byte_chunks (MAP bitU_of_bool (w2v (reverse_endianness (EL i code)))) of | SOME chunks => (FLOOKUP s.memstate (k+0) = SOME (EL 0 (REVERSE chunks))) ∧ (FLOOKUP s.memstate (k+1) = SOME (EL 1 (REVERSE chunks))) ∧ (FLOOKUP s.memstate (k+2) = SOME (EL 2 (REVERSE chunks))) ∧ (FLOOKUP s.memstate (k+3) = SOME (EL 3 (REVERSE chunks))) | NONE => F`; val registers_inited_def = Define` registers_inited initPC s = (s.regstate.nextPC = initPC) ∧ (s.regstate.CP0Status = Mk_StatusReg 0x400000w) ∧ (s.regstate.nextPCC = capStructToCapReg default_cap) (* ∧ a bunch of stuff about s.CX *)`; (* val cycle_result = computeLib.CBV_CONV cs ``fetch_and_execute () s`` |> SIMP_RULE(srw_ss())[] *) (* val result1 = ``install_and_run test_raw_add_insts 1 ^empty_state`` |> time (computeLib.CBV_CONV cs) *) (* doing this for 2 clock ticks blows up because I haven't got the right definitions in the compset... trying with everything in cheri and cheri_types and mips_extra doesn't help... update: works after adding LUPDATE_compute *) (* val result2 = ``install_and_run test_raw_add_insts 2 ^empty_state`` |> time (computeLib.CBV_CONV cs) *) (* 12s for 20 steps *) (* val result3 = ``install_and_run test_raw_add_insts 20 ^empty_state`` |> time (computeLib.CBV_CONV cs) *) (* 15s to completion *) val result4 = ``install_and_run test_raw_add_insts 40 ^empty_state`` |> time (computeLib.CBV_CONV cs) (* val tm1 = result |> concl |> rhs |> funpow 4 rand |> rator |> rator |> rator |> rand |> rator |> rator |> rator |> rand |> rator |> rator |> rand |> rator |> rand |> CHANGED_CONV(computeLib.CBV_CONV cs) type_of``B0`` val tm2 = ``initial_regstate.branchPending`` computeLib.CBV_CONV cs tm1 computeLib.CBV_CONV cs tm2 computeLib.CBV_CONV cs ``initial_regstate.branchPending`` dest_term tm1 dest_term tm2 set_trace"simplifier"0; SIMP_CONV (srw_ss())[initial_regstate_thms] tm1 SIMP_CONV (srw_ss())[initial_regstate_thms] tm2 |> concl |> rhs |> aconv tm1 rator tm1 rator tm2 m``regstate_branchPending r = regstate_brss__2_branchPending (regstate_brss__sf2 r)`` *) (* val updates = install_code_result |> concl |> rhs |> rator |> rand |> rand |> rator |> rand |> rand |> finite_mapSyntax.strip_fupdate |> #2 *) val test_raw_add_thm = Q.store_thm("test_raw_add_thm", `PrePost (λs. s = init_state initial_regstate) (install_and_run test_raw_add_insts 40) (λ_ s. test_raw_add_post s)`, rw[PrePost_def] \\ pop_assum(mp_tac o REWRITE_RULE[result4]) \\ simp_tac (std_ss ++ pred_setLib.PRED_SET_ss) [] \\ strip_tac \\ BasicProvers.VAR_EQ_TAC \\ ONCE_REWRITE_TAC[test_raw_add_post_def] \\ CONV_TAC(LAND_CONV(computeLib.CBV_CONV cs)) \\ REFL_TAC); (* interactive approach to slighly more general theorem val TLBEntries_zero_def = Define` TLBEntries_zero rs ⇔ (rs.TLBEntry00 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry01 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry02 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry03 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry04 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry05 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry06 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry07 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry08 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry09 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry10 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry11 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry12 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry13 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry14 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry15 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry16 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry17 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry18 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry19 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry20 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry21 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry22 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry23 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry24 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry25 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry26 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry27 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry28 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry29 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry30 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry31 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry32 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry33 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry34 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry35 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry36 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry37 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry38 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry39 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry40 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry41 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry42 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry43 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry44 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry45 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry46 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry47 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry48 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry49 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry50 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry51 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry52 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry53 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry54 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry55 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry56 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry57 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry58 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry59 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry60 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry61 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry62 = Mk_TLBEntry 0w) ∧ (rs.TLBEntry63 = Mk_TLBEntry 0w)`; val init_registers_result_initial = init_registers_result |> Q.GEN`s` |> Q.SPEC`<| regstate := initial_regstate |>` |> concl |> rhs |> rator |> rand |> rand |> rator |> rand |> rand |> funpow 4 RAND_CONV (SIMP_CONV (srw_ss()) []) |> concl |> rhs val test_raw_add_thm = Q.store_thm("test_raw_add_thm", `PrePost (λs. (* ((s.regstate.GPR = REPLICATE 64 0w) ∧ (s.regstate.branchPending = 0w) ∧ (s.regstate.UART_WRITTEN = 0w) ∧ (s.regstate.TLBRandom = 0w) ∧ (s.regstate.TLBWired = 0w) ∧ (TLBEntries_zero s.regstate) ∧ (s.regstate.nextPCC = 0w) ∧ (s.regstate.CP0Count = 0w) ∧ (s.regstate.CP0Status = Mk_StatusReg 0w) ∧ (s.regstate.CP0Compare = 0w)) *) s.regstate = initial_regstate ) (install_and_run test_raw_add_insts 100000) (λ_ s. test_raw_add_post s)`, rw[install_and_run_def] \\ match_mp_tac PrePost_seqS \\ simp[] \\ qmatch_goalsub_abbrev_tac`install_code initPC` \\ qmatch_goalsub_abbrev_tac`init_registers vinitPC` \\ qexists_tac`λs. code_installed initPC test_raw_add_insts s ∧ (* registers_inited vinitPC s ∧ *) (s.regstate = ^init_registers_result_initial (*^(init_registers_result |> concl |> rhs |> rator |> rand |> rand |> rator |> rand |> rand )*)) (* <| nextPC := vinitPC ; CP0Status := Mk_StatusReg 0x400000w; nextPCC := capStructToCapReg default_cap |> ) *) (* ((s.regstate.branchPending = 0w) ∧ (s.regstate.GPR = REPLICATE 64 0w) ∧ (s.regstate.UART_WRITTEN = 0w) ∧ (s.regstate.TLBRandom = 0w) ∧ (s.regstate.TLBWired = 0w) ∧ (TLBEntries_zero s.regstate) ∧ (s.regstate.CP0Count = 0w) ∧ (s.regstate.CP0Compare = 0w)) *)` \\ conj_tac >- ( match_mp_tac PrePost_seqS \\ simp[] \\ qexists_tac`λs. code_installed initPC test_raw_add_insts s ∧ (s.regstate = initial_regstate) (* ((s.regstate.branchPending = 0w) ∧ (s.regstate.GPR = REPLICATE 64 0w) ∧ (s.regstate.UART_WRITTEN = 0w) ∧ (s.regstate.TLBRandom = 0w) ∧ (s.regstate.TLBWired = 0w) ∧ (TLBEntries_zero s.regstate) ∧ (s.regstate.nextPCC = 0w) ∧ (s.regstate.CP0Count = 0w) ∧ (s.regstate.CP0Status = Mk_StatusReg 0w) ∧ (s.regstate.CP0Compare = 0w))*)` \\ conj_tac >- ( rw[PrePost_def,Abbr`initPC`] \\ fs[install_code_result] \\ BasicProvers.VAR_EQ_TAC \\ rw[code_installed_def] \\ pop_assum mp_tac \\ CONV_TAC(LAND_CONV(computeLib.CBV_CONV cs)) \\ CONV_TAC(LAND_CONV(SIMP_CONV(srw_ss())[wordsTheory.NUMERAL_LESS_THM])) \\ strip_tac \\ BasicProvers.VAR_EQ_TAC \\ CONV_TAC(computeLib.CBV_CONV cs)) \\ rw[PrePost_def,Abbr`initPC`] \\ pop_assum(assume_tac o REWRITE_RULE [init_registers_result,pred_setTheory.IN_INSERT,pred_setTheory.NOT_IN_EMPTY]) \\ BasicProvers.VAR_EQ_TAC \\ qmatch_goalsub_abbrev_tac`v2w l1` (* \\ simp[registers_inited_def] *) \\ fs[code_installed_def] (* \\ fs[code_installed_def,Abbr`l1`(*,TLBEntries_zero_def*)] \\ CONV_TAC (computeLib.CBV_CONV cs) *) ) \\ match_mp_tac (GEN_ALL PrePost_clocked_whileS_unit_T) \\ simp[seqS_returnS] \\ qmatch_goalsub_abbrev_tac`_.regstate = RS` \\ qmatch_goalsub_abbrev_tac`PrePostE CI` \\ qexists_tac`λs. code_installed initPC test_raw_add_insts s ∧ (s.regstate = RS with <| GPR := LUPDATE 1w (32-1-19) RS.GPR ; instCount := 1 ; CP0Count := 1w ; TLBRandom := TLBIndexMax ; PC := vinitPC ; nextPC := vinitPC + 4w; |>) ` \\ fs[] \\ conj_tac >- ( rw[PrePostE_def] \\ rw[fetch_and_execute_def] \\ simp[PrePost_def] \\ gen_tac \\ strip_tac \\ gen_tac \\ `s.regstate = RS` by fs[Abbr`CI`] \\ qunabbrev_tac`RS` \\ qunabbrev_tac`vinitPC` \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV(computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC[])) \\ ASM_REWRITE_TAC[TLBTranslateC_def] \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC [])) \\ ASM_REWRITE_TAC[read_memS_def, read_mem_bytesS_def] (* \\ `s.regstate.nextPC = vinitPC` by fs[Abbr`CI`,registers_inited_def] \\ `(s.regstate.branchPending = 0w) ∧ (s.regstate.GPR = REPLICATE 64 0w) ∧ (s.regstate.UART_WRITTEN = 0w) ∧ (s.regstate.TLBRandom = 0w) ∧ (s.regstate.TLBWired = 0w) ∧ (TLBEntries_zero s.regstate) ∧ (s.regstate.nextPCC = capStructToCapReg default_cap) ∧ (s.regstate.CP0Count = 0w) ∧ (s.regstate.CP0Status = Mk_StatusReg 0x400000w) ∧ (s.regstate.CP0Compare = 0w)` by fs[Abbr`CI`, registers_inited_def] \\ ntac 11 (pop_assum mp_tac) \\ PURE_REWRITE_TAC[AND_IMP_INTRO] \\ PURE_REWRITE_TAC[TLBEntries_zero_def] \\ CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ PURE_REWRITE_TAC[GSYM AND_IMP_INTRO] \\ qunabbrev_tac`vinitPC` \\ ntac (10+64) strip_tac \\ ASM_REWRITE_TAC[] \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC [])) \\ ASM_REWRITE_TAC[TLBTranslateC_def] \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC [])) \\ ASM_REWRITE_TAC[read_memS_def, read_mem_bytesS_def] *) \\ ASM_SIMP_TAC (bool_ss ++ boolSimps.LET_ss) [bindS_returnS_1, bindS_readS] \\ qmatch_goalsub_abbrev_tac`bindS (bindS m1 m2) m3 ss` \\ qunabbrev_tac`m1` \\ `ss.memstate = s.memstate` by simp[Abbr`ss`] \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ qunabbrev_tac`m2` \\ CONV_TAC(DEPTH_CONV BETA_CONV) \\ qmatch_goalsub_abbrev_tac`just_list ls` \\ qmatch_goalsub_abbrev_tac`f ls` \\ qunabbrev_tac`ls` \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ `code_installed initPC test_raw_add_insts s` by fs[Abbr`CI`] \\ pop_assum(mp_tac o SIMP_RULE(srw_ss())[code_installed_def]) \\ disch_then(qspec_then`0`mp_tac) \\ impl_tac >- EVAL_TAC \\ disch_then(mp_tac o CONV_RULE(RATOR_CONV(computeLib.CBV_CONV cs))) \\ qunabbrev_tac`initPC` \\ disch_then(mp_tac o CONV_RULE(computeLib.CBV_CONV cs)) \\ strip_tac \\ map_every qunabbrev_tac[`f`,`m3`] \\ CHANGED_TAC(ASM_REWRITE_TAC[sign_extend1_def]) \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ qunabbrev_tac`ss` \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ SIMP_TAC (srw_ss()) [] \\ strip_tac \\ BasicProvers.VAR_EQ_TAC \\ fs[code_installed_def,Abbr`CI`] \\ ONCE_REWRITE_TAC[cheri_typesTheory.regstate_component_equality] \\ CONV_TAC(computeLib.CBV_CONV cs) \\ rpt AP_THM_TAC \\ AP_TERM_TAC \\ CONV_TAC(computeLib.CBV_CONV cs) ) \\ qunabbrev_tac`RS` \\ qunabbrev_tac`CI` \\ CONV_TAC (PATH_CONV"llrar"(computeLib.CBV_CONV cs)) \\ qmatch_goalsub_abbrev_tac`v2w ll` \\ match_mp_tac (GEN_ALL PrePost_clocked_whileS_unit_T) \\ simp[seqS_returnS] \\ qmatch_goalsub_abbrev_tac`_.regstate = RS` \\ qmatch_goalsub_abbrev_tac`PrePostE CI` \\ qexists_tac`λs. code_installed initPC test_raw_add_insts s ∧ (s.regstate = RS with <| GPR := LUPDATE 2w (32-1-20) RS.GPR ; instCount := 2 ; CP0Count := 2w ; TLBRandom := 62w ; PC := vinitPC + 4w ; nextPC := vinitPC + 8w; |>) ` \\ fs[] \\ conj_tac >- ( rw[PrePostE_def] \\ rw[fetch_and_execute_def] \\ simp[PrePost_def] \\ gen_tac \\ strip_tac \\ gen_tac \\ `s.regstate = RS` by fs[Abbr`CI`] \\ qunabbrev_tac`RS` \\ qunabbrev_tac`vinitPC` \\ qunabbrev_tac`ll` \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV(computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC[])) \\ ASM_REWRITE_TAC[TLBTranslateC_def] \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC [])) \\ ASM_REWRITE_TAC[read_memS_def, read_mem_bytesS_def] \\ ASM_SIMP_TAC (bool_ss ++ boolSimps.LET_ss) [bindS_returnS_1, bindS_readS] \\ qmatch_goalsub_abbrev_tac`bindS (bindS m1 m2) m3 ss` \\ qunabbrev_tac`m1` \\ `ss.memstate = s.memstate` by simp[Abbr`ss`] \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ qunabbrev_tac`m2` \\ CONV_TAC(DEPTH_CONV BETA_CONV) \\ qmatch_goalsub_abbrev_tac`just_list ls` \\ qmatch_goalsub_abbrev_tac`f ls` \\ qunabbrev_tac`ls` \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ `code_installed initPC test_raw_add_insts s` by fs[Abbr`CI`] \\ pop_assum(mp_tac o SIMP_RULE(srw_ss())[code_installed_def]) \\ disch_then(qspec_then`1`mp_tac) \\ impl_tac >- EVAL_TAC \\ disch_then(mp_tac o CONV_RULE(RATOR_CONV(computeLib.CBV_CONV cs))) \\ qunabbrev_tac`initPC` \\ disch_then(mp_tac o CONV_RULE(computeLib.CBV_CONV cs)) \\ strip_tac \\ map_every qunabbrev_tac[`f`,`m3`] \\ CHANGED_TAC(ASM_REWRITE_TAC[sign_extend1_def]) \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ qunabbrev_tac`ss` \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ SIMP_TAC (srw_ss()) [] \\ strip_tac \\ BasicProvers.VAR_EQ_TAC \\ fs[code_installed_def,Abbr`CI`] \\ ONCE_REWRITE_TAC[cheri_typesTheory.regstate_component_equality] \\ qmatch_goalsub_abbrev_tac`v2w ll` \\ CONV_TAC(computeLib.CBV_CONV cs) \\ rpt AP_THM_TAC \\ AP_TERM_TAC \\ CONV_TAC(computeLib.CBV_CONV cs)) \\ qunabbrev_tac`RS` \\ qunabbrev_tac`CI` \\ CONV_TAC (PATH_CONV"llrar"(computeLib.CBV_CONV cs)) \\ match_mp_tac (GEN_ALL PrePost_clocked_whileS_unit_T) \\ simp[seqS_returnS] \\ qmatch_goalsub_abbrev_tac`_.regstate = RS` \\ qexists_tac`λs. code_installed initPC test_raw_add_insts s ∧ (s.regstate = RS with <| GPR := LUPDATE 3w (32-1-4) RS.GPR ; instCount := 3 ; CP0Count := 3w ; TLBRandom := 62w ; PC := vinitPC + 8w ; nextPC := vinitPC + 12w; |>) ` \\ fs[] \\ conj_tac >- ( rw[PrePostE_def] \\ rw[fetch_and_execute_def] \\ simp[PrePost_def] \\ gen_tac \\ strip_tac \\ gen_tac \\ qunabbrev_tac`RS` \\ qunabbrev_tac`vinitPC` \\ qunabbrev_tac`ll` \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV(computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC[])) \\ ASM_REWRITE_TAC[TLBTranslateC_def] \\ rpt(CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC [])) \\ ASM_REWRITE_TAC[read_memS_def, read_mem_bytesS_def] \\ ASM_SIMP_TAC (bool_ss ++ boolSimps.LET_ss) [bindS_returnS_1, bindS_readS] \\ qmatch_goalsub_abbrev_tac`bindS (bindS m1 m2) m3 ss` \\ qunabbrev_tac`m1` \\ `ss.memstate = s.memstate` by simp[Abbr`ss`] \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ qunabbrev_tac`m2` \\ CONV_TAC(DEPTH_CONV BETA_CONV) \\ qmatch_goalsub_abbrev_tac`just_list ls` \\ qmatch_goalsub_abbrev_tac`f ls` \\ qunabbrev_tac`ls` \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ qpat_assum`code_installed _ _ _`(mp_tac o SIMP_RULE(srw_ss())[code_installed_def]) \\ disch_then(qspec_then`2`mp_tac) \\ impl_tac >- EVAL_TAC \\ disch_then(mp_tac o CONV_RULE(RATOR_CONV(computeLib.CBV_CONV cs))) \\ qunabbrev_tac`initPC` \\ disch_then(mp_tac o CONV_RULE(computeLib.CBV_CONV cs)) \\ strip_tac \\ map_every qunabbrev_tac[`f`,`m3`] \\ CHANGED_TAC(ASM_REWRITE_TAC[sign_extend1_def]) \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ qunabbrev_tac`ss` \\ CHANGED_TAC(ASM_REWRITE_TAC[execute_ADD_def, sign_extend1_def]) \\ qmatch_asmsub_abbrev_tac`v2w ll` \\ CHANGED_TAC(CONV_TAC(LAND_CONV (computeLib.CBV_CONV cs)) \\ ASM_REWRITE_TAC []) \\ simp[] \\ strip_tac \\ BasicProvers.VAR_EQ_TAC \\ fs[code_installed_def] \\ ONCE_REWRITE_TAC[cheri_typesTheory.regstate_component_equality] \\ rpt(conj_tac >- CONV_TAC(computeLib.CBV_CONV cs)) \\ rpt AP_THM_TAC \\ AP_TERM_TAC \\ CONV_TAC(computeLib.CBV_CONV cs)) (* top_goal() |> #2 |> rand |> rator |> rand |> rand |> rator |> rator |> rand |> rand |> listSyntax.dest_list |> #1 |> length top_goal() |> #2 |> dest_imp |> #1 |> funpow 5 rand |> rand |> rand |> rator |> rand |> rator |> rand |> rand |> rator |> rator |> rand |> rator |> rator |> rand |> rand computeLib.CBV_CONV cs ``LENGTH (LUPDATE 1n 2 [3;4;9;8;7;76;3;8;9;9;9;9;0;0;0])`` |> rator |> rand |> rand |> rator |> rand |> rator execute_ADD_def |> SIMP_RULE std_ss [sign_extend1_def] |> SPEC_ALL |> concl |> rhs ``SignalException XTLBRefillL s`` |> SIMP_CONV(srw_ss())[SignalException_def] |> concl |> rhs |> rator |> rand |> dest_abs |> #2 |> rator `` (capRegToCapStruct (v2w [T; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; F; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T; T])).CapStruct_access_system_regs `` (* set_trace"simplifier"0 SIMP_CONV (srw_ss()) [] `` regstate_brss__6_TLBRandom (regstate_brss__6_nextPC_fupd (K 0x9000000040000004w) (regstate_brss__6_PC_fupd (K 0x9000000040000000w) (regstate_brss__sf6 s.regstate)))`` top_goal() |> #2 |> dest_imp |> #1 |> dest_exists |> #2 |> strip_conj |> last |> dest_exists |> #2 |> strip_conj |> last |> rand |> rator |> funpow 13 rand top_goal() |> #2 |> dest_imp |> #1 |> funpow 5 rand |> rator |> rator |> rator |> rand |> rand |> rator |> rand |> rator |> rand |> rand |> rand |> rator top_goal() |> #1 |> el 9 |> lhs |> computeLib.CBV_CONV cs |> concl |> rhs |> rator |> rator |> funpow 13 rand top_goal() |> #1 |> el 2 |> rand |> rhs |> rator \\ pop_assum(SUBST_ALL_TAC) *) *) \\ cheat); *) (* computeLib.CBV_CONV cs ``decode (EL 1 test_raw_add_insts)`` val th1 = EVAL ``THE (decode (EL 1 test_raw_add_insts))`` val s1 = EVAL ``init_cp0_state () (init_state (regs:regstate))`` val th2 = ``execute ^(rhs(concl th1)) ^s1`` |> SIMP_CONV(srw_ss())[execute_def] |> SIMP_RULE(srw_ss())[execute_ADDIU_def] f"bindS" type_of ``execute ast `` f"init_state" execute_ADDIU_def type_of``OPTION_BIND`` tyabbrev_info"M" val (_, execute_rng) = dom_rng (type_of``execute``) val (mdom, mrng) = dom_rng execute_rng val state_ty = ``:regstate sequential_state`` dest_thy_type state_ty TypeBase.fields_of state_ty disable_tyabbrev_printing"rel" dest_type``:unit M`` f"vec_of_bits" f"of_bits_fail" f"maybe_failw" f"nat_of_int" f"just_list" f"sfunpow" show_assums := true *) val _ = export_theory ();