val lprecomp_get_vartime_neg:
    q:Ghost.erased (LSeq.lseq uint64 15){point_inv_lseq q} -> is_negate:bool ->
  BE.pow_a_to_small_b_st U64 15ul 0ul mk_k256_concrete_ops 5ul 32ul
    (table_neg_inv_precomp q is_negate)
let lprecomp_get_vartime_neg q is_negate ctx lambda_q table r_small res =
  let h0 = ST.get () in
  assert (table_neg_inv_precomp q is_negate lambda_q (as_seq h0 table));
  // table.[r_small] = [r_small]Q
  BE.lprecomp_get_vartime 15ul 0ul mk_k256_concrete_ops 5ul 32ul ctx q table r_small res;
  SE.pow_lemma S.mk_k256_concrete_ops (point_eval_lseq q) (v r_small);
  let h1 = ST.get () in
  assert (S.to_aff_point (point_eval h1 res) ==
    S.to_aff_point (SE.pow S.mk_k256_concrete_ops (point_eval_lseq q) (v r_small)));

  point_negate_conditional_vartime res is_negate;
  let h2 = ST.get () in
  assert (point_eval h2 res == SG.point_negate_cond (point_eval h1 res) is_negate);
  SL.to_aff_point_negate_lemma (point_eval h1 res);
  assert (S.to_aff_point (point_eval h2 res) ==
    SG.aff_point_negate_cond (S.to_aff_point (point_eval h1 res)) is_negate);

  // -[r_small]Q = [r_small](-Q)
  SGL.aff_point_negate_cond_pow_lemma is_negate (point_eval_lseq q) (v r_small);
  assert (S.to_aff_point (point_eval h2 res) ==
    LE.pow S.mk_k256_comm_monoid
      (S.to_aff_point (SG.point_negate_cond (point_eval_lseq q) is_negate)) (v r_small))
val lprecomp_get_vartime_neg:
    q:Ghost.erased (LSeq.lseq uint64 15){point_inv_lseq q} -> is_negate:bool ->
  BE.pow_a_to_small_b_st U64 15ul 0ul mk_k256_concrete_ops 5ul 32ul
    (table_neg_inv_precomp q is_negate)
let lprecomp_get_vartime_neg q is_negate ctx lambda_q table r_small res =
let h0 = ST.get () in
assert (table_neg_inv_precomp q is_negate lambda_q (as_seq h0 table));
BE.lprecomp_get_vartime 15ul 0ul mk_k256_concrete_ops 5ul 32ul ctx q table r_small res;
SE.pow_lemma S.mk_k256_concrete_ops (point_eval_lseq q) (v r_small);
let h1 = ST.get () in
assert (S.to_aff_point (point_eval h1 res) ==
    S.to_aff_point (SE.pow S.mk_k256_concrete_ops (point_eval_lseq q) (v r_small)));
point_negate_conditional_vartime res is_negate;
let h2 = ST.get () in
assert (point_eval h2 res == SG.point_negate_cond (point_eval h1 res) is_negate);
SL.to_aff_point_negate_lemma (point_eval h1 res);
assert (S.to_aff_point (point_eval h2 res) ==
    SG.aff_point_negate_cond (S.to_aff_point (point_eval h1 res)) is_negate);
SGL.aff_point_negate_cond_pow_lemma is_negate (point_eval_lseq q) (v r_small);
assert (S.to_aff_point (point_eval h2 res) ==
    LE.pow S.mk_k256_comm_monoid
      (S.to_aff_point (SG.point_negate_cond (point_eval_lseq q) is_negate))
      (v r_small))
Hacl.Impl.K256.GLV.fst.checked
Spec.K256.Lemmas.fsti.checked Spec.K256.fst.checked Spec.Exponentiation.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.GLV.Lemmas.fst.checked Hacl.Spec.K256.GLV.fst.checked Hacl.Spec.K256.ECSM.Lemmas.fst.checked Hacl.K256.Scalar.fsti.checked Hacl.K256.PrecompTable.fsti.checked Hacl.K256.Field.fsti.checked Hacl.Impl.PrecompTable.fsti.checked Hacl.Impl.MultiExponentiation.fsti.checked Hacl.Impl.K256.PointMul.fsti.checked Hacl.Impl.K256.Point.fsti.checked Hacl.Impl.K256.Group.fst.checked Hacl.Impl.K256.GLV.Constants.fsti.checked Hacl.Impl.Exponentiation.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 FStar.Ghost.fsti.checked
Hacl.Impl.K256.GLV.fst
FStar.Ghost.erased Lib.Sequence.lseq Lib.IntTypes.uint64 Hacl.Impl.K256.Point.point_inv_lseq FStar.Ghost.reveal Prims.bool Lib.Buffer.lbuffer Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.__uint_to_t Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.clbuffer Lib.IntTypes.op_Star_Bang Prims.b2t Prims.op_LessThan Prims.pow2 Prims._assert Prims.eq2 Spec.K256.PointOps.aff_point Spec.K256.PointOps.to_aff_point Hacl.Impl.K256.Point.point_eval Lib.Exponentiation.Definition.pow Spec.K256.mk_k256_comm_monoid Hacl.Spec.K256.GLV.point_negate_cond Hacl.Impl.K256.Point.point_eval_lseq Prims.unit Hacl.Spec.K256.GLV.Lemmas.aff_point_negate_cond_pow_lemma Hacl.Spec.K256.GLV.aff_point_negate_cond Spec.K256.Lemmas.to_aff_point_negate_lemma Spec.K256.PointOps.proj_point FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Impl.K256.Point.point_negate_conditional_vartime Spec.Exponentiation.pow Spec.K256.mk_k256_concrete_ops Spec.Exponentiation.pow_lemma Hacl.Impl.Exponentiation.lprecomp_get_vartime Hacl.Impl.K256.Group.mk_k256_concrete_ops Hacl.Impl.K256.GLV.table_neg_inv_precomp Lib.Buffer.as_seq Lib.Buffer.CONST
module Hacl.Impl.K256.GLV

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

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST
module LSeq = Lib.Sequence

module LE = Lib.Exponentiation
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation
module ME = Hacl.Impl.MultiExponentiation
module PT = Hacl.Impl.PrecompTable

module S = Spec.K256
module SL = Spec.K256.Lemmas
module SG = Hacl.Spec.K256.GLV
module SGL = Hacl.Spec.K256.GLV.Lemmas
module PML = Hacl.Spec.K256.ECSM.Lemmas
module PM = Hacl.Impl.K256.PointMul

open Hacl.K256.Field
open Hacl.K256.Scalar
open Hacl.Impl.K256.Point

open Hacl.Impl.K256.GLV.Constants
include Hacl.Impl.K256.Group
include Hacl.K256.PrecompTable

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

let _: squash(pow2 5 = 32) =
  assert_norm (pow2 5 = 32)

let _: squash(pow2 128 < S.q) =
  assert_norm (pow2 128 < S.q)


inline_for_extraction noextract
let table_inv_w5 : BE.table_inv_t U64 15ul 32ul =
  [@inline_let] let len = 15ul in
  [@inline_let] let ctx_len = 0ul in
  [@inline_let] let k = mk_k256_concrete_ops in
  [@inline_let] let l = 5ul in
  [@inline_let] let table_len = 32ul in
  BE.table_inv_precomp len ctx_len k l table_len


inline_for_extraction noextract
let table_neg_inv_precomp
  (q:LSeq.lseq uint64 15) (is_negate:bool) : BE.table_inv_t U64 15ul 32ul =
  fun a table ->
    point_eval_lseq a == SG.point_negate_cond (point_eval_lseq q) is_negate /\
    (forall (j:nat{j < 32}).
      PT.precomp_table_inv 15ul 0ul mk_k256_concrete_ops q 32ul table j)


// This function returns [r_small]Q or [r_small](-Q)
// using a precomputed table [0; Q; 2Q; ...; 15Q]
inline_for_extraction noextract
val lprecomp_get_vartime_neg:
    q:Ghost.erased (LSeq.lseq uint64 15){point_inv_lseq q} -> is_negate:bool ->
  BE.pow_a_to_small_b_st U64 15ul 0ul mk_k256_concrete_ops 5ul 32ul
    (table_neg_inv_precomp q is_negate)
val lprecomp_get_vartime_neg:
    q:Ghost.erased (LSeq.lseq uint64 15){point_inv_lseq q} -> is_negate:bool ->
  BE.pow_a_to_small_b_st U64 15ul 0ul mk_k256_concrete_ops 5ul 32ul
    (table_neg_inv_precomp q is_negate)

    q:
      FStar.Ghost.erased (Lib.Sequence.lseq Lib.IntTypes.uint64 15)
        {Hacl.Impl.K256.Point.point_inv_lseq (FStar.Ghost.reveal q)} ->
    is_negate: Prims.bool
  -> Hacl.Impl.Exponentiation.pow_a_to_small_b_st Lib.IntTypes.U64
      15ul
      0ul
      Hacl.Impl.K256.Group.mk_k256_concrete_ops
      5ul
      32ul
      (Hacl.Impl.K256.GLV.table_neg_inv_precomp (FStar.Ghost.reveal q) is_negate)