val blake2_update'
      (a: alg)
      (kk: size_nat{kk <= max_key a})
      (k: lbytes kk)
      (d: bytes{if kk = 0 then length d <= max_limb a else length d + (size_block a) <= max_limb a})
      (s: state a)
    : Tot (state a)
let blake2_update'
  (a:alg)
  (kk:size_nat{kk <= max_key a})
  (k:lbytes kk)
  (d:bytes{if kk = 0 then length d <= max_limb a else length d + (size_block a) <= max_limb a})
  (s:state a): Tot (state a)
= let ll = length d in
  let key_block: bytes = if kk > 0 then blake2_key_block a kk k else Seq.empty in
  blake2_update_blocks a 0 (key_block `Seq.append` d) s
val blake2_update'
      (a: alg)
      (kk: size_nat{kk <= max_key a})
      (k: lbytes kk)
      (d: bytes{if kk = 0 then length d <= max_limb a else length d + (size_block a) <= max_limb a})
      (s: state a)
    : Tot (state a)
let blake2_update'
      (a: alg)
      (kk: size_nat{kk <= max_key a})
      (k: lbytes kk)
      (d: bytes{if kk = 0 then length d <= max_limb a else length d + (size_block a) <= max_limb a})
      (s: state a)
    : Tot (state a) =
let ll = length d in
let key_block:bytes = if kk > 0 then blake2_key_block a kk k else Seq.empty in
blake2_update_blocks a 0 (key_block `Seq.append` d) s
Spec.Blake2.Alternative.fsti.checked
Spec.Blake2.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Spec.Blake2.Alternative.fsti
Spec.Blake2.alg Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThanOrEqual Spec.Blake2.max_key Lib.ByteSequence.lbytes Lib.ByteSequence.bytes Prims.op_Equality Prims.int Lib.Sequence.length Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Spec.Blake2.max_limb Prims.bool Prims.op_Addition Spec.Blake2.size_block Spec.Blake2.state Spec.Blake2.blake2_update_blocks FStar.Seq.Base.append Lib.IntTypes.int_t Lib.Sequence.seq Prims.op_GreaterThan Spec.Blake2.blake2_key_block FStar.Seq.Base.empty Prims.nat
module Spec.Blake2.Alternative

open Spec.Blake2

open Lib.IntTypes
open Lib.ByteSequence
open Lib.Sequence

let blake2_update'
  (a:alg)
  (kk:size_nat{kk <= max_key a})
  (k:lbytes kk)
  (d:bytes{if kk = 0 then length d <= max_limb a else length d + (size_block a) <= max_limb a})
val blake2_update'
      (a: alg)
      (kk: size_nat{kk <= max_key a})
      (k: lbytes kk)
      (d: bytes{if kk = 0 then length d <= max_limb a else length d + (size_block a) <= max_limb a})
      (s: state a)
    : Tot (state a)

    a: Spec.Blake2.alg ->
    kk: Lib.IntTypes.size_nat{kk <= Spec.Blake2.max_key a} ->
    k: Lib.ByteSequence.lbytes kk ->
    d:
      Lib.ByteSequence.bytes
        { (match kk = 0 with
            | true -> Lib.Sequence.length d <= Spec.Blake2.max_limb a
            | _ -> Lib.Sequence.length d + Spec.Blake2.size_block a <= Spec.Blake2.max_limb a)
          <:
          Type0 } ->
    s: Spec.Blake2.state a
  -> Spec.Blake2.state a