Comparing encoded signed words

The low bits distinguish opposite signs. Within one sign, the encoded unsigned comparison has the usual order for nonnegative integers and the reverse order for negative integers. No signed comparison is added to the target machine.

Main definitions

• Signed.less: an unsigned instruction block comparing the encoded input registers.

Main results

• Signed.exec_less: comparison in at most eleven instructions, with the arithmetic frame.

References

The instruction block is an original implementation using the sign-and-magnitude encoding.

def Cslib.WordRAM.Signed.less {r : ℕ} : Code Basis.standard (r + 9)

Compare two encoded signed integers, returning zero or one in result.

theorem Cslib.WordRAM.Signed.exec_less {r w : ℕ} (h2 : Fits w 2) (x : Data (r + 9)) {a b : ℤ} (hxa : x.regs left = encode a) (hxb : x.regs right = encode b) : ∃ (y : Data (r + 9)), ExecWithin w less x y 11 ∧ (y.regs result = if a < b then 1 else 0) ∧ Frame x y

Signed comparison costs at most eleven unsigned instructions. The input encodings may be used at any physical width admitting the constant two; the frame preserves the operands.