Theory Example_Keyed_Solver_Update_Rule_Regression

theory Example_Keyed_Solver_Update_Rule_Regression
  imports
    "Voblint_Analysis_Interval.Interval_Exec"
begin

section ‹Minimal keyed update-rule regression: multiple Side writes per RHS evaluation (keyed)›

text ‹
  Isolates the keyed-generator instance of multiple Side writes per RHS evaluation at
  \<^const>‹routed_node_rhs›'s own interface, independent of a real
  \<^typ>‹cfg›, procedure calls, or Interval program construction: a dummy
  \<^typ>‹cfg› with no edges of its own (‹intra = {}›, ‹calls = {}›) paired with a
  hand-supplied ‹pred_sel› that reports two intra predecessors for one node --
  exactly the shape a real merge node with two incoming intra edges produces
  (\<^theory>‹Voblint_Framework.DG_Constraint_Programs›'s own ‹intra› fold), collapsed to its
  essential two-write pattern.

  The two predecessor edges carry different ‹edge_action›s (‹EA_Nop› vs.
  ‹EA_Assign›) against ‹keyed_step› below, so their \<^const>‹dg_edge_program_at›
  contributions publish genuinely different global values -- reproducing the
  same per-origin-gate destabilization \<^const>‹update_global_warrowing_apinis›
  exhibits, from two ‹intra› list entries of the same equation.
›

text ‹An edge step in the framework's own ‹'dl ⇒ 'dg ⇒ 'dg × 'dl› shape rather
  than a \<^type>‹dg_spec›: what is under test is the generator's ‹Side› discipline, so
  the step is supplied directly to \<^const>‹dg_edge_program_at› and its Side-free
  analogue. Only ‹EA_Assign› raises the published global, so the two predecessor
  edges below publish different values.›
definition keyed_step :: "edge_action ⇒ ivl ⇒ ivl ⇒ ivl × ivl" where
  "keyed_step a d g =
     (case a of EA_Assign _ _ ⇒ (g ⊔ Ivl (Fin 1) (Fin 1), d) | _ ⇒ (g, d))"

definition keyed_dummy_cfg :: cfg where
  "keyed_dummy_cfg = ⦇ intra = {}, calls = {}, cfg_entry = Statement 0 ⦈"

text ‹Two predecessors of ‹Statement 1›, both from ‹Statement 0›, with different
  ‹edge_action›s so their \<^const>‹dg_edge_program_at› contributions differ.›
definition keyed_pred_sel ::
  "cfg ⇒ pp ⇒ unit ⇒ ((pp × unit + unit) × edge_action) list" where
  "keyed_pred_sel g v ctx =
     (if v = Statement 1 then
        [(Inl (Statement 0, ctx), EA_Nop),
         (Inl (Statement 0, ctx), EA_Assign (STR ''x'') (exp.N 0))]
      else [])"

text ‹‹cmb›/‹extra› are never invoked: ‹calls = {}› makes
  ‹return_call_action_list›/‹entry_call_list› empty for every node.›
definition keyed_cmb :: "(pp ⇒ unit ⇒ ivl ⇒ call_action ⇒ unit) ⇒ unit ⇒ call_action ⇒ pp ⇒ pp
    ⇒ (pp × unit, unit, (ivl, ivl) dg_state, (ivl, ivl) dg_state) strategy_program" where
  "keyed_cmb route ctx ca cc ex = sp_return (DG bot bot)"

definition keyed_cmb_c :: "(pp ⇒ unit ⇒ ivl ⇒ call_action ⇒ unit) ⇒ unit ⇒ call_action ⇒ pp ⇒ pp
    ⇒ (pp × unit, unit, (ivl, ivl) dg_state, (ivl, ivl) dg_state) strategy_program" where
  "keyed_cmb_c route ctx ca cc ex = sp_return (DG bot bot)"

definition keyed_extra :: "(pp ⇒ unit ⇒ ivl ⇒ call_action ⇒ unit) ⇒ unit ⇒ pp
    ⇒ (pp × unit, unit, (ivl, ivl) dg_state, (ivl, ivl) dg_state) strategy_program list" where
  "keyed_extra route ctx v = []"

text ‹The unbuffered generator: ‹Statement 1›'s equation issues two ‹Side ()›
  writes -- ‹EA_Nop›'s and ‹EA_Assign›'s -- in one RHS evaluation. This
  equation is not evaluated because its non-termination would hang the session.›

definition keyed_multiwrite_eqs :: "(pp × unit, unit, (ivl, ivl) dg_state) eqsT" where
  "keyed_multiwrite_eqs =
     routed_node_rhs keyed_pred_sel call_site_list (λ_. ()) (λ_ _ _ _. ())
       (λctx' src a. dg_edge_program_at (keyed_step a) src ())
       keyed_cmb keyed_extra keyed_dummy_cfg bot bot bot"

text ‹The buffered generator: the same two predecessor contributions, folded
  Side-free via \<^const>‹dg_edge_contribution_program_at› and \<^const>‹fold_rhs_program›,
  published exactly once. Terminates under the completely unmodified vendored
  \<^const>‹TD_side_warrowing_apinis_Interp_solve_c›.›
definition keyed_multiwrite_buffered_eqs :: "(pp × unit, unit, (ivl, ivl) dg_state) eqsT" where
  "keyed_multiwrite_buffered_eqs =
     routed_node_rhs_buffered keyed_pred_sel call_site_list (λ_. ()) (λ_ _ _ _. ())
       (λctx' src a. dg_edge_contribution_program_at (keyed_step a) src ())
       keyed_cmb_c keyed_extra keyed_dummy_cfg bot bot bot"

lemma keyed_multiwrite_buffered_terminates:
  "TD_side_warrowing_apinis_Interp_solve_c keyed_multiwrite_buffered_eqs (Statement 1, ()) ≠ None"
  by eval

section ‹Merge-node regression: a real two-predecessor CFG node›

text ‹
  Unlike ‹keyed_multiwrite_buffered_eqs› above, this uses a genuine \<^typ>‹cfg›
  with two real ‹intra› edges into one merge node and the PRODUCTION
  \<^const>‹intra_predecessor_list› selector (no hand-rolled ‹pred_sel›) --
  exactly the shape ‹FunctionResult factorial› has in the real factorial
  regression (two incoming intra edges, one per branch). ‹merge_step›
  answers fixed constants at ‹EA_Nop›/‹EA_Assign› regardless of the incoming
  local/global state, so the solved global value at ‹buffer_key_at ()› is exactly
  the join of the two edges' own contributions, not a self-referential
  fixpoint -- letting the check below assert that join directly.
›

definition merge_step :: "edge_action ⇒ ivl ⇒ ivl ⇒ ivl × ivl" where
  "merge_step a d g =
     (case a of EA_Nop ⇒ (Ivl (Fin 0) (Fin 0), d)
              | EA_Assign _ _ ⇒ (Ivl (Fin 1) (Fin 1), d)
              | _ ⇒ (g, d))"

text ‹Two real predecessors of ‹Statement 2›: ‹Statement 0› via ‹EA_Nop›,
  ‹Statement 1› via ‹EA_Assign›. ‹calls = {}› keeps ‹cmb›/‹extra› unused, as
  in ‹keyed_dummy_cfg›.›
definition merge_cfg :: cfg where
  "merge_cfg = ⦇
     intra = {(Statement 0, EA_Nop, Statement 2),
              (Statement 1, EA_Assign (STR ''x'') (exp.N 0), Statement 2)},
     calls = {}, cfg_entry = Statement 0 ⦈"

definition merge_eqs :: "(pp × unit, unit, (ivl, ivl) dg_state) eqsT" where
  "merge_eqs =
     routed_node_rhs_buffered intra_predecessor_addr_list call_site_list (λ_. ()) (λ_ _ _ _. ())
       (λctx' src a. dg_edge_contribution_program_at (merge_step a) src ())
       keyed_cmb_c keyed_extra merge_cfg bot bot bot"

lemma merge_terminates:
  "TD_side_warrowing_apinis_Interp_solve_c merge_eqs (Statement 2, ()) ≠ None"
  by eval

lemma merge_global_value:
  "map_option (λsol. dg_global (snd sol (Inr ()))) (TD_side_warrowing_apinis_Interp_solve_c merge_eqs (Statement 2, ()))
     = Some (Ivl (Fin 0) (Fin 0) ⊔ Ivl (Fin 1) (Fin 1))"
  by eval

section ‹Routed enter regression: one entered frame, keyed and published together›

text ‹
  \<^const>‹routed_call_program› selects the callee's context and publishes the callee's
  entry state. Both must read the ∗‹same› entered frame: the frame entered
  from the caller's local state ❙‹and› the solver's global unknown. A route
  reading anything else -- the caller's own local state, or a frame entered
  against a bottom global -- keys the seed under a context the published value
  does not belong to.

  ‹w0_spec› makes that observable: its \<^const>‹dgs_enter› answers the incoming
  global as the entered local, so the entered frame and the caller's local
  state are different values by construction. ‹w0_route› is the identity on
  the state it is handed, so the seed key ∗‹is› whichever frame the
  generator routes on.
›

datatype w0_gk = W0Global | W0Seed pp ivl

text ‹Every field but ‹dgs_enter› is the local-only default. ‹dgs_enter› is the
  one effectful field: it reads the solver's global unknown and answers it as the
  entered local, publishing nothing, so the entered frame differs from the caller's
  own local state by construction.›
definition w0_spec :: "(pp × ivl, w0_gk, unit, ivl, ivl) dg_spec" where
  "w0_spec = local_dg_spec_template⦇
     dgs_enter := (λci m K. man_global m () (λg. K [(man_local m, g)])),
     dgs_combine_env := (λci. local_combine_transfer (λdc de. dc ⊔ de)) ⦈"

definition w0_route :: "pp ⇒ ivl ⇒ ivl ⇒ call_action ⇒ ivl" where
  "w0_route u ctx d ca = d"

text ‹The caller's local state is ‹[1,1]› and the solver's global is ‹[7,7]›, so
  the entered frame is ‹[7,7]› -- a value the caller's own local state never
  takes.›
definition w0_sigma :: "pp × ivl + w0_gk ⇒ (ivl, ivl) dg_state" where
  "w0_sigma z =
     (case z of Inl _ ⇒ DG (Ivl (Fin 1) (Fin 1)) bot
              | Inr W0Global ⇒ DG bot (Ivl (Fin 7) (Fin 7))
              | Inr (W0Seed _ _) ⇒ bot)"

text ‹The call site resolves to the single callee ‹f›. Stated directly rather than
  through \<^const>‹static_resolve›, because this witness builds one call tree by hand
  instead of compiling a program.›

definition w0_resolve :: "pp ⇒ pp ⇒ call_action ⇒ ivl ⇒ pname list" where
  "w0_resolve v cc ca d = [STR ''f'']"

definition w0_program ::
  "(pp × ivl, w0_gk, (ivl, ivl) dg_state, (ivl, ivl) dg_state) strategy_program" where
  "w0_program =
     routed_call_program w0_spec (λ_. W0Global) W0Seed w0_resolve (λd. d = bot) w0_route bot
       (CallEdge None [STR ''p''] []) (Statement 0) (FunctionResult (STR ''f''))"

text ‹The seed lands at the entered frame's own key, carrying that same frame.›
lemma w0_seed_at_entered_frame:
  "sides_of_program w0_program w0_sigma
     (Inr (W0Seed (FunctionEntry (STR ''f'')) (Ivl (Fin 7) (Fin 7))))
   = DG (Ivl (Fin 7) (Fin 7)) bot"
  unfolding w0_program_def w0_sigma_def w0_spec_def w0_route_def by eval

text ‹Nothing is published at the key a caller-state route would have chosen.›
lemma w0_no_seed_at_caller_frame:
  "sides_of_program w0_program w0_sigma
     (Inr (W0Seed (FunctionEntry (STR ''f'')) (Ivl (Fin 1) (Fin 1)))) = bot"
  unfolding w0_program_def w0_sigma_def w0_spec_def w0_route_def by eval

text ‹The callee-exit unknown the combine reads back is the same entered
  context, so the return leg and the seed agree on which activation they
  are talking about.›
lemma w0_dep_at_entered_frame:
  "dep_program w0_sigma w0_program
   = {Inl (Statement 0, bot), Inr W0Global,
      Inl (FunctionResult (STR ''f''), Ivl (Fin 7) (Fin 7))}"
  unfolding w0_program_def w0_sigma_def w0_spec_def w0_route_def
  by (simp add: routed_call_program_def routed_callee_call_program_def
        routed_call_alternative_program_def w0_resolve_def
        dg_spec_combine_transfer_def mk_dg_man_def
        dg_read_global_def local_transfer_def local_combine_transfer_def
        Let_def insert_commute sp_compile_def sp_compile_with_bind sp_read_global_def
        sp_publish_def sp_read_local_def sp_bind_def sp_return_def comp_def bot_ivl_def)

end