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_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)
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 FStar.Pervasives.Native.Mktuple2 Spec.Exponentiation.__proj__Mkconcrete_ops__item__sqr Prims.op_Equality Prims.int Lib.Exponentiation.get_ith_bit Prims.bool Spec.Exponentiation.__proj__Mkconcrete_ops__item__mul
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})
val exp_rl_f : k: Spec.Exponentiation.concrete_ops t ->
    bBits: Prims.nat ->
    b: Prims.nat{b < Prims.pow2 bBits} ->
    i: Prims.nat{i < bBits} ->
    _: (t * t)
  -> t * t

    k: Spec.Exponentiation.concrete_ops t ->
    bBits: Prims.nat ->
    b: Prims.nat{b < Prims.pow2 bBits} ->
    i: Prims.nat{i < bBits} ->
    _: (t * t)
  -> t * t