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))
let loc_includes_none_elim #al #c s =
  assert (s `loc_equal` 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))
let loc_includes_none_elim #al #c s =
assert (s `loc_equal` loc_none)
FStar.ModifiesGen.fst.checked
prims.fst.checked FStar.Universe.fsti.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.SMT.fst.checked FStar.Tactics.Effect.fsti.checked FStar.StrongExcludedMiddle.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.GSet.fsti.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
FStar.ModifiesGen.fst
FStar.ModifiesGen.aloc_t FStar.ModifiesGen.cls FStar.ModifiesGen.loc Prims._assert FStar.ModifiesGen.loc_equal FStar.ModifiesGen.loc_none Prims.unit
(*
   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

#set-options "--split_queries no"
#set-options "--using_facts_from '*,-FStar.Tactics,-FStar.Reflection,-FStar.List'"

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

noeq
type aloc (#al: aloc_t) (c: cls al) = | ALoc:
  (region: HS.rid) ->
  (addr: nat) ->
  (loc: option (al region addr)) ->
  aloc c

let aloc_domain (#al: aloc_t) (c: cls al) (regions: Ghost.erased (Set.set HS.rid)) (addrs: ((r: HS.rid { Set.mem r (Ghost.reveal regions) } ) -> GTot (GSet.set nat))) : GTot (GSet.set (aloc c)) =
  GSet.comprehend (fun a -> Set.mem a.region (Ghost.reveal regions) && GSet.mem a.addr (addrs a.region))

module F = FStar.FunctionalExtensionality

[@@(unifier_hint_injective)]
let i_restricted_g_t = F.restricted_g_t

let addrs_dom regions =
    (r: HS.rid { Set.mem r (Ghost.reveal regions) } )

let non_live_addrs_codom
      (regions: Ghost.erased (Set.set HS.rid))
      (region_liveness_tags: Ghost.erased (Set.set HS.rid) { Ghost.reveal region_liveness_tags `Set.subset` Ghost.reveal regions } )
      (r:addrs_dom regions) =
      (y: GSet.set nat { r `Set.mem` (Ghost.reveal region_liveness_tags) ==> GSet.subset (GSet.complement GSet.empty) y })

let live_addrs_codom
      (regions: Ghost.erased (Set.set HS.rid))
      (region_liveness_tags: Ghost.erased (Set.set HS.rid) { Ghost.reveal region_liveness_tags `Set.subset` Ghost.reveal regions } )
      (non_live_addrs:
        i_restricted_g_t
          (addrs_dom regions)
          (non_live_addrs_codom regions region_liveness_tags))
      (r:addrs_dom regions) = (y: GSet.set nat { GSet.subset (non_live_addrs r) y } )

noeq
type loc' (#al: aloc_t u#x) (c: cls al) : Type u#x =
  | Loc:
      (regions: Ghost.erased (Set.set HS.rid)) ->
      (region_liveness_tags: Ghost.erased (Set.set HS.rid) { Ghost.reveal region_liveness_tags `Set.subset` Ghost.reveal regions } ) ->
      (non_live_addrs:
        i_restricted_g_t
          (addrs_dom regions)
          (non_live_addrs_codom regions region_liveness_tags)) ->
      (live_addrs:
        i_restricted_g_t
          (addrs_dom regions)
          (live_addrs_codom regions region_liveness_tags non_live_addrs)) ->
      (aux: Ghost.erased (GSet.set (aloc c)) {
        aloc_domain c regions live_addrs `GSet.subset` Ghost.reveal aux /\
        Ghost.reveal aux `GSet.subset` (aloc_domain c regions (fun _ -> GSet.complement GSet.empty))
      } ) ->
      loc' c

let loc = loc'

let mk_non_live_addrs (#regions:_) (#region_liveness_tags:_)
                      (f: (x:addrs_dom regions -> GTot (non_live_addrs_codom regions region_liveness_tags x)))
    : i_restricted_g_t
          (addrs_dom regions)
          (non_live_addrs_codom regions region_liveness_tags) =
    F.on_dom_g _ f

let mk_live_addrs (#regions:_) (#region_liveness_tags:_)
                  (#non_live_addrs_codom: _)
                  (f: (x:addrs_dom regions -> GTot (live_addrs_codom regions region_liveness_tags non_live_addrs_codom x)))
    : i_restricted_g_t
          (addrs_dom regions)
          (live_addrs_codom regions region_liveness_tags non_live_addrs_codom) =
    F.on_dom_g _ f

let loc_none #a #c =
  Loc
    (Ghost.hide (Set.empty))
    (Ghost.hide (Set.empty))
    (mk_non_live_addrs (fun _ -> GSet.empty))
    (mk_live_addrs (fun _ -> GSet.empty))
    (Ghost.hide GSet.empty)

let regions_of_loc
  (#al: aloc_t) (#c: cls al)
  (s: loc c)
: GTot (Set.set HS.rid)
= Ghost.reveal (Loc?.regions s)

let addrs_of_loc_liveness_not_preserved
  (#al: aloc_t) (#c: cls al)
  (l: loc c)
  (r: HS.rid)
: GTot (GSet.set nat)
= if Set.mem r (regions_of_loc l)
  then Loc?.non_live_addrs l r
  else GSet.empty

let addrs_of_loc_weak
  (#al: aloc_t) (#c: cls al)
  (l: loc c)
  (r: HS.rid)
: GTot (GSet.set nat)
= if Set.mem r (regions_of_loc l)
  then Loc?.live_addrs l r
  else GSet.empty

let addrs_of_loc_aux_pred
  (#al: aloc_t) (#c: cls al)
  (l: loc c)
  (r: HS.rid)
  (addr: nat)
: GTot bool
= StrongExcludedMiddle.strong_excluded_middle (exists a . GSet.mem a (Ghost.reveal (Loc?.aux l)) /\ a.region == r /\ a.addr == addr)

let addrs_of_loc_aux
  (#al: aloc_t) (#c: cls al)
  (l: loc c)
  (r: HS.rid)
: GTot (y: GSet.set nat { GSet.subset (GSet.intersect y (addrs_of_loc_weak l r)) GSet.empty } )
= GSet.comprehend (addrs_of_loc_aux_pred l r)
    `GSet.intersect` (GSet.complement (addrs_of_loc_weak l r))

let addrs_of_loc
  (#al: aloc_t) (#c: cls al)
  (l: loc c)
  (r: HS.rid)
: GTot (GSet.set nat)
= GSet.union
    (addrs_of_loc_weak l r)
    (addrs_of_loc_aux l r)

let addrs_of_loc_aux_prop
  (#al: aloc_t) (#c: cls al)
  (l: loc c)
  (r: HS.rid)
: Lemma
  (GSet.subset (GSet.intersect (addrs_of_loc_aux l r) (addrs_of_loc_weak l r)) GSet.empty)
  [SMTPatOr [
    [SMTPat (addrs_of_loc_aux l r)];
    [SMTPat (addrs_of_loc_weak l r)];
    [SMTPat (addrs_of_loc l r)];
  ]]
= ()

let loc_union #al #c s1 s2 =
  let regions1 = Ghost.reveal (Loc?.regions s1) in
  let regions2 = Ghost.reveal (Loc?.regions s2) in
  let regions = Set.union regions1 regions2 in
  let region_liveness_tags : Ghost.erased (Set.set HS.rid) = (Ghost.hide (Set.union (Ghost.reveal (Loc?.region_liveness_tags s1)) (Ghost.reveal (Loc?.region_liveness_tags s2)))) in
  let gregions = Ghost.hide regions in
  let non_live_addrs =
    F.on_dom_g (addrs_dom gregions) #(non_live_addrs_codom gregions region_liveness_tags)
    (fun r ->
    GSet.union
      (if Set.mem r regions1 then Loc?.non_live_addrs s1 r else GSet.empty)
      (if Set.mem r regions2 then Loc?.non_live_addrs s2 r else GSet.empty))
  in
  let live_addrs =
    F.on_dom_g (addrs_dom gregions) #(live_addrs_codom gregions region_liveness_tags non_live_addrs)
      (fun r ->
        GSet.union
          (if Set.mem r regions1 then addrs_of_loc_weak s1 r else GSet.empty)
          (if Set.mem r regions2 then addrs_of_loc_weak s2 r else GSet.empty))
  in
  let aux = Ghost.hide
      (Ghost.reveal (Loc?.aux s1) `GSet.union` Ghost.reveal (Loc?.aux s2))
  in
  Loc
    (Ghost.hide regions)
    region_liveness_tags
    non_live_addrs
    live_addrs
    aux

let fun_set_equal (#t: Type) (#t': Type)
                  (#p:(t -> GSet.set t' -> Type))
                  (f1 f2: i_restricted_g_t t (fun x -> g:GSet.set t'{p x g})) :Tot Type0 =
  forall (x: t) . {:pattern (f1 x) \/ (f2 x) } f1 x `GSet.equal` f2 x

let fun_set_equal_elim (#t: Type) (#t': Type)
                       (#p:(t -> GSet.set t' -> Type))
                       (f1 f2: i_restricted_g_t t (fun x -> g:GSet.set t'{p x g})) : Lemma
  (requires (fun_set_equal f1 f2))
  (ensures (f1 == f2))
//  [SMTPat (fun_set_equal f1 f2)]
= assert (f1 `FunctionalExtensionality.feq_g` f2)

let loc_equal (#al: aloc_t) (#c: cls al) (s1 s2: loc c) : GTot Type0 =
  let Loc regions1 region_liveness_tags1 _ _ aux1 = s1 in
  let Loc regions2 region_liveness_tags2 _ _ aux2 = s2 in
  Ghost.reveal regions1 `Set.equal` Ghost.reveal regions2 /\
  Ghost.reveal region_liveness_tags1 `Set.equal` Ghost.reveal region_liveness_tags2 /\
  fun_set_equal (Loc?.non_live_addrs s1) (Loc?.non_live_addrs s2) /\
  fun_set_equal (Loc?.live_addrs s1) (Loc?.live_addrs s2) /\
  Ghost.reveal (Loc?.aux s1) `GSet.equal` Ghost.reveal (Loc?.aux s2)

let loc_equal_elim (#al: aloc_t) (#c: cls al) (s1 s2: loc c) : Lemma
  (requires (loc_equal s1 s2))
  (ensures (s1 == s2))
  [SMTPat (s1 `loc_equal` s2)]
= fun_set_equal_elim (Loc?.non_live_addrs s1) (Loc?.non_live_addrs s2);
  fun_set_equal_elim (Loc?.live_addrs s1) (Loc?.live_addrs s2)


let loc_union_idem #al #c s =
  assert (loc_union s s `loc_equal` s)

let loc_union_comm #al #c s1 s2 =
  assert (loc_union s1 s2 `loc_equal` loc_union s2 s1)

let loc_union_assoc #al #c s1 s2 s3 =
  assert (loc_union s1 (loc_union s2 s3) `loc_equal` loc_union (loc_union s1 s2) s3)

let loc_union_loc_none_l #al #c s =
  assert (loc_union loc_none s `loc_equal` s)

let loc_union_loc_none_r #al #c s =
  assert (loc_union s loc_none `loc_equal` s)

let loc_of_aloc #al #c #r #n b =
  let regions =        (Ghost.hide (Set.singleton r)) in
  let region_liveness_tags = (Ghost.hide (Set.empty)) in
  Loc
    regions
    region_liveness_tags
    (mk_non_live_addrs (fun _ -> GSet.empty))
    (mk_live_addrs (fun _ -> GSet.empty))
    (Ghost.hide (GSet.singleton (ALoc r n (Some b))))

let loc_of_aloc_not_none #al #c #r #n b = ()

let loc_addresses #al #c preserve_liveness r n =
  let regions = (Ghost.hide (Set.singleton r)) in
  Loc
    regions
    (Ghost.hide Set.empty)
    (mk_non_live_addrs (fun _ -> if preserve_liveness then GSet.empty else GSet.of_set n))
    (mk_live_addrs (fun _ -> GSet.of_set n))
    (Ghost.hide (aloc_domain c regions (fun _ -> GSet.of_set n)))

let loc_regions_region_liveness_tags (preserve_liveness: bool) (r: Set.set HS.rid) : Tot (Ghost.erased (Set.set HS.rid)) =
  if preserve_liveness then Ghost.hide Set.empty else Ghost.hide r

let loc_regions #al #c preserve_liveness r =
  let region_liveness_tags = loc_regions_region_liveness_tags preserve_liveness r in
  let addrs (r' : HS.rid { Set.mem r' r } ) : GTot (y: GSet.set nat { r' `Set.mem` (Ghost.reveal region_liveness_tags) ==> GSet.subset (GSet.complement GSet.empty) y } ) =
    GSet.complement GSet.empty
  in
  let live_addrs (r' : HS.rid { Set.mem r' r } ) : GTot (y: GSet.set nat { addrs r' `GSet.subset` y } ) =
    addrs r'
  in
  Loc
    (Ghost.hide r)
    region_liveness_tags
    (mk_non_live_addrs addrs)
    (mk_live_addrs live_addrs)
    (Ghost.hide (aloc_domain c (Ghost.hide r) addrs))

let aloc_includes (#al: aloc_t) (#c: cls al) (b0 b: aloc c) : GTot Type0 =
  b0.region == b.region /\ b0.addr == b.addr /\ Some? b0.loc == Some? b.loc /\ (if Some? b0.loc && Some? b.loc then c.aloc_includes (Some?.v b0.loc) (Some?.v b.loc) else True)

let loc_aux_includes_buffer
  (#al: aloc_t) (#c: cls al)
  (s: GSet.set (aloc c))
  (b: aloc c)
: GTot Type0
  (decreases s)
= exists (b0 : aloc c) . b0 `GSet.mem` s /\ b0 `aloc_includes` b

let loc_aux_includes
  (#al: aloc_t) (#c: cls al)
  (s1 s2: GSet.set (aloc c))
: GTot Type0
  (decreases s2)
= forall (b2: aloc c) . GSet.mem b2 s2 ==> loc_aux_includes_buffer s1 b2

let loc_aux_includes_union_l
  (#al: aloc_t) (#c: cls al)
  (s1 s2 s: GSet.set (aloc c))
: Lemma
  (requires (loc_aux_includes s1 s \/ loc_aux_includes s2 s))
  (ensures (loc_aux_includes (GSet.union s1 s2) s))
  (decreases s)
= ()

let loc_aux_includes_refl
  (#al: aloc_t) (#c: cls al)
  (s: GSet.set (aloc c))
: Lemma
  (loc_aux_includes s s)
= Classical.forall_intro_3 (fun r a b -> c.aloc_includes_refl #r #a b)

let loc_aux_includes_subset
  (#al: aloc_t) (#c: cls al)
  (s1 s2: GSet.set (aloc c))
: Lemma
  (requires (s1 `GSet.subset` s2))
  (ensures (loc_aux_includes s2 s1))
= Classical.forall_intro_3 (fun r a b -> c.aloc_includes_refl #r #a b)

let loc_aux_includes_subset'
  (#al: aloc_t) (#c: cls al)
  (s1 s2: GSet.set (aloc c))
: Lemma
  (requires (s1 `GSet.subset` s2))
  (ensures (loc_aux_includes s2 s1))
  [SMTPatOr [
    [SMTPat (s1 `GSet.subset` s2)];
    [SMTPat (loc_aux_includes s2 s1)];
  ]]
= loc_aux_includes_subset s1 s2

let loc_aux_includes_union_l_r
  (#al: aloc_t) (#c: cls al)
  (s s': GSet.set (aloc c))
: Lemma
  (loc_aux_includes (GSet.union s s') s)
= loc_aux_includes_refl s;
  loc_aux_includes_union_l s s' s

let loc_aux_includes_union_l_l
  (#al: aloc_t) (#c: cls al)
  (s s': GSet.set (aloc c))
: Lemma
  (loc_aux_includes (GSet.union s' s) s)
= loc_aux_includes_refl s;
  loc_aux_includes_union_l s' s s

let loc_aux_includes_buffer_includes
  (#al: aloc_t) (#c: cls al)
  (s: GSet.set (aloc c))
  (b1 b2: aloc c)
: Lemma
  (requires (loc_aux_includes_buffer s b1 /\ b1 `aloc_includes` b2))
  (ensures (loc_aux_includes_buffer s b2))
= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3))

let loc_aux_includes_loc_aux_includes_buffer
  (#al: aloc_t) (#c: cls al)
  (s1 s2: GSet.set (aloc c))
  (b: aloc c)
: Lemma
  (requires (loc_aux_includes s1 s2 /\ loc_aux_includes_buffer s2 b))
  (ensures (loc_aux_includes_buffer s1 b))
= Classical.forall_intro_3 (fun s b1 b2 -> Classical.move_requires (loc_aux_includes_buffer_includes #al #c s b1) b2)

let loc_aux_includes_trans
  (#al: aloc_t) (#c: cls al)
  (s1 s2 s3: GSet.set (aloc c))
: Lemma
  (requires (loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3))
  (ensures (loc_aux_includes s1 s3))
= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3))

let addrs_of_loc_weak_loc_union
  (#al: aloc_t) (#c: cls al)
  (l1 l2: loc c)
  (r: HS.rid)
: Lemma
  (addrs_of_loc_weak (loc_union l1 l2) r == GSet.union (addrs_of_loc_weak l1 r) (addrs_of_loc_weak l2 r))
  [SMTPat (addrs_of_loc_weak (loc_union l1 l2) r)]
= assert (GSet.equal (addrs_of_loc_weak (loc_union l1 l2) r) (GSet.union (addrs_of_loc_weak l1 r) (addrs_of_loc_weak l2 r)))

let addrs_of_loc_union
  (#al: aloc_t) (#c: cls al)
  (l1 l2: loc c)
  (r: HS.rid)
: Lemma
  (addrs_of_loc (loc_union l1 l2) r == GSet.union (addrs_of_loc l1 r) (addrs_of_loc l2 r))
  [SMTPat (addrs_of_loc (loc_union l1 l2) r)]
= assert (GSet.equal (addrs_of_loc (loc_union l1 l2) r) (GSet.union (addrs_of_loc l1 r) (addrs_of_loc l2 r)))

unfold
let loc_includes' #al (#c: cls al) (s1 s2: loc c) =
  let regions1 = Ghost.reveal (Loc?.regions s1) in
  let regions2 = Ghost.reveal (Loc?.regions s2) in (
    Set.subset regions2 regions1 /\
    Set.subset (Ghost.reveal (Loc?.region_liveness_tags s2)) (Ghost.reveal (Loc?.region_liveness_tags s1)) /\
    (
      forall (r: HS.rid { Set.mem r regions2 } ) .
      GSet.subset (Loc?.non_live_addrs s2 r) (Loc?.non_live_addrs s1 r)
    ) /\
    (
      forall (r: HS.rid) .
      GSet.subset (addrs_of_loc_weak s2 r) (addrs_of_loc_weak s1 r)
    ) /\ (
      forall (r: HS.rid) .
      GSet.subset (addrs_of_loc s2 r) (addrs_of_loc s1 r)
    ) /\ (
      (Ghost.reveal (Loc?.aux s1)) `loc_aux_includes` (Ghost.reveal (Loc?.aux s2))
    )
  )

let loc_includes #al #c s1 s2 =
  loc_includes' s1 s2

let loc_includes_refl #al #c s =
  loc_aux_includes_refl (Ghost.reveal (Loc?.aux s))

let loc_includes_refl'
  (#al: aloc_t) (#c: cls al)
  (s: loc c)
: Lemma
  (loc_includes s s)
  [SMTPat (loc_includes s s)]
= loc_includes_refl s

let loc_includes_trans #al #c s1 s2 s3 =
  loc_aux_includes_trans (Ghost.reveal (Loc?.aux s1)) (Ghost.reveal (Loc?.aux s2)) (Ghost.reveal (Loc?.aux s3))

let loc_includes_union_r #al #c s s1 s2 = ()

let loc_includes_union_l #al #c s1 s2 s =
  let u12 = loc_union s1 s2 in
    Classical.or_elim
      #(loc_includes s1 s)
      #(loc_includes s2 s)
      #(fun _ -> loc_includes (loc_union s1 s2) s)
      (fun _ ->
        loc_aux_includes_union_l_r (Ghost.reveal (Loc?.aux s1)) (Ghost.reveal (Loc?.aux s2));
        assert (loc_includes (loc_union s1 s2) s1);
        loc_includes_trans u12 s1 s)
      (fun _ ->
        loc_aux_includes_union_l_l (Ghost.reveal (Loc?.aux s2)) (Ghost.reveal (Loc?.aux s1));
        assert (loc_includes (loc_union s1 s2) s2);
        loc_includes_trans u12 s2 s)

let loc_includes_none #al #c s = ()
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))
s: FStar.ModifiesGen.loc c
  -> FStar.Pervasives.Lemma (requires FStar.ModifiesGen.loc_includes FStar.ModifiesGen.loc_none s)
      (ensures s == FStar.ModifiesGen.loc_none)