val array_swap_partial_invariant
      (#t: Type)
      (n l: nat)
      (bz: Prf.bezout n l)
      (s0 s: Ghost.erased (Seq.seq t))
      (i: nat)
    : GTot prop
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
  )))
val array_swap_partial_invariant
      (#t: Type)
      (n l: nat)
      (bz: Prf.bezout n l)
      (s0 s: Ghost.erased (Seq.seq t))
      (i: nat)
    : GTot prop
let array_swap_partial_invariant
      (#t: Type)
      (n l: nat)
      (bz: Prf.bezout n l)
      (s0 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)))
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
Prims.nat Steel.ST.GenArraySwap.Proof.bezout FStar.Ghost.erased FStar.Seq.Base.seq Prims.l_and Prims.eq2 FStar.Seq.Base.length FStar.Ghost.reveal Prims.b2t Prims.op_LessThan Prims.op_LessThanOrEqual Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__d Prims.l_Forall Steel.ST.GenArraySwap.Proof.nat_up_to Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__q_n Prims.l_imp FStar.Seq.Base.index Steel.ST.GenArraySwap.Proof.jump Steel.ST.GenArraySwap.Proof.iter_fun Prims.op_GreaterThan Prims.prop
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)
val array_swap_partial_invariant
      (#t: Type)
      (n l: nat)
      (bz: Prf.bezout n l)
      (s0 s: Ghost.erased (Seq.seq t))
      (i: nat)
    : GTot prop

    n: Prims.nat ->
    l: Prims.nat ->
    bz: Steel.ST.GenArraySwap.Proof.bezout n l ->
    s0: FStar.Ghost.erased (FStar.Seq.Base.seq t) ->
    s: FStar.Ghost.erased (FStar.Seq.Base.seq t) ->
    i: Prims.nat
  -> Prims.GTot Prims.prop