val exp_mont_ladder_swap (#t: Type) (k: concrete_ops t) (a: t) (bBits: nat) (b: nat{b < pow2 bBits})
    : t
let exp_mont_ladder_swap (#t:Type) (k:concrete_ops t) (a:t) (bBits:nat) (b:nat{b < pow2 bBits}) : t =
  let (r0, r1, sw) = Loops.repeati bBits (exp_mont_ladder_swap_f k bBits b) (one (), a, 0) in
  let (r0, r1) = S.cswap sw r0 r1 in
  r0
val exp_mont_ladder_swap (#t: Type) (k: concrete_ops t) (a: t) (bBits: nat) (b: nat{b < pow2 bBits})
    : t
let exp_mont_ladder_swap (#t: Type) (k: concrete_ops t) (a: t) (bBits: nat) (b: nat{b < pow2 bBits})
    : t =
let r0, r1, sw = Loops.repeati bBits (exp_mont_ladder_swap_f k bBits b) (one (), a, 0) in
let r0, r1 = S.cswap sw r0 r1 in
r0
Spec.Exponentiation.fsti.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Exponentiation.fsti
Spec.Exponentiation.concrete_ops Prims.nat Prims.b2t Prims.op_LessThan Prims.pow2 FStar.Pervasives.Native.tuple2 Lib.Exponentiation.cswap FStar.Pervasives.Native.tuple3 Lib.LoopCombinators.repeati Spec.Exponentiation.exp_mont_ladder_swap_f FStar.Pervasives.Native.Mktuple3 Spec.Exponentiation.one
module Spec.Exponentiation

open FStar.Mul

open Lib.IntTypes
open Lib.Sequence

module S = Lib.Exponentiation
module Loops = Lib.LoopCombinators

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

(**
 This is a specification for generic exponentiation defined as
 a repeated application of a commutative monoid operation.

  • Modular Exponentiation: repeated modular multiplication
  • Elliptic Curve Scalar Multiplication: repeated point addition

 In hacl-star, in order to obtain a verified C implementation,
 we split our proofs into three steps:

  • high-level specification (lib/Lib.Exponentiation)
  • low-level specification (specs/Spec.Exponentiation)
  • low-star implementation (code/bignum/Hacl.Impl.Exponentiation)

 For example, to efficiently compute the EC scalar multiplication
 for Ed25519, we use point addition and doubling formulas in
 projective coordinates (see specs/Spec.Ed25519).

  • we first prove that (points on the curve, aff_point_add) forms
    a commutative monoid (`mk_ed25519_comm_monoid`)
  • we then prove the relation between point addition and doubling
    formulas in projective and affine coordinates (`mk_ed25519_concrete_ops`)
  • finally, we can obtain any implementation of exponentiation,
    e.g., a double fixed-window method, by providing the corresponding
    instance of the `concrete_ops` type class (`point_mul_double`)

 Another example is using Montgomery arithmetic (code/bignum) to compute
 a modular exponentiation (lib/Lib.NatMod).
*)

inline_for_extraction
class to_comm_monoid (t:Type) = {
  a_spec: Type;
  comm_monoid: S.comm_monoid a_spec;
  refl: x:t -> a_spec;
}


inline_for_extraction
let one_st (t:Type) (to:to_comm_monoid t) = unit -> Pure t
  (requires True)
  (ensures  fun one ->
    to.refl one == to.comm_monoid.S.one)


inline_for_extraction
let mul_st (t:Type) (to:to_comm_monoid t) = x:t -> y:t -> Pure t
  (requires True)
  (ensures  fun xy ->
    to.refl xy == to.comm_monoid.S.mul (to.refl x) (to.refl y))


inline_for_extraction
let sqr_st (t:Type) (to:to_comm_monoid t) = x:t -> Pure t
  (requires True)
  (ensures  fun xy ->
    to.refl xy == to.comm_monoid.S.mul (to.refl x) (to.refl x))


inline_for_extraction
class concrete_ops (t:Type) = {
  to: to_comm_monoid t;
  one: one_st t to;
  mul: mul_st t to;
  sqr: sqr_st t to;
}


let exp_rl_f (#t:Type) (k:concrete_ops t)
  (bBits:nat) (b:nat{b < pow2 bBits})
  (i:nat{i < bBits}) ((acc, c) : tuple2 t t) : tuple2 t t
 =
  let acc = if (S.get_ith_bit bBits b i = 0) then acc else k.mul acc c in
  let c = k.sqr c in
  (acc, c)


let exp_rl (#t:Type) (k:concrete_ops t) (a:t) (bBits:nat) (b:nat{b < pow2 bBits}) : t =
  let one = k.one () in
  let (acc, c) = Loops.repeati bBits (exp_rl_f k bBits b) (one, a) in
  acc


val exp_rl_lemma: #t:Type -> k:concrete_ops t -> a:t -> bBits:nat -> b:nat{b < pow2 bBits} ->
  Lemma (k.to.refl (exp_rl k a bBits b) == S.exp_rl k.to.comm_monoid (k.to.refl a) bBits b)


let exp_mont_ladder_swap_f (#t:Type) (k:concrete_ops t)
  (bBits:nat) (b:nat{b < pow2 bBits})
  (i:nat{i < bBits}) ((r0, r1, privbit) : tuple3 t t nat) : tuple3 t t nat
 =
  let bit = S.get_ith_bit bBits b (bBits - 1 - i) in
  let sw = (bit + privbit) % 2 in
  let r0, r1 = S.cswap sw r0 r1 in
  let r0, r1 = (k.sqr r0, k.mul r1 r0) in
  (r0, r1, bit)
val exp_mont_ladder_swap (#t: Type) (k: concrete_ops t) (a: t) (bBits: nat) (b: nat{b < pow2 bBits})
    : t

    k: Spec.Exponentiation.concrete_ops t ->
    a: t ->
    bBits: Prims.nat ->
    b: Prims.nat{b < Prims.pow2 bBits}
  -> t