theory Sorting_Ex_Array_Idxs imports Sorting_Introsort begin subsection ‹Compare Indexes into Value Array› term nao_assn term narray_assn lemma narray_assn_alt: "narray_assn = mk_assn (λxs p. if xs=[] then ↑(p=null) else ↿LLVM_DS_Array.array_assn xs p)" by (auto simp: narray_assn_def fun_eq_iff split: list.splits) definition "woarray_slice_diff_assn n p ≡ if n=0 then ↑(p=null) else ↿array_base_assn n p" find_theorems abase context begin interpretation llvm_prim_mem_setup . (* TODO: Move *) lemma ll_malloc_tag_null[sep_algebra_simps]: "ll_malloc_tag n null = sep_false" unfolding ll_malloc_tag_def null_def llvm_blockp_def by simp (* TODO: Move *) lemma array_base_assn_simps[sep_algebra_simps]: "↿array_base_assn 0 null = □" "↿array_base_assn 0 p = ↑(p=null)" "↿array_base_assn n null = ↑(n=0)" unfolding array_base_assn_def by (auto simp: sep_algebra_simps) end lemma wo_array_assn_to_slice: "woarray_assn A xs p = (woarray_slice_assn A xs p ** woarray_slice_diff_assn (length xs) p)" unfolding woarray_assn_conv eoarray_assn_def Proto_EOArray.nao_assn_def array_assn_split hr_comp_def apply (clarsimp simp add: sep_algebra_simps fun_eq_iff) unfolding woarray_slice_assn_conv eoarray_slice_assn_def sao_assn_def woarray_slice_diff_assn_def apply (cases "xs=[]"; cases "p=null"; simp) subgoal by (auto simp: sep_algebra_simps) subgoal by (clarsimp simp: sep_algebra_simps) subgoal by (clarsimp simp: sep_algebra_simps) apply (clarsimp simp: sep_algebra_simps sep_conj_c) apply safe subgoal for s xs' apply (cases "length xs = length xs'"; simp) apply auto done subgoal for s xs' apply (cases "length xs = length xs'"; cases "xs'≠[]"; simp) apply auto done done lemma pure_part_invalid_assn: "pure_part (invalid_assn A x xi) ⟹ invalid_assn A x xi = □" unfolding invalid_assn_def by (auto simp: sep_algebra_simps) lemma wo_array_sort_adapt: assumes LP: "⋀p xs l h. s p xs l h ≤⇩n SPEC (λxs'. length xs'=length xs)" assumes A: "(si,uncurry3 s) ∈ [λ_. True]⇩c A⇧k *⇩a (woarray_slice_assn elem_assn)⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k → (woarray_slice_assn elem_assn) [λ(((_, ai), _), _) r. r = ai]⇩c" shows "(si,uncurry3 s) ∈ [λ_. True]⇩c A⇧k *⇩a (woarray_assn elem_assn)⇧d *⇩a size_assn⇧k *⇩a size_assn⇧k → woarray_assn elem_assn [λ(((_, ai), _), _) r. r = ai]⇩c" proof - { fix p xs l h xs' assume "nofail (s p xs l h)" "RETURN xs' ≤ s p xs l h" hence "length xs' = length xs" using LP by (auto simp: pw_leof_iff pw_le_iff) } note [simp] = this show ?thesis apply sepref_to_hoare subgoal for h hi l li xs xsi p pi unfolding wo_array_assn_to_slice apply clarsimp supply R = A[to_hnr, simplified, THEN hn_refineD, unfolded hn_ctxt_def] supply [vcg_rules] = R supply [simp] = pure_def apply vcg (* TODO: Hack! Handle the hn-invalid cleanly *) apply vcg_try_solve apply (auto dest!: pure_part_split_conj simp: pure_part_invalid_assn sep_algebra_simps FRI_END_def FRAME_INFER_def) done done qed lemma woarray_iterator: "random_access_iterator (woarray_assn snat_assn) (eoarray_assn snat_assn) snat_assn Mreturn Mreturn eo_extract_impl array_upd" apply unfold_locales apply (rule eo_hnr_dep)+ done lemma list_assn_oelem_assn_map_Some: "↿(list_assn (oelem_assn A)) (map Some xs) xsi = ↿(list_assn A) xs xsi" apply (cases "length xs = length xsi"; simp?) apply (induction xs xsi rule: list_induct2) by (auto) lemma nao_to_wo_assn: "↿(nao_assn A Map.empty) = woarray_assn (↿A)" unfolding woarray_assn_conv eoarray_assn_def unfolding nao_assn_def Proto_EOArray.nao_assn_def hr_comp_def apply (auto simp: sep_algebra_simps fun_eq_iff list_assn_oelem_assn_map_Some) unfolding list_assn_def apply (auto simp: sep_algebra_simps dest: sym) done lemma wo_to_nao_assn: "woarray_assn A = ↿(nao_assn (mk_assn A) Map.empty)" unfolding nao_to_wo_assn sel_mk_assn .. locale idxs_comp = INNER: sort_impl_context inner_less_eq inner_less inner_less_impl A for inner_less_eq inner_less :: "'a ⇒ 'a ⇒ bool" and inner_less_impl :: "'ai::llvm_rep ⇒ 'ai ⇒ 1 word llM" and A :: "'a ⇒ 'ai ⇒ assn" begin definition idx_cdom :: "'a list ⇒ nat set" where "idx_cdom vs ≡ {0..<length vs}" definition "idx_less vs i j ≡ (inner_less (vs!i) (vs!j))" definition "idx_pcmp vs i j ≡ if i=j then RETURN False else INNER.mop_cmp_idxs vs i j" lemma snat_assn_eq_refine: "⟦♭⇩psnat.assn ba bia; ♭⇩psnat.assn b bi⟧ ⟹ bia = bi ⟷ ba=b" apply (simp add: snat.assn_def) by (metis snat_eq_unat_aux2 unsigned_word_eqI) sepref_register idx_pcmp sepref_def idx_pcmp_impl is "uncurry2 (PR_CONST idx_pcmp)" :: "(woarray_slice_assn A)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn" unfolding PR_CONST_def unfolding idx_pcmp_def by sepref interpretation weak_ordering_on_lt "idx_cdom vs" "idx_less vs" apply unfold_locales unfolding idx_less_def apply (erule INNER.asym) apply (erule INNER.itrans) done interpretation parameterized_weak_ordering idx_cdom idx_less "PR_CONST idx_pcmp" apply unfold_locales unfolding idx_pcmp_def PR_CONST_def apply refine_vcg apply (auto simp: idx_less_def idx_cdom_def) done sublocale parameterized_sort_impl_context "woarray_assn size_assn" "eoarray_assn size_assn" size_assn Mreturn Mreturn eo_extract_impl array_upd idx_cdom idx_less "PR_CONST idx_pcmp" idx_pcmp_impl "woarray_slice_assn A" apply unfold_locales apply (rule eo_hnr_dep)+ unfolding GEN_ALGO_def refines_param_relp_def (* TODO: thm gen_refines_param_relpI *) by (rule idx_pcmp_impl.refine) term introsort_param_impl find_theorems introsort_param_impl term arr_assn thm introsort_param_impl_correct wo_array_sort_adapt end (* definition idx_less :: "'a::linorder list ⇒ nat ⇒ nat ⇒ bool" where "idx_less vs i j ≡ vs!i < vs!j" definition idx_cdom :: "'a::linorder list ⇒ nat set" where "idx_cdom vs ≡ {0..<length vs}" definition "idx_pcmp vs i j ≡ do { ASSERT (i<length vs ∧ j<length vs); RETURN (vs!i < vs!j) }" sepref_def idx_pcmp_impl is "uncurry2 idx_pcmp" :: "(al_assn snat_assn)⇧k *⇩a size_assn⇧k *⇩a size_assn⇧k →⇩a bool1_assn" unfolding idx_pcmp_def by sepref interpretation IDXO: weak_ordering_on_lt "idx_cdom vs" "idx_less vs" apply unfold_locales unfolding idx_less_def by auto interpretation IDXO: parameterized_weak_ordering idx_cdom idx_less idx_pcmp apply unfold_locales unfolding idx_pcmp_def apply refine_vcg apply (auto simp: idx_less_def idx_cdom_def) done global_interpretation IDXO: parameterized_sort_impl_context "woarray_assn snat_assn" "eoarray_assn snat_assn" snat_assn return return eo_extract_impl array_upd idx_cdom idx_less idx_pcmp idx_pcmp_impl "al_assn snat_assn" defines IDXO_is_guarded_insert_impl = IDXO.is_guarded_param_insert_impl and IDXO_is_unguarded_insert_impl = IDXO.is_unguarded_param_insert_impl and IDXO_unguarded_insertion_sort_impl = IDXO.unguarded_insertion_sort_param_impl and IDXO_guarded_insertion_sort_impl = IDXO.guarded_insertion_sort_param_impl and IDXO_final_insertion_sort_impl = IDXO.final_insertion_sort_param_impl (*and IDXO_mop_lchild_impl = IDXO.mop_lchild_impl and IDXO_mop_rchild_impl = IDXO.mop_rchild_impl and IDXO_has_rchild_impl = IDXO.has_rchild_impl and IDXO_has_lchild_impl = IDXO.has_lchild_impl *) and IDXO_pcmpo_idxs_impl = IDXO.pcmpo_idxs_impl and IDXO_pcmpo_v_idx_impl = IDXO.pcmpo_v_idx_impl and IDXO_pcmpo_idx_v_impl = IDXO.pcmpo_idx_v_impl and IDXO_pcmp_idxs_impl = IDXO.pcmp_idxs_impl and IDXO_mop_geth_impl = IDXO.mop_geth_impl and IDXO_mop_seth_impl = IDXO.mop_seth_impl and IDXO_sift_down_impl = IDXO.sift_down_impl and IDXO_heapify_btu_impl = IDXO.heapify_btu_impl and IDXO_heapsort_impl = IDXO.heapsort_param_impl and IDXO_qsp_next_l_impl = IDXO.qsp_next_l_impl and IDXO_qsp_next_h_impl = IDXO.qsp_next_h_impl and IDXO_qs_partition_impl = IDXO.qs_partition_impl (* and IDXO_qs_partitionXXX_impl = IDXO.qs_partitionXXX_impl *) and IDXO_partition_pivot_impl = IDXO.partition_pivot_impl and IDXO_introsort_aux_impl = IDXO.introsort_aux_param_impl and IDXO_introsort_impl = IDXO.introsort_param_impl and IDXO_move_median_to_first_impl = IDXO.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 idx_pcmp_impl.refine) (* TODO: This seems to be a quirk in llvm monadify and inline! FIXME! *) lemmas [abs_def,llvm_inline] = array_upd_def eo_extract_impl_def (*llvm_deps "IDXO_heapsort_impl :: 32 word ptr ⇒ _" *) locale pure_eo_adapter = fixes elem_assn :: "'a ⇒ 'ai::llvm_rep ⇒ assn" and wo_assn :: "'a list ⇒ 'oi::llvm_rep ⇒ assn" and wo_get_impl :: "'oi ⇒ 'size::len2 word ⇒ 'ai llM" and wo_set_impl :: "'oi ⇒ 'size::len2 word ⇒ 'ai ⇒ 'oi llM" assumes pure[safe_constraint_rules]: "is_pure elem_assn" and get_hnr: "(uncurry wo_get_impl,uncurry mop_list_get) ∈ wo_assn⇧k *⇩a snat_assn⇧k →⇩a elem_assn" and set_hnr: "(uncurry2 wo_set_impl,uncurry2 mop_list_set) ∈ [λ_.True]⇩c wo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧k → wo_assn [λ((ai,_),_) r. r=ai]⇩c" begin lemmas [sepref_fr_rules] = get_hnr set_hnr definition "only_some_rel ≡ {(a, Some a) | a. True} ∪ {(x, None) | x. True}" definition "eo_assn ≡ hr_comp wo_assn (⟨only_some_rel⟩list_rel)" definition "eo_extract1 p i ≡ doN { r ← mop_list_get p i; RETURN (r,p) }" sepref_definition eo_extract_impl is "uncurry eo_extract1" :: "wo_assn⇧d *⇩a (snat_assn' TYPE('size))⇧k →⇩a elem_assn ×⇩a wo_assn" unfolding eo_extract1_def by sepref lemma mop_eo_extract_aux: "mop_eo_extract p i = doN { r ← mop_list_get p i; ASSERT (r≠None ∧ i<length p); RETURN (the r, p[i:=None]) }" by (auto simp: pw_eq_iff refine_pw_simps) lemma assign_none_only_some_list_rel: assumes SR[param]: "(a, a') ∈ ⟨only_some_rel⟩list_rel" and L: "i < length a'" shows "(a, a'[i := None]) ∈ ⟨only_some_rel⟩list_rel" proof - have "(a[i := a!i], a'[i := None]) ∈ ⟨only_some_rel⟩list_rel" apply (parametricity) by (auto simp: only_some_rel_def) also from L list_rel_imp_same_length[OF SR] have "a[i := a!i] = a" by auto finally show ?thesis . qed lemma eo_extract1_refine: "(eo_extract1, mop_eo_extract) ∈ ⟨only_some_rel⟩list_rel → nat_rel → ⟨Id ×⇩r ⟨only_some_rel⟩list_rel⟩nres_rel" unfolding eo_extract1_def mop_eo_extract_aux supply R = mop_list_get.fref[THEN frefD, OF TrueI prod_relI, unfolded uncurry_apply, THEN nres_relD] apply (refine_rcg R) apply assumption apply (clarsimp simp: assign_none_only_some_list_rel) by (auto simp: only_some_rel_def) lemma eo_list_set_refine: "(mop_list_set, mop_eo_set) ∈ ⟨only_some_rel⟩list_rel → Id → Id → ⟨⟨only_some_rel⟩list_rel⟩nres_rel" unfolding mop_list_set_alt mop_eo_set_alt apply refine_rcg apply (simp add: list_rel_imp_same_length) apply simp apply parametricity apply (auto simp: only_some_rel_def) done lemma set_hnr': "(uncurry2 wo_set_impl,uncurry2 mop_list_set) ∈ wo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧k →⇩a wo_assn" apply (rule hfref_cons[OF set_hnr]) apply (auto simp: entails_lift_extract_simps sep_algebra_simps) done context notes [fcomp_norm_unfold] = eo_assn_def[symmetric] begin lemmas eo_extract_refine_aux = eo_extract_impl.refine[FCOMP eo_extract1_refine] lemma eo_extract_refine: "(uncurry eo_extract_impl, uncurry mop_eo_extract) ∈ [λ_. True]⇩c eo_assn⇧d *⇩a snat_assn⇧k → (elem_assn ×⇩a eo_assn) [λ(ai,_) (_,r). r=ai]⇩c" unfolding oops apply (sepref_to_hnr) apply (rule hn_refine_nofailI) unfolding cnc_assn_prod_conv apply (rule hnr_ceq_assnI) subgoal supply R = eo_extract_refine_aux[to_hnr, unfolded APP_def] apply (rule hn_refine_cons[OF _ R]) apply (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def) done subgoal unfolding eo_extract_impl_def mop_eo_extract_def hn_ctxt_def eo_assn_def hr_comp_def supply R = get_hnr[to_hnr, THEN hn_refineD, unfolded APP_def hn_ctxt_def] thm R supply [vcg_rules] = R supply [simp] = refine_pw_simps list_rel_imp_same_length apply (vcg) done done lemmas eo_set_refine_aux = set_hnr'[FCOMP eo_list_set_refine] lemma pure_part_cnc_imp_eq: "pure_part (cnc_assn (λx. x = cc) wo_assn a c) ⟹ c=cc" by (auto simp: pure_part_def cnc_assn_def pred_lift_extract_simps) (* TODO: Move *) lemma pure_entails_empty: "is_pure A ⟹ A a c ⊢ □" by (auto simp: is_pure_def sep_algebra_simps entails_lift_extract_simps) lemma eo_set_refine: "(uncurry2 wo_set_impl, uncurry2 mop_eo_set) ∈ eo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧d →⇩a⇩d (λ_ ((ai, _), _). cnc_assn (λx. x = ai) eo_assn)" apply (sepref_to_hnr) apply (rule hn_refine_nofailI) apply (rule hnr_ceq_assnI) subgoal supply R = eo_set_refine_aux[to_hnr, unfolded APP_def] apply (rule hn_refine_cons[OF _ R]) apply (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def pure_entails_empty[OF pure]) done subgoal unfolding hn_ctxt_def eo_assn_def hr_comp_def supply R = set_hnr[to_hnr, THEN hn_refineD, unfolded APP_def hn_ctxt_def] supply [vcg_rules] = R supply [simp] = refine_pw_simps list_rel_imp_same_length pure_part_cnc_imp_eq apply (vcg') done done end thm mop_eo_extract_def find_theorems mop_eo_set mop_list_set thm mop_eo_set_alt lemma id_Some_only_some_rel: "(id, Some) ∈ Id → only_some_rel" by (auto simp: only_some_rel_def) lemma map_some_only_some_rel_iff: "(xs, map Some ys) ∈ ⟨only_some_rel⟩list_rel ⟷ xs=ys" apply (rule iffI) subgoal apply (induction xs "map Some ys" arbitrary: ys rule: list_rel_induct) apply (auto simp: only_some_rel_def) done subgoal apply (rewrite in "(⌑,_)" list.map_id[symmetric]) apply (parametricity add: id_Some_only_some_rel) by simp done lemma wo_assn_conv: "wo_assn xs ys = eo_assn (map Some xs) ys" unfolding eo_assn_def hr_comp_def by (auto simp: pred_lift_extract_simps sep_algebra_simps fun_eq_iff map_some_only_some_rel_iff) lemma to_eo_conv_refine: "(return, mop_to_eo_conv) ∈ wo_assn⇧d →⇩a⇩d (λ_ ai. cnc_assn (λx. x = ai) eo_assn)" unfolding mop_to_eo_conv_def cnc_assn_def apply sepref_to_hoare apply (rewrite wo_assn_conv) apply vcg done lemma "None ∉ set xs ⟷ (∃ys. xs = map Some ys)" using None_not_in_set_conv by auto lemma to_wo_conv_refine: "(return, mop_to_wo_conv) ∈ eo_assn⇧d →⇩a⇩d (λ_ ai. cnc_assn (λx. x = ai) wo_assn)" unfolding mop_to_wo_conv_def cnc_assn_def eo_assn_def hr_comp_def apply sepref_to_hoare apply (auto simp add: refine_pw_simps map_some_only_some_rel_iff elim!: None_not_in_set_conv) by vcg lemma random_access_iterator: "random_access_iterator wo_assn eo_assn elem_assn return return eo_extract_impl wo_set_impl" apply unfold_locales using to_eo_conv_refine to_wo_conv_refine eo_extract_refine eo_set_refine apply blast+ done sublocale random_access_iterator wo_assn eo_assn elem_assn return return eo_extract_impl wo_set_impl by (rule random_access_iterator) find_theorems "?a = UNPROTECT ?a" end (*global_interpretation IDXO: random_access_iterator "woarray_assn snat_assn" "eoarray_assn snat_assn" snat_assn return return eo_extract_impl array_upd defines IDXO_swap_eo_impl = IDXO.swap_eo_impl apply unfold_locales apply (rule eo_hnr_dep)+ done *) print_named_simpset llvm_inline lemma al_pure_eo: "is_pure A ⟹ pure_eo_adapter A (al_assn A) arl_nth arl_upd" apply unfold_locales apply assumption apply (rule al_nth_hnr_mop; simp) subgoal apply (sepref_to_hnr) apply (rule hn_refine_nofailI) apply (rule hnr_ceq_assnI) subgoal supply R = al_upd_hnr_mop[to_hnr, unfolded APP_def, of A] apply (rule hn_refine_cons[OF _ R]) apply (auto simp: hn_ctxt_def pure_def invalid_assn_def sep_algebra_simps entails_lift_extract_simps) done subgoal unfolding hn_ctxt_def al_assn_def hr_comp_def pure_def in_snat_rel_conv_assn apply (erule is_pureE) apply (simp add: refine_pw_simps) supply [simp] = list_rel_imp_same_length by vcg done done global_interpretation ALO: pure_eo_adapter snat_assn "al_assn snat_assn" arl_nth arl_upd defines ALO_eo_extract_impl = ALO.eo_extract_impl apply (rule al_pure_eo) by simp global_interpretation ALO: parameterized_sort_impl_context "al_assn snat_assn" "ALO.eo_assn" snat_assn return return ALO_eo_extract_impl arl_upd idx_cdom idx_less idx_pcmp idx_pcmp_impl "al_assn snat_assn" defines ALO_is_guarded_insert_impl = ALO.is_guarded_param_insert_impl and ALO_is_unguarded_insert_impl = ALO.is_unguarded_param_insert_impl and ALO_unguarded_insertion_sort_impl = ALO.unguarded_insertion_sort_param_impl and ALO_guarded_insertion_sort_impl = ALO.guarded_insertion_sort_param_impl and ALO_final_insertion_sort_impl = ALO.final_insertion_sort_param_impl (*and ALO_mop_lchild_impl = ALO.mop_lchild_impl and ALO_mop_rchild_impl = ALO.mop_rchild_impl and ALO_has_rchild_impl = ALO.has_rchild_impl and ALO_has_lchild_impl = ALO.has_lchild_impl *) and ALO_pcmpo_idxs_impl = ALO.pcmpo_idxs_impl and ALO_pcmpo_v_idx_impl = ALO.pcmpo_v_idx_impl and ALO_pcmpo_idx_v_impl = ALO.pcmpo_idx_v_impl and ALO_pcmp_idxs_impl = ALO.pcmp_idxs_impl and ALO_mop_geth_impl = ALO.mop_geth_impl and ALO_mop_seth_impl = ALO.mop_seth_impl and ALO_sift_down_impl = ALO.sift_down_impl and ALO_heapify_btu_impl = ALO.heapify_btu_impl and ALO_heapsort_impl = ALO.heapsort_param_impl and ALO_qsp_next_l_impl = ALO.qsp_next_l_impl and ALO_qsp_next_h_impl = ALO.qsp_next_h_impl and ALO_qs_partition_impl = ALO.qs_partition_impl (* and ALO_qs_partitionXXX_impl = ALO.qs_partitionXXX_impl *) and ALO_partition_pivot_impl = ALO.partition_pivot_impl and ALO_introsort_aux_impl = ALO.introsort_aux_param_impl and ALO_introsort_impl = ALO.introsort_param_impl and ALO_move_median_to_first_impl = ALO.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 idx_pcmp_impl.refine) done lemmas [llvm_inline] = ALO.eo_extract_impl_def[THEN meta_fun_cong, THEN meta_fun_cong] print_named_simpset llvm_inline find_in_thms ALO_partition_pivot_impl in llvm_code (*oops llvm_deps "ALO_heapsort_impl :: (32 word,64) array_list ⇒ (64 word,64) array_list ⇒ _"*) (*export_llvm "ALO_heapsort_impl :: (32 word,64) array_list ⇒ (64 word,64) array_list ⇒ _"*) export_llvm "ALO_heapsort_impl :: (32 word,64) array_list ⇒ (64 word,64) array_list ⇒ _" "ALO_introsort_impl :: (32 word,64) array_list ⇒ (64 word,64) array_list ⇒ _" export_llvm "ALO_heapsort_impl :: (32 word,64) array_list ⇒ (64 word,64) array_list ⇒ _" "ALO_introsort_impl :: (32 word,64) array_list ⇒ (64 word,64) array_list ⇒ _" "IDXO_heapsort_impl :: (32 word,64) array_list ⇒ _" is "uint64_t* heapsort_idxs(array_list_32_64, uint64_t*, int64_t, int64_t)" "IDXO_introsort_impl :: (32 word,64) array_list ⇒ _" is "uint64_t* introsort_idxs(array_list_32_64, uint64_t*, int64_t, int64_t)" defines ‹ typedef struct {int64_t size; struct {int64_t capacity; int32_t *data;};} array_list_32_64; typedef struct {int64_t size; struct {int64_t capacity; int64_t *data;};} array_list_64_64; › file "../code/introsort_param.ll" thm ALO.introsort_param_impl_correct *) end