val fmul_eq_vartime (r z x: felem) : Stack bool
  (requires fun h ->
    live h r /\ live h z /\ live h x /\ eq_or_disjoint r z /\
    felem_fits5 (as_felem5 h r) (2,2,2,2,2) /\ as_nat h r < S.prime /\
    inv_lazy_reduced2 h z /\ inv_fully_reduced h x)
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    b == (S.fmul (as_nat h0 r) (feval h0 z) = as_nat h0 x))
let fmul_eq_vartime r z x =
  push_frame ();
  let tmp = create_felem () in
  fmul tmp r z;
  let h1 = ST.get () in
  fnormalize tmp tmp;
  let h2 = ST.get () in
  BL.normalize5_lemma (1,1,1,1,2) (as_felem5 h1 tmp);
  assert (inv_fully_reduced h2 tmp);
  let b = is_felem_eq_vartime tmp x in
  pop_frame ();
  b
val fmul_eq_vartime (r z x: felem) : Stack bool
  (requires fun h ->
    live h r /\ live h z /\ live h x /\ eq_or_disjoint r z /\
    felem_fits5 (as_felem5 h r) (2,2,2,2,2) /\ as_nat h r < S.prime /\
    inv_lazy_reduced2 h z /\ inv_fully_reduced h x)
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    b == (S.fmul (as_nat h0 r) (feval h0 z) = as_nat h0 x))
let fmul_eq_vartime r z x =
push_frame ();
let tmp = create_felem () in
fmul tmp r z;
let h1 = ST.get () in
fnormalize tmp tmp;
let h2 = ST.get () in
BL.normalize5_lemma (1, 1, 1, 1, 2) (as_felem5 h1 tmp);
assert (inv_fully_reduced h2 tmp);
let b = is_felem_eq_vartime tmp x in
pop_frame ();
b
Hacl.Impl.K256.Verify.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Field52.Lemmas.fsti.checked Hacl.K256.Scalar.fsti.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.Qinv.fst.checked Hacl.Impl.K256.PointMul.fsti.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Impl.K256.GLV.fsti.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.fst.checked
Hacl.Impl.K256.Verify.fst
Hacl.K256.Field.felem Prims.bool Prims.unit FStar.HyperStack.ST.pop_frame Hacl.K256.Field.is_felem_eq_vartime Prims._assert Hacl.K256.Field.inv_fully_reduced Hacl.Spec.K256.Field52.Lemmas.normalize5_lemma FStar.Pervasives.Native.Mktuple5 Prims.nat Hacl.K256.Field.as_felem5 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.K256.Field.fnormalize Hacl.K256.Field.fmul Hacl.K256.Field.create_felem FStar.HyperStack.ST.push_frame
module Hacl.Impl.K256.Verify

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST

module S = Spec.K256
module KL = Spec.K256.Lemmas

open Hacl.K256.Field
open Hacl.Impl.K256.Point
open Hacl.Impl.K256.PointMul
open Hacl.Impl.K256.GLV

module QA = Hacl.K256.Scalar
module QI = Hacl.Impl.K256.Qinv
module BL = Hacl.Spec.K256.Field52.Lemmas
module BSeq = Lib.ByteSequence

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

inline_for_extraction noextract
let lbytes len = lbuffer uint8 len

inline_for_extraction noextract
val ecdsa_verify_get_u12 (u1 u2 r s z: QA.qelem) : Stack unit
  (requires fun h ->
    live h r /\ live h s /\ live h z /\ live h u1 /\ live h u2 /\
    disjoint u1 u2 /\ disjoint u1 z /\ disjoint u1 r /\ disjoint u1 s /\
    disjoint u2 z /\ disjoint u2 r /\ disjoint u2 s /\
    QA.qas_nat h s < S.q /\ QA.qas_nat h z < S.q /\ QA.qas_nat h r < S.q)
  (ensures fun h0 _ h1 -> modifies (loc u1 |+| loc u2) h0 h1 /\
    (let sinv = S.qinv (QA.qas_nat h0 s) in
    QA.qas_nat h1 u1 == QA.qas_nat h0 z * sinv % S.q /\
    QA.qas_nat h1 u2 == QA.qas_nat h0 r * sinv % S.q))

let ecdsa_verify_get_u12 u1 u2 r s z =
  push_frame ();
  let sinv = QA.create_qelem () in
  QI.qinv sinv s;
  QA.qmul u1 z sinv;
  QA.qmul u2 r sinv;
  pop_frame ()


val fmul_eq_vartime (r z x: felem) : Stack bool
  (requires fun h ->
    live h r /\ live h z /\ live h x /\ eq_or_disjoint r z /\
    felem_fits5 (as_felem5 h r) (2,2,2,2,2) /\ as_nat h r < S.prime /\
    inv_lazy_reduced2 h z /\ inv_fully_reduced h x)
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    b == (S.fmul (as_nat h0 r) (feval h0 z) = as_nat h0 x))

[@CInline]
val fmul_eq_vartime (r z x: felem) : Stack bool
  (requires fun h ->
    live h r /\ live h z /\ live h x /\ eq_or_disjoint r z /\
    felem_fits5 (as_felem5 h r) (2,2,2,2,2) /\ as_nat h r < S.prime /\
    inv_lazy_reduced2 h z /\ inv_fully_reduced h x)
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    b == (S.fmul (as_nat h0 r) (feval h0 z) = as_nat h0 x))
r: Hacl.K256.Field.felem -> z: Hacl.K256.Field.felem -> x: Hacl.K256.Field.felem
  -> FStar.HyperStack.ST.Stack Prims.bool