val gcd_inv0 (n0 l0: SZ.t) (pn pl: R.ref SZ.t) (b: bool) : Tot vprop
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)
  ))
val gcd_inv0 (n0 l0: SZ.t) (pn pl: R.ref SZ.t) (b: bool) : Tot vprop
let gcd_inv0 (n0 l0: SZ.t) (pn 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))))
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
FStar.SizeT.t Steel.ST.Reference.ref Prims.bool Steel.ST.Util.exists_ Steel.Effect.Common.star Steel.ST.Reference.pts_to Steel.FractionalPermission.full_perm Steel.ST.Util.pure Steel.ST.GenArraySwap.gcd_inv_prop FStar.SizeT.v 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)
val gcd_inv0 (n0 l0: SZ.t) (pn pl: R.ref SZ.t) (b: bool) : Tot vprop

    n0: FStar.SizeT.t ->
    l0: FStar.SizeT.t ->
    pn: Steel.ST.Reference.ref FStar.SizeT.t ->
    pl: Steel.ST.Reference.ref FStar.SizeT.t ->
    b: Prims.bool
  -> Steel.Effect.Common.vprop