autocorres, crefine: remove early AutoCorres–CRefine experiment
This has been superseded by actual AutoCorres integration with CRefine.
This commit is contained in:
Japheth Lim
parent
0cb839c7da
commit
dc626e99d3
|
|
@ -1,26 +0,0 @@
|
|||
(*
|
||||
* Copyright 2014, NICTA
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(NICTA_GPL)
|
||||
*)
|
||||
|
||||
theory AutoCorresCRefine
|
||||
imports Ctac LegacyAutoCorres
|
||||
begin
|
||||
|
||||
context kernel begin
|
||||
|
||||
ML {* val ckernel_fn_info = (FunctionInfo.init_fn_info @{context} "../c/build/$L4V_ARCH/kernel_all.c_pp") *}
|
||||
ML {* val ckernel_prog_info = ProgramInfo.get_prog_info @{context} "../c/build/$L4V_ARCH/kernel_all.c_pp" *}
|
||||
|
||||
end
|
||||
|
||||
method_setup autocorres_legacy
|
||||
= {* AutoCorresLegacy.method ckernel_prog_info ckernel_fn_info
|
||||
@{term "globals :: globals myvars \<Rightarrow> _"} *}
|
||||
|
||||
end
|
||||
|
|
@ -1,89 +0,0 @@
|
|||
(*
|
||||
* Copyright 2014, NICTA
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(NICTA_BSD)
|
||||
*)
|
||||
|
||||
theory LegacyAutoCorres
|
||||
|
||||
imports "AutoCorres.AutoCorres" "Corres_UL_C"
|
||||
|
||||
begin
|
||||
|
||||
text {* This theory adds some legacy support to the autocorres framework. It allows
|
||||
the use of autocorres in single ccorres_underlying goals without performing an
|
||||
autocorres translation on the entire program base. *}
|
||||
|
||||
lemma fst_c_with_gets_xf:
|
||||
"fst ((doE _ \<leftarrow> c'; liftE (gets xf) odE) s)
|
||||
= (\<lambda>(rv, s). (case rv of Inr _ \<Rightarrow> Inr (xf s) | Inl v \<Rightarrow> Inl v, s)) ` fst (c' s)"
|
||||
by (auto simp: in_bindE image_def in_monad split: sum.splits,
|
||||
auto elim: rev_bexI)
|
||||
|
||||
lemma ccorres_underlying_L1corres:
|
||||
"L1corres check_term Gamma c' c
|
||||
\<Longrightarrow> corres_underlying sr False True ((\<lambda>_ _. False) \<oplus> r) P (\<lambda>s. s \<in> P')
|
||||
(liftE a) (doE c'; liftE (gets xf) odE)
|
||||
\<Longrightarrow> ccorres_underlying sr Gamma r xf arrel axf P P' [] a c"
|
||||
apply (clarsimp simp: L1corres_def ccorres_underlying_def corres_underlying_def
|
||||
ball_cong[OF fst_c_with_gets_xf refl])
|
||||
apply (drule(1) bspec, clarsimp simp: in_monad snd_bindE)
|
||||
apply (drule spec, drule(1) mp)
|
||||
apply (erule exec_handlers.cases, simp_all)
|
||||
apply (erule exec_handlers.cases, simp_all)
|
||||
apply fastforce
|
||||
apply clarsimp
|
||||
apply (drule spec, drule(1) mp)
|
||||
apply (clarsimp split: xstate.split_asm)
|
||||
apply (fastforce simp: unif_rrel_def in_monad)
|
||||
done
|
||||
|
||||
lemma corres_underlying_L2corres:
|
||||
"L2corres gs ret_xf ex_xf P c' c
|
||||
\<Longrightarrow> corres_underlying gs_sr
|
||||
nf True (ftr \<oplus> r) Q Q' a c'
|
||||
\<Longrightarrow> corres_underlying {(s, s'). (s, gs s') \<in> gs_sr}
|
||||
nf True (ftr \<oplus> r)
|
||||
Q (\<lambda>s. P s \<and> Q' (gs s))
|
||||
a (doE c; liftE (gets ret_xf) odE)"
|
||||
apply (clarsimp simp: corres_underlying_def L2corres_def corresXF_def
|
||||
ball_cong[OF fst_c_with_gets_xf refl]
|
||||
snd_bindE snd_liftE snd_gets)
|
||||
apply (drule(1) bspec, clarsimp)
|
||||
apply (drule spec, drule mp, erule conjI, simp)
|
||||
apply clarsimp
|
||||
apply (fastforce split: sum.splits)
|
||||
done
|
||||
|
||||
text {* This rule allows three autocorres-generated theorems to be
|
||||
used to initialise a ccorres_underlying proof. *}
|
||||
lemma ccorres_underlying_autocorres:
|
||||
"L1corres check_term Gamma c' c
|
||||
\<Longrightarrow> (\<And>s. L2corres gs ret_xf ex_xf (L2P s) c'' c')
|
||||
\<Longrightarrow> c'' \<equiv> c'''
|
||||
\<Longrightarrow> \<forall>s. s \<in> P' \<longrightarrow> L2P s s
|
||||
\<Longrightarrow> \<forall>s. xf s = xf_fudge (ret_xf s)
|
||||
\<Longrightarrow> \<forall>s s'. (s, s') \<in> sr = gs_sr s (gs s')
|
||||
\<Longrightarrow> corres_underlying {(s, s'). gs_sr s s'}
|
||||
False True ((\<lambda>_ (_ :: unit). False) \<oplus> (\<lambda>rv rv'. r rv (xf_fudge rv'))) Q Q' (liftE a) c'''
|
||||
\<Longrightarrow> \<forall>s s'. P s \<and> s' \<in> P' \<and> (s, s') \<in> sr \<longrightarrow> Q s \<and> Q' (gs s')
|
||||
\<Longrightarrow> ccorres_underlying sr Gamma r xf arrel axf P P' [] a c"
|
||||
apply (erule ccorres_underlying_L1corres)
|
||||
apply (subst corres_underlying_def, clarsimp)
|
||||
apply (drule corres_underlying_L2corres[rotated], assumption)
|
||||
apply (clarsimp simp: corres_underlying_def ball_cong[OF fst_c_with_gets_xf refl]
|
||||
snd_bindE snd_liftE snd_gets)
|
||||
apply (rename_tac s s')
|
||||
apply (drule spec, drule spec, drule_tac P="gs_sr s (gs s')" in mp, assumption)
|
||||
apply (drule mp, blast, clarsimp)
|
||||
apply (drule(1) bspec)+
|
||||
apply (auto split: sum.splits)
|
||||
done
|
||||
|
||||
ML_file "legacy.ML"
|
||||
|
||||
end
|
||||
|
|
@ -1,118 +0,0 @@
|
|||
(*
|
||||
* Copyright 2014, NICTA
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_BSD2.txt" for details.
|
||||
*
|
||||
* @TAG(NICTA_BSD)
|
||||
*)
|
||||
|
||||
structure AutoCorresLegacy = struct
|
||||
|
||||
fun mk_l1corres_trivial_thm fn_info ctxt fn_name = let
|
||||
val info = Symtab.lookup (FunctionInfo.get_all_functions fn_info) fn_name
|
||||
|> the
|
||||
val const = #const info
|
||||
val impl_thm = Proof_Context.get_thm ctxt (fn_name ^ "_impl")
|
||||
val gamma = safe_mk_meta_eq impl_thm |> Thm.concl_of |> Logic.dest_equals
|
||||
|> fst |> (fn (f $ _) => f | t => raise TERM ("gamma", [t]))
|
||||
val thm = Utils.named_cterm_instantiate ctxt
|
||||
[("proc", Thm.cterm_of ctxt const), ("Gamma", Thm.cterm_of ctxt gamma)]
|
||||
@{thm L1corres_call_simpl}
|
||||
val body = SimplConv.get_body_of_l1corres_thm thm
|
||||
val term = Abs ("measure", @{typ nat}, body)
|
||||
in (term, thm) end
|
||||
|
||||
fun get_ext_l1corres_thm prog_info fn_info ctxt fn_name = let
|
||||
val callees = FunctionInfo.get_function_callees fn_info fn_name
|
||||
fun fake_callee nm = let
|
||||
val (term, thm) = mk_l1corres_trivial_thm fn_info ctxt nm
|
||||
in (nm, (false, term, thm)) end
|
||||
val callee_tab = Symtab.make (map fake_callee callees)
|
||||
in SimplConv.get_l1corres_thm prog_info fn_info ctxt true false fn_name
|
||||
callee_tab @{term "ameasure :: nat"} |> fst
|
||||
end
|
||||
|
||||
fun mk_l2corres_trivial_thm fn_info ctxt gs fn_name = let
|
||||
val info = Symtab.lookup (FunctionInfo.get_functions fn_info) fn_name
|
||||
|> the
|
||||
val const = #const info
|
||||
val args = #args info
|
||||
val impl_thm = Proof_Context.get_thm ctxt (fn_name ^ "_impl")
|
||||
val gamma = safe_mk_meta_eq impl_thm |> Thm.concl_of |> Logic.dest_equals
|
||||
|> fst |> (fn (f $ _) => f | t => raise TERM ("gamma", [t]))
|
||||
val (sT, gsT) = case strip_type (fastype_of gs) of
|
||||
([sT], gsT) => (sT, gsT) | _ => raise TERM ("mk_l2corres_trivial_thm", [gs])
|
||||
val ex_xf = Abs ("s", sT, HOLogic.unit)
|
||||
|
||||
fun set_domain_type (Const (s, T)) = Const (s, sT --> range_type T)
|
||||
| set_domain_type t = raise TERM ("set_domain_type", [t])
|
||||
val params = Symtab.lookup (#proc_info (Hoare.get_data ctxt))
|
||||
(fn_name ^ "_'proc") |> the |> #params
|
||||
|> map (apsnd (Proof_Context.read_const {proper=true, strict=true} ctxt #> set_domain_type))
|
||||
val arg_accs = filter (fn p => fst p = HoarePackage.In) params |> map snd
|
||||
val ret_accs = filter (fn p => fst p = HoarePackage.Out) params |> map snd
|
||||
|
||||
val arg_xf = Abs ("s", sT, HOLogic.mk_tuple (map (fn t => t $ Bound 0) arg_accs))
|
||||
val ret_xf = Abs ("s", sT, HOLogic.mk_tuple (map (fn t => t $ Bound 0) ret_accs))
|
||||
val arg_frees = map (fn (s, T) => Var ((s, 0), T)) args
|
||||
val arg_v = HOLogic.mk_tuple arg_frees
|
||||
|
||||
val thm = Utils.named_cterm_instantiate ctxt
|
||||
(map (apsnd (Thm.cterm_of ctxt))
|
||||
[("proc", const), ("Gamma", gamma), ("ex_xf", ex_xf), ("gs", gs),
|
||||
("ret_xf", ret_xf), ("arg_fn", arg_xf), ("args", arg_v)])
|
||||
@{thm L2corres_L2_call_simpl}
|
||||
val body = LocalVarExtract.get_body_of_thm ctxt thm
|
||||
val term = fold_rev Term.lambda (@{term "ameasure :: nat"} :: arg_frees) body
|
||||
in (term, thm) end
|
||||
|
||||
fun get_ext_l2corres_thm prog_info fn_info ctxt gs fn_name l1_body = let
|
||||
val callees = FunctionInfo.get_function_callees fn_info fn_name
|
||||
fun fake_callee nm = let
|
||||
val (term, thm) = mk_l2corres_trivial_thm fn_info ctxt gs nm
|
||||
in (nm, (false, term, thm)) end
|
||||
val callee_tab = Symtab.make (map fake_callee callees)
|
||||
val args = Symtab.lookup (FunctionInfo.get_functions fn_info) fn_name
|
||||
|> the |> #args
|
||||
val (thm, _) = LocalVarExtract.get_l2corres_thm ctxt prog_info fn_info true false fn_name
|
||||
callee_tab (map Free args) l1_body @{thm refl}
|
||||
val body = LocalVarExtract.get_body_of_thm ctxt thm
|
||||
in (body, Drule.generalize ([], map fst args) thm) end
|
||||
|
||||
fun get_ext_type_strengthen_thm ctxt prog_info fn_info fn_name body = let
|
||||
val rules = Monad_Types.get_ordered_rules ["nondet"] (Context.Proof @{context})
|
||||
|> hd
|
||||
val res = TypeStrengthen.perform_lift_and_polish ctxt prog_info fn_info rules true
|
||||
((Utils.named_cterm_instantiate ctxt [("t", Thm.cterm_of ctxt body)] @{thm refl}) |> mk_meta_eq)
|
||||
fn_name
|
||||
val args = Symtab.lookup (FunctionInfo.get_functions fn_info) fn_name
|
||||
|> the |> #args
|
||||
in case res of SOME (thm, _) => Drule.generalize ([], map fst args) thm
|
||||
| NONE => raise TERM ("get_ext_type_strengthen_thm: NONE", [])
|
||||
end
|
||||
|
||||
fun dest_ccorres_underlying_call t = case strip_comb t |> apsnd List.rev
|
||||
of (Const (@{const_name ccorres_underlying}, _),
|
||||
((Const (@{const_name com.Call}, _) $ proc) :: _)) => proc
|
||||
| _ => raise TERM ("dest_ccorres_underlying_call", [t])
|
||||
|
||||
fun tac prog_info fn_info globals ctxt = SUBGOAL (fn (t, i) => let
|
||||
val proc = dest_ccorres_underlying_call (HOLogic.dest_Trueprop
|
||||
(Logic.strip_assums_concl t))
|
||||
val fn_name = FunctionInfo.get_function_from_const fn_info proc
|
||||
|> the |> #name
|
||||
val l1corres = get_ext_l1corres_thm prog_info fn_info ctxt fn_name
|
||||
val l2corres = get_ext_l2corres_thm prog_info fn_info ctxt
|
||||
globals fn_name (SimplConv.get_body_of_l1corres_thm l1corres)
|
||||
val ts = get_ext_type_strengthen_thm ctxt prog_info fn_info
|
||||
fn_name (fst l2corres)
|
||||
in resolve0_tac [@{thm ccorres_underlying_autocorres}]
|
||||
THEN' resolve0_tac [l1corres] THEN' resolve0_tac [snd l2corres] THEN' resolve0_tac [ts] end i)
|
||||
|
||||
fun method prog_info fn_info globals
|
||||
= Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (tac
|
||||
prog_info fn_info globals ctxt 1))
|
||||
|
||||
end
|
||||
Loading…
Reference in New Issue