val update_keypair_opt :
  #nc : iconfig ->
  #b : bool ->
  dst : keypair_m nc ->
  src_priv : private_key_t_or_unit nc b ->
  src_pub : public_key_t_or_unit nc b ->
  Stack unit
  (requires (fun h ->
    live_kpm h dst /\
    lbuffer_or_unit_live h src_priv /\ lbuffer_or_unit_live h src_pub /\
    disjoint_kpm dst /\
    kpm_loc_disjoint dst (B.loc_union (lbuffer_or_unit_loc src_priv)
                                      (lbuffer_or_unit_loc src_pub)) /\
    ((g_is_null (kpm_get_priv dst) || g_is_null (kpm_get_pub dst)) ==> not b)
    ))
  (ensures (fun h0 _ h1 ->
    (if not b then modifies0 h0 h1
     else modifies (B.loc_union (loc (kpm_get_priv dst)) (loc (kpm_get_pub dst))) h0 h1) /\
    begin
    if b
    then eval_keypair_m h1 dst == Some?.v (keys_t_or_unit_to_keypair h0 src_priv src_pub)
    else True
    end))
val update_keypair_opt :
  #nc : iconfig ->
  #b : bool ->
  dst : keypair_m nc ->
  src_priv : private_key_t_or_unit nc b ->
  src_pub : public_key_t_or_unit nc b ->
  Stack unit
  (requires (fun h ->
    live_kpm h dst /\
    lbuffer_or_unit_live h src_priv /\ lbuffer_or_unit_live h src_pub /\
    disjoint_kpm dst /\
    kpm_loc_disjoint dst (B.loc_union (lbuffer_or_unit_loc src_priv)
                                      (lbuffer_or_unit_loc src_pub)) /\
    ((g_is_null (kpm_get_priv dst) || g_is_null (kpm_get_pub dst)) ==> not b)
    ))
  (ensures (fun h0 _ h1 ->
    (if not b then modifies0 h0 h1
     else modifies (B.loc_union (loc (kpm_get_priv dst)) (loc (kpm_get_pub dst))) h0 h1) /\
    begin
    if b
    then eval_keypair_m h1 dst == Some?.v (keys_t_or_unit_to_keypair h0 src_priv src_pub)
    else True
    end))
let update_keypair_opt #nc #b dst src_priv src_pub =
  if b then
    begin
    update_sub ((kpm_get_priv dst) <: private_key_t nc) 0ul (private_key_vs nc)
               (src_priv <: private_key_t nc);
    update_sub ((kpm_get_pub dst) <: public_key_t nc) 0ul (public_key_vs nc)
               (src_pub <: public_key_t nc)
    end
  else ()
module Impl.Noise.HandshakeState

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
open Lib.ByteSequence

module B = LowStar.Buffer
open Lib.Buffer
open Lib.ByteBuffer

open LowStar.BufferOps

module Spec = Spec.Noise
open Spec.Noise
open Meta.Noise
open Impl.Noise.Types
open Impl.Noise.CipherState
open Impl.Noise.HKDF
open Impl.Noise.SymmetricState
open Impl.Noise.TypeOrUnit

friend Spec.Noise.Base.Definitions

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

(* Align the .fst and the .fsti *)
let _align_beg = ()

(*** Initialization *)
// TODO: move. Note that there are functions with the same name in Impl.Noise.Types (those from Impl.Noise.Types will be removed)
inline_for_extraction noextract
val update_sub_opt :
  #a : Type0 ->
  (* Warning: len must be valid for extraction *)
  #len : size_t ->
  #b : bool ->
  dst : lbuffer_or_null a len ->
  src : type_or_unit (lbuffer a len) b ->
  Stack unit
  (requires (fun h ->
    live h dst /\ lbuffer_or_unit_live h src /\
    B.(loc_disjoint (loc_buffer (dst <: buffer a)) (lbuffer_or_unit_loc src)) /\
    (b ==> not (g_is_null dst))))
  (ensures (fun h0 _ h1 ->
    (if not b then modifies0 h0 h1 else modifies1 dst h0 h1) /\
    (if not b then
      (if g_is_null dst then True else h1.[|dst <: lbuffer_t MUT a len|] `S.equal`
                                    h0.[|dst <: lbuffer_t MUT a len|])
     else h1.[|dst <: lbuffer_t MUT a len|] `S.equal` lbuffer_or_unit_to_seq h0 src)))
let update_sub_opt #a #len #b dst src =
  if b then update_sub (dst <: lbuffer_t MUT a len) 0ul len (src <: lbuffer_t MUT a len)
  else ()

inline_for_extraction noextract
val update_keypair_opt :
  #nc : iconfig ->
  #b : bool ->
  dst : keypair_m nc ->
  src_priv : private_key_t_or_unit nc b ->
  src_pub : public_key_t_or_unit nc b ->
  Stack unit
  (requires (fun h ->
    live_kpm h dst /\
    lbuffer_or_unit_live h src_priv /\ lbuffer_or_unit_live h src_pub /\
    disjoint_kpm dst /\
    kpm_loc_disjoint dst (B.loc_union (lbuffer_or_unit_loc src_priv)
                                      (lbuffer_or_unit_loc src_pub)) /\
    ((g_is_null (kpm_get_priv dst) || g_is_null (kpm_get_pub dst)) ==> not b)
    ))
  (ensures (fun h0 _ h1 ->
    (if not b then modifies0 h0 h1
     else modifies (B.loc_union (loc (kpm_get_priv dst)) (loc (kpm_get_pub dst))) h0 h1) /\
    begin
    if b
    then eval_keypair_m h1 dst == Some?.v (keys_t_or_unit_to_keypair h0 src_priv src_pub)
    else True
    end))
/
Spec.Noise.Base.Definitions.fst.checked Spec.Noise.fst.checked prims.fst.checked Meta.Noise.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.Memzero0.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.TypeOrUnit.fsti.checked Impl.Noise.SymmetricState.fsti.checked Impl.Noise.HKDF.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 FStar.Ghost.fsti.checked
Impl.Noise.HandshakeState.fst

    dst: Impl.Noise.Types.keypair_m nc ->
    src_priv: Impl.Noise.TypeOrUnit.private_key_t_or_unit nc b ->
    src_pub: Impl.Noise.TypeOrUnit.public_key_t_or_unit nc b
  -> FStar.HyperStack.ST.Stack Prims.unit
Impl.Noise.Types.iconfig Prims.bool Impl.Noise.Types.keypair_m Impl.Noise.TypeOrUnit.private_key_t_or_unit Impl.Noise.TypeOrUnit.public_key_t_or_unit Lib.Buffer.update_sub Lib.Buffer.MUT Lib.IntTypes.uint8 Impl.Noise.Types.public_key_vs Impl.Noise.Types.kpm_get_pub Impl.Noise.Types.public_key_t FStar.UInt32.__uint_to_t Prims.unit Impl.Noise.Types.private_key_vs Impl.Noise.Types.kpm_get_priv Impl.Noise.Types.private_key_t
let update_keypair_opt #nc #b dst src_priv src_pub =
  
if b
then
  (update_sub ((kpm_get_priv dst) <: private_key_t nc)
      0ul
      (private_key_vs nc)
      (src_priv <: private_key_t nc);
    update_sub ((kpm_get_pub dst) <: public_key_t nc)
      0ul
      (public_key_vs nc)
      (src_pub <: public_key_t nc))