Library copy_u_u_prg

Require Import machine_int.
Import MachineInt.
Require Import mips_cmd.
Import expr_m.

Local Open Scope mips_cmd_scope.

Definition copy_u_u rk ry rx tmp ytmp i :=
  addiu ytmp ry zero16 ;
  addiu i r0 zero16 ;
  While (bne i rk) {{
    lwxs tmp i rx ;
    sw tmp zero16 ytmp ;
    addiu i i one16 ;
    addiu ytmp ytmp four16 }}.