val point_mul_g_double_split_lambda_table:
    out:point
  -> r1:qelem -> q1:point
  -> r2:qelem -> q2:point
  -> r3:qelem -> q3:point
  -> r4:qelem -> q4:point
  -> p1:point -> p2:point
  -> is_negate1:bool -> is_negate2:bool
  -> is_negate3:bool -> is_negate4:bool ->
  Stack unit
  (requires fun h ->
    live h out /\ live h r1 /\ live h r2 /\ live h r3 /\ live h r4 /\
    live h q1 /\ live h q2 /\ live h q3 /\ live h q4 /\ live h p1 /\ live h p2 /\
    eq_or_disjoint q1 q2 /\ eq_or_disjoint q1 q3 /\ eq_or_disjoint q1 q4 /\
    eq_or_disjoint q2 q3 /\ eq_or_disjoint q2 q4 /\ eq_or_disjoint q3 q4 /\
    disjoint out q1 /\ disjoint out q2 /\ disjoint out q3 /\ disjoint out q4 /\
    disjoint out r1 /\ disjoint out r2 /\ disjoint out r3 /\ disjoint out r4 /\
    disjoint out p1  /\ disjoint out p2 /\
    point_inv h q1 /\ point_inv h q2 /\ point_inv h q3 /\ point_inv h q4 /\
    point_inv h p1 /\ point_inv h p2 /\
    point_eval h p1 == S.g /\
    point_eval h q1==SG.point_negate_cond (point_eval h p1) is_negate1 /\
    point_eval h q2==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p1)) is_negate2 /\
    point_eval h q3==SG.point_negate_cond (point_eval h p2) is_negate3 /\
    point_eval h q4==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p2)) is_negate4 /\
    qas_nat h r1 < S.q /\ qas_nat h r1 < pow2 128 /\
    qas_nat h r2 < S.q /\ qas_nat h r2 < pow2 128 /\
    qas_nat h r3 < S.q /\ qas_nat h r3 < pow2 128 /\
    qas_nat h r4 < S.q /\ qas_nat h r4 < pow2 128)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    point_inv h1 out /\
    refl (as_seq h1 out) ==
      LE.exp_four_fw S.mk_k256_comm_monoid
        (refl (as_seq h0 q1)) 128 (qas_nat h0 r1)
        (refl (as_seq h0 q2)) (qas_nat h0 r2)
        (refl (as_seq h0 q3)) (qas_nat h0 r3)
        (refl (as_seq h0 q4)) (qas_nat h0 r4) 5)
let point_mul_g_double_split_lambda_table out r1 q1 r2 q2 r3 q3 r4 q4
  p1 p2 is_negate1 is_negate2 is_negate3 is_negate4 =
  [@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 table_len = 32ul in

  let h0 = ST.get () in
  push_frame ();
  let table2 = create (table_len *! len) (u64 0) in
  PT.lprecomp_table len ctx_len k (null uint64) p2 table_len table2;
  point_mul_g_double_split_lambda_table_noalloc out table2 r1 q1 r2 q2 r3 q3 r4 q4
    p1 p2 is_negate1 is_negate2 is_negate3 is_negate4;
  let h1 = ST.get () in
  assert (modifies (loc out |+| loc table2) h0 h1);
  pop_frame ();
  let h2 = ST.get () in
  assert (modifies (loc out) h0 h2)
val point_mul_g_double_split_lambda_table:
    out:point
  -> r1:qelem -> q1:point
  -> r2:qelem -> q2:point
  -> r3:qelem -> q3:point
  -> r4:qelem -> q4:point
  -> p1:point -> p2:point
  -> is_negate1:bool -> is_negate2:bool
  -> is_negate3:bool -> is_negate4:bool ->
  Stack unit
  (requires fun h ->
    live h out /\ live h r1 /\ live h r2 /\ live h r3 /\ live h r4 /\
    live h q1 /\ live h q2 /\ live h q3 /\ live h q4 /\ live h p1 /\ live h p2 /\
    eq_or_disjoint q1 q2 /\ eq_or_disjoint q1 q3 /\ eq_or_disjoint q1 q4 /\
    eq_or_disjoint q2 q3 /\ eq_or_disjoint q2 q4 /\ eq_or_disjoint q3 q4 /\
    disjoint out q1 /\ disjoint out q2 /\ disjoint out q3 /\ disjoint out q4 /\
    disjoint out r1 /\ disjoint out r2 /\ disjoint out r3 /\ disjoint out r4 /\
    disjoint out p1  /\ disjoint out p2 /\
    point_inv h q1 /\ point_inv h q2 /\ point_inv h q3 /\ point_inv h q4 /\
    point_inv h p1 /\ point_inv h p2 /\
    point_eval h p1 == S.g /\
    point_eval h q1==SG.point_negate_cond (point_eval h p1) is_negate1 /\
    point_eval h q2==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p1)) is_negate2 /\
    point_eval h q3==SG.point_negate_cond (point_eval h p2) is_negate3 /\
    point_eval h q4==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p2)) is_negate4 /\
    qas_nat h r1 < S.q /\ qas_nat h r1 < pow2 128 /\
    qas_nat h r2 < S.q /\ qas_nat h r2 < pow2 128 /\
    qas_nat h r3 < S.q /\ qas_nat h r3 < pow2 128 /\
    qas_nat h r4 < S.q /\ qas_nat h r4 < pow2 128)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    point_inv h1 out /\
    refl (as_seq h1 out) ==
      LE.exp_four_fw S.mk_k256_comm_monoid
        (refl (as_seq h0 q1)) 128 (qas_nat h0 r1)
        (refl (as_seq h0 q2)) (qas_nat h0 r2)
        (refl (as_seq h0 q3)) (qas_nat h0 r3)
        (refl (as_seq h0 q4)) (qas_nat h0 r4) 5)
let point_mul_g_double_split_lambda_table
      out
      r1
      q1
      r2
      q2
      r3
      q3
      r4
      q4
      p1
      p2
      is_negate1
      is_negate2
      is_negate3
      is_negate4
     =
[@@ 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 table_len = 32ul in
let h0 = ST.get () in
push_frame ();
let table2 = create (table_len *! len) (u64 0) in
PT.lprecomp_table len ctx_len k (null uint64) p2 table_len table2;
point_mul_g_double_split_lambda_table_noalloc out table2 r1 q1 r2 q2 r3 q3 r4 q4 p1 p2 is_negate1
  is_negate2 is_negate3 is_negate4;
let h1 = ST.get () in
assert (modifies (loc out |+| loc table2) h0 h1);
pop_frame ();
let h2 = ST.get () in
assert (modifies (loc out) h0 h2)
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
Hacl.Impl.K256.Point.point Hacl.K256.Scalar.qelem Prims.bool Prims._assert Lib.Buffer.modifies Lib.Buffer.loc Lib.Buffer.MUT Lib.IntTypes.uint64 Prims.unit FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get FStar.HyperStack.ST.pop_frame Lib.Buffer.op_Bar_Plus_Bar Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC Hacl.Impl.K256.GLV.point_mul_g_double_split_lambda_table_noalloc Hacl.Impl.PrecompTable.lprecomp_table Lib.Buffer.null Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.mul Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Buffer.create Lib.IntTypes.op_Star_Bang Lib.IntTypes.u64 Lib.Buffer.lbuffer FStar.HyperStack.ST.push_frame FStar.UInt32.t FStar.UInt32.__uint_to_t Hacl.Impl.Exponentiation.Definitions.concrete_ops FStar.UInt32.uint_to_t Hacl.Impl.K256.Group.mk_k256_concrete_ops
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
  (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)


// This function returns [r_small]([lambda]Q) or [r_small](-[lambda]Q)
// using a precomputed table [0; Q; 2Q; ...; 15Q]
inline_for_extraction noextract
val lprecomp_get_vartime_lambda_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_lambda_neg_inv_precomp q is_negate)

let lprecomp_get_vartime_lambda_neg q is_negate ctx lambda_q table r_small res =
  let h0 = ST.get () in
  assert (table_lambda_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)));

  // -[r_small]Q = [r_small](-Q)
  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);

  // [lambda]([r_small]Q) or [lambda]([r_small](-Q))
  point_mul_lambda_inplace res;
  let h3 = ST.get () in
  assert (point_eval h3 res == SG.point_mul_lambda (point_eval h2 res));
  SGL.lemma_glv (point_eval h2 res);
  assert (S.to_aff_point (point_eval h3 res) ==
    SG.aff_point_mul SG.lambda (S.to_aff_point (point_eval h2 res)));

  // [r_small]([lambda]Q) or [r_small](-[lambda]Q)
  SGL.aff_point_negate_cond_lambda_pow_lemma is_negate (point_eval_lseq q) (v r_small);
  assert (S.to_aff_point (point_eval h3 res) ==
    LE.pow S.mk_k256_comm_monoid
      (S.to_aff_point
        (SG.point_negate_cond (SG.point_mul_lambda (point_eval_lseq q)) is_negate)) (v r_small))

//------------------------------

inline_for_extraction noextract
val point_mul_g_double_split_lambda_table_noalloc:
    out:point
  -> table2:lbuffer uint64 (32ul *! 15ul)
  -> r1:qelem -> q1:point
  -> r2:qelem -> q2:point
  -> r3:qelem -> q3:point
  -> r4:qelem -> q4:point
  -> p1:point -> p2:point
  -> is_negate1:bool -> is_negate2:bool
  -> is_negate3:bool -> is_negate4:bool ->
  Stack unit
  (requires fun h ->
    live h out /\ live h table2 /\
    live h r1 /\ live h r2 /\ live h r3 /\ live h r4 /\
    live h q1 /\ live h q2 /\ live h q3 /\ live h q4 /\
    live h p1 /\ live h p2 /\

    eq_or_disjoint q1 q2 /\ eq_or_disjoint q1 q3 /\ eq_or_disjoint q1 q4 /\
    eq_or_disjoint q2 q3 /\ eq_or_disjoint q2 q4 /\ eq_or_disjoint q3 q4 /\
    disjoint out q1 /\ disjoint out q2 /\ disjoint out q3 /\ disjoint out q4 /\
    disjoint out r1 /\ disjoint out r2 /\ disjoint out r3 /\ disjoint out r4 /\
    disjoint out p1  /\ disjoint out p2 /\

    disjoint table2 out /\ disjoint table2 r1 /\ disjoint table2 r2 /\
    disjoint table2 r3 /\ disjoint table2 r4 /\  disjoint table2 p1 /\
    disjoint table2 p2 /\ disjoint table2 q1 /\ disjoint table2 q2 /\
    disjoint table2 q3 /\ disjoint table2 q4 /\

    point_inv h q1 /\ point_inv h q2 /\ point_inv h q3 /\ point_inv h q4 /\
    point_inv h p1 /\ point_inv h p2 /\
    point_eval h p1 == S.g /\
    point_eval h q1==SG.point_negate_cond (point_eval h p1) is_negate1 /\
    point_eval h q2==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p1)) is_negate2 /\
    point_eval h q3==SG.point_negate_cond (point_eval h p2) is_negate3 /\
    point_eval h q4==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p2)) is_negate4 /\
    qas_nat h r1 < S.q /\ qas_nat h r1 < pow2 128 /\
    qas_nat h r2 < S.q /\ qas_nat h r2 < pow2 128 /\
    qas_nat h r3 < S.q /\ qas_nat h r3 < pow2 128 /\
    qas_nat h r4 < S.q /\ qas_nat h r4 < pow2 128 /\
    table_inv_w5 (as_seq h p2) (as_seq h table2))
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    point_inv h1 out /\
    refl (as_seq h1 out) ==
      LE.exp_four_fw S.mk_k256_comm_monoid
        (refl (as_seq h0 q1)) 128 (qas_nat h0 r1)
        (refl (as_seq h0 q2)) (qas_nat h0 r2)
        (refl (as_seq h0 q3)) (qas_nat h0 r3)
        (refl (as_seq h0 q4)) (qas_nat h0 r4) 5)

let point_mul_g_double_split_lambda_table_noalloc out table2 r1 q1 r2 q2 r3 q3 r4 q4 p1 p2
  is_negate1 is_negate2 is_negate3 is_negate4 =
  [@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
  [@inline_let] let bLen = 4ul in
  [@inline_let] let bBits = 128ul in

  let h0 = ST.get () in
  recall_contents precomp_basepoint_table_w5 precomp_basepoint_table_lseq_w5;
  let h1 = ST.get () in
  precomp_basepoint_table_lemma_w5 ();
  assert (table_inv_w5 (as_seq h1 p1) (as_seq h1 precomp_basepoint_table_w5));
  assert (table_inv_w5 (as_seq h1 p2) (as_seq h1 table2));

  assert (point_eval_lseq (as_seq h1 q1) ==
    SG.point_negate_cond (point_eval_lseq (as_seq h1 p1)) is_negate1);
  [@inline_let]
  let table_inv1 : BE.table_inv_t U64 len table_len =
    table_neg_inv_precomp (as_seq h0 p1) is_negate1 in
  assert (table_inv1 (as_seq h1 q1) (as_seq h1 precomp_basepoint_table_w5));

  assert (point_eval_lseq (as_seq h1 q2) ==
    SG.point_negate_cond (SG.point_mul_lambda (point_eval_lseq (as_seq h1 p1))) is_negate2);
  [@inline_let]
  let table_inv2 : BE.table_inv_t U64 len table_len =
    table_lambda_neg_inv_precomp (as_seq h0 p1) is_negate2 in
  assert (table_inv2 (as_seq h1 q2) (as_seq h1 precomp_basepoint_table_w5));

  assert (point_eval_lseq (as_seq h1 q3) ==
    SG.point_negate_cond (point_eval_lseq (as_seq h1 p2)) is_negate3);
  [@inline_let]
  let table_inv3 : BE.table_inv_t U64 len table_len =
    table_neg_inv_precomp (as_seq h0 p2) is_negate3 in
  assert (table_inv3 (as_seq h1 q3) (as_seq h1 table2));

  assert (point_eval_lseq (as_seq h1 q4) ==
    SG.point_negate_cond (SG.point_mul_lambda (point_eval_lseq (as_seq h1 p2))) is_negate4);
  [@inline_let]
  let table_inv4 : BE.table_inv_t U64 len table_len =
    table_lambda_neg_inv_precomp (as_seq h0 p2) is_negate4 in
  assert (table_inv4 (as_seq h1 q4) (as_seq h1 table2));

  ME.mk_lexp_four_fw_tables len ctx_len k l table_len
    table_inv1 table_inv2 table_inv3 table_inv4
    (lprecomp_get_vartime_neg (as_seq h0 p1) is_negate1)
    (lprecomp_get_vartime_lambda_neg (as_seq h0 p1) is_negate2)
    (lprecomp_get_vartime_neg (as_seq h0 p2) is_negate3)
    (lprecomp_get_vartime_lambda_neg (as_seq h0 p2) is_negate4)
    (null uint64) q1 bLen bBits r1 q2 r2 q3 r3 q4 r4
    (to_const precomp_basepoint_table_w5)
    (to_const precomp_basepoint_table_w5)
    (to_const table2) (to_const table2) out


val point_mul_g_double_split_lambda_table:
    out:point
  -> r1:qelem -> q1:point
  -> r2:qelem -> q2:point
  -> r3:qelem -> q3:point
  -> r4:qelem -> q4:point
  -> p1:point -> p2:point
  -> is_negate1:bool -> is_negate2:bool
  -> is_negate3:bool -> is_negate4:bool ->
  Stack unit
  (requires fun h ->
    live h out /\ live h r1 /\ live h r2 /\ live h r3 /\ live h r4 /\
    live h q1 /\ live h q2 /\ live h q3 /\ live h q4 /\ live h p1 /\ live h p2 /\
    eq_or_disjoint q1 q2 /\ eq_or_disjoint q1 q3 /\ eq_or_disjoint q1 q4 /\
    eq_or_disjoint q2 q3 /\ eq_or_disjoint q2 q4 /\ eq_or_disjoint q3 q4 /\
    disjoint out q1 /\ disjoint out q2 /\ disjoint out q3 /\ disjoint out q4 /\
    disjoint out r1 /\ disjoint out r2 /\ disjoint out r3 /\ disjoint out r4 /\
    disjoint out p1  /\ disjoint out p2 /\
    point_inv h q1 /\ point_inv h q2 /\ point_inv h q3 /\ point_inv h q4 /\
    point_inv h p1 /\ point_inv h p2 /\
    point_eval h p1 == S.g /\
    point_eval h q1==SG.point_negate_cond (point_eval h p1) is_negate1 /\
    point_eval h q2==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p1)) is_negate2 /\
    point_eval h q3==SG.point_negate_cond (point_eval h p2) is_negate3 /\
    point_eval h q4==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p2)) is_negate4 /\
    qas_nat h r1 < S.q /\ qas_nat h r1 < pow2 128 /\
    qas_nat h r2 < S.q /\ qas_nat h r2 < pow2 128 /\
    qas_nat h r3 < S.q /\ qas_nat h r3 < pow2 128 /\
    qas_nat h r4 < S.q /\ qas_nat h r4 < pow2 128)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    point_inv h1 out /\
    refl (as_seq h1 out) ==
      LE.exp_four_fw S.mk_k256_comm_monoid
        (refl (as_seq h0 q1)) 128 (qas_nat h0 r1)
        (refl (as_seq h0 q2)) (qas_nat h0 r2)
        (refl (as_seq h0 q3)) (qas_nat h0 r3)
        (refl (as_seq h0 q4)) (qas_nat h0 r4) 5)

[@CInline]
let point_mul_g_double_split_lambda_table out r1 q1 r2 q2 r3 q3 r4 q4
val point_mul_g_double_split_lambda_table:
    out:point
  -> r1:qelem -> q1:point
  -> r2:qelem -> q2:point
  -> r3:qelem -> q3:point
  -> r4:qelem -> q4:point
  -> p1:point -> p2:point
  -> is_negate1:bool -> is_negate2:bool
  -> is_negate3:bool -> is_negate4:bool ->
  Stack unit
  (requires fun h ->
    live h out /\ live h r1 /\ live h r2 /\ live h r3 /\ live h r4 /\
    live h q1 /\ live h q2 /\ live h q3 /\ live h q4 /\ live h p1 /\ live h p2 /\
    eq_or_disjoint q1 q2 /\ eq_or_disjoint q1 q3 /\ eq_or_disjoint q1 q4 /\
    eq_or_disjoint q2 q3 /\ eq_or_disjoint q2 q4 /\ eq_or_disjoint q3 q4 /\
    disjoint out q1 /\ disjoint out q2 /\ disjoint out q3 /\ disjoint out q4 /\
    disjoint out r1 /\ disjoint out r2 /\ disjoint out r3 /\ disjoint out r4 /\
    disjoint out p1  /\ disjoint out p2 /\
    point_inv h q1 /\ point_inv h q2 /\ point_inv h q3 /\ point_inv h q4 /\
    point_inv h p1 /\ point_inv h p2 /\
    point_eval h p1 == S.g /\
    point_eval h q1==SG.point_negate_cond (point_eval h p1) is_negate1 /\
    point_eval h q2==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p1)) is_negate2 /\
    point_eval h q3==SG.point_negate_cond (point_eval h p2) is_negate3 /\
    point_eval h q4==SG.point_negate_cond (SG.point_mul_lambda (point_eval h p2)) is_negate4 /\
    qas_nat h r1 < S.q /\ qas_nat h r1 < pow2 128 /\
    qas_nat h r2 < S.q /\ qas_nat h r2 < pow2 128 /\
    qas_nat h r3 < S.q /\ qas_nat h r3 < pow2 128 /\
    qas_nat h r4 < S.q /\ qas_nat h r4 < pow2 128)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    point_inv h1 out /\
    refl (as_seq h1 out) ==
      LE.exp_four_fw S.mk_k256_comm_monoid
        (refl (as_seq h0 q1)) 128 (qas_nat h0 r1)
        (refl (as_seq h0 q2)) (qas_nat h0 r2)
        (refl (as_seq h0 q3)) (qas_nat h0 r3)
        (refl (as_seq h0 q4)) (qas_nat h0 r4) 5)

    out: Hacl.Impl.K256.Point.point ->
    r1: Hacl.K256.Scalar.qelem ->
    q1: Hacl.Impl.K256.Point.point ->
    r2: Hacl.K256.Scalar.qelem ->
    q2: Hacl.Impl.K256.Point.point ->
    r3: Hacl.K256.Scalar.qelem ->
    q3: Hacl.Impl.K256.Point.point ->
    r4: Hacl.K256.Scalar.qelem ->
    q4: Hacl.Impl.K256.Point.point ->
    p1: Hacl.Impl.K256.Point.point ->
    p2: Hacl.Impl.K256.Point.point ->
    is_negate1: Prims.bool ->
    is_negate2: Prims.bool ->
    is_negate3: Prims.bool ->
    is_negate4: Prims.bool
  -> FStar.HyperStack.ST.Stack Prims.unit