val qmod_short: res:felem -> x:felem -> Stack unit
  (requires fun h ->
    live h x /\ live h res /\ eq_or_disjoint x res)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res == as_nat h0 x % S.order)
let qmod_short res x =
  push_frame ();
  let tmp = create_felem () in
  make_order tmp;
  let h0 = ST.get () in
  let c = bn_sub4 tmp x tmp in
  bn_cmovznz4 res c tmp x;
  BD.bn_eval_bound (as_seq h0 x) 4;
  qmod_short_lemma (as_nat h0 x);
  pop_frame ()
val qmod_short: res:felem -> x:felem -> Stack unit
  (requires fun h ->
    live h x /\ live h res /\ eq_or_disjoint x res)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res == as_nat h0 x % S.order)
let qmod_short res x =
push_frame ();
let tmp = create_felem () in
make_order tmp;
let h0 = ST.get () in
let c = bn_sub4 tmp x tmp in
bn_cmovznz4 res c tmp x;
BD.bn_eval_bound (as_seq h0 x) 4;
qmod_short_lemma (as_nat h0 x);
pop_frame ()
Hacl.Impl.P256.Scalar.fst.checked
Spec.P256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.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
Hacl.Impl.P256.Scalar.fst
Hacl.Impl.P256.Bignum.felem FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.P256.Scalar.qmod_short_lemma Hacl.Impl.P256.Bignum.as_nat Hacl.Spec.Bignum.Definitions.bn_eval_bound Lib.IntTypes.U64 Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.size Lib.Buffer.as_seq Lib.Buffer.MUT Lib.IntTypes.uint64 Hacl.Impl.P256.Bignum.bn_cmovznz4 Lib.IntTypes.int_t Lib.IntTypes.SEC Hacl.Impl.P256.Bignum.bn_sub4 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Impl.P256.Constants.make_order Hacl.Impl.P256.Bignum.create_felem FStar.HyperStack.ST.push_frame
module Hacl.Impl.P256.Scalar

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

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

///  Create one

[@CInline]
let make_qone f =
  [@inline_let] let f0 = u64 0xc46353d039cdaaf in
  [@inline_let] let f1 = u64 0x4319055258e8617b in
  [@inline_let] let f2 = u64 0x0 in
  [@inline_let] let f3 = u64 0xffffffff in
  assert_norm (v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192 < S.order);
  assert_norm (v f0 + v f1 * pow2 64 + v f2 * pow2 128 + v f3 * pow2 192 == SM.to_qmont 1);
  SM.lemma_to_from_qmont_id 1;
  bn_make_u64_4 f f0 f1 f2 f3


///  Comparison

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


[@CInline]
let bn_is_lt_order_and_gt_zero_mask4 f =
  let h0 = ST.get () in
  let is_lt_order = bn_is_lt_order_mask4 f in
  assert (v is_lt_order = (if as_nat h0 f < S.order then ones_v U64 else 0));
  let is_eq_zero = bn_is_zero_mask4 f in
  assert (v is_eq_zero = (if as_nat h0 f = 0 then ones_v U64 else 0));
  lognot_lemma is_eq_zero;
  assert (v (lognot is_eq_zero) = (if 0 < as_nat h0 f then ones_v U64 else 0));

  let res = logand is_lt_order (lognot is_eq_zero) in
  logand_lemma is_lt_order (lognot is_eq_zero);
  assert (v res == (if 0 < as_nat h0 f && as_nat h0 f < S.order then ones_v U64 else 0));
  res


let load_qelem_conditional res b =
  push_frame ();
  bn_from_bytes_be4 res b;
  let is_b_valid = bn_is_lt_order_and_gt_zero_mask4 res in

  let oneq = create_felem () in
  bn_set_one4 oneq;
  let h0 = ST.get () in
  Lib.ByteBuffer.buf_mask_select res oneq is_b_valid res;
  let h1 = ST.get () in
  assert (as_seq h1 res == (if (v is_b_valid = 0) then as_seq h0 oneq else as_seq h0 res));
  pop_frame ();
  is_b_valid


///  Field Arithmetic

val qmod_short_lemma: a:nat{a < pow2 256} ->
  Lemma (let r = if a >= S.order then a - S.order else a in r = a % S.order)

let qmod_short_lemma a =
  let r = if a >= S.order then a - S.order else a in
  if a >= S.order then begin
    Math.Lemmas.lemma_mod_sub a S.order 1;
    assert_norm (pow2 256 - S.order < S.order);
    Math.Lemmas.small_mod r S.order end
  else
   Math.Lemmas.small_mod r S.order


[@CInline]
val qmod_short: res:felem -> x:felem -> Stack unit
  (requires fun h ->
    live h x /\ live h res /\ eq_or_disjoint x res)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res == as_nat h0 x % S.order)
res: Hacl.Impl.P256.Bignum.felem -> x: Hacl.Impl.P256.Bignum.felem
  -> FStar.HyperStack.ST.Stack Prims.unit