From d88551c34e2f9cca699a8c1c3749ee74dbd5e760 Mon Sep 17 00:00:00 2001 From: ordinarymath Date: Wed, 30 Apr 2025 14:07:18 +0000 Subject: [PATCH 1/4] Cleanup stackprops --- .../backend/semantics/stackPropsScript.sml | 441 ++++++++++-------- 1 file changed, 234 insertions(+), 207 deletions(-) diff --git a/compiler/backend/semantics/stackPropsScript.sml b/compiler/backend/semantics/stackPropsScript.sml index d67703b710..235c051193 100644 --- a/compiler/backend/semantics/stackPropsScript.sml +++ b/compiler/backend/semantics/stackPropsScript.sml @@ -73,6 +73,50 @@ Proof EVAL_TAC QED +Triviality set_fp_var_with_const[simp]: + set_fp_var x y (z with clock := k) = set_fp_var x y z with clock := k +Proof + EVAL_TAC +QED + +Triviality set_fp_var_const[simp]: + (set_fp_var x y z).ffi = z.ffi ∧ + (set_fp_var x y z).clock = z.clock ∧ + (set_fp_var x y z).use_alloc = z.use_alloc ∧ + (set_fp_var x y z).use_store = z.use_store ∧ + (set_fp_var x y z).use_stack = z.use_stack ∧ + (set_fp_var x y z).code = z.code ∧ + (set_fp_var x y z).be = z.be ∧ + (set_fp_var x y z).gc_fun = z.gc_fun ∧ + (set_fp_var x y z).mdomain = z.mdomain ∧ + (set_fp_var x y z).sh_mdomain = z.sh_mdomain ∧ + (set_fp_var x y z).bitmaps = z.bitmaps ∧ + (set_fp_var x y z).compile = z.compile ∧ + (set_fp_var x y z).compile_oracle = z.compile_oracle ∧ + (set_fp_var x y z).stack = z.stack ∧ + (set_fp_var x y z).stack_space = z.stack_space +Proof + EVAL_TAC +QED + +Triviality get_fp_var_with_const[simp]: + get_fp_var x (y with clock := k) = get_fp_var x y +Proof + EVAL_TAC +QED + +Triviality get_var_with_const[simp]: + get_var x (y with clock := k) = get_var x y +Proof + EVAL_TAC +QED + +Triviality get_vars_with_const[simp]: + get_vars xs (y with clock := k) = get_vars xs y +Proof + Induct_on `xs` >> EVAL_TAC >> simp[] +QED + Theorem get_var_imm_with_const[simp]: get_var_imm x (y with clock := k) = get_var_imm x y Proof @@ -175,31 +219,52 @@ Proof QED Theorem sh_mem_load_with_const[simp]: - FST (sh_mem_load r x (y with clock := k)) = FST (sh_mem_load r x y) + (sh_mem_load r x (y with clock := k)) = (I ## (\s. s with clock := k)) (sh_mem_load r x y) Proof simp[sh_mem_load_def,ffiTheory.call_FFI_def]>>every_case_tac>> fs[] QED Theorem sh_mem_store_with_const[simp]: - FST (sh_mem_store x y (z with clock := k)) = FST (sh_mem_store x y z) + (sh_mem_store x y (z with clock := k)) = (I ## (\s. s with clock := k)) (sh_mem_store x y z) Proof gs[sh_mem_store_def,ffiTheory.call_FFI_def]>>every_case_tac>> - gs[get_var_def] + gs[] +QED + +Theorem sh_mem_load32_with_const[simp]: + (sh_mem_load32 r x (y with clock := k)) = (I ## (\s. s with clock := k)) (sh_mem_load32 r x y) +Proof + simp[sh_mem_load32_def,ffiTheory.call_FFI_def]>>every_case_tac>> + fs[] +QED + +Theorem sh_mem_store32_with_const[simp]: + (sh_mem_store32 x y (z with clock := k)) = (I ## (\s. s with clock := k)) (sh_mem_store32 x y z) +Proof + gs[sh_mem_store32_def,ffiTheory.call_FFI_def]>>every_case_tac>> + gs[] QED Theorem sh_mem_load_byte_with_const[simp]: - FST (sh_mem_load_byte r x (y with clock := k)) = FST (sh_mem_load_byte r x y) + (sh_mem_load_byte r x (y with clock := k)) = (I ## (\s. s with clock := k)) (sh_mem_load_byte r x y) Proof simp[sh_mem_load_byte_def,ffiTheory.call_FFI_def]>>every_case_tac>> fs[] QED Theorem sh_mem_store_byte_with_const[simp]: - FST (sh_mem_store_byte x y (z with clock := k)) = FST (sh_mem_store_byte x y z) + (sh_mem_store_byte x y (z with clock := k)) = (I ## (\s. s with clock := k)) (sh_mem_store_byte x y z) Proof gs[sh_mem_store_byte_def,ffiTheory.call_FFI_def]>>every_case_tac>> - gs[get_var_def] + gs[] +QED + +Triviality sh_mem_op_with_const[simp]: + (sh_mem_op op x y (z with clock := k)) = (I ## (\s. s with clock := k)) (sh_mem_op op x y z) +Proof + gs[oneline sh_mem_op_def] >> + TOP_CASE_TAC >> gs[] QED Theorem word_exp_with_const[simp]: @@ -222,6 +287,7 @@ Proof srw_tac[][assign_def] >> every_case_tac >> full_simp_tac(srw_ss())[] QED + Theorem inst_const: inst i s = SOME t ⇒ t.ffi = s.ffi ∧ @@ -238,22 +304,16 @@ Theorem inst_const: t.compile = s.compile ∧ t.compile_oracle = s.compile_oracle Proof - Cases_on`i`>>srw_tac[][inst_def,assign_def] >> - every_case_tac >> full_simp_tac(srw_ss())[set_fp_var_def,set_var_def,word_exp_def,LET_THM] >> srw_tac[][] >> - full_simp_tac(srw_ss())[mem_store_def] >> srw_tac[][] >> - fs[get_vars_def]>>every_case_tac>>fs[state_component_equality] + Cases_on`i`>> strip_tac >> + gvs[inst_def,assign_def,word_exp_def, + mem_store_def,AllCaseEqs(),UNCURRY_EQ] QED Theorem inst_with_const[simp]: inst i (s with clock := k) = OPTION_MAP (λs. s with clock := k) (inst i s) Proof - srw_tac[][inst_def] >> - CASE_TAC >> full_simp_tac(srw_ss())[] >> - every_case_tac >> full_simp_tac(srw_ss())[get_var_def] >> rveq >> full_simp_tac(srw_ss())[]>> - fs[get_vars_def,get_var_def,get_fp_var_def,set_fp_var_def]>> - every_case_tac>>fs[]>> - rw[]>>fs[]>>rw[]>>fs[] >> - gvs [mem_load_def] + srw_tac[][inst_def] + >> rpt (TOP_CASE_TAC >> gvs[mem_load_def]) QED Theorem dec_clock_const[simp]: @@ -311,16 +371,10 @@ Proof recInduct evaluate_ind >> rpt conj_tac >> simp[evaluate_def] >> - rpt gen_tac >> - rpt ( - (strip_tac >> CHANGED_TAC(imp_res_tac alloc_const) >> full_simp_tac(srw_ss())[]) ORELSE - (strip_tac >> CHANGED_TAC(imp_res_tac inst_const) >> full_simp_tac(srw_ss())[]) ORELSE - (strip_tac >> CHANGED_TAC(imp_res_tac sh_mem_op_const) >> full_simp_tac(srw_ss())[]) ORELSE - (strip_tac >> var_eq_tac >> rveq >> full_simp_tac(srw_ss())[]) ORELSE - (CASE_TAC >> full_simp_tac(srw_ss())[]) ORELSE - (pairarg_tac >> simp[]))>> - (every_case_tac>>fs[]>>rw[]) >> - imp_res_tac store_const_sem_const >> fs [] + rpt (gen_tac ORELSE disch_tac) >> + gvs[AllCaseEqs(),UNCURRY_EQ] >> + map_every imp_res_tac [alloc_const,inst_const,store_const_sem_const,sh_mem_op_const] >> + fs[] QED Theorem evaluate_code_bitmaps: @@ -332,45 +386,16 @@ Theorem evaluate_code_bitmaps: s1.bitmaps = s.bitmaps ++ FLAT (MAP (SND o SND) (GENLIST s.compile_oracle n)) Proof recInduct evaluate_ind >> - rw[evaluate_def] >> - TRY(qexists_tac`0` \\ fsrw_tac[ETA_ss][shift_seq_def] \\ NO_TAC) \\ - TRY( - fs[case_eq_thms,empty_env_def,dec_clock_def]>>rw[]>> - TRY (qpat_x_assum ‘(r',s1) = _’ $ assume_tac o GSYM)>> - imp_res_tac alloc_const \\ imp_res_tac inst_const \\ - imp_res_tac store_const_sem_const \\ - imp_res_tac sh_mem_op_const \\ - qexists_tac`0` \\ fsrw_tac[ETA_ss][shift_seq_def] \\ NO_TAC) - (* Seq *) - >- ( - fs[case_eq_thms,UNCURRY_EQ] \\ rw[] \\ - gs[] \\ - PURE_REWRITE_TAC[GSYM FLAT_APPEND,GSYM MAP_APPEND,GSYM GENLIST_APPEND, - GSYM FOLDL_APPEND, shift_seq_def] \\ - fs[GSYM shift_seq_def] \\ METIS_TAC[]) - (* If *) - >- ( - fs[case_eq_thms,UNCURRY_EQ] \\ rw[] \\ - TRY(qexists_tac`0` \\ fsrw_tac[ETA_ss][shift_seq_def] \\ NO_TAC) \\ - gs[] \\ - PURE_REWRITE_TAC[GSYM FLAT_APPEND,GSYM MAP_APPEND,GSYM GENLIST_APPEND, - GSYM FOLDL_APPEND, shift_seq_def] \\ - fs[GSYM shift_seq_def] \\ METIS_TAC[]) - (* While *) - >- ( - fs[case_eq_thms,UNCURRY_EQ] \\ rw[] \\ - TRY(qexists_tac`0` \\ fsrw_tac[ETA_ss][shift_seq_def] \\ NO_TAC) \\ - gs[] \\ - PURE_REWRITE_TAC[GSYM FLAT_APPEND,GSYM MAP_APPEND,GSYM GENLIST_APPEND, - GSYM FOLDL_APPEND, shift_seq_def] \\ - fs[GSYM shift_seq_def] \\ METIS_TAC[]) - (* Call *) - >- ( - fs[case_eq_thms,UNCURRY_EQ] \\ rw[] \\ - TRY(qexists_tac`0` \\ fsrw_tac[ETA_ss][shift_seq_def] \\ NO_TAC) \\ - qmatch_goalsub_abbrev_tac`shift_seq w` \\ - qexists_tac`w` \\ simp[] \\ - simp[Abbr`w`]) + rpt conj_tac >> + simp[evaluate_def] >> + rpt (gen_tac ORELSE disch_tac) >> + gvs[AllCaseEqs(),UNCURRY_EQ] >> + map_every imp_res_tac [alloc_const,inst_const,store_const_sem_const,sh_mem_op_const] >> + fs[shift_seq_def] >> + TRY(qexists_tac`0` \\ fsrw_tac[ETA_ss][] \\ NO_TAC) >> + PURE_REWRITE_TAC[GSYM FLAT_APPEND,GSYM MAP_APPEND,GSYM GENLIST_APPEND,GSYM FOLDL_APPEND] >> + TRY ( qmatch_goalsub_abbrev_tac `s.compile_oracle (_ + N)`>> + qexists_tac `N` >> fsrw_tac[ETA_ss][Abbr`N`] \\ NO_TAC) QED Theorem evaluate_mono: @@ -392,22 +417,25 @@ Theorem evaluate_io_events_mono: s1.ffi.io_events ≼ s2.ffi.io_events Proof recInduct evaluate_ind >> - srw_tac[][evaluate_def] >> - every_case_tac >> full_simp_tac(srw_ss())[LET_THM] >> - TRY pairarg_tac >> full_simp_tac(srw_ss())[] >> - imp_res_tac alloc_const >> full_simp_tac(srw_ss())[] >> - imp_res_tac store_const_sem_const >> full_simp_tac(srw_ss())[] >> - imp_res_tac inst_const >> full_simp_tac(srw_ss())[] >> - full_simp_tac(srw_ss())[set_var_def] >> srw_tac[][] >> - every_case_tac >> full_simp_tac(srw_ss())[] >> srw_tac[][] >> - TRY (CHANGED_TAC(full_simp_tac(srw_ss())[ffiTheory.call_FFI_def]) >> - every_case_tac >> full_simp_tac(srw_ss())[] >> srw_tac[][] ) >> - TRY (Cases_on ‘op’>>fs[sh_mem_op_def]>> - fs[sh_mem_load_def,sh_mem_store_def,sh_mem_load32_def,sh_mem_store32_def, - sh_mem_load_byte_def,sh_mem_store_byte_def]>> - fs[ffiTheory.call_FFI_def]>> - rpt (FULL_CASE_TAC>>gvs[]))>> - metis_tac[IS_PREFIX_TRANS] + rpt conj_tac >> + simp[evaluate_def] >> + rpt (gen_tac ORELSE disch_tac) >> + gvs[AllCaseEqs(),UNCURRY_EQ] >> + map_every imp_res_tac [alloc_const,inst_const,store_const_sem_const] >> + fs[] >> rpt (drule_then MATCH_MP_TAC IS_PREFIX_TRANS) >> fs[] + >~[`sh_mem_op`] + >-( + gvs[oneline sh_mem_op_def,sh_mem_load_def,sh_mem_store_def, + sh_mem_load32_def,sh_mem_store32_def,sh_mem_load_byte_def, + sh_mem_store_byte_def,ffiTheory.call_FFI_def,AllCaseEqs()]) + >-(gvs[ffiTheory.call_FFI_def,AllCaseEqs()]) +QED + +Theorem pair_map_eq: + (f ## g) p = (x,y) <=> (∃q r. p = (q,r) /\ x = (f q) /\ y = (g r)) +Proof + Cases_on `p` >> simp[] >> + EQ_TAC >> simp[] QED Theorem evaluate_add_clock: @@ -415,87 +443,36 @@ Theorem evaluate_add_clock: evaluate (p,s) = (r,s') ∧ r ≠ SOME TimeOut ⇒ evaluate (p,s with clock := s.clock + extra) = (r,s' with clock := s'.clock + extra) Proof - recInduct evaluate_ind >> - srw_tac[][evaluate_def] >> full_simp_tac(srw_ss())[LET_THM] >> - TRY ( - rename1`find_code dest (_ \\ _)` >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >- ( - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - every_case_tac >> full_simp_tac(srw_ss())[] >> rveq >> - fsrw_tac[ARITH_ss][dec_clock_def] >> - rev_full_simp_tac(srw_ss()++ARITH_ss)[]) >> - ntac 3 BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> + recInduct evaluate_ind >> rpt conj_tac + >~[`Call`] + >-(srw_tac[][evaluate_def] >> full_simp_tac(srw_ss())[LET_THM] >> + gvs[AllCaseEqs(),UNCURRY_EQ] >> fsrw_tac[ARITH_ss][dec_clock_def] >> - reverse BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> full_simp_tac(srw_ss())[] >- ( - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.FULL_CASE_TAC >> full_simp_tac(srw_ss())[] >> - every_case_tac >> full_simp_tac(srw_ss())[] >> rveq >> full_simp_tac(srw_ss())[] >> - fsrw_tac[ARITH_ss][] >> - rev_full_simp_tac(srw_ss()++ARITH_ss)[]) >> - qpat_x_assum`_ = (_,_)`mp_tac >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - every_case_tac >> full_simp_tac(srw_ss())[] >> strip_tac >> rveq >> - fsrw_tac[ARITH_ss][] >> rveq >> - rev_full_simp_tac(srw_ss()++ARITH_ss)[] >> - NO_TAC) >> - TRY ( - rename1`find_code` >> - full_simp_tac(srw_ss())[get_var_def] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> full_simp_tac(srw_ss())[] >> - every_case_tac >> full_simp_tac(srw_ss())[] >> - rveq >> fsrw_tac[ARITH_ss][dec_clock_def] >> - rev_full_simp_tac(srw_ss()++ARITH_ss)[]) >> - TRY ( - rename1`While` - \\ BasicProvers.TOP_CASE_TAC \\ fs[get_var_def] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ qpat_x_assum`_ = (_,_)`mp_tac - \\ pairarg_tac \\ fs[] - \\ reverse BasicProvers.TOP_CASE_TAC \\ fs[] - >- ( - strip_tac \\ rveq \\ fs[] - \\ pairarg_tac \\ fs[] ) - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - >- ( strip_tac \\ rveq \\ fs[] ) - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ strip_tac \\ fs[] \\ rfs[] - \\ fsrw_tac[ARITH_ss][dec_clock_def] ) >> - TRY ( - rename1 `buffer_flush _ _ _` >> - qpat_x_assum`_ = (_,_)` mp_tac>> - TOP_CASE_TAC>>fs[get_var_def]>- - (rw[]>>fs[])>> - ntac 11 (TOP_CASE_TAC>>fs[])>> - pairarg_tac>>fs[]>> - ntac 5 (TOP_CASE_TAC>>fs[])>> - rw[]>>fs[])>> - TRY pairarg_tac >> full_simp_tac(srw_ss())[] >> - TRY BasicProvers.TOP_CASE_TAC \\ fs[get_var_def] >> - every_case_tac >> full_simp_tac(srw_ss())[] >> rveq >> - full_simp_tac(srw_ss())[get_var_def] >> rveq >> full_simp_tac(srw_ss())[] >> - imp_res_tac alloc_const >> full_simp_tac(srw_ss())[] >> - imp_res_tac store_const_sem_const >> full_simp_tac(srw_ss())[] >> - imp_res_tac inst_const >> full_simp_tac(srw_ss())[] >> - fsrw_tac[ARITH_ss][dec_clock_def] >> - TRY ( - rename1`call_FFI` >> - pairarg_tac >> full_simp_tac(srw_ss())[] >> rveq >> simp[] ) >> - Cases_on ‘op’>>fs[sh_mem_op_def]>> - gs[sh_mem_load_def,sh_mem_store_def,get_var_def,sh_mem_load32_def,sh_mem_store32_def, - sh_mem_load_byte_def,sh_mem_store_byte_def,ffiTheory.call_FFI_def]>> - rpt (FULL_CASE_TAC>>gvs[]) + rev_full_simp_tac(arith_ss)[] >> + fs[]) + >~[`RawCall`] + >-(srw_tac[][evaluate_def] >> full_simp_tac(srw_ss())[LET_THM] >> + gvs[AllCaseEqs(),UNCURRY_EQ] >> + fsrw_tac[ARITH_ss][dec_clock_def] >> + rev_full_simp_tac(arith_ss)[] >> + fs[]) + >~[`While`] + >-(srw_tac[][evaluate_def] >> full_simp_tac(srw_ss())[LET_THM] >> + gvs[AllCaseEqs(),UNCURRY_EQ] >> + fsrw_tac[ARITH_ss][dec_clock_def] >> + irule pair_CASES) + >~[`Tick`] + >-(srw_tac[][evaluate_def] >> full_simp_tac(srw_ss())[LET_THM] >> + gvs[AllCaseEqs(),UNCURRY_EQ] >> + fsrw_tac[ARITH_ss][dec_clock_def] >> + rev_full_simp_tac(arith_ss)[] >> + fs[]) + >> srw_tac[][evaluate_def] >> full_simp_tac(srw_ss())[LET_THM] + >> gvs[AllCaseEqs(),UNCURRY_EQ] + >> map_every imp_res_tac [alloc_const,inst_const,store_const_sem_const,sh_mem_op_const] + >> fs[] + >> fsrw_tac[ARITH_ss][dec_clock_def] + >> fs[pair_map_eq] QED Theorem with_clock_ffi: @@ -509,51 +486,101 @@ Theorem evaluate_add_clock_io_events_mono: (SND(evaluate(e,s))).ffi.io_events ≼ (SND(evaluate(e,s with clock := s.clock + extra))).ffi.io_events Proof - recInduct evaluate_ind >> - srw_tac[][evaluate_def] >> full_simp_tac(srw_ss())[LET_THM,get_var_def] >> - TRY BasicProvers.TOP_CASE_TAC >> full_simp_tac(srw_ss())[] >> - TRY ( - rename1`While` - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ pairarg_tac \\ fs[] - \\ pairarg_tac \\ fs[] - \\ fsrw_tac[ARITH_ss][dec_clock_def] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ imp_res_tac evaluate_io_events_mono \\ fs[] - \\ imp_res_tac evaluate_add_clock \\ fs[] - \\ qmatch_assum_rename_tac`evaluate (c1,s) = (res1,_)` - \\ Cases_on`res1=NONE` \\fs[] - \\ rpt(first_x_assum(qspec_then`extra`mp_tac))\\ simp[] - \\ TRY ( - strip_tac \\ CHANGED_TAC rveq \\ fs[] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ TRY BasicProvers.TOP_CASE_TAC \\ fs[] - \\ metis_tac[evaluate_io_events_mono,PAIR,with_clock_ffi] ) - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ BasicProvers.TOP_CASE_TAC \\ fs[] - \\ metis_tac[IS_PREFIX_TRANS,evaluate_io_events_mono,PAIR,with_clock_ffi] ) >> - every_case_tac >> full_simp_tac(srw_ss())[] >> - imp_res_tac evaluate_add_clock >> full_simp_tac(srw_ss())[] >> - imp_res_tac evaluate_io_events_mono >> full_simp_tac(srw_ss())[dec_clock_def] >> - rveq >> fsrw_tac[ARITH_ss][] >> - rev_full_simp_tac(srw_ss()++ARITH_ss)[] >> - rpt(first_x_assum(qspec_then`extra`mp_tac)>>simp[])>> full_simp_tac(srw_ss())[] >> - TRY( - CHANGED_TAC(simp[ffiTheory.call_FFI_def,get_var_def]) >> - every_case_tac >> full_simp_tac(srw_ss())[get_var_def] >> - rveq >> full_simp_tac(srw_ss())[] >> rveq >> full_simp_tac(srw_ss())[] >> rveq >> full_simp_tac(srw_ss())[]) >> - TRY( - rename1 `buffer_flush _ _ _ = _`>> - pairarg_tac>>fs[]>> - every_case_tac >> fs[get_var_def])>> - TRY (Cases_on ‘op’>>fs[sh_mem_op_def]>> - gs[sh_mem_load_def,sh_mem_store_def,ffiTheory.call_FFI_def, - sh_mem_load32_def,sh_mem_store32_def, - sh_mem_load_byte_def,sh_mem_store_byte_def,get_var_def]>> - rpt (FULL_CASE_TAC>>gvs[]))>> - metis_tac[IS_PREFIX_TRANS,evaluate_io_events_mono,PAIR] + rw[oneline SND] >> ntac 2 (TOP_CASE_TAC >> fs[]) >> + reverse $ Cases_on `q = (SOME TimeOut)` >> gvs[] + >- ( + drule_all evaluate_add_clock >> + strip_tac >> gvs[]) >> + rpt (pop_assum mp_tac) >> + map_every qid_spec_tac (rev [`e`,`s`,`r`,`q'`,`r'`]) >> + recInduct evaluate_ind >> rpt conj_tac + >~ [`Seq`] + >- + (rpt strip_tac >> pop_assum mp_tac >> + gvs[evaluate_def,UNCURRY_EQ,AllCaseEqs()] + >-(imp_res_tac evaluate_add_clock >> fs[]) >> + strip_tac >> gvs[] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) + >~ [`While`] + >- + (rpt strip_tac >> + gvs[evaluate_def,Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 7] + >-( + gvs[AllCaseEqs(),UNCURRY_EQ] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) >> + imp_res_tac evaluate_add_clock >> fs[] >> + gvs[AllCaseEqs()] + >-( + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) >> + fsrw_tac[ARITH_ss][dec_clock_def]) + >~ [`JumpLower`] + >- (rpt strip_tac >> + gvs[evaluate_def,Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 7] + >-( + gvs[AllCaseEqs(),UNCURRY_EQ] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) >> + gvs[AllCaseEqs()] + >- (fsrw_tac[ARITH_ss][dec_clock_def]) + >- (fsrw_tac[ARITH_ss][dec_clock_def])) + >~ [`RawCall`] + >- (rpt strip_tac >> + gvs[evaluate_def,Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 7] + >-( + gvs[AllCaseEqs(),UNCURRY_EQ] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) >> + gvs[AllCaseEqs()] + >- fsrw_tac[ARITH_ss][dec_clock_def] + >- fsrw_tac[ARITH_ss][dec_clock_def]) + >~ [`Call`] + >- (rpt strip_tac >> + gvs[evaluate_def,Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 2] + >- ( + gvs[Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 2] + >-( + gvs[AllCaseEqs(),UNCURRY_EQ] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) >> + gvs[AllCaseEqs()] + >- fsrw_tac[ARITH_ss][dec_clock_def] + >- fsrw_tac[ARITH_ss][dec_clock_def]) + >- ( + gvs[Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 5] + >-( + gvs[AllCaseEqs(),UNCURRY_EQ] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) >> + gvs[Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 3] + >-( + imp_res_tac evaluate_add_clock >> fs[] >> + fsrw_tac[ARITH_ss][dec_clock_def] >> + gvs[] >> gvs[AllCaseEqs()]) + >-( + imp_res_tac evaluate_add_clock >> fs[] >> + fsrw_tac[ARITH_ss][dec_clock_def] >> + gvs[] >> gvs[AllCaseEqs()]) >> + fsrw_tac[ARITH_ss][dec_clock_def] >> + gvs[Ntimes (CONJ UNCURRY_EQ (AllCaseEqs())) 3] + >-( + gvs[AllCaseEqs(),UNCURRY_EQ] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]) + >-( + gvs[AllCaseEqs(),UNCURRY_EQ] >> + imp_res_tac evaluate_io_events_mono >> fs[] >> + METIS_TAC[IS_PREFIX_TRANS]))) + >~ [`ShMemOp`] + >- (rpt strip_tac >> + imp_res_tac evaluate_io_events_mono >> + gvs[evaluate_def,AllCaseEqs()] >> + fsrw_tac[ARITH_ss][dec_clock_def] >> + gvs[pair_map_eq]) + >> (rpt (strip_tac) >> gvs[evaluate_def,AllCaseEqs(),UNCURRY_EQ] >> + NO_TAC) QED Definition clock_neutral_def: From 4b7f7e0d4ac7d2d1bab3e5d401c4cd6441510a56 Mon Sep 17 00:00:00 2001 From: ordinarymath Date: Wed, 30 Apr 2025 14:07:39 +0000 Subject: [PATCH 2/4] Fix word_bignum --- compiler/backend/proofs/word_bignumProofScript.sml | 1 + 1 file changed, 1 insertion(+) diff --git a/compiler/backend/proofs/word_bignumProofScript.sml b/compiler/backend/proofs/word_bignumProofScript.sml index 13a029a14d..7c86ec1d1a 100644 --- a/compiler/backend/proofs/word_bignumProofScript.sml +++ b/compiler/backend/proofs/word_bignumProofScript.sml @@ -2002,6 +2002,7 @@ fun derive_corr_thm const_def = let [DOMSUB_FAPPLY_THM,FAPPLY_FUPDATE_THM,APPLY_UPDATE_THM])) \\ simp_tac std_ss [Once LET_THM])) \\ fs [] \\ rw [] + \\ TRY (CHANGED_TAC (simp[oneline SND]) \\ TOP_CASE_TAC \\ fs[]) \\ imp_res_tac single_add_word_imp_0_1 \\ rw [] \\ TRY eq_tac \\ rw [] \\ fs [true_pres] \\ CONV_TAC sort_writes_conv \\ fs [] From 513a1dabc41ffbc90750906369f31646af88321b Mon Sep 17 00:00:00 2001 From: ordinarymath Date: Fri, 2 May 2025 08:28:39 +0000 Subject: [PATCH 3/4] Fix pull_wordsTheory --- icing/pull_wordsScript.sml | 329 ++++++++++++++++++++++--------------- 1 file changed, 192 insertions(+), 137 deletions(-) diff --git a/icing/pull_wordsScript.sml b/icing/pull_wordsScript.sml index 37c3236f2d..ec4ab20e76 100644 --- a/icing/pull_wordsScript.sml +++ b/icing/pull_wordsScript.sml @@ -1279,149 +1279,204 @@ val mem_tac = >> first_x_assum $ qspec_then ‘n’ assume_tac >> gs[] >> Cases_on ‘EL n refs2’ >> gs[ref_rel_def]; +Triviality v_rel_do_eq': + do_eq a b = A ==> + v_rel a c /\ v_rel b d ==> + do_eq c d = A +Proof + rw[] >> imp_res_tac v_rel_do_eq >> fs[] +QED + +Triviality v_rel_store_assign': + store_assign lnum a refs1 = A ==> + ref_rel a b /\ LIST_REL ref_rel refs1 refs2 ==> + ?B. store_assign lnum b refs2 = B /\ + OPTREL (LIST_REL ref_rel) A B +Proof + rw[] >> + imp_res_tac LIST_REL_LENGTH >> gs[] >> + imp_res_tac LIST_REL_EL_EQN >> gs[] >> + first_x_assum $ qspec_then `lnum` assume_tac >> gs[] >> + gs[store_assign_def] >> + Cases_on `lnum < LENGTH refs2` >> gs[] >> + IF_CASES_TAC >> fs[] >> + gs[oneline store_v_same_type_def,AllCasePreds()] >> + gs[oneline ref_rel_def,AllCasePreds()] >> + fs[LIST_REL_EL_EQN,EL_LUPDATE] >> + rw[] >> + fs[LIST_REL_EL_EQN] +QED + +Triviality v_rel_store_lookup': + store_lookup lnum refs1 = A ==> + LIST_REL ref_rel refs1 refs2 ==> + ?B. store_lookup lnum refs2 = B /\ + OPTREL (ref_rel) A B +Proof + rw[] >> + imp_res_tac LIST_REL_LENGTH >> gs[] >> + imp_res_tac LIST_REL_EL_EQN >> gs[] >> + first_x_assum $ qspec_then `lnum` assume_tac >> gs[] >> + gs[store_lookup_def] >> + Cases_on `lnum < LENGTH refs2` >> gs[] >> + IF_CASES_TAC >> fs[] +QED + +Triviality v_rel_fp_translate': + fp_translate a = A ==> + v_rel a b ==> + fp_translate b = A +Proof + rw[] >> imp_res_tac v_rel_fp_translate >> simp[] +QED + +val RESTR_EVAL_TAC = computeLib.RESTR_EVAL_TAC; +val LENGTH_EQ_NUM_compute' = LIST_CONJ $ map (GEN_ALL o CONV_RULE (LHS_CONV SYM_CONV) o SPEC_ALL) (CONJUNCTS LENGTH_EQ_NUM_compute) +val trivial_tac = gs[AllCaseEqs(),UNCURRY_EQ,Once $ oneline do_app_def, + Excl "IF_NONE_EQUALS_OPTION"] >> + strip_tac >> + rveq >> gs[LENGTH_EQ_NUM_compute,LENGTH_EQ_NUM_compute'] >> + RESTR_EVAL_TAC[``store_assign``,``store_lookup``, + ``store_alloc``, + ``copy_array``,``ws_to_chars``,``chars_to_ws``, + ``EXPLODE``,``call_FFI``]; + Theorem do_app_thm: ∀op a1 a2 refs1 refs2 ffi. LIST_REL v_rel a1 a2 ∧ LIST_REL ref_rel refs1 refs2 ⇒ OPTREL (λ((r1,f1),v1) ((r2,f2),v2). f1 = f2 ∧ res1_rel v1 v2 ∧ LIST_REL ref_rel r1 r2) (do_app (refs1,ffi) op a1) (do_app (refs2,ffi) op a2) -Proof - Cases_on ‘op’ >> gs[Once do_app_def, OPTREL_def] - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- ( - rpt strip_tac - >> ‘LENGTH a1 = LENGTH a2’ by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[]) - >> ntac 3 (TOP_CASE_TAC >> gs[do_app_def]) - >> imp_res_tac $ GSYM v_rel_do_eq - >> TOP_CASE_TAC >> gs[Boolv_def] - >> COND_CASES_TAC >> gs[]) - >- fp_tac - >- fp_tac - >- fp_tac - >- fp_tac - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- ( - rpt strip_tac - >> ‘LENGTH a1 = LENGTH a2’ by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[]) - >> ‘LENGTH refs1 = LENGTH refs2’ by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[]) - >> rpt (TOP_CASE_TAC >> gs[]) - >> gs[do_app_def] - >> gs[store_assign_def, store_v_same_type_def] - >> Cases_on ‘n < LENGTH refs2’ >> gs[] - >> Cases_on ‘EL n refs1’ >> gs[] - >> imp_res_tac LIST_REL_EL_EQN - >> first_x_assum $ qspec_then ‘n’ assume_tac - >> Cases_on ‘EL n refs2’ >> rveq >> gs[ref_rel_def] - >> irule EVERY2_LUPDATE_same - >> gs[ref_rel_def]) - >- mem_tac - >- mem_tac - >- mem_tac - >- mem_tac - >- mem_tac - >- ( - mem_tac - >> rveq >> irule EVERY2_LUPDATE_same >> gs[ref_rel_def]) - >- trivial_tac - >- trivial_tac - >- mem_tac - >- ( - mem_tac - >> rveq >> irule EVERY2_LUPDATE_same >> gs[ref_rel_def]) - >- mem_tac - >- ( - mem_tac - >> imp_res_tac LIST_REL_EL_EQN - >> first_x_assum $ qspec_then ‘n'’ assume_tac >> gs[] - >> Cases_on ‘EL n' refs2’ >> gs[ref_rel_def] - >> rveq >> irule EVERY2_LUPDATE_same >> gs[ref_rel_def]) - >- trivial_tac - >- trivial_tac - >- trivial_tac - >- ( - mem_tac - >> imp_res_tac $ GSYM v_rel_v_to_char_list >> gs[]) - >- mem_tac - >- mem_tac - >- mem_tac - >- ( - mem_tac - >> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def] - >> imp_res_tac $ GSYM v_rel_vs_to_string >> gs[]) - >- ( - mem_tac - >> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def]) - >- ( - mem_tac - >> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def]) - >- ( - mem_tac - >> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def]) - >- ( - mem_tac - >> rewrite_tac $ single LIST_REL_REPLICATE_same - >> strip_tac >> gs[]) - >- mem_tac - >- mem_tac - >- ( - mem_tac - >> TOP_CASE_TAC >> gs[] - >> ‘LENGTH l = LENGTH l'’ - by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[]) - >> gs $ single LIST_REL_EL_EQN) - >- ( mem_tac >> gs $ single LIST_REL_EL_EQN) - >- ( - mem_tac - >> ‘LIST_REL v_rel l l'’ by (gs $ single LIST_REL_EL_EQN) - >> ‘LENGTH l = LENGTH l'’ - by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[]) - >> TOP_CASE_TAC >> gs[store_v_same_type_def] - >> rveq >> irule EVERY2_LUPDATE_same >> gs[] - >> irule EVERY2_LUPDATE_same >> gs[]) - >- ( - mem_tac >> TOP_CASE_TAC >> gs[] - >> ‘LENGTH l = LENGTH l'’ - by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[]) - >> gs[LIST_REL_EL_EQN]) - >- ( - mem_tac >> TOP_CASE_TAC >> gs[] - >> ‘LENGTH l = LENGTH l'’ - by (irule LIST_REL_LENGTH >> asm_exists_tac >> gs[]) - >> gs[LIST_REL_EL_EQN] - >> COND_CASES_TAC >> gs[store_v_same_type_def] - >> Cases_on ‘i < 0’ >> gs[] >> rveq - >> gs[LENGTH_LUPDATE] - >> rpt strip_tac >> gs[LIST_REL_EL_EQN] - >> res_tac >> rewrite_tac [EL_LUPDATE] - >> COND_CASES_TAC >> gs[] - >> irule EVERY2_LUPDATE_same >> gs[] - >> res_tac >> pop_assum $ mp_tac - >> asm_rewrite_tac [] >> gs[ref_rel_def]) - >- mem_tac - >- ( - mem_tac - >> Cases_on ‘i < 0’ >> gs[] - >> rveq >> gs[LIST_REL_EL_EQN] - >> rpt strip_tac - >> res_tac >> rewrite_tac [EL_LUPDATE] - >> COND_CASES_TAC >> gs[]) +Proof[exclude_simps = IF_NONE_EQUALS_OPTION] + rpt strip_tac >> imp_res_tac LIST_REL_LENGTH >> + Cases_on `(do_app (refs1,ffi) op a1)` >> gs[OPTREL_SOME] >> + pop_assum mp_tac + (*NONE Case*) + >- ( + trivial_tac + >>~ [`do_eq`] + >- ( + dxrule_then (drule_all_then SUBST_ALL_TAC) v_rel_do_eq' >> + EVAL_TAC) + >>~-([`fp_translate`], + rpt $ dxrule_then (drule_all_then SUBST_ALL_TAC) v_rel_fp_translate' >> + EVAL_TAC) + >> rpt (dxrule_then (drule_all_then strip_assume_tac) + v_rel_store_lookup' >> + gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), + Excl "IF_NONE_EQUALS_OPTION"]) + >> rpt (dxrule v_rel_store_assign' >> + gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), + Excl "IF_NONE_EQUALS_OPTION"]) + >- (imp_res_tac $ GSYM v_rel_v_to_char_list >> gs[]) + >- (imp_res_tac v_rel_v_to_list >> gs[]) + >- ( + imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME] >> + imp_res_tac v_rel_vs_to_string >> gs[]) + >- (imp_res_tac v_rel_v_to_list >> gs[]) + >- ( + imp_res_tac LIST_REL_LENGTH >> fs[] >> + qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >> + disch_then (drule_at (Pos (el 2))) >> + simp[oneline ref_rel_def,AllCasePreds()] >> + disch_then (qspec_then `VARRAY` mp_tac) >> + simp[Abbr `VARRAY`] >> + impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >> + fs[]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[]) + >- ( + imp_res_tac LIST_REL_LENGTH >> fs[] >> + qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >> + disch_then (drule_at (Pos (el 2))) >> + simp[oneline ref_rel_def,AllCasePreds()] >> + disch_then (qspec_then `VARRAY` mp_tac) >> + simp[Abbr `VARRAY`] >> + impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >> + fs[]) + >- (imp_res_tac v_rel_v_to_list >> gs[]) + >- ( + imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME] >> + imp_res_tac v_rel_vs_to_string >> gs[])) >- ( - mem_tac - >> imp_res_tac v_rel_v_to_list >> gs[OPTREL_def] - >> irule v_rel_list_to_v_app >> gs[]) - >- trivial_tac - >- (mem_tac >> rveq >> irule EVERY2_LUPDATE_same >> gs[]) - >- (mem_tac >> rveq >> irule EVERY2_LUPDATE_same >> gs[]) - >> fp_tac >> simp[nat_to_v_def] + trivial_tac >> fs[] + >>~ [`do_eq`] + >- ( + imp_res_tac v_rel_do_eq >> fs[] + >> fs[COND_RAND]) + >>~-([`fp_translate`], + rpt $ dxrule_then (drule_all_then SUBST_ALL_TAC) v_rel_fp_translate' >> + EVAL_TAC >> + fs[]) + >>~-([`store_alloc`], + gvs[store_alloc_def] >> + fs[LIST_REL_REPLICATE_same]) + >> rpt (dxrule_then (drule_all_then strip_assume_tac) + v_rel_store_lookup' >> + gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), + Excl "IF_NONE_EQUALS_OPTION"]) + >> rpt (dxrule_then (drule_at_then (Pos (el 2)) mp_tac) + v_rel_store_assign' >> + gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), + Excl "IF_NONE_EQUALS_OPTION"]) + >>~ [`store_assign`] + >- ( + qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >> + disch_then (qspec_then `VARRAY` mp_tac) >> + simp[Abbr `VARRAY`] >> + strip_tac >> fs[]) + >- (fs[PULL_EXISTS]) + >- (fs[PULL_EXISTS]) + >- (fs[PULL_EXISTS]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[]) + >- ( + imp_res_tac LIST_REL_LENGTH >> fs[] >> + qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >> + disch_then (qspec_then `VARRAY` mp_tac) >> + simp[Abbr `VARRAY`] >> + impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >> + strip_tac >> fs[]) + >- ( + imp_res_tac LIST_REL_LENGTH >> fs[] >> + qmatch_goalsub_abbrev_tac `store_assign _ VARRAY _` >> + disch_then (qspec_then `VARRAY` mp_tac) >> + simp[Abbr `VARRAY`] >> + impl_tac >- (irule EVERY2_LUPDATE_same >> fs[]) >> + strip_tac >> fs[]) + >- (fs[PULL_EXISTS]) + >- (fs[PULL_EXISTS]) + >>~ [`v_to_char_list`] + >- (imp_res_tac $ GSYM v_rel_v_to_char_list >> gs[]) + >>~ [`v_to_list`,`vs_to_string`] + >- ( + imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME] >> + imp_res_tac v_rel_vs_to_string >> gs[]) + >>~ [`v_to_list`,`list_to_v`] + >- (imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME] + >> irule v_rel_list_to_v >> fs[] + >> irule LIST_REL_APPEND_suff >> fs[]) + >>~ [`v_to_list`] + >- (imp_res_tac v_rel_v_to_list >> gs[OPTREL_SOME]) + >>~ [`list_to_v`] + >- fs[v_rel_list_to_v_char] + (*TODO figure out a way to automate this*) + >- (Cases_on `n2 = 0` >> gvs[]) + >- (fs[COND_RAND]) + >- (fs[COND_RAND]) + >- (TOP_CASE_TAC >> fs[]) + >- (TOP_CASE_TAC >> fs[]) + >- (TOP_CASE_TAC >> fs[]) + >- (TOP_CASE_TAC >> fs[]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[] >> + fs[LIST_REL_EL_EQN]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[] >> + fs[LIST_REL_EL_EQN]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[]) + >- (imp_res_tac LIST_REL_LENGTH >> fs[] >> + fs[LIST_REL_EL_EQN])) QED @@ -1942,7 +1997,7 @@ Theorem ALL_DISTINCT_MAP: Proof Induct_on ‘funs’ >> gs[] >> rpt strip_tac >> Cases_on ‘h’ >> gs[] - >> Cases_on ‘r’ >> gs[MEM_MAP] >> EQ_TAC >> rpt strip_tac + >> gs[MEM_MAP] >> EQ_TAC >> rpt strip_tac >- (rveq >> Cases_on ‘y'’ >> gs[] >> Cases_on ‘r’ >> gs[]) >- (gs[]) From 175c6c779bd1915754f948568ddced72cb86a0b4 Mon Sep 17 00:00:00 2001 From: ordinarymath Date: Fri, 2 May 2025 08:31:58 +0000 Subject: [PATCH 4/4] remove whitespace --- icing/pull_wordsScript.sml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/icing/pull_wordsScript.sml b/icing/pull_wordsScript.sml index ec4ab20e76..14e3d28c82 100644 --- a/icing/pull_wordsScript.sml +++ b/icing/pull_wordsScript.sml @@ -1291,7 +1291,7 @@ Triviality v_rel_store_assign': store_assign lnum a refs1 = A ==> ref_rel a b /\ LIST_REL ref_rel refs1 refs2 ==> ?B. store_assign lnum b refs2 = B /\ - OPTREL (LIST_REL ref_rel) A B + OPTREL (LIST_REL ref_rel) A B Proof rw[] >> imp_res_tac LIST_REL_LENGTH >> gs[] >> @@ -1304,14 +1304,14 @@ Proof gs[oneline ref_rel_def,AllCasePreds()] >> fs[LIST_REL_EL_EQN,EL_LUPDATE] >> rw[] >> - fs[LIST_REL_EL_EQN] + fs[LIST_REL_EL_EQN] QED Triviality v_rel_store_lookup': store_lookup lnum refs1 = A ==> LIST_REL ref_rel refs1 refs2 ==> ?B. store_lookup lnum refs2 = B /\ - OPTREL (ref_rel) A B + OPTREL (ref_rel) A B Proof rw[] >> imp_res_tac LIST_REL_LENGTH >> gs[] >> @@ -1347,7 +1347,7 @@ Theorem do_app_thm: OPTREL (λ((r1,f1),v1) ((r2,f2),v2). f1 = f2 ∧ res1_rel v1 v2 ∧ LIST_REL ref_rel r1 r2) (do_app (refs1,ffi) op a1) (do_app (refs2,ffi) op a2) -Proof[exclude_simps = IF_NONE_EQUALS_OPTION] +Proof[exclude_simps = IF_NONE_EQUALS_OPTION] rpt strip_tac >> imp_res_tac LIST_REL_LENGTH >> Cases_on `(do_app (refs1,ffi) op a1)` >> gs[OPTREL_SOME] >> pop_assum mp_tac @@ -1361,11 +1361,11 @@ Proof[exclude_simps = IF_NONE_EQUALS_OPTION] >>~-([`fp_translate`], rpt $ dxrule_then (drule_all_then SUBST_ALL_TAC) v_rel_fp_translate' >> EVAL_TAC) - >> rpt (dxrule_then (drule_all_then strip_assume_tac) - v_rel_store_lookup' >> + >> rpt (dxrule_then (drule_all_then strip_assume_tac) + v_rel_store_lookup' >> gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), Excl "IF_NONE_EQUALS_OPTION"]) - >> rpt (dxrule v_rel_store_assign' >> + >> rpt (dxrule v_rel_store_assign' >> gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), Excl "IF_NONE_EQUALS_OPTION"]) >- (imp_res_tac $ GSYM v_rel_v_to_char_list >> gs[]) @@ -1411,12 +1411,12 @@ Proof[exclude_simps = IF_NONE_EQUALS_OPTION] >>~-([`store_alloc`], gvs[store_alloc_def] >> fs[LIST_REL_REPLICATE_same]) - >> rpt (dxrule_then (drule_all_then strip_assume_tac) - v_rel_store_lookup' >> + >> rpt (dxrule_then (drule_all_then strip_assume_tac) + v_rel_store_lookup' >> gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), Excl "IF_NONE_EQUALS_OPTION"]) >> rpt (dxrule_then (drule_at_then (Pos (el 2)) mp_tac) - v_rel_store_assign' >> + v_rel_store_assign' >> gs[OPTREL_SOME,oneline ref_rel_def,AllCasePreds(), Excl "IF_NONE_EQUALS_OPTION"]) >>~ [`store_assign`]