val exp_mont_ladder_swap_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 (r0s, r1s, sws) =
      Loops.repeati i (S.exp_mont_ladder_swap_f k.to.comm_monoid bBits b) (k.to.refl one, k.to.refl a, 0) in
    let (r0, r1, sw) =
      Loops.repeati i (exp_mont_ladder_swap_f k bBits b) (one, a, 0) in
    k.to.refl r0 == r0s /\ k.to.refl r1 == r1s /\ sw == sws)
let rec exp_mont_ladder_swap_lemma_loop #t k a bBits b i =
  let one = k.one () in
  let inp0 = (k.to.refl one, k.to.refl a, 0) in
  let inp1 = (one, a, 0) in
  let f0 = S.exp_mont_ladder_swap_f k.to.comm_monoid bBits b in
  let f1 = exp_mont_ladder_swap_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_mont_ladder_swap_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_mont_ladder_swap_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 (r0s, r1s, sws) =
      Loops.repeati i (S.exp_mont_ladder_swap_f k.to.comm_monoid bBits b) (k.to.refl one, k.to.refl a, 0) in
    let (r0, r1, sw) =
      Loops.repeati i (exp_mont_ladder_swap_f k bBits b) (one, a, 0) in
    k.to.refl r0 == r0s /\ k.to.refl r1 == r1s /\ sw == sws)
let rec exp_mont_ladder_swap_lemma_loop #t k a bBits b i =
let one = k.one () in
let inp0 = (k.to.refl one, k.to.refl a, 0) in
let inp1 = (one, a, 0) in
let f0 = S.exp_mont_ladder_swap_f k.to.comm_monoid bBits b in
let f1 = exp_mont_ladder_swap_f k bBits b in
if i = 0
then
  (Loops.eq_repeati0 bBits f0 inp0;
    Loops.eq_repeati0 bBits f1 inp1)
else
  (exp_mont_ladder_swap_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))
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 Prims.op_LessThanOrEqual Prims.op_Equality Prims.int Lib.LoopCombinators.eq_repeati0 FStar.Pervasives.Native.tuple3 Prims.unit Spec.Exponentiation.__proj__Mkto_comm_monoid__item__a_spec Spec.Exponentiation.__proj__Mkconcrete_ops__item__to Prims.bool Lib.LoopCombinators.unfold_repeati Prims.op_Subtraction Spec.Exponentiation.exp_mont_ladder_swap_lemma_loop Spec.Exponentiation.exp_mont_ladder_swap_f Lib.Exponentiation.exp_mont_ladder_swap_f Spec.Exponentiation.__proj__Mkto_comm_monoid__item__comm_monoid FStar.Pervasives.Native.Mktuple3 Spec.Exponentiation.__proj__Mkto_comm_monoid__item__refl Spec.Exponentiation.__proj__Mkconcrete_ops__item__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 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


let exp_rl_lemma #t k a bBits b =
  exp_rl_lemma_loop #t k a bBits b bBits


val exp_mont_ladder_swap_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 (r0s, r1s, sws) =
      Loops.repeati i (S.exp_mont_ladder_swap_f k.to.comm_monoid bBits b) (k.to.refl one, k.to.refl a, 0) in
    let (r0, r1, sw) =
      Loops.repeati i (exp_mont_ladder_swap_f k bBits b) (one, a, 0) in
    k.to.refl r0 == r0s /\ k.to.refl r1 == r1s /\ sw == sws)
val exp_mont_ladder_swap_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 (r0s, r1s, sws) =
      Loops.repeati i (S.exp_mont_ladder_swap_f k.to.comm_monoid bBits b) (k.to.refl one, k.to.refl a, 0) in
    let (r0, r1, sw) =
      Loops.repeati i (exp_mont_ladder_swap_f k bBits b) (one, a, 0) in
    k.to.refl r0 == r0s /\ k.to.refl r1 == r1s /\ sw == sws)

    k: Spec.Exponentiation.concrete_ops t ->
    a: t ->
    bBits: Prims.nat ->
    b: Prims.nat{b < Prims.pow2 bBits} ->
    i: Prims.nat{i <= bBits}
  -> FStar.Pervasives.Lemma
    (ensures
      (let one = Mkconcrete_ops?.one k () in
        let _ =
          Lib.LoopCombinators.repeati i
            (Lib.Exponentiation.exp_mont_ladder_swap_f (Mkto_comm_monoid?.comm_monoid (Mkconcrete_ops?.to
                        k))
                bBits
                b)
            (Mkto_comm_monoid?.refl (Mkconcrete_ops?.to k) one,
              Mkto_comm_monoid?.refl (Mkconcrete_ops?.to k) a,
              0)
        in
        (let FStar.Pervasives.Native.Mktuple3 #_ #_ #_ r0s r1s sws = _ in
          let _ =
            Lib.LoopCombinators.repeati i
              (Spec.Exponentiation.exp_mont_ladder_swap_f k bBits b)
              (one, a, 0)
          in
          (let FStar.Pervasives.Native.Mktuple3 #_ #_ #_ r0 r1 sw = _ in
            Mkto_comm_monoid?.refl (Mkconcrete_ops?.to k) r0 == r0s /\
            Mkto_comm_monoid?.refl (Mkconcrete_ops?.to k) r1 == r1s /\ sw == sws)
          <:
          Type0)
        <:
        Type0))