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>

1 files changed, 39 insertions, 0 deletions

diff --git a/crypto/cipher/tls_cbc.c b/crypto/cipher/tls_cbc.c
index 510b4c73..fbc93fa6 100644
--- a/crypto/cipher/tls_cbc.c
+++ b/crypto/cipher/tls_cbc.c
@@ -177,6 +177,45 @@ void EVP_tls_cbc_copy_mac(uint8_t *out, unsigned md_size,
    * + 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) {