let size_publickey = 32
let size_publickey =
32
Spec.Box.fst.checked
Spec.SecretBox.fst.checked Spec.Salsa20.fst.checked Spec.Curve25519.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 FStar.Mul.fst.checked
Spec.Box.fst
module Spec.Box

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.SecretBox

#set-options "--z3rlimit 20 --max_fuel 0 --max_ifuel 0"
val size_publickey : Prims.int
Prims.int