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_rl_lemma #t k a bBits b =
  exp_rl_lemma_loop #t k a bBits b bBits
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_rl_lemma #t k a bBits b =
exp_rl_lemma_loop #t k a bBits b bBits
Spec.Exponentiation.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Exponentiation.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Exponentiation.fst
Spec.Exponentiation.concrete_ops Prims.nat Prims.b2t Prims.op_LessThan Prims.pow2 Spec.Exponentiation.exp_rl_lemma_loop Prims.unit
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 1"

val exp_rl_lemma_loop: #t:Type -> k:concrete_ops t
  -> a:t -> bBits:nat -> b:nat{b < pow2 bBits} -> i:nat{i <= bBits} ->
  Lemma (let one = k.one () in
    let (accs, cs) = Loops.repeati i (S.exp_rl_f k.to.comm_monoid bBits b) (k.to.refl one, k.to.refl a) in
    let (acc, c) = Loops.repeati i (exp_rl_f k bBits b) (one, a) in
    k.to.refl acc == accs /\ k.to.refl c == cs)

let rec exp_rl_lemma_loop #t k a bBits b i =
  let one = k.one () in
  let inp0 = (k.to.refl one, k.to.refl a) in
  let inp1 = (one, a) in
  let f0 = S.exp_rl_f k.to.comm_monoid bBits b in
  let f1 = exp_rl_f k bBits b in

  if i = 0 then begin
    Loops.eq_repeati0 bBits f0 inp0;
    Loops.eq_repeati0 bBits f1 inp1 end
  else begin
    exp_rl_lemma_loop #t k a bBits b (i - 1);
    Loops.unfold_repeati bBits f0 inp0 (i - 1);
    Loops.unfold_repeati bBits f1 inp1 (i - 1) end
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)

    k: Spec.Exponentiation.concrete_ops t ->
    a: t ->
    bBits: Prims.nat ->
    b: Prims.nat{b < Prims.pow2 bBits}
  -> FStar.Pervasives.Lemma
    (ensures
      Mkto_comm_monoid?.refl (Mkconcrete_ops?.to k) (Spec.Exponentiation.exp_rl k a bBits b) ==
      Lib.Exponentiation.exp_rl (Mkto_comm_monoid?.comm_monoid (Mkconcrete_ops?.to k))
        (Mkto_comm_monoid?.refl (Mkconcrete_ops?.to k) a)
        bBits
        b)