val bn_reduce_once_lemma:
    #t:limb_t
  -> #len:size_nat
  -> n:lbignum t len
  -> c:carry t
  -> a:lbignum t len -> Lemma
  (requires v c * pow2 (bits t * len) + bn_v a < 2 * bn_v n)
  (ensures  bn_v (bn_reduce_once n c a) == (v c * pow2 (bits t * len) + bn_v a) % bn_v n)
let bn_reduce_once_lemma #t #len n c0 res0 =
  let pbits = bits t in
  let tmp = bn_v res0 + v c0 * pow2 (pbits * len) in
  let c1, res1 = bn_sub res0 n in
  bn_sub_lemma res0 n;
  assert (bn_v res1 - v c1 * pow2 (pbits * len) == bn_v res0 - bn_v n);
  let c = c0 -. c1 in
  assert (bn_v res1 + (v c0 - v c1) * pow2 (pbits * len) == tmp - bn_v n);
  let res = map2 (mask_select c) res0 res1 in

  if tmp < bn_v n then begin
    assert (v c0 == 0);
    assert (v c1 == 1);
    assert (v c == pow2 pbits - 1);
    lseq_mask_select_lemma res0 res1 c;
    assert (bn_v res == bn_v res0);
    Math.Lemmas.small_mod tmp (bn_v n);
    assert (bn_v res == tmp % bn_v n) end
  else begin
    assert (tmp - bn_v n < bn_v n);
    bn_eval_bound res1 len;
    bn_eval_bound n len;
    assert (v c == 0);
    lseq_mask_select_lemma res0 res1 c;
    assert (bn_v res == bn_v res1);
    Math.Lemmas.modulo_addition_lemma tmp (bn_v n) (- 1);
    assert (bn_v res % bn_v n == tmp % bn_v n);
    Math.Lemmas.small_mod (bn_v res) (bn_v n) end
val bn_reduce_once_lemma:
    #t:limb_t
  -> #len:size_nat
  -> n:lbignum t len
  -> c:carry t
  -> a:lbignum t len -> Lemma
  (requires v c * pow2 (bits t * len) + bn_v a < 2 * bn_v n)
  (ensures  bn_v (bn_reduce_once n c a) == (v c * pow2 (bits t * len) + bn_v a) % bn_v n)
let bn_reduce_once_lemma #t #len n c0 res0 =
let pbits = bits t in
let tmp = bn_v res0 + v c0 * pow2 (pbits * len) in
let c1, res1 = bn_sub res0 n in
bn_sub_lemma res0 n;
assert (bn_v res1 - v c1 * pow2 (pbits * len) == bn_v res0 - bn_v n);
let c = c0 -. c1 in
assert (bn_v res1 + (v c0 - v c1) * pow2 (pbits * len) == tmp - bn_v n);
let res = map2 (mask_select c) res0 res1 in
if tmp < bn_v n
then
  (assert (v c0 == 0);
    assert (v c1 == 1);
    assert (v c == pow2 pbits - 1);
    lseq_mask_select_lemma res0 res1 c;
    assert (bn_v res == bn_v res0);
    Math.Lemmas.small_mod tmp (bn_v n);
    assert (bn_v res == tmp % bn_v n))
else
  (assert (tmp - bn_v n < bn_v n);
    bn_eval_bound res1 len;
    bn_eval_bound n len;
    assert (v c == 0);
    lseq_mask_select_lemma res0 res1 c;
    assert (bn_v res == bn_v res1);
    Math.Lemmas.modulo_addition_lemma tmp (bn_v n) (- 1);
    assert (bn_v res % bn_v n == tmp % bn_v n);
    Math.Lemmas.small_mod (bn_v res) (bn_v n))
Hacl.Spec.Bignum.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.Bignum.Squaring.fst.checked Hacl.Spec.Bignum.Multiplication.fst.checked Hacl.Spec.Bignum.Lib.fst.checked Hacl.Spec.Bignum.Karatsuba.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Spec.Bignum.Comparison.fst.checked Hacl.Spec.Bignum.Addition.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked
Hacl.Spec.Bignum.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_nat Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Base.carry Prims.op_LessThan Hacl.Spec.Bignum.Definitions.bn_v Prims._assert Prims.eq2 Prims.int Prims.op_Modulus Prims.unit FStar.Math.Lemmas.small_mod Prims.nat Hacl.Spec.Bignum.Base.lseq_mask_select_lemma Lib.IntTypes.v Lib.IntTypes.SEC Prims.op_Subtraction Prims.pow2 Prims.bool FStar.Math.Lemmas.modulo_addition_lemma Prims.op_Minus Hacl.Spec.Bignum.Definitions.bn_eval_bound Prims.b2t Lib.Sequence.lseq Hacl.Spec.Bignum.Definitions.limb Prims.l_Forall Prims.l_imp Lib.Sequence.index Hacl.Spec.Bignum.Base.mask_select Lib.Sequence.map2 Prims.op_Addition FStar.Mul.op_Star Lib.IntTypes.int_t Lib.IntTypes.op_Subtraction_Dot Hacl.Spec.Bignum.bn_sub_lemma FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.bn_sub Lib.IntTypes.bits
module Hacl.Spec.Bignum

module Loops = Lib.LoopCombinators


#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"

let bn_add1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1 a b1

let bn_add1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_add1_lemma a b1

let bn_sub1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_sub1 a b1

let bn_sub1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Addition.bn_sub1_lemma a b1

let bn_add #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_add a b

let bn_add_lemma #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_add_lemma a b

let bn_sub #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_sub a b

let bn_sub_lemma #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Addition.bn_sub_lemma a b

let bn_reduce_once #t #len n c0 a =
  let c1, res = bn_sub a n in
  let c = c0 -. c1 in
  map2 (mask_select c) a res
val bn_reduce_once_lemma:
    #t:limb_t
  -> #len:size_nat
  -> n:lbignum t len
  -> c:carry t
  -> a:lbignum t len -> Lemma
  (requires v c * pow2 (bits t * len) + bn_v a < 2 * bn_v n)
  (ensures  bn_v (bn_reduce_once n c a) == (v c * pow2 (bits t * len) + bn_v a) % bn_v n)

    n: Hacl.Spec.Bignum.Definitions.lbignum t len ->
    c: Hacl.Spec.Bignum.Base.carry t ->
    a: Hacl.Spec.Bignum.Definitions.lbignum t len
  -> FStar.Pervasives.Lemma
      (requires
        Lib.IntTypes.v c * Prims.pow2 (Lib.IntTypes.bits t * len) +
        Hacl.Spec.Bignum.Definitions.bn_v a <
        2 * Hacl.Spec.Bignum.Definitions.bn_v n)
      (ensures
        Hacl.Spec.Bignum.Definitions.bn_v (Hacl.Spec.Bignum.bn_reduce_once n c a) ==
        (Lib.IntTypes.v c * Prims.pow2 (Lib.IntTypes.bits t * len) +
          Hacl.Spec.Bignum.Definitions.bn_v a) %
        Hacl.Spec.Bignum.Definitions.bn_v n)