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)))
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 ()
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|])
/
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.lbuffer_or_null a len ->
    src: Impl.Noise.TypeOrUnit.type_or_unit (Lib.Buffer.lbuffer a len) b
  -> FStar.HyperStack.ST.Stack Prims.unit
Lib.IntTypes.size_t Prims.bool Impl.Noise.Types.lbuffer_or_null Impl.Noise.TypeOrUnit.type_or_unit Lib.Buffer.lbuffer Lib.Buffer.update_sub Lib.Buffer.MUT Lib.Buffer.lbuffer_t FStar.UInt32.__uint_to_t Prims.unit
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)