Revert "Update NSS to 3.35-RTM"

This reverts commit f1a0f0a56fdd0fc39f255174ce08c06b91c66c94.

4 files changed, 0 insertions, 542 deletions

diff --git a/security/nss/lib/freebl/verified/specs/Spec.CTR.fst b/security/nss/lib/freebl/verified/specs/Spec.CTR.fst
deleted file mode 100644
index e411cd353..000000000
--- a/security/nss/lib/freebl/verified/specs/Spec.CTR.fst
+++ /dev/null
@@ -1,98 +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.
- */
-
-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/security/nss/lib/freebl/verified/specs/Spec.Chacha20.fst b/security/nss/lib/freebl/verified/specs/Spec.Chacha20.fst
deleted file mode 100644
index 0bdc69725..000000000
--- a/security/nss/lib/freebl/verified/specs/Spec.Chacha20.fst
+++ /dev/null
@@ -1,169 +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.
- */
-
-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
diff --git a/security/nss/lib/freebl/verified/specs/Spec.Curve25519.fst b/security/nss/lib/freebl/verified/specs/Spec.Curve25519.fst
deleted file mode 100644
index af4035b09..000000000
--- a/security/nss/lib/freebl/verified/specs/Spec.Curve25519.fst
+++ /dev/null
@@ -1,168 +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.
- */
-
-module Spec.Curve25519
-
-module ST = FStar.HyperStack.ST
-
-open FStar.Mul
-open FStar.Seq
-open FStar.UInt8
-open FStar.Endianness
-open Spec.Lib
-open Spec.Curve25519.Lemmas
-
-#reset-options "--initial_fuel 0 --max_fuel 0 --z3rlimit 20"
-
-(* Field types and parameters *)
-let prime = pow2 255 - 19
-type elem : Type0 = e:int{e >= 0 /\ e < prime}
-let fadd e1 e2 = (e1 + e2) % prime
-let fsub e1 e2 = (e1 - e2) % prime
-let fmul e1 e2 = (e1 * e2) % prime
-let zero : elem = 0
-let one  : elem = 1
-let ( +@ ) = fadd
-let ( *@ ) = fmul
-
-(** Exponentiation *)
-let rec ( ** ) (e:elem) (n:pos) : Tot elem (decreases n) =
-  if n = 1 then e
-  else
-    if n % 2 = 0 then op_Star_Star (e `fmul` e) (n / 2)
-    else e `fmul` (op_Star_Star (e `fmul` e) ((n-1)/2))
-
-(* Type aliases *)
-type scalar = lbytes 32
-type serialized_point = lbytes 32
-type proj_point = | Proj: x:elem -> z:elem -> proj_point
-
-let decodeScalar25519 (k:scalar) =
-  let k   = k.[0] <- (k.[0] &^ 248uy)          in
-  let k   = k.[31] <- ((k.[31] &^ 127uy) |^ 64uy) in k
-
-let decodePoint (u:serialized_point) =
-  (little_endian u % pow2 255) % prime
-
-let add_and_double qx nq nqp1 =
-  let x_1 = qx in
-  let x_2, z_2 = nq.x, nq.z in
-  let x_3, z_3 = nqp1.x, nqp1.z in
-  let a  = x_2 `fadd` z_2 in
-  let aa = a**2 in
-  let b  = x_2 `fsub` z_2 in
-  let bb = b**2 in
-  let e = aa `fsub` bb in
-  let c = x_3 `fadd` z_3 in
-  let d = x_3 `fsub` z_3 in
-  let da = d `fmul` a in
-  let cb = c `fmul` b in
-  let x_3 = (da `fadd` cb)**2 in
-  let z_3 = x_1 `fmul` ((da `fsub` cb)**2) in
-  let x_2 = aa `fmul` bb in
-  let z_2 = e `fmul` (aa `fadd` (121665 `fmul` e)) in
-  Proj x_2 z_2, Proj x_3 z_3
-
-let ith_bit (k:scalar) (i:nat{i < 256}) =
-  let q = i / 8 in let r = i % 8 in
-  (v (k.[q]) / pow2 r) % 2
-
-let rec montgomery_ladder_ (init:elem) x xp1 (k:scalar) (ctr:nat{ctr<=256})
-  : Tot proj_point (decreases ctr) =
-  if ctr = 0 then x
-  else (
-    let ctr' = ctr - 1 in
-    let (x', xp1') =
-      if ith_bit k ctr' = 1 then (
-        let nqp2, nqp1 = add_and_double init xp1 x in
-        nqp1, nqp2
-      ) else add_and_double init x xp1 in
-    montgomery_ladder_ init x' xp1' k ctr'
-  )
-
-let montgomery_ladder (init:elem) (k:scalar) : Tot proj_point =
-  montgomery_ladder_ init (Proj one zero) (Proj init one) k 256
-
-let encodePoint (p:proj_point) : Tot serialized_point =
-  let p = p.x `fmul` (p.z ** (prime - 2)) in
-  little_bytes 32ul p
-
-let scalarmult (k:scalar) (u:serialized_point) : Tot serialized_point =
-  let k = decodeScalar25519 k in
-  let u = decodePoint u in
-  let res = montgomery_ladder u k in
-  encodePoint res
-
-
-(* ********************* *)
-(* RFC 7748 Test Vectors *)
-(* ********************* *)
-
-let scalar1 = [
-  0xa5uy; 0x46uy; 0xe3uy; 0x6buy; 0xf0uy; 0x52uy; 0x7cuy; 0x9duy;
-  0x3buy; 0x16uy; 0x15uy; 0x4buy; 0x82uy; 0x46uy; 0x5euy; 0xdduy;
-  0x62uy; 0x14uy; 0x4cuy; 0x0auy; 0xc1uy; 0xfcuy; 0x5auy; 0x18uy;
-  0x50uy; 0x6auy; 0x22uy; 0x44uy; 0xbauy; 0x44uy; 0x9auy; 0xc4uy
-]
-
-let scalar2 = [
-  0x4buy; 0x66uy; 0xe9uy; 0xd4uy; 0xd1uy; 0xb4uy; 0x67uy; 0x3cuy;
-  0x5auy; 0xd2uy; 0x26uy; 0x91uy; 0x95uy; 0x7duy; 0x6auy; 0xf5uy;
-  0xc1uy; 0x1buy; 0x64uy; 0x21uy; 0xe0uy; 0xeauy; 0x01uy; 0xd4uy;
-  0x2cuy; 0xa4uy; 0x16uy; 0x9euy; 0x79uy; 0x18uy; 0xbauy; 0x0duy
-]
-
-let input1 = [
-  0xe6uy; 0xdbuy; 0x68uy; 0x67uy; 0x58uy; 0x30uy; 0x30uy; 0xdbuy;
-  0x35uy; 0x94uy; 0xc1uy; 0xa4uy; 0x24uy; 0xb1uy; 0x5fuy; 0x7cuy;
-  0x72uy; 0x66uy; 0x24uy; 0xecuy; 0x26uy; 0xb3uy; 0x35uy; 0x3buy;
-  0x10uy; 0xa9uy; 0x03uy; 0xa6uy; 0xd0uy; 0xabuy; 0x1cuy; 0x4cuy
-]
-
-let input2 = [
-  0xe5uy; 0x21uy; 0x0fuy; 0x12uy; 0x78uy; 0x68uy; 0x11uy; 0xd3uy;
-  0xf4uy; 0xb7uy; 0x95uy; 0x9duy; 0x05uy; 0x38uy; 0xaeuy; 0x2cuy;
-  0x31uy; 0xdbuy; 0xe7uy; 0x10uy; 0x6fuy; 0xc0uy; 0x3cuy; 0x3euy;
-  0xfcuy; 0x4cuy; 0xd5uy; 0x49uy; 0xc7uy; 0x15uy; 0xa4uy; 0x93uy
-]
-
-let expected1 = [
-  0xc3uy; 0xdauy; 0x55uy; 0x37uy; 0x9duy; 0xe9uy; 0xc6uy; 0x90uy;
-  0x8euy; 0x94uy; 0xeauy; 0x4duy; 0xf2uy; 0x8duy; 0x08uy; 0x4fuy;
-  0x32uy; 0xecuy; 0xcfuy; 0x03uy; 0x49uy; 0x1cuy; 0x71uy; 0xf7uy;
-  0x54uy; 0xb4uy; 0x07uy; 0x55uy; 0x77uy; 0xa2uy; 0x85uy; 0x52uy
-]
-let expected2 = [
-  0x95uy; 0xcbuy; 0xdeuy; 0x94uy; 0x76uy; 0xe8uy; 0x90uy; 0x7duy;
-  0x7auy; 0xaduy; 0xe4uy; 0x5cuy; 0xb4uy; 0xb8uy; 0x73uy; 0xf8uy;
-  0x8buy; 0x59uy; 0x5auy; 0x68uy; 0x79uy; 0x9fuy; 0xa1uy; 0x52uy;
-  0xe6uy; 0xf8uy; 0xf7uy; 0x64uy; 0x7auy; 0xacuy; 0x79uy; 0x57uy
-]
-
-let test () =
-  assert_norm(List.Tot.length scalar1 = 32);
-  assert_norm(List.Tot.length scalar2 = 32);
-  assert_norm(List.Tot.length input1 = 32);
-  assert_norm(List.Tot.length input2 = 32);
-  assert_norm(List.Tot.length expected1 = 32);
-  assert_norm(List.Tot.length expected2 = 32);
-  let scalar1 = createL scalar1 in
-  let scalar2 = createL scalar2 in
-  let input1 = createL input1 in
-  let input2 = createL input2 in
-  let expected1 = createL expected1 in
-  let expected2 = createL expected2 in
-  scalarmult scalar1 input1 = expected1
-  && scalarmult scalar2 input2 = expected2
diff --git a/security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst b/security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst
deleted file mode 100644
index f9d8a4cb2..000000000
--- a/security/nss/lib/freebl/verified/specs/Spec.Poly1305.fst
+++ /dev/null
@@ -1,107 +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.
- */
-
-module Spec.Poly1305
-
-module ST = FStar.HyperStack.ST
-
-open FStar.Math.Lib
-open FStar.Mul
-open FStar.Seq
-open FStar.UInt8
-open FStar.Endianness
-open Spec.Poly1305.Lemmas
-
-#set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0"
-
-(* Field types and parameters *)
-let prime = pow2 130 - 5
-type elem = e:int{e >= 0 /\ e < prime}
-let fadd (e1:elem) (e2:elem) = (e1 + e2) % prime
-let fmul (e1:elem) (e2:elem) = (e1 * e2) % prime
-let zero : elem = 0
-let one  : elem = 1
-let op_Plus_At = fadd
-let op_Star_At = fmul
-(* Type aliases *)
-let op_Amp_Bar = UInt.logand #128
-type word = w:bytes{length w <= 16}
-type word_16 = w:bytes{length w = 16}
-type tag = word_16
-type key = lbytes 32
-type text = seq word
-
-(* Specification code *)
-let encode (w:word) =
-  (pow2 (8 * length w)) `fadd` (little_endian w)
-
-let rec poly (txt:text) (r:e:elem) : Tot elem (decreases (length txt)) =
-  if length txt = 0 then zero
-  else
-    let a = poly (Seq.tail txt) r in
-    let n = encode (Seq.head txt) in
-    (n `fadd` a) `fmul` r
-
-let encode_r (rb:word_16) =
-  (little_endian rb) &| 0x0ffffffc0ffffffc0ffffffc0fffffff
-
-let finish (a:elem) (s:word_16) : Tot tag =
-  let n = (a + little_endian s) % pow2 128 in
-  little_bytes 16ul n
-
-let rec encode_bytes (txt:bytes) : Tot text (decreases (length txt)) =
-  if length txt = 0 then createEmpty
-  else
-    let w, txt = split txt (min (length txt) 16) in
-    append_last (encode_bytes txt) w
-
-let poly1305 (msg:bytes) (k:key) : Tot tag =
-  let text = encode_bytes msg in
-  let r = encode_r (slice k 0 16) in
-  let s = slice k 16 32 in
-  finish (poly text r) s
-
-
-(* ********************* *)
-(* RFC 7539 Test Vectors *)
-(* ********************* *)
-
-#reset-options "--initial_fuel 0 --max_fuel 0 --z3rlimit 20"
-
-unfold let msg = [
-  0x43uy; 0x72uy; 0x79uy; 0x70uy; 0x74uy; 0x6fuy; 0x67uy; 0x72uy;
-  0x61uy; 0x70uy; 0x68uy; 0x69uy; 0x63uy; 0x20uy; 0x46uy; 0x6fuy;
-  0x72uy; 0x75uy; 0x6duy; 0x20uy; 0x52uy; 0x65uy; 0x73uy; 0x65uy;
-  0x61uy; 0x72uy; 0x63uy; 0x68uy; 0x20uy; 0x47uy; 0x72uy; 0x6fuy;
-  0x75uy; 0x70uy ]
-
-unfold let k = [
-  0x85uy; 0xd6uy; 0xbeuy; 0x78uy; 0x57uy; 0x55uy; 0x6duy; 0x33uy;
-  0x7fuy; 0x44uy; 0x52uy; 0xfeuy; 0x42uy; 0xd5uy; 0x06uy; 0xa8uy;
-  0x01uy; 0x03uy; 0x80uy; 0x8auy; 0xfbuy; 0x0duy; 0xb2uy; 0xfduy;
-  0x4auy; 0xbfuy; 0xf6uy; 0xafuy; 0x41uy; 0x49uy; 0xf5uy; 0x1buy ]
-
-unfold let expected = [
-  0xa8uy; 0x06uy; 0x1duy; 0xc1uy; 0x30uy; 0x51uy; 0x36uy; 0xc6uy;
-  0xc2uy; 0x2buy; 0x8buy; 0xafuy; 0x0cuy; 0x01uy; 0x27uy; 0xa9uy ]
-
-let test () : Tot bool =
-  assert_norm(List.Tot.length msg      = 34);
-  assert_norm(List.Tot.length k        = 32);
-  assert_norm(List.Tot.length expected = 16);
-  let msg      = createL msg in
-  let k        = createL k   in
-  let expected = createL expected in
-  poly1305 msg k = expected