val message_update_nonce_as_update_sym_key_flag_expr :
     has_sk : bool
  -> is_psk : bool
  -> pattern : list message_token
  -> nonce : nat ->
  Lemma (
    let has_sk1 = tokens_update_sym_key_flag has_sk is_psk pattern in
    let nonce1 = tokens_update_nonce has_sk is_psk pattern nonce in
    message_update_nonce has_sk is_psk pattern nonce ==
      (if has_sk1 then nonce1 + 1 else nonce1))
val message_update_nonce_as_update_sym_key_flag_expr :
     has_sk : bool
  -> is_psk : bool
  -> pattern : list message_token
  -> nonce : nat ->
  Lemma (
    let has_sk1 = tokens_update_sym_key_flag has_sk is_psk pattern in
    let nonce1 = tokens_update_nonce has_sk is_psk pattern nonce in
    message_update_nonce has_sk is_psk pattern nonce ==
      (if has_sk1 then nonce1 + 1 else nonce1))
let message_update_nonce_as_update_sym_key_flag_expr has_sk is_psk pattern nonce =
  tokens_update_sk_nonce_same_as_update_sym_key_flag is_psk pattern (has_sk, nonce)
module Spec.Noise.NonceCounter
open FStar.Mul

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base
open Spec.Noise.HandshakeFlags

friend Spec.Noise.Base.Definitions

#set-options "--z3rlimit 25 --fuel 1 --ifuel 1"

(*** Lemmas *)

let rec tokens_update_sk_nonce_same_as_update_sym_key_flag is_psk pattern sk_nonce =
  match pattern with
  | [] -> ()
  | tk :: pattern1 ->
    let sk_nonce1 = token_update_sk_nonce is_psk tk sk_nonce in
    tokens_update_sk_nonce_same_as_update_sym_key_flag is_psk pattern1 sk_nonce1

val message_update_nonce_as_update_sym_key_flag_expr :
     has_sk : bool
  -> is_psk : bool
  -> pattern : list message_token
  -> nonce : nat ->
  Lemma (
    let has_sk1 = tokens_update_sym_key_flag has_sk is_psk pattern in
    let nonce1 = tokens_update_nonce has_sk is_psk pattern nonce in
    message_update_nonce has_sk is_psk pattern nonce ==
      (if has_sk1 then nonce1 + 1 else nonce1))
/
Spec.Noise.HandshakeFlags.fsti.checked Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.Definitions.fst.checked Spec.Noise.Base.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Noise.NonceCounter.fst

    has_sk: Prims.bool ->
    is_psk: Prims.bool ->
    pattern: Prims.list Spec.Noise.Base.Definitions.message_token ->
    nonce: Prims.nat
  -> FStar.Pervasives.Lemma
    (ensures
      (let has_sk1 = Spec.Noise.HandshakeFlags.tokens_update_sym_key_flag has_sk is_psk pattern in
        let nonce1 = Spec.Noise.NonceCounter.tokens_update_nonce has_sk is_psk pattern nonce in
        Spec.Noise.NonceCounter.message_update_nonce has_sk is_psk pattern nonce ==
        (match has_sk1 with
          | true -> nonce1 + 1
          | _ -> nonce1)))
Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Prims.nat Spec.Noise.NonceCounter.tokens_update_sk_nonce_same_as_update_sym_key_flag FStar.Pervasives.Native.Mktuple2 Prims.unit
let message_update_nonce_as_update_sym_key_flag_expr has_sk is_psk pattern nonce =
  
tokens_update_sk_nonce_same_as_update_sym_key_flag is_psk pattern (has_sk, nonce)