val crypto_bytes:r: size_t{v r == FP.crypto_bytes FP.Frodo1344}
let crypto_bytes :r:size_t{v r == FP.crypto_bytes FP.Frodo1344} =
  crypto_bytes FP.Frodo1344
val crypto_bytes:r: size_t{v r == FP.crypto_bytes FP.Frodo1344}
let crypto_bytes:r: size_t{v r == FP.crypto_bytes FP.Frodo1344} =
crypto_bytes FP.Frodo1344
Hacl.Frodo1344.fst.checked
Spec.Frodo.Params.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Frodo.Params.fst.checked Hacl.Frodo.KEM.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Frodo1344.fst
Hacl.Impl.Frodo.Params.crypto_bytes Spec.Frodo.Params.Frodo1344
module Hacl.Frodo1344

open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open Hacl.Frodo.KEM
open Hacl.Impl.Frodo.Params

module FP = Spec.Frodo.Params

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val crypto_bytes:r: size_t{v r == FP.crypto_bytes FP.Frodo1344}
r:
Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB
  {Lib.IntTypes.v r == Spec.Frodo.Params.crypto_bytes Spec.Frodo.Params.Frodo1344}