val get_has_sk_nonce (#nc: config) (state: handshake_state nc) : sk_nonce_info
val get_has_sk_nonce (#nc: config) (state: handshake_state nc) : sk_nonce_info
let get_has_sk_nonce (#nc : config) (state : handshake_state nc) : sk_nonce_info =
  has_symmetric_key state, get_nonce state
module Spec.Noise.NonceCounter
open FStar.Mul

open Lib.ByteSequence
open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.HandshakeFlags

/// The following file implements functions and predicates to compute and reason
/// about the value of the nonce counter at every step of the handshake.

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

inline_for_extraction noextract
type sk_nonce_info = bool & nat
/
Spec.Noise.HandshakeFlags.fsti.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.fst.checked prims.fst.checked Lib.ByteSequence.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.NonceCounter.fsti
state: Spec.Noise.Base.Definitions.handshake_state nc -> Spec.Noise.NonceCounter.sk_nonce_info
Spec.Noise.CryptoPrimitives.config Spec.Noise.Base.Definitions.handshake_state FStar.Pervasives.Native.Mktuple2 Prims.bool Prims.nat Spec.Noise.Base.Definitions.has_symmetric_key Spec.Noise.Base.Definitions.get_nonce Spec.Noise.NonceCounter.sk_nonce_info
let get_has_sk_nonce (#nc: config) (state: handshake_state nc) : sk_nonce_info =
  
has_symmetric_key state, get_nonce state