val has_array_of_base_inj
      (#t: Type)
      (#tn: Type0)
      (#n: array_size_t)
      (#td: typedef t)
      (r: ref (base_array0 tn td n))
      (a1 a2: array td)
    : Lemma
      (requires (has_array_of_base #t #tn #n #td r a1 /\ has_array_of_base #t #tn #n #td r a2))
      (ensures (a1 == a2))
let has_array_of_base_inj
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (a1 a2: array td)
: Lemma
  (requires (
      has_array_of_base #t #tn #n #td r a1 /\
      has_array_of_base #t #tn #n #td r a2
  ))
  (ensures (a1 == a2))
= let (| ar1, _ |) = a1 in
  let (| ar2, _ |) = a2 in
  array_ref_base_offset_inj #t #td #tn ar1 r ar2 r
val has_array_of_base_inj
      (#t: Type)
      (#tn: Type0)
      (#n: array_size_t)
      (#td: typedef t)
      (r: ref (base_array0 tn td n))
      (a1 a2: array td)
    : Lemma
      (requires (has_array_of_base #t #tn #n #td r a1 /\ has_array_of_base #t #tn #n #td r a2))
      (ensures (a1 == a2))
let has_array_of_base_inj
      (#t: Type)
      (#tn: Type0)
      (#n: array_size_t)
      (#td: typedef t)
      (r: ref (base_array0 tn td n))
      (a1 a2: array td)
    : Lemma
      (requires (has_array_of_base #t #tn #n #td r a1 /\ has_array_of_base #t #tn #n #td r a2))
      (ensures (a1 == a2)) =
let (| ar1 , _ |) = a1 in
let (| ar2 , _ |) = a2 in
array_ref_base_offset_inj #t #td #tn ar1 r ar2 r
Steel.ST.C.Types.Array.fsti.checked
Steel.ST.Util.fsti.checked Steel.ST.C.Types.Base.fsti.checked Steel.ST.C.Types.Array.Base.fst.checked Steel.FractionalPermission.fst.checked Steel.C.Typenat.fsti.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.C.Types.Array.fsti
Steel.ST.C.Types.Array.array_size_t Steel.ST.C.Types.Base.typedef Steel.ST.C.Types.Base.ref Steel.ST.C.Types.Array.base_array_t Steel.ST.C.Types.Array.base_array0 Steel.ST.C.Types.Array.array Steel.ST.C.Types.Array.array_ptr Steel.ST.C.Types.Array.array_len_t Steel.ST.C.Types.Array.array_ref_base_offset_inj Prims.unit Prims.l_and Steel.ST.C.Types.Array.has_array_of_base Prims.squash Prims.eq2 Prims.Nil FStar.Pervasives.pattern
module Steel.ST.C.Types.Array
open Steel.ST.Util
include Steel.ST.C.Types.Base
open Steel.C.Typenat

module P = Steel.FractionalPermission
module SZ = FStar.SizeT

// To be extracted as: t[tn]
// Per the C standard, base array types must be of nonzero size
inline_for_extraction [@@noextract_to "krml"]
let array_size_t = (n: SZ.t { SZ.v n > 0 })
val base_array_t ([@@@strictly_positive] t: Type0) (tn: Type0 (* using Typenat (or Typestring for `#define`d constants) *)) (n: array_size_t) : Type0
inline_for_extraction [@@noextract_to "krml"]
let base_array_index_t (n: array_size_t) : Tot eqtype =
  Steel.ST.C.Types.Array.Base.array_domain (Ghost.hide n)
[@@noextract_to "krml"]
val base_array0 (#t: Type0) (tn: Type0) (td: typedef t) (n: array_size_t) : Tot (typedef (base_array_t t tn n))

inline_for_extraction
[@@noextract_to "krml"] // proof-only
let base_array (#t: Type0) (#tn: Type0) (td: typedef t) (n: nat {SZ.fits n /\ n > 0}) (# [solve_nat_t_of_nat ()] prf: squash (norm norm_typenat (nat_t_of_nat n == tn))) : Tot (typedef (base_array_t t tn (SZ.uint_to_t n)))
= base_array0 tn td (SZ.uint_to_t n)

val base_array_index (#t: Type0) (#tn: Type0) (#n: array_size_t) (a: base_array_t t tn n) (i: base_array_index_t n) : GTot t
val base_array_eq (#t: Type0) (#tn: Type0) (#n: array_size_t) (a1 a2: base_array_t t tn n) : Ghost prop
  (requires True)
  (ensures (fun y ->
    (y <==> (a1 == a2)) /\
    (y <==> (forall (i: base_array_index_t n) . base_array_index a1 i == base_array_index a2 i))
  ))
val mk_base_array (#t: Type) (tn: Type0) (n: array_size_t) (v: Seq.seq t) : Ghost (base_array_t t tn n)
  (requires (
    Seq.length v == SZ.v n
  ))
  (ensures (fun y -> True))
val mk_base_array_index (#t: Type) (tn: Type) (n: array_size_t) (v: Seq.seq t) (i: base_array_index_t n) : Lemma
  (requires (Seq.length v == SZ.v n))
  (ensures (
    Seq.length v == SZ.v n /\
    base_array_index (mk_base_array tn n v) i == Seq.index v (SZ.v i)
  ))
  [SMTPat (base_array_index (mk_base_array tn n v) i)]

let mk_base_array_inj  (#t: Type) (tn: Type0) (n: array_size_t) (v1 v2: Seq.seq t) : Lemma
  (requires (
    Seq.length v1 == SZ.v n /\
    Seq.length v2 == SZ.v n /\
    mk_base_array tn n v1 == mk_base_array tn n v2
  ))
  (ensures (v1 == v2))
  [SMTPat (mk_base_array tn n v1); SMTPat (mk_base_array tn n v2)]
= assert (forall (i: nat) . i < SZ.v n ==> base_array_index (mk_base_array tn n v1) (SZ.uint_to_t i) == base_array_index (mk_base_array tn n v2) (SZ.uint_to_t i));
  assert (v1 `Seq.equal` v2)
val base_array_fractionable (#t: Type) (#tn: Type0) (#n: array_size_t) (a: base_array_t t tn n) (td: typedef t) : Lemma
  (
    fractionable (base_array0 tn td n) a <==>
      (forall (i: base_array_index_t n) . fractionable td (base_array_index a i))
  )
  [SMTPat (fractionable (base_array0 tn td n) a)]
val base_array_mk_fraction   (#t: Type) (#tn: Type0) (#n: array_size_t) (a: base_array_t t tn n) (td: typedef t) (p: P.perm) (i: base_array_index_t n) : Lemma
  (requires (
    fractionable (base_array0 tn td n) a
  ))
  (ensures (
    fractionable (base_array0 tn td n) a /\
    base_array_index (mk_fraction (base_array0 tn td n) a p) i == mk_fraction td (base_array_index a i) p
  ))
  [SMTPat (base_array_index (mk_fraction (base_array0 tn td n) a p) i)]

val base_array_index_unknown (#t: Type) (tn: Type0) (n: array_size_t) (td: typedef t) (i: base_array_index_t n) : Lemma
  (base_array_index (unknown (base_array0 tn td n)) i == unknown td)
  [SMTPat (base_array_index (unknown (base_array0 tn td n)) i)]

val base_array_index_uninitialized (#t: Type) (tn: Type0) (n: array_size_t) (td: typedef t) (i: base_array_index_t n) : Lemma
  (base_array_index (uninitialized (base_array0 tn td n)) i == uninitialized td)
  [SMTPat (base_array_index (uninitialized (base_array0 tn td n)) i)]

val base_array_index_full (#t: Type) (#tn: Type0) (#n: array_size_t) (td: typedef t) (x: base_array_t t tn n) : Lemma
  (full (base_array0 tn td n) x <==> (forall (i: base_array_index_t n) . full td (base_array_index x i)))
  [SMTPat (full (base_array0 tn td n) x)]

val has_base_array_cell
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (i: SZ.t)
  (r': ref td)
: Tot vprop

val has_base_array_cell_post
  (#opened: _)
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (i: SZ.t)
  (r': ref td)
: STGhost unit opened
    (has_base_array_cell r i r')
    (fun _ -> has_base_array_cell r i r')
    (True)
    (fun _ -> SZ.v i < SZ.v n)

val has_base_array_cell_dup
  (#opened: _)
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (i: SZ.t)
  (r': ref td)
: STGhostT unit opened
    (has_base_array_cell r i r')
    (fun _ -> has_base_array_cell r i r' `star` has_base_array_cell r i r')

val has_base_array_cell_inj
  (#opened: _)
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (i: SZ.t)
  (r1 r2: ref td)
: STGhostT unit opened
    (has_base_array_cell r i r1 `star` has_base_array_cell r i r2)
    (fun _ -> has_base_array_cell r i r1 `star` has_base_array_cell r i r2 `star` ref_equiv r1 r2)

val has_base_array_cell_equiv_from
  (#opened: _)
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r1 r2: ref (base_array0 tn td n))
  (i: SZ.t)
  (r': ref td)
: STGhostT unit opened
    (has_base_array_cell r1 i r' `star` ref_equiv r1 r2)
    (fun _ -> has_base_array_cell r2 i r' `star` ref_equiv r1 r2)

val has_base_array_cell_equiv_to
  (#opened: _)
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (i: SZ.t)
  (r1 r2: ref td)
: STGhostT unit opened
    (has_base_array_cell r i r1 `star` ref_equiv r1 r2)
    (fun _ -> has_base_array_cell r i r2 `star` ref_equiv r1 r2)

// contrary to array fields, one is not supposed to take an array cell directly from a base array. one should use arrays instead

// To be extracted to: t*  (array type decays to pointer type)

// We still want to prove that cutting off some cell range on the
// right-hand end of an array won't change the C pointer to which an
// array extracts to. This is why we separately introduce `array_ref`
// to represent the "base+offset" pointer, and `array` which holds the
// ghost length of an array.

[@@noextract_to "krml"] // primitive
val array_void_ptr : Type0
[@@noextract_to "krml"] // primitive
let array_ptr_gen ([@@@unused] t: Type0) : Tot Type0 = array_void_ptr
inline_for_extraction [@@noextract_to "krml"] // primitive
let array_ptr (#t: Type) (td: typedef t) = array_ptr_gen t
[@@noextract_to "krml"] // primitive
val null_array_void_ptr: array_void_ptr
[@@noextract_to "krml"] // primitive
let null_array_ptr (#t: Type) (td: typedef t) : Tot (array_ptr td) = null_array_void_ptr
val g_array_ptr_is_null (#t: Type) (#td: typedef t) (a: array_ptr td) : Ghost bool
  (requires True)
  (ensures (fun y -> y == true <==> a == null_array_ptr td))
inline_for_extraction [@@noextract_to "krml"]
let array_ref (#t: Type) (td: typedef t) = (a: array_ptr td { g_array_ptr_is_null a == false })

(*
val array_ref_base_size_type (#t: Type) (#td: typedef t) (a: array_ref td) : GTot Type0
*)
val array_ref_base_size (#t: Type) (#td: typedef t) (a: array_ptr td) : Ghost SZ.t
  (requires True)
  (ensures (fun y -> SZ.v y == 0 <==> a == null_array_ptr td))
val has_array_ref_base (#t: Type) (#td: typedef t) (a: array_ref td) (#ty: Type) (r: ref (base_array0 ty td (array_ref_base_size a))) : GTot prop
val has_array_ref_base_inj (#t: Type) (#td: typedef t) (a: array_ref td) (#ty: Type) (r1 r2: ref (base_array0 ty td (array_ref_base_size a))) : Lemma
  (requires (has_array_ref_base a r1 /\ has_array_ref_base a r2))
  (ensures (r1 == r2))
val array_ref_offset (#t: Type) (#td: typedef t) (a: array_ptr td) : Ghost SZ.t
  (requires True)
  (ensures (fun y -> SZ.v y <= SZ.v (array_ref_base_size a)))
val array_ref_base_offset_inj (#t: Type) (#td: typedef t) (#ty: Type) (a1: array_ref td) (r1: ref (base_array0 ty td (array_ref_base_size a1))) (a2: array_ref td) (r2: ref (base_array0 ty td (array_ref_base_size a2))) : Lemma
  (requires (
    array_ref_base_size a1 == array_ref_base_size a2 /\
    has_array_ref_base a1 r1 /\
    has_array_ref_base a2 r2 /\
    r1 == coerce_eq () r2 /\
    array_ref_offset a1 == array_ref_offset a2
  ))
  (ensures (a1 == a2))

inline_for_extraction [@@noextract_to "krml"]
let array_len_t (#t: Type) (#td: typedef t) (r: array_ptr td) : Tot Type0 =
  (len: Ghost.erased SZ.t { SZ.v (array_ref_offset r) + SZ.v len <= SZ.v (array_ref_base_size r) })

inline_for_extraction [@@noextract_to "krml"]
let array_or_null (#t: Type) (td: typedef t) : Tot Type0 = (r: array_ptr td & array_len_t r)

inline_for_extraction [@@noextract_to "krml"]
let array_ptr_of (#t: Type) (#td: typedef t) (ar: array_or_null td) : Tot (array_ptr td) =
  match ar with
  | (| a, _ |) -> a

let array_len_of (#t: Type) (#td: typedef t) (ar: array_or_null td) : Tot (array_len_t (array_ptr_of ar)) =
  match ar with
  | (| _, a |) -> a

let g_array_is_null (#t: Type) (#td: typedef t) (a: array_or_null td) : GTot bool =
  g_array_ptr_is_null (array_ptr_of a)

inline_for_extraction [@@noextract_to "krml"]
let array (#t: Type) (td: typedef t) : Tot Type0 = (a: array_or_null td { g_array_is_null a == false })

inline_for_extraction [@@noextract_to "krml"]
let array_ref_of (#t: Type) (#td: typedef t) (ar: array td) : Tot (array_ref td) =
  array_ptr_of ar

inline_for_extraction [@@noextract_to "krml"]
let mk_array (#t: Type) (#td: typedef t) (a: array_ref td) (len: array_len_t a) : Tot (array td) =
  (| a, len |)

let array_length
  (#t: Type)
  (#td: typedef t)
  (a: array td)
: GTot nat
= SZ.v (dsnd a)

val array_pts_to
  (#t: Type)
  (#td: typedef t)
  (r: array td)
  (v: Ghost.erased (Seq.seq t))
: Tot vprop

let array_pts_to_or_null
  (#t: Type)
  (#td: typedef t)
  (r: array_or_null td)
  (v: Ghost.erased (Seq.seq t))
: Tot vprop
= if g_array_is_null r
  then emp
  else array_pts_to r v

[@@noextract_to "krml"] // primitive
val array_ptr_is_null
  (#t: Type)
  (#opened: _)
  (#td: typedef t)
  (#v: Ghost.erased (Seq.seq t))
  (r: array_ptr td)
  (len: array_len_t r)
: STAtomicBase bool false opened Unobservable
    (array_pts_to_or_null (| r, len |) v)
    (fun _ -> array_pts_to_or_null (| r, len |) v)
    (True)
    (fun b -> b == g_array_is_null (| r, len |))

inline_for_extraction [@@noextract_to "krml"]
let array_is_null
  (#t: Type)
  (#opened: _)
  (#td: typedef t)
  (#v: Ghost.erased (Seq.seq t))
  (r: array_or_null td)
: STAtomicBase bool false opened Unobservable
    (array_pts_to_or_null r v)
    (fun _ -> array_pts_to_or_null r v)
    (True)
    (fun b -> b == g_array_is_null r)
= let a = array_ptr_of r in
  let len : array_len_t a = dsnd r in
  rewrite (array_pts_to_or_null _ _) (array_pts_to_or_null (| a, len |) v);
  let res = array_ptr_is_null a len in
  rewrite (array_pts_to_or_null _ _) (array_pts_to_or_null r v);
  return res

val array_pts_to_length
  (#opened: _)
  (#t: Type)
  (#td: typedef t)
  (r: array td)
  (v: Ghost.erased (Seq.seq t))
: STGhost unit opened
    (array_pts_to r v)
    (fun _ -> array_pts_to r v)
    (True)
    (fun _ -> Seq.length v == SZ.v (dsnd r))

#set-options "--print_implicits"

let has_array_of_base
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (a: array td)
: GTot prop
=   let (| al, len |) = a in
    array_ref_base_size al == n /\
    has_array_ref_base al #tn r /\
    array_ref_offset al == 0sz /\
    Ghost.reveal len == n

let has_array_of_base_inj
  (#t: Type)
  (#tn: Type0)
  (#n: array_size_t)
  (#td: typedef t)
  (r: ref (base_array0 tn td n))
  (a1 a2: array td)
: Lemma
  (requires (
      has_array_of_base #t #tn #n #td r a1 /\
      has_array_of_base #t #tn #n #td r a2
  ))
val has_array_of_base_inj
      (#t: Type)
      (#tn: Type0)
      (#n: array_size_t)
      (#td: typedef t)
      (r: ref (base_array0 tn td n))
      (a1 a2: array td)
    : Lemma
      (requires (has_array_of_base #t #tn #n #td r a1 /\ has_array_of_base #t #tn #n #td r a2))
      (ensures (a1 == a2))

    r: Steel.ST.C.Types.Base.ref (Steel.ST.C.Types.Array.base_array0 tn td n) ->
    a1: Steel.ST.C.Types.Array.array td ->
    a2: Steel.ST.C.Types.Array.array td
  -> FStar.Pervasives.Lemma
      (requires
        Steel.ST.C.Types.Array.has_array_of_base r a1 /\
        Steel.ST.C.Types.Array.has_array_of_base r a2) (ensures a1 == a2)