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_add_signed_unsigned_prg

Require Import machine_int.
Import MachineInt.
Require Import mips_bipl mips_cmd.
Import expr_m.
Require Import while.

Local Open Scope mips_cmd_scope.

Require Import pick_sign_prg multi_lt_prg multi_add_prg multi_sub_prg multi_negate_prg copy_prg multi_is_zero_prg.

x <- x + y with x signed and y unsigned <> 0 expect x and y to be rk words long
Definition multi_add_s_u' rk rx ry a0 a1 a2 a3 a4 a5 X :=
  lw X four16 rx ;
  pick_sign rx a0 a1 ;
  ifte (bgez a1)
  (ifte (beq a1 r0)
    (copy rk X ry a2 a3 a4 ;
     addiu a3 r0 zero16 ;
     sw rk zero16 rx)
    (addiu a3 r0 one16 ;
     multi_add rk a3 ry X X a0 a1 a2 ;
     mflo a3))
  (multi_lt rk ry X a0 a1 a5 a2 a3 a4 ;
   ifte (beq a5 r0)
   (ifte (beq a2 r0)
     (addiu a3 r0 zero16 ;
      sw r0 zero16 rx)
     (multi_sub rk ry X X a0 a1 a2 a3 a4 a5 ;
      negate rx a0) )
   (multi_sub rk X ry X a0 a1 a5 a3 a2 a4)).

same as above except that y can be 0
Definition multi_add_s_u rk rx ry a0 a1 a2 a3 a4 a5 X :=
  multi_is_zero rk ry a0 a1 a2 ;
  ifte (bne a2 r0)
  (addiu a3 r0 zero16)
  (multi_add_s_u' rk rx ry a0 a1 a2 a3 a4 a5 X).