val handle_pts_to_body0 (r2: state_t) : Tot vprop
val handle_pts_to_body0 (r2: state_t) : Tot vprop
let handle_pts_to_body0
  (r2: state_t)
: Tot vprop
= exists_ (fun p3 ->
    R.pts_to r2.state p3 r2.tl_state `star`
    M.core_inv r2.tl_state
  )
module Zeta.Steel.SafeMain.Handle

module M = Zeta.Steel.Main
module AEH = Zeta.Steel.AggregateEpochHashes
module AT = Zeta.Steel.ApplicationTypes
module U16 = FStar.UInt16
module U32 = FStar.UInt32

module Lock = Steel.ST.SpinLock
module R = Steel.ST.Reference
module A = Steel.ST.Array

open Steel.ST.GenElim

noeq
type state_t = {
  state: R.ref (M.top_level_state false);
  tl_state: Ghost.erased (M.top_level_state false);
}
/
Zeta.Steel.Main.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.AggregateEpochHashes.fsti.checked Steel.ST.SpinLock.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.GenElim.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.SafeMain.Handle.fst
r2: Zeta.Steel.SafeMain.Handle.state_t -> Steel.Effect.Common.vprop
Zeta.Steel.SafeMain.Handle.state_t Steel.ST.Util.exists_ Steel.FractionalPermission.perm Steel.Effect.Common.star Steel.ST.Reference.pts_to Zeta.Steel.Main.top_level_state FStar.Ghost.hide Prims.bool Zeta.Steel.SafeMain.Handle.__proj__Mkstate_t__item__state FStar.Ghost.reveal Zeta.Steel.SafeMain.Handle.__proj__Mkstate_t__item__tl_state Zeta.Steel.Main.core_inv Steel.Effect.Common.vprop
let handle_pts_to_body0 (r2: state_t) : Tot vprop =
  
exists_ (fun p3 -> (R.pts_to r2.state p3 r2.tl_state) `star` (M.core_inv r2.tl_state))