val assert_null (#t: Type) (#opened: _) (#td: typedef t) (#v: Ghost.erased t) (p: ptr td)
    : STGhost unit opened (pts_to_or_null p v) (fun _ -> emp) (p == null _) (fun _ -> True)
let assert_null
  (#t: Type)
  (#opened: _)
  (#td: typedef t)
  (#v: Ghost.erased t)
  (p: ptr td)
: STGhost unit opened
    (pts_to_or_null p v)
    (fun _ -> emp)
    (p == null _)
    (fun _ -> True)
= rewrite (pts_to_or_null p v) emp
val assert_null (#t: Type) (#opened: _) (#td: typedef t) (#v: Ghost.erased t) (p: ptr td)
    : STGhost unit opened (pts_to_or_null p v) (fun _ -> emp) (p == null _) (fun _ -> True)
let assert_null (#t: Type) (#opened: _) (#td: typedef t) (#v: Ghost.erased t) (p: ptr td)
    : STGhost unit opened (pts_to_or_null p v) (fun _ -> emp) (p == null _) (fun _ -> True) =
rewrite (pts_to_or_null p v) emp
Steel.ST.C.Types.Base.fsti.checked
Steel.ST.Util.fsti.checked Steel.FractionalPermission.fst.checked prims.fst.checked FStar.StrongExcludedMiddle.fst.checked FStar.Real.fsti.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.C.Types.Base.fsti
Steel.Memory.inames Steel.ST.C.Types.Base.typedef FStar.Ghost.erased Steel.ST.C.Types.Base.ptr Steel.ST.Util.rewrite Steel.ST.C.Types.Base.pts_to_or_null Steel.Effect.Common.emp Prims.unit Steel.Effect.Common.vprop Prims.eq2 Steel.ST.C.Types.Base.null Prims.l_True
module Steel.ST.C.Types.Base
open Steel.ST.Util

module P = Steel.FractionalPermission

/// Helper to compose two permissions into one
val prod_perm (p1 p2: P.perm) : Pure P.perm
  (requires True)
  (ensures (fun p ->
    ((p1 `P.lesser_equal_perm` P.full_perm /\ p2 `P.lesser_equal_perm` P.full_perm) ==>
    p `P.lesser_equal_perm` P.full_perm) /\
    p.v == (let open FStar.Real in p1.v *. p2.v)
  ))

[@@noextract_to "krml"] // proof-only
val typedef (t: Type0) : Type0

inline_for_extraction [@@noextract_to "krml"]
let typeof (#t: Type0) (td: typedef t) : Tot Type0 = t

val fractionable (#t: Type0) (td: typedef t) (x: t) : GTot prop

val mk_fraction (#t: Type0) (td: typedef t) (x: t) (p: P.perm) : Ghost t
  (requires (fractionable td x))
  (ensures (fun y -> p `P.lesser_equal_perm` P.full_perm ==> fractionable td y))

val mk_fraction_full (#t: Type0) (td: typedef t) (x: t) : Lemma
  (requires (fractionable td x))
  (ensures (mk_fraction td x P.full_perm == x))
  [SMTPat (mk_fraction td x P.full_perm)]

val mk_fraction_compose (#t: Type0) (td: typedef t) (x: t) (p1 p2: P.perm) : Lemma
  (requires (fractionable td x /\ p1 `P.lesser_equal_perm` P.full_perm /\ p2 `P.lesser_equal_perm` P.full_perm))
  (ensures (mk_fraction td (mk_fraction td x p1) p2 == mk_fraction td x (p1 `prod_perm` p2)))

val full (#t: Type0) (td: typedef t) (v: t) : GTot prop

val uninitialized (#t: Type0) (td: typedef t) : Ghost t
  (requires True)
  (ensures (fun y -> full td y /\ fractionable td y))

val unknown (#t: Type0) (td: typedef t) : Ghost t
  (requires True)
  (ensures (fun y -> fractionable td y))

val full_not_unknown
  (#t: Type)
  (td: typedef t)
  (v: t)
: Lemma
  (requires (full td v))
  (ensures (~ (v == unknown td)))
  [SMTPat (full td v)]

val mk_fraction_unknown (#t: Type0) (td: typedef t) (p: P.perm) : Lemma
  (ensures (mk_fraction td (unknown td) p == unknown td))

val mk_fraction_eq_unknown (#t: Type0) (td: typedef t) (v: t) (p: P.perm) : Lemma
  (requires (fractionable td v /\ mk_fraction td v p == unknown td))
  (ensures (v == unknown td))


// To be extracted as: void*

[@@noextract_to "krml"] // primitive
val void_ptr : Type0
 
// To be extracted as: NULL
[@@noextract_to "krml"] // primitive
val void_null: void_ptr

// To be extracted as: *t
[@@noextract_to "krml"] // primitive
val ptr_gen ([@@@unused] t: Type) : Type0
[@@noextract_to "krml"] // primitive
val null_gen (t: Type) : Tot (ptr_gen t)

val ghost_void_ptr_of_ptr_gen (#[@@@unused] t: Type) (x: ptr_gen t) : GTot void_ptr
val ghost_ptr_gen_of_void_ptr (x: void_ptr) ([@@@unused] t: Type) : GTot (ptr_gen t)

val ghost_void_ptr_of_ptr_gen_of_void_ptr
  (x: void_ptr)
  (t: Type)
: Lemma
  (ghost_void_ptr_of_ptr_gen (ghost_ptr_gen_of_void_ptr x t) == x)
  [SMTPat (ghost_void_ptr_of_ptr_gen (ghost_ptr_gen_of_void_ptr x t))]

val ghost_ptr_gen_of_void_ptr_of_ptr_gen
  (#t: Type)
  (x: ptr_gen t)
: Lemma
  (ghost_ptr_gen_of_void_ptr (ghost_void_ptr_of_ptr_gen x) t == x)
  [SMTPat (ghost_ptr_gen_of_void_ptr (ghost_void_ptr_of_ptr_gen x) t)]

inline_for_extraction [@@noextract_to "krml"] // primitive
let ptr (#t: Type) (td: typedef t) : Tot Type0 = ptr_gen t
inline_for_extraction [@@noextract_to "krml"] // primitive
let null (#t: Type) (td: typedef t) : Tot (ptr td) = null_gen t

inline_for_extraction [@@noextract_to "krml"]
let ref (#t: Type) (td: typedef t) : Tot Type0 = (p: ptr td { ~ (p == null td) })

val pts_to (#t: Type) (#td: typedef t) (r: ref td) ([@@@smt_fallback] v: Ghost.erased t) : vprop

let pts_to_or_null
  (#t: Type) (#td: typedef t) (p: ptr td) (v: Ghost.erased t) : vprop
= if FStar.StrongExcludedMiddle.strong_excluded_middle (p == null _)
  then emp
  else pts_to p v

[@@noextract_to "krml"] // primitive
val is_null
  (#t: Type)
  (#opened: _)
  (#td: typedef t)
  (#v: Ghost.erased t)
  (p: ptr td)
: STAtomicBase bool false opened Unobservable
    (pts_to_or_null p v)
    (fun _ -> pts_to_or_null p v)
    (True)
    (fun res -> res == true <==> p == null _)

let assert_null
  (#t: Type)
  (#opened: _)
  (#td: typedef t)
  (#v: Ghost.erased t)
  (p: ptr td)
: STGhost unit opened
    (pts_to_or_null p v)
    (fun _ -> emp)
    (p == null _)
val assert_null (#t: Type) (#opened: _) (#td: typedef t) (#v: Ghost.erased t) (p: ptr td)
    : STGhost unit opened (pts_to_or_null p v) (fun _ -> emp) (p == null _) (fun _ -> True)
p: Steel.ST.C.Types.Base.ptr td -> Steel.ST.Effect.Ghost.STGhost Prims.unit