val bn_sign_abs_lemma:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> b:lbignum t aLen ->
  Lemma (let c, res = bn_sign_abs a b in
   bn_v res == K.abs (bn_v a) (bn_v b) /\
   v c == (if bn_v a < bn_v b then 1 else 0))
let bn_sign_abs_lemma #t #aLen a b =
  let s, r = K.sign_abs (bn_v a) (bn_v b) in

  let c0, t0 = bn_sub a b in
  bn_sub_lemma a b;
  assert (bn_v t0 - v c0 * pow2 (bits t * aLen) == bn_v a - bn_v b);

  let c1, t1 = bn_sub b a in
  bn_sub_lemma b a;
  assert (bn_v t1 - v c1 * pow2 (bits t * aLen) == bn_v b - bn_v a);

  let mask = uint #t 0 -. c0 in
  assert (v mask == (if v c0 = 0 then 0 else v (ones t SEC)));
  let res = map2 (mask_select mask) t1 t0 in
  lseq_mask_select_lemma t1 t0 mask;
  assert (bn_v res == (if v mask = 0 then bn_v t0 else bn_v t1));

  bn_eval_bound a aLen;
  bn_eval_bound b aLen;
  bn_eval_bound t0 aLen;
  bn_eval_bound t1 aLen
val bn_sign_abs_lemma:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> b:lbignum t aLen ->
  Lemma (let c, res = bn_sign_abs a b in
   bn_v res == K.abs (bn_v a) (bn_v b) /\
   v c == (if bn_v a < bn_v b then 1 else 0))
let bn_sign_abs_lemma #t #aLen a b =
let s, r = K.sign_abs (bn_v a) (bn_v b) in
let c0, t0 = bn_sub a b in
bn_sub_lemma a b;
assert (bn_v t0 - v c0 * pow2 (bits t * aLen) == bn_v a - bn_v b);
let c1, t1 = bn_sub b a in
bn_sub_lemma b a;
assert (bn_v t1 - v c1 * pow2 (bits t * aLen) == bn_v b - bn_v a);
let mask = uint #t 0 -. c0 in
assert (v mask == (if v c0 = 0 then 0 else v (ones t SEC)));
let res = map2 (mask_select mask) t1 t0 in
lseq_mask_select_lemma t1 t0 mask;
assert (bn_v res == (if v mask = 0 then bn_v t0 else bn_v t1));
bn_eval_bound a aLen;
bn_eval_bound b aLen;
bn_eval_bound t0 aLen;
bn_eval_bound t1 aLen
Hacl.Spec.Bignum.Karatsuba.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Lib.fst.checked Hacl.Spec.Karatsuba.Lemmas.fst.checked Hacl.Spec.Bignum.Squaring.fst.checked Hacl.Spec.Bignum.Multiplication.fst.checked Hacl.Spec.Bignum.Lib.fst.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Base.fst.checked Hacl.Spec.Bignum.Addition.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Hacl.Spec.Bignum.Karatsuba.fst
Hacl.Spec.Bignum.Definitions.limb_t Lib.IntTypes.size_nat Hacl.Spec.Bignum.Definitions.lbignum Hacl.Spec.Karatsuba.Lemmas.sign Prims.nat Hacl.Spec.Bignum.Base.carry Hacl.Spec.Bignum.Definitions.bn_eval_bound Prims.unit Prims._assert Prims.eq2 Hacl.Spec.Bignum.Definitions.bn_v Prims.op_Equality Prims.int Lib.IntTypes.v Lib.IntTypes.SEC Prims.bool Hacl.Spec.Bignum.Base.lseq_mask_select_lemma Lib.Sequence.lseq Hacl.Spec.Bignum.Definitions.limb Prims.l_Forall Prims.l_imp Prims.b2t Prims.op_LessThan Lib.Sequence.index Hacl.Spec.Bignum.Base.mask_select Lib.Sequence.map2 Lib.IntTypes.ones Lib.IntTypes.int_t Lib.IntTypes.op_Subtraction_Dot Lib.IntTypes.uint Prims.op_Subtraction FStar.Mul.op_Star Prims.pow2 Lib.IntTypes.bits Hacl.Spec.Bignum.Addition.bn_sub_lemma FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.Addition.bn_sub Hacl.Spec.Karatsuba.Lemmas.sign_abs
module Hacl.Spec.Bignum.Karatsuba

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence
open Lib.LoopCombinators

open Hacl.Spec.Bignum.Definitions
open Hacl.Spec.Bignum.Base
open Hacl.Spec.Bignum.Lib
open Hacl.Spec.Lib

open Hacl.Spec.Bignum.Addition
open Hacl.Spec.Bignum.Multiplication
open Hacl.Spec.Bignum.Squaring

module K = Hacl.Spec.Karatsuba.Lemmas

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

inline_for_extraction noextract
let bn_mul_threshold = 32

(* this carry means nothing but the sign of the result *)
val bn_sign_abs:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> b:lbignum t aLen ->
  tuple2 (carry t) (lbignum t aLen)

let bn_sign_abs #t #aLen a b =
  let c0, t0 = bn_sub a b in
  let c1, t1 = bn_sub b a in
  let res = map2 (mask_select (uint #t 0 -. c0)) t1 t0 in
  c0, res


val bn_sign_abs_lemma:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> b:lbignum t aLen ->
  Lemma (let c, res = bn_sign_abs a b in
   bn_v res == K.abs (bn_v a) (bn_v b) /\
   v c == (if bn_v a < bn_v b then 1 else 0))
val bn_sign_abs_lemma:
    #t:limb_t
  -> #aLen:size_nat
  -> a:lbignum t aLen
  -> b:lbignum t aLen ->
  Lemma (let c, res = bn_sign_abs a b in
   bn_v res == K.abs (bn_v a) (bn_v b) /\
   v c == (if bn_v a < bn_v b then 1 else 0))
a: Hacl.Spec.Bignum.Definitions.lbignum t aLen -> b: Hacl.Spec.Bignum.Definitions.lbignum t aLen
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = Hacl.Spec.Bignum.Karatsuba.bn_sign_abs a b in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ c res = _ in
          Hacl.Spec.Bignum.Definitions.bn_v res ==
          Hacl.Spec.Karatsuba.Lemmas.abs (Hacl.Spec.Bignum.Definitions.bn_v a)
            (Hacl.Spec.Bignum.Definitions.bn_v b) /\
          Lib.IntTypes.v c ==
          (match Hacl.Spec.Bignum.Definitions.bn_v a < Hacl.Spec.Bignum.Definitions.bn_v b with
            | true -> 1
            | _ -> 0))
        <:
        Type0))