Theory Default_St_Transfer

theory Default_St_Transfer
  imports Default_St_Algebra "Voblint_Framework.Transfer_Algebra"
begin

unbundle default_st_carrier_syntax

section ‹Refinement to variable-indexed states›

text ‹
  Everything so far is stated about locations. A program, though, talks about
  variable names, and which names are global is a property of the program, not
  of the carrier. ‹location_of› is that classifier applied: it turns a name
  into the location holding its value, and ‹default_st_rep_to_fun› maps a
  whole state to the function \<^typ>‹'a abs_state› it represents, the form
  soundness is stated over.

  The rest of the theory is the operations a call and a return need --
  assignment, formal binding, restriction to one side of the ownership split,
  frame entry, and the caller/callee combination -- each paired with the
  equation saying that performing it on the carrier and then taking the
  represented function agrees with performing its counterpart on that
  function. Those equations are the interface every soundness proof downstream
  actually uses.
›

subsection ‹Location classification and projection›

definition location_of ::
  "(vname => bool) => vname => location" where
  "location_of 𝒢 x =
     (if 𝒢 x then Global_Location x else Local_Location x)"

text ‹
  Both tags carry the vname they classify, so a classified location determines
  its own name and two names collide only when they are equal.  Proofs about
  \<^const>‹location_of› therefore need no case split on \<^term>‹𝒢 x› against
  \<^term>‹𝒢 y›.
›

lemma location_vname_location_of [simp]:
  "location_vname (location_of 𝒢 x) = x"
  by (simp add: location_of_def)

lemma location_of_eq_iff [simp]:
  "location_of 𝒢 x = location_of 𝒢 y ⟷ x = y"
  by (auto simp: location_of_def)

text ‹
  Deliberately no ‹[simp]› rule matching \<^term>‹location_of 𝒢 x = Local_Location y›
  against a constructor. Such a rule reads well in isolation, but proofs here
  derive facts of exactly that shape and then use them as rewrites for
  \<^const>‹location_of›; a simp rule on the same left-hand side collapses the
  equation to its classification side and takes the rewrite away.
›

definition default_st_rep_to_fun ::
  "(vname => bool) => ('a::bot) default_st_rep => vname => 'a" where
  "default_st_rep_to_fun 𝒢 s x =
     default_st_rep_get s (location_of 𝒢 x)"

lemma default_st_rep_to_fun_set_location [simp]:
  "default_st_rep_to_fun 𝒢
      (default_st_rep_set s (location_of 𝒢 x) a) =
   (default_st_rep_to_fun 𝒢 s)(x := a)"
proof (rule ext)
  fix y
  show "default_st_rep_to_fun 𝒢
      (default_st_rep_set s (location_of 𝒢 x) a) y =
    ((default_st_rep_to_fun 𝒢 s)(x := a)) y"
    unfolding default_st_rep_to_fun_def    by (cases "x = y"; cases "𝒢 x"; cases "𝒢 y";
        simp_all add: location_of_def)
qed


definition default_st_to_fun ::
  "(vname => bool) => ('a::bot) default_st => vname => 'a"
where
  "default_st_to_fun 𝒢 s x =
     s⟨location_of 𝒢 x⟩"

text ‹
  The function a state represents is its \<^const>‹readback›, written
  ‹ρ⇘𝒢⇙ s›; a lifted state reads back pointwise under the lift.
  The notation joins the carrier notation in the opt-in bundle
  ‹default_st_syntax›: vendored theories bind ‹ρ› as a
  variable, so it must never be global.
›

adhoc_overloading readback == default_st_to_fun

bundle default_st_syntax
begin
unbundle default_st_carrier_syntax
notation readback ("ρ⇘_⇙")
end

unbundle default_st_syntax

lemma default_st_to_fun_bot [simp]:
  "ρ⇘𝒢⇙ (bot :: ('a::order_bot) default_st) = bot"
  by (rule ext) (simp add: default_st_to_fun_def)

text ‹
  The state a run starts in gives every local one value and every global
  another: C initializes a declared global to zero and leaves a local
  unconstrained. Each domain's C-initial state is this construction at its own
  abstraction of zero and its whole-value element, so the equation for its
  function is one lemma rather than one per domain. The two empty dictionaries
  are abstracted directly rather than lifted, because a domain whose value type
  is itself a typedef would otherwise descend through both quotients.
›

definition initial_default_st :: "'a::bot => 'a => 'a default_st" where
  "initial_default_st local_value global_value =
     ⟪(local_value, []), (global_value, [])⟫"

lemma default_st_get_initial [simp]:
  "ρ⇘𝒢⇙ (initial_default_st local_value global_value) x =
   (if 𝒢 x then global_value else local_value)"
  unfolding default_st_to_fun_def initial_default_st_def
  by (auto simp: location_of_def split: if_splits)

lemma default_st_to_fun_initial:
  "ρ⇘𝒢⇙ (initial_default_st local_value global_value) =
   (λx. if 𝒢 x then global_value else local_value)"
  by (rule ext) simp

text ‹
  The quotient-level projection agrees with the raw one at ‹s›'s own chosen
  representative -- so any raw-level fact about @{const default_st_rep_to_fun}
  transports directly to @{const default_st_to_fun} through
  @{const rep_default_st}, with no separate quotient-respectfulness argument
  needed: @{const rep_default_st} is a genuine function of ‹s›, so anything
  defined through it is automatically well-defined on the quotient.
›

lemma default_st_to_fun_rep:
  "ρ⇘𝒢⇙ s = default_st_rep_to_fun 𝒢 (rep_default_st s)"
  unfolding default_st_to_fun_def default_st_rep_to_fun_def
  by (rule ext) (simp add: default_st_get_rep)

lemma default_st_to_fun_mono:
  assumes "s ≤ t"
  shows "ρ⇘𝒢⇙ s ≤ ρ⇘𝒢⇙ t"
  using assms
  unfolding default_st_to_fun_def le_fun_def
  by (simp add: le_default_st_iff)


text ‹
  Each quotient-level refinement equation is its raw counterpart transported
  along the quotient: unfolding the projection leaves a goal in
  \<^const>‹default_st_get›, ‹transfer› lowers it to
  \<^const>‹default_st_rep_get›, and the raw lemma -- read at the same unfolded
  shape -- closes it. An operation returning the quotient has no ‹rep_eq› to
  unfold instead, since its representative is fixed only up to
  \<^const>‹eq_default_st_rep›.
›


subsection ‹Assignment and formal binding›

definition combine_assign_default_st_rep ::
  "(vname => bool) => vname option => 'a => ('a::bot) default_st_rep
   => 'a default_st_rep"
where
  "combine_assign_default_st_rep 𝒢 dst v s =
     (case dst of None => s
      | Some x => default_st_rep_set s (location_of 𝒢 x) v)"

lemma eq_default_st_rep_combine_assign:
  assumes "eq_default_st_rep s t"
  shows "eq_default_st_rep (combine_assign_default_st_rep 𝒢 dst v s)
      (combine_assign_default_st_rep 𝒢 dst v t)"
  by (unfold combine_assign_default_st_rep_def; cases dst;
      simp_all add: assms eq_default_st_rep_set)

lift_definition combine_assign_default_st ::
  "(vname => bool) => vname option => 'a => ('a::bot) default_st
   => 'a default_st"
  is combine_assign_default_st_rep
  by (rule eq_default_st_rep_combine_assign)

lemma default_st_get_combine_assign [simp]:
  "(combine_assign_default_st 𝒢 dst v s)⟨loc⟩ =
     (case dst of
        None => s⟨loc⟩
      | Some x => if location_of 𝒢 x = loc then v else s⟨loc⟩)"
  by transfer (auto simp add:combine_assign_default_st_rep_def split:option.splits)

lemma default_st_rep_to_fun_combine_assign [simp]:
  "default_st_rep_to_fun 𝒢
      (combine_assign_default_st_rep 𝒢 dst v s) =
   combine_assign dst v (default_st_rep_to_fun 𝒢 s)"
  by (cases dst)
     (simp_all add: combine_assign_default_st_rep_def)

lemma default_st_to_fun_combine_assign [simp]:
  "ρ⇘𝒢⇙
      (combine_assign_default_st 𝒢 dst v s) =
   combine_assign dst v (ρ⇘𝒢⇙ s)"
  unfolding default_st_to_fun_def
  by transfer
     (rule default_st_rep_to_fun_combine_assign[unfolded default_st_rep_to_fun_def])

definition bind_formals_default_st_rep ::
  "(vname => bool) => vname list => 'a list => ('a::bot) default_st_rep
   => 'a default_st_rep"
where
  "bind_formals_default_st_rep 𝒢 xs avs s =
     fold (λ(x, a) t. default_st_rep_set t (location_of 𝒢 x) a)
       (zip xs avs) s"

lemma eq_default_st_rep_fold_set:
  "eq_default_st_rep s t ⟹
     eq_default_st_rep
       (fold (λ(x, a) t. default_st_rep_set t (location_of 𝒢 x) a) ps s)
       (fold (λ(x, a) t. default_st_rep_set t (location_of 𝒢 x) a) ps t)"
proof (induction ps arbitrary: s t)
  case Nil
  then show ?case by simp
next
  case (Cons p ps)
  then show ?case
    by (cases p) (simp_all add: eq_default_st_rep_set)
qed

lemma eq_default_st_rep_bind_formals:
  assumes "eq_default_st_rep s t"
  shows "eq_default_st_rep (bind_formals_default_st_rep 𝒢 xs avs s)
      (bind_formals_default_st_rep 𝒢 xs avs t)"
  unfolding bind_formals_default_st_rep_def
  using assms by (rule eq_default_st_rep_fold_set)

lift_definition bind_formals_default_st ::
  "(vname => bool) => vname list => 'a list => ('a::bot) default_st
   => 'a default_st"
  is bind_formals_default_st_rep
  by (rule eq_default_st_rep_bind_formals)

text ‹A single-formal call binds exactly one location, so its reduction is a
  plain \<^const>‹default_st_set›. An instance with a
  one-argument procedure call cites this directly instead of unfolding
  \<^const>‹bind_formals_default_st›'s fold.›

lemma bind_formals_default_st_singleton:
  "bind_formals_default_st 𝒢 [x] [a] s = s⟨location_of 𝒢 x := a⟩"
  by transfer (simp add: bind_formals_default_st_rep_def eq_default_st_rep_def)

lemma default_st_rep_to_fun_fold_set:
  "default_st_rep_to_fun 𝒢
      (fold (λ(x, a) t. default_st_rep_set t (location_of 𝒢 x) a) ps s) =
   fold (λ(x, a) t. t(x := a)) ps
      (default_st_rep_to_fun 𝒢 s)"
  by (induction ps arbitrary: s)
     (simp_all split: prod.splits)

lemma default_st_rep_to_fun_bind_formals [simp]:
  "default_st_rep_to_fun 𝒢
      (bind_formals_default_st_rep 𝒢 xs avs s) =
   bind_formals xs avs (default_st_rep_to_fun 𝒢 s)"
  unfolding bind_formals_default_st_rep_def
  by (rule default_st_rep_to_fun_fold_set)

lemma default_st_to_fun_bind_formals [simp]:
  "ρ⇘𝒢⇙
      (bind_formals_default_st 𝒢 xs avs s) =
   bind_formals xs avs (ρ⇘𝒢⇙ s)"
  unfolding default_st_to_fun_def
  by transfer
     (rule default_st_rep_to_fun_bind_formals[unfolded default_st_rep_to_fun_def])

lemma default_st_to_fun_set [simp]:
  "ρ⇘𝒢⇙ s⟨location_of 𝒢 x := a⟩ =
   (ρ⇘𝒢⇙ s)(x := a)"
proof (rule ext)
  fix y
  show "ρ⇘𝒢⇙ s⟨location_of 𝒢 x := a⟩ y =
    ((ρ⇘𝒢⇙ s)(x := a)) y"
    unfolding default_st_to_fun_def
    by (cases "x = y"; cases "𝒢 x"; cases "𝒢 y";
        simp_all add: location_of_def)
qed


subsection ‹Ownership restriction and combination›

text ‹
  Each dictionary holds one partition, so the ownership operations below move
  whole dictionaries: a restriction keeps one and empties the other to
  ‹bot›, and the combination takes the caller's local dictionary and the
  callee's global one.
›

definition restrict_local_default_st_rep ::
  "('a::bot) default_st_rep => 'a default_st_rep" where
  "restrict_local_default_st_rep s = (fst s, (bot, []))"

definition restrict_global_default_st_rep ::
  "('a::bot) default_st_rep => 'a default_st_rep" where
  "restrict_global_default_st_rep s = ((bot, []), snd s)"


lemma default_st_rep_get_restrict_local:
  "default_st_rep_get (restrict_local_default_st_rep s) loc =
     (case loc of
        Local_Location x => default_st_rep_get s loc
      | Global_Location x => bot)"
  by (cases s; cases loc) (simp_all add: restrict_local_default_st_rep_def)

lemma default_st_rep_get_restrict_global:
  "default_st_rep_get (restrict_global_default_st_rep s) loc =
     (case loc of
        Local_Location x => bot
      | Global_Location x => default_st_rep_get s loc)"
  by (cases s; cases loc) (simp_all add: restrict_global_default_st_rep_def)

lemma eq_default_st_rep_restrict_local:
  assumes "eq_default_st_rep s t"
  shows "eq_default_st_rep (restrict_local_default_st_rep s)
      (restrict_local_default_st_rep t)"
  by (rule eq_default_st_repI)
     (simp add: default_st_rep_get_restrict_local eq_default_st_repD[OF assms]
       split: location.split)

lemma eq_default_st_rep_restrict_global:
  assumes "eq_default_st_rep s t"
  shows "eq_default_st_rep (restrict_global_default_st_rep s)
      (restrict_global_default_st_rep t)"
  by (rule eq_default_st_repI)
     (simp add: default_st_rep_get_restrict_global eq_default_st_repD[OF assms]
       split: location.split)

lift_definition restrict_local_default_st ::
  "('a::bot) default_st => 'a default_st"
  is restrict_local_default_st_rep
  by (rule eq_default_st_rep_restrict_local)

lift_definition restrict_global_default_st ::
  "('a::bot) default_st => 'a default_st"
  is restrict_global_default_st_rep
  by (rule eq_default_st_rep_restrict_global)

text ‹
  \<^const>‹restrict_local_default_st›/\<^const>‹restrict_global_default_st›
  preserve the caller's semantic default over the (potentially infinite)
  location space: the kept side carries over its input's own dictionary
  verbatim, whose default need not be \<^term>‹bot›, and only the dropped side
  is replaced by the empty dictionary over \<^term>‹bot›. A scope-parametric
  projection over a bounded materialized support would disagree with this
  pair outside its bound, so the pair is stated over the full location
  space and preserves the default by construction.
›

lemma default_st_get_restrict_local [simp]:
  "(restrict_local_default_st s)⟨loc⟩ =
     (case loc of
        Local_Location x => s⟨loc⟩
      | Global_Location x => bot)"
  by transfer (rule default_st_rep_get_restrict_local)

lemma default_st_get_restrict_global [simp]:
  "(restrict_global_default_st s)⟨loc⟩ =
     (case loc of
        Local_Location x => bot
      | Global_Location x => s⟨loc⟩)"
  by transfer (rule default_st_rep_get_restrict_global)

lemma default_st_to_fun_restrict_local [simp]:
  "ρ⇘𝒢⇙ (restrict_local_default_st s) x =
     (if 𝒢 x then bot else ρ⇘𝒢⇙ s x)"
  unfolding default_st_to_fun_def location_of_def
  by (cases "𝒢 x") simp_all

lemma default_st_to_fun_restrict_global [simp]:
  "ρ⇘𝒢⇙ (restrict_global_default_st s) x =
     (if 𝒢 x then ρ⇘𝒢⇙ s x else bot)"
  unfolding default_st_to_fun_def location_of_def
  by (cases "𝒢 x") simp_all

definition combine_default_st_rep ::
  "('a::bot) default_st_rep => 'a default_st_rep => 'a default_st_rep"
where
  "combine_default_st_rep sc se = (fst sc, snd se)"

lemma default_st_rep_get_combine [simp]:
  "default_st_rep_get (combine_default_st_rep sc se) loc =
   (case loc of
      Local_Location x => default_st_rep_get sc loc
    | Global_Location x => default_st_rep_get se loc)"
  by (cases sc; cases se; cases loc) (simp_all add: combine_default_st_rep_def)

lemma eq_default_st_rep_combine:
  assumes "eq_default_st_rep sc1 sc2"
    and "eq_default_st_rep se1 se2"
  shows "eq_default_st_rep (combine_default_st_rep sc1 se1)
      (combine_default_st_rep sc2 se2)"
  by (rule eq_default_st_repI)
     (simp add: eq_default_st_repD[OF assms(1)] eq_default_st_repD[OF assms(2)]
       split: location.split)

lift_definition combine_default_st ::
  "('a::bot) default_st => 'a default_st => 'a default_st"
  is combine_default_st_rep
  by (rule eq_default_st_rep_combine)

lemma default_st_get_combine [simp]:
  "(combine_default_st sc se)⟨loc⟩ =
     (case loc of
        Local_Location x => sc⟨loc⟩
      | Global_Location x => se⟨loc⟩)"
  by transfer (rule default_st_rep_get_combine)


lemma default_st_rep_to_fun_combine [simp]:
  "default_st_rep_to_fun 𝒢 (combine_default_st_rep sc se) =
   combine_env 𝒢 (default_st_rep_to_fun 𝒢 sc)
     (default_st_rep_to_fun 𝒢 se)"
proof (rule ext)
  fix x
  show "default_st_rep_to_fun 𝒢 (combine_default_st_rep sc se) x =
      combine_env 𝒢 (default_st_rep_to_fun 𝒢 sc)
        (default_st_rep_to_fun 𝒢 se) x"
    unfolding default_st_rep_to_fun_def combine_env_def location_of_def
    by (cases "𝒢 x") simp_all
qed

lemma default_st_to_fun_combine [simp]:
  "ρ⇘𝒢⇙ (combine_default_st sc se) =
   combine_env 𝒢 (ρ⇘𝒢⇙ sc)
     (ρ⇘𝒢⇙ se)"
proof (rule ext)
  fix x
  show "ρ⇘𝒢⇙ (combine_default_st sc se) x =
      combine_env 𝒢 (ρ⇘𝒢⇙ sc)
        (ρ⇘𝒢⇙ se) x"
    unfolding default_st_to_fun_def combine_env_def location_of_def
    by (cases "𝒢 x") simp_all
qed


lemma default_st_to_fun_sup [simp]:
  "ρ⇘𝒢⇙ (s ⊔ t) =
   ρ⇘𝒢⇙ s ⊔ ρ⇘𝒢⇙ t"
  by (rule ext) (simp add: default_st_to_fun_def sup_fun_def)


subsection ‹Frame entry›

text ‹
  Entering a frame sets every local to ‹top_val› and keeps the globals;
  the lemmas carry this through the quotient and the readback.
›

definition enter_frame_D_default_st_rep ::
  "'a => ('a::bot) default_st_rep => 'a default_st_rep"
where
  "enter_frame_D_default_st_rep top_val s = ((top_val, []), snd s)"

lemma default_st_rep_get_enter_frame_D [simp]:
  "default_st_rep_get (enter_frame_D_default_st_rep top_val s) loc =
   (case loc of
      Local_Location x => top_val
    | Global_Location x => default_st_rep_get s loc)"
  by (cases s; cases loc) (simp_all add: enter_frame_D_default_st_rep_def)

lemma eq_default_st_rep_enter_frame_D:
  assumes "eq_default_st_rep s t"
  shows "eq_default_st_rep (enter_frame_D_default_st_rep top_val s)
      (enter_frame_D_default_st_rep top_val t)"
  by (rule eq_default_st_repI)
     (simp add: eq_default_st_repD[OF assms] split: location.split)

lift_definition enter_frame_D_default_st ::
  "'a => ('a::bot) default_st => 'a default_st"
  is enter_frame_D_default_st_rep
  by (rule eq_default_st_rep_enter_frame_D)

lemma default_st_get_enter_frame_D [simp]:
  "(enter_frame_D_default_st top_val s)⟨loc⟩ =
     (case loc of
        Local_Location x => top_val
      | Global_Location x => s⟨loc⟩)"
  by transfer (rule default_st_rep_get_enter_frame_D)

lemma default_st_rep_to_fun_enter_frame [simp]:
  "default_st_rep_to_fun 𝒢 (enter_frame_D_default_st_rep top_val s) =
   enter_frame 𝒢 top_val (default_st_rep_to_fun 𝒢 s)"
proof (rule ext)
  fix x
  show "default_st_rep_to_fun 𝒢 (enter_frame_D_default_st_rep top_val s) x =
      enter_frame 𝒢 top_val (default_st_rep_to_fun 𝒢 s) x"
    unfolding enter_frame_def default_st_rep_to_fun_def location_of_def
    by (cases "𝒢 x") simp_all
qed

lemma default_st_to_fun_enter_frame [simp]:
  "ρ⇘𝒢⇙
      (enter_frame_D_default_st top_val s) =
   enter_frame 𝒢 top_val (ρ⇘𝒢⇙ s)"
  unfolding default_st_to_fun_def
  by transfer
     (rule default_st_rep_to_fun_enter_frame[unfolded default_st_rep_to_fun_def])


subsection ‹Executable restriction and combination laws›

text ‹
  Algebraic identities of the carrier itself: no abstract state, no
  concretization, no classifier. They say that combining and then projecting
  recovers the projected side, and that the two projections recombine by join.
  Executable trees use them to split and rebuild a routed state.
›

lemma combine_default_st_eq_restrict_sup:
  "combine_default_st A B =
     restrict_local_default_st A ⊔ restrict_global_default_st B"
  by (rule default_st_eqI) (simp split: location.split)

lemma restrict_local_default_st_combine [simp]:
  "restrict_local_default_st (combine_default_st A B) =
     restrict_local_default_st A"
  by (rule default_st_eqI) (simp split: location.split)

lemma restrict_global_default_st_combine [simp]:
  "restrict_global_default_st (combine_default_st A B) =
     restrict_global_default_st B"
  by (rule default_st_eqI) (simp split: location.split)

lemma restrict_local_default_st_split [simp]:
  "restrict_local_default_st (restrict_local_default_st A ⊔
      restrict_global_default_st B) = restrict_local_default_st A"
  by (rule default_st_eqI) (simp split: location.split)

lemma restrict_global_default_st_split [simp]:
  "restrict_global_default_st (restrict_local_default_st A ⊔
      restrict_global_default_st B) = restrict_global_default_st B"
  by (rule default_st_eqI) (simp split: location.split)

text ‹
  Combining reads only the local half of its first argument and the global half
  of its second, so a state recombines from its own two projections.
›

lemma combine_default_st_restrict_split [simp]:
  "combine_default_st (restrict_local_default_st x) (restrict_global_default_st x) = x"
  by (rule default_st_eqI) (simp split: location.split)

lemma combine_default_st_restrict_local_left [simp]:
  "combine_default_st (restrict_local_default_st x) y = combine_default_st x y"
  by (rule default_st_eqI) (simp split: location.split)

lemma combine_default_st_self_restrict_global [simp]:
  "combine_default_st x (restrict_global_default_st x) = x"
  by (rule default_st_eqI) (simp split: location.split)

subsection ‹The stores a carrier state describes›

text ‹
  A carrier state denotes the stores its function denotes. This is the one
  concretization the carrier offers to semantic statements; the represented
  function itself stays a refinement device, used to relate carrier operations
  to their counterparts on \<^typ>‹'a abs_state›. Only the classifier
  ‹𝒢› is needed besides the state, because it decides which location holds each
  name's value. A context that fixes ‹𝒢› may register
  ‹default_st_gamma 𝒢› under ‹γ _› with ‹adhoc_overloading›.
›

definition default_st_gamma ::
  "(vname => bool) => ('a::numeric_domain) default_st => store set" where
  "default_st_gamma 𝒢 s = γ (ρ⇘𝒢⇙ s)"

lemma default_st_gamma_mono:
  "s ≤ t ⟹ default_st_gamma 𝒢 s ⊆ default_st_gamma 𝒢 t"
  unfolding default_st_gamma_def by (intro gamma_state_mono default_st_to_fun_mono)

lemma default_st_gamma_bot [simp]: "default_st_gamma 𝒢 bot = {}"
  by (simp add: default_st_gamma_def)

lemma default_st_gamma_initial:
  "default_st_gamma 𝒢 (initial_default_st local_value global_value) =
   γ (λx. if 𝒢 x then global_value else local_value)"
  by (simp add: default_st_gamma_def default_st_to_fun_initial)

unbundle no default_st_syntax

end