Theory IsaSAT_VMTF_Setup_LLVM

theory IsaSAT_VMTF_Setup_LLVM
imports IsaSAT_Setup IsaSAT_Literals_LLVM
begin
  (* TODO: Define vmtf_node_rel, such that sepref sees syntactically an assertion of form ‹pure ...›*)
type_synonym vmtf_node_assn = ‹(64 word × 32 word × 32 word)›

definition ‹vmtf_node1_rel ≡ { ((a,b,c),(VMTF_Node a b c)) | a b c. True}›
definition ‹vmtf_node2_assn ≡ uint64_nat_assn ×⇩a atom.option_assn ×⇩a atom.option_assn›

definition ‹vmtf_node_assn ≡ hr_comp vmtf_node2_assn vmtf_node1_rel›
lemmas [fcomp_norm_unfold] = vmtf_node_assn_def[symmetric]


lemma vmtf_node_assn_pure[safe_constraint_rules]: ‹CONSTRAINT is_pure vmtf_node_assn›
  unfolding vmtf_node_assn_def vmtf_node2_assn_def
  by solve_constraint


(*

  TODO: Test whether this setup is safe in general?
    E.g., synthesize destructors when side-tac can prove is_pure.

lemmas [sepref_frame_free_rules] = mk_free_is_pure
lemmas [simp] = vmtf_node_assn_pure[unfolded CONSTRAINT_def]
*)

lemmas [sepref_frame_free_rules] = mk_free_is_pure[OF vmtf_node_assn_pure[unfolded CONSTRAINT_def]]

lemma
    vmtf_Node_refine1: ‹(λa b c. (a,b,c), VMTF_Node) ∈ Id → Id → Id → vmtf_node1_rel›
and vmtf_stamp_refine1: ‹(λ(a,b,c). a, stamp) ∈ vmtf_node1_rel → Id›
and vmtf_get_prev_refine1: ‹(λ(a,b,c). b, get_prev) ∈ vmtf_node1_rel → ⟨Id⟩option_rel›
and vmtf_get_next_refine1: ‹(λ(a,b,c). c, get_next) ∈ vmtf_node1_rel → ⟨Id⟩option_rel›
  by (auto simp: vmtf_node1_rel_def)

sepref_def VMTF_Node_impl is []
  ‹uncurry2 (RETURN ooo (λa b c. (a,b,c)))›
  :: ‹uint64_nat_assn⇧k *⇩a (atom.option_assn)⇧k *⇩a (atom.option_assn)⇧k →⇩a vmtf_node2_assn›
  unfolding vmtf_node2_assn_def by sepref

sepref_def VMTF_stamp_impl
  is [] ‹RETURN o (λ(a,b,c). a)›
  :: ‹vmtf_node2_assn⇧k →⇩a uint64_nat_assn›
  unfolding vmtf_node2_assn_def
  by sepref

sepref_def VMTF_get_prev_impl
  is [] ‹RETURN o (λ(a,b,c). b)›
  :: ‹vmtf_node2_assn⇧k →⇩a atom.option_assn›
  unfolding vmtf_node2_assn_def
  by sepref

sepref_def VMTF_get_next_impl
  is [] ‹RETURN o (λ(a,b,c). c)›
  :: ‹vmtf_node2_assn⇧k →⇩a atom.option_assn›
  unfolding vmtf_node2_assn_def
  by sepref

(* TODO: This should be done automatically! For all structured ID-relations on hr_comp! *)
lemma workaround_hrcomp_id_norm[fcomp_norm_unfold]: ‹hr_comp R (⟨nat_rel⟩option_rel) = R› by simp

lemmas [sepref_fr_rules] =
  VMTF_Node_impl.refine[FCOMP vmtf_Node_refine1]
  VMTF_stamp_impl.refine[FCOMP vmtf_stamp_refine1]
  VMTF_get_prev_impl.refine[FCOMP vmtf_get_prev_refine1]
  VMTF_get_next_impl.refine[FCOMP vmtf_get_next_refine1]


type_synonym vmtf_assn = ‹vmtf_node_assn ptr × 64 word × 32 word × 32 word × 32 word›

type_synonym vmtf_remove_assn = ‹vmtf_assn × (32 word array_list64 × 1 word ptr)›


definition vmtf_assn :: ‹_ ⇒ vmtf_assn ⇒ assn› where
  ‹vmtf_assn ≡ (array_assn vmtf_node_assn ×⇩a uint64_nat_assn ×⇩a atom_assn ×⇩a atom_assn
    ×⇩a atom.option_assn)›

abbreviation atoms_hash_assn :: ‹bool list ⇒ 1 word ptr ⇒ assn› where
  ‹atoms_hash_assn ≡ array_assn bool1_assn›

abbreviation distinct_atoms_assn where
  ‹distinct_atoms_assn ≡ arl64_assn atom_assn ×⇩a atoms_hash_assn›

sepref_def vmtf_heur_fst_code
  is ‹RETURN o vmtf_heur_fst›
  :: ‹vmtf_assn⇧k →⇩a atom_assn›
  unfolding vmtf_heur_fst_def vmtf_assn_def
  by sepref

definition vmtf_heur_array_nth :: ‹vmtf ⇒ _›where
  ‹vmtf_heur_array_nth = (λ(ns, _, _, _) i. RETURN (ns ! i))›

sepref_def vmtf_heur_array_nth_code
  is ‹uncurry (vmtf_heur_array_nth)›
  :: ‹[λ(vm,i). i < length (fst vm)]⇩a vmtf_assn⇧k *⇩a atom_assn⇧k → vmtf_node_assn›
  supply [[eta_contract = false, goals_limit=1]]
  supply [sepref_fr_rules] = al_nth_hnr array_get_hnr
  unfolding vmtf_heur_array_nth_def vmtf_assn_def
  apply (rewrite at ‹(!) _ ⌑› value_of_atm_def[symmetric])
  unfolding  index_of_atm_def[symmetric]
  by sepref

end