diff --git a/compiler/bootstrap/translation/from_pancake32ProgScript.sml b/compiler/bootstrap/translation/from_pancake32ProgScript.sml index 3d6e76a53a..1dbea6d3c2 100644 --- a/compiler/bootstrap/translation/from_pancake32ProgScript.sml +++ b/compiler/bootstrap/translation/from_pancake32ProgScript.sml @@ -249,6 +249,8 @@ open crep_to_loopTheory; val _ = translate $ spec32 prog_if_def; +val _ = translate $ spec32 compile_crepop_def; + val _ = translate $ spec32 compile_exp_def; val _ = translate $ spec32 compile_def; @@ -429,6 +431,8 @@ val res = translate $ spec32 isSubOp_def; val res = translate $ preprocess $ spec32 conv_Shift_def; +val res = translate $ conv_panop_def; + Definition conv_Exp_alt_def: (conv_mmap_exp l = (case l of @@ -441,79 +445,89 @@ Definition conv_Exp_alt_def: NONE => NONE | SOME ys => SOME (y::ys))))) ∧ (conv_ArgList_alt tree = - case argsNT tree ArgListNT of - NONE => NONE - | SOME [] => NONE - | SOME (t::ts) => conv_mmap_exp (t::ts)) ∧ + case argsNT tree ArgListNT of + NONE => NONE + | SOME [] => NONE + | SOME (t::ts) => conv_mmap_exp (t::ts)) ∧ (conv_Exp_alt tree = (case tree of Nd nodeNT args => - if isNT nodeNT EBaseNT then - case args of - [] => NONE - | [t] => - OPTION_CHOICE (OPTION_CHOICE (conv_const t) (conv_var t)) - (conv_Exp_alt t) - | t::v4::v5 => - FOLDR (λt. OPTION_MAP2 Field (conv_nat t)) (conv_Exp_alt t) (v4::v5) - else if isNT nodeNT LabelNT then - case args of - [] => NONE - | [t] => OPTION_MAP Label (conv_ident t) - | t::v6::v7 => NONE - else if isNT nodeNT StructNT then - case args of - [] => NONE - | [ts] => do es <- conv_ArgList_alt ts; SOME (Struct es) od - | ts::v6::v7 => NONE - else if isNT nodeNT LoadByteNT then - case args of - [] => NONE - | [t] => OPTION_MAP LoadByte (conv_Exp_alt t) - | t::v6::v7 => NONE - else if isNT nodeNT LoadNT then - case args of - [] => NONE - | [t1] => NONE - | [t1; t2] => - (case conv_Shape t1 of - NONE => NONE - | SOME s => - (case conv_Exp_alt t2 of - NONE => NONE - | SOME e => SOME (Load s e))) - | t1::t2::v10::v11 => NONE - else if isNT nodeNT ECmpNT ∨ isNT nodeNT EEqNT then - case args of - [] => NONE - | [e] => conv_Exp_alt e - | [e; op] => NONE - | [e; op; e2] => - (case conv_Exp_alt e of - NONE => NONE - | SOME e1' => - (case conv_cmp op of - NONE => NONE - | SOME (op', b) => - (case conv_Exp_alt e2 of - NONE => NONE - | SOME e2' => if b then SOME (Cmp op' e2' e1') - else SOME (Cmp op' e1' e2')))) - | e::op::e2::v14::v15 => NONE - else if isNT nodeNT EShiftNT then - case args of - [] => NONE - | e::es => monad_bind (conv_Exp_alt e) (conv_Shift es) - else if EXISTS (isNT nodeNT) binaryExps then - case args of - [] => NONE - | e::es => - (case conv_Exp_alt e of - NONE => NONE - | SOME a => conv_binaryExps_alt es a) - else NONE + if isNT nodeNT EBaseNT then + case args of + [] => NONE + | [t] => + OPTION_CHOICE (OPTION_CHOICE (conv_const t) (conv_var t)) + (conv_Exp_alt t) + | t::v4::v5 => + FOLDR (λt. OPTION_MAP2 Field (conv_nat t)) (conv_Exp_alt t) (v4::v5) + else if isNT nodeNT LabelNT then + case args of + [] => NONE + | [t] => OPTION_MAP Label (conv_ident t) + | t::v6::v7 => NONE + else if isNT nodeNT StructNT then + case args of + [] => NONE + | [ts] => do es <- conv_ArgList_alt ts; SOME (Struct es) od + | ts::v6::v7 => NONE + else if isNT nodeNT LoadByteNT then + case args of + [] => NONE + | [t] => OPTION_MAP LoadByte (conv_Exp_alt t) + | t::v6::v7 => NONE + else if isNT nodeNT LoadNT then + case args of + [] => NONE + | [t1] => NONE + | [t1; t2] => + (case conv_Shape t1 of + NONE => NONE + | SOME s => + (case conv_Exp_alt t2 of + NONE => NONE + | SOME e => SOME (Load s e))) + | t1::t2::v10::v11 => NONE + else if isNT nodeNT ECmpNT ∨ isNT nodeNT EEqNT then + case args of + [] => NONE + | [e] => conv_Exp_alt e + | [e; op] => NONE + | [e; op; e2] => + (case conv_Exp_alt e of + NONE => NONE + | SOME e1' => + (case conv_cmp op of + NONE => NONE + | SOME (op', b) => + (case conv_Exp_alt e2 of + NONE => NONE + | SOME e2' => if b then SOME (Cmp op' e2' e1') + else SOME (Cmp op' e1' e2')))) + | e::op::e2::v14::v15 => NONE + else if isNT nodeNT EShiftNT then + case args of + [] => NONE + | e::es => monad_bind (conv_Exp_alt e) (conv_Shift es) + else if EXISTS (isNT nodeNT) binaryExps then + case args of + [] => NONE + | e::es => + (case conv_Exp_alt e of + NONE => NONE + | SOME a => conv_binaryExps_alt es a) + else if EXISTS (isNT nodeNT) panExps then + case args of + [] => NONE + | (e::es) => + (case conv_Exp_alt e of + NONE => NONE + | SOME a => conv_panops_alt es a) + else NONE | Lf v12 => - if tokcheck (Lf v12) (kw BaseK) then SOME BaseAddr else NONE)) ∧ + if tokcheck (Lf v12) (kw BaseK) then SOME BaseAddr + else if tokcheck (Lf v12) (kw TrueK) then SOME $ Const 1w + else if tokcheck (Lf v12) (kw FalseK) then SOME $ Const 0w + else NONE)) ∧ (conv_binaryExps_alt trees res = (case trees of [] => SOME res @@ -526,25 +540,28 @@ Definition conv_Exp_alt_def: NONE => NONE | SOME e' => (case res of - Const v17 => conv_binaryExps_alt ts (Op op [Const v17; e']) - | Var v18 => conv_binaryExps_alt ts (Op op [Var v18; e']) - | Label v19 => conv_binaryExps_alt ts (Op op [Label v19; e']) - | Struct v20 => conv_binaryExps_alt ts (Op op [Struct v20; e']) - | Field v21 v22 => conv_binaryExps_alt ts (Op op [Field v21 v22; e']) - | Load v23 v24 => conv_binaryExps_alt ts (Op op [Load v23 v24; e']) - | LoadByte v25 => conv_binaryExps_alt ts (Op op [LoadByte v25; e']) - | Op bop es => + Op bop es => if bop ≠ op ∨ isSubOp res then - conv_binaryExps_alt ts (Op bop [res; e']) + conv_binaryExps_alt ts (Op op [res; e']) else conv_binaryExps_alt ts (Op bop (es ++ [e'])) - | Cmp v28 v29 v30 => - conv_binaryExps_alt ts (Op op [Cmp v28 v29 v30; e']) - | Shift v31 v32 v33 => - conv_binaryExps_alt ts (Op op [Shift v31 v32 v33; e']) - | BaseAddr => conv_binaryExps_alt ts (Op op [BaseAddr; e'])))))) + | e => + conv_binaryExps_alt ts (Op op [e; e'])))))) ∧ + (conv_panops_alt trees res = + (case trees of + [] => SOME res + | [x] => NONE + | t1::t2::ts => + (case conv_panop t1 of + NONE => NONE + | SOME op => + (case conv_Exp_alt t2 of + NONE => NONE + | SOME e' => + conv_panops_alt ts (Panop op [res; e']))))) Termination WF_REL_TAC ‘measure (λx. case x of - INR (INR (INR x)) => ptree1_size (FST x) + INR (INR (INR (INL x))) => ptree1_size (FST x) + | INR (INR (INR (INR x))) => ptree1_size (FST x) | INR (INR (INL x)) => ptree_size x | INR (INL x) => ptree_size x | INL x => ptree1_size x)’ >> rw[] @@ -562,7 +579,8 @@ Triviality conv_Exp_thm: ∧ (∀tree. conv_Exp_alt ^tree = (conv_Exp ^tree:'a panLang$exp option)) ∧ - (∀trees res. conv_binaryExps_alt ^trees res = (conv_binaryExps ^trees res: 'a panLang$exp option)) + (∀trees res. conv_binaryExps_alt ^trees res = (conv_binaryExps ^trees res: 'a panLang$exp option)) ∧ + (∀trees res. conv_panops_alt ^trees res = (conv_panops (^trees) res: 'a panLang$exp option)) Proof ho_match_mp_tac (fetch "-" "conv_Exp_alt_ind") \\ rpt strip_tac >- (Cases_on ‘trees’>-(fs[]>>gs[conv_Exp_alt_def])>> @@ -572,7 +590,7 @@ Proof simp[conv_Exp_def]>> rename1 ‘_ = SOME x’>>Cases_on ‘x’>>gs[]) >- (Cases_on ‘tree’>>fs[] - >- simp[conv_Exp_alt_def, conv_Exp_def]>> + >- (simp[conv_Exp_alt_def, conv_Exp_def])>> rename1 ‘Nd p l’>> rewrite_tac[Once conv_Exp_alt_def,Once conv_Exp_def]>> IF_CASES_TAC @@ -591,11 +609,11 @@ Proof IF_CASES_TAC>>fs[] >- (rpt (CASE_TAC>>fs[]))>> IF_CASES_TAC>>fs[]>>rpt (CASE_TAC>>fs[]))>> - Cases_on ‘trees’>>fs[] - >- simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> - rename1 ‘h::t’>>Cases_on ‘t’>>fs[]>> - simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> - rpt (CASE_TAC>>fs[parserProgTheory.OPTION_BIND_THM]) + (Cases_on ‘trees’>>fs[] + >- simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> + rename1 ‘h::t’>>Cases_on ‘t’>>fs[]>> + simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> + rpt (CASE_TAC>>fs[parserProgTheory.OPTION_BIND_THM])) QED val res = translate_no_ind $ spec32 $ SIMP_RULE std_ss [option_map_thm, OPTION_MAP2_thm, FOLDR_eta] conv_Exp_alt_def; @@ -616,9 +634,8 @@ Proof ntac 3 strip_tac>> rename1 ‘tree = Nd p l’>> rpt (first_x_assum (qspecl_then [‘p’, ‘l’] assume_tac))>> - rw[]>>fs[])>> - last_x_assum match_mp_tac>> - ntac 9 strip_tac>>fs[] + rw[]>>fs[]) + \\ last_x_assum match_mp_tac \\ metis_tac[CONS_11] QED val _ = conv_Exp_ind |> update_precondition; diff --git a/compiler/bootstrap/translation/from_pancake64ProgScript.sml b/compiler/bootstrap/translation/from_pancake64ProgScript.sml index 340542bec1..3cafb37f22 100644 --- a/compiler/bootstrap/translation/from_pancake64ProgScript.sml +++ b/compiler/bootstrap/translation/from_pancake64ProgScript.sml @@ -250,6 +250,8 @@ open crep_to_loopTheory; val _ = translate $ spec64 prog_if_def; +val _ = translate $ spec64 compile_crepop_def; + val _ = translate $ spec64 compile_exp_def; val _ = translate $ spec64 compile_def; @@ -433,6 +435,8 @@ val res = translate $ spec64 isSubOp_def; val res = translate $ preprocess $ spec64 conv_Shift_def; +val res = translate $ conv_panop_def; + Definition conv_Exp_alt_def: (conv_mmap_exp l = (case l of @@ -515,9 +519,19 @@ Definition conv_Exp_alt_def: (case conv_Exp_alt e of NONE => NONE | SOME a => conv_binaryExps_alt es a) + else if EXISTS (isNT nodeNT) panExps then + case args of + [] => NONE + | (e::es) => + (case conv_Exp_alt e of + NONE => NONE + | SOME a => conv_panops_alt es a) else NONE | Lf v12 => - if tokcheck (Lf v12) (kw BaseK) then SOME BaseAddr else NONE)) ∧ + if tokcheck (Lf v12) (kw BaseK) then SOME BaseAddr + else if tokcheck (Lf v12) (kw TrueK) then SOME $ Const 1w + else if tokcheck (Lf v12) (kw FalseK) then SOME $ Const 0w + else NONE)) ∧ (conv_binaryExps_alt trees res = (case trees of [] => SOME res @@ -530,25 +544,28 @@ Definition conv_Exp_alt_def: NONE => NONE | SOME e' => (case res of - Const v17 => conv_binaryExps_alt ts (Op op [Const v17; e']) - | Var v18 => conv_binaryExps_alt ts (Op op [Var v18; e']) - | Label v19 => conv_binaryExps_alt ts (Op op [Label v19; e']) - | Struct v20 => conv_binaryExps_alt ts (Op op [Struct v20; e']) - | Field v21 v22 => conv_binaryExps_alt ts (Op op [Field v21 v22; e']) - | Load v23 v24 => conv_binaryExps_alt ts (Op op [Load v23 v24; e']) - | LoadByte v25 => conv_binaryExps_alt ts (Op op [LoadByte v25; e']) - | Op bop es => + Op bop es => if bop ≠ op ∨ isSubOp res then - conv_binaryExps_alt ts (Op bop [res; e']) + conv_binaryExps_alt ts (Op op [res; e']) else conv_binaryExps_alt ts (Op bop (es ++ [e'])) - | Cmp v28 v29 v30 => - conv_binaryExps_alt ts (Op op [Cmp v28 v29 v30; e']) - | Shift v31 v32 v33 => - conv_binaryExps_alt ts (Op op [Shift v31 v32 v33; e']) - | BaseAddr => conv_binaryExps_alt ts (Op op [BaseAddr; e'])))))) + | e => + conv_binaryExps_alt ts (Op op [e; e'])))))) ∧ + (conv_panops_alt trees res = + (case trees of + [] => SOME res + | [x] => NONE + | t1::t2::ts => + (case conv_panop t1 of + NONE => NONE + | SOME op => + (case conv_Exp_alt t2 of + NONE => NONE + | SOME e' => + conv_panops_alt ts (Panop op [res; e']))))) Termination WF_REL_TAC ‘measure (λx. case x of - INR (INR (INR x)) => ptree1_size (FST x) + INR (INR (INR (INL x))) => ptree1_size (FST x) + | INR (INR (INR (INR x))) => ptree1_size (FST x) | INR (INR (INL x)) => ptree_size x | INR (INL x) => ptree_size x | INL x => ptree1_size x)’ >> rw[] @@ -566,7 +583,8 @@ Triviality conv_Exp_thm: ∧ (∀tree. conv_Exp_alt ^tree = (conv_Exp ^tree:'a panLang$exp option)) ∧ - (∀trees res. conv_binaryExps_alt ^trees res = (conv_binaryExps ^trees res: 'a panLang$exp option)) + (∀trees res. conv_binaryExps_alt ^trees res = (conv_binaryExps ^trees res: 'a panLang$exp option)) ∧ + (∀trees res. conv_panops_alt ^trees res = (conv_panops (^trees) res: 'a panLang$exp option)) Proof ho_match_mp_tac (fetch "-" "conv_Exp_alt_ind") \\ rpt strip_tac >- (Cases_on ‘trees’>-(fs[]>>gs[conv_Exp_alt_def])>> @@ -576,7 +594,7 @@ Proof simp[conv_Exp_def]>> rename1 ‘_ = SOME x’>>Cases_on ‘x’>>gs[]) >- (Cases_on ‘tree’>>fs[] - >- simp[conv_Exp_alt_def, conv_Exp_def]>> + >- (simp[conv_Exp_alt_def, conv_Exp_def])>> rename1 ‘Nd p l’>> rewrite_tac[Once conv_Exp_alt_def,Once conv_Exp_def]>> IF_CASES_TAC @@ -595,11 +613,11 @@ Proof IF_CASES_TAC>>fs[] >- (rpt (CASE_TAC>>fs[]))>> IF_CASES_TAC>>fs[]>>rpt (CASE_TAC>>fs[]))>> - Cases_on ‘trees’>>fs[] - >- simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> - rename1 ‘h::t’>>Cases_on ‘t’>>fs[]>> - simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> - rpt (CASE_TAC>>fs[parserProgTheory.OPTION_BIND_THM]) + (Cases_on ‘trees’>>fs[] + >- simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> + rename1 ‘h::t’>>Cases_on ‘t’>>fs[]>> + simp[Once conv_Exp_alt_def, Once conv_Exp_def]>> + rpt (CASE_TAC>>fs[parserProgTheory.OPTION_BIND_THM])) QED val res = translate_no_ind $ spec64 $ SIMP_RULE std_ss [option_map_thm, OPTION_MAP2_thm, FOLDR_eta] conv_Exp_alt_def; @@ -620,9 +638,8 @@ Proof ntac 3 strip_tac>> rename1 ‘tree = Nd p l’>> rpt (first_x_assum (qspecl_then [‘p’, ‘l’] assume_tac))>> - rw[]>>fs[])>> - last_x_assum match_mp_tac>> - ntac 9 strip_tac>>fs[] + rw[]>>fs[]) + \\ last_x_assum match_mp_tac \\ metis_tac[CONS_11] QED val _ = conv_Exp_ind |> update_precondition; diff --git a/pancake/crepLangScript.sml b/pancake/crepLangScript.sml index ec91db1cf6..cb28b6fa40 100644 --- a/pancake/crepLangScript.sml +++ b/pancake/crepLangScript.sml @@ -18,6 +18,10 @@ Type varname = ``:num`` Type funname = ``:mlstring`` +Datatype: + crepop = (* Div | *)Mul (*| Mod*) +End + Datatype: exp = Const ('a word) | Var varname @@ -26,6 +30,7 @@ Datatype: | LoadByte exp | LoadGlob (5 word) | Op binop (exp list) + | Crepop crepop (exp list) | Cmp cmp exp exp | Shift shift exp num | BaseAddr @@ -120,6 +125,7 @@ Definition var_cexp_def: (var_cexp (LoadByte e) = var_cexp e) ∧ (var_cexp (LoadGlob a) = []) ∧ (var_cexp (Op bop es) = FLAT (MAP var_cexp es)) ∧ + (var_cexp (Crepop cop es) = FLAT (MAP var_cexp es)) ∧ (var_cexp (Cmp c e1 e2) = var_cexp e1 ++ var_cexp e2) ∧ (var_cexp (Shift sh e num) = var_cexp e) ∧ (var_cexp BaseAddr = []) @@ -185,6 +191,7 @@ Definition exps_def: (exps (LoadByte e) = exps e) ∧ (exps (LoadGlob a) = [LoadGlob a]) ∧ (exps (Op bop es) = FLAT (MAP exps es)) ∧ + (exps (Crepop pop es) = FLAT (MAP exps es)) ∧ (exps (Cmp c e1 e2) = exps e1 ++ exps e2) ∧ (exps (Shift sh e num) = exps e) ∧ (exps BaseAddr = [BaseAddr]) diff --git a/pancake/crep_to_loopScript.sml b/pancake/crep_to_loopScript.sml index 3708852759..d923f0c3e4 100644 --- a/pancake/crep_to_loopScript.sml +++ b/pancake/crep_to_loopScript.sml @@ -15,7 +15,9 @@ Datatype: context = <| vars : crepLang$varname |-> num; funcs : crepLang$funname |-> num # num; (* loc, length args *) - vmax : num|> + vmax : num; + target : architecture + |> End Definition find_var_def: @@ -40,6 +42,13 @@ Definition prog_if_def: (Assign n (Const 1w)) (Assign n (Const 0w)) (list_insert [n; m] l)] End +Definition compile_crepop_def: + (compile_crepop crepLang$Mul target x y tmp l = + if target = ARMv7 then + ([Arith (LLongMul tmp (tmp+1) x y)],tmp+1) + else + ([Arith (LLongMul tmp tmp x y)],tmp)) +End Definition compile_exp_def: (compile_exp ctxt tmp l ((BaseAddr):'a crepLang$exp) = ([], BaseAddr, tmp, l)) /\ @@ -56,6 +65,12 @@ Definition compile_exp_def: (compile_exp ctxt tmp l (Op bop es) = let (p, les, tmp, l) = compile_exps ctxt tmp l es in (p, Op bop les, tmp, l)) /\ + (compile_exp ctxt tmp'' l (Crepop cop es) = + let (p, les, tmp, l) = compile_exps ctxt tmp'' l es; + (p',tmp') = compile_crepop cop ctxt.target (tmp) (tmp+1) (tmp+LENGTH les) $ list_insert (GENLIST ($+ tmp) (LENGTH les)) l + in + (p ++ MAPi (λn. Assign (tmp+n)) les ++ p', + Var tmp', tmp'+1, insert tmp' () $ list_insert (GENLIST ($+ tmp) (tmp'-tmp)) l)) /\ (compile_exp ctxt tmp l (Cmp cmp e e') = let (p, le, tmp, l) = compile_exp ctxt tmp l e in let (p', le', tmp', l) = compile_exp ctxt tmp l e' in @@ -183,10 +198,12 @@ End Definition mk_ctxt_def: - mk_ctxt vmap fs vmax = + mk_ctxt target vmap fs vmax = <|vars := vmap; funcs := fs; - vmax := vmax|> + vmax := vmax; + target := target + |> End Definition make_vmap_def: @@ -195,11 +212,11 @@ Definition make_vmap_def: End Definition comp_func_def: - comp_func fs params body = + comp_func target fs params body = let vmap = make_vmap params; vmax = LENGTH params - 1; l = list_to_num_set (GENLIST I (LENGTH params)) in - compile (mk_ctxt vmap fs vmax) l body + compile (mk_ctxt target vmap fs vmax) l body End Definition first_name_def: @@ -217,9 +234,9 @@ Definition make_funcs_def: End Definition compile_prog_def: - compile_prog prog = + compile_prog target prog = let fnums = GENLIST (λn. n + first_name) (LENGTH prog); - comp = comp_func (make_funcs prog) in + comp = comp_func target (make_funcs prog) in MAP2 (λn (name, params, body). (n, (GENLIST I o LENGTH) params, diff --git a/pancake/loopLangScript.sml b/pancake/loopLangScript.sml index d88cff18d8..12f6dd0523 100644 --- a/pancake/loopLangScript.sml +++ b/pancake/loopLangScript.sml @@ -19,9 +19,14 @@ Datatype: | BaseAddr End +Datatype: + loop_arith = LLongMul num num num num | LLongDiv num num num num num | LDiv num num num +End + Datatype: prog = Skip | Assign num ('a exp) (* dest, source *) + | Arith loop_arith | Store ('a exp) num (* dest, source *) | SetGlobal (5 word) ('a exp) (* dest, source *) | LoadByte num num (* TODISC: have removed imm, why num num? *) @@ -80,6 +85,11 @@ End Definition assigned_vars_def: (assigned_vars Skip = []) ∧ (assigned_vars (Assign n e) = [n]) ∧ + (assigned_vars (Arith arith) = + case arith of + LLongMul v1 v2 v3 v4 => [v1;v2] + | LLongDiv v1 v2 v3 v4 v5 => [v1;v2] + | LDiv v1 v2 v3 => [v1]) ∧ (assigned_vars (LoadByte n m) = [m]) ∧ (assigned_vars (Seq p q) = assigned_vars p ++ assigned_vars q) ∧ (assigned_vars (If cmp n r p q ns) = assigned_vars p ++ assigned_vars q) ∧ @@ -99,6 +109,11 @@ Definition acc_vars_def: (acc_vars Continue l = l) ∧ (acc_vars (Loop l1 body l2) l = acc_vars body l) ∧ (acc_vars (If x1 x2 x3 p1 p2 l1) l = acc_vars p1 (acc_vars p2 l)) ∧ + (acc_vars (Arith arith) l = + case arith of + LLongMul v1 v2 v3 v4 => insert v1 () $ insert v2 () l + | LLongDiv v1 v2 v3 v4 v5 => insert v1 () $ insert v2 () l + | LDiv v1 v2 v3 => insert v1 () l) ∧ (acc_vars (Mark p1) l = acc_vars p1 l) /\ (acc_vars Tick l = l) /\ (acc_vars Skip l = l) /\ diff --git a/pancake/loop_callScript.sml b/pancake/loop_callScript.sml index e8f23e4a0e..3d9eca62a4 100644 --- a/pancake/loop_callScript.sml +++ b/pancake/loop_callScript.sml @@ -50,6 +50,28 @@ Definition comp_def: (comp l Tick = (Tick, LN)) /\ (comp l (Raise n) = (Raise n, LN)) /\ (comp l (Return n) = (Return n, LN)) /\ + (comp l (Arith arith) = + (Arith arith, + case arith of + LLongMul r1 r2 r3 r4 => + (case (lookup r1 l, lookup r2 l) of + (NONE, NONE) => l + | (SOME _ , NONE) => delete r1 l + | (NONE, SOME loc) => delete r2 l + | _ => delete r1 $ delete r2 l + ) + | LLongDiv r1 r2 r3 r4 r5 => + (case (lookup r1 l, lookup r2 l) of + (NONE, NONE) => l + | (SOME _ , NONE) => delete r1 l + | (NONE, SOME loc) => delete r2 l + | _ => delete r1 $ delete r2 l + ) + | LDiv r1 r2 r3 => + (case lookup r1 l of + NONE => l + | _ => delete r1 l) + | _ => l)) ∧ (comp l p = (p, l)) End diff --git a/pancake/loop_liveScript.sml b/pancake/loop_liveScript.sml index a7a7a7346a..d1cc3f7dec 100644 --- a/pancake/loop_liveScript.sml +++ b/pancake/loop_liveScript.sml @@ -46,6 +46,14 @@ Proof QED +Definition arith_vars: + arith_vars (LLongMul r1 r2 r3 r4) l = + insert r3 () $ insert r4 () $ delete r1 $ delete r2 l ∧ + arith_vars (LDiv r1 r2 r3) l = insert r2 () $ insert r3 () $ delete r1 l ∧ + arith_vars (LLongDiv r1 r2 r3 r4 r5) l = + insert r3 () $ insert r4 () $ insert r5 () $ delete r1 $ delete r2 l +End + (* This optimisation shrinks all cutsets and also deletes assignments to unused variables. The Loop case is the interesting one: an auxiliary function is used to find a fixed-point. *) @@ -75,6 +83,9 @@ Definition shrink_def: (shrink b Skip l = (Skip,l)) /\ (shrink b (Return v) l = (Return v, insert v () LN)) /\ (shrink b (Raise v) l = (Raise v, insert v () LN)) /\ + (shrink b (Arith arith) l = + (Arith arith, arith_vars arith l) + ) ∧ (shrink b (LocValue n m) l = case lookup n l of | NONE => (Skip,l) diff --git a/pancake/loop_to_wordScript.sml b/pancake/loop_to_wordScript.sml index fc878993d2..f99add4b9b 100644 --- a/pancake/loop_to_wordScript.sml +++ b/pancake/loop_to_wordScript.sml @@ -61,6 +61,16 @@ Definition comp_def: (comp ctxt Skip l = (wordLang$Skip,l)) /\ (comp ctxt (Assign n e) l = (Assign (find_var ctxt n) (comp_exp ctxt e),l)) /\ + (comp ctxt (Arith arith) l = + (case arith of + LLongMul r1 r2 r3 r4 => + (Inst(Arith(LongMul (find_var ctxt r1) (find_var ctxt r2) + (find_var ctxt r3) (find_var ctxt r4))),l) + | LLongDiv r1 r2 r3 r4 r5 => + (Inst(Arith(LongDiv (find_var ctxt r1) (find_var ctxt r2) + (find_var ctxt r3) (find_var ctxt r4) (find_var ctxt r5))),l) + | LDiv r1 r2 r3 => + (Inst(Arith(Div (find_var ctxt r1) (find_var ctxt r2) (find_var ctxt r3))),l))) /\ (comp ctxt (Store e v) l = (Store (comp_exp ctxt e) (find_var ctxt v), l)) /\ (comp ctxt (SetGlobal a e) l = diff --git a/pancake/panLangScript.sml b/pancake/panLangScript.sml index 8f584c9cbc..50cc698626 100644 --- a/pancake/panLangScript.sml +++ b/pancake/panLangScript.sml @@ -32,6 +32,10 @@ Datatype: | Comb (shape list) End +Datatype: + panop = (* Div | *)Mul (* | Mod*) +End + Datatype: exp = Const ('a word) | Var varname @@ -42,6 +46,7 @@ Datatype: | Load shape exp (* exp: start addr of value with given shape *) | LoadByte exp | Op binop (exp list) + | Panop panop (exp list) | Cmp cmp exp exp | Shift shift exp num | BaseAddr @@ -176,6 +181,7 @@ Definition var_exp_def: (var_exp (Load sh e) = var_exp e) ∧ (var_exp (LoadByte e) = var_exp e) ∧ (var_exp (Op bop es) = FLAT (MAP var_exp es)) ∧ + (var_exp (Panop op es) = FLAT (MAP var_exp es)) ∧ (var_exp (Cmp c e1 e2) = var_exp e1 ++ var_exp e2) ∧ (var_exp (Shift sh e num) = var_exp e) Termination @@ -192,5 +198,4 @@ Definition destruct_def: (destruct _ = []) End - val _ = export_theory(); diff --git a/pancake/pan_to_crepScript.sml b/pancake/pan_to_crepScript.sml index 45566414b9..69032fd235 100644 --- a/pancake/pan_to_crepScript.sml +++ b/pancake/pan_to_crepScript.sml @@ -32,6 +32,10 @@ Definition comp_field_def: else comp_field (i-1) shs (DROP (size_of_shape sh) es)) End +Definition compile_panop_def: + compile_panop panLang$Mul = crepLang$Mul +End + Definition compile_exp_def: (compile_exp ctxt ((Const c):'a panLang$exp) = ([(Const c): 'a crepLang$exp], One)) /\ @@ -64,6 +68,11 @@ Definition compile_exp_def: case cexp_heads cexps of | SOME es => ([Op bop es], One) | _ => ([Const 0w], One)) /\ + (compile_exp ctxt (Panop pop es) = + let cexps = MAP FST (MAP (compile_exp ctxt) es) in + case cexp_heads cexps of + | SOME es => ([Crepop (compile_panop pop) es], One) + | _ => ([Const 0w], One)) /\ (compile_exp ctxt (Cmp cmp e e') = let ce = FST (compile_exp ctxt e); ce' = FST (compile_exp ctxt e') in diff --git a/pancake/pan_to_targetScript.sml b/pancake/pan_to_targetScript.sml index 6b7123af1c..cdda37a648 100644 --- a/pancake/pan_to_targetScript.sml +++ b/pancake/pan_to_targetScript.sml @@ -11,7 +11,7 @@ val _ = new_theory "pan_to_target"; Definition compile_prog_def: compile_prog c prog = - let prog = pan_to_word$compile_prog prog in + let prog = pan_to_word$compile_prog c.lab_conf.asm_conf.ISA prog in let (col,prog) = word_to_word$compile c.word_to_word_conf c.lab_conf.asm_conf prog in from_word c LN prog End diff --git a/pancake/pan_to_wordScript.sml b/pancake/pan_to_wordScript.sml index f8adb4baee..6c53b1a3f7 100644 --- a/pancake/pan_to_wordScript.sml +++ b/pancake/pan_to_wordScript.sml @@ -10,10 +10,10 @@ val _ = new_theory "pan_to_word"; Definition compile_prog_def: - compile_prog prog = + compile_prog arch prog = let prog = pan_simp$compile_prog prog; prog = pan_to_crep$compile_prog prog; - prog = crep_to_loop$compile_prog prog in + prog = crep_to_loop$compile_prog arch prog in loop_to_word$compile prog End diff --git a/pancake/parser/panConcreteExamplesScript.sml b/pancake/parser/panConcreteExamplesScript.sml index 0501ad02fe..e074ca8815 100644 --- a/pancake/parser/panConcreteExamplesScript.sml +++ b/pancake/parser/panConcreteExamplesScript.sml @@ -83,7 +83,7 @@ val ex3 = ‘ else { return false; } }’; -val treeEx3 = (* check_success $ *) parse_pancake ex3; +val treeEx3 = check_success $ parse_pancake ex3; (** Loops: standard looping construct. *) @@ -171,6 +171,17 @@ val ex8 = ‘ val treeEx8 = check_success $ parse_pancake ex8; +(* Multiplication + *) + +val ex8_and_a_half = ‘x = a * b; + x = a * b * c; + x = (a + b) * c; + x = a + b * c; + x = a * b + c;’; + +val treeEx8_and_a_half = check_success $ parse_pancake ex8_and_a_half; + (** Statments. *) (** Small test modelled after the minimal working example. *) @@ -208,8 +219,6 @@ val ex_much_fun = ‘ val treeExMuchFun = check_success $ parse_pancake ex_much_fun; (** We can assign boolean expressions to variables. *) -(** FIXME: Does not parse correctly. *) -(** Expected: Xor (And b a) (And c d) *) val exN = ‘fun blah() { x = b & a ^ c & d; }’; val treeExN = check_success $ parse_pancake exN; diff --git a/pancake/parser/panLexerScript.sml b/pancake/parser/panLexerScript.sml index ceebc2f4c7..6e808ec39b 100644 --- a/pancake/parser/panLexerScript.sml +++ b/pancake/parser/panLexerScript.sml @@ -19,7 +19,7 @@ val _ = new_theory "panLexer"; Datatype: keyword = SkipK | StoreK | StoreBK | IfK | ElseK | WhileK | BrK | ContK | RaiseK | RetK | TicK | VarK | WithK | HandleK - | LdsK | LdbK | BaseK | InK | FunK + | LdsK | LdbK | BaseK | InK | FunK | TrueK | FalseK End Datatype: @@ -27,7 +27,7 @@ Datatype: | EqT | NeqT | LessT | GreaterT | GeqT | LeqT | PlusT | MinusT | HashT | DotT | StarT | LslT | LsrT | AsrT | RorT - | TrueT | FalseT | IntT int | IdentT string + | IntT int | IdentT string | LParT | RParT | CommaT | SemiT | ColonT | DArrowT | AddrT | LBrakT | RBrakT | LCurT | RCurT | AssignT @@ -110,8 +110,8 @@ Definition get_keyword_def: if s = "lds" then (KeywordT LdsK) else if s = "ldb" then (KeywordT LdbK) else if s = "@base" then (KeywordT BaseK) else - if s = "true" then TrueT else - if s = "false" then FalseT else + if s = "true" then (KeywordT TrueK) else + if s = "false" then (KeywordT FalseK) else if s = "fun" then (KeywordT FunK) else if isPREFIX "@" s ∨ s = "" then LexErrorT else IdentT s diff --git a/pancake/parser/panPEGScript.sml b/pancake/parser/panPEGScript.sml index 9325df17f8..055cd980e0 100644 --- a/pancake/parser/panPEGScript.sml +++ b/pancake/parser/panPEGScript.sml @@ -21,11 +21,11 @@ Datatype: | ArgListNT | ParamListNT | EXorNT | EAndNT | EEqNT | ECmpNT - | EShiftNT | EAddNT + | EShiftNT | EAddNT | EMulNT | EBaseNT | StructNT | LoadNT | LoadByteNT | LabelNT | ShapeNT | ShapeCombNT - | EqOpsNT | CmpOpsNT | ShiftOpsNT | AddOpsNT + | EqOpsNT | CmpOpsNT | ShiftOpsNT | AddOpsNT | MulOpsNT End Definition mknt_def: @@ -212,16 +212,21 @@ Definition pancake_peg_def[nocompute]: rpt (seql [mknt ShiftOpsNT; keep_nat] I) FLAT] (mksubtree EShiftNT)); - (INL EAddNT, seql [mknt EBaseNT; - rpt (seql [mknt AddOpsNT; mknt EBaseNT] I) + (INL EAddNT, seql [mknt EMulNT; + rpt (seql [mknt AddOpsNT; mknt EMulNT] I) FLAT] (mksubtree EAddNT)); + (INL EMulNT, seql [mknt EBaseNT; + rpt (seql [mknt MulOpsNT; mknt EBaseNT] I) FLAT] + (mksubtree EMulNT)); (INL EBaseNT, seql [choicel [seql [consume_tok LParT; mknt ExpNT; consume_tok RParT] I; + keep_kw TrueK; keep_kw FalseK; keep_int; keep_ident; mknt LabelNT; mknt StructNT; mknt LoadNT; - mknt LoadByteNT; keep_kw BaseK]; + mknt LoadByteNT; keep_kw BaseK; + ]; rpt (seql [consume_tok DotT; keep_nat] I) FLAT] (mksubtree EBaseNT)); @@ -247,7 +252,8 @@ Definition pancake_peg_def[nocompute]: (INL CmpOpsNT, choicel [keep_tok LessT; keep_tok GeqT; keep_tok GreaterT; keep_tok LeqT]); (INL ShiftOpsNT, choicel [keep_tok LslT; keep_tok LsrT; keep_tok AsrT; keep_tok RorT]); - (INL AddOpsNT, choicel [keep_tok PlusT; keep_tok MinusT])] + (INL AddOpsNT, choicel [keep_tok PlusT; keep_tok MinusT]); + (INL MulOpsNT, keep_tok StarT)] |> End @@ -484,11 +490,11 @@ in th::acc end -val topo_nts = [“AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT”, +val topo_nts = [“MulOpsNT”, “AddOpsNT”, “ShiftOpsNT”, “CmpOpsNT”, “EqOpsNT”, “ShapeNT”, “ShapeCombNT”, “LabelNT”, “LoadByteNT”, “LoadNT”, “StructNT”, - “EBaseNT”, “EAddNT”, “EShiftNT”, “ECmpNT”, + “EBaseNT”, “EMulNT”, “EAddNT”, “EShiftNT”, “ECmpNT”, “EEqNT”, “EAndNT”, “EXorNT”, “ExpNT”, “ArgListNT”, “ReturnNT”, “RaiseNT”, “ExtCallNT”, diff --git a/pancake/parser/panPtreeConversionScript.sml b/pancake/parser/panPtreeConversionScript.sml index fcbe8ac31c..884e9265ad 100644 --- a/pancake/parser/panPtreeConversionScript.sml +++ b/pancake/parser/panPtreeConversionScript.sml @@ -99,6 +99,10 @@ Definition binaryExps_def: binaryExps = [ExpNT; EXorNT; EAndNT; EAddNT] End +Definition panExps_def: + panExps = [EMulNT] +End + (** Subtraction must apply to only two subexpressions. * See the pancake semantics script. *) Definition isSubOp_def: @@ -123,6 +127,18 @@ Definition conv_binop_def: else NONE End +Definition conv_panop_def: + (conv_panop (Nd nodeNT args) = + if isNT nodeNT MulOpsNT then + case args of + [leaf] => conv_panop leaf + | _ => NONE + else NONE) ∧ + conv_panop leaf = + if tokcheck leaf StarT then SOME Mul + else NONE +End + Definition conv_shift_def: (conv_shift (Nd nodeNT args) = if isNT nodeNT ShiftOpsNT then @@ -262,8 +278,14 @@ Definition conv_Exp_def: case args of [] => NONE | (e::es) => conv_binaryExps es ' (conv_Exp e) + else if EXISTS (isNT nodeNT) panExps then + case args of + [] => NONE + | (e::es) => conv_panops es ' (conv_Exp e) else NONE) ∧ (conv_Exp leaf = if tokcheck leaf (kw BaseK) then SOME BaseAddr + else if tokcheck leaf (kw TrueK) then SOME $ Const 1w + else if tokcheck leaf (kw FalseK) then SOME $ Const 0w else NONE) ∧ conv_binaryExps [] e = SOME e ∧ (conv_binaryExps (t1::t2::ts) res = @@ -271,16 +293,26 @@ Definition conv_Exp_def: e <- conv_Exp t2; case res of Op bop es => if bop ≠ op ∨ isSubOp res then - conv_binaryExps ts (Op bop [res; e]) + conv_binaryExps ts (Op op [res; e]) else conv_binaryExps ts (Op bop (APPEND es [e])) | e' => conv_binaryExps ts (Op op [e'; e]) od) ∧ - conv_binaryExps _ _ = NONE (* Impossible: ruled out by grammar. *) + conv_binaryExps _ _ = NONE ∧ (* Impossible: ruled out by grammar. *) + conv_panops [] e = SOME e ∧ + (conv_panops (t1::t2::ts) res = + do op <- conv_panop t1; + e <- conv_Exp t2; + case res of + Panop bop es => conv_panops ts (Panop op [res; e]) + | e' => conv_panops ts (Panop op [e'; e]) + od) ∧ + conv_panops _ _ = NONE (* Impossible: ruled out by grammar. *) Termination WF_REL_TAC ‘measure (λx. case x of - INR (INR x) => ptree1_size (FST x) | INR (INL x) => ptree_size x - | INL x => ptree_size x)’ >> rw[] + | INL x => ptree_size x + | INR (INR(INL x)) => ptree1_size (FST x) + | INR (INR(INR x)) => ptree1_size (FST x))’ >> rw[] >> Cases_on ‘tree’ >> gvs[argsNT_def,parsetree_size_def] >> drule_then assume_tac mem_ptree_thm >> gvs[] diff --git a/pancake/proofs/crep_to_loopProofScript.sml b/pancake/proofs/crep_to_loopProofScript.sml index ad5c1ae9d3..d07423d741 100644 --- a/pancake/proofs/crep_to_loopProofScript.sml +++ b/pancake/proofs/crep_to_loopProofScript.sml @@ -78,10 +78,12 @@ End (* could have been stated differently *) Definition ctxt_fc_def: - ctxt_fc cvs ns args = + ctxt_fc c cvs ns args = <|vars := FEMPTY |++ ZIP (ns, args); funcs := cvs; - vmax := list_max args|> + vmax := list_max args; + target := c + |> End Definition code_rel_def: @@ -92,7 +94,7 @@ Definition code_rel_def: ?loc len. FLOOKUP ctxt.funcs f = SOME (loc, len) /\ LENGTH ns = len /\ let args = GENLIST I len; - nctxt = ctxt_fc ctxt.funcs ns args in + nctxt = ctxt_fc ctxt.target ctxt.funcs ns args in lookup loc t_code = SOME (args, ocompile nctxt (list_to_num_set args) prog) @@ -191,7 +193,7 @@ Theorem code_rel_intro: ?loc len. FLOOKUP ctxt.funcs f = SOME (loc, len) /\ LENGTH ns = len /\ let args = GENLIST I len; - nctxt = ctxt_fc ctxt.funcs ns args in + nctxt = ctxt_fc ctxt.target ctxt.funcs ns args in lookup loc t_code = SOME (args, ocompile nctxt (list_to_num_set args) prog) @@ -342,6 +344,83 @@ Proof fs [evaluate_def] QED +Theorem cut_sets_MAPi_Assign: + ∀les cs offset. + cut_sets cs (nested_seq (MAPi (λn. Assign (n + offset)) les)) = + list_insert (GENLIST ($+ offset) (LENGTH les)) cs +Proof + Induct_on ‘les’ \\ + rw[nested_seq_def,cut_sets_def,list_insert_def,o_DEF,GENLIST_CONS] \\ + PURE_ONCE_REWRITE_TAC[DECIDE “∀n m. n + SUC m = m + SUC n”] \\ + first_x_assum $ PURE_REWRITE_TAC o single \\ + rpt (AP_THM_TAC ORELSE AP_TERM_TAC) \\ + simp[FUN_EQ_THM] +QED + +Theorem assigned_vars_MAPi_Assign: + ∀les offset. + assigned_vars (nested_seq (MAPi (λn. Assign (n + offset)) les)) = + GENLIST ($+ offset) (LENGTH les) +Proof + Induct_on ‘les’ \\ + rw[nested_seq_def,assigned_vars_def,o_DEF,GENLIST_CONS] \\ + PURE_ONCE_REWRITE_TAC[DECIDE “∀n m. n + SUC m = m + SUC n”] \\ + first_x_assum $ PURE_REWRITE_TAC o single \\ + rpt (AP_THM_TAC ORELSE AP_TERM_TAC) \\ + simp[FUN_EQ_THM] +QED + +Theorem survives_MAPi_Assign: + ∀n les offset. + survives n (nested_seq (MAPi (λn. Assign (n + offset)) les)) = T +Proof + Induct_on ‘les’ \\ + rw[nested_seq_def,survives_def,o_DEF,GENLIST_CONS] \\ + PURE_ONCE_REWRITE_TAC[DECIDE “∀n m. n + SUC m = m + SUC n”] \\ + first_x_assum $ PURE_REWRITE_TAC o single \\ + rpt (AP_THM_TAC ORELSE AP_TERM_TAC) \\ + simp[FUN_EQ_THM] +QED + +Theorem insert_insert_eq: + insert a b $ insert a b c = insert a b c +Proof + rw[Once insert_insert] +QED + +Theorem list_insert_SNOC: + ∀y l x. + list_insert (SNOC x y) l = + insert x () $ list_insert y l +Proof + Induct_on ‘y’ \\ rw[list_insert_def] +QED + +Theorem compile_exps_alt: + compile_exps ctxt tmp l [] = ([],[],tmp,l) ∧ + compile_exps ctxt tmp l (e::es) = + let + (p,le,tmp',l') = compile_exp ctxt tmp l e; + (p1,les,tmp'',l'') = compile_exps ctxt tmp' l' es + in + (p ++ p1,le::les,tmp'',l'') +Proof + rw[] \\ rw[Once compile_exp_def] +QED + +Theorem list_insert_insert: + ∀x xs l. insert x () $ list_insert xs l = list_insert xs $ insert x () l +Proof + Induct_on ‘xs’ \\ rw[list_insert_def] \\ + rename1 ‘insert a () $ insert b () _’ \\ + Cases_on ‘a = b’ \\ rw[insert_shadow,insert_swap] +QED + +Theorem list_insert_append: + ∀xs ys l. list_insert (xs ++ ys) l = list_insert xs $ list_insert ys l +Proof + Induct \\ rw[list_insert_def,list_insert_insert] +QED Theorem compile_exp_out_rel_cases: (!ct tmp l (e:'a crepLang$exp) p le ntmp nl. @@ -357,13 +436,7 @@ Proof TRY ( fs [Once compile_exp_def] >> rveq >> TRY (pairarg_tac >> fs [] >> rveq >> NO_TAC) >> - fs [nested_seq_def, comp_syn_ok_basic_cases, cut_sets_def] >> NO_TAC) - >- ( - rename [‘compile_exp _ _ _ (Label f)’] >> - fs [compile_exp_def] >> rveq >> - fs [nested_seq_def, cut_sets_def] >> - match_mp_tac comp_syn_ok_seq2 >> - fs [comp_syn_ok_basic_cases]) + fs [nested_seq_def, comp_syntax_ok_def, cut_sets_def] >> NO_TAC) >- ( rename [‘compile_exp _ _ _ (LoadByte e)’] >> rpt gen_tac >> strip_tac >> @@ -376,7 +449,7 @@ Proof fs [nested_seq_def] >> rpt ( match_mp_tac comp_syn_ok_seq2 >> - fs [comp_syn_ok_basic_cases])) >> + fs [comp_syntax_ok_def])) >> fs [compile_exp_def] >> pairarg_tac >> fs [] >> rveq >> res_tac >> fs [] >> @@ -394,6 +467,45 @@ Proof >- fs [compile_exp_def] >> fs [] >> fs [Once compile_exp_def]) + >- ( + rename [‘compile_exp _ _ _ (Crepop _ _)’] >> + simp [Once compile_exp_def] >> + pairarg_tac >> fs [] >> rveq >> + rpt gen_tac >> disch_then strip_assume_tac >> + Cases_on ‘cop’ >> + gvs[DefnBase.one_line_ify NONE compile_crepop_def,ELIM_UNCURRY,AllCaseEqs()] >> + (conj_asm1_tac + >- (rpt (match_mp_tac comp_syn_ok_nested_seq >> conj_tac) >> + rw[] >> + simp[nested_seq_def,comp_syntax_ok_def] + >- (rpt $ pop_assum kall_tac >> + rename1 ‘comp_syntax_ok cs’ >> + qid_spec_tac ‘cs’ >> + qid_spec_tac ‘tmp'’ >> + Induct_on ‘les’ >> gvs[nested_seq_def,comp_syntax_ok_def] >> + simp[o_DEF] >> + rpt strip_tac >> + first_x_assum(qspec_then ‘SUC tmp'’ mp_tac) >> + rename1 ‘comp_syntax_ok css’ >> + disch_then(qspec_then ‘css’ mp_tac) >> + qmatch_goalsub_abbrev_tac ‘a1 ⇒ a2’ >> + ‘a1 = a2’ suffices_by simp[] >> + unabbrev_all_tac >> + ntac 2 AP_TERM_TAC >> + match_mp_tac MAPi_CONG >> + rw[]) >> + simp[cut_sets_nested_seq,nested_seq_def,cut_sets_def,cut_sets_MAPi_Assign, + comp_syntax_ok_def] >> + simp[insert_swap] >> + conj_tac >> qexists_tac ‘[]’ >> simp[insert_swap,insert_shadow])) >> + rw[] >> + simp[cut_sets_nested_seq,nested_seq_def,cut_sets_def,cut_sets_MAPi_Assign] >> + simp[insert_insert_eq] >> + simp[Once insert_insert,SimpR “$=”,insert_insert_eq] >> + simp[insert_insert_eq,GSYM ADD1,GENLIST,list_insert_SNOC] >> + simp[insert_swap,insert_shadow] >> + rw[CONV_RULE (STRIP_QUANT_CONV $ LHS_CONV $ PURE_ONCE_REWRITE_CONV [ADD_SYM]) GENLIST_APPEND] \\ + rw[list_insert_append,list_insert_insert,list_insert_def,insert_swap,ADD1]) >- ( rename [‘compile_exp _ _ _ (Cmp _ _ _)’] >> rpt gen_tac >> strip_tac >> @@ -409,20 +521,14 @@ Proof match_mp_tac comp_syn_ok_nested_seq >> fs []) >> fs [list_insert_def, nested_seq_def, cut_sets_def] >> - rpt (match_mp_tac comp_syn_ok_seq2 >> - fs [comp_syn_ok_basic_cases]) >> + fs [comp_syntax_ok_def] >> fs [cut_sets_def] >> rw [Once comp_syntax_ok_def, list_insert_def] >> fs [cut_sets_nested_seq] >> qmatch_goalsub_abbrev_tac ‘insert t2 _ (insert t1 _ cc)’ >> - match_mp_tac EQ_SYM >> - ‘insert t1 () (insert t2 () (insert t1 () cc)) = insert t2 () (insert t1 () cc)’ by ( - ‘insert t2 () (insert t1 () cc) = insert t1 () (insert t2 () cc)’ - by (fs [Abbr ‘t1’, Abbr ‘t2’] >> match_mp_tac insert_swap >> fs []) >> - fs [Abbr ‘t1’, Abbr ‘t2’] >> fs [Once insert_insert]) >> - fs [] >> pop_assum kall_tac >> - fs [Once insert_insert]) >> - conj_tac >- (res_tac >> fs []) >> + qexists_tac ‘[t1;t2]’ >> + simp[] >> + Cases_on ‘t1 = t2’ >> simp[insert_swap,insert_shadow]) >> res_tac >> fs [] >> qmatch_goalsub_abbrev_tac ‘list_insert _ ll’ >> fs [prog_if_def] >> @@ -434,15 +540,11 @@ Proof fs [Abbr ‘np’, nested_seq_def] >> ntac 3 (rw [Once comp_syntax_ok_def]) >> rw [Once comp_syntax_ok_def, cut_sets_def, Abbr ‘l''’, list_insert_def] >> - fs [cut_sets_nested_seq] >> + fs [cut_sets_nested_seq,comp_syntax_ok_def] >> qmatch_goalsub_abbrev_tac ‘insert t2 _ (insert t1 _ cc)’ >> - match_mp_tac EQ_SYM >> - ‘insert t1 () (insert t2 () (insert t1 () cc)) = insert t2 () (insert t1 () cc)’ by ( - ‘insert t2 () (insert t1 () cc) = insert t1 () (insert t2 () cc)’ - by (fs [Abbr ‘t1’, Abbr ‘t2’] >> match_mp_tac insert_swap >> fs []) >> - fs [Abbr ‘t1’, Abbr ‘t2’] >> fs [Once insert_insert]) >> - fs [] >> pop_assum kall_tac >> - fs [Once insert_insert]) >> + qexists_tac ‘[t1;t2]’ >> + simp[] >> + Cases_on ‘t1 = t2’ >> simp[insert_swap,insert_shadow]) >> qpat_x_assum ‘comp_syntax_ok l (nested_seq (p' ++ p''))’ assume_tac >> fs [cut_sets_nested_seq] >> fs [Abbr ‘np’, nested_seq_def, cut_sets_def]) >> @@ -495,6 +597,17 @@ Proof >- ( once_rewrite_tac [compile_exp_def] >> fs [] >> strip_tac >> pairarg_tac >> fs []) + >- ( + once_rewrite_tac [compile_exp_def] >> fs [DefnBase.one_line_ify NONE compile_crepop_def] >> strip_tac >> + PURE_TOP_CASE_TAC >> fs[] >> + pairarg_tac >> fs [] >> + ‘tmp <= tmp'’ by metis_tac [compile_exp_out_rel_cases] >> + rw[] >> + gvs[assigned_vars_nested_seq_split,nested_seq_def,assigned_vars_def,assigned_vars_MAPi_Assign, + MEM_GENLIST] >> + res_tac >> + DECIDE_TAC + ) >- ( rpt gen_tac >> strip_tac >> fs [compile_exp_def] >> @@ -545,47 +658,55 @@ Theorem compile_exp_le_tmp_domain_cases: MEM n (FLAT (MAP locals_touched les)) ==> n < tmp' /\ n ∈ domain l') Proof ho_match_mp_tac compile_exp_ind >> - rpt conj_tac >> rpt gen_tac >> strip_tac >> - TRY ( - rename [‘Op bop es’] >> - rpt gen_tac >> - strip_tac >> - qpat_x_assum ‘compile_exp _ _ _ _ = _’ mp_tac >> - once_rewrite_tac [compile_exp_def] >> - strip_tac >> fs [] >> - pairarg_tac >> fs [] >> rveq >> - fs [locals_touched_def, crepLangTheory.var_cexp_def, ETA_AX]) >> - TRY ( - rename [‘compile_exps’] >> - rpt gen_tac >> - strip_tac >> - qpat_x_assum ‘compile_exps _ _ _ _ = _’ mp_tac >> - once_rewrite_tac [compile_exp_def] >> - cases_on ‘es’ >> fs [] >> rveq - >- ( - strip_tac >> rveq >> - fs [MAP]) >> - strip_tac >> - pairarg_tac >> fs [] >> - pairarg_tac >> fs [] >> rveq >> - ‘tmp <= tmp'' /\ tmp'' <= tmp' /\ l'' = cut_sets l (nested_seq p') /\ + rpt conj_tac >> rpt gen_tac >> strip_tac + >~ [‘Op bop es’] >- + (rpt gen_tac >> + strip_tac >> + qpat_x_assum ‘compile_exp _ _ _ _ = _’ mp_tac >> + once_rewrite_tac [compile_exp_def] >> + strip_tac >> fs [] >> + pairarg_tac >> fs [] >> rveq >> + fs [locals_touched_def, crepLangTheory.var_cexp_def, ETA_AX]) + >~ [‘Crepop bop es’] >- + (rpt gen_tac >> + strip_tac >> + qpat_x_assum ‘compile_exp _ _ _ _ = _’ mp_tac >> + once_rewrite_tac [compile_exp_def] >> + strip_tac >> fs [DefnBase.one_line_ify NONE compile_crepop_def] >> + Cases_on ‘bop’ >> + rpt(pairarg_tac >> fs [] >> rveq) >> + fs [locals_touched_def, crepLangTheory.var_cexp_def, ETA_AX,AllCaseEqs()] + ) + >~ [‘compile_exps’] >- + (rpt gen_tac >> + strip_tac >> + qpat_x_assum ‘compile_exps _ _ _ _ = _’ mp_tac >> + once_rewrite_tac [compile_exp_def] >> + cases_on ‘es’ >> fs [] >> rveq + >- ( + strip_tac >> rveq >> + fs [MAP]) >> + strip_tac >> + pairarg_tac >> fs [] >> + pairarg_tac >> fs [] >> rveq >> + ‘tmp <= tmp'' /\ tmp'' <= tmp' /\ l'' = cut_sets l (nested_seq p') /\ l' = cut_sets l'' (nested_seq p1)’ by - metis_tac [compile_exp_out_rel_cases] >> - fs [MAP] - >- ( - res_tac >> fs [subspt_domain] >> - drule compile_exps_out_rel >> - strip_tac >> - drule cut_sets_union_domain_union >> - strip_tac >> fs []) >> - last_x_assum match_mp_tac >> - fs [] >> - rw [] >> - res_tac >> fs [subspt_domain] >> - drule compile_exp_out_rel >> - strip_tac >> - drule cut_sets_union_domain_union >> - strip_tac >> fs [] >> NO_TAC) >> + metis_tac [compile_exp_out_rel_cases] >> + fs [MAP] + >- ( + res_tac >> fs [subspt_domain] >> + drule compile_exps_out_rel >> + strip_tac >> + drule cut_sets_union_domain_union >> + strip_tac >> fs []) >> + last_x_assum match_mp_tac >> + fs [] >> + rw [] >> + res_tac >> fs [subspt_domain] >> + drule compile_exp_out_rel >> + strip_tac >> + drule cut_sets_union_domain_union >> + strip_tac >> fs []) >> fs [compile_exp_def] >> TRY (pairarg_tac >> fs []) >> rveq >> TRY (pairarg_tac >> fs []) >> rveq >> @@ -615,58 +736,306 @@ Theorem comp_exp_preserves_eval: locals_rel ctxt nl s.locals st.locals Proof ho_match_mp_tac crepSemTheory.eval_ind >> - rpt conj_tac >> rpt gen_tac >> strip_tac >> - TRY ( - rename [‘eval s (Op op es)’] >> - rw [] >> - fs [Once compile_exp_def] >> fs [] >> - pairarg_tac >> fs [] >> rveq >> - fs [crepSemTheory.eval_def, CaseEq "option"] >> rveq >> - fs [loopSemTheory.eval_def, wlab_wloc_def] >> - qsuff_tac ‘∃ck st. - evaluate (nested_seq p,t with clock := ck + t.clock) = (NONE,st) ∧ - the_words (MAP (λa. eval st a) les) = - SOME ((MAP (λw. case w of Word n => n | Label v1 => ARB) ws)) /\ - state_rel s st ∧ mem_rel ctxt.funcs s.memory st.memory ∧ - globals_rel ctxt.funcs s.globals st.globals ∧ - code_rel ctxt s.code st.code ∧ locals_rel ctxt l' s.locals st.locals’ - >- ( - strip_tac >> - qexists_tac ‘ck’ >> - fs [wlab_wloc_def]) >> - qpat_x_assum ‘word_op _ _ = _’ kall_tac >> - rpt (pop_assum mp_tac) >> - MAP_EVERY qid_spec_tac [‘t’, ‘p’, ‘les’ , ‘tmp’, ‘l’,‘ws’, ‘es’] >> - Induct - >- ( - rw [] >> - fs [OPT_MMAP_def] >> rveq >> - fs [compile_exp_def] >> rveq >> - fs [nested_seq_def, loopSemTheory.evaluate_def, - wordSemTheory.the_words_def, state_rel_clock_add_zero]) >> + rpt conj_tac >> rpt gen_tac >> strip_tac + >~ [‘eval s $ Op bop es’] >- + (rename [‘eval s (Op op es)’] >> + rw [] >> + fs [Once compile_exp_def] >> fs [] >> + pairarg_tac >> fs [] >> rveq >> + fs [crepSemTheory.eval_def, CaseEq "option"] >> rveq >> + fs [loopSemTheory.eval_def, wlab_wloc_def] >> + qsuff_tac ‘∃ck st. + evaluate (nested_seq p,t with clock := ck + t.clock) = (NONE,st) ∧ + the_words (MAP (λa. eval st a) les) = + SOME ((MAP (λw. case w of Word n => n | Label v1 => ARB) ws)) /\ + state_rel s st ∧ mem_rel ctxt.funcs s.memory st.memory ∧ + globals_rel ctxt.funcs s.globals st.globals ∧ + code_rel ctxt s.code st.code ∧ locals_rel ctxt l' s.locals st.locals’ + >- ( + strip_tac >> + qexists_tac ‘ck’ >> + fs [wlab_wloc_def]) >> + qpat_x_assum ‘word_op _ _ = _’ kall_tac >> + rpt (pop_assum mp_tac) >> + MAP_EVERY qid_spec_tac [‘t’, ‘p’, ‘les’ , ‘tmp’, ‘l’,‘ws’, ‘es’] >> + Induct + >- ( + rw [] >> + fs [OPT_MMAP_def] >> rveq >> + fs [compile_exp_def] >> rveq >> + fs [nested_seq_def, loopSemTheory.evaluate_def, + wordSemTheory.the_words_def, state_rel_clock_add_zero]) >> + rw [] >> + last_x_assum mp_tac >> + impl_tac >- metis_tac [] >> + strip_tac >> fs [] >> + qpat_x_assum ‘compile_exps _ _ _ (h::_) = _’ mp_tac >> + once_rewrite_tac [compile_exp_def] >> + fs [] >> pairarg_tac >> fs [] >> + pairarg_tac >> fs [] >> + strip_tac >> rveq >> + fs [OPT_MMAP_def] >> rveq >> + last_x_assum (qspec_then ‘h’ mp_tac) >> + fs [] >> + disch_then drule_all >> + strip_tac >> fs [] >> rveq >> + qmatch_asmsub_rename_tac ‘compile_exp _ _ _ h = (p,le,itmp,il)’ >> + qmatch_asmsub_rename_tac ‘compile_exps _ _ _ _ = (fp,les,ntmp,nl)’ >> + last_x_assum (qspecl_then + [‘t'’, ‘il’, ‘itmp’, ‘les’, ‘fp’, ‘st’] mp_tac) >> + fs [] >> + imp_res_tac compile_exp_out_rel >> + fs [] >> + strip_tac >> fs [] >> + qpat_x_assum ‘evaluate (nested_seq p, _) = _’ assume_tac >> + drule evaluate_add_clock_eq >> + fs [] >> + disch_then (qspec_then ‘ck'’ assume_tac) >> + drule evaluate_comb_seq >> + disch_then drule >> + fs [evaluate_nested_seq_comb_seq] >> + strip_tac >> + qexists_tac ‘ck + ck'’ >> + qexists_tac ‘st'’ >> + fs [] >> + cases_on ‘h'’ >> fs [] >> + fs [wordSemTheory.the_words_def] >> + ‘eval st' le = eval st le’ suffices_by fs [wlab_wloc_def] >> + imp_res_tac compile_exps_out_rel >> + qpat_x_assum ‘evaluate (nested_seq fp, _) = _’ assume_tac >> + drule comp_syn_ok_upd_local_clock >> + disch_then drule >> + fs [] >> strip_tac >> + qpat_x_assum ‘evaluate (nested_seq p,_) = _’ mp_tac >> + once_rewrite_tac [ADD_ASSOC] >> + strip_tac >> + fs [wlab_wloc_def] >> + assume_tac nested_seq_pure_evaluation >> + pop_assum (qspecl_then [‘p’, ‘fp’, ‘t’, ‘st'’, ‘st with clock := ck' + st.clock’, ‘l’, + ‘itmp’, ‘le’, ‘Word c’, ‘ck + ck'’, ‘0’] mp_tac) >> + fs [] >> + impl_tac + >- ( + fs [eval_upd_clock_eq] >> + drule comp_exp_assigned_vars_tmp_bound >> fs [] >> + strip_tac >> + drule comp_exps_assigned_vars_tmp_bound >> fs [] >> + strip_tac >> + gen_tac >> + strip_tac >> fs [] >> + imp_res_tac locals_rel_intro >> + drule compile_exp_le_tmp_domain >> + disch_then (qspecl_then [‘tmp’, ‘l’, ‘h’, ‘p’, ‘le’, + ‘itmp’, ‘cut_sets l (nested_seq p)’, ‘n’] mp_tac) >> + fs [] >> + impl_tac + >- ( + rw [] >> + drule eval_some_var_cexp_local_lookup >> + disch_then drule >> + strip_tac >> res_tac >> fs []) >> + fs []) >> + fs []) + >~ [‘eval s $ Crepop bop es’] >- + (rw [] >> + fs [Once compile_exp_def] >> fs [] >> + pairarg_tac >> fs [] >> rveq >> + fs [crepSemTheory.eval_def, CaseEq "option"] >> rveq >> + fs [loopSemTheory.eval_def, wlab_wloc_def] >> + fs [wlab_wloc_def] >> + gvs[AllCaseEqs(),DefnBase.one_line_ify NONE crep_op_def, + DefnBase.one_line_ify NONE compile_crepop_def,MAP_EQ_CONS, + opt_mmap_eq_some,SF DNF_ss, + compile_exps_alt + ] >> + rpt (pairarg_tac >> gvs[]) >> + gvs[AllCaseEqs()] >> + rpt $ qpat_x_assum ‘SOME _ = _’ $ assume_tac o GSYM >> + first_x_assum drule_all >> strip_tac >> + first_x_assum drule >> rpt $ disch_then drule >> + (impl_keep_tac + >- (imp_res_tac compile_exp_out_rel_cases >> DECIDE_TAC) >> + strip_tac >> + qexists_tac ‘ck + ck'’ >> + qpat_x_assum ‘evaluate _ = (NONE,_)’ mp_tac >> + drule loopPropsTheory.evaluate_add_clock_eq >> + disch_then(qspec_then ‘ck'’ mp_tac) >> + impl_tac >> simp[] >> + strip_tac >> + FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] >> + drule_then (PURE_REWRITE_TAC o single) (cj 2 evaluate_nested_seq_cases) >> + strip_tac >> + drule_then (PURE_REWRITE_TAC o single) (cj 2 evaluate_nested_seq_cases) >> + drule_then drule nested_seq_pure_evaluation >> + disch_then $ drule_at $ Pos last >> + imp_res_tac compile_exp_out_rel_cases >> rveq >> + ntac 2 $ disch_then drule >> + simp[GSYM PULL_EXISTS] >> + impl_tac >- + (qexists_tac ‘tmp''’ (* generated name *) >> + rw[] >> + imp_res_tac comp_exp_assigned_vars_tmp_bound_cases >> + TRY DECIDE_TAC >> + MAP_FIRST match_mp_tac [cj 1 compile_exp_le_tmp_domain, + cj 2 compile_exp_le_tmp_domain] >> + imp_res_tac locals_rel_intro >> + first_x_assum $ irule_at $ Pos last >> + ntac 2 $ first_x_assum $ irule_at $ Pos hd >> + simp[] >> + rw[] >> + drule_all eval_some_var_cexp_local_lookup >> + metis_tac[]) >> + strip_tac >> + simp[evaluate_def,nested_seq_def,eval_def,loop_arith_def,set_var_def,lookup_insert] >> + rename1 ‘eval(st' with locals := insert tmp' (wlab_wloc ctxt.funcs (Word ww)) st'.locals) lee’ >> + ‘∀w. eval (set_var tmp' (wlab_wloc ctxt.funcs w) st') lee + = + eval st' lee + ’ + by(strip_tac >> + match_mp_tac locals_touched_eq_eval_eq >> + simp[set_var_def] >> + imp_res_tac locals_rel_intro >> + drule compile_exp_le_tmp_domain >> + disch_then $ drule_then drule >> + simp[GSYM AND_IMP_INTRO,GSYM PULL_FORALL] >> + impl_tac + >- (rw[] >> + imp_res_tac eval_some_var_cexp_local_lookup >> + metis_tac[]) >> + rw[] >> + res_tac >> + rw[lookup_insert]) >> + gvs[set_var_def] >> + simp[set_var_def,wlab_wloc_def,lookup_insert,GSYM word_mul_def] >> + simp[word_mul_def] >> + conj_tac >- gvs[state_rel_def] >> + gvs[locals_rel_def,list_insert_def] >> + conj_tac + >- (drule_then match_mp_tac SUBSET_TRANS >> + rw[SUBSET_DEF]) >> + rw[] >> + res_tac >> + gvs[] >> + gvs[ctxt_max_def] >> + res_tac >> + rw[lookup_insert])) + >~ [‘Const w’] >- + (fs [crepSemTheory.eval_def, compile_exp_def] >> rveq >> + fs [nested_seq_def, evaluate_def, eval_def, + wlab_wloc_def, state_rel_clock_add_zero]) + >~ [‘eval s (Var vname)’] >- + (fs [crepSemTheory.eval_def, compile_exp_def] >> rveq >> + fs [nested_seq_def, evaluate_def, find_var_def] >> + imp_res_tac locals_rel_intro >> + fs [eval_def, state_rel_clock_add_zero]) + >~ [‘eval s (Label fname)’] >- + (fs [crepSemTheory.eval_def, compile_exp_def, CaseEq "option"] >> + rveq >> + qexists_tac ‘0’ >> fs [] >> + ‘t with clock := t.clock = t’ by fs [state_component_equality] >> + fs [] >> pop_assum kall_tac >> + fs [nested_seq_def, evaluate_def, find_lab_def] >> + cases_on ‘v1’ >> rveq >> + imp_res_tac code_rel_intro >> + fs [eval_def, set_var_def, domain_lookup, wlab_wloc_def, + state_rel_def, locals_rel_def, SUBSET_INSERT_RIGHT] >> + rw [] >> + first_x_assum drule >> fs [] >> + strip_tac >> fs [] >> + fs [lookup_insert] >> + TOP_CASE_TAC >> fs [] >> + fs [ctxt_max_def] >> + first_x_assum drule >> fs []) + >~ [‘eval s (Load e)’] >- + (fs [crepSemTheory.eval_def] >> + TOP_CASE_TAC >> fs [] >> + TOP_CASE_TAC >> fs [] >> + rw [] >> + fs [compile_exp_def] >> + pairarg_tac >> fs [] >> rveq >> + last_x_assum drule_all >> fs [] >> rveq >> + strip_tac >> fs [] >> + qexists_tac ‘ck’ >> fs [] >> + fs [loopSemTheory.eval_def, wlab_wloc_def] >> + fs [crepSemTheory.mem_load_def, loopSemTheory.mem_load_def] >> rveq >> + imp_res_tac state_rel_intro >> + imp_res_tac mem_rel_intro >> + last_x_assum (qspec_then ‘c’ mp_tac) >> fs []) + >~ [‘eval s (LoadByte e)’] >- + (fs [crepSemTheory.eval_def] >> + TOP_CASE_TAC >> fs [] >> + TOP_CASE_TAC >> fs [] >> + TOP_CASE_TAC >> fs [] >> + rw [] >> + fs [compile_exp_def] >> + pairarg_tac >> fs [] >> rveq >> + last_x_assum drule_all >> + fs [] >> rveq >> + strip_tac >> fs [] >> + qexists_tac ‘ck’ >> fs [] >> + drule evaluate_none_nested_seq_append >> + disch_then (qspec_then + ‘[Assign tmp' le'; LoadByte tmp' tmp']’ mp_tac) >> + strip_tac >> fs [] >> + pop_assum kall_tac >> + fs [nested_seq_def, loopSemTheory.evaluate_def] >> + fs [set_var_def, wlab_wloc_def] >> + fs [panSemTheory.mem_load_byte_def, CaseEq "word_lab", + wordSemTheory.mem_load_byte_aux_def] >> + imp_res_tac mem_rel_intro >> + last_x_assum (qspec_then ‘byte_align c’ (mp_tac o GSYM)) >> + strip_tac >> fs [] >> + last_x_assum (qspec_then ‘byte_align c’ (mp_tac o GSYM)) >> + strip_tac >> fs [wlab_wloc_def] >> + imp_res_tac state_rel_intro >> + fs [eval_def, state_rel_def] >> + imp_res_tac compile_exp_out_rel >> + fs [locals_rel_def, SUBSET_INSERT_RIGHT] >> rw [] >> + first_x_assum drule >> fs [] >> + strip_tac >> fs [] >> + fs [lookup_insert] >> + TOP_CASE_TAC >> fs [] >> + fs [ctxt_max_def] >> + first_x_assum drule >> fs []) + >~ [‘eval s (LoadGlob gadr)’] >- + (fs [crepSemTheory.eval_def, compile_exp_def] >> rveq >> + fs [nested_seq_def, loopSemTheory.evaluate_def] >> + fs [eval_def] >> + imp_res_tac globals_rel_intro >> + fs [] >> + qexists_tac ‘0’ >> fs [] >> + ‘t with clock := t.clock = t’ suffices_by fs [] >> + fs [state_component_equality]) + >~ [‘Shift’] >- + (rw [] >> + fs [crepSemTheory.eval_def, CaseEq "option", CaseEq "word_lab", + compile_exp_def] >> + rveq >> fs [] >> + pairarg_tac >> fs [] >> rveq >> + fs [loopSemTheory.evaluate_def] >> + last_x_assum drule_all >> + strip_tac >> rfs [] >> + qexists_tac ‘ck’ >> fs [] >> + fs [loopSemTheory.eval_def, wlab_wloc_def]) + >-( rw [] >> - last_x_assum mp_tac >> - impl_tac >- metis_tac [] >> - strip_tac >> fs [] >> - qpat_x_assum ‘compile_exps _ _ _ (h::_) = _’ mp_tac >> - once_rewrite_tac [compile_exp_def] >> - fs [] >> pairarg_tac >> fs [] >> + fs [crepSemTheory.eval_def, CaseEq "option", CaseEq "word_lab"] >> + rveq >> fs [compile_exp_def] >> pairarg_tac >> fs [] >> - strip_tac >> rveq >> - fs [OPT_MMAP_def] >> rveq >> - last_x_assum (qspec_then ‘h’ mp_tac) >> - fs [] >> - disch_then drule_all >> + pairarg_tac >> fs [] >> + rveq >> fs [] >> + fs [prog_if_def] >> + last_x_assum drule_all >> strip_tac >> fs [] >> rveq >> - qmatch_asmsub_rename_tac ‘compile_exp _ _ _ h = (p,le,itmp,il)’ >> - qmatch_asmsub_rename_tac ‘compile_exps _ _ _ _ = (fp,les,ntmp,nl)’ >> - last_x_assum (qspecl_then - [‘t'’, ‘il’, ‘itmp’, ‘les’, ‘fp’, ‘st’] mp_tac) >> - fs [] >> - imp_res_tac compile_exp_out_rel >> + qmatch_asmsub_rename_tac ‘compile_exp _ _ _ e = (p1,le1,tmp1,l1)’ >> + qmatch_asmsub_rename_tac ‘compile_exp _ _ _ e' = (p2,le2,tmp2,l2)’ >> + last_x_assum (qspecl_then [‘st’, ‘ctxt’, ‘tmp1’, ‘l1’] mp_tac) >> fs [] >> + imp_res_tac compile_exp_out_rel >> fs [] >> rveq >> strip_tac >> fs [] >> - qpat_x_assum ‘evaluate (nested_seq p, _) = _’ assume_tac >> + qmatch_goalsub_abbrev_tac ‘nested_seq (_ ++ _ ++ np)’ >> + qpat_x_assum ‘evaluate (nested_seq p1,_) = _’ assume_tac >> drule evaluate_add_clock_eq >> fs [] >> disch_then (qspec_then ‘ck'’ assume_tac) >> @@ -674,198 +1043,27 @@ Proof disch_then drule >> fs [evaluate_nested_seq_comb_seq] >> strip_tac >> - qexists_tac ‘ck + ck'’ >> - qexists_tac ‘st'’ >> + drule evaluate_add_clock_eq >> fs [] >> - cases_on ‘h'’ >> fs [] >> - fs [wordSemTheory.the_words_def] >> - ‘eval st' le = eval st le’ suffices_by fs [wlab_wloc_def] >> - imp_res_tac compile_exps_out_rel >> - qpat_x_assum ‘evaluate (nested_seq fp, _) = _’ assume_tac >> - drule comp_syn_ok_upd_local_clock >> - disch_then drule >> - fs [] >> strip_tac >> - qpat_x_assum ‘evaluate (nested_seq p,_) = _’ mp_tac >> - once_rewrite_tac [ADD_ASSOC] >> - strip_tac >> - fs [wlab_wloc_def] >> - assume_tac nested_seq_pure_evaluation >> - pop_assum (qspecl_then [‘p’, ‘fp’, ‘t’, ‘st'’, ‘st with clock := ck' + st.clock’, ‘l’, - ‘itmp’, ‘le’, ‘Word c’, ‘ck + ck'’, ‘0’] mp_tac) >> + disch_then (qspec_then ‘1’ assume_tac) >> fs [] >> - impl_tac - >- ( - fs [eval_upd_clock_eq] >> - drule comp_exp_assigned_vars_tmp_bound >> fs [] >> - strip_tac >> - drule comp_exps_assigned_vars_tmp_bound >> fs [] >> - strip_tac >> - gen_tac >> - strip_tac >> fs [] >> - imp_res_tac locals_rel_intro >> - drule compile_exp_le_tmp_domain >> - disch_then (qspecl_then [‘tmp’, ‘l’, ‘h’, ‘p’, ‘le’, - ‘itmp’, ‘cut_sets l (nested_seq p)’, ‘n’] mp_tac) >> - fs [] >> - impl_tac - >- ( - rw [] >> - drule eval_some_var_cexp_local_lookup >> - disch_then drule >> - strip_tac >> res_tac >> fs []) >> - fs []) >> - fs []) >> - TRY ( - rename [‘Const w’] >> - fs [crepSemTheory.eval_def, compile_exp_def] >> rveq >> - fs [nested_seq_def, evaluate_def, eval_def, - wlab_wloc_def, state_rel_clock_add_zero]) >> - TRY ( - rename [‘eval s (Var vname)’] >> - fs [crepSemTheory.eval_def, compile_exp_def] >> rveq >> - fs [nested_seq_def, evaluate_def, find_var_def] >> - imp_res_tac locals_rel_intro >> - fs [eval_def, state_rel_clock_add_zero]) >> - TRY ( - rename [‘eval s (Label fname)’] >> - fs [crepSemTheory.eval_def, compile_exp_def, CaseEq "option"] >> - rveq >> - qexists_tac ‘0’ >> fs [] >> - ‘t with clock := t.clock = t’ by fs [state_component_equality] >> - fs [] >> pop_assum kall_tac >> - fs [nested_seq_def, evaluate_def, find_lab_def] >> - cases_on ‘v1’ >> rveq >> - imp_res_tac code_rel_intro >> - fs [eval_def, set_var_def, domain_lookup, wlab_wloc_def, - state_rel_def, locals_rel_def, SUBSET_INSERT_RIGHT] >> - rw [] >> - first_x_assum drule >> fs [] >> - strip_tac >> fs [] >> - fs [lookup_insert] >> - TOP_CASE_TAC >> fs [] >> - fs [ctxt_max_def] >> - first_x_assum drule >> fs []) >> - TRY ( - rename [‘eval s (Load e)’] >> - fs [crepSemTheory.eval_def] >> - TOP_CASE_TAC >> fs [] >> - TOP_CASE_TAC >> fs [] >> - rw [] >> - fs [compile_exp_def] >> - pairarg_tac >> fs [] >> rveq >> - last_x_assum drule_all >> fs [] >> rveq >> - strip_tac >> fs [] >> - qexists_tac ‘ck’ >> fs [] >> - fs [loopSemTheory.eval_def, wlab_wloc_def] >> - fs [crepSemTheory.mem_load_def, loopSemTheory.mem_load_def] >> rveq >> - imp_res_tac state_rel_intro >> - imp_res_tac mem_rel_intro >> - last_x_assum (qspec_then ‘c’ mp_tac) >> fs []) >> - TRY ( - rename [‘eval s (LoadByte e)’] >> - fs [crepSemTheory.eval_def] >> - TOP_CASE_TAC >> fs [] >> - TOP_CASE_TAC >> fs [] >> - TOP_CASE_TAC >> fs [] >> - rw [] >> - fs [compile_exp_def] >> - pairarg_tac >> fs [] >> rveq >> - last_x_assum drule_all >> - fs [] >> rveq >> - strip_tac >> fs [] >> - qexists_tac ‘ck’ >> fs [] >> + qexists_tac ‘ck + ck' + 1’ >> drule evaluate_none_nested_seq_append >> - disch_then (qspec_then - ‘[Assign tmp' le'; LoadByte tmp' tmp']’ mp_tac) >> - strip_tac >> fs [] >> - pop_assum kall_tac >> - fs [nested_seq_def, loopSemTheory.evaluate_def] >> - fs [set_var_def, wlab_wloc_def] >> - fs [panSemTheory.mem_load_byte_def, CaseEq "word_lab", - wordSemTheory.mem_load_byte_aux_def] >> - imp_res_tac mem_rel_intro >> - last_x_assum (qspec_then ‘byte_align c’ (mp_tac o GSYM)) >> - strip_tac >> fs [] >> - last_x_assum (qspec_then ‘byte_align c’ (mp_tac o GSYM)) >> - strip_tac >> fs [wlab_wloc_def] >> - imp_res_tac state_rel_intro >> - fs [eval_def, state_rel_def] >> - imp_res_tac compile_exp_out_rel >> - fs [locals_rel_def, SUBSET_INSERT_RIGHT] >> rw [] >> - first_x_assum drule >> fs [] >> - strip_tac >> fs [] >> - fs [lookup_insert] >> - TOP_CASE_TAC >> fs [] >> - fs [ctxt_max_def] >> - first_x_assum drule >> fs []) >> - TRY ( - rename [‘eval s (LoadGlob gadr)’] >> - fs [crepSemTheory.eval_def, compile_exp_def] >> rveq >> - fs [nested_seq_def, loopSemTheory.evaluate_def] >> - fs [eval_def] >> - imp_res_tac globals_rel_intro >> - fs [] >> - qexists_tac ‘0’ >> fs [] >> - ‘t with clock := t.clock = t’ suffices_by fs [] >> - fs [state_component_equality]) >> - TRY ( - rename [‘Shift’] >> - rw [] >> - fs [crepSemTheory.eval_def, CaseEq "option", CaseEq "word_lab", - compile_exp_def] >> - rveq >> fs [] >> - pairarg_tac >> fs [] >> rveq >> - fs [loopSemTheory.evaluate_def] >> - last_x_assum drule_all >> - strip_tac >> rfs [] >> - qexists_tac ‘ck’ >> fs [] >> - fs [loopSemTheory.eval_def, wlab_wloc_def]) - >-( - rw [] >> - fs [crepSemTheory.eval_def, CaseEq "option", CaseEq "word_lab"] >> - rveq >> fs [compile_exp_def] >> + disch_then (qspec_then ‘np’ assume_tac) >> + fs [] >> pop_assum kall_tac >> + fs [Abbr ‘np’, nested_seq_def] >> + fs [evaluate_def] >> pairarg_tac >> fs [] >> pairarg_tac >> fs [] >> - rveq >> fs [] >> - fs [prog_if_def] >> - last_x_assum drule_all >> - strip_tac >> fs [] >> rveq >> - qmatch_asmsub_rename_tac ‘compile_exp _ _ _ e = (p1,le1,tmp1,l1)’ >> - qmatch_asmsub_rename_tac ‘compile_exp _ _ _ e' = (p2,le2,tmp2,l2)’ >> - last_x_assum (qspecl_then [‘st’, ‘ctxt’, ‘tmp1’, ‘l1’] mp_tac) >> - fs [] >> - imp_res_tac compile_exp_out_rel >> fs [] >> rveq >> - strip_tac >> fs [] >> - qmatch_goalsub_abbrev_tac ‘nested_seq (_ ++ _ ++ np)’ >> - qpat_x_assum ‘evaluate (nested_seq p1,_) = _’ assume_tac >> - drule evaluate_add_clock_eq >> - fs [] >> - disch_then (qspec_then ‘ck'’ assume_tac) >> - drule evaluate_comb_seq >> - disch_then drule >> - fs [evaluate_nested_seq_comb_seq] >> - strip_tac >> - drule evaluate_add_clock_eq >> - fs [] >> - disch_then (qspec_then ‘1’ assume_tac) >> - fs [] >> - qexists_tac ‘ck + ck' + 1’ >> - drule evaluate_none_nested_seq_append >> - disch_then (qspec_then ‘np’ assume_tac) >> - fs [] >> pop_assum kall_tac >> - fs [Abbr ‘np’, nested_seq_def] >> - fs [evaluate_def] >> - pairarg_tac >> fs [] >> - pairarg_tac >> fs [] >> - pairarg_tac >> fs [] >> rveq >> - rfs [eval_upd_clock_eq] >> - ‘eval st' le1 = eval st le1’ by ( - qpat_x_assum ‘_ = (_, st)’ assume_tac >> - drule nested_seq_pure_evaluation >> - disch_then (qspecl_then [‘p2’, ‘st'’, ‘l’, ‘tmp1’, ‘le1’, ‘Word w1’, ‘ck'’] mp_tac) >> - fs [wlab_wloc_def] >> - impl_tac - >- ( + pairarg_tac >> fs [] >> rveq >> + rfs [eval_upd_clock_eq] >> + ‘eval st' le1 = eval st le1’ by ( + qpat_x_assum ‘_ = (_, st)’ assume_tac >> + drule nested_seq_pure_evaluation >> + disch_then (qspecl_then [‘p2’, ‘st'’, ‘l’, ‘tmp1’, ‘le1’, ‘Word w1’, ‘ck'’] mp_tac) >> + fs [wlab_wloc_def] >> + impl_tac + >- ( imp_res_tac comp_exp_assigned_vars_tmp_bound >> fs [] >> gen_tac >> strip_tac >> fs [] >> @@ -876,57 +1074,57 @@ Proof fs [] >> impl_tac >- ( - rw [] >> - imp_res_tac eval_some_var_cexp_local_lookup >> - res_tac >> fs []) >> + rw [] >> + imp_res_tac eval_some_var_cexp_local_lookup >> + res_tac >> fs []) >> fs []) >> - fs []) >> - fs [] >> rfs [] >> - pop_assum kall_tac >> - rveq >> - fs [wlab_wloc_def, loopSemTheory.set_var_def, - loopSemTheory.eval_def] >> - fs [Once eval_upd_locals_clock_eq] >> - ‘eval (st' with locals := insert (tmp2 + 1) (Word w1) st'.locals) le2 = - eval st' le2’ by ( - ho_match_mp_tac locals_touched_eq_eval_eq >> - fs [] >> rw [] >> fs [lookup_insert] >> - TOP_CASE_TAC >> fs [] >> - imp_res_tac locals_rel_intro >> - drule compile_exp_le_tmp_domain >> - disch_then (qspecl_then - [‘tmp1’, ‘cut_sets l (nested_seq p1)’, ‘e'’, ‘p2’, ‘le2’, ‘tmp2’, - ‘cut_sets (cut_sets l (nested_seq p1)) (nested_seq p2)’, - ‘n’] mp_tac) >> - impl_tac - >- ( + fs []) >> + fs [] >> rfs [] >> + pop_assum kall_tac >> + rveq >> + fs [wlab_wloc_def, loopSemTheory.set_var_def, + loopSemTheory.eval_def] >> + fs [Once eval_upd_locals_clock_eq] >> + ‘eval (st' with locals := insert (tmp2 + 1) (Word w1) st'.locals) le2 = + eval st' le2’ by ( + ho_match_mp_tac locals_touched_eq_eval_eq >> + fs [] >> rw [] >> fs [lookup_insert] >> + TOP_CASE_TAC >> fs [] >> + imp_res_tac locals_rel_intro >> + drule compile_exp_le_tmp_domain >> + disch_then (qspecl_then + [‘tmp1’, ‘cut_sets l (nested_seq p1)’, ‘e'’, ‘p2’, ‘le2’, ‘tmp2’, + ‘cut_sets (cut_sets l (nested_seq p1)) (nested_seq p2)’, + ‘n’] mp_tac) >> + impl_tac + >- ( fs [] >> rw [] >> drule_all eval_some_var_cexp_local_lookup >> strip_tac >> res_tac >> fs [] >> rveq >> fs []) >> - fs []) >> - fs [] >> - pop_assum kall_tac >> - fs [] >> rfs [] >> rveq >> - fs [lookup_insert] >> - fs [get_var_imm_def, list_insert_def] >> - cases_on ‘word_cmp cmp w1 w2’ >> - fs [loopSemTheory.evaluate_def, loopSemTheory.eval_def, - loopSemTheory.set_var_def] >> ( - fs [cut_res_def, list_insert_def] >> - fs [cut_state_def] >> - imp_res_tac locals_rel_intro >> - fs [SUBSET_INSERT_RIGHT] >> - rveq >> fs [dec_clock_def] >> - fs [lookup_inter, lookup_insert] >> - conj_tac >- EVAL_TAC >> - conj_tac >- fs [state_rel_def] >> - fs [list_insert_def, locals_rel_def, domain_inter, SUBSET_INSERT_RIGHT] >> - rw [] >> - fs [lookup_inter, lookup_insert] >> - res_tac >> fs [] >> rveq >> fs [] >> - ‘n <= tmp2’ by (fs [ctxt_max_def] >> res_tac >> fs []) >> - fs [domain_lookup])) >> + fs []) >> + fs [] >> + pop_assum kall_tac >> + fs [] >> rfs [] >> rveq >> + fs [lookup_insert] >> + fs [get_var_imm_def, list_insert_def] >> + cases_on ‘word_cmp cmp w1 w2’ >> + fs [loopSemTheory.evaluate_def, loopSemTheory.eval_def, + loopSemTheory.set_var_def] >> ( + fs [cut_res_def, list_insert_def] >> + fs [cut_state_def] >> + imp_res_tac locals_rel_intro >> + fs [SUBSET_INSERT_RIGHT] >> + rveq >> fs [dec_clock_def] >> + fs [lookup_inter, lookup_insert] >> + conj_tac >- EVAL_TAC >> + conj_tac >- fs [state_rel_def] >> + fs [list_insert_def, locals_rel_def, domain_inter, SUBSET_INSERT_RIGHT] >> + rw [] >> + fs [lookup_inter, lookup_insert] >> + res_tac >> fs [] >> rveq >> fs [] >> + ‘n <= tmp2’ by (fs [ctxt_max_def] >> res_tac >> fs []) >> + fs [domain_lookup])) >> fs [crepSemTheory.eval_def, compile_exp_def] >> rveq >> fs [nested_seq_def, evaluate_def, eval_def, wlab_wloc_def, state_rel_clock_add_zero]>> qexists_tac ‘0’ >> @@ -1042,6 +1240,16 @@ Proof pop_assum mp_tac >> rw [Once compile_exp_def, AllCaseEqs()] >> rveq >> pairarg_tac >> fs []) + >- ( + rw [] >> + pop_assum mp_tac >> + rw [Once compile_exp_def, DefnBase.one_line_ify NONE compile_crepop_def, AllCaseEqs()] >> rveq >> + rpt(pairarg_tac >> gvs[AllCaseEqs()]) >> + match_mp_tac survives_nested_seq_intro >> + simp[nested_seq_def,survives_def] >> + match_mp_tac survives_nested_seq_intro >> + res_tac >> + simp[survives_MAPi_Assign]) >- ( rw [] >> pop_assum mp_tac >> @@ -1189,6 +1397,17 @@ Proof qpat_x_assum ‘compile_exp _ _ _ (Op _ _) = _’ mp_tac >> rw [Once compile_exp_def, AllCaseEqs()] >> rveq >> pairarg_tac >> fs []) + >- ( + rw [] >> + qpat_x_assum ‘compile_exp _ _ _ (Crepop _ _) = _’ mp_tac >> + rw [Once compile_exp_def, AllCaseEqs(),DefnBase.one_line_ify NONE compile_crepop_def + ] >> rveq >> + rpt(pairarg_tac >> fs []) >> + gvs[assigned_vars_MAPi_Assign,assigned_vars_nested_seq_split,MEM_GENLIST, + assigned_vars_def,nested_seq_def,AllCaseEqs() + ] >> + imp_res_tac compile_exp_out_rel_cases >> + DECIDE_TAC) >- ( rw [] >> qpat_x_assum ‘compile_exp _ _ _ (Cmp _ _ _) = _’ mp_tac >> @@ -2453,7 +2672,7 @@ Theorem call_preserve_state_code_locals_rel: FLOOKUP s.code fname = SOME (ns,prog) /\ FLOOKUP ctxt.funcs fname = SOME (loc,LENGTH lns) /\ MAP (eval s) argexps = MAP SOME args ==> - let nctxt = ctxt_fc ctxt.funcs ns lns in + let nctxt = ctxt_fc ctxt.target ctxt.funcs ns lns in state_rel (s with <|locals := FEMPTY |++ ZIP (ns,args); clock := s.clock − 1|>) @@ -2626,11 +2845,11 @@ val tail_case_tac = (qspecl_then [ ‘dec_clock (st with locals := fromAList (ZIP (lns,FRONT (MAP (wlab_wloc ctxt.funcs) args ++ [Loc loc 0]))))’, - ‘(ctxt_fc ctxt.funcs ns lns)’, ‘list_to_num_set lns’] mp_tac) >> + ‘(ctxt_fc ctxt.target ctxt.funcs ns lns)’, ‘list_to_num_set lns’] mp_tac) >> impl_tac >- ( fs [crepSemTheory.dec_clock_def, dec_clock_def] >> - ‘(ctxt_fc ctxt.funcs ns lns).funcs = ctxt.funcs’ by ( + ‘(ctxt_fc ctxt.target ctxt.funcs ns lns).funcs = ctxt.funcs’ by ( fs [ctxt_fc_def]) >> fs [] >> match_mp_tac (call_preserve_state_code_locals_rel |> SIMP_RULE bool_ss [LET_THM]) >> fs [Abbr ‘lns’] >> @@ -3030,11 +3249,11 @@ Proof (qspecl_then [ ‘dec_clock (st with locals := fromAList (ZIP (lns,FRONT (MAP (wlab_wloc ctxt.funcs) args ++ [Loc loc 0]))))’, - ‘(ctxt_fc ctxt.funcs ns lns)’, ‘list_to_num_set lns’] mp_tac) >> + ‘(ctxt_fc ctxt.target ctxt.funcs ns lns)’, ‘list_to_num_set lns’] mp_tac) >> impl_tac >- ( fs [crepSemTheory.dec_clock_def, dec_clock_def] >> - ‘(ctxt_fc ctxt.funcs ns lns).funcs = ctxt.funcs’ by ( + ‘(ctxt_fc ctxt.target ctxt.funcs ns lns).funcs = ctxt.funcs’ by ( fs [ctxt_fc_def]) >> fs [] >> match_mp_tac (call_preserve_state_code_locals_rel |> SIMP_RULE bool_ss [LET_THM]) >> fs [Abbr ‘lns’] >> @@ -3049,7 +3268,7 @@ Proof (* case split on return option variable *) fs [CaseEq "option"] >> rveq >> fs [rt_var_def] >> - ‘(ctxt_fc ctxt.funcs ns lns).funcs = ctxt.funcs’ by ( + ‘(ctxt_fc ctxt.target ctxt.funcs ns lns).funcs = ctxt.funcs’ by ( fs [ctxt_fc_def]) >> fs [] >> pop_assum kall_tac >> TRY ( @@ -3866,7 +4085,6 @@ Proof fcalled_timed_out_tac QED - Theorem ncompile_correct: ^(compile_prog_tm ()) Proof @@ -3996,8 +4214,8 @@ QED Theorem first_compile_prog_all_distinct: - !crep_code. - ALL_DISTINCT (MAP FST (compile_prog crep_code)) + !c crep_code. + ALL_DISTINCT (MAP FST (compile_prog c crep_code)) Proof rw [] >> fs [crep_to_loopTheory.compile_prog_def] >> @@ -4015,16 +4233,16 @@ Proof “:'d”|->“:'a crepLang$prog”, “:'e”|-> “:'a prog”] map_map2_fst) >> disch_then (qspec_then ‘λparams body. loop_live$optimise - (comp_func (make_funcs crep_code) + (comp_func c (make_funcs crep_code) params body)’ mp_tac) >> fs [] QED Theorem mk_ctxt_code_imp_code_rel: - !crep_code start np. ALL_DISTINCT (MAP FST crep_code) /\ + !c crep_code start np. ALL_DISTINCT (MAP FST crep_code) /\ ALOOKUP crep_code start = SOME ([],np) ==> - code_rel (mk_ctxt FEMPTY (make_funcs crep_code) 0) + code_rel (mk_ctxt c FEMPTY (make_funcs crep_code) 0) (alist_to_fmap crep_code) - (fromAList (crep_to_loop$compile_prog crep_code)) + (fromAList (crep_to_loop$compile_prog c crep_code)) Proof rw [code_rel_def, mk_ctxt_def] >- fs [distinct_make_funcs] >> @@ -4103,7 +4321,7 @@ Proof “:'c”|-> “:num # num list # 'a prog”] EL_MAP2) >> disch_then (qspec_then ‘λn' (name,params,body). (n',GENLIST I (LENGTH params), - loop_live$optimise (comp_func (make_funcs crep_code) + loop_live$optimise (comp_func c (make_funcs crep_code) params body))’ mp_tac) >> strip_tac >> fs [] >> pop_assum kall_tac >> fs [] >> @@ -4118,8 +4336,8 @@ QED Theorem make_funcs_domain_compile_prog: - !start lc crep_code. FLOOKUP (make_funcs crep_code) start = SOME (lc,0) ==> - lc ∈ domain (fromAList (compile_prog crep_code)) + !start lc crep_code c. FLOOKUP (make_funcs crep_code) start = SOME (lc,0) ==> + lc ∈ domain (fromAList (compile_prog c crep_code)) Proof rw [] >> fs [domain_fromAList] >> @@ -4238,9 +4456,9 @@ Proof QED Theorem compile_prog_distinct_params: - ∀prog. + ∀prog c. EVERY (λ(name,params,body). ALL_DISTINCT params) prog ⇒ - EVERY (λ(name,params,body). ALL_DISTINCT params) (compile_prog prog) + EVERY (λ(name,params,body). ALL_DISTINCT params) (compile_prog c prog) Proof rw [] >> fs [EVERY_MEM] >> @@ -4262,14 +4480,14 @@ QED Theorem state_rel_imp_semantics: - !s t crep_code start prog lc. s.memaddrs = t.mdomain ∧ + !s t crep_code start prog lc c. s.memaddrs = t.mdomain ∧ s.be = t.be ∧ s.ffi = t.ffi ∧ s.base_addr = t.base_addr ∧ mem_rel (make_funcs crep_code) s.memory t.memory ∧ globals_rel (make_funcs crep_code) s.globals t.globals ∧ ALL_DISTINCT (MAP FST crep_code) ∧ s.code = alist_to_fmap crep_code ∧ - t.code = fromAList (crep_to_loop$compile_prog crep_code) ∧ + t.code = fromAList (crep_to_loop$compile_prog c crep_code) ∧ s.locals = FEMPTY ∧ ALOOKUP crep_code start = SOME ([],prog) ∧ FLOOKUP (make_funcs crep_code) start = SOME (lc, 0) ∧ @@ -4278,7 +4496,7 @@ Theorem state_rel_imp_semantics: Proof rw [] >> drule mk_ctxt_code_imp_code_rel >> - disch_then (qspecl_then [‘start’, ‘prog’] mp_tac) >> + disch_then (qspecl_then [‘c’,‘start’, ‘prog’] mp_tac) >> fs [] >> strip_tac >> qmatch_asmsub_abbrev_tac ‘code_rel nctxt _ _’ >> reverse (Cases_on ‘semantics s start’) >> fs [] @@ -5352,7 +5570,7 @@ QED (* first_name offset *) Theorem crep_to_loop_compile_prog_lab_min: - crep_to_loop$compile_prog cprog = lprog ⇒ + crep_to_loop$compile_prog c cprog = lprog ⇒ EVERY (λprog. 60 ≤ FST prog) lprog Proof gs[crep_to_loopTheory.compile_prog_def]>> diff --git a/pancake/proofs/loop_callProofScript.sml b/pancake/proofs/loop_callProofScript.sml index 0c41d7febe..892613fcc8 100644 --- a/pancake/proofs/loop_callProofScript.sml +++ b/pancake/proofs/loop_callProofScript.sml @@ -370,6 +370,16 @@ Proof fs [labels_in_def, lookup_def] QED +Theorem compile_Arith: + ^(get_goal "comp _ (loopLang$Arith _)") +Proof + rpt conj_tac >> + rpt gen_tac >> strip_tac >> + gvs [evaluate_def, labels_in_def, comp_def,AllCaseEqs(), + DefnBase.one_line_ify NONE loop_arith_def + ] >> + rw[set_var_def,lookup_insert,lookup_delete] +QED Theorem compile_others: ^(get_goal "comp _ loopLang$Skip") ∧ @@ -398,7 +408,7 @@ Proof match_mp_tac (the_ind_thm()) >> EVERY (map strip_assume_tac [compile_others,compile_LocValue,compile_LoadByte,compile_StoreByte, - compile_Mark, compile_Assign, compile_Store, + compile_Mark, compile_Assign, compile_Store, compile_Arith, compile_Call, compile_Seq, compile_If, compile_FFI, compile_Loop]) >> asm_rewrite_tac [] >> rw [] >> rpt (pop_assum kall_tac) QED diff --git a/pancake/proofs/loop_liveProofScript.sml b/pancake/proofs/loop_liveProofScript.sml index 8b555588da..5ec3f7dce4 100644 --- a/pancake/proofs/loop_liveProofScript.sml +++ b/pancake/proofs/loop_liveProofScript.sml @@ -192,7 +192,6 @@ Proof THEN1 fs [domain_insert,domain_union,EXTENSION] THEN1 fs [domain_insert,domain_union,EXTENSION] \\ TRY (rpt (pop_assum (qspec_then ‘l’ mp_tac)) \\ fs [] \\ NO_TAC) - \\ TRY (rpt (pop_assum (qspec_then ‘l'’ mp_tac)) \\ fs [] \\ NO_TAC) \\ Cases_on ‘exp’ \\ fs [] \\ simp_tac std_ss [domain_union] \\ rpt (pop_assum (fn th => once_rewrite_tac [th])) @@ -476,12 +475,25 @@ Proof \\ res_tac \\ fs [domain_lookup] QED +Theorem compile_Arith: + ^(get_goal "loopLang$Arith") +Proof + rpt strip_tac >> + gvs[evaluate_def, DefnBase.one_line_ify NONE loop_arith_def, + AllCaseEqs(),shrink_def,PULL_EXISTS, + subspt_lookup,lookup_inter_alt,domain_insert, + cut_state_def, domain_inter,arith_vars,SF DNF_ss + ] >> + rw[state_component_equality,set_var_def,lookup_insert] >> + rw[] >> gvs[] +QED + Theorem compile_correct: ^(compile_correct_tm()) Proof match_mp_tac (the_ind_thm()) \\ EVERY (map strip_assume_tac [compile_Skip, compile_Continue, - compile_Mark, compile_Return, compile_Assign, compile_Store, + compile_Mark, compile_Return, compile_Assign, compile_Store, compile_Arith, compile_Call, compile_Seq, compile_If, compile_FFI, compile_Loop]) \\ asm_rewrite_tac [] \\ rw [] \\ rpt (pop_assum kall_tac) QED diff --git a/pancake/proofs/loop_removeProofScript.sml b/pancake/proofs/loop_removeProofScript.sml index 31ed86cc00..29e08ad839 100644 --- a/pancake/proofs/loop_removeProofScript.sml +++ b/pancake/proofs/loop_removeProofScript.sml @@ -959,6 +959,16 @@ Proof \\ fs [call_env_def] QED +Theorem compile_Arith: + ^(get_goal "loopLang$Arith") +Proof + fs [syntax_ok_def,no_Loop_def,every_prog_def] \\ rpt strip_tac + \\ gvs[evaluate_def,AllCaseEqs(),DefnBase.one_line_ify NONE loop_arith_def, + comp_no_loop_def,PULL_EXISTS + ] + \\ gvs[state_rel_def,set_var_def,state_component_equality] \\ metis_tac[] +QED + Theorem compile_correct: ^(compile_correct_tm()) Proof @@ -966,7 +976,7 @@ Proof \\ EVERY (map strip_assume_tac [compile_Skip, compile_Continue, compile_Mark, compile_Return, compile_Assign, compile_Store, compile_SetGlobal, compile_Call, compile_Seq, compile_If, - compile_FFI, compile_Loop]) + compile_FFI, compile_Loop,compile_Arith]) \\ asm_rewrite_tac [] \\ rw [] \\ rpt (pop_assum kall_tac) QED diff --git a/pancake/proofs/loop_to_wordProofScript.sml b/pancake/proofs/loop_to_wordProofScript.sml index 531e7e26d2..29716de28f 100644 --- a/pancake/proofs/loop_to_wordProofScript.sml +++ b/pancake/proofs/loop_to_wordProofScript.sml @@ -977,6 +977,26 @@ Proof fs [mk_new_cutset_def] QED +Theorem compile_Arith: + ^(get_goal "loopLang$Arith") +Proof + rpt strip_tac >> + gvs [loopSemTheory.evaluate_def, + comp_def, evaluate_def,DefnBase.one_line_ify NONE loop_arith_def, + AllCaseEqs(),inst_def,PULL_EXISTS,get_vars_def,find_var_def,get_var_def, + loopSemTheory.set_var_def,wordSemTheory.set_var_def, + state_rel_def,SUBSET_DEF,loopLangTheory.acc_vars_def, + SF DNF_ss + ] >> + imp_res_tac locals_rel_intro >> + gvs[lookup_insert,lookup_insert,domain_lookup] >> + rw[] >> + gvs[locals_rel_def,lookup_insert] >> + rw[] >> + res_tac >> gvs[] >> rw[] >> + gvs[INJ_DEF,domain_lookup,PULL_EXISTS,find_var_def] +QED + Theorem compile_correct: ^(compile_correct_tm()) Proof @@ -984,7 +1004,7 @@ Proof >> EVERY (map strip_assume_tac [compile_Skip, compile_Raise, compile_Mark, compile_Return, compile_Assign, compile_Store, compile_SetGlobal, compile_Call, compile_Seq, compile_If, - compile_FFI, compile_Loop, compile_LoadByte]) + compile_FFI, compile_Loop, compile_LoadByte, compile_Arith]) >> asm_rewrite_tac [] >> rw [] >> rpt (pop_assum kall_tac) QED @@ -1721,6 +1741,7 @@ Proof ho_match_mp_tac loop_to_wordTheory.comp_ind>> rw[loop_to_wordTheory.comp_def]>> gs[wordPropsTheory.extract_labels_def] + >- gvs[AllCaseEqs(),extract_labels_def] >- (pairarg_tac>>gs[]>> pairarg_tac>>gs[]>> rveq>>gs[wordPropsTheory.extract_labels_def]>> @@ -1756,6 +1777,7 @@ Proof ho_match_mp_tac loop_to_wordTheory.comp_ind>> rw[loop_to_wordTheory.comp_def]>> gs[wordPropsTheory.extract_labels_def] + >- gvs[AllCaseEqs(),extract_labels_def] >- (pairarg_tac>>gs[]>> pairarg_tac>>gs[]>> rveq>>gs[wordPropsTheory.extract_labels_def]>> @@ -1802,6 +1824,7 @@ Proof ho_match_mp_tac loop_to_wordTheory.comp_ind>> rw[loop_to_wordTheory.comp_def]>> gs[wordPropsTheory.extract_labels_def] + >- gvs[AllCaseEqs(),extract_labels_def] >- (pairarg_tac>>gs[]>> pairarg_tac>>gs[]>> rveq>> @@ -1942,36 +1965,77 @@ Proof rename1 ‘SOME x’>>PairCases_on ‘x’>>gs[] QED +(* TODO: move to loopProps *) +Definition loop_inst_ok_def: + (loop_inst_ok c (Arith (LDiv r1 r2 r3)) ⇔ c.ISA ∈ {ARMv8; MIPS; RISC_V}) ∧ + (loop_inst_ok c (Arith (LLongMul r1 r2 r3 r4)) ⇔ + (c.ISA = ARMv7 ⇒ r1 ≠ r2) ∧ + (c.ISA = ARMv8 ∨ c.ISA = RISC_V ∨ c.ISA = Ag32 ⇒ r1 ≠ r3 ∧ r1 ≠ r4)) ∧ + (loop_inst_ok c (Arith (LLongDiv r1 r2 r3 r4 r5)) ⇔ c.ISA = x86_64) ∧ + (loop_inst_ok c _ ⇔ T) +End + Theorem loop_to_word_comp_every_inst_ok_less: ∀ctxt prog l. - byte_offset_ok c 0w ⇒ + byte_offset_ok c 0w ∧ every_prog (loop_inst_ok c) prog ∧ + domain(acc_vars prog LN) ⊆ domain ctxt ∧ + INJ (find_var ctxt) (domain ctxt) 𝕌(:num) ∧ + (∀n m. lookup n ctxt = SOME m ⇒ m ≠ 0) + ⇒ every_inst (inst_ok_less c) (FST (comp ctxt prog l)) Proof ho_match_mp_tac loop_to_wordTheory.comp_ind >> rw[loop_to_wordTheory.comp_def, wordPropsTheory.every_inst_def, - wordPropsTheory.inst_ok_less_def] >> + wordPropsTheory.inst_ok_less_def, + every_prog_def,DefnBase.one_line_ify NONE loop_inst_ok_def, + loopLangTheory.acc_vars_def + ] + >~ [‘loop_arith_CASE arith’] >- + (Cases_on ‘arith’ >> + gvs[every_inst_def,inst_ok_less_def] >> + rw[] >> + res_tac >> + fs[INJ_DEF] + >- (spose_not_then strip_assume_tac \\ res_tac \\ simp[]) >> + rename1 ‘_ ≠ find_var _ nm’ >> + Cases_on ‘nm ∈ domain ctxt’ >- metis_tac[] >> + fs[GSYM lookup_NONE_domain] >> + fs[find_var_def,domain_lookup] >> + metis_tac[SOME_11]) >> TRY (Cases_on ‘ret’>-gs[wordPropsTheory.every_inst_def]>> rename1 ‘SOME x’>>PairCases_on ‘x’>>gs[]>> Cases_on ‘handler’>-gs[wordPropsTheory.every_inst_def]>> rename1 ‘SOME x’>>PairCases_on ‘x’)>> gs[]>>rpt (pairarg_tac>>gs[])>> - gs[wordPropsTheory.every_inst_def] + gs[wordPropsTheory.every_inst_def, + PURE_ONCE_REWRITE_CONV [acc_vars_acc] “domain(acc_vars x (acc_vars y z))”, + PURE_ONCE_REWRITE_CONV [acc_vars_acc] “domain(acc_vars x (insert y () z))” + ] QED Theorem loop_to_word_comp_func_every_inst_ok_less: comp_func n params body = p ∧ + every_prog (loop_inst_ok c) body ∧ byte_offset_ok c 0w ⇒ every_inst (inst_ok_less c) p Proof strip_tac>>gs[loop_to_wordTheory.comp_func_def]>> rveq>> - drule_then irule loop_to_word_comp_every_inst_ok_less + drule_then irule loop_to_word_comp_every_inst_ok_less >> + assume_tac $ DECIDE “0 < 2:num” >> + dxrule locals_rel_mk_ctxt_ln >> + qmatch_goalsub_abbrev_tac ‘make_ctxt _ lista’ >> + disch_then $ qspecl_then [‘lista’] mp_tac >> + rw[locals_rel_def,Abbr ‘lista’,domain_make_ctxt] >> + rw[SUBSET_DEF,set_fromNumSet,domain_difference,domain_toNumSet] QED Theorem loop_to_word_compile_prog_every_inst_ok_less: compile_prog lprog = wprog0 ∧ - byte_offset_ok c 0w ⇒ + byte_offset_ok c 0w ∧ + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) lprog + ⇒ EVERY (λ(n,m,p). every_inst (inst_ok_less c) p) wprog0 Proof strip_tac>>gs[loop_to_wordTheory.compile_prog_def]>> @@ -1979,17 +2043,124 @@ Proof pairarg_tac>>gs[]>> pairarg_tac>>gs[]>> drule_then irule loop_to_word_comp_func_every_inst_ok_less>> - gs[] + gs[] >> + first_x_assum drule >> + simp[] +QED + +Triviality comp_with_loop_alt_ind = + loop_removeTheory.comp_with_loop_ind + |> PURE_REWRITE_RULE [METIS_PROVE [] “(a,b) = comp_with_loop x y z w ⇔ comp_with_loop x y z w = (a,b)”, + METIS_PROVE [] “(a,b) = store_cont x y z ⇔ store_cont x y z = (a,b)”]; + + +Triviality eq_forall_elim: + (∀x. y = x ⇒ P x) = P y +Proof + metis_tac[] +QED + +Theorem every_loop_inst_ok_comp_no_loop: + ∀p prog. + every_prog (loop_inst_ok c) prog ∧ + every_prog (loop_inst_ok c) (FST p) ∧ + every_prog (loop_inst_ok c) (SND p) + ⇒ + every_prog (loop_inst_ok c) (comp_no_loop p prog) +Proof + ho_match_mp_tac loop_removeTheory.comp_no_loop_ind \\ + rw[every_prog_def,loop_inst_ok_def, loop_removeTheory.comp_no_loop_def] \\ + Cases_on ‘handler’ \\ gvs[] \\ + PairCases_on ‘x’ \\ gvs[] +QED + +Theorem every_loop_inst_ok_comp: + ∀p prog cont s body n funs. + comp_with_loop p prog cont s = (body,n,funs) ∧ + every_prog (loop_inst_ok c) prog ∧ + every_prog (loop_inst_ok c) cont ∧ + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) (SND s) ∧ + every_prog (loop_inst_ok c) (FST p) ∧ + every_prog (loop_inst_ok c) (SND p) ⇒ + (every_prog (loop_inst_ok c) body ∧ + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) funs) +Proof + (* slow *) + ho_match_mp_tac comp_with_loop_alt_ind \\ + rw[loop_removeTheory.comp_with_loop_def,every_prog_def,loop_inst_ok_def] \\ + rpt(pairarg_tac \\ fs[] \\ rveq) + >~ [‘option_CASE’] (* handler case*) >- + (PRED_ASSUM is_forall (fn thm => + PRED_ASSUM is_forall (fn thm' => + fs[AllCaseEqs(),every_prog_def,loop_inst_ok_def] \\ + rpt(pairarg_tac \\ fs[]) \\ + gs[every_prog_def,loop_inst_ok_def,AllCaseEqs(), + DefnBase.one_line_ify NONE loop_removeTheory.store_cont_def] \\ + mp_tac thm \\ mp_tac thm')) \\ + rveq \\ gvs[DefnBase.one_line_ify NONE loop_removeTheory.store_cont_def, + every_prog_def,loop_inst_ok_def] \\ + metis_tac[FST,SND,PAIR]) + >~ [‘option_CASE’] (* handler case, snd conjunct*) >- + (PRED_ASSUM is_forall (fn thm => + PRED_ASSUM is_forall (fn thm' => + fs[AllCaseEqs(),every_prog_def,loop_inst_ok_def] \\ + rpt(pairarg_tac \\ fs[]) \\ + gs[every_prog_def,loop_inst_ok_def,AllCaseEqs(), + DefnBase.one_line_ify NONE loop_removeTheory.store_cont_def] \\ + mp_tac thm \\ mp_tac thm')) \\ + rveq \\ gvs[DefnBase.one_line_ify NONE loop_removeTheory.store_cont_def, + every_prog_def,loop_inst_ok_def] \\ + metis_tac[FST,SND,PAIR]) \\ + rpt $ PRED_ASSUM is_forall mp_tac \\ + gvs[AllCaseEqs(),every_prog_def,loop_inst_ok_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + gvs[every_prog_def,loop_inst_ok_def,AllCaseEqs(), + DefnBase.one_line_ify NONE loop_removeTheory.store_cont_def] \\ + metis_tac[FST,SND,PAIR,every_loop_inst_ok_comp_no_loop] +QED + +Theorem every_loop_inst_ok_comp: + every_prog (loop_inst_ok c) prog ∧ + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) (SND s) ∧ + comp (name,params,prog) s = (n,funs) ⇒ + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) funs +Proof + rw[loop_removeTheory.comp_def] \\ + pairarg_tac \\ gvs[] \\ + drule_then match_mp_tac every_loop_inst_ok_comp \\ + rw[every_prog_def,loop_inst_ok_def] +QED + +Theorem every_loop_inst_ok_comp_prog: + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) lprog ⇒ + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) (comp_prog lprog) +Proof + rw[loop_removeTheory.comp_prog_def,EVERY_MEM] \\ + qmatch_asmsub_abbrev_tac ‘FOLDR comp acc’ \\ + ‘EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) (SND acc)’ + by(rw[Abbr ‘acc’]) \\ + qhdtm_x_assum ‘Abbrev’ kall_tac \\ + rpt $ pop_assum mp_tac \\ + qid_spec_tac ‘acc’ \\ + Induct_on ‘lprog’ using SNOC_INDUCT + THEN1 rw[EVERY_MEM] \\ + rw[SF DNF_ss,FOLDR_SNOC] \\ + rpt(pairarg_tac \\ gvs[]) \\ + first_x_assum $ match_mp_tac o MP_CANON \\ + first_x_assum $ irule_at $ Pos hd \\ + match_mp_tac $ GEN_ALL every_loop_inst_ok_comp \\ + metis_tac[PAIR,FST,SND] QED Theorem loop_to_word_every_inst_ok_less: compile lprog = wprog0 ∧ - byte_offset_ok c 0w ⇒ + byte_offset_ok c 0w ∧ + EVERY (λ(n,params,body). every_prog (loop_inst_ok c) body) lprog ⇒ EVERY (λ(n,m,p). every_inst (inst_ok_less c) p) wprog0 Proof strip_tac>>gs[loop_to_wordTheory.compile_def]>> drule_then irule loop_to_word_compile_prog_every_inst_ok_less>> - gs[] + gs[every_loop_inst_ok_comp_prog] QED val _ = export_theory(); diff --git a/pancake/proofs/pan_simpProofScript.sml b/pancake/proofs/pan_simpProofScript.sml index b494380928..7271af750d 100644 --- a/pancake/proofs/pan_simpProofScript.sml +++ b/pancake/proofs/pan_simpProofScript.sml @@ -415,6 +415,12 @@ Proof rpt gen_tac >> strip_tac >> fs [OPT_MMAP_def] >> rewrite_tac [AND_IMP_INTRO] >> strip_tac >> rveq >> fs []) + >- ( + rename [‘eval s (Panop op es)’] >> + rw[eval_def] \\ + gvs[AllCaseEqs(),DefnBase.one_line_ify NONE pan_op_def,MAP_EQ_CONS,PULL_EXISTS, + pan_commonPropsTheory.opt_mmap_eq_some,SF DNF_ss] \\ + metis_tac[]) >- ( rpt gen_tac >> strip_tac >> fs [panSemTheory.eval_def] >> @@ -426,6 +432,24 @@ Proof fs [state_rel_def, state_component_equality] QED +(* TODO: move *) +Theorem OPT_MMAP_NONE: + OPT_MMAP f xs = NONE ⇒ + ∃x. MEM x xs ∧ f x = NONE +Proof + Induct_on ‘xs’ \\ rw[PULL_EXISTS] \\ + metis_tac[] +QED + +(* TODO: move *) +Theorem OPT_MMAP_NONE': + MEM x xs ∧ f x = NONE ⇒ OPT_MMAP f xs = NONE +Proof + Induct_on ‘xs’ \\ rw[PULL_EXISTS] + THEN1 metis_tac[] \\ + Cases_on ‘x = h’ \\ gvs[] \\ + Cases_on ‘f h’ \\ gvs[] +QED Theorem compile_eval_correct_none: ∀s e t. @@ -512,6 +536,34 @@ Proof fs [] >> imp_res_tac compile_eval_correct >> fs []) + >- ( + rename [‘eval s (Panop op es)’] >> + rw[eval_def] \\ + PURE_TOP_CASE_TAC + THEN1 (gvs[AllCaseEqs(),DefnBase.one_line_ify NONE pan_op_def,MAP_EQ_CONS,PULL_EXISTS, + SF DNF_ss] \\ + imp_res_tac OPT_MMAP_NONE \\ + gvs[] \\ + res_tac \\ + disj1_tac \\ + metis_tac[OPT_MMAP_NONE']) \\ + gvs[] \\ + strip_tac \\ + gvs[eval_def,AllCaseEqs()] + THEN1 (imp_res_tac OPT_MMAP_NONE \\ + fs[] \\ + metis_tac[NOT_NONE_SOME,OPT_MMAP_NONE']) \\ + qpat_x_assum ‘_ ⇒ _’ mp_tac \\ impl_keep_tac + THEN1 (gvs[EVERY_MEM] \\ + rw[] \\ + gvs[pan_commonPropsTheory.opt_mmap_eq_some,MAP_EQ_EVERY2,LIST_REL_EL_EQN,MEM_EL,PULL_EXISTS] \\ + res_tac \\ + drule_all_then strip_assume_tac compile_eval_correct \\ + gvs[]) \\ + imp_res_tac pan_commonPropsTheory.opt_mmap_length_eq \\ + rw[DefnBase.one_line_ify NONE pan_op_def,AllCaseEqs(),MAP_EQ_CONS,PULL_EXISTS] \\ + gvs[quantHeuristicsTheory.LIST_LENGTH_1,LENGTH_CONS] \\ + every_case_tac \\ gvs[]) >- ( rpt gen_tac >> strip_tac >> fs [panSemTheory.eval_def] >> diff --git a/pancake/proofs/pan_to_crepProofScript.sml b/pancake/proofs/pan_to_crepProofScript.sml index 81b21fa605..3ec925d544 100644 --- a/pancake/proofs/pan_to_crepProofScript.sml +++ b/pancake/proofs/pan_to_crepProofScript.sml @@ -316,6 +316,18 @@ Proof fs [] >> TOP_CASE_TAC >> fs [] >> TOP_CASE_TAC >> fs [v2word_def]) >> unabbrev_all_tac >> fs []) + >- ( + rename1 ‘Panop’ >> + rpt gen_tac >> strip_tac >> + gvs[compile_exp_def,AllCaseEqs(),eval_def,panLangTheory.size_of_shape_def, + panSemTheory.eval_def,crepSemTheory.eval_def,flatten_def,shape_of_def, + DefnBase.one_line_ify NONE pan_op_def,MAP_EQ_CONS,opt_mmap_eq_some, + cexp_heads_def,PULL_EXISTS, SF DNF_ss + ] >> + rpt $ qpat_x_assum ‘SOME _ = _’ $ assume_tac o GSYM >> + rpt $ first_x_assum $ drule_then $ drule_then $ drule_then drule >> + rpt $ disch_then $ resolve_then Any assume_tac $ GSYM PAIR >> + gvs[flatten_def,shape_of_def,DefnBase.one_line_ify NONE compile_panop_def,crep_op_def]) >- ( rpt gen_tac >> strip_tac >> fs [panSemTheory.eval_def] >> @@ -770,6 +782,19 @@ Proof qexists_tac ‘var_cexp y’ >> fs [] >> metis_tac []) >> fs []) + >- (rpt strip_tac >> + gvs[panSemTheory.eval_def,AllCaseEqs(), + DefnBase.one_line_ify NONE pan_op_def, + MAP_EQ_CONS,MEM_MAP,MEM_FLAT,compile_exp_def, + opt_mmap_eq_some,cexp_heads_def,PULL_EXISTS, + SF DNF_ss,var_cexp_def + ] >> + rpt $ first_x_assum $ resolve_then (Pat ‘_ = (_,_)’) assume_tac $ GSYM PAIR >> + rpt $ qpat_x_assum ‘SOME _ = _’ $ assume_tac o GSYM >> + rpt $ first_x_assum $ drule_then $ drule_then $ drule_then $ drule >> + rpt strip_tac >> + metis_tac[FST,MEM] + ) >- ( rpt gen_tac >> strip_tac >> fs [panSemTheory.eval_def, option_case_eq, v_case_eq, @@ -1657,6 +1682,16 @@ Proof impl_tac >- metis_tac [] >> impl_tac >- fs [] >> fs [EVERY_MEM]) + >- ( + rpt strip_tac >> + gvs[panSemTheory.eval_def,compile_exp_def,AllCaseEqs(),cexp_heads_def, + DefnBase.one_line_ify NONE pan_op_def,MAP_EQ_CONS,exps_def, + opt_mmap_eq_some, SF DNF_ss + ] >> + rpt $ first_x_assum $ resolve_then (Pos last) assume_tac $ GSYM PAIR >> + rpt $ qpat_x_assum ‘SOME _ = _’ $ assume_tac o GSYM >> + rpt $ first_x_assum $ drule_then $ drule_then $ drule_then drule >> + rw[] >> metis_tac[]) >- ( rpt gen_tac >> strip_tac >> fs [panSemTheory.eval_def, option_case_eq, v_case_eq, diff --git a/pancake/proofs/pan_to_targetProofScript.sml b/pancake/proofs/pan_to_targetProofScript.sml index 1b38d65dce..00d53bf3bd 100644 --- a/pancake/proofs/pan_to_targetProofScript.sml +++ b/pancake/proofs/pan_to_targetProofScript.sml @@ -18,13 +18,19 @@ Overload word_to_stack_compile[local] = ``word_to_stack$compile`` Overload stack_to_lab_compile[local] = ``stack_to_lab$compile`` Overload pan_to_word_compile_prog[local] = ``pan_to_word$compile_prog`` +Definition pancake_good_code_def: + pancake_good_code pan_code = + EVERY (λ(name,params,body). EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of body)) pan_code +End + Theorem pan_to_lab_good_code_lemma: compile c.stack_conf c.data_conf lim1 lim2 offs stack_prog = code ∧ compile asm_conf3 word_prog = (bm, wc, fs, stack_prog) ∧ word_to_word$compile word_conf asm_conf3 word_prog0 = (col, word_prog) ∧ - compile_prog pan_prog = word_prog0 ∧ + compile_prog asm_conf3.ISA pan_prog = word_prog0 ∧ stack_to_labProof$labels_ok code ∧ - all_enc_ok_pre conf code ⇒ + all_enc_ok_pre conf code + ⇒ lab_to_targetProof$good_code conf LN code Proof (* start of 'good_code' proof for initial compilation *) @@ -81,7 +87,7 @@ Proof QED Theorem pan_to_stack_first_ALL_DISTINCT: - pan_to_word_compile_prog pan_code = wprog0 ∧ + pan_to_word_compile_prog mc.target.config.ISA pan_code = wprog0 ∧ word_to_word_compile c.word_to_word_conf mc.target.config wprog0 = (col,wprog) ∧ word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧ ALL_DISTINCT (MAP FST pan_code) ⇒ @@ -98,11 +104,12 @@ Proof strip_tac>> gs[GSYM EVERY_MAP]>>EVAL_TAC>>gs[EVERY_MEM]>> rw[]>- (first_x_assum $ qspec_then ‘5’ assume_tac>>gs[])>> - first_x_assum $ qspec_then ‘6’ assume_tac>>gs[] + first_x_assum $ qspec_then ‘6’ assume_tac>>gs[]>> + metis_tac[FST,SND,PAIR] QED Theorem pan_to_stack_compile_lab_pres: - pan_to_word$compile_prog pan_code = wprog0 ∧ + pan_to_word$compile_prog mc.target.config.ISA pan_code = wprog0 ∧ word_to_word_compile c.word_to_word_conf mc.target.config wprog0 =(col,wprog) ∧ word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧ ALL_DISTINCT (MAP FST pan_code) ⇒ @@ -159,7 +166,7 @@ Proof QED Theorem pan_to_lab_labels_ok: - pan_to_word_compile_prog pan_code = wprog0 ∧ + pan_to_word_compile_prog mc.target.config.ISA pan_code = wprog0 ∧ word_to_word_compile c.word_to_word_conf mc.target.config wprog0 = (col,wprog) ∧ word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧ stack_to_lab_compile c.stack_conf c.data_conf max_heap sp mc.target.config.addr_offset p = lprog ∧ @@ -176,7 +183,7 @@ QED Theorem word_to_stack_good_code_lemma: word_to_word_compile c.word_to_word_conf mc.target.config - (pan_to_word_compile_prog pan_code) = (col,wprog) ∧ + (pan_to_word_compile_prog mc.target.config.ISA pan_code) = (col,wprog) ∧ word_to_stack_compile mc.target.config wprog = (bitmaps,c'',fs,p) ∧ LENGTH mc.target.config.avoid_regs + 13 ≤ mc.target.config.reg_count ∧ (* from backend_config_ok c *) @@ -187,7 +194,8 @@ Proof gs[stack_to_labProofTheory.good_code_def]>>strip_tac>> qmatch_asmsub_abbrev_tac ‘word_to_word_compile _ _ wprog0 = _’>> qpat_x_assum ‘Abbrev (wprog0 = _)’ (assume_tac o GSYM o REWRITE_RULE [markerTheory.Abbrev_def])>> - drule_all pan_to_stack_compile_lab_pres>>strip_tac>>gs[]>> + drule_at (Pat ‘word_to_word_compile _ _ _ = _’) pan_to_stack_compile_lab_pres>> + disch_then drule_all>>strip_tac>>gs[]>> drule backendProofTheory.compile_to_word_conventions2>> strip_tac>> drule pan_to_wordProofTheory.first_compile_prog_all_distinct>> @@ -829,6 +837,7 @@ QED (* new *) Theorem pan_to_target_compile_semantics: pan_to_target$compile_prog c pan_code = SOME (bytes, bitmaps, c') ∧ + pancake_good_code pan_code ∧ distinct_params pan_code ∧ consistent_labels s.memory pan_code ∧ ALL_DISTINCT (MAP FST pan_code) ∧ @@ -968,7 +977,7 @@ Proof qpat_assum ‘EVERY _ wprog’ $ irule_at Any>> rpt strip_tac>>pairarg_tac>>gs[]>> first_x_assum $ irule>> - irule pan_to_word_every_inst_ok_less>>metis_tac[])>> + irule pan_to_word_every_inst_ok_less>>metis_tac[pancake_good_code_def])>> gs[])>>gs[]>> first_assum $ irule_at Any>> qmatch_goalsub_abbrev_tac ‘labSem$semantics labst’>> @@ -1211,12 +1220,12 @@ Proof (* word_to_word *) drule (word_to_wordProofTheory.word_to_word_compile_semantics |> INST_TYPE [beta |-> “: num # 'a lab_to_target$config”])>> - disch_then (qspecl_then [‘wst’, ‘InitGlobals_location’, ‘wst with code := fromAList (pan_to_word_compile_prog pan_code)’] mp_tac)>> + disch_then (qspecl_then [‘wst’, ‘InitGlobals_location’, ‘wst with code := fromAList (pan_to_word_compile_prog mc.target.config.ISA pan_code)’] mp_tac)>> gs[]>> ‘gc_fun_const_ok wst.gc_fun ∧ - no_install_code (fromAList (pan_to_word_compile_prog pan_code)) ∧ - no_alloc_code (fromAList (pan_to_word_compile_prog pan_code)) ∧ - no_mt_code (fromAList (pan_to_word_compile_prog pan_code))’ + no_install_code (fromAList (pan_to_word_compile_prog mc.target.config.ISA pan_code)) ∧ + no_alloc_code (fromAList (pan_to_word_compile_prog mc.target.config.ISA pan_code)) ∧ + no_mt_code (fromAList (pan_to_word_compile_prog mc.target.config.ISA pan_code))’ by (conj_tac >- ( gs[Abbr ‘wst’, word_to_stackProofTheory.make_init_def]>> gs[stack_to_labProofTheory.full_make_init_def, @@ -1237,7 +1246,7 @@ Proof metis_tac[])>> irule pan_to_word_compile_prog_no_mt_code>> metis_tac[])>>gs[]>> - ‘ALL_DISTINCT (MAP FST (pan_to_word_compile_prog pan_code)) ∧ + ‘ALL_DISTINCT (MAP FST (pan_to_word_compile_prog mc.target.config.ISA pan_code)) ∧ wst.stack = [] ∧ wst.code = fromAList wprog ∧ lookup 0 wst.locals = SOME (Loc 1 0) ∧ wst = wst with code := wst.code’ @@ -1374,7 +1383,7 @@ Proof reverse conj_asm2_tac>-gs[ALOOKUP_MAP]>> gs[stack_removeTheory.init_stubs_def]>> mp_tac (GEN_ALL pan_to_wordProofTheory.pan_to_word_compile_prog_lab_min)>> - disch_then $ qspecl_then [‘wprog0’,‘pan_code’] mp_tac>> + disch_then $ qspecl_then [‘wprog0’,‘pan_code’,‘mc.target.config.ISA’] mp_tac>> impl_tac>- gs[Abbr ‘wprog0’]>> simp[GSYM EVERY_MAP]>> qpat_assum ‘MAP FST wprog = MAP FST _’ (fn h => PURE_REWRITE_TAC[GSYM h])>> @@ -1575,7 +1584,7 @@ Proof (* pan_to_word *) qpat_x_assum ‘lc + _ = _’ (SUBST_ALL_TAC o GSYM)>> - ‘(wst0 with memory := m0).code = fromAList (pan_to_word_compile_prog pan_code)’ + ‘(wst0 with memory := m0).code = fromAList (pan_to_word_compile_prog mc.target.config.ISA pan_code)’ by gs[Abbr ‘wst0’, wordSemTheory.state_component_equality]>> drule_at Any (INST_TYPE [beta|-> “:num # α lab_to_target$config”] pan_to_wordProofTheory.state_rel_imp_semantics)>>gs[]>> diff --git a/pancake/proofs/pan_to_wordProofScript.sml b/pancake/proofs/pan_to_wordProofScript.sml index 9b6e5ccef4..f49c538afe 100644 --- a/pancake/proofs/pan_to_wordProofScript.sml +++ b/pancake/proofs/pan_to_wordProofScript.sml @@ -35,12 +35,12 @@ Definition mk_mem_def: End Definition loop_state_def: - loop_state (s:('a,'ffi) crepSem$state) crep_code ck = + loop_state (s:('a,'ffi) crepSem$state) c crep_code ck = <| locals := LN; globals := FEMPTY; memory := mk_mem (make_funcs crep_code) s.memory; mdomain := s.memaddrs; - code := fromAList (crep_to_loop$compile_prog crep_code); + code := fromAList (crep_to_loop$compile_prog c crep_code); clock := ck; be := s.be; ffi := s.ffi; @@ -64,7 +64,7 @@ End Theorem first_compile_prog_all_distinct: !prog. ALL_DISTINCT (MAP FST prog) ==> - ALL_DISTINCT (MAP FST (pan_to_word$compile_prog prog)) + ALL_DISTINCT (MAP FST (pan_to_word$compile_prog c prog)) Proof rw [] >> fs [pan_to_wordTheory.compile_prog_def] >> @@ -381,7 +381,7 @@ Theorem state_rel_imp_semantics: ALOOKUP pan_code start = SOME ([],prog) ∧ lc < LENGTH pan_code ∧ EL lc pan_code = (start,[],prog) ∧ s.code = alist_to_fmap pan_code ∧ - t.code = fromAList (pan_to_word$compile_prog pan_code) ∧ + t.code = fromAList (pan_to_word$compile_prog c pan_code) ∧ s.locals = FEMPTY ∧ size_of_eids pan_code < dimword (:α) ∧ FDOM s.eshapes = FDOM ((get_eids pan_code):mlstring |-> 'a word) ∧ lookup 0 t.locals = SOME (Loc 1 0) /\ @@ -496,13 +496,13 @@ Proof fs []) >> fs [pan_simpTheory.compile_prog_def]) >> ‘cst.memaddrs = - (loop_state cst ccode t.clock).mdomain’ by + (loop_state cst c ccode t.clock).mdomain’ by fs [Abbr ‘ccode’, Abbr ‘pcode’, Abbr ‘cst’, Abbr ‘pst’, crep_state_def, loop_state_def] >> drule crep_to_loopProofTheory.state_rel_imp_semantics >> disch_then (qspecl_then [‘ccode’, ‘start’, ‘comp_func (make_funcs pcode) (get_eids pcode) [] (compile prog)’, - ‘lc+first_name’] mp_tac) >> + ‘lc+first_name’,‘c’] mp_tac) >> impl_tac >- ( fs [Abbr ‘ccode’, Abbr ‘pcode’, Abbr ‘pst’, Abbr ‘cst’, @@ -527,12 +527,12 @@ Proof strip_tac >> drule pan_to_crepProofTheory.first_compile_prog_all_distinct >> strip_tac >> - ‘st_rel lst t (compile_prog ccode)’ by ( + ‘st_rel lst t (compile_prog c ccode)’ by ( fs [st_rel_def] >> conj_tac >- ( fs [loop_removeProofTheory.state_rel_def] >> - qexists_tac ‘fromAList (comp_prog (compile_prog ccode))’ >> + qexists_tac ‘fromAList (comp_prog (compile_prog c ccode))’ >> fs [] >> rw [] >- ( fs [Abbr ‘lst’, loop_state_def] >> @@ -634,7 +634,7 @@ Proof fs []) >> drule fstate_rel_imp_semantics >> disch_then (qspecl_then [‘lc+first_name’, - ‘loop_live$optimise (comp_func (make_funcs ccode) [] cprog)’] mp_tac) >> + ‘loop_live$optimise (comp_func c (make_funcs ccode) [] cprog)’] mp_tac) >> impl_tac >- ( fs [Abbr ‘lst’, loop_state_def, @@ -726,7 +726,7 @@ QED (*** no_install/no_alloc/no_mt lemmas ***) Theorem pan_to_word_compile_prog_no_install_code: - compile_prog prog = prog' ⇒ + compile_prog c prog = prog' ⇒ no_install_code (fromAList prog') Proof gs[compile_prog_def]>>strip_tac>> @@ -734,7 +734,7 @@ Proof QED Theorem pan_to_word_compile_prog_no_alloc_code: - compile_prog prog = prog' ⇒ + compile_prog c prog = prog' ⇒ no_alloc_code (fromAList prog') Proof gs[compile_prog_def]>>strip_tac>> @@ -742,7 +742,7 @@ Proof QED Theorem pan_to_word_compile_prog_no_mt_code: - compile_prog prog = prog' ⇒ + compile_prog c prog = prog' ⇒ no_mt_code (fromAList prog') Proof gs[compile_prog_def]>>strip_tac>> @@ -752,7 +752,7 @@ QED (*** pan_to_word good_handlers ***) Theorem pan_to_word_good_handlers: - compile_prog prog = prog' ⇒ + compile_prog c prog = prog' ⇒ EVERY (λ(n,m,pp). good_handlers n pp) prog' Proof gs[compile_prog_def, @@ -764,7 +764,7 @@ QED (* lab_pres *) Theorem pan_to_word_compile_lab_pres: - pan_to_word$compile_prog prog = prog' ⇒ + pan_to_word$compile_prog c prog = prog' ⇒ EVERY (λ(n,m,p). (let @@ -781,7 +781,7 @@ QED (* first_name offset : lab_min *) Theorem pan_to_word_compile_prog_lab_min: - compile_prog pprog = wprog ⇒ + compile_prog c pprog = wprog ⇒ EVERY (λprog. 60 ≤ FST prog) wprog Proof gs[pan_to_wordTheory.compile_prog_def]>> @@ -792,13 +792,473 @@ QED (* inst_ok_less *) +Theorem every_inst_ok_loop_call: + ∀l prog. + every_prog (loop_inst_ok c) prog ⇒ + every_prog (loop_inst_ok c) (FST(loop_call$comp l prog)) +Proof + ho_match_mp_tac loop_callTheory.comp_ind \\ + rw[loopPropsTheory.every_prog_def,loop_callTheory.comp_def, + loop_inst_ok_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + rw[loopPropsTheory.every_prog_def,loop_callTheory.comp_def, + loop_inst_ok_def] \\ + every_case_tac \\ + rw[loopPropsTheory.every_prog_def,loop_callTheory.comp_def, + loop_inst_ok_def] +QED + +val prog = “prog:'a loopLang$prog” + +Theorem every_inst_ok_loop_live: + ∀prog. + every_prog (loop_inst_ok c) ^prog ⇒ + every_prog (loop_inst_ok c) (loop_live$comp prog) +Proof + rw[loop_liveTheory.comp_def] \\ + ‘(∀p prog q. every_prog (loop_inst_ok c) ^prog ⇒ every_prog (loop_inst_ok c) (FST $ shrink p prog q)) ∧ + (∀p q r prog. every_prog (loop_inst_ok c) ^prog ⇒ OPTION_ALL (every_prog (loop_inst_ok c) o FST) (fixedpoint p q r prog)) + ’ + by(pop_assum kall_tac \\ + ho_match_mp_tac loop_liveTheory.shrink_ind \\ rw[] \\ + gvs $ loopPropsTheory.every_prog_def::loop_inst_ok_def:: + butlast(CONJUNCTS loop_liveTheory.shrink_def) \\ + rpt(pairarg_tac \\ gvs[]) \\ + gvs $ loopPropsTheory.every_prog_def::loop_inst_ok_def:: + butlast(CONJUNCTS loop_liveTheory.shrink_def) \\ + rpt TOP_CASE_TAC \\ gvs[loopPropsTheory.every_prog_def,loop_inst_ok_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + gvs $ loopPropsTheory.every_prog_def::loop_inst_ok_def:: + butlast(CONJUNCTS loop_liveTheory.shrink_def) \\ + simp[Once loop_liveTheory.shrink_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + rw[]) \\ + ‘∀prog. every_prog (loop_inst_ok c) ^prog ⇒ + every_prog (loop_inst_ok c) (FST $ mark_all prog)’ + by(rpt $ pop_assum kall_tac \\ + ho_match_mp_tac loop_liveTheory.mark_all_ind \\ + rw[loopPropsTheory.every_prog_def,loop_inst_ok_def, + loop_liveTheory.mark_all_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + every_case_tac \\ + gvs[loopPropsTheory.every_prog_def,loop_inst_ok_def, + loop_liveTheory.mark_all_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + rw[loopPropsTheory.every_prog_def,loop_inst_ok_def, + loop_liveTheory.mark_all_def]) \\ + metis_tac[] +QED + +Theorem every_inst_ok_less_optimise: + every_prog (loop_inst_ok c) prog ⇒ + every_prog (loop_inst_ok c) (optimise prog) +Proof + rw[loop_liveTheory.optimise_def] \\ + metis_tac[every_inst_ok_loop_call,every_inst_ok_loop_live] +QED + +Theorem every_inst_ok_less_crep_to_loop_compile_exp: + (∀ctxt n ns (e:'a crepLang$exp). + ctxt.target = c.ISA ∧ + every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2) e + ⇒ + EVERY (every_prog (loop_inst_ok c)) (FST $ crep_to_loop$compile_exp ctxt n ns e)) ∧ + (∀ctxt n ns (es: 'a crepLang$exp list). + ctxt.target = c.ISA ∧ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) es + ⇒ + EVERY (every_prog (loop_inst_ok c)) (FST $ crep_to_loop$compile_exps ctxt n ns es)) +Proof + ho_match_mp_tac crep_to_loopTheory.compile_exp_ind \\ + rw $ [loopPropsTheory.every_prog_def,loop_inst_ok_def,crep_to_loopTheory.prog_if_def,crepPropsTheory.every_exp_def] @ butlast(CONJUNCTS crep_to_loopTheory.compile_exp_def) \\ + rpt(pairarg_tac \\ gvs[]) \\ + gvs[loopPropsTheory.every_prog_def,loop_inst_ok_def,crep_to_loopTheory.prog_if_def] + THEN1 (gvs[DefnBase.one_line_ify NONE crep_to_loopTheory.compile_crepop_def,AllCaseEqs(), + loopPropsTheory.every_prog_def,loop_inst_ok_def] \\ + rw[EVERY_MEM,MEM_MAPi] \\ + rw[loopPropsTheory.every_prog_def,loop_inst_ok_def] \\ + Cases_on ‘es’ \\ gvs[quantHeuristicsTheory.LIST_LENGTH_1, + crep_to_loopProofTheory.compile_exps_alt] \\ + rpt(pairarg_tac \\ gvs[]) \\ + metis_tac[EVERY_MEM]) + THEN1 (gvs[DefnBase.one_line_ify NONE crep_to_loopTheory.compile_crepop_def,AllCaseEqs(), + loopPropsTheory.every_prog_def,loop_inst_ok_def] \\ + rw[EVERY_MEM,MEM_MAPi] \\ + rw[loopPropsTheory.every_prog_def,loop_inst_ok_def] \\ + Cases_on ‘es’ \\ gvs[quantHeuristicsTheory.LIST_LENGTH_1, + crep_to_loopProofTheory.compile_exps_alt] \\ + rpt(pairarg_tac \\ gvs[]) \\ + metis_tac[EVERY_MEM]) \\ + Cases_on ‘es’ \\ + gvs[crep_to_loopProofTheory.compile_exps_alt] \\ + rpt(pairarg_tac \\ gvs[]) +QED + +Theorem every_prog_loop_inst_ok_nested_seq: + ∀c ps. + every_prog (loop_inst_ok c) $ nested_seq ps = EVERY (every_prog (loop_inst_ok c)) ps +Proof + strip_tac \\ Induct \\ + gvs[loopPropsTheory.every_prog_def,loopLangTheory.nested_seq_def, + loop_to_wordProofTheory.loop_inst_ok_def] +QED + +Theorem every_inst_ok_less_crep_to_loop_compile: + ∀ctxt ns body. + ctxt.target = c.ISA ∧ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) (exps_of body) + ⇒ + every_prog (loop_inst_ok c) (crep_to_loop$compile ctxt ns body) +Proof + ho_match_mp_tac crep_to_loopTheory.compile_ind \\ + rw[loopPropsTheory.every_prog_def,loop_inst_ok_def, + crep_to_loopTheory.compile_def,crepPropsTheory.exps_of_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + gvs[loopPropsTheory.every_prog_def,loop_inst_ok_def, + crep_to_loopTheory.compile_def, + every_prog_loop_inst_ok_nested_seq] \\ + gvs[EVERY_APPEND,loopPropsTheory.every_prog_def,loop_inst_ok_def, + crep_to_loopTheory.compile_def] + >~ [‘MAP2’] >- + (drule $ cj 2 every_inst_ok_less_crep_to_loop_compile_exp \\ + disch_then $ qspecl_then [‘ctxt.vmax + 1’,‘ns’,‘es ++ [e]’] mp_tac \\ + rw[MAP2_ZIP,EVERY_MEM,crep_to_loopTheory.gen_temps_def,MEM_MAP,MEM_ZIP,PULL_EXISTS, + loopPropsTheory.every_prog_def,loop_inst_ok_def + ]) + >~ [‘MAP2’] >- + (conj_asm1_tac + >- (drule $ cj 2 every_inst_ok_less_crep_to_loop_compile_exp \\ + disch_then $ qspecl_then [‘ctxt.vmax + 1’,‘ns’,‘es ++ [e]’] mp_tac \\ + Cases_on ‘hdl’ \\ + rw[MAP2_ZIP,EVERY_MEM,crep_to_loopTheory.gen_temps_def,MEM_MAP,MEM_ZIP,PULL_EXISTS, + loopPropsTheory.every_prog_def,loop_inst_ok_def + ] \\ + gvs[crepPropsTheory.exps_of_def,EVERY_MEM] \\ + rename1 ‘SOME (_,_,SOME xx)’ \\ Cases_on ‘xx’ \\ + gvs[crepPropsTheory.exps_of_def,EVERY_MEM]) \\ + rpt(PURE_TOP_CASE_TAC \\ gvs[]) \\ + gvs[loopPropsTheory.every_prog_def,loop_inst_ok_def, + crep_to_loopTheory.compile_def, + every_prog_loop_inst_ok_nested_seq, + crepPropsTheory.exps_of_def + ]) \\ + imp_res_tac (cj 1 every_inst_ok_less_crep_to_loop_compile_exp) \\ + every_case_tac \\ + gvs[loopPropsTheory.every_prog_def,loopLangTheory.nested_seq_def, + loop_to_wordProofTheory.loop_inst_ok_def, + every_prog_loop_inst_ok_nested_seq] \\ + metis_tac[FST,SND,PAIR] +QED + +Theorem every_inst_ok_less_comp_func: + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) (exps_of body) ⇒ + every_prog (loop_inst_ok c) (comp_func c.ISA (crep_to_loop$make_funcs prog) params body) +Proof + rw[crep_to_loopTheory.comp_func_def,crep_to_loopTheory.make_funcs_def] \\ + match_mp_tac every_inst_ok_less_crep_to_loop_compile \\ + rw[crep_to_loopTheory.mk_ctxt_def] +QED + +Theorem every_inst_ok_nested_decs: + ∀ns ps p. + LENGTH ns = LENGTH ps ⇒ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) (exps_of(nested_decs ns ps p)) = + (EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) ps ∧ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) (exps_of p)) +Proof + ho_match_mp_tac crepLangTheory.nested_decs_ind \\ + rw[crepLangTheory.nested_decs_def,crepPropsTheory.exps_of_def] \\ + metis_tac[] +QED + +Theorem every_inst_ok_less_pan_to_crep_comp_field: + ∀index shapes es es' sh. + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) es ∧ + comp_field index shapes es = (es',sh) ⇒ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) es' +Proof + Induct_on ‘shapes’ \\ + rw[pan_to_crepTheory.comp_field_def,crepPropsTheory.every_exp_def,EVERY_TAKE] >> + res_tac >> + gvs[EVERY_DROP,EVERY_TAKE] +QED + +Theorem every_inst_ok_less_pan_to_crep_load_shape: + ∀w n e. + every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2) e ⇒ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) + (load_shape w n e) +Proof + Induct_on ‘n’ \\ + rw[crepLangTheory.load_shape_def,crepPropsTheory.every_exp_def] +QED + +Theorem every_inst_ok_less_pan_to_crep_cexp_heads: + ∀ces es. + EVERY (EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2))) ces ∧ + cexp_heads ces = SOME es + ⇒ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) es +Proof + Induct_on ‘ces’ \\ + rw[pan_to_crepTheory.cexp_heads_def] \\ + gvs[AllCaseEqs()] +QED + +Theorem every_inst_ok_less_pan_to_crep_compile_exp: + ∀ctxt e es sh. + every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2) e ∧ + compile_exp ctxt e = (es,sh) ⇒ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) es +Proof + ho_match_mp_tac pan_to_crepTheory.compile_exp_ind \\ + rw[pan_to_crepTheory.compile_exp_def, + crepPropsTheory.every_exp_def, + panPropsTheory.every_exp_def + ] \\ + gvs[crepPropsTheory.every_exp_def, + panPropsTheory.every_exp_def, + AllCaseEqs(),EVERY_MAP,EVERY_FLAT] \\ + rpt(pairarg_tac \\ gvs[]) \\ + gvs[AllCaseEqs(),crepPropsTheory.every_exp_def, + panPropsTheory.every_exp_def] \\ + imp_res_tac every_inst_ok_less_pan_to_crep_comp_field \\ + imp_res_tac every_inst_ok_less_pan_to_crep_load_shape + >~ [‘cexp_heads’] >- + (drule_at (Pos last) every_inst_ok_less_pan_to_crep_cexp_heads \\ + reverse impl_tac >- metis_tac[] \\ + gvs[EVERY_MEM,MEM_MAP,PULL_EXISTS] \\ + metis_tac[FST,SND,PAIR]) + >~ [‘cexp_heads’] >- + (drule_at (Pos last) every_inst_ok_less_pan_to_crep_cexp_heads \\ + impl_keep_tac >- + (gvs[EVERY_MEM,MEM_MAP,PULL_EXISTS] \\ + metis_tac[FST,SND,PAIR]) \\ + reverse $ rw[] + >- metis_tac[ETA_AX] \\ + gvs[crepPropsTheory.cexp_heads_simp_def,pan_to_crepProofTheory.cexp_heads_eq]) \\ + gvs[EVERY_MEM,PULL_FORALL] \\ + gvs[EVERY_MAP,MEM_MAP,PULL_FORALL] \\ + metis_tac[FST,SND,PAIR,EVERY_DEF,MEM] +QED + +Theorem every_inst_ok_less_exps_of_nested_seq: + ∀es. + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) + (exps_of (nested_seq es)) = + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) + (FLAT (MAP exps_of es)) +Proof + Induct \\ + gvs[crepLangTheory.nested_seq_def,crepPropsTheory.exps_of_def] +QED + + +Theorem every_inst_ok_less_stores: + ∀e es a. + EVERY + (λx. EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) + (exps_of x)) + (stores e es a) ⇔ + (es ≠ [] ⇒ every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2) e) ∧ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) es +Proof + Induct_on ‘es’ \\ + rw[crepLangTheory.stores_def,crepPropsTheory.exps_of_def,crepPropsTheory.every_exp_def] \\ + metis_tac[] +QED + +Theorem every_inst_ok_less_store_globals: + ∀w es. + EVERY + (λx. EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) + (exps_of x)) + (store_globals w es) ⇔ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) es +Proof + Induct_on ‘es’ \\ + rw[crepLangTheory.store_globals_def,crepPropsTheory.exps_of_def,crepPropsTheory.every_exp_def] +QED + +Theorem load_globals_alt: + ∀ad n. load_globals ad n = + GENLIST (λn. LoadGlob $ ad + n2w n) n +Proof + Induct_on ‘n’ \\ rw[crepLangTheory.load_globals_def,GENLIST_CONS,o_DEF,n2w_SUC] +QED + +Theorem every_inst_ok_less_pan_to_crep_compile: + ∀ctxt body e. + EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of body) ⇒ + EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) (exps_of(pan_to_crep$compile ctxt body)) +Proof + ho_match_mp_tac pan_to_crepTheory.compile_ind \\ + rw[panPropsTheory.exps_of_def,pan_to_crepTheory.compile_def, + crepPropsTheory.exps_of_def] \\ + rpt(pairarg_tac \\ gvs[]) \\ + rw[every_inst_ok_nested_decs,crepPropsTheory.exps_of_def] \\ + rpt(PURE_FULL_CASE_TAC \\ gvs[]) \\ + gvs[panPropsTheory.exps_of_def,pan_to_crepTheory.compile_def, + crepPropsTheory.exps_of_def,every_inst_ok_less_exps_of_nested_seq, + EVERY_FLAT,EVERY_MAP,every_inst_ok_nested_decs,every_inst_ok_less_stores, + every_inst_ok_less_store_globals + ] \\ + imp_res_tac every_inst_ok_less_pan_to_crep_compile_exp + >~ [‘ret_hdl’] >- + (gvs[] \\ + conj_tac >- + (gvs[EVERY_MEM,PULL_FORALL] \\ + metis_tac[every_inst_ok_less_pan_to_crep_compile_exp,EVERY_MEM,FST,SND,PAIR]) \\ + simp[DefnBase.one_line_ify NONE pan_to_crepTheory.ret_hdl_def] \\ + PURE_TOP_CASE_TAC \\ rw[crepPropsTheory.exps_of_def,crepLangTheory.assign_ret_def] \\ + rw[every_inst_ok_less_exps_of_nested_seq,EVERY_FLAT,EVERY_MAP,load_globals_alt,MAP2_MAP,MEM_ZIP] \\ + gvs[EVERY_MEM,MEM_ZIP,PULL_EXISTS,PULL_FORALL,crepPropsTheory.exps_of_def, + crepPropsTheory.every_exp_def]) + >~ [‘ret_hdl’] >- + (gvs[] \\ + conj_tac >- + (gvs[EVERY_MEM,PULL_FORALL] \\ + metis_tac[every_inst_ok_less_pan_to_crep_compile_exp,EVERY_MEM,FST,SND,PAIR]) \\ + simp[DefnBase.one_line_ify NONE pan_to_crepTheory.ret_hdl_def] \\ + PURE_TOP_CASE_TAC \\ rw[crepPropsTheory.exps_of_def,crepLangTheory.assign_ret_def] \\ + rw[every_inst_ok_less_exps_of_nested_seq,EVERY_FLAT,EVERY_MAP,load_globals_alt,MAP2_MAP,MEM_ZIP] \\ + gvs[EVERY_MEM,MEM_ZIP,PULL_EXISTS,PULL_FORALL,crepPropsTheory.exps_of_def, + crepPropsTheory.every_exp_def]) + >~ [‘exp_hdl’] >- + (gvs[] \\ + conj_tac >- + (gvs[EVERY_MEM,PULL_FORALL] \\ + metis_tac[every_inst_ok_less_pan_to_crep_compile_exp,EVERY_MEM,FST,SND,PAIR]) \\ + simp[DefnBase.one_line_ify NONE pan_to_crepTheory.exp_hdl_def] \\ + rpt(PURE_TOP_CASE_TAC \\ gvs[]) \\ rw[crepPropsTheory.exps_of_def,crepLangTheory.assign_ret_def] \\ + rw[every_inst_ok_less_exps_of_nested_seq,EVERY_FLAT,EVERY_MAP,load_globals_alt,MAP2_MAP,MEM_ZIP] \\ + gvs[EVERY_MEM,MEM_ZIP,PULL_EXISTS,PULL_FORALL,crepPropsTheory.exps_of_def, + crepPropsTheory.every_exp_def]) + >~ [‘exp_hdl’] >- + (gvs[] \\ + rpt conj_tac >- + (gvs[EVERY_MEM,PULL_FORALL] \\ + metis_tac[every_inst_ok_less_pan_to_crep_compile_exp,EVERY_MEM,FST,SND,PAIR]) \\ + simp[DefnBase.one_line_ify NONE pan_to_crepTheory.exp_hdl_def, + DefnBase.one_line_ify NONE pan_to_crepTheory.ret_hdl_def] \\ + rpt(PURE_TOP_CASE_TAC \\ gvs[]) \\ rw[crepPropsTheory.exps_of_def,crepLangTheory.assign_ret_def] \\ + rw[every_inst_ok_less_exps_of_nested_seq,EVERY_FLAT,EVERY_MAP,load_globals_alt,MAP2_MAP,MEM_ZIP] \\ + gvs[EVERY_MEM,MEM_ZIP,PULL_EXISTS,PULL_FORALL,crepPropsTheory.exps_of_def, + crepPropsTheory.every_exp_def]) \\ + rw[EVERY_MEM,MAP2_MAP,MEM_ZIP,MEM_MAP,UNCURRY_DEF] \\ + gvs[UNCURRY_DEF,crepPropsTheory.exps_of_def,EVERY_MEM,MEM_EL,PULL_EXISTS,EL_MAP, + crepPropsTheory.every_exp_def,DefnBase.one_line_ify NONE pan_to_crepTheory.ret_hdl_def] \\ + metis_tac[every_inst_ok_less_pan_to_crep_compile_exp,MEM_EL,EVERY_MEM, + FST,SND,PAIR] +QED + +Theorem every_inst_ok_less_pan_to_crep_compile_prog: + EVERY (λ(name,params,body). EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of body)) pan_code ⇒ + EVERY (λ(name,params,body). EVERY (every_exp (λx. ∀op es. x = Crepop op es ⇒ LENGTH es = 2)) (exps_of body)) (pan_to_crep$compile_prog pan_code) +Proof + rw[EVERY_MEM] \\ pairarg_tac \\ + gvs[pan_to_crepTheory.compile_prog_def,MEM_MAP] \\ + pairarg_tac \\ gvs[] \\ + pairarg_tac \\ gvs[] \\ + first_x_assum drule \\ + rw[pan_to_crepTheory.comp_func_def] \\ + match_mp_tac $ MP_CANON $ Ho_Rewrite.REWRITE_RULE [EVERY_MEM,PULL_EXISTS,PULL_FORALL] every_inst_ok_less_pan_to_crep_compile \\ + metis_tac[] +QED + +Theorem every_inst_ok_less_ret_to_tail: + ∀p. + EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of $ ret_to_tail p) ⇔ + EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of p) +Proof + ho_match_mp_tac pan_simpTheory.ret_to_tail_ind \\ + rw[panPropsTheory.exps_of_def,pan_simpTheory.compile_def, + pan_simpTheory.ret_to_tail_def,pan_simpTheory.seq_assoc_def, + panPropsTheory.every_exp_def, + pan_simpTheory.seq_call_ret_def] \\ + rpt(PURE_TOP_CASE_TAC \\ gvs[]) \\ + gvs[panPropsTheory.exps_of_def,pan_simpTheory.compile_def, + pan_simpTheory.ret_to_tail_def,pan_simpTheory.seq_assoc_def, + panPropsTheory.every_exp_def, + pan_simpTheory.seq_call_ret_def] \\ + metis_tac[] +QED + +Theorem every_inst_ok_less_seq_assoc: + ∀p q. + EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of $ seq_assoc p q) ⇔ + EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of p ++ exps_of q) +Proof + ho_match_mp_tac pan_simpTheory.seq_assoc_ind \\ + rw[panPropsTheory.exps_of_def,pan_simpTheory.compile_def, + pan_simpTheory.seq_assoc_def,pan_simpTheory.seq_assoc_def, + panPropsTheory.every_exp_def, + pan_simpTheory.seq_call_ret_def] \\ + rpt(PURE_TOP_CASE_TAC \\ gvs[]) \\ + gvs[panPropsTheory.exps_of_def,pan_simpTheory.compile_def, + pan_simpTheory.seq_assoc_def,pan_simpTheory.seq_assoc_def, + panPropsTheory.every_exp_def, + pan_simpTheory.seq_call_ret_def] \\ + metis_tac[] +QED + +Theorem every_inst_ok_less_pan_simp_compile: + ∀body. + EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of body) ⇒ + EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of(compile body)) +Proof + Induct \\ + gvs[panPropsTheory.exps_of_def,pan_simpTheory.compile_def, + pan_simpTheory.ret_to_tail_def,pan_simpTheory.seq_assoc_def, + every_inst_ok_less_ret_to_tail, + every_inst_ok_less_seq_assoc] +QED + +Theorem every_inst_ok_less_pan_simp_compile_prog: + EVERY (λ(name,params,body). EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of body)) pan_code ⇒ + EVERY (λ(name,params,body). EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of body)) (pan_simp$compile_prog pan_code) +Proof + rw[pan_simpTheory.compile_prog_def,EVERY_MAP] >> + gvs[EVERY_MEM] >> + rw[] >> + first_x_assum dxrule >> + pairarg_tac >> + rw[]>> + metis_tac[every_inst_ok_less_pan_simp_compile,EVERY_MEM] +QED + Theorem pan_to_word_every_inst_ok_less: - pan_to_word$compile_prog pan_code = wprog0 ∧ - byte_offset_ok c 0w ⇒ + pan_to_word$compile_prog c.ISA pan_code = wprog0 ∧ + byte_offset_ok c 0w ∧ + EVERY (λ(name,params,body). EVERY (every_exp (λx. ∀op es. x = Panop op es ⇒ LENGTH es = 2)) (exps_of body)) pan_code + ⇒ EVERY (λ(n,m,p). every_inst (inst_ok_less c) p) wprog0 Proof gs[pan_to_wordTheory.compile_prog_def]>>strip_tac>> - drule_then irule loop_to_word_every_inst_ok_less>>gs[] + drule_then irule loop_to_word_every_inst_ok_less>>gs[]>> + last_x_assum kall_tac>> + simp[crep_to_loopTheory.compile_prog_def,EVERY_MEM]>> + dep_rewrite.DEP_ONCE_REWRITE_TAC [MAP2_ZIP]>>simp[]>> + rw[MEM_MAP,MEM_ZIP]>> + rpt(pairarg_tac>>gvs[])>> + match_mp_tac every_inst_ok_less_optimise>> + match_mp_tac every_inst_ok_less_comp_func>> + rw[EVERY_MEM,MEM_EL]>> + drule_at (Pos last) $ MP_CANON $ SIMP_RULE std_ss [MEM_EL,EVERY_MEM,PULL_EXISTS,PULL_FORALL] every_inst_ok_less_pan_to_crep_compile_prog>> + simp[] >> + disch_then $ match_mp_tac o MP_CANON>> + rw[] >> + pairarg_tac>> + rw[]>> + drule_at (Pos last) $ MP_CANON $ SIMP_RULE std_ss [MEM_EL,EVERY_MEM,PULL_EXISTS,PULL_FORALL] every_inst_ok_less_pan_simp_compile_prog>> + simp[]>> + disch_then $ match_mp_tac o MP_CANON>> + rw[]>> + pairarg_tac >> + rw[]>> + gvs[EVERY_MEM,MEM_EL,PULL_EXISTS]>> + first_x_assum dxrule>> + simp[] QED val _ = export_theory(); diff --git a/pancake/semantics/crepPropsScript.sml b/pancake/semantics/crepPropsScript.sml index 643d78ecc2..122c4b7b1b 100644 --- a/pancake/semantics/crepPropsScript.sml +++ b/pancake/semantics/crepPropsScript.sml @@ -171,7 +171,14 @@ Proof MAP_EQ_EVERY2, LIST_REL_EL_EQN] >> rw [] >> fs [MEM_FLAT, MEM_MAP] >> - metis_tac [EL_MEM]) >> + metis_tac [EL_MEM]) + >- ( + rpt gen_tac >> + strip_tac >> + gvs [var_cexp_def, eval_def, AllCaseEqs(),opt_mmap_eq_some,SF DNF_ss, + DefnBase.one_line_ify NONE crep_op_def,MAP_EQ_CONS,MEM_FLAT,MEM_MAP,PULL_EXISTS] >> + metis_tac[] + ) >> rpt gen_tac >> rpt strip_tac >> fs [var_cexp_def, ETA_AX] >> fs [eval_def, CaseEq "option", CaseEq "word_lab"] >> @@ -221,7 +228,16 @@ Proof rw[]\\ gvs[var_cexp_def,MEM_MAP,MEM_FLAT] \\ first_x_assum(match_mp_tac o MP_CANON) \\ - metis_tac[]) \\ + metis_tac[]) + >- ( + rpt strip_tac >> + gvs[eval_def,var_cexp_def,MEM_FLAT,MEM_MAP] >> + qmatch_goalsub_abbrev_tac ‘option_CASE a1 _ _ = option_CASE a2 _ _’ >> + ‘a1 = a2’ suffices_by simp[] >> + unabbrev_all_tac >> + match_mp_tac OPT_MMAP_cong >> + rw[] >> + metis_tac[]) >> rpt gen_tac >> rpt strip_tac >> fs [var_cexp_def, ETA_AX] >> fs [eval_def, CaseEq "option", CaseEq "word_lab"] >> @@ -646,7 +662,6 @@ Proof fs [eval_def, CaseEq "option", CaseEq "word_lab"] >> rveq >> metis_tac []) >- fs [exps_def, eval_def, CaseEq "option"] - >- ( rpt gen_tac >> strip_tac >> fs [exps_def, ETA_AX] >> @@ -656,7 +671,16 @@ Proof MAP_EQ_EVERY2, LIST_REL_EL_EQN] >> rw [] >> fs [MEM_FLAT, MEM_MAP] >> - metis_tac [EL_MEM]) >> + metis_tac [EL_MEM]) + >- ( + rpt gen_tac >> + strip_tac >> + gvs [exps_def, eval_def, AllCaseEqs(),opt_mmap_eq_some,SF DNF_ss, + MAP_EQ_CONS,MEM_FLAT,MEM_MAP,PULL_EXISTS] >> + first_x_assum $ irule_at $ Pos last >> + simp[] >> + gvs[MAP_EQ_EVERY2,LIST_REL_EL_EQN] >> + metis_tac[EL_MEM]) >> rpt gen_tac >> rpt strip_tac >> fs [exps_def, ETA_AX] >> fs [eval_def, CaseEq "option", CaseEq "word_lab"] >> @@ -819,21 +843,14 @@ Proof TRY ( fs [eval_def, var_cexp_def] >> FULL_CASE_TAC >> fs [] >> NO_TAC) - >- ( - fs [var_cexp_def, ETA_AX] >> - fs [eval_def] >> - FULL_CASE_TAC >> fs [ETA_AX] >> rveq >> - pop_assum kall_tac >> pop_assum kall_tac >> - rpt (pop_assum mp_tac) >> - MAP_EVERY qid_spec_tac [`n`,`x`,`s`, `es`] >> - Induct >- rw [] >> - rpt gen_tac >> - rpt strip_tac >> - fs [OPT_MMAP_def] >> rveq >> fs [] >> - last_x_assum (qspecl_then [‘s’, ‘t’, ‘n’] mp_tac) >> - fs [] >> - impl_tac >- metis_tac [] >> - fs []) >> + >- (gvs [var_cexp_def,MEM_FLAT,MEM_MAP,eval_def,AllCaseEqs(),opt_mmap_eq_some, + MAP_EQ_EVERY2, LIST_REL_EL_EQN] >> + first_x_assum $ drule_then match_mp_tac >> + metis_tac[MEM_EL]) + >- (gvs [var_cexp_def,MEM_FLAT,MEM_MAP,eval_def,AllCaseEqs(),opt_mmap_eq_some, + MAP_EQ_EVERY2, LIST_REL_EL_EQN] >> + first_x_assum $ drule_then match_mp_tac >> + metis_tac[MEM_EL]) >> fs [var_cexp_def, eval_def] >> every_case_tac >> fs [] QED @@ -1248,5 +1265,40 @@ Proof fs [] QED +Definition exps_of_def: + (exps_of (Dec _ e p) = e::exps_of p) ∧ + (exps_of (Seq p q) = exps_of p ++ exps_of q) ∧ + (exps_of (If e p q) = e::exps_of p ++ exps_of q) ∧ + (exps_of (While e p) = e::exps_of p) ∧ + (exps_of (Call NONE e es) = e::es) ∧ + (exps_of (Call (SOME (_,p,NONE)) e es) = e::es++exps_of p) ∧ + (exps_of (Call (SOME (_,p,SOME(_,p'))) e es) = e::es++exps_of p++exps_of p') ∧ + (exps_of (Store e1 e2) = [e1;e2]) ∧ + (exps_of (StoreByte e1 e2) = [e1;e2]) ∧ + (exps_of (StoreGlob _ e) = [e]) ∧ + (exps_of (Return e) = [e]) ∧ + (exps_of (Assign _ e) = [e]) ∧ + (exps_of _ = []) +End + +Definition every_exp_def: + (every_exp P (crepLang$Const w) = P(Const w)) ∧ + (every_exp P (Var v) = P(Var v)) ∧ + (every_exp P (Label f) = P(Label f)) ∧ + (every_exp P (Load e) = (P(Load e) ∧ every_exp P e)) ∧ + (every_exp P (LoadByte e) = (P(LoadByte e) ∧ every_exp P e)) ∧ + (every_exp P (LoadGlob w) = (P(LoadGlob w))) ∧ + (every_exp P (Op bop es) = (P(Op bop es) ∧ EVERY (every_exp P) es)) ∧ + (every_exp P (Crepop op es) = (P(Crepop op es) ∧ EVERY (every_exp P) es)) ∧ + (every_exp P (Cmp c e1 e2) = (P(Cmp c e1 e2) ∧ every_exp P e1 ∧ every_exp P e2)) ∧ + (every_exp P (Shift sh e num) = (P(Shift sh e num) ∧ every_exp P e)) ∧ + (every_exp P (BaseAddr) = P BaseAddr) +Termination + wf_rel_tac `measure (exp_size ARB o SND)` >> + rpt strip_tac >> + imp_res_tac MEM_IMP_exp_size >> + TRY (first_x_assum (assume_tac o Q.SPEC `ARB`)) >> + decide_tac +End val _ = export_theory(); diff --git a/pancake/semantics/crepSemScript.sml b/pancake/semantics/crepSemScript.sml index 0822307bc8..21b96e2a11 100644 --- a/pancake/semantics/crepSemScript.sml +++ b/pancake/semantics/crepSemScript.sml @@ -82,6 +82,11 @@ Definition lookup_code_def: | _ => NONE End +Definition crep_op_def: + crep_op crepLang$Mul [w1:'a word;w2] = SOME(w1 * w2) ∧ + crep_op _ _ = NONE +End + Definition eval_def: (eval (s:('a,'ffi) crepSem$state) ((Const w):'a crepLang$exp) = SOME (Word w)) ∧ (eval s (Var v) = FLOOKUP s.locals v) ∧ @@ -108,6 +113,13 @@ Definition eval_def: then OPTION_MAP Word (word_op op (MAP (\w. case w of Word n => n) ws)) else NONE | _ => NONE) /\ + (eval s (Crepop op es) = + case (OPT_MMAP (eval s) es) of + | SOME ws => + if (EVERY (\w. case w of (Word _) => T | _ => F) ws) + then OPTION_MAP Word + (crep_op op (MAP (\w. case w of Word n => n) ws)) else NONE + | _ => NONE) /\ (eval s (Cmp cmp e1 e2) = case (eval s e1, eval s e2) of | (SOME (Word w1), SOME (Word w2)) => SOME (Word (bitstring$v2w [word_cmp cmp w1 w2])) diff --git a/pancake/semantics/loopPropsScript.sml b/pancake/semantics/loopPropsScript.sml index 739ec5d34b..494f43b44d 100644 --- a/pancake/semantics/loopPropsScript.sml +++ b/pancake/semantics/loopPropsScript.sml @@ -72,17 +72,28 @@ Definition cut_sets_def: (cut_sets l (LoadByte n m) = insert m () l) ∧ (cut_sets l (Seq p q) = cut_sets (cut_sets l p) q) ∧ (cut_sets l (If _ _ _ p q nl) = nl) ∧ + (cut_sets l (Arith arith) = + case arith of + LLongDiv r1 r2 _ _ _ => insert r1 () $ insert r2 () l + | LLongMul r1 r2 _ _ => insert r1 () $ insert r2 () l + | LDiv r1 _ _ => insert r1 () l + ) ∧ (cut_sets l _ = l) End Definition comp_syntax_ok_def: (comp_syntax_ok l loopLang$Skip = T) ∧ (comp_syntax_ok l (Assign n e) = T) ∧ + (comp_syntax_ok l (Loop lin p lout) = (l = lin ∧ l = lout ∧ comp_syntax_ok lin p)) ∧ + (comp_syntax_ok l (Arith arith) = T) ∧ + (comp_syntax_ok l Break = T) ∧ (comp_syntax_ok l (LocValue n m) = T) ∧ (comp_syntax_ok l (LoadByte n m) = T) ∧ (comp_syntax_ok l (Seq p q) = (comp_syntax_ok l p ∧ comp_syntax_ok (cut_sets l p) q)) ∧ (comp_syntax_ok l (If c n r p q nl) = - (∃m v v'. r = Reg m ∧ p = Assign n v ∧ q = Assign n v' ∧ nl = list_insert [n; m] l)) ∧ + (comp_syntax_ok l p ∧ comp_syntax_ok l q ∧ + ∃ns. nl = FOLDL (λsp n. insert n () sp) l ns)) + ∧ (comp_syntax_ok _ _ = F) End @@ -111,17 +122,15 @@ Proof ntac 4 (once_asm_rewrite_tac [acc_vars_def]) >> simp_tac (srw_ss()) [domain_def,AC UNION_COMM UNION_ASSOC,domain_union, domain_insert,LET_THM] >> - every_case_tac >> - simp_tac (srw_ss()) [domain_def,AC UNION_COMM UNION_ASSOC,domain_union, - domain_insert,LET_THM] >> - once_rewrite_tac [INSERT_SING_UNION] >> - simp_tac (srw_ss()) [domain_def,AC UNION_COMM UNION_ASSOC,domain_union, - domain_insert,LET_THM] >> - rpt (pop_assum (fn th => mp_tac (SIMP_RULE std_ss [] th))) >> - rewrite_tac [AND_IMP_INTRO] >> - disch_then (fn th => ntac 6 (once_rewrite_tac [th])) >> - simp_tac (srw_ss()) [domain_def,AC UNION_COMM UNION_ASSOC,domain_union, - domain_insert,LET_THM] >> fs [EXTENSION] >> metis_tac [] + every_case_tac + >~ [‘domain (acc_vars _ _) = domain _ ∪ domain(acc_vars _ _)’] >- + (rpt (pop_assum (fn th => mp_tac (SIMP_RULE std_ss [] th))) >> + rewrite_tac [AND_IMP_INTRO] >> + disch_then (fn th => ntac 6 (once_rewrite_tac [th])) >> + simp_tac (srw_ss()) [domain_def,AC UNION_COMM UNION_ASSOC,domain_union, + domain_insert,LET_THM] >> + fs [EXTENSION] >> metis_tac []) >> + rw[SET_EQ_SUBSET,SUBSET_DEF] >> rw[] QED Theorem evaluate_Loop_body_same: @@ -186,42 +195,13 @@ Theorem locals_touched_eq_eval_eq: (!n. MEM n (locals_touched e) ==> lookup n s.locals = lookup n t.locals) ==> eval t e = eval s e Proof - ho_match_mp_tac eval_ind >> rw [] - >- fs [eval_def] - >- fs [eval_def, locals_touched_def] - >- fs [eval_def, locals_touched_def] - >- ( - fs [eval_def, locals_touched_def] >> - every_case_tac >> fs [mem_load_def]) - >- ( - fs [eval_def, locals_touched_def] >> - every_case_tac >> fs [] - >- ( - ‘the_words (MAP (λa. eval t a) wexps) = SOME x’ suffices_by fs [] >> - pop_assum mp_tac >> pop_assum kall_tac >> - rpt (pop_assum mp_tac) >> - MAP_EVERY qid_spec_tac [‘x’, ‘t’, ‘s’, ‘wexps’] >> - Induct >> rw [] >> - fs [wordSemTheory.the_words_def, - CaseEq "option", CaseEq "word_loc"] >> rveq >> fs [] >> - last_x_assum (qspecl_then [‘s’, ‘t’, ‘xs’] mp_tac) >> fs []) - >- ( - ‘the_words (MAP (λa. eval s a) wexps) = SOME x’ suffices_by fs [] >> - pop_assum kall_tac >> - rpt (pop_assum mp_tac) >> - MAP_EVERY qid_spec_tac [‘x’, ‘t’, ‘s’, ‘wexps’] >> - Induct >> rw [] >> - fs [wordSemTheory.the_words_def, - CaseEq "option", CaseEq "word_loc"] >> rveq >> fs [] >> - last_x_assum (qspecl_then [‘s’, ‘t’, ‘xs’] mp_tac) >> fs []) >> - ‘x = x'’ suffices_by fs [] >> - rpt (pop_assum mp_tac) >> - MAP_EVERY qid_spec_tac [‘x'’, ‘x’, ‘t’, ‘s’, ‘wexps’] >> - Induct >> rw [] >> - fs [wordSemTheory.the_words_def, - CaseEq "option", CaseEq "word_loc"] >> rveq >> fs [] >> - last_x_assum (qspecl_then [‘s’, ‘t’, ‘xs’] mp_tac) >> fs []) >> - fs [eval_def, locals_touched_def] + ho_match_mp_tac eval_ind >> rw [] >> + gvs[locals_touched_def,MEM_FLAT,MEM_MAP,PULL_EXISTS,eval_def,mem_load_def] >> + ntac 2 AP_THM_TAC >> ntac 2 AP_TERM_TAC >> + match_mp_tac MAP_CONG >> + rw[] >> + first_x_assum $ match_mp_tac o MP_CANON >> + rw[] >> res_tac QED Theorem loop_eval_nested_assign_distinct_eq: @@ -342,143 +322,146 @@ Theorem unassigned_vars_evaluate_same: lookup n t.locals = lookup n s.locals Proof recInduct evaluate_ind >> - rpt conj_tac >> rpt gen_tac >> - TRY ( - rename [‘Mark’] >> - rw [] >> - fs [Once evaluate_def, AllCaseEqs(), assigned_vars_def, - survives_def]) >> - TRY ( - rename [‘FFI’] >> - rw [] >> - fs [Once evaluate_def,AllCaseEqs(), assigned_vars_def, survives_def] >> - rveq >> fs [cut_state_def] >> rveq >> - fs [lookup_inter,AllCaseEqs(), domain_lookup]) >> - TRY ( - rename [‘Seq’] >> - rw [] >> - fs [Once evaluate_def,AllCaseEqs(), assigned_vars_def, - survives_def] >> - pairarg_tac >> fs [AllCaseEqs()] >> rveq >> - res_tac >> fs []) >> - TRY ( - rename [‘If’] >> - rw [] >> - fs [Once evaluate_def, AllCaseEqs(), assigned_vars_def, - survives_def] >> rveq >> - FULL_CASE_TAC >> fs [] >> - rename [‘cut_res _ (evaluate (c1,s))’] >> - cases_on ‘evaluate (c1,s)’ >> fs [] >> - cases_on ‘q’ >> fs [cut_res_def, AllCaseEqs(), dec_clock_def, cut_state_def] >> - rveq >> fs [lookup_inter, AllCaseEqs()] >> - res_tac >> rfs [domain_lookup]) >> - TRY ( - rename [‘Loop’] >> - rpt strip_tac >> - qpat_x_assum ‘evaluate (Loop _ _ _,_) = _’ mp_tac >> - once_rewrite_tac [evaluate_def] >> - rewrite_tac [cut_res_def, cut_state_def, dec_clock_def] >> - reverse (cases_on ‘domain live_in ⊆ domain s.locals’) - >- rw [] >> - rw [] >> - FULL_CASE_TAC >> - cases_on ‘q’ >> fs [] >> - fs [Once cut_res_def, cut_state_def] >> - fs [survives_def, assigned_vars_def, dec_clock_def] >> - fs [AllCaseEqs()] >> rveq >> fs [] >> - res_tac >> rfs [lookup_inter, AllCaseEqs(), domain_lookup]) >> - TRY ( - rename [‘Call’] >> - rpt strip_tac - >- ( - (* NONE result *) - qpat_x_assum ‘evaluate (Call _ _ _ _,_) = _’ mp_tac >> - once_rewrite_tac [evaluate_def] >> - rpt TOP_CASE_TAC - >- ( - strip_tac >> - rfs [] >> rveq >> - fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, - dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> - rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup]) - >- ( - pop_assum kall_tac >> - pop_assum mp_tac >> - pop_assum kall_tac >> - strip_tac >> - rfs [] >> rveq >> - fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, - dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> - rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> - qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> - cases_on ‘evaluate (rq, ar)’ >> - qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> - strip_tac >> cases_on ‘tq’ >> - fs [cut_res_def, cut_state_def, dec_clock_def, - AllCaseEqs()] >> rveq >> - fs [] >> - unabbrev_all_tac >> fs [] >> - qsuff_tac ‘lookup n tr.locals = SOME v’ - >- (strip_tac >> fs [lookup_inter]) >> - first_x_assum match_mp_tac >> - fs []) >> - pop_assum mp_tac >> - pop_assum kall_tac >> - pop_assum kall_tac >> - strip_tac >> - rfs [] >> rveq >> - fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, - dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> - rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> - qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> - cases_on ‘evaluate (rq, ar)’ >> - qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> - strip_tac >> cases_on ‘tq’ >> - fs [cut_res_def, cut_state_def, dec_clock_def, - AllCaseEqs()] >> rveq >> - fs [] >> - unabbrev_all_tac >> fs [] >> - qsuff_tac ‘lookup n tr.locals = SOME v’ - >- (strip_tac >> fs [lookup_inter]) >> - first_x_assum match_mp_tac >> - fs []) >> - (* non-NONE result *) - (qpat_x_assum ‘evaluate (Call _ _ _ _,_) = _’ mp_tac >> - once_rewrite_tac [evaluate_def] >> - rpt TOP_CASE_TAC - >- ( - pop_assum kall_tac >> - pop_assum mp_tac >> - pop_assum kall_tac >> - strip_tac >> - rfs [] >> rveq >> - fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, - dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> - rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> - qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> - cases_on ‘evaluate (rq, ar)’ >> - qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> - strip_tac >> cases_on ‘tq’ >> - fs [cut_res_def, cut_state_def, dec_clock_def, - AllCaseEqs()]) >> - pop_assum mp_tac >> - pop_assum kall_tac >> - pop_assum kall_tac >> - strip_tac >> - rfs [] >> rveq >> - fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, - dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> - rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> - qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> - cases_on ‘evaluate (rq, ar)’ >> - qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> - strip_tac >> cases_on ‘tq’ >> - fs [cut_res_def, cut_state_def, dec_clock_def, - AllCaseEqs()])) >> + rpt conj_tac >> rpt gen_tac + >~ [‘Mark’] >- + (rw [] >> + fs [Once evaluate_def, AllCaseEqs(), assigned_vars_def, + survives_def]) + >~ [‘FFI’] >- + (rw [] >> + fs [Once evaluate_def,AllCaseEqs(), assigned_vars_def, survives_def] >> + rveq >> fs [cut_state_def] >> rveq >> + fs [lookup_inter,AllCaseEqs(), domain_lookup]) + >~ [‘Seq’] >- + (rw [] >> + fs [Once evaluate_def,AllCaseEqs(), assigned_vars_def, + survives_def] >> + pairarg_tac >> fs [AllCaseEqs()] >> rveq >> + res_tac >> fs []) + >~ [‘If’] >- + (rw [] >> + fs [Once evaluate_def, AllCaseEqs(), assigned_vars_def, + survives_def] >> rveq >> + FULL_CASE_TAC >> fs [] >> + rename [‘cut_res _ (evaluate (c1,s))’] >> + cases_on ‘evaluate (c1,s)’ >> fs [] >> + cases_on ‘q’ >> fs [cut_res_def, AllCaseEqs(), dec_clock_def, cut_state_def] >> + rveq >> fs [lookup_inter, AllCaseEqs()] >> + res_tac >> rfs [domain_lookup]) + >~ [‘Loop’] >- + (rpt strip_tac >> + qpat_x_assum ‘evaluate (Loop _ _ _,_) = _’ mp_tac >> + once_rewrite_tac [evaluate_def] >> + rewrite_tac [cut_res_def, cut_state_def, dec_clock_def] >> + reverse (cases_on ‘domain live_in ⊆ domain s.locals’) + >- rw [] >> + rw [] >> + FULL_CASE_TAC >> + cases_on ‘q’ >> fs [] >> + fs [Once cut_res_def, cut_state_def] >> + fs [survives_def, assigned_vars_def, dec_clock_def] >> + fs [AllCaseEqs()] >> rveq >> fs [] >> + res_tac >> rfs [lookup_inter, AllCaseEqs(), domain_lookup]) + >~ [‘Call’] >- + (rpt strip_tac + >- ( + (* NONE result *) + qpat_x_assum ‘evaluate (Call _ _ _ _,_) = _’ mp_tac >> + once_rewrite_tac [evaluate_def] >> + rpt TOP_CASE_TAC + >- ( + strip_tac >> + rfs [] >> rveq >> + fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, + dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> + rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup]) + >- ( + pop_assum kall_tac >> + pop_assum mp_tac >> + pop_assum kall_tac >> + strip_tac >> + rfs [] >> rveq >> + fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, + dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> + rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> + qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> + cases_on ‘evaluate (rq, ar)’ >> + qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> + strip_tac >> cases_on ‘tq’ >> + fs [cut_res_def, cut_state_def, dec_clock_def, + AllCaseEqs()] >> rveq >> + fs [] >> + unabbrev_all_tac >> fs [] >> + qsuff_tac ‘lookup n tr.locals = SOME v’ + >- (strip_tac >> fs [lookup_inter]) >> + first_x_assum match_mp_tac >> + fs []) >> + pop_assum mp_tac >> + pop_assum kall_tac >> + pop_assum kall_tac >> + strip_tac >> + rfs [] >> rveq >> + fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, + dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> + rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> + qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> + cases_on ‘evaluate (rq, ar)’ >> + qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> + strip_tac >> cases_on ‘tq’ >> + fs [cut_res_def, cut_state_def, dec_clock_def, + AllCaseEqs()] >> rveq >> + fs [] >> + unabbrev_all_tac >> fs [] >> + qsuff_tac ‘lookup n tr.locals = SOME v’ + >- (strip_tac >> fs [lookup_inter]) >> + first_x_assum match_mp_tac >> + fs []) >> + (* non-NONE result *) + (qpat_x_assum ‘evaluate (Call _ _ _ _,_) = _’ mp_tac >> + once_rewrite_tac [evaluate_def] >> + rpt TOP_CASE_TAC + >- ( + pop_assum kall_tac >> + pop_assum mp_tac >> + pop_assum kall_tac >> + strip_tac >> + rfs [] >> rveq >> + fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, + dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> + rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> + qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> + cases_on ‘evaluate (rq, ar)’ >> + qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> + strip_tac >> cases_on ‘tq’ >> + fs [cut_res_def, cut_state_def, dec_clock_def, + AllCaseEqs()]) >> + pop_assum mp_tac >> + pop_assum kall_tac >> + pop_assum kall_tac >> + strip_tac >> + rfs [] >> rveq >> + fs [assigned_vars_def, survives_def, set_var_def, cut_res_def, + dec_clock_def, cut_state_def, AllCaseEqs(), lookup_insert] >> + rveq >> fs [lookup_inter, AllCaseEqs(), domain_lookup] >> + qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> + cases_on ‘evaluate (rq, ar)’ >> + qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> + strip_tac >> cases_on ‘tq’ >> + fs [cut_res_def, cut_state_def, dec_clock_def, + AllCaseEqs()])) + >~ [‘Arith arith’] >- + (Cases_on ‘arith’ >> + rw [] >> + fs [Once evaluate_def,AllCaseEqs(), set_var_def, set_globals_def, + dec_clock_def, assigned_vars_def, survives_def,loop_arith_def] >> + rveq >> fs [lookup_insert, mem_store_def, AllCaseEqs()] >> + rveq >> fs [state_component_equality] + ) >> rw [] >> fs [Once evaluate_def,AllCaseEqs(), set_var_def, set_globals_def, dec_clock_def, assigned_vars_def, survives_def] >> - rveq >> fs [lookup_insert, mem_store_def, AllCaseEqs()] >> + rveq >> fs [lookup_insert, mem_store_def, AllCaseEqs(), + DefnBase.one_line_ify NONE loop_arith_def] >> rveq >> fs [state_component_equality] QED @@ -526,41 +509,6 @@ Proof fs [nested_seq_def, survives_def] QED - - -(* from here *) -Theorem comp_syn_ok_basic_cases: - (!l. comp_syntax_ok l Skip) /\ - (!l n m. comp_syntax_ok l (LocValue n m)) /\ - (!l n e. comp_syntax_ok l (Assign n e)) /\ - (!l n m. comp_syntax_ok l (LoadByte n m)) /\ - (!l c n m v v'. comp_syntax_ok l (If c n (Reg m) - (Assign n v) (Assign n v') (list_insert [n; m] l))) -Proof - rw [] >> - ntac 3 (fs [Once comp_syntax_ok_def]) -QED - - -Theorem comp_syn_ok_seq: - !l p q. comp_syntax_ok l (Seq p q) ==> - comp_syntax_ok l p /\ comp_syntax_ok (cut_sets l p) q -Proof - rw [] >> - fs [Once comp_syntax_ok_def] -QED - - -Theorem comp_syn_ok_if: - comp_syntax_ok l (If cmp n ri p q ns) ==> - ?v v' m. ri = Reg m /\ p = Assign n v /\ - q = Assign n v' /\ ns = list_insert [n; m] l -Proof - rw [] >> - fs [Once comp_syntax_ok_def] -QED - - Theorem comp_syn_ok_seq2: !l p q. comp_syntax_ok l p /\ comp_syntax_ok (cut_sets l p) q ==> comp_syntax_ok l (Seq p q) @@ -577,11 +525,7 @@ Theorem comp_syn_ok_nested_seq: comp_syntax_ok l (nested_seq (p ++ q)) Proof Induct >> rw [] >> - fs [nested_seq_def] >> - fs [cut_sets_def] >> - drule comp_syn_ok_seq >> - strip_tac >> res_tac >> fs [] >> - metis_tac [comp_syn_ok_seq2] + fs [nested_seq_def,cut_sets_def,comp_syntax_ok_def] QED Theorem comp_syn_ok_nested_seq2: @@ -590,9 +534,8 @@ Theorem comp_syn_ok_nested_seq2: comp_syntax_ok (cut_sets l (nested_seq p)) (nested_seq q) Proof Induct >> rw [] >> - fs [nested_seq_def, comp_syn_ok_basic_cases, cut_sets_def] >> - drule comp_syn_ok_seq >> strip_tac >> fs [] >> - metis_tac [comp_syn_ok_seq2] + fs [nested_seq_def, cut_sets_def,comp_syntax_ok_def] >> + metis_tac[comp_syn_ok_nested_seq] QED @@ -606,10 +549,9 @@ Proof fs [cut_sets_def] QED - Theorem cut_sets_union_accumulate: - !p l. comp_syntax_ok l p ==> (* need this assumption for the If case *) - ?(l' :sptree$num_set). cut_sets l p = union l l' + ∀p l. comp_syntax_ok l p ==> (* need this assumption for the If case *) + ∃(l' :sptree$num_set). cut_sets l p = union l l' Proof Induct >> rw [] >> TRY (fs [Once comp_syntax_ok_def] >> NO_TAC) >> @@ -619,20 +561,25 @@ Proof rename [‘insert vn () l’] >> qexists_tac ‘insert vn () LN’ >> fs [Once insert_union, union_num_set_sym] >> NO_TAC) + >- (rename1 ‘Arith l’ >> Cases_on ‘l’ >> rw[] >> + simp[Once insert_union,union_num_set_sym] >> + simp[Once insert_union,SimpR “union”, union_num_set_sym] >> + metis_tac[union_num_set_sym,union_assoc]) >- ( - drule comp_syn_ok_seq >> - strip_tac >> - last_x_assum drule >> - strip_tac >> fs [] >> - last_x_assum (qspec_then ‘union l l'’ mp_tac) >> - fs [] >> strip_tac >> - qexists_tac ‘union l' l''’ >> - fs [] >> metis_tac [union_assoc]) >> - drule comp_syn_ok_if >> - strip_tac >> rveq >> - qexists_tac ‘insert m () (insert n () LN)’ >> - fs [list_insert_def] >> - metis_tac [union_insert_LN, insert_union, union_num_set_sym, union_assoc] + gvs[comp_syntax_ok_def] >> + res_tac >> + simp[] >> + metis_tac[union_assoc]) >> + gvs[comp_syntax_ok_def] >> + rpt $ pop_assum kall_tac >> + qid_spec_tac ‘l’ >> + Induct_on ‘ns’ >> + rw[] + >- metis_tac[union_LN] >> + rename1 ‘insert x () sp’ >> + first_x_assum $ qspec_then ‘insert x () sp’ strip_assume_tac >> + rw[] >> + metis_tac[union_num_set_sym,union_assoc,union_insert_LN] QED @@ -684,29 +631,29 @@ Theorem comp_syn_ok_upd_local_clock: comp_syntax_ok l p ==> t = s with <|locals := t.locals; clock := t.clock|> Proof - recInduct evaluate_ind >> rw [] >> - TRY (fs [Once comp_syntax_ok_def, every_prog_def] >> NO_TAC) >> - TRY ( - fs [evaluate_def] >> rveq >> - TRY every_case_tac >> fs [set_var_def, state_component_equality] >> NO_TAC) - >- ( - drule comp_syn_ok_seq >> - strip_tac >> - fs [evaluate_def] >> - pairarg_tac >> fs [] >> - FULL_CASE_TAC >> fs [] >> rveq >> - res_tac >> fs [state_component_equality]) >> - drule comp_syn_ok_if >> - strip_tac >> rveq >> - fs [evaluate_def] >> - every_case_tac >> fs [] >> rveq >> - fs [state_component_equality, evaluate_def, comp_syn_ok_basic_cases] >> - every_case_tac >> - fs [cut_res_def, cut_state_def, dec_clock_def, set_var_def] >> - every_case_tac >> fs [] >> rveq >> fs [] + recInduct evaluate_ind >> rw [] + >~ [‘Arith’] >- + (gvs[comp_syntax_ok_def,evaluate_def,AllCaseEqs(), + DefnBase.one_line_ify NONE loop_arith_def] >> + simp[state_component_equality,set_var_def]) + >~ [‘Loop’] >- + (qpat_x_assum ‘evaluate _ = _’ $ strip_assume_tac o PURE_ONCE_REWRITE_RULE [evaluate_def] >> + gvs[comp_syntax_ok_def,DefnBase.one_line_ify NONE cut_res_def,cut_state_def, + AllCaseEqs(),dec_clock_def] >> + res_tac >> gvs[state_component_equality]) + >~ [‘If’] >- + (gvs[comp_syntax_ok_def,Once evaluate_def,DefnBase.one_line_ify NONE cut_res_def,cut_state_def, + AllCaseEqs(),dec_clock_def] >> + simp[state_component_equality] >> + Cases_on ‘word_cmp cmp x y’ >> gvs[] >> + res_tac >> gvs[state_component_equality]) >> + gvs[comp_syntax_ok_def,Once evaluate_def] >> + gvs[AllCaseEqs(),set_var_def] >> + TRY pairarg_tac >> gvs[AllCaseEqs()] >> + res_tac >> + gvs[state_component_equality] QED - Theorem assigned_vars_nested_seq_split: !p q. assigned_vars (nested_seq (p ++ q)) = @@ -742,52 +689,36 @@ Theorem comp_syn_ok_lookup_locals_eq: ~MEM n (assigned_vars p) ==> lookup n t.locals = lookup n s.locals Proof - recInduct evaluate_ind >> rw [] >> - TRY (fs [Once comp_syntax_ok_def, every_prog_def] >> NO_TAC) >> - TRY ( - fs [evaluate_def] >> - every_case_tac >> fs [] >> rveq >> - fs [set_var_def, assigned_vars_def, lookup_insert] >> NO_TAC) - >- ( - drule comp_syn_ok_seq >> - strip_tac >> - fs [evaluate_def, assigned_vars_def] >> - pairarg_tac >> fs [AllCaseEqs ()] >> rveq >> fs [] - >- ( - qpat_x_assum ‘evaluate (_,s1) = _’ assume_tac >> - drule evaluate_clock >> fs [] >> - strip_tac >> fs [] >> - dxrule comp_syn_ok_seq >> - strip_tac >> + recInduct evaluate_ind >> rw [] + >~ [‘Arith’] >- + (gvs[evaluate_def,assigned_vars_def, + DefnBase.one_line_ify NONE loop_arith_def, + AllCaseEqs(),set_var_def,lookup_insert + ]) + >~ [‘Loop’] >- + (qpat_x_assum ‘evaluate _ = _’ $ strip_assume_tac o PURE_ONCE_REWRITE_RULE [evaluate_def] >> + gvs[comp_syntax_ok_def,DefnBase.one_line_ify NONE cut_res_def,cut_state_def, + AllCaseEqs(),dec_clock_def,assigned_vars_def] >> + first_x_assum $ drule_then $ drule_at $ Pos last >> + rw[lookup_inter_alt]) + >~ [‘If’] >- + (gvs[comp_syntax_ok_def,Once evaluate_def,DefnBase.one_line_ify NONE cut_res_def,cut_state_def, + AllCaseEqs(),dec_clock_def,assigned_vars_def] >> + Cases_on ‘word_cmp cmp x y’ >> + gvs[] >> + res_tac >> + rw[lookup_inter_alt]) + >~ [‘Seq’] >- + (gvs[comp_syntax_ok_def,assigned_vars_def,Once evaluate_def] >> + pairarg_tac >> + gvs[AllCaseEqs()] >> + last_x_assum drule_all >> + rw[] >> first_x_assum drule >> - disch_then (qspec_then ‘n’ mp_tac) >> - fs [] >> - strip_tac >> - first_x_assum drule >> - disch_then (qspec_then ‘n’ mp_tac) >> - fs [] >> - impl_tac - >- ( - qpat_x_assum ‘comp_syntax_ok l c1’ assume_tac >> - drule cut_sets_union_domain_union >> - strip_tac >> fs []) >> + disch_then $ drule_at $ Pos last >> + imp_res_tac cut_sets_union_domain_union >> fs []) >> - drule comp_syn_ok_seq >> - strip_tac >> - res_tac >> fs []) >> - drule evaluate_clock >> fs [] >> - strip_tac >> fs [] >> - drule comp_syn_ok_if >> - strip_tac >> rveq >> fs [] >> - fs [evaluate_def, assigned_vars_def] >> - fs [AllCaseEqs()] >> rveq >> fs [domain_inter] >> - cases_on ‘word_cmp cmp x y’ >> fs [] >> - fs [evaluate_def, list_insert_def, AllCaseEqs()] >> - FULL_CASE_TAC >> fs [cut_res_def, set_var_def, dec_clock_def, cut_state_def] >> - FULL_CASE_TAC >> fs [] >> rveq >> - every_case_tac >> rfs [] >> rveq >> fs [] >> - fs [state_component_equality, lookup_inter, lookup_insert] >> - every_case_tac >> rfs [domain_lookup] + gvs[comp_syntax_ok_def,assigned_vars_def,Once evaluate_def,AllCaseEqs(),set_var_def,lookup_insert] QED Theorem eval_upd_clock_eq: @@ -798,36 +729,19 @@ Proof >- ( every_case_tac >> fs [] >> fs [mem_load_def]) >> - qsuff_tac ‘the_words (MAP (λa. eval (t with clock := ck) a) wexps) = - the_words (MAP (λa. eval t a) wexps)’ >> - fs [] >> - pop_assum mp_tac >> - qid_spec_tac ‘wexps’ >> - Induct >> rw [] >> - last_x_assum mp_tac >> - impl_tac >- metis_tac [] >> - strip_tac >> fs [wordSemTheory.the_words_def] + ntac 2 AP_THM_TAC >> ntac 2 AP_TERM_TAC >> + match_mp_tac MAP_CONG >> + rw[] QED -(* should be trivial, but record updates are annoying *) - Theorem eval_upd_locals_clock_eq: !t e l ck. eval (t with <|locals := l; clock := ck|>) e = eval (t with locals := l) e Proof - ho_match_mp_tac eval_ind >> rw [] >> - fs [eval_def] - >- ( - every_case_tac >> fs [] >> - fs [mem_load_def]) >> - qsuff_tac ‘the_words (MAP (λa. eval (t with <|locals := l; clock := ck|>) a) wexps) = - the_words (MAP (λa. eval (t with locals := l) a) wexps)’ >> - fs [] >> - pop_assum mp_tac >> - qid_spec_tac ‘wexps’ >> - Induct >> rw [] >> - last_x_assum mp_tac >> - impl_tac >- metis_tac [] >> - strip_tac >> fs [wordSemTheory.the_words_def] + rpt strip_tac >> + qspec_then ‘ck’ + (dep_rewrite.DEP_ONCE_REWRITE_TAC o single o GSYM) + (CONV_RULE (RESORT_FORALL_CONV List.rev) eval_upd_clock_eq) >> + simp[] QED Theorem cut_res_add_clock: @@ -845,90 +759,85 @@ Theorem evaluate_add_clock_eq: evaluate (p,t) = (res,st) /\ res <> SOME TimeOut ==> evaluate (p,t with clock := t.clock + ck) = (res,st with clock := st.clock + ck) Proof - recInduct evaluate_ind >> rw [] >> - TRY (fs [Once evaluate_def] >> NO_TAC) >> - TRY ( - rename [‘Seq’] >> - fs [evaluate_def] >> pairarg_tac >> fs [] >> - pairarg_tac >> fs [] >> rveq >> - fs [AllCaseEqs ()] >> rveq >> fs [] >> - first_x_assum (qspec_then ‘ck’ mp_tac) >> - fs []) >> - TRY ( - rename [‘If’] >> - fs [evaluate_def, AllCaseEqs ()] >> - rveq >> cases_on ‘ri’ >> fs [get_var_imm_def] >> - TOP_CASE_TAC >> cases_on ‘evaluate (c1,s)’ >> cases_on ‘evaluate (c2,s)’ >> - fs [cut_res_def, cut_state_def, AllCaseEqs (), dec_clock_def] >> - rveq >> fs []) >> - TRY ( - rename [‘FFI’] >> - fs [evaluate_def, AllCaseEqs (), cut_state_def, call_env_def] >> - rveq >> fs []) >> - TRY ( - rename [‘Loop’] >> - fs [Once evaluate_def] >> - TOP_CASE_TAC >> fs [] >> - cases_on ‘cut_res live_in ((NONE:'a result option),s)’ >> - fs [] >> - ‘q' <> SOME TimeOut’ by ( - CCONTR_TAC >> - fs [cut_res_def, cut_state_def, AllCaseEqs(), dec_clock_def]) >> - drule cut_res_add_clock >> - disch_then (qspec_then ‘ck’ mp_tac) >> fs [] >> - strip_tac >> fs [] >> rveq >> - TOP_CASE_TAC >> fs [] >> - cases_on ‘evaluate (body,r')’ >> fs [] >> rveq >> - cases_on ‘q’ >> fs [] >> - cases_on ‘x’ >> fs [] >> rveq >> fs [] - >- (imp_res_tac cut_res_add_clock >> res_tac >> fs []) >> - first_x_assum match_mp_tac >> - TOP_CASE_TAC >> fs [] >> - reverse TOP_CASE_TAC >> fs [] - >- fs [Once evaluate_def] >> - TOP_CASE_TAC >> fs [] >> - TOP_CASE_TAC >> fs [] >> - fs [Once evaluate_def]) >> - TRY ( - rename [‘Call’] >> - fs [evaluate_def, get_vars_clock_upd_eq, dec_clock_def] >> - ntac 4 (TOP_CASE_TAC >> fs []) - >- ( - fs [AllCaseEqs()] >> - ‘s.clock <> 0’ by ( - fs [AllCaseEqs()] >> rveq >> fs []) >> - rveq >> fs []) >> - TOP_CASE_TAC >> fs [] >> - cases_on ‘cut_res r' ((NONE:'a result option),s)’ >> - fs [] >> - ‘q'' <> SOME TimeOut’ by ( - CCONTR_TAC >> - fs [cut_res_def, cut_state_def, AllCaseEqs(), dec_clock_def]) >> - drule cut_res_add_clock >> - disch_then (qspec_then ‘ck’ mp_tac) >> fs [] >> - strip_tac >> fs [] >> - TOP_CASE_TAC >> fs [] >> - cases_on ‘evaluate (r,r'' with locals := q)’ >> fs [] >> rveq >> - cases_on ‘q''’ >> fs [] >> rveq >> - cases_on ‘x'’ >> fs [] >> rveq >> - TOP_CASE_TAC >> fs [] >> rveq >> - fs [set_var_def] >> - rpt (TOP_CASE_TAC >> fs []) >> - qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> - qmatch_asmsub_abbrev_tac ‘evaluate (rq, lr)’ >> - cases_on ‘evaluate (rq, lr)’ >> - qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> - ‘tq <> SOME TimeOut’ by ( - CCONTR_TAC >> - unabbrev_all_tac >> - fs [cut_res_def, cut_state_def, AllCaseEqs(), dec_clock_def]) >> - first_x_assum (qspecl_then [‘tq’, ‘tr’, ‘ck’] mp_tac) >> - fs [] >> strip_tac >> - imp_res_tac cut_res_add_clock >> - res_tac >> fs []) >> + recInduct evaluate_ind >> rw [] + >~ [‘Seq’] >- + (fs [evaluate_def] >> pairarg_tac >> fs [] >> + pairarg_tac >> fs [] >> rveq >> + fs [AllCaseEqs ()] >> rveq >> fs [] >> + first_x_assum (qspec_then ‘ck’ mp_tac) >> + fs []) + >~ [‘If’] >- + (fs [evaluate_def, AllCaseEqs ()] >> + rveq >> cases_on ‘ri’ >> fs [get_var_imm_def] >> + TOP_CASE_TAC >> cases_on ‘evaluate (c1,s)’ >> cases_on ‘evaluate (c2,s)’ >> + fs [cut_res_def, cut_state_def, AllCaseEqs (), dec_clock_def] >> + rveq >> fs []) + >~ [‘FFI’] >- + (fs [evaluate_def, AllCaseEqs (), cut_state_def, call_env_def] >> + rveq >> fs []) + >~ [‘Loop’] >- + (fs [Once evaluate_def] >> + TOP_CASE_TAC >> fs [] >> + cases_on ‘cut_res live_in ((NONE:'a result option),s)’ >> + fs [] >> + ‘q' <> SOME TimeOut’ by ( + CCONTR_TAC >> + fs [cut_res_def, cut_state_def, AllCaseEqs(), dec_clock_def]) >> + drule cut_res_add_clock >> + disch_then (qspec_then ‘ck’ mp_tac) >> fs [] >> + strip_tac >> fs [] >> rveq >> + TOP_CASE_TAC >> fs [] >> + cases_on ‘evaluate (body,r')’ >> fs [] >> rveq >> + cases_on ‘q’ >> fs [] >> + cases_on ‘x’ >> fs [] >> rveq >> fs [] + >- (imp_res_tac cut_res_add_clock >> res_tac >> fs []) >> + first_x_assum match_mp_tac >> + TOP_CASE_TAC >> fs [] >> + reverse TOP_CASE_TAC >> fs [] + >- fs [Once evaluate_def] >> + TOP_CASE_TAC >> fs [] >> + TOP_CASE_TAC >> fs [] >> + fs [Once evaluate_def]) + >~ [‘Call’] >- + (fs [evaluate_def, get_vars_clock_upd_eq, dec_clock_def] >> + ntac 4 (TOP_CASE_TAC >> fs []) + >- ( + fs [AllCaseEqs()] >> + ‘s.clock <> 0’ by ( + fs [AllCaseEqs()] >> rveq >> fs []) >> + rveq >> fs []) >> + TOP_CASE_TAC >> fs [] >> + cases_on ‘cut_res r' ((NONE:'a result option),s)’ >> + fs [] >> + ‘q'' <> SOME TimeOut’ by ( + CCONTR_TAC >> + fs [cut_res_def, cut_state_def, AllCaseEqs(), dec_clock_def]) >> + drule cut_res_add_clock >> + disch_then (qspec_then ‘ck’ mp_tac) >> fs [] >> + strip_tac >> fs [] >> + TOP_CASE_TAC >> fs [] >> + cases_on ‘evaluate (r,r'' with locals := q)’ >> fs [] >> rveq >> + cases_on ‘q''’ >> fs [] >> rveq >> + cases_on ‘x'’ >> fs [] >> rveq >> + TOP_CASE_TAC >> fs [] >> rveq >> + fs [set_var_def] >> + rpt (TOP_CASE_TAC >> fs []) >> + qmatch_goalsub_abbrev_tac ‘cut_res nr (evaluate (rq,ar)) = _’ >> + qmatch_asmsub_abbrev_tac ‘evaluate (rq, lr)’ >> + cases_on ‘evaluate (rq, lr)’ >> + qmatch_asmsub_rename_tac ‘ evaluate _ = (tq,tr)’ >> + ‘tq <> SOME TimeOut’ by ( + CCONTR_TAC >> + unabbrev_all_tac >> + fs [cut_res_def, cut_state_def, AllCaseEqs(), dec_clock_def]) >> + first_x_assum (qspecl_then [‘tq’, ‘tr’, ‘ck’] mp_tac) >> + fs [] >> strip_tac >> + imp_res_tac cut_res_add_clock >> + res_tac >> fs []) >> fs [evaluate_def, eval_upd_clock_eq, AllCaseEqs () , set_var_def, mem_store_def, set_globals_def, - call_env_def, dec_clock_def] >> rveq >> + call_env_def, dec_clock_def, + DefnBase.one_line_ify NONE loop_arith_def] >> rveq >> fs [state_component_equality] QED @@ -986,55 +895,49 @@ Theorem evaluate_io_events_mono: s1.ffi.io_events ≼ s2.ffi.io_events Proof recInduct evaluate_ind >> - rw [] >> - TRY ( - rename [‘Seq’] >> - fs [evaluate_def] >> - pairarg_tac >> fs [] >> rveq >> - every_case_tac >> fs [] >> rveq >> - metis_tac [IS_PREFIX_TRANS]) >> - TRY ( - rename [‘If’] >> - fs [evaluate_def] >> - every_case_tac >> fs [] >> rveq >> - fs [] >> - TRY (cases_on ‘evaluate (c1,s)’) >> - TRY (cases_on ‘evaluate (c2,s)’) >> - fs [cut_res_def] >> - every_case_tac >> fs [] >> rveq >> - fs [cut_state_def] >> rveq >> fs [dec_clock_def]) >> - TRY ( - rename [‘Loop’] >> - pop_assum mp_tac >> - once_rewrite_tac [evaluate_def, LET_THM] >> - fs [AllCaseEqs()] >> - fs [cut_res_def, cut_state_def, dec_clock_def] >> rveq >> - fs [AllCaseEqs()] >> - strip_tac >> fs [] >> rveq >> fs [] >> - metis_tac [IS_PREFIX_TRANS]) >> - TRY ( - rename [‘Call’] >> - pop_assum mp_tac >> - once_rewrite_tac [evaluate_def, LET_THM] >> - fs [AllCaseEqs(), cut_res_def, cut_state_def, - dec_clock_def, set_var_def] >> - strip_tac >> fs [] >> rveq >> fs [] - >- ( - cases_on ‘evaluate (r,st with locals := insert n retv (inter s.locals live))’ >> - fs [AllCaseEqs(), cut_res_def, cut_state_def, - dec_clock_def, set_var_def] >> rveq >> fs [] >> - metis_tac [IS_PREFIX_TRANS]) >> - cases_on ‘evaluate (h,st with locals := insert n' exn (inter s.locals live))’ >> - fs [AllCaseEqs(), cut_res_def, cut_state_def, - dec_clock_def, set_var_def] >> rveq >> fs [] >> - metis_tac [IS_PREFIX_TRANS]) >> - TRY ( - rename [‘FFI’] >> - fs [evaluate_def, AllCaseEqs(), cut_state_def, - dec_clock_def, ffiTheory.call_FFI_def, call_env_def] >> - rveq >> fs []) >> - fs [evaluate_def] >> - every_case_tac >> + rw [] + >~ [‘Seq’] >- + (fs [evaluate_def] >> + pairarg_tac >> fs [] >> rveq >> + every_case_tac >> fs [] >> rveq >> + metis_tac [IS_PREFIX_TRANS]) + >~ [‘If’] >- + (fs [evaluate_def] >> + every_case_tac >> fs [] >> rveq >> + fs [] >> + TRY (cases_on ‘evaluate (c1,s)’) >> + TRY (cases_on ‘evaluate (c2,s)’) >> + fs [cut_res_def] >> + every_case_tac >> fs [] >> rveq >> + fs [cut_state_def] >> rveq >> fs [dec_clock_def]) + >~ [‘Loop’] >- + (pop_assum mp_tac >> + once_rewrite_tac [evaluate_def, LET_THM] >> + fs [AllCaseEqs()] >> + fs [cut_res_def, cut_state_def, dec_clock_def] >> rveq >> + fs [AllCaseEqs()] >> + strip_tac >> fs [] >> rveq >> fs [] >> + metis_tac [IS_PREFIX_TRANS]) + >~ [‘Call’] >- + (pop_assum mp_tac >> + once_rewrite_tac [evaluate_def, LET_THM] >> + fs [AllCaseEqs(), cut_res_def, cut_state_def, + dec_clock_def, set_var_def] >> + strip_tac >> fs [] >> rveq >> fs [] + >- ( + cases_on ‘evaluate (r,st with locals := insert n retv (inter s.locals live))’ >> + fs [AllCaseEqs(), cut_res_def, cut_state_def, + dec_clock_def, set_var_def] >> rveq >> fs [] >> + metis_tac [IS_PREFIX_TRANS]) >> + cases_on ‘evaluate (h,st with locals := insert n' exn (inter s.locals live))’ >> + fs [AllCaseEqs(), cut_res_def, cut_state_def, + dec_clock_def, set_var_def] >> rveq >> fs [] >> + metis_tac [IS_PREFIX_TRANS]) + >~ [‘FFI’] >- + (fs [evaluate_def, AllCaseEqs(), cut_state_def, + dec_clock_def, ffiTheory.call_FFI_def, call_env_def] >> + rveq >> fs []) >> + fs [evaluate_def,DefnBase.one_line_ify NONE loop_arith_def,AllCaseEqs()] >> fs [set_var_def, mem_store_def, set_globals_def, call_env_def, dec_clock_def] >> rveq >> fs [] @@ -1312,7 +1215,7 @@ Proof fs [cut_state_def, dec_clock_def, ffiTheory.call_FFI_def, call_env_def] >> rveq >> fs [] >> rveq >> fs []) >> - fs [evaluate_def] >> + fs [evaluate_def,DefnBase.one_line_ify NONE loop_arith_def] >> every_case_tac >> fs [set_var_def, mem_store_def, set_globals_def, call_env_def, dec_clock_def] >> rveq >> diff --git a/pancake/semantics/loopSemScript.sml b/pancake/semantics/loopSemScript.sml index 675b5ea7aa..4d73ad348f 100644 --- a/pancake/semantics/loopSemScript.sml +++ b/pancake/semantics/loopSemScript.sml @@ -115,6 +115,35 @@ Definition set_vars_def: (s with locals := (alist_insert vs xs s.locals)) End +Definition loop_arith_def: + (loop_arith ^s (LDiv r1 r2 r3) = + case (lookup r3 s.locals, lookup r2 s.locals) of + (SOME (Word q), SOME(Word w2)) => + if q ≠ 0w then + SOME(set_var r1 (Word (w2 / q)) s) + else NONE + | _ => NONE + ) ∧ + (loop_arith ^s (LLongMul r1 r2 r3 r4) = + case (lookup r3 s.locals, lookup r4 s.locals) of + (SOME (Word w3), SOME(Word w4)) => + (let r = w2n w3 * w2n w4 in + SOME (set_var r2 (Word (n2w r)) (set_var r1 (Word (n2w (r DIV dimword(:'a)))) s))) + | _ => NONE) ∧ + (loop_arith ^s (LLongDiv r1 r2 r3 r4 r5) = + case (lookup r3 s.locals, lookup r4 s.locals, lookup r5 s.locals) of + (SOME (Word w3), SOME(Word w4), SOME(Word w5)) => + (let n = w2n w3 * dimword (:'a) + w2n w4; + d = w2n w5; + q = n DIV d + in + if (d ≠ 0 ∧ q < dimword(:'a)) then + SOME (set_var r1 (Word (n2w q)) (set_var r2 (Word (n2w (n MOD d))) s)) + else NONE) + | _ => NONE + ) +End + Definition find_code_def: (find_code (SOME p) args code = case sptree$lookup p code of @@ -173,6 +202,10 @@ Definition evaluate_def: case eval s exp of | NONE => (SOME Error, s) | SOME w => (NONE, set_var v w s)) /\ + (evaluate (Arith arith,s) = + case loop_arith s arith of + NONE => (SOME Error, s) + | SOME s' => (NONE,s')) /\ (evaluate (Store exp v,s) = case (eval s exp, lookup v s.locals) of | (SOME (Word adr), SOME w) => @@ -320,7 +353,8 @@ Proof \\ rpt (pairarg_tac \\ fs []) \\ fs [CaseEq"option",CaseEq"word_loc",mem_store_def,CaseEq"bool",CaseEq"result", pair_case_eq,cut_res_def] - \\ fs [] \\ rveq \\ fs [set_var_def,set_globals_def] + \\ fs[DefnBase.one_line_ify NONE loop_arith_def,CaseEq "loop_arith", + CaseEq "option", CaseEq "word_loc",set_var_def] \\ rveq \\ fs[] \\ imp_res_tac fix_clock_IMP_LESS_EQ \\ fs [] \\ rename [‘cut_res _ xx’] \\ PairCases_on ‘xx’ \\ fs [] \\ fs [cut_res_def] diff --git a/pancake/semantics/panPropsScript.sml b/pancake/semantics/panPropsScript.sml index 7b7cd648d3..e03536e27f 100644 --- a/pancake/semantics/panPropsScript.sml +++ b/pancake/semantics/panPropsScript.sml @@ -1192,8 +1192,6 @@ Proof fs [] QED - - Theorem update_locals_not_vars_eval_eq: ∀s e v n w. ~MEM n (var_exp e) /\ @@ -1258,6 +1256,13 @@ Proof rw [] >> fs [MEM_FLAT, MEM_MAP] >> metis_tac [EL_MEM]) + >- ( + rpt gen_tac >> + strip_tac >> + gvs [var_exp_def, eval_def, AllCaseEqs(),opt_mmap_eq_some,SF DNF_ss, + DefnBase.one_line_ify NONE pan_op_def,MAP_EQ_CONS,MEM_FLAT,MEM_MAP,PULL_EXISTS] >> + metis_tac[] + ) >- ( rw [] >> gs [var_exp_def, eval_def] >> @@ -1323,4 +1328,43 @@ Proof metis_tac[PAIR,FST,SND]) QED + +Definition every_exp_def: + (every_exp P (panLang$Const w) = P(Const w)) ∧ + (every_exp P (Var v) = P(Var v)) ∧ + (every_exp P (Label f) = P(Label f)) ∧ + (every_exp P (Struct es) = (P(Struct es) ∧ EVERY (every_exp P) es)) ∧ + (every_exp P (Field i e) = (P(Field i e) ∧ every_exp P e)) ∧ + (every_exp P (Load sh e) = (P(Load sh e) ∧ every_exp P e)) ∧ + (every_exp P (LoadByte e) = (P(LoadByte e) ∧ every_exp P e)) ∧ + (every_exp P (Op bop es) = (P(Op bop es) ∧ EVERY (every_exp P) es)) ∧ + (every_exp P (Panop op es) = (P(Panop op es) ∧ EVERY (every_exp P) es)) ∧ + (every_exp P (Cmp c e1 e2) = (P(Cmp c e1 e2) ∧ every_exp P e1 ∧ every_exp P e2)) ∧ + (every_exp P (Shift sh e num) = (P(Shift sh e num) ∧ every_exp P e)) ∧ + (every_exp P BaseAddr = P BaseAddr) +Termination + wf_rel_tac `measure (exp_size ARB o SND)` >> + rpt strip_tac >> + imp_res_tac MEM_IMP_exp_size >> + TRY (first_x_assum (assume_tac o Q.SPEC `ARB`)) >> + decide_tac +End + +Definition exps_of_def: + (exps_of (Raise _ e) = [e]) ∧ + (exps_of (Dec _ e p) = e::exps_of p) ∧ + (exps_of (Seq p q) = exps_of p ++ exps_of q) ∧ + (exps_of (If e p q) = e::exps_of p ++ exps_of q) ∧ + (exps_of (While e p) = e::exps_of p) ∧ + (exps_of (Call NONE e es) = e::es) ∧ + (exps_of (Call (SOME (_ , (SOME (_ , _ , ep)))) e es) = e::es++exps_of ep) ∧ + (exps_of (Call (SOME (_ , NONE)) e es) = e::es) ∧ + (exps_of (Store e1 e2) = [e1;e2]) ∧ + (exps_of (StoreByte e1 e2) = [e1;e2]) ∧ + (exps_of (Return e) = [e]) ∧ + (exps_of (ExtCall _ e1 e2 e3 e4) = [e1;e2;e3;e4]) ∧ + (exps_of (Assign _ e) = [e]) ∧ + (exps_of _ = []) +End + val _ = export_theory(); diff --git a/pancake/semantics/panSemScript.sml b/pancake/semantics/panSemScript.sml index b36bcddc8e..57f9a14dcd 100644 --- a/pancake/semantics/panSemScript.sml +++ b/pancake/semantics/panSemScript.sml @@ -116,6 +116,11 @@ Termination fs [list_size_def, shape_size_def] End +Definition pan_op_def: + pan_op Mul [w1:'a word;w2] = SOME(w1 * w2) ∧ + pan_op _ _ = NONE +End + Definition eval_def: (eval ^s (Const w) = SOME (ValWord w)) /\ (eval s (Var v) = FLOOKUP s.locals v) /\ @@ -155,6 +160,13 @@ Definition eval_def: then OPTION_MAP ValWord (word_op op (MAP (\w. case w of ValWord n => n) ws)) else NONE | _ => NONE) /\ + (eval s (Panop op es) = + case (OPT_MMAP (eval s) es) of + | SOME ws => + if (EVERY (\w. case w of (ValWord _) => T | _ => F) ws) + then OPTION_MAP ValWord + (pan_op op (MAP (\w. case w of ValWord n => n) ws)) else NONE + | _ => NONE) /\ (eval s (Cmp cmp e1 e2) = case (eval s e1, eval s e2) of | (SOME (ValWord w1), SOME (ValWord w2)) =>