val table_lambda_neg_inv_precomp (q: LSeq.lseq uint64 15) (is_negate: bool)
    : BE.table_inv_t U64 15ul 32ul
let table_lambda_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 (SG.point_mul_lambda (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)
val table_lambda_neg_inv_precomp (q: LSeq.lseq uint64 15) (is_negate: bool)
    : BE.table_inv_t U64 15ul 32ul
let table_lambda_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 (SG.point_mul_lambda (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)
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
Lib.Sequence.lseq Lib.IntTypes.uint64 Prims.bool Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.UInt32.__uint_to_t Lib.IntTypes.op_Star_Bang Prims.l_and Prims.eq2 Spec.K256.PointOps.proj_point Hacl.Impl.K256.Point.point_eval_lseq Hacl.Spec.K256.GLV.point_negate_cond Hacl.Spec.K256.GLV.point_mul_lambda Prims.l_Forall Prims.nat Prims.b2t Prims.op_LessThan Hacl.Impl.PrecompTable.precomp_table_inv Hacl.Impl.K256.Group.mk_k256_concrete_ops Hacl.Impl.Exponentiation.table_inv_t
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)

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))


inline_for_extraction noextract
let table_lambda_neg_inv_precomp
val table_lambda_neg_inv_precomp (q: LSeq.lseq uint64 15) (is_negate: bool)
    : BE.table_inv_t U64 15ul 32ul
q: Lib.Sequence.lseq Lib.IntTypes.uint64 15 -> is_negate: Prims.bool
  -> Hacl.Impl.Exponentiation.table_inv_t Lib.IntTypes.U64 15ul 32ul