Library mont_mul_strict_prg

Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd.
Require Import multi_lt_prg multi_sub_prg multi_zero_prg mont_mul_prg.

Local Open Scope machine_int_scope.
Local Open Scope mips_cmd_scope.

Definition mont_mul_strict
  (k alpha x y z m_ one ext int_ X_ Y_ M_ Z_ quot C t s_ : reg)
  : while.cmd :=
  montgomery k alpha x y z m_ one ext int_ X_ Y_ M_ Z_ quot C t s_ ;
  ifte_beq C, r0 thendo
    (multi_lt k z m_ X_ Y_ int_ ext Z_ M_;
    ifte_beq int_, r0 thendo
      multi_sub k z m_ z ext int_ quot C Z_ Y_
    elsedo
      nop)
  elsedo
    (addiu t t four16 ;
    sw C zero16 t ;
    addiu ext k one16 ;
    multi_sub ext z m_ z M_ int_ quot C Z_ Y_).

Definition mont_mul_strict_init
  (k alpha x y z m_ one ext int_ X_ Y_ M_ Z_ quot C t s_ : reg)
  : while.cmd :=
  multi_zero k z ext Z_ ;
  (mflhxu r0 ;
  mthi r0 ;
  mtlo r0) ;
  
  mont_mul_strict k alpha x y z m_ one ext int_ X_ Y_ M_ Z_ quot C t s_.