val keypair_vs : nc: Impl.Noise.Types.iconfig -> Lib.IntTypes.size_t
let keypair_vs (nc : iconfig) = size (keypair_vsv nc)
module Impl.Noise.FlatStructures

open FStar.Mul
module HS = FStar.HyperStack
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

module HST = FStar.HyperStack.ST
open Lib.Sequence
module S = Lib.Sequence

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module LB = Lib.Buffer
open Lib.Buffer
open Lib.ByteBuffer

open LowStar.BufferOps

module Spec = Spec.Noise
open Spec.Noise
open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.SymmetricState
open Impl.Noise.HandshakeState

#set-options "--z3rlimit 15 --fuel 0 --ifuel 0"

/// This module provides concrete implementations for some structures used by 
/// Noise (cipher state, symmetric state...) in the form of flattened structures
/// (buffers).

(*** Key pair *)
inline_for_extraction noextract
/
Spec.Noise.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.CipherState.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Impl.Noise.FlatStructures.fst
nc: Impl.Noise.Types.iconfig -> Lib.IntTypes.size_t
Impl.Noise.Types.iconfig Lib.IntTypes.size Impl.Noise.FlatStructures.keypair_vsv Lib.IntTypes.size_t
let keypair_vs (nc: iconfig) =
  
size (keypair_vsv nc)