val inv_p:vprop
val inv_p:vprop
let inv_p : vprop =
  exists* (v_done:bool) (v_res:option int) (v_claimed:bool).
       pts_to done #one_half v_done
    ** pts_to res #one_half v_res
    ** GR.pts_to claimed #one_half v_claimed
    ** (if not v_claimed then pts_to res #one_half v_res else emp)
    ** pure (v_claimed ==> v_done)
    ** pure (v_done ==> Some? v_res)
(*
   Copyright 2023 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 Promises.Examples3

open Pulse.Lib.Pervasives
open Pulse.Lib.Par.Pledge
open Pulse.Lib.InvList
module GR = Pulse.Lib.GhostReference

assume val done : ref bool
assume val res : ref (option int)
assume val claimed : GR.ref bool
/
Pulse.Lib.Pervasives.fst.checked Pulse.Lib.Par.Pledge.fsti.checked Pulse.Lib.InvList.fsti.checked Pulse.Lib.GhostReference.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Promises.Examples3.fst
Pulse.Lib.Core.vprop
Pulse.Lib.Core.op_exists_Star Prims.bool FStar.Pervasives.Native.option Prims.int Pulse.Lib.Core.op_Star_Star Pulse.Lib.Reference.pts_to Promises.Examples3.done Pulse.Lib.Core.one_half Promises.Examples3.res Pulse.Lib.GhostReference.pts_to Promises.Examples3.claimed Prims.op_Negation Pulse.Lib.Core.emp Pulse.Lib.Core.vprop Pulse.Lib.Core.pure Prims.l_imp Prims.b2t FStar.Pervasives.Native.uu___is_Some
let inv_p:vprop =
  
exists* (v_done: bool) (v_res: option int) (v_claimed: bool).
  ((((pts_to done #one_half v_done ** pts_to res #one_half v_res) **
  GR.pts_to claimed #one_half v_claimed) **
  (if not v_claimed then pts_to res #one_half v_res else emp)) **
  pure (v_claimed ==> v_done)) **
  pure (v_done ==> Some? v_res)