val state_correspondence (inames:inames)
  : Lemma
    (let s = state_uses inames in
     s.S.hprop == slprop /\
     s.S.mem == mem /\
     s.S.interp == interp /\
     s.S.star == star /\
     s.S.locks_invariant == locks_invariant inames /\
     (forall (p q frame:slprop)
        (m0:mem{interp (p `star` frame `star` locks_invariant inames m0) m0})
        (m1:mem{interp (q `star` frame `star` locks_invariant inames m1) m1}).
       (forall (f_frame:mprop frame). f_frame (core_mem m0) == f_frame (core_mem m1)) ==> 
       S.post_preserves_frame #s q frame m0 m1))
let state_correspondence inames =
    let s = state_uses inames in
    assert_norm (s.S.hprop == slprop)  ;
    assert_norm (s.S.mem == mem)  ;
    assert_norm (s.S.interp == interp);
    assert_norm (s.S.star == star);
    assert_norm (s.S.locks_invariant == locks_invariant inames)
val state_correspondence (inames:inames)
  : Lemma
    (let s = state_uses inames in
     s.S.hprop == slprop /\
     s.S.mem == mem /\
     s.S.interp == interp /\
     s.S.star == star /\
     s.S.locks_invariant == locks_invariant inames /\
     (forall (p q frame:slprop)
        (m0:mem{interp (p `star` frame `star` locks_invariant inames m0) m0})
        (m1:mem{interp (q `star` frame `star` locks_invariant inames m1) m1}).
       (forall (f_frame:mprop frame). f_frame (core_mem m0) == f_frame (core_mem m1)) ==> 
       S.post_preserves_frame #s q frame m0 m1))
let state_correspondence inames =
let s = state_uses inames in
assert_norm (s.S.hprop == slprop);
assert_norm (s.S.mem == mem);
assert_norm (s.S.interp == interp);
assert_norm (s.S.star == star);
assert_norm (s.S.locks_invariant == locks_invariant inames)
Steel.Semantics.Instantiate.fst.checked
Steel.Semantics.Hoare.MST.fst.checked Steel.Memory.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
Steel.Semantics.Instantiate.fst
Steel.Memory.inames FStar.Pervasives.assert_norm Prims.eq2 Steel.Semantics.Hoare.MST.__proj__Mkst0__item__mem Steel.Memory.slprop Steel.Semantics.Hoare.MST.__proj__Mkst0__item__locks_invariant Steel.Memory.locks_invariant Prims.unit Steel.Semantics.Hoare.MST.__proj__Mkst0__item__hprop Steel.Semantics.Hoare.MST.__proj__Mkst0__item__star Steel.Memory.star Steel.Memory.mem Prims.prop Steel.Semantics.Hoare.MST.__proj__Mkst0__item__interp Steel.Memory.interp Steel.Semantics.Hoare.MST.st Steel.Semantics.Instantiate.state_uses
(*
   Copyright 2020 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module Steel.Semantics.Instantiate
open Steel.Memory
module S = Steel.Semantics.Hoare.MST

let is_unit ()
  : Lemma (S.is_unit emp equiv star)
  = let aux (y:slprop)
      : Lemma (star emp y `equiv` y /\ star y emp `equiv` y)
      = emp_unit y; star_commutative emp y
    in
    Classical.forall_intro aux

#push-options "--warn_error -271"
let state_obeys_st_laws uses =
  Classical.forall_intro_3 star_associative;
  Classical.forall_intro_2 star_commutative;
  is_unit ();
  FStar.Classical.forall_intro_3 disjoint_join;
  let aux (m0 m1:mem)
    : Lemma (requires disjoint m0 m1)
            (ensures join m0 m1 == join m1 m0)
            [SMTPat (disjoint m0 m1)]
    = join_commutative m0 m1
  in
  let aux (m0 m1 m2:mem)
    : Lemma
      (requires
        disjoint m1 m2 /\
        disjoint m0 (join m1 m2))
      (ensures
        (disjoint_join m0 m1 m2;
        join m0 (join m1 m2) == join (join m0 m1) m2))
      [SMTPat (disjoint m0 (join m1 m2))]
    = join_associative m0 m1 m2
  in
  let aux (p1 p2 p3:slprop)
    : Lemma (p1 `equiv` p2 ==> (p1 `star` p3) `equiv` (p2 `star` p3))
      [SMTPat ()]
    = equiv_extensional_on_star  p1 p2 p3
  in
  ()
#pop-options
val state_correspondence (inames:inames)
  : Lemma
    (let s = state_uses inames in
     s.S.hprop == slprop /\
     s.S.mem == mem /\
     s.S.interp == interp /\
     s.S.star == star /\
     s.S.locks_invariant == locks_invariant inames /\
     (forall (p q frame:slprop)
        (m0:mem{interp (p `star` frame `star` locks_invariant inames m0) m0})
        (m1:mem{interp (q `star` frame `star` locks_invariant inames m1) m1}).
       (forall (f_frame:mprop frame). f_frame (core_mem m0) == f_frame (core_mem m1)) ==> 
       S.post_preserves_frame #s q frame m0 m1))
inames: Steel.Memory.inames
  -> FStar.Pervasives.Lemma
    (ensures
      (let s = Steel.Semantics.Instantiate.state_uses inames in
        Mkst0?.hprop s == Steel.Memory.slprop /\ Mkst0?.mem s == Steel.Memory.mem /\
        Mkst0?.interp s == Steel.Memory.interp /\ Mkst0?.star s == Steel.Memory.star /\
        Mkst0?.locks_invariant s == Steel.Memory.locks_invariant inames /\
        (forall (p: Steel.Memory.slprop)
            (q: Steel.Memory.slprop)
            (frame: Steel.Memory.slprop)
            (m0:
            Steel.Memory.mem
              { Steel.Memory.interp (Steel.Memory.star (Steel.Memory.star p frame)
                      (Steel.Memory.locks_invariant inames m0))
                  m0 })
            (m1:
            Steel.Memory.mem
              { Steel.Memory.interp (Steel.Memory.star (Steel.Memory.star q frame)
                      (Steel.Memory.locks_invariant inames m1))
                  m1 }).
            (forall (f_frame: Steel.Memory.mprop frame).
                f_frame (Steel.Memory.core_mem m0) == f_frame (Steel.Memory.core_mem m1)) ==>
            Steel.Semantics.Hoare.MST.post_preserves_frame q frame m0 m1)))