val receive_premessage_tokens_m
      (#nc: iconfig)
      (receive_premessage_token_impl: receive_premessage_token_st nc)
    : receive_premessage_tokens_st nc
val receive_premessage_tokens_m
      (#nc: iconfig)
      (receive_premessage_token_impl: receive_premessage_token_st nc)
    : receive_premessage_tokens_st nc
let rec receive_premessage_tokens_m
    (#nc : iconfig)
    (receive_premessage_token_impl : receive_premessage_token_st nc) :
    receive_premessage_tokens_st nc =
  fun smi pattern st input ->
  match pattern with
  | Nil ->
    (**) let h0 = HST.get () in
    (**) assert(Seq.equal h0.[|input|] Seq.empty);
    (**) receive_premessage_tokens_nil_lem (eval_handshake_state_m h0 st smi);
    success _
  | tk :: pattern' ->
    (**) let h0 = HST.get () in
    let tk_input = sub input 0ul (public_key_vs nc) in
    let input' = sub input (public_key_vs nc)
        (with_norm (size (List.length pattern' * (public_key_vsv nc)))) in
    (**) assert(h0.[|input|] `S.equal` (S.concat h0.[|tk_input|] h0.[|input'|]));
    (**) let st0_v : Ghost.erased _ = eval_handshake_state_m h0 st smi in
    (**) receive_premessage_tokens_unfold_lem tk pattern' h0.[|input|] st0_v;
    let _ = receive_premessage_token_impl smi tk st tk_input in
    (**) let smi' : Ghost.erased meta_info = receive_pretoken_update_smi tk smi in
    receive_premessage_tokens_m receive_premessage_token_impl smi' pattern' st input'
module Impl.Noise.RecursivePremessages

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 SB = FStar.Seq.Base
module L = FStar.List
module Seq = FStar.Seq

module B = LowStar.Buffer
module BS = Lib.ByteSequence
module LB = Lib.Buffer
open Lib.Buffer
module BB = Lib.ByteBuffer
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.HandshakeState

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

/// This file contains the recursive functions we need to make visible to the user
/// in order to allow proper normalisation for the generated code.
(*** Premessages *)
#push-options "--z3rlimit 100 --fuel 1 --ifuel 2"
[@(strict_on_arguments [3])]
inline_for_extraction noextract
let rec send_premessage_tokens_m
    (#nc : iconfig)
    (send_premessage_token_impl : send_premessage_token_st nc) :
    send_premessage_tokens_st nc =
  fun smi pattern st out ->
  match pattern with
  | Nil ->
    (**) let h0 = HST.get () in
    (**) send_premessage_tokens_nil_lem (eval_handshake_state_m h0 st smi);
    success tokens_premessage_return_type
  | tk :: pattern' ->
    (**) let h0 = HST.get () in
    let tk_out = sub out 0ul (public_key_vs nc) in
    let out' = sub out (public_key_vs nc)
                   (with_norm (size (List.length pattern' * (public_key_vsv nc)))) in
    (**) assert(h0.[|out|] `S.equal` (S.concat h0.[|tk_out|] h0.[|out'|]));
    (**) let st0_v : Ghost.erased _ = eval_handshake_state_m h0 st smi in
    (**) send_premessage_tokens_unfold_lem tk pattern' st0_v;
    let _ = send_premessage_token_impl smi tk st tk_out in
    send_premessage_tokens_m send_premessage_token_impl smi pattern' st out'
#pop-options

#push-options "--z3rlimit 100 --fuel 1 --ifuel 2"
[@(strict_on_arguments [3])]
/
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.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.HKDF.fsti.checked Impl.Noise.HandshakeState.fsti.checked Impl.Noise.CipherState.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.RecursivePremessages.fst
receive_premessage_token_impl: Impl.Noise.HandshakeState.receive_premessage_token_st nc
  -> Impl.Noise.HandshakeState.receive_premessage_tokens_st nc
Impl.Noise.Types.iconfig Impl.Noise.HandshakeState.receive_premessage_token_st FStar.Ghost.erased Spec.Noise.MetaInfo.meta_info Prims.list Spec.Noise.Base.Definitions.premessage_token Impl.Noise.HandshakeState.premessage_size_pred Impl.Noise.HandshakeState.valid_receive_premessage_hsm FStar.Ghost.reveal Impl.Noise.HandshakeState.premessage_t Impl.Noise.Types.success Impl.Noise.HandshakeState.tokens_premessage_return_type Prims.unit Spec.Noise.Base.Lemmas.receive_premessage_tokens_nil_lem Impl.Noise.Types.get_config Impl.Noise.HandshakeState.eval_handshake_state_m Prims._assert FStar.Seq.Base.equal Lib.IntTypes.uint8 Lib.Buffer.op_Brack_Lens_Access Lib.Buffer.MUT Impl.Noise.HandshakeState.premessage_vs FStar.Seq.Base.empty Impl.Noise.Types.rtype FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Impl.Noise.RecursivePremessages.receive_premessage_tokens_m FStar.Ghost.hide Spec.Noise.MetaInfo.receive_pretoken_update_smi Impl.Noise.HandshakeState.token_premessage_return_type Spec.Noise.Base.Lemmas.receive_premessage_tokens_unfold_lem Spec.Noise.Base.Definitions.handshake_state Lib.Sequence.equal Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.Sequence.concat Impl.Noise.Types.public_key_vs Meta.Noise.with_norm Lib.IntTypes.size_t Lib.IntTypes.size FStar.Mul.op_Star FStar.List.Tot.Base.length Impl.Noise.Types.public_key_vsv Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.mk_int Prims.op_Multiply Lib.Buffer.sub FStar.UInt32.__uint_to_t
let rec receive_premessage_tokens_m
      (#nc: iconfig)
      (receive_premessage_token_impl: receive_premessage_token_st nc)
    : receive_premessage_tokens_st nc =
  
fun smi pattern st input ->
  match pattern with
  | Nil ->
    let h0 = HST.get () in
    assert (Seq.equal h0.[| input |] Seq.empty);
    receive_premessage_tokens_nil_lem (eval_handshake_state_m h0 st smi);
    success _
  | tk :: pattern' ->
    let h0 = HST.get () in
    let tk_input = sub input 0ul (public_key_vs nc) in
    let input' =
      sub input (public_key_vs nc) (with_norm (size (List.length pattern' * (public_key_vsv nc))))
    in
    assert (h0.[| input |] `S.equal` (S.concat h0.[| tk_input |] h0.[| input' |]));
    let st0_v:Ghost.erased _ = eval_handshake_state_m h0 st smi in
    receive_premessage_tokens_unfold_lem tk pattern' h0.[| input |] st0_v;
    let _ = receive_premessage_token_impl smi tk st tk_input in
    let smi':Ghost.erased meta_info = receive_pretoken_update_smi tk smi in
    receive_premessage_tokens_m receive_premessage_token_impl smi' pattern' st input'