0
$\begingroup$

Let n > 0 be a natural number and for any two reminders a, b modulo 2^n we have that a < b iff a xor 0x800..00 <(signed) b xor 0x800...00.

It is also true that a <(signed) b iff (0x800...00 & b <= 0x800...00 & a) && (a & 0x7FF...FFF < b & 0x7FF...FFF).

Is there a way to prove the equivalence of these two propositions?

$\endgroup$
4
  • $\begingroup$ Two "iff" propositions are logically equivalent iff both are true or both are false. Are you asking whether both "iff" propositions in the question are true? $\endgroup$
    – John L.
    Jul 31 '19 at 17:33
  • $\begingroup$ @Apass.Jack Yes, exactly. Especially I could not prove formally the first iff is true. I treat the second iff to be true as the definition of signed order relation on 2s complement reminders. So I expected that equivalence could be proven. $\endgroup$
    – Some Name
    Jul 31 '19 at 17:35
  • $\begingroup$ Does "two reminders a, b modulo $2^n$" mean two integers $a$ and $b$ such that $0\le a,b\lt2^n$? Does 0x800..00 mean $2^{n-1}$$? What does it mean by (signed) b? Does a xor 0x800..00 <(signed) b xor 0x800...00 mean (a xor 0x800..00) < ((signed)b) xor 0x800...00) where xor is bit xor? $\endgroup$
    – John L.
    Jul 31 '19 at 17:51
  • $\begingroup$ @Apass.Jack Yes, 0 <= a, b < 2^n. By a <(signed) b I meant signed comparison of two arbitrary reminders 2s complement. So not really (signed) b, but < (signed) $\endgroup$
    – Some Name
    Jul 31 '19 at 18:04
2
$\begingroup$

It's even a bit simpler, namely both:

  • a <u b == (a ^ m) <s (b ^ m), and,
  • a <s b == (a ^ m) <u (b ^ m)

Where m is the mask with the sign bit set.

I don't have a formal proof for that, but the image below shows what is happening. The top row shows the "unsigned order" of the number line, chopped in half, with the first part having a 0 in the top bit and the second half having a 1 in the top bit. The bottom row shows the same sub-ranges but in the "signed order". The bottom block in the signed case is the same block as the top block in the unsigned case. Notice that the signed and unsigned order of the two sub-ranges is swapped, but the order within the sub-ranges is the same.

XORing by m is equivalent to adding m and to subtracting m, so you may think of it as:

  • swapping the order of the two sub-ranges (xor)
  • pushing the two sub-ranges to the right (by the width of a block), with wrap-around to the left side (addition)
  • pushing the two sub-ranges to the left, with wrap-around to the right side (subtraction)

In any case the order of the blocks is swapped, so it swaps between the signed order and the unsigned order.

enter image description here

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.