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_zero_prg

Require Import machine_int.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.
Import expr_m.

Definition multi_zero (k z ext Z_ : reg) : while.cmd :=
  addiu Z_ z zero16 ;
  addiu ext k zero16 ;
  while.while (bne ext r0) (
    sw r0 zero16 Z_ ;
    addiu Z_ Z_ four16 ;
    addiu ext ext mone16).

Definition multi_zero_signed (rx a0 a1 a2 a3 : reg) : while.cmd :=
  lw a0 zero16 rx ;
  lw a1 four16 rx ;
  multi_zero a0 a1 a2 a3.