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_lt_prg

Require Import machine_int.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.
Import expr_m.

Definition multi_lt (k a b i flag ret ret2 atmp btmp : reg) : while.cmd :=
addiu i k zero16 ;
addiu flag r0 one16 ;
while.ifte (beq i r0) (
  addiu ret r0 zero16 ;
  addiu ret2 r0 zero16)
(while.while (bne flag r0) (
  addiu i i mone16 ;
  lwxs atmp i a ;
  lwxs btmp i b ;
  sltu ret atmp btmp ;
  movn flag r0 ret ;
  sltu ret2 btmp atmp ;
  movn flag r0 ret2 ;
  movz flag r0 i )).