Theory Example_Per_Origin_Widening_Precision

theory Example_Per_Origin_Widening_Precision
  imports
    "Voblint_Analysis_Interval.Interval_Exec"
begin

section ‹Per-origin widening keeps a precision the joined-then-widened slot loses›

text ‹
  Two producers write a different constant to the same global unknown, and nothing else
  happens: each producer issues one \<^const>‹Side› contribution and stabilises.  The
  concrete slot value is therefore exactly ‹[1, 2]›, and any update rule reporting more
  than that is losing precision to its own combination discipline rather than to the
  program.

  This separates the two widening rules, which agree everywhere a global has a single
  producer:

  ▪ \<^const>‹update_global_warrowing_apinis› widens the slot value ∗‹after› the join.  The
    left producer's write leaves the slot at ‹[1, 1]›.  The right producer's write then
    recomputes \<^const>‹sup_over_origins› as ‹[1, 2]› and widens ‹[1, 1] ∇ [1, 2]›; the upper
    bound grew, so it goes to \<^const>‹PlusInf›.  The growth is an artifact of two producers
    sharing one slot -- neither producer's own contribution ever moved.
  ▪ \<^const>‹update_global_warrowing_per_origin› widens each contribution against that
    origin's previous contribution and joins afterwards.  Both writes are first writes for
    their origin, so the ‹bot ∇ x = x› law (\<^theory>‹Voblint_Analysis_Interval.Interval_Warrowing›)
    keeps each exact, and the read joins them to ‹[1, 2]›.

  The narrowing half of warrowing cannot repair the joined rule here: once both producers
  are stable neither re-issues its contribution, so there is no later recomputation for
  \<^const>‹narrow› to descend from and ‹[1, +inf]› is a genuine fixpoint.
›

datatype two_writer_unknown = TW_Main | TW_Left | TW_Right
datatype two_writer_global = TW_Slot

text ‹‹TW_Main› forces both producers before reading the slot; the producers carry no local
  value of their own, so the slot is the only thing the run computes.›
fun two_writer_eqs :: "(two_writer_unknown, two_writer_global, ivl) eqsT" where
  "two_writer_eqs TW_Main =
     QueryL TW_Left (λ_. QueryL TW_Right (λ_. QueryG TW_Slot Answer))"
| "two_writer_eqs TW_Left = Side TW_Slot (Ivl (Fin 1) (Fin 1)) (Answer bot)"
| "two_writer_eqs TW_Right = Side TW_Slot (Ivl (Fin 2) (Fin 2)) (Answer bot)"

subsection ‹The slot under every update rule›

text ‹‹join› and ‹per_origin› agree at the exact ‹[1, 2]›: neither widens, and storing a
  contribution per origin then taking \<^const>‹sup_over_origins› reconstructs the value
  accumulating them into one slot produces.  They are the precision ceiling on this
  system, and \<^const>‹update_global_warrowing_per_origin› meets it while keeping the
  termination guarantee that ‹join› and ‹per_origin› do not carry. Pinned as one fact
  per update rule, so a change to
  any single rule fails on the claim it breaks rather than on a list mismatch.›

lemma two_writer_slot_join:
  "snd (TD_side_always_join_Interp_solve two_writer_eqs TW_Main) (Inr TW_Slot)
     = Ivl (Fin 1) (Fin 2)"
  by eval

lemma two_writer_slot_per_origin:
  "snd (TD_side_per_origin_Interp_solve two_writer_eqs TW_Main) (Inr TW_Slot)
     = Ivl (Fin 1) (Fin 2)"
  by eval

lemma two_writer_slot_warrow_loses_upper_bound:
  "snd (TD_side_warrowing_apinis_Interp_solve two_writer_eqs TW_Main) (Inr TW_Slot)
     = Ivl (Fin 1) PlusInf"
  by eval

lemma two_writer_slot_warrow_per_origin_exact:
  "snd (TD_side_warrowing_per_origin_Interp_solve two_writer_eqs TW_Main) (Inr TW_Slot)
     = Ivl (Fin 1) (Fin 2)"
  by eval

end