Theory Globals_Rule

theory Globals_Rule
  imports TD_Solver_Bridge
begin

section ‹Which rule updates a side-effected global›

text ‹
  The vendored solver warrows every local unknown at a widening point, whichever
  instance runs. What its instances differ in is how a contribution side-effected into
  a global unknown is merged: joined into the value, joined per origin, warrowed into
  the value, warrowed per origin, or widened per origin with narrowing cut short once
  an origin has switched from widening to narrowing a given number of times. That
  merge is the one choice a caller makes, so it is a value here rather than a choice
  between five solvers: a single interpretation takes the rule as a parameter, and
  every solver fact holds for all five at once.
›

datatype globals_rule =
    Globals_Join
  | Globals_Per_Origin
  | Globals_Warrow
  | Globals_Warrow_Per_Origin
  | Globals_Bounded_Narrowing nat

subsection ‹One update state for every rule›

text ‹
  The bounded-narrowing rule keeps a counter per global and origin beside the
  recorded contributions; the other four rules keep only the contributions. So the
  single interpretation runs on the state with the counter, and each of the four
  runs on its contribution part and leaves the counter unchanged. Every
  \<^locale>‹update_rule› obligation speaks about the contributions alone, so the
  lifted rule inherits them.

  The lifted rule also reports no change when the merged value equals the old one.
  The two warrowing rules answer with a new value whenever an origin's contribution
  changes, even when the merge over all origins stays the same, and the solver
  destabilizes every reader of a global it is handed a value for. Recording the
  contribution and reporting nothing keeps those readers stable.
›

definition changed :: "'d ⇒ 'd option ⇒ 'd option" where
  "changed d res = (case res of Some d'' ⇒ if d'' = d then None else Some d'' | None ⇒ None)"

lemma changed_SomeD: "changed d res = Some d'' ⟹ res = Some d''"
  by (cases res) (auto simp: changed_def split: if_splits)

lemma changed_NoneD: "changed d res = None ⟹ res = None ∨ res = Some d"
  by (cases res) (auto simp: changed_def split: if_splits)

definition lift_basic_rule ::
    "('d ⇒ 'x ⇒ 'g ⇒ 'd ⇒ ('x, 'g, 'd) ug_state ⇒ 'd option × ('x, 'g, 'd) ug_state)
     ⇒ 'd ⇒ 'x ⇒ 'g ⇒ 'd ⇒ ('x, 'g, 'd) ug_state_with_gas
     ⇒ 'd option × ('x, 'g, 'd) ug_state_with_gas" where
  "lift_basic_rule f d orig g d' state =
     (let (res, st) = f d orig g d' (ug_state.truncate state)
      in (changed d res, ug_state.ρ_update (λ_. ug_state.ρ st) state))"

lemma lift_basic_ruleE:
  assumes "(res, state') = lift_basic_rule f d orig g d' state"
  obtains res0 st where "(res0, st) = f d orig g d' (ug_state.truncate state)"
    and "res = changed d res0" and "ug_state.ρ state' = ug_state.ρ st"
  using assms by (auto simp: lift_basic_rule_def split: prod.splits)

lemma update_rule_lift_basic_rule:
  assumes f: "update_rule init_basic_ug_state f"
  shows "update_rule init_ug_state_with_gas (lift_basic_rule f)"
proof
  show "∀g orig. rho_lookup (ug_state.ρ init_ug_state_with_gas) g orig ≤ ⊥"
    by (simp add: init_ug_state_with_gas_def fmlookup_default_def)
next
  fix res state' d orig g d' state g' orig'
  assume step: "(res, state') = lift_basic_rule f d orig g d' state" and ne: "g' ≠ g"
  from step obtain res0 st where e: "(res0, st) = f d orig g d' (ug_state.truncate state)"
    and r: "ug_state.ρ state' = ug_state.ρ st" by (rule lift_basic_ruleE)
  show "rho_lookup (ug_state.ρ state') g' orig' = rho_lookup (ug_state.ρ state) g' orig'"
    using update_rule.update_global_untouched(1)[OF f e ne] by (simp add: r)
next
  fix res state' d orig g d' state g' orig'
  assume step: "(res, state') = lift_basic_rule f d orig g d' state" and ne: "orig' ≠ orig"
  from step obtain res0 st where e: "(res0, st) = f d orig g d' (ug_state.truncate state)"
    and r: "ug_state.ρ state' = ug_state.ρ st" by (rule lift_basic_ruleE)
  show "rho_lookup (ug_state.ρ state') g' orig' = rho_lookup (ug_state.ρ state) g' orig'"
    using update_rule.update_global_untouched(2)[OF f e ne] by (simp add: r)
next
  fix res state' d orig g d' state
  assume step: "(res, state') = lift_basic_rule f d orig g d' state"
  from step obtain res0 st where e: "(res0, st) = f d orig g d' (ug_state.truncate state)"
    and r: "ug_state.ρ state' = ug_state.ρ st" by (rule lift_basic_ruleE)
  show "d' ≤ rho_lookup (ug_state.ρ state') g orig"
    using update_rule.update_global_recorded_in_rho[OF f e] by (simp add: r)
next
  fix state' d orig g d' state
  assume step: "(None, state') = lift_basic_rule f d orig g d' state"
    and inv: "∀orig. rho_lookup (ug_state.ρ state) g orig ≤ d"
  from step obtain res0 st where e: "(res0, st) = f d orig g d' (ug_state.truncate state)"
    and c: "None = changed d res0" and r: "ug_state.ρ state' = ug_state.ρ st"
    by (rule lift_basic_ruleE)
  from changed_NoneD[OF c[symmetric]] show "rho_lookup (ug_state.ρ state') g orig ≤ d"
  proof
    assume "res0 = None"
    then show ?thesis
      using update_rule.update_global_preserves_rho_invariant(1)[OF f] e inv by (simp add: r)
  next
    assume "res0 = Some d"
    then show ?thesis
      using update_rule.update_global_preserves_rho_invariant(2)[OF f] e inv by (simp add: r)
  qed
next
  fix d'' state' d orig g d' state orig'
  assume step: "(Some d'', state') = lift_basic_rule f d orig g d' state"
    and inv: "∀orig. rho_lookup (ug_state.ρ state) g orig ≤ d"
  from step obtain res0 st where e: "(res0, st) = f d orig g d' (ug_state.truncate state)"
    and c: "Some d'' = changed d res0" and r: "ug_state.ρ state' = ug_state.ρ st"
    by (rule lift_basic_ruleE)
  have "res0 = Some d''" by (rule changed_SomeD) (use c in simp)
  then show "rho_lookup (ug_state.ρ state') g orig' ≤ d''"
    using update_rule.update_global_preserves_rho_invariant(2)[OF f] e inv by (simp add: r)
qed

subsection ‹The rule as a value›

text ‹
  ‹update_global_of› maps each ‹globals_rule› to its update rule, so
  one interpretation of ‹TD_side_upd_rule› covers every rule a
  configuration can select.
›

definition update_global_of ::
    "globals_rule ⇒ '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_of r =
     (case r of
        Globals_Join ⇒ lift_basic_rule update_global_always_join
      | Globals_Per_Origin ⇒ lift_basic_rule update_global_per_origin
      | Globals_Warrow ⇒ lift_basic_rule update_global_warrowing_apinis
      | Globals_Warrow_Per_Origin ⇒ lift_basic_rule update_global_warrowing_per_origin
      | Globals_Bounded_Narrowing n ⇒ update_global_bounded_narrowing n)"

lemma update_rule_update_global_of:
  "update_rule init_ug_state_with_gas (update_global_of r)"
  by (cases r)
     (simp_all add: update_global_of_def update_rule_lift_basic_rule
        always_join.update_rule_axioms per_origin.update_rule_axioms
        warrowing_apinis.update_rule_axioms warrowing_per_origin.update_rule_axioms
        bounded_narrowing.update_rule_axioms)

global_interpretation TD_side_rule_Interp:
  TD_side_upd_rule init_ug_state_with_gas "update_global_of r" T for r T
  defines TD_side_rule_Interp_solve = TD_side_rule_Interp.solve
    and TD_side_rule_Interp_solve_c = TD_side_rule_Interp.solve_c
    and TD_side_rule_Interp_solve_rec_c = TD_side_rule_Interp.solve_rec_c
  by (simp add: TD_side_upd_rule.intro update_rule_update_global_of)

text ‹The solver contract of the pipeline, once for every rule.›

lemma td_certified_solver:
  "certified_solver (TD_side_rule_Interp_solve r)
     (TD_side_rule_Interp.solve_dom TYPE('g) TYPE('d::{bounded_semilattice_sup_bot,warrowing}) r)
     (TD_side_rule_Interp_solve_c r)"
  by unfold_locales
     (erule TD_side_rule_Interp.partial_post_solution[OF _ surjective_pairing],
      erule TD_side_rule_Interp.finite_stabl_solve,
      erule TD_side_rule_Interp.solve_dom_of_solve_c,
      simp add: TD_side_rule_Interp.solve_code_equation)

end