Theory DG_Indexed_Generator
theory DG_Indexed_Generator
imports DG_Constraint_Programs CFG_Enumeration "TD.TD_side_Interface"
"Voblint_Solver.Strategy_Tree_Side_Buffering"
begin
context
begin
text ‹
\<^const>‹sp_compile› stays folded here. Every fact this theory needs about a
compiled program --- what it answers, publishes and reads --- is available
as a named observation equation stated against \<^const>‹sp_compile› itself,
so a proof meets those rather than the compiler's representation.
›
section ‹Keyed equation generators›
text ‹
Builds a strategy-tree equation system over a CFG from supplied
edge/combine/extra program hooks, where every unknown carries an extra ‹'k›
key alongside its node -- context, activation, or any other routing tag a
caller wants the generator to thread through. Specifications, routing
conventions, and analysis-specific representations are instantiated above
this layer; the generator itself never sees one.
The ten parameters, once:
▪ ‹pred_sel› --- which intra predecessors a node folds, each at its address.
▪ ‹site_sel› --- which call sites return at a node.
▪ ‹route› --- the callee context a call site selects, threaded to ‹cmb› and
‹extra› and never inspected here.
▪ ‹it› --- the program for one intra edge.
▪ ‹cmb› --- the program for one call returning at this node.
▪ ‹extra› --- the routing protocol's own per-node programs, such as an
activation-seed read.
▪ ‹buffer_key_at› --- the node-owned global buffer address for a context.
▪ ‹bot0› --- the local value a node starts its fold from.
▪ ‹d⇩0› --- the local value injected at the CFG entry.
▪ ‹g⇩0› --- the global value published at the CFG entry.
Two encodings, and they are not peers. ‹routed_node_rhs› is the direct,
reference one: each publishing hook emits its own \<^const>‹Side›, keyed
and folded independently. ‹routed_node_rhs_buffered› is what production
runs --- every executable analysis in this development reaches the solver
through it. It differs deliberately: contributions return their global part
in the answer, so the node's own ‹buffer_key_at c› is published once, after the whole
fold has been evaluated, and the enclosing \<^const>‹buffer_sides› then
consolidates ∗‹every› key it names --- activation seeds included --- into
one flush apiece. The flush comes before the next local read at a node where
at most one call returns, and at the answer elsewhere.
‹routed_node_rhs_buffered_correspondence› relates the two declaratively:
equal answer, publications and dependencies at a fixed valuation, under
explicit per-hook hypotheses. That is all it says. Nothing here claims the
two run the same: equal observations at each valuation leave the iteration
order free, and where the first occurrence of a key falls decides which
update the solver widens against. Deferring the node-global publication past
the contributions is therefore a scheduling decision, not an encoding
detail, and swapping the encodings is a question for the executable
regression corpus rather than for these theorems.
‹routed_node_rhs_mono_eq›,
‹routed_node_rhs_mono_sides› and
‹routed_node_rhs_mono_deps› close the file by
discharging the vendored solver's own @{const TD_side_mono} preconditions
from per-hook properties --- well-formedness, traverse/sides monotonicity
and dependency monotonicity --- for an arbitrary generator instance. They are
the hypotheses of the vendored least-solution theorem for the solver without
widening and narrowing, not a property of the result. The warrowing solver
‹TD_side_upd_rule› that the shipped analyses run needs none of them, and no
shipped analysis discharges the per-hook properties.
›
subsection ‹The heterogeneous seeded keyed generator›
text ‹
The one context-generic generator. Every program it folds comes from a hook, so
a monovariant and a context-sensitive analysis are both instances, and the
generator itself never sees a specification:
▪ ‹pred_sel g v ctx› selects the intra predecessors folded as Answers into a node,
each paired with the ∗‹address› in the solver's valuation space that carries its
value. ‹intra_predecessor_addr_list› over \<^const>‹intra› addresses every
predecessor at its own ‹(pp, 'c)› local unknown. Callee entries are not
predecessors: every routed instance reaches them through published seeds.
▪ ‹site_sel g v› selects the call sites whose calls return at a node.
\<^const>‹call_site_list› reads them off \<^const>‹calls›; an executable
instance may answer from an index built once per graph, since the generator
only folds the list.
▪ ‹it c src a› is the intra edge program itself -- an instantiator supplies the
compiled right-hand side for one edge action at one source address, e.g.
a spec's compiled ‹dg_spec_edge_program› at the routed key. Which unknowns it
reads and which keys it publishes are its own business; the generator makes
no assumption about either.
▪ ‹cmb› is the procedure-return combine program (already fully abstract: the
context-sensitive instance reads the callee exit under the routed context).
▪ ‹extra c v› supplies additional per-node programs folded after the intra and
combine programs. Their Answers add to the node's local accumulator and their
\<^const>‹Side› effects are collected --- this is where a frame-entry seed
∗‹read› (a \<^const>‹QueryG› of the incoming seed slot) and the caller-side
call-entry ∗‹publication› (a routed \<^const>‹Side› to the callee seed
slot) live. Every routed instance supplies one, the context-insensitive
one included: seeding is what activates a callee at all, so no analysis
reaching a call leaves this hook empty.
›
text ‹The standard predecessor selection: every intra predecessor is carried by its
own ‹(pp, 'c)› local unknown, so its address is \<^const>‹Inl› of that pair.›
definition intra_predecessor_addr_list ::
"cfg ⇒ pp ⇒ 'c ⇒ ((pp × 'c + 'k) × edge_action) list"
where
"intra_predecessor_addr_list g v ctx =
map (λ(u, a). (Inl (u, ctx), a)) (intra_predecessor_list g v)"
text ‹
Everything that flows into one unknown, in one list: the intra edges
entering ‹v›, the calls returning at it, and whatever the routing protocol
adds there. Both generators fold exactly this list --- the buffered one at
its own hooks --- and every bound, correspondence and monotonicity statement
below is about it, so it is named once rather than spelled out at each.
The three membership rules are how a per-hook hypothesis reaches a selected
contribution. They stay untagged: the list is a concatenation of two maps
and a hook's own list, so a membership goal is decided by ‹auto› from the
definition, and tagging them would put three rules in front of every
\<^const>‹set› membership goal in scope.
›
definition routed_contribution_programs ::
"(cfg ⇒ pp ⇒ 'c ⇒ ((pp × 'c + 'k) × edge_action) list)
⇒ (cfg ⇒ pp ⇒ (pp × call_action) list)
⇒ (pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c)
⇒ ('c ⇒ pp × 'c + 'k ⇒ edge_action
⇒ (pp × 'c, 'k, ('d::bounded_semilattice_sup_bot,
'h::bounded_semilattice_sup_bot) dg_state,
('d, 'h) dg_state) strategy_program)
⇒ ((pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program)
⇒ ((pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ pp
⇒ (pp × 'c, 'k, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program list)
⇒ cfg ⇒ 'c ⇒ pp
⇒ (pp × 'c, 'k, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program list"
where
"routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v =
map (λ(src, a). it ctx src a) (pred_sel g v ctx)
@ map (λ(cc, ca). cmb route ctx ca cc v) (site_sel g v)
@ extra route ctx v"
text ‹
Every contribution runs its continuation once, given that each hook does.
The fold's observation lemmas all carry that side condition, and this is
where a generator instance discharges it: the hooks a context policy
supplies are built from \<^const>‹sp_return›, the reads and \<^const>‹sp_publish›,
whose closure lemmas fire by ‹simp›.
›
lemma routed_contribution_programs_wf:
assumes "⋀c' src a. sp_wf (it c' src a)"
and "⋀c' ca cc ex. sp_wf (cmb route c' ca cc ex)"
and "⋀c' w p. p ∈ set (extra route c' w) ⟹ sp_wf p"
shows "∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v).
sp_wf p"
using assms by (auto simp: routed_contribution_programs_def)
lemma routed_contribution_programs_combineI:
"(cc, ca) ∈ set (site_sel g v)
⟹ cmb route ctx ca cc v
∈ set (routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v)"
by (force simp: routed_contribution_programs_def)
lemma :
"t ∈ set (extra route ctx v)
⟹ t ∈ set (routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v)"
by (simp add: routed_contribution_programs_def)
lemma routed_contribution_programsE:
assumes "t ∈ set (routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v)"
obtains src a where "(src, a) ∈ set (pred_sel g v ctx)" "t = it ctx src a"
| cc ca where "(cc, ca) ∈ set (site_sel g v)" "t = cmb route ctx ca cc v"
| "t ∈ set (extra route ctx v)"
using assms by (auto simp: routed_contribution_programs_def)
text ‹
The local value a node's fold starts from: ‹bot0›, joined with the injected
‹d⇩0› at the CFG entry. An abbreviation, so every statement that spells the
conditional out prints as ‹rhs_init› and needs no unfolding.
‹rhs_init_global› is the global counterpart: the injected ‹g⇩0› at the
CFG entry, \<^const>‹bot› elsewhere.
›
abbreviation rhs_init :: "cfg ⇒ 'd::sup ⇒ 'd ⇒ pp ⇒ 'd" where
"rhs_init g bot0 d⇩0 v ≡ (if v = cfg_entry g then bot0 ⊔ d⇩0 else bot0)"
abbreviation rhs_init_global :: "cfg ⇒ 'h::bot ⇒ pp ⇒ 'h" where
"rhs_init_global g g⇩0 v ≡ (if v = cfg_entry g then g⇩0 else bot)"
definition routed_node_rhs ::
"(cfg ⇒ pp ⇒ 'c ⇒ ((pp × 'c + 'k) × edge_action) list)
⇒ (cfg ⇒ pp ⇒ (pp × call_action) list)
⇒ ('c ⇒ 'k)
⇒ (pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c)
⇒ ('c ⇒ pp × 'c + 'k ⇒ edge_action
⇒ (pp × 'c, 'k, ('d::bounded_semilattice_sup_bot,
'h::bounded_semilattice_sup_bot) dg_state,
('d, 'h) dg_state) strategy_program)
⇒ ((pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program)
⇒ ((pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ pp
⇒ (pp × 'c, 'k, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program list)
⇒ cfg ⇒ 'd ⇒ 'd ⇒ 'h
⇒ (pp × 'c, 'k, ('d, 'h) dg_state) eqsT"
where
"routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 =
(λ(v, c).
let t = sp_compile (side_rhs_fold_dg (rhs_init g bot0 d⇩0 v)
(routed_contribution_programs pred_sel site_sel route it cmb extra g c v))
in if v = cfg_entry g then Side (buffer_key_at c) (DG bot g⇩0) t else t)"
lemma eq_routed_node_rhs:
assumes wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g ctx w). sp_wf p"
shows
"eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)
(v, ctx) τ =
DG (side_acc_dg (rhs_init g bot0 d⇩0 v) τ
(routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v)) bot"
by (simp add: routed_node_rhs_def Let_def
traverse_side_rhs_fold_dg[OF wf])
lemma sides_routed_node_rhs:
assumes wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g ctx w). sp_wf p"
shows
"sides_of_rhs (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0
(v, ctx)) τ (Inr (buffer_key_at ctx)) =
(if v = cfg_entry g then DG bot g⇩0 else bot)
⊔ (⨆t←routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v.
sides_of_program t τ (Inr (buffer_key_at ctx)))"
by (simp add: routed_node_rhs_def Let_def
sides_of_program_side_rhs_fold_dg_char[OF wf]
bot_dg_state_def[symmetric] ac_simps)
subsection ‹The right-hand side as a join of its parts›
text ‹
At a fixed valuation the answer of \<^const>‹routed_node_rhs› is a join: the
node's initial value, one value per intra edge entering it, one per call
returning at it, and the values of the routing protocol's own programs, the
seed read among them. \<^const>‹rhs_init› names the first part in the
generator itself; the definitions below name the other three, and
‹routed_node_rhs_parts› states the answer as the join of all four. Every
part is the local half of a contribution's answer at the valuation;
publications do not enter the answer and are characterized by
‹sides_routed_node_rhs›.
›
definition rhs_edge where
"rhs_edge it τ ctx u a = dg_local (traverse_program (it ctx u a) τ)"
definition rhs_call where
"rhs_call cmb route τ ctx u ca v = dg_local (traverse_program (cmb route ctx ca u v) τ)"
definition rhs_seed where
"rhs_seed extra route τ ctx v = (⨆p←extra route ctx v. dg_local (traverse_program p τ))"
lemma routed_node_rhs_parts:
assumes wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c w). sp_wf p"
shows
"eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)
(v, c) τ =
DG (rhs_init g bot0 d⇩0 v
⊔ (⨆(u, a)←pred_sel g v c. rhs_edge it τ c u a)
⊔ (⨆(u, ca)←site_sel g v. rhs_call cmb route τ c u ca v)
⊔ rhs_seed extra route τ c v) bot"
by (simp add: eq_routed_node_rhs[OF wf] side_acc_dg_as_foldr routed_contribution_programs_def
rhs_edge_def rhs_call_def rhs_seed_def split_def comp_def sup_assoc)
subsection ‹Buffered generator: fold Side-free contributions, publish once›
text ‹
\<^const>‹routed_node_rhs› writes a node's own key once per contribution
that publishes there: several intra predecessors or several return call actions can
each independently emit a ‹Side (buffer_key_at c) ...›, so several writes to the same
‹buffer_key_at c› land in one RHS evaluation. ‹routed_node_rhs_buffered› folds
Side-free contribution programs (the caller's own ‹it_c› for ‹intra› and ‹cmb_c› for
‹comb›) with \<^const>‹fold_rhs_program› and publishes ‹buffer_key_at c› once, after every
contribution has been read.
That fold shapes the node's ∗‹own› key, but each call returning at the node
still publishes its callee's seed from inside its ‹cmb_c› program. Two call sites
resuming at the same node, as the two branches of a conditional that both end in a call
do, can therefore name one seed key twice. \<^const>‹buffer_sides› accumulates the
writes per key and preserves the declarative
\<^const>‹traverse_rhs›/\<^const>‹sides_of_rhs› value wherever it flushes, so the
correspondence with the unbuffered generator below is unaffected by the choice of
flush points.
The choice does decide when a seed reaches the solver. A call program publishes the
seed and then reads the callee's exit, and that read is what makes the solver evaluate
the callee. Held back to the answer, the seed arrives after the callee has been solved
from \<^const>‹bot›, and the seed's change then sends the caller round again. So a node
at which at most one call returns flushes before every local read, and the seed is
published before the exit is read, in the order of Goblint's ‹sidel› and
‹getl›. A node at which several calls return flushes at the answer only: a flush
before the first call's exit read would write a seed the second call may write again,
and an update rule that keeps one slot per origin would see a partial contribution
first in every evaluation. There ‹distinct_side_path_buffer_sides_answers_only›
bounds the writes unconditionally; at the other nodes the bound
‹distinct_side_path_buffer_sides› holds as long as one call program does not
write a seed again after reading an exit, which the shipped specifications'
single-alternative entry transfers ensure.
›
definition routed_node_rhs_buffered ::
"(cfg ⇒ pp ⇒ 'c ⇒ ((pp × 'c + 'k) × edge_action) list)
⇒ (cfg ⇒ pp ⇒ (pp × call_action) list)
⇒ ('c ⇒ 'k)
⇒ (pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c)
⇒ ('c ⇒ pp × 'c + 'k ⇒ edge_action
⇒ (pp × 'c, 'k, ('d::bounded_semilattice_sup_bot,
'h::bounded_semilattice_sup_bot) dg_state,
('d, 'h) dg_state) strategy_program)
⇒ ((pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program)
⇒ ((pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ pp
⇒ (pp × 'c, 'k, ('d, 'h) dg_state, ('d, 'h) dg_state) strategy_program list)
⇒ cfg ⇒ 'd ⇒ 'd ⇒ 'h
⇒ (pp × 'c, 'k, ('d, 'h) dg_state) eqsT"
where
"routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0 =
(λ(v, c).
let acc0 = DG (rhs_init g bot0 d⇩0 v) (rhs_init_global g g⇩0 v);
t = sp_compile (fold_rhs_program acc0
(routed_contribution_programs pred_sel site_sel route it_c cmb_c extra g c v))
in buffer_sides (λ_. length (site_sel g v) ≤ 1) (sp_lift_tree t (λres.
Side (buffer_key_at c) (DG bot (dg_global res)) (Answer (DG (dg_local res) bot)))))"
text ‹
\<^const>‹fold_rhs_program› threads its accumulator in evaluation order (a left
fold); the lemmas below need the equivalent right fold, since that is how each of
their own goals is already phrased. \<^const>‹traverse_rhs› only ever joins, so the
two forms agree by ‹foldr_sup_seed_swap›.
›
lemma eq_routed_node_rhs_buffered:
assumes wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it_c cmb_c
extra g ctx w). sp_wf p"
shows
"eq (routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0)
(v, ctx) τ =
DG (dg_local (foldr (λt acc'. traverse_program t τ ⊔ acc')
(routed_contribution_programs pred_sel site_sel route it_c cmb_c extra g ctx v)
(DG (rhs_init g bot0 d⇩0 v) (rhs_init_global g g⇩0 v)))) bot"
by (simp add: routed_node_rhs_buffered_def Let_def
traverse_fold_rhs_program_char_foldr[OF wf])
text ‹
The buffered generator answers the same join of parts as the reference
generator, over its own contribution programs. Its answer carries no global
half; the global part of the initial accumulator leaves through the
publication at ‹buffer_key_at c›.
›
lemma routed_node_rhs_buffered_parts:
assumes wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c w). sp_wf p"
shows
"eq (routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)
(v, c) τ =
DG (rhs_init g bot0 d⇩0 v
⊔ (⨆(u, a)←pred_sel g v c. rhs_edge it τ c u a)
⊔ (⨆(u, ca)←site_sel g v. rhs_call cmb route τ c u ca v)
⊔ rhs_seed extra route τ c v) bot"
proof -
have "eq (routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)
(v, c) τ
= eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) (v, c) τ"
by (simp add: eq_routed_node_rhs_buffered[OF wf] eq_routed_node_rhs[OF wf]
dg_local_foldr_generic side_acc_dg_as_foldr_seeded)
then show ?thesis
by (simp only: routed_node_rhs_parts[OF wf])
qed
lemma sides_routed_node_rhs_buffered:
assumes wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it_c cmb_c
extra g ctx w). sp_wf p"
and intra_free_at_key:
"⋀c' src a σ. sides_of_program (it_c c' src a) σ (Inr (buffer_key_at c')) = bot"
and comb_free_at_key: "⋀c' ca cc ex σ.
sides_of_program (cmb_c route c' ca cc ex) σ (Inr (buffer_key_at c')) = bot"
and extra_free: "⋀c' w σ z x. x ∈ set (extra route c' w) ⟹ sides_of_program x σ z = bot"
shows "sides_of_rhs (routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g
bot0 d⇩0 g⇩0 (v, ctx)) τ (Inr (buffer_key_at ctx)) =
DG bot (dg_global (foldr (λt acc'. traverse_program t τ ⊔ acc')
(routed_contribution_programs pred_sel site_sel route it_c cmb_c extra g ctx v)
(DG (rhs_init g bot0 d⇩0 v) (rhs_init_global g g⇩0 v))))"
proof -
have free: "⋀w σ x.
x ∈ set (routed_contribution_programs pred_sel site_sel route it_c cmb_c extra g ctx w)
⟹ sides_of_program x σ (Inr (buffer_key_at ctx)) = bot"
using intra_free_at_key comb_free_at_key extra_free
by (blast elim: routed_contribution_programsE)
show ?thesis
proof (cases "v = cfg_entry g")
case True
have z0: "(sides_of_program (fold_rhs_program (DG (bot0 ⊔ d⇩0) g⇩0)
(routed_contribution_programs pred_sel site_sel route it_c cmb_c extra g ctx
(cfg_entry g))) τ) (Inr (buffer_key_at ctx)) = bot"
by (simp only: sides_of_program_fold_rhs_program_char[OF wf]
foldr_sup_bot_of_all_bot[OF free[where w = "cfg_entry g"]])
from True show ?thesis
by (simp add: routed_node_rhs_buffered_def Let_def
traverse_fold_rhs_program_char_foldr[OF wf]
bot_dg_state_def sup_dg_state_def z0)
next
case False
have z0: "(sides_of_program (fold_rhs_program (DG bot0 bot)
(routed_contribution_programs pred_sel site_sel route it_c cmb_c extra g ctx v)) τ) (Inr (buffer_key_at ctx)) = bot"
by (simp only: sides_of_program_fold_rhs_program_char[OF wf]
foldr_sup_bot_of_all_bot[OF free[where w = v]])
from False show ?thesis
by (simp add: routed_node_rhs_buffered_def Let_def
traverse_fold_rhs_program_char_foldr[OF wf]
bot_dg_state_def sup_dg_state_def z0)
qed
qed
subsection ‹Correspondence: the buffered generator against the direct one›
text ‹
A pointwise correspondence between two parallel contribution lists -- one Side-free
(feeding \<^const>‹fold_rhs_program›), one Side-emitting (feeding \<^const>‹side_rhs_fold_dg›)
-- lifts to their whole-list fold, in both the local-answer and global-side
components. This is the list-level engine behind
‹routed_node_rhs_buffered_correspondence›: each of ‹intra›, ‹comb›, and
‹extra› instantiates it once, and ‹list_all2_appendI› combines the three.
›
text ‹
‹routed_node_rhs_buffered›'s declarative value matches
‹routed_node_rhs›'s, given that each buffered hook is the Side-free
contribution analogue of its unbuffered counterpart at the SAME ‹buffer_key_at ctx› slot.
‹intra› and ‹comb› carry the same six hypotheses -- pairwise local/global/dep
agreement, buffered-side freeness at the key, side purity, and off-key agreement --
and ‹extra› is Side-free and answers only its local slot
(‹extra_free›/‹extra_local_only› -- ‹routed_entry_seed_programs› discharges both by direct
inspection, since it answers on its ‹dg_local› half and issues no ‹Side›). A local-only
intra hook discharges its six trivially: its program publishes nothing, so the
contribution analogue is the program itself and every hypothesis is reflexive or
‹bot›; an intra hook that genuinely publishes at ‹buffer_key_at ctx› supplies its reshaped
contribution program, exactly as a reshaped ‹routed_call_program› does for ‹cmb›.
›
lemma routed_node_rhs_buffered_correspondence:
fixes cmb cmb_c ::
"(pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('d::bounded_semilattice_sup_bot,
'h::bounded_semilattice_sup_bot) dg_state,
('d, 'h) dg_state) strategy_program"
assumes wf_c: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it_c cmb_c
extra g ctx w). sp_wf p"
and wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g ctx w). sp_wf p"
and intra_t: "⋀c' src a τ. dg_local (traverse_program (it_c c' src a) τ)
= dg_local (traverse_program (it c' src a) τ)"
and intra_side_pure: "⋀c' src a τ.
dg_local (sides_of_program (it c' src a) τ (Inr (buffer_key_at c'))) = bot"
and intra_s: "⋀c' src a τ. dg_global (traverse_program (it_c c' src a) τ)
= dg_global (sides_of_program (it c' src a) τ (Inr (buffer_key_at c')))"
and intra_free_at_key:
"⋀c' src a τ. sides_of_program (it_c c' src a) τ (Inr (buffer_key_at c')) = bot"
and intra_sides_off_key: "⋀c' src a τ z. z ≠ Inr (buffer_key_at c')
⟹ sides_of_program (it_c c' src a) τ z = sides_of_program (it c' src a) τ z"
and intra_dep: "⋀c' src a τ. dep_program τ (it_c c' src a) = dep_program τ (it c' src a)"
and comb_t: "⋀c' ca cc ex τ. dg_local (traverse_program (cmb_c route c' ca cc ex) τ)
= dg_local (traverse_program (cmb route c' ca cc ex) τ)"
and comb_side_pure: "⋀c' ca cc ex τ.
dg_local (sides_of_program (cmb route c' ca cc ex) τ (Inr (buffer_key_at c'))) = bot"
and comb_s: "⋀c' ca cc ex τ. dg_global (traverse_program (cmb_c route c' ca cc ex) τ)
= dg_global (sides_of_program (cmb route c' ca cc ex) τ (Inr (buffer_key_at c')))"
and comb_free_at_key: "⋀c' ca cc ex τ.
sides_of_program (cmb_c route c' ca cc ex) τ (Inr (buffer_key_at c')) = bot"
and comb_sides_off_key: "⋀c' ca cc ex τ z. z ≠ Inr (buffer_key_at c')
⟹ sides_of_program (cmb_c route c' ca cc ex) τ z
= sides_of_program (cmb route c' ca cc ex) τ z"
and comb_dep: "⋀c' ca cc ex τ. dep_program τ (cmb_c route c' ca cc ex)
= dep_program τ (cmb route c' ca cc ex)"
and extra_free: "⋀c' w τ z x. x ∈ set (extra route c' w) ⟹ sides_of_program x τ z = bot"
and extra_local_only: "⋀c' w τ x.
x ∈ set (extra route c' w) ⟹ dg_global (traverse_program x τ) = bot"
shows "traverse_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ
= traverse_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ"
(is ?T)
and "dep_aux τ
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx))
= dep_aux τ
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx))"
(is ?D)
and "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ
= sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ"
(is ?S)
proof -
let ?intra_new = "map (λ(src, a). it_c ctx src a) (pred_sel g v ctx)"
let ?intra_old = "map (λ(src, a). it ctx src a) (pred_sel g v ctx)"
let ?comb_new = "map (λ(cc, ca). cmb_c route ctx ca cc v) (site_sel g v)"
let ?comb_old = "map (λ(cc, ca). cmb route ctx ca cc v) (site_sel g v)"
let ?extra = "extra route ctx v"
let ?acc0 = "DG (rhs_init g bot0 d⇩0 v) (rhs_init_global g g⇩0 v)"
let ?new = "routed_contribution_programs pred_sel site_sel route it_c cmb_c extra g ctx v"
let ?old = "routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v"
have new_split: "?new = ?intra_new @ ?comb_new @ ?extra"
by (simp add: routed_contribution_programs_def)
have old_split: "?old = ?intra_old @ ?comb_old @ ?extra"
by (simp add: routed_contribution_programs_def)
have intra_local: "list_all2
(λt_new t_old. dg_local (traverse_program t_new τ) = dg_local (traverse_program t_old τ))
?intra_new ?intra_old"
by (rule list_all2_map_diag) (auto simp: intra_t)
have intra_global: "list_all2
(λt_new t_old. dg_global (traverse_program t_new τ)
= dg_global (sides_of_program t_old τ (Inr (buffer_key_at ctx))))
?intra_new ?intra_old"
by (rule list_all2_map_diag) (auto simp: intra_s)
have comb_local: "list_all2
(λt_new t_old. dg_local (traverse_program t_new τ) = dg_local (traverse_program t_old τ))
?comb_new ?comb_old"
by (rule list_all2_map_diag) (auto simp: comb_t)
have comb_global: "list_all2
(λt_new t_old. dg_global (traverse_program t_new τ)
= dg_global (sides_of_program t_old τ (Inr (buffer_key_at ctx))))
?comb_new ?comb_old"
by (rule list_all2_map_diag) (auto simp: comb_s)
have extra_local: "list_all2
(λt_new t_old. dg_local (traverse_program t_new τ) = dg_local (traverse_program t_old τ))
?extra ?extra"
by (rule list.rel_refl_strong) simp
have extra_global: "list_all2
(λt_new t_old. dg_global (traverse_program t_new τ)
= dg_global (sides_of_program t_old τ (Inr (buffer_key_at ctx))))
?extra ?extra"
by (rule list.rel_refl_strong) (simp add: extra_free extra_local_only bot_dg_state_def)
have local_list: "list_all2
(λt_new t_old. dg_local (traverse_program t_new τ) = dg_local (traverse_program t_old τ))
?new ?old"
unfolding new_split old_split
using intra_local comb_local extra_local by (intro list_all2_appendI)
have global_list: "list_all2 (λt_new t_old. dg_global (traverse_program t_new τ)
= dg_global (sides_of_program t_old τ (Inr (buffer_key_at ctx))))
?new ?old"
unfolding new_split old_split
using intra_global comb_global extra_global by (intro list_all2_appendI)
show ?T
proof -
have "traverse_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ
= DG (dg_local (foldr (λt acc'. traverse_program t τ ⊔ acc') ?new ?acc0)) bot"
by (simp add: eq_routed_node_rhs_buffered[OF wf_c] routed_contribution_programs_def)
also have "… = DG (dg_local ?acc0 ⊔ (⨆t←?new. dg_local (traverse_program t τ))) bot"
by (simp add: dg_local_foldr_generic foldr_join_seed_out dg_local_join_list)
also have "… = DG (dg_local ?acc0 ⊔ (⨆t←?old. dg_local (traverse_program t τ))) bot"
by (simp only: foldr_sup_list_all2_cong[OF local_list])
also have "… = DG (side_acc_dg (dg_local ?acc0) τ ?old) bot"
by (simp add: side_acc_dg_as_foldr)
also have "… = traverse_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ"
by (simp add: eq_routed_node_rhs[OF wf] routed_contribution_programs_def)
finally show ?thesis .
qed
have global_new: "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ (Inr (buffer_key_at ctx))
= DG bot (dg_global (foldr (λt acc'. traverse_program t τ ⊔ acc') ?new ?acc0))"
unfolding routed_contribution_programs_def[symmetric]
by (intro sides_routed_node_rhs_buffered[OF wf_c])
(use intra_free_at_key comb_free_at_key extra_free in blast)+
have dg_global_new_char: "dg_global (foldr (λt acc'. traverse_program t τ ⊔ acc') ?new ?acc0)
= dg_global ?acc0
⊔ (⨆t←?old. dg_global (sides_of_program t τ (Inr (buffer_key_at ctx))))"
proof -
have "dg_global (foldr (λt acc'. traverse_program t τ ⊔ acc') ?new ?acc0)
= dg_global ?acc0 ⊔ (⨆t←?new. dg_global (traverse_program t τ))"
by (simp add: dg_global_foldr_generic foldr_join_seed_out dg_global_join_list)
also have "… = dg_global ?acc0
⊔ (⨆t←?old. dg_global (sides_of_program t τ (Inr (buffer_key_at ctx))))"
by (simp only: foldr_sup_list_all2_cong[OF global_list])
finally show ?thesis .
qed
have old_elem_side_pure: "⋀t. t ∈ set ?old
⟹ dg_local (sides_of_program t τ (Inr (buffer_key_at ctx))) = bot"
using comb_side_pure extra_free
by (auto simp: intra_side_pure bot_dg_state_def routed_contribution_programs_def
split: prod.splits)
have old_fold_side_pure:
"dg_local (⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx))) = bot"
by (rule foldr_sides_dg_local_bot) (rule old_elem_side_pure)
have old_fold_collapse: "(⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx)))
= DG bot (dg_global (⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx))))"
using old_fold_side_pure
by (cases "⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx))") simp
have old_sides: "sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ
(Inr (buffer_key_at ctx))
= DG bot (dg_global ?acc0
⊔ dg_global (⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx))))"
proof -
have "sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ
(Inr (buffer_key_at ctx))
= (if v = cfg_entry g then DG bot g⇩0 else bot)
⊔ (⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx)))"
by (rule sides_routed_node_rhs[OF wf])
also have "… = DG bot (dg_global ?acc0
⊔ dg_global (⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx))))"
by (subst old_fold_collapse)
(cases "v = cfg_entry g", simp_all add: DG_sup_bot_left bot_dg_state_def)
finally show ?thesis .
qed
have S_at_key: "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ (Inr (buffer_key_at ctx))
= sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ
(Inr (buffer_key_at ctx))"
proof -
have "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ (Inr (buffer_key_at ctx))
= DG bot (dg_global (foldr (λt acc'. traverse_program t τ ⊔ acc') ?new ?acc0))"
by (rule global_new)
also have "… = DG bot (dg_global ?acc0
⊔ dg_global (⨆t←?old. sides_of_program t τ (Inr (buffer_key_at ctx))))"
by (simp only: dg_global_new_char foldr_dg_global_sides_char)
also have "… = sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ
(Inr (buffer_key_at ctx))"
by (rule old_sides[symmetric])
finally show ?thesis .
qed
have intra_dep_list: "list_all2 (λt_new t_old. dep_program τ t_new = dep_program τ t_old)
?intra_new ?intra_old"
by (rule list_all2_map_diag) (auto simp: intra_dep)
have comb_dep_list: "list_all2 (λt_new t_old. dep_program τ t_new = dep_program τ t_old)
?comb_new ?comb_old"
by (rule list_all2_map_diag) (auto simp: comb_dep)
have extra_dep: "list_all2 (λt_new t_old. dep_program τ t_new = dep_program τ t_old)
?extra ?extra"
by (rule list.rel_refl_strong) simp
have dep_list: "list_all2 (λt_new t_old. dep_program τ t_new = dep_program τ t_old)
?new ?old"
unfolding new_split old_split
using intra_dep_list comb_dep_list extra_dep by (intro list_all2_appendI)
show ?D
proof -
have "dep_aux τ
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx))
= (⋃t∈set ?new. dep_program τ t)"
by (simp add: routed_node_rhs_buffered_def Let_def
dep_program_fold_rhs_program_char[OF wf_c])
also have "… = (⋃t∈set ?old. dep_program τ t)"
by (rule list_all2_Union_eq[OF dep_list])
also have "… = dep_aux τ
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx))"
by (simp add: routed_node_rhs_def Let_def
dep_program_side_rhs_fold_dg_char[OF wf])
finally show ?thesis .
qed
have intra_sides_off: "⋀z. z ≠ Inr (buffer_key_at ctx)
⟹ list_all2 (λt_new t_old. sides_of_program t_new τ z = sides_of_program t_old τ z)
?intra_new ?intra_old"
by (rule list_all2_map_diag) (auto simp: intra_sides_off_key)
have comb_sides_off: "⋀z. z ≠ Inr (buffer_key_at ctx)
⟹ list_all2 (λt_new t_old. sides_of_program t_new τ z = sides_of_program t_old τ z)
?comb_new ?comb_old"
by (rule list_all2_map_diag) (auto simp: comb_sides_off_key)
have extra_sides_off: "⋀z.
list_all2 (λt_new t_old. sides_of_program t_new τ z = sides_of_program t_old τ z)
?extra ?extra"
by (rule list.rel_refl_strong) simp
have sides_list_off: "⋀z. z ≠ Inr (buffer_key_at ctx)
⟹ list_all2 (λt_new t_old. sides_of_program t_new τ z = sides_of_program t_old τ z)
?new ?old"
unfolding new_split old_split
using intra_sides_off comb_sides_off extra_sides_off by (intro list_all2_appendI)
have fold_sides_off: "⋀z. z ≠ Inr (buffer_key_at ctx) ⟹
(⨆t←?new. sides_of_program t τ z) = (⨆t←?old. sides_of_program t τ z)"
by (rule foldr_sup_list_all2_cong) (rule sides_list_off)
show ?S
proof (rule ext)
fix z
show "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ z
= sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ z"
proof (cases "z = Inr (buffer_key_at ctx)")
case True
with S_at_key show ?thesis by simp
next
case False
have new_off: "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0
(v, ctx)) τ z
= (⨆t←?new. sides_of_program t τ z)"
using False
by (simp add: routed_node_rhs_buffered_def Let_def
sides_of_program_fold_rhs_program_char[OF wf_c] bot_dg_state_def[symmetric])
have old_off: "sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ z
= (⨆t←?old. sides_of_program t τ z)"
using False
by (simp add: routed_node_rhs_def Let_def
sides_of_program_side_rhs_fold_dg_char[OF wf])
from new_off old_off fold_sides_off[OF False] show ?thesis by simp
qed
qed
qed
text ‹
The observational interface \<^const>‹part_post_solution› actually consumes: given the
correspondence, a buffered post-solution is also an unbuffered one. Callers only need
this fact, never the tree-shape argument behind ‹routed_node_rhs_buffered_correspondence›
itself -- \<^const>‹part_post_solution›'s three conjuncts (‹dep⇩L›, ‹eq›, ‹sides_of_rhs›) are
exactly ‹?D›/‹?T›/‹?S›, read pointwise at each ‹u ∈ vars›.
›
lemma part_post_solution_routed_node_rhs_buffered:
fixes cmb cmb_c ::
"(pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('d::bounded_semilattice_sup_bot,
'h::bounded_semilattice_sup_bot) dg_state,
('d, 'h) dg_state) strategy_program"
assumes wf_c: "⋀c' w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it_c
cmb_c extra g c' w). sp_wf p"
and wf: "⋀c' w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c' w). sp_wf p"
and intra_t: "⋀c' src a τ. dg_local (traverse_program (it_c c' src a) τ)
= dg_local (traverse_program (it c' src a) τ)"
and intra_side_pure: "⋀c' src a τ.
dg_local (sides_of_program (it c' src a) τ (Inr (buffer_key_at c'))) = bot"
and intra_s: "⋀c' src a τ. dg_global (traverse_program (it_c c' src a) τ)
= dg_global (sides_of_program (it c' src a) τ (Inr (buffer_key_at c')))"
and intra_free_at_key:
"⋀c' src a τ. sides_of_program (it_c c' src a) τ (Inr (buffer_key_at c')) = bot"
and intra_sides_off_key: "⋀c' src a τ z. z ≠ Inr (buffer_key_at c')
⟹ sides_of_program (it_c c' src a) τ z = sides_of_program (it c' src a) τ z"
and intra_dep: "⋀c' src a τ. dep_program τ (it_c c' src a) = dep_program τ (it c' src a)"
and comb_t: "⋀c' ca cc ex τ. dg_local (traverse_program (cmb_c route c' ca cc ex) τ)
= dg_local (traverse_program (cmb route c' ca cc ex) τ)"
and comb_side_pure: "⋀c' ca cc ex τ.
dg_local (sides_of_program (cmb route c' ca cc ex) τ (Inr (buffer_key_at c'))) = bot"
and comb_s: "⋀c' ca cc ex τ. dg_global (traverse_program (cmb_c route c' ca cc ex) τ)
= dg_global (sides_of_program (cmb route c' ca cc ex) τ (Inr (buffer_key_at c')))"
and comb_free_at_key: "⋀c' ca cc ex τ.
sides_of_program (cmb_c route c' ca cc ex) τ (Inr (buffer_key_at c')) = bot"
and comb_sides_off_key: "⋀c' ca cc ex τ z. z ≠ Inr (buffer_key_at c')
⟹ sides_of_program (cmb_c route c' ca cc ex) τ z
= sides_of_program (cmb route c' ca cc ex) τ z"
and comb_dep: "⋀c' ca cc ex τ. dep_program τ (cmb_c route c' ca cc ex)
= dep_program τ (cmb route c' ca cc ex)"
and extra_free: "⋀c' w τ z x. x ∈ set (extra route c' w) ⟹ sides_of_program x τ z = bot"
and extra_local_only: "⋀c' w τ x.
x ∈ set (extra route c' w) ⟹ dg_global (traverse_program x τ) = bot"
and pp_buf: "part_post_solution
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0)
x sigma vars"
shows "part_post_solution
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) x sigma vars"
proof -
let ?Tbuf =
"routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it_c cmb_c extra g bot0 d⇩0 g⇩0"
let ?Told =
"routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0"
have corr: "⋀u. traverse_rhs (?Tbuf u) sigma = traverse_rhs (?Told u) sigma
∧ dep_aux sigma (?Tbuf u) = dep_aux sigma (?Told u)
∧ sides_of_rhs (?Tbuf u) sigma = sides_of_rhs (?Told u) sigma"
proof -
fix u :: "pp × 'c"
obtain v ctx where u: "u = (v, ctx)" by (cases u) auto
show "traverse_rhs (?Tbuf u) sigma = traverse_rhs (?Told u) sigma
∧ dep_aux sigma (?Tbuf u) = dep_aux sigma (?Told u)
∧ sides_of_rhs (?Tbuf u) sigma = sides_of_rhs (?Told u) sigma"
unfolding u
using routed_node_rhs_buffered_correspondence
[where cmb = cmb and cmb_c = cmb_c and it = it and it_c = it_c
and route = route and buffer_key_at = buffer_key_at,
OF wf_c wf
intra_t intra_side_pure intra_s intra_free_at_key intra_sides_off_key intra_dep
comb_t comb_side_pure comb_s comb_free_at_key comb_sides_off_key comb_dep
extra_free extra_local_only]
by simp
qed
have "part_post_solution ?Tbuf x sigma vars = part_post_solution ?Told x sigma vars"
by (rule part_post_solution_cong) (use corr in blast)+
with pp_buf show ?thesis by simp
qed
text ‹
The same correspondence without reshaped hooks, for contribution programs that
answer nothing on their global half. Such a program may still publish at
‹buffer_key_at ctx›: the buffered generator keeps that publication as it is
and adds only the seed it hoists, which is the unbuffered generator's entry
publication. A specification that splits its state and publishes the global
half through its manager is of this kind.
›
lemma routed_node_rhs_buffered_correspondence_answers_local:
fixes cmb ::
"(pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('d::bounded_semilattice_sup_bot,
'h::bounded_semilattice_sup_bot) dg_state,
('d, 'h) dg_state) strategy_program"
assumes wf: "⋀w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g ctx w). sp_wf p"
and answers_local: "⋀w p τ. p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g ctx w) ⟹ dg_global (traverse_program p τ) = bot"
shows "traverse_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0
(v, ctx)) τ
= traverse_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ"
(is ?T)
and "dep_aux τ
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0
(v, ctx))
= dep_aux τ
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx))"
(is ?D)
and "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0
(v, ctx)) τ
= sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ"
(is ?S)
proof -
let ?ps = "routed_contribution_programs pred_sel site_sel route it cmb extra g ctx v"
let ?acc0 = "DG (rhs_init g bot0 d⇩0 v) (rhs_init_global g g⇩0 v)"
have glob: "dg_global (foldr (λt acc'. traverse_program t τ ⊔ acc') ?ps ?acc0)
= dg_global ?acc0"
proof -
have "(⨆t←?ps. dg_global (traverse_program t τ)) = bot"
by (rule foldr_sup_bot_of_all_bot) (rule answers_local)
then show ?thesis
by (simp only: dg_global_foldr_generic foldr_join_seed_out[where a = "dg_global ?acc0"]
sup_bot_right)
qed
show ?T
proof -
have "traverse_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0
(v, ctx)) τ
= DG (foldr (λt acc'. dg_local (traverse_program t τ) ⊔ acc') ?ps (dg_local ?acc0)) bot"
by (simp add: eq_routed_node_rhs_buffered[OF wf] dg_local_foldr_generic)
also have "… = DG (side_acc_dg (dg_local ?acc0) τ ?ps) bot"
by (simp add: side_acc_dg_as_foldr_seeded)
also have "… = traverse_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ"
by (simp add: eq_routed_node_rhs[OF wf])
finally show ?thesis .
qed
show ?D
by (simp add: routed_node_rhs_buffered_def routed_node_rhs_def Let_def
dep_program_fold_rhs_program_char[OF wf] dep_program_side_rhs_fold_dg_char[OF wf])
show ?S
proof (rule ext)
fix z
show "sides_of_rhs
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0
(v, ctx)) τ z
= sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 (v, ctx)) τ z"
using glob
by (cases "v = cfg_entry g")
(auto simp: routed_node_rhs_buffered_def routed_node_rhs_def Let_def
sides_of_program_fold_rhs_program_char[OF wf]
sides_of_program_side_rhs_fold_dg_char[OF wf]
traverse_fold_rhs_program_char_foldr[OF wf] sup_commute bot_dg_state_def[symmetric])
qed
qed
lemma part_post_solution_routed_node_rhs_buffered_answers_local:
fixes cmb ::
"(pp ⇒ 'c ⇒ 'd ⇒ call_action ⇒ 'c) ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
⇒ (pp × 'c, 'k, ('d::bounded_semilattice_sup_bot,
'h::bounded_semilattice_sup_bot) dg_state,
('d, 'h) dg_state) strategy_program"
assumes wf: "⋀c' w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c' w). sp_wf p"
and answers_local: "⋀c' w p τ. p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c' w) ⟹ dg_global (traverse_program p τ) = bot"
and pp_buf: "part_post_solution
(routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)
x sigma vars"
shows "part_post_solution
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) x sigma vars"
proof -
let ?Tbuf =
"routed_node_rhs_buffered pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0"
let ?Told =
"routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0"
have corr: "⋀u. traverse_rhs (?Tbuf u) sigma = traverse_rhs (?Told u) sigma
∧ dep_aux sigma (?Tbuf u) = dep_aux sigma (?Told u)
∧ sides_of_rhs (?Tbuf u) sigma = sides_of_rhs (?Told u) sigma"
proof -
fix u :: "pp × 'c"
obtain v ctx where u: "u = (v, ctx)" by (cases u) auto
show "traverse_rhs (?Tbuf u) sigma = traverse_rhs (?Told u) sigma
∧ dep_aux sigma (?Tbuf u) = dep_aux sigma (?Told u)
∧ sides_of_rhs (?Tbuf u) sigma = sides_of_rhs (?Told u) sigma"
unfolding u
by (intro conjI routed_node_rhs_buffered_correspondence_answers_local[OF wf])
(erule answers_local)+
qed
have "part_post_solution ?Tbuf x sigma vars = part_post_solution ?Told x sigma vars"
by (rule part_post_solution_cong) (use corr in blast)+
with pp_buf show ?thesis by simp
qed
subsection ‹Threefold monotonicity for an arbitrary generator instance›
text ‹
The three
@{const TD_side_mono} preconditions reduce to a per-program contract on the
intra, combine, and extra hooks, discharged once here and reusable at every
context policy --- a routed context policy is then a second interpretation
of this reduction, not a second monotonicity proof. The outer @{const Side}
wrapper at @{term "cfg_entry g"} is invisible to @{const traverse_rhs} and
@{const dep_aux} (a \<^const>‹Side› node only ever repackages, never queries);
it only has to be threaded through the @{const sides_of_rhs} case via
‹fun_upd_sup_mono›, below.
›
lemma routed_node_rhs_mono_eq:
fixes g :: cfg
assumes wf: "⋀c w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c w). sp_wf p"
assumes intra_mono: "⋀v c src a s1 s2. (src, a) ∈ set (pred_sel g v c) ⟹ s1 ≤ s2 ⟹
traverse_program (it c src a) s1 ≤ traverse_program (it c src a) s2"
assumes comb_mono: "⋀v c cc ca s1 s2. (cc, ca) ∈ set (site_sel g v) ⟹ s1 ≤ s2 ⟹
traverse_program (cmb route c ca cc v) s1 ≤ traverse_program (cmb route c ca cc v) s2"
assumes extra_mono: "⋀v c t s1 s2. t ∈ set (extra route c v) ⟹ s1 ≤ s2 ⟹
traverse_program t s1 ≤ traverse_program t s2"
shows
"is_mono_eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)"
proof (unfold is_mono_eq_def, intro allI)
fix x s1 s2
show "s1 ≤ s2 ⟶
eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) x s1
≤ eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) x s2"
proof (intro impI)
assume le: "s1 ≤ s2"
obtain v c where x: "x = (v, c)" by (cases x)
have tree_mono:
"∀t ∈ set (routed_contribution_programs pred_sel site_sel route it cmb extra g c v).
∀s1 s2. s1 ≤ s2 ⟶ traverse_program t s1 ≤ traverse_program t s2"
using intra_mono comb_mono extra_mono
by (auto simp: routed_contribution_programs_def)
show "eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) x s1
≤ eq (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) x s2"
unfolding x eq_routed_node_rhs[OF wf]
using side_rhs_fold_dg_mono[OF wf tree_mono le]
by (simp add: traverse_side_rhs_fold_dg[OF wf])
qed
qed
text ‹A generic fact about pointwise-ordered functions, function update, and
join --- nothing here mentions a strategy tree. It has exactly one use, in
the publication case below, so it stays beside that call site rather than in
generic infrastructure.›
lemma fun_upd_sup_mono:
fixes m1 m2 :: "'b ⇒ 'a::bounded_semilattice_sup_bot"
assumes "m1 ≤ m2"
shows "m1(y := m1 y ⊔ cd) ≤ m2(y := m2 y ⊔ cd)"
proof -
have eq: "⋀m. m(y := m y ⊔ cd) = m ⊔ ((λ_. bot)(y := cd))"
unfolding fun_upd_def sup_fun_def by (rule ext) simp
show ?thesis unfolding eq by (rule sup_mono[OF assms order_refl])
qed
lemma routed_node_rhs_mono_sides:
fixes g :: cfg
assumes wf: "⋀c w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c w). sp_wf p"
assumes intra_sides_mono: "⋀v c src a s1 s2. (src, a) ∈ set (pred_sel g v c) ⟹ s1 ≤ s2 ⟹
sides_of_program (it c src a) s1 ≤ sides_of_program (it c src a) s2"
assumes comb_sides_mono: "⋀v c cc ca s1 s2. (cc, ca) ∈ set (site_sel g v) ⟹ s1 ≤ s2 ⟹
sides_of_program (cmb route c ca cc v) s1 ≤ sides_of_program (cmb route c ca cc v) s2"
assumes extra_sides_mono: "⋀v c t s1 s2. t ∈ set (extra route c v) ⟹ s1 ≤ s2 ⟹
sides_of_program t s1 ≤ sides_of_program t s2"
shows
"mono_sides (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)"
proof (unfold mono_sides_def, intro allI)
fix x s1 s2
show "s1 ≤ s2 ⟶
sides_of_rhs (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 x) s1
≤ sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 x) s2"
proof (intro impI)
assume le: "s1 ≤ s2"
obtain v c where x: "x = (v, c)" by (cases x)
have tree_sides_mono: "⋀w. ∀t ∈ set
(routed_contribution_programs pred_sel site_sel route it cmb extra g c w).
∀s1 s2. s1 ≤ s2 ⟶ sides_of_program t s1 ≤ sides_of_program t s2"
using intra_sides_mono comb_sides_mono extra_sides_mono
by (auto simp: routed_contribution_programs_def)
have fold_le: "⋀acc w. sides_of_program (side_rhs_fold_dg acc
(routed_contribution_programs pred_sel site_sel route it cmb extra g c w)) s1
≤ sides_of_program (side_rhs_fold_dg acc
(routed_contribution_programs pred_sel site_sel route it cmb extra g c w)) s2"
by (rule side_rhs_fold_dg_sides_mono[OF wf tree_sides_mono le])
show "sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 x) s1
≤ sides_of_rhs
(routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0 x) s2"
unfolding x routed_node_rhs_def
by (simp add: Let_def fold_le fun_upd_sup_mono[OF fold_le] split: if_splits)
qed
qed
lemma routed_node_rhs_mono_deps:
fixes g :: cfg
assumes wf: "⋀c w. ∀p ∈ set (routed_contribution_programs pred_sel site_sel route it cmb
extra g c w). sp_wf p"
assumes intra_deps_mono: "⋀v c src a. (src, a) ∈ set (pred_sel g v c) ⟹
mono_tree_deps (sp_compile (it c src a))"
assumes comb_deps_mono: "⋀v c cc ca. (cc, ca) ∈ set (site_sel g v) ⟹
mono_tree_deps (sp_compile (cmb route c ca cc v))"
assumes extra_deps_mono: "⋀v c t. t ∈ set (extra route c v)
⟹ mono_tree_deps (sp_compile t)"
shows
"mono_deps (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0)"
proof (unfold mono_deps_def, intro allI)
fix x s1 s2
show "s1 ≤ s2 ⟶
dep (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) s1 x
⊆ dep (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) s2 x"
proof (intro impI)
assume ord: "s1 ≤ s2"
obtain v c where x: "x = (v, c)" by (cases x)
have tree_deps_mono: "⋀w t.
t ∈ set (routed_contribution_programs pred_sel site_sel route it cmb extra g c w)
⟹ mono_tree_deps (sp_compile t)"
using intra_deps_mono comb_deps_mono extra_deps_mono
by (auto simp: routed_contribution_programs_def)
have fold_mono: "⋀acc w. mono_tree_deps (sp_compile (side_rhs_fold_dg acc
(routed_contribution_programs pred_sel site_sel route it cmb extra g c w)))"
by (rule side_rhs_fold_dg_mono_tree_deps[OF wf]) (rule tree_deps_mono)
have dsub: "⋀acc w. dep_program s1 (side_rhs_fold_dg acc
(routed_contribution_programs pred_sel site_sel route it cmb extra g c w))
⊆ dep_program s2 (side_rhs_fold_dg acc
(routed_contribution_programs pred_sel site_sel route it cmb extra g c w))"
using fold_mono[unfolded mono_tree_deps_def] ord by blast
show "dep (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) s1 x
⊆ dep (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0) s2 x"
unfolding x dep_def routed_node_rhs_def
by (simp add: Let_def dsub split: if_splits)
qed
qed
text ‹
The generator never sees a specification: the intra hook supplies each
edge's program, exactly as ‹cmb› and ‹extra› already supply theirs,
so which unknowns an equation reads and which keys it publishes are
properties of the supplied programs, not of the generator. The one key the
generator names itself is ‹buffer_key_at c›, at the CFG entry, where it publishes
‹g⇩0›; a routed activation seed is not its own but arrives through
‹extra›.
›
subsection ‹Initial global values as side effects›
text ‹
We represent an initial global value as an actual contribution to its global
unknown, so the solved unknown itself contains that value. Reads do not need
to join initialization into the stored value implicitly.
‹with_init init T› provides this for any equation system: the right-hand side of an
unknown ‹x› first publishes every pair of ‹init x›, then continues as ‹T x›. An
instance that publishes no initial values passes ‹λ_. []›, and the system is ‹T›.
›
definition init_sides :: "('g × 'd) list ⇒ ('x, 'g, 'd) strategy_tree ⇒ ('x, 'g, 'd) strategy_tree"
where
"init_sides xs t = foldr (λ(k, d) t. Side k d t) xs t"
definition with_init :: "('x ⇒ ('g × 'd) list) ⇒ ('x, 'g, 'd) eqsT ⇒ ('x, 'g, 'd) eqsT"
where
"with_init init T = (λx. init_sides (init x) (T x))"
lemma with_init_Nil [simp]: "with_init (λ_. []) T = T"
by (simp add: with_init_def init_sides_def)
lemma init_sides_Cons [simp]: "init_sides ((k, d) # xs) t = Side k d (init_sides xs t)"
by (simp add: init_sides_def)
lemma init_sides_Nil [simp]: "init_sides [] t = t"
by (simp add: init_sides_def)
lemma traverse_rhs_init_sides [simp]: "traverse_rhs (init_sides xs t) σ = traverse_rhs t σ"
proof (induction xs)
case (Cons p xs) then show ?case by (cases p) simp
qed simp
lemma dep_aux_init_sides [simp]: "dep_aux σ (init_sides xs t) = dep_aux σ t"
proof (induction xs)
case (Cons p xs) then show ?case by (cases p) simp
qed simp
lemma sides_of_rhs_init_sides_ge:
"sides_of_rhs t σ ≤ sides_of_rhs (init_sides xs (t :: ('x, 'g, 'd::bounded_semilattice_sup_bot) strategy_tree)) σ"
proof (induction xs)
case (Cons p xs)
obtain k d where p: "p = (k, d)" by (cases p)
have "sides_of_rhs (init_sides xs t) σ
≤ sides_of_rhs (init_sides (p # xs) t) σ"
unfolding p le_fun_def by (simp add: Let_def)
with Cons.IH show ?case by (rule order_trans)
qed simp
lemma sides_of_rhs_init_sides_at:
"(k, d) ∈ set xs
⟹ d ≤ sides_of_rhs (init_sides xs (t :: ('x, 'g, 'd::bounded_semilattice_sup_bot) strategy_tree)) σ (Inr k)"
proof (induction xs)
case (Cons p xs)
obtain k' d' where p: "p = (k', d')" by (cases p)
show ?case
proof (cases "(k, d) = p")
case True
with p show ?thesis by (simp add: Let_def)
next
case False
with Cons.prems have "d ≤ sides_of_rhs (init_sides xs t) σ (Inr k)"
by (intro Cons.IH) simp
also have "… ≤ sides_of_rhs (init_sides (p # xs) t) σ (Inr k)"
unfolding p by (simp add: Let_def)
finally show ?thesis .
qed
qed simp
text ‹
A post-solution of the wrapped system bounds the wrapped system's own equations, since
the wrapper only adds side effects, and covers every initial value at its key.
›
lemma tree_covered_at_init_sides:
"tree_covered_at (init_sides xs (t :: ('x, 'g, 'd::bounded_semilattice_sup_bot) strategy_tree)) σ u
⟹ tree_covered_at t σ u"
unfolding tree_covered_at_def
by simp (meson order_trans sides_of_rhs_init_sides_ge)
lemma dep_with_init [simp]: "dep (with_init init T) σ x = dep T σ x"
by (simp add: dep_def with_init_def)
lemma post_bounded_with_init_at:
assumes
"post_bounded (with_init init (T :: ('x, 'g, 'd::bounded_semilattice_sup_bot) eqsT)) x σ vars"
and "u ∈ vars" and "(k, d) ∈ set (init u)"
shows "d ≤ σ (Inr k)"
proof -
have "sides_of_rhs (init_sides (init u) (T u)) σ ≤ σ"
using post_boundedD[OF assms(1,2)] by (simp add: with_init_def tree_covered_at_def)
then have "sides_of_rhs (init_sides (init u) (T u)) σ (Inr k) ≤ σ (Inr k)"
by (rule le_funD)
with sides_of_rhs_init_sides_at[OF assms(3)] show ?thesis by (rule order_trans)
qed
lemma part_post_solution_with_init:
"part_post_solution (with_init init (T :: ('x, 'g, 'd::bounded_semilattice_sup_bot) eqsT)) x σ vars
⟹ part_post_solution T x σ vars"
unfolding part_post_solution_iff_tree_covered_at
proof (intro conjI ballI; elim conjE)
assume all: "∀u∈vars. dep⇩L (with_init init T) σ u ⊆ vars
∧ tree_covered_at (with_init init T u) σ u"
fix u assume u: "u ∈ vars"
show "dep⇩L T σ u ⊆ vars" using all u by (simp add: dep⇩L_def)
show "tree_covered_at (T u) σ u"
using all u by (simp add: with_init_def) (blast intro: tree_covered_at_init_sides)
qed
end
end