let loc_disjoint_addresses #aloc #c = loc_disjoint_addresses_intro #aloc #c
let loc_disjoint_addresses #aloc #c =
loc_disjoint_addresses_intro #aloc #c
FStar.ModifiesGen.fsti.checked
prims.fst.checked FStar.Set.fsti.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked
FStar.ModifiesGen.fsti
FStar.ModifiesGen.aloc_t FStar.ModifiesGen.cls FStar.ModifiesGen.loc_disjoint_addresses_intro Prims.bool FStar.Monotonic.HyperHeap.rid FStar.Set.set Prims.nat Prims.unit Prims.l_or Prims.b2t Prims.op_disEquality FStar.Set.subset FStar.Set.intersect FStar.Set.empty Prims.squash FStar.ModifiesGen.loc_disjoint FStar.ModifiesGen.loc_addresses Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2008-2018 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 FStar.ModifiesGen

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

(*** The modifies clause *)

(* NOTE: aloc cannot be a member of the class, because of OCaml
   extraction. So it must be a parameter of the class instead. *)

type aloc_t = HS.rid -> nat -> Tot Type

noeq
type cls (aloc: aloc_t) : Type = | Cls:
  (aloc_includes: (
    (#r: HS.rid) ->
    (#a: nat) ->
    aloc r a ->
    aloc r a ->
    GTot Type0
  )) ->
  (aloc_includes_refl: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x: aloc r a) ->
    Lemma
    (aloc_includes x x)
  )) ->
  (aloc_includes_trans: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x1: aloc r a) ->
    (x2: aloc r a) ->
    (x3: aloc r a) ->
    Lemma
    (requires (aloc_includes x1 x2 /\ aloc_includes x2 x3))
    (ensures (aloc_includes x1 x3))
  )) ->
  (aloc_disjoint: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x1: aloc r a) ->
    (x2: aloc r a) ->
    GTot Type0
  )) ->
  (aloc_disjoint_sym: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x1: aloc r a) ->
    (x2: aloc r a) ->
    Lemma
    (aloc_disjoint x1 x2 <==> aloc_disjoint x2 x1)
  )) ->
  (aloc_disjoint_includes: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (larger1: aloc r a) ->
    (larger2: aloc r a) ->
    (smaller1: aloc r a) ->
    (smaller2: aloc r a) ->
    Lemma
    (requires (aloc_disjoint larger1 larger2 /\ larger1 `aloc_includes` smaller1 /\ larger2 `aloc_includes` smaller2))
    (ensures (aloc_disjoint smaller1 smaller2))
  )) ->
  (aloc_preserved: (
    (#r: HS.rid) ->
    (#a: nat) ->
    aloc r a ->
    HS.mem ->
    HS.mem ->
    GTot Type0
  )) ->
  (aloc_preserved_refl: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x: aloc r a) ->
    (h: HS.mem) ->
    Lemma
    (aloc_preserved x h h)
  )) ->
  (aloc_preserved_trans: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (x: aloc r a) ->
    (h1: HS.mem) ->
    (h2: HS.mem) ->
    (h3: HS.mem) ->
    Lemma
    (requires (aloc_preserved x h1 h2 /\ aloc_preserved x h2 h3))
    (ensures (aloc_preserved x h1 h3))
  )) ->
  (* if any reference at this address is preserved, then any location at this address is preserved *)
  (same_mreference_aloc_preserved: (
    (#r: HS.rid) ->
    (#a: nat) ->
    (b: aloc r a) ->
    (h1: HS.mem) ->
    (h2: HS.mem) ->
    (f: (
      (a' : Type0) ->
      (pre: Preorder.preorder a') ->
      (r': HS.mreference a' pre) ->
      Lemma
      (requires (h1 `HS.contains` r' /\ r == HS.frameOf r' /\ a == HS.as_addr r'))
      (ensures (h2 `HS.contains` r' /\ h1 `HS.sel` r' == h2 `HS.sel` r'))
    )) ->
    Lemma
    (aloc_preserved b h1 h2)
  )) ->
  cls aloc

val loc (#aloc: aloc_t u#x) (c: cls aloc) : Tot (Type u#x)

val loc_none (#aloc: aloc_t) (#c: cls aloc): Tot (loc c)

val loc_union
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2: loc c)
: GTot (loc c)

(** The following is useful to make Z3 cut matching loops with
modifies_trans and modifies_refl *)
val loc_union_idem
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_union s s == s)

val loc_union_comm
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2: loc c)
: Lemma
  (loc_union s1 s2 == loc_union s2 s1)

val loc_union_assoc
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2 s3: loc c)
: Lemma
  (loc_union s1 (loc_union s2 s3) == loc_union (loc_union s1 s2) s3)

val loc_union_loc_none_l
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_union loc_none s == s)

val loc_union_loc_none_r
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_union s loc_none == s)


val loc_of_aloc
  (#aloc: aloc_t) (#c: cls aloc)
  (#r: HS.rid)
  (#n: nat)
  (b: aloc r n)
: GTot (loc c)

val loc_of_aloc_not_none
  (#aloc: aloc_t) (#c: cls aloc)
  (#r: HS.rid)
  (#n: nat)
  (b: aloc r n)
: Lemma (loc_of_aloc #_ #c b == loc_none ==> False)

val loc_addresses
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
  (n: Set.set nat)
: GTot (loc c)

val loc_regions
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: Set.set HS.rid)
: GTot (loc c)

let loc_mreference
  (#aloc: aloc_t) (#c: cls aloc)
  (#a: Type)
  (#p: Preorder.preorder a)
  (b: HS.mreference a p)
: GTot (loc c)
= loc_addresses true (HS.frameOf b) (Set.singleton (HS.as_addr b))

let loc_freed_mreference
  (#aloc: aloc_t) (#c: cls aloc)
  (#a: Type)
  (#p: Preorder.preorder a)
  (b: HS.mreference a p)
: GTot (loc c)
= loc_addresses false (HS.frameOf b) (Set.singleton (HS.as_addr b))

let loc_region_only
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
: GTot (loc c)
= loc_regions preserve_liveness (Set.singleton r)

let loc_all_regions_from
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
: GTot (loc c)
= loc_regions preserve_liveness (HS.mod_set (Set.singleton r))


(* Inclusion of memory locations *)

val loc_includes
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2: loc c)
: GTot Type0

val loc_includes_refl
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_includes s s)

val loc_includes_trans
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2 s3: loc c)
: Lemma
  (requires (loc_includes s1 s2 /\ loc_includes s2 s3))
  (ensures (loc_includes s1 s3))

val loc_includes_union_r
  (#aloc: aloc_t) (#c: cls aloc)
  (s s1 s2: loc c)
: Lemma
  (requires (loc_includes s s1 /\ loc_includes s s2))
  (ensures (loc_includes s (loc_union s1 s2)))

val loc_includes_union_l
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2 s: loc c)
: Lemma
  (requires (loc_includes s1 s \/ loc_includes s2 s))
  (ensures (loc_includes (loc_union s1 s2) s))

val loc_includes_none
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (loc_includes s loc_none)

val loc_includes_none_elim
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (requires (loc_includes loc_none s))
  (ensures (s == loc_none))


val loc_includes_aloc
  (#aloc: aloc_t) (#c: cls aloc)
  (#r: HS.rid)
  (#n: nat)
  (b1 b2: aloc r n)
: Lemma
  (requires (c.aloc_includes b1 b2))
  (ensures (loc_includes (loc_of_aloc b1) (loc_of_aloc #_ #c b2)))

val loc_includes_aloc_elim
  (#aloc: aloc_t) (#c: cls aloc)
  (#r1 #r2: HS.rid)
  (#n1 #n2: nat)
  (b1: aloc r1 n1)
  (b2: aloc r2 n2)
: Lemma
  (requires (loc_includes (loc_of_aloc b1) (loc_of_aloc #_ #c b2)))
  (ensures (r1 == r2 /\ n1 == n2 /\ c.aloc_includes b1 b2))

val loc_includes_addresses_aloc
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (r: HS.rid)
  (s: Set.set nat)
  (#a: nat)
  (p: aloc r a)
: Lemma
  (requires (Set.mem a s))
  (ensures (loc_includes (loc_addresses preserve_liveness r s) (loc_of_aloc #_ #c p)))

val loc_includes_region_aloc
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (s: Set.set HS.rid)
  (#r: HS.rid)
  (#a: nat)
  (b: aloc r a)
: Lemma
  (requires (Set.mem r s))
  (ensures (loc_includes (loc_regions preserve_liveness s) (loc_of_aloc #_ #c b)))

val loc_includes_region_addresses
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness1 preserve_liveness2: bool)
  (s: Set.set HS.rid)
  (r: HS.rid)
  (a: Set.set nat)
: Lemma
  (requires (Set.mem r s))
  (ensures (loc_includes (loc_regions #_ #c preserve_liveness1 s) (loc_addresses preserve_liveness2 r a)))

val loc_includes_region_region
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness1 preserve_liveness2: bool)
  (s1 s2: Set.set HS.rid)
: Lemma
  (requires ((preserve_liveness1 ==> preserve_liveness2) /\ Set.subset s2 s1))
  (ensures (loc_includes (loc_regions #_ #c preserve_liveness1 s1) (loc_regions preserve_liveness2 s2)))

val loc_includes_region_union_l
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness: bool)
  (l: loc c)
  (s1 s2: Set.set HS.rid)
: Lemma
  (requires (loc_includes l (loc_regions preserve_liveness (Set.intersect s2 (Set.complement s1)))))
  (ensures (loc_includes (loc_union (loc_regions preserve_liveness s1) l) (loc_regions preserve_liveness s2)))

val loc_includes_addresses_addresses
  (#aloc: aloc_t) (c: cls aloc)
  (preserve_liveness1 preserve_liveness2: bool)
  (r: HS.rid)
  (a1 a2: Set.set nat)
: Lemma
  (requires ((preserve_liveness1 ==> preserve_liveness2) /\ Set.subset a2 a1))
  (ensures (loc_includes #_ #c (loc_addresses preserve_liveness1 r a1) (loc_addresses preserve_liveness2 r a2)))


(* Disjointness of two memory locations *)

val loc_disjoint
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2: loc c)
: GTot Type0

val loc_disjoint_sym
  (#aloc: aloc_t) (#c: cls aloc)
  (s1 s2: loc c)
: Lemma
  (requires (loc_disjoint s1 s2))
  (ensures (loc_disjoint s2 s1))

val loc_disjoint_none_r
  (#aloc: aloc_t) (#c: cls aloc)
  (s: loc c)
: Lemma
  (ensures (loc_disjoint s loc_none))

val loc_disjoint_union_r
  (#aloc: aloc_t) (#c: cls aloc)
  (s s1 s2: loc c)
: Lemma
  (requires (loc_disjoint s s1 /\ loc_disjoint s s2))
  (ensures (loc_disjoint s (loc_union s1 s2)))

val loc_disjoint_includes
  (#aloc: aloc_t) (#c: cls aloc)
  (p1 p2 p1' p2' : loc c)
: Lemma
  (requires (loc_includes p1 p1' /\ loc_includes p2 p2' /\ loc_disjoint p1 p2))
  (ensures (loc_disjoint p1' p2'))

val loc_disjoint_aloc_intro
  (#aloc: aloc_t) (#c: cls aloc)
  (#r1: HS.rid)
  (#a1: nat)
  (#r2: HS.rid)
  (#a2: nat)
  (b1: aloc r1 a1)
  (b2: aloc r2 a2)
: Lemma
  (requires ((r1 == r2 /\ a1 == a2) ==> c.aloc_disjoint b1 b2))
  (ensures (loc_disjoint (loc_of_aloc b1) (loc_of_aloc #_ #c b2)))

val loc_disjoint_aloc_elim
  (#aloc: aloc_t) (#c: cls aloc)
  (#r1: HS.rid)
  (#a1: nat)
  (#r2: HS.rid)
  (#a2: nat)
  (b1: aloc r1 a1)
  (b2: aloc r2 a2)
: Lemma
  (requires (loc_disjoint (loc_of_aloc b1) (loc_of_aloc #_ #c b2)))
  (ensures ((r1 == r2 /\ a1 == a2) ==> c.aloc_disjoint b1 b2))

val loc_disjoint_addresses_intro
  (#aloc: aloc_t) (#c: cls aloc)
  (preserve_liveness1 preserve_liveness2: bool)
  (r1 r2: HS.rid)
  (n1 n2: Set.set nat)
: Lemma
  (requires (r1 <> r2 \/ Set.subset (Set.intersect n1 n2) Set.empty))
  (ensures (loc_disjoint (loc_addresses #_ #c preserve_liveness1 r1 n1) (loc_addresses preserve_liveness2 r2 n2)))
val loc_disjoint_addresses : preserve_liveness1: Prims.bool ->
    preserve_liveness2: Prims.bool ->
    r1: FStar.Monotonic.HyperHeap.rid ->
    r2: FStar.Monotonic.HyperHeap.rid ->
    n1: FStar.Set.set Prims.nat ->
    n2: FStar.Set.set Prims.nat
  -> FStar.Pervasives.Lemma
      (requires r1 <> r2 \/ FStar.Set.subset (FStar.Set.intersect n1 n2) FStar.Set.empty)
      (ensures
        FStar.ModifiesGen.loc_disjoint (FStar.ModifiesGen.loc_addresses preserve_liveness1 r1 n1)
          (FStar.ModifiesGen.loc_addresses preserve_liveness2 r2 n2))

    preserve_liveness1: Prims.bool ->
    preserve_liveness2: Prims.bool ->
    r1: FStar.Monotonic.HyperHeap.rid ->
    r2: FStar.Monotonic.HyperHeap.rid ->
    n1: FStar.Set.set Prims.nat ->
    n2: FStar.Set.set Prims.nat
  -> FStar.Pervasives.Lemma
      (requires r1 <> r2 \/ FStar.Set.subset (FStar.Set.intersect n1 n2) FStar.Set.empty)
      (ensures
        FStar.ModifiesGen.loc_disjoint (FStar.ModifiesGen.loc_addresses preserve_liveness1 r1 n1)
          (FStar.ModifiesGen.loc_addresses preserve_liveness2 r2 n2))