Theory LBD_LLVM

theory LBD_LLVM
  imports LBD IsaSAT_Literals_LLVM
begin
(*TODO bundle?*)
no_notation WB_More_Refinement.fref ("[_]⇩f _ → _" [0,60,60] 60)
no_notation WB_More_Refinement.freft ("_ →⇩f _" [60,60] 60)

type_synonym 'a larray64 = "('a,64) larray"
type_synonym lbd_assn = ‹(1 word) larray64 × 32 word × 32 word›

(*TODO use 32*)
abbreviation lbd_int_assn :: ‹lbd_ref ⇒ lbd_assn ⇒ assn› where
  ‹lbd_int_assn ≡ larray64_assn bool1_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] uint32_max_def[simp]
  using level_in_lbd_code.refine[FCOMP level_in_lbd_ref_level_in_lbd[unfolded convert_fref]]
  unfolding lbd_assn_def[symmetric]
  by simp

sepref_def lbd_empty_code
  is [] ‹lbd_empty_ref›
  :: ‹lbd_int_assn⇧d  →⇩a lbd_int_assn›
  unfolding lbd_empty_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)")
  apply (rewrite in "_ ≤ ⌑" annot_unat_snat_upcast[where 'l="64"])
  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[unfolded convert_fref]]
  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 convert_fref .

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 convert_fref],
     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 (uint32_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 (uint32_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[unfolded convert_fref]]
  unfolding lbd_assn_def .


experiment begin

export_llvm
  level_in_lbd_code
  lbd_empty_code
  empty_lbd_code
  get_LBD_code
  lbd_write_code

end

end