Theory Gabow_Skeleton_Code
section ‹Code Generation for the Skeleton Algorithm \label{sec:skel_code}›
theory Gabow_Skeleton_Code
imports
Gabow_Skeleton "../ds/Stack" "../ds/Graph_Impl" "../lib/More_B_Assn"
begin
section ‹BCONST lemmas›
definition BCONST :: "'b ⇒ 'a ⇒ 'a" where "BCONST c m ≡ m"
lemma annot_BCONST: "m = BCONST c m" by (simp add: BCONST_def)
definition bind_const :: "'a ⇒ 'a nres ⇒ ('a ⇒ 'b nres) ⇒ 'b nres"
where "bind_const c ≡ Refine_Basic.bind"
lemma bind_BCONST_pat[def_pat_rules]: "Refine_Basic.bind$(BCONST$c$m)$f ≡ UNPROTECT (bind_const c)$m$f"
unfolding BCONST_def bind_const_def by auto
lemma Let_BCONST_pat[def_pat_rules]: "Let$(BCONST$c$cc)$f ≡ UNPROTECT (bind_const c)$(RETURN$cc)$f"
unfolding BCONST_def bind_const_def by auto
lemma id_op_bind_const[id_rules]:
"PR_CONST (bind_const c) ::⇩i TYPE('a nres ⇒ ('a ⇒ 'b nres) ⇒ 'b nres)"
by simp
lemma hn_bind_const[sepref_comb_rules]:
assumes PRE: "vassn_tag Γ ⟹ m ≤ RETURN c"
assumes D1: "hn_refine Γ m' Γ1 Rh CP⇩1 m"
assumes D2:
"⋀x'. bind_ref_tag c m ⟹ CP_assm (CP⇩1 x') ⟹
hn_refine (hn_ctxt Rh c x' ** Γ1) (f' x') (Γ2 x') R (CP⇩2 x') (f c)"
assumes IMP: "⋀x'. Γ2 x' ⊢ hn_ctxt Rx c x' ** Γ'"
assumes "MK_FREE Rx fr"
shows "hn_refine Γ (doM {x←m'; r←f' x; fr x; Mreturn r}) Γ' R (CP_SEQ CP⇩1 CP⇩2) (PR_CONST (bind_const c)$m$(λ⇩2x. f x))"
proof (rule hn_refine_vassn_tagI)
assume "vassn_tag Γ"
then have X: "m = RETURN c ∧ x=c" if "RETURN x ≤ m" for x
using PRE that dual_order.trans by fastforce
show ?thesis
unfolding APP_def PROTECT2_def bind_const_def PR_CONST_def CP_SEQ_def
apply (rule hnr_bind[where ?Γ2.0="λx x'. ↑(x=c) ** G x'" for G])
apply fact
apply (drule X) apply (clarsimp simp: sep_algebra_simps) apply (rule D2)
unfolding bind_ref_tag_def CP_assm_def apply simp apply simp
apply (clarsimp simp: entails_lift_extract_simps sep_algebra_simps) apply fact
by fact
qed
section ‹snat lemmas›
lemma m1_notin_snat_rel: "(-1,x)∉snat_rel' TYPE(size_T)"
by (auto simp: snat_rel_def snat.rel_def snat_invar_def in_br_conv)
lemma in_snat_rel_snat: "(ii,i)∈snat_rel ⟹ snat ii = i"
by (auto dest!: in_snat_rel_int simp: snat_def)
lemma in_snat_rel_leq: "(a, j + i) ∈ snat_rel ⟹ j ≤ snat a"
by (auto dest!: in_snat_rel_snat )
subsection ‹Adaptations from @thm‹snat_bin_ops›‹snat_cmp_ops›› thm snat_bin_ops snat_cmp_ops
lemmas snat_simps = snat_invar_alt max_snat_def snat_eq_unat unat_word_ariths
lemma plus_snat_refine: "a + b < max_snat LENGTH('a::len2) ⟹ (ai, a) ∈ snat_rel ⟹ (bi, b) ∈ snat_rel ⟹ (ai + bi, a + b) ∈ snat_rel" for ai bi ::"'a::len2 word"
unfolding snat_rel_def snat.rel_def
apply (auto simp: in_br_conv snat_simps)
done
lemma minus_snat_refine: "a ≥ b ⟹ (ai, a) ∈ snat_rel ⟹ (bi, b) ∈ snat_rel ⟹ (ai - bi, a - b) ∈ snat_rel"
unfolding snat_rel_def snat.rel_def
apply (auto simp: in_br_conv snat_simps unat_sub_if')
done
lemma lt_snat_refine: "(ai, a) ∈ snat_rel ⟹ (bi, b) ∈ snat_rel ⟹ a < b ⟷ ai < bi"
unfolding snat_rel_def snat.rel_def
apply(auto simp: in_br_conv snat_simps word_less_nat_alt)
done
lemma le_snat_refine: "(ai, a) ∈ snat_rel ⟹ (bi, b) ∈ snat_rel ⟹ a ≤ b ⟷ ai ≤ bi"
unfolding snat_rel_def snat.rel_def
apply(auto simp: in_br_conv snat_simps word_le_nat_alt)
done
locale fr_graph_impl_def_loc = fr_graph_defs E V0
for E :: "(nat × nat) set" and V0 and N :: nat and D :: nat +
fixes E_assn :: "(nat × nat) set ⇒ 'ei::llvm_rep ⇒ assn"
fixes succi :: "'ei ⇒ node_t ⇒ (node_t,size_T) stack llM"
fixes ni :: "size_t"
begin
abbreviation "node_rel ≡ b_rel (snat_rel' TYPE(node_T)) (λx. x<N)"
abbreviation "node_assn ≡ b_assn (snat_assn' TYPE(node_T)) (λx. x<N)"
abbreviation "data_rel ≡ b_rel (snat_rel' TYPE(node_T)) (λx. x<Suc D)"
abbreviation "data_assn ≡ b_assn (snat_assn' TYPE(node_T)) (λx. x<Suc D)"
fun α_node_state_inv where
" α_node_state_inv (STACK i) = i"
| "α_node_state_inv (DONE i) = N + i"
fun invar_node_state_inv where
"invar_node_state_inv (STACK i) = (i < N)"
| "invar_node_state_inv (DONE i) = (i < Suc D)"
definition "α_node_state N' i = (if i < N' then STACK i else DONE (i - N'))"
definition "invar_node_state N' i = (i < N' + Suc D)"
definition "node_state_rel N' = size_rel O br (α_node_state N') (invar_node_state N')"
definition "node_state_rel_alt' = {(nsi,ns)| nsi ns. case ns of STACK i ⇒ (nsi,i) ∈ node_rel | DONE j ⇒ (nsi-ni,j) ∈ data_rel}"
lemma node_state_rel_alt_def_aux1: "D + N < max_snat 64 ⟹ (ni, N) ∈ snat_rel ⟹ b = DONE x2 ⟹ (a - ni, x2) ∈ snat_rel ⟹ x2 < Suc D ⟹ ((a - ni) + ni, x2 + N) ∈ snat_rel"
apply (rule plus_snat_refine)
apply (drule nat_Suc_less_le_imp[of x2])
apply auto
done
lemma node_state_rel_alt_def_aux2: "D + N < max_snat 64 ⟹ (ni, N) ∈ snat_rel ⟹ ∀x1. b = STACK x1 ⟶ (a, x1) ∈ snat_rel ∧ x1 < N ⟹ ∀x2. b = DONE x2 ⟶ (a - ni, x2) ∈ snat_rel ∧ x2 < Suc D ⟹ (a, case b of STACK i ⇒ i| DONE j ⇒ j + N) ∈ snat_rel"
using node_state_rel_alt_def_aux1
apply(auto split: node_state.splits)
done
lemma node_state_rel_alt_def: "D + N < max_snat 64 ⟹ (ni, N) ∈ size_rel ⟹ node_state_rel N = node_state_rel_alt'"
unfolding node_state_rel_alt'_def node_state_rel_def
apply (auto split: node_state.splits simp: in_br_conv α_node_state_def invar_node_state_def split_ifs)
apply (meson leI minus_snat_refine)
apply (rule relcompI)
using node_state_rel_alt_def_aux2
apply blast
apply(auto split: node_state.splits simp: in_br_conv α_node_state_def invar_node_state_def)
done
abbreviation "node_state_assn N' ≡ pure (node_state_rel N')"
definition "is_DONE ns ≡ ∃i. ns = DONE i"
definition "is_STACK_v ns ≡ ∃v. ns = STACK v"
definition "is_SOME_DONE nso ≡ if is_None nso then False else is_DONE (the nso)"
definition "is_SOME_STACK_v nso ≡ if is_None nso then False else is_STACK_v (the nso)"
lemma m1_notin_node_state_rel: "(-1,x) ∉ node_state_rel N'"
unfolding node_state_rel_def
apply (auto split: node_state.splits simp: m1_notin_snat_rel)
done
definition [llvm_inline]: "is_DONE_impl x ≡ from_bool (x≥ni)"
definition [llvm_inline]: "is_STACK_v_impl x ≡ from_bool (x<ni)"
sublocale node: dflt_pure_option "-1" node_assn "ll_icmp_eq (-1)"
apply unfold_locales
subgoal
apply (auto simp: pure_def pred_lift_extract_simps del: ext intro!: ext)
unfolding node_state_rel_def
apply (auto simp: snat_rel_def snat.rel_def in_br_conv snat_invar_def split: node_state.splits)
done
subgoal proof goal_cases
case 1
interpret llvm_prim_arith_setup .
show ?case
unfolding bool.assn_def
apply vcg'
done
qed
subgoal by simp
done
definition node_none :: "nat option" where "node_none = None"
lemmas [sepref_fr_rules] = node.hn_None[folded node_none_def]
sepref_register node_none
sublocale node_state: dflt_pure_option "-1" "(node_state_assn N)" "ll_icmp_eq (-1)"
apply unfold_locales
subgoal
apply (auto simp: pure_def pred_lift_extract_simps del: ext intro!: ext)
unfolding node_state_rel_def
apply (auto simp: snat_rel_def snat.rel_def in_br_conv snat_invar_def split: node_state.splits)
done
subgoal proof goal_cases
case 1
interpret llvm_prim_arith_setup .
show ?case
unfolding bool.assn_def
apply vcg'
done
qed
subgoal by simp
done
definition node_state_none :: "node_state option" where "node_state_none = None"
lemmas [sepref_fr_rules] = node_state.hn_None[folded node_state_none_def]
sepref_register node_state_none
concrete_definition node_state_am_empty[llvm_code,llvm_inline] is node_state.am2_empty_def
concrete_definition node_state_am_lookup[llvm_code,llvm_inline] is node_state.am2_lookup_def
concrete_definition node_state_am_contains_key[llvm_code,llvm_inline] is node_state.am2_contains_key_def
concrete_definition node_state_am_update[llvm_code,llvm_inline] is node_state.am2_update_def
concrete_definition node_state_am_delete[llvm_code,llvm_inline] is node_state.am2_delete_def
lemmas [unfolded node_state_am_empty.refine,sepref_fr_rules] = node_state.am2_empty_hnr node_state.am2_empty_hnr_mop
lemmas [unfolded node_state_am_lookup.refine,sepref_fr_rules] = node_state.am2_lookup_hnr node_state.am2_lookup_hnr_mop
lemmas [unfolded node_state_am_contains_key.refine,sepref_fr_rules] = node_state.am2_contains_key_hnr node_state.am2_contains_key_hnr_mop
lemmas [unfolded node_state_am_update.refine,sepref_fr_rules] = node_state.am2_update_hnr node_state.am2_update_hnr_mop
lemmas [unfolded node_state_am_delete.refine,sepref_fr_rules] = node_state.am2_delete_hnr node_state.am2_delete_hnr_mop
end
locale fr_graph_impl_loc = fr_graph_impl_def_loc E V0 N D E_assn succi ni + fr_graph E V0
for E :: "(nat × nat) set" and V0 and N :: nat and D::nat
and E_assn :: "(nat × nat) set ⇒ 'ei::llvm_rep ⇒ assn"
and succi :: "'ei ⇒ node_t ⇒ (node_t,size_T) stack llM"
and ni
+
assumes succi_ref [sepref_fr_rules]: "(uncurry succi, uncurry mop_graph_succ) ∈ E_assn⇧k *⇩a node_assn⇧k →⇩a stack_assn node_assn"
assumes E_BOUND: "E ⊆ {0..<N} × {0..<N}"
assumes V0_BOUND: "V0 = {0..<N}"
assumes D_N_BOUND: "D + N < max_snat (LENGTH(size_T))"
assumes n_impl: "(ni, N) ∈ size_rel"
begin
definition "N_assn = pure {(ni,N)}"
lemmas [sepref_import_param] = n_impl
lemma reachable_bound: "E⇧*``V0 = {0..<N}"
proof safe
fix u v
assume "(u,v) ∈ E⇧*" "u ∈ V0"
then show "v ∈ {0..<N}"
apply (induction rule: rtrancl_induct)
using V0_BOUND E_BOUND by auto
next
fix v
assume "v ∈ {0..<N}"
then show "v ∈ E⇧*``V0"
unfolding V0_BOUND by blast
qed
lemma card_reachable_bound: "card (E⇧*``V0) = N"
using reachable_bound
by simp
lemma DONE_impl_refine_aux: "(a, a') ∈ snat_rel ⟹ a' < Suc D ⟹ (ni + a, N + a') ∈ snat_rel"
apply (rule plus_snat_refine)
using D_N_BOUND apply simp
using n_impl by simp
lemma STACK_impl_refine: "(id, STACK) ∈ node_rel → node_state_rel N"
by (auto simp: node_state_rel_def br_def α_node_state_def invar_node_state_def)
lemma DONE_impl_refine: "((+) ni, DONE) ∈ data_rel → node_state_rel N"
apply (clarsimp simp: node_state_rel_def br_def α_node_state_def invar_node_state_def)
apply (rule relcompI)
apply (erule DONE_impl_refine_aux; assumption)
apply auto
done
lemma is_STACK_v_impl_refine: "(is_STACK_v_impl, is_STACK_v) ∈ node_state_rel N → bool1_rel"
unfolding is_STACK_v_impl_def is_STACK_v_def
apply clarsimp
using n_impl
apply (auto simp: in_snat_rel_snat node_state_rel_def bool1_rel_def bool.rel_def in_br_conv
m1_notin_snat_rel α_node_state_def split_ifs
split: node_state.splits
dest: lt_snat_refine)
done
lemma is_DONE_impl_refine: "(is_DONE_impl, is_DONE) ∈ node_state_rel N → bool1_rel"
unfolding is_DONE_impl_def is_DONE_def
apply clarsimp
using n_impl
apply (auto simp: in_snat_rel_snat node_state_rel_def bool1_rel_def bool.rel_def in_br_conv
m1_notin_snat_rel in_snat_rel_leq α_node_state_def invar_node_state_def
split: node_state.splits
dest: lt_snat_refine)
done
lemmas [sepref_import_param] = STACK_impl_refine is_DONE_impl_refine is_STACK_v_impl_refine DONE_impl_refine
lemma hn_node_val[sepref_fr_rules]: "(Mreturn, RETURN o val) ∈ [λx. ∃j. x = STACK j]⇩a (node_state_assn N)⇧k → size_assn"
apply sepref_to_hoare
unfolding node_state_rel_alt_def[OF D_N_BOUND[simplified] n_impl] node_state_rel_alt'_def br_def
apply clarsimp
apply vcg
done
sepref_def is_SOME_DONE_impl is "RETURN o is_SOME_DONE" :: "node_state.option_assn⇧k →⇩a bool1_assn"
unfolding is_SOME_DONE_def
by sepref
concrete_definition (in -) is_SOME_DONE_ll' [llvm_code] is fr_graph_impl_loc.is_SOME_DONE_impl_def
lemmas [sepref_fr_rules] = is_SOME_DONE_impl.refine[unfolded is_SOME_DONE_ll'.refine[OF fr_graph_impl_loc_axioms]]
sepref_def is_SOME_STACK_v_impl is "RETURN o is_SOME_STACK_v" :: "node_state.option_assn⇧k →⇩a bool1_assn"
unfolding is_SOME_STACK_v_def
by sepref
concrete_definition (in -) is_SOME_STACK_v_ll' [llvm_code] is fr_graph_impl_loc.is_SOME_STACK_v_impl_def
lemmas [sepref_fr_rules] = is_SOME_STACK_v_impl.refine[unfolded is_SOME_STACK_v_ll'.refine[OF fr_graph_impl_loc_axioms]]
definition "GS_assn = stack_assn' TYPE(size_T) node_assn ×⇩a stack_assn' TYPE(size_T) size_assn ×⇩a node_state.am_assn N
×⇩a stack_assn' TYPE(size_T) (node_assn ×⇩a stack_assn' TYPE(size_T) node_assn)"
sepref_definition open_GS_ll is "RETURN o open_GS" :: "GS_assn⇧d →⇩a stack_assn' TYPE(size_T) node_assn ×⇩a stack_assn' TYPE(size_T) size_assn ×⇩a node_state.am_assn N
×⇩a stack_assn' TYPE(size_T) (node_assn ×⇩a stack_assn' TYPE(size_T) node_assn)"
unfolding GS_assn_def open_GS_def
by sepref
concrete_definition (in -) open_GS_ll' [llvm_code] is fr_graph_impl_loc.open_GS_ll_def
lemmas [sepref_fr_rules] = open_GS_ll.refine[unfolded open_GS_ll'.refine[OF fr_graph_impl_loc_axioms]]
sepref_definition close_GS_ll is "uncurry3 (RETURN oooo close_GS)" :: "(stack_assn' TYPE(size_T) node_assn)⇧d *⇩a (stack_assn' TYPE(size_T) size_assn)⇧d *⇩a (node_state.am_assn N)⇧d
*⇩a (stack_assn' TYPE(size_T) (node_assn ×⇩a stack_assn' TYPE(size_T) node_assn))⇧d →⇩a GS_assn"
unfolding GS_assn_def close_GS_def
apply sepref
done
concrete_definition (in -) close_GS_ll' [llvm_code] is fr_graph_impl_loc.close_GS_ll_def
lemmas [sepref_fr_rules] = close_GS_ll.refine[unfolded close_GS_ll'.refine[OF fr_graph_impl_loc_axioms]]
section ‹The operations for gabow skeleton are registered here.›
subsection ‹Operation: is_done_oimpl:›
lemma is_done_oimpl_alt: "is_done_oimpl v I = is_SOME_DONE (I v)"
unfolding is_done_oimpl_def is_SOME_DONE_def is_DONE_def
by (auto split: node_state.splits)
sepref_definition is_done_oimpl_ll is "uncurry (RETURN oo is_done_oimpl)" :: "node_assn⇧k *⇩a (node_state.am_assn N)⇧k →⇩a bool1_assn"
unfolding is_done_oimpl_alt
by sepref
concrete_definition (in -) is_done_oimpl_ll' [llvm_code] is fr_graph_impl_loc.is_done_oimpl_ll_def
lemmas [sepref_fr_rules] = is_done_oimpl_ll.refine[unfolded is_done_oimpl_ll'.refine[OF fr_graph_impl_loc_axioms]]
subsection ‹Operation: initial_impl›
definition initial_impl' :: "(nat × nat) set ⇒ _" where
"initial_impl' E' v0 I = do{ succs ← mop_graph_succ E' v0; RETURN (GS_initial_impl I v0 succs) }"
sepref_register initial_impl' :: "(nat × nat) set ⇒ nat ⇒ ((nat, node_state) i_map) ⇒ (nat list × nat list × (nat ⇒ node_state option) × (nat × nat list) list) nres"
lemma initial_impl_alt: "initial_impl = initial_impl' E"
unfolding initial_impl_def initial_impl'_def
by (simp add:)
lemma initial_impl'_alt: "initial_impl' = (λ E v0 I. (
do{
succs ← mop_graph_succ E v0;
if op_list_is_empty succs then do {
RETURN ([v0], [0], I(v0 ↦ STACK 0), [])
} else
RETURN ([v0], [0], I(v0 ↦ STACK 0), [(v0, succs)])
}))"
unfolding initial_impl'_def GS_initial_impl_def
by (auto simp: fun_eq_iff pw_eq_iff refine_pw_simps)
sepref_definition initial_ll is "uncurry2 (initial_impl')"::"E_assn⇧k *⇩a node_assn⇧k *⇩a (node_state.am_assn N)⇧d →⇩a GS_assn"
unfolding initial_impl'_alt GS_assn_def singleton_list_append
unfolding stack_fold_custom_empty[where 'l = size_T]
apply (annot_snat_const "TYPE(size_T)")
by sepref
concrete_definition (in -) initial_ll' [llvm_code] is fr_graph_impl_loc.initial_ll_def
lemmas [sepref_fr_rules] = initial_ll.refine[unfolded initial_ll'.refine[OF fr_graph_impl_loc_axioms]]
subsection ‹Operation: path_is_empty_impl›
sepref_definition path_is_empty_impl_ll is "RETURN o path_is_empty_impl" :: "GS_assn⇧k →⇩a bool1_assn"
unfolding path_is_empty_impl_def GS_assn_def GS_defs.S_def
unfolding prod.case_distrib[where h="λa. a=_"]
by sepref
concrete_definition (in -) path_is_empty_impl_ll' [llvm_code] is fr_graph_impl_loc.path_is_empty_impl_ll_def
lemmas [sepref_fr_rules] = path_is_empty_impl_ll.refine[unfolded path_is_empty_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
definition "select_edge_impl' SBIP ≡
do {
let (S,B,I,P) = open_GS SBIP;
if P=[] then
RETURN (node_none, close_GS S B I P)
else do {
let ((v,succs), P') = op_list_pop_last P;
ASSERT (∃j. I v = Some (STACK j));
j ← mop_map_lookup v I;
ASSERT (length B ≥ 1);
if val (the j) ≥ B ! (length B - 1) then do {
ASSERT (succs≠[]);
(w, succs) ← mop_list_pop_last succs;
let P = (if succs=[] then P' else op_list_append P' (v,succs));
RETURN (Some w, close_GS S B I P)
} else RETURN (node_none, close_GS S B I (op_list_append P' (v,succs)))
}
}"
lemma select_edge_impl_alt_def: "select_edge_impl SBIP = select_edge_impl' SBIP"
unfolding select_edge_impl_def GS_defs.sel_rem_last_def select_edge_impl'_def open_GS_def close_GS_def GS_defs.seg_start_def GS_defs.S_idx_of_def
apply(cases SBIP; simp)
apply(simp cong: if_cong)
apply(auto simp: node_none_def neq_Nil_conv_rev split: prod.splits)
done
sepref_definition select_edge_impl_ll is "select_edge_impl" :: "GS_assn⇧d →⇩a node.option_assn ×⇩a GS_assn"
unfolding select_edge_impl_alt_def select_edge_impl'_def
apply (annot_snat_const "TYPE(size_T)")
apply sepref
done
concrete_definition (in -) select_edge_impl_ll' [llvm_code] is fr_graph_impl_loc.select_edge_impl_ll_def
lemmas [sepref_fr_rules] = select_edge_impl_ll.refine[unfolded select_edge_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
subsection ‹Operation: is_on_stack_impl›
lemma is_on_stack_impl_alt: "is_on_stack_impl v s = is_SOME_STACK_v (GS_defs.I s v)"
unfolding is_on_stack_impl_def GS_defs.is_on_stack_impl_def is_SOME_STACK_v_def is_STACK_v_def
by (auto split: node_state.splits)
sepref_definition is_on_stack_impl_ll is "uncurry (RETURN oo is_on_stack_impl)" :: "node_assn⇧k *⇩a GS_assn⇧k →⇩a bool1_assn"
unfolding GS_assn_def is_on_stack_impl_alt GS_defs.I_def
by sepref
concrete_definition (in -) is_on_stack_impl_ll' [llvm_code] is fr_graph_impl_loc.is_on_stack_impl_ll_def
lemmas [sepref_fr_rules] = is_on_stack_impl_ll.refine[unfolded is_on_stack_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
subsection ‹Operation: collapse_impl›
sepref_definition find_seg_impl_ll is "uncurry GS_defs.find_seg_impl" :: "GS_assn⇧k *⇩a size_assn⇧k →⇩a size_assn"
unfolding GS_assn_def GS_defs.find_seg_impl_def GS_defs.B_def
unfolding prod.case_distrib[where h="length"]
unfolding prod.case_distrib[where h="λa. a ! _"]
apply (annot_snat_const "TYPE(size_T)")
by sepref
concrete_definition (in -) find_seg_impl_ll' [llvm_code] is fr_graph_impl_loc.find_seg_impl_ll_def
lemmas [sepref_fr_rules] = find_seg_impl_ll.refine[unfolded find_seg_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
definition "S_idx_of_impl SBIP v ≡
do {
ASSERT (∃ j. GS_defs.I SBIP v = Some (STACK j));
RETURN (val (the (GS_defs.I SBIP v)))
}"
sepref_definition S_idx_of_ll is "uncurry S_idx_of_impl" :: "GS_assn⇧k *⇩a node_assn⇧k →⇩a size_assn"
unfolding GS_assn_def S_idx_of_impl_def GS_defs.I_def
by sepref
concrete_definition (in -) S_idx_of_ll' [llvm_code] is fr_graph_impl_loc.S_idx_of_ll_def
lemmas [sepref_fr_rules] = S_idx_of_ll.refine[unfolded S_idx_of_ll'.refine[OF fr_graph_impl_loc_axioms]]
lemma idx_of_impl_alt_def: "GS_defs.idx_of_impl SBIP = (λ v.
do {
j ← S_idx_of_impl SBIP v;
ASSERT (j<length (GS_defs.S SBIP));
i ← GS_defs.find_seg_impl SBIP j;
RETURN i
})"
unfolding GS_defs.idx_of_impl_def GS_defs.S_idx_of_def
unfolding S_idx_of_impl_def
apply(auto simp: fun_eq_iff)
by metis
sepref_definition idx_of_impl_ll is "uncurry GS_defs.idx_of_impl" :: "GS_assn⇧k *⇩a node_assn⇧k →⇩a size_assn"
unfolding idx_of_impl_alt_def
unfolding prod.case_distrib[where h="λa. a _"]
unfolding prod.case_distrib[where h="λa. val (the a)"]
unfolding prod.case_distrib[where h="λa. a ≠ None"]
by sepref
concrete_definition (in -) idx_of_impl_ll' [llvm_code] is fr_graph_impl_loc.idx_of_impl_ll_def
lemmas [sepref_fr_rules] = idx_of_impl_ll.refine[unfolded idx_of_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
definition "collapse_impl_fr' v SBIP =
do {
i←GS_defs.idx_of_impl SBIP v;
let (S,B,I,P) = open_GS SBIP;
ASSERT (i+1 ≤ length B);
let B = take (i+1) B;
RETURN (close_GS S B I P)
}"
lemma collapse_impl_fr_alt_def: "collapse_impl_fr v SBIP = collapse_impl_fr' v SBIP"
unfolding collapse_impl_fr_def collapse_impl_fr'_def GS_defs.collapse_impl_def GS_defs.S_def GS_defs.B_def GS_defs.I_def GS_defs.P_def open_GS_def close_GS_def
apply(cases SBIP)
apply (auto split: prod.splits simp: fun_eq_iff)
done
sepref_definition collapse_ll is "uncurry collapse_impl_fr" :: "node_assn⇧k *⇩a GS_assn⇧d →⇩a GS_assn"
unfolding collapse_impl_fr_alt_def collapse_impl_fr'_def
apply (annot_snat_const "TYPE(size_T)")
apply sepref
done
concrete_definition (in -) collapse_ll' [llvm_code] is fr_graph_impl_loc.collapse_ll_def
lemmas [sepref_fr_rules] = collapse_ll.refine[unfolded collapse_ll'.refine[OF fr_graph_impl_loc_axioms]]
subsection ‹Operation: is_done_impl›
lemma is_done_impl_alt: "is_done_impl v s = is_SOME_DONE (GS_defs.I s v)"
unfolding is_done_impl_def GS_defs.is_done_impl_def is_SOME_DONE_def is_DONE_def
by (auto split: node_state.splits)
sepref_definition is_done_impl_ll is "uncurry (RETURN oo is_done_impl)" :: "node_assn⇧k *⇩a GS_assn⇧k →⇩a bool1_assn"
unfolding GS_assn_def is_done_impl_alt GS_defs.I_def
by sepref
concrete_definition (in -) is_done_impl_ll' [llvm_code] is fr_graph_impl_loc.is_done_impl_ll_def
lemmas [sepref_fr_rules] = is_done_impl_ll.refine[unfolded is_done_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
subsection ‹Operation: push_impl›
definition "GS_push_impl_alt s v succs ≡
case s of (S, B, I, P) ⇒ do {
ASSERT(length S < card(E⇧*``V0));
ASSERT(length B < card(E⇧*``V0));
ASSERT(length P < card(E⇧*``V0));
let j = length S;
let S = op_list_append S v;
let B = op_list_append B j;
let I = I(v ↦ STACK j);
let P = (if op_list_is_empty succs then P else op_list_append P (v,succs));
RETURN (S,B,I,P)
}"
definition push_impl' :: "(nat × nat) set ⇒ _" where "push_impl' E' v s = do { succs ← mop_graph_succ E' v; GS_push_impl_alt s v succs }"
sepref_register push_impl'
lemma push_impl_alt_def: "push_impl_fr = push_impl' E"
unfolding GS_push_impl_alt_def push_impl'_def push_impl_fr_def GS_defs.push_impl_def GS_defs.S_def GS_defs.B_def GS_defs.I_def GS_defs.P_def
GS_defs.push_impl_core_def Let_def
by (auto simp: fun_eq_iff pw_eq_iff refine_pw_simps)
lemma push_bound_aux: "n < card (E⇧* `` V0) ⟹ Suc n < max_snat LENGTH(size_T)"
using D_N_BOUND card_reachable_bound by linarith
lemma push_bound_aux2: "n < card (E⇧* `` V0) ⟹ n < N"
using D_N_BOUND card_reachable_bound by linarith
sepref_definition push_impl_ll is "uncurry2 (PR_CONST push_impl')" :: "E_assn⇧k *⇩a node_assn⇧k *⇩a GS_assn⇧d →⇩a GS_assn"
unfolding GS_assn_def push_impl'_def GS_push_impl_alt_def singleton_list_append PR_CONST_def
unfolding stack_fold_custom_empty[where 'l = size_T]
supply [simp] = push_bound_aux[simplified] push_bound_aux2
apply sepref
done
concrete_definition (in -) push_impl_ll' [llvm_code] is fr_graph_impl_loc.push_impl_ll_def
lemmas [sepref_fr_rules] = push_impl_ll.refine[unfolded push_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
subsection ‹Operation: pop_impl›
sepref_definition mark_as_done_ll is "uncurry4 mark_as_done" :: "(stack_assn' TYPE(size_T) node_assn)⇧k *⇩a (node_state.am_assn N)⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k *⇩a data_assn⇧k →⇩a (node_state.am_assn N)"
unfolding mark_as_done_def GS_defs.S_def GS_assn_def
by sepref
concrete_definition (in -) mark_as_done_ll' [llvm_code] is fr_graph_impl_loc.mark_as_done_ll_def
lemmas [sepref_fr_rules] = mark_as_done_ll.refine[unfolded mark_as_done_ll'.refine[OF fr_graph_impl_loc_axioms]]
definition "pop_impl2 SBIP i ≡
do {
let (S,B,I,P) = open_GS SBIP;
ASSERT (length B ≥ 1);
let lsi = length B - 1;
ASSERT (lsi<length B);
let l = B ! lsi;
let u = (if lsi + 1 = length B then length S else B ! (lsi + 1));
I ← mark_as_done S I l u i;
ASSERT (B≠[]);
S ← mop_list_take (last B) S;
ASSERT (B≠[]);
let (_,B) = op_list_pop_last B;
RETURN (close_GS S B I P)
}"
lemma pop_impl_fr_alt: "pop_impl_fr SBIP i = pop_impl2 SBIP i"
unfolding pop_impl_fr_def GS_defs.pop_impl_def pop_impl2_def GS_defs.seg_start_def GS_defs.seg_end_def open_GS_def close_GS_def
apply(cases SBIP; simp)
apply(simp cong: if_cong)
done
sepref_definition pop_impl_ll is "uncurry pop_impl_fr" :: "GS_assn⇧d *⇩a data_assn⇧k →⇩a GS_assn"
unfolding pop_impl_fr_alt pop_impl2_def
apply (annot_snat_const "TYPE(size_T)")
apply sepref
done
concrete_definition (in -) pop_impl_ll' [llvm_code] is fr_graph_impl_loc.pop_impl_ll_def
lemmas [sepref_fr_rules] = pop_impl_ll.refine[unfolded pop_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
sepref_register N
sepref_register path_is_empty_impl is_on_stack_impl collapse_impl_fr
is_done_impl push_impl_fr pop_impl_fr select_edge_impl
lemma list_to_set_rel: "distinct xs ⟹ (xs, set xs) ∈ ⟨Id⟩list_set_rel"
unfolding list_set_rel_def
apply(auto simp: br_def)
done
lemma bounded_list_set_rel: "([0..<N], V0) ∈ ⟨Id⟩list_set_rel"
unfolding list_set_rel_def
apply (auto simp: br_def V0_BOUND)
done
subsection ‹Refinement to nfoldli›
definition "skeleton_inner_while_body2 E' s =
do {
(vo,s) ← select_edge_impl s;
if (vo = None) then
pop_impl_fr s 0
else do {
let v = the(vo);
ASSERT (v ∈ E'⇧*``V0);
if is_on_stack_impl v s then do {
collapse_impl_fr v s
} else if ¬is_done_impl v s then do {
push_impl' E' v s
} else do {
RETURN s
}
}
}"
sepref_register skeleton_inner_while_body2 :: "(nat × nat) set
⇒ nat list × nat list × (nat ⇒ node_state option) × (nat × nat list) list
⇒ (nat list × nat list × (nat ⇒ node_state option) × (nat × nat list) list) nres"
lemma skeleton_inner_while_body_alt_def: "skeleton_inner_while_body SBIP = skeleton_inner_while_body2 E SBIP"
unfolding skeleton_inner_while_body_def skeleton_inner_while_body2_def
apply (fo_rule arg_cong)
apply (rule ext)
apply (auto simp: push_impl_alt_def )
done
sepref_definition skeleton_inner_while_body_ll is "uncurry (PR_CONST skeleton_inner_while_body2)" :: "E_assn⇧k *⇩a GS_assn⇧d →⇩a GS_assn"
unfolding skeleton_inner_while_body2_def PR_CONST_def
apply (annot_snat_const "TYPE(size_T)")
apply sepref
done
concrete_definition (in -) skeleton_inner_while_body_ll' [llvm_code] is fr_graph_impl_loc.skeleton_inner_while_body_ll_def
lemmas [sepref_fr_rules] = skeleton_inner_while_body_ll.refine[unfolded skeleton_inner_while_body_ll'.refine[OF fr_graph_impl_loc_axioms]]
definition skeleton_impl_nfoldli :: "(nat × nat) set ⇒ nat oGS nres" where
"skeleton_impl_nfoldli E' ≡ do {
let I=Map.empty;
r ← nfoldli [0..<N] (λ_. True)(λv0 I0 :: (nat ⇒ node_state option). do {
v0 ← mop_bound_val (λ x. x < N) v0;
ASSERT (v0 ∈ E'⇧*``V0);
if ¬is_done_oimpl v0 I0 then do {
s ← initial_impl' E' v0 I0;
s← WHILEIT ((λ(p,D,pE). ∃vE. invar v0 (oGS_α I0) (p,D,pE,vE)) o GS_defs.α)
(λs. ¬path_is_empty_impl s)
(skeleton_inner_while_body2 E') s;
let (S,B,I,P) = open_GS s;
RETURN I
} else
RETURN I0
}) I;
RETURN r
}"
lemma skeleton_impl_nfoldli_refine: "skeleton_impl_nfoldli E ≤ ⇓ Id skeleton_impl"
unfolding skeleton_impl_nfoldli_def skeleton_impl_def open_GS_def mop_bound_val_def
apply (simp only: Refine_Basic.nres_monad_laws)
apply (refine_rcg LFOi_refine[where A=Id and R=Id])
apply refine_dref_type
apply (vc_solve (nopre) solve: asm_rl I_to_outer
simp: bounded_list_set_rel skeleton_inner_while_body_alt_def initial_impl_alt)
using reachable_bound by simp
lemma fold_am_custom_empty': "(let i = Map.empty in f i) = (let N'= (BCONST N N); i = op_am_custom_empty N' in f i)"
by simp
sepref_definition skeleton_impl_ll is "PR_CONST skeleton_impl_nfoldli" :: "E_assn⇧k →⇩a node_state.am_assn N"
unfolding skeleton_impl_nfoldli_def PR_CONST_def
unfolding fold_am_custom_empty' nfoldli_upt_by_while
apply (annot_snat_const "TYPE(size_T)")
apply sepref
done
concrete_definition (in -) skeleton_impl_ll' [llvm_code] is fr_graph_impl_loc.skeleton_impl_ll_def
lemmas [sepref_fr_rules] = skeleton_impl_ll.refine[unfolded skeleton_impl_ll'.refine[OF fr_graph_impl_loc_axioms]]
end
lemmas [llvm_code] = stack_nth_copy_def
concrete_definition list_graph_skeleton_impl[llvm_code] is skeleton_impl_ll'_def[of list_graph_succ_ll]