val point_mul:
    out:point
  -> scalar:lbuffer uint8 32ul
  -> q:point ->
  Stack unit
  (requires fun h ->
    live h scalar /\ live h q /\ live h out /\
    disjoint q out /\ disjoint q scalar /\
    F51.point_inv_t h q /\ F51.inv_ext_point (as_seq h q))
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F51.point_inv_t h1 out /\ F51.inv_ext_point (as_seq h1 out) /\
    S.to_aff_point (F51.point_eval h1 out) ==
    S.to_aff_point (S.point_mul (as_seq h0 scalar) (F51.point_eval h0 q)))
let point_mul out scalar q =
  let h0 = ST.get () in
  SE.exp_fw_lemma S.mk_ed25519_concrete_ops
    (F51.point_eval h0 q) 256 (BSeq.nat_from_bytes_le (as_seq h0 scalar)) 4;
  push_frame ();
  let bscalar = create 4ul (u64 0) in
  convert_scalar scalar bscalar;
  point_mul_noalloc out bscalar q;
  pop_frame ()
val point_mul:
    out:point
  -> scalar:lbuffer uint8 32ul
  -> q:point ->
  Stack unit
  (requires fun h ->
    live h scalar /\ live h q /\ live h out /\
    disjoint q out /\ disjoint q scalar /\
    F51.point_inv_t h q /\ F51.inv_ext_point (as_seq h q))
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F51.point_inv_t h1 out /\ F51.inv_ext_point (as_seq h1 out) /\
    S.to_aff_point (F51.point_eval h1 out) ==
    S.to_aff_point (S.point_mul (as_seq h0 scalar) (F51.point_eval h0 q)))
let point_mul out scalar q =
let h0 = ST.get () in
SE.exp_fw_lemma S.mk_ed25519_concrete_ops
  (F51.point_eval h0 q)
  256
  (BSeq.nat_from_bytes_le (as_seq h0 scalar))
  4;
push_frame ();
let bscalar = create 4ul (u64 0) in
convert_scalar scalar bscalar;
point_mul_noalloc out bscalar q;
pop_frame ()
Hacl.Impl.Ed25519.Ladder.fst.checked
Spec.Exponentiation.fsti.checked Spec.Ed25519.Lemmas.fsti.checked Spec.Ed25519.fst.checked prims.fst.checked LowStar.Ignore.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked Lib.ByteSequence.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.PrecompBaseTable256.fsti.checked Hacl.Spec.Bignum.Definitions.fst.checked Hacl.Spec.Bignum.Convert.fst.checked Hacl.Impl.PrecompTable.fsti.checked Hacl.Impl.MultiExponentiation.fsti.checked Hacl.Impl.Exponentiation.fsti.checked Hacl.Impl.Ed25519.PointNegate.fst.checked Hacl.Impl.Ed25519.PointConstants.fst.checked Hacl.Impl.Ed25519.Group.fst.checked Hacl.Impl.Ed25519.Field51.fst.checked Hacl.Ed25519.PrecompTable.fsti.checked Hacl.Bignum25519.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Convert.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked
Hacl.Impl.Ed25519.Ladder.fst
Hacl.Bignum25519.point Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Ed25519.Ladder.point_mul_noalloc Hacl.Impl.Ed25519.Ladder.convert_scalar Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.create Lib.IntTypes.uint64 Lib.IntTypes.u64 FStar.HyperStack.ST.push_frame Spec.Exponentiation.exp_fw_lemma Spec.Ed25519.ext_point_c Spec.Ed25519.mk_ed25519_concrete_ops Hacl.Impl.Ed25519.Field51.point_eval Lib.ByteSequence.nat_from_bytes_le Lib.Buffer.as_seq FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Impl.Ed25519.Ladder

module ST = FStar.HyperStack.ST
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum25519
module F51 = Hacl.Impl.Ed25519.Field51

module BSeq = Lib.ByteSequence

module LE = Lib.Exponentiation
module SE = Spec.Exponentiation
module BE = Hacl.Impl.Exponentiation
module ME = Hacl.Impl.MultiExponentiation
module PT = Hacl.Impl.PrecompTable
module SPT256 = Hacl.Spec.PrecompBaseTable256
module BD = Hacl.Bignum.Definitions
module SD = Hacl.Spec.Bignum.Definitions

module S = Spec.Ed25519

open Hacl.Impl.Ed25519.PointConstants
include Hacl.Impl.Ed25519.Group
include Hacl.Ed25519.PrecompTable

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

inline_for_extraction noextract
let table_inv_w4 : BE.table_inv_t U64 20ul 16ul =
  [@inline_let] let len = 20ul in
  [@inline_let] let ctx_len = 0ul in
  [@inline_let] let k = mk_ed25519_concrete_ops in
  [@inline_let] let l = 4ul in
  [@inline_let] let table_len = 16ul in
  BE.table_inv_precomp len ctx_len k l table_len


inline_for_extraction noextract
let table_inv_w5 : BE.table_inv_t U64 20ul 32ul =
  [@inline_let] let len = 20ul in
  [@inline_let] let ctx_len = 0ul in
  [@inline_let] let k = mk_ed25519_concrete_ops in
  [@inline_let] let l = 5ul in
  [@inline_let] let table_len = 32ul in
  assert_norm (pow2 (v l) = v table_len);
  BE.table_inv_precomp len ctx_len k l table_len


inline_for_extraction noextract
val convert_scalar: scalar:lbuffer uint8 32ul -> bscalar:lbuffer uint64 4ul ->
  Stack unit
  (requires fun h -> live h scalar /\ live h bscalar /\ disjoint scalar bscalar)
  (ensures fun h0 _ h1 -> modifies (loc bscalar) h0 h1 /\
    BD.bn_v h1 bscalar == BSeq.nat_from_bytes_le (as_seq h0 scalar))

let convert_scalar scalar bscalar =
  let h0 = ST.get () in
  Hacl.Spec.Bignum.Convert.bn_from_bytes_le_lemma #U64 32 (as_seq h0 scalar);
  Hacl.Bignum.Convert.mk_bn_from_bytes_le true 32ul scalar bscalar


inline_for_extraction noextract
val point_mul_noalloc:
    out:point
  -> bscalar:lbuffer uint64 4ul
  -> q:point ->
  Stack unit
  (requires fun h ->
    live h bscalar /\ live h q /\ live h out /\
    disjoint q out /\ disjoint q bscalar /\ disjoint out bscalar /\
    F51.point_inv_t h q /\ F51.inv_ext_point (as_seq h q) /\
    BD.bn_v h bscalar < pow2 256)
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F51.point_inv_t h1 out /\ F51.inv_ext_point (as_seq h1 out) /\
    S.to_aff_point (F51.point_eval h1 out) ==
    LE.exp_fw S.mk_ed25519_comm_monoid
      (S.to_aff_point (F51.point_eval h0 q)) 256 (BD.bn_v h0 bscalar) 4)

let point_mul_noalloc out bscalar q =
  BE.lexp_fw_consttime 20ul 0ul mk_ed25519_concrete_ops
    4ul (null uint64) q 4ul 256ul bscalar out
val point_mul:
    out:point
  -> scalar:lbuffer uint8 32ul
  -> q:point ->
  Stack unit
  (requires fun h ->
    live h scalar /\ live h q /\ live h out /\
    disjoint q out /\ disjoint q scalar /\
    F51.point_inv_t h q /\ F51.inv_ext_point (as_seq h q))
  (ensures  fun h0 _ h1 -> modifies (loc out) h0 h1 /\
    F51.point_inv_t h1 out /\ F51.inv_ext_point (as_seq h1 out) /\
    S.to_aff_point (F51.point_eval h1 out) ==
    S.to_aff_point (S.point_mul (as_seq h0 scalar) (F51.point_eval h0 q)))

    out: Hacl.Bignum25519.point ->
    scalar: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    q: Hacl.Bignum25519.point
  -> FStar.HyperStack.ST.Stack Prims.unit