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_unsigned_prg

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

Require Import pick_sign_prg multi_add_signed_unsigned_prg multi_add_prg multi_lt_prg multi_sub_prg multi_negate_prg copy_prg multi_is_zero_prg.

Local Open Scope mips_cmd_scope.

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

same as above, but y can be 0
Definition multi_sub_s_u rk rx ry a0 a1 a2 a3 a4 ret X :=
  multi_is_zero rk ry a0 a1 a2 ;
  while.ifte (expr_m.bne a2 r0)
  (addiu a3 r0 zero16)
  (multi_sub_s_u' rk rx ry a0 a1 a2 a3 a4 ret X).