plonky2/system_zero/src/alu/div-constraints-proof.txt

Constraints A (implemented in code):
A1. dividend ∈ {0, …, u32::MAX}
A2. divisor ∈ {0, …, u32::MAX}
A3. quotient ∈ {0, …, u32::MAX}
A4. remainder ∈ {0, …, u32::MAX}
A5. divisor_rem_diff_m1 ∈ {0, …, u32::MAX}
A6. divisor * div_inverse = div_div_inverse
A7. (div_div_inverse - 1) * (remainder - quotient - u32::MAX) = 0
A8. divisor * (div_div_inverse - 1) = 0
A9. div_inverse * dividend = quotient + remainder * div_inverse
A10. divisor * (divisor - remainder - 1 - divisor_rem_diff_m1) = 0

Constraints B (intuitive division):
B1. dividend ∈ {0, …, u32::MAX}
B2. divisor ∈ {0, …, u32::MAX}
B3. divisor = 0 => quotient = 0
B4. divisor = 0 => remainder = u32::MAX
B5. divisor ≠ 0 => dividend = quotient * divisor + remainder
B6. divisor ≠ 0 => quotient ∈ {0, …, u32::MAX}
B7. divisor ≠ 0 => remainder ∈ {0, …, divisor - 1}



Assume we meet constraints A for some dividend, divisor, quotient, remainder, divisor_rem_diff_m1, div_inverse, and div_div_inverse. We want to show that constrants B are met.

B1. Trivial by A1.

B2. Trivial by A2.

B3. Assume divisor = 0. Then div_div_inverse = 0 by A6. div_div_inverse - 1 ≠ 0, so remainder - quotient = u32::MAX by A7.
quotient ∈ {0, …, u32::MAX} by A3 and remainder ∈ {0, …, u32::MAX} by A4. Then remainder - quotient ∈ {-quotient, …, u32::MAX - quotient}.
If quotient ≠ 0, then quotient ∈ {1, …, u32::MAX} and remainder - quotient ∈ {-u32::MAX, …, u32::MAX - 1}, which does not include u32::MAX, contradicting A7.

B4. Assume divisor = 0. Then div_div_inverse = 0 by A6. div_div_inverse - 1 ≠ 0, so remainder - quotient = u32::MAX by A7.
quotient ∈ {0, …, u32::MAX} by A3 and remainder ∈ {0, …, u32::MAX} by A4. Then remainder - quotient ∈ {remainder - u32::MAX, …, remainder}.
If remainder ≠ u32::MAX, then remainder ∈ {0, …, u32::MAX - 1} and remainder - quotient ∈ {-u32::MAX, …, u32::MAX - 1} which does not include u32::MAX, contradicting A7.

B5. Assume divisor ≠ 0. By A8, div_div_inverse = 1. By A6, div_inverse = divisor^-1. Multiplying both sides of A9 by divisor, dividend = quotient * divisor + remainder.

B6. Follows from A3.

B7. remainder ∈ {0, …, u32::MAX} by A4. Assume divisor ≠ 0. Then divisor_rem_diff_m1 = divisor - remainder - 1 by A10. divisor ∈ {1, …, u32::MAX} by A2. If remainder ∈ {divisor, …, u32::MAX}, then divisor - remainder - 1 ∈ {-u32::MAX, …, u32::MAX - divisor} ⊆ {-u32::MAX, …, u32::MAX - 1}, contradicting A5. Hence, remainder ∈ {0, …, divisor - 1}.



Assume we meet constraints B for some dividend, divisor, quotient, and remainder. We want to show
that there exist divisor_rem_diff_m1, div_inverse, div_div_inverse, such that constrants A are met.

If divisor = 0, set divisor_rem_diff_m1 = 0, div_inverse = 0, div_div_inverse = 0.
Otherwise, set divisor_rem_diff_m1 = divisor - remainder - 1, div_inverse = divisor^-1, div_div_inverse = 1.

A1. Trivial by B1.

A2. Trivial by B2.

The remainder is by cases:

(divisor = 0)

    A3. Follows from B3.
    
    A4. Follows from B4.
    
    A5. Follows from our choice of divisor_rem_diff_m1 = 0.

    A6. Follows from our choice of div_div_inverse = 0.

    A7. quotient = 0 by B3. remainder = u32::MAX by B4. Then remainder - quotient = u32::MAX.

    A8. Trivial since divisor = 0.

    A9. By our choice, div_inverse = 0. quotient = 0 by B3.

    A10. Trivial since divisor = 0.


(divisor ≠ 0)

    A3. Follows from B6.

    A4. By B7, remainder ∈ {0, …, divisor - 1}, and by B2, divisor ∈ {0, …, u32::MAX}, implying that remainder ∈ {0, …, u32::MAX - 1}.

    A5. We've set divisor_rem_diff_m1 = divisor - remainder - 1. remainder ∈ {0, …, divisor - 1}, so divisor - remainder ∈ {1, …, divisor} and divisor - remainder - 1 = divisor_rem_diff_m1 ∈ {0, …, divisor - 1}. From B2, divisor ∈ {0, …, u32::MAX}, so divisor_rem_diff_m1 ∈ {0, …, u32::MAX - 1} as desired.

    A6. div_inverse = divisor^-1 by choice, so divisor * div_inverse = 1. div_div_inverse = 1 by choice.

    A7. div_div_inverse = 1 by choice, so div_div_inverse - 1 = 0.

    A8. div_div_inverse = 1 by choice, so div_div_inverse - 1 = 0.

    A9. From B5, dividend = quotient * divisor + remainder. Since divisor ≠ 0, div_inverse = divisor^-1 by choice. Multiplying both sides by div_inverse, dividend * div_inverse = quotient * divisor * div_inverse + remainder * div_inverse = quotient + remainder * div_inverse.

    A10. By our choice of divisor_rem_diff_m1 = divisor - remainder - 1.