NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library multi_sub_prg

Require Import machine_int.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.
Import expr_m.

Definition multi_sub (k a b c t j u bor atmp btmp : reg) :=
  addiu j r0 zero16;
  addiu t c zero16;
  addiu bor r0 zero16;
  while.while (bne j k) (
    lwxs atmp j b;
    addu btmp atmp bor;
    sltu u btmp atmp;
    lwxs atmp j a;
    ifte_beq u, r0 thendo
      addiu u r0 one16;
      multu atmp u;
      msubu btmp u;
      sltu bor atmp btmp;
      mflhxu atmp
    elsedo
      nop ;
    sw atmp zero16 t;
    addiu t t four16;
    addiu j j one16).