To be clear, I am certain that the derivation below is incorrect, but I am hoping someone can point out where in my "proof" I am wrong.
I am trying to prove that the x86 instruction setb indeed implements x<y as an unsigned comparison when used after a cmp instruction. Specifically, let us consider (ATT syntax, and I will neglect suffixes indicting the number of bits)
# Compare two registers, e.g., %eax and %ebx with values y and x, respectively, when unsigned
cmp %ebx, %eax
# Set %al to 1 if %eax is below %ebx (unsigned comparison)
setb %al
The claim is that %al gets value 1 at the end of this if and only if the values of x,y obey x<y when considered as unsigned. We note that in the ATT syntax, the cmp instruction is subtracting the contents of %ebx from the contents of %eax and that this operation sets the relevant condition flags appropriately--including the carry out flag, which is of interest here. That is, it is putting the bit pattern into a subtractor unit to calculate x(-^u)y, where I use that notation to describe unsigned subtraction and I'll use - to describe subtraction of the corresponding integers.
Now here is my problem. Let's suppose x<y. We want to show that a carry out results from the subtraction. Suppose each number is w bits. I know (from my text, Bryant and O'Hallaron's CS:APP3e) that
x(-^u)y := x(+^u)((-^u) y) = x(+^u)(2^w - y) = 2^w + x - y < 2^w,
so ostensibly no carry out was obtained since the result fits into our w bits. That is, no carry out. This is just one direction of the "proof", but already I can clearly see I am wrong. Where am I going wrong though?
x86's sub and cmp set CF if there's a borrow from the subtraction. This is the case if there's no carry-out from adding the bitwise-inverse with a carry-in of 1, like the binary adder-subtractor in the ALU does.
Some ISAs (like ARM) are opposite of x86 for sub, set their carry flag directly from the carry-out of the adder-subtractor. x86 (and some other ISAs) invert it.
Related: Arithmetic identities and EFLAGS - note that a correct asm equivalent to sub is a single add with carry-in of 1 and a cmc, not a separate neg and add, if you care about the EFLAGS result.