val gather_body (#opened: _) (r2: state_t)
    : STGhostT unit
      opened
      ((handle_pts_to_body r2) `star` (handle_pts_to_body r2))
      (fun _ -> handle_pts_to_body r2)
val gather_body (#opened: _) (r2: state_t)
    : STGhostT unit
      opened
      ((handle_pts_to_body r2) `star` (handle_pts_to_body r2))
      (fun _ -> handle_pts_to_body r2)
let gather_body
  (#opened: _)
  (r2: state_t)
: STGhostT unit opened
    (handle_pts_to_body r2 `star` handle_pts_to_body r2)
    (fun _ -> handle_pts_to_body r2)
= rewrite (handle_pts_to_body r2) (handle_pts_to_body0 r2);
  let _ = gen_elim () in
  let ps = vpattern_replace (fun ps -> R.pts_to r2.state ps _) in
  rewrite (handle_pts_to_body r2) (handle_pts_to_body0 r2);
  let _ = gen_elim () in
  R.gather ps r2.state;
  M.core_inv_gather _;
  rewrite (handle_pts_to_body0 r2) (handle_pts_to_body r2)
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);
}

[@@__reduce__]
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
  )

let handle_pts_to_body
  (r2: state_t)
: Tot vprop
= handle_pts_to_body0 r2
/
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.ST.Effect.Ghost.STGhostT Prims.unit
Steel.Memory.inames Zeta.Steel.SafeMain.Handle.state_t Steel.ST.Util.rewrite Zeta.Steel.SafeMain.Handle.handle_pts_to_body0 Zeta.Steel.SafeMain.Handle.handle_pts_to_body Prims.unit Zeta.Steel.Main.core_inv_gather FStar.Ghost.hide Prims.bool FStar.Ghost.reveal Zeta.Steel.Main.top_level_state Zeta.Steel.SafeMain.Handle.__proj__Mkstate_t__item__tl_state Steel.ST.Reference.gather Steel.FractionalPermission.perm Zeta.Steel.SafeMain.Handle.__proj__Mkstate_t__item__state FStar.Ghost.erased Steel.ST.GenElim.gen_elim Steel.Effect.Common.VStar Steel.ST.Reference.pts_to Zeta.Steel.Main.core_inv Steel.ST.Util.exists_ Steel.Effect.Common.vprop Steel.Effect.Common.star Prims.l_and Prims.l_True Prims.prop Steel.ST.Util.vpattern_replace
let gather_body (#opened: _) (r2: state_t)
    : STGhostT unit
      opened
      ((handle_pts_to_body r2) `star` (handle_pts_to_body r2))
      (fun _ -> handle_pts_to_body r2) =
  
rewrite (handle_pts_to_body r2) (handle_pts_to_body0 r2);
let _ = gen_elim () in
let ps = vpattern_replace (fun ps -> R.pts_to r2.state ps _) in
rewrite (handle_pts_to_body r2) (handle_pts_to_body0 r2);
let _ = gen_elim () in
R.gather ps r2.state;
M.core_inv_gather _;
rewrite (handle_pts_to_body0 r2) (handle_pts_to_body r2)