Theory Micro_Rust_Interfaces_Core.References

(* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
   SPDX-License-Identifier: MIT *)

(*<*)
theory References
  imports 
    Shallow_Separation_Logic.Assertion_Language 
    Shallow_Separation_Logic.Tree_Shares
    Shallow_Separation_Logic.Triple 
    Shallow_Separation_Logic.Weakest_Precondition
    Shallow_Micro_Rust.Core_Expression
begin
(*>*)

named_theorems reference_axioms

locale reference_defs = 
  fixes reference_types :: ‹'s::{sepalg} ⇒ 'a ⇒ 'b ⇒ 'abort ⇒ 'i ⇒ 'o ⇒ unit›

    and update_raw_fun :: ‹('a, 'b) gref ⇒ 'b ⇒ ('s, unit, 'abort, 'i, 'o) function_body›
    and dereference_raw_fun :: ‹('a, 'b) gref ⇒ ('s, 'b, 'abort, 'i, 'o) function_body›
    and reference_raw_fun :: ‹'b ⇒ ('s, ('a, 'b) gref, 'abort, 'i, 'o) function_body›

    and points_to_raw' :: ‹('a, 'b) gref ⇒ share ⇒ 'b ⇒ 's assert› 

    and gref_can_store :: ‹('a, 'b) gref ⇒ 'b set›
    and new_gref_can_store :: ‹'b set›

    and can_alloc_reference :: ‹'s assert›
begin

named_theorems all_reference_defs'

definition [all_reference_defs']: ‹points_to_raw ≡ points_to_raw'›
notation points_to_raw ("(_) ↦ ⟨_⟩ (_)" [69,0,69]70)

text‹Specifications›

definition update_raw_contract :: ‹('a, 'b) gref ⇒ 'b ⇒ 'b ⇒ ('s, unit, 'abort) function_contract› where 
  [all_reference_defs']: ‹update_raw_contract r g0 g ≡
     let pre = ⟨g ∈ gref_can_store r⟩ ⋆ points_to_raw r ⊤ g0 in
     let post = λ_. (points_to_raw r ⊤ g) in
     make_function_contract pre post›

definition reference_raw_contract :: ‹'b ⇒ ('s, ('a, 'b) gref, 'abort) function_contract› where 
  [all_reference_defs']: ‹reference_raw_contract g ≡
      let pre = can_alloc_reference ⋆ ⟨g ∈ new_gref_can_store⟩ in
     let post = λr. points_to_raw r ⊤ g ⋆ 
                    ⟨new_gref_can_store ⊆ gref_can_store r⟩ ⋆ can_alloc_reference in
     make_function_contract pre post›

definition dereference_raw_contract 
  :: ‹('a, 'b) gref ⇒ share ⇒ 'b ⇒ ('s, 'b, 'abort) function_contract› where 
  [all_reference_defs']: ‹dereference_raw_contract r sh g ≡
     let pre = points_to_raw r sh g in
     let post = λg'. (points_to_raw r sh g ⋆ ⟨g=g'⟩) in
     make_function_contract pre post›

text‹Lifting the raw reference operations to typed ones using foci:›

definition reference_fun ::
  ‹('b, 'v) prism ⇒
   'v ⇒
   ('s, ('a, 'b, 'v) ref, 'abort, 'i, 'o) function_body› where
  [all_reference_defs']: ‹reference_fun p e ≡ FunctionBody ⟦
       let r = reference_raw_fun (⟪prism_embed p e⟫);
       ⟪make_ref_typed_from_untyped⟫⇩2(r, ⟪prism_to_focus p⟫)
   ⟧›

―‹▩‹prism_to_focus p› has no (unconditional) code equations. Instead, specific instances of
for valid ▩‹p› have to be wrapped as definitions and given code equations by instantiating
▩‹prism_to_focus.rep_eq›. However, those specialized code equations will only be recognized 
during code generation if ▩‹reference_fun› is inlined -- thus the need for ▩‹code_unfold›.›
declare reference_fun_def[code_unfold]

definition modify_raw_fun :: ‹('a, 'b) gref ⇒ ('b ⇒ 'b) ⇒ ('s, unit, 'abort, 'i, 'o) function_body› where
  [all_reference_defs']: ‹modify_raw_fun r f ≡ FunctionBody ⟦
     let g = dereference_raw_fun(r);
     update_raw_fun(r, ⟪f⟫⇩1(g))
  ⟧›

definition modify_fun :: ‹('a, 'b, 'v) ref ⇒ ('v ⇒ 'v) ⇒ ('s, unit, 'abort, 'i, 'o) function_body› where
  [all_reference_defs']: ‹modify_fun ref f ≡ FunctionBody ⟦
     modify_raw_fun (⟪untype_ref⟫⇩1(ref), ⟪focus_modify (get_focus ref) f⟫)
  ⟧›

definition update_fun :: ‹('a, 'b, 'v) ref ⇒ 'v ⇒ ('s, unit, 'abort, 'i, 'o) function_body› where
  [all_reference_defs']: ‹update_fun ref v ≡ FunctionBody ⟦
     modify_fun(ref, ⟪λ_. v⟫)
   ⟧›

definition dereference_fun :: ‹('a, 'b, 'v) ref ⇒ ('s, 'v, 'abort, 'i, 'o) function_body› where
  [all_reference_defs']: ‹dereference_fun ref ≡ FunctionBody ⟦
      let b = dereference_raw_fun(⟪untype_ref⟫⇩1(ref));
      match (⟪focus_view (∫ ref) b⟫) {
         None ⇒ ε‹abort TypeError›,
         Some(v) ⇒ v
      }
  ⟧›

definition ro_dereference_fun ::
      ‹('a, 'b, 'v) ro_ref ⇒ ('s, 'v, 'abort, 'i, 'o) function_body› where
  [all_reference_defs']: ‹ro_dereference_fun r ≡ FunctionBody ⟦ dereference_fun(⟪unsafe_ref_from_ro_ref⟫⇩1(r)) ⟧›

definition is_valid_ref_for :: ‹('a, 'b, 'v) ref ⇒ 'b set ⇒ bool›
  where ‹is_valid_ref_for r P ≡ focus_dom (get_focus r) ⊆ P›

lemma is_valid_ref_for_compose[focus_intros]:
  assumes ‹is_valid_ref_for r P›
  shows ‹is_valid_ref_for (focus_reference f r) P› 
  using assms by (simp add: is_valid_ref_for_def focus_factors_trans focus_focused_get_focus)

abbreviation points_to_localizes :: ‹('a, 'b, 'v) ref ⇒ 'b ⇒ 'v ⇒ bool› where
  ‹points_to_localizes r b v ≡ is_valid_ref_for r (gref_can_store (unwrap_focused r)) 
                                ∧ focus_view (get_focus r) b = Some v›

definition points_to :: ‹('a, 'b, 'v) ref ⇒ share ⇒ 'b ⇒ 'v ⇒ 's assert› where
  [all_reference_defs']: ‹points_to r sh b v ≡ points_to_raw (unwrap_focused r) sh b ⋆ ⟨points_to_localizes r b v⟩›

notation points_to ("(_) ↦ ⟨_⟩/_/ ↓/ _" [69,0,69,69]70)

abbreviation points_to_modified :: ‹('a, 'b, 'v) ref ⇒ share ⇒ ('v ⇒ 'v) ⇒ 'b ⇒ 'v ⇒ 's assert› where
  ‹points_to_modified r sh op b v ≡ points_to_raw (♭ r) sh (focus_modify (get_focus r) op b) ⋆
     ⟨points_to_localizes r b v⟩›

notation points_to_modified ("(_) ↦ ⟨_⟩/ _· '(_↓_')" [69,0,69,69,69]70)

definition modify_raw_contract :: ‹('a, 'b) gref ⇒ 'b ⇒ ('b ⇒ 'b) ⇒ ('s, unit, 'abort) function_contract› where 
  [all_reference_defs']: ‹modify_raw_contract r g f ≡
     let pre = ⟨f g ∈ gref_can_store r⟩ ⋆ points_to_raw r ⊤ g in
     let post = λ_. (points_to_raw r ⊤ (f g)) in
     make_function_contract pre post›

definition update_contract :: ‹('a, 'b, 'v) ref ⇒ 'b ⇒ 'v ⇒ 'v ⇒ ('s, unit, 'abort) function_contract› where 
  [all_reference_defs']: ‹update_contract r g0 v0 v ≡
     let pre = points_to r ⊤ g0 v0 in
     let post = λ_. points_to_modified r ⊤ (λ_. v) g0 v0 in
     make_function_contract pre post›

definition modify_contract :: ‹('a, 'b, 'v) ref ⇒ 'b ⇒ 'v ⇒ ('v ⇒ 'v) ⇒ ('s, unit, 'abort) function_contract› 
  where [all_reference_defs']: ‹modify_contract r g0 v0 f ≡
     let pre = points_to r ⊤ g0 v0 in
     let post = λ_. (points_to_modified r ⊤ f g0 v0) in
     make_function_contract pre post›

definition dereference_contract 
  :: ‹('a, 'b, 'v) ref ⇒ share ⇒ 'b ⇒ 'v ⇒ ('s, 'v, 'abort) function_contract› where 
  [all_reference_defs']: ‹dereference_contract r sh g v ≡
     let pre = points_to r sh g v in
     let post = λv'. (points_to r sh g v ⋆ ⟨v=v'⟩) in
     make_function_contract pre post›

definition ro_dereference_contract
  :: ‹('a, 'b, 'v) ro_ref ⇒ share ⇒ 'b ⇒ 'v ⇒ ('s, 'v, 'abort) function_contract› where 
  [all_reference_defs']: ‹ro_dereference_contract r sh g v ≡
     let pre = points_to (unsafe_ref_from_ro_ref r) sh g v in
     let post = λv'. points_to (unsafe_ref_from_ro_ref r) sh g v ⋆ ⟨v=v'⟩ in
     make_function_contract pre post›

definition reference_contract :: ‹('b, 'v) prism ⇒ 'v ⇒ ('s, ('a, 'b, 'v) ref, 'abort) function_contract› where 
  [all_reference_defs']: ‹reference_contract p v ≡
     let pre = can_alloc_reference in
     let post = λr. points_to r ⊤ (prism_embed p v) v ⋆ ⟨∫r = prism_to_focus p⟩ ⋆ can_alloc_reference in
     make_function_contract pre post›

lemmas all_reference_defs = all_reference_defs'
named_theorems all_reference_specs

end

locale reference = reference_defs reference_types 
    update_raw_fun 
    dereference_raw_fun
    reference_raw_fun
    points_to_raw'
    gref_can_store
    new_gref_can_store
    can_alloc_reference
  for reference_types :: ‹'s::{sepalg} ⇒ 'a ⇒ 'b ⇒ 'abort ⇒ 'i prompt ⇒ 'o prompt_output ⇒ unit› 
    and update_raw_fun dereference_raw_fun reference_raw_fun points_to_raw' gref_can_store 
      new_gref_can_store can_alloc_reference +

  assumes update_raw_spec [all_reference_specs]:      ‹Γ ; update_raw_fun r g    ⊨⇩F update_raw_contract r g0 g›
      and dereference_raw_spec[all_reference_specs]: ‹Γ ; dereference_raw_fun r ⊨⇩F dereference_raw_contract r sh g›
      and reference_raw_spec[all_reference_specs]:   ‹Γ ; reference_raw_fun g   ⊨⇩F reference_raw_contract g›

      and ucincl_points_to_raw[ucincl_intros, all_reference_specs]: ‹⋀r sh g. ucincl (points_to_raw r sh g)›
      and ucincl_can_alloc_reference[ucincl_intros, all_reference_specs]: ‹ucincl can_alloc_reference›

      and points_to_raw_combine[all_reference_specs]: 
         ‹⋀r sh1 sh2 v1 v2. r ↦⟨sh1⟩ v1 ⋆ r ↦⟨sh2⟩ v2 ⤏ r ↦⟨sh1+sh2⟩ v1 ⋆ ⟨v1 = v2⟩›
      and points_to_raw_split[all_reference_specs]: 
         ‹⋀sh shA shB r v. sh = shA+shB ⟹ shA ♯ shB ⟹ 0 < shA ⟹ 0 < shB ⟹ 
            r ↦⟨sh⟩ v ⤏ r ↦⟨shA⟩ v ⋆ r ↦⟨shB⟩ v›
begin

lemma points_to_raw'_ucincl[ucincl_intros]:
  shows ‹⋀r sh g. ucincl (points_to_raw' r sh g)›
  using ucincl_points_to_raw unfolding points_to_raw_def by simp

lemma points_to_raw_aentails[intro]:
  assumes ‹g0 = g1›  
    shows ‹r ↦⟨sh⟩ g0 ⤏ r ↦⟨sh⟩ g1›
using assms by (auto intro!: aentails_refl)

lemma points_to_aentails[intro]: 
  assumes ‹g0 = g1›  
      and ‹v0 = v1›
    shows ‹r ↦⟨sh⟩ g0↓v0 ⤏ r ↦⟨sh⟩ g1↓v1›
using assms by (auto intro!: aentails_refl)

lemma aentails_split_single_points_to_assm:
  assumes ‹points_to_localizes r g v ⟹ ♭ r ↦⟨sh⟩ g ⤏ φ›
  shows ‹r↦⟨sh⟩ g↓v ⤏ φ› 
by (metis (full_types) apure_entailsL asepconj_comm assms points_to_def ucincl_points_to_raw)

lemma aentails_split_top_points_to_assm:
  assumes ‹points_to_localizes r g v ⟹ ♭ r ↦⟨sh⟩ g ⋆ ψ ⤏ φ›
    shows ‹r↦⟨sh⟩ g↓v ⋆ ψ ⤏ φ› 
by (metis aentails_split_single_points_to_assm assms awand_adjoint)

lemma aentails_cancel_points_to_raw_with_typed:
  assumes ‹rr' = ♭ r›
      and ‹g' = g›
      and ‹ψ ⤏ ⟨points_to_localizes r g v⟩ ⋆ φ›
    shows ‹rr'↦⟨sh⟩ g' ⋆ ψ ⤏ r↦⟨sh⟩ g↓v ⋆ φ› 
using assms points_to_def by (metis (no_types, lifting) asepconj_assoc asepconj_mono)

lemma aentails_cancel_points_to_raw_with_typed_0LR:
    notes asat_simp [simp]
  assumes ‹rr' = ♭ r›
      and ‹g' = g›
      and ‹points_to_localizes r g v›
    shows ‹rr'↦⟨sh⟩ g' ⤏ r↦⟨sh⟩ g↓v›   
using assms by (simp add: aentails_def points_to_def ucincl_points_to_raw)

lemma aentails_cancel_points_to_raw_with_typed_0L:
  assumes ‹rr' = ♭ r›
      and ‹g' = g›
      and ‹φ ⤏ ⟨points_to_localizes r g v⟩›
    shows ‹rr'↦⟨sh⟩ g' ⋆ φ ⤏ r↦⟨sh⟩ g↓v›   
using assms by (simp add: asepconj_mono points_to_def)

lemma aentails_cancel_points_to_raw_with_typed_0R:
  assumes ‹rr' = ♭ r›
      and ‹g' = g›
      and ‹⊤ ⤏ ⟨points_to_localizes r g v⟩ ⋆ ψ›
    shows ‹rr'↦⟨sh⟩ g' ⤏ r↦⟨sh⟩ g↓v ⋆ ψ›   
  using aentails_cancel_points_to_raw_with_typed by (metis asepconj_ident2 assms ucincl_points_to_raw) 

declare reference_axioms [reference_axioms]
end

end
(*>*)