val tokens_update_sk_nonce_decompose_lem (is_psk : bool)
                                         (tokens1 tokens2 : list message_token)
                                         (skn : sk_nonce_info) :
  Lemma
  (requires True)
  (ensures (
    let skn1 = tokens_update_sk_nonce is_psk tokens1 skn in
    let skn2 = tokens_update_sk_nonce is_psk tokens2 skn1 in
    let skn2' = tokens_update_sk_nonce is_psk (List.Tot.append tokens1 tokens2) skn in
    skn2' = skn2))
  (decreases tokens1)
val tokens_update_sk_nonce_decompose_lem (is_psk : bool)
                                         (tokens1 tokens2 : list message_token)
                                         (skn : sk_nonce_info) :
  Lemma
  (requires True)
  (ensures (
    let skn1 = tokens_update_sk_nonce is_psk tokens1 skn in
    let skn2 = tokens_update_sk_nonce is_psk tokens2 skn1 in
    let skn2' = tokens_update_sk_nonce is_psk (List.Tot.append tokens1 tokens2) skn in
    skn2' = skn2))
  (decreases tokens1)
let rec tokens_update_sk_nonce_decompose_lem is_psk tokens1 tokens2 skn =
  match tokens1 with
  | [] -> ()
  | tk :: tokens1' ->
    let skn' = token_update_sk_nonce is_psk tk skn in
    tokens_update_sk_nonce_decompose_lem is_psk tokens1' tokens2 skn'
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 = ()

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

let send_message_update_nonce_lem #nc initiator is_psk pattern payload state =
  send_tokens_update_sk_nonce_lem initiator is_psk pattern state

(**** receive *)

let receive_token_update_nonce_lem #nc initiator is_psk tk message state = ()

let rec receive_tokens_update_sk_nonce_lem #nc initiator is_psk pattern message state =
  match pattern with
  | [] -> ()
  | tk :: pattern1 ->
    receive_token_update_nonce_lem initiator is_psk tk message state;
    match receive_message_token initiator is_psk tk message state with
    | Fail _ -> ()
    | Res (msg1, state1) ->
      receive_tokens_update_sk_nonce_lem initiator is_psk pattern1 msg1 state1

let receive_message_update_nonce_lem #nc initiator is_psk pattern message state =
  receive_tokens_update_sk_nonce_lem initiator is_psk pattern message state


(**** Decomposition 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 ->
    tokens1: Prims.list Spec.Noise.Base.Definitions.message_token ->
    tokens2: Prims.list Spec.Noise.Base.Definitions.message_token ->
    skn: Spec.Noise.NonceCounter.sk_nonce_info
  -> FStar.Pervasives.Lemma
      (ensures
        (let skn1 = Spec.Noise.NonceCounter.tokens_update_sk_nonce is_psk tokens1 skn in
          let skn2 = Spec.Noise.NonceCounter.tokens_update_sk_nonce is_psk tokens2 skn1 in
          let skn2' =
            Spec.Noise.NonceCounter.tokens_update_sk_nonce is_psk (tokens1 @ tokens2) skn
          in
          skn2' = skn2)) (decreases tokens1)
Prims.bool Prims.list Spec.Noise.Base.Definitions.message_token Spec.Noise.NonceCounter.sk_nonce_info Spec.Noise.NonceCounter.tokens_update_sk_nonce_decompose_lem Spec.Noise.NonceCounter.token_update_sk_nonce Prims.unit
let rec tokens_update_sk_nonce_decompose_lem is_psk tokens1 tokens2 skn =
  
match tokens1 with
| [] -> ()
| tk :: tokens1' ->
  let skn' = token_update_sk_nonce is_psk tk skn in
  tokens_update_sk_nonce_decompose_lem is_psk tokens1' tokens2 skn'