Theory DG_Constraint_Programs

theory DG_Constraint_Programs
  imports DG_State "Voblint_Solver.Strategy_Program_Fold"
begin

context
begin

text ‹
  This theory states its observations at the program level --- ‹traverse_program›,
  ‹sides_of_program›, ‹dep_program› --- reaching for \<^const>‹sp_compile› only
  where a statement must meet the vendored solver's own tree vocabulary,
  and does not unfold it globally: the named observation
  equations in \<^theory>‹Voblint_Solver.Strategy_Tree_Program› are stated
  against ‹sp_compile› itself, and proofs meet those rather than the
  compiler's representation.
›

section ‹What a right-hand side over the packed D/G carrier is›

text ‹
  What a generator hands the solver, and how several of those combine. An edge
  former takes its source as an address in the solver's own valuation space and
  its published slot as an explicit key, and produces a strategy program the
  solver can run: the program reads what it needs, publishes what it must, and
  answers with a \<^type>‹dg_state›. A generator with several such programs for
  one unknown --- several predecessors, several call sites --- folds them here,
  and the fold's own answer, publications and dependencies are each the join,
  respectively union, over the members.

  \<^theory>‹Voblint_Framework.DG_State› supplies the value type and its lattice.
  Nothing here inspects a domain, a variable, a global classifier, or a CFG: an
  address and a key are all a former sees, which is why the same former reads a
  contribution-only unknown and an equation-driven one.›

subsection ‹Low-level edge formers over a solution address›

text ‹
  The two formers in this subsection take a step in the direct shape
  ‹'dl ⇒ 'dg ⇒ 'dg × 'dl›, which no analysis writes: a specification
  supplies manager-native transfers, and ‹DG_Spec› compiles those. They
  survive because the keyed-solver update-rule regression
  needs a step it can vary directly, without a ‹dg_spec› in the way, and that
  regression is their only consumer. Read them as the minimal thing a
  right-hand side can be, not as the shape production equations take.

  An edge or combine former takes its source as an ∗‹address› in the solver's
  own valuation space \<^typ>‹'x + 'k› and its published slot as an explicit key,
  rather than fixing the source to a local unknown and the slot to the
  \<^typ>‹unit› key -- what lets a keyed generator target an arbitrary
  activation-indexed unknown directly, with no separate address-rewriting pass.

  A program point whose value is carried by a contribution-only unknown --
  one with no equation of its own, so that its value is exactly the join of
  what was published to it -- is then read by exactly the same former as one
  carried by an equation-driven unknown, since \<^const>‹QueryL› and
  \<^const>‹QueryG› project the same valuation.

  \<^const>‹sp_read_at› itself (\<^theory>‹Voblint_Solver.Strategy_Tree_Program›) is a
  generic solver-address dispatcher with no notion of ‹D›/‹G›; here it is
  instantiated at ‹'d = ('dl, 'dg) dg_state›, so the value it returns is
  already one of this file's packed ‹DG _ bot› / ‹DG bot _› slots, not a raw
  ‹D›. Reading through an address is therefore an operation on already-packed
  DG state, not a general "query something of unknown kind" primitive.
›

definition dg_edge_program_at ::
  "('dl::bounded_semilattice_sup_bot ⇒ 'dg::bounded_semilattice_sup_bot ⇒ 'dg × 'dl)
   ⇒ 'x + 'k ⇒ 'k
   ⇒ ('x, 'k, ('dl, 'dg) dg_state, ('dl, 'dg) dg_state) strategy_program"
where
  "dg_edge_program_at step src gk =
     (do {
       d ← sp_read_at src;
       g ← sp_read_global gk;
       _ ← sp_publish gk (DG bot (fst (step (dg_local d) (dg_global g))));
       sp_return (DG (snd (step (dg_local d) (dg_global g))) bot)
     })"

definition dg_edge_contribution_program_at ::
  "('dl::bounded_semilattice_sup_bot ⇒ 'dg::bounded_semilattice_sup_bot ⇒ 'dg × 'dl)
   ⇒ 'x + 'k ⇒ 'k
   ⇒ ('x, 'k, ('dl, 'dg) dg_state, ('dl, 'dg) dg_state) strategy_program"
where
  "dg_edge_contribution_program_at step src gk =
     (do {
       d ← sp_read_at src;
       g ← sp_read_global gk;
       sp_return (DG (snd (step (dg_local d) (dg_global g))) (fst (step (dg_local d) (dg_global g))))
     })"

lemma dep_dg_edge_program_at:
  "dep_program tau (dg_edge_program_at step src gk) = {src, Inr gk}"
  by (cases src) (simp_all add: dg_edge_program_at_def sp_compile_def)

lemma sp_wf_dg_edge_program_at [intro, simp]: "sp_wf (dg_edge_program_at step src gk)"
  unfolding dg_edge_program_at_def by (intro sp_wf_bind) simp_all

lemma sp_wf_dg_edge_contribution_program_at [intro, simp]:
  "sp_wf (dg_edge_contribution_program_at step src gk)"
  unfolding dg_edge_contribution_program_at_def by (intro sp_wf_bind) simp_all

subsection ‹The framework boundary, as theorems›

text ‹
  Two independent opaque domains. An analysis provides
  ‹step : D ⇒ G ⇒ G × D› --- transfer plus publication; the framework reads the
  source address's ‹D› and the published slot's ‹G›, and transports the step's
  ‹Side : G› and ‹Answer : D›. Slot packing (‹DG _ bot› / ‹DG bot _›) encodes the
  two-typed unknown space into the solver's single value type; the framework
  never looks inside ‹D› or ‹G›. The two theorems say so for ∗‹every› step and
  every address: an answer carries no ‹G›, a publication no ‹D›.
›

subsection ‹Why a Side-free analogue exists›

text ‹
  \<^const>‹dg_edge_program_at› publishes its ‹G› contribution as soon as it is
  evaluated (\<^const>‹Side›). When a generator folds several such programs into one
  equation's right-hand side --- several intra predecessors, or several return
  sites --- each one's ‹Side› is published at a different moment within the same
  evaluation, and the vendored solver's warrowing/APINIS update rule gates
  convergence per ∗‹origin›: repeated writes to one key from one origin can
  destabilize the equation's own dependency and never converge.

  \<^const>‹dg_edge_contribution_program_at› is the Side-free analogue. It answers the
  ∗‹unsplit› ‹(G, D)› result as one \<^type>‹dg_state› and publishes nothing, so a
  caller folds several of them with \<^const>‹fold_rhs_program› --- whose own
  \<^const>‹Side› is empty --- and splits the aggregate once, after every
  contribution has been read. The two lemmas below are what makes that
  substitution legitimate: each half of the contribution answer is exactly the
  observation the Side form makes.
›

subsection ‹Folding a list of programs into one D/G value›

text ‹
  One unknown can have several right-hand sides --- one per intra predecessor,
  one per call site --- and the solver takes one tree per equation.
  ‹side_rhs_fold_dg› is that reduction: it runs the programs in order, joins their
  answers into a running local accumulator, and answers ‹DG acc bot›, letting
  each program's own publications pass through untouched. ‹side_acc_dg› is the
  same accumulator read declaratively off a valuation, and it is what the
  characterization lemmas below state the fold's three observations --- answer,
  publications, dependencies --- in terms of.

  Both this and \<^const>‹fold_rhs_program› are specializations of one
  fold, \<^const>‹fold_rhs_program_projected›, and the choice of specialization is the
  whole direct/buffered split. The identity specialization accumulates
  complete answers, so a contribution's global half joins into the node's
  answer; this one accumulates only \<^const>‹dg_local› and embeds the result as
  ‹DG d bot›, so a global half never reaches the answer and each program
  publishes its own \<^const>‹Side› as it runs. The buffered generator wants the
  first --- it gathers every global contribution into the answer precisely so
  it can publish once per node --- and the direct generator wants the second.
  Replacing either fold by the other would exchange the two generators, not
  simplify them.

  The narrow definitions here exist to keep the D/G vocabulary the generators
  and the routed soundness development actually reason in, rather than
  spelling out ‹fold_rhs_program_projected dg_local (λd. DG d bot)› in every statement.
  Their algebra is inherited: each observation and monotonicity fact below is
  a specialization of the generic one.
›

definition side_rhs_fold_dg ::
  "'d::bounded_semilattice_sup_bot
   ⇒ ('x, 'g, ('d, 'h::bounded_semilattice_sup_bot) dg_state,
        ('d, 'h) dg_state) strategy_program list
   ⇒ ('x, 'g, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program"
where
  "side_rhs_fold_dg acc ps = fold_rhs_program_projected dg_local (λd. DG d bot) acc ps"

lemma side_rhs_fold_dg_simps [simp, code]:
  "side_rhs_fold_dg acc [] = sp_return (DG acc bot)"
  "side_rhs_fold_dg acc (p # ps) =
     do {
       res ← p;
       side_rhs_fold_dg (acc ⊔ dg_local res) ps
     }"
  by (simp_all add: side_rhs_fold_dg_def)

lemma sp_wf_side_rhs_fold_dg [intro]:
  "∀p ∈ set ps. sp_wf p ⟹ sp_wf (side_rhs_fold_dg acc ps)"
  unfolding side_rhs_fold_dg_def by (rule sp_wf_fold_rhs_program_projected)

definition side_acc_dg ::
  "'d::bounded_semilattice_sup_bot
   ⇒ ('x + 'g ⇒ ('d, 'h::bounded_semilattice_sup_bot) dg_state)
   ⇒ ('x, 'g, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program list ⇒ 'd"
where
  "side_acc_dg acc τ ps = fold_acc_projected dg_local acc τ ps"

lemma side_acc_dg_simps [simp, code]:
  "side_acc_dg acc τ [] = acc"
  "side_acc_dg acc τ (p # ps) =
     side_acc_dg (acc ⊔ dg_local (traverse_program p τ)) τ ps"
  by (simp_all add: side_acc_dg_def)

lemma traverse_side_rhs_fold_dg:
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "traverse_program (side_rhs_fold_dg acc ps) τ = DG (side_acc_dg acc τ ps) bot"
  unfolding side_rhs_fold_dg_def side_acc_dg_def
  by (rule traverse_fold_rhs_program_projected_char[OF wf])

text ‹
  ‹side_rhs_fold_dg›'s accumulator only ever reaches the terminal ‹Answer›,
  so its dependency set is independent of the accumulator: the recursion
  skeleton over ‹ps› never branches on ‹acc›.
›

lemma dep_program_side_rhs_fold_dg_char:
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "dep_program sigma (side_rhs_fold_dg acc ps) = (⋃p∈set ps. dep_program sigma p)"
  unfolding side_rhs_fold_dg_def
  by (rule dep_program_fold_rhs_program_projected_char[OF wf])

lemma dep_program_side_rhs_fold_dg_acc_indep:
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "dep_program sigma (side_rhs_fold_dg acc1 ps)
     = dep_program sigma (side_rhs_fold_dg acc2 ps)"
  by (simp add: dep_program_side_rhs_fold_dg_char[OF wf])

text ‹
  The two order-preservation facts the generic fold asks for before it will
  carry its contributions' environment-monotonicity: the D/G instance's
  projection and its embedding.
›

lemma mono_dg_local: "mono (dg_local :: ('d::order, 'h::order) dg_state ⇒ 'd)"
  by (rule monoI) (simp add: less_eq_dg_state_def)

lemma mono_DG_bot:
  "mono (λd. DG d bot :: ('d::order, 'h::order_bot) dg_state)"
  by (rule monoI) simp

text ‹
  Environment-monotonicity of the fold, given every folded program is itself
  environment-monotone. The content is
  ‹traverse_fold_rhs_program_projected_mono›'s; this instance only supplies the two
  monotonicity facts above.
›

lemma side_rhs_fold_dg_mono:
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and prog_mono: "∀p ∈ set ps. ∀s1 s2. s1 ≤ s2 ⟶ traverse_program p s1 ≤ traverse_program p s2"
  shows "⋀acc s1 s2. s1 ≤ s2 ⟹
           traverse_program (side_rhs_fold_dg acc ps) s1
             ≤ traverse_program (side_rhs_fold_dg acc ps) s2"
  using prog_mono
  unfolding side_rhs_fold_dg_def
  by (auto intro!: traverse_fold_rhs_program_projected_mono[OF wf mono_dg_local mono_DG_bot])

text ‹
  The vendored solver's own @{const mono_deps} precondition only needs the
  weaker, order-conditional guarantee @{const mono_tree_deps}, not the full
  equality @{const env_indep_deps}; the generic fold already carries it, so
  this instance is one line.
›

lemma side_rhs_fold_dg_mono_tree_deps:
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and prog_mono: "⋀p. p ∈ set ps ⟹ mono_tree_deps (sp_compile p)"
  shows "mono_tree_deps (sp_compile (side_rhs_fold_dg acc ps))"
  unfolding side_rhs_fold_dg_def
  by (rule mono_tree_deps_fold_rhs_program_projected[OF wf prog_mono])

text ‹
  The fold's contributions are carried only by the per-contribution Side
  nodes; the accumulator flows into the final ‹Answer› (whose own sides are
  ‹bot›), so the side map is acc-independent --- the same fact
  @{thm dep_program_side_rhs_fold_dg_acc_indep} established for dependencies,
  mirrored here for sides. This is what lets @{thm side_rhs_fold_dg_mono}'s
  proof strategy repeat for @{const sides_of_rhs} without also needing
  @{const traverse_rhs}-monotonicity as a hypothesis.
›

lemma sides_of_program_side_rhs_fold_dg_acc_indep:
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "sides_of_program (side_rhs_fold_dg acc1 ps) sigma
     = sides_of_program (side_rhs_fold_dg acc2 ps) sigma"
  unfolding side_rhs_fold_dg_def
  by (rule sides_of_program_fold_rhs_program_projected_acc_indep[OF wf])

text ‹
  The declarative twin of \<^const>‹side_acc_dg›: ‹side_rhs_fold_dg›'s contribution
  at any one key is a plain fold over each element's own \<^const>‹sides_of_rhs›, seeded at
  ‹bot› rather than the running local accumulator -- @{thm
  sides_of_program_side_rhs_fold_dg_acc_indep} already shows the accumulator never affects a
  side read, so unfolding \<^const>‹sp_lift_tree›'s side equation and re-seeding at ‹bot›
  after each step is exact, not merely a bound.
›

lemma sides_of_program_side_rhs_fold_dg_char:
  fixes ps :: "('x, 'k, ('d::bounded_semilattice_sup_bot, 'h::bounded_semilattice_sup_bot) dg_state,
                 ('d, 'h) dg_state) strategy_program list"
  assumes wf: "∀p ∈ set ps. sp_wf p"
  shows "sides_of_program (side_rhs_fold_dg acc ps) τ z
           = (⨆p←ps. sides_of_program p τ z)"
  unfolding side_rhs_fold_dg_def
  by (rule sides_of_program_fold_rhs_program_projected_char[OF wf])

lemma side_acc_dg_as_foldr:
  "side_acc_dg acc τ ps = acc ⊔ (⨆p←ps. dg_local (traverse_program p τ))"
  by (simp add: side_acc_dg_def fold_acc_projected_as_foldr)

text ‹The same equation with the accumulator left as the fold's seed, which is
  how a proof that already has a right fold in hand meets it.›

lemma side_acc_dg_as_foldr_seeded:
  "side_acc_dg acc τ ps = foldr (λp a. dg_local (traverse_program p τ) ⊔ a) ps acc"
  by (simp only: side_acc_dg_as_foldr foldr_join_seed_out)

lemma side_rhs_fold_dg_sides_mono:
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and prog_sides_mono:
      "∀p ∈ set ps. ∀s1 s2. s1 ≤ s2 ⟶ sides_of_program p s1 ≤ sides_of_program p s2"
  shows "⋀acc s1 s2. s1 ≤ s2 ⟹
           sides_of_program (side_rhs_fold_dg acc ps) s1
             ≤ sides_of_program (side_rhs_fold_dg acc ps) s2"
  using prog_sides_mono
  unfolding side_rhs_fold_dg_def
  by (auto intro!: sides_of_program_fold_rhs_program_projected_mono[OF wf])

subsection ‹Pushing a projection through a join-fold›

text ‹
  A \<^type>‹dg_state› join is componentwise, so either projection commutes with
  a join-fold. These are what let a proof that has folded whole states read
  off one component afterwards, rather than carrying two folds along.
›

lemma dg_local_foldr_generic:
  "dg_local (foldr (λt acc'. h t ⊔ acc') L
      (acc::('d::bounded_semilattice_sup_bot, 'h::bounded_semilattice_sup_bot) dg_state))
     = foldr (λt acc'. dg_local (h t) ⊔ acc') L (dg_local acc)"
  by (induction L) simp_all

lemma dg_global_foldr_generic:
  "dg_global (foldr (λt acc'. h t ⊔ acc') L
      (acc::('d::bounded_semilattice_sup_bot, 'h::bounded_semilattice_sup_bot) dg_state))
     = foldr (λt acc'. dg_global (h t) ⊔ acc') L (dg_global acc)"
  by (induction L) simp_all

lemma dg_local_join_list:
  "dg_local (⨆t←L. h t :: ('d::bounded_semilattice_sup_bot, 'h::bounded_semilattice_sup_bot) dg_state)
     = (⨆t←L. dg_local (h t))"
  by (induction L) simp_all

lemma dg_global_join_list:
  "dg_global (⨆t←L. h t :: ('d::bounded_semilattice_sup_bot, 'h::bounded_semilattice_sup_bot) dg_state)
     = (⨆t←L. dg_global (h t))"
  by (induction L) simp_all

lemma foldr_dg_global_sides_char:
  fixes L :: "('x, 'k, ('d::bounded_semilattice_sup_bot, 'h::bounded_semilattice_sup_bot) dg_state,
                ('d, 'h) dg_state) strategy_program list"
  shows "(⨆t←L. dg_global (sides_of_program t τ z))
       = dg_global (⨆t←L. sides_of_program t τ z)"
  by (simp add: dg_global_foldr_generic foldr_join_list[symmetric])

lemma foldr_sides_dg_local_bot:
  fixes L :: "('x, 'k, ('d::bounded_semilattice_sup_bot, 'h::bounded_semilattice_sup_bot) dg_state,
                ('d, 'h) dg_state) strategy_program list"
  assumes "⋀t. t ∈ set L ⟹ dg_local (sides_of_program t τ z) = bot"
  shows "dg_local (⨆t←L. sides_of_program t τ z) = bot"
  using assms
  by (induction L) simp_all

lemma DG_sup_bot_left:
  "DG (bot::'d::bounded_semilattice_sup_bot) a ⊔ DG bot b = DG bot (a ⊔ b)"
  by (simp add: sup_dg_state_def bot_dg_state_def)

subsection ‹What one folded program contributes›

text ‹
  Lower bounds, the counterpart of the upper bounds above: every folded program's
  answer and contribution is below the fold's, and the accumulator only
  grows. A soundness proof reaches one selected contribution through these,
  having reached the fold itself through the generator.

  All three are the same fact about a join-fold --- ‹foldr_sup_member_le›,
  proved once with the rest of that algebra where the fold itself is defined
  --- read off the two characterizations above.
›

lemma side_acc_dg_ge_acc:
  "acc ≤ side_acc_dg acc σ ts"
  by (simp add: side_acc_dg_as_foldr)

lemma dg_local_traverse_le_side_acc_dg:
  assumes "p ∈ set ps"
  shows "dg_local (traverse_program p σ) ≤ side_acc_dg acc σ ps"
  unfolding side_acc_dg_as_foldr
  using foldr_sup_member_le[where h = "λp. dg_local (traverse_program p σ)", OF assms]
  by (rule le_supI2)

lemma sides_le_side_rhs_fold_dg:
  assumes wf: "∀p ∈ set ps. sp_wf p"
    and mem: "p ∈ set ps"
  shows "sides_of_program p σ k ≤ sides_of_program (side_rhs_fold_dg acc ps) σ k"
  unfolding sides_of_program_side_rhs_fold_dg_char[OF wf]
  by (rule foldr_sup_member_le[OF mem])

end

end