val lemma_middle_karatsuba: a0:nat -> a1:nat -> b0:nat -> b1:nat ->
  Lemma
   (let s0, t0 = sign_abs a0 a1 in
    let s1, t1 = sign_abs b0 b1 in
    let t23 = t0 * t1 in
    let t01 = a0 * b0 + a1 * b1 in
    let t45 = if s0 = s1 then t01 - t23 else t01 + t23 in
    t45 == a0 * b1 + a1 * b0)
let lemma_middle_karatsuba a0 a1 b0 b1 =
  let s0, t0 = sign_abs a0 a1 in
  let s1, t1 = sign_abs b0 b1 in
  let t23 = t0 * t1 in
  let t01 = a0 * b0 + a1 * b1 in
  let t45 = if s0 = s1 then t01 - t23 else t01 + t23 in
  match (s0, s1) with
  | (Positive, Positive) ->
    calc (==) { //t45
     t01 - t23;
     (==) { }
     a0 * b0 + a1 * b1 - (a0 - a1) * (b0 - b1);
     (==) { Math.Lemmas.distributivity_sub_right (a0 - a1) b0 b1 }
     a0 * b0 + a1 * b1 - ((a0 - a1) * b0 - (a0 - a1) * b1);
     (==) { Math.Lemmas.distributivity_sub_left a0 a1 b0; Math.Lemmas.distributivity_sub_left a0 a1 b1 }
     a0 * b0 + a1 * b1 - (a0 * b0 - a1 * b0 - (a0 * b1 - a1 * b1));
     (==) { }
     a1 * b0 + a0 * b1;
     }

  | (Negative, Negative) ->
    calc (==) { //t45
     t01 - t23;
     (==) { }
     a0 * b0 + a1 * b1 - (a1 - a0) * (b1 - b0);
     (==) { Math.Lemmas.distributivity_sub_right (a1 - a0) b1 b0 }
     a0 * b0 + a1 * b1 - ((a1 - a0) * b1 - (a1 - a0) * b0);
     (==) { Math.Lemmas.distributivity_sub_left a1 a0 b1; Math.Lemmas.distributivity_sub_left a1 a0 b0 }
     a0 * b0 + a1 * b1 - (a1 * b1 - a0 * b1 - (a1 * b0 - a0 * b0));
     (==) { }
     a1 * b0 + a0 * b1;
     }

  | (Positive, Negative) ->
    calc (==) { //t45
     t01 + t23;
     (==) { }
     a0 * b0 + a1 * b1 + (a0 - a1) * (b1 - b0);
     (==) { Math.Lemmas.distributivity_sub_right (a0 - a1) b1 b0 }
     a0 * b0 + a1 * b1 + ((a0 - a1) * b1 - (a0 - a1) * b0);
     (==) { Math.Lemmas.distributivity_sub_left a0 a1 b1; Math.Lemmas.distributivity_sub_left a0 a1 b0 }
     a0 * b0 + a1 * b1 + (a0 * b1 - a1 * b1 - (a0 * b0 - a1 * b0));
     (==) { }
     a1 * b0 + a0 * b1;
     }

  | (Negative, Positive) ->
    calc (==) { //t45
     t01 + t23;
     (==) { }
     a0 * b0 + a1 * b1 + (a1 - a0) * (b0 - b1);
     (==) { Math.Lemmas.distributivity_sub_right (a1 - a0) b0 b1 }
     a0 * b0 + a1 * b1 + ((a1 - a0) * b0 - (a1 - a0) * b1);
     (==) { Math.Lemmas.distributivity_sub_left a1 a0 b0; Math.Lemmas.distributivity_sub_left a1 a0 b1 }
     a0 * b0 + a1 * b1 + (a1 * b0 - a0 * b0 - (a1 * b1 - a0 * b1));
     (==) { }
     a1 * b0 + a0 * b1;
     }
val lemma_middle_karatsuba: a0:nat -> a1:nat -> b0:nat -> b1:nat ->
  Lemma
   (let s0, t0 = sign_abs a0 a1 in
    let s1, t1 = sign_abs b0 b1 in
    let t23 = t0 * t1 in
    let t01 = a0 * b0 + a1 * b1 in
    let t45 = if s0 = s1 then t01 - t23 else t01 + t23 in
    t45 == a0 * b1 + a1 * b0)
let lemma_middle_karatsuba a0 a1 b0 b1 =
let s0, t0 = sign_abs a0 a1 in
let s1, t1 = sign_abs b0 b1 in
let t23 = t0 * t1 in
let t01 = a0 * b0 + a1 * b1 in
let t45 = if s0 = s1 then t01 - t23 else t01 + t23 in
match (s0, s1) with
| Positive, Positive ->
  calc ( == ) {
    t01 - t23;
    ( == ) { () }
    a0 * b0 + a1 * b1 - (a0 - a1) * (b0 - b1);
    ( == ) { Math.Lemmas.distributivity_sub_right (a0 - a1) b0 b1 }
    a0 * b0 + a1 * b1 - ((a0 - a1) * b0 - (a0 - a1) * b1);
    ( == ) { (Math.Lemmas.distributivity_sub_left a0 a1 b0;
      Math.Lemmas.distributivity_sub_left a0 a1 b1) }
    a0 * b0 + a1 * b1 - (a0 * b0 - a1 * b0 - (a0 * b1 - a1 * b1));
    ( == ) { () }
    a1 * b0 + a0 * b1;
  }
| Negative, Negative ->
  calc ( == ) {
    t01 - t23;
    ( == ) { () }
    a0 * b0 + a1 * b1 - (a1 - a0) * (b1 - b0);
    ( == ) { Math.Lemmas.distributivity_sub_right (a1 - a0) b1 b0 }
    a0 * b0 + a1 * b1 - ((a1 - a0) * b1 - (a1 - a0) * b0);
    ( == ) { (Math.Lemmas.distributivity_sub_left a1 a0 b1;
      Math.Lemmas.distributivity_sub_left a1 a0 b0) }
    a0 * b0 + a1 * b1 - (a1 * b1 - a0 * b1 - (a1 * b0 - a0 * b0));
    ( == ) { () }
    a1 * b0 + a0 * b1;
  }
| Positive, Negative ->
  calc ( == ) {
    t01 + t23;
    ( == ) { () }
    a0 * b0 + a1 * b1 + (a0 - a1) * (b1 - b0);
    ( == ) { Math.Lemmas.distributivity_sub_right (a0 - a1) b1 b0 }
    a0 * b0 + a1 * b1 + ((a0 - a1) * b1 - (a0 - a1) * b0);
    ( == ) { (Math.Lemmas.distributivity_sub_left a0 a1 b1;
      Math.Lemmas.distributivity_sub_left a0 a1 b0) }
    a0 * b0 + a1 * b1 + (a0 * b1 - a1 * b1 - (a0 * b0 - a1 * b0));
    ( == ) { () }
    a1 * b0 + a0 * b1;
  }
| Negative, Positive ->
  calc ( == ) {
    t01 + t23;
    ( == ) { () }
    a0 * b0 + a1 * b1 + (a1 - a0) * (b0 - b1);
    ( == ) { Math.Lemmas.distributivity_sub_right (a1 - a0) b0 b1 }
    a0 * b0 + a1 * b1 + ((a1 - a0) * b0 - (a1 - a0) * b1);
    ( == ) { (Math.Lemmas.distributivity_sub_left a1 a0 b0;
      Math.Lemmas.distributivity_sub_left a1 a0 b1) }
    a0 * b0 + a1 * b1 + (a1 * b0 - a0 * b0 - (a1 * b1 - a0 * b1));
    ( == ) { () }
    a1 * b0 + a0 * b1;
  }
Hacl.Spec.Karatsuba.Lemmas.fst.checked
prims.fst.checked Lib.IntTypes.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.Karatsuba.Lemmas.fst
Prims.nat Hacl.Spec.Karatsuba.Lemmas.sign FStar.Pervasives.Native.Mktuple2 FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Subtraction Prims.op_Addition FStar.Mul.op_Star Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash FStar.Math.Lemmas.distributivity_sub_right FStar.Math.Lemmas.distributivity_sub_left Prims.op_Equality Prims.bool FStar.Pervasives.Native.tuple2 Hacl.Spec.Karatsuba.Lemmas.sign_abs
module Hacl.Spec.Karatsuba.Lemmas

open FStar.Mul
open Lib.IntTypes

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

type sign =
  | Positive
  | Negative

let abs (a:nat) (b:nat) : nat =
  if a < b then b - a else a - b

val sign_abs: a:nat -> b:nat ->
  Pure (tuple2 sign nat)
  (requires True)
  (ensures  fun (s, res) -> res == abs a b /\
    s == (if a < b then Negative else Positive))

let sign_abs a b =
  if a < b then (Negative, b - a) else (Positive, a - b)


val lemma_double_p: pbits:pos -> aLen:nat{aLen % 2 = 0} ->
  Lemma (let p = pow2 (aLen / 2 * pbits) in p * p == pow2 (pbits * aLen))
let lemma_double_p pbits aLen =
  let p = pow2 (aLen / 2 * pbits) in
  calc (==) {
    p * p;
    (==) { Math.Lemmas.pow2_plus (aLen / 2 * pbits) (aLen / 2 * pbits) }
    pow2 (aLen / 2 * pbits + aLen / 2 * pbits);
    (==) { Math.Lemmas.distributivity_add_left (aLen / 2) (aLen / 2) pbits }
    pow2 ((aLen / 2 * 2) * pbits);
    (==) { Math.Lemmas.lemma_div_exact aLen 2 }
    pow2 (aLen * pbits);
    }


val lemma_bn_halves: pbits:pos -> aLen:nat{aLen % 2 = 0} -> a:nat{a < pow2 (pbits * aLen)} ->
  Lemma (let p = pow2 (aLen / 2 * pbits) in a / p < p /\ a % p < p /\ a == a / p * p + a % p)
let lemma_bn_halves pbits aLen a = lemma_double_p pbits aLen


val lemma_middle_karatsuba: a0:nat -> a1:nat -> b0:nat -> b1:nat ->
  Lemma
   (let s0, t0 = sign_abs a0 a1 in
    let s1, t1 = sign_abs b0 b1 in
    let t23 = t0 * t1 in
    let t01 = a0 * b0 + a1 * b1 in
    let t45 = if s0 = s1 then t01 - t23 else t01 + t23 in
    t45 == a0 * b1 + a1 * b0)
val lemma_middle_karatsuba: a0:nat -> a1:nat -> b0:nat -> b1:nat ->
  Lemma
   (let s0, t0 = sign_abs a0 a1 in
    let s1, t1 = sign_abs b0 b1 in
    let t23 = t0 * t1 in
    let t01 = a0 * b0 + a1 * b1 in
    let t45 = if s0 = s1 then t01 - t23 else t01 + t23 in
    t45 == a0 * b1 + a1 * b0)
a0: Prims.nat -> a1: Prims.nat -> b0: Prims.nat -> b1: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      (let _ = Hacl.Spec.Karatsuba.Lemmas.sign_abs a0 a1 in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ s0 t0 = _ in
          let _ = Hacl.Spec.Karatsuba.Lemmas.sign_abs b0 b1 in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ s1 t1 = _ in
            let t23 = t0 * t1 in
            let t01 = a0 * b0 + a1 * b1 in
            let t45 =
              (match s0 = s1 with
                | true -> t01 - t23
                | _ -> t01 + t23)
              <:
              Prims.int
            in
            t45 == a0 * b1 + a1 * b0)
          <:
          Type0)
        <:
        Type0))