val gauss (n l: pos) (b: bezout n l) (kl kn: int)
    : Ghost int (requires (kl * l == kn * n)) (ensures (fun k -> kl == k * b.q_n))
let gauss
  (n: pos)
  (l: pos) // necessary here
  (b: bezout n l)
  (kl kn: int)
: Ghost int
  (requires (
    kl * l == kn * n
  ))
  (ensures (fun k ->
    kl == k * b.q_n
  ))
= assert ((b.d * b.q_n) * b.u_n + (b.d * b.q_l) * b.u_l == b.d * (b.u_n * b.q_n + b.u_l * b.q_l)) by (int_semiring ());
  assert (b.d == b.d * 1) by (int_semiring ());
  assert (b.d * (b.u_n * b.q_n + b.u_l * b.q_l) == b.d * 1);
  lemma_mult_reg_l b.d (b.u_n * b.q_n + b.u_l * b.q_l) 1;
  assert (b.u_n * b.q_n + b.u_l * b.q_l == 1);
  if b.u_l = 0
  then begin
    lemma_bezout_one_zero b.u_n b.q_n b.u_l b.q_l;
    assert (b.q_n == 1);
    assert (kl * 1 == kl) by (int_semiring ());
    kl
  end else begin
    assert (kl * (b.d * b.q_l) == kn * (b.d * b.q_n));
    assert (kl * (b.d * b.q_l) == b.d * (kl * b.q_l)) by (int_semiring ());
    assert (kn * (b.d * b.q_n) == b.d * (kn * b.q_n)) by (int_semiring ());
    assert (b.d * (kl * b.q_l) == b.d * (kn * b.q_n));
    lemma_mult_reg_l b.d (kl * b.q_l) (kn * b.q_n);
    assert (kl * b.q_l == kn * b.q_n);
    assert (b.u_l * (kl * b.q_l) == b.u_l * (kn * b.q_n));
    assert (b.u_l * (kl * b.q_l) == kl * (b.u_l * b.q_l)) by (int_semiring ());
    assert (b.u_l * (kn * b.q_n) == (kn * b.u_l) * b.q_n) by (int_semiring ());
    assert (kl * (b.u_l * b.q_l) == (kn * b.u_l) * b.q_n);
    assert (kl * (1 + - (b.u_n * b.q_n)) == kl + - kl * b.u_n * b.q_n) by (int_semiring ());
    assert (kl * b.u_n * b.q_n + (kn * b.u_l) * b.q_n == (kn * b.u_l + kl * b.u_n) * b.q_n) by (int_semiring ());
    kn * b.u_l + kl * b.u_n
  end
val gauss (n l: pos) (b: bezout n l) (kl kn: int)
    : Ghost int (requires (kl * l == kn * n)) (ensures (fun k -> kl == k * b.q_n))
let gauss (n l: pos) (b: bezout n l) (kl kn: int)
    : Ghost int (requires (kl * l == kn * n)) (ensures (fun k -> kl == k * b.q_n)) =
FStar.Tactics.Effect.assert_by_tactic ((b.d * b.q_n) * b.u_n + (b.d * b.q_l) * b.u_l ==
    b.d * (b.u_n * b.q_n + b.u_l * b.q_l))
  (fun _ ->
      ();
      (int_semiring ()));
FStar.Tactics.Effect.assert_by_tactic (b.d == b.d * 1)
  (fun _ ->
      ();
      (int_semiring ()));
assert (b.d * (b.u_n * b.q_n + b.u_l * b.q_l) == b.d * 1);
lemma_mult_reg_l b.d (b.u_n * b.q_n + b.u_l * b.q_l) 1;
assert (b.u_n * b.q_n + b.u_l * b.q_l == 1);
if b.u_l = 0
then
  (lemma_bezout_one_zero b.u_n b.q_n b.u_l b.q_l;
    assert (b.q_n == 1);
    FStar.Tactics.Effect.assert_by_tactic (kl * 1 == kl)
      (fun _ ->
          ();
          (int_semiring ()));
    kl)
else
  (assert (kl * (b.d * b.q_l) == kn * (b.d * b.q_n));
    FStar.Tactics.Effect.assert_by_tactic (kl * (b.d * b.q_l) == b.d * (kl * b.q_l))
      (fun _ ->
          ();
          (int_semiring ()));
    FStar.Tactics.Effect.assert_by_tactic (kn * (b.d * b.q_n) == b.d * (kn * b.q_n))
      (fun _ ->
          ();
          (int_semiring ()));
    assert (b.d * (kl * b.q_l) == b.d * (kn * b.q_n));
    lemma_mult_reg_l b.d (kl * b.q_l) (kn * b.q_n);
    assert (kl * b.q_l == kn * b.q_n);
    assert (b.u_l * (kl * b.q_l) == b.u_l * (kn * b.q_n));
    FStar.Tactics.Effect.assert_by_tactic (b.u_l * (kl * b.q_l) == kl * (b.u_l * b.q_l))
      (fun _ ->
          ();
          (int_semiring ()));
    FStar.Tactics.Effect.assert_by_tactic (b.u_l * (kn * b.q_n) == (kn * b.u_l) * b.q_n)
      (fun _ ->
          ();
          (int_semiring ()));
    assert (kl * (b.u_l * b.q_l) == (kn * b.u_l) * b.q_n);
    FStar.Tactics.Effect.assert_by_tactic (kl * (1 + - (b.u_n * b.q_n)) ==
        kl + - (kl * b.u_n) * b.q_n)
      (fun _ ->
          ();
          (int_semiring ()));
    FStar.Tactics.Effect.assert_by_tactic ((kl * b.u_n) * b.q_n + (kn * b.u_l) * b.q_n ==
        (kn * b.u_l + kl * b.u_n) * b.q_n)
      (fun _ ->
          ();
          (int_semiring ()));
    kn * b.u_l + kl * b.u_n)
Steel.ST.GenArraySwap.Proof.fst.checked
prims.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Steel.ST.GenArraySwap.Proof.fst
Prims.pos Steel.ST.GenArraySwap.Proof.bezout Prims.int Prims.op_Equality Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__u_l Prims.unit FStar.Tactics.Effect.assert_by_tactic Prims.eq2 FStar.Mul.op_Star Steel.ST.GenArraySwap.Proof.int_semiring Prims._assert Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__q_n Steel.ST.GenArraySwap.Proof.lemma_bezout_one_zero Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__u_n Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__q_l Prims.bool Prims.op_Addition Prims.op_Minus Steel.ST.GenArraySwap.Proof.lemma_mult_reg_l Steel.ST.GenArraySwap.Proof.__proj__Mkbezout_t__item__d
module Steel.ST.GenArraySwap.Proof
open FStar.Math.Lemmas
open FStar.Mul

let lemma_mod_lt
  (a:int)
  (b:pos)
: Lemma
  (let r = a % b in 0 <= r /\ r < b)
  [SMTPat (a % b)]
= ()

let lemma_mul_nat_nat_is_nat
  (a b: nat)
: Lemma
  (a * b >= 0)
  [SMTPat (a * b)]
= ()

let lemma_pos_mul_pos_args
  (a: nat)
  (b: nat)
: Lemma
  (requires (a * b > 0))
  (ensures (a > 0 /\ b > 0 /\ a <= a * b /\ b <= a * b /\ a * b == b * a))
= ()

let lemma_div_nat
  (a: nat)
  (b: pos)
: Lemma
  (a / b >= 0)
  [SMTPat (a / b)]
= ()

let lemma_mult_reg_l
  (k: int)
  (x1 x2: int)
: Lemma
  (requires (
    k * x1 == k * x2 /\
    k <> 0
  ))
  (ensures (
    x1 == x2
  ))
= ()

let lemma_bezout_one_zero
  (x1: int)
  (x2: nat)
  (y1 y2: int)
: Lemma
  (requires (
    x1 * x2 + y1 * y2 == 1 /\
    y1 == 0
  ))
  (ensures (
    x1 == 1 /\ x2 == 1
  ))
= ()

#set-options "--z3cliopt smt.arith.nl=false"

let int_semiring () =
  FStar.Tactics.CanonCommSemiring.int_semiring ();
  FStar.Tactics.trefl ();
  FStar.Tactics.qed ()

[@@erasable]
noeq
type bezout_t = {
  d: pos;
  q_n: nat;
  q_l: nat;
  u_n: int;
  u_l: int;
}

let bezout_prop'
  (n: nat)
  (l: nat)
  (d: pos)
  (q_n: nat)
  (q_l: nat)
  (u_n: int)
  (u_l: int)
: Tot prop
= n == d * q_n /\
  l == d * q_l /\
  d == n * u_n + l * u_l

let bezout_prop
  (n: nat)
  (l: nat)
  (b: bezout_t)
: Tot prop
= bezout_prop' n l b.d b.q_n b.q_l b.u_n b.u_l

let bezout
  (n: nat)
  (l: nat)
: Tot Type
= (b: bezout_t { bezout_prop n l b })

#restart-solver
let rec mk_bezout
  (n: pos)
  (l: nat)
: Pure (bezout n l)
  (requires (l < n))
  (ensures (fun _ -> True))
  (decreases l)
= if l = 0
  then begin
    let d : pos = n in
    let q_n : nat = 1 in
    let q_l : nat = 0 in
    let u_n : int = 1 in
    let u_l : int = 0 in
    let res = {
      d = d;
      q_n = q_n;
      q_l = q_l;
      u_n = u_n;
      u_l = u_l;
    }
    in
    assert (eq2 #int n (d * q_n)) by (int_semiring ());
    assert (eq2 #int 0 (d * q_l)) by (int_semiring ());
    assert (eq2 #int d (n * 1 + 0 * res.u_l)) by (int_semiring ());
    res
  end
  else begin
    let lpre = n % l in
    let ql = n / l in
    euclidean_division_definition n l;
    let bpre = mk_bezout l lpre in
    let d = bpre.d in
    let q_l = bpre.q_n in
    let qpre_lpre = bpre.q_l in
    let upre_l = bpre.u_n in
    let upre_lpre = bpre.u_l in
    let n_alt0 = l * ql + lpre in
    assert (n == n_alt0);
    let l_alt = d * q_l in
    let lpre_alt1 = d * qpre_lpre in
    let n_alt1 = l_alt * ql + lpre_alt1 in
    assert (n_alt1 == n);
    let q_n = q_l * ql + qpre_lpre in
    assert (eq2 #int n_alt1 (d * q_n)) by (int_semiring ());
    let lpre_alt2 = n + - l * ql in
    assert (lpre_alt2 == lpre);
    let d_alt = l * upre_l + lpre_alt2 * upre_lpre in
    assert (d_alt == d);
    let u_l = upre_l + - ql * upre_lpre in
    assert (eq2 #int (n * upre_lpre + l * u_l) d_alt) by (int_semiring ());
    let res = {
      d = d;
      q_n = q_n;
      q_l = q_l;
      u_n = upre_lpre;
      u_l = u_l;
    }
    in
    res
  end

let bezout_q_eq
  (n: nat)
  (l: nat)
  (bz: bezout n l)
: Lemma
  (bz.q_n == n / bz.d)
  [SMTPat (bezout_prop n l bz); SMTPat bz.q_n]
= cancel_mul_div bz.q_n bz.d

let rec iter_fun
  (#t: Type)
  (f: (t -> GTot t))
  (n: nat)
  (x: t)
: GTot t
  (decreases n)
= if n = 0
  then x
  else iter_fun f (n - 1) (f x)

let nat_up_to (n: nat) : Tot Type = (i: nat { i < n })

let jump
  (n: pos)
  (l: nat)
  (x: nat_up_to n)
: GTot (nat_up_to n)
= (x + l) % n

#restart-solver
let jump_mod_d
  (n: pos)
  (l: nat)
  (b: bezout n l)
  (x: nat_up_to n)
: Lemma
  (jump n l x % b.d == x % b.d)
=
  let x' = jump n l x in
  let x'q = (x + l) / n in
  euclidean_division_definition (x + l) n;
  let l_alt = b.d * b.q_l in
  assert (l_alt == l);
  let n_alt = b.d * b.q_n in
  assert (n_alt == n);
  let x'_alt = x + l_alt + - x'q * n_alt in
  assert (x'_alt == x');
  let qx = b.q_l + - x'q * b.q_n in
  assert (eq2 #int x'_alt (x + qx * b.d)) by (int_semiring ());
  lemma_mod_plus x qx b.d

let rec jump_iter_mod_d
  (n: pos)
  (l: nat)
  (b: bezout n l)
  (x: nat_up_to n)
  (k: nat)
: Lemma
  (ensures (iter_fun #(nat_up_to n) (jump n l) k x % b.d == x % b.d))
  (decreases k)
= if k = 0
  then ()
  else begin
    jump_mod_d n l b x;
    jump_iter_mod_d n l b (jump n l x) (k - 1)
  end

(* Coverage *)

let rec jump_iter
  (n: pos)
  (l: nat)
  (x: nat_up_to n)
  (k: nat)
: Lemma
  (ensures (iter_fun #(nat_up_to n) (jump n l) k x == (x + k * l) % n))
  (decreases k)
= if k = 0
  then begin
    assert (eq2 #int (x + 0 * l) x) by (int_semiring ());
    small_mod x n
  end else begin
    let k' = k - 1 in
    assert (eq2 #int (x + (k' + 1) * l) ((x + l) + k' * l)) by (int_semiring ());
    jump_iter n l ((x + l) % n) k';
    lemma_mod_add_distr (k' * l) (x + l) n
  end

let bezout_pos_le
  (n: pos)
  (l: nat)
  (b: bezout n l)
: Lemma
  (b.d <= n /\ b.q_n > 0)
  [SMTPat (bezout_prop n l b)]
= lemma_pos_mul_pos_args b.q_n b.d

#restart-solver
[@@"opaque_to_smt"]
irreducible
let jump_coverage
  (n: pos)
  (l: nat)
  (b: bezout n l)
  (x: nat_up_to n)
: Ghost nat
  (requires True)
  (ensures (fun k ->
    x == iter_fun (jump n l) k (x % b.d)
  ))
=
  let i = x % b.d in
  let qx = x / b.d in
  euclidean_division_definition x b.d;
  let k1 = qx * b.u_l in
  let m = qx * b.u_n in
  assert (eq2 #int (qx * (n * b.u_n + l * b.u_l) + i) (i + k1 * l + m * n)) by (int_semiring ());
  assert (x == i + k1 * l + m * n);
  small_mod x n;
  lemma_mod_plus (i + k1 * l) m n;
  assert (x == (i + k1 * l) % n);
  let k = k1 % n in
  let qk = k1 / n in
  euclidean_division_definition k1 n;
  assert (i + (qk * n + k) * l == i + k * l + (qk * l) * n) by (int_semiring ());
  lemma_mod_plus (i + k * l) (qk * l) n;
  assert (eq2 #int x ((i + k * l) % n));
  jump_iter n l i k;
  k

[@@"opaque_to_smt"]
irreducible
let rec minimal_exists'
  (p: (nat -> GTot bool))
  (n: nat)
  (i: nat)
: Ghost nat
  (requires (
    p n == true /\
    i <= n /\
    (forall (j: nat) . j < i ==> p j == false)
  ))
  (ensures (fun k ->
    p k == true /\
    (forall (j: nat) . j < k ==> p j == false)
  ))
  (decreases (n - i))
= if p i
  then i
  else minimal_exists' p n (i + 1)

[@@"opaque_to_smt"]
irreducible
let minimal_exists
  (p: (nat -> GTot bool))
  (n: nat)
: Ghost nat
  (requires (
    p n == true
  ))
  (ensures (fun k ->
    p k == true /\
    (forall (j: nat) . j < k ==> p j == false)
  ))
= minimal_exists' p n 0

[@@"opaque_to_smt"]
irreducible
let jump_coverage_strong
  (n: pos)
  (l: nat)
  (b: bezout n l)
  (x: nat_up_to n)
: Ghost nat
  (requires True)
  (ensures (fun k ->
    x == iter_fun (jump n l) k (x % b.d) /\
    (forall (k': nat) . k' < k ==> (~ (x == iter_fun (jump n l) k' (x % b.d))))
  ))
= let k' = jump_coverage n l b x in
  minimal_exists (fun k -> x = iter_fun (jump n l) k (x % b.d)) k'

#restart-solver
let jump_iter_mod_q
  (n: pos)
  (l: nat)
  (b: bezout n l)
  (x: nat_up_to n)
  (k: nat)
: Lemma
  (ensures (
    b.q_n > 0 /\
    iter_fun (jump n l) (k % b.q_n) x == iter_fun (jump n l) k x
  ))
= assert (b.q_n > 0);
  let k' = k % b.q_n in
  let qk = k / b.q_n in
  euclidean_division_definition k b.q_n;
  jump_iter n l x k';
  jump_iter n l x k;
  assert (eq2 #int (x + (qk * b.q_n + k') * (b.d * b.q_l)) (x + k' * (b.d * b.q_l) + (qk * b.q_l) * (b.d * b.q_n))) by (int_semiring ());
  assert (x + k * l == x + k' * l + (qk * b.q_l) * n);
  lemma_mod_plus (x + k' * l) (qk * b.q_l) n

let jump_coverage_strong_bound
  (n: pos)
  (l: nat)
  (b: bezout n l)
  (x: nat_up_to n)
: Lemma
  (b.q_n > 0 /\
    jump_coverage_strong n l b x < b.q_n
  )
  [SMTPat (jump_coverage_strong n l b x)]
= let k = jump_coverage_strong n l b x in
  jump_iter_mod_q n l b (x % b.d) k

#restart-solver

[@@"opaque_to_smt"]
irreducible
let mod_eq_elim
  (n: pos)
  (x1 x2: int)
: Ghost int
  (requires (x1 % n == x2 % n))
  (ensures (fun k -> x1 - x2 == k * n))
= euclidean_division_definition x1 n;
  euclidean_division_definition x2 n;
  let q1 = x1 / n in
  let q2 = x2 / n in
  let k = q1 + - q2 in
  let r = x1 % n in
  assert (q1 * n + r + - (q2 * n + r) == k * n) by (int_semiring ());
  k

let mod_eq_intro
  (n: pos)
  (x1 x2: int)
  (k: int)
: Lemma
  (requires (x1 - x2 == k * n))
  (ensures (x1 % n == x2 % n))
= lemma_mod_plus x2 k n

#restart-solver
[@@"opaque_to_smt"]
irreducible
let gauss
  (n: pos)
  (l: pos) // necessary here
  (b: bezout n l)
  (kl kn: int)
: Ghost int
  (requires (
    kl * l == kn * n
  ))
  (ensures (fun k ->
    kl == k * b.q_n
val gauss (n l: pos) (b: bezout n l) (kl kn: int)
    : Ghost int (requires (kl * l == kn * n)) (ensures (fun k -> kl == k * b.q_n))

    n: Prims.pos ->
    l: Prims.pos ->
    b: Steel.ST.GenArraySwap.Proof.bezout n l ->
    kl: Prims.int ->
    kn: Prims.int
  -> Prims.Ghost Prims.int