val qmul_mont: sinv:felem -> b:felem -> res:felem -> Stack unit
  (requires fun h ->
    live h sinv /\ live h b /\ live h res /\
    disjoint sinv res /\ disjoint b res /\
    as_nat h sinv < S.order /\ as_nat h b < S.order)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res < S.order /\
    as_nat h1 res = (as_nat h0 sinv * SM.from_qmont (as_nat h0 b) * SM.qmont_R_inv) % S.order)
let qmul_mont sinv b res =
  let h0 = ST.get () in
  push_frame ();
  let tmp = create_felem () in
  from_qmont tmp b;
  let h1 = ST.get () in
  assert (as_nat h1 tmp == SM.from_qmont (as_nat h0 b));
  qmul res sinv tmp;
  let h2 = ST.get () in
  assert (as_nat h2 res = (as_nat h1 sinv * as_nat h1 tmp * SM.qmont_R_inv) % S.order);
  pop_frame ()
val qmul_mont: sinv:felem -> b:felem -> res:felem -> Stack unit
  (requires fun h ->
    live h sinv /\ live h b /\ live h res /\
    disjoint sinv res /\ disjoint b res /\
    as_nat h sinv < S.order /\ as_nat h b < S.order)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res < S.order /\
    as_nat h1 res = (as_nat h0 sinv * SM.from_qmont (as_nat h0 b) * SM.qmont_R_inv) % S.order)
let qmul_mont sinv b res =
let h0 = ST.get () in
push_frame ();
let tmp = create_felem () in
from_qmont tmp b;
let h1 = ST.get () in
assert (as_nat h1 tmp == SM.from_qmont (as_nat h0 b));
qmul res sinv tmp;
let h2 = ST.get () in
assert (as_nat h2 res = ((as_nat h1 sinv * as_nat h1 tmp) * SM.qmont_R_inv) % S.order);
pop_frame ()
Hacl.Impl.P256.Verify.fst.checked
Spec.P256.Lemmas.fsti.checked Spec.P256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.P256.Montgomery.fsti.checked Hacl.Impl.P256.Scalar.fsti.checked Hacl.Impl.P256.Qinv.fsti.checked Hacl.Impl.P256.PointMul.fsti.checked Hacl.Impl.P256.Point.fsti.checked Hacl.Impl.P256.Bignum.fsti.checked Hacl.Bignum.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.P256.Verify.fst
Hacl.Impl.P256.Bignum.felem FStar.HyperStack.ST.pop_frame Prims.unit Prims._assert Prims.b2t Prims.op_Equality Prims.int Hacl.Impl.P256.Bignum.as_nat Prims.op_Modulus FStar.Mul.op_Star Hacl.Spec.P256.Montgomery.qmont_R_inv Spec.P256.PointOps.order FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Impl.P256.Scalar.qmul Prims.eq2 Prims.nat Hacl.Spec.P256.Montgomery.from_qmont Hacl.Impl.P256.Scalar.from_qmont Hacl.Impl.P256.Bignum.create_felem FStar.HyperStack.ST.push_frame
module Hacl.Impl.P256.Verify

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.Point
open Hacl.Impl.P256.Scalar
open Hacl.Impl.P256.PointMul

module BSeq = Lib.ByteSequence

module S = Spec.P256
module SL = Spec.P256.Lemmas
module SM = Hacl.Spec.P256.Montgomery
module QI = Hacl.Impl.P256.Qinv

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

inline_for_extraction noextract
let lbytes len = lbuffer uint8 len

val qmul_mont: sinv:felem -> b:felem -> res:felem -> Stack unit
  (requires fun h ->
    live h sinv /\ live h b /\ live h res /\
    disjoint sinv res /\ disjoint b res /\
    as_nat h sinv < S.order /\ as_nat h b < S.order)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res < S.order /\
    as_nat h1 res = (as_nat h0 sinv * SM.from_qmont (as_nat h0 b) * SM.qmont_R_inv) % S.order)
val qmul_mont: sinv:felem -> b:felem -> res:felem -> Stack unit
  (requires fun h ->
    live h sinv /\ live h b /\ live h res /\
    disjoint sinv res /\ disjoint b res /\
    as_nat h sinv < S.order /\ as_nat h b < S.order)
  (ensures fun h0 _ h1 -> modifies (loc res) h0 h1 /\
    as_nat h1 res < S.order /\
    as_nat h1 res = (as_nat h0 sinv * SM.from_qmont (as_nat h0 b) * SM.qmont_R_inv) % S.order)

    sinv: Hacl.Impl.P256.Bignum.felem ->
    b: Hacl.Impl.P256.Bignum.felem ->
    res: Hacl.Impl.P256.Bignum.felem
  -> FStar.HyperStack.ST.Stack Prims.unit