Theory Pairing_Heaps_Impl_LLVM

theory Pairing_Heaps_Impl_LLVM
  imports Pairing_Heap_LLVM.Pairing_Heaps_Impl IsaSAT_Literals_LLVM
begin

type_synonym hp_assn = ‹32 word ptr × 32 word ptr × 32 word ptr × 32 word ptr × 64 word ptr × 32 word›

definition hp_assn :: ‹_ ⇒ hp_assn ⇒ assn› where
  ‹hp_assn ≡ (IICF_Array.array_assn atom.option_assn ×⇩a
    IICF_Array.array_assn atom.option_assn ×⇩a
    IICF_Array.array_assn atom.option_assn ×⇩a
    IICF_Array.array_assn atom.option_assn ×⇩a
    IICF_Array.array_assn uint64_nat_assn ×⇩a atom.option_assn)›

sepref_def mop_hp_read_prev_imp_code
  is ‹uncurry mop_hp_read_prev_imp›
  :: ‹atom_assn⇧k *⇩a hp_assn⇧k →⇩a atom.option_assn›
  unfolding mop_hp_read_prev_imp_def hp_assn_def
  apply (rewrite at ‹_! ⌑› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_read_nxt_imp_code
  is ‹uncurry mop_hp_read_nxt_imp›
  :: ‹atom_assn⇧k *⇩a hp_assn⇧k →⇩a atom.option_assn›
  unfolding mop_hp_read_nxt_imp_def hp_assn_def
  apply (rewrite at ‹_! ⌑› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_read_parent_imp_code
  is ‹uncurry mop_hp_read_parent_imp›
  :: ‹atom_assn⇧k *⇩a hp_assn⇧k →⇩a atom.option_assn›
  unfolding mop_hp_read_parent_imp_def hp_assn_def
  apply (rewrite at ‹_! ⌑› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_read_child_imp_code
  is ‹uncurry mop_hp_read_child_imp›
  :: ‹atom_assn⇧k *⇩a hp_assn⇧k →⇩a atom.option_assn›
  unfolding mop_hp_read_child_imp_def hp_assn_def
  apply (rewrite at ‹_! ⌑› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_read_score_imp_code
  is ‹uncurry mop_hp_read_score_imp›
  :: ‹atom_assn⇧k *⇩a hp_assn⇧k →⇩a uint64_nat_assn›
  unfolding mop_hp_read_score_imp_def hp_assn_def
  apply (rewrite at ‹_! ⌑› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

lemma source_node_impl_alt_def:
  ‹source_node_impl = (λ(prevs, nxts, parents, children, scores,i). i)›
  by (auto intro!: ext)

sepref_def source_node_impl_code
  is ‹(RETURN o source_node_impl)›
  :: ‹hp_assn⇧k →⇩a atom.option_assn›
  unfolding source_node_impl_alt_def hp_assn_def
  by sepref

lemma update_source_node_impl_alt_def:
  ‹update_source_node_impl = (λi (prevs, nxts, parents, children, scores,_). (prevs, nxts, parents, children, scores, i))›
  by (auto intro!: ext)

sepref_def update_source_node_impl_code
  is ‹uncurry (RETURN oo update_source_node_impl)›
  :: ‹atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding update_source_node_impl_alt_def hp_assn_def
  by sepref

sepref_def mop_hp_update_prev'_imp_code
  is ‹uncurry2 mop_hp_update_prev'_imp›
  :: ‹atom_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_hp_update_prev'_imp_def hp_assn_def
  apply (rewrite at ‹_[⌑:=_]› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ [⌑:=_]› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_update_child'_imp_code
  is ‹uncurry2 mop_hp_update_child'_imp›
  :: ‹atom_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_hp_update_child'_imp_def hp_assn_def
  apply (rewrite at ‹_[⌑:=_]› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ [⌑:=_]› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_update_nxt'_imp_code
  is ‹uncurry2 mop_hp_update_nxt'_imp›
  :: ‹atom_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_hp_update_nxt'_imp_def hp_assn_def
  apply (rewrite at ‹_[⌑:=_]› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ [⌑:=_]› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_update_parent'_imp_code
  is ‹uncurry2 mop_hp_update_parent'_imp›
  :: ‹atom_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_hp_update_parent'_imp_def hp_assn_def
  apply (rewrite at ‹_[⌑:=_]› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ [⌑:=_]› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_def mop_hp_set_all_imp_code
  is ‹uncurry6 mop_hp_set_all_imp›
  ::  ‹atom_assn⇧k *⇩a atom.option_assn⇧k *⇩a atom.option_assn⇧k *⇩a atom.option_assn⇧k *⇩a atom.option_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_hp_set_all_imp_def hp_assn_def
  apply (rewrite at ‹_[⌑:=_]› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ [⌑:=_]› annot_unat_snat_upcast[where 'l=‹64›])
  apply (rewrite at ‹(_, _[⌑:=_], _)› value_of_atm_def[symmetric])
  apply (rewrite in ‹(_, _ [⌑:=_],_)› annot_unat_snat_upcast[where 'l=‹64›])
  apply (rewrite at ‹(_, _, _[⌑:=_], _)› value_of_atm_def[symmetric])
  apply (rewrite in ‹(_, _, _ [⌑:=_],_)› annot_unat_snat_upcast[where 'l=‹64›])
  apply (rewrite at ‹(_, _, _, _[⌑:=_], _)› value_of_atm_def[symmetric])
  apply (rewrite in ‹(_, _, _, _ [⌑:=_],_)› annot_unat_snat_upcast[where 'l=‹64›])
  apply (rewrite at ‹(_, _, _, _, _[⌑:=_], _)› value_of_atm_def[symmetric])
  apply (rewrite in ‹(_, _, _, _, _ [⌑:=_],_)› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref

sepref_register mop_hp_set_all_imp
  mop_hp_update_parent'_imp mop_hp_update_nxt'_imp mop_hp_update_child'_imp mop_hp_update_prev'_imp
  mop_hp_read_score_imp mop_hp_read_nxt_imp mop_hp_read_prev_imp mop_hp_read_parent_imp mop_hp_read_child_imp
  maybe_mop_hp_update_prev'_imp maybe_mop_hp_update_nxt'_imp maybe_mop_hp_update_child'_imp maybe_mop_hp_update_parent'_imp


sepref_def mop_hp_insert_impl_code
  is ‹uncurry2 mop_hp_insert_impl›
  :: ‹atom_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_hp_insert_impl_def
    atom.fold_option
  by sepref

sepref_def maybe_mop_hp_update_prev'_imp_code
  is ‹uncurry2 maybe_mop_hp_update_prev'_imp›
  :: ‹atom.option_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding maybe_mop_hp_update_prev'_imp_def
    atom.fold_option
  by sepref

sepref_def maybe_mop_hp_update_nxt'_imp_code
  is ‹uncurry2 maybe_mop_hp_update_nxt'_imp›
  :: ‹atom.option_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding maybe_mop_hp_update_nxt'_imp_def
    atom.fold_option
  by sepref

sepref_def maybe_mop_hp_update_child'_imp_code
  is ‹uncurry2 maybe_mop_hp_update_child'_imp›
  :: ‹atom.option_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding maybe_mop_hp_update_child'_imp_def
    atom.fold_option
  by sepref

sepref_def maybe_mop_hp_update_parent'_imp_code
  is ‹uncurry2 maybe_mop_hp_update_parent'_imp›
  :: ‹atom.option_assn⇧k *⇩a atom.option_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding maybe_mop_hp_update_parent'_imp_def
    atom.fold_option
  by sepref

sepref_def mop_hp_link_imp_impl
  is ‹uncurry2 mop_hp_link_imp›
  :: ‹atom_assn⇧k *⇩a atom_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn ×⇩a atom_assn›
  unfolding mop_hp_link_imp_def
    atom.fold_option
  by sepref

sepref_register mop_hp_link_imp mop_vsids_pass⇩1_imp  mop_vsids_pass⇩2_imp mop_merge_pairs_imp
  mop_vsids_pop_min_impl mop_unroot_hp_tree

sepref_def mop_vsids_pass⇩1_imp_code
  is ‹uncurry mop_vsids_pass⇩1_imp›
  :: ‹hp_assn⇧d *⇩a atom_assn⇧k →⇩a hp_assn ×⇩a atom_assn›
  unfolding mop_vsids_pass⇩1_imp_def
    atom.fold_option
  by sepref

sepref_def mop_vsids_pass⇩2_imp_code
  is ‹uncurry mop_vsids_pass⇩2_imp›
  :: ‹hp_assn⇧d *⇩a atom_assn⇧k →⇩a hp_assn›
  unfolding mop_vsids_pass⇩2_imp_def
    atom.fold_option
  by sepref

sepref_def mop_merge_pairs_imp_code
  is ‹uncurry mop_merge_pairs_imp›
  :: ‹hp_assn⇧d *⇩a atom_assn⇧k →⇩a hp_assn›
  unfolding mop_merge_pairs_imp_def
  by sepref

sepref_def mop_vsids_pop_min_impl_code
  is mop_vsids_pop_min_impl
  :: ‹hp_assn⇧d →⇩a atom.option_assn ×⇩a hp_assn›
  unfolding mop_vsids_pop_min_impl_def
    atom.fold_option
  by sepref


definition mop_source_node_impl where
  "mop_source_node_impl = RETURN o source_node_impl"
sepref_register mop_source_node_impl

sepref_def mop_source_node_impl_code
  is mop_source_node_impl
  :: ‹hp_assn⇧k →⇩a atom.option_assn›
  unfolding mop_source_node_impl_def
  by sepref

sepref_register
  "source_node_impl :: (nat,nat)pairing_heaps_imp ⇒ _"

hide_const (open) NEMonad.ASSERT NEMonad.RETURN NEMonad.SPEC
lemma mop_unroot_hp_tree_alt_def:
  ‹mop_unroot_hp_tree arr h = do {
    a ← mop_source_node_impl arr;
    nnext ← mop_hp_read_nxt_imp h arr;
    parent ← mop_hp_read_parent_imp h arr;
    prev ← mop_hp_read_prev_imp h arr;
    if prev = None ∧ parent = None ∧ ¬(a ≠ None ∧ the a = h) then RETURN (update_source_node_impl None arr)
    else if a ≠ None ∧ the a = h then RETURN (update_source_node_impl None arr)
    else do {
      ASSERT (a ≠ None);
      let a' = the a;
      arr ←  maybe_mop_hp_update_child'_imp parent nnext arr;
      arr ←  maybe_mop_hp_update_nxt'_imp prev nnext arr;
      arr ←  maybe_mop_hp_update_prev'_imp nnext prev arr;
      arr ←  maybe_mop_hp_update_parent'_imp nnext parent arr;

      arr ←  mop_hp_update_nxt'_imp h None arr;
      arr ←  mop_hp_update_prev'_imp h None arr;
      arr ←  mop_hp_update_parent'_imp h None arr;

      arr ←  mop_hp_update_nxt'_imp h (Some a') arr;
      arr ←  mop_hp_update_prev'_imp a' (Some h) arr;
      RETURN (update_source_node_impl None arr)
    }
}›
   unfolding mop_unroot_hp_tree_def mop_source_node_impl_def
   by (cases ‹source_node_impl arr›)
    (auto intro!: bind_cong[OF refl] simp: Let_def)

sepref_def mop_unroot_hp_tree_code
  is ‹uncurry (mop_unroot_hp_tree :: (nat,nat)pairing_heaps_imp ⇒ _)›
  :: ‹hp_assn⇧d *⇩a atom_assn⇧k →⇩a hp_assn›
  unfolding mop_unroot_hp_tree_alt_def
    atom.fold_option short_circuit_conv
  by sepref

sepref_def mop_hp_update_score_imp_code
  is ‹uncurry2 mop_hp_update_score_imp›
  :: ‹atom_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_hp_update_score_imp_def hp_assn_def
  apply (rewrite at ‹_[⌑:=_]› value_of_atm_def[symmetric])
  apply (rewrite in ‹_ [⌑:=_]› annot_unat_snat_upcast[where 'l=‹64›])
  by sepref


lemma Some_eq_not_None_sepref_id_work_around: ‹Some h = a ⟷ (a ≠ None ∧ h = the a)›
  by (cases a) auto

sepref_def mop_rescale_and_reroot_code
  is ‹uncurry2 mop_rescale_and_reroot›
  :: ‹atom_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a hp_assn⇧d →⇩a hp_assn›
  unfolding mop_rescale_and_reroot_def Some_eq_not_None_sepref_id_work_around
  unfolding atom.fold_option short_circuit_conv
  by sepref

sepref_def mop_hp_is_in_code
  is ‹uncurry mop_hp_is_in›
  :: ‹atom_assn⇧k *⇩a hp_assn⇧k →⇩a bool1_assn›
  unfolding mop_hp_is_in_def Some_eq_not_None_sepref_id_work_around
  unfolding atom.fold_option short_circuit_conv
  by sepref

sepref_def mop_vsids_pop_min2_impl_code
  is mop_vsids_pop_min2_impl
  :: ‹hp_assn⇧d →⇩a atom_assn ×⇩a hp_assn›
  unfolding mop_vsids_pop_min2_impl_def
  unfolding atom.fold_option
  by sepref

lemma mop_hp_insert_impl_spec2:
  ‹(uncurry2 mop_hp_insert_impl, uncurry2 hp_insert) ∈
    nat_rel ×⇩f nat_rel ×⇩f ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel →⇩f
    ⟨⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel⟩nres_rel›
  by (intro frefI nres_relI) (auto intro!: mop_hp_insert_impl_spec[THEN order_trans])

lemma mop_rescale_and_reroot_spec2:
   ‹(uncurry2 mop_rescale_and_reroot, uncurry2 rescale_and_reroot) ∈
    nat_rel ×⇩f nat_rel ×⇩f  ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel →⇩f
    ⟨⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel⟩nres_rel›
  by (intro frefI nres_relI) (auto intro!: mop_rescale_and_reroot_spec[THEN order_trans])

lemma rescale_and_reroot_mop_prio_change_weight2:
  ‹(uncurry2 rescale_and_reroot, uncurry2 (PR_CONST ACIDS.mop_prio_change_weight)) ∈
  nat_rel ×⇩f  nat_rel ×⇩f acids_encoded_hmrel →⇩f ⟨acids_encoded_hmrel⟩nres_rel›
  by (intro frefI nres_relI)
   (auto intro!: rescale_and_reroot_mop_prio_change_weight[THEN order_trans])

lemma mop_hp_is_in_spec2:
  ‹(uncurry mop_hp_is_in, uncurry hp_is_in) ∈ nat_rel ×⇩f ⟨⟨nat_rel⟩option_rel, ⟨nat_rel⟩option_rel⟩pairing_heaps_rel →⇩f ⟨bool_rel⟩nres_rel›
  by (intro frefI nres_relI)
   (auto intro!: mop_hp_is_in_spec[THEN order_trans])

lemma vsids_pop_min2_mop_prio_pop_min2:
  ‹(vsids_pop_min2, PR_CONST ACIDS.mop_prio_pop_min) ∈ acids_encoded_hmrel →⇩f ⟨nat_rel ×⇩r acids_encoded_hmrel⟩nres_rel›
  by (intro frefI nres_relI)
   (auto intro!: vsids_pop_min2_mop_prio_pop_min[THEN order_trans])

lemma mop_vsids_pop_min2_impl2:
  shows ‹(mop_vsids_pop_min2_impl, vsids_pop_min2) ∈
    ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel →⇩f
    ⟨nat_rel ×⇩r ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel⟩nres_rel›
  by (intro frefI nres_relI)
   (auto intro!: mop_vsids_pop_min2_impl[THEN order_trans])

lemma mop_hp_read_score_imp_mop_hp_read_score2:
  ‹(uncurry mop_hp_read_score_imp, uncurry mop_hp_read_score) ∈
  Id ×⇩f ⟨⟨nat_rel⟩option_rel,⟨nat_rel⟩option_rel⟩pairing_heaps_rel →⇩f ⟨nat_rel⟩nres_rel›
  by (intro frefI nres_relI)
   (auto intro!: mop_hp_read_score_imp_mop_hp_read_score[THEN order_trans])


thm mop_hp_read_score_imp_mop_hp_read_score
definition acids_assn :: ‹_› where
  ‹acids_assn = hr_comp (hr_comp hp_assn (⟨⟨nat_rel⟩option_rel, ⟨nat_rel⟩option_rel⟩pairing_heaps_rel))
              acids_encoded_hmrel›

lemmas [fcomp_norm_unfold] = acids_assn_def[symmetric]

sepref_register ACIDS.mop_prio_change_weight ACIDS.mop_prio_insert
  ACIDS.mop_prio_pop_min ACIDS.mop_prio_is_in

lemmas [sepref_fr_rules] =
  mop_hp_insert_impl_code.refine[FCOMP mop_hp_insert_impl_spec2, FCOMP hp_insert_spec_mop_prio_insert2]
  mop_rescale_and_reroot_code.refine[FCOMP mop_rescale_and_reroot_spec2, FCOMP rescale_and_reroot_mop_prio_change_weight2]
  mop_hp_is_in_code.refine[FCOMP mop_hp_is_in_spec2, FCOMP hp_is_in_mop_prio_is_in2]
  mop_vsids_pop_min2_impl_code.refine[FCOMP mop_vsids_pop_min2_impl2, FCOMP vsids_pop_min2_mop_prio_pop_min2]
  mop_hp_read_score_imp_code.refine[FCOMP mop_hp_read_score_imp_mop_hp_read_score2, FCOMP mop_hp_read_score_mop_prio_old_weight2]

end