Theory IsaSAT_Arena_Sorting_LLVM

theory IsaSAT_Arena_Sorting_LLVM
  imports IsaSAT_Sorting_LLVM IsaSAT_Arena_LLVM
begin

type_synonym vdom_fast_assn = ‹64 word array_list64›
abbreviation vdom_fast_assn :: ‹vdom ⇒ vdom_fast_assn ⇒ assn› where
  ‹vdom_fast_assn ≡ arl64_assn sint64_nat_assn›

sepref_def delete_index_and_swap_code2
  is ‹uncurry (RETURN oo delete_index_and_swap)›
  :: ‹[λ(xs, i). i < length xs]⇩a
      vdom_fast_assn⇧d *⇩a sint64_nat_assn⇧k → vdom_fast_assn›
  unfolding delete_index_and_swap.simps
  by sepref

definition idx_cdom :: ‹arena ⇒ nat set› where
 ‹idx_cdom arena ≡ {i. valid_sort_clause_score_pre_at arena i}›

sepref_register clause_score_extract arena_status arena_lbd unat32_max DELETED

lemma valid_sort_clause_score_pre_at_alt_def:
  ‹valid_sort_clause_score_pre_at arena C ⟷
    (∃i vdom. C = vdom ! i ∧ arena_is_valid_clause_vdom arena (vdom!i) ∧
          (arena_status arena (vdom!i) ≠ DELETED ⟶
            ((get_clause_LBD_pre arena (vdom!i) ∧ arena_act_pre arena (vdom!i)) ∧
            arena_is_valid_clause_idx arena C))
          ∧ i < length vdom)›
  unfolding valid_sort_clause_score_pre_at_def arena_is_valid_clause_idx_def
     arena_act_pre_def arena_is_valid_clause_idx_def by auto

sepref_def (in -) clause_score_extract_code
  is ‹uncurry (RETURN oo clause_score_extract)›
  :: ‹[uncurry valid_sort_clause_score_pre_at]⇩a
      arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → uint32_nat_assn ×⇩a sint64_nat_assn ×⇩a sint64_nat_assn›
  supply [[goals_limit = 1]]
  unfolding clause_score_extract_def valid_sort_clause_score_pre_at_alt_def unat64_max_def[simplified]
  by sepref

sepref_def (in -) clause_score_ordering_code
  is ‹uncurry (RETURN oo clause_score_ordering)›
  :: ‹(uint32_nat_assn ×⇩a sint64_nat_assn ×⇩a sint64_nat_assn)⇧k *⇩a (uint32_nat_assn ×⇩a sint64_nat_assn ×⇩a sint64_nat_assn)⇧k →⇩a bool1_assn›
  supply [[goals_limit = 1]]
  unfolding clause_score_ordering_def
  by sepref

sepref_register mop_clause_score_less clause_score_less clause_score_ordering
sepref_def mop_clause_score_less_impl
  is ‹uncurry2 mop_clause_score_less›
  :: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a bool1_assn›
  unfolding mop_clause_score_less_def
  by sepref


interpretation LBD: weak_ordering_on_lt where
  C = ‹idx_cdom vs› and
  less = ‹clause_score_less vs›
  by unfold_locales
   (auto simp: clause_score_less_def clause_score_extract_def
      clause_score_ordering_def split: if_splits)

interpretation LBD: parameterized_weak_ordering idx_cdom clause_score_less
    mop_clause_score_less
  by unfold_locales
   (auto simp: mop_clause_score_less_def
     idx_cdom_def clause_score_less_def)

global_interpretation LBD: parameterized_sort_impl_context
  ‹woarray_assn snat_assn› ‹eoarray_assn snat_assn› snat_assn
  Mreturn Mreturn
  eo_extract_impl
  array_upd
  idx_cdom clause_score_less mop_clause_score_less mop_clause_score_less_impl
  ‹arena_fast_assn›
  defines
          LBD_is_guarded_insert_impl = LBD.is_guarded_param_insert_impl
      and LBD_is_unguarded_insert_impl = LBD.is_unguarded_param_insert_impl
      and LBD_unguarded_insertion_sort_impl = LBD.unguarded_insertion_sort_param_impl
      and LBD_guarded_insertion_sort_impl = LBD.guarded_insertion_sort_param_impl
      and LBD_final_insertion_sort_impl = LBD.final_insertion_sort_param_impl
      (*and LBD_mop_lchild_impl  = LBD.mop_lchild_impl
      and LBD_mop_rchild_impl  = LBD.mop_rchild_impl
      and LBD_has_rchild_impl  = LBD.has_rchild_impl
      and LBD_has_lchild_impl  = LBD.has_lchild_impl *)

      and LBD_pcmpo_idxs_impl  = LBD.pcmpo_idxs_impl
      and LBD_pcmpo_v_idx_impl  = LBD.pcmpo_v_idx_impl
      and LBD_pcmpo_idx_v_impl  = LBD.pcmpo_idx_v_impl
      and LBD_pcmp_idxs_impl  = LBD.pcmp_idxs_impl

      and LBD_mop_geth_impl    = LBD.mop_geth_impl
      and LBD_mop_seth_impl    = LBD.mop_seth_impl
      and LBD_sift_down_impl   = LBD.sift_down_impl
      and LBD_heapify_btu_impl = LBD.heapify_btu_impl
      and LBD_heapsort_impl    = LBD.heapsort_param_impl
      and LBD_qsp_next_l_impl       = LBD.qsp_next_l_impl
      and LBD_qsp_next_h_impl       = LBD.qsp_next_h_impl
      and LBD_qs_partition_impl     = LBD.qs_partition_impl
(*      and LBD_qs_partitionXXX_impl     = LBD.qs_partitionXXX_impl *)
      and LBD_partition_pivot_impl  = LBD.partition_pivot_impl
      and LBD_introsort_aux_impl = LBD.introsort_aux_param_impl
      and LBD_introsort_impl        = LBD.introsort_param_impl
      and LBD_move_median_to_first_impl = LBD.move_median_to_first_param_impl

  apply unfold_locales
  apply (rule eo_hnr_dep)+
  unfolding GEN_ALGO_def refines_param_relp_def (* TODO: thm gen_refines_param_relpI *)
  by (rule mop_clause_score_less_impl.refine)


global_interpretation
  LBD_it: pure_eo_adapter sint64_nat_assn vdom_fast_assn arl_nth arl_upd
  defines LBD_it_eo_extract_impl = LBD_it.eo_extract_impl
  apply (rule al_pure_eo)
  by simp



global_interpretation LBD_it: parameterized_sort_impl_context
  vdom_fast_assn ‹LBD_it.eo_assn› sint64_nat_assn
  Mreturn Mreturn
  LBD_it_eo_extract_impl
  arl_upd
  idx_cdom clause_score_less mop_clause_score_less mop_clause_score_less_impl
  ‹arena_fast_assn›
  defines
          LBD_it_is_guarded_insert_impl = LBD_it.is_guarded_param_insert_impl
      and LBD_it_is_unguarded_insert_impl = LBD_it.is_unguarded_param_insert_impl
      and LBD_it_unguarded_insertion_sort_impl = LBD_it.unguarded_insertion_sort_param_impl
      and LBD_it_guarded_insertion_sort_impl = LBD_it.guarded_insertion_sort_param_impl
      and LBD_it_final_insertion_sort_impl = LBD_it.final_insertion_sort_param_impl
      (*and LBD_it_mop_lchild_impl  = LBD_it.mop_lchild_impl
      and LBD_it_mop_rchild_impl  = LBD_it.mop_rchild_impl
      and LBD_it_has_rchild_impl  = LBD_it.has_rchild_impl
      and LBD_it_has_lchild_impl  = LBD_it.has_lchild_impl *)

      and LBD_it_pcmpo_idxs_impl  = LBD_it.pcmpo_idxs_impl
      and LBD_it_pcmpo_v_idx_impl  = LBD_it.pcmpo_v_idx_impl
      and LBD_it_pcmpo_idx_v_impl  = LBD_it.pcmpo_idx_v_impl
      and LBD_it_pcmp_idxs_impl  = LBD_it.pcmp_idxs_impl

      and LBD_it_mop_geth_impl    = LBD_it.mop_geth_impl
      and LBD_it_mop_seth_impl    = LBD_it.mop_seth_impl
      and LBD_it_sift_down_impl   = LBD_it.sift_down_impl
      and LBD_it_heapify_btu_impl = LBD_it.heapify_btu_impl
      and LBD_it_heapsort_impl    = LBD_it.heapsort_param_impl
      and LBD_it_qsp_next_l_impl       = LBD_it.qsp_next_l_impl
      and LBD_it_qsp_next_h_impl       = LBD_it.qsp_next_h_impl
      and LBD_it_qs_partition_impl     = LBD_it.qs_partition_impl
(*      and LBD_it_qs_partitionXXX_impl     = LBD_it.qs_partitionXXX_impl *)
      and LBD_it_partition_pivot_impl  = LBD_it.partition_pivot_impl
      and LBD_it_introsort_aux_impl = LBD_it.introsort_aux_param_impl
      and LBD_it_introsort_impl        = LBD_it.introsort_param_impl
      and LBD_it_move_median_to_first_impl = LBD_it.move_median_to_first_param_impl

  apply unfold_locales
  unfolding GEN_ALGO_def refines_param_relp_def (* TODO: thm gen_refines_param_relpI *)
  apply (rule mop_clause_score_less_impl.refine)
  done


definition idx_clause_cdom :: ‹arena ⇒ nat set› where
 ‹idx_clause_cdom arena ≡ {i. arena_is_valid_clause_idx arena i}›

sepref_def (in -) arena_length_code
  is ‹uncurry (RETURN oo arena_length)›
  :: ‹[uncurry arena_is_valid_clause_idx]⇩a
      arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k → sint64_nat_assn›
  supply [[goals_limit = 1]]
  unfolding clause_score_extract_def valid_sort_clause_score_pre_at_alt_def unat64_max_def[simplified]
  by sepref

sepref_def (in -) clause_size_ordering_code
  is ‹uncurry (RETURN oo (≤))›
  :: ‹(sint64_nat_assn)⇧k *⇩a (sint64_nat_assn)⇧k →⇩a bool1_assn›
  supply [[goals_limit = 1]]
  unfolding clause_score_ordering_def
  by sepref

definition clause_size_less where
  ‹clause_size_less arena i j = (arena_length arena i < arena_length arena j)›

definition mop_clause_size_less where
  ‹mop_clause_size_less arena i j = do {
    ASSERT(arena_is_valid_clause_idx arena i);
    ASSERT(arena_is_valid_clause_idx arena j);
    RETURN (clause_size_less arena i j)
  }›

sepref_def mop_clause_size_less_impl
  is ‹uncurry2 mop_clause_size_less›
  :: ‹arena_fast_assn⇧k *⇩a sint64_nat_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a bool1_assn›
  unfolding mop_clause_size_less_def clause_size_less_def
  by sepref


interpretation Size_Ordering: weak_ordering_on_lt where
  C = ‹idx_clause_cdom vs› and
  less = ‹clause_size_less vs›
  by unfold_locales
   (auto simp: clause_size_less_def clause_score_extract_def
      clause_score_ordering_def split: if_splits)

interpretation Size_Ordering: parameterized_weak_ordering idx_clause_cdom clause_size_less
    mop_clause_size_less
  by unfold_locales
   (auto simp: mop_clause_size_less_def
     idx_clause_cdom_def clause_size_less_def)

global_interpretation Size_Ordering: parameterized_sort_impl_context
  ‹woarray_assn snat_assn› ‹eoarray_assn snat_assn› snat_assn
  Mreturn Mreturn
  eo_extract_impl
  array_upd
  idx_clause_cdom clause_size_less mop_clause_size_less mop_clause_size_less_impl
  ‹arena_fast_assn›
  defines
          Size_Ordering_is_guarded_insert_impl = Size_Ordering.is_guarded_param_insert_impl
      and Size_Ordering_is_unguarded_insert_impl = Size_Ordering.is_unguarded_param_insert_impl
      and Size_Ordering_unguarded_insertion_sort_impl = Size_Ordering.unguarded_insertion_sort_param_impl
      and Size_Ordering_guarded_insertion_sort_impl = Size_Ordering.guarded_insertion_sort_param_impl
      and Size_Ordering_final_insertion_sort_impl = Size_Ordering.final_insertion_sort_param_impl
      (*and Size_Ordering_mop_lchild_impl  = Size_Ordering.mop_lchild_impl
      and Size_Ordering_mop_rchild_impl  = Size_Ordering.mop_rchild_impl
      and Size_Ordering_has_rchild_impl  = Size_Ordering.has_rchild_impl
      and Size_Ordering_has_lchild_impl  = Size_Ordering.has_lchild_impl *)

      and Size_Ordering_pcmpo_idxs_impl  = Size_Ordering.pcmpo_idxs_impl
      and Size_Ordering_pcmpo_v_idx_impl  = Size_Ordering.pcmpo_v_idx_impl
      and Size_Ordering_pcmpo_idx_v_impl  = Size_Ordering.pcmpo_idx_v_impl
      and Size_Ordering_pcmp_idxs_impl  = Size_Ordering.pcmp_idxs_impl

      and Size_Ordering_mop_geth_impl    = Size_Ordering.mop_geth_impl
      and Size_Ordering_mop_seth_impl    = Size_Ordering.mop_seth_impl
      and Size_Ordering_sift_down_impl   = Size_Ordering.sift_down_impl
      and Size_Ordering_heapify_btu_impl = Size_Ordering.heapify_btu_impl
      and Size_Ordering_heapsort_impl    = Size_Ordering.heapsort_param_impl
      and Size_Ordering_qsp_next_l_impl       = Size_Ordering.qsp_next_l_impl
      and Size_Ordering_qsp_next_h_impl       = Size_Ordering.qsp_next_h_impl
      and Size_Ordering_qs_partition_impl     = Size_Ordering.qs_partition_impl
(*      and Size_Ordering_qs_partitionXXX_impl     = Size_Ordering.qs_partitionXXX_impl *)
      and Size_Ordering_partition_pivot_impl  = Size_Ordering.partition_pivot_impl
      and Size_Ordering_introsort_aux_impl = Size_Ordering.introsort_aux_param_impl
      and Size_Ordering_introsort_impl        = Size_Ordering.introsort_param_impl
      and Size_Ordering_move_median_to_first_impl = Size_Ordering.move_median_to_first_param_impl

  apply unfold_locales
  unfolding GEN_ALGO_def refines_param_relp_def (* TODO: thm gen_refines_param_relpI *)
  by (rule mop_clause_size_less_impl.refine)

global_interpretation Size_Ordering_it: parameterized_sort_impl_context
  vdom_fast_assn ‹LBD_it.eo_assn› sint64_nat_assn
  Mreturn Mreturn
  LBD_it_eo_extract_impl
  arl_upd
  idx_clause_cdom clause_size_less mop_clause_size_less mop_clause_size_less_impl
  ‹arena_fast_assn›
  defines
          Size_Ordering_it_is_guarded_insert_impl = Size_Ordering_it.is_guarded_param_insert_impl
      and Size_Ordering_it_is_unguarded_insert_impl = Size_Ordering_it.is_unguarded_param_insert_impl
      and Size_Ordering_it_unguarded_insertion_sort_impl = Size_Ordering_it.unguarded_insertion_sort_param_impl
      and Size_Ordering_it_guarded_insertion_sort_impl = Size_Ordering_it.guarded_insertion_sort_param_impl
      and Size_Ordering_it_final_insertion_sort_impl = Size_Ordering_it.final_insertion_sort_param_impl
      (*and Size_Ordering_it_mop_lchild_impl  = Size_Ordering_it.mop_lchild_impl
      and Size_Ordering_it_mop_rchild_impl  = Size_Ordering_it.mop_rchild_impl
      and Size_Ordering_it_has_rchild_impl  = Size_Ordering_it.has_rchild_impl
      and Size_Ordering_it_has_lchild_impl  = Size_Ordering_it.has_lchild_impl *)

      and Size_Ordering_it_pcmpo_idxs_impl  = Size_Ordering_it.pcmpo_idxs_impl
      and Size_Ordering_it_pcmpo_v_idx_impl  = Size_Ordering_it.pcmpo_v_idx_impl
      and Size_Ordering_it_pcmpo_idx_v_impl  = Size_Ordering_it.pcmpo_idx_v_impl
      and Size_Ordering_it_pcmp_idxs_impl  = Size_Ordering_it.pcmp_idxs_impl

      and Size_Ordering_it_mop_geth_impl    = Size_Ordering_it.mop_geth_impl
      and Size_Ordering_it_mop_seth_impl    = Size_Ordering_it.mop_seth_impl
      and Size_Ordering_it_sift_down_impl   = Size_Ordering_it.sift_down_impl
      and Size_Ordering_it_heapify_btu_impl = Size_Ordering_it.heapify_btu_impl
      and Size_Ordering_it_heapsort_impl    = Size_Ordering_it.heapsort_param_impl
      and Size_Ordering_it_qsp_next_l_impl       = Size_Ordering_it.qsp_next_l_impl
      and Size_Ordering_it_qsp_next_h_impl       = Size_Ordering_it.qsp_next_h_impl
      and Size_Ordering_it_qs_partition_impl     = Size_Ordering_it.qs_partition_impl
(*      and Size_Ordering_it_qs_partitionXXX_impl     = Size_Ordering_it.qs_partitionXXX_impl *)
      and Size_Ordering_it_partition_pivot_impl  = Size_Ordering_it.partition_pivot_impl
      and Size_Ordering_it_introsort_aux_impl = Size_Ordering_it.introsort_aux_param_impl
      and Size_Ordering_it_introsort_impl        = Size_Ordering_it.introsort_param_impl
      and Size_Ordering_it_move_median_to_first_impl = Size_Ordering_it.move_median_to_first_param_impl

  apply unfold_locales
  unfolding GEN_ALGO_def refines_param_relp_def (* TODO: thm gen_refines_param_relpI *)
  apply (rule mop_clause_size_less_impl.refine)
  done



lemmas [llvm_inline] = LBD_it.eo_extract_impl_def[THEN meta_fun_cong, THEN meta_fun_cong]

export_llvm
  ‹LBD_heapsort_impl :: _ ⇒ _ ⇒ _›
  ‹LBD_introsort_impl :: _ ⇒ _ ⇒ _›
  ‹Size_Ordering_heapsort_impl :: _ ⇒ _ ⇒ _›
  ‹Size_Ordering_introsort_impl :: _ ⇒ _ ⇒ _›


type_synonym virtual_vdom_fast_assn = ‹64 word›
definition virtual_vdom_fast_assn :: ‹vdom ⇒ virtual_vdom_fast_assn ⇒ _› where
  ‹virtual_vdom_fast_assn = hr_comp sint64_nat_assn {(a,b). a= 0}›

definition qqq where ‹qqq xs _ = Mreturn xs›
lemmas [llvm_inline] = qqq_def

lemma [unfolded qqq_def, sepref_fr_rules]:
  ‹(uncurry (qqq), uncurry (RETURN oo op_list_append))
  ∈ virtual_vdom_fast_assn⇧k *⇩a sint64_nat_assn⇧k →⇩a virtual_vdom_fast_assn›
proof -
  have [iff]: ‹x = snat u ∧ snat_invar u ∧ x = 0 ⟷ x = 0 ∧ u= 0› for x u
    by (auto intro: snat_invar_0)
     (auto simp add: snat_eq_unat_aux2 unat_arith_simps(3))

  have [simp]: "⋀ns u. virtual_vdom_fast_assn (ns::nat list) (u) = ↑(u=0)"
    by (auto simp add: Sepref_Basic.pure_def virtual_vdom_fast_assn_def hr_comp_def snat_rel_def
      snat.rel_def br_def
      simp flip: import_param_3
      simp del: import_param_3)
     (auto simp: import_param_3 exists_eq_star_conv)

  have [simp]: ‹(∃x. (↑True ∧* ↑(x = a @ [b])) s) = □ s› for a b s
    by (auto simp: Exists_eq_simp, simp_all add: pure_true_conv) 
  show ?thesis
    unfolding qqq_def
    apply sepref_to_hoare
    by (vcg)
qed


definition empty_virtual_vdom :: ‹nat list› where
  ‹empty_virtual_vdom = []›

sepref_register empty_virtual_vdom
lemma [sepref_fr_rules]:
  ‹(uncurry0 (Mreturn 0), uncurry0 (RETURN empty_virtual_vdom))
  ∈ unit_assn⇧k →⇩a virtual_vdom_fast_assn›
proof -
  have [iff]: ‹x = snat u ∧ snat_invar u ∧ x = 0 ⟷ x = 0 ∧ u= 0› for x u
    by (auto intro: snat_invar_0)
     (auto simp add: snat_eq_unat_aux2 unat_arith_simps(3))

  have [simp]: "⋀ns u. virtual_vdom_fast_assn (ns::nat list) (u) = ↑(u=0)"
    by (auto simp add: Sepref_Basic.pure_def virtual_vdom_fast_assn_def hr_comp_def snat_rel_def
      snat.rel_def br_def
      simp flip: import_param_3
      simp del: import_param_3)
     (auto simp: import_param_3 exists_eq_star_conv)

  have [simp]: ‹(∃x. (↑True ∧* ↑(x = a @ [b])) s) = □ s› for a b s
    by (auto simp: Exists_eq_simp, simp_all add: pure_true_conv) 
  show ?thesis
    unfolding qqq_def
    apply sepref_to_hoare
    by (vcg)
qed

schematic_goal mk_free_ghost_assn[sepref_frame_free_rules]: ‹MK_FREE virtual_vdom_fast_assn ?fr›
  unfolding virtual_vdom_fast_assn_def
  by synthesize_free

experiment
begin
definition ‹test0 ≡ (λ xs C. RETURN (xs @ [C]))›
sepref_def test
  is ‹uncurry test0›
  :: ‹virtual_vdom_fast_assn⇧k  *⇩a sint64_nat_assn⇧k →⇩a virtual_vdom_fast_assn›
  supply [[goals_limit=1]]
  unfolding test0_def
  by sepref

    export_llvm test
 end
end