Theory Network_Impl
section ‹Implementation of Flow Networks›
theory Network_Impl
imports
"Lib/Refine_Add_Fofu"
Ford_Fulkerson
begin
subsection ‹Type Constraints›
text ‹We constrain the types that we use for implementation.›
text ‹We define capacities to be integer values.›
type_synonym capacity_impl = int
type_synonym flow_impl = "capacity_impl flow"
text ‹We define a locale that assumes that the nodes are natural numbers in the
range @{term "{0..<N}"}.›
locale Network_Impl = Network c s t for c :: "capacity_impl graph" and s t +
fixes N :: nat
assumes V_ss: "V⊆{0..<N}"
begin
lemma E_ss: "E ⊆ {0..<N}×{0..<N}" using E_ss_VxV V_ss by auto
end
subsection ‹Basic Operations›
context Network_Impl
begin
subsubsection ‹Residual Graph›
text ‹Get the residual capacity of an edge.›
definition cf_get :: "flow_impl ⇒ edge ⇒ capacity_impl nres"
where "cf_get cf e ≡ do {
assert (e∈E ∪ E¯);
return (cf e)
}"
text ‹Update the residual capacity of an edge.›
definition cf_set :: "flow_impl ⇒ edge ⇒ capacity_impl ⇒ flow_impl nres"
where "cf_set cf e x ≡ do {
assert (e∈E ∪ E¯);
return (cf (e:=x))
}"
text ‹Obtain the initial residual graph.›
definition cf_init :: "flow_impl nres"
where "cf_init ≡ return (op_mtx_new c)"
subsubsection ‹Adjacency Map›
text ‹Obtain the list of adjacent nodes for a specified node.›
definition am_get :: "(node ⇒ node list) ⇒ node ⇒ node list nres"
where "am_get am u ≡ do {
assert (u∈V);
return (am u)
}"
text ‹Test whether a node identifier is actually a node.
As not all numbers in the range @{term ‹{0..<N}›} must identify nodes,
this function uses the adjacency map to check whether there are adjacent
edges. Due to the network constraints, all nodes have adjacent edges.
›
definition am_is_in_V :: "(node ⇒ node list) ⇒ node ⇒ bool nres"
where "am_is_in_V am u ≡ do {
return (am u ≠ [])
}"
lemma am_is_in_V_correct[THEN order_trans, refine_vcg]:
assumes "(am,adjacent_nodes) ∈ nat_rel → ⟨nat_rel⟩list_set_rel"
shows "am_is_in_V am u ≤ (spec x. x ⟷ u∈V)"
proof -
have "u∈V ⟷ adjacent_nodes u ≠ {}"
unfolding V_def adjacent_nodes_def by auto
also have "… ⟷ am u ≠ []"
using fun_relD[OF assms IdI[of u]]
by (auto simp: list_set_rel_def in_br_conv)
finally show ?thesis unfolding am_is_in_V_def by refine_vcg auto
qed
end
subsubsection ‹Registration of Basic Operations to Sepref›
text ‹Bundles the setup for registration of abstract operations.›
bundle Network_Impl_Sepref_Register begin
text ‹Automatically rewrite to ‹i_mtx› interface type›
lemmas [map_type_eqs] =
map_type_eqI[of "TYPE(capacity_impl flow)" "TYPE(capacity_impl i_mtx)"]
end
context Network_Impl
begin
subsubsection ‹Registration of Abstract Operations›
context
includes Network_Impl_Sepref_Register
begin
sepref_register N s t
sepref_register c :: "capacity_impl graph"
sepref_register cf_get cf_set cf_init
sepref_register am_get am_is_in_V
end
end
subsection ‹Refinement To Efficient Data Structures›
subsubsection ‹Functions from Nodes by Arrays›
text ‹
We provide a template for implementing functions from nodes by arrays.
Outside the node range, the abstract functions have a default value.
This template is then used for refinement of various data structures.
›
definition "is_nf N dflt f a
≡ ∃⇩Al. a↦⇩al * ↑(length l = N ∧ (∀i<N. l!i = f i) ∧ (∀i≥N. f i = dflt))"
lemma nf_init_rule:
"<emp> Array.new N dflt <is_nf N dflt (λ_. dflt)>"
unfolding is_nf_def by sep_auto
lemma nf_copy_rule[sep_heap_rules]:
"<is_nf N dflt f a> array_copy a <λr. is_nf N dflt f a * is_nf N dflt f r>"
unfolding is_nf_def by sep_auto
lemma nf_lookup_rule[sep_heap_rules]:
"v<N ⟹ <is_nf N dflt f a> Array.nth a v <λr. is_nf N dflt f a *↑(r = f v)>"
unfolding is_nf_def by sep_auto
lemma nf_update_rule[sep_heap_rules]:
"v<N ⟹ <is_nf N dflt f a> Array.upd v x a <is_nf N dflt (f(v:=x))>"
unfolding is_nf_def by sep_auto
subsubsection ‹Automation Setup for Side-Condition Discharging›
context Network_Impl
begin
lemma mtx_nonzero_iff[simp]: "mtx_nonzero c = E"
unfolding E_def by (auto simp: mtx_nonzero_def)
lemma mtx_nonzeroN: "mtx_nonzero c ⊆ {0..<N}×{0..<N}" using E_ss by simp
lemma in_mtx_nonzeroN[simp]: "(u,v) ∈ mtx_nonzero c ⟹ u<N ∧ v<N"
using mtx_nonzeroN by auto
lemma inV_less_N[simp]: "v∈V ⟹ v<N" using V_ss by auto
lemma inEIE_lessN[simp]: "e∈E ∨ e∈E¯ ⟹ case e of (u,v) ⇒ u<N ∧ v<N"
using E_ss by auto
lemmas [simp] = nested_case_prod_simp
subsubsection ‹Network Parameters by Identity›
abbreviation (in -) cap_assn :: "capacity_impl ⇒ _" where "cap_assn ≡ id_assn"
abbreviation (in -) "edge_assn ≡ nat_assn ×⇩a nat_assn"
abbreviation (in -) (input) "node_assn ≡ nat_assn"
text ‹Refine number of nodes, and source and sink node by themselves›
lemmas [sepref_import_param] =
IdI[of N]
IdI[of s]
IdI[of t]
lemma c_hnr[sepref_fr_rules]:
"(uncurry0 (return c),uncurry0 (RETURN c))
∈unit_assn⇧k →⇩a pure (nat_rel ×⇩r nat_rel → Id)"
by (sepref_to_hoare) sep_auto
subsubsection ‹Residual Graph by Adjacency Matrix›
definition (in -) "cf_assn N ≡ asmtx_assn N cap_assn"
abbreviation cf_assn where "cf_assn ≡ Network_Impl.cf_assn N"
lemma [intf_of_assn]: "intf_of_assn (cf_assn) TYPE(capacity_impl i_mtx)"
by simp
sepref_thm cf_get_impl is "uncurry (PR_CONST cf_get)"
:: "cf_assn⇧k *⇩a edge_assn⇧k →⇩a cap_assn"
unfolding cf_get_def cf_assn_def PR_CONST_def
by sepref
concrete_definition (in -) cf_get_impl
uses Network_Impl.cf_get_impl.refine_raw is "(uncurry ?f,_)∈_"
sepref_thm cf_set_impl is "uncurry2 (PR_CONST cf_set)"
:: "cf_assn⇧d *⇩a edge_assn⇧k *⇩a cap_assn⇧k →⇩a cf_assn"
unfolding cf_set_def cf_assn_def PR_CONST_def by sepref
concrete_definition (in -) cf_set_impl
uses Network_Impl.cf_set_impl.refine_raw is "(uncurry2 ?f,_)∈_"
sepref_thm cf_init_impl is "uncurry0 (PR_CONST cf_init)"
:: "unit_assn⇧k →⇩a cf_assn"
unfolding PR_CONST_def cf_assn_def cf_init_def
apply (rewrite amtx_fold_custom_new[of N N])
by sepref
concrete_definition (in -) cf_init_impl
uses Network_Impl.cf_init_impl.refine_raw is "(uncurry0 ?f,_)∈_"
lemmas [sepref_fr_rules] =
cf_get_impl.refine[OF Network_Impl_axioms]
cf_set_impl.refine[OF Network_Impl_axioms]
cf_init_impl.refine[OF Network_Impl_axioms]
subsubsection ‹Adjacency Map by Array›
definition (in -) "am_assn N ≡ is_nf N ([]::nat list)"
abbreviation am_assn where "am_assn ≡ Network_Impl.am_assn N"
lemma am_get_hnr[sepref_fr_rules]:
"(uncurry Array.nth, uncurry (PR_CONST am_get))
∈ am_assn⇧k *⇩a node_assn⇧k →⇩a list_assn id_assn"
unfolding am_assn_def am_get_def list_assn_pure_conv
by sepref_to_hoare (sep_auto simp: refine_pw_simps)
definition (in -) "am_is_in_V_impl am u ≡ do {
amu ← Array.nth am u;
return (¬is_Nil amu)
}"
lemma am_is_in_V_hnr[sepref_fr_rules]: "(uncurry am_is_in_V_impl, uncurry (am_is_in_V))
∈ [λ(_,v). v<N]⇩a am_assn⇧k *⇩a node_assn⇧k → bool_assn"
unfolding am_assn_def am_is_in_V_def am_is_in_V_impl_def
apply sepref_to_hoare
apply (sep_auto simp: refine_pw_simps split: list.split)
done
end
subsection ‹Computing the Flow Value›
text ‹We define an algorithm to compute the value of a flow from
the residual graph
›
locale RGraph_Impl = RGraph c s t cf + Network_Impl c s t N
for c :: "capacity_impl flow" and s t N cf
lemma rgraph_and_network_impl_imp_rgraph_impl:
assumes "RGraph c s t cf"
assumes "Network_Impl c s t N"
shows "RGraph_Impl c s t N cf"
using assms by (rule Network_Impl.RGraph_Impl.intro)
lemma (in RGraph) val_by_adj_map:
assumes AM: "is_adj_map am"
shows "f.val = (∑v∈set (am s). cf (v,s))"
proof -
have [simp]: "set (am s) = E``{s}"
using AM unfolding is_adj_map_def
by auto
note f.val_by_cf
also note rg_is_cf
also have "(∑(u, v)∈outgoing s. cf (v, u))
= ((∑v∈set (am s). cf (v,s)))"
by (simp add: sum_outgoing_pointwise)
finally show ?thesis .
qed
context Network_Impl
begin
definition "compute_flow_val_aux am cf ≡ do {
succs ← am_get am s;
sum_impl (λv. cf_get cf (v,s)) (set succs)
}"
lemma (in RGraph_Impl) compute_flow_val_aux_correct:
assumes "is_adj_map am"
shows "compute_flow_val_aux am cf ≤ (spec v. v = f.val)"
unfolding val_by_adj_map[OF assms]
unfolding compute_flow_val_aux_def cf_get_def am_get_def
apply (refine_vcg sum_impl_correct)
apply (vc_solve simp: s_node)
subgoal using assms unfolding is_adj_map_def by auto
done
text ‹For technical reasons (poor foreach-support of Sepref tool),
we have to add another refinement step: ›
definition "compute_flow_val am cf ≡ (do {
succs ← am_get am s;
nfoldli succs (λ_. True) (λx a. do {
b ← cf_get cf (x, s);
return (a + b)
}) 0
})"
lemma (in RGraph_Impl) compute_flow_val_correct[THEN order_trans, refine_vcg]:
assumes "is_adj_map am"
shows "compute_flow_val am cf ≤ (spec v. v = f.val)"
proof -
have [refine_dref_RELATES]: "RELATES (⟨Id⟩list_set_rel)"
by (simp add: RELATES_def)
show ?thesis
apply (rule order_trans[OF _ compute_flow_val_aux_correct[OF assms]])
unfolding compute_flow_val_def compute_flow_val_aux_def sum_impl_def
apply (rule refine_IdD)
apply (refine_rcg LFO_refine bind_refine')
apply refine_dref_type
apply vc_solve
using assms
by (auto
simp: list_set_rel_def br_def am_get_def is_adj_map_def
simp: refine_pw_simps)
qed
context
includes Network_Impl_Sepref_Register
begin
sepref_register compute_flow_val
end
sepref_thm compute_flow_val_impl
is "uncurry (PR_CONST compute_flow_val)"
:: "am_assn⇧k *⇩a cf_assn⇧k →⇩a cap_assn"
unfolding compute_flow_val_def PR_CONST_def
by sepref
concrete_definition (in -) compute_flow_val_impl
uses Network_Impl.compute_flow_val_impl.refine_raw is "(uncurry ?f,_)∈_"
lemmas compute_flow_val_impl_hnr[sepref_fr_rules]
= compute_flow_val_impl.refine[OF Network_Impl_axioms]
end
text ‹We also export a correctness theorem on the separation logic level›
lemma compute_flow_val_impl_correct[sep_heap_rules]:
assumes "RGraph_Impl c s t N cf"
assumes AM: "Graph.is_adj_map c am"
shows "<cf_assn N cf cfi * am_assn N am ami>
compute_flow_val_impl s N ami cfi
<λv. cf_assn N cf cfi * am_assn N am ami
* ↑( v = Flow.val c s (RPreGraph.f c cf) )>⇩t"
proof -
interpret RGraph_Impl c s t N cf by fact
from hn_refine_ref[OF
compute_flow_val_correct[OF AM order_refl]
compute_flow_val_impl_hnr[to_hnr, unfolded autoref_tag_defs]]
show ?thesis
apply (simp add: hn_ctxt_def pure_def hn_refine_def f_def)
apply (rule cons_post_rule)
apply assumption
apply sep_auto
done
qed
subsubsection ‹Computing the Exact Number of Nodes›
context Network_Impl
begin
lemma am_to_adj_nodes_refine:
assumes AM: "is_adj_map am"
shows "(am u, adjacent_nodes u) ∈ ⟨nat_rel⟩list_set_rel"
using AM
unfolding adjacent_nodes_def is_adj_map_def
by (auto simp: list_set_rel_def in_br_conv)
definition "init_C am ≡ do {
let cardV=0;
nfoldli [0..<N] (λ_. True) (λv cardV. do {
assert (v<N);
inV ← am_is_in_V am v;
if inV then do {
return (cardV + 1)
} else
return cardV
}) cardV
}"
lemma init_C_correct:
assumes AM: "is_adj_map am"
shows "init_C am ≤ SPEC (λC. C = card V)"
unfolding init_C_def
apply (refine_vcg
nfoldli_rule[where I="λl1 _ C. C = card (V∩set l1)"]
)
apply clarsimp_all
using V_ss
apply (auto simp: upt_eq_lel_conv Int_absorb2 am_to_adj_nodes_refine[OF AM])
done
context
includes Network_Impl_Sepref_Register
begin
sepref_register init_C
end
sepref_thm fifo_init_C_impl is "(PR_CONST init_C)"
:: "am_assn⇧k →⇩a nat_assn"
unfolding init_C_def PR_CONST_def
by sepref
concrete_definition (in -) fifo_init_C_impl
uses Network_Impl.fifo_init_C_impl.refine_raw is "(?f,_)∈_"
lemmas [sepref_fr_rules] = fifo_init_C_impl.refine[OF Network_Impl_axioms]
end
end