text: /* 
    This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
    KreMLin invocation: /home/everest/everest/kremlin/krml -minimal -add-include "kremlib.h" -fnoanonymous-unions -warn-error -9-7-6@4-14-15 -fsopts --debug,yes -verbose -library EverCrypt,EverCrypt.*,Hacl.*,Interop_assumptions,Check_sha_stdcall,Sha_update_bytes_stdcall,Check_aesni_stdcall -drop MonotoneMap -drop MonotoneMapNonDep -drop FStar.Tactics.\* -drop FStar.Tactics -drop Crypto.AEAD.\* -drop Crypto.HKDF -drop Crypto.HMAC -add-include "hacks.h" -add-include "kremlin/internal/compat.h" -bundle LowParse.\*,LowParseWrappers[rename=LowParse] -bundle Format.\* -bundle EverCrypt=EverCrypt,EverCrypt.\* -bundle FStar.\*,LowStar.\*,C,C.\*[rename=Mitls_Kremlib] -bundle Parsers.\* -bundle Spec.\* -bundle Meta.\* -bundle Lib.*[rename=Hacl_Lib] -bundle TLSConstants=TLSConstants,QD.TLS_protocolVersion,List.Helpers -bundle Hashing=Hashing.Spec,Hashing,Hashing.CRF,HMAC,HKDF,HMAC.UFCMA -bundle Old.Handshake=Old.HMAC.UFCMA,Old.Epochs,Old.KeySchedule,Old.Handshake -bundle StatefulLHAE=AEAD_GCM,LHAEPlain,StatefulPlain,StatefulLHAE -bundle StreamAE=StreamPlain,StreamAE -bundle CommonDH=TLS.Curve25519,DHGroup,ECGroup,CommonDH -bundle Content=Content,DataStream -bundle Record=Record,StAE,Transport,StreamDeltas -bundle PMS=PMS,RSAKey,TLSPRF -bundle Crypto.Plain=Buffer.Utils,Crypto.Indexing,Crypto.Plain,Crypto.Symmetric.Bytes -bundle Flags=DebugFlags,Flags,Flag,TLSInfoFlags -bundle Vale.Stdcalls.*,Vale.Interop,Vale.Interop.*,Vale.Wrapper.X64.*[rename=Vale] -bundle Vale.Inline.X64.*[rename=Vale_Inline] -bundle Vale.*[rename=Unused2] -ldopts -L,/home/everest/everest/MLCrypto/openssl,-lcrypto,-lssl extract/Kremlin/FStar_Pervasives_Native.krml extract/Kremlin/FStar_Pervasives.krml extract/Kremlin/FStar_Squash.krml extract/Kremlin/FStar_Classical.krml extract/Kremlin/FStar_Preorder.krml extract/Kremlin/FStar_Calc.krml extract/Kremlin/FStar_Mul.krml extract/Kremlin/FStar_Math_Lib.krml extract/Kremlin/FStar_Math_Lemmas.krml extract/Kremlin/FStar_StrongExcludedMiddle.krml extract/Kremlin/FStar_FunctionalExtensionality.krml extract/Kremlin/FStar_List_Tot_Base.krml extract/Kremlin/FStar_List_Tot_Properties.krml extract/Kremlin/FStar_List_Tot.krml extract/Kremlin/FStar_Seq_Base.krml extract/Kremlin/FStar_Seq_Properties.krml extract/Kremlin/FStar_Seq.krml extract/Kremlin/FStar_BitVector.krml extract/Kremlin/FStar_UInt.krml extract/Kremlin/FStar_UInt32.krml extract/Kremlin/FStar_UInt8.krml extract/Kremlin/FStar_Exn.krml extract/Kremlin/FStar_Set.krml extract/Kremlin/FStar_Monotonic_Witnessed.krml extract/Kremlin/FStar_Ghost.krml extract/Kremlin/FStar_ErasedLogic.krml extract/Kremlin/FStar_PropositionalExtensionality.krml extract/Kremlin/FStar_PredicateExtensionality.krml extract/Kremlin/FStar_TSet.krml extract/Kremlin/FStar_Monotonic_Heap.krml extract/Kremlin/FStar_Heap.krml extract/Kremlin/FStar_ST.krml extract/Kremlin/FStar_All.krml extract/Kremlin/Lib_LoopCombinators.krml extract/Kremlin/FStar_Int.krml extract/Kremlin/FStar_Int64.krml extract/Kremlin/FStar_Int63.krml extract/Kremlin/FStar_Int32.krml extract/Kremlin/FStar_Int16.krml extract/Kremlin/FStar_Int8.krml extract/Kremlin/FStar_UInt64.krml extract/Kremlin/FStar_UInt63.krml extract/Kremlin/FStar_UInt16.krml extract/Kremlin/FStar_Int_Cast.krml extract/Kremlin/FStar_UInt128.krml extract/Kremlin/FStar_Int_Cast_Full.krml extract/Kremlin/FStar_Int128.krml extract/Kremlin/Lib_IntTypes.krml extract/Kremlin/Lib_RawIntTypes.krml extract/Kremlin/Lib_Sequence.krml extract/Kremlin/Lib_ByteSequence.krml extract/Kremlin/Spec_Chacha20.krml extract/Kremlin/Meta_Attribute.krml extract/Kremlin/FStar_Map.krml extract/Kremlin/FStar_Monotonic_HyperHeap.krml extract/Kremlin/FStar_Monotonic_HyperStack.krml extract/Kremlin/FStar_HyperStack.krml extract/Kremlin/FStar_HyperStack_ST.krml extract/Kremlin/FStar_Universe.krml extract/Kremlin/FStar_GSet.krml extract/Kremlin/FStar_ModifiesGen.krml extract/Kremlin/FStar_Range.krml extract/Kremlin/FStar_Reflection_Types.krml extract/Kremlin/FStar_Tactics_Types.krml extract/Kremlin/FStar_Tactics_Result.krml extract/Kremlin/FStar_Tactics_Effect.krml extract/Kremlin/FStar_Tactics_Util.krml extract/Kremlin/FStar_Reflection_Data.krml extract/Kremlin/FStar_Reflection_Const.krml extract/Kremlin/FStar_Char.krml extract/Kremlin/FStar_List.krml extract/Kremlin/FStar_String.krml extract/Kremlin/FStar_Order.krml extract/Kremlin/FStar_Reflection_Basic.krml extract/Kremlin/FStar_Reflection_Derived.krml extract/Kremlin/FStar_Tactics_Builtins.krml extract/Kremlin/FStar_Reflection_Formula.krml extract/Kremlin/FStar_Reflection_Derived_Lemmas.krml extract/Kremlin/FStar_Reflection.krml extract/Kremlin/FStar_Tactics_Derived.krml extract/Kremlin/FStar_Tactics_Logic.krml extract/Kremlin/FStar_Tactics.krml extract/Kremlin/FStar_BigOps.krml extract/Kremlin/LowStar_Monotonic_Buffer.krml extract/Kremlin/LowStar_Buffer.krml extract/Kremlin/LowStar_BufferOps.krml extract/Kremlin/Spec_Loops.krml extract/Kremlin/C_Loops.krml extract/Kremlin/Lib_Loops.krml extract/Kremlin/FStar_Endianness.krml extract/Kremlin/LowStar_Endianness.krml extract/Kremlin/LowStar_ImmutableBuffer.krml extract/Kremlin/Lib_Buffer.krml extract/Kremlin/Lib_ByteBuffer.krml extract/Kremlin/FStar_HyperStack_All.krml extract/Kremlin/Lib_IntVector_Intrinsics.krml extract/Kremlin/Spec_GaloisField.krml extract/Kremlin/Spec_AES.krml extract/Kremlin/Lib_IntVector.krml extract/Kremlin/Hacl_Spec_Chacha20_Vec.krml extract/Kremlin/Hacl_Spec_Chacha20_Lemmas.krml extract/Kremlin/Lib_Sequence_Lemmas.krml extract/Kremlin/Hacl_Spec_Chacha20_Equiv.krml extract/Kremlin/Hacl_Impl_Chacha20_Core32xN.krml extract/Kremlin/Hacl_Impl_Chacha20_Vec.krml extract/Kremlin/Vale_Lib_Set.krml extract/Kremlin/Vale_Def_Opaque_s.krml extract/Kremlin/Vale_Lib_Meta.krml extract/Kremlin/Vale_Def_Words_s.krml extract/Kremlin/Vale_Def_Words_Two_s.krml extract/Kremlin/Vale_Lib_Seqs_s.krml extract/Kremlin/Vale_Def_Words_Four_s.krml extract/Kremlin/Vale_Def_Words_Seq_s.krml extract/Kremlin/Vale_Def_Types_s.krml extract/Kremlin/Vale_Def_Words_Two.krml extract/Kremlin/Vale_Lib_Seqs.krml extract/Kremlin/Vale_Def_TypesNative_s.krml extract/Kremlin/Vale_Arch_TypesNative.krml extract/Kremlin/Vale_Def_Words_Seq.krml extract/Kremlin/Vale_Arch_Types.krml extract/Kremlin/Vale_Def_Prop_s.krml extract/Kremlin/Vale_Arch_MachineHeap_s.krml extract/Kremlin/Vale_Arch_MachineHeap.krml extract/Kremlin/FStar_Option.krml extract/Kremlin/Vale_X64_Machine_s.krml extract/Kremlin/Vale_X64_Instruction_s.krml extract/Kremlin/Vale_X64_Bytes_Code_s.krml extract/Kremlin/Vale_AES_AES_s.krml extract/Kremlin/Vale_Math_Poly2_Defs_s.krml extract/Kremlin/Vale_Math_Poly2_s.krml extract/Kremlin/Vale_Math_Poly2_Bits_s.krml extract/Kremlin/Spec_Hash_Definitions.krml extract/Kremlin/Spec_Hash_Lemmas0.krml extract/Kremlin/Spec_Hash_PadFinish.krml extract/Kremlin/Spec_SHA2_Constants.krml extract/Kremlin/Spec_SHA2.krml extract/Kremlin/Vale_X64_CryptoInstructions_s.krml extract/Kremlin/Vale_X64_CPU_Features_s.krml extract/Kremlin/Vale_X64_Instructions_s.krml extract/Kremlin/LowStar_BufferView_Down.krml extract/Kremlin/LowStar_BufferView_Up.krml extract/Kremlin/Vale_Interop_Views.krml extract/Kremlin/Vale_Arch_HeapTypes_s.krml extract/Kremlin/Vale_Interop_Types.krml extract/Kremlin/Vale_Interop_Heap_s.krml extract/Kremlin/LowStar_Modifies.krml extract/Kremlin/LowStar_ModifiesPat.krml extract/Kremlin/LowStar_BufferView.krml extract/Kremlin/Vale_Lib_BufferViewHelpers.krml extract/Kremlin/Vale_Interop.krml extract/Kremlin/Vale_Arch_HeapImpl.krml extract/Kremlin/Vale_Arch_Heap.krml extract/Kremlin/Vale_X64_Machine_Semantics_s.krml extract/Kremlin/Vale_Interop_Base.krml extract/Kremlin/Vale_X64_Memory.krml extract/Kremlin/Vale_X64_Stack_i.krml extract/Kremlin/Vale_Lib_Map16.krml extract/Kremlin/Vale_X64_Flags.krml extract/Kremlin/Vale_Curve25519_Fast_lemmas_internal.krml extract/Kremlin/Vale_Curve25519_Fast_defs.krml extract/Kremlin/FStar_Algebra_CommMonoid.krml extract/Kremlin/FStar_Tactics_CanonCommSemiring.krml extract/Kremlin/Vale_Curve25519_FastUtil_helpers.krml extract/Kremlin/Vale_Curve25519_FastHybrid_helpers.krml extract/Kremlin/Vale_Curve25519_Fast_lemmas_external.krml extract/Kremlin/Vale_X64_Regs.krml extract/Kremlin/FStar_Float.krml extract/Kremlin/FStar_IO.krml extract/Kremlin/Vale_Def_PossiblyMonad.krml extract/Kremlin/Vale_X64_Stack_Sems.krml extract/Kremlin/Vale_X64_BufferViewStore.krml extract/Kremlin/Vale_X64_Memory_Sems.krml extract/Kremlin/Vale_X64_State.krml extract/Kremlin/Vale_X64_StateLemmas.krml extract/Kremlin/Vale_X64_Lemmas.krml extract/Kremlin/Vale_X64_Print_s.krml extract/Kremlin/Vale_X64_Decls.krml extract/Kremlin/Vale_X64_QuickCode.krml extract/Kremlin/Vale_X64_QuickCodes.krml extract/Kremlin/Vale_X64_Taint_Semantics.krml extract/Kremlin/Vale_X64_InsLemmas.krml extract/Kremlin/Vale_X64_InsBasic.krml extract/Kremlin/Vale_X64_InsMem.krml extract/Kremlin/Vale_X64_InsVector.krml extract/Kremlin/Vale_X64_InsStack.krml extract/Kremlin/Vale_Curve25519_X64_FastHybrid.krml extract/Kremlin/Vale_Bignum_Defs.krml extract/Kremlin/Vale_Bignum_X64.krml extract/Kremlin/Vale_Curve25519_FastSqr_helpers.krml extract/Kremlin/Vale_Curve25519_X64_FastSqr.krml extract/Kremlin/Vale_Curve25519_FastMul_helpers.krml extract/Kremlin/Vale_Curve25519_X64_FastMul.krml extract/Kremlin/Vale_Curve25519_X64_FastWide.krml extract/Kremlin/Vale_Curve25519_X64_FastUtil.krml extract/Kremlin/Vale_X64_MemoryAdapters.krml extract/Kremlin/Vale_Interop_Assumptions.krml extract/Kremlin/Vale_Interop_X64.krml extract/Kremlin/Vale_AsLowStar_ValeSig.krml extract/Kremlin/Vale_AsLowStar_LowStarSig.krml extract/Kremlin/Vale_AsLowStar_MemoryHelpers.krml extract/Kremlin/Vale_AsLowStar_Wrapper.krml extract/Kremlin/Vale_Stdcalls_X64_Fadd.krml extract/Kremlin/Vale_Wrapper_X64_Fadd.krml extract/Kremlin/Spec_SHA1.krml extract/Kremlin/Spec_MD5.krml extract/Kremlin/Spec_Agile_Hash.krml extract/Kremlin/Spec_Hash_Incremental.krml extract/Kremlin/Spec_Hash_Lemmas.krml extract/Kremlin/FStar_Kremlin_Endianness.krml extract/Kremlin/Hacl_Hash_Lemmas.krml extract/Kremlin/Hacl_Hash_Definitions.krml extract/Kremlin/Hacl_Hash_PadFinish.krml extract/Kremlin/Hacl_Hash_MD.krml extract/Kremlin/Spec_SHA2_Lemmas.krml extract/Kremlin/Vale_X64_Stack.krml extract/Kremlin/Vale_SHA_SHA_helpers.krml extract/Kremlin/Vale_X64_InsSha.krml extract/Kremlin/Vale_SHA_X64.krml extract/Kremlin/Vale_Stdcalls_X64_Sha.krml extract/Kremlin/FStar_BV.krml extract/Kremlin/FStar_Reflection_Arith.krml extract/Kremlin/FStar_Tactics_BV.krml extract/Kremlin/Vale_Lib_Bv_s.krml extract/Kremlin/Vale_Math_Bits.krml extract/Kremlin/Vale_Lib_Tactics.krml extract/Kremlin/Vale_Poly1305_Bitvectors.krml extract/Kremlin/Vale_Math_Lemmas_Int.krml extract/Kremlin/FStar_Tactics_Canon.krml extract/Kremlin/Vale_Poly1305_Spec_s.krml extract/Kremlin/Vale_Poly1305_Math.krml extract/Kremlin/Vale_Poly1305_Util.krml extract/Kremlin/Vale_Poly1305_X64.krml extract/Kremlin/Vale_Stdcalls_X64_Poly.krml extract/Kremlin/Vale_Wrapper_X64_Poly.krml extract/Kremlin/Vale_Arch_BufferFriend.krml extract/Kremlin/Vale_SHA_Simplify_Sha.krml extract/Kremlin/Vale_Wrapper_X64_Sha.krml extract/Kremlin/Hacl_Hash_Core_SHA2_Constants.krml extract/Kremlin/Hacl_Hash_Core_SHA2.krml extract/Kremlin/Hacl_Hash_SHA2.krml extract/Kremlin/Hacl_Hash_Core_SHA1.krml extract/Kremlin/Hacl_Hash_SHA1.krml extract/Kremlin/Hacl_Hash_Core_MD5.krml extract/Kremlin/Hacl_Hash_MD5.krml extract/Kremlin/C_Endianness.krml extract/Kremlin/C.krml extract/Kremlin/C_String.krml extract/Kremlin/C_Failure.krml extract/Kremlin/FStar_Int31.krml extract/Kremlin/FStar_UInt31.krml extract/Kremlin/FStar_Integers.krml extract/Kremlin/EverCrypt_StaticConfig.krml extract/Kremlin/EverCrypt_TargetConfig.krml extract/Kremlin/Vale_Lib_Basic.krml extract/Kremlin/Vale_Lib_X64_Cpuid.krml extract/Kremlin/Vale_Lib_X64_Cpuidstdcall.krml extract/Kremlin/Vale_Stdcalls_X64_Cpuid.krml extract/Kremlin/Vale_Wrapper_X64_Cpuid.krml extract/Kremlin/EverCrypt_AutoConfig2.krml extract/Kremlin/EverCrypt_Helpers.krml extract/Kremlin/EverCrypt_Hash.krml extract/Kremlin/Spec_Agile_HMAC.krml extract/Kremlin/Hacl_HMAC.krml extract/Kremlin/EverCrypt_HMAC.krml extract/Kremlin/Declassify.krml extract/Kremlin/FStar_Bytes.krml extract/Kremlin/Hashing_Spec.krml extract/Kremlin/LowParse_Bytes32.krml extract/Kremlin/LowParse_Bytes.krml extract/Kremlin/LowParse_Spec_Base.krml extract/Kremlin/LowParse_SLow_Base.krml extract/Kremlin/LowParse_Spec_Option.krml extract/Kremlin/LowParse_SLow_Option.krml extract/Kremlin/LowParse_Spec_Combinators.krml extract/Kremlin/LowParse_Spec_IfThenElse.krml extract/Kremlin/Spec_Curve25519_Lemmas.krml extract/Kremlin/Spec_Curve25519.krml extract/Kremlin/Hacl_Spec_Curve25519_AddAndDouble.krml extract/Kremlin/Hacl_Impl_Curve25519_Lemmas.krml extract/Kremlin/Hacl_Spec_Curve25519_Field64_Definition.krml extract/Kremlin/Hacl_Spec_Curve25519_Field64_Lemmas.krml extract/Kremlin/Hacl_Spec_Curve25519_Field64_Core.krml extract/Kremlin/Hacl_Spec_Curve25519_Field64.krml extract/Kremlin/Hacl_Spec_Curve25519_Field51_Definition.krml extract/Kremlin/Hacl_Spec_Curve25519_Field51_Lemmas.krml extract/Kremlin/Hacl_Spec_Curve25519_Field51.krml extract/Kremlin/Hacl_Impl_Curve25519_Fields_Core.krml extract/Kremlin/Hacl_Impl_Curve25519_Field64.krml extract/Kremlin/Hacl_Impl_Curve25519_Field51.krml extract/Kremlin/Hacl_Impl_Curve25519_Fields.krml extract/Kremlin/Hacl_Impl_Curve25519_AddAndDouble.krml extract/Kremlin/LowParse_SLow_Combinators.krml extract/Kremlin/LowParse_Spec_List.krml extract/Kremlin/LowParse_SLow_List.krml extract/Kremlin/Spec_Poly1305.krml extract/Kremlin/Hacl_Spec_Poly1305_Vec.krml extract/Kremlin/Hacl_Spec_Poly1305_Field32xN.krml extract/Kremlin/Hacl_Poly1305_Field32xN_Lemmas.krml extract/Kremlin/Hacl_Impl_Poly1305_Lemmas.krml extract/Kremlin/Hacl_Spec_Poly1305_Field32xN_Lemmas.krml extract/Kremlin/Hacl_Impl_Poly1305_Field32xN.krml extract/Kremlin/Hacl_Spec_Poly1305_Lemmas.krml extract/Kremlin/Hacl_Spec_Poly1305_Equiv.krml extract/Kremlin/Hacl_Impl_Poly1305_Field32xN_256.krml extract/Kremlin/Hacl_Impl_Poly1305_Field32xN_128.krml extract/Kremlin/Hacl_Impl_Poly1305_Field32xN_32.krml extract/Kremlin/Hacl_Impl_Poly1305_Fields.krml extract/Kremlin/Hacl_Impl_Poly1305.krml extract/Kremlin/Spec_Chacha20Poly1305.krml extract/Kremlin/Hacl_Impl_Chacha20Poly1305_PolyCore.krml extract/Kremlin/Hacl_Impl_Chacha20Poly1305.krml extract/Kremlin/FStar_List_Pure_Base.krml extract/Kremlin/FStar_List_Pure_Properties.krml extract/Kremlin/FStar_List_Pure.krml extract/Kremlin/Meta_Interface.krml extract/Kremlin/Hacl_Meta_Chacha20Poly1305.krml extract/Kremlin/Hacl_Impl_Chacha20_Core32.krml extract/Kremlin/Hacl_Impl_Chacha20.krml extract/Kremlin/Hacl_Chacha20.krml extract/Kremlin/Hacl_Meta_Poly1305.krml extract/Kremlin/Hacl_Poly1305_32.krml extract/Kremlin/Hacl_Chacha20Poly1305_32.krml extract/Kremlin/FStar_Dyn.krml extract/Kremlin/EverCrypt_Vale.krml extract/Kremlin/EverCrypt_Specs.krml extract/Kremlin/EverCrypt_OpenSSL.krml extract/Kremlin/EverCrypt_Hacl.krml extract/Kremlin/EverCrypt_BCrypt.krml extract/Kremlin/EverCrypt_Cipher.krml extract/Kremlin/Hacl_Spec_Curve25519_Finv.krml extract/Kremlin/Hacl_Impl_Curve25519_Finv.krml extract/Kremlin/Hacl_Impl_Curve25519_Generic.krml extract/Kremlin/Hacl_Meta_Curve25519.krml extract/Kremlin/Hacl_Curve25519_51.krml extract/Kremlin/Vale_Stdcalls_X64_Fswap.krml extract/Kremlin/Vale_Wrapper_X64_Fswap.krml extract/Kremlin/Vale_X64_Print_Inline_s.krml extract/Kremlin/Vale_Inline_X64_Fswap_inline.krml extract/Kremlin/Vale_Stdcalls_X64_Fsqr.krml extract/Kremlin/Vale_Wrapper_X64_Fsqr.krml extract/Kremlin/Vale_Inline_X64_Fsqr_inline.krml extract/Kremlin/Vale_Stdcalls_X64_Fmul.krml extract/Kremlin/Vale_Wrapper_X64_Fmul.krml extract/Kremlin/Vale_Inline_X64_Fmul_inline.krml extract/Kremlin/Vale_Stdcalls_X64_Fsub.krml extract/Kremlin/Vale_Wrapper_X64_Fsub.krml extract/Kremlin/Vale_Inline_X64_Fadd_inline.krml extract/Kremlin/Hacl_Impl_Curve25519_Field64_Vale.krml extract/Kremlin/Hacl_Curve25519_64.krml extract/Kremlin/EverCrypt_Curve25519.krml extract/Kremlin/Hacl_Poly1305_128.krml extract/Kremlin/Hacl_Poly1305_256.krml extract/Kremlin/Vale_Poly1305_Equiv.krml extract/Kremlin/Vale_Poly1305_CallingFromLowStar.krml extract/Kremlin/EverCrypt_Poly1305.krml extract/Kremlin/Lib_Memzero.krml extract/Kremlin/Spec_HMAC_DRBG.krml extract/Kremlin/Hacl_HMAC_DRBG.krml extract/Kremlin/Lib_RandomBuffer_System.krml extract/Kremlin/EverCrypt_DRBG.krml extract/Kremlin/Spec_Agile_HKDF.krml extract/Kremlin/Hacl_HKDF.krml extract/Kremlin/EverCrypt_HKDF.krml extract/Kremlin/EverCrypt.krml extract/Kremlin/FStar_Printf.krml extract/Kremlin/FStar_Error.krml extract/Kremlin/FStar_Tcp.krml extract/Kremlin/LowParse_Spec_FLData.krml extract/Kremlin/LowParse_Math.krml extract/Kremlin/LowParse_Slice.krml extract/Kremlin/LowParse_Low_Base.krml extract/Kremlin/LowParse_Low_Combinators.krml extract/Kremlin/LowParse_Low_FLData.krml extract/Kremlin/LowParse_BigEndian.krml extract/Kremlin/LowParse_Spec_Int_Aux.krml extract/Kremlin/LowParse_Spec_Int.krml extract/Kremlin/LowParse_Spec_BoundedInt.krml extract/Kremlin/LowParse_BigEndianImpl_Base.krml extract/Kremlin/LowParse_BigEndianImpl_Low.krml extract/Kremlin/LowParse_Low_BoundedInt.krml extract/Kremlin/LowParse_Spec_SeqBytes_Base.krml extract/Kremlin/LowParse_Spec_DER.krml extract/Kremlin/LowParse_Spec_BCVLI.krml extract/Kremlin/LowParse_Spec_AllIntegers.krml extract/Kremlin/LowParse_Spec_VLData.krml extract/Kremlin/LowParse_Low_VLData.krml extract/Kremlin/LowParse_Spec_VLGen.krml extract/Kremlin/LowParse_Low_VLGen.krml extract/Kremlin/LowParse_Spec_Int_Unique.krml extract/Kremlin/LowParse_Low_Int_Aux.krml extract/Kremlin/LowParse_Low_Int.krml extract/Kremlin/LowParse_Low_DER.krml extract/Kremlin/LowParse_Low_BCVLI.krml extract/Kremlin/LowParse_Low_List.krml extract/Kremlin/LowParse_Spec_Array.krml extract/Kremlin/LowParse_Spec_VCList.krml extract/Kremlin/LowParse_Low_VCList.krml extract/Kremlin/LowParse_Low_IfThenElse.krml extract/Kremlin/LowParse_TacLib.krml extract/Kremlin/LowParse_Spec_Enum.krml extract/Kremlin/LowParse_Spec_Sum.krml extract/Kremlin/LowParse_Low_Enum.krml extract/Kremlin/LowParse_Low_Sum.krml extract/Kremlin/LowParse_Low_Tac_Sum.krml extract/Kremlin/LowParse_Low_Option.krml extract/Kremlin/LowParse_Spec_Bytes.krml extract/Kremlin/LowParse_Low_Bytes.krml extract/Kremlin/LowParse_Low_Array.krml extract/Kremlin/LowParse_Low.krml extract/Kremlin/LowParse_SLow_FLData.krml extract/Kremlin/LowParse_SLow_VLGen.krml extract/Kremlin/LowParse_BigEndianImpl_SLow.krml extract/Kremlin/LowParse_SLow_BoundedInt.krml extract/Kremlin/LowParse_SLow_Int_Aux.krml extract/Kremlin/LowParse_SLow_Int.krml extract/Kremlin/LowParse_SLow_DER.krml extract/Kremlin/LowParse_SLow_BCVLI.krml extract/Kremlin/LowParse_SLow_VCList.krml extract/Kremlin/LowParse_SLow_IfThenElse.krml extract/Kremlin/LowParse_SLow_Enum.krml extract/Kremlin/LowParse_SLow_Sum.krml extract/Kremlin/LowParse_SLow_Tac_Enum.krml extract/Kremlin/LowParse_SLow_Tac_Sum.krml extract/Kremlin/LowParse_SLow_VLData.krml extract/Kremlin/LowParse_SLow_Bytes.krml extract/Kremlin/LowParse_SLow_Array.krml extract/Kremlin/LowParse_Spec_Tac_Combinators.krml extract/Kremlin/LowParse_SLow.krml extract/Kremlin/Parsers_AlertDescription.krml extract/Kremlin/Parsers_AlertLevel.krml extract/Kremlin/Parsers_Alert.krml extract/Kremlin/TLSError.krml extract/Kremlin/Parsers_NamedGroup.krml extract/Kremlin/Format_Constants.krml extract/Kremlin/Format_UncompressedPointRepresentation.krml extract/Kremlin/Format_KeyShareEntry.krml extract/Kremlin/Flags.krml extract/Kremlin/Parsers_ECCurveType.krml extract/Kremlin/DebugFlags.krml extract/Kremlin/FStar_DependentMap.krml extract/Kremlin/FStar_Monotonic_DependentMap.krml extract/Kremlin/Mem.krml extract/Kremlin/Random.krml extract/Kremlin/TLS_Curve25519.krml extract/Kremlin/Parse.krml extract/Kremlin/ECGroup.krml extract/Kremlin/DHGroup.krml extract/Kremlin/Parsers_NamedGroupList.krml extract/Kremlin/CommonDH.krml extract/Kremlin/FFICallbacks.krml extract/Kremlin/Parsers_CompressionMethod.krml extract/Kremlin/Parsers_SignatureScheme.krml extract/Kremlin/Parsers_SignatureSchemeList.krml extract/Kremlin/LowParseWrappers.krml extract/Kremlin/Parsers_CipherSuite.krml extract/Kremlin/CipherSuite.krml extract/Kremlin/Parsers_ProtocolVersion.krml extract/Kremlin/TLSConstants.krml extract/Kremlin/HMAC.krml extract/Kremlin/RSAKey.krml extract/Kremlin/PMS.krml extract/Kremlin/List_Helpers.krml extract/Kremlin/PSK.krml extract/Kremlin/Extensions.krml extract/Kremlin/Cert.krml extract/Kremlin/TLSInfoFlags.krml extract/Kremlin/FStar_Date.krml extract/Kremlin/Nonce.krml extract/Kremlin/TLSInfo.krml extract/Kremlin/Crypto_Indexing.krml extract/Kremlin/Flag.krml extract/Kremlin/FStar_Old_Endianness.krml extract/Kremlin/FStar_Buffer.krml extract/Kremlin/C_Compat_Loops.krml extract/Kremlin/Buffer_Utils.krml extract/Kremlin/Crypto_Symmetric_Bytes.krml extract/Kremlin/Crypto_Plain.krml extract/Kremlin/AEADProvider.krml extract/Kremlin/Range.krml extract/Kremlin/DataStream.krml extract/Kremlin/Alert.krml extract/Kremlin/Content.krml extract/Kremlin/StreamPlain.krml extract/Kremlin/Hashing.krml extract/Kremlin/TLSPRF.krml extract/Kremlin/Hashing_CRF.krml extract/Kremlin/HandshakeMessages.krml extract/Kremlin/HandshakeLog.krml extract/Kremlin/Parsers_Boolean.krml extract/Kremlin/Parsers_TicketContents13_custom_data.krml extract/Kremlin/Parsers_TicketContents13_nonce.krml extract/Kremlin/Parsers_TicketContents13_rms.krml extract/Kremlin/Parsers_TicketContents13.krml extract/Kremlin/Parsers_TicketContents12_master_secret.krml extract/Kremlin/Parsers_TicketContents12.krml extract/Kremlin/Parsers_TicketVersion.krml extract/Kremlin/Parsers_TicketContents.krml extract/Kremlin/Parsers_TicketContents12_master_secret_Low.krml extract/Kremlin/Parsers_Ticket_Low.krml extract/Kremlin/Ticket.krml extract/Kremlin/Negotiation.krml extract/Kremlin/FStar_Monotonic_Seq.krml extract/Kremlin/StreamAE.krml extract/Kremlin/StatefulPlain.krml extract/Kremlin/LHAEPlain.krml extract/Kremlin/AEAD_GCM.krml extract/Kremlin/StatefulLHAE.krml extract/Kremlin/StAE.krml extract/Kremlin/Old_HMAC_UFCMA.krml extract/Kremlin/Parsers_HKDF_HkdfLabel_context.krml extract/Kremlin/Parsers_HKDF_HkdfLabel_label.krml extract/Kremlin/Parsers_HKDF_HkdfLabel.krml extract/Kremlin/HKDF.krml extract/Kremlin/Old_KeySchedule.krml extract/Kremlin/Old_Epochs.krml extract/Kremlin/FStar_HyperStack_IO.krml extract/Kremlin/StreamDeltas.krml extract/Kremlin/Old_Handshake.krml extract/Kremlin/Transport.krml extract/Kremlin/BufferBytes.krml extract/Kremlin/Record.krml extract/Kremlin/Connection.krml extract/Kremlin/TLS.krml extract/Kremlin/FFI.krml extract/Kremlin/Pkg.krml extract/Kremlin/Idx.krml extract/Kremlin/Model.krml extract/Kremlin/FStar_Test.krml extract/Kremlin/Pkg_Tree.krml extract/Kremlin/KDF.krml extract/Kremlin/QUIC.krml extract/Kremlin/IV.krml extract/Kremlin/KDF_Rekey.krml -tmpdir extract/Kremlin-Library -skip-compilation
    F* version: 946ec3ee
    KreMLin version: 88253438
   */
  
  #include "Range.h"
  
  uint32_t Range_hashLen(Spec_Hash_Definitions_hash_alg a)
  {
    switch (a)
    {
      case Spec_Hash_Definitions_MD5:
        {
          return (uint32_t)16U;
        }
      case Spec_Hash_Definitions_SHA1:
        {
          return (uint32_t)20U;
        }
      case Spec_Hash_Definitions_SHA2_224:
        {
          return (uint32_t)28U;
        }
      case Spec_Hash_Definitions_SHA2_256:
        {
          return (uint32_t)32U;
        }
      case Spec_Hash_Definitions_SHA2_384:
        {
          return (uint32_t)48U;
        }
      case Spec_Hash_Definitions_SHA2_512:
        {
          return (uint32_t)64U;
        }
      default:
        {
          KRML_HOST_EPRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
          KRML_HOST_EXIT(253U);
        }
    }
  }
  
  Prims_int FStar_Pervasives_Native_fst__Prims_int_Prims_int(K___Prims_int_Prims_int x)
  {
    return x.fst;
  }
  
  Prims_int FStar_Pervasives_Native_snd__Prims_int_Prims_int(K___Prims_int_Prims_int x)
  {
    return x.snd;
  }
  
  bool Range_within(Prims_int n1, K___Prims_int_Prims_int r)
  {
    return
      Prims_op_LessThanOrEqual(FStar_Pervasives_Native_fst__Prims_int_Prims_int(r),
        n1)
      && Prims_op_LessThanOrEqual(n1, FStar_Pervasives_Native_snd__Prims_int_Prims_int(r));
  }
  
  bool Range_wider(K___Prims_int_Prims_int r1, K___Prims_int_Prims_int r2)
  {
    return
      Prims_op_LessThanOrEqual(FStar_Pervasives_Native_fst__Prims_int_Prims_int(r1),
        FStar_Pervasives_Native_fst__Prims_int_Prims_int(r2))
      &&
        Prims_op_LessThanOrEqual(FStar_Pervasives_Native_snd__Prims_int_Prims_int(r2),
          FStar_Pervasives_Native_snd__Prims_int_Prims_int(r1));
  }
  
  K___Prims_int_Prims_int Range_point(Prims_int n1)
  {
    return ((K___Prims_int_Prims_int){ .fst = n1, .snd = n1 });
  }
  
  K___Prims_int_Prims_int Range_zero;
  
  K___Prims_int_Prims_int
  Range_sum(K___Prims_int_Prims_int uu____83, K___Prims_int_Prims_int uu____84)
  {
    K___K___Prims_int_Prims_int_K___Prims_int_Prims_int
    scrut = { .fst = uu____83, .snd = uu____84 };
    Prims_int h1 = scrut.snd.snd;
    Prims_int l1 = scrut.snd.fst;
    Prims_int h0 = scrut.fst.snd;
    Prims_int l0 = scrut.fst.fst;
    return
      (
        (K___Prims_int_Prims_int){
          .fst = Prims_op_Addition(l0, l1),
          .snd = Prims_op_Addition(h0, h1)
        }
      );
  }
  
  EverCrypt_aead_alg Range_aeAlg(TLSInfo_id i1)
  {
    CipherSuite_aeAlg x0 = TLSInfo_aeAlg_of_id(i1);
    if (x0.tag == CipherSuite_AEAD)
      return x0.val.case_AEAD._0;
    else
    {
      KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
        __FILE__,
        __LINE__,
        "unreachable (pattern matches are exhaustive in F*)");
      KRML_HOST_EXIT(255U);
    }
  }
  
  Prims_int Range_ivSize(TLSInfo_id i1)
  {
    CipherSuite_aeAlg authEnc = TLSInfo_aeAlg_of_id(i1);
    if (authEnc.tag == CipherSuite_MACOnly)
      return (krml_checked_int_t)0;
    else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Stream)
      return (krml_checked_int_t)0;
    else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Block)
    {
      EverCrypt_block_cipher_alg alg1 = authEnc.val.case_MtE._0.val.case_Block;
      return FStar_UInt32_v(EverCrypt_block_cipher_blockLen(alg1));
    }
    else
    {
      KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
        __FILE__,
        __LINE__,
        "unreachable (pattern matches are exhaustive in F*)");
      KRML_HOST_EXIT(255U);
    }
  }
  
  Prims_int Range_fixedPadSize(TLSInfo_id i1)
  {
    if (TLSInfo_uu___is_PlaintextID(i1))
      return (krml_checked_int_t)0;
    else
    {
      CipherSuite_aeAlg authEnc = TLSInfo_aeAlg_of_id(i1);
      if (authEnc.tag == CipherSuite_MACOnly)
        return (krml_checked_int_t)0;
      else if (authEnc.tag == CipherSuite_AEAD)
        return (krml_checked_int_t)0;
      else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Stream)
        return (krml_checked_int_t)0;
      else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Block)
        return (krml_checked_int_t)1;
      else
      {
        KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
          __FILE__,
          __LINE__,
          "unreachable (pattern matches are exhaustive in F*)");
        KRML_HOST_EXIT(255U);
      }
    }
  }
  
  Prims_int Range_maxPadSize(TLSInfo_id i1)
  {
    CipherSuite_aeAlg authEnc = TLSInfo_aeAlg_of_id(i1);
    if (authEnc.tag == CipherSuite_MACOnly)
      return (krml_checked_int_t)0;
    else if (authEnc.tag == CipherSuite_AEAD)
      return (krml_checked_int_t)0;
    else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Stream)
      return (krml_checked_int_t)0;
    else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Block)
    {
      EverCrypt_block_cipher_alg alg1 = authEnc.val.case_MtE._0.val.case_Block;
      Parsers_ProtocolVersion_protocolVersion scrut = TLSInfo_pv_of_id(i1);
      if (scrut.tag == Parsers_ProtocolVersion_SSL_3p0)
        return FStar_UInt32_v(EverCrypt_block_cipher_blockLen(alg1));
      else if (scrut.tag == Parsers_ProtocolVersion_TLS_1p0)
        return (krml_checked_int_t)256;
      else if (scrut.tag == Parsers_ProtocolVersion_TLS_1p1)
        return (krml_checked_int_t)256;
      else if (scrut.tag == Parsers_ProtocolVersion_TLS_1p2)
        return (krml_checked_int_t)256;
      else
      {
        KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
          __FILE__,
          __LINE__,
          "unreachable (pattern matches are exhaustive in F*)");
        KRML_HOST_EXIT(255U);
      }
    }
    else
    {
      KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
        __FILE__,
        __LINE__,
        "unreachable (pattern matches are exhaustive in F*)");
      KRML_HOST_EXIT(255U);
    }
  }
  
  Prims_int Range_minimalPadding(TLSInfo_id i1, Prims_int len1)
  {
    if (TLSInfo_uu___is_PlaintextID(i1))
      return (krml_checked_int_t)0;
    else
    {
      CipherSuite_aeAlg authEnc = TLSInfo_aeAlg_of_id(i1);
      if (authEnc.tag == CipherSuite_MACOnly)
        return Range_fixedPadSize(i1);
      else if (authEnc.tag == CipherSuite_AEAD)
        return Range_fixedPadSize(i1);
      else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Stream)
        return Range_fixedPadSize(i1);
      else if (authEnc.tag == CipherSuite_MtE && authEnc.val.case_MtE._0.tag == CipherSuite_Block)
      {
        EverCrypt_block_cipher_alg alg1 = authEnc.val.case_MtE._0.val.case_Block;
        Prims_int bs = FStar_UInt32_v(EverCrypt_block_cipher_blockLen(alg1));
        Prims_int lp = Prims_op_Modulus(len1, bs);
        return Prims_op_Subtraction(bs, lp);
      }
      else
      {
        KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
          __FILE__,
          __LINE__,
          "unreachable (pattern matches are exhaustive in F*)");
        KRML_HOST_EXIT(255U);
      }
    }
  }
  
  K___Prims_int_Prims_int Range_minMaxPad(TLSInfo_id i1)
  {
    return
      ((K___Prims_int_Prims_int){ .fst = Range_fixedPadSize(i1), .snd = Range_maxPadSize(i1) });
  }
  
  bool Range_valid_clen(TLSInfo_id i1, Prims_int clen)
  {
    if (TLSInfo_uu___is_PlaintextID(i1))
      return
        Prims_op_LessThanOrEqual((krml_checked_int_t)0,
          clen)
        && Prims_op_LessThanOrEqual(clen, TLSConstants_max_TLSPlaintext_fragment_length);
    else if (TLSInfo_uu___is_ID13(i1))
    {
      Prims_int tlen = FStar_UInt32_v(EverCrypt_aead_tagLen(Range_aeAlg(i1)));
      return
        Prims_op_GreaterThanOrEqual(Prims_op_Subtraction(clen, tlen),
          (krml_checked_int_t)0)
        &&
          Prims_op_LessThanOrEqual(Prims_op_Subtraction(clen, tlen),
            TLSConstants_max_TLSCiphertext_fragment_length_13);
    }
    else if (CipherSuite_uu___is_AEAD(TLSInfo_aeAlg_of_id(i1)))
    {
      Prims_int tlen = FStar_UInt32_v(EverCrypt_aead_tagLen(Range_aeAlg(i1)));
      return
        Prims_op_GreaterThanOrEqual(Prims_op_Subtraction(Prims_op_Subtraction(clen,
              AEADProvider_explicit_iv_length(i1)),
            tlen),
          (krml_checked_int_t)0)
        &&
          Prims_op_LessThanOrEqual(Prims_op_Subtraction(Prims_op_Subtraction(clen,
                AEADProvider_explicit_iv_length(i1)),
              tlen),
            TLSConstants_max_TLSPlaintext_fragment_length);
    }
    else if (CipherSuite_uu___is_MtE(TLSInfo_aeAlg_of_id(i1)))
      return
        Prims_op_GreaterThanOrEqual(Prims_op_Subtraction(Prims_op_Subtraction(Prims_op_Subtraction(clen,
                Range_ivSize(i1)),
              FStar_UInt32_v(CipherSuite_macSize(TLSInfo_macAlg_of_id(i1)))),
            Range_fixedPadSize(i1)),
          (krml_checked_int_t)0)
        &&
          Prims_op_LessThanOrEqual(Prims_op_Subtraction(Prims_op_Subtraction(Prims_op_Subtraction(clen,
                  Range_ivSize(i1)),
                FStar_UInt32_v(CipherSuite_macSize(TLSInfo_macAlg_of_id(i1)))),
              Range_maxPadSize(i1)),
            TLSConstants_max_TLSPlaintext_fragment_length);
    else
    {
      CipherSuite_aeAlg scrut = TLSInfo_aeAlg_of_id(i1);
      if (scrut.tag == CipherSuite_MACOnly)
      {
        Spec_Hash_Definitions_hash_alg h1 = scrut.val.case_MACOnly;
        return
          Prims_op_GreaterThanOrEqual(Prims_op_Subtraction(clen, FStar_UInt32_v(Range_hashLen(h1))),
            (krml_checked_int_t)0)
          &&
            Prims_op_LessThanOrEqual(Prims_op_Subtraction(clen, FStar_UInt32_v(Range_hashLen(h1))),
              TLSConstants_max_TLSPlaintext_fragment_length);
      }
      else
      {
        KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
          __FILE__,
          __LINE__,
          "unreachable (pattern matches are exhaustive in F*)");
        KRML_HOST_EXIT(255U);
      }
    }
  }
  
  Prims_int Range_min0(Prims_int i1)
  {
    if (Prims_op_GreaterThanOrEqual(i1, (krml_checked_int_t)0))
      return i1;
    else
      return (krml_checked_int_t)0;
  }
  
  Prims_int Range_minP(Prims_int n1)
  {
    if (Prims_op_GreaterThanOrEqual(n1, TLSConstants_max_TLSPlaintext_fragment_length))
      return TLSConstants_max_TLSPlaintext_fragment_length;
    else
      return n1;
  }
  
  K___Prims_int_Prims_int Range_cipherRangeClass(TLSInfo_id i1, Prims_int clen)
  {
    CipherSuite_aeAlg scrut0 = TLSInfo_aeAlg_of_id(i1);
    if (scrut0.tag == CipherSuite_MACOnly)
    {
      Spec_Hash_Definitions_hash_alg h1 = scrut0.val.case_MACOnly;
      uint32_t hLen = Range_hashLen(h1);
      Prims_int minmax = Prims_op_Subtraction(clen, FStar_UInt32_v(hLen));
      return ((K___Prims_int_Prims_int){ .fst = minmax, .snd = minmax });
    }
    else if (scrut0.tag == CipherSuite_MtE)
    {
      Prims_int ivL = Range_ivSize(i1);
      uint32_t macLen = CipherSuite_macSize(TLSInfo_macAlg_of_id(i1));
      K___Prims_int_Prims_int scrut = Range_minMaxPad(i1);
      Prims_int minPad = scrut.fst;
      Prims_int maxPad = scrut.snd;
      Prims_int
      max1 =
        Prims_op_Subtraction(Prims_op_Subtraction(Prims_op_Subtraction(clen, ivL),
            FStar_UInt32_v(macLen)),
          minPad);
      Prims_int
      min1 =
        Prims_op_Subtraction(Prims_op_Subtraction(Prims_op_Subtraction(clen, ivL),
            FStar_UInt32_v(macLen)),
          maxPad);
      return ((K___Prims_int_Prims_int){ .fst = Range_min0(min1), .snd = Range_minP(max1) });
    }
    else if (scrut0.tag == CipherSuite_AEAD)
    {
      EverCrypt_aead_alg aeadAlg = scrut0.val.case_AEAD._0;
      Prims_int ivL = AEADProvider_explicit_iv_length(i1);
      Prims_int tagL = FStar_UInt32_v(EverCrypt_aead_tagLen(aeadAlg));
      Prims_int minmax = Prims_op_Subtraction(Prims_op_Subtraction(clen, ivL), tagL);
      return ((K___Prims_int_Prims_int){ .fst = minmax, .snd = minmax });
    }
    else
    {
      KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
        __FILE__,
        __LINE__,
        "unreachable (pattern matches are exhaustive in F*)");
      KRML_HOST_EXIT(255U);
    }
  }
  
  Prims_int Range_targetLength(TLSInfo_id i1, K___Prims_int_Prims_int uu____436)
  {
    Prims_int h1 = uu____436.snd;
    CipherSuite_aeAlg scrut = TLSInfo_aeAlg_of_id(i1);
    if (scrut.tag == CipherSuite_MACOnly)
    {
      Spec_Hash_Definitions_hash_alg hash1 = scrut.val.case_MACOnly;
      uint32_t hLen = Range_hashLen(hash1);
      Prims_int prePad = Prims_op_Addition(h1, FStar_UInt32_v(hLen));
      Prims_int padLen = Range_minimalPadding(i1, prePad);
      return Prims_op_Addition(prePad, padLen);
    }
    else if (scrut.tag == CipherSuite_MtE)
    {
      Prims_int ivL = Range_ivSize(i1);
      uint32_t macLen = CipherSuite_macSize(TLSInfo_macAlg_of_id(i1));
      Prims_int prePad = Prims_op_Addition(h1, FStar_UInt32_v(macLen));
      Prims_int padLen = Range_minimalPadding(i1, prePad);
      Prims_int
      clen =
        Prims_op_Addition(Prims_op_Addition(Prims_op_Addition(ivL, FStar_UInt32_v(macLen)), padLen),
          h1);
      return clen;
    }
    else if (scrut.tag == CipherSuite_AEAD)
    {
      EverCrypt_aead_alg aeadAlg = scrut.val.case_AEAD._0;
      Prims_int ivL = AEADProvider_explicit_iv_length(i1);
      Prims_int tagL = FStar_UInt32_v(EverCrypt_aead_tagLen(aeadAlg));
      Prims_int fp = Range_fixedPadSize(i1);
      Prims_int clen = Prims_op_Addition(Prims_op_Addition(Prims_op_Addition(ivL, h1), fp), tagL);
      return clen;
    }
    else
    {
      KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
        __FILE__,
        __LINE__,
        "unreachable (pattern matches are exhaustive in F*)");
      KRML_HOST_EXIT(255U);
    }
  }
  
  K___Prims_int_Prims_int Range_rangeClass(TLSInfo_id i1, K___Prims_int_Prims_int r)
  {
    if
    (
      CipherSuite_uu___is_MACOnly(TLSInfo_aeAlg_of_id(i1))
      && !Parsers_ProtocolVersion_uu___is_SSL_3p0(TLSInfo_pv_of_id(i1))
    )
    {
      KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
        __FILE__,
        __LINE__,
        "[rangeClass] given an invalid algorithm identifier");
      KRML_HOST_EXIT(255U);
    }
    else if
    (
      Prims_op_LessThanOrEqual(FStar_Pervasives_Native_snd__Prims_int_Prims_int(r),
        TLSConstants_max_TLSPlaintext_fragment_length)
      &&
        (!CipherSuite_uu___is_AEAD(TLSInfo_aeAlg_of_id(i1))
        &&
          Prims_op_LessThanOrEqual(Prims_op_Subtraction(FStar_Pervasives_Native_snd__Prims_int_Prims_int(r),
              FStar_Pervasives_Native_fst__Prims_int_Prims_int(r)),
            Prims_op_Subtraction(Range_maxPadSize(i1),
              Range_minimalPadding(i1,
                Prims_op_Addition(FStar_Pervasives_Native_snd__Prims_int_Prims_int(r),
                  FStar_UInt32_v(CipherSuite_macSize(TLSInfo_macAlg_of_id(i1)))))))
        ||
          CipherSuite_uu___is_AEAD(TLSInfo_aeAlg_of_id(i1))
          &&
            FStar_Pervasives_Native_fst__Prims_int_Prims_int(r)
            == FStar_Pervasives_Native_snd__Prims_int_Prims_int(r))
    )
    {
      Prims_int tlen = Range_targetLength(i1, r);
      CipherSuite_aeAlg scrut0 = TLSInfo_aeAlg_of_id(i1);
      if (scrut0.tag == CipherSuite_MACOnly)
      {
        Prims_int ivL = Range_ivSize(i1);
        Prims_int macLen = FStar_UInt32_v(CipherSuite_macSize(TLSInfo_macAlg_of_id(i1)));
        K___Prims_int_Prims_int scrut = Range_minMaxPad(i1);
        Prims_int minPad = scrut.fst;
        Prims_int
        max1 =
          Prims_op_Subtraction(Prims_op_Subtraction(Prims_op_Subtraction(tlen, ivL), macLen),
            minPad);
        if (Prims_op_LessThanOrEqual(tlen, TLSConstants_max_TLSCiphertext_fragment_length))
          return Range_cipherRangeClass(i1, tlen);
        else
        {
          KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
            __FILE__,
            __LINE__,
            "[rangeClass] given an invalid plaintext length.");
          KRML_HOST_EXIT(255U);
        }
      }
      else if (scrut0.tag == CipherSuite_MtE && scrut0.val.case_MtE._0.tag == CipherSuite_Stream)
      {
        Prims_int ivL = Range_ivSize(i1);
        Prims_int macLen = FStar_UInt32_v(CipherSuite_macSize(TLSInfo_macAlg_of_id(i1)));
        K___Prims_int_Prims_int scrut = Range_minMaxPad(i1);
        Prims_int minPad = scrut.fst;
        Prims_int
        max1 =
          Prims_op_Subtraction(Prims_op_Subtraction(Prims_op_Subtraction(tlen, ivL), macLen),
            minPad);
        if (Prims_op_LessThanOrEqual(tlen, TLSConstants_max_TLSCiphertext_fragment_length))
          return Range_cipherRangeClass(i1, tlen);
        else
        {
          KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
            __FILE__,
            __LINE__,
            "[rangeClass] given an invalid plaintext length.");
          KRML_HOST_EXIT(255U);
        }
      }
      else if (scrut0.tag == CipherSuite_MtE && scrut0.val.case_MtE._0.tag == CipherSuite_Block)
      {
        Prims_int ivL = Range_ivSize(i1);
        Prims_int macLen = FStar_UInt32_v(CipherSuite_macSize(TLSInfo_macAlg_of_id(i1)));
        K___Prims_int_Prims_int scrut = Range_minMaxPad(i1);
        Prims_int minPad = scrut.fst;
        Prims_int
        max1 =
          Prims_op_Subtraction(Prims_op_Subtraction(Prims_op_Subtraction(tlen, ivL), macLen),
            minPad);
        if (Prims_op_LessThanOrEqual(tlen, TLSConstants_max_TLSCiphertext_fragment_length))
          return Range_cipherRangeClass(i1, tlen);
        else
        {
          KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
            __FILE__,
            __LINE__,
            "[rangeClass] given an invalid plaintext length.");
          KRML_HOST_EXIT(255U);
        }
      }
      else if (scrut0.tag == CipherSuite_AEAD)
        return Range_cipherRangeClass(i1, tlen);
      else
      {
        KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
          __FILE__,
          __LINE__,
          "unreachable (pattern matches are exhaustive in F*)");
        KRML_HOST_EXIT(255U);
      }
    }
    else
    {
      KRML_HOST_EPRINTF("KreMLin abort at %s:%d\n%s\n",
        __FILE__,
        __LINE__,
        "[rangeClass] given an invalid range.");
      KRML_HOST_EXIT(255U);
    }
  }
  
  K___Prims_int_Prims_int Range_fragment_range;
  
  