val 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)]
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 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)]
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)
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 FStar.Seq.Base.seq Prims._assert FStar.Seq.Base.equal Prims.unit Prims.l_Forall Prims.nat Prims.l_imp Prims.b2t Prims.op_LessThan FStar.SizeT.v Prims.eq2 Steel.ST.C.Types.Array.base_array_index Steel.ST.C.Types.Array.mk_base_array FStar.SizeT.uint_to_t Prims.l_and FStar.Seq.Base.length Steel.ST.C.Types.Array.base_array_t Prims.squash Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
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))
val 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)]

    tn: Type0 ->
    n: Steel.ST.C.Types.Array.array_size_t ->
    v1: FStar.Seq.Base.seq t ->
    v2: FStar.Seq.Base.seq t
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Seq.Base.length v1 == FStar.SizeT.v n /\ FStar.Seq.Base.length v2 == FStar.SizeT.v n /\
        Steel.ST.C.Types.Array.mk_base_array tn n v1 == Steel.ST.C.Types.Array.mk_base_array tn n v2
      )
      (ensures v1 == v2)
      [
        SMTPat (Steel.ST.C.Types.Array.mk_base_array tn n v1);
        SMTPat (Steel.ST.C.Types.Array.mk_base_array tn n v2)
      ]