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_div2_prg

Require Import machine_int.
Require Import mips_cmd.

Local Open Scope mips_cmd_scope.
Import expr_m.

Definition multi_div2 (k a i tmp prev next : reg) :=
  addiu i k zero16 ;
  addiu prev r0 zero16 ;
  while.while (bne i r0) (
    addiu i i mone16 ;
    lwxs tmp i a ;
    andi next tmp one16 ;
    srl tmp tmp one5 ;
    cmd_or tmp tmp prev ;
    addiu prev next zero16 ;
    sll prev prev thirtyone5 ;
    sll next i two5 ;
    addu next a next ;
    sw tmp zero16 next).