val gcd_post (n0 l0 res: SZ.t) : Tot prop
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
val gcd_post (n0 l0 res: SZ.t) : Tot prop
let gcd_post (n0 l0 res: SZ.t) : Tot prop =
SZ.v l0 < SZ.v n0 /\ SZ.v res == (Prf.mk_bezout (SZ.v n0) (SZ.v l0)).d
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 Prims.l_and Prims.b2t Prims.op_LessThan FStar.SizeT.v Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThanOrEqual Prims.op_GreaterThan Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__d Steel.ST.GenArraySwap.Proof.mk_bezout 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)
val gcd_post (n0 l0 res: SZ.t) : Tot prop
n0: FStar.SizeT.t -> l0: FStar.SizeT.t -> res: FStar.SizeT.t -> Prims.prop