Bug 1383369 - formally verified code from HaCl* for Chacha20 (non-vectorized), r=ttaubert,beurdouche

Differential Revision: https://phabricator.services.mozilla.com/D272

7 files changed, 557 insertions, 107 deletions

diff --git a/lib/freebl/Makefile b/lib/freebl/Makefile
index 41332f202..61e2ed21c 100644
--- a/lib/freebl/Makefile
+++ b/lib/freebl/Makefile
@@ -524,12 +524,14 @@ ifndef NSS_DISABLE_CHACHAPOLY
 
         ifneq (1,$(CC_IS_GCC))
             EXTRA_SRCS += chacha20.c
+            VERIFIED_SRCS += Hacl_Chacha20.c
         else
             EXTRA_SRCS += chacha20_vec.c
         endif
     else
         EXTRA_SRCS += poly1305.c
         EXTRA_SRCS += chacha20.c
+        VERIFIED_SRCS += Hacl_Chacha20.c
     endif # x86_64
 endif # NSS_DISABLE_CHACHAPOLY
 
@@ -590,11 +592,6 @@ ECL_OBJS += $(addprefix $(OBJDIR)/$(PROG_PREFIX), $(ECL_USERS:.c=$(OBJ_SUFFIX)))
 
 $(ECL_OBJS): $(ECL_HDRS)
 
-VERIFIED_OBJS = $(addprefix $(OBJDIR)/$(PROG_PREFIX), $(VERIFIED_SRCS:.c=$(OBJ_SUFFIX)))
-
-$(VERIFIED_OBJS): $(VERIFIED_HDRS)
-
-
 $(OBJDIR)/sysrand$(OBJ_SUFFIX): sysrand.c unix_rand.c win_rand.c
 
 $(OBJDIR)/$(PROG_PREFIX)mpprime$(OBJ_SUFFIX): primes.c
diff --git a/lib/freebl/chacha20.c b/lib/freebl/chacha20.c
index f55d1e670..15ed67b5b 100644
--- a/lib/freebl/chacha20.c
+++ b/lib/freebl/chacha20.c
@@ -7,113 +7,13 @@
 #include <string.h>
 #include <stdio.h>
 
-#include "prtypes.h"
-#include "secport.h"
 #include "chacha20.h"
-
-#if defined(_MSC_VER)
-#pragma intrinsic(_lrotl)
-#define ROTL32(x, n) _lrotl(x, n)
-#else
-#define ROTL32(x, n) ((x << n) | (x >> ((8 * sizeof x) - n)))
-#endif
-
-#define ROTATE(v, c) ROTL32((v), (c))
-
-#define U32TO8_LITTLE(p, v)          \
-    {                                \
-        (p)[0] = ((v)) & 0xff;       \
-        (p)[1] = ((v) >> 8) & 0xff;  \
-        (p)[2] = ((v) >> 16) & 0xff; \
-        (p)[3] = ((v) >> 24) & 0xff; \
-    }
-#define U8TO32_LITTLE(p)                                \
-    (((PRUint32)((p)[0])) | ((PRUint32)((p)[1]) << 8) | \
-     ((PRUint32)((p)[2]) << 16) | ((PRUint32)((p)[3]) << 24))
-
-#define QUARTERROUND(x, a, b, c, d) \
-    x[a] = x[a] + x[b];             \
-    x[d] = ROTATE(x[d] ^ x[a], 16); \
-    x[c] = x[c] + x[d];             \
-    x[b] = ROTATE(x[b] ^ x[c], 12); \
-    x[a] = x[a] + x[b];             \
-    x[d] = ROTATE(x[d] ^ x[a], 8);  \
-    x[c] = x[c] + x[d];             \
-    x[b] = ROTATE(x[b] ^ x[c], 7);
-
-static void
-ChaChaCore(unsigned char output[64], const PRUint32 input[16], int num_rounds)
-{
-    PRUint32 x[16];
-    int i;
-
-    PORT_Memcpy(x, input, sizeof(PRUint32) * 16);
-    for (i = num_rounds; i > 0; i -= 2) {
-        QUARTERROUND(x, 0, 4, 8, 12)
-        QUARTERROUND(x, 1, 5, 9, 13)
-        QUARTERROUND(x, 2, 6, 10, 14)
-        QUARTERROUND(x, 3, 7, 11, 15)
-        QUARTERROUND(x, 0, 5, 10, 15)
-        QUARTERROUND(x, 1, 6, 11, 12)
-        QUARTERROUND(x, 2, 7, 8, 13)
-        QUARTERROUND(x, 3, 4, 9, 14)
-    }
-
-    for (i = 0; i < 16; ++i) {
-        x[i] = x[i] + input[i];
-    }
-    for (i = 0; i < 16; ++i) {
-        U32TO8_LITTLE(output + 4 * i, x[i]);
-    }
-}
-
-static const unsigned char sigma[16] = "expand 32-byte k";
+#include "verified/Hacl_Chacha20.h"
 
 void
 ChaCha20XOR(unsigned char *out, const unsigned char *in, unsigned int inLen,
             const unsigned char key[32], const unsigned char nonce[12],
             uint32_t counter)
 {
-    unsigned char block[64];
-    PRUint32 input[16];
-    unsigned int i;
-
-    input[4] = U8TO32_LITTLE(key + 0);
-    input[5] = U8TO32_LITTLE(key + 4);
-    input[6] = U8TO32_LITTLE(key + 8);
-    input[7] = U8TO32_LITTLE(key + 12);
-
-    input[8] = U8TO32_LITTLE(key + 16);
-    input[9] = U8TO32_LITTLE(key + 20);
-    input[10] = U8TO32_LITTLE(key + 24);
-    input[11] = U8TO32_LITTLE(key + 28);
-
-    input[0] = U8TO32_LITTLE(sigma + 0);
-    input[1] = U8TO32_LITTLE(sigma + 4);
-    input[2] = U8TO32_LITTLE(sigma + 8);
-    input[3] = U8TO32_LITTLE(sigma + 12);
-
-    input[12] = counter;
-    input[13] = U8TO32_LITTLE(nonce + 0);
-    input[14] = U8TO32_LITTLE(nonce + 4);
-    input[15] = U8TO32_LITTLE(nonce + 8);
-
-    while (inLen >= 64) {
-        ChaChaCore(block, input, 20);
-        for (i = 0; i < 64; i++) {
-            out[i] = in[i] ^ block[i];
-        }
-
-        input[12]++;
-        inLen -= 64;
-        in += 64;
-        out += 64;
-    }
-
-    if (inLen > 0) {
-        ChaChaCore(block, input, 20);
-        for (i = 0; i < inLen; i++) {
-            out[i] = in[i] ^ block[i];
-        }
-    }
+    Hacl_Chacha20_chacha20(out, (uint8_t *)in, inLen, (uint8_t *)key, (uint8_t *)nonce, counter);
 }
diff --git a/lib/freebl/freebl_base.gypi b/lib/freebl/freebl_base.gypi
index faef1e02f..d9415a7c6 100644
--- a/lib/freebl/freebl_base.gypi
+++ b/lib/freebl/freebl_base.gypi
@@ -154,6 +154,7 @@
           # not x64
           'sources': [
             'chacha20.c',
+            'verified/Hacl_Chacha20.c',
             'poly1305.c',
           ],
         }],
diff --git a/lib/freebl/verified/Hacl_Chacha20.c b/lib/freebl/verified/Hacl_Chacha20.c
new file mode 100644
index 000000000..68d0ad21a
--- /dev/null
+++ b/lib/freebl/verified/Hacl_Chacha20.c
@@ -0,0 +1,255 @@
+/* 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.
+ */
+
+#include "Hacl_Chacha20.h"
+
+static void
+Hacl_Lib_LoadStore32_uint32s_from_le_bytes(uint32_t *output, uint8_t *input, uint32_t len)
+{
+    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+        uint8_t *x0 = input + (uint32_t)4U * i;
+        uint32_t inputi = load32_le(x0);
+        output[i] = inputi;
+    }
+}
+
+static void
+Hacl_Lib_LoadStore32_uint32s_to_le_bytes(uint8_t *output, uint32_t *input, uint32_t len)
+{
+    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+        uint32_t hd1 = input[i];
+        uint8_t *x0 = output + (uint32_t)4U * i;
+        store32_le(x0, hd1);
+    }
+}
+
+inline static uint32_t
+Hacl_Impl_Chacha20_rotate_left(uint32_t a, uint32_t s)
+{
+    return a << s | a >> ((uint32_t)32U - s);
+}
+
+inline static void
+Hacl_Impl_Chacha20_setup(uint32_t *st, uint8_t *k, uint8_t *n1, uint32_t c)
+{
+    uint32_t *stcst = st;
+    uint32_t *stk = st + (uint32_t)4U;
+    uint32_t *stc = st + (uint32_t)12U;
+    uint32_t *stn = st + (uint32_t)13U;
+    stcst[0U] = (uint32_t)0x61707865U;
+    stcst[1U] = (uint32_t)0x3320646eU;
+    stcst[2U] = (uint32_t)0x79622d32U;
+    stcst[3U] = (uint32_t)0x6b206574U;
+    Hacl_Lib_LoadStore32_uint32s_from_le_bytes(stk, k, (uint32_t)8U);
+    stc[0U] = c;
+    Hacl_Lib_LoadStore32_uint32s_from_le_bytes(stn, n1, (uint32_t)3U);
+}
+
+inline static void
+Hacl_Impl_Chacha20_quarter_round(uint32_t *st, uint32_t a, uint32_t b, uint32_t c, uint32_t d)
+{
+    uint32_t sa = st[a];
+    uint32_t sb0 = st[b];
+    st[a] = sa + sb0;
+    uint32_t sd = st[d];
+    uint32_t sa10 = st[a];
+    uint32_t sda = sd ^ sa10;
+    st[d] = Hacl_Impl_Chacha20_rotate_left(sda, (uint32_t)16U);
+    uint32_t sa0 = st[c];
+    uint32_t sb1 = st[d];
+    st[c] = sa0 + sb1;
+    uint32_t sd0 = st[b];
+    uint32_t sa11 = st[c];
+    uint32_t sda0 = sd0 ^ sa11;
+    st[b] = Hacl_Impl_Chacha20_rotate_left(sda0, (uint32_t)12U);
+    uint32_t sa2 = st[a];
+    uint32_t sb2 = st[b];
+    st[a] = sa2 + sb2;
+    uint32_t sd1 = st[d];
+    uint32_t sa12 = st[a];
+    uint32_t sda1 = sd1 ^ sa12;
+    st[d] = Hacl_Impl_Chacha20_rotate_left(sda1, (uint32_t)8U);
+    uint32_t sa3 = st[c];
+    uint32_t sb = st[d];
+    st[c] = sa3 + sb;
+    uint32_t sd2 = st[b];
+    uint32_t sa1 = st[c];
+    uint32_t sda2 = sd2 ^ sa1;
+    st[b] = Hacl_Impl_Chacha20_rotate_left(sda2, (uint32_t)7U);
+}
+
+inline static void
+Hacl_Impl_Chacha20_double_round(uint32_t *st)
+{
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)0U, (uint32_t)4U, (uint32_t)8U, (uint32_t)12U);
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)1U, (uint32_t)5U, (uint32_t)9U, (uint32_t)13U);
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)2U, (uint32_t)6U, (uint32_t)10U, (uint32_t)14U);
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)3U, (uint32_t)7U, (uint32_t)11U, (uint32_t)15U);
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)0U, (uint32_t)5U, (uint32_t)10U, (uint32_t)15U);
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)1U, (uint32_t)6U, (uint32_t)11U, (uint32_t)12U);
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)2U, (uint32_t)7U, (uint32_t)8U, (uint32_t)13U);
+    Hacl_Impl_Chacha20_quarter_round(st, (uint32_t)3U, (uint32_t)4U, (uint32_t)9U, (uint32_t)14U);
+}
+
+inline static void
+Hacl_Impl_Chacha20_rounds(uint32_t *st)
+{
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)10U; i = i + (uint32_t)1U)
+        Hacl_Impl_Chacha20_double_round(st);
+}
+
+inline static void
+Hacl_Impl_Chacha20_sum_states(uint32_t *st, uint32_t *st_)
+{
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
+        uint32_t xi = st[i];
+        uint32_t yi = st_[i];
+        st[i] = xi + yi;
+    }
+}
+
+inline static void
+Hacl_Impl_Chacha20_copy_state(uint32_t *st, uint32_t *st_)
+{
+    memcpy(st, st_, (uint32_t)16U * sizeof st_[0U]);
+}
+
+inline static void
+Hacl_Impl_Chacha20_chacha20_core(uint32_t *k, uint32_t *st, uint32_t ctr)
+{
+    st[12U] = ctr;
+    Hacl_Impl_Chacha20_copy_state(k, st);
+    Hacl_Impl_Chacha20_rounds(k);
+    Hacl_Impl_Chacha20_sum_states(k, st);
+}
+
+inline static void
+Hacl_Impl_Chacha20_chacha20_block(uint8_t *stream_block, uint32_t *st, uint32_t ctr)
+{
+    uint32_t st_[16U] = { 0U };
+    Hacl_Impl_Chacha20_chacha20_core(st_, st, ctr);
+    Hacl_Lib_LoadStore32_uint32s_to_le_bytes(stream_block, st_, (uint32_t)16U);
+}
+
+inline static void
+Hacl_Impl_Chacha20_init(uint32_t *st, uint8_t *k, uint8_t *n1)
+{
+    Hacl_Impl_Chacha20_setup(st, k, n1, (uint32_t)0U);
+}
+
+static void
+Hacl_Impl_Chacha20_update(uint8_t *output, uint8_t *plain, uint32_t *st, uint32_t ctr)
+{
+    uint32_t b[48U] = { 0U };
+    uint32_t *k = b;
+    uint32_t *ib = b + (uint32_t)16U;
+    uint32_t *ob = b + (uint32_t)32U;
+    Hacl_Impl_Chacha20_chacha20_core(k, st, ctr);
+    Hacl_Lib_LoadStore32_uint32s_from_le_bytes(ib, plain, (uint32_t)16U);
+    for (uint32_t i = (uint32_t)0U; i < (uint32_t)16U; i = i + (uint32_t)1U) {
+        uint32_t xi = ib[i];
+        uint32_t yi = k[i];
+        ob[i] = xi ^ yi;
+    }
+    Hacl_Lib_LoadStore32_uint32s_to_le_bytes(output, ob, (uint32_t)16U);
+}
+
+static void
+Hacl_Impl_Chacha20_update_last(
+    uint8_t *output,
+    uint8_t *plain,
+    uint32_t len,
+    uint32_t *st,
+    uint32_t ctr)
+{
+    uint8_t block[64U] = { 0U };
+    Hacl_Impl_Chacha20_chacha20_block(block, st, ctr);
+    uint8_t *mask = block;
+    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+        uint8_t xi = plain[i];
+        uint8_t yi = mask[i];
+        output[i] = xi ^ yi;
+    }
+}
+
+static void
+Hacl_Impl_Chacha20_chacha20_counter_mode_blocks(
+    uint8_t *output,
+    uint8_t *plain,
+    uint32_t len,
+    uint32_t *st,
+    uint32_t ctr)
+{
+    for (uint32_t i = (uint32_t)0U; i < len; i = i + (uint32_t)1U) {
+        uint8_t *b = plain + (uint32_t)64U * i;
+        uint8_t *o = output + (uint32_t)64U * i;
+        Hacl_Impl_Chacha20_update(o, b, st, ctr + i);
+    }
+}
+
+static void
+Hacl_Impl_Chacha20_chacha20_counter_mode(
+    uint8_t *output,
+    uint8_t *plain,
+    uint32_t len,
+    uint32_t *st,
+    uint32_t ctr)
+{
+    uint32_t blocks_len = len >> (uint32_t)6U;
+    uint32_t part_len = len & (uint32_t)0x3fU;
+    uint8_t *output_ = output;
+    uint8_t *plain_ = plain;
+    uint8_t *output__ = output + (uint32_t)64U * blocks_len;
+    uint8_t *plain__ = plain + (uint32_t)64U * blocks_len;
+    Hacl_Impl_Chacha20_chacha20_counter_mode_blocks(output_, plain_, blocks_len, st, ctr);
+    if (part_len > (uint32_t)0U)
+        Hacl_Impl_Chacha20_update_last(output__, plain__, part_len, st, ctr + blocks_len);
+}
+
+static void
+Hacl_Impl_Chacha20_chacha20(
+    uint8_t *output,
+    uint8_t *plain,
+    uint32_t len,
+    uint8_t *k,
+    uint8_t *n1,
+    uint32_t ctr)
+{
+    uint32_t buf[16U] = { 0U };
+    uint32_t *st = buf;
+    Hacl_Impl_Chacha20_init(st, k, n1);
+    Hacl_Impl_Chacha20_chacha20_counter_mode(output, plain, len, st, ctr);
+}
+
+void
+Hacl_Chacha20_chacha20_key_block(uint8_t *block, uint8_t *k, uint8_t *n1, uint32_t ctr)
+{
+    uint32_t buf[16U] = { 0U };
+    uint32_t *st = buf;
+    Hacl_Impl_Chacha20_init(st, k, n1);
+    Hacl_Impl_Chacha20_chacha20_block(block, st, ctr);
+}
+
+void
+Hacl_Chacha20_chacha20(
+    uint8_t *output,
+    uint8_t *plain,
+    uint32_t len,
+    uint8_t *k,
+    uint8_t *n1,
+    uint32_t ctr)
+{
+    Hacl_Impl_Chacha20_chacha20(output, plain, len, k, n1, ctr);
+}
diff --git a/lib/freebl/verified/Hacl_Chacha20.h b/lib/freebl/verified/Hacl_Chacha20.h
new file mode 100644
index 000000000..b5c86968b
--- /dev/null
+++ b/lib/freebl/verified/Hacl_Chacha20.h
@@ -0,0 +1,60 @@
+/* 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.
+ */
+
+#include "kremlib.h"
+#ifndef __Hacl_Chacha20_H
+#define __Hacl_Chacha20_H
+
+typedef uint32_t Hacl_Impl_Xor_Lemmas_u32;
+
+typedef uint8_t Hacl_Impl_Xor_Lemmas_u8;
+
+typedef uint8_t *Hacl_Lib_LoadStore32_uint8_p;
+
+typedef uint32_t Hacl_Impl_Chacha20_u32;
+
+typedef uint32_t Hacl_Impl_Chacha20_h32;
+
+typedef uint8_t *Hacl_Impl_Chacha20_uint8_p;
+
+typedef uint32_t *Hacl_Impl_Chacha20_state;
+
+typedef uint32_t Hacl_Impl_Chacha20_idx;
+
+typedef struct
+{
+    void *k;
+    void *n;
+} Hacl_Impl_Chacha20_log_t_;
+
+typedef void *Hacl_Impl_Chacha20_log_t;
+
+typedef uint32_t Hacl_Lib_Create_h32;
+
+typedef uint8_t *Hacl_Chacha20_uint8_p;
+
+typedef uint32_t Hacl_Chacha20_uint32_t;
+
+void Hacl_Chacha20_chacha20_key_block(uint8_t *block, uint8_t *k, uint8_t *n1, uint32_t ctr);
+
+void
+Hacl_Chacha20_chacha20(
+    uint8_t *output,
+    uint8_t *plain,
+    uint32_t len,
+    uint8_t *k,
+    uint8_t *n1,
+    uint32_t ctr);
+#endif
diff --git a/lib/freebl/verified/specs/Spec.CTR.fst b/lib/freebl/verified/specs/Spec.CTR.fst
new file mode 100644
index 000000000..fecc53ad5
--- /dev/null
+++ b/lib/freebl/verified/specs/Spec.CTR.fst
@@ -0,0 +1,83 @@
+module Spec.CTR
+
+module ST = FStar.HyperStack.ST
+
+open FStar.Mul
+open FStar.Seq
+open Spec.Lib
+
+#reset-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
+
+type block_cipher_ctx = {
+     keylen: nat ;
+     blocklen: (x:nat{x>0});
+     noncelen: nat;
+     counterbits: nat;
+     incr: pos}
+
+type key (c:block_cipher_ctx) = lbytes c.keylen
+type nonce (c:block_cipher_ctx) = lbytes c.noncelen
+type block (c:block_cipher_ctx) = lbytes (c.blocklen*c.incr)
+type counter (c:block_cipher_ctx) = UInt.uint_t c.counterbits
+type block_cipher (c:block_cipher_ctx) =  key c -> nonce c -> counter c -> block c
+
+val xor: #len:nat -> x:lbytes len -> y:lbytes len -> Tot (lbytes len)
+let xor #len x y = map2 FStar.UInt8.(fun x y -> x ^^ y) x y
+
+
+val counter_mode_blocks:
+  ctx: block_cipher_ctx ->
+  bc: block_cipher ctx ->
+  k:key ctx -> n:nonce ctx -> c:counter ctx ->
+  plain:seq UInt8.t{c + ctx.incr * (length plain / ctx.blocklen) < pow2 ctx.counterbits /\
+    length plain % (ctx.blocklen * ctx.incr) = 0} ->
+  Tot (lbytes (length plain))
+      (decreases (length plain))
+#reset-options "--z3rlimit 200 --max_fuel 0"
+let rec counter_mode_blocks ctx block_enc key nonce counter plain =
+  let len  = length plain in
+  let len' = len / (ctx.blocklen * ctx.incr) in
+  Math.Lemmas.lemma_div_mod len (ctx.blocklen * ctx.incr) ;
+  if len = 0 then Seq.createEmpty #UInt8.t
+  else (
+    let prefix, block = split plain (len - ctx.blocklen * ctx.incr) in    
+      (* TODO: move to a single lemma for clarify *)
+      Math.Lemmas.lemma_mod_plus (length prefix) 1 (ctx.blocklen * ctx.incr);
+      Math.Lemmas.lemma_div_le (length prefix) len ctx.blocklen;
+      Spec.CTR.Lemmas.lemma_div len (ctx.blocklen * ctx.incr);
+      (* End TODO *)
+    let cipher        = counter_mode_blocks ctx block_enc key nonce counter prefix in
+    let mask          = block_enc key nonce (counter + (len / ctx.blocklen - 1) * ctx.incr) in
+    let eb            = xor block mask in
+    cipher @| eb
+  )
+
+
+val counter_mode:
+  ctx: block_cipher_ctx ->
+  bc: block_cipher ctx ->
+  k:key ctx -> n:nonce ctx -> c:counter ctx ->
+  plain:seq UInt8.t{c + ctx.incr * (length plain / ctx.blocklen) < pow2 ctx.counterbits} ->
+  Tot (lbytes (length plain))
+      (decreases (length plain))
+#reset-options "--z3rlimit 200 --max_fuel 0"
+let counter_mode ctx block_enc key nonce counter plain =
+  let len = length plain in
+  let blocks_len = (ctx.incr * ctx.blocklen) * (len / (ctx.blocklen * ctx.incr)) in
+  let part_len   = len % (ctx.blocklen * ctx.incr) in
+    (* TODO: move to a single lemma for clarify *)
+    Math.Lemmas.lemma_div_mod len (ctx.blocklen * ctx.incr);
+    Math.Lemmas.multiple_modulo_lemma (len / (ctx.blocklen * ctx.incr)) (ctx.blocklen * ctx.incr);
+    Math.Lemmas.lemma_div_le (blocks_len) len ctx.blocklen;
+    (* End TODO *)
+  let blocks, last_block = split plain blocks_len in
+  let cipher_blocks = counter_mode_blocks ctx block_enc key nonce counter blocks in
+  let cipher_last_block =
+    if part_len > 0
+    then (* encrypt final partial block(s) *)
+      let mask = block_enc key nonce (counter+ctx.incr*(length plain / ctx.blocklen)) in
+      let mask = slice mask 0 part_len in
+      assert(length last_block = part_len);
+      xor #part_len last_block mask
+    else createEmpty in
+  cipher_blocks @| cipher_last_block
diff --git a/lib/freebl/verified/specs/Spec.Chacha20.fst b/lib/freebl/verified/specs/Spec.Chacha20.fst
new file mode 100644
index 000000000..2cc3ea714
--- /dev/null
+++ b/lib/freebl/verified/specs/Spec.Chacha20.fst
@@ -0,0 +1,154 @@
+module Spec.Chacha20
+
+module ST = FStar.HyperStack.ST
+
+open FStar.Mul
+open FStar.Seq
+open FStar.UInt32
+open FStar.Endianness
+open Spec.Lib
+open Spec.Chacha20.Lemmas
+open Seq.Create
+
+#set-options "--max_fuel 0 --z3rlimit 100"
+
+(* Constants *)
+let keylen = 32   (* in bytes *)
+let blocklen = 64 (* in bytes *)
+let noncelen = 12 (* in bytes *)
+
+type key = lbytes keylen
+type block = lbytes blocklen
+type nonce = lbytes noncelen
+type counter = UInt.uint_t 32
+
+// using @ as a functional substitute for ;
+// internally, blocks are represented as 16 x 4-byte integers
+type state = m:seq UInt32.t {length m = 16}
+type idx = n:nat{n < 16}
+type shuffle = state -> Tot state
+
+let line (a:idx) (b:idx) (d:idx) (s:t{0 < v s /\ v s < 32}) (m:state) : Tot state =
+  let m = m.[a] <- (m.[a] +%^ m.[b]) in
+  let m = m.[d] <- ((m.[d] ^^ m.[a]) <<< s) in m
+
+let quarter_round a b c d : shuffle =
+  line a b d 16ul @
+  line c d b 12ul @
+  line a b d 8ul  @
+  line c d b 7ul
+
+let column_round : shuffle =
+  quarter_round 0 4 8  12 @
+  quarter_round 1 5 9  13 @
+  quarter_round 2 6 10 14 @
+  quarter_round 3 7 11 15
+
+let diagonal_round : shuffle =
+  quarter_round 0 5 10 15 @
+  quarter_round 1 6 11 12 @
+  quarter_round 2 7 8  13 @
+  quarter_round 3 4 9  14
+
+let double_round: shuffle =
+    column_round @ diagonal_round (* 2 rounds *)
+
+let rounds : shuffle =
+    iter 10 double_round (* 20 rounds *)
+
+let chacha20_core (s:state) : Tot state =
+    let s' = rounds s in
+    Spec.Loops.seq_map2 (fun x y -> x +%^ y) s' s
+
+(* state initialization *)
+let c0 = 0x61707865ul
+let c1 = 0x3320646eul
+let c2 = 0x79622d32ul
+let c3 = 0x6b206574ul
+
+let setup (k:key) (n:nonce) (c:counter): Tot state =
+  create_4 c0 c1 c2 c3          @|
+  uint32s_from_le 8 k           @|
+  create_1 (UInt32.uint_to_t c) @|
+  uint32s_from_le 3 n
+
+let chacha20_block (k:key) (n:nonce) (c:counter): Tot block =
+    let st  = setup k n c in
+    let st' = chacha20_core st in
+    uint32s_to_le 16 st'
+
+let chacha20_ctx: Spec.CTR.block_cipher_ctx =
+    let open Spec.CTR in
+    {
+    keylen = keylen;
+    blocklen = blocklen;
+    noncelen = noncelen;
+    counterbits = 32;
+    incr = 1
+    }
+
+let chacha20_cipher: Spec.CTR.block_cipher chacha20_ctx = chacha20_block
+
+let chacha20_encrypt_bytes key nonce counter m =
+    Spec.CTR.counter_mode chacha20_ctx chacha20_cipher key nonce counter m
+
+
+unfold let test_plaintext = [
+    0x4cuy; 0x61uy; 0x64uy; 0x69uy; 0x65uy; 0x73uy; 0x20uy; 0x61uy;
+    0x6euy; 0x64uy; 0x20uy; 0x47uy; 0x65uy; 0x6euy; 0x74uy; 0x6cuy;
+    0x65uy; 0x6duy; 0x65uy; 0x6euy; 0x20uy; 0x6fuy; 0x66uy; 0x20uy;
+    0x74uy; 0x68uy; 0x65uy; 0x20uy; 0x63uy; 0x6cuy; 0x61uy; 0x73uy;
+    0x73uy; 0x20uy; 0x6fuy; 0x66uy; 0x20uy; 0x27uy; 0x39uy; 0x39uy;
+    0x3auy; 0x20uy; 0x49uy; 0x66uy; 0x20uy; 0x49uy; 0x20uy; 0x63uy;
+    0x6fuy; 0x75uy; 0x6cuy; 0x64uy; 0x20uy; 0x6fuy; 0x66uy; 0x66uy;
+    0x65uy; 0x72uy; 0x20uy; 0x79uy; 0x6fuy; 0x75uy; 0x20uy; 0x6fuy;
+    0x6euy; 0x6cuy; 0x79uy; 0x20uy; 0x6fuy; 0x6euy; 0x65uy; 0x20uy;
+    0x74uy; 0x69uy; 0x70uy; 0x20uy; 0x66uy; 0x6fuy; 0x72uy; 0x20uy;
+    0x74uy; 0x68uy; 0x65uy; 0x20uy; 0x66uy; 0x75uy; 0x74uy; 0x75uy;
+    0x72uy; 0x65uy; 0x2cuy; 0x20uy; 0x73uy; 0x75uy; 0x6euy; 0x73uy;
+    0x63uy; 0x72uy; 0x65uy; 0x65uy; 0x6euy; 0x20uy; 0x77uy; 0x6fuy;
+    0x75uy; 0x6cuy; 0x64uy; 0x20uy; 0x62uy; 0x65uy; 0x20uy; 0x69uy;
+    0x74uy; 0x2euy
+]
+
+unfold let test_ciphertext = [
+    0x6euy; 0x2euy; 0x35uy; 0x9auy; 0x25uy; 0x68uy; 0xf9uy; 0x80uy;
+    0x41uy; 0xbauy; 0x07uy; 0x28uy; 0xdduy; 0x0duy; 0x69uy; 0x81uy;
+    0xe9uy; 0x7euy; 0x7auy; 0xecuy; 0x1duy; 0x43uy; 0x60uy; 0xc2uy;
+    0x0auy; 0x27uy; 0xafuy; 0xccuy; 0xfduy; 0x9fuy; 0xaeuy; 0x0buy;
+    0xf9uy; 0x1buy; 0x65uy; 0xc5uy; 0x52uy; 0x47uy; 0x33uy; 0xabuy;
+    0x8fuy; 0x59uy; 0x3duy; 0xabuy; 0xcduy; 0x62uy; 0xb3uy; 0x57uy;
+    0x16uy; 0x39uy; 0xd6uy; 0x24uy; 0xe6uy; 0x51uy; 0x52uy; 0xabuy;
+    0x8fuy; 0x53uy; 0x0cuy; 0x35uy; 0x9fuy; 0x08uy; 0x61uy; 0xd8uy;
+    0x07uy; 0xcauy; 0x0duy; 0xbfuy; 0x50uy; 0x0duy; 0x6auy; 0x61uy;
+    0x56uy; 0xa3uy; 0x8euy; 0x08uy; 0x8auy; 0x22uy; 0xb6uy; 0x5euy;
+    0x52uy; 0xbcuy; 0x51uy; 0x4duy; 0x16uy; 0xccuy; 0xf8uy; 0x06uy;
+    0x81uy; 0x8cuy; 0xe9uy; 0x1auy; 0xb7uy; 0x79uy; 0x37uy; 0x36uy;
+    0x5auy; 0xf9uy; 0x0buy; 0xbfuy; 0x74uy; 0xa3uy; 0x5buy; 0xe6uy;
+    0xb4uy; 0x0buy; 0x8euy; 0xeduy; 0xf2uy; 0x78uy; 0x5euy; 0x42uy;
+    0x87uy; 0x4duy
+]
+
+unfold let test_key = [
+    0uy;   1uy;  2uy;  3uy;  4uy;  5uy;  6uy;  7uy;
+    8uy;   9uy; 10uy; 11uy; 12uy; 13uy; 14uy; 15uy;
+    16uy; 17uy; 18uy; 19uy; 20uy; 21uy; 22uy; 23uy;
+    24uy; 25uy; 26uy; 27uy; 28uy; 29uy; 30uy; 31uy
+    ]
+unfold let test_nonce = [
+    0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0uy; 0x4auy; 0uy; 0uy; 0uy; 0uy
+    ]
+
+unfold let test_counter = 1
+
+let test() =
+  assert_norm(List.Tot.length test_plaintext = 114);
+  assert_norm(List.Tot.length test_ciphertext = 114);
+  assert_norm(List.Tot.length test_key = 32);
+  assert_norm(List.Tot.length test_nonce = 12);
+  let test_plaintext = createL test_plaintext in
+  let test_ciphertext = createL test_ciphertext in
+  let test_key = createL test_key in
+  let test_nonce = createL test_nonce in
+  chacha20_encrypt_bytes test_key test_nonce test_counter test_plaintext
+  = test_ciphertext