Theory TD.Update_rules

section ‹An Interface for Update Rules›

theory Update_rules
  imports Basics_side Warrowing
begin

subsection ‹Definition of Update Rules for Globals›

record ('x,'g,'d) ug_state =
  ρ :: "'g ⇒ ('x, 'd) fmap"

lemma rho_truncate [simp]: "ρ (ug_state.truncate s) = ρ s"
  by (simp add: ug_state.defs)

abbreviation rho_lookup :: "('g ⇒ ('x, 'd::bot) fmap) ⇒ 'g ⇒ 'x ⇒ 'd" where
  "rho_lookup rho g orig ≡ fmlookup_default (rho g) ⊥ orig"

interpretation s: comp_fun_commute "((⊔) :: 'd::bounded_semilattice_sup_bot ⇒ _ ⇒ _)"
  by standard (simp add: sup_left_commute comp_def)

definition sup_fset :: "'d::semilattice_sup fset ⇒ 'd" where
  "sup_fset S ≡ ⨆⇩f⇩i⇩n (fset S)"

lemma sup_fset_upper: "i |∈| S ⟹ i ≤ sup_fset S"
  unfolding sup_fset_def
  by (induct S) (auto simp add: Sup_fin.coboundedI)

definition sup_over_origins ::
  "('x,'g,'d :: bounded_semilattice_sup_bot,'a) ug_state_scheme ⇒ 'g ⇒ 'd" where
  "sup_over_origins state g = sup_fset (rho_lookup (ρ state) g |`| fmdom (ρ state g))"

lemma sup_over_origins_upper: "rho_lookup (ρ state) g orig = d ⟹ d ≤ sup_over_origins state g"
  unfolding sup_over_origins_def
  apply (cases "orig |∈| fmdom (ρ state g)")
  apply (intro sup_fset_upper fimage_eqI[where ?x=orig])
  by (auto simp add: fmlookup_default_def fmlookup_dom_iff)

locale update_rule =
  fixes init_ug_state :: "('x,'g,'d :: order_bot,'a) ug_state_scheme"
  and update_global ::
    "'d ⇒ 'x ⇒ 'g ⇒ 'd ⇒ ('x,'g,'d,'a) ug_state_scheme
      ⇒ 'd option × ('x,'g,'d,'a) ug_state_scheme"
  assumes init_rho_leq_bot: "∀g orig. rho_lookup (ρ init_ug_state) g orig ≤ ⊥"
  and update_global_untouched:
    "(do, state') = update_global d orig g d' state ⟹ g' ≠ g
      ⟹ rho_lookup (ρ state') g' orig' = rho_lookup (ρ state) g' orig'"
    "(do, state') = update_global d orig g d' state ⟹ orig' ≠ orig
      ⟹ rho_lookup (ρ state') g' orig' = rho_lookup (ρ state) g' orig'"
  and update_global_recorded_in_rho:
    "(do, state') = update_global d orig g d' state ⟹ d' ≤ rho_lookup (ρ state') g orig"
  and update_global_preserves_rho_invariant:
    "(None, state') = update_global d orig g d' state ⟹ ∀orig. rho_lookup (ρ state) g orig ≤ d
     ⟹ rho_lookup (ρ state') g orig ≤ d"
    "(Some d'', state') = update_global d orig g d' state
     ⟹ ∀orig. rho_lookup (ρ state) g orig ≤ d ⟹ rho_lookup (ρ state') g orig' ≤ d''"

text‹Update rule Listing 3
     (modification: always return some to always record contribution in rho, the
     equal-to-sigma check is done by the solver anyway)›

definition init_basic_ug_state :: "('x,'g,'d::order_bot) ug_state" where
  "init_basic_ug_state ≡ ⦇ρ = λ_. fmempty ⦈"

definition update_global_always_join ::
  "'d ⇒ 'x ⇒ 'g ⇒ 'd :: bounded_semilattice_sup_bot ⇒ ('x,'g,'d) ug_state
    ⇒ 'd option × ('x,'g,'d) ug_state" where
  "update_global_always_join d orig g d' state ≡
    let state = state⦇ρ := (ρ state)(g := fmupd orig d' ((ρ state) g))⦈ in
    let d' = d ⊔ d' in
    if d' = d then (None, state) else (Some d', state)"

interpretation always_join: update_rule init_basic_ug_state update_global_always_join
  unfolding update_rule_def update_global_always_join_def init_basic_ug_state_def
    fmlookup_default_def
  apply (auto simp add: Let_def fun_upd_def simp flip: sup.absorb_iff1 split: if_splits)
  by (auto intro: le_supI1)

text‹Update rule Listing 4
     (modification: always return some to always record contribution in rho, the
     equal-to-sigma check is done by the solver anyway)›

definition update_global_per_origin ::
  "'d ⇒ 'x ⇒ 'g ⇒ 'd :: bounded_semilattice_sup_bot ⇒ ('x,'g,'d) ug_state
    ⇒ 'd option × ('x,'g,'d) ug_state" where
  "update_global_per_origin d orig g d' state ≡
    let state = state⦇ρ := (ρ state)(g := fmupd orig d' (ρ state g))⦈ in
    let d' = sup_over_origins state g in
    if d' = d then (None, state) else (Some d', state)"

interpretation per_origin: update_rule init_basic_ug_state update_global_per_origin
  unfolding update_rule_def update_global_per_origin_def init_basic_ug_state_def
  apply (auto intro: sup_over_origins_upper ord_le_eq_trans[OF sup_ge1]
      simp add: Let_def fmlookup_default_def split: option.splits)
  subgoal for _ _ _ _ _ orig'
    apply (intro sup_over_origins_upper[where ?orig=orig'])
    by (simp add: fmlookup_default_def)
  done

text‹Update rule Listing 5: update globals using widening and narrowing following Apinis'13
     (modification: always return some to always record contribution in rho, the
     equal-to-sigma check is done by the solver anyway)›

definition update_global_warrowing_apinis ::
  "'d ⇒ 'x ⇒ 'g ⇒ 'd :: {bounded_semilattice_sup_bot,warrowing} ⇒ ('x,'g,'d) ug_state
    ⇒ 'd option × ('x,'g,'d) ug_state" where
  "update_global_warrowing_apinis d orig g d' state ≡
    (if rho_lookup (ρ state) g orig = d' then (None, state) else
    let state = state⦇ρ := (ρ state)(g := fmupd orig d' (ρ state g))⦈ in
    let d' = d ∇Δ (sup_over_origins state g) in
    (Some d', state))"

interpretation warrowing_apinis: update_rule init_basic_ug_state update_global_warrowing_apinis
  unfolding update_rule_def update_global_warrowing_apinis_def init_basic_ug_state_def
  by (auto intro!: sup_over_origins_upper order.trans[OF sup_ge1 warrowing_properties(1)]
      order.trans[OF _ warrowing_properties(1)]
      simp add: Let_def fmlookup_default_def
      split: if_splits option.splits)

text‹Update rule Listing 7: employ warrowing per origin and recompute the join over all origins as
  return value.›

definition update_global_warrowing_per_origin ::
  "'d ⇒ 'x ⇒ 'g ⇒ 'd :: {bounded_semilattice_sup_bot,warrowing} ⇒ ('x,'g,'d) ug_state
    ⇒ 'd option × ('x,'g,'d) ug_state" where
  "update_global_warrowing_per_origin d orig g d' state ≡
    (if rho_lookup (ρ state) g orig = d' then (None, state) else
    let warrow_per_orig = rho_lookup (ρ state) g orig ∇Δ d' in
    let state = state⦇ρ := (ρ state)(g := fmupd orig warrow_per_orig (ρ state g))⦈ in
    let join_over_origins = sup_over_origins state g in
    (Some join_over_origins, state))"

interpretation warrowing_per_origin:
    update_rule init_basic_ug_state update_global_warrowing_per_origin
  unfolding update_rule_def update_global_warrowing_per_origin_def init_basic_ug_state_def
  by (auto intro!: sup_over_origins_upper warrowing_properties(1)
      simp add: Let_def fmlookup_default_def
      split: if_splits option.split)

text‹Update rule Listing 9: localized widening and bounded narrowing.›

datatype phase = Widening | Narrowing

record ('x,'g,'d) ug_state_with_gas = "('x,'g,'d) ug_state" +
  gas :: "'g ⇒ 'x ⇒ phase × nat"

definition init_ug_state_with_gas :: "('x,'g,'d::order_bot) ug_state_with_gas" where
  "init_ug_state_with_gas ≡ ⦇ρ = λ_. fmempty, gas = λ_ _. (Widening,0) ⦈"

definition update_global_bounded_narrowing ::
  "nat ⇒ 'd ⇒ 'x ⇒ 'g ⇒ 'd :: {bounded_semilattice_sup_bot,warrowing}
    ⇒ ('x,'g,'d) ug_state_with_gas ⇒ 'd option × ('x,'g,'d) ug_state_with_gas" where
  "update_global_bounded_narrowing I d orig g d' state ≡ (
    if rho_lookup (ρ state) g orig = d' then (None, state) else
    let (phase, i) = gas state g orig in
    if d' ≤ rho_lookup (ρ state) g orig ∧ phase = Narrowing ∧ i ≥ I then (None, state) else
    let (d', phase, i) = (
      if ¬ d' ≤ rho_lookup (ρ state) g orig then (rho_lookup (ρ state) g orig ∇ d', Widening, i)
      else if phase = Narrowing then (rho_lookup (ρ state) g orig Δ d', phase, i)
      else (rho_lookup (ρ state) g orig Δ d', Narrowing, i + 1)) in
    let state = state⦇ρ := (ρ state)(g := fmupd orig d' (ρ state g)),
          gas := (gas state)(g := (gas state g)(orig := (phase, i)))⦈ in
    let join_over_origins = sup_over_origins state g in
    if join_over_origins = d then (None, state) else (Some join_over_origins, state))"

interpretation bounded_narrowing:
    update_rule init_ug_state_with_gas "update_global_bounded_narrowing x" for x
  unfolding update_rule_def update_global_bounded_narrowing_def init_ug_state_with_gas_def
  apply (intro conjI allI impI)
  apply (simp add: fmlookup_default_def)
  apply (simp add: Let_def fmlookup_default_def
         split: prod.splits if_splits option.splits)
  apply (simp add: Let_def fmlookup_default_def
         split: prod.splits if_splits option.splits)
  subgoal
    by (auto intro: widen_ge2 narrow_ge
        simp add: Let_def fmlookup_default_def
        split: if_splits prod.splits option.splits)
  subgoal for _ _ orig
    by (auto intro: sup_over_origins_upper[where ?orig=orig]
        simp add: Let_def fmlookup_default_def
        split: if_splits prod.splits option.splits)
  subgoal for _ _ _ _ _ _ _ orig'
    by (auto intro: sup_over_origins_upper[where ?orig=orig']
        simp add: Let_def fmlookup_default_def
        split: if_splits prod.splits option.splits)
  done

end