val elim_array_swap_inner_invariant
      (#opened: _)
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (n l: SZ.t)
      (bz: Prf.bezout (SZ.v n) (SZ.v l))
      (s0: Ghost.erased (Seq.seq t))
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (pj pidx: R.ref SZ.t)
      (b: bool)
    : STGhost (array_swap_inner_invariant_t t)
      opened
      (array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)
      (fun w -> array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s)
      True
      (fun w ->
          array_swap_inner_invariant_prop (SZ.v n)
            (SZ.v l)
            bz
            s0
            w.s
            (SZ.v i)
            (SZ.v w.j)
            (SZ.v w.idx)
            b)
let elim_array_swap_inner_invariant
  (#opened: _)
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (pj: R.ref SZ.t)
  (pidx: R.ref SZ.t)
  (b: bool)
: STGhost (array_swap_inner_invariant_t t) opened
    (array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)
    (fun w -> array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s)
    True
    (fun w -> array_swap_inner_invariant_prop (SZ.v n) (SZ.v l) bz s0 w.s (SZ.v i) (SZ.v w.j) (SZ.v w.idx) b)
= let w = elim_exists () in
  elim_pure _;
  w
val elim_array_swap_inner_invariant
      (#opened: _)
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (n l: SZ.t)
      (bz: Prf.bezout (SZ.v n) (SZ.v l))
      (s0: Ghost.erased (Seq.seq t))
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (pj pidx: R.ref SZ.t)
      (b: bool)
    : STGhost (array_swap_inner_invariant_t t)
      opened
      (array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)
      (fun w -> array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s)
      True
      (fun w ->
          array_swap_inner_invariant_prop (SZ.v n)
            (SZ.v l)
            bz
            s0
            w.s
            (SZ.v i)
            (SZ.v w.j)
            (SZ.v w.idx)
            b)
let elim_array_swap_inner_invariant
      (#opened: _)
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (n l: SZ.t)
      (bz: Prf.bezout (SZ.v n) (SZ.v l))
      (s0: Ghost.erased (Seq.seq t))
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (pj pidx: R.ref SZ.t)
      (b: bool)
    : STGhost (array_swap_inner_invariant_t t)
      opened
      (array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)
      (fun w -> array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s)
      True
      (fun w ->
          array_swap_inner_invariant_prop (SZ.v n)
            (SZ.v l)
            bz
            s0
            w.s
            (SZ.v i)
            (SZ.v w.j)
            (SZ.v w.idx)
            b) =
let w = elim_exists () in
elim_pure _;
w
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.Memory.inames Steel.ST.GenArraySwap.array_pts_to_t FStar.SizeT.t Steel.ST.GenArraySwap.Proof.bezout FStar.SizeT.v FStar.Ghost.erased FStar.Seq.Base.seq Steel.ST.Reference.ref Prims.bool FStar.Ghost.reveal Steel.ST.GenArraySwap.array_swap_inner_invariant_t Prims.unit Steel.ST.Util.elim_pure Steel.ST.GenArraySwap.array_swap_inner_invariant_prop Steel.ST.GenArraySwap.__proj__Mkarray_swap_inner_invariant_t__item__s Steel.ST.GenArraySwap.__proj__Mkarray_swap_inner_invariant_t__item__j Steel.ST.GenArraySwap.__proj__Mkarray_swap_inner_invariant_t__item__idx Steel.ST.Util.elim_exists Steel.Effect.Common.star Steel.ST.GenArraySwap.array_swap_inner_invariant_body0 Steel.ST.Util.pure Steel.Effect.Common.vprop Steel.ST.GenArraySwap.array_swap_inner_invariant Prims.l_True
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
=
    R.pts_to pi full_perm i `star`
    pts_to s

[@@erasable]
noeq
type array_swap_outer_invariant_t (t: Type)
= {
    i: SZ.t;
    s: Ghost.erased (Seq.seq t);
  }

[@@__reduce__]
let array_swap_outer_invariant0
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (b: bool)
: Tot vprop
= exists_ (fun w ->
    array_swap_outer_invariant_body0 pts_to pi w.i w.s `star`
    pure (array_swap_outer_invariant_prop (SZ.v n) (SZ.v l) bz s0 w.s (SZ.v w.i) b)
 )

let array_swap_outer_invariant
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (b: bool)
: Tot vprop
= array_swap_outer_invariant0 pts_to n l bz s0 pi b

let intro_array_swap_outer_invariant
  (#opened: _)
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (b: bool)
  (i: SZ.t)
  (s: Ghost.erased (Seq.seq t))
: STGhost unit opened
    (array_swap_outer_invariant_body0 pts_to pi i s)
    (fun _ -> array_swap_outer_invariant pts_to n l bz s0 pi b)
    (array_swap_outer_invariant_prop (SZ.v n) (SZ.v l) bz s0 s (SZ.v i) b)
    (fun _ -> True)
= let w = {
    i = i;
    s = s;
  }
  in
  rewrite (array_swap_outer_invariant_body0 pts_to pi i s) (array_swap_outer_invariant_body0 pts_to pi w.i w.s);
  rewrite (array_swap_outer_invariant0 pts_to n l bz s0 pi b) (array_swap_outer_invariant pts_to n l bz s0 pi b)

let elim_array_swap_outer_invariant
  (#opened: _)
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (b: bool)
: STGhost (array_swap_outer_invariant_t t) opened
    (array_swap_outer_invariant pts_to n l bz s0 pi b)
    (fun w -> array_swap_outer_invariant_body0 pts_to pi w.i w.s)
    True
    (fun w ->
      array_swap_outer_invariant_prop (SZ.v n) (SZ.v l) bz s0 w.s (SZ.v w.i) b /\
True //      (b == false ==> Ghost.reveal w.s `Seq.equal` (Seq.slice s0 (SZ.v l) (SZ.v n) `Seq.append` Seq.slice s0 0 (SZ.v l)))
    )
= let w = elim_exists () in
  let _ = gen_elim () in
//  Classical.move_requires (array_swap_outer_invariant_prop_end (SZ.v n) (SZ.v l) bz s0 w.s (SZ.v w.i)) b;
  noop ();
  w

[@@erasable]
noeq
type array_swap_inner_invariant_t (t: Type)
= {
    j: SZ.t;
    idx: SZ.t;
    s: Ghost.erased (Seq.seq t)
  }

[@@__reduce__]
let array_swap_inner_invariant_body0
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (pj: R.ref SZ.t)
  (pidx: R.ref SZ.t)
  (b: bool)
  (j: SZ.t)
  (idx: SZ.t)
  (s: Ghost.erased (Seq.seq t))
: Tot vprop
=   R.pts_to pi full_perm i `star`
    R.pts_to pj full_perm j `star`
    R.pts_to pidx full_perm idx `star`
    pts_to s

[@@__reduce__]
let array_swap_inner_invariant0
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (pj: R.ref SZ.t)
  (pidx: R.ref SZ.t)
  (b: bool)
: Tot vprop
= exists_ (fun w ->
    array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s `star`
    pure (array_swap_inner_invariant_prop (SZ.v n) (SZ.v l) bz s0 w.s (SZ.v i) (SZ.v w.j) (SZ.v w.idx) b)
  )

let array_swap_inner_invariant
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (pj: R.ref SZ.t)
  (pidx: R.ref SZ.t)
  (b: bool)
: Tot vprop
= array_swap_inner_invariant0 pts_to n l bz s0 pi i pj pidx b

let intro_array_swap_inner_invariant
  (#opened: _)
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (pj: R.ref SZ.t)
  (pidx: R.ref SZ.t)
  (b: bool)
  (j: SZ.t)
  (idx: SZ.t)
  (s: Ghost.erased (Seq.seq t))
: STGhost unit opened
    (array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b j idx s)
    (fun _ -> array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)
    (array_swap_inner_invariant_prop (SZ.v n) (SZ.v l) bz s0 s (SZ.v i) (SZ.v j) (SZ.v idx) b)
    (fun _ -> True)
= let w = {
    j = j;
    idx = idx;
    s = s;
  }
  in
  rewrite
    (array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b j idx s)
    (array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s);
  rewrite
    (array_swap_inner_invariant0 pts_to n l bz s0 pi i pj pidx b)
    (array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)

let elim_array_swap_inner_invariant
  (#opened: _)
  (#t: Type)
  (pts_to: array_pts_to_t t)
  (n: SZ.t)
  (l: SZ.t)
  (bz: Prf.bezout (SZ.v n) (SZ.v l))
  (s0: Ghost.erased (Seq.seq t))
  (pi: R.ref SZ.t)
  (i: SZ.t)
  (pj: R.ref SZ.t)
  (pidx: R.ref SZ.t)
  (b: bool)
: STGhost (array_swap_inner_invariant_t t) opened
    (array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)
    (fun w -> array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s)
    True
val elim_array_swap_inner_invariant
      (#opened: _)
      (#t: Type)
      (pts_to: array_pts_to_t t)
      (n l: SZ.t)
      (bz: Prf.bezout (SZ.v n) (SZ.v l))
      (s0: Ghost.erased (Seq.seq t))
      (pi: R.ref SZ.t)
      (i: SZ.t)
      (pj pidx: R.ref SZ.t)
      (b: bool)
    : STGhost (array_swap_inner_invariant_t t)
      opened
      (array_swap_inner_invariant pts_to n l bz s0 pi i pj pidx b)
      (fun w -> array_swap_inner_invariant_body0 pts_to n l bz s0 pi i pj pidx b w.j w.idx w.s)
      True
      (fun w ->
          array_swap_inner_invariant_prop (SZ.v n)
            (SZ.v l)
            bz
            s0
            w.s
            (SZ.v i)
            (SZ.v w.j)
            (SZ.v w.idx)
            b)

    pts_to: Steel.ST.GenArraySwap.array_pts_to_t t ->
    n: FStar.SizeT.t ->
    l: FStar.SizeT.t ->
    bz: Steel.ST.GenArraySwap.Proof.bezout (FStar.SizeT.v n) (FStar.SizeT.v l) ->
    s0: FStar.Ghost.erased (FStar.Seq.Base.seq t) ->
    pi: Steel.ST.Reference.ref FStar.SizeT.t ->
    i: FStar.SizeT.t ->
    pj: Steel.ST.Reference.ref FStar.SizeT.t ->
    pidx: Steel.ST.Reference.ref FStar.SizeT.t ->
    b: Prims.bool
  -> Steel.ST.Effect.Ghost.STGhost (Steel.ST.GenArraySwap.array_swap_inner_invariant_t t)