From 40742f24bcf9d820e3daf03dd65a1d9de3b42287 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 16 May 2018 12:17:41 +0200 Subject: [PATCH] Update CF for fun sem in translator and remove some cheats --- characteristic/Holmakefile | 8 +- characteristic/cfAppScript.sml | 124 ++++++++--------------- characteristic/cfMainScript.sml | 170 +++++++++++++------------------- characteristic/cfScript.sml | 36 +++---- 4 files changed, 129 insertions(+), 209 deletions(-) diff --git a/characteristic/Holmakefile b/characteristic/Holmakefile index eefed0e0a7..0c86ab0173 100644 --- a/characteristic/Holmakefile +++ b/characteristic/Holmakefile @@ -1,4 +1,4 @@ -INCLUDES = ../misc ../semantics ../semantics/alt_semantics/proofs ../basis/pure ../translator $(HOLDIR)/examples/machine-code/hoare-triple ../compiler/parsing +INCLUDES = ../misc ../semantics ../basis/pure ../translator $(HOLDIR)/examples/machine-code/hoare-triple ../compiler/parsing OPTIONS = QUIT_ON_FAILURE ifdef POLY @@ -15,13 +15,11 @@ all: $(TARGETS) $(HOLHEAP) .PHONY: all PRE_BARE_THYS1 = astTheory tokensTheory semanticPrimitivesTheory astPP -PRE_BARE_THYS3 = determTheory bigClockTheory BARE_THYS1 = $(patsubst %,../semantics/%,$(PRE_BARE_THYS1)) -BARE_THYS3 = $(patsubst %,../semantics/alt_semantics/proofs/%,$(PRE_BARE_THYS3)) -DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(patsubst %,%.uo,$(BARE_THYS3)) $(PARENTHEAP) +DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP) $(HOLHEAP): $(DEPS) - $(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS1) $(BARE_THYS3) $(BARE_THYS2) + $(protect $(HOLDIR)/bin/buildheap) -b $(PARENT_HOLHEAP) -o $(HOLHEAP) $(BARE_THYS1) endif diff --git a/characteristic/cfAppScript.sml b/characteristic/cfAppScript.sml index 6937544d93..cc98925c14 100644 --- a/characteristic/cfAppScript.sml +++ b/characteristic/cfAppScript.sml @@ -229,22 +229,7 @@ val app_basic_weaken = Q.store_thm("app_basic_weaken", app_basic p v v1 x Q)`, fs [app_basic_def] \\ metis_tac []); -val evaluate_list_SING = Q.prove( - `bigStep$evaluate_list b env st [exp] (st', Rval [v]) <=> - bigStep$evaluate b env st exp (st', Rval v)`, - simp [Once bigStepTheory.evaluate_cases, PULL_EXISTS] - \\ once_rewrite_tac [CONJ_COMM] - \\ simp [Once bigStepTheory.evaluate_cases, PULL_EXISTS]); - -val evaluate_list_raise_SING = Q.prove( - `bigStep$evaluate_list b env st [exp] (st', Rerr (Rraise v)) <=> - bigStep$evaluate b env st exp (st', Rerr (Rraise v))`, - simp [Once bigStepTheory.evaluate_cases, PULL_EXISTS] - \\ eq_tac \\ fs [] \\ strip_tac - \\ pop_assum (assume_tac o - SIMP_RULE std_ss [Once bigStepTheory.evaluate_cases]) - \\ fs []); - +(* val app_basic_rel = Q.store_thm("app_basic_rel", `app_basic (p:'ffi ffi_proj) (f: v) (x: v) (H: hprop) (Q: res -> hprop) = !(h_i: heap) (h_k: heap) (st: 'ffi state). @@ -275,6 +260,7 @@ val app_basic_rel = Q.store_thm("app_basic_rel", (rewrite_tac [CONJ_ASSOC] \\ once_rewrite_tac [CONJ_COMM] \\ asm_exists_tac \\ fs [] \\ fs [st2heap_def] \\ asm_exists_tac \\ fs [])); +*) (* TODO: move to appropriate locations *) @@ -329,21 +315,6 @@ open terminationTheory evaluatePropsTheory val dec_clock_def = evaluateTheory.dec_clock_def val evaluate_empty_state_IMP = ml_translatorTheory.evaluate_empty_state_IMP -val big_remove_clock = Q.store_thm("big_remove_clock", - `∀c ck env s e s' r. - evaluate ck env s e (s',r) ∧ - r ≠ Rerr (Rabort Rtimeout_error) - ⇒ - evaluate F env (s with clock := c) e (s' with clock := c,r)`, - gen_tac \\ reverse Cases - >- ( - rw[] \\ - imp_res_tac bigClockTheory.big_unclocked \\ - `∀s. s = s with clock := s.clock` by simp[state_component_equality] \\ - metis_tac[bigClockTheory.big_unclocked] ) \\ - rw[bigClockTheory.big_clocked_unclocked_equiv] \\ - metis_tac[bigClockTheory.clocked_min_counter]); - val evaluate_refs_length_mono = Q.store_thm("evaluate_refs_length_mono",` (∀(s:'a state) env e s' r. evaluate s env e = (s',r) ⇒ LENGTH s.refs ≤ LENGTH s'.refs) ∧ @@ -357,14 +328,6 @@ val evaluate_refs_length_mono = Q.store_thm("evaluate_refs_length_mono",` \\ fs[semanticPrimitivesTheory.store_alloc_def,semanticPrimitivesTheory.store_assign_def] \\ rw[]); -val big_refs_length_mono = Q.store_thm("big_refs_length_mono", - `evaluate ck env s exp (s',r) ⇒ LENGTH s.refs ≤ LENGTH s'.refs`, - Cases_on`ck` - \\ rw[funBigStepEquivTheory.functional_evaluate] - \\ fs[bigClockTheory.big_clocked_unclocked_equiv,funBigStepEquivTheory.functional_evaluate] - \\ imp_res_tac evaluate_refs_length_mono - \\ fs[]); - val SPLIT_st2heap_length_leq = Q.store_thm("SPLIT_st2heap_length_leq", `SPLIT (st2heap p s') (st2heap p s, h_g) ∧ LENGTH s.refs ≤ LENGTH s'.refs ∧ s'.ffi = s.ffi ⇒ @@ -548,6 +511,7 @@ val SPLIT_st2heap_ffi = Q.store_thm("SPLIT_st2heap_ffi", \\ match_mp_tac FILTER_ffi_has_index_in_MEM \\ fs [] \\ asm_exists_tac \\ fs []) +(* val SPLIT_st2heap_evaluate_ffi_same = Q.store_thm("SPLIT_st2heap_evaluate_ffi_same", `evaluate F env st exp (st',Rval res) ∧ SPLIT (st2heap p st') (st2heap p st, h_g) ⇒ @@ -561,26 +525,7 @@ val SPLIT_st2heap_evaluate_ffi_same = Q.store_thm("SPLIT_st2heap_evaluate_ffi_sa \\ `LENGTH st.ffi.io_events = LENGTH st'.ffi.io_events` by metis_tac [LENGTH_FILTER_EQ_IMP_LENGTH_EQ] \\ metis_tac [IS_PREFIX_LENGTH_ANTI]); - -val evaluate_imp_evaluate_empty_state = Q.store_thm("evaluate_imp_evaluate_empty_state", - `evaluate F env s es (s',Rval r) ∧ s.refs ≼ s'.refs ∧ s'.ffi = s.ffi ∧ s.ffi.final_event = NONE ∧ - t = empty_state with <| refs := s.refs |> ∧ - t' = empty_state with <| refs := s'.refs |> - ⇒ - evaluate F env t es (t',Rval r)`, - rw[Once bigClockTheory.big_clocked_unclocked_equiv] - \\ fs[funBigStepEquivTheory.functional_evaluate] - \\ drule (REWRITE_RULE[GSYM AND_IMP_INTRO]( - INST_TYPE[beta|->oneSyntax.one_ty]( - CONJUNCT1 evaluate_ffi_intro))) - \\ simp[] - \\ disch_then(qspec_then`empty_state with <| clock := c; refs := s.refs |>`mp_tac) - \\ simp[] \\ strip_tac - \\ `Rval [r] = list_result ((Rval r):(v,v) result)` by EVAL_TAC - \\ pop_assum SUBST_ALL_TAC - \\ fs[GSYM funBigStepEquivTheory.functional_evaluate] - \\ simp[bigClockTheory.big_clocked_unclocked_equiv] - \\ asm_exists_tac \\ fs[]); +*) val Arrow_IMP_app_basic = Q.store_thm("Arrow_IMP_app_basic", `(Arrow a b) f v ==> @@ -589,16 +534,13 @@ val Arrow_IMP_app_basic = Q.store_thm("Arrow_IMP_app_basic", app_basic (p:'ffi ffi_proj) v v1 emp (POSTv v. &b (f x) v)`, fs [app_basic_def,emp_def,cfHeapsBaseTheory.SPLIT_emp1, ml_translatorTheory.Arrow_def,ml_translatorTheory.AppReturns_def,PULL_EXISTS] - \\ fs [evaluate_ck_def, funBigStepEquivTheory.functional_evaluate_list] - \\ rw [] + \\ fs [evaluate_ck_def] \\ rw [] \\ first_x_assum drule \\ strip_tac \\ first_x_assum (qspec_then`st.refs`strip_assume_tac) \\ instantiate - \\ simp [Once bigStepTheory.evaluate_cases, PULL_EXISTS] - \\ simp [Once (CONJUNCT2 bigStepTheory.evaluate_cases)] \\ drule evaluate_empty_state_IMP \\ strip_tac - \\ fs [bigClockTheory.big_clocked_unclocked_equiv] - \\ rename1 `evaluate _ _ (st with clock := ck) _ _` + \\ fs [ml_progTheory.eval_rel_def] + \\ rename1 `evaluate (st with clock := ck) _ _ = _` \\ simp[POSTv_cond,PULL_EXISTS] \\ instantiate \\ fs[st2heap_clock] @@ -619,25 +561,39 @@ val Arrow_IMP_app_basic = Q.store_thm("Arrow_IMP_app_basic", \\ decide_tac); val app_basic_IMP_Arrow = Q.store_thm("app_basic_IMP_Arrow", - `(∀x v1. a x v1 ⇒ app_basic p v v1 emp (POSTv v. cond (b (f x) v))) ⇒ Arrow a b f v`, - rw[app_basic_def,ml_translatorTheory.Arrow_def,ml_translatorTheory.AppReturns_def,emp_def,SPLIT_emp1] \\ - first_x_assum drule \\ - fs[evaluate_ck_def,funBigStepEquivTheory.functional_evaluate_list] \\ - fs[POSTv_cond,SPLIT3_emp1,PULL_EXISTS] \\ - disch_then( qspec_then`ARB with <| refs := refs; ffi := <| final_event := NONE |> |>` mp_tac) \\ - rw[] \\ instantiate \\ - fs[Once (CONJUNCT2 bigStepTheory.evaluate_cases)] \\ - fs[Once (CONJUNCT2 bigStepTheory.evaluate_cases)] \\ rw[] \\ - drule big_remove_clock \\ rw[] \\ - first_x_assum(qspec_then`0`strip_assume_tac) \\ - drule SPLIT_st2heap_evaluate_ffi_same \\ - fs[st2heap_clock] \\ strip_tac \\ - drule SPLIT_st2heap_length_leq \\ simp[] \\ - imp_res_tac big_refs_length_mono \\ fs[] \\ - rw[IS_PREFIX_APPEND] \\ - qexists_tac`l` \\ - match_mp_tac (INST_TYPE[alpha|->beta](GEN_ALL evaluate_imp_evaluate_empty_state)) \\ - instantiate); + `(∀x v1. a x v1 ⇒ app_basic p v v1 emp (POSTv v. cond (b (f x) v))) ⇒ + Arrow a b f v`, + rw[app_basic_def,ml_translatorTheory.Arrow_def, + ml_translatorTheory.AppReturns_def,emp_def,SPLIT_emp1] + \\ first_x_assum drule + \\ fs[evaluate_ck_def] + \\ fs[POSTv_cond,SPLIT3_emp1,PULL_EXISTS] + \\ disch_then( qspec_then`ARB with + <| refs := refs; ffi := <| final_event := NONE |> |>` mp_tac) + \\ rw [] \\ instantiate + \\ rename1 `SPLIT (st2heap p st1) _` + \\ drule (CONJUNCT1 evaluate_ffi_intro |> INST_TYPE [beta|->``:unit``]) \\ fs [] + \\ disch_then (qspec_then + `empty_state with <| clock := ck ;refs := refs |>` mp_tac) \\ fs [] + \\ qsuff_tac `?refs1. st1.refs = refs ++ refs1 /\ + st1.ffi = <|final_event := NONE|>` + THEN1 + (fs [ml_progTheory.eval_rel_def] \\ rw [] + \\ qexists_tac `refs1` + \\ qexists_tac `ck` \\ fs [state_component_equality]) + \\ imp_res_tac evaluate_refs_length_mono \\ fs [] + \\ imp_res_tac evaluate_io_events_mono_imp + \\ fs[io_events_mono_def] + \\ simp [GSYM PULL_EXISTS] + \\ conj_asm2_tac + THEN1 (drule SPLIT_st2heap_length_leq \\ fs [IS_PREFIX_APPEND]) + \\ imp_res_tac SPLIT_st2heap_ffi \\ fs [] + \\ Cases_on`st1.ffi.final_event` \\ fs[] \\ rfs [] + \\ qmatch_assum_rename_tac `!n. FILTER (ffi_has_index_in [n]) _ = + FILTER (ffi_has_index_in [n]) st2.io_events` + \\ `LENGTH st1.ffi.io_events = LENGTH st2.io_events` + by metis_tac [LENGTH_FILTER_EQ_IMP_LENGTH_EQ] + \\ metis_tac [IS_PREFIX_LENGTH_ANTI]); val Arrow_eq_app_basic = Q.store_thm("Arrow_eq_app_basic", `Arrow a b f fv ⇔ (∀x xv. a x xv ⇒ app_basic p fv xv emp (POSTv v'. &b (f x) v'))`, diff --git a/characteristic/cfMainScript.sml b/characteristic/cfMainScript.sml index 0d3a2872cf..2fc9080bd5 100644 --- a/characteristic/cfMainScript.sml +++ b/characteristic/cfMainScript.sml @@ -2,14 +2,18 @@ open preamble semanticPrimitivesTheory ml_translatorTheory ml_translatorLib ml_progLib cfHeapsTheory cfTheory cfTacticsBaseLib cfTacticsLib - semanticsLib + semanticsLib evaluatePropsTheory val _ = new_theory "cfMain"; -(*The following section culminates in call_main_thm2 which takes a spec and some aspects - of the current state, and proves a Semantics_prog statement. It also proves call_FFI_rel^* - between the initial state, and the state after creating the prog and then calling the main - function - this is useful for theorizing about the output of the program *) +(* + The following section culminates in call_main_thm2 which takes a + spec and some aspects of the current state, and proves a + Semantics_prog statement. It also proves call_FFI_rel^* between the + initial state, and the state after creating the prog and then + calling the main function - this is useful for theorizing about the + output of the program +*) fun mk_main_call s = (* TODO: don't use the parser so much here? *) @@ -23,101 +27,60 @@ val call_main_thm1 = Q.store_thm("call_main_thm1", app p fv [Conv NONE []] P (POSTv uv. &UNIT_TYPE () uv * Q) ==> (* this should be the CF spec you prove for the "main" function *) SPLIT (st2heap p st2) (h1,h2) /\ P h1 ==> (* this might need simplification, but some of it may need to stay on the final theorem *) ∃st3. - Decls env1 st1 (SNOC ^main_call prog) env2 st3 /\ - (?h3 h4. SPLIT3 (st2heap p st3) (h3,h2,h4) /\ Q h3)`, + Decls env1 st1 (SNOC ^main_call prog) env2 st3 /\ + (?h3 h4. SPLIT3 (st2heap p st3) (h3,h2,h4) /\ Q h3)`, rw[ml_progTheory.ML_code_def,SNOC_APPEND,ml_progTheory.Decls_APPEND,PULL_EXISTS] - \\ asm_exists_tac \\ fs[] \\ simp[ml_progTheory.Decls_def] - \\ ONCE_REWRITE_TAC [bigStepTheory.evaluate_dec_cases] \\ SIMP_TAC (srw_ss()) [] - \\ ONCE_REWRITE_TAC [bigStepTheory.evaluate_dec_cases |> CONJUNCT2] \\ SIMP_TAC (srw_ss()) [] - \\ FULL_SIMP_TAC (srw_ss()) [astTheory.pat_bindings_def,ALL_DISTINCT,MEM, - pmatch_def, Once bigStepTheory.evaluate_dec_cases,combine_dec_result_def] - \\ fs[PULL_EXISTS] - \\ fs[app_def,app_basic_def] - \\ first_x_assum drule \\ rw[] - \\ rw[Once bigStepTheory.evaluate_cases] - \\ rw[Once bigStepTheory.evaluate_cases] - \\ rw[Once bigStepTheory.evaluate_cases] - \\ rw[Once bigStepTheory.evaluate_cases] - \\ rw[Once bigStepTheory.evaluate_cases] - \\ rw[Once bigStepTheory.evaluate_cases] - \\ rw[Once bigStepTheory.evaluate_cases] - \\ rw[PULL_EXISTS] - \\ CONV_TAC(STRIP_QUANT_CONV(LAND_CONV (LAND_CONV EVAL))) \\ simp[] - \\ CONV_TAC(STRIP_QUANT_CONV(LAND_CONV (LAND_CONV EVAL))) \\ simp[] - \\ CONV_TAC(STRIP_QUANT_CONV(LAND_CONV (LAND_CONV EVAL))) \\ simp[] - \\ fs[ml_progTheory.lookup_var_def,ALOOKUP_APPEND] - \\ reverse every_case_tac >- fs[cond_def] \\ fs[] - \\ fs[evaluate_ck_def,funBigStepEquivTheory.functional_evaluate_list] - \\ fs[Once (CONJUNCT2 bigStepTheory.evaluate_cases)] - \\ fs[Once (CONJUNCT2 bigStepTheory.evaluate_cases)] - \\ imp_res_tac cfAppTheory.big_remove_clock \\ fs[] - \\ first_x_assum(qspec_then`st2.clock`mp_tac) - \\ simp[semanticPrimitivesPropsTheory.with_same_clock] - \\ strip_tac - \\ simp[build_conv_def,do_con_check_def,ml_progTheory.nsLookup_merge_env] - \\ asm_exists_tac \\ simp[] - \\ fs[STAR_def,cond_def,UNIT_TYPE_def] - \\ CONV_TAC(STRIP_QUANT_CONV(LAND_CONV (LAND_CONV EVAL))) \\ simp[] - \\ srw_tac[QI_ss][ml_progTheory.merge_env_def,sem_env_component_equality,cfStoreTheory.st2heap_clock] - \\ asm_exists_tac \\ fs[cfHeapsBaseTheory.SPLIT_emp1] \\ rw[] -); - -val evaluate_prog_RTC_call_FFI_rel = Q.store_thm("evaluate_prog_RTC_call_FFI_rel", - `evaluate_decs F env st prog (st',res) ==> - RTC call_FFI_rel st.ffi st'.ffi`, - cheat (* - rw[bigClockTheory.dec_clocked_unclocked_equiv] - \\ (funBigStepEquivTheory.functional_evaluate_tops - |> CONV_RULE(LAND_CONV SYM_CONV) |> LET_INTRO - |> Q.GENL[`env`,`s`,`tops`] - |> qspecl_then[`env`,`st with clock := c`,`prog`]mp_tac) - \\ rw[] \\ pairarg_tac \\ fs[] - \\ drule evaluatePropsTheory.evaluate_tops_call_FFI_rel_imp - \\ imp_res_tac determTheory.prog_determ - \\ fs[] \\ rw[] *)); - -(* -val evaluate_prog_rel_IMP_evaluate_prog_fun = Q.store_thm( - "evaluate_prog_rel_IMP_evaluate_prog_fun", - `bigStep$evaluate_whole_prog F env st prog (st',Rval r) ==> - ?k. evaluate$evaluate_prog (st with clock := k) env prog = - (st',Rval r)`, - rw[bigClockTheory.prog_clocked_unclocked_equiv,bigStepTheory.evaluate_whole_prog_def] - \\ qexists_tac`c + st.clock` - \\ (funBigStepEquivTheory.functional_evaluate_prog - |> CONV_RULE(LAND_CONV SYM_CONV) |> LET_INTRO |> GEN_ALL - |> CONV_RULE(RESORT_FORALL_CONV(sort_vars["s","env","prog"])) - |> qspecl_then[`st with clock := c + st.clock`,`env`,`prog`]mp_tac) - \\ rw[] \\ pairarg_tac \\ fs[] - \\ fs[bigStepTheory.evaluate_whole_prog_def] - \\ drule bigClockTheory.prog_add_to_counter \\ simp[] - \\ disch_then(qspec_then`st.clock`strip_assume_tac) - \\ drule determTheory.prog_determ - \\ every_case_tac \\ fs[] - \\ TRY (disch_then drule \\ rw[]) - \\ fs[semanticPrimitivesTheory.state_component_equality]); -*) + \\ fs [terminationTheory.evaluate_decs_def,PULL_EXISTS, + EVAL ``(pat_bindings (Pcon NONE []) [])``,pair_case_eq,result_case_eq] + \\ fs [terminationTheory.evaluate_def,PULL_EXISTS,pair_case_eq, + result_case_eq,do_con_check_def,build_conv_def,bool_case_eq, + ml_progTheory.lookup_var_def,option_case_eq,match_result_case_eq, + EVAL ``nsLookup (merge_env env2 env1).v (Short fname)``,app_def, + app_basic_def] + \\ first_x_assum drule \\ fs [] \\ strip_tac \\ fs [] + \\ fs [cfHeapsBaseTheory.POSTv_def] + \\ Cases_on `r` \\ fs [cond_STAR] \\ fs [cond_def] + \\ fs [UNIT_TYPE_def] \\ rveq \\ fs [] + \\ fs [ml_progTheory.Decls_def,evaluate_ck_def] + \\ drule evaluate_add_to_clock + \\ disch_then (qspec_then `ck2` mp_tac) \\ simp [] + \\ qpat_x_assum `_ env1 prog = _` assume_tac + \\ drule evaluate_decs_add_to_clock + \\ disch_then (qspec_then `ck` mp_tac) \\ simp [] + \\ rpt strip_tac + \\ once_rewrite_tac [CONJ_COMM] + \\ `evaluate_decs (st1 with clock := ck + ck1) env1 prog = + (st2 with clock := ck + ck2,Rval env2)` by fs [] + \\ asm_exists_tac \\ fs [] + \\ once_rewrite_tac [CONJ_COMM] \\ rewrite_tac [GSYM CONJ_ASSOC] + \\ once_rewrite_tac [CONJ_COMM] \\ rewrite_tac [GSYM CONJ_ASSOC] + \\ once_rewrite_tac [EQ_SYM_EQ] \\ fs [evaluateTheory.dec_clock_def] + \\ `evaluate (st2 with clock := (ck + ck2 + 1) - 1) env [exp] = + ((st' with clock := st2.clock) with clock := ck2 + st'.clock, + Rval [Conv NONE []])` by fs [] + \\ asm_exists_tac \\ fs [terminationTheory.pmatch_def] + \\ fs [ml_progTheory.merge_env_def] + \\ fs [cfStoreTheory.st2heap_clock] + \\ asm_exists_tac \\ fs []); val prog_to_semantics_prog = Q.prove( - `!init_env inp prog st c r env2 s2. - Decls init_env inp prog env2 s2 /\ - s2.ffi.final_event = NONE (*This will comes from FFI_outcomes*) ==> - (semantics_prog inp init_env prog (Terminate Success s2.ffi.io_events))`, - cheat (* - rw[ml_progTheory.Decls_def] \\ - `evaluate_whole_prog F init_env' inp prog (s2,Rval env2)` - by simp[bigStepTheory.evaluate_whole_prog_def] - \\ imp_res_tac evaluate_prog_rel_IMP_evaluate_prog_fun - \\ fs[semanticsTheory.semantics_prog_def,PULL_EXISTS] - \\ fs[semanticsTheory.evaluate_prog_with_clock_def] - \\ qexists_tac `k` \\ fs[] - \\ rw[] \\ pairarg_tac \\ fs[] - \\ pop_assum mp_tac - \\ drule evaluatePropsTheory.evaluate_prog_clock_determ - \\ ntac 2 strip_tac \\ first_x_assum drule - \\ fs[] \\ rpt (CASE_TAC \\ fs[]) *) -); + `!init_env inp prog st c r env2 s2. + Decls init_env inp prog env2 s2 /\ + s2.ffi.final_event = NONE (* This will comes from FFI_outcomes *) ==> + (semantics_prog inp init_env prog (Terminate Success s2.ffi.io_events))`, + rw[ml_progTheory.Decls_def] + \\ fs[semanticsTheory.semantics_prog_def,PULL_EXISTS] + \\ fs[semanticsTheory.evaluate_prog_with_clock_def] + \\ qexists_tac `ck1` \\ fs [] + \\ CCONTR_TAC \\ fs [] + \\ pairarg_tac \\ fs [] \\ rveq + \\ drule evaluate_decs_add_to_clock + \\ disch_then (qspec_then `ck1` mp_tac) + \\ qpat_x_assum `_ = (_,Rval _)` assume_tac + \\ drule evaluate_decs_add_to_clock + \\ disch_then (qspec_then `k` mp_tac) + \\ rpt strip_tac \\ fs []); val FFI_part_hprop_def = Define` FFI_part_hprop Q = @@ -146,10 +109,14 @@ val call_main_thm2 = Q.store_thm("call_main_thm2", call_FFI_rel^* st1.ffi st3.ffi`, rw[] \\ qho_match_abbrev_tac`?st3. A st3 /\ B st3 /\ C st1 st3` - \\ `?st3. Decls env1 st1 (SNOC ^main_call prog) env2 st3 ∧ st3.ffi.final_event = NONE /\ B st3 /\ C st1 st3` - suffices_by metis_tac[prog_to_semantics_prog] - \\ `?st3. Decls env1 st1 (SNOC ^main_call prog) env2 st3 ∧ st3.ffi.final_event = NONE /\ B st3` - suffices_by metis_tac[ml_progTheory.Decls_def, evaluate_prog_RTC_call_FFI_rel] + \\ `?st3. Decls env1 st1 (SNOC ^main_call prog) env2 st3 ∧ + st3.ffi.final_event = NONE /\ B st3 /\ C st1 st3` + suffices_by metis_tac[prog_to_semantics_prog] + \\ reverse (sg `?st3. Decls env1 st1 (SNOC ^main_call prog) env2 st3 ∧ + st3.ffi.final_event = NONE /\ B st3`) + THEN1 (asm_exists_tac \\ fs [Abbr`C`] + \\ fs [ml_progTheory.ML_code_def,ml_progTheory.Decls_def] + \\ imp_res_tac evaluate_decs_call_FFI_rel_imp \\ fs []) \\ simp[Abbr`A`,Abbr`B`] \\ drule (GEN_ALL call_main_thm1) \\ rpt (disch_then drule) @@ -166,7 +133,6 @@ val call_main_thm2 = Q.store_thm("call_main_thm2", \\ first_x_assum drule \\ strip_tac \\ fs[EXTENSION] \\ last_x_assum(qspec_then`FFI_part s u ns us`mp_tac) - \\ simp[FFI_part_NOT_IN_store2heap] -); + \\ simp[FFI_part_NOT_IN_store2heap]); val _ = export_theory() diff --git a/characteristic/cfScript.sml b/characteristic/cfScript.sml index a8574c1f11..f8ebefb3e2 100644 --- a/characteristic/cfScript.sml +++ b/characteristic/cfScript.sml @@ -1303,27 +1303,27 @@ val app_aw8update_def = Define ` Q ==e> POST_F)` val app_copyaw8aw8_def = Define ` - app_copyaw8aw8 s so l d do H Q = + app_copyaw8aw8 s so l d do' H Q = ((?ws wd F. - 0 <= do /\ 0 <= so /\ 0 <= l /\ - (Num do + Num l) <= LENGTH wd /\(Num so + Num l) <= LENGTH ws /\ + 0 <= do' /\ 0 <= so /\ 0 <= l /\ + (Num do' + Num l) <= LENGTH wd /\(Num so + Num l) <= LENGTH ws /\ (H ==>> F * W8ARRAY s ws * W8ARRAY d wd) /\ (F * W8ARRAY s ws * - W8ARRAY d (TAKE (Num do) wd ⧺ + W8ARRAY d (TAKE (Num do') wd ⧺ TAKE (Num l) (DROP (Num so) ws) ⧺ - DROP (Num do + Num l) wd) + DROP (Num do' + Num l) wd) ==>> Q (Val (Conv NONE [])))) /\ Q ==e> POST_F)` val app_copystraw8_def = Define ` - app_copystraw8 s so l d do H Q = + app_copystraw8 s so l d do' H Q = ((?wd F. - 0 <= do /\ 0 <= so /\ 0 <= l /\ - (Num do + Num l) <= LENGTH wd /\(Num so + Num l) <= LENGTH s /\ + 0 <= do' /\ 0 <= so /\ 0 <= l /\ + (Num do' + Num l) <= LENGTH wd /\(Num so + Num l) <= LENGTH s /\ (H ==>> F * W8ARRAY d wd) /\ - (F * W8ARRAY d (TAKE (Num do) wd ⧺ + (F * W8ARRAY d (TAKE (Num do') wd ⧺ MAP (n2w o ORD) (TAKE (Num l) (DROP (Num so) s)) ⧺ - DROP (Num do + Num l) wd) + DROP (Num do' + Num l) wd) ==>> Q (Val (Conv NONE [])))) /\ Q ==e> POST_F)` @@ -1550,23 +1550,23 @@ val cf_aw8update_def = Define ` val cf_copyaw8aw8_def = Define ` cf_copyaw8aw8 xs xso xl xd xdo = \env. local (\H Q. - ?s so l d do. + ?s so l d do'. exp2v env xs = SOME s /\ exp2v env xd = SOME d /\ exp2v env xl = SOME (Litv (IntLit l)) /\ exp2v env xso = SOME (Litv (IntLit so)) /\ - exp2v env xdo = SOME (Litv (IntLit do)) /\ - app_copyaw8aw8 s so l d do H Q)` + exp2v env xdo = SOME (Litv (IntLit do')) /\ + app_copyaw8aw8 s so l d do' H Q)` val cf_copystraw8_def = Define ` cf_copystraw8 xs xso xl xd xdo = \env. local (\H Q. - ?s so l d do. + ?s so l d do'. exp2v env xs = SOME (Litv (StrLit s)) /\ exp2v env xd = SOME d /\ exp2v env xl = SOME (Litv (IntLit l)) /\ exp2v env xso = SOME (Litv (IntLit so)) /\ - exp2v env xdo = SOME (Litv (IntLit do)) /\ - app_copystraw8 s so l d do H Q)` + exp2v env xdo = SOME (Litv (IntLit do')) /\ + app_copystraw8 s so l d do' H Q)` val cf_copyaw8str_def = Define ` cf_copyaw8str xs xso xl = \env. local (\H Q. @@ -1739,11 +1739,11 @@ val cf_def = tDefine "cf" ` | _ => cf_bottom) | CopyAw8Aw8 => (case args of - | [s; so; l; d; do] => cf_copyaw8aw8 s so l d do + | [s; so; l; d; do'] => cf_copyaw8aw8 s so l d do' | _ => cf_bottom) | CopyStrAw8 => (case args of - | [s; so; l; d; do] => cf_copystraw8 s so l d do + | [s; so; l; d; do'] => cf_copystraw8 s so l d do' | _ => cf_bottom) | CopyAw8Str => (case args of