val token_update_nonce (has_sk is_psk: bool) (tk: message_token) (nonce: nat) : nat
val token_update_nonce (has_sk is_psk: bool) (tk: message_token) (nonce: nat) : nat
let token_update_nonce (has_sk is_psk : bool) (tk : message_token)
                       (nonce : nat) : nat =
  match tk with
  | S -> if has_sk then nonce + 1 else nonce
  | E -> if is_psk then 0 else nonce
  | _ -> 0
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

let get_has_sk_nonce (#nc : config) (state : handshake_state nc) : sk_nonce_info =
  has_symmetric_key state, get_nonce state

(*** Definitions *)
/
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

    has_sk: Prims.bool ->
    is_psk: Prims.bool ->
    tk: Spec.Noise.Base.Definitions.message_token ->
    nonce: Prims.nat
  -> Prims.nat
Prims.bool Spec.Noise.Base.Definitions.message_token Prims.nat Prims.op_Addition
let token_update_nonce (has_sk is_psk: bool) (tk: message_token) (nonce: nat) : nat =
  
match tk with
| S -> if has_sk then nonce + 1 else nonce
| E -> if is_psk then 0 else nonce
| _ -> 0