val message1_len : Lib.IntTypes.size_t
let message1_len = size message1_length
/// This module implements a minimal example using the Noise API. Note that it
/// can't be extracted to C, and is here only to check that the API is usable
/// (ie: that the function preconditions are reasonable and that the API provides
/// enough information to reason about aliasing).

module Impl.Noise.API.Instances.IKpsk2_25519_ChaChaPoly_BLAKE2s.Test

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

open Lib.IntTypes
open Lib.Sequence
open Lib.Buffer
open LowStar.BufferOps
module B = LowStar.Buffer
module G = FStar.Ghost

open Spec.Noise.API.MetaInfo

open Impl.Noise.Types
open Impl.Noise.API.Device
open Impl.Noise.API.DState
open Impl.Noise.API.Session
open Impl.Noise.TypeOrUnit
open Impl.Noise.Allocate
module Str = Impl.Noise.String
open Spec.Noise

open Impl.Noise.API.Instances.IKpsk2_25519_ChaChaPoly_BLAKE2s

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

(*** Tests *)

let _ : squash(
 key_slots_from_pattern true (idc_get_pattern idc) =
 {
   ks_s = true;
   ks_e = true;
   ks_re = true;
   ks_rs = true;
   ks_psk = true;
   ks_send = true;
   ks_receive = true;
 }) = normalize_term_spec(key_slots_from_pattern true (idc_get_pattern idc))

let _ : squash(
 key_slots_from_pattern false (idc_get_pattern idc) =
 {
   ks_s = true;
   ks_e = true;
   ks_re = true;
   ks_rs = true;
   ks_psk = true;
   ks_send = true;
   ks_receive = true;
 }) = normalize_term_spec(key_slots_from_pattern false (idc_get_pattern idc))

/// In the case of IKpsk2, all the private key types are the same, and all the
/// public key types are the same

[@@ noextract_to "krml"] inline_for_extraction noextract
let private_key_t = sprivate_key_t idc true

[@@ noextract_to "krml"] inline_for_extraction noextract
let public_key_t = spublic_key_t idc true

[@@ noextract_to "krml"] inline_for_extraction noextract
let hashable_size_t = hashable_size_t (idc_get_nc idc)

let _ : squash(knows_remote_at_init idc true = true) =
  normalize_term_spec(knows_remote_at_init idc true)
let _ : squash(knows_remote_at_init idc false = false) =
  normalize_term_spec(knows_remote_at_init idc false)
let _ : squash(List.Tot.length (idc_get_pattern idc).messages = 2) =
  normalize_term_spec(List.Tot.length (idc_get_pattern idc).messages)
module Helpers = FStar.InteractiveHelpers

open Lib.RandomSequence
open Lib.RandomBuffer.System

[@@ noextract_to "krml"] inline_for_extraction noextract
let message0_length : l:nat{l = compute_message_length idc 0} =
  (**) normalize_term_spec (compute_message_length idc 0);
  96

[@@ noextract_to "krml"] inline_for_extraction noextract
let message0_len = size message0_length

[@@ noextract_to "krml"] inline_for_extraction noextract
let message1_length : l:nat{l = compute_message_length idc 1} =
  (**) normalize_term_spec (compute_message_length idc 1);
  48
/
Spec.Noise.API.Session.fsti.checked Spec.Noise.API.MetaInfo.fst.checked Spec.Noise.API.Device.Definitions.fsti.checked Spec.Noise.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.RandomSequence.fsti.checked Lib.RandomBuffer.System.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Impl.Noise.Types.fst.checked Impl.Noise.TypeOrUnit.fsti.checked Impl.Noise.String.fst.checked Impl.Noise.API.Session.fsti.checked Impl.Noise.API.Instances.IKpsk2_25519_ChaChaPoly_BLAKE2s.fsti.checked Impl.Noise.API.DState.fsti.checked Impl.Noise.API.Device.fsti.checked Impl.Noise.Allocate.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.InteractiveHelpers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Impl.Noise.API.Instances.IKpsk2_25519_ChaChaPoly_BLAKE2s.Test.fst
Lib.IntTypes.size_t
Lib.IntTypes.size Impl.Noise.API.Instances.IKpsk2_25519_ChaChaPoly_BLAKE2s.Test.message1_length
let message1_len =
  
size message1_length