val symmetric_state_vs : nc: Impl.Noise.Types.iconfig -> Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB
let symmetric_state_vs (nc : iconfig) = size (symmetric_state_vsv nc)
module Impl.Noise.FlatStructures

open FStar.Mul
module HS = FStar.HyperStack
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.RawIntTypes
open Lib.IntTypes

module HST = FStar.HyperStack.ST
open Lib.Sequence
module S = Lib.Sequence

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module LB = Lib.Buffer
open Lib.Buffer
open Lib.ByteBuffer

open LowStar.BufferOps

module Spec = Spec.Noise
open Spec.Noise
open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.SymmetricState
open Impl.Noise.HandshakeState

#set-options "--z3rlimit 15 --fuel 0 --ifuel 0"

/// This module provides concrete implementations for some structures used by 
/// Noise (cipher state, symmetric state...) in the form of flattened structures
/// (buffers).

(*** Key pair *)
inline_for_extraction noextract
let keypair_vsv (nc : iconfig) = private_key_vsv nc + public_key_vsv nc
let keypair_vs (nc : iconfig) = size (keypair_vsv nc)
type keypair_t (nc : iconfig) = lbuffer uint8 (keypair_vs nc)

unfold let keypair_gget_priv (#nc : iconfig) (kp : keypair_t nc) :
  GTot (private_key_t nc) =
  gsub kp 0ul (private_key_vs nc)
unfold let keypair_gget_pub (#nc : iconfig) (kp : keypair_t nc) :
  GTot (public_key_t nc) =
  gsub kp (private_key_vs nc) (public_key_vs nc)

let eval_keypair (#nc : iconfig) (h : HS.mem) (kp : keypair_t nc) :
  GTot (keypair (get_config nc)) =
  let priv = keypair_gget_priv kp in
  let pub = keypair_gget_pub kp in
  { priv = eval_private_key h priv; pub = eval_public_key h pub; }

#push-options "--fuel 1 --ifuel 1"
inline_for_extraction noextract
let keypair_get_priv (#nc : iconfig) (kp : keypair_t nc) :
  Stack (private_key_t nc)
  (requires (fun h -> live h kp))
  (ensures (fun h0 b h1 -> h0 == h1 /\ live h1 b /\
              b == keypair_gget_priv kp /\
              eval_private_key h1 b == (eval_keypair h1 kp).priv)) =
  sub kp 0ul (private_key_vs nc)

inline_for_extraction noextract
let keypair_get_pub (#nc : iconfig) (kp : keypair_t nc) :
  Stack (public_key_t nc)
  (requires (fun h -> live h kp))
  (ensures (fun h0 b h1 -> h0 == h1 /\ live h1 b /\
              b == keypair_gget_pub kp /\
              eval_public_key h1 b == (eval_keypair h1 kp).pub)) =
  sub kp (private_key_vs nc) (public_key_vs nc)

let eval_opt_split_keypair (#nc : iconfig) (h : HS.mem)
                           (priv : opt_private_key_t nc) (pub : opt_public_key_t nc) :
  GTot (option (keypair (get_config nc))) =
  if g_is_null priv || g_is_null pub then None
  else Some ({ priv = eval_private_key h priv; pub = eval_public_key h pub; })

(*** Cipher state *)
(**** Definition, getters, setters *)
inline_for_extraction noextract
let cipher_state_vsv : size_nat = aead_key_vsv
let cipher_state_vs = size cipher_state_vsv
let cipher_state_t = lbuffer uint8 cipher_state_vs

inline_for_extraction noextract
let cs_k_offs_v = 0
inline_for_extraction noextract
let cs_k_offs = size cs_k_offs_v

unfold let cs_gget_k (st : cipher_state_t) : GTot aead_key_t =
  gsub st cs_k_offs aead_key_vs

let eval_cipher_state (h : HS.mem) (st : cipher_state_t) (has_key : bool) (n : nat) :
  GTot (st_v:cipher_state{Some? st_v.k == has_key}) =
  let k_v = if has_key then Some (eval_aead_key h (cs_gget_k st)) else None in
  { k = k_v; n = n; }

(* Note that it doesn't make sense to use this function if the cipher state doesn't have a key *)
inline_for_extraction noextract
let cs_get_k (st : cipher_state_t) :
  Stack aead_key_t
  (requires (fun h -> live h st))
  (ensures (fun h0 k h1 -> h0 == h1 /\ live h1 k /\
              k == gsub st 0ul aead_key_vs)) =
  sub st cs_k_offs aead_key_vs

(*** Symmetric state *)
(**** Definition, getters, setters *)
inline_for_extraction noextract
let symmetric_state_vsv (nc : iconfig) : size_nat =
/
Spec.Noise.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.CipherState.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Impl.Noise.FlatStructures.fst
nc: Impl.Noise.Types.iconfig -> Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB
Impl.Noise.Types.iconfig Lib.IntTypes.size Impl.Noise.FlatStructures.symmetric_state_vsv Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB
let symmetric_state_vs (nc: iconfig) =
  
size (symmetric_state_vsv nc)