Theory Relabel_To_Front_Impl

section ‹Implementation of Relabel-to-Front›
theory Relabel_To_Front_Impl
imports
  Relabel_To_Front
  Prpu_Common_Impl
begin
  
  
subsection ‹Basic Operations›  
  
context Network_Impl
begin
  
subsubsection ‹Neighbor Lists›
definition n_init :: "(node  node list)  (node  node list) nres" 
  where "n_init am  return (am( s := [], t := []) )"
  
definition n_at_end :: "(node  node list)  node  bool nres" 
  where "n_at_end n u  do {
    assert (uV-{s,t});
    return (n u = [])
  }"
    
definition n_get_hd :: "(node  node list)  node  node nres"    
  where "n_get_hd n u  do {
    assert (uV-{s,t}  n u  []);
    return (hd (n u))
  }"

definition n_move_next 
  :: "(node  node list)  node  (node  node list) nres"
  where "n_move_next n u  do {
    assert (uV-{s,t}  n u  []);
    return (n (u := tl (n u)))
  }"
    
definition n_reset 
  :: "(node  node list)  (node  node list)  node 
     (node  node list) nres"
  where "n_reset am n u  do {
    assert (uV-{s,t});
    return (n (u := am u))
  }"
  
lemma n_init_refine[refine2]: 
  assumes AM: "is_adj_map am"  
  shows "n_init am 
     (spec c. (c, rtf_init_n)  (nat_rel  nat_rellist_set_rel))"
proof -
  have[simp]: "am v = []" if "vV" for v
  proof -
    from that have "adjacent_nodes v = {}" 
      unfolding adjacent_nodes_def using E_ss_VxV by auto
    thus ?thesis using am_to_adj_nodes_refine[OF AM] 
      by (auto simp: list_set_rel_def in_br_conv)
  qed
  show ?thesis      
    unfolding n_init_def rtf_init_n_def 
    by (auto 
        simp: pw_le_iff refine_pw_simps list_set_autoref_empty 
        simp: am_to_adj_nodes_refine[OF AM])
qed  
  
subsection ‹Refinement to Basic Operations›  
  
subsubsection ‹Discharge›  
definition "discharge2 am x cf l n u  do {  
  assert (u  V);
  monadic_WHILEIT (λ_. True) 
    (λ((x,cf),l,n). do { xu  x_get x u; return (xu  0) } ) 
    (λ((x,cf),l,n). do {
      at_end  n_at_end n u;
      if at_end then do {
        l  relabel2 am cf l u;
        n  n_reset am n u;
        return ((x,cf),l,n)
      } else do {
        v  n_get_hd n u;
        cfuv  cf_get cf (u,v);
        lu  l_get l u;
        lv  l_get l v;
        if (cfuv  0  lu = lv + 1) then do {
          (x,cf)  push2 x cf (u,v);
          return ((x,cf),l,n)
        } else do {
          n  n_move_next n u;
          return ((x,cf),l,n)
        }
      }
    }) ((x,cf),l,n)
}"

lemma discharge_structure_refine_aux:
  assumes SR: "(ni,n)nat_rel  nat_rellist_set_rel"
  assumes SU: "(ui,u)Id"  
  assumes fNR: "fNi  R fN"
  assumes UIV: "uV-{s,t}"  
  assumes fSR: "v vi vs.  
      (vi,v)Id; vn u; ni u = v#vs; (v#vs,n u)nat_rellist_set_rel 
      fSi vi  R (fS v)"
  shows
  "( do {
    at_end  n_at_end ni ui;
    if at_end then fNi
    else do {
      v  n_get_hd ni ui;
      fSi v
    }
  } )  R (

  do {
    v  select v. vn u;
    case v of
      None  fN
    | Some v  fS v
  })" (is "?lhs R ?rhs")
  unfolding n_at_end_def n_get_hd_def
  apply (simp only: nres_monad_laws)  
  apply (cases "ni u")
  subgoal
    using fun_relD[OF SR SU] SU UIV fNR
    by (auto simp: list_set_rel_def in_br_conv pw_le_iff refine_pw_simps)
    
  subgoal for v vs
    using fun_relD[OF SR SU] SU UIV
    using fSR[OF IdI[of v], of vs]  
    apply (clarsimp 
        simp: list_set_rel_def in_br_conv pw_le_iff refine_pw_simps 
        split: option.splits)
    by fastforce  
  done    
  
lemma xf_rel_RELATES[refine_dref_RELATES]: "RELATES xf_rel" 
  by (auto simp: RELATES_def)
  
lemma discharge2_refine[refine]:     
  assumes A: "((x,cf),f)  xf_rel"
  assumes AM: "(am,adjacent_nodes)nat_relnat_rellist_set_rel"
  assumes [simplified,simp]: "(li,l)Id" "(ui,u)Id"
  assumes NR: "(ni,n)nat_rel  nat_rellist_set_rel"  
  shows "discharge2 am x cf li ni ui 
     (xf_rel ×r Id ×r (nat_rel  nat_rellist_set_rel)) (discharge f l n u)"  
  unfolding discharge2_def discharge_def
  apply (rewrite in "monadic_WHILEIT _ _  _" vcg_intro_frame)  
  apply refine_rcg  
  apply (vc_solve simp: A NR)
  subgoal by (simp add: xf_rel_def x_get_def)  
  subgoal for f l n x cf ni   
    apply (subst vcg_rem_frame)
    unfolding n_reset_def cf_get_def l_get_def n_move_next_def  
    apply (simp only: nres_monad_laws)  
    apply (rule discharge_structure_refine_aux; (refine_vcg AM)?; (assumption)?)  
    apply (vc_solve simp: fun_relD fun_relD[OF AM])  
    subgoal for v vs unfolding xf_rel_def Graph.E_def by auto
    subgoal for v vs by (auto simp: list_set_rel_def in_br_conv)  
    done
  done
  
subsubsection ‹ Initialization of Queue ›
    
lemma V_is_adj_nodes: "V = { v . adjacent_nodes v  {} }"
  unfolding V_def adjacent_nodes_def by auto
    
definition "init_CQ am  do {
  let cardV=0;
  let Q=[];
  nfoldli [0..<N] (λ_. True) (λv (cardV,Q). do {
    assert (v<N);
    inV  am_is_in_V am v;
    if inV then do {
      let cardV = cardV + 1;
      if vs  vt then
        return (cardV,v#Q)
      else 
        return (cardV,Q)
    } else
      return (cardV,Q)
  }) (cardV,Q)
}"    

lemma init_CQ_correct[THEN order_trans, refine_vcg]:
  assumes AM: "is_adj_map am"  
  shows "init_CQ am  SPEC (λ(C,Q). C = card V  distinct Q  set Q = V-{s,t})"
  unfolding init_CQ_def  
  apply (refine_vcg 
      nfoldli_rule[where 
        I="λl1 _ (C,Q). 
             C = card (Vset l1)  distinct Q  set Q = (Vset l1)-{s,t} "]
      )  
  apply (clarsimp_all simp: am_to_adj_nodes_refine[OF AM])
  using V_ss by (auto simp: upt_eq_lel_conv Int_absorb2)
    
subsubsection ‹Main Algorithm›    
    
definition "relabel_to_front2 am  do {
  (cardV, L_right)  init_CQ am;

  xcf  pp_init_xcf2 am;
  l  l_init cardV;
  n  n_init am;

  let L_left=[];

  ((x,cf),l,n,L_left,L_right)  whileT 
    (λ((x,cf),l,n,L_left,L_right). L_right  []) 
    (λ((x,cf),l,n,L_left,L_right). do {
      assert (L_right  []);
      let u = hd L_right;
      old_lu  l_get l u;
  
      ((x,cf),l,n)  discharge2 am x cf l n u;
  
      lu  l_get l u;
      if (lu  old_lu) then do {
        ― ‹Move u› to front of l›, and restart scanning L›. The cost for›
        ― ‹rev_append› is amortized by going to next node in L›
        let (L_left,L_right) = ([u],rev_append L_left (tl L_right));
        return ((x,cf),l,n,L_left,L_right)
      } else do {
        ― ‹Goto next node in L›
        let (L_left,L_right) = (u#L_left, tl L_right);
        return ((x,cf),l,n,L_left,L_right)
      }
  
    }) (xcf,l,n,L_left,L_right);

  return cf
}"
  
    
lemma relabel_to_front2_refine[refine]: 
  assumes AM: "is_adj_map am"  
  shows "relabel_to_front2 am 
     (br (flow_of_cf) (RPreGraph c s t)) relabel_to_front"
proof -
  define s_rel 
    :: "( _ × (
       capacity_impl flow 
    × (natnat) 
    × (nodenode set) 
    × node list 
    × node list)) set"
    where "s_rel  
       xf_rel 
    ×r Id 
    ×r (nat_rel  nat_rellist_set_rel) 
    ×r br rev (λ_. True) 
    ×r Id"
  
  have [refine_dref_RELATES]: "RELATES s_rel" unfolding RELATES_def ..
      
  {
    fix f l n
    assume "neighbor_invar c s t f l n"
    then interpret neighbor_invar c s t f l n .  
    have G1: "flow_of_cf cf = f" by (rule fo_rg_inv)
    have G2: "RPreGraph c s t cf" by (rule is_RPreGraph)
    note G1 G2    
  } note AUX1=this   
      
  have AUXR: "do {
      (cardV, L_right)  init_CQ am;
      xcf  pp_init_xcf2 am;
      l  l_init cardV;
      n  n_init am;
      Fi L_right xcf l n
    }
     R (do {
      L_right  spec l. distinct l  set l = V - {s, t};
      F L_right
    })
  " 
  if "L_right xcf n. 
     (xcf,pp_init_f)xf_rel; (n,rtf_init_n)  nat_rel  nat_rellist_set_rel 
     Fi L_right xcf pp_init_l n  R (F L_right)"
  for Fi F R
    unfolding l_init_def
    apply (rule refine2specI)
    supply pp_init_xcf2_refine
            [OF AM, unfolded conc_fun_RETURN, THEN order_trans, refine_vcg]  
    supply n_init_refine[OF AM,THEN order_trans, refine_vcg]  
    apply (refine_vcg AM V_ss)
    apply clarsimp  
    subgoal for L_right x cf n
      using that[of "(x,cf)" n L_right]
      unfolding pp_init_l_def  
      by (clarsimp simp: pw_le_iff refine_pw_simps; meson)  
    done  
  show ?thesis
    unfolding relabel_to_front2_def relabel_to_front_def Let_def l_get_def
    apply (simp only: nres_monad_laws)  
    apply (rule AUXR)  
    apply (refine_rcg)
    apply refine_dref_type
    unfolding s_rel_def
    apply (vc_solve 
        simp: in_br_conv rev_append_eq xf_rel_def AUX1 fun_relD 
        simp: am_to_adj_nodes_refine[OF AM])
    done  
qed  
  
  
subsection ‹Refinement to Efficient Data Structures›  
  
context includes Network_Impl_Sepref_Register 
begin  
  sepref_register n_init  
  sepref_register n_at_end
  sepref_register n_get_hd
  sepref_register n_move_next
  sepref_register n_reset
  sepref_register discharge2
  sepref_register "init_CQ"
  sepref_register relabel_to_front2
end  
  
subsubsection ‹Neighbor Lists by Array of Lists›  
definition "n_assn  is_nf N ([]::nat list)"    
    
definition (in -) "n_init_impl s t am  do {
  n  array_copy am;
  n  Array.upd s [] n;
  n  Array.upd t [] n;
  return n
}"      
    
lemma [sepref_fr_rules]: 
  "(n_init_impl s t,PR_CONST n_init)  am_assnk a n_assn" 
  apply sepref_to_hoare
  unfolding am_assn_def n_assn_def n_init_impl_def n_init_def
  by (sep_auto)  
    
definition (in -) "n_at_end_impl n u  do {
  nu  Array.nth n u;
  return (is_Nil nu)
}"
    
lemma [sepref_fr_rules]: 
  "(uncurry n_at_end_impl, uncurry (PR_CONST n_at_end)) 
   n_assnk *a node_assnk a bool_assn"  
  apply sepref_to_hoare unfolding n_at_end_impl_def n_at_end_def n_assn_def
  by (sep_auto simp: refine_pw_simps split: list.split)
  
definition (in -) "n_get_hd_impl n u  do {
  nu  Array.nth n u;
  return (hd nu)
}"      
lemma [sepref_fr_rules]: 
  "(uncurry n_get_hd_impl, uncurry (PR_CONST n_get_hd)) 
   n_assnk *a node_assnk a node_assn"  
  apply sepref_to_hoare unfolding n_get_hd_impl_def n_get_hd_def n_assn_def
  by (sep_auto simp: refine_pw_simps)
  
definition (in -) "n_move_next_impl n u  do {
  nu  Array.nth n u;
  n  Array.upd u (tl nu) n;
  return n
}" 
lemma [sepref_fr_rules]: 
  "(uncurry n_move_next_impl, uncurry (PR_CONST n_move_next)) 
   n_assnd *a node_assnk a n_assn"  
  apply sepref_to_hoare 
  unfolding n_move_next_impl_def n_move_next_def n_assn_def
  by (sep_auto simp: refine_pw_simps)
  
definition (in -) "n_reset_impl am n u  do {
  nu  Array.nth am u;
  n  Array.upd u nu n;
  return n
}"
lemma [sepref_fr_rules]: 
  "(uncurry2 n_reset_impl, uncurry2 (PR_CONST n_reset)) 
   am_assnk *a n_assnd *a node_assnk a n_assn"  
  apply sepref_to_hoare 
  unfolding n_reset_impl_def n_reset_def n_assn_def am_assn_def
  by (sep_auto simp: refine_pw_simps)
  
subsubsection ‹Discharge›  
sepref_thm discharge_impl is "uncurry5 (PR_CONST discharge2)" 
  :: "am_assnk *a x_assnd *a cf_assnd *a l_assnd *a n_assnd *a node_assnk 
    a (x_assn ×a cf_assn) ×a l_assn ×a n_assn"  
  unfolding discharge2_def PR_CONST_def
  by sepref  
concrete_definition (in -) discharge_impl 
  uses Network_Impl.discharge_impl.refine_raw is "(uncurry5 ?f,_)_"
lemmas [sepref_fr_rules] = discharge_impl.refine[OF Network_Impl_axioms]    

subsubsection ‹Initialization of Queue›  
  
sepref_thm init_CQ_impl is "(PR_CONST init_CQ)" 
  :: "am_assnk a nat_assn ×a list_assn nat_assn"
  unfolding init_CQ_def PR_CONST_def
  apply (rewrite HOL_list.fold_custom_empty)
  by sepref
concrete_definition (in -) init_CQ_impl 
  uses Network_Impl.init_CQ_impl.refine_raw is "(?f,_)_"
lemmas [sepref_fr_rules] = init_CQ_impl.refine[OF Network_Impl_axioms]    
  
subsubsection ‹Main Algorithm›  
sepref_thm relabel_to_front_impl is 
  "(PR_CONST relabel_to_front2)" :: "am_assnk a cf_assn"  
  unfolding relabel_to_front2_def PR_CONST_def
  supply [[goals_limit = 1]]  
  apply (rewrite in "Let [] _" HOL_list.fold_custom_empty)
  apply (rewrite in "[_]" HOL_list.fold_custom_empty)
  by sepref  
concrete_definition (in -) relabel_to_front_impl 
  uses Network_Impl.relabel_to_front_impl.refine_raw is "(?f,_)_"
lemmas [sepref_fr_rules] = relabel_to_front_impl.refine[OF Network_Impl_axioms]
  
end ― ‹Network Implementation Locale› 
  
export_code relabel_to_front_impl checking SML_imp
  
subsection ‹Combination with Network Checker and Correctness›  
context Network_Impl begin
  
  theorem relabel_to_front_impl_correct[sep_heap_rules]: 
    assumes AM: "is_adj_map am"
    shows "
      <am_assn am ami> 
        relabel_to_front_impl c s t N ami
      <λcfi. Acf. cf_assn cf cfi 
                * (isMaxFlow (flow_of_cf cf)  RGraph_Impl c s t N cf)>t"
  proof -
    note relabel_to_front2_refine[OF AM]    
    also note relabel_to_front_correct
    finally have R1: 
      "relabel_to_front2 am 
        (br flow_of_cf (RPreGraph c s t)) (SPEC isMaxFlow)" .  

    have [simp]: "nofail (R (RES X))" for R X by (auto simp: refine_pw_simps)
        
    note R2 = relabel_to_front_impl.refine[
      OF Network_Impl_axioms, to_hnr, unfolded autoref_tag_defs]
    note R3 = hn_refine_ref[OF R1 R2, of ami]  
    note R4 = R3[unfolded hn_ctxt_def pure_def, THEN hn_refineD, simplified]

    note RGII = rgraph_and_network_impl_imp_rgraph_impl[OF 
      RPreGraph.maxflow_imp_rgraph
      Network_Impl_axioms
        ]  
      
    show ?thesis  
      by (sep_auto heap: R4 simp: pw_le_iff refine_pw_simps in_br_conv RGII)
  qed
end    

definition "relabel_to_front_impl_tab_am c s t N am  do {
  ami  Array.make N am;  ― ‹TODO/DUP: Called init_ps› in Edmonds-Karp impl›
  relabel_to_front_impl c s t N ami
}"  
  
theorem relabel_to_front_impl_tab_am_correct[sep_heap_rules]: 
  assumes NW: "Network c s t"
  assumes VN: "Graph.V c  {0..<N}"
  assumes ABS_PS: "Graph.is_adj_map c am"
  shows "
    <emp> 
      relabel_to_front_impl_tab_am c s t N am
    <λcfi. Acf. 
        asmtx_assn N id_assn cf cfi 
      * (Network.isMaxFlow c s t (Network.flow_of_cf c cf)
         RGraph_Impl c s t N cf
        )>t"
proof -
  interpret Network c s t by fact
  interpret Network_Impl c s t N using VN by unfold_locales    
  
  from ABS_PS have [simp]: "am u = []" if "uN" for u
    unfolding is_adj_map_def
    using E_ss_VxV VN that 
    apply (subgoal_tac "uV") 
    by (auto simp del: inV_less_N)
  
  show ?thesis
    unfolding relabel_to_front_impl_tab_am_def 
    apply vcg
    apply (rule 
        Hoare_Triple.cons_rule[OF _ _ relabel_to_front_impl_correct[OF ABS_PS]])
    subgoal unfolding am_assn_def is_nf_def by sep_auto
    subgoal unfolding cf_assn_def by sep_auto
    done  
qed        
  
definition "relabel_to_front el s t  do {
  case prepareNet el s t of
    None  return None
  | Some (c,am,N)  do {
      cf  relabel_to_front_impl_tab_am c s t N am;
      return (Some (c,am,N,cf))
  }
}"
export_code relabel_to_front checking SML_imp

text ‹
  Main correctness statement:
   If relabel_to_front› returns None›, the edge list was invalid or described 
    an invalid network. 
   If it returns Some (c,am,N,cfi)›, then the edge list is valid and describes
    a valid network. Moreover, cfi› is an integer square matrix of 
    dimension N›, which describes a valid residual graph in the network, whose
    corresponding flow is maximal. Finally, am› is a valid adjacency map of the
    graph, and the nodes of the graph are integers less than N›.
›  
theorem relabel_to_front_correct:
  "<emp>
  relabel_to_front el s t
  <λ
    None  (¬ln_invar el  ¬Network (ln_α el) s t)
  | Some (c,am,N,cfi)  
      (c = ln_α el  ln_invar el) 
    * (Acf. asmtx_assn N int_assn cf cfi
          * (RGraph_Impl c s t N cf 
             Network.isMaxFlow c s t (Network.flow_of_cf c cf))) 
    * (Graph.is_adj_map c am)
  >t
  "
  unfolding relabel_to_front_def
  using prepareNet_correct[of el s t]
  by (sep_auto simp: ln_rel_def in_br_conv)
  

end