(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

theory Substitute

imports
  "CKernel.Kernel_C"
  "AsmRefine.GlobalsSwap"
begin

ML \<open>

structure SubstituteSpecs = struct

val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));

fun get_rhs thm =
    snd (Logic.dest_equals (Thm.concl_of thm))
    handle TYPE _ =>
      snd (HOLogic.dest_eq (Thm.concl_of thm));

fun get_lhs thm =
    fst (Logic.dest_equals (Thm.concl_of thm))
    handle TYPE _ =>
      fst (HOLogic.dest_eq (Thm.concl_of thm));

fun term_convert prefix convs (tm as Const (name, _)) =
    if not (String.isPrefix prefix name) then tm
    else the (Termtab.lookup convs tm)
  | term_convert _ _ tm = tm;

fun suspicious_term ctxt s t = if Term.add_var_names t [] = [] then ()
  else (tracing ("suspicious " ^ s);
    Syntax.pretty_term ctxt t |> Pretty.string_of |> tracing;
    ())

val debug_trace = ref (Bound 0);

fun convert prefix src_ctxt proc (tm as Const (name, _)) (convs, ctxt) =
  ((term_convert prefix convs tm; (convs, ctxt))
  handle Option =>
 let
    val cname = unprefix prefix name;
    val def_thm = Proof_Context.get_thm src_ctxt (cname ^ "_def")
    val rhs = get_rhs def_thm;
    val _ = suspicious_term ctxt "init rhs" rhs;
    val consts = Term.add_consts rhs [];
    val (convs, ctxt) = fold (convert prefix src_ctxt proc o Const)
        consts (convs, ctxt);
    val rhs' = map_aterms (term_convert prefix convs) rhs;
    val rhs'' = proc ctxt cname rhs';
    val _ = suspicious_term ctxt "adjusted rhs" rhs'';

  in if rhs'' aconv rhs
    then (Termtab.insert (K true) (tm, tm) convs,
        ctxt
        |> Local_Theory.open_target |> snd
        |> Local_Theory.abbrev Syntax.mode_default ((Binding.name cname, NoSyn), get_lhs def_thm)
        |> snd |> Local_Theory.note ((Binding.name (cname ^ "_def"), []), [def_thm])
        |> snd |> Local_Theory.close_target
    )

  else let
      val _ = tracing ("Defining " ^ cname);

      val pre_def_ctxt = ctxt
      val b = Binding.name cname
      val ctxt = Local_Theory.open_target ctxt |> snd
      val ((tm', _), ctxt) = Local_Theory.define
          ((b, NoSyn), ((Thm.def_binding b, []), rhs'')) ctxt
      val tm'' = Morphism.term (Proof_Context.export_morphism ctxt pre_def_ctxt) tm'
      val ctxt = Local_Theory.close_target ctxt

      val lhs_argTs = get_lhs def_thm |> strip_comb |> snd |> map fastype_of;
      val abs_tm = list_abs (map (pair "_") lhs_argTs, tm'')

    in (Termtab.insert (K true) (tm, abs_tm) convs, ctxt) end
  end)
  | convert _ _ _ (tm) _ = raise TERM ("convert: not Const", [tm])


fun prove_impl_tac ctxt ss =
    SUBGOAL (fn (t, n) => let
        val lhs = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst;
        val cnames = Term.add_const_names lhs []
          |> filter (String.isSuffix "_'proc");
        val unfolds = map (Proof_Context.get_thm ctxt o suffix "_def"
          o Long_Name.base_name) cnames;
      in simp_tac (put_simpset ss ctxt addsimps unfolds) n
      end);

fun convert_impls ctxt = let

    val thm = Proof_Context.get_thm ctxt "\<Gamma>_def"

    val proc_defs = (Term.add_const_names (Thm.concl_of thm) [])
      |> filter (String.isSuffix Hoare.proc_deco)
      |> map (suffix "_def" #> Proof_Context.get_thm ctxt)

    val tree_lemmata = StaticFun.prove_partial_map_thms thm
        (ctxt addsimps proc_defs)

    fun impl_name_from_proc (Const (s, _)) = s
            |> Long_Name.base_name
            |> unsuffix Hoare.proc_deco
            |> suffix HoarePackage.implementationN
      | impl_name_from_proc t = raise TERM ("impl_name_from_proc", [t])

    val saves = tree_lemmata |> map (apfst (fst #> impl_name_from_proc))

  in Local_Theory.notes (map (fn (n, t) => ((Binding.name n, []), [([t], [])])) saves)
    ctxt |> snd end

fun take_all_actions prefix src_ctxt proc tm csenv
      styargs ctxt = let
    val (_, ctxt) = convert prefix src_ctxt proc tm (Termtab.empty, ctxt);
  in ctxt
    |> convert_impls
    |> Modifies_Proofs.prove_all_modifies_goals_local csenv (fn _ => true) styargs
  end

end

\<close>

ML \<open>
fun com_rewrite f t = case fastype_of t of
    (comT as Type (@{type_name com}, [s, _, ft]))
      => let
    val gd = Const (@{const_name Guard},
                ft --> (HOLogic.mk_setT s) --> comT --> comT)
    fun add_guard ((f, gd_s), c) = gd $ f $ gd_s $ c;

    val seq = Const (@{const_name Seq}, comT --> comT --> comT);
    val skip = Const (@{const_name Skip}, comT);
    fun add_guards_to_seq gs (Const (@{const_name Seq}, _) $ a $ b)
        = seq $ add_guards_to_seq gs a $ b
      | add_guards_to_seq gs c
        = seq $ foldr add_guard skip gs $ c;

    fun add_guards c [] = c
      | add_guards ((w as Const (@{const_name While}, _)) $ S $ c) gs
        = seq $ (w $ S $ add_guards_to_seq gs c) $ foldr add_guard skip gs
      | add_guards (call as (Const (@{const_name call}, _) $ _ $ _ $ _ $ _)) gs
        = foldr add_guard (seq $ call $ foldr add_guard skip gs) gs
      | add_guards c gs = foldr add_guard c gs;

    fun inner t = case t of
      (Const (@{const_name "switch"}, T) $ v $ set_com_list) => let
        val (ss, cs) = map_split HOLogic.dest_prod
          (HOLogic.dest_list set_com_list);
        val cs' = map inner cs;
        val (v', gs) = f v;
        val (ss', gss) = map_split f ss;
        val listT = HOLogic.mk_prodT
          (HOLogic.mk_setT (range_type (domain_type T)), comT);
      in foldr add_guard (head_of t $ v' $ HOLogic.mk_list listT
            (map HOLogic.mk_prod (ss' ~~ cs')))
          (gs @ flat gss)
      end
      | _ => let
        val (h, xs) = strip_comb t;
        (* assumption: we can only get into the com type with one of the
           constructors or pseudo-constructors, which don't need rewriting,
           so we can ignore h *)
        val xTs = xs ~~ (fastype_of h |> strip_type |> fst);
        fun upd_arg (x, T) = if T = comT then (inner x, []) else f x;
        val (ys, gss) = map_split upd_arg xTs;
      in add_guards (list_comb (h, ys)) (flat gss) end
  in inner (Envir.beta_eta_contract t) end
  | _ => t;

\<close>

setup \<open>DefineGlobalsList.define_globals_list_i
  "../c/build/$L4V_ARCH/kernel_all.c_pp" @{typ globals}\<close>


locale substitute_pre
  = fixes symbol_table :: "string \<Rightarrow> addr"
      and domain :: "addr set"

begin

abbreviation
 "globals_list \<equiv> kernel_all_global_addresses.global_data_list"

end

locale kernel_all_substitute = substitute_pre
begin

ML \<open>
fun mk_rew (t as Abs (s, T, _)) = mk_rew (betapply (t, Var ((s, 0), T)))
  | mk_rew t = HOLogic.dest_eq t

val mk_varifyT = Term.map_types Logic.varifyT_global

local
val c_guard_rew =
  @{term "\<lambda>p b. Guard C_Guard {s. c_guard (p s)} b
     = Guard C_Guard {s. h_t_valid (hrs_htd (t_hrs_' (globals s))) c_guard (p s)} b"}
  |> mk_varifyT |> mk_rew

val c_guard_rew_weak =
  @{term "\<lambda>p b. Guard C_Guard {s. c_guard (p s)} b
         = Guard C_Guard {s. ptr_safe (p s) (hrs_htd (t_hrs_' (globals s)))
            \<and> c_guard (p s)} b"}
      |> mk_varifyT |> mk_rew

in
fun strengthen_c_guards ss thy s =
  if (exists (curry (=) s) ss)
  then Pattern.rewrite_term thy [c_guard_rew_weak] []
  else Pattern.rewrite_term thy [c_guard_rew] []
end;
\<close>

lemmas global_data_defs
    = kernel_all_global_addresses.global_data_defs

lemmas globals_list_def
    = kernel_all_global_addresses.global_data_list_def

ML \<open>

(* the unvarify sets ?symbol_table back to symbol_table. be careful *)
val global_datas = @{thms global_data_defs}
  |> map (Thm.concl_of #> Logic.unvarify_global
        #> Logic.dest_equals #> snd #> Envir.beta_eta_contract)

val const_globals = map_filter
    (fn (Const (@{const_name const_global_data}, _) $ nm $ t)
        => SOME (HOLogic.dest_string nm, t)
        | _ => NONE) global_datas

local

val hrs_htd_update_guard_rew1 =
    @{term "\<lambda>u. Basic (\<lambda>s. globals_update (t_hrs_'_update (hrs_htd_update (u s))) s)
         = Guard C_Guard {s. globals_list_distinct (fst ` dom_s (u s (hrs_htd (t_hrs_' (globals s)))))
                         symbol_table globals_list}
           (Basic (\<lambda>s. globals_update (t_hrs_'_update (id hrs_htd_update (u s))) s))"}
        |> mk_rew

val hrs_htd_update_guard_rew2 =
  @{term "t_hrs_'_update (id hrs_htd_update f) = t_hrs_'_update (hrs_htd_update f)"}
  |> Logic.varify_global |> HOLogic.dest_eq;

val consts = map snd const_globals

val index_eq_set_helper
  = Syntax.parse_term @{context} (String.concat
    ["\<lambda>str t n c. {s :: globals myvars. c \<longrightarrow>",
        "h_val (hrs_mem (t_hrs_' (globals s)))",
        " (CTypesDefs.ptr_add (Ptr (symbol_table str)) (of_nat (n s)))",
        " = t s}"])

val eq_set_helper
  = Syntax.parse_term @{context} (String.concat
    ["\<lambda>str t c. {s :: globals myvars. c \<longrightarrow>",
        "h_val (hrs_mem (t_hrs_' (globals s)))",
        " (Ptr (symbol_table str)) = t}"])

val s = @{term "s :: globals myvars"}

val grab_name_str = head_of #> dest_Const #> fst #> Long_Name.base_name
    #> HOLogic.mk_string

in

fun const_global_asserts ctxt cond
  (t as (Const (@{const_name index}, _) $ arr $ n)) = if member (=) consts arr
    then [(index_eq_set_helper $ grab_name_str arr
        $ lambda s t $ lambda s n $ cond) |> Syntax.check_term ctxt]
    else []
  | const_global_asserts ctxt cond (Const c) = if member (=) consts (Const c)
    then [(eq_set_helper $ grab_name_str (Const c) $ Const c $ cond)
        |> Syntax.check_term ctxt]
    else []
  | const_global_asserts ctxt cond (f $ x) = if member (=) consts (f $ x)
    then [(eq_set_helper $ grab_name_str (f $ x) $ (f $ x) $ cond)
        |> Syntax.check_term ctxt]
    else const_global_asserts ctxt cond f @ const_global_asserts ctxt cond x
  | const_global_asserts ctxt cond (a as Abs (_, @{typ "globals myvars"}, _))
    = const_global_asserts ctxt cond (betapply (a, s))
  | const_global_asserts ctxt cond (Abs (_, _, t))
    = const_global_asserts ctxt cond t
  | const_global_asserts _ _ _ = []

fun guard_rewritable_globals const_cond ctxt =
  Pattern.rewrite_term @{theory} [hrs_htd_update_guard_rew2] []
  o Pattern.rewrite_term @{theory} [hrs_htd_update_guard_rew1] []
  o com_rewrite (fn t =>
     (t, map (pair @{term C_Guard})
        (case const_cond of SOME cond => const_global_asserts ctxt cond t
                | NONE => [])))

val guard_htd_updates_with_domain = com_rewrite
  (fn t => if fastype_of t = @{typ "globals myvars \<Rightarrow> globals myvars"}
        andalso Term.exists_Const (fn (s, _) => s = @{const_name "hrs_htd_update"}) t
        then (t, [(@{term MemorySafety}, betapply (@{term "\<lambda>f :: globals myvars \<Rightarrow> globals myvars.
                {s. htd_safe domain (hrs_htd (t_hrs_' (globals s)))
              \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (f s))))}"}, t))])
        else (t, []))

val guard_halt = com_rewrite
  (fn t => if t = @{term "halt_'proc"}
    then (t, [(@{term DontReach}, @{term "{} :: globals myvars set"})])
    else (t, []))

fun acc_ptr_adds (Const (@{const_name h_val}, _) $ m $ (Const (@{const_name ptr_add}, _) $ p $ n))
    = [(p, n, true)] @ maps acc_ptr_adds [m, p, n]
  | acc_ptr_adds (Const (@{const_name heap_update}, _) $ (Const (@{const_name ptr_add}, _) $ p $ n))
    = [(p, n, true)] @ maps acc_ptr_adds [p, n]
  | acc_ptr_adds (Const (@{const_name ptr_add}, _) $ p $ n)
    = [(p, n, false)] @ maps acc_ptr_adds [p, n]
  | acc_ptr_adds (f $ x) = maps acc_ptr_adds [f, x]
  | acc_ptr_adds (abs as Abs (_, T, t)) = if T = @{typ "globals myvars"}
    then acc_ptr_adds (betapply (abs, @{term "s :: globals myvars"}))
    else acc_ptr_adds t
  | acc_ptr_adds _ = []

fun mk_bool true = @{term True} | mk_bool false = @{term False}

val guard_acc_ptr_adds = com_rewrite
  (fn t => (t, acc_ptr_adds t |> map (fn (p, n, strong) => let
    val assn = Const (@{const_name ptr_add_assertion'},
            fastype_of p --> @{typ "int \<Rightarrow> bool \<Rightarrow> heap_typ_desc \<Rightarrow> bool"})
        $ p $ n $ mk_bool strong
        $ @{term "hrs_htd (t_hrs_' (globals (s :: globals myvars)))"}
    val gd = HOLogic.mk_Collect ("s", @{typ "globals myvars"}, assn)
  in (@{term MemorySafety}, gd) end)))

end

\<close>

cond_sorry_modifies_proofs SORRY_MODIFIES_PROOFS

local_setup \<open>
SubstituteSpecs.take_all_actions
  "Kernel_C.kernel_all_global_addresses."
  (Locale.init "Kernel_C.kernel_all_global_addresses" @{theory})
  (fn ctxt => fn s => guard_rewritable_globals NONE ctxt
    o (strengthen_c_guards ["memset_body", "memcpy_body", "memzero_body"]
          (Proof_Context.theory_of ctxt) s)
    o guard_halt
    o guard_htd_updates_with_domain
    o guard_acc_ptr_adds)
  @{term kernel_all_global_addresses.\<Gamma>}
  (CalculateState.get_csenv @{theory} "../c/build/$L4V_ARCH/kernel_all.c_pp" |> the)
  [@{typ "globals myvars"}, @{typ int}, @{typ strictc_errortype}]
\<close>

end

end