val message_update_nonce (has_sk is_psk: bool) (pattern: list message_token) (nonce: nat) : nat
val message_update_nonce (has_sk is_psk: bool) (pattern: list message_token) (nonce: nat) : nat
let message_update_nonce (has_sk is_psk : bool) (pattern : list message_token)
                         (nonce : nat) : nat =
  let has_sk1, nonce1 = tokens_update_sk_nonce is_psk pattern (has_sk, nonce) in
  if has_sk1 then nonce1 + 1 else nonce1
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 *)
inline_for_extraction noextract
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

inline_for_extraction noextract
let token_update_sk_nonce (is_psk : bool) (tk : message_token)
                          (sk_nonce : sk_nonce_info) : sk_nonce_info  =
  let has_sk, nonce = sk_nonce in
  let has_sk1 = token_update_sym_key_flag has_sk is_psk tk in
  let nonce1 = token_update_nonce has_sk is_psk tk nonce in
  has_sk1, nonce1

(** Updates the symmetric key boolean and nonce over a list of tokens *)
[@(strict_on_arguments [1])]
inline_for_extraction noextract
let rec tokens_update_sk_nonce (is_psk : bool) (pattern : list message_token)
                               (sk_nonce : sk_nonce_info) :
  Tot sk_nonce_info (decreases pattern) =
  match pattern with
  | [] -> sk_nonce
  | tk :: pattern1 ->
    let sk_nonce1 = token_update_sk_nonce is_psk tk sk_nonce in
    tokens_update_sk_nonce is_psk pattern1 sk_nonce1

inline_for_extraction noextract
let tokens_update_nonce (has_sk is_psk : bool) (pattern : list message_token)
                        (nonce : nat) :
  Tot nat =
  snd (tokens_update_sk_nonce is_psk pattern (has_sk, nonce))

(** Updates the nonce over a message with payload *)
/
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 ->
    pattern: Prims.list Spec.Noise.Base.Definitions.message_token ->
    nonce: Prims.nat
  -> Prims.nat
Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Prims.nat Prims.op_Addition Spec.Noise.NonceCounter.sk_nonce_info Spec.Noise.NonceCounter.tokens_update_sk_nonce FStar.Pervasives.Native.Mktuple2
let message_update_nonce (has_sk is_psk: bool) (pattern: list message_token) (nonce: nat) : nat =
  
let has_sk1, nonce1 = tokens_update_sk_nonce is_psk pattern (has_sk, nonce) in
if has_sk1 then nonce1 + 1 else nonce1