val is_valid_state (e1: extern_ptr) (n1: SizeT.t) (e2: extern_ptr) (n2: SizeT.t) (b: bool)
    : Tot vprop
val is_valid_state (e1: extern_ptr) (n1: SizeT.t) (e2: extern_ptr) (n2: SizeT.t) (b: bool)
    : Tot vprop
let is_valid_state
  (e1: extern_ptr)
  (n1: SizeT.t)
  (e2: extern_ptr)
  (n2: SizeT.t)
  (b: bool)
: Tot vprop
= if b then is_valid_state_true e1 n1 e2 n2 else emp
module Zeta.Steel.ExternalPtr

// DO NOT FRIEND this module!

module A = Steel.ST.Array
module U32 = FStar.UInt32
module U8 = FStar.UInt8

open Steel.ST.Util

inline_for_extraction
val extern_ptr : Type0

[@@erasable]
noeq
type state =
| Unread: (out_len: SizeT.t) -> state
| Read: (out_len: SizeT.t) -> state
| Written: (written: Seq.seq U8.t) -> state

val extern_in_out_pts_to (e1: extern_ptr) (e2: extern_ptr) (in_contents: Seq.seq U8.t) (s: state) : vprop

[@@__reduce__]
let is_valid_state_true
  (e1: extern_ptr)
  (n1: SizeT.t)
  (e2: extern_ptr)
  (n2: SizeT.t)
: Tot vprop
= exists_ (fun in_contents ->
    extern_in_out_pts_to e1 e2 in_contents (Unread n2) `star`
    pure (SizeT.v n1 == Seq.length in_contents)
  )
/
Steel.ST.Util.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.ExternalPtr.fsti

    e1: Zeta.Steel.ExternalPtr.extern_ptr ->
    n1: FStar.SizeT.t ->
    e2: Zeta.Steel.ExternalPtr.extern_ptr ->
    n2: FStar.SizeT.t ->
    b: Prims.bool
  -> Steel.Effect.Common.vprop
Zeta.Steel.ExternalPtr.extern_ptr FStar.SizeT.t Prims.bool Zeta.Steel.ExternalPtr.is_valid_state_true Steel.Effect.Common.emp Steel.Effect.Common.vprop
let is_valid_state (e1: extern_ptr) (n1: SizeT.t) (e2: extern_ptr) (n2: SizeT.t) (b: bool)
    : Tot vprop =
  
if b then is_valid_state_true e1 n1 e2 n2 else emp