val array_swap_outer_invariant_body0
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (s: Ghost.erased (Seq.seq t))
    : Tot vprop
let array_swap_outer_invariant_body0
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (s: Ghost.erased (Seq.seq t))
: Tot vprop
=
    R.pts_to pi full_perm i `star`
    pts_to s
val array_swap_outer_invariant_body0
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (s: Ghost.erased (Seq.seq t))
    : Tot vprop
let array_swap_outer_invariant_body0
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (s: Ghost.erased (Seq.seq t))
    : Tot vprop =
(R.pts_to pi full_perm i) `star` (pts_to s)
Steel.ST.GenArraySwap.fst.checked
Steel.ST.Reference.fsti.checked Steel.ST.Loops.fsti.checked Steel.ST.GenElim.fsti.checked Steel.ST.GenArraySwap.Proof.fst.checked prims.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Steel.ST.GenArraySwap.fst
Steel.ST.GenArraySwap.array_pts_to_t Steel.ST.Reference.ref FStar.SizeT.t FStar.Ghost.erased FStar.Seq.Base.seq Steel.Effect.Common.star Steel.ST.Reference.pts_to Steel.FractionalPermission.full_perm Steel.Effect.Common.vprop
module Steel.ST.GenArraySwap
open Steel.ST.GenElim

module Prf = Steel.ST.GenArraySwap.Proof
module R = Steel.ST.Reference

let gcd_inv_prop
  (n0: nat)
  (l0: nat)
  (n: nat)
  (l: nat)
  (b: bool)
: Tot prop
= l0 < n0 /\
  l < n /\
  (Prf.mk_bezout n0 l0).d == (Prf.mk_bezout n l).d /\
  b == (l > 0)

[@@__reduce__]
let gcd_inv0
  (n0: SZ.t)
  (l0: SZ.t)
  (pn: R.ref SZ.t)
  (pl: R.ref SZ.t)
  (b: bool)
: Tot vprop
= exists_ (fun n -> exists_ (fun l ->
    R.pts_to pn full_perm n `star`
    R.pts_to pl full_perm l `star`
    pure (gcd_inv_prop (SZ.v n0) (SZ.v l0) (SZ.v n) (SZ.v l) b)
  ))

let gcd_inv
  (n0: SZ.t)
  (l0: SZ.t)
  (pn: R.ref SZ.t)
  (pl: R.ref SZ.t)
  (b: bool)
: Tot vprop
= gcd_inv0 n0 l0 pn pl b

let gcd_post
  (n0: SZ.t)
  (l0: SZ.t)
  (res: SZ.t)
: Tot prop
= SZ.v l0 < SZ.v n0 /\
  SZ.v res == (Prf.mk_bezout (SZ.v n0) (SZ.v l0)).d

#push-options "--z3rlimit 16"

#restart-solver
let gcd
  (n0: SZ.t)
  (l0: SZ.t)
: ST SZ.t
    emp
    (fun _ -> emp)
    (SZ.v l0 < SZ.v n0)
    (fun res -> gcd_post n0 l0 res)
= let res =
    R.with_local n0 (fun pn ->
      R.with_local l0 (fun pl ->
        noop ();
        rewrite (gcd_inv0 n0 l0 pn pl (l0 `SZ.gt` 0sz)) (gcd_inv n0 l0 pn pl (l0 `SZ.gt` 0sz));
        Steel.ST.Loops.while_loop
          (gcd_inv n0 l0 pn pl)
          (fun _ ->
            let gb = elim_exists () in
            rewrite (gcd_inv n0 l0 pn pl gb) (gcd_inv0 n0 l0 pn pl gb);
            let _ = gen_elim () in
            let l = R.read pl in
            [@@inline_let]
            let b = l `SZ.gt` 0sz in
            noop ();
            rewrite (gcd_inv0 n0 l0 pn pl b) (gcd_inv n0 l0 pn pl b);
            return b
          )
          (fun _ ->
            rewrite (gcd_inv n0 l0 pn pl true) (gcd_inv0 n0 l0 pn pl true);
            let _ = gen_elim () in
            let n = R.read pn in
            let l = R.read pl in
            [@@inline_let]
            let l' = SZ.rem n l in
            R.write pn l;
            R.write pl l';
            rewrite (gcd_inv0 n0 l0 pn pl (l' `SZ.gt` 0sz)) (gcd_inv n0 l0 pn pl (l' `SZ.gt` 0sz));
            noop ()
          );
        rewrite (gcd_inv n0 l0 pn pl false) (gcd_inv0 n0 l0 pn pl false);
        let _ = gen_elim () in
        let res = R.read pn in
        return res
      )
    )
  in
  elim_pure (gcd_post n0 l0 res);
  return res

#pop-options

let array_swap_partial_invariant
  (#t: Type)
  (n: nat)
  (l: nat)
  (bz: Prf.bezout n l)
  (s0: Ghost.erased (Seq.seq t))
  (s: Ghost.erased (Seq.seq t))
  (i: nat)
: GTot prop
= n == Seq.length s0 /\
  n == Seq.length s /\
  0 < l /\
  l < n /\
  i <= bz.d /\
  (forall (i': Prf.nat_up_to bz.d) .
    (forall (j: Prf.nat_up_to bz.q_n) .
      (i' < i) ==> (
      let idx = Prf.iter_fun #(Prf.nat_up_to n) (Prf.jump n l) j i' in
      Seq.index s idx == Seq.index s0 (Prf.jump n l idx)
  ))) /\
  (forall (i': Prf.nat_up_to bz.d) .
    (forall (j: Prf.nat_up_to bz.q_n) .
      (i' > i) ==> (
      let idx = Prf.iter_fun #(Prf.nat_up_to n) (Prf.jump n l) j i' in
      Seq.index s idx == Seq.index s0 idx
  )))

let array_swap_inner_invariant_prop
  (#t: Type)
  (n: nat)
  (l: nat)
  (bz: Prf.bezout n l)
  (s0: Ghost.erased (Seq.seq t))
  (s: Ghost.erased (Seq.seq t))
  (i: nat)
  (j: nat)
  (idx: nat)
  (b: bool)
: GTot prop
= Prf.array_swap_inner_invariant s0 n l bz s i j idx /\
  (b == (j < bz.q_n - 1))

let array_swap_outer_invariant_prop
  (#t: Type)
  (n: nat)
  (l: nat)
  (bz: Prf.bezout n l)
  (s0: Ghost.erased (Seq.seq t))
  (s: Ghost.erased (Seq.seq t))
  (i: nat)
  (b: bool)
: GTot prop
= Prf.array_swap_outer_invariant s0 n l bz s i /\
  (b == (i < bz.d))

[@@__reduce__]
let array_swap_outer_invariant_body0
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (s: Ghost.erased (Seq.seq t))
: Tot vprop
val array_swap_outer_invariant_body0
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (s: Ghost.erased (Seq.seq t))
    : Tot vprop

    pts_to: Steel.ST.GenArraySwap.array_pts_to_t t ->
    pi: Steel.ST.Reference.ref FStar.SizeT.t ->
    i: FStar.SizeT.t ->
    s: FStar.Ghost.erased (FStar.Seq.Base.seq t)
  -> Steel.Effect.Common.vprop