val ecdsa_verify_avoid_finv: p:point -> r:QA.qelem -> Stack bool
  (requires fun h ->
    live h p /\ live h r /\ disjoint p r /\
    point_inv h p /\ QA.qe_lt_q h r /\ 0 < QA.qas_nat h r /\
    not (S.is_proj_point_at_inf (point_eval h p)))
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    (let (_X, _Y, _Z) = point_eval h0 p in
     b <==> (S.fmul _X (S.finv _Z) % S.q = QA.qas_nat h0 r)))
let ecdsa_verify_avoid_finv p r =
  let h0 = ST.get () in
  let x, y, z = getx p, gety p, getz p in

  push_frame ();
  let r_bytes = create 32ul (u8 0) in
  let r_fe = create_felem () in
  let tmp_q = create_felem () in
  let tmp_x = create_felem () in

  QA.store_qelem r_bytes r;
  load_felem r_fe r_bytes;
  let h1 = ST.get () in
  //assert (inv_fully_reduced h1 r_fe);
  //assert (as_nat h1 r_fe == qas_nat h1 r);

  let h2 = ST.get () in
  fnormalize tmp_x x;
  let h3 = ST.get () in
  BL.normalize5_lemma (1,1,1,1,2) (as_felem5 h2 x);
  //assert (inv_fully_reduced h3 tmp_x);
  //assert (inv_lazy_reduced2 h3 z);

  let is_rz_x = fmul_eq_vartime r_fe z tmp_x in
  //assert (is_rz_x == (S.fmul (as_nat h3 r_fe) (feval h3 z) = as_nat h3 tmp_x));

  let res : bool =
    if not is_rz_x then begin
     let is_r_lt_p_m_q = is_felem_lt_prime_minus_order_vartime r_fe in
     if is_r_lt_p_m_q then begin
       assert (as_nat h1 r_fe < S.prime - S.q);
       make_u52_5 tmp_q (make_order_k256 ());
       let h4 = ST.get () in
       BL.add5_lemma (1,1,1,1,1) (1,1,1,1,1) (as_felem5 h4 r_fe) (as_felem5 h4 tmp_q);
       fadd tmp_q r_fe tmp_q;
       fmul_eq_vartime tmp_q z tmp_x end
       //assert (is_rqz_x == (S.fmul (feval h5 tmp) (feval h5 z) = as_nat h5 tmp_x));
     else false end
    else true in

  pop_frame ();
  KL.ecdsa_verify_avoid_finv (point_eval h0 p) (QA.qas_nat h0 r);
  assert (res <==> (S.fmul (feval h0 x) (S.finv (feval h0 z)) % S.q = QA.qas_nat h0 r));
  let h5 = ST.get () in
  assert (modifies0 h0 h5);
  res
val ecdsa_verify_avoid_finv: p:point -> r:QA.qelem -> Stack bool
  (requires fun h ->
    live h p /\ live h r /\ disjoint p r /\
    point_inv h p /\ QA.qe_lt_q h r /\ 0 < QA.qas_nat h r /\
    not (S.is_proj_point_at_inf (point_eval h p)))
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    (let (_X, _Y, _Z) = point_eval h0 p in
     b <==> (S.fmul _X (S.finv _Z) % S.q = QA.qas_nat h0 r)))
let ecdsa_verify_avoid_finv p r =
let h0 = ST.get () in
let x, y, z = getx p, gety p, getz p in
push_frame ();
let r_bytes = create 32ul (u8 0) in
let r_fe = create_felem () in
let tmp_q = create_felem () in
let tmp_x = create_felem () in
QA.store_qelem r_bytes r;
load_felem r_fe r_bytes;
let h1 = ST.get () in
let h2 = ST.get () in
fnormalize tmp_x x;
let h3 = ST.get () in
BL.normalize5_lemma (1, 1, 1, 1, 2) (as_felem5 h2 x);
let is_rz_x = fmul_eq_vartime r_fe z tmp_x in
let res:bool =
  if not is_rz_x
  then
    let is_r_lt_p_m_q = is_felem_lt_prime_minus_order_vartime r_fe in
    if is_r_lt_p_m_q
    then
      (assert (as_nat h1 r_fe < S.prime - S.q);
        make_u52_5 tmp_q (make_order_k256 ());
        let h4 = ST.get () in
        BL.add5_lemma (1, 1, 1, 1, 1) (1, 1, 1, 1, 1) (as_felem5 h4 r_fe) (as_felem5 h4 tmp_q);
        fadd tmp_q r_fe tmp_q;
        fmul_eq_vartime tmp_q z tmp_x)
    else false
  else true
in
pop_frame ();
KL.ecdsa_verify_avoid_finv (point_eval h0 p) (QA.qas_nat h0 r);
assert (res <==> (S.fmul (feval h0 x) (S.finv (feval h0 z)) % S.q = QA.qas_nat h0 r));
let h5 = ST.get () in
assert (modifies0 h0 h5);
res
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.Impl.K256.Point.point Hacl.K256.Scalar.qelem Hacl.K256.Field.felem Prims.unit Prims._assert Lib.Buffer.modifies0 Prims.bool FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Prims.l_iff Prims.b2t Prims.op_Equality Prims.int Prims.op_Modulus Spec.K256.PointOps.fmul Hacl.K256.Field.feval Spec.K256.PointOps.finv Spec.K256.PointOps.q Hacl.K256.Scalar.qas_nat Spec.K256.Lemmas.ecdsa_verify_avoid_finv Hacl.Impl.K256.Point.point_eval FStar.HyperStack.ST.pop_frame Prims.op_Negation Hacl.Impl.K256.Verify.fmul_eq_vartime Hacl.K256.Field.fadd Hacl.Spec.K256.Field52.Lemmas.add5_lemma FStar.Pervasives.Native.Mktuple5 Prims.nat Hacl.K256.Field.as_felem5 Hacl.K256.Field.make_u52_5 Hacl.K256.Field.make_order_k256 Prims.op_LessThan Hacl.K256.Field.as_nat Prims.op_Subtraction Spec.K256.PointOps.prime Hacl.K256.Field.is_felem_lt_prime_minus_order_vartime Hacl.Spec.K256.Field52.Lemmas.normalize5_lemma Hacl.K256.Field.fnormalize Hacl.K256.Field.load_felem Hacl.K256.Scalar.store_qelem Hacl.K256.Field.create_felem Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.create Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.u8 Lib.Buffer.lbuffer FStar.HyperStack.ST.push_frame FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.Mktuple3 Hacl.Impl.K256.Point.getz Hacl.Impl.K256.Point.gety Hacl.Impl.K256.Point.getx
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]
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


inline_for_extraction noextract
val ecdsa_verify_avoid_finv: p:point -> r:QA.qelem -> Stack bool
  (requires fun h ->
    live h p /\ live h r /\ disjoint p r /\
    point_inv h p /\ QA.qe_lt_q h r /\ 0 < QA.qas_nat h r /\
    not (S.is_proj_point_at_inf (point_eval h p)))
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    (let (_X, _Y, _Z) = point_eval h0 p in
     b <==> (S.fmul _X (S.finv _Z) % S.q = QA.qas_nat h0 r)))
val ecdsa_verify_avoid_finv: p:point -> r:QA.qelem -> Stack bool
  (requires fun h ->
    live h p /\ live h r /\ disjoint p r /\
    point_inv h p /\ QA.qe_lt_q h r /\ 0 < QA.qas_nat h r /\
    not (S.is_proj_point_at_inf (point_eval h p)))
  (ensures  fun h0 b h1 -> modifies0 h0 h1 /\
    (let (_X, _Y, _Z) = point_eval h0 p in
     b <==> (S.fmul _X (S.finv _Z) % S.q = QA.qas_nat h0 r)))
p: Hacl.Impl.K256.Point.point -> r: Hacl.K256.Scalar.qelem -> FStar.HyperStack.ST.Stack Prims.bool