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 } )
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})
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.Ghost.erased FStar.Set.set FStar.Monotonic.HyperHeap.rid FStar.Set.subset FStar.Ghost.reveal FStar.ModifiesGen.i_restricted_g_t FStar.ModifiesGen.addrs_dom FStar.ModifiesGen.non_live_addrs_codom FStar.GSet.set Prims.nat FStar.GSet.subset
(*
   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)
val live_addrs_codom : regions: FStar.Ghost.erased (FStar.Set.set FStar.Monotonic.HyperHeap.rid) ->
    region_liveness_tags:
      FStar.Ghost.erased (FStar.Set.set FStar.Monotonic.HyperHeap.rid)
        {FStar.Set.subset (FStar.Ghost.reveal region_liveness_tags) (FStar.Ghost.reveal regions)} ->
    non_live_addrs:
      FStar.ModifiesGen.i_restricted_g_t (FStar.ModifiesGen.addrs_dom regions)
        (FStar.ModifiesGen.non_live_addrs_codom regions region_liveness_tags) ->
    r: FStar.ModifiesGen.addrs_dom regions
  -> Type0

    regions: FStar.Ghost.erased (FStar.Set.set FStar.Monotonic.HyperHeap.rid) ->
    region_liveness_tags:
      FStar.Ghost.erased (FStar.Set.set FStar.Monotonic.HyperHeap.rid)
        {FStar.Set.subset (FStar.Ghost.reveal region_liveness_tags) (FStar.Ghost.reveal regions)} ->
    non_live_addrs:
      FStar.ModifiesGen.i_restricted_g_t (FStar.ModifiesGen.addrs_dom regions)
        (FStar.ModifiesGen.non_live_addrs_codom regions region_liveness_tags) ->
    r: FStar.ModifiesGen.addrs_dom regions
  -> Type0