val swap
  (#t: Type0)
  (#s0: Ghost.erased (Seq.seq t))
  (a: array t)
  (n: SZ.t)
  (l: SZ.t)
: ST (Ghost.erased (Seq.seq t))
    (pts_to a full_perm s0)
    (fun s -> pts_to a full_perm s)
    (
      SZ.v n == length a /\
      SZ.v l <= SZ.v n
    )
    (fun s ->
      SZ.v n == Seq.length s0 /\
      SZ.v l <= SZ.v n /\
      s `Seq.equal` (Seq.slice s0 (SZ.v l) (SZ.v n) `Seq.append` Seq.slice s0 0 (SZ.v l))
    )
let swap
  a n l
= pts_to_length a _;
  Gen.array_swap_gen (array_index a) (array_upd a) _ n l
val swap
  (#t: Type0)
  (#s0: Ghost.erased (Seq.seq t))
  (a: array t)
  (n: SZ.t)
  (l: SZ.t)
: ST (Ghost.erased (Seq.seq t))
    (pts_to a full_perm s0)
    (fun s -> pts_to a full_perm s)
    (
      SZ.v n == length a /\
      SZ.v l <= SZ.v n
    )
    (fun s ->
      SZ.v n == Seq.length s0 /\
      SZ.v l <= SZ.v n /\
      s `Seq.equal` (Seq.slice s0 (SZ.v l) (SZ.v n) `Seq.append` Seq.slice s0 0 (SZ.v l))
    )
let swap a n l =
pts_to_length a _;
Gen.array_swap_gen (array_index a) (array_upd a) _ n l
Steel.ST.Array.Swap.fst.checked
Steel.ST.GenElim.fsti.checked Steel.ST.GenArraySwap.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.Array.Swap.fst
FStar.Ghost.erased FStar.Seq.Base.seq Steel.ST.Array.array FStar.SizeT.t Steel.ST.GenArraySwap.array_swap_gen Steel.ST.Array.Swap.array_pts_to Steel.ST.Array.Swap.array_index Steel.ST.Array.Swap.array_upd Prims.unit Steel.ST.Array.pts_to_length FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.FractionalPermission.full_perm FStar.Ghost.reveal
module Steel.ST.Array.Swap
open Steel.ST.GenElim
open Steel.ST.Array // for pts_to

module Gen = Steel.ST.GenArraySwap

[@@__reduce__]
let array_pts_to (#t: Type) (a: array t) : Tot (Gen.array_pts_to_t t) =
  fun s -> pts_to a full_perm (Ghost.reveal s)

inline_for_extraction
let array_index
  (#t: Type)
  (a: array t)
: Tot (Gen.array_index_t (array_pts_to a))
= fun s n i ->
    index a i

inline_for_extraction
let array_upd
  (#t: Type)
  (a: array t)
: Tot (Gen.array_upd_t (array_pts_to a))
= fun s n i x ->
    upd a i x;
    return _

let swap
val swap
  (#t: Type0)
  (#s0: Ghost.erased (Seq.seq t))
  (a: array t)
  (n: SZ.t)
  (l: SZ.t)
: ST (Ghost.erased (Seq.seq t))
    (pts_to a full_perm s0)
    (fun s -> pts_to a full_perm s)
    (
      SZ.v n == length a /\
      SZ.v l <= SZ.v n
    )
    (fun s ->
      SZ.v n == Seq.length s0 /\
      SZ.v l <= SZ.v n /\
      s `Seq.equal` (Seq.slice s0 (SZ.v l) (SZ.v n) `Seq.append` Seq.slice s0 0 (SZ.v l))
    )
a: Steel.ST.Array.array t -> n: FStar.SizeT.t -> l: FStar.SizeT.t
  -> Steel.ST.Effect.ST (FStar.Ghost.erased (FStar.Seq.Base.seq t))