Add a comment with an SMT verification of the Barrett reductions.
Change-Id: I32dc13b16733fc09e53e3891ca68f51df6c1624c
Reviewed-on: https://boringssl-review.googlesource.com/7850
Reviewed-by: David Benjamin <davidben@google.com>
diff --git a/crypto/cipher/tls_cbc.c b/crypto/cipher/tls_cbc.c
index 510b4c7..fbc93fa 100644
--- a/crypto/cipher/tls_cbc.c
+++ b/crypto/cipher/tls_cbc.c
@@ -177,6 +177,45 @@
* + md_size = 256 + 48 (since SHA-384 is the largest hash) = 304. */
assert(rotate_offset <= 304);
+ /* Below is an SMT-LIB2 verification that the Barrett reductions below are
+ * correct within this range:
+ *
+ * (define-fun barrett (
+ * (x (_ BitVec 32))
+ * (mul (_ BitVec 32))
+ * (shift (_ BitVec 32))
+ * (divisor (_ BitVec 32)) ) (_ BitVec 32)
+ * (let ((q (bvsub x (bvmul divisor (bvlshr (bvmul x mul) shift))) ))
+ * (ite (bvuge q divisor)
+ * (bvsub q divisor)
+ * q)))
+ *
+ * (declare-fun x () (_ BitVec 32))
+ *
+ * (assert (or
+ * (let (
+ * (divisor (_ bv20 32))
+ * (mul (_ bv25 32))
+ * (shift (_ bv9 32))
+ * (limit (_ bv853 32)))
+ *
+ * (and (bvule x limit) (not (= (bvurem x divisor)
+ * (barrett x mul shift divisor)))))
+ *
+ * (let (
+ * (divisor (_ bv48 32))
+ * (mul (_ bv10 32))
+ * (shift (_ bv9 32))
+ * (limit (_ bv768 32)))
+ *
+ * (and (bvule x limit) (not (= (bvurem x divisor)
+ * (barrett x mul shift divisor)))))
+ * ))
+ *
+ * (check-sat)
+ * (get-model)
+ */
+
if (md_size == 16) {
rotate_offset &= 15;
} else if (md_size == 20) {
