val minus_x_mul_pow2_256_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires felem_fits5 f m)
  (ensures
   (let x, r = minus_x_mul_pow2_256 f in
    let (r0,r1,r2,r3,r4) = r in
    let (m0,m1,m2,m3,m4) = m in
    let (t0,t1,t2,t3,t4) = f in
    v x < pow2 16 /\ v x = v t4 / pow2 48 /\
    v r4 = v t4 % pow2 48 /\
    as_nat5 r == as_nat5 f - v x * pow2 256 /\
    felem_fits5 r (m0,m1,m2,m3,1)))
let minus_x_mul_pow2_256_lemma m f =
  let (m0,m1,m2,m3,m4) = m in
  let (t0,t1,t2,t3,t4) = f in

  let x = t4 >>. 48ul in let t4' = t4 &. mask48 in
  LD.lemma_mask48 t4;

  let r = (t0,t1,t2,t3,t4') in
  calc (==) { // as_nat5 f
    v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + v t4 * pow208;
    (==) { Math.Lemmas.euclidean_division_definition (v t4) (pow2 48) }
    v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + (v t4 / pow2 48 * pow2 48 + v t4 % pow2 48) * pow208;
    (==) { Math.Lemmas.distributivity_add_left (v t4 / pow2 48 * pow2 48) (v t4 % pow2 48) pow208 }
    v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + (v t4 / pow2 48 * pow2 48) * pow208 + (v t4 % pow2 48) * pow208;
    (==) { }
    (v x * pow2 48) * pow208 + as_nat5 r;
    (==) { Math.Lemmas.paren_mul_right (v x) (pow2 48) pow208; Math.Lemmas.pow2_plus 48 208 }
    v x * pow2 256 + as_nat5 r;
  };

  Math.Lemmas.lemma_div_lt (v t4) 64 48
val minus_x_mul_pow2_256_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires felem_fits5 f m)
  (ensures
   (let x, r = minus_x_mul_pow2_256 f in
    let (r0,r1,r2,r3,r4) = r in
    let (m0,m1,m2,m3,m4) = m in
    let (t0,t1,t2,t3,t4) = f in
    v x < pow2 16 /\ v x = v t4 / pow2 48 /\
    v r4 = v t4 % pow2 48 /\
    as_nat5 r == as_nat5 f - v x * pow2 256 /\
    felem_fits5 r (m0,m1,m2,m3,1)))
let minus_x_mul_pow2_256_lemma m f =
let m0, m1, m2, m3, m4 = m in
let t0, t1, t2, t3, t4 = f in
let x = t4 >>. 48ul in
let t4' = t4 &. mask48 in
LD.lemma_mask48 t4;
let r = (t0, t1, t2, t3, t4') in
calc ( == ) {
  v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + v t4 * pow208;
  ( == ) { Math.Lemmas.euclidean_division_definition (v t4) (pow2 48) }
  v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 +
  ((v t4 / pow2 48) * pow2 48 + v t4 % pow2 48) * pow208;
  ( == ) { Math.Lemmas.distributivity_add_left ((v t4 / pow2 48) * pow2 48) (v t4 % pow2 48) pow208 }
  v t0 + v t1 * pow52 + v t2 * pow104 + v t3 * pow156 + ((v t4 / pow2 48) * pow2 48) * pow208 +
  (v t4 % pow2 48) * pow208;
  ( == ) { () }
  (v x * pow2 48) * pow208 + as_nat5 r;
  ( == ) { (Math.Lemmas.paren_mul_right (v x) (pow2 48) pow208;
    Math.Lemmas.pow2_plus 48 208) }
  v x * pow2 256 + as_nat5 r;
};
Math.Lemmas.lemma_div_lt (v t4) 64 48
Hacl.Spec.K256.Field52.Lemmas2.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.MathLemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.Lemmas.fst.checked Hacl.Spec.K256.Field52.Definitions.fst.checked Hacl.Spec.K256.Field52.fst.checked FStar.UInt32.fsti.checked FStar.UInt.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.K256.Field52.Lemmas2.fst
Hacl.Spec.K256.Field52.Definitions.scale64_5 Hacl.Spec.K256.Field52.Definitions.felem5 Prims.nat Lib.IntTypes.uint64 FStar.Math.Lemmas.lemma_div_lt Lib.IntTypes.v Lib.IntTypes.U64 Lib.IntTypes.SEC Prims.unit FStar.Calc.calc_finish Prims.int Prims.eq2 Prims.op_Addition FStar.Mul.op_Star Hacl.Spec.K256.Field52.Definitions.pow52 Hacl.Spec.K256.Field52.Definitions.pow104 Hacl.Spec.K256.Field52.Definitions.pow156 Hacl.Spec.K256.Field52.Definitions.pow208 Prims.pow2 Hacl.Spec.K256.Field52.Definitions.as_nat5 Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Prims.op_Division Prims.op_Modulus FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Math.Lemmas.euclidean_division_definition Prims.squash FStar.Math.Lemmas.distributivity_add_left FStar.Math.Lemmas.pow2_plus FStar.Math.Lemmas.paren_mul_right FStar.Pervasives.Native.tuple5 Lib.IntTypes.int_t FStar.Pervasives.Native.Mktuple5 Hacl.Spec.K256.Field52.Definitions.Lemmas.lemma_mask48 Lib.IntTypes.op_Amp_Dot Hacl.Spec.K256.Field52.Definitions.mask48 Lib.IntTypes.op_Greater_Greater_Dot FStar.UInt32.__uint_to_t
module Hacl.Spec.K256.Field52.Lemmas2

open FStar.Mul
open Lib.IntTypes

module S = Spec.K256

include Hacl.Spec.K256.Field52.Definitions
include Hacl.Spec.K256.Field52

module ML = Hacl.Spec.K256.MathLemmas
module LD = Hacl.Spec.K256.Field52.Definitions.Lemmas

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

///  Normalize-weak

val minus_x_mul_pow2_256_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires felem_fits5 f m)
  (ensures
   (let x, r = minus_x_mul_pow2_256 f in
    let (r0,r1,r2,r3,r4) = r in
    let (m0,m1,m2,m3,m4) = m in
    let (t0,t1,t2,t3,t4) = f in
    v x < pow2 16 /\ v x = v t4 / pow2 48 /\
    v r4 = v t4 % pow2 48 /\
    as_nat5 r == as_nat5 f - v x * pow2 256 /\
    felem_fits5 r (m0,m1,m2,m3,1)))
val minus_x_mul_pow2_256_lemma: m:scale64_5 -> f:felem5 -> Lemma
  (requires felem_fits5 f m)
  (ensures
   (let x, r = minus_x_mul_pow2_256 f in
    let (r0,r1,r2,r3,r4) = r in
    let (m0,m1,m2,m3,m4) = m in
    let (t0,t1,t2,t3,t4) = f in
    v x < pow2 16 /\ v x = v t4 / pow2 48 /\
    v r4 = v t4 % pow2 48 /\
    as_nat5 r == as_nat5 f - v x * pow2 256 /\
    felem_fits5 r (m0,m1,m2,m3,1)))
m: Hacl.Spec.K256.Field52.Definitions.scale64_5 -> f: Hacl.Spec.K256.Field52.Definitions.felem5
  -> FStar.Pervasives.Lemma (requires Hacl.Spec.K256.Field52.Definitions.felem_fits5 f m)
      (ensures
        (let _ = Hacl.Spec.K256.Field52.minus_x_mul_pow2_256 f in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ x r = _ in
            let _ = r in
            (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ _ _ _ _ r4 = _ in
              let _ = m in
              (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ m0 m1 m2 m3 _ = _ in
                let _ = f in
                (let FStar.Pervasives.Native.Mktuple5 #_ #_ #_ #_ #_ _ _ _ _ t4 = _ in
                  Lib.IntTypes.v x < Prims.pow2 16 /\
                  Lib.IntTypes.v x = Lib.IntTypes.v t4 / Prims.pow2 48 /\
                  Lib.IntTypes.v r4 = Lib.IntTypes.v t4 % Prims.pow2 48 /\
                  Hacl.Spec.K256.Field52.Definitions.as_nat5 r ==
                  Hacl.Spec.K256.Field52.Definitions.as_nat5 f - Lib.IntTypes.v x * Prims.pow2 256 /\
                  Hacl.Spec.K256.Field52.Definitions.felem_fits5 r (m0, m1, m2, m3, 1))
                <:
                Type0)
              <:
              Type0)
            <:
            Type0)
          <:
          Type0))