val fdouble: res:felem -> x:felem -> Stack unit
  (requires fun h ->
    live h x /\ live h res /\ eq_or_disjoint x res /\
    as_nat h x < S.prime)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res == (2 * as_nat h0 x) % S.prime /\
    fmont_as_nat h1 res == (2 * fmont_as_nat h0 x) % S.prime)
let fdouble out x =
  fadd out x x
val fdouble: res:felem -> x:felem -> Stack unit
  (requires fun h ->
    live h x /\ live h res /\ eq_or_disjoint x res /\
    as_nat h x < S.prime)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res == (2 * as_nat h0 x) % S.prime /\
    fmont_as_nat h1 res == (2 * fmont_as_nat h0 x) % S.prime)
let fdouble out x =
fadd out x x
Hacl.Impl.P256.Field.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Impl.P256.Constants.fst.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Bignum256.fst.checked Hacl.Bignum.Montgomery.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Calc.fsti.checked
Hacl.Impl.P256.Field.fst
Hacl.Impl.P256.Bignum.felem Hacl.Impl.P256.Field.fadd Prims.unit
module Hacl.Impl.P256.Field

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

open Lib.IntTypes
open Lib.Buffer

open Hacl.Impl.P256.Bignum
open Hacl.Impl.P256.Constants

module S = Spec.P256
module SM = Hacl.Spec.P256.Montgomery

module BD = Hacl.Spec.Bignum.Definitions
module BM = Hacl.Bignum.Montgomery

friend Hacl.Bignum256

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

///  Create zero and one

[@CInline]
let make_fzero n =
  bn_set_zero4 n;
  assert_norm (SM.to_mont 0 = 0);
  SM.lemma_to_from_mont_id 0


[@CInline]
let make_fone n =
  // 0xfffffffeffffffffffffffffffffffff000000000000000000000001
  [@inline_let] let n0 = u64 0x1 in
  [@inline_let] let n1 = u64 0xffffffff00000000 in
  [@inline_let] let n2 = u64 0xffffffffffffffff in
  [@inline_let] let n3 = u64 0xfffffffe in
  assert_norm (v n0 + v n1 * pow2 64 + v n2 * pow2 128 + v n3 * pow2 192 < S.prime);
  assert_norm (v n0 + v n1 * pow2 64 + v n2 * pow2 128 + v n3 * pow2 192 == SM.to_mont 1);
  SM.lemma_to_from_mont_id 1;
  bn_make_u64_4 n n0 n1 n2 n3


///  Comparison

[@CInline]
let bn_is_lt_prime_mask4 f =
  let h0 = ST.get () in
  push_frame ();
  let tmp = create_felem () in
  make_prime tmp;
  let c = bn_sub4 tmp f tmp in
  assert (if v c = 0 then as_nat h0 f >= S.prime else as_nat h0 f < S.prime);
  pop_frame ();
  u64 0 -. c


[@CInline]
let feq_mask a b =
  let h0 = ST.get () in
  let r = bn_is_eq_mask4 a b in
  let h1 = ST.get () in
  assert (if as_nat h1 a = as_nat h1 b then v r == ones_v U64 else v r = 0);
  SM.lemma_from_to_mont_id (as_nat h0 a);
  SM.lemma_from_to_mont_id (as_nat h0 b);
  assert (if fmont_as_nat h1 a = fmont_as_nat h1 b then v r == ones_v U64 else v r = 0);
  r


///  Field Arithmetic

[@CInline]
let fadd res x y =
  let h0 = ST.get () in
  push_frame ();
  let n = create_felem () in
  make_prime n;
  bn_add_mod4 res n x y;
  let h1 = ST.get () in
  assert (as_nat h1 res == (as_nat h0 x + as_nat h0 y) % S.prime);
  SM.fmont_add_lemma (as_nat h0 x) (as_nat h0 y);
  pop_frame ()
val fdouble: res:felem -> x:felem -> Stack unit
  (requires fun h ->
    live h x /\ live h res /\ eq_or_disjoint x res /\
    as_nat h x < S.prime)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res == (2 * as_nat h0 x) % S.prime /\
    fmont_as_nat h1 res == (2 * fmont_as_nat h0 x) % S.prime)
res: Hacl.Impl.P256.Bignum.felem -> x: Hacl.Impl.P256.Bignum.felem
  -> FStar.HyperStack.ST.Stack Prims.unit