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_sub_signed_signed_prg

Require Import machine_int.
Import MachineInt.
Require Import mips_bipl mips_cmd.

Require Import pick_sign_prg multi_negate_prg multi_add_signed_unsigned_prg multi_sub_signed_unsigned_prg.

Local Open Scope mips_cmd_scope.

x <- x - y with x and y signed, expect x and y to be rk words long
Definition multi_sub_s_s rk rx ry a0 a1 a2 a3 a4 ret X Y :=
  lw Y four16 ry;
  pick_sign ry a0 a1 ;
  while.ifte (expr_m.bgez a1)
  (while.ifte (expr_m.beq a1 r0)
    (addiu a3 r0 zero16)
    (multi_sub_s_u rk rx Y a0 a1 a2 a3 a4 ret X))
  (multi_add_s_u rk rx Y a0 a1 a2 a3 a4 ret X).