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_even_prg

Require Import machine_int.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.
Import expr_m.

Definition multi_is_even (k a ret : reg) :=
  while.ifte (beq k r0)
  (addiu ret r0 one16)
  (lw ret zero16 a ;
  andi ret ret one16 ;
  xori ret ret one16).