Library mont_exp_prg

Require Import mips_cmd.
Require Import machine_int.
Require Import mont_mul_strict_prg.

Local Open Scope mips_cmd_scope.
Import expr_m.

Definition mont_exp (k alpha x a' x' i l a ei e one' m one ext int_ X_ Y_ M_ Z_ quot C t s_ : reg) :=
mont_mul_strict_init k alpha x a' x' m one ext int_ X_ Y_ M_ Z_ quot C t s_ ;
(addiu i l zero16 ;
while.while (bgez i) (
  mont_mul_strict_init k alpha a a a' m one ext int_ X_ Y_ M_ Z_ quot C t s_;
  srlv ei e i ;
  andi ei ei one16 ;
  ifte_beq ei, r0 thendo
   (xor a a a';
    xor a' a a';
    xor a a a')
  elsedo
   mont_mul_strict_init k alpha a' x' a m one ext int_ X_ Y_ M_ Z_ quot C t s_ ;
  addiu i i mone16));
mont_mul_strict_init k alpha a one' a' m one ext int_ X_ Y_ M_ Z_ quot C t s_.