val bn_is_eq_mask4: x:felem -> y:felem -> Stack uint64
  (requires fun h -> live h x /\ live h y)
  (ensures fun h0 r h1 -> modifies0 h0 h1 /\
    (if as_nat h0 x = as_nat h0 y then v r == ones_v U64 else v r = 0))
let bn_is_eq_mask4 a b =
  let h0 = ST.get () in
  SN.bn_eq_mask_lemma (as_seq h0 a) (as_seq h0 b);
  bn_v_is_as_nat (as_seq h0 a);
  bn_v_is_as_nat (as_seq h0 b);
  BN.bn_eq_mask #U64 4ul a b
val bn_is_eq_mask4: x:felem -> y:felem -> Stack uint64
  (requires fun h -> live h x /\ live h y)
  (ensures fun h0 r h1 -> modifies0 h0 h1 /\
    (if as_nat h0 x = as_nat h0 y then v r == ones_v U64 else v r = 0))
let bn_is_eq_mask4 a b =
let h0 = ST.get () in
SN.bn_eq_mask_lemma (as_seq h0 a) (as_seq h0 b);
bn_v_is_as_nat (as_seq h0 a);
bn_v_is_as_nat (as_seq h0 b);
BN.bn_eq_mask #U64 4ul a b
Hacl.Impl.P256.Bignum.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Spec.Bignum.fsti.checked Hacl.Bignum.Convert.fst.checked Hacl.Bignum.Base.fst.checked Hacl.Bignum.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked
Hacl.Impl.P256.Bignum.fst
Hacl.Impl.P256.Bignum.felem Hacl.Bignum.bn_eq_mask Lib.IntTypes.U64 FStar.UInt32.__uint_to_t Hacl.Bignum.Definitions.limb Prims.unit Hacl.Impl.P256.Bignum.bn_v_is_as_nat Lib.Buffer.as_seq Lib.Buffer.MUT Lib.IntTypes.uint64 Lib.IntTypes.size Hacl.Spec.Bignum.bn_eq_mask_lemma Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Impl.P256.Bignum

open FStar.Mul
open FStar.HyperStack.All
open FStar.HyperStack
module ST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

module BN = Hacl.Bignum
module SN = Hacl.Spec.Bignum
module BD = Hacl.Spec.Bignum.Definitions
module LSeq = Lib.Sequence

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

let bn_v_is_as_nat a =
  let open Lib.Sequence in
  let open Hacl.Spec.Bignum.Definitions in
  assert_norm (pow2 64 * pow2 64 = pow2 128);
  assert_norm (pow2 64 * pow2 64 * pow2 64 = pow2 192);

  calc (==) {
    bn_v a;
  (==) { bn_eval1 (slice a 0 1); bn_eval_split_i #U64 a 1 }
    v a.[0] + pow2 64 * bn_v (slice a 1 4);
  (==) { bn_eval_split_i #U64 (slice a 1 4) 1; bn_eval1 (slice a 1 2) }
    v a.[0] + pow2 64 * v a.[1] + pow2 64 * pow2 64 * bn_v (slice a 2 4);
  (==) { bn_eval_split_i #U64 (slice a 2 4) 1; bn_eval1 (slice a 2 3) }
    v a.[0] + pow2 64 * v a.[1] + pow2 64 * pow2 64 * v a.[2]
    + pow2 64 * pow2 64 * pow2 64 * bn_v (slice a 3 4);
  (==) { bn_eval1 (slice a 3 4) }
    v a.[0] + pow2 64 * v a.[1] + pow2 64 * pow2 64 * v a.[2]
    + pow2 64 * pow2 64 * pow2 64 * v a.[3];
  }


///  Create a bignum

let create_felem () =
  BD.bn_eval_zeroes #U64 4 4;
  create 4ul (u64 0)


let create_widefelem () =
  BD.bn_eval_zeroes #U64 8 8;
  create 8ul (u64 0)


let bn_make_u64_4 res a0 a1 a2 a3 =
  let h0 = ST.get () in
  upd res 0ul a0;
  let h1 = ST.get () in
  upd res 1ul a1;
  let h2 = ST.get () in
  upd res 2ul a2;
  let h3 = ST.get () in
  upd res 3ul a3;
  let h4 = ST.get () in
  BD.bn_upd_eval (as_seq h0 res) a0 0;
  BD.bn_upd_eval (as_seq h1 res) a1 1;
  BD.bn_upd_eval (as_seq h2 res) a2 2;
  BD.bn_upd_eval (as_seq h3 res) a3 3;
  bn_v_is_as_nat (as_seq h0 res)


///  Create zero and one

let bn_set_zero4 f =
  bn_make_u64_4 f (u64 0) (u64 0) (u64 0) (u64 0)


let bn_set_one4 f =
  bn_make_u64_4 f (u64 1) (u64 0) (u64 0) (u64 0)


///  Comparison

[@CInline]
let bn_is_zero_mask4 f =
  let h0 = ST.get () in
  SN.bn_is_zero_mask_lemma (as_seq h0 f);
  bn_v_is_as_nat (as_seq h0 f);
  BN.bn_is_zero_mask #U64 4ul f


[@CInline]
let bn_is_zero_vartime4 f =
  let m = bn_is_zero_mask4 f in
  Hacl.Bignum.Base.unsafe_bool_of_limb m
val bn_is_eq_mask4: x:felem -> y:felem -> Stack uint64
  (requires fun h -> live h x /\ live h y)
  (ensures fun h0 r h1 -> modifies0 h0 h1 /\
    (if as_nat h0 x = as_nat h0 y then v r == ones_v U64 else v r = 0))
x: Hacl.Impl.P256.Bignum.felem -> y: Hacl.Impl.P256.Bignum.felem
  -> FStar.HyperStack.ST.Stack Lib.IntTypes.uint64