theory LBD_LLVM imports LBD IsaSAT_Literals_LLVM begin type_synonym 'a larray64 = ‹('a,64) larray› type_synonym lbd_assn = ‹(32 word) larray64 × 32 word × 32 word› (*TODO use 32*) abbreviation lbd_int_assn :: ‹lbd_ref ⇒ lbd_assn ⇒ assn› where ‹lbd_int_assn ≡ larray64_assn uint32_nat_assn ×⇩a uint32_nat_assn ×⇩a uint32_nat_assn› definition lbd_assn :: ‹lbd ⇒ lbd_assn ⇒ assn› where ‹lbd_assn ≡ hr_comp lbd_int_assn lbd_ref› paragraph ‹Testing if a level is marked› sepref_def level_in_lbd_code is [] ‹uncurry (RETURN oo level_in_lbd_ref)› :: ‹uint32_nat_assn⇧k *⇩a lbd_int_assn⇧k →⇩a bool1_assn› supply [[goals_limit=1]] unfolding level_in_lbd_ref_def short_circuit_conv length_uint32_nat_def apply (rewrite in ‹⌑ < _› annot_unat_snat_upcast[where 'l=‹64›]) apply (rewrite in ‹_ ! ⌑› annot_unat_snat_upcast[where 'l=‹64›]) by sepref lemma level_in_lbd_hnr[sepref_fr_rules]: ‹(uncurry level_in_lbd_code, uncurry (RETURN ∘∘ level_in_lbd)) ∈ uint32_nat_assn⇧k *⇩a lbd_assn⇧k →⇩a bool1_assn› supply lbd_ref_def[simp] unat32_max_def[simp] using level_in_lbd_code.refine[FCOMP level_in_lbd_ref_level_in_lbd] unfolding lbd_assn_def[symmetric] by simp sepref_def lbd_empty_loop_code is ‹lbd_empty_loop_ref› :: ‹lbd_int_assn⇧d →⇩a lbd_int_assn› unfolding lbd_empty_loop_ref_def supply [[goals_limit=1]] apply (rewrite at ‹_ + ⌑› snat_const_fold[where 'a=64])+ apply (rewrite at ‹(_, ⌑)› snat_const_fold[where 'a=64]) apply (annot_unat_const ‹TYPE(32)›) by sepref sepref_def lbd_empty_cheap_code is ‹lbd_empty_cheap_ref› :: ‹[λ(_, stamp, _). stamp < unat32_max]⇩a lbd_int_assn⇧d → lbd_int_assn› unfolding lbd_empty_cheap_ref_def supply [[goals_limit=1]] apply (annot_unat_const ‹TYPE(32)›) by sepref lemma unat32_max_alt_def: "unat32_max = 4294967295" by (auto simp: unat32_max_def) sepref_register lbd_empty_cheap_ref lbd_empty_loop_ref sepref_def lbd_empty_code is ‹lbd_empty_ref› :: ‹lbd_int_assn⇧d →⇩a lbd_int_assn› unfolding lbd_empty_ref_def unat32_max_alt_def supply [[goals_limit=1]] apply (annot_unat_const ‹TYPE(32)›) by sepref lemma lbd_empty_hnr[sepref_fr_rules]: ‹(lbd_empty_code, lbd_empty) ∈ lbd_assn⇧d →⇩a lbd_assn› using lbd_empty_code.refine[FCOMP lbd_empty_ref_lbd_empty] unfolding lbd_assn_def . sepref_def empty_lbd_code is [] ‹uncurry0 (RETURN empty_lbd_ref)› :: ‹unit_assn⇧k →⇩a lbd_int_assn› supply [[goals_limit=1]] unfolding empty_lbd_ref_def larray_fold_custom_replicate apply (rewrite at ‹op_larray_custom_replicate ⌑ _› snat_const_fold[where 'a=64]) apply (annot_unat_const ‹TYPE(32)›) by sepref lemma empty_lbd_ref_empty_lbd: ‹(uncurry0 (RETURN empty_lbd_ref), uncurry0 (RETURN empty_lbd)) ∈ unit_rel →⇩f ⟨lbd_ref⟩nres_rel› using empty_lbd_ref_empty_lbd unfolding uncurry0_def . lemma empty_lbd_hnr[sepref_fr_rules]: ‹(Sepref_Misc.uncurry0 empty_lbd_code, Sepref_Misc.uncurry0 (RETURN empty_lbd)) ∈ unit_assn⇧k →⇩a lbd_assn› using empty_lbd_code.refine[FCOMP empty_lbd_ref_empty_lbd] unfolding lbd_assn_def . sepref_def get_LBD_code is [] ‹get_LBD_ref› :: ‹lbd_int_assn⇧k →⇩a uint32_nat_assn› unfolding get_LBD_ref_def by sepref lemma get_LBD_hnr[sepref_fr_rules]: ‹(get_LBD_code, get_LBD) ∈ lbd_assn⇧k →⇩a uint32_nat_assn› using get_LBD_code.refine[FCOMP get_LBD_ref_get_LBD, unfolded lbd_assn_def[symmetric]] . paragraph ‹Marking more levels› lemmas list_grow_alt = list_grow_def[unfolded op_list_grow_init'_def[symmetric]] sepref_def lbd_write_code is [] ‹uncurry lbd_ref_write› :: ‹ [λ(lbd, i). i ≤ Suc (unat32_max div 2)]⇩a lbd_int_assn⇧d *⇩a uint32_nat_assn⇧k → lbd_int_assn› supply [[goals_limit=1]] unfolding lbd_ref_write_def length_uint32_nat_def list_grow_alt max_def op_list_grow_init'_alt apply (rewrite at ‹_ + ⌑› unat_const_fold[where 'a=32]) apply (rewrite at ‹_ + ⌑› unat_const_fold[where 'a=32]) apply (rewrite in ‹If (⌑ < _)› annot_unat_snat_upcast[where 'l=64]) apply (rewrite in ‹If (_ ! ⌑ = _)› annot_unat_snat_upcast[where 'l=64]) apply (rewrite in ‹_[ ⌑ := _]› annot_unat_snat_upcast[where 'l=64]) apply (rewrite in ‹op_list_grow_init _ ⌑ _› annot_unat_snat_upcast[where 'l=64]) apply (rewrite at ‹( _[ ⌑ := _], _, _ + _)› annot_unat_snat_upcast[where 'l=64]) apply (annot_unat_const ‹TYPE(32)›) by sepref lemma lbd_write_hnr_[sepref_fr_rules]: ‹(uncurry lbd_write_code, uncurry (RETURN ∘∘ lbd_write)) ∈ [λ(lbd, i). i ≤ Suc (unat32_max div 2)]⇩a lbd_assn⇧d *⇩a uint32_nat_assn⇧k → lbd_assn› using lbd_write_code.refine[FCOMP lbd_ref_write_lbd_write] unfolding lbd_assn_def . schematic_goal mk_free_lbd_assn[sepref_frame_free_rules]: ‹MK_FREE lbd_assn ?fr› unfolding lbd_assn_def by synthesize_free experiment begin export_llvm level_in_lbd_code lbd_empty_code empty_lbd_code get_LBD_code lbd_write_code end end