val handshake_state_same_keys (#nc: config) (st0 st1: handshake_state nc) : Type0
val handshake_state_same_keys (#nc: config) (st0 st1: handshake_state nc) : Type0
let handshake_state_same_keys (#nc : config) (st0 st1 : handshake_state nc) : Type0 =
  st0.static == st1.static /\
  st0.ephemeral == st1.ephemeral /\
  st0.remote_static == st1.remote_static /\
  st0.remote_ephemeral == st1.remote_ephemeral /\
  st0.preshared == st1.preshared
module Spec.Noise.Base.Lemmas

open FStar.Mul

open Lib.IntTypes
open Lib.RawIntTypes
open Lib.ByteSequence
open Lib.Sequence

open Spec.Noise.CryptoPrimitives
open Spec.Noise.Base.Definitions

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

(*** Initialization *)

val initialize_unfold_lem :
     #nc : config
  -> protocol_name : hashable nc
  -> prologue : hashable nc
  -> static_key : option (keypair nc)
  -> ephemeral_key : option (keypair nc)
  -> preshared_key : option preshared_key ->
  Lemma(
    initialize #nc protocol_name prologue static_key ephemeral_key preshared_key ==
    initialize_handshake_state protocol_name prologue static_key ephemeral_key None None preshared_key)

(*** Recursive definitions unfoldings *)

(**** Premessages *)

val send_premessage_tokens_nil_lem :
     #nc : config
  -> st : handshake_state nc ->
  Lemma (send_premessage_tokens #nc [] st == Res (lbytes_empty, st))

val send_premessage_tokens_unfold_lem :
     #nc : config
  -> tk : premessage_token
  -> tokens : list premessage_token
  -> st : handshake_state nc ->
  Lemma (
    send_premessage_tokens #nc (tk :: tokens) st ==
    begin match send_premessage_token tk st with
    | Fail e -> Fail e
    | Res (msg1, st1) ->
      match send_premessage_tokens tokens st1 with
      | Fail e -> Fail e
      | Res (msg2, st2) ->
        Res (Seq.append msg1 msg2, st2)
    end)

val receive_premessage_tokens_nil_lem :
     #nc : config
  -> st : handshake_state nc ->
  Lemma (receive_premessage_tokens #nc [] Seq.empty st == Res st)

val receive_premessage_tokens_unfold_lem :
     #nc : config
  -> tk : premessage_token
  -> tokens : list premessage_token
  -> msg : bytes
  -> st : handshake_state nc ->
  Lemma (
    receive_premessage_tokens #nc (tk :: tokens) msg st ==
    begin
    if length msg <> List.Tot.length (tk :: tokens) * public_key_size nc
    then Fail PE_input_size else
    let msg1, msg2 = split_bytes msg (public_key_size nc) in
    match receive_premessage_token tk msg1 st with
    | Fail e -> Fail e
    | Res st' -> receive_premessage_tokens tokens msg2 st'
    end)

(**** Messages *)

val send_message_tokens_nil_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> st : handshake_state nc ->
  Lemma (send_message_tokens #nc initiator is_psk [] st == Res (lbytes_empty, st))

val send_message_tokens_unfold_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> tk : message_token
  -> tokens : list message_token
  -> st : handshake_state nc ->
  Lemma (
    send_message_tokens #nc initiator is_psk (tk :: tokens) st ==
    begin match send_message_token initiator is_psk tk st with
    | Fail e -> Fail e
    | Res (msg, st') ->
      match send_message_tokens initiator is_psk tokens st' with
      | Fail e -> Fail e
      | Res (msg', st'') ->
        Res (Seq.append msg msg', st'')
    end)

// We can't directly use an equality and have to write a match because the
// return types aren't exactly the same
val send_message_tokens_one_token_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> tk : message_token
  -> st : handshake_state nc ->
  Lemma (
    send_message_tokens #nc initiator is_psk [tk] st ==
    begin match send_message_token initiator is_psk tk st with
    | Fail e -> Fail e
    | Res (msg', st') -> Res (msg', st')
    end)

val receive_message_tokens_nil_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> msg : bytes
  -> st : handshake_state nc ->
  Lemma (receive_message_tokens #nc initiator is_psk [] msg st == Res (msg, st))

val receive_message_tokens_unfold_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> tk : message_token
  -> tokens : list message_token
  -> msg : bytes
  -> st : handshake_state nc ->
  Lemma (
    receive_message_tokens #nc initiator is_psk (tk :: tokens) msg st ==
    begin match receive_message_token initiator is_psk tk msg st with
    | Fail e -> Fail e
    | Res (msg', st') ->
      match receive_message_tokens initiator is_psk tokens msg' st' with
      | Fail e -> Fail e
      | Res (msg'', st'') ->
        Res (msg'', st'')
    end)

val receive_message_tokens_one_token_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> tk : message_token
  -> msg : bytes
  -> st : handshake_state nc ->
  Lemma (
    receive_message_tokens #nc initiator is_psk [tk] msg st ==
    begin match receive_message_token initiator is_psk tk msg st with
    | Fail e -> Fail e
    | Res (msg', st') -> Res (msg', st')
    end)


(*** Messages with payload *)

val send_message_tokens_with_payload_unfold_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> pattern : list message_token
  -> payload : plain_message nc
  -> st : handshake_state nc ->
  Lemma(
    send_message_tokens_with_payload initiator is_psk pattern payload st ==
    begin match send_message_tokens initiator is_psk pattern st with
    | Fail e -> Fail e
    | Res (msg1, st1) ->
      match encrypt_and_hash payload st1.sym_state with
      | Fail x -> Fail x
      | Res (msg2, sym_st1) ->
        Res (Seq.append msg1 msg2, {st1 with sym_state = sym_st1})
    end)

(*** Error classes *)

(**** Cipher *)
val encrypt_with_ad_error_lem :
     nc:config   
  -> aad:aead_aad nc
  -> plain:bytes
  -> cs:cipher_state ->
  Lemma(
    match encrypt_with_ad nc aad plain cs with
    | Res _
    | Fail Saturated_nonce
    | Fail Input_size -> True
    | _ -> False) 

val decrypt_with_ad_error_lem :
     nc:config
  -> aad:aead_aad nc
  -> cipher:bytes
  -> cs:cipher_state ->
  Lemma(
    match decrypt_with_ad nc aad cipher cs with
    | Res _
    | Fail Saturated_nonce
    | Fail Input_size
    | Fail Decryption -> True
    | _ -> False) 

(**** Premessages *)

val send_premessage_tokens_error_lem :
     #nc : config
  -> tokens : list premessage_token
  -> st : handshake_state nc ->
  Lemma
  (ensures (
    match send_premessage_tokens #nc tokens st with
    | Res _
    | Fail PE_no_key -> True
    | _ -> False))
  (decreases tokens)

val receive_premessage_tokens_error_lem :
     #nc : config
  -> tokens:list premessage_token
  -> msg:bytes
  -> st:handshake_state nc ->
  Lemma
  (ensures (
    match receive_premessage_tokens #nc tokens msg st with
    | Res _
    | Fail PE_already_key | Fail PE_input_size -> True
    | _ -> False))
  (decreases tokens)


(**** Messages *)
val send_message_tokens_error_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> tokens : list message_token
  -> st : handshake_state nc ->
  Lemma
  (ensures (
    match send_message_tokens #nc initiator is_psk tokens st with
    | Res _
    | Fail No_key | Fail Input_size | Fail DH | Fail Saturated_nonce -> True
    | _ -> False))
  (decreases tokens)

val send_message_tokens_with_payload_error_lem :
     #nc : config
  -> initiator : bool
  -> is_psk : bool
  -> pattern : list message_token
  -> payload : plain_message nc
  -> st : handshake_state nc ->
  Lemma(
    match send_message_tokens_with_payload initiator is_psk pattern payload st with
    | Res _ -> True
    | Fail No_key | Fail Input_size | Fail DH | Fail Saturated_nonce -> True
    | _ -> False)

(*** Framing lemmas *)

let some_implies_same (#a : Type0) (x y : option a) : Type0 =
  match x, y with
  | Some x, Some y -> x == y
  | None, None -> True
  | None, Some _ -> True
  | Some _, None -> False
/
Spec.Noise.CryptoPrimitives.fsti.checked Spec.Noise.Base.Definitions.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.Base.Lemmas.fsti

    st0: Spec.Noise.Base.Definitions.handshake_state nc ->
    st1: Spec.Noise.Base.Definitions.handshake_state nc
  -> Type0
Spec.Noise.CryptoPrimitives.config Spec.Noise.Base.Definitions.handshake_state Prims.l_and Prims.eq2 FStar.Pervasives.Native.option Spec.Noise.CryptoPrimitives.keypair Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__static Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__ephemeral Spec.Noise.CryptoPrimitives.public_key Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__remote_static Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__remote_ephemeral Spec.Noise.CryptoPrimitives.preshared_key Spec.Noise.Base.Definitions.__proj__Mkhandshake_state__item__preshared
let handshake_state_same_keys (#nc: config) (st0 st1: handshake_state nc) : Type0 =
  
st0.static == st1.static /\ st0.ephemeral == st1.ephemeral /\ st0.remote_static == st1.remote_static /\
st0.remote_ephemeral == st1.remote_ephemeral /\ st0.preshared == st1.preshared