From 6d3a605ae9abb831c3d28268fd3cfdd07311fae3 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Mon, 15 Aug 2022 21:35:32 +0200 Subject: [PATCH] update for FMCAD 2022 artifact --- README.md | 10 +- bir/Holmakefile | 2 +- cakeml/Holmakefile | 2 +- .../milExampleBranchEqualScript.sml | 246 ++++++----- .../milExampleCopyEqualScript.sml | 4 +- misc/milUtilityScript.sml | 17 + semantics/milCompositionalScript.sml | 6 +- semantics/milLifeCycleOoOScript.sml | 6 +- semantics/milMetaScript.sml | 362 +-------------- semantics/milMetaSpScript.sml | 19 - semantics/milScript.sml | 39 +- semantics/milSemanticsUtilityScript.sml | 414 +++++++++++++++++- 12 files changed, 587 insertions(+), 540 deletions(-) rename executable/milBranchEqualScript.sml => examples/milExampleBranchEqualScript.sml (80%) rename executable/milCopyEqualScript.sml => examples/milExampleCopyEqualScript.sml (99%) delete mode 100644 semantics/milMetaSpScript.sml diff --git a/README.md b/README.md index 1175f4e..51fb6e1 100644 --- a/README.md +++ b/README.md @@ -123,11 +123,11 @@ This can take around 15 minutes on a modern machine. The directory `bir` contains an (unverified) SML function that translates a BIR program to a MIL program, and some examples of using this function. -To build the translator, [HolBA](https://github.com/kth-step/HolBA) with the tag `mil` must be present in a sibling directory named `HolBA`: +To build the translator, [HolBA](https://github.com/kth-step/HolBA) with the tag `FMCAD2022_artifact` must be present in a sibling directory named `HolBA`: ```shell git clone https://github.com/kth-step/HolBA.git cd HolBA -git checkout mil +git checkout FMCAD2022_artifact ``` With the `HolBA` directory available as a sibling, the translator can be built by running: @@ -166,8 +166,12 @@ cp path/to/MIL/cakeml/mil_reg_translate.cml . make mil_reg_translate.cake ./mil_reg_translate.cake ``` + On a modern machine, compilation can take a few minutes, but running the program should take -only a few milliseconds to output a MIL trace. +only a few milliseconds to output the following MIL trace: +``` +[il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4, il 0wx0, il 0wx4] +``` In comparison, the HOL4 `EVAL_TAC` call that proves the equivalent theorem `ex_bir_prog_IO_bounded_trace_long` in `bir/bir_to_mil_test_basicScript.sml` diff --git a/bir/Holmakefile b/bir/Holmakefile index 8a00302..26c27a8 100644 --- a/bir/Holmakefile +++ b/bir/Holmakefile @@ -1,4 +1,4 @@ -# tested with: https://github.com/kth-step/HolBA/releases/tag/mil +# tested with: https://github.com/kth-step/HolBA/releases/tag/FMCAD2022_artifact HOLBADIR = ../../HolBA INCLUDES = $(MILDIR)/misc \ $(MILDIR)/semantics \ diff --git a/cakeml/Holmakefile b/cakeml/Holmakefile index acef0c7..de773e7 100644 --- a/cakeml/Holmakefile +++ b/cakeml/Holmakefile @@ -1,6 +1,6 @@ # tested with: https://github.com/CakeML/cakeml/releases/tag/v1469 CAKEMLDIR = ../../cakeml -# tested with: https://github.com/kth-step/HolBA/releases/tag/mil +# tested with: https://github.com/kth-step/HolBA/releases/tag/FMCAD2022_artifact HOLBADIR = ../../HolBA INCLUDES = $(MILDIR)/misc \ $(MILDIR)/semantics \ diff --git a/executable/milBranchEqualScript.sml b/examples/milExampleBranchEqualScript.sml similarity index 80% rename from executable/milBranchEqualScript.sml rename to examples/milExampleBranchEqualScript.sml index fdb5889..7f2f5d1 100644 --- a/executable/milBranchEqualScript.sml +++ b/examples/milExampleBranchEqualScript.sml @@ -1,10 +1,10 @@ -open HolKernel boolLib Parse bossLib metisTools wordsLib wordsTheory finite_mapTheory listTheory pred_setTheory sortingTheory milUtilityTheory milTheory milSemanticsUtilityTheory milMetaTheory milMetaIOTheory milTracesTheory milCompositionalTheory milExampleUtilityTheory milStoreTheory milExecutableExamplesTheory milExecutableUtilityTheory milExecutableTransitionTheory milExecutableIOTheory milExecutableIOTraceTheory milExecutableCompositionalTheory; +open HolKernel boolLib Parse bossLib metisTools wordsLib wordsTheory finite_mapTheory listTheory pred_setTheory sortingTheory milUtilityTheory milTheory milSemanticsUtilityTheory milMetaTheory milMetaIOTheory milTracesTheory milInitializationTheory milCompositionalTheory milExampleUtilityTheory milStoreTheory milExecutableExamplesTheory milExecutableUtilityTheory milExecutableTransitionTheory milExecutableInitializationTheory milExecutableIOTheory milExecutableIOTraceTheory milExecutableCompositionalTheory; (* ======================= *) -(* Branch-on-equal program *) +(* Branch-on-equal example *) (* ======================= *) -val _ = new_theory "milBranchEqual"; +val _ = new_theory "milExampleBranchEqual"; (* ------------------- *) (* Program definitions *) @@ -77,7 +77,7 @@ Proof rw [example_beq_list_t,example_beq_t,example_beq_list_set] QED -Theorem example_beq_list_map: +Theorem example_beq_list_map[local]: !tb0 tb1 tb2 tb3 tb4 tb5 tb6 tb7 tb8 reg adr. MAP bound_name_instr (example_beq_list tb0 tb1 tb2 tb3 tb4 tb5 tb6 tb7 tb8 reg adr) = [tb0; tb1; tb2; tb3; tb4; tb5; tb6; tb7; tb8] @@ -374,51 +374,27 @@ QED (* Generic initialization *) (* ---------------------- *) -(* FIXME: replace with initialize_state when possible *) -Definition initialize_state_beq: - initialize_state_beq reg reg0 pc0 = - State_st - { i_assign 1 (e_val val_true) (o_internal (e_val reg)); - i_assign 2 (e_val val_true) (o_internal (e_val reg0)); - i_assign 3 (e_val val_true) (o_store res_REG 1 2); - i_assign 4 (e_val val_true) (o_internal (e_val val_zero)); - i_assign 5 (e_val val_true) (o_internal (e_val pc0)); - i_assign 6 (e_val val_true) (o_store res_PC 4 5) } - (FEMPTY |+ (1,reg) |+ (2,reg0) |+ (3,reg0) |+ (4,val_zero) |+ (5,pc0) |+ (6,pc0)) - {} {6} -End - -(* FIXME: replace with initialize_state_list when possible *) -Definition initialize_state_list_beq: - initialize_state_list_beq reg reg0 pc0 = - (State_st_list - [ i_assign 1 (e_val val_true) (o_internal (e_val reg)); - i_assign 2 (e_val val_true) (o_internal (e_val reg0)); - i_assign 3 (e_val val_true) (o_store res_REG 1 2); - i_assign 4 (e_val val_true) (o_internal (e_val val_zero)); - i_assign 5 (e_val val_true) (o_internal (e_val pc0)); - i_assign 6 (e_val val_true) (o_store res_PC 4 5) ] - (FEMPTY |+ (1,reg) |+ (2,reg0) |+ (3,reg0) |+ (4,val_zero) |+ (5,pc0) |+ (6,pc0)) - [] [6], 6:num) -End - -Theorem initialize_state_beq_state_list_to_state: - !reg reg0 pc0. - state_list_to_state (FST (initialize_state_list_beq reg reg0 pc0)) = - initialize_state_beq reg reg0 pc0 -Proof - rw [initialize_state_list_beq,initialize_state_beq,state_list_to_state] -QED - -Theorem initialize_state_list_beq_NO_DUPLICATES: - !reg reg0 pc0. - NO_DUPLICATES (state_program_list (FST (initialize_state_list_beq reg reg0 pc0))) +(* FIXME: not needed with general well_formed_ok proof *) +Theorem initialize_state_list_reg_expand[local]: + !reg adr reg0 pc0. + initialize_state_list [] [(reg,reg0)] pc0 = + (State_st_list + [ + i_assign 1 (e_val val_true) (o_internal (e_val reg)); + i_assign 2 (e_val val_true) (o_internal (e_val reg0)); + i_assign 3 (e_val val_true) (o_store res_REG 1 2); + i_assign 4 (e_val val_true) (o_internal (e_val val_zero)); + i_assign 5 (e_val val_true) (o_internal (e_val pc0)); + i_assign 6 (e_val val_true) (o_store res_PC 4 5) + ] + (FEMPTY |+ (1,reg) |+ (2,reg0) |+ (3,reg0) |+ (4,val_zero) |+ (5,pc0) |+ (6,pc0)) + [] [6], 6) Proof - rw [state_program_list,initialize_state_list_beq,NO_DUPLICATES,ALL_DISTINCT,bound_name_instr] + rw [] >> EVAL_TAC QED (* FIXME: should not be needed *) -Theorem initialize_state_beq_FLOOKUP_expand: +Theorem initialize_state_list_reg_FLOOKUP_expand[local]: !reg reg0 pc0. FLOOKUP (FEMPTY |+ (1:num,reg) |+ (2,reg0) |+ (3,reg0) |+ (4,val_zero) |+ (5,pc0) |+ (6,pc0)) 1 = SOME reg /\ FLOOKUP (FEMPTY |+ (1:num,reg) |+ (2,reg0) |+ (3,reg0) |+ (4,val_zero) |+ (5,pc0) |+ (6,pc0)) 2 = SOME reg0 /\ @@ -430,77 +406,100 @@ Proof rw [] >> EVAL_TAC >> rw [] QED -Theorem addr_of_initialize_state_beq: +(* FIXME: should not be needed *) +Theorem initialize_state_list_reg_NO_DUPLICATES[local]: !reg reg0 pc0. - addr_of (state_program (initialize_state_beq reg reg0 pc0)) 6 = - SOME (res_PC,4) + NO_DUPLICATES + [i_assign 1 (e_val val_true) (o_internal (e_val reg)); + i_assign 2 (e_val val_true) (o_internal (e_val reg0)); + i_assign 3 (e_val val_true) (o_store res_REG 1 2); + i_assign 4 (e_val val_true) (o_internal (e_val val_zero)); + i_assign 5 (e_val val_true) (o_internal (e_val pc0)); + i_assign 6 (e_val val_true) (o_store res_PC 4 5)] Proof - rw [] >> - MP_TAC (Q.SPECL [`reg`,`reg0`,`pc0`] initialize_state_list_beq_NO_DUPLICATES) >> - rw [GSYM initialize_state_beq_state_list_to_state,GSYM state_program_list_correct] >> - rw [GSYM addr_of_list_correct] >> - rw [addr_of_list,state_program_list,initialize_state_list_beq,FIND_instr,bound_name_instr] -QED - -(* FIXME: derive from general lemma *) -Theorem initialize_state_beq_well_formed_state: - !reg reg0 pc0. well_formed_state (initialize_state_beq reg reg0 pc0) -Proof - rw [initialize_state_beq,well_formed_state,bound_names_program] >> - fs [bound_name_instr,free_names_instr,names_e,names_o,map_down,sem_instr] >> - rw [sem_expr_correct,val_true,val_false] >> - fs [initialize_state_beq_FLOOKUP_expand] >> - TRY(METIS_TAC[bound_name_instr]) >> - rw [str_may,SUBSET_DEF] >> fs [bound_name_instr,val_true] >> - MP_TAC (Q.SPECL [`reg`,`reg0`,`pc0`] addr_of_initialize_state_beq) >> - rw [state_program,initialize_state_beq,val_true] >> - strip_tac >> - rw [] >> fs [] + rw [NO_DUPLICATES,ALL_DISTINCT,bound_name_instr] +QED + +(* FIXME: should not be needed *) +Theorem initialize_state_list_reg_state_list_to_set[local]: + !reg adr reg0 pc0. + { i_assign 1 (e_val val_true) (o_internal (e_val reg)); + i_assign 2 (e_val val_true) (o_internal (e_val reg0)); + i_assign 3 (e_val val_true) (o_store res_REG 1 2); + i_assign 4 (e_val val_true) (o_internal (e_val val_zero)); + i_assign 5 (e_val val_true) (o_internal (e_val pc0)); + i_assign 6 (e_val val_true) (o_store res_PC 4 5) } = + set [ i_assign 1 (e_val val_true) (o_internal (e_val reg)); + i_assign 2 (e_val val_true) (o_internal (e_val reg0)); + i_assign 3 (e_val val_true) (o_store res_REG 1 2); + i_assign 4 (e_val val_true) (o_internal (e_val val_zero)); + i_assign 5 (e_val val_true) (o_internal (e_val pc0)); + i_assign 6 (e_val val_true) (o_store res_PC 4 5) + ] +Proof + rw [] QED (* FIXME: not needed with general well_formed_ok proof *) -Theorem initialize_state_list_beq_well_formed_ok: - !reg reg0 pc0 stl tmax. - initialize_state_list_beq reg reg0 pc0 = (stl,tmax) ==> +Theorem initialize_state_list_reg_well_formed_ok[local]: + !reg adr reg0 pc0 stl tmax. + initialize_state_list [] [(reg,reg0)] pc0 = (stl,tmax) ==> State_st_list_well_formed_ok stl /\ max_name_in_state_list stl <= tmax Proof - strip_tac >> strip_tac >> strip_tac >> strip_tac >> strip_tac >> - MP_TAC (Q.SPECL [`reg`,`reg0`,`pc0`] initialize_state_list_beq_NO_DUPLICATES) >> - MP_TAC (Q.SPECL [`reg`,`reg0`,`pc0`] initialize_state_beq_well_formed_state) >> - MP_TAC (Q.SPECL [`reg`,`reg0`,`pc0`] initialize_state_beq_state_list_to_state) >> - rw [ - initialize_state_list_beq, - initialize_state_beq, - state_program_list, - max_name_in_state_list - ] >- - (once_rewrite_tac [State_st_list_well_formed_ok] >> rw []) >> - EVAL_TAC + rw [initialize_state_list_reg_expand] >- + (rw [State_st_list_well_formed_ok] >- + rw [NO_DUPLICATES,bound_name_instr] >> + rw [well_formed_state,state_list_to_state,bound_names_program] >> + fs [bound_name_instr,free_names_instr,names_e,names_o,map_down,sem_instr] >> + rw [sem_expr_correct,val_true,val_false] >> + fs [initialize_state_list_reg_FLOOKUP_expand] >> + TRY(METIS_TAC[bound_name_instr]) >> + MP_TAC (Q.SPECL [`reg`,`reg0`,`pc0`] initialize_state_list_reg_NO_DUPLICATES) >> + rw [str_may,SUBSET_DEF] >> fs [bound_name_instr,val_true] >> + `addr_of_list [ + i_assign 1 (e_val 1w) (o_internal (e_val reg)); + i_assign 2 (e_val 1w) (o_internal (e_val reg0)); + i_assign 3 (e_val 1w) (o_store res_REG 1 2); + i_assign 4 (e_val 1w) (o_internal (e_val val_zero)); + i_assign 5 (e_val 1w) (o_internal (e_val pc0)); + i_assign 6 (e_val 1w) (o_store res_PC 4 5) + ] 6 = SOME (res_REG,ta)` + by METIS_TAC [val_true,initialize_state_list_reg_state_list_to_set,addr_of_list_correct] >| [ + fs [addr_of_list,FIND_instr,bound_name_instr], + fs [initialize_state_list_reg_FLOOKUP_expand], + fs [addr_of_list,FIND_instr,bound_name_instr], + fs [addr_of_list,FIND_instr,bound_name_instr], + fs [initialize_state_list_reg_FLOOKUP_expand], + fs [addr_of_list,FIND_instr,bound_name_instr] + ]) >> + rw [max_name_in_state_list,max_bound_name_list,bound_name_instr] QED -Theorem initialize_state_list_beq_tmax_6: - !reg reg0 pc0 stl tmax. - initialize_state_list_beq reg reg0 pc0 = (stl,tmax) ==> +(* FIXME: derivable from more general lemmas *) +Theorem initialize_state_list_reg_tmax_6[local]: + !reg adr reg0 pc0 stl tmax. + initialize_state_list [] [(reg,reg0)] pc0 = (stl,tmax) ==> tmax = 6 Proof - EVAL_TAC >> rw [] + rw [initialize_state_list_reg_expand] QED -Theorem initialize_state_list_beq_length_6: - !reg reg0 pc0 stl tmax. - initialize_state_list_beq reg reg0 pc0 = (stl,tmax) ==> +(* FIXME: derivable from more general lemmas *) +Theorem initialize_state_list_reg_length_6[local]: + !reg adr reg0 pc0 stl tmax. + initialize_state_list [] [(reg,reg0)] pc0 = (stl,tmax) ==> LENGTH (state_program_list stl) = 6 Proof - EVAL_TAC >> rw [] >> rw [state_program_list] + rw [initialize_state_list_reg_expand] >> rw [state_program_list] QED (* FIXME: derivable from more general lemmas *) -Theorem initialize_state_list_beq_SORTED: - !reg reg0 pc0 stl tmax. - initialize_state_list_beq reg reg0 pc0 = (stl,tmax) ==> +Theorem initialize_state_list_reg_SORTED[local]: + !reg adr reg0 pc0 stl tmax. + initialize_state_list [] [(reg,reg0)] pc0 = (stl,tmax) ==> SORTED bound_name_instr_le (state_program_list stl) Proof - EVAL_TAC >> rw [] >> + rw [initialize_state_list_reg_expand] >> rw [state_program_list,bound_name_instr_le,name_le,bound_name_instr] QED @@ -510,27 +509,32 @@ QED Definition initialize_example_beq: initialize_example_beq reg adr reg0 pc0 = - let st = initialize_state_beq reg reg0 pc0 in + let st = initialize_state {} {(reg,reg0)} pc0 in union_program_state st (example_beq_t (max_name_in_State st) reg adr) End Definition initialize_example_beq_list: initialize_example_beq_list reg adr reg0 pc0 = - let (stl,tmax) = initialize_state_list_beq reg reg0 pc0 in + let (stl,tmax) = initialize_state_list [] [(reg,reg0)] pc0 in append_program_state_list stl (example_beq_list_t tmax reg adr) End (* FIXME: prove using general theorems *) -Theorem initialize_example_beq_list_eq: +Theorem initialize_example_beq_list_eq[local]: !reg adr reg0 pc0. state_list_to_state (initialize_example_beq_list reg adr reg0 pc0) = initialize_example_beq reg adr reg0 pc0 Proof - rw [initialize_example_beq_list,initialize_example_beq] >> + rw [initialize_example_beq,initialize_example_beq_list] >> rw [example_beq_list_t_set] >> - rw [GSYM initialize_state_beq_state_list_to_state] >> - rw [GSYM append_program_state_list_correct] >> + `FINITE {}` by rw [] >> + `FINITE {(reg,reg0)}` by rw [] >> + `SET_TO_LIST {(reg,reg0)} = [(reg,reg0)]` by rw [SET_TO_LIST_SING] >> + `SET_TO_LIST {} = []` by rw [] >> + `initialize_state {} {(reg,reg0)} pc0 = state_list_to_state (FST (initialize_state_list [] [(reg,reg0)] pc0))` + by rw [GSYM initialize_state_list_eq] >> rw [max_name_in_state_list_correct] >> + rw [GSYM append_program_state_list_correct] >> EVAL_TAC QED @@ -539,43 +543,43 @@ Theorem initialize_example_beq_list_well_formed_ok: State_st_list_well_formed_ok (initialize_example_beq_list reg adr reg0 pc0) Proof rw [initialize_example_beq_list] >> - Cases_on `initialize_state_list_beq reg reg0 pc0` >> + Cases_on `initialize_state_list [] [(reg,reg0)] pc0` >> rename1 `(stl,tmax)` >> `State_st_list_well_formed_ok stl /\ max_name_in_state_list stl <= tmax` - by METIS_TAC [initialize_state_list_beq_well_formed_ok] >> + by METIS_TAC [initialize_state_list_reg_well_formed_ok] >> rw [] >> - METIS_TAC [example_beq_list_t_compositional_well_formed_ok] + METIS_TAC [example_beq_list_t_compositional_well_formed_ok] QED -Theorem initialize_example_beq_list_not_Completed_list: +Theorem initialize_example_beq_list_not_Completed_list[local]: !reg adr reg0 pc0. ~(Completed_list sem_expr (initialize_example_beq_list reg adr reg0 pc0) (i_assign 7 (e_val val_true) (o_internal (e_val val_zero)))) Proof rw [initialize_example_beq_list] >> - Cases_on `initialize_state_list_beq reg reg0 pc0` >> + Cases_on `initialize_state_list [] [(reg,reg0)] pc0` >> rename1 `(stl,tmax)` >> rw [] >> `7:num = 6 + 1` by DECIDE_TAC >> `tmax = 6` suffices_by METIS_TAC [ - initialize_state_list_beq_well_formed_ok, + initialize_state_list_reg_well_formed_ok, example_beq_list_t_not_Completed_list_HD ] >> - METIS_TAC [initialize_state_list_beq_tmax_6] + METIS_TAC [initialize_state_list_reg_tmax_6] QED -Theorem initialize_example_beq_list_NTH: +Theorem initialize_example_beq_list_NTH[local]: !reg adr reg0 pc0. NTH (PRE 7) (state_program_list (initialize_example_beq_list reg adr reg0 pc0)) = SOME (i_assign 7 (e_val val_true) (o_internal (e_val val_zero))) Proof rw [initialize_example_beq_list] >> - Cases_on `initialize_state_list_beq reg reg0 pc0` >> + Cases_on `initialize_state_list [] [(reg,reg0)] pc0` >> rename1 `(stl,tmax)` >> rw [] >> `LENGTH (state_program_list stl) = 6` - by METIS_TAC [initialize_state_list_beq_length_6] >> + by METIS_TAC [initialize_state_list_reg_length_6] >> Cases_on `stl` >> rename1 `State_st_list il0 s0 cl0 fl0` >> fs [state_program_list,append_program_state_list] >> @@ -584,20 +588,20 @@ Proof `6 = PRE (SUC (LENGTH il0)) /\ tmax = 6` suffices_by METIS_TAC [example_beq_list_t_NTH] >> rw [] >> - METIS_TAC [initialize_state_list_beq_tmax_6] + METIS_TAC [initialize_state_list_reg_tmax_6] QED -Theorem initialize_example_beq_list_SORTED: +Theorem initialize_example_beq_list_SORTED[local]: !reg adr reg0 pc0. SORTED bound_name_instr_le (state_program_list (initialize_example_beq_list reg adr reg0 pc0)) Proof rw [initialize_example_beq_list] >> - Cases_on `initialize_state_list_beq reg reg0 pc0` >> + Cases_on `initialize_state_list [] [(reg,reg0)] pc0` >> rename1 `(stl,tmax)` >> rw [] >> `SORTED bound_name_instr_le (state_program_list stl)` - by METIS_TAC [initialize_state_list_beq_SORTED] >> - `max_name_in_state_list stl <= tmax` by METIS_TAC [initialize_state_list_beq_well_formed_ok] >> + by METIS_TAC [initialize_state_list_reg_SORTED] >> + `max_name_in_state_list stl <= tmax` by METIS_TAC [initialize_state_list_reg_well_formed_ok] >> `compositional_program (set (example_beq_list_t tmax reg adr)) (max_name_in_state_list stl)` by METIS_TAC [example_beq_t_compositional_program,example_beq_list_t_set] >> METIS_TAC [compositional_program_append_program_state_list_SORTED,example_beq_list_t_SORTED] @@ -608,12 +612,12 @@ Theorem example_beq_list_Completed_up_to: Proof rw [ initialize_example_beq_list, - initialize_state_list_beq, + initialize_state_list_reg_expand, append_program_state_list, Completed_list_up_to ] >> fs [Completed_list] >> - rw [initialize_state_beq_FLOOKUP_expand] + rw [initialize_state_list_reg_FLOOKUP_expand] QED (* --------------------------------------- *) @@ -628,7 +632,9 @@ Theorem initialize_example_beq_list_reg_not_1_IO_bounded_trace: Proof rw [val_one,val_four] >> POP_ASSUM (fn thm => - CONV_TAC (computeLib.RESTR_EVAL_CONV [] + CONV_TAC (computeLib.RESTR_EVAL_CONV + [``IO_bounded_trace translate_val_list sem_expr_exe + (initialize_example_beq_list reg adr reg0 pc0) 7 (SUC 8)``] THENC (REWRITE_CONV [thm]) THENC EVAL)) QED diff --git a/executable/milCopyEqualScript.sml b/examples/milExampleCopyEqualScript.sml similarity index 99% rename from executable/milCopyEqualScript.sml rename to examples/milExampleCopyEqualScript.sml index 119214d..9496c9a 100644 --- a/executable/milCopyEqualScript.sml +++ b/examples/milExampleCopyEqualScript.sml @@ -1,10 +1,10 @@ open HolKernel boolLib Parse bossLib metisTools wordsLib wordsTheory finite_mapTheory listTheory pred_setTheory sortingTheory milUtilityTheory milTheory milSemanticsUtilityTheory milMetaTheory milMetaIOTheory milTracesTheory milInitializationTheory milCompositionalTheory milExampleUtilityTheory milStoreTheory milExecutableExamplesTheory milExecutableUtilityTheory milExecutableTransitionTheory milExecutableInitializationTheory milExecutableIOTheory milExecutableIOTraceTheory milExecutableCompositionalTheory; (* ===================== *) -(* Copy-on-equal program *) +(* Copy-on-equal example *) (* ===================== *) -val _ = new_theory "milCopyEqual"; +val _ = new_theory "milExampleCopyEqual"; (* ------------------- *) (* Program definitions *) diff --git a/misc/milUtilityScript.sml b/misc/milUtilityScript.sml index b300797..18fed33 100644 --- a/misc/milUtilityScript.sml +++ b/misc/milUtilityScript.sml @@ -390,6 +390,23 @@ Proof METIS_TAC [NOT_FDOM_FAPPLY_FEMPTY] QED +Theorem FLOOKUP_FEMPTY_FUNION_EQ: + !f t v. t NOTIN FDOM f ==> + f |+ (t,v) = FUNION (FEMPTY |+ (t,v)) f +Proof + rw [] >> + `FDOM (f |+ (t,v)) = t INSERT (FDOM f)` by rw [FDOM_FUPDATE] >> + sg `FDOM (FUNION (FEMPTY |+ (t,v)) f) = t INSERT (FDOM f)` >- + (fs [FDOM_FUNION] >> + rw [UNION_DEF] >> once_rewrite_tac [INSERT_DEF] >> + rw [EXTENSION] >> METIS_TAC []) >> + `!t'. t IN FDOM (f |+ (t,v)) ==> (f |+ (t,v)) ' t' = (FUNION (FEMPTY |+ (t,v)) f) ' t'` + suffices_by fs [fmap_EXT] >> + rw [] >> Cases_on `t = t'` >- rw [FUNION_DEF] >> + rw [FUNION_DEF,NOT_EQ_FAPPLY] >> + METIS_TAC [NOT_FDOM_FAPPLY_FEMPTY] +QED + Theorem fupdate_fupdate_neq_reorder: !s k1 k2 v1 v2. k1 NOTIN FDOM s ==> diff --git a/semantics/milCompositionalScript.sml b/semantics/milCompositionalScript.sml index 6ab067a..ac3b8b3 100644 --- a/semantics/milCompositionalScript.sml +++ b/semantics/milCompositionalScript.sml @@ -203,8 +203,7 @@ Proof `!t'. t' IN bound_names_program I1 ==> t < t'` by (rw [bound_names_program] >> METIS_TAC [compositional_program_state_lt_bound_name_instr,bound_name_instr]) >> - rw [GSYM str_may_union_I_eq] >> - METIS_TAC [wfs_C_str_may], + METIS_TAC [wfs_C_str_may, GSYM str_may_union_I_eq], `?t1 t2 c. i_assign t c (o_store res_PC t1 t2) IN I0` by METIS_TAC [wfs_F_exists_store_pc] >> @@ -220,8 +219,7 @@ Proof `!t'. t' IN bound_names_program I1 ==> t < t'` by (rw [bound_names_program] >> METIS_TAC [compositional_program_state_lt_bound_name_instr,bound_name_instr]) >> - rw [GSYM str_may_union_I_eq] >> - METIS_TAC [wfs_F_str_may] + METIS_TAC [wfs_F_str_may,GSYM str_may_union_I_eq] ] QED diff --git a/semantics/milLifeCycleOoOScript.sml b/semantics/milLifeCycleOoOScript.sml index 2522a95..a58d5be 100644 --- a/semantics/milLifeCycleOoOScript.sml +++ b/semantics/milLifeCycleOoOScript.sml @@ -8,8 +8,10 @@ val _ = new_theory "milLifeCycleOoO"; Datatype: out_of_order_lifecycle = - | out_of_order_lifecycle_Decoded | out_of_order_lifecycle_Executed - | out_of_order_lifecycle_Committed | out_of_order_lifecycle_Fetched + | out_of_order_lifecycle_Decoded + | out_of_order_lifecycle_Executed + | out_of_order_lifecycle_Committed + | out_of_order_lifecycle_Fetched End val out_of_order_lifecycle_distinct = fetch "-" "out_of_order_lifecycle_distinct"; diff --git a/semantics/milMetaScript.sml b/semantics/milMetaScript.sml index a5cade5..574010e 100644 --- a/semantics/milMetaScript.sml +++ b/semantics/milMetaScript.sml @@ -1132,253 +1132,7 @@ Proof Cases_on `FLOOKUP s t` >> fs [FLOOKUP_DEF] QED -(* Lemma 10, part 2 *) -Theorem str_may_union_I_eq: - !I s C Fs I' t. - t IN bound_names_program I ==> - (!t'. t' IN bound_names_program I' ==> t < t') ==> - str_may (State_st I s C Fs) t = str_may (State_st (I UNION I') s C Fs) t -Proof - rw [] >> fs [str_may] >> rw [EXTENSION] >> fs [] >> - EQ_TAC >- METIS_TAC [addr_of_union_I_eq] >> - sg `t NOTIN bound_names_program I''` >- - (`t IN bound_names_program I'' ==> F` suffices_by METIS_TAC [] >> STRIP_TAC >> - `t < t` by METIS_TAC [] >> fs []) >> - rw [] >> fs [] >> TRY(METIS_TAC [instr_in_bound_names_program,addr_of_union_I_eq]) >> - `t' IN bound_names_program I''` by METIS_TAC [instr_in_bound_names_program] >> - `t < t'` by METIS_TAC [] >> fs [] -QED - -(* Lemma 10, part 3 *) -Theorem str_may_funion_s_eq[local]: - !I s C Fs s' t. t IN bound_names_program I ==> - (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> - (!t'. t' IN FDOM s' ==> t' >= t) ==> - str_may (State_st I s C Fs) t = str_may (State_st I (FUNION s s') C Fs) t -Proof - rw [] >> fs [str_may] >> rw [EXTENSION] >> fs [] >> EQ_TAC >- - (rw [] >> fs [] >| [ - `sem_expr c' (FUNION s s') = SOME v` by rw [sem_expr_funion] >> - rw [FLOOKUP_FUNION], - - `sem_expr c' (FUNION s s') = SOME v` by rw [sem_expr_funion] >> - METIS_TAC [store_in_flookup_eq], - - `sem_expr c' (FUNION s s') = SOME v` by rw [sem_expr_funion] >> - rw [store_in_flookup_eq] >> - `FLOOKUP s ta = FLOOKUP (FUNION s s') ta` suffices_by METIS_TAC [] >> - `(?c. i_assign t c (o_load r ta) IN I') \/ - (?c tv. i_assign t c (o_store r ta tv) IN I')` - by METIS_TAC [addr_of_some_exist_load_or_store] >- - METIS_TAC [load_t_in_flookup_eq] >> - METIS_TAC [store_t_in_flookup_eq], - - rw [FLOOKUP_FUNION] >> METIS_TAC [store_in_sem_expr_eq], - - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> METIS_TAC [store_in_flookup_eq], - - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> - `FLOOKUP s ta = FLOOKUP (FUNION s s') ta` suffices_by METIS_TAC [] >> - `(?c. i_assign t c (o_load r ta) IN I') \/ - (?c tv. i_assign t c (o_store r ta tv) IN I')` - by METIS_TAC [addr_of_some_exist_load_or_store] >- - METIS_TAC [load_t_in_flookup_eq] >> - METIS_TAC [store_t_in_flookup_eq] - ]) >> - rw [] >> fs [] >| [ - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> - `FLOOKUP s ta' = SOME v'` by METIS_TAC [store_in_flookup_eq] >> - `FLOOKUP s ta = SOME v'` suffices_by METIS_TAC [] >> - `(?c. i_assign t c (o_load r ta) IN I') \/ - (?c tv. i_assign t c (o_store r ta tv) IN I')` - by METIS_TAC [addr_of_some_exist_load_or_store] >- - METIS_TAC [load_t_in_flookup_eq] >> - METIS_TAC [store_t_in_flookup_eq], - - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> - fs [FLOOKUP_FUNION] >> - Cases_on `FLOOKUP s ta'` >> fs [] >> Cases_on `FLOOKUP s ta` >> fs [], - - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> - fs [FLOOKUP_FUNION] >> Cases_on `FLOOKUP s ta` >> fs [], - - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> - `FLOOKUP s ta' = SOME v` by METIS_TAC [store_in_flookup_eq] >> - `FLOOKUP s ta = SOME v` suffices_by METIS_TAC [] >> - `(?c. i_assign t c (o_load r ta) IN I') \/ - (?c tv. i_assign t c (o_store r ta tv) IN I')` - by METIS_TAC [addr_of_some_exist_load_or_store] >- - METIS_TAC [load_t_in_flookup_eq] >> - METIS_TAC [store_t_in_flookup_eq], - - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> - METIS_TAC [store_in_flookup_eq], - - rw [] >- METIS_TAC [store_in_sem_expr_eq] >> - `FLOOKUP s ta = NONE` suffices_by METIS_TAC [] >> - `(?c. i_assign t c (o_load r ta) IN I') \/ - (?c tv. i_assign t c (o_store r ta tv) IN I')` - by METIS_TAC [addr_of_some_exist_load_or_store] >- - METIS_TAC [load_t_in_flookup_eq] >> - METIS_TAC [store_t_in_flookup_eq] - ] -QED - -(* Lemma 10, part 4 *) -Theorem str_may_union_eq[local]: - !I s C Fs I' s' C' Fs' t. - t IN bound_names_program I ==> - (!t'. t' IN bound_names_program I' ==> t < t') ==> - (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> - (!t'. t' IN FDOM s' ==> t' >= t) ==> - str_may (State_st I s C Fs) t = str_may (State_st (I UNION I') (FUNION s s') C' Fs') t -Proof - rw [] >> - `str_may (State_st I' s C Fs) t = str_may (State_st I' s C' Fs') t` - by rw [str_may_unaffected_C_F] >> - `str_may (State_st I' s C' Fs') t = - str_may (State_st I' (FUNION s s') C' Fs') t` - by rw [str_may_funion_s_eq] >> - `str_may (State_st I' (FUNION s s') C' Fs') t = - str_may (State_st (I' UNION I'') (FUNION s s') C' Fs') t` - by rw [str_may_union_I_eq] >> - METIS_TAC [] -QED - -(* Lemma 10, part 5 *) -Theorem str_act_unaffected_C_F[local]: - !I s C Fs C' Fs' t. - str_act (State_st I s C Fs) t = str_act (State_st I s C' Fs') t -Proof - rw [str_act,EXTENSION] >> EQ_TAC >> rw [] >> METIS_TAC [str_may] -QED - -(* Lemma 10, part 6 *) -Theorem str_act_union_I_eq[local]: - !I s C Fs I' t. - t IN bound_names_program I ==> - (!t'. t' IN bound_names_program I' ==> t < t') ==> - str_act (State_st I s C Fs) t = str_act (State_st (I UNION I') s C Fs) t -Proof - rw [] >> fs [str_act] >> rw [EXTENSION] >> - fs [] >> EQ_TAC >> rw [] >| [ - METIS_TAC [str_may_union_I_eq], - METIS_TAC [addr_of_union_I_eq,str_may_union_I_eq], - METIS_TAC [str_may_union_I_eq], - METIS_TAC [addr_of_union_I_eq,str_may_union_I_eq] - ] -QED - -(* Lemma 10, part 7 *) -Theorem str_act_funion_s_eq[local]: - !I s C Fs s' t. - t IN bound_names_program I ==> - (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> - (!t'. t' IN FDOM s' ==> t' >= t) ==> - str_act (State_st I s C Fs) t = str_act (State_st I (FUNION s s') C Fs) t -Proof - rw [] >> fs [str_act] >> rw [EXTENSION] >> fs [] >> EQ_TAC >> rw [] >| [ - METIS_TAC [str_may_funion_s_eq], - - rw [] >> - Cases_on `i'' IN str_may (State_st I' (FUNION s s') C Fs) t` >> rw [] >> - `i_assign t'' c'' (o_store r ta'' tv'') IN I'` by fs [str_may] >> - Cases_on `t'' > t'` >> rw [] >> - `i_assign t' c' (o_store r ta' tv') IN I'` by fs [str_may] >> - `i_assign t'' c'' (o_store r ta'' tv'') IN str_may (State_st I' s C Fs) t` - by METIS_TAC [str_may_funion_s_eq] >> - `t' < t''` by DECIDE_TAC >> - `t'' < t` by fs [str_may] >> - `(!v. sem_expr c'' s <> SOME v \/ v = val_false) \/ - (!v. FLOOKUP s ta'' <> SOME v \/ FLOOKUP s ta <> SOME v) /\ - !v. FLOOKUP s ta'' <> SOME v \/ FLOOKUP s ta' <> SOME v` - by METIS_TAC [] >- METIS_TAC [store_in_sem_expr_eq] >> - `t' < t` by fs [str_may] >> - `FLOOKUP (FUNION s s') ta'' = FLOOKUP s ta''` - by METIS_TAC [store_in_flookup_eq] >> - `FLOOKUP (FUNION s s') ta' = FLOOKUP s ta'` - by METIS_TAC [store_in_flookup_eq] >> - `FLOOKUP (FUNION s s') ta = FLOOKUP s ta` - suffices_by METIS_TAC [] >> - `(?c. i_assign t c (o_load r ta) IN I') \/ - (?c tv. i_assign t c (o_store r ta tv) IN I')` - by METIS_TAC [addr_of_some_exist_load_or_store] >- - METIS_TAC [load_t_in_flookup_eq] >> - METIS_TAC [store_t_in_flookup_eq], - - METIS_TAC [str_may_funion_s_eq], - - rw [] >> - `i_assign t' c' (o_store r ta' tv') IN I'` by fs [str_may] >> - `i_assign t' c' (o_store r ta' tv') IN str_may (State_st I' s C Fs) t` - by METIS_TAC [str_may_funion_s_eq] >> - `t' < t` by fs [str_may] >> - Cases_on `i'' IN str_may (State_st I' s C Fs) t` >> rw [] >> - `i_assign t'' c'' (o_store r ta'' tv'') IN I'` by fs [str_may] >> - `t'' < t` by fs [str_may] >> - Cases_on `t'' > t'` >> rw [] >> - `i_assign t'' c'' (o_store r ta'' tv'') IN str_may (State_st I' (FUNION s s') C Fs) t` - by METIS_TAC [str_may_funion_s_eq] >> - `(!v. sem_expr c'' (FUNION s s') <> SOME v \/ v = val_false) \/ - (!v. FLOOKUP (FUNION s s') ta'' <> SOME v \/ - FLOOKUP (FUNION s s') ta <> SOME v) /\ - !v. FLOOKUP (FUNION s s') ta'' <> SOME v \/ - FLOOKUP (FUNION s s') ta' <> SOME v` - by METIS_TAC [] >- METIS_TAC [store_in_sem_expr_eq] >> - `FLOOKUP (FUNION s s') ta'' = FLOOKUP s ta''` - by METIS_TAC [store_in_flookup_eq] >> - `FLOOKUP (FUNION s s') ta' = FLOOKUP s ta'` - by METIS_TAC [store_in_flookup_eq] >> - `FLOOKUP (FUNION s s') ta = FLOOKUP s ta` - suffices_by METIS_TAC [] >> - `(?c. i_assign t c (o_load r ta) IN I') \/ - (?c tv. i_assign t c (o_store r ta tv) IN I')` - by METIS_TAC [addr_of_some_exist_load_or_store] >- - METIS_TAC [load_t_in_flookup_eq] >> - METIS_TAC [store_t_in_flookup_eq] -] -QED - -(* Lemma 10, part 8 *) -Theorem str_act_union_eq[local]: - !I s C Fs I' s' C' Fs' t. - t IN bound_names_program I ==> - (!t'. t' IN bound_names_program I' ==> t < t') ==> - (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> - (!t'. t' IN FDOM s' ==> t' >= t) ==> - str_act (State_st I s C Fs) t = - str_act (State_st (I UNION I') (FUNION s s') C' Fs') t -Proof - rw [] >> - `str_act (State_st I' s C Fs) t = str_act (State_st I' s C' Fs') t` - by rw [str_act_unaffected_C_F] >> - `str_act (State_st I' s C' Fs') t = str_act (State_st I' (FUNION s s') C' Fs') t` - by rw [str_act_funion_s_eq] >> - `str_act (State_st I' (FUNION s s') C' Fs') t = - str_act (State_st (I' UNION I'') (FUNION s s') C' Fs') t` - by rw [str_act_union_I_eq] >> - METIS_TAC [] -QED - -(* Lemma 10 *) -Theorem str_may_act_union_eq: - !I s C Fs I' s' C' Fs' t. - t IN bound_names_program I ==> - (!t'. t' IN bound_names_program I' ==> t < t') ==> - (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> - (!t'. t' IN FDOM s' ==> t' >= t) ==> - str_may (State_st I s C Fs) t = - str_may (State_st (I UNION I') (FUNION s s') C' Fs') t /\ - str_act (State_st I s C Fs) t = - str_act (State_st (I UNION I') (FUNION s s') C' Fs') t -Proof - METIS_TAC [ - str_may_union_eq, - str_act_union_eq - ] -QED - -(* not needed probably: i IN I *) +(* not needed: i IN I *) (* Lemma 11, part 1 *) Theorem OoO_transition_str_may_subset[local]: !I s C Fs I' s' C' Fs' t obs al t. @@ -1393,30 +1147,19 @@ Proof by METIS_TAC [well_formed_OoO_transition_well_formed,step_invariant] >> Cases_on `i` >> rw [bound_name_instr] >> fs [out_of_order_step_cases] >> rw [] >| [ - `t NOTIN FDOM s` by (fs [map_up,map_down] >> - Cases_on `FLOOKUP s t` >> - fs [FLOOKUP_DEF]) >> + `t NOTIN FDOM s` + by (fs [map_up,map_down] >> Cases_on `FLOOKUP s t` >> fs [FLOOKUP_DEF]) >> METIS_TAC [fupdate_in_str_may], `str_may (State_st I' s (C UNION {t}) Fs) n = str_may (State_st I' s C Fs) n` suffices_by METIS_TAC [SUBSET_REFL] >> rw [str_may_unaffected_C_F], - `str_may (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C (Fs UNION {t})) n = - str_may (State_st I' s C Fs) n` - suffices_by METIS_TAC [SUBSET_REFL] >> - `str_may (State_st I' s C Fs) n = - str_may (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C Fs) n` - suffices_by METIS_TAC [str_may_unaffected_C_F] >> - `n IN bound_names_program I'` - by METIS_TAC [instr_in_bound_names_program] >> - `!t'. t' IN bound_names_program (translate_val v (MAX_SET (bound_names_program I'))) ==> n < t'` - suffices_by METIS_TAC [str_may_union_I_eq] >> - rw [] >> - `FINITE I'` by METIS_TAC [wfs_FINITE] >> - `?c' mop'. i_assign t' c' mop' IN translate_val v (MAX_SET (bound_names_program I'))` - by METIS_TAC [bound_names_program_in_instr] >> - METIS_TAC [translate_val_max_name_lt_i_assign] + METIS_TAC [ + union_translate_val_subset_str_may, + wfs_FINITE, + instr_in_bound_names_program + ] ] QED @@ -1429,76 +1172,9 @@ Theorem str_act_step_subset[local]: Proof Cases_on `al` >| [ rw [SUBSET_DEF] >> - `I' = I''` by METIS_TAC [OoO_exe_transition_same_I] >> rw [] >> - `x IN str_may (State_st I' s' C' Fs') (bound_name_instr i)` by - fs [str_act] >> - `?t1 c1 r t11 t12. x = i_assign t1 c1 (o_store r t11 t12)` - by METIS_TAC [in_str_may_store] >> rw [] >> - - sg `(?c ta. i = i_assign (bound_name_instr i) c (o_load r ta)) \/ - (?c ta tv. i = i_assign (bound_name_instr i) c (o_store r ta tv))` >- - (`(?c ta. i_assign (bound_name_instr i) c (o_load r ta) IN I') \/ - (?c ta tv. i_assign (bound_name_instr i) c (o_store r ta tv) IN I')` - suffices_by METIS_TAC [wfs_unique_instr_names,bound_name_instr] >> - METIS_TAC [in_str_may_load_or_store]) >- - (Cases_on `i` >> rw [] >> fs [bound_name_instr] >> rw [] >> - sg `i_assign t1 c1 (o_store r t11 t12) IN str_may (State_st I' s C Fs) n` >- - METIS_TAC [OoO_transition_str_may_subset,SUBSET_DEF,bound_name_instr] >> - Cases_on `i_assign t1 c1 (o_store r t11 t12) IN str_act (State_st I' s C Fs) n` >> - rw [] >> - `addr_of I' n = SOME (r,ta)` - by METIS_TAC [addr_of_contains_unique_load,wfs_unique_instr_names] >> - sg `?t2 c2 t21 t22. i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s C Fs) n /\ - t2 > t1 /\ (?v. sem_expr c2 s = SOME v /\ v <> val_false) /\ - ((?v. FLOOKUP s t21 = SOME v /\ FLOOKUP s ta = SOME v) \/ - (?v. FLOOKUP s t21 = SOME v /\ FLOOKUP s t11 = SOME v))` >- - (fs [str_act] >> METIS_TAC []) >- - (`sem_expr c2 s' = SOME v` by METIS_TAC [OoO_transition_monotonicity_sem_expr_s] >> - `FLOOKUP s' t21 = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - `FLOOKUP s' ta = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s' C' Fs') n` >- - (fs [str_act] >- METIS_TAC [] >> - PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> - fs [] >> rw [] >> METIS_TAC []) >> - `?v''. FLOOKUP s' ta = SOME v'' /\ v'' <> v'` suffices_by rw [] >> - fs [str_may] >> METIS_TAC []) >> - `sem_expr c2 s' = SOME v` by METIS_TAC [OoO_transition_monotonicity_sem_expr_s] >> - `FLOOKUP s' t21 = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - `FLOOKUP s' t11 = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s' C' Fs') n` >- - (fs [str_act] >- METIS_TAC [] >> - PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> - fs [] >> rw [] >> METIS_TAC []) >> - fs [str_may] >> METIS_TAC []) >> - Cases_on `i` >> rw [] >> fs [bound_name_instr] >> rw [] >> - sg `i_assign t1 c1 (o_store r t11 t12) IN str_may (State_st I' s C Fs) n` >- - METIS_TAC [OoO_transition_str_may_subset,SUBSET_DEF,bound_name_instr] >> - Cases_on `i_assign t1 c1 (o_store r t11 t12) IN str_act (State_st I' s C Fs) n` >> - rw [] >> - `addr_of I' n = SOME (r,ta)` - by METIS_TAC [addr_of_contains_unique_store,wfs_unique_instr_names] >> - sg `?t2 c2 t21 t22. i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s C Fs) n /\ - t2 > t1 /\ (?v. sem_expr c2 s = SOME v /\ v <> val_false) /\ - ((?v. FLOOKUP s t21 = SOME v /\ FLOOKUP s ta = SOME v) \/ - (?v. FLOOKUP s t21 = SOME v /\ FLOOKUP s t11 = SOME v))` >- - (fs [str_act] >> METIS_TAC []) >- - (`sem_expr c2 s' = SOME v` by METIS_TAC [OoO_transition_monotonicity_sem_expr_s] >> - `FLOOKUP s' t21 = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - `FLOOKUP s' ta = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s' C' Fs') n` >- - (fs [str_act] >- METIS_TAC [] >> - PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> - fs [] >> rw [] >> METIS_TAC []) >> - `?v''. FLOOKUP s' ta = SOME v'' /\ v'' <> v'` suffices_by rw [] >> - fs [str_may] >> METIS_TAC []) >> - `sem_expr c2 s' = SOME v` by METIS_TAC [OoO_transition_monotonicity_sem_expr_s] >> - `FLOOKUP s' t21 = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - `FLOOKUP s' t11 = SOME v'` by METIS_TAC [OoO_transition_monotonicity_lookup_s] >> - Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s' C' Fs') n` >- - (fs [str_act] >- METIS_TAC [] >> - PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> - fs [] >> rw [] >> METIS_TAC []) >> - fs [str_may] >> METIS_TAC [], + fs [out_of_order_step_cases,map_up,map_down] >> rw [] >> + `t' NOTIN FDOM s` by fs [FLOOKUP_DEF] >> + METIS_TAC [fupdate_in_str_act,wfs_unique_instr_names], rw [] >> fs [out_of_order_step_cases] >> rw [] >> `str_act (State_st I' s (C UNION {t'}) Fs) (bound_name_instr i) = @@ -1507,21 +1183,9 @@ Proof rw [str_act_unaffected_C_F], rw [] >> fs [out_of_order_step_cases] >> rw [] >> - `str_act (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C (Fs UNION {t'})) (bound_name_instr i) = - str_act (State_st I' s C Fs) (bound_name_instr i)` - suffices_by METIS_TAC [SUBSET_REFL] >> - `str_act (State_st I' s C Fs) (bound_name_instr i) = - str_act (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C Fs) (bound_name_instr i)` - suffices_by METIS_TAC [str_act_unaffected_C_F] >> `bound_name_instr i IN bound_names_program I'` - by (Cases_on `i` >> rw [bound_name_instr] >> METIS_TAC [instr_in_bound_names_program]) >> - `!t'. t' IN bound_names_program (translate_val v (MAX_SET (bound_names_program I'))) ==> (bound_name_instr i) < t'` - suffices_by METIS_TAC [str_act_union_I_eq] >> rw [] >> - `FINITE I'` by METIS_TAC [wfs_FINITE] >> - `?c' mop. i_assign t'' c' mop IN translate_val v (MAX_SET (bound_names_program I'))` - by METIS_TAC [bound_names_program_in_instr] >> - Cases_on `i` >> rw [bound_name_instr] >> - METIS_TAC [translate_val_max_name_lt_i_assign] + by (fs [bound_names_program] >> METIS_TAC []) >> + METIS_TAC [union_translate_val_subset_str_act,wfs_FINITE] ] QED diff --git a/semantics/milMetaSpScript.sml b/semantics/milMetaSpScript.sml deleted file mode 100644 index d05da5d..0000000 --- a/semantics/milMetaSpScript.sml +++ /dev/null @@ -1,19 +0,0 @@ -open HolKernel boolLib Parse bossLib wordsTheory finite_mapTheory pred_setTheory milTheory milUtilityTheory milTracesTheory milMetaTheory; - -(* -------------------------------------- *) -(* Metatheory of MIL's In-Order Semantics *) -(* -------------------------------------- *) - -val _ = new_theory "milMetaSp"; - -Definition name_instr_in_state_ext: - name_instr_in_state_ext t (State_ext_st I' s Cs Fs d' Ps) = - (t IN bound_names_program I') -End - -(* FIXME *) -Definition well_formed_state_ext: - well_formed_state_ext (State_ext_st I' s Cs Fs d' Ps) = T -End - -val _ = export_theory (); diff --git a/semantics/milScript.sml b/semantics/milScript.sml index 633373a..c058f4f 100644 --- a/semantics/milScript.sml +++ b/semantics/milScript.sml @@ -5,7 +5,6 @@ local open arithmeticTheory stringTheory containerTheory pred_setTheory listTheo val _ = new_theory "mil"; - open wordsTheory; val _ = type_abbrev("k", ``:num``); (* index variable (subscript) *) @@ -65,30 +64,12 @@ obs = (* observation *) | obs_il of v (* load from instructions *) `; val _ = Hol_datatype ` -act_ext = (* extended action *) - act_ext_prd (* predict *) - | act_ext_exe (* execute *) - | act_ext_pexe (* execute predicted *) - | act_ext_cmt of v => v (* commit *) - | act_ext_ftc of I (* fetch *) - | act_ext_ret (* retire *) - | act_ext_rbk (* rollback *) -`; -val _ = Hol_datatype ` act = (* action *) act_exe (* execute *) | act_cmt of v => v (* commit *) | act_ftc of I (* fetch *) `; val _ = Hol_datatype ` -State_ext = (* extended state *) - State_ext_st of I => s => N => N => d => N -`; -val _ = Hol_datatype ` -m = (* extended label *) - m_lb of obs => act_ext => t -`; -val _ = Hol_datatype ` State = (* state *) State_st of I => s => N => N `; @@ -132,21 +113,6 @@ Definition instr_in_State: instr_in_State (i:i) ((State_st I s C f):State) = (i IN I) End -(* FIXME: dummy definition *) -Definition deps_t_State: - deps_t_State (t:t) (S:State) : N = {} -End - -(* FIXME: dummy definition *) -Definition state_equiv_t: - state_equiv_t (S:State) (t:t) (S':State) = T -End - -(* FIXME: dummy definition *) -Definition Delta_plus: - Delta_plus (d:d) (t:t) : N = {} -End - Definition bound_name_instr: bound_name_instr ((i_assign t e opm):i) = t End @@ -156,10 +122,9 @@ Definition bound_names_program: { t | ?i. i IN I /\ t = bound_name_instr i } End -(* FIXME: to be validated *) Definition program_difference_names: - program_difference_names (I:I) (N:N) : I = - { i | i IN I /\ ~((bound_name_instr i) IN N) } + program_difference_names (I0:I) (N0:N) : I = + { i | i IN I0 /\ bound_name_instr i NOTIN N0 } End Definition names_e: diff --git a/semantics/milSemanticsUtilityScript.sml b/semantics/milSemanticsUtilityScript.sml index 6238afa..2ef7070 100644 --- a/semantics/milSemanticsUtilityScript.sml +++ b/semantics/milSemanticsUtilityScript.sml @@ -1136,9 +1136,9 @@ Proof QED Theorem fupdate_in_str_may: - !I s C Fs t v c mop n c' mop' i. + !I s C Fs C' Fs' t v n. t NOTIN FDOM s ==> - str_may (State_st I (s |+ (t,v)) C Fs) n SUBSET str_may (State_st I s C Fs) n + str_may (State_st I (s |+ (t,v)) C' Fs') n SUBSET str_may (State_st I s C Fs) n Proof fs [SUBSET_DEF] >> rw [] >> Cases_on `x` >> @@ -1358,6 +1358,416 @@ Proof rw [] >> fs [Completed,str_may] >> fs [] QED +(* Lemma 10, part 5 *) +Theorem str_act_unaffected_C_F: + !I s C Fs C' Fs' t. + str_act (State_st I s C Fs) t = str_act (State_st I s C' Fs') t +Proof + rw [str_act,EXTENSION] >> EQ_TAC >> rw [] >> METIS_TAC [str_may] +QED + +Theorem fupdate_in_str_act: + !I' s' C Fs C' Fs'. + (!i i'. i IN I' ==> i' IN I' ==> bound_name_instr i = bound_name_instr i' ==> i = i') ==> + !i t t' v. + t NOTIN FDOM s' ==> + i IN str_act (State_st I' (s' |+ (t,v)) C' Fs') t' ==> + i IN str_act (State_st I' s' C Fs) t' +Proof + rw [] >> + `i IN str_act (State_st I' (s' |+ (t,v)) C Fs) t'` + by METIS_TAC [str_act_unaffected_C_F] >> + PAT_X_ASSUM ``i IN str_act (State_st I' (s' |+ (t,v)) C' Fs') t'`` (fn thm => ALL_TAC) >> + `?i'. i' IN I' /\ bound_name_instr i' = t'` + by (`?r ta. addr_of I' t' = SOME (r,ta)` by fs [str_act,str_may] >> + METIS_TAC [addr_of_some_exist_load_or_store,bound_name_instr]) >> + rw [] >> + rename1 `x IN str_act (State_st I' (s' |+ (t,v)) C Fs) (bound_name_instr i')` >> + rename1 `i IN I'` >> + `x IN str_may (State_st I' (s' |+ (t,v)) C Fs) (bound_name_instr i)` by + fs [str_act] >> + `?t1 c1 r t11 t12. x = i_assign t1 c1 (o_store r t11 t12)` + by METIS_TAC [in_str_may_store] >> rw [] >> + + sg `(?c ta. i = i_assign (bound_name_instr i) c (o_load r ta)) \/ + (?c ta tv. i = i_assign (bound_name_instr i) c (o_store r ta tv))` >- + (`(?c ta. i_assign (bound_name_instr i) c (o_load r ta) IN I') \/ + (?c ta tv. i_assign (bound_name_instr i) c (o_store r ta tv) IN I')` + suffices_by METIS_TAC [bound_name_instr] >> + METIS_TAC [in_str_may_load_or_store]) >- + (Cases_on `i` >> rw [] >> fs [bound_name_instr] >> rw [] >> + + `i_assign t1 c1 (o_store r t11 t12) IN str_may (State_st I' s' C Fs) n` + by METIS_TAC [fupdate_in_str_may,SUBSET_DEF,bound_name_instr] >> + Cases_on `i_assign t1 c1 (o_store r t11 t12) IN str_act (State_st I' s' C Fs) n` >> + rw [] >> + `addr_of I' n = SOME (r,ta)` + by METIS_TAC [addr_of_contains_unique_load] >> + + sg `?t2 c2 t21 t22. i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s' C Fs) n /\ + t2 > t1 /\ (?v. sem_expr c2 s' = SOME v /\ v <> val_false) /\ + ((?v. FLOOKUP s' t21 = SOME v /\ FLOOKUP s' ta = SOME v) \/ + (?v. FLOOKUP s' t21 = SOME v /\ FLOOKUP s' t11 = SOME v))` >- + (fs [str_act] >> METIS_TAC []) >- + (`sem_expr c2 (s' |+ (t,v)) = SOME v'` by METIS_TAC [sem_expr_notin_fdom_some_fupdate] >> + `t21 IN FDOM s'` by fs [FLOOKUP_DEF] >> + `t21 <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) t21 = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + `ta IN FDOM s'` by fs [FLOOKUP_DEF] >> + `ta <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) ta = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' (s' |+ (t,v)) C Fs) n` >- + (fs [str_act] >- METIS_TAC [] >> + PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> + fs [] >> rw [] >> METIS_TAC []) >> + `?v'''. FLOOKUP (s' |+ (t,v)) ta = SOME v''' /\ v''' <> v''` suffices_by rw [] >> + fs [str_may] >> METIS_TAC []) >> + + `sem_expr c2 (s' |+ (t,v)) = SOME v'` by METIS_TAC [sem_expr_notin_fdom_some_fupdate] >> + `t21 IN FDOM s'` by fs [FLOOKUP_DEF] >> + `t21 <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) t21 = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + `t11 IN FDOM s'` by fs [FLOOKUP_DEF] >> + `t11 <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) t11 = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' (s' |+ (t,v)) C Fs) n` >- + (fs [str_act] >- METIS_TAC [] >> + PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> + fs [] >> rw [] >> METIS_TAC []) >> + fs [str_may] >> METIS_TAC []) >> + + Cases_on `i` >> rw [] >> fs [bound_name_instr] >> rw [] >> + sg `i_assign t1 c1 (o_store r t11 t12) IN str_may (State_st I' s' C Fs) n` >- + METIS_TAC [fupdate_in_str_may,SUBSET_DEF,bound_name_instr] >> + Cases_on `i_assign t1 c1 (o_store r t11 t12) IN str_act (State_st I' s' C Fs) n` >> + rw [] >> + `addr_of I' n = SOME (r,ta)` by METIS_TAC [addr_of_contains_unique_store] >> + sg `?t2 c2 t21 t22. i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' s' C Fs) n /\ + t2 > t1 /\ (?v. sem_expr c2 s' = SOME v /\ v <> val_false) /\ + ((?v. FLOOKUP s' t21 = SOME v /\ FLOOKUP s' ta = SOME v) \/ + (?v. FLOOKUP s' t21 = SOME v /\ FLOOKUP s' t11 = SOME v))` >- + (fs [str_act] >> METIS_TAC []) >- + (`sem_expr c2 (s' |+ (t,v)) = SOME v'` by METIS_TAC [sem_expr_notin_fdom_some_fupdate] >> + `t21 IN FDOM s'` by fs [FLOOKUP_DEF] >> + `t21 <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) t21 = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + `ta IN FDOM s'` by fs [FLOOKUP_DEF] >> + `ta <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) ta = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + + Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' (s' |+ (t,v)) C Fs) n` >- + (fs [str_act] >- METIS_TAC [] >> + PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> + fs [] >> rw [] >> METIS_TAC []) >> + `?v'''. FLOOKUP s' ta = SOME v''' /\ v''' <> v''` suffices_by rw [] >> + fs [str_may] >> METIS_TAC []) >> + + `sem_expr c2 (s' |+ (t,v)) = SOME v'` by METIS_TAC [sem_expr_notin_fdom_some_fupdate] >> + `t21 IN FDOM s'` by fs [FLOOKUP_DEF] >> + `t21 <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) t21 = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + `t11 IN FDOM s'` by fs [FLOOKUP_DEF] >> + `t11 <> t` by METIS_TAC [] >> + `FLOOKUP (s' |+ (t,v)) t11 = SOME v''` by fs [FLOOKUP_DEF,NOT_EQ_FAPPLY] >> + Cases_on `i_assign t2 c2 (o_store r t21 t22) IN str_may (State_st I' (s' |+ (t,v)) C Fs) n` >- + (fs [str_act] >- METIS_TAC [] >> + PAT_ASSUM ``!i''. P`` (fn thm => ASSUME_TAC (SPEC ``i_assign t2 c2 (o_store r t21 t22)`` thm)) >> + fs [] >> rw [] >> METIS_TAC []) >> + fs [str_may] >> METIS_TAC [] +QED + +Theorem fupdate_subset_str_act: + !I s C Fs. + (!i i'. i IN I ==> i' IN I ==> bound_name_instr i = bound_name_instr i' ==> i = i') ==> + !t t' v. t NOTIN FDOM s ==> + str_act (State_st I (s |+ (t,v)) C Fs) t' SUBSET str_act (State_st I s C Fs) t' +Proof + rw [SUBSET_DEF] >> METIS_TAC [fupdate_in_str_act] +QED + +(* Lemma 10, part 2 *) +Theorem str_may_union_I_eq: + !I s C Fs I' C' Fs' t. + t IN bound_names_program I ==> + (!t'. t' IN bound_names_program I' ==> t < t') ==> + str_may (State_st I s C Fs) t = str_may (State_st (I UNION I') s C' Fs') t +Proof + rw [] >> fs [str_may] >> rw [EXTENSION] >> fs [] >> + EQ_TAC >- METIS_TAC [addr_of_union_I_eq] >> + sg `t NOTIN bound_names_program I''` >- + (`t IN bound_names_program I'' ==> F` suffices_by METIS_TAC [] >> STRIP_TAC >> + `t < t` by METIS_TAC [] >> fs []) >> + rw [] >> fs [] >> TRY(METIS_TAC [instr_in_bound_names_program,addr_of_union_I_eq]) >> + `t' IN bound_names_program I''` by METIS_TAC [instr_in_bound_names_program] >> + `t < t'` by METIS_TAC [] >> fs [] +QED + +(* Lemma 10, part 3 *) +Theorem str_may_funion_s_eq: + !I s C Fs s' t. t IN bound_names_program I ==> + (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> + (!t'. t' IN FDOM s' ==> t' >= t) ==> + str_may (State_st I s C Fs) t = str_may (State_st I (FUNION s s') C Fs) t +Proof + rw [] >> fs [str_may] >> rw [EXTENSION] >> fs [] >> EQ_TAC >- + (rw [] >> fs [] >| [ + `sem_expr c' (FUNION s s') = SOME v` by rw [sem_expr_funion] >> + rw [FLOOKUP_FUNION], + + `sem_expr c' (FUNION s s') = SOME v` by rw [sem_expr_funion] >> + METIS_TAC [store_in_flookup_eq], + + `sem_expr c' (FUNION s s') = SOME v` by rw [sem_expr_funion] >> + rw [store_in_flookup_eq] >> + `FLOOKUP s ta = FLOOKUP (FUNION s s') ta` suffices_by METIS_TAC [] >> + `(?c. i_assign t c (o_load r ta) IN I') \/ + (?c tv. i_assign t c (o_store r ta tv) IN I')` + by METIS_TAC [addr_of_some_exist_load_or_store] >- + METIS_TAC [load_t_in_flookup_eq] >> + METIS_TAC [store_t_in_flookup_eq], + + rw [FLOOKUP_FUNION] >> METIS_TAC [store_in_sem_expr_eq], + + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> METIS_TAC [store_in_flookup_eq], + + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> + `FLOOKUP s ta = FLOOKUP (FUNION s s') ta` suffices_by METIS_TAC [] >> + `(?c. i_assign t c (o_load r ta) IN I') \/ + (?c tv. i_assign t c (o_store r ta tv) IN I')` + by METIS_TAC [addr_of_some_exist_load_or_store] >- + METIS_TAC [load_t_in_flookup_eq] >> + METIS_TAC [store_t_in_flookup_eq] + ]) >> + rw [] >> fs [] >| [ + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> + `FLOOKUP s ta' = SOME v'` by METIS_TAC [store_in_flookup_eq] >> + `FLOOKUP s ta = SOME v'` suffices_by METIS_TAC [] >> + `(?c. i_assign t c (o_load r ta) IN I') \/ + (?c tv. i_assign t c (o_store r ta tv) IN I')` + by METIS_TAC [addr_of_some_exist_load_or_store] >- + METIS_TAC [load_t_in_flookup_eq] >> + METIS_TAC [store_t_in_flookup_eq], + + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> + fs [FLOOKUP_FUNION] >> + Cases_on `FLOOKUP s ta'` >> fs [] >> Cases_on `FLOOKUP s ta` >> fs [], + + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> + fs [FLOOKUP_FUNION] >> Cases_on `FLOOKUP s ta` >> fs [], + + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> + `FLOOKUP s ta' = SOME v` by METIS_TAC [store_in_flookup_eq] >> + `FLOOKUP s ta = SOME v` suffices_by METIS_TAC [] >> + `(?c. i_assign t c (o_load r ta) IN I') \/ + (?c tv. i_assign t c (o_store r ta tv) IN I')` + by METIS_TAC [addr_of_some_exist_load_or_store] >- + METIS_TAC [load_t_in_flookup_eq] >> + METIS_TAC [store_t_in_flookup_eq], + + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> + METIS_TAC [store_in_flookup_eq], + + rw [] >- METIS_TAC [store_in_sem_expr_eq] >> + `FLOOKUP s ta = NONE` suffices_by METIS_TAC [] >> + `(?c. i_assign t c (o_load r ta) IN I') \/ + (?c tv. i_assign t c (o_store r ta tv) IN I')` + by METIS_TAC [addr_of_some_exist_load_or_store] >- + METIS_TAC [load_t_in_flookup_eq] >> + METIS_TAC [store_t_in_flookup_eq] + ] +QED + +(* Lemma 10, part 4 *) +Theorem str_may_union_eq: + !I s C Fs I' s' C' Fs' t. + t IN bound_names_program I ==> + (!t'. t' IN bound_names_program I' ==> t < t') ==> + (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> + (!t'. t' IN FDOM s' ==> t' >= t) ==> + str_may (State_st I s C Fs) t = str_may (State_st (I UNION I') (FUNION s s') C' Fs') t +Proof + rw [] >> + `str_may (State_st I' s C Fs) t = str_may (State_st I' s C' Fs') t` + by rw [str_may_unaffected_C_F] >> + `str_may (State_st I' s C' Fs') t = + str_may (State_st I' (FUNION s s') C' Fs') t` + by rw [str_may_funion_s_eq] >> + `str_may (State_st I' (FUNION s s') C' Fs') t = + str_may (State_st (I' UNION I'') (FUNION s s') C' Fs') t` + by rw [str_may_union_I_eq] >> + METIS_TAC [] +QED + +(* Lemma 10, part 6 *) +Theorem str_act_union_I_eq: + !I s C Fs I' C' Fs' t. + t IN bound_names_program I ==> + (!t'. t' IN bound_names_program I' ==> t < t') ==> + str_act (State_st I s C Fs) t = str_act (State_st (I UNION I') s C' Fs') t +Proof + rw [] >> fs [str_act] >> rw [EXTENSION] >> + fs [] >> EQ_TAC >> rw [] >| [ + METIS_TAC [str_may_union_I_eq], + METIS_TAC [addr_of_union_I_eq,str_may_union_I_eq], + METIS_TAC [str_may_union_I_eq], + METIS_TAC [addr_of_union_I_eq,str_may_union_I_eq] + ] +QED + +(* Lemma 10, part 7 *) +Theorem str_act_funion_s_eq: + !I s C Fs s' t. + t IN bound_names_program I ==> + (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> + (!t'. t' IN FDOM s' ==> t' >= t) ==> + str_act (State_st I s C Fs) t = str_act (State_st I (FUNION s s') C Fs) t +Proof + rw [] >> fs [str_act] >> rw [EXTENSION] >> fs [] >> EQ_TAC >> rw [] >| [ + METIS_TAC [str_may_funion_s_eq], + + rw [] >> + Cases_on `i'' IN str_may (State_st I' (FUNION s s') C Fs) t` >> rw [] >> + `i_assign t'' c'' (o_store r ta'' tv'') IN I'` by fs [str_may] >> + Cases_on `t'' > t'` >> rw [] >> + `i_assign t' c' (o_store r ta' tv') IN I'` by fs [str_may] >> + `i_assign t'' c'' (o_store r ta'' tv'') IN str_may (State_st I' s C Fs) t` + by METIS_TAC [str_may_funion_s_eq] >> + `t' < t''` by DECIDE_TAC >> + `t'' < t` by fs [str_may] >> + `(!v. sem_expr c'' s <> SOME v \/ v = val_false) \/ + (!v. FLOOKUP s ta'' <> SOME v \/ FLOOKUP s ta <> SOME v) /\ + !v. FLOOKUP s ta'' <> SOME v \/ FLOOKUP s ta' <> SOME v` + by METIS_TAC [] >- METIS_TAC [store_in_sem_expr_eq] >> + `t' < t` by fs [str_may] >> + `FLOOKUP (FUNION s s') ta'' = FLOOKUP s ta''` + by METIS_TAC [store_in_flookup_eq] >> + `FLOOKUP (FUNION s s') ta' = FLOOKUP s ta'` + by METIS_TAC [store_in_flookup_eq] >> + `FLOOKUP (FUNION s s') ta = FLOOKUP s ta` + suffices_by METIS_TAC [] >> + `(?c. i_assign t c (o_load r ta) IN I') \/ + (?c tv. i_assign t c (o_store r ta tv) IN I')` + by METIS_TAC [addr_of_some_exist_load_or_store] >- + METIS_TAC [load_t_in_flookup_eq] >> + METIS_TAC [store_t_in_flookup_eq], + + METIS_TAC [str_may_funion_s_eq], + + rw [] >> + `i_assign t' c' (o_store r ta' tv') IN I'` by fs [str_may] >> + `i_assign t' c' (o_store r ta' tv') IN str_may (State_st I' s C Fs) t` + by METIS_TAC [str_may_funion_s_eq] >> + `t' < t` by fs [str_may] >> + Cases_on `i'' IN str_may (State_st I' s C Fs) t` >> rw [] >> + `i_assign t'' c'' (o_store r ta'' tv'') IN I'` by fs [str_may] >> + `t'' < t` by fs [str_may] >> + Cases_on `t'' > t'` >> rw [] >> + `i_assign t'' c'' (o_store r ta'' tv'') IN str_may (State_st I' (FUNION s s') C Fs) t` + by METIS_TAC [str_may_funion_s_eq] >> + `(!v. sem_expr c'' (FUNION s s') <> SOME v \/ v = val_false) \/ + (!v. FLOOKUP (FUNION s s') ta'' <> SOME v \/ + FLOOKUP (FUNION s s') ta <> SOME v) /\ + !v. FLOOKUP (FUNION s s') ta'' <> SOME v \/ + FLOOKUP (FUNION s s') ta' <> SOME v` + by METIS_TAC [] >- METIS_TAC [store_in_sem_expr_eq] >> + `FLOOKUP (FUNION s s') ta'' = FLOOKUP s ta''` + by METIS_TAC [store_in_flookup_eq] >> + `FLOOKUP (FUNION s s') ta' = FLOOKUP s ta'` + by METIS_TAC [store_in_flookup_eq] >> + `FLOOKUP (FUNION s s') ta = FLOOKUP s ta` + suffices_by METIS_TAC [] >> + `(?c. i_assign t c (o_load r ta) IN I') \/ + (?c tv. i_assign t c (o_store r ta tv) IN I')` + by METIS_TAC [addr_of_some_exist_load_or_store] >- + METIS_TAC [load_t_in_flookup_eq] >> + METIS_TAC [store_t_in_flookup_eq] +] +QED + +(* Lemma 10, part 8 *) +Theorem str_act_union_eq: + !I s C Fs I' s' C' Fs' t. + t IN bound_names_program I ==> + (!t'. t' IN bound_names_program I' ==> t < t') ==> + (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> + (!t'. t' IN FDOM s' ==> t' >= t) ==> + str_act (State_st I s C Fs) t = + str_act (State_st (I UNION I') (FUNION s s') C' Fs') t +Proof + rw [] >> + `str_act (State_st I' s C Fs) t = str_act (State_st I' s C' Fs') t` + by rw [str_act_unaffected_C_F] >> + `str_act (State_st I' s C' Fs') t = str_act (State_st I' (FUNION s s') C' Fs') t` + by rw [str_act_funion_s_eq] >> + `str_act (State_st I' (FUNION s s') C' Fs') t = + str_act (State_st (I' UNION I'') (FUNION s s') C' Fs') t` + by rw [str_act_union_I_eq] >> + METIS_TAC [] +QED + +(* Lemma 10 *) +Theorem str_may_act_union_eq: + !I s C Fs I' s' C' Fs' t. + t IN bound_names_program I ==> + (!t'. t' IN bound_names_program I' ==> t < t') ==> + (!i. i IN I ==> !t'. t' IN free_names_instr i ==> t' < bound_name_instr i) ==> + (!t'. t' IN FDOM s' ==> t' >= t) ==> + str_may (State_st I s C Fs) t = + str_may (State_st (I UNION I') (FUNION s s') C' Fs') t /\ + str_act (State_st I s C Fs) t = + str_act (State_st (I UNION I') (FUNION s s') C' Fs') t +Proof + METIS_TAC [ + str_may_union_eq, + str_act_union_eq + ] +QED + +Theorem union_translate_val_subset_str_may: + !I' s C C' Fs Fs'. FINITE I' ==> + !t t' v. t IN bound_names_program I' ==> + str_may (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C' Fs') t + SUBSET str_may (State_st I' s C Fs) t +Proof + rw [] >> + `str_may (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C' Fs') t = + str_may (State_st I' s C Fs) t` + suffices_by METIS_TAC [SUBSET_REFL] >> + `str_may (State_st I' s C Fs) t = + str_may (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C' Fs') t` + suffices_by METIS_TAC [str_may_unaffected_C_F] >> + `!t'. t' IN bound_names_program (translate_val v (MAX_SET (bound_names_program I'))) ==> t < t'` + suffices_by METIS_TAC [str_may_union_I_eq] >> + rw [] >> + `?c' mop. i_assign t c' mop IN I'` + by METIS_TAC [bound_names_program_in_instr] >> + `?c'' mop'. i_assign t' c'' mop' IN translate_val v (MAX_SET (bound_names_program I'))` + by METIS_TAC [bound_names_program_in_instr] >> + METIS_TAC [translate_val_max_name_lt_i_assign] +QED + +Theorem union_translate_val_subset_str_act: + !I' s C C' Fs Fs'. FINITE I' ==> + !t t' v. t IN bound_names_program I' ==> + str_act (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C' Fs') t + SUBSET str_act (State_st I' s C Fs) t +Proof + rw [] >> + `str_act (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C' Fs') t = + str_act (State_st I' s C Fs) t` + suffices_by METIS_TAC [SUBSET_DEF,SUBSET_REFL] >> + `str_act (State_st I' s C Fs) t = + str_act (State_st (I' UNION translate_val v (MAX_SET (bound_names_program I'))) s C' Fs') t` + suffices_by METIS_TAC [str_act_unaffected_C_F] >> + `!t'. t' IN bound_names_program (translate_val v (MAX_SET (bound_names_program I'))) ==> t < t'` + suffices_by METIS_TAC [str_act_union_I_eq] >> rw [] >> + `?c' mop. i_assign t c' mop IN I'` + by METIS_TAC [bound_names_program_in_instr] >> + `?c'' mop'. i_assign t' c'' mop' IN translate_val v (MAX_SET (bound_names_program I'))` + by METIS_TAC [bound_names_program_in_instr] >> + METIS_TAC [translate_val_max_name_lt_i_assign] +QED + (* --------- *) (* sem_instr *) (* --------- *)