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_is_zero_prg

Require Import machine_int.
Import MachineInt.
Require Import mips_bipl mips_cmd.

Local Open Scope mips_cmd_scope.

Definition multi_is_zero k z k0 a0 ret :=
  addiu k0 r0 zero16 ;
  addiu ret r0 one16;
  while.while (expr_m.bne k0 k) (
    lwxs a0 k0 z ;
    movn ret r0 a0 ;

    addiu k0 k0 one16 ).