Better documentation of polynomial division mod 2

Author: TDecking

src/shims/x86/sse42.rs

@@ -458,6 +458,25 @@ pub(super) trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                 };
 
                 // Perform polynomial division modulo 2.
+                // The algorithm for the division is an adapted version of the
+                // schoolbook division algorithm used for normal integer or polynomial
+                // division. In this context, the quotient is not calculated, since
+                // only the remainder is needed.
+                //
+                // The algorithm works as follows:
+                // 1. Pull down digits until division can be performed. In the context of division
+                //    modulo 2 it means locating the most significant digit of the dividend and shifting
+                //    the divisor such that the position of the divisors most significand digit and the
+                //    dividends most significand digit match.
+                // 2. Perform a division and determine the remainder. Since it is arithmetic modulo 2,
+                //    this operation is a simple bitwise exclusive or.
+                // 3. Repeat steps 1. and 2. until the full remainder is calculated. This is the case
+                //    once the degree of the remainder polynomial is smaller than the degree of the
+                //    divisor polynomial. In other words, the number of leading zeros of the remainder
+                //    is larger than the number of leading zeros of the divisor. It is important to
+                //    note that standard arithmetic comparison is not applicable here:
+                //    0b10011 / 0b11111 = 0b01100 is a valid division, even though the dividend is
+                //    smaller than the divisor.
                 let mut dividend = (crc << bit_size) ^ (v << 32);
                 const POLYNOMIAL: u128 = 0x11EDC6F41;
                 while dividend.leading_zeros() <= POLYNOMIAL.leading_zeros() {