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_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);
}
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.pos Prims.nat Prims.b2t Prims.op_Equality Prims.int Prims.op_Modulus FStar.Calc.calc_finish Prims.eq2 FStar.Mul.op_Star Prims.pow2 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Prims.op_Division Prims.op_Addition FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.pow2_plus Prims.squash FStar.Math.Lemmas.distributivity_add_left FStar.Math.Lemmas.lemma_div_exact
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} ->
val lemma_double_p: pbits:pos -> aLen:nat{aLen % 2 = 0} ->
  Lemma (let p = pow2 (aLen / 2 * pbits) in p * p == pow2 (pbits * aLen))
pbits: Prims.pos -> aLen: Prims.nat{aLen % 2 = 0}
  -> FStar.Pervasives.Lemma
    (ensures
      (let p = Prims.pow2 ((aLen / 2) * pbits) in
        p * p == Prims.pow2 (pbits * aLen)))