val tokens_update_sk_nonce_same_as_update_sym_key_flag :
     is_psk : bool
  -> pattern : list message_token
  -> sk_nonce : sk_nonce_info ->
  Lemma
  (ensures (
    let sk1, nonce = tokens_update_sk_nonce is_psk pattern sk_nonce in
    let sk2 = tokens_update_sym_key_flag (fst sk_nonce) is_psk pattern in
    sk1 == sk2))
  (decreases pattern)
val tokens_update_sk_nonce_same_as_update_sym_key_flag :
     is_psk : bool
  -> pattern : list message_token
  -> sk_nonce : sk_nonce_info ->
  Lemma
  (ensures (
    let sk1, nonce = tokens_update_sk_nonce is_psk pattern sk_nonce in
    let sk2 = tokens_update_sym_key_flag (fst sk_nonce) is_psk pattern in
    sk1 == sk2))
  (decreases pattern)
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
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 *)
/
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

    is_psk: Prims.bool ->
    pattern: Prims.list Spec.Noise.Base.Definitions.message_token ->
    sk_nonce: Spec.Noise.NonceCounter.sk_nonce_info
  -> FStar.Pervasives.Lemma
      (ensures
        (let _ = Spec.Noise.NonceCounter.tokens_update_sk_nonce is_psk pattern sk_nonce in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ sk1 _ = _ in
            let sk2 =
              Spec.Noise.HandshakeFlags.tokens_update_sym_key_flag (FStar.Pervasives.Native.fst sk_nonce
                  )
                is_psk
                pattern
            in
            sk1 == sk2)
          <:
          Type0)) (decreases pattern)
Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.NonceCounter.sk_nonce_info Spec.Noise.NonceCounter.tokens_update_sk_nonce_same_as_update_sym_key_flag Spec.Noise.NonceCounter.token_update_sk_nonce Prims.unit
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