val 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))
val 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))
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)
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)
/
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
kp: Impl.Noise.FlatStructures.keypair_t nc
  -> FStar.HyperStack.ST.Stack (Impl.Noise.Types.public_key_t nc)
Impl.Noise.Types.iconfig Impl.Noise.FlatStructures.keypair_t Lib.Buffer.sub Lib.Buffer.MUT Lib.IntTypes.uint8 Impl.Noise.FlatStructures.keypair_vs Impl.Noise.Types.private_key_vs Impl.Noise.Types.public_key_vs Lib.Buffer.lbuffer_t Impl.Noise.Types.public_key_t FStar.Monotonic.HyperStack.mem Lib.Buffer.live Prims.l_and Prims.eq2 Impl.Noise.FlatStructures.keypair_gget_pub Spec.Noise.CryptoPrimitives.public_key Impl.Noise.Types.get_config Impl.Noise.Types.eval_public_key Spec.Noise.CryptoPrimitives.__proj__Mkkeypair__item__pub Impl.Noise.FlatStructures.eval_keypair
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)