checked_ilog: add comments explaining the correctness of the 128 bit optimization

Author: FedericoStra

library/core/src/num/int_macros.rs

@@ -2481,6 +2481,14 @@ macro_rules! int_impl {
 
                 // Optimization for 128 bit wide integers.
                 if Self::BITS == 128 {
+                    // The following is a correct lower bound for ⌊log(base,self)⌋ because
+                    //
+                    // log(base,self) = log(2,self) / log(2,base)
+                    //                ≥ ⌊log(2,self)⌋ / (⌊log(2,base)⌋ + 1)
+                    //
+                    // hence
+                    //
+                    // ⌊log(base,self)⌋ ≥ ⌊ ⌊log(2,self)⌋ / (⌊log(2,base)⌋ + 1) ⌋ .
                     n = self.ilog2() / (base.ilog2() + 1);
                     r = base.pow(n);
                 }

library/core/src/num/uint_macros.rs

@@ -814,6 +814,14 @@ macro_rules! uint_impl {
 
                 // Optimization for 128 bit wide integers.
                 if Self::BITS == 128 {
+                    // The following is a correct lower bound for ⌊log(base,self)⌋ because
+                    //
+                    // log(base,self) = log(2,self) / log(2,base)
+                    //                ≥ ⌊log(2,self)⌋ / (⌊log(2,base)⌋ + 1)
+                    //
+                    // hence
+                    //
+                    // ⌊log(base,self)⌋ ≥ ⌊ ⌊log(2,self)⌋ / (⌊log(2,base)⌋ + 1) ⌋ .
                     n = self.ilog2() / (base.ilog2() + 1);
                     r = base.pow(n);
                 }