val bn_karatsuba_sqr_lemma:
    #t:limb_t
  -> #aLen:size_nat{aLen + aLen <= max_size_t}
  -> a:lbignum t aLen ->
  Lemma (bn_karatsuba_sqr a == bn_mul a a /\
    bn_v (bn_karatsuba_sqr a) == bn_v a * bn_v a)
let bn_karatsuba_sqr_lemma #t #aLen a =
  Hacl.Spec.Bignum.Karatsuba.bn_karatsuba_sqr_lemma a
val bn_karatsuba_sqr_lemma:
    #t:limb_t
  -> #aLen:size_nat{aLen + aLen <= max_size_t}
  -> a:lbignum t aLen ->
  Lemma (bn_karatsuba_sqr a == bn_mul a a /\
    bn_v (bn_karatsuba_sqr a) == bn_v a * bn_v a)
let bn_karatsuba_sqr_lemma #t #aLen a =
Hacl.Spec.Bignum.Karatsuba.bn_karatsuba_sqr_lemma a
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 Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.max_size_t Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Bignum.Karatsuba.bn_karatsuba_sqr_lemma Prims.unit
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


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


let bn_add_mod_n #t #len n a b =
  let c0, res0 = bn_add a b in
  bn_reduce_once n c0 res0


let bn_add_mod_n_lemma #t #len n a b =
  let c0, res0 = bn_add a b in
  bn_add_lemma a b;
  bn_reduce_once_lemma n c0 res0


let bn_sub_mod_n #t #len n a b =
  let c0, res0 = bn_sub a b in
  let c1, res1 = bn_add res0 n in
  let c = uint #t 0 -. c0 in
  map2 (mask_select c) res1 res0


let bn_sub_mod_n_lemma #t #len n a b =
  let c0, res0 = bn_sub a b in
  bn_sub_lemma a b;
  assert (bn_v res0 - v c0 * pow2 (bits t * len) == bn_v a - bn_v b);
  let c1, res1 = bn_add res0 n in
  let c = uint #t 0 -. c0 in
  assert (v c == 0 \/ v c == v (ones t SEC));
  let res = map2 (mask_select c) res1 res0 in
  lseq_mask_select_lemma res1 res0 c;

  if v c0 = 0 then begin
    assert (bn_v res0 == bn_v a - bn_v b);
    Math.Lemmas.small_mod (bn_v res0) (bn_v n);
    assert (bn_v res == (bn_v a - bn_v b) % bn_v n);
    () end
  else begin
    bn_add_lemma res0 n;
    assert (bn_v res1 + v c1 * pow2 (bits t * len) == bn_v res0 + bn_v n);

    bn_eval_bound res0 len;
    bn_eval_bound res1 len;
    bn_eval_bound n len;
    assert (v c0 - v c1 = 0);
    assert (bn_v res1 == bn_v a - bn_v b + bn_v n);
    assert (bn_v res1 < bn_v n);
    Math.Lemmas.modulo_addition_lemma (bn_v a - bn_v b) (bn_v n) 1;
    Math.Lemmas.small_mod (bn_v res1) (bn_v n);
    assert (bn_v res == (bn_v a - bn_v b) % bn_v n);
    () end


let bn_mul1 #t #aLen a b1 =
  Hacl.Spec.Bignum.Multiplication.bn_mul1 a b1

let bn_mul1_lemma #t #aLen a b1 =
  Hacl.Spec.Bignum.Multiplication.bn_mul1_lemma a b1

let bn_mul #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Multiplication.bn_mul a b

let bn_mul_lemma #t #aLen #bLen a b =
  Hacl.Spec.Bignum.Multiplication.bn_mul_lemma a b

let bn_karatsuba_mul #t #aLen a b =
  Hacl.Spec.Bignum.Karatsuba.bn_karatsuba_mul a b

let bn_karatsuba_mul_lemma #t #aLen a b =
  Hacl.Spec.Bignum.Karatsuba.bn_karatsuba_mul_lemma a b

let bn_sqr #t #aLen a =
  Hacl.Spec.Bignum.Squaring.bn_sqr a

let bn_sqr_lemma #t #aLen a =
  Hacl.Spec.Bignum.Squaring.bn_sqr_lemma a

let bn_karatsuba_sqr #t #aLen a =
  Hacl.Spec.Bignum.Karatsuba.bn_karatsuba_sqr a
val bn_karatsuba_sqr_lemma:
    #t:limb_t
  -> #aLen:size_nat{aLen + aLen <= max_size_t}
  -> a:lbignum t aLen ->
  Lemma (bn_karatsuba_sqr a == bn_mul a a /\
    bn_v (bn_karatsuba_sqr a) == bn_v a * bn_v a)
a: Hacl.Spec.Bignum.Definitions.lbignum t aLen
  -> FStar.Pervasives.Lemma
    (ensures
      Hacl.Spec.Bignum.bn_karatsuba_sqr a == Hacl.Spec.Bignum.bn_mul a a /\
      Hacl.Spec.Bignum.Definitions.bn_v (Hacl.Spec.Bignum.bn_karatsuba_sqr a) ==
      Hacl.Spec.Bignum.Definitions.bn_v a * Hacl.Spec.Bignum.Definitions.bn_v a)