Bug 1451395 - update hacl* version to fix image build, r=ttaubert
authorFranziskus Kiefer <franziskuskiefer@gmail.com>
Wed, 04 Apr 2018 10:35:35 +0200
changeset 14307 0b0eb03449450c5af1e2bb4c32a3259923ca2542
parent 14306 954032211d2d303bcee85f448f4db24bb8ec9a0c
child 14308 92ec52c839cb3ae890d7a9f228e3c12dc72b6f38
push id3043
push userfranziskuskiefer@gmail.com
push dateThu, 05 Apr 2018 10:05:13 +0000
reviewersttaubert
bugs1451395
Bug 1451395 - update hacl* version to fix image build, r=ttaubert This version of HACL* has an incomplete proof and has to be update soon. This is to fix the image build til taskcluster is fixed. Differential Revision: https://phabricator.services.mozilla.com/D842
automation/taskcluster/docker-hacl/Dockerfile
lib/freebl/verified/Hacl_Poly1305_32.c
--- a/automation/taskcluster/docker-hacl/Dockerfile
+++ b/automation/taskcluster/docker-hacl/Dockerfile
@@ -4,17 +4,17 @@ MAINTAINER Franziskus Kiefer <franziskus
 # Based on the HACL* image from Benjamin Beurdouche and
 # the original F* formula with Daniel Fabian
 
 # Pinned versions of HACL* (F* and KreMLin are pinned as submodules)
 ENV haclrepo https://github.com/mitls/hacl-star.git
 
 # Define versions of dependencies
 ENV opamv 4.04.2
-ENV haclversion 426abe1c4e55f3e569bd9815d52bffc4daac44e5
+ENV haclversion d10bcb3394f3203318f43259ac8f492c8d28aa66
 
 # Install required packages and set versions
 ADD setup.sh /tmp/setup.sh
 RUN bash /tmp/setup.sh
 
 # Create user, add scripts.
 RUN useradd -ms /bin/bash worker
 WORKDIR /home/worker
--- a/lib/freebl/verified/Hacl_Poly1305_32.c
+++ b/lib/freebl/verified/Hacl_Poly1305_32.c
@@ -54,17 +54,19 @@ Hacl_Bignum_Fproduct_copy_from_wide_(uin
 }
 
 inline static void
 Hacl_Bignum_Fproduct_sum_scalar_multiplication_(uint64_t *output, uint32_t *input, uint32_t s)
 {
     for (uint32_t i = (uint32_t)0U; i < (uint32_t)5U; i = i + (uint32_t)1U) {
         uint64_t xi = output[i];
         uint32_t yi = input[i];
-        output[i] = xi + (uint64_t)yi * (uint64_t)s;
+        uint64_t x_wide = (uint64_t)yi;
+        uint64_t y_wide = (uint64_t)s;
+        output[i] = xi + x_wide * y_wide;
     }
 }
 
 inline static void
 Hacl_Bignum_Fproduct_carry_wide_(uint64_t *tmp)
 {
     for (uint32_t i = (uint32_t)0U; i < (uint32_t)4U; i = i + (uint32_t)1U) {
         uint32_t ctr = i;