Bug 1574643 - NSS changes for haclv2 r=jcj,kjacobs
☠☠ backed out by f6d8c73584e0 ☠ ☠
authorFranziskus Kiefer <franziskuskiefer@gmail.com>
Wed, 18 Dec 2019 18:03:47 +0000
changeset 15436 ac51d2490f9c3fccae9fd1408f4b5ef3b20c9cb4
parent 15435 c351b2f60b400c8cc4ecffe3418cb8b2d0e5520b
child 15437 3ba8a584ddeaf1b4d81fabc650ff7c86223a72d5
push id3617
push userfranziskuskiefer@gmail.com
push dateThu, 19 Dec 2019 07:52:30 +0000
reviewersjcj, kjacobs
bugs1574643, 1604130, 1593647
Bug 1574643 - NSS changes for haclv2 r=jcj,kjacobs This patch contains the changes in NSS, necessary to pick up HACL*v2 in D55413. It has a couple of TODOs: * The chacha20 saw verification fails for some reason; it's disabled pending Bug 1604130. * The hacl task on CI requires Bug 1593647 to get fixed. Depends on D55413. Differential Revision: https://phabricator.services.mozilla.com/D55414
automation/saw/chacha20.saw
automation/taskcluster/docker-builds/Dockerfile
automation/taskcluster/docker-hacl/B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc
automation/taskcluster/docker-hacl/Dockerfile
automation/taskcluster/docker-hacl/bin/checkout.sh
automation/taskcluster/docker-hacl/license.txt
automation/taskcluster/docker-hacl/setup-user.sh
automation/taskcluster/docker-hacl/setup.sh
automation/taskcluster/graph/src/extend.js
automation/taskcluster/scripts/run_hacl.sh
gtests/pk11_gtest/pk11_chacha20poly1305_unittest.cc
lib/freebl/Makefile
lib/freebl/blapii.h
lib/freebl/blinit.c
lib/freebl/chacha20poly1305.c
lib/freebl/det_rng.c
lib/freebl/ecl/curve25519_64.c
lib/freebl/freebl.gyp
lib/freebl/freebl_base.gypi
nss-tool/hw-support.c
--- a/automation/saw/chacha20.saw
+++ b/automation/saw/chacha20.saw
@@ -29,12 +29,12 @@ let SpecChaCha20 n = do {
   ctr <- llvm_var "ctr" (llvm_int 32);
 
   llvm_ensure_eq "*output" {{ chacha20::encrypt k ctr n1 plain }};
 
   llvm_verify_tactic abc;
 };
 
 print "Proving equality for a single block...";
-time (llvm_verify m "Hacl_Chacha20_chacha20" [] (SpecChaCha20 64));
+time (llvm_verify m "Hacl_Chacha20_chacha20_encrypt" [] (SpecChaCha20 64));
 
 print "Proving equality for multiple blocks...";
-time (llvm_verify m "Hacl_Chacha20_chacha20" [] (SpecChaCha20 256));
+time (llvm_verify m "Hacl_Chacha20_chacha20_encrypt" [] (SpecChaCha20 256));
--- a/automation/taskcluster/docker-builds/Dockerfile
+++ b/automation/taskcluster/docker-builds/Dockerfile
@@ -29,19 +29,23 @@ RUN apt-get update \
     linux-libc-dev:i386 \
     llvm-dev \
     locales \
     mercurial \
     ninja-build \
     pkg-config \
     valgrind \
     zlib1g-dev \
+    clang-format-3.9 \
  && rm -rf /var/lib/apt/lists/* \
  && apt-get autoremove -y && apt-get clean -y
 
+RUN update-alternatives --install /usr/bin/clang-format \
+    clang-format $(which clang-format-3.9) 10
+
 # Latest version of abigail-tools
 RUN apt-get update \
  && apt-get install -y --no-install-recommends automake libtool libxml2-dev \
  && git clone git://sourceware.org/git/libabigail.git /tmp/libabigail \
  && cd /tmp/libabigail \
  && autoreconf -fi \
  && ./configure --prefix=/usr --disable-static --disable-apidoc --disable-manual \
  && make && make install \
deleted file mode 100644
--- a/automation/taskcluster/docker-hacl/B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc
+++ /dev/null
@@ -1,143 +0,0 @@
------BEGIN PGP PUBLIC KEY BLOCK-----
-
-mQINBFS+1SABEACnmkESkY7eZq0GhDjbkWpKmURGk9+ycsfAhA44NqUvf4tk1GPM
-5SkJ/fYedYZJaDVhIp98fHgucD0O+vjOzghtgwtITusYjiPHPFBd/MN+MQqSEAP+
-LUa/kjHLjgyXxKhFUIDGVaDWL5tKOA7/AQKl1TyJ8lz89NHQoUHFsF/hu10+qhJe
-V65d32MXFehIUSvegh8DrPuExrliSiORO4HOhuc6151dWA4YBWVg4rX5kfKrGMMT
-pTWnSSZtgoRhkKW2Ey8cmZUqPuUJIfWyeNVu1e4SFtAivLvu/Ymz2WBJcNA1ZlTr
-RCOR5SIRgZ453pQnI/Bzna2nnJ/TV1gGJIGRahj/ini0cs2x1CILfS/YJQ3rWGGo
-OxwG0BVmPk0cmLVtyTq8gUPwxcPUd6WcBKhot3TDMlrffZACnQwQjlVjk5S1dEEz
-atUfpEuNitU9WOM4jr/gjv36ZNCOWm95YwLhsuci/NddBN8HXhyvs+zYTVZEXa2W
-l/FqOdQsQqZBcJjjWckGKhESdd7934+cesGD3O8KaeSGxww7slJrS0+6QJ8oBoAB
-P/WCn/y2AiY2syEKp3wYIGJyAbsm542zMZ4nc7pYfSu49mcyhQQICmqN5QvOyYUx
-OSqwbAOUNtlOyeRLZNIKoXtTqWDEu5aEiDROTw6Rkq+dIcxPNgOLdeQ3HwARAQAB
-tCFIYW5zIFdlbm5ib3JnIDxoYW5zQGNocm9taXVtLm9yZz6JARwEEAECAAYFAlT2
-MQAACgkQVfXNcLtaBWnDKgf/fjusXk+kh1zuyn5eOCe16+2vV1lmXZrDIGdJtXDW
-ZtHKele1Yv1BA3kUi5tKQi+VOOrvHL0+TMjFWFiCy1sYJS9qgkS08kReI2nAnhZ7
-INdqEVxtVk1TTOhtYjOPy6txwujoICuPv5F4rHVhn1LPKGTLtYD2LOwf/8eKYQox
-51gaJ8dNxpcHE/iFOIDXdebJPufo3EhqDRihchxb8AVLhrNss7pGGG/tVfichmHK
-djPT2KfSh14pq1ahFOz0zH4nmTu7CCLnLAdRBHuhL8HVDbi0vKBtCiSmQggdxvoj
-u+hpXiiDFQoCjLh0zVCwtFqWDZbnKMTBNNF26aTmQ+2fiYkBMwQQAQgAHRYhBB/m
-NI7eqCWiKXDlxI3TBA8SPMP0BQJbcLU1AAoJEI3TBA8SPMP021sH/jD1m7azNCN6
-DVL1iDJT6uIIYCTylygH5XI46CRoWaz/LwdFnUqWHHTcQxJ5pIkWV9KF+SIgMT42
-brdZZmNvvSdX0odjFKqj5UR6w+wDN+uZ6Q40zu4pNoNzbk7pRpbFf1XIfGB1liyu
-m28EJ58IXu/0AV7FiDAHGGBqppK/cwQN8pGLwmz1n6YELtXeFmtOGnusO6iLYOE7
-3ByFCCqJB6twT5+7dDqFYqqQJgQ6jDTy19dDZ1vDhDttL+2Rn0OYXqPw7gy/1D2p
-Y1cM9PgPBsR4EXhbtV0uKUNomk8tM/HnGMFT0KirI/tSwEP3v9g5YH992mrvNuIV
-TkyQn0jGeMeJATMEEAEIAB0WIQRswFHTwdmkr54mDFjT45SsdE4uuwUCW3haCQAK
-CRDT45SsdE4uu4JjCACppkreiMrpJSREKbUscdOvFxFRYzkTFeSCwX9Ih7r5ENpa
-zjczfIqCCfWzioV6y4K0V04y8CXt/5S5a9vfW801pBUdF9nG4X8YbUn/xSe+8A9m
-MsfDjMNcF7Cp5czVoSS4/4oHm9mQUMYQsn3AwwCPDKFORRRv5Eb0om9JawKtt++7
-ZW0fOgDkvOCm14SN0UtVc4mxTx6iyxdMDgrKinBZVjxEh5oeqUyXh5TYM+XyWFVh
-/gDUvUWwLI0GUWNTyOyUQU1oPVp+sWqrEe1BXLVCKFVWaSTtgJtJ5FyP+z2uzRcv
-aanPOj/ohHAo8VBq9QbefYVAkShNBEuJkATnXhcGiQEzBBABCAAdFiEEvlzFWRM6
-4JjNAb2a+j2ZL9Cqr7wFAlkBCcIACgkQ+j2ZL9Cqr7yB9AgArj+0+i0DCo1nm4MF
-TLnW1Y9GF/Hq/mBva1MhkT0j3BzENK3xgqrqac8KqupsporNEmJ0ZbZzilJdZImb
-o4X5BFdmmnjMiGaH6GAiPqRBBHGvLV2r2pG467J4tOMWO3XipFRf7FibbfhAU1lV
-/GLWYTSwLqwWwBE8u5rriEvDngWUJw2Yd4Yqwduef7O6F+JfsGPRXFomR3387II0
-8AXo/C+P5cl64llaxV6BmkJhQ6ydL0/KwSkHVdlXugk1sPtV/qOyPQ5L1Ibqbsvh
-lLq/jhHlUUNLFjlQ2lrS9bhHGw9OIHTMJvS8RDrk0yAmoHAyRWNgbFN7aA62vBhq
-pcUVzokBMwQQAQgAHRYhBPZ+fW6ADyQOg+vIZ/9qyaZGTfCcBQJa+ZAwAAoJEP9q
-yaZGTfCcKMgH/jRxGfYhhGnlMnDLAEpYC+TGSDLMgmg9cOZbonqyMv+7Kts+pV03
-KUr9SPV+VtGtOxRNiqwFt6V2MHcwPJfTXuH/bBW/HCCpr6UlOVWqIiCNK0Gnpcj5
-rRt5unjG9CwsgyaK9QPI8bGin/c6m8BjwmEdfJ01ATLiUb8WuDHQy9OCyrEAnzSq
-FD5ZtFmAFxvzm2x1nwb5HPuqkOqbRatp8aRJzTxIeSJPpgLw0PawHKGN3Ckp7REc
-g26P1spkPe7SIVRsobH3al4uw7mgs7wiDWN3t8CdmuHAzmB2UrsR84JMTb45GboO
-Bc1CX8xZcHyNaDEpyWHav+P8nZqwfBm+cLiJAjMEEAEIAB0WIQSawVDb4dGOtiX0
-+gWyD0lU8+/LPwUCW/4O9QAKCRCyD0lU8+/LPyI7EACWtj0GEb1VT02gKwtKwgFn
-RJ2pz8vYm188wgJwCJaL04d2D/VwE0jMvmfH80hSKgSLPAVMG06RIOb/tGhHsQKU
-zBlHiAFmfjlJo1FC/Mp44RrERRsFAWBg0/URIs4vP8+5Vl+5m70sZrQpKeq+6TLM
-1dQ0Ohz+QkQ04Z+DTroChWU8/7Uw0E3CqGGKYqPvDh54T1q4s8FoN0no8ZUlt/O+
-r/3c7awr85ZnxqtnHIcuMbVyIZ+gOqXdrLa85yZITsh4zQrjYuyTEg7dpziReyiZ
-+rkpdIdFKl8YeD+d0JWzVm7kq9D4K3+x9C509z0IgJUT3bhsX/N0Yf/QUtUW5oxI
-T7fod86B/Q2M7zBTttFhd1vAjiSjEalK48SjTzWqTDYVIkea1+f1kZK5A0QlthqG
-P2zy5GUjZVzOiCSOhyEOvAorU3zKD2s84VFKlayZEqlHJh8u5U59TWBdkW3qZUJd
-ewW31xt0s8IovYSgOwX3wbsClQs6eVwNuCZT2yQAgAyXA5iFztBvDRQ0qmetvzV2
-Ay9SrjvkQ3qr/eZmbMErEwEUxIO4b1rctCQ6jcbyVxMTAZAfaDoVKWEMXNiF2KSw
-F9SSzGPIZDgiEXUlgaJBlUIYSFxrPuE+da0CM5RixyYIinU6AER6crl9C4C9XL6a
-u3jf+5MTGxviRGn2oQzSCYkCMwQQAQgAHRYhBKeHFU4z7cw4HFbYuaxFYRTTj42I
-BQJboq6kAAoJEKxFYRTTj42IWIAP/3rc9GjDTM4nI6Oi4OzLkwm/I2Vr7LUKG8oX
-8E4Nj3amvNGupzGySjB+vrM6APrMSScXunvM0f19LV84EnNrUQ3KFZcSC6r5WC0B
-2+TVRYGpY+6R9AQpqnuxicW0sa/AlV9WSEb4fDavCel2nW0arH4wkkCzTThUxoBB
-X4I9nf4ZzGoUnnDAwTD9rN0gpI6Td/7faa3t99dRLb6AHJ1KhvyiiV3lr0xtTssD
-xVHo0SpzQTnOcRJnYf/2rTny8bVfROPWieh6HuEiP7SxT1HyeTr4WSAjSCoG95O2
-b3OgSMl0Z82FRMoJYmxID/V5YqH7015SjCxKdYhEZVp9YwWruEJIH8r6MGbWYNAl
-REnyDvfGzAF0L0+gAUymDRmtp1jeXLo+HmLgVEUWegafs1TPfCWS/H9n10Upjmuq
-akituzacz6Kjleq9qbnl81Xmh4AKmOILRwE7Pmcbl8HATOrmi5EaKffjMdWFzOWh
-3U4/VsNDujqSTXD88EjGcpLiIiYefGy0sURJbIMTkfXVt3ruHLyuvhsRE/2QEAi7
-gWB0zuBV8iGBaag+6RQkxGdpemPiogzuDijqZHoUXlp7Q6IYLanXeweyivdrSyTB
-4HOECDbWEPZwk6tCxnuklW5iJndxBmxjSxefIMGU7G2JS9quppCVFCrKUjIWnf7b
-gXnNji5JiQIzBBABCAAdFiEExZuSbLy7rtFhdiOuHt8NuZ2LeoQFAluirpUACgkQ
-Ht8NuZ2LeoR/gQ/6A71JxUavzyBlCXlMy2Hx2+gOfy68b8UWl7DwKTOBSoZOzPC7
-dVCSTzoK8dRELqsp7CkFImWcEwLJWMptuH2I1nK+Ua8bvxJSMJnOlPxYE8Wz5EK3
-SQ2mQvifRezQTe8zjdpxEDSR6xocSiigvJow4X+Mivrxxj8sMgu1KA1ud2VGX/IR
-wMbwuBTH9YydgvzmFzTxdlJHEYmsI8koHrVWPHm//QqqPBn+qz2z9uAzDmGAiDYg
-qtQijo5IJC8ZjxgdcTfCkN6he+GhHtOhyP/KF/FcRHY83DoNCtqexQZWGuKtbd8o
-nQYtmemRFob5kR7GxuNdAqF74oQfXcvXZNtHSuN3VtLqkB4fzW+21JBJCsP3XCzd
-nKjR4erXNrQycmp3shSoJbnVvdbDwaVlWhDen1DvJb0Lj2sO3PQPcwVQbf5XHWR/
-ZCf2OQTfVgwFEB4/0Twv70XwYIui2Ry9hmTPbD4Nn+UXbMQ3SOp90tj/e2yY/MFt
-FvcIYcJTk9LM5IsnKgh+fSWDmdS3HD5Kjv2EPUHTNalruwwfmhS+ScJwM4XqHTJY
-JkB16j/Xv2FTF+6KlbA1zdOVycPzoFKjAENYccQBVo2B+WQac7dFDqGEVNal9z66
-DyU4ciAHl6PsbuN7DWeuScLoqq5jwx61bZgn71mUOYC1/47ypat2BKCOXZ2JAjME
-EgEIAB0WIQSm5op4O95BdGcqQkHwXKpE5VGK/wUCWie53AAKCRDwXKpE5VGK/3rM
-D/9jcYKOjYaPJh3Q7wNC1HjjUa73eo5GvJqyXbsXufIh/RAYgQkD08P5JgzfXvQ0
-zOQTtDlDTVG8VMFoBYeMJVDd0k9LBbaljxcttMPfOll+AlQGAL7iQIqTAndknkJL
-CFdl0ypa5GVsl1tzqmNC5fuMJ3vBoRtYbMitlHQkO0vLjZ7yl9fz+7YkREpEo/d5
-Ya8t4+L6el6lrETYaiGCTxHcbYD7VdiJxpxFQlpgl+XKtobrj70RocGQ5JwUNilC
-nRJKUb33lbmntwDwQ1y1AjCnhB++3GHjJDXBPgYFDCSZPCndKeOXhxmB2psFf41i
-8foJPJXuh1vWOqArdwseFCRM6W2deF1utZmROMSkUo6IC8dYlucO/hjpjhG+C8Zv
-QiM5uLylD3IPMX9wCz1tAhMNs3v4pEPo/4A//1cdLkor9cQVLFj3+TkS888EWZdj
-Y8mUTIXU6yL1DXcj8CfDPS29fMpDorDpK1swl4pN5qgGfsL5BSAXUf1AZDWbxnEY
-xf5rakfHDzrfbtbTSSfrBxS8gdW2vBKM+3nL21BeP8hQ0tkLA7bn2fNGz3aCOw46
-XeVJdBk1gVTwazspylqrh1ljr0hQEN4gs/8kM645BRdD0IyAFFcI44VmuVwd8+2g
-5miAGmVKSqN77w2cgMRnF7xpUsanv+3zKzaTnG+2liTeCokCPgQTAQIAKAUCVL7V
-IAIbAwUJBaOagAYLCQgHAwIGFQgCCQoLBBYCAwECHgECF4AACgkQD8MELjRa0F1m
-RhAAj9X+/4iiQsN888dNW/H1wEFFTd/1vqb2j0sHP3t02LkEPN5Ii9u71TSD2gSD
-WTu1Eb46nRDcapFNv5M0vXcWrEt7PK9b51Kuj4KpP5IjJHpTl2g7umaYQWC8fqcY
-TJTH0guMSCzZlsP0xGLbAj3cG6X5OPzCO+IxEafXmE//SfS9w46n1OC57ca1Y0Fp
-WXfjA0sJrcozgNchsptu3jg/oEteYJoxDAzNO45O4geNONq5D9PUQPb+H5Vv5zpy
-MI7iUJhVnTOFvnoUgRS7v6pWiA3flh5FelK8tYPCzEfvxfe7EB5GO7MaJEO3ZLni
-COaAZ3Nfn6Tt28tCOgd052W4FeGWow7iYCS1Wgd30bq/FNgnl+tKv2woxmWt4jJv
-ioBHQ4PbUnap2RCmBFaG7llRkrKP8nhWSUdwSS3OmDwAfxTTXjPaESK9EX9OV9Xo
-or07thq+7OMs+2cyiy2jSfIau0SELy/tVioZBhoB7hzAJUB8sGHOxMPlVDFdUr3x
-F/cgCclWANhw2xvgPim1wQ0XpeZe6w9RpmjZR7ReMYwxn8APBDP/e9R5aLDUQAep
-2hrJUPK38D0L69RnpWQsR9hZ2hEOrMV2M6ChlvhwHbGSdJ2CcqG5Jx4ZAP23DK3A
-N26TB88H9F7IMrM0REZeu7KzvYwCWlpg0zMXXKQ/2vovoe2JAlUEEwECAD8CGwMG
-CwkIBwMCBhUIAgkKCwQWAgMBAh4BAheAFiEEtsj5goK5ROOw1cJTD8MELjRa0F0F
-Alpd+i0FCQ8FJo0ACgkQD8MELjRa0F3X3A//dBQLm6GmXlQFjxZbukTw0lZsevFR
-M/6ljZTxp7bsC+HFzYoaCKv6rikaWzytxk//SOaLKrB4Z9HjAlpBMtyLl2Hk7tcZ
-bPpFafNmQ+4KgWNjLXCvt9se8BGrQvGQUrbE6YowbXa2YIgxIVEncFzIECAsp/+N
-xbMcZN5/X1PJxKi/N22gP4nn47muN6L3pKez3CXgWnhGYSc7BuD5ALWYH7yMYUem
-d4jlXfu5xkBIqirj1arIYC9wmF4ldbLNDPuracc8LmXcSqa5Rpao0s4iVzAD+tkX
-vE/73m3rhepwBXxrfk0McXuI9aucf5h4/KkIBzZsaJ6JM1tzlrJzzjaBKJF9OI5T
-jA0qTxdGzdPztS8gPaPcMkRFfh9ti0ZDx4VeF3s8sOtmMRHeGEWfxqUAbBUbwFsa
-JDu/+8/VO4KijfcuUi8tqJ/JHeosCuGE7TM93LwJu6ZcqMYOPDROE/hsnGm0ZU92
-xedu+07/X1ESHkSFPoaSHD5/DCNa/tXIyJZ8X7gF3eoDP5mSmrJqIqsOBR9WOVYv
-dI8i0GHTXbrZj8WXdoS+N8wlyMLLbAS2jvTe7M5RoqbLz4ABOUUnLVoEE0CiccVZ
-bW75BPxOfaD0szbinAeX6HDPI7St0MbKrRPjuDXjD0JVkLqFINtZfYLGMLss4tgn
-suefr0Bo9ISwG3u5Ag0EVL7VIAEQAOxBxrQesChjrCqKjY5PnSsSYpeb4froucrC
-898AFw2DgN/Zz+W7wtSTbtz/GRcCurjzZvN7o2rCuNk0j0+s1sgZZm2BdldlabLy
-+UF/kSW1rb5qhfXcGGubu48OMdtSfok9lOc0Q1L4HNlGE4lUBkZzmI7Ykqfl+Bwr
-m9rpi54g4ua9PIiiHIAmMoZIcbtOG1KaDr6CoXRk/3g2ZiGUwhq3jFGroiBsKEap
-2FJ1bh5NJk2Eg8pV7fMOF7hUQKBZrNOtIPu8hA5WEgku3U3VYjRSI3SDi6QXnDL+
-xHxajiWpKtF3JjZh8y/CCTD8PyP34YjfZuFmkdske5cdx6H0V2UCiH453ncgFVdQ
-DXkY4n+0MTzhy2xu0IVVnBxYDYNhi+3MjTHJd9C4xMi9t+5IuEvDAPhgfZjDpQak
-EPz6hVmgj0mlKIgRilBRK9/kOxky9utBpGk3jEJGru/hKNloFNspoYtY6zATAr8E
-cOgoCFQE0nIktcg3wF9+OCEnV28/a7XZwUZ7Gl/qfOHtdr374wo8kd8R3V8d2G9q
-5w0/uCV9NNQ0fGWZDPDoYt6wnPL6gZv/nJM8oZY+u0rC24WwScZIniaryC4JHDas
-Ahr2S2CtgCvBgslK6f3gD16KHxPZMBpX73TzOYIhMEP/vXgVJbUD6dYht+U9c4Oh
-EDJown0dABEBAAGJAjwEGAECACYCGwwWIQS2yPmCgrlE47DVwlMPwwQuNFrQXQUC
-Wl36SwUJDwUmqwAKCRAPwwQuNFrQXT1/D/9YpRDNgaJl3YVDtVZoeQwh7BQ6ULZT
-eXFPogYkF2j3VWg8s9UmAs4sg/4a+9KLSantXjX+JFsRv0lQe5Gr/Vl8VQ4LKEXB
-fiGmSivjIZ7eopdd3YP2w6G5T3SA4d2CQfsg4rnJPnXIjzKNiSOi368ybnt9fL0Y
-2r2aqLTmP6Y7issDUO+J1TW1XHm349JPR0Hl4cTuNnWm4JuX2m2CJEc5XBlDAha9
-pUVs+J5C2D0UFFkyeOzeJPwy6x5ApWHm84n8AjhQSpu1qRKxKXdwei6tkQWWMHui
-+TgSY/zCkmD9/oY15Ei5avJ4WgIbTLJUoZMi70riPmU8ThjpzA7S+Nk0g7rMPq+X
-l1whjKU/u0udlsrIJjzkh6ftqKUmIkbxYTpjhnEujNrEr5m2S6Z6x3y9E5QagBMR
-dxRhfk+HbyACcP/p9rXOzl4M291DoKeAAH70GHniGxyNs9rAoMr/hD5XW/Wrz3dc
-KMc2s555E6MZILE2ZiolcRn+bYOMPZtWlbx98t8uqMf49gY4FGQBZAwPglMrx7mr
-m7HTIiXahThQGOJg6izJDAD5RwSEGlAcL28T8KAuM6CLLkhlBfQwiKsUBNnh9r8w
-V3lB+pV0GhL+3i077gTYfZBRwLzjFdhm9xUKEaZ6rN1BX9lzix4eSNK5nln0jUq1
-67H2IH//2sf8dw==
-=fTDu
------END PGP PUBLIC KEY BLOCK-----
\ No newline at end of file
deleted file mode 100644
--- a/automation/taskcluster/docker-hacl/Dockerfile
+++ /dev/null
@@ -1,31 +0,0 @@
-FROM ubuntu:xenial
-
-MAINTAINER Franziskus Kiefer <franziskuskiefer@gmail.com>
-# 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.05.0
-ENV haclversion 1442c015dab97cdf203ae238b1f3aeccf511bd1e
-
-# Install required packages and set versions
-ADD B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc /tmp/B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc
-ADD setup.sh /tmp/setup.sh
-RUN bash /tmp/setup.sh
-
-# Create user, add scripts.
-RUN useradd -ms /bin/bash worker
-WORKDIR /home/worker
-ADD bin /home/worker/bin
-RUN chmod +x /home/worker/bin/*
-USER worker
-
-# Build F*, HACL*, verify. Install a few more dependencies.
-ENV OPAMYES true
-ENV PATH "/home/worker/hacl-star/dependencies/z3/bin:$PATH"
-ADD setup-user.sh /tmp/setup-user.sh
-ADD license.txt /tmp/license.txt
-RUN bash /tmp/setup-user.sh
deleted file mode 100755
--- a/automation/taskcluster/docker-hacl/bin/checkout.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/usr/bin/env bash
-
-set -v -e -x
-
-if [ $(id -u) = 0 ]; then
-    # Drop privileges by re-running this script.
-    exec su worker $0
-fi
-
-# Default values for testing.
-REVISION=${NSS_HEAD_REVISION:-default}
-REPOSITORY=${NSS_HEAD_REPOSITORY:-https://hg.mozilla.org/projects/nss}
-
-# Clone NSS.
-for i in 0 2 5; do
-    sleep $i
-    hg clone -r $REVISION $REPOSITORY nss && exit 0
-    rm -rf nss
-done
-exit 1
deleted file mode 100644
--- a/automation/taskcluster/docker-hacl/license.txt
+++ /dev/null
@@ -1,15 +0,0 @@
-/* Copyright 2016-2017 INRIA and Microsoft Corporation
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- *     http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- */
-
deleted file mode 100644
--- a/automation/taskcluster/docker-hacl/setup-user.sh
+++ /dev/null
@@ -1,25 +0,0 @@
-#!/usr/bin/env bash
-
-set -v -e -x
-
-# Prepare build (OCaml packages)
-opam init
-echo ". /home/worker/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> .bashrc
-opam switch -v ${opamv}
-opam install ocamlfind batteries sqlite3 fileutils yojson ppx_deriving_yojson zarith pprint menhir ulex process fix wasm stdint
-
-# Get the HACL* code
-git clone ${haclrepo} hacl-star
-git -C hacl-star checkout ${haclversion}
-
-# Prepare submodules, and build, verify, test, and extract c code
-# This caches the extracted c code (pins the HACL* version). All we need to do
-# on CI now is comparing the code in this docker image with the one in NSS.
-opam config exec -- make -C hacl-star prepare -j$(nproc)
-make -C hacl-star -f Makefile.build snapshots/nss -j$(nproc)
-KOPTS="-funroll-loops 5" make -C hacl-star/code/curve25519 test -j$(nproc)
-make -C hacl-star/code/salsa-family test -j$(nproc)
-make -C hacl-star/code/poly1305 test -j$(nproc)
-
-# Cleanup.
-rm -rf ~/.ccache ~/.cache
deleted file mode 100644
--- a/automation/taskcluster/docker-hacl/setup.sh
+++ /dev/null
@@ -1,34 +0,0 @@
-#!/usr/bin/env bash
-
-set -v -e -x
-
-# Update packages.
-export DEBIAN_FRONTEND=noninteractive
-apt-get -qq update
-apt-get install --yes libssl-dev libsqlite3-dev g++-5 gcc-5 m4 make opam pkg-config python libgmp3-dev cmake curl libtool-bin autoconf wget locales
-update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 200
-update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 200
-
-# Get clang-format-3.9
-curl -LO https://releases.llvm.org/3.9.1/clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz
-curl -LO https://releases.llvm.org/3.9.1/clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz.sig
-
-# Verify the signature. The key used for verification was fetched via:
-#    gpg --keyserver pgp.key-server.io --recv-keys B6C8F98282B944E3B0D5C2530FC3042E345AD05D
-# Use a local copy to workaround bug 1565013.
-gpg --no-default-keyring --keyring tmp.keyring --import /tmp/B6C8F98282B944E3B0D5C2530FC3042E345AD05D.asc
-gpg --no-default-keyring --keyring tmp.keyring --verify clang+llvm-3.9.1-x86_64-linux-gnu-ubuntu-16.04.tar.xz.sig
-
-# Install into /usr/local/.
-tar xJvf *.tar.xz -C /usr/local --strip-components=1
-# Cleanup.
-rm *.tar.xz*
-
-locale-gen en_US.UTF-8
-dpkg-reconfigure locales
-
-# Cleanup.
-rm -rf ~/.ccache ~/.cache
-apt-get autoremove -y
-apt-get clean
-apt-get autoclean
--- a/automation/taskcluster/graph/src/extend.js
+++ b/automation/taskcluster/graph/src/extend.js
@@ -36,21 +36,16 @@ const FUZZ_IMAGE = {
 };
 
 // Bug 1488148 - temporary image for fuzzing 32-bit builds.
 const FUZZ_IMAGE_32 = {
   name: "fuzz32",
   path: "automation/taskcluster/docker-fuzz32"
 };
 
-const HACL_GEN_IMAGE = {
-  name: "hacl",
-  path: "automation/taskcluster/docker-hacl"
-};
-
 const SAW_IMAGE = {
   name: "saw",
   path: "automation/taskcluster/docker-saw"
 };
 
 const WINDOWS_CHECKOUT_CMD =
   "bash -c \"hg clone -r $NSS_HEAD_REVISION $NSS_HEAD_REPOSITORY nss || " +
     "(sleep 2; hg clone -r $NSS_HEAD_REVISION $NSS_HEAD_REPOSITORY nss) || " +
@@ -1021,16 +1016,20 @@ function scheduleTests(task_build, task_
   }));
   queue.scheduleTask(merge(cert_base_long, {
     name: "Cipher tests", symbol: "NoSSSE3|NEON", tests: "cipher",
     env: {
       NSS_DISABLE_ARM_NEON: "1",
       NSS_DISABLE_SSSE3: "1"
     }, group: "Cipher"
   }));
+  queue.scheduleTask(merge(cert_base_long, {
+    name: "Cipher tests", symbol: "NoSSE4.1", tests: "cipher",
+    env: {NSS_DISABLE_SSE4_1: "1"}, group: "Cipher"
+  }));
   queue.scheduleTask(merge(cert_base, {
     name: "EC tests", symbol: "EC", tests: "ec"
   }));
   queue.scheduleTask(merge(cert_base, {
     name: "Lowhash tests", symbol: "Lowhash", tests: "lowhash"
   }));
   queue.scheduleTask(merge(cert_base, {
     name: "SDR tests", symbol: "SDR", tests: "sdr"
@@ -1149,17 +1148,17 @@ async function scheduleTools() {
       "-c",
       "bin/checkout.sh && nss/automation/taskcluster/scripts/run_coverity.sh"
     ]
   }));
 
   queue.scheduleTask(merge(base, {
     symbol: "hacl",
     name: "hacl",
-    image: HACL_GEN_IMAGE,
+    image: LINUX_BUILDS_IMAGE,
     command: [
       "/bin/bash",
       "-c",
       "bin/checkout.sh && nss/automation/taskcluster/scripts/run_hacl.sh"
     ]
   }));
 
   let task_saw = queue.scheduleTask(merge(base, {
@@ -1195,28 +1194,32 @@ async function scheduleTools() {
     image: SAW_IMAGE,
     command: [
       "/bin/bash",
       "-c",
       "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh bmul"
     ]
   }));
 
-  queue.scheduleTask(merge(base, {
-    parent: task_saw,
-    symbol: "ChaCha20",
-    group: "SAW",
-    name: "chacha20.saw",
-    image: SAW_IMAGE,
-    command: [
-      "/bin/bash",
-      "-c",
-      "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh chacha20"
-    ]
-  }));
+  // TODO: The ChaCha20 saw verification is currently disabled because the new
+  //       HACL 32-bit code can't be verified by saw right now to the best of
+  //       my knowledge.
+  //       Bug 1604130
+  // queue.scheduleTask(merge(base, {
+  //   parent: task_saw,
+  //   symbol: "ChaCha20",
+  //   group: "SAW",
+  //   name: "chacha20.saw",
+  //   image: SAW_IMAGE,
+  //   command: [
+  //     "/bin/bash",
+  //     "-c",
+  //     "bin/checkout.sh && nss/automation/taskcluster/scripts/run_saw.sh chacha20"
+  //   ]
+  // }));
 
   queue.scheduleTask(merge(base, {
     parent: task_saw,
     symbol: "Poly1305",
     group: "SAW",
     name: "poly1305.saw",
     image: SAW_IMAGE,
     command: [
--- a/automation/taskcluster/scripts/run_hacl.sh
+++ b/automation/taskcluster/scripts/run_hacl.sh
@@ -3,38 +3,30 @@
 if [[ $(id -u) -eq 0 ]]; then
     # Drop privileges by re-running this script.
     # Note: this mangles arguments, better to avoid running scripts as root.
     exec su worker -c "$0 $*"
 fi
 
 set -e -x -v
 
-# The docker image this is running in has the HACL* and NSS sources.
-# The extracted C code from HACL* is already generated and the HACL* tests were
-# successfully executed.
-
-# Verify HACL*. Taskcluster fails when we do this in the image build.
-make -C hacl-star verify-nss -j$(nproc)
+# The docker image this is running in has NSS sources.
+# Get the HACL* source, containing a snapshot of the C code, extracted on the
+# HACL CI.
+# When bug 1593647 is resolved, extract the code on CI again.
+git clone -q "https://github.com/project-everest/hacl-star" ~/hacl-star
+git -C ~/hacl-star checkout -q 186a985597d57e3b587ceb0ef6deb0b5de706ae2
 
-# Add license header to specs
-spec_files=($(find ~/hacl-star/specs -type f -name '*.fst'))
-for f in "${spec_files[@]}"; do
-    cat /tmp/license.txt "$f" > /tmp/tmpfile && mv /tmp/tmpfile "$f"
-done
-
-# Format the extracted C code.
-cd ~/hacl-star/snapshots/nss
+# Format the C snapshot.
+cd ~/hacl-star/dist/mozilla
+cp ~/nss/.clang-format .
+find . -type f -name '*.[ch]' -exec clang-format -i {} \+
+cd ~/hacl-star/dist/kremlin
 cp ~/nss/.clang-format .
 find . -type f -name '*.[ch]' -exec clang-format -i {} \+
 
 # These diff commands will return 1 if there are differences and stop the script.
 files=($(find ~/nss/lib/freebl/verified/ -type f -name '*.[ch]'))
 for f in "${files[@]}"; do
-    diff $f $(basename "$f")
+    file_name=$(basename "$f")
+    hacl_file=($(find ~/hacl-star/dist/mozilla/ ~/hacl-star/dist/kremlin/ -type f -name $file_name))
+    diff $hacl_file $f
 done
-
-# Check that the specs didn't change either.
-cd ~/hacl-star/specs
-files=($(find ~/nss/lib/freebl/verified/specs -type f))
-for f in "${files[@]}"; do
-    diff $f $(basename "$f")
-done
--- a/gtests/pk11_gtest/pk11_chacha20poly1305_unittest.cc
+++ b/gtests/pk11_gtest/pk11_chacha20poly1305_unittest.cc
@@ -69,16 +69,17 @@ class Pkcs11ChaCha20Poly1305Test
     }
 
     EXPECT_EQ(rv, SECSuccess);
     EXPECT_EQ(encrypted.size(), static_cast<size_t>(encrypted_len));
 
     // Check ciphertext and tag.
     if (ct) {
       ASSERT_EQ(ct_len, encrypted_len);
+      EXPECT_TRUE(!memcmp(ct, encrypted.data(), encrypted.size() - 16));
       EXPECT_TRUE(!memcmp(ct, encrypted.data(), encrypted.size()) !=
                   invalid_tag);
     }
 
     // Get the *estimated* plaintext length. This value should
     // never be zero as it could lead to a NULL outPtr being
     // passed to a subsequent decryption call (for AEAD we
     // must authenticate even when the pt is zero-length).
--- a/lib/freebl/Makefile
+++ b/lib/freebl/Makefile
@@ -530,52 +530,36 @@ ifneq ($(shell $(CC) -? 2>&1 >/dev/null 
             HAVE_INT128_SUPPORT = 1
             DEFINES += -DHAVE_INT128_SUPPORT
         endif
     endif
 endif # lcc
 endif # USE_64
 
 ifndef HAVE_INT128_SUPPORT
-    DEFINES += -DKRML_NOUINT128
+    DEFINES += -DKRML_VERIFIED_UINT128
 endif
 
 ifndef NSS_DISABLE_CHACHAPOLY
     ifeq ($(CPU_ARCH),x86_64)
-        ifdef HAVE_INT128_SUPPORT
-            EXTRA_SRCS += Hacl_Poly1305_64.c
-        else
-            EXTRA_SRCS += Hacl_Poly1305_32.c
-        endif
-    else
-        ifeq ($(CPU_ARCH),aarch64)
-            EXTRA_SRCS += Hacl_Poly1305_64.c
-        else
-            EXTRA_SRCS += Hacl_Poly1305_32.c
-        endif
+        EXTRA_SRCS += Hacl_Poly1305_128.c Hacl_Chacha20_Vec128.c Hacl_Chacha20Poly1305_128.c
     endif # x86_64
 
-    VERIFIED_SRCS += Hacl_Chacha20.c
-    VERIFIED_SRCS += Hacl_Chacha20_Vec128.c
+    VERIFIED_SRCS += Hacl_Poly1305_32.c Hacl_Chacha20.c Hacl_Chacha20Poly1305_32.c
 endif # NSS_DISABLE_CHACHAPOLY
 
-ifeq (,$(filter-out i386 x386 x86 x86_64 aarch64,$(CPU_ARCH)))
-    # All intel architectures get the 64 bit version
-    # With custom uint128 if necessary (faster than generic 32 bit version).
+ifeq (,$(filter-out x86_64 aarch64,$(CPU_ARCH)))
+    # All 64-bit architectures get the 64 bit version.
     ECL_SRCS += curve25519_64.c
-    VERIFIED_SRCS += Hacl_Curve25519.c
+    VERIFIED_SRCS += Hacl_Curve25519_51.c
 else
-    # All non intel architectures get the generic 32 bit implementation (slow!)
+    # All other architectures get the generic 32 bit implementation
     ECL_SRCS += curve25519_32.c
 endif
 
-ifndef HAVE_INT128_SUPPORT
-    VERIFIED_SRCS += FStar.c
-endif
-
 #######################################################################
 # (5) Execute "global" rules. (OPTIONAL)                              #
 #######################################################################
 
 include $(CORE_DEPTH)/coreconf/rules.mk
 
 #######################################################################
 # (6) Execute "component" rules. (OPTIONAL)                           #
@@ -594,17 +578,17 @@ rijndael_tables:
 	         $(DEFINES) $(INCLUDES) $(OBJDIR)/libfreebl.a
 	$(OBJDIR)/make_rijndael_tab
 
 vpath %.h mpi ecl verified
 vpath %.c mpi ecl verified
 vpath %.S mpi ecl
 vpath %.s mpi ecl
 vpath %.asm mpi ecl
-INCLUDES += -Impi -Iecl -Iverified
+INCLUDES += -Impi -Iecl -Iverified -Iverified/kremlin/include -Iverified/kremlin/kremlib/dist/minimal
 
 
 DEFINES += -DMP_API_COMPATIBLE
 
 MPI_USERS = dh.c pqg.c dsa.c rsa.c ec.c
 
 MPI_OBJS = $(addprefix $(OBJDIR)/$(PROG_PREFIX), $(MPI_SRCS:.c=$(OBJ_SUFFIX)))
 MPI_OBJS += $(addprefix $(OBJDIR)/$(PROG_PREFIX), $(MPI_USERS:.c=$(OBJ_SUFFIX)))
@@ -787,8 +771,12 @@ endif
 ifeq ($(CPU_ARCH),aarch64)
 $(OBJDIR)/$(PROG_PREFIX)aes-armv8$(OBJ_SUFFIX): CFLAGS += -march=armv8-a+crypto
 $(OBJDIR)/$(PROG_PREFIX)gcm-aarch64$(OBJ_SUFFIX): CFLAGS += -march=armv8-a+crypto
 endif
 
 ifeq ($(CPU_ARCH),ppc)
 $(OBJDIR)/$(PROG_PREFIX)gcm-ppc$(OBJ_SUFFIX): CFLAGS += -mcrypto -maltivec
 endif
+
+$(OBJDIR)/$(PROG_PREFIX)Hacl_Chacha20_Vec128$(OBJ_SUFFIX): CFLAGS += -mssse3 -msse4 -mavx -maes 
+$(OBJDIR)/$(PROG_PREFIX)Hacl_Chacha20Poly1305_128$(OBJ_SUFFIX): CFLAGS += -mssse3 -msse4 -mavx -maes 
+$(OBJDIR)/$(PROG_PREFIX)Hacl_Poly1305_128$(OBJ_SUFFIX): CFLAGS += -mssse3 -msse4 -mavx -maes -mpclmul
--- a/lib/freebl/blapii.h
+++ b/lib/freebl/blapii.h
@@ -76,16 +76,18 @@ SEC_END_PROTOS
 SECStatus RSA_Init();
 SECStatus generate_prime(mp_int *prime, int primeLen);
 
 /* Freebl state. */
 PRBool aesni_support();
 PRBool clmul_support();
 PRBool avx_support();
 PRBool ssse3_support();
+PRBool sse4_1_support();
+PRBool sse4_2_support();
 PRBool arm_neon_support();
 PRBool arm_aes_support();
 PRBool arm_pmull_support();
 PRBool arm_sha1_support();
 PRBool arm_sha2_support();
 PRBool ppc_crypto_support();
 
 #endif /* _BLAPII_H_ */
--- a/lib/freebl/blinit.c
+++ b/lib/freebl/blinit.c
@@ -19,16 +19,18 @@
 
 static PRCallOnceType coFreeblInit;
 
 /* State variables. */
 static PRBool aesni_support_ = PR_FALSE;
 static PRBool clmul_support_ = PR_FALSE;
 static PRBool avx_support_ = PR_FALSE;
 static PRBool ssse3_support_ = PR_FALSE;
+static PRBool sse4_1_support_ = PR_FALSE;
+static PRBool sse4_2_support_ = PR_FALSE;
 static PRBool arm_neon_support_ = PR_FALSE;
 static PRBool arm_aes_support_ = PR_FALSE;
 static PRBool arm_sha1_support_ = PR_FALSE;
 static PRBool arm_sha2_support_ = PR_FALSE;
 static PRBool arm_pmull_support_ = PR_FALSE;
 static PRBool ppc_crypto_support_ = PR_FALSE;
 
 #ifdef NSS_X86_OR_X64
@@ -65,35 +67,43 @@ check_xcr0_ymm()
 }
 
 #define ECX_AESNI (1 << 25)
 #define ECX_CLMUL (1 << 1)
 #define ECX_XSAVE (1 << 26)
 #define ECX_OSXSAVE (1 << 27)
 #define ECX_AVX (1 << 28)
 #define ECX_SSSE3 (1 << 9)
+#define ECX_SSE4_1 (1 << 19)
+#define ECX_SSE4_2 (1 << 20)
 #define AVX_BITS (ECX_XSAVE | ECX_OSXSAVE | ECX_AVX)
 
 void
 CheckX86CPUSupport()
 {
     unsigned long eax, ebx, ecx, edx;
     char *disable_hw_aes = PR_GetEnvSecure("NSS_DISABLE_HW_AES");
     char *disable_pclmul = PR_GetEnvSecure("NSS_DISABLE_PCLMUL");
     char *disable_avx = PR_GetEnvSecure("NSS_DISABLE_AVX");
     char *disable_ssse3 = PR_GetEnvSecure("NSS_DISABLE_SSSE3");
+    char *disable_sse4_1 = PR_GetEnvSecure("NSS_DISABLE_SSE4_1");
+    char *disable_sse4_2 = PR_GetEnvSecure("NSS_DISABLE_SSE4_2");
     freebl_cpuid(1, &eax, &ebx, &ecx, &edx);
     aesni_support_ = (PRBool)((ecx & ECX_AESNI) != 0 && disable_hw_aes == NULL);
     clmul_support_ = (PRBool)((ecx & ECX_CLMUL) != 0 && disable_pclmul == NULL);
     /* For AVX we check AVX, OSXSAVE, and XSAVE
      * as well as XMM and YMM state. */
     avx_support_ = (PRBool)((ecx & AVX_BITS) == AVX_BITS) && check_xcr0_ymm() &&
                    disable_avx == NULL;
     ssse3_support_ = (PRBool)((ecx & ECX_SSSE3) != 0 &&
                               disable_ssse3 == NULL);
+    sse4_1_support_ = (PRBool)((ecx & ECX_SSE4_1) != 0 &&
+                               disable_sse4_1 == NULL);
+    sse4_2_support_ = (PRBool)((ecx & ECX_SSE4_2) != 0 &&
+                               disable_sse4_2 == NULL);
 }
 #endif /* NSS_X86_OR_X64 */
 
 /* clang-format off */
 #if defined(__aarch64__) || defined(__arm__)
 #ifndef __has_include
 #define __has_include(x) 0
 #endif
@@ -320,16 +330,26 @@ avx_support()
     return avx_support_;
 }
 PRBool
 ssse3_support()
 {
     return ssse3_support_;
 }
 PRBool
+sse4_1_support()
+{
+    return sse4_1_support_;
+}
+PRBool
+sse4_2_support()
+{
+    return sse4_2_support_;
+}
+PRBool
 arm_neon_support()
 {
     return arm_neon_support_;
 }
 PRBool
 arm_aes_support()
 {
     return arm_aes_support_;
--- a/lib/freebl/chacha20poly1305.c
+++ b/lib/freebl/chacha20poly1305.c
@@ -8,101 +8,50 @@
 
 #include <string.h>
 #include <stdio.h>
 
 #include "seccomon.h"
 #include "secerr.h"
 #include "blapit.h"
 #include "blapii.h"
-
-#ifndef NSS_DISABLE_CHACHAPOLY
 #include "chacha20poly1305.h"
-// Forward declaration from "Hacl_Chacha20_Vec128.h".
-extern void Hacl_Chacha20_Vec128_chacha20(uint8_t *output, uint8_t *plain,
-                                          uint32_t len, uint8_t *k, uint8_t *n1,
-                                          uint32_t ctr);
-// Forward declaration from "Hacl_Chacha20.h".
-extern void Hacl_Chacha20_chacha20(uint8_t *output, uint8_t *plain, uint32_t len,
-                                   uint8_t *k, uint8_t *n1, uint32_t ctr);
 
-#if defined(HAVE_INT128_SUPPORT) && (defined(NSS_X86_OR_X64) || defined(__aarch64__))
-/* Use HACL* Poly1305 on 64-bit Intel and ARM */
-#include "verified/Hacl_Poly1305_64.h"
-#define NSS_POLY1305_64 1
-#define Hacl_Poly1305_update Hacl_Poly1305_64_update
-#define Hacl_Poly1305_mk_state Hacl_Poly1305_64_mk_state
-#define Hacl_Poly1305_init Hacl_Poly1305_64_init
-#define Hacl_Poly1305_finish Hacl_Poly1305_64_finish
-typedef Hacl_Impl_Poly1305_64_State_poly1305_state Hacl_Impl_Poly1305_State_poly1305_state;
-#else
-/* All other platforms get the 32-bit poly1305 HACL* implementation. */
-#include "verified/Hacl_Poly1305_32.h"
-#define NSS_POLY1305_32 1
-#define Hacl_Poly1305_update Hacl_Poly1305_32_update
-#define Hacl_Poly1305_mk_state Hacl_Poly1305_32_mk_state
-#define Hacl_Poly1305_init Hacl_Poly1305_32_init
-#define Hacl_Poly1305_finish Hacl_Poly1305_32_finish
-typedef Hacl_Impl_Poly1305_32_State_poly1305_state Hacl_Impl_Poly1305_State_poly1305_state;
-#endif /* HAVE_INT128_SUPPORT */
+// There are two implementations of ChaCha20Poly1305:
+// 1) 128-bit with hardware acceleration used on x64
+// 2) 32-bit used on all other platforms
+// Instead of including the headers (they bring other things we don't want),
+// we declare the functions here.
+// Usage is guarded by runtime checks of required hardware features.
 
-static void
-Poly1305PadUpdate(Hacl_Impl_Poly1305_State_poly1305_state state,
-                  unsigned char *block, const unsigned char *p,
-                  const unsigned int pLen)
-{
-    unsigned int pRemLen = pLen % 16;
-    Hacl_Poly1305_update(state, (uint8_t *)p, (pLen / 16));
-    if (pRemLen > 0) {
-        memcpy(block, p + (pLen - pRemLen), pRemLen);
-        Hacl_Poly1305_update(state, block, 1);
-    }
-}
+// Forward declaration from Hacl_Chacha20_Vec128.h and Hacl_Chacha20Poly1305_128.h.
+extern void Hacl_Chacha20_Vec128_chacha20_encrypt_128(uint32_t len, uint8_t *out,
+                                                      uint8_t *text, uint8_t *key,
+                                                      uint8_t *n1, uint32_t ctr);
+extern void
+Hacl_Chacha20Poly1305_128_aead_encrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
+                                       uint8_t *aad, uint32_t mlen, uint8_t *m,
+                                       uint8_t *cipher, uint8_t *mac);
+extern uint32_t
+Hacl_Chacha20Poly1305_128_aead_decrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
+                                       uint8_t *aad, uint32_t mlen, uint8_t *m,
+                                       uint8_t *cipher, uint8_t *mac);
 
-/* Poly1305Do writes the Poly1305 authenticator of the given additional data
- * and ciphertext to |out|. */
-static void
-Poly1305Do(unsigned char *out, const unsigned char *ad, unsigned int adLen,
-           const unsigned char *ciphertext, unsigned int ciphertextLen,
-           const unsigned char key[32])
-{
-#ifdef NSS_POLY1305_64
-    uint64_t stateStack[6U] = { 0U };
-    size_t offset = 3;
-#elif defined NSS_POLY1305_32
-    uint32_t stateStack[10U] = { 0U };
-    size_t offset = 5;
-#else
-#error "This can't happen."
-#endif
-    Hacl_Impl_Poly1305_State_poly1305_state state =
-        Hacl_Poly1305_mk_state(stateStack, stateStack + offset);
-
-    unsigned char block[16] = { 0 };
-    Hacl_Poly1305_init(state, (uint8_t *)key);
-
-    Poly1305PadUpdate(state, block, ad, adLen);
-    memset(block, 0, 16);
-    Poly1305PadUpdate(state, block, ciphertext, ciphertextLen);
-
-    unsigned int i;
-    unsigned int j;
-    for (i = 0, j = adLen; i < 8; i++, j >>= 8) {
-        block[i] = j;
-    }
-    for (i = 8, j = ciphertextLen; i < 16; i++, j >>= 8) {
-        block[i] = j;
-    }
-
-    Hacl_Poly1305_update(state, block, 1);
-    Hacl_Poly1305_finish(state, out, (uint8_t *)(key + 16));
-#undef NSS_POLY1305_64
-#undef NSS_POLY1305_32
-}
-#endif /* NSS_DISABLE_CHACHAPOLY */
+// Forward declaration from Hacl_Chacha20.h and Hacl_Chacha20Poly1305_32.h.
+extern void Hacl_Chacha20_chacha20_encrypt(uint32_t len, uint8_t *out,
+                                           uint8_t *text, uint8_t *key,
+                                           uint8_t *n1, uint32_t ctr);
+extern void
+Hacl_Chacha20Poly1305_32_aead_encrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
+                                      uint8_t *aad, uint32_t mlen, uint8_t *m,
+                                      uint8_t *cipher, uint8_t *mac);
+extern uint32_t
+Hacl_Chacha20Poly1305_32_aead_decrypt(uint8_t *k, uint8_t *n1, uint32_t aadlen,
+                                      uint8_t *aad, uint32_t mlen, uint8_t *m,
+                                      uint8_t *cipher, uint8_t *mac);
 
 SECStatus
 ChaCha20Poly1305_InitContext(ChaCha20Poly1305Context *ctx,
                              const unsigned char *key, unsigned int keyLen,
                              unsigned int tagLen)
 {
 #ifdef NSS_DISABLE_CHACHAPOLY
     return SECFailure;
@@ -157,20 +106,23 @@ ChaCha20Poly1305_DestroyContext(ChaCha20
 #endif
 }
 
 #ifndef NSS_DISABLE_CHACHAPOLY
 void
 ChaCha20Xor(uint8_t *output, uint8_t *block, uint32_t len, uint8_t *k,
             uint8_t *nonce, uint32_t ctr)
 {
-    if (ssse3_support() || arm_neon_support()) {
-        Hacl_Chacha20_Vec128_chacha20(output, block, len, k, nonce, ctr);
-    } else {
-        Hacl_Chacha20_chacha20(output, block, len, k, nonce, ctr);
+#ifdef NSS_X64
+    if (ssse3_support() && sse4_1_support()) {
+        Hacl_Chacha20_Vec128_chacha20_encrypt_128(len, output, block, k, nonce, ctr);
+    } else
+#endif
+    {
+        Hacl_Chacha20_chacha20_encrypt(len, output, block, k, nonce, ctr);
     }
 }
 #endif /* NSS_DISABLE_CHACHAPOLY */
 
 SECStatus
 ChaCha20_Xor(unsigned char *output, const unsigned char *block, unsigned int len,
              const unsigned char *k, const unsigned char *nonce, PRUint32 ctr)
 {
@@ -193,61 +145,59 @@ ChaCha20Poly1305_Seal(const ChaCha20Poly
                       unsigned int *outputLen, unsigned int maxOutputLen,
                       const unsigned char *input, unsigned int inputLen,
                       const unsigned char *nonce, unsigned int nonceLen,
                       const unsigned char *ad, unsigned int adLen)
 {
 #ifdef NSS_DISABLE_CHACHAPOLY
     return SECFailure;
 #else
-    unsigned char block[64];
-    unsigned char tag[16];
 
     if (nonceLen != 12) {
         PORT_SetError(SEC_ERROR_INPUT_LEN);
         return SECFailure;
     }
     // ChaCha has a 64 octet block, with a 32-bit block counter.
     if (sizeof(inputLen) > 4 && inputLen >= (1ULL << (6 + 32))) {
         PORT_SetError(SEC_ERROR_INPUT_LEN);
         return SECFailure;
     }
     if (maxOutputLen < inputLen + ctx->tagLen) {
         PORT_SetError(SEC_ERROR_OUTPUT_LEN);
         return SECFailure;
     }
 
-    PORT_Memset(block, 0, sizeof(block));
-    // Generate a block of keystream. The first 32 bytes will be the poly1305
-    // key. The remainder of the block is discarded.
-    ChaCha20Xor(block, (uint8_t *)block, sizeof(block), (uint8_t *)ctx->key,
-                (uint8_t *)nonce, 0);
-    ChaCha20Xor(output, (uint8_t *)input, inputLen, (uint8_t *)ctx->key,
-                (uint8_t *)nonce, 1);
-
-    Poly1305Do(tag, ad, adLen, output, inputLen, block);
-    PORT_Memcpy(output + inputLen, tag, ctx->tagLen);
+#ifdef NSS_X64
+    if (ssse3_support() && sse4_1_support()) {
+        Hacl_Chacha20Poly1305_128_aead_encrypt(
+            (uint8_t *)ctx->key, (uint8_t *)nonce, adLen, (uint8_t *)ad, inputLen,
+            (uint8_t *)input, output, output + inputLen);
+    } else
+#endif
+    {
+        Hacl_Chacha20Poly1305_32_aead_encrypt(
+            (uint8_t *)ctx->key, (uint8_t *)nonce, adLen, (uint8_t *)ad, inputLen,
+            (uint8_t *)input, output, output + inputLen);
+    }
 
     *outputLen = inputLen + ctx->tagLen;
     return SECSuccess;
 #endif
 }
 
 SECStatus
 ChaCha20Poly1305_Open(const ChaCha20Poly1305Context *ctx, unsigned char *output,
                       unsigned int *outputLen, unsigned int maxOutputLen,
                       const unsigned char *input, unsigned int inputLen,
                       const unsigned char *nonce, unsigned int nonceLen,
                       const unsigned char *ad, unsigned int adLen)
 {
 #ifdef NSS_DISABLE_CHACHAPOLY
     return SECFailure;
 #else
-    unsigned char block[64];
-    unsigned char tag[16];
     unsigned int ciphertextLen;
 
     if (nonceLen != 12) {
         PORT_SetError(SEC_ERROR_INPUT_LEN);
         return SECFailure;
     }
     if (inputLen < ctx->tagLen) {
         PORT_SetError(SEC_ERROR_INPUT_LEN);
@@ -259,26 +209,31 @@ ChaCha20Poly1305_Open(const ChaCha20Poly
         return SECFailure;
     }
     // ChaCha has a 64 octet block, with a 32-bit block counter.
     if (inputLen >= (1ULL << (6 + 32)) + ctx->tagLen) {
         PORT_SetError(SEC_ERROR_INPUT_LEN);
         return SECFailure;
     }
 
-    PORT_Memset(block, 0, sizeof(block));
-    // Generate a block of keystream. The first 32 bytes will be the poly1305
-    // key. The remainder of the block is discarded.
-    ChaCha20Xor(block, (uint8_t *)block, sizeof(block), (uint8_t *)ctx->key,
-                (uint8_t *)nonce, 0);
-    Poly1305Do(tag, ad, adLen, input, ciphertextLen, block);
-    if (NSS_SecureMemcmp(tag, &input[ciphertextLen], ctx->tagLen) != 0) {
+    uint32_t res = 1;
+#ifdef NSS_X64
+    if (ssse3_support() && sse4_1_support()) {
+        res = Hacl_Chacha20Poly1305_128_aead_decrypt(
+            (uint8_t *)ctx->key, (uint8_t *)nonce, adLen, (uint8_t *)ad, ciphertextLen,
+            (uint8_t *)output, (uint8_t *)input, (uint8_t *)input + ciphertextLen);
+    } else
+#endif
+    {
+        res = Hacl_Chacha20Poly1305_32_aead_decrypt(
+            (uint8_t *)ctx->key, (uint8_t *)nonce, adLen, (uint8_t *)ad, ciphertextLen,
+            (uint8_t *)output, (uint8_t *)input, (uint8_t *)input + ciphertextLen);
+    }
+
+    if (res) {
         PORT_SetError(SEC_ERROR_BAD_DATA);
         return SECFailure;
     }
 
-    ChaCha20Xor(output, (uint8_t *)input, ciphertextLen, (uint8_t *)ctx->key,
-                (uint8_t *)nonce, 1);
-
     *outputLen = ciphertextLen;
     return SECSuccess;
 #endif
 }
--- a/lib/freebl/det_rng.c
+++ b/lib/freebl/det_rng.c
@@ -94,17 +94,18 @@ RNG_GenerateGlobalRandomBytes(void *dest
     if (!cx) {
         PORT_SetError(SEC_ERROR_NO_MEMORY);
         PZ_Unlock(rng_lock);
         return SECFailure;
     }
 
     memset(dest, 0, len);
     memcpy(dest, globalBytes, PR_MIN(len, GLOBAL_BYTES_SIZE));
-    Hacl_Chacha20_chacha20(dest, (uint8_t *)dest, len, (uint8_t *)key, nonce, 0);
+    Hacl_Chacha20_chacha20_encrypt(len, (uint8_t *)dest, (uint8_t *)dest,
+                                   (uint8_t *)key, nonce, 0);
     ChaCha20Poly1305_DestroyContext(cx, PR_TRUE);
 
     PZ_Unlock(rng_lock);
     /* --- UNLOCKED --- */
 
     return SECSuccess;
 }
 
--- a/lib/freebl/ecl/curve25519_64.c
+++ b/lib/freebl/ecl/curve25519_64.c
@@ -1,14 +1,14 @@
 /* This Source Code Form is subject to the terms of the Mozilla Public
  * License, v. 2.0. If a copy of the MPL was not distributed with this
  * file, You can obtain one at http://mozilla.org/MPL/2.0/. */
 
 #include "ecl-priv.h"
-#include "../verified/Hacl_Curve25519.h"
+#include "../verified/Hacl_Curve25519_51.h"
 
 SECStatus
 ec_Curve25519_mul(uint8_t *mypublic, const uint8_t *secret, const uint8_t *basepoint)
 {
     // Note: this cast is safe because HaCl* state has a post-condition that only "mypublic" changed.
-    Hacl_Curve25519_crypto_scalarmult(mypublic, (uint8_t *)secret, (uint8_t *)basepoint);
+    Hacl_Curve25519_51_ecdh(mypublic, (uint8_t *)secret, (uint8_t *)basepoint);
     return 0;
 }
--- a/lib/freebl/freebl.gyp
+++ b/lib/freebl/freebl.gyp
@@ -52,42 +52,74 @@
       'cflags_mozilla': [
         '-mssse3'
       ],
     },
     {
       # TODO: make this so that all hardware accelerated code is in here.
       'target_name': 'hw-acc-crypto',
       'type': 'static_library',
-      'sources': [
-        'verified/Hacl_Chacha20_Vec128.c',
-      ],
+      # 'sources': [
+      #   All hardware accelerated crypto currently requires x64
+      # ],
       'dependencies': [
         '<(DEPTH)/exports.gyp:nss_exports'
       ],
       'conditions': [
-        [ 'target_arch=="ia32" or target_arch=="x64"', {
+        [ 'target_arch=="x64"', {
           'cflags': [
-            '-mssse3'
+            '-mssse3',
+            '-msse4'
           ],
           'cflags_mozilla': [
-            '-mssse3'
+            '-mssse3',
+            '-msse4',
+            '-mpclmul',
+            '-maes',
+            '-mavx',
           ],
           # GCC doesn't define this.
           'defines': [
             '__SSSE3__',
           ],
         }],
+        [ 'OS=="linux" or OS=="android" or OS=="dragonfly" or OS=="freebsd" or \
+           OS=="netbsd" or OS=="openbsd"', {
+          'cflags': [
+            '-mpclmul',
+            '-maes',
+            '-mavx',
+          ],
+        }],
+        # macOS build doesn't use cflags.
+        [ 'OS=="mac" or OS=="ios"', {
+          'xcode_settings': {
+            'OTHER_CFLAGS': [
+              '-mssse3',
+              '-msse4',
+              '-mpclmul',
+              '-maes',
+              '-mavx',
+            ],
+          },
+        }],
         [ 'target_arch=="arm"', {
           # Gecko doesn't support non-NEON platform on Android, but tier-3
           # platform such as Linux/arm will need it
           'cflags_mozilla': [
             '-mfpu=neon'
           ],
         }],
+        [ 'target_arch=="x64"', {
+          'sources': [
+            'verified/Hacl_Poly1305_128.c',
+            'verified/Hacl_Chacha20_Vec128.c',
+            'verified/Hacl_Chacha20Poly1305_128.c',
+          ],
+        }],
       ],
     },
     {
       'target_name': 'gcm-aes-x86_c_lib',
       'type': 'static_library',
       'sources': [
         'gcm-x86.c', 'aes-x86.c'
       ],
@@ -400,16 +432,18 @@
       ],
     }],
   ],
   'target_defaults': {
     'include_dirs': [
       'mpi',
       'ecl',
       'verified',
+      'verified/kremlin/include',
+      'verified/kremlin/kremlib/dist/minimal',
     ],
     'defines': [
       'SHLIB_SUFFIX=\"<(dll_suffix)\"',
       'SHLIB_PREFIX=\"<(dll_prefix)\"',
       'SHLIB_VERSION=\"3\"',
       'SOFTOKEN_SHLIB_VERSION=\"3\"',
       'RIJNDAEL_INCLUDE_TABLES',
       'MP_API_COMPATIBLE'
@@ -456,17 +490,17 @@
       }],
       [ 'have_int128_support==1', {
         'defines': [
           # The Makefile does version-tests on GCC, but we're not doing that here.
           'HAVE_INT128_SUPPORT',
         ],
       }, {
         'defines': [
-          'KRML_NOUINT128',
+          'KRML_VERIFIED_UINT128',
         ],
       }],
       [ 'OS=="linux"', {
         'defines': [
           'FREEBL_LOWHASH',
           'FREEBL_NO_DEPEND',
         ],
       }],
--- a/lib/freebl/freebl_base.gypi
+++ b/lib/freebl/freebl_base.gypi
@@ -128,64 +128,37 @@
         [ 'cc_is_clang!=1', {
           # MSVC
           'sources': [
             'intel-gcm-wrap.c',
           ],
         }],
       ],
     }],
-    ['target_arch=="ia32" or target_arch=="x64" or target_arch=="arm64" or target_arch=="aarch64"', {
+    ['have_int128_support==1 and \
+      (target_arch=="x64" or target_arch=="arm64" or target_arch=="aarch64")', {
       'sources': [
-        # All intel and 64-bit ARM architectures get the 64 bit version.
+        # All intel x64 and 64-bit ARM architectures get the 64 bit version.
         'ecl/curve25519_64.c',
-        'verified/Hacl_Curve25519.c',
+        'verified/Hacl_Curve25519_51.c',
       ],
     }, {
       'sources': [
-        # All other architectures get the generic 32 bit implementation (slow!)
+        # All other architectures get the generic 32 bit implementation.
         'ecl/curve25519_32.c',
       ],
     }],
     [ 'disable_chachapoly==0', {
       # The ChaCha20 code is linked in through the static ssse3-crypto lib on
       # all platforms that support SSSE3. There are runtime checks in place to
       # choose the correct ChaCha implementation at runtime.
       'sources': [
         'verified/Hacl_Chacha20.c',
-      ],
-      'conditions': [
-        [ 'OS!="win"', {
-          'conditions': [
-            [ 'target_arch=="x64"', {
-              'sources': [
-                'verified/Hacl_Poly1305_64.c',
-              ],
-            }, {
-              # !Windows & !x64
-              'conditions': [
-                [ 'target_arch=="arm64" or target_arch=="aarch64"', {
-                  'sources': [
-                    'verified/Hacl_Poly1305_64.c',
-                  ],
-                }, {
-                  # !Windows & !x64 & !arm64 & !aarch64
-                  'sources': [
-                    'verified/Hacl_Poly1305_32.c',
-                  ],
-                }],
-              ],
-            }],
-          ],
-        }, {
-          # Windows
-          'sources': [
-            'verified/Hacl_Poly1305_32.c',
-          ],
-        }],
+        'verified/Hacl_Chacha20Poly1305_32.c',
+        'verified/Hacl_Poly1305_32.c',
       ],
     }],
     [ 'fuzz==1', {
       'sources!': [ 'drbg.c' ],
       'sources': [ 'det_rng.c' ],
     }],
     [ 'fuzz_tls==1', {
       'defines': [
@@ -212,16 +185,13 @@
             'MP_USE_UINT_DIGIT',
             'MP_ASSEMBLY_MULTIPLY',
             'MP_ASSEMBLY_SQUARE',
             'MP_ASSEMBLY_DIV_2DX1D',
           ],
         }],
       ],
     }],
-    [ 'have_int128_support==0', {
-        'sources': [ 'verified/FStar.c' ],
-    }],
   ],
  'ldflags': [
    '-Wl,-Bsymbolic'
  ],
 }
--- a/nss-tool/hw-support.c
+++ b/nss-tool/hw-support.c
@@ -19,16 +19,18 @@
 int main(int argc, char const *argv[]) {
   BL_Init();
   printf("\n\n ========== NSS Hardware Report ==========\n");
 #if defined(NSS_X86_OR_X64)
   printf("\tAES-NI \t%s supported\n", aesni_support() ? "" : "not");
   printf("\tPCLMUL \t%s supported\n", clmul_support() ? "" : "not");
   printf("\tAVX \t%s supported\n", avx_support() ? "" : "not");
   printf("\tSSSE3 \t%s supported\n", ssse3_support() ? "" : "not");
+  printf("\tSSE4.1 \t%s supported\n", sse4_1_support() ? "" : "not");
+  printf("\tSSE4.2 \t%s supported\n", sse4_2_support() ? "" : "not");
 #elif defined(__aarch64__) || defined(__arm__)
   printf("\tNEON \t%s supported\n", arm_neon_support() ? "" : "not");
   printf("\tAES \t%s supported\n", arm_aes_support() ? "" : "not");
   printf("\tPMULL \t%s supported\n", arm_pmull_support() ? "" : "not");
   printf("\tSHA1 \t%s supported\n", arm_sha1_support() ? "" : "not");
   printf("\tSHA2 \t%s supported\n", arm_sha2_support() ? "" : "not");
 #endif
   printf(" ========== Hardware Report End ==========\n\n\n");