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 copy_prg

Require Import machine_int.
Import MachineInt.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.

Definition copy rk ry rx tmp ytmp i :=
  addiu ytmp ry zero16 ;
  addiu i r0 zero16 ;
  while.while (expr_m.bne i rk) (
    lwxs tmp i rx ;
    sw tmp zero16 ytmp ;
    addiu i i one16 ;
    addiu ytmp ytmp four16).