Theory IsaSAT_Sorting_LLVM

theory IsaSAT_Sorting_LLVM
  imports IsaSAT_Sorting
    Examples.Sorting_Ex_Array_Idxs
    IsaSAT_Literals_LLVM 
begin

declare α_butlast[simp del]
hide_const (open) NEMonad.RETURN NEMonad.ASSERT

text ‹All the weird proofs comes from the fact that, while very useful, \<^text>‹vcg› enjoys 
instantiating schematic variables by true, rendering proofs impossible.›
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 assert_true_bind_conv summarize_ASSERT_conv intro!: bind_cong arg_cong[of _ _ ASSERT])

  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"
      apply (sepref_to_hnr)
      apply (rule hn_refine_nofailI)
      apply (rule hnr_ceq_assnI)
      supply R = eo_extract_refine_aux[to_hnr, unfolded APP_def]
        apply (rule hn_refine_cons[OF _ R])
      subgoal by (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def)
      subgoal by (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def)
      subgoal by (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def)
      unfolding eo_extract_impl_def mop_eo_extract_def hn_ctxt_def eo_assn_def hr_comp_def
      apply (subst (3) sep.add_commute)
      supply R = get_hnr[to_hnr, THEN hn_refineD, unfolded APP_def hn_ctxt_def]
      thm R
      apply vcg
        supply [vcg_rules] = R
(*         supply [simp] = refine_pw_simps list_rel_imp_same_length *)
       apply (vcg)
        supply [simp] = refine_pw_simps list_rel_imp_same_length 
        apply vcg[]
       apply (auto simp: POSTCOND_def EXTRACT_def)
      apply (rule STATE_monoI)
       apply assumption
      apply (auto simp: entails_def)
      by (simp add: pure_true_conv)

    lemmas eo_set_refine_aux = set_hnr'[FCOMP eo_list_set_refine]

    (* 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) ∈ [λ_. True]⇩c eo_assn⇧d *⇩a snat_assn⇧k *⇩a elem_assn⇧d → (eo_assn) [λ((ai,_),_) r. r=ai]⇩c›
      apply (sepref_to_hnr)
      apply (rule hn_refine_nofailI)
      apply (rule hnr_ceq_assnI)
      supply R = eo_set_refine_aux[to_hnr, unfolded APP_def]
      apply (rule hn_refine_cons[OF _ R])
      subgoal by (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def pure_entails_empty[OF pure])
      subgoal by (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def pure_entails_empty[OF pure])
      subgoal by (auto simp: sep_algebra_simps entails_lift_extract_simps hn_ctxt_def pure_def invalid_assn_def pure_entails_empty[OF pure])
      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
       apply (vcg)
       supply [simp] = refine_pw_simps list_rel_imp_same_length
       apply (vcg)[]
       apply (auto simp: POSTCOND_def EXTRACT_def)
      apply (rule STATE_monoI)
       apply assumption
      apply (auto simp: entails_def)
      by (simp add: pure_true_conv)

  end

  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: ‹(Mreturn, mop_to_eo_conv) ∈ [λ_. True]⇩c wo_assn⇧d → (eo_assn) [λ(ai) (r). r=ai]⇩c›
    unfolding mop_to_eo_conv_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: ‹(Mreturn, mop_to_wo_conv) ∈  [λ_. True]⇩c eo_assn⇧d → (wo_assn) [λ(ai) (r). r=ai]⇩c›
    unfolding mop_to_wo_conv_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
    Mreturn Mreturn
    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
    Mreturn Mreturn
    eo_extract_impl
    wo_set_impl
    by (rule random_access_iterator)

end

lemma is_pureE_abs:
  assumes "is_pure P"
  obtains P' where "P = (λx x'. ↑(P' x x'))"
  using assms unfolding is_pure_def by blast


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)
      supply R = al_upd_hnr_mop[to_hnr, unfolded APP_def, of A]
      apply (rule hn_refine_cons[OF _ R])
    subgoal by (auto simp: hn_ctxt_def pure_def invalid_assn_def sep_algebra_simps entails_lift_extract_simps)
    subgoal by (auto simp: hn_ctxt_def pure_def invalid_assn_def sep_algebra_simps entails_lift_extract_simps)
    subgoal by (auto simp: hn_ctxt_def pure_def invalid_assn_def sep_algebra_simps entails_lift_extract_simps)
    subgoal by (auto simp: hn_ctxt_def pure_def invalid_assn_def sep_algebra_simps entails_lift_extract_simps)
    unfolding hn_ctxt_def al_assn_def hr_comp_def pure_def in_snat_rel_conv_assn
      (*     apply (erule is_pureE) *)
     apply (erule is_pureE)
     apply (auto simp add: refine_pw_simps)[]
     apply vcg
     apply (rule wpa_monoI)
       apply (rule arl_upd_rule[unfolded htriple_def, rule_format])
       apply (rule STATE_monoI)
        apply assumption
       apply (auto simp flip: in_snat_rel_conv_assn simp: fri_basic_extract_simps
        dr_assn_pure_asm_prefix_def entails_def pred_lift_extract_simps
        SOLVE_AUTO_DEFER_def list_rel_imp_same_length)[]
      apply (simp add: POSTCOND_def EXTRACT_def)
      apply (subst(asm) sep_algebra_class.sep_conj_commute)
      apply (subst STATE_monoI)
        apply assumption
       apply (rule conj_entails_mono[OF frame_rem1])
       apply simp_all
    done
  done

end