val send_tokens_update_sk_nonce_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> pattern : list message_token
  -> state : handshake_state nc ->
  Lemma
  (ensures (
    match send_message_tokens initiator is_psk pattern state with
    | Fail _ -> True
    | Res (_, state1) ->
      let sk_nonce = get_has_sk_nonce state in
      let sk_nonce1 = get_has_sk_nonce state1 in
      sk_nonce1 == tokens_update_sk_nonce is_psk pattern sk_nonce))
  (decreases pattern)
val send_tokens_update_sk_nonce_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> pattern : list message_token
  -> state : handshake_state nc ->
  Lemma
  (ensures (
    match send_message_tokens initiator is_psk pattern state with
    | Fail _ -> True
    | Res (_, state1) ->
      let sk_nonce = get_has_sk_nonce state in
      let sk_nonce1 = get_has_sk_nonce state1 in
      sk_nonce1 == tokens_update_sk_nonce is_psk pattern sk_nonce))
  (decreases pattern)
let rec send_tokens_update_sk_nonce_lem #nc initiator is_psk pattern state =
  match pattern with
  | [] -> ()
  | tk :: pattern1 ->
    send_token_update_nonce_lem initiator is_psk tk state;
    match send_message_token initiator is_psk tk state with
    | Fail _ -> ()
    | Res (msg, state1) ->
      send_tokens_update_sk_nonce_lem initiator is_psk pattern1 state1
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))

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)

(**** send *)

let send_token_update_nonce_lem #nc initiator is_psk tk state = ()
/
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

    initiator: Prims.bool ->
    is_psk: Prims.bool ->
    pattern: Prims.list Spec.Noise.Base.Definitions.message_token ->
    state: Spec.Noise.Base.Definitions.handshake_state nc
  -> FStar.Pervasives.Lemma
      (ensures
        ((match Spec.Noise.Base.Definitions.send_message_tokens initiator is_psk pattern state with
            | Spec.Noise.Base.Definitions.Fail #_ #_ _ -> Prims.l_True
            | Spec.Noise.Base.Definitions.Res
              #_
              #_
              (FStar.Pervasives.Native.Mktuple2 #_ #_ _ state1) ->
              let sk_nonce = Spec.Noise.NonceCounter.get_has_sk_nonce state in
              let sk_nonce1 = Spec.Noise.NonceCounter.get_has_sk_nonce state1 in
              sk_nonce1 == Spec.Noise.NonceCounter.tokens_update_sk_nonce is_psk pattern sk_nonce)
          <:
          Type0)) (decreases pattern)
Spec.Noise.CryptoPrimitives.config Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.Base.Definitions.handshake_state Spec.Noise.Base.Definitions.send_message_token Spec.Noise.Base.Definitions.error Lib.ByteSequence.bytes Spec.Noise.NonceCounter.send_tokens_update_sk_nonce_lem Prims.unit Spec.Noise.NonceCounter.send_token_update_nonce_lem
let rec send_tokens_update_sk_nonce_lem #nc initiator is_psk pattern state =
  
match pattern with
| [] -> ()
| tk :: pattern1 ->
  send_token_update_nonce_lem initiator is_psk tk state;
  match send_message_token initiator is_psk tk state with
  | Fail _ -> ()
  | Res (msg, state1) -> send_tokens_update_sk_nonce_lem initiator is_psk pattern1 state1