Process completed with exit code 1.

Process completed with exit code 1.

Process completed with exit code 1.

Process completed with exit code 2.

Process completed with exit code 2.

(17) * Error 17 at CDDLTest.DPE.InitializeContextInput.fst(95,2-104,39): - Failed to discharge match guard for goal: Pulse.Lib.Trade.trade (_ ** _ ** _) (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair r0 r1) r2) r3 x y) with resource from context: Pulse.Lib.Trade.trade ((CDDL.Pulse.Types.rel_pair r0 r1 (FStar.Pervasives.Native.fst (FStar.Pervasives.Native.fst x)) (FStar.Pervasives.Native.fst (FStar.Pervasives.Native.fst y)) ** r2 (FStar.Pervasives.Native.snd (FStar.Pervasives.Native.fst x)) (FStar.Pervasives.Native.snd (FStar.Pervasives.Native.fst y))) ** r3 (FStar.Pervasives.Native.snd x) (FStar.Pervasives.Native.snd y)) (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair r0 r1) r2) r3 x y) - Discharging guard failed. - g = Pulse.Lib.Trade.trade ((CDDL.Pulse.Types.rel_pair r0 r1 (FStar.Pervasives.Native.fst (FStar.Pervasives.Native.fst x)) (FStar.Pervasives.Native.fst (FStar.Pervasives.Native.fst y)) ** r2 (FStar.Pervasives.Native.snd (FStar.Pervasives.Native.fst x)) (FStar.Pervasives.Native.snd (FStar.Pervasives.Native.fst y))) ** r3 (FStar.Pervasives.Native.snd x) (FStar.Pervasives.Native.snd y)) (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair r0 r1) r2) r3 x y) == Pulse.Lib.Trade.trade ((CDDL.Pulse.Types.rel_pair r0 r1 (FStar.Pervasives.Native.fst (FStar.Pervasives.Native.fst x)) (FStar.Pervasives.Native.fst (FStar.Pervasives.Native.fst y)) ** r2 (FStar.Pervasives.Native.snd (FStar.Pervasives.Native.fst x)) (FStar.Pervasives.Native.snd (FStar.Pervasives.Native.fst y))) ** _ ** _) (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair (CDDL.Pulse.Types.rel_pair r0 r1) r2) r3 x y) - Guard policy is ForceSMT - Forcing the guard failed (refl_typing_guard) Failure("Bound term variable not found uu___ in environment: ...,C.EXIT_FAILURE, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x")

(19) * Error 19 at CDDLTest.DPE.CertifyKeyOutput.fst(95,10-97,15): - rewrite: could not prove equality of - CDDLTest.Test.rel_certifykeyoutputargs x hres - CDDLTest.Test.rel_bytes x.certificate.v hres.certificate.v ** CDDLTest.Test.rel_bytes x.derived_public_key.v hres.derived_public_key.v - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details.

(19) * Error 19 at CDDLTest.DPE.DeriveContextInput.fst(51,8-53,30): - Failed to prove pure property: CDDLTest.Test.rel_derive_context_engine_record x w == CDDLTest.DPE.DeriveContextInput.is_engine_record_core x w - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - Also see: CDDLTest.DPE.DeriveContextInput.fst(51,8-53,30) - Other related locations: dummy(0,0-0,0) - See also CDDLTest.DPE.DeriveContextInput.fst(51,2-53,31)

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1991,4-1991,12): - Global binding 'FStarC.Parser.ToDocument.p_tmNoEq' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1727,4-1727,21): - Global binding 'FStarC.Parser.ToDocument.p_maybeFocusArrow' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(1095,4-1095,24): - Global binding 'FStarC.Parser.ToDocument.p_disjunctivePattern' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(756,4-756,13): - Global binding 'FStarC.Parser.ToDocument.p_justSig' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/FStar/src/parser/FStarC.Parser.ToDocument.fst(735,8-735,14): - Global binding 'FStarC.Parser.ToDocument.p_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(88,16-88,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(87,16-87,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(86,16-86,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/basic/FStarC.Plugins.fst(85,16-85,17): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(271) * Warning 271 at /__w/FStar/FStar/FStar/ulib/FStar.UInt.fsti(436,8-436,51): - Pattern uses these theory symbols or terms that should not be in an SMT pattern: Prims.op_Subtraction

(288) * Warning 288 at FStar.Krml.Endianness.fst(58,34-58,41): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(58,11-58,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(57,56-57,63): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(57,4-57,28): - FStar.Krml.Endianness.lemma_euclidean_division is deprecated - FStar.Endianness.lemma_euclidean_division - See also FStar.Krml.Endianness.fst(36,4-36,28)

(288) * Warning 288 at FStar.Krml.Endianness.fst(56,11-56,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(55,11-55,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(47,8-47,32): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(288) * Warning 288 at FStar.Krml.Endianness.fst(45,13-45,20): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

(328) * Warning 328 at Spec.Loops.fst(47,8-47,19): - Global binding 'Spec.Loops.repeat_base' is recursive but not used in its body

* Warning <unknown> at Examples.Guess.fst(87,5-87,20): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also HigherOrderContracts.fst(109,85-109,111)

* Warning <unknown> at Examples.Guess.fst(87,5-87,20): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also HigherOrderContracts.fst(109,42-109,68)

* Warning <unknown> at Examples.Guess.fst(79,2-79,17): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also HigherOrderContracts.fst(361,83-361,107)

(272) * Warning 272 at Monitor.fst(15,0-15,36): - Top-level let-bindings must be total; this term may have effects

(361) * Warning 361 at GoodHandler1.fst(150,0-150,37): - Some #push-options have not been popped. Current depth is 1.

(272) * Warning 272 at GoodHandler1.fst(150,0-150,37): - Top-level let-bindings must be total; this term may have effects

(361) * Warning 361 at StlcHandlers.fst(121,0-124,16): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at ../../Compiler.StlcToFStar.fst(385,0-394,18): - Some #push-options have not been popped. Current depth is 1.

(361) * Warning 361 at WebServer.fst(237,0-238,38): - Some #push-options have not been popped. Current depth is 1.

* Warning <unknown> at WebServer.fst(184,2-184,32): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also ../../Compiler.MIO.To.Interm.fst(391,8-391,43)

* Warning <unknown> at WebServer.fst(184,2-184,32): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also ../../Compiler.MIO.To.Interm.fst(390,8-390,42)

(349) * Warning 349 at Utils.fst(377,2-381,5): - The verification condition succeeded after splitting it to localize potential errors, although the original non-split verification condition failed. If you want to rely on splitting queries for verifying your program please use the '--split_queries always' option rather than relying on it implicitly.

(352) * Warning 352 at ../../MIO.fst(217,27-217,44): - Combinator Prims.PURE ~> MIO.MIOwp is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(242) * Warning 242 at case-studies/IOLogging.fst(111,0-118,59): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/IOLogging.fst(112,11-112,14)

* Warning <unknown> at case-studies/IOLogging.fst(103,3-103,33): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also Compiler.MIO.To.Interm.fst(391,8-391,43)

* Warning <unknown> at case-studies/Compiler.Model1.Examples.fst(202,22-202,52): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances. - See also Compiler.MIO.To.Interm.fst(390,8-390,42)

* Warning <unknown> at case-studies/NoState.fst(75,57-75,62): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances.

* Warning <unknown> at case-studies/Zip.fst(59,76-59,81): - Warning: fuel exhausted during typeclass resolution. - This usually indicates a loop in your instances.

(242) * Warning 242 at case-studies/Compiler.Model1.Examples.fst(136,0-143,58): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/Compiler.Model1.Examples.fst(137,10-137,13)

(242) * Warning 242 at case-studies/Compiler.Model1.Examples.fst(95,0-103,58): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/Compiler.Model1.Examples.fst(96,10-96,13)

(242) * Warning 242 at case-studies/NoState.fst(48,0-56,58): - Definitions of inner let-rec aux and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: case-studies/NoState.fst(49,10-49,13)

(361) * Warning 361 at Compiler.StlcToFStar.fst(385,0-394,18): - Some #push-options have not been popped. Current depth is 1.

(352) * Warning 352 at MIO.fst(217,27-217,44): - Combinator Prims.PURE ~> MIO.MIOwp is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(272) * Warning 272 at Wasm10.fst(16,0-17,77): - Top-level let-bindings must be total; this term may have effects

(242) * Warning 242: - Not extracting uu___is_S to KaRaMeL

(250) * Warning 250: - Error while extracting (["FStar", "List"], "index") to KaRaMeL. - Got an exception:Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "filter_map") to KaRaMeL. - Got an exception:Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting (["LowStar", "Monotonic", "Buffer"], "mgcmalloc_of_list_partial") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["FStar", "Tactics", "NamedView"], "close_term_n") to KaRaMeL. - Got an exception:Failure("Internal error: name not found aux\n")

(242) * Warning 242: - Not extracting __proj__TAC__item__bind to KaRaMeL

(242) * Warning 242: - Not extracting __proj__TAC__item__return to KaRaMeL

(285) * Warning 285 at TopLevelArray.fst(7,5-7,7): - No modules in namespace ST and no file with that name either

(285) * Warning 285 at MemCpyModel.fst(10,5-10,7): - No modules in namespace ST and no file with that name either

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.AtomicAndGhost.fsti(185,16-185,20): - Combinator (Steel.ST.Effect.AtomicAndGhost.STAGCommon , Steel.ST.Effect.AtomicAndGhost.STAGCommon) |> Steel.ST.Effect.AtomicAndGhost.STAGCommon is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36): - Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26): - Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20): - Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |> Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(169,24-169,36): - Combinator ite_Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(168,19-168,26): - Combinator Steel.ST.Effect.STBase <: Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(167,16-167,20): - Combinator (Steel.ST.Effect.STBase , Steel.ST.Effect.STBase) |> Steel.ST.Effect.STBase is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(340) * Warning 340 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(461,24-461,37): - Unfolding name which is marked as a plugin: frame_vc_norm - See also /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(415,4-415,17)

(337) * Warning 337 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2066,65-2066,66): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/steel/src/extraction/ExtractSteel.Krml.fst(33,41-33,42): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(304,14-304,16): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of q1 (bound in Pulse.Syntax.Base.fst(304,14-304,16)) and t1 (bound in Pulse.Syntax.Base.fst(171,20-171,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.qualifier - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(123,20-123,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22)) and pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern - The type of the second term is: Pulse.Syntax.Base.pattern & Prims.bool - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(139,16-139,19): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in Pulse.Syntax.Base.fst(139,16-139,19)) and p1 (bound in Pulse.Syntax.Base.fst(123,20-123,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Prims.bool - The type of the second term is: Pulse.Syntax.Base.pattern - If the proof fails, try annotating these with the same type.

(318) * Warning 318 at /__w/FStar/FStar/pulse/lib/common/Pulse.Lib.Raise.fst(21,4-21,12): - Values of type `raisable` will be erased during extraction, but its interface hides this fact. - Add the `must_erase_for_extraction` attribute to the `val raisable` declaration for this symbol in the interface

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst(892,4-892,16): - Global binding 'PulseSyntaxExtension.Desugar.desugar_decl' is recursive but not used in its body

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/checker/Pulse.Common.fst(84,11-84,12): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(635,47-635,48): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(634,47-634,48): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(526,8-526,17): - Global binding 'PulseSyntaxExtension.Sugar.scan_decl' is recursive but not used in its body

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Sugar.fst(376,8-376,15): - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body

(330) * Warning 330 at SteelT.Effect.fst(51,44-51,59): - Polymonadic binds ((SteelT, PURE) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(352) * Warning 352 at SteelT.Effect.fst(51,0-51,59): - Combinator (SteelT.Effect.SteelT , Prims.PURE) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(330) * Warning 330 at SteelT.Effect.fst(51,44-51,59): - Polymonadic binds ((SteelT, PURE) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(352) * Warning 352 at SteelT.Effect.fst(51,0-51,59): - Combinator (SteelT.Effect.SteelT , Prims.PURE) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(330) * Warning 330 at SteelT.Effect.fst(41,44-41,59): - Polymonadic binds ((PURE, SteelT) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(330) * Warning 330 at SteelT.Effect.fst(41,44-41,59): - Polymonadic binds ((PURE, SteelT) |> SteelT) in this case) is an experimental feature;it is subject to some redesign in the future. Please keep us informed (on github etc.) about how you are using it

(352) * Warning 352 at SteelT.Effect.fst(31,9-31,13): - Combinator (SteelT.Effect.SteelT , SteelT.Effect.SteelT) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(352) * Warning 352 at SteelT.Effect.fst(31,9-31,13): - Combinator (SteelT.Effect.SteelT , SteelT.Effect.SteelT) |> SteelT.Effect.SteelT is not a substitutive indexed effect combinator, it is better to make it one if possible for better performance and ease of use

(274) * Warning 274: - Implicitly opening namespace 'duplex.' shadows module 'pingpong' in file "PingPong.fst". - Rename "PingPong.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'cqueue.' shadows module 'llist' in file "LList.fst". - Rename "LList.fst" to avoid conflicts.

(249) * Warning 249 at Bug166.fst(13,9-13,10): - Losing precision when encoding a function literal: fun _ -> Pulse.Lib.Core.emp - Unannotated abstraction in the compiler? - See also Bug166.fst(9,11-9,14)

(249) * Warning 249 at Bug166.fst(13,9-13,10): - Losing precision when encoding a function literal: fun _ -> Pulse.Lib.Core.emp - Unannotated abstraction in the compiler? - See also Bug166.fst(9,11-9,14)

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(361) * Warning 361 at PulseTutorial.Array.fst(269,0-278,1): - Some #push-options have not been popped. Current depth is 1.

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(285) * Warning 285 at PulseTutorial.LinkedList.fst(223,5-223,6): - No modules in namespace I and no file with that name either

(285) * Warning 285 at PulseTutorial.ImplicationAndForall.fst(24,5-24,7): - No modules in namespace GR and no file with that name either

(274) * Warning 274: - Implicitly opening namespace 'pulsetutorial.' shadows module 'parallelincrement' in file "ParallelIncrement.fst". - Rename "ParallelIncrement.fst" to avoid conflicts.

(337) * Warning 337 at Pulse2Rust.Rust.Syntax.fst(136,13-136,14): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(337) * Warning 337 at Pulse2Rust.Rust.Syntax.fst(131,21-131,22): - The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(272) * Warning 272 at ./src/Prelude.fst(8,0-8,48): - Top-level let-bindings must be total; this term may have effects

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "src/Prelude.fst". - Rename "src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "/__w/FStar/FStar/starmalloc/src/Prelude.fst". - Rename "/__w/FStar/FStar/starmalloc/src/Prelude.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.' shadows module 'prelude' in file "./src/Prelude.fst". - Rename "./src/Prelude.fst" to avoid conflicts.

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Scalar to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Scalar.fsti.checked instead of _cache/Steel.ST.C.Types.Scalar.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Rewrite to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Rewrite.fsti.checked instead of _cache/Steel.ST.C.Types.Rewrite.fsti.checked

(321) * Warning 321: - Did not expect module Steel.C.Typestring to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typestring.fst.checked instead of _cache/Steel.C.Typestring.fst.checked

(321) * Warning 321: - Did not expect module Steel.C.Typestring to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typestring.fsti.checked instead of _cache/Steel.C.Typestring.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Fields to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Fields.fsti.checked instead of _cache/Steel.ST.C.Types.Fields.fsti.checked

(321) * Warning 321: - Did not expect module Steel.C.Typenat to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typenat.fst.checked instead of _cache/Steel.C.Typenat.fst.checked

(321) * Warning 321: - Did not expect module Steel.C.Typenat to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.C.Typenat.fsti.checked instead of _cache/Steel.C.Typenat.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Array to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Array.fsti.checked instead of _cache/Steel.ST.C.Types.Array.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Struct.Aux to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Struct.Aux.fsti.checked instead of _cache/Steel.ST.C.Types.Struct.Aux.fsti.checked

(321) * Warning 321: - Did not expect module Steel.ST.C.Types.Base to be already checked. - Found it in an unexpected location: ../../../lib/steel/c/Steel.ST.C.Types.Base.fsti.checked instead of _cache/Steel.ST.C.Types.Base.fsti.checked

(290) * Warning 290 at Binding.fst(470,22-470,25): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of ts1 (bound in Binding.fst(470,22-470,25)) and t1 (bound in Binding.fst(459,25-459,27)) are equal. - The type of the first term is: Prims.list Ast.typ - The type of the second term is: Ast.typ - If the proof fails, try annotating these with the same type.

(271) * Warning 271 at src/lowparse/LowParse.Spec.Base.fsti(546,14-546,16): - SMT pattern misses at least one bound variable: t

(271) * Warning 271 at src/lowparse/LowParse.Spec.Base.fsti(546,6-546,17): - Pattern misses at least one bound variable: t

(242) * Warning 242 at Ast.fst(1795,0-1797,54): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: Ast.fst(418,12-418,15)

(290) * Warning 290 at Ast.fst(1477,16-1477,18): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of t1 (bound in Ast.fst(1477,16-1477,18)) and ts1 (bound in Ast.fst(1491,13-1491,16)) are equal. - The type of the first term is: Ast.typ - The type of the second term is: Prims.list Ast.typ - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at Ast.fst(1491,13-1491,16): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of ts1 (bound in Ast.fst(1491,13-1491,16)) and t1 (bound in Ast.fst(1477,16-1477,18)) are equal. - The type of the first term is: Prims.list Ast.typ - The type of the second term is: Ast.typ - If the proof fails, try annotating these with the same type.

(242) * Warning 242 at Ast.fst(416,0-450,18): - Definitions of inner let-rec seq and its enclosing top-level letbinding are not encoded to the solver, you will only be able to reason with their types - Also see: Ast.fst(418,12-418,15)

(361) * Warning 361 at Options.fst(634,0-637,15): - Some #push-options have not been popped. Current depth is 1.

(274) * Warning 274: - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c' in file "/__w/FStar/FStar/karamel/krmllib/C.fst". - Rename "/__w/FStar/FStar/karamel/krmllib/C.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'cbor.pulse.api.det.' shadows module 'c' in file "/__w/FStar/FStar/karamel/krmllib/C.fst". - Rename "/__w/FStar/FStar/karamel/krmllib/C.fst" to avoid conflicts.

(333) * Warning 333: - Unable to open hints file: /__w/FStar/FStar/everparse/tests/lowparse/LowParseExample9.fsti.hints; ran without hints

(333) * Warning 333: - Unable to open hints file: /__w/FStar/FStar/everparse/tests/lowparse/LowParseExample2.fsti.hints; ran without hints

(333) * Warning 333: - Unable to open hints file: /__w/FStar/FStar/everparse/tests/lowparse/LowParseExampleConstInt32le.fst.hints; ran without hints

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'fstar.stubs.reflection.v2.' shadows module 'data' in file "Data.fsti, Data.fst". - Rename "Data.fsti, Data.fst" to avoid conflicts.

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "igcmalloc_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "ialloca_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "Monotonic", "Buffer"], "mgcmalloc_of_list_partial") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "index") to KaRaMeL. - Got an exception:Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "filter_map") to KaRaMeL. - Got an exception:Failure("Internal error: name not found filter_map_acc\n")

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(361) * Warning 361 at /__w/FStar/FStar/hacl-star/lib/Lib.IntTypes.fsti(988,0-988,21): - Some #push-options have not been popped. Current depth is 1.

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(321) * Warning 321: - Did not expect module FStar.Pervasives to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Pervasives.fsti.checked instead of cache/Model/FStar.Pervasives.fsti.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fst.checked instead of cache/Model/FStar.NormSteps.fst.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fsti.checked instead of cache/Model/FStar.NormSteps.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Attributes to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Attributes.fsti.checked instead of cache/Model/FStar.Attributes.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Prelude to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Prelude.fsti.checked instead of cache/Model/FStar.Prelude.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Mul to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Mul.fst.checked instead of cache/Model/FStar.Mul.fst.checked

(321) * Warning 321: - Did not expect module Prims to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/Prims.fst.checked instead of cache/Model/Prims.fst.checked

(321) * Warning 321: - Did not expect module FStar.UInt32 to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.UInt32.fsti.checked instead of cache/Model/FStar.UInt32.fsti.checked

(321) * Warning 321: - Did not expect module LowStar.Buffer to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Buffer.fst.checked instead of cache/Model/LowStar.Buffer.fst.checked

(321) * Warning 321: - Did not expect module LowStar.Modifies to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Modifies.fst.checked instead of cache/Model/LowStar.Modifies.fst.checked

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "igcmalloc_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "ImmutableBuffer"], "ialloca_of_list") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["LowStar", "Monotonic", "Buffer"], "mgcmalloc_of_list_partial") to KaRaMeL. - Got an exception:Failure("Argument of FStar.Buffer.createL is not a list literal!")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "index") to KaRaMeL. - Got an exception:Failure("Internal error: name not found index\n")

(250) * Warning 250: - Error while extracting (["FStar", "List"], "filter_map") to KaRaMeL. - Got an exception:Failure("Internal error: name not found filter_map_acc\n")

(250) * Warning 250: - Error while extracting (["FStar", "Tactics", "NamedView"], "close_term_n") to KaRaMeL. - Got an exception:Failure("Internal error: name not found aux\n")

(242) * Warning 242: - Not extracting __proj__TAC__item__bind to KaRaMeL

(242) * Warning 242: - Not extracting __proj__TAC__item__return to KaRaMeL

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(321) * Warning 321: - Did not expect module FStar.Pervasives to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Pervasives.fsti.checked instead of cache/Karamel/FStar.Pervasives.fsti.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fst.checked instead of cache/Karamel/FStar.NormSteps.fst.checked

(321) * Warning 321: - Did not expect module FStar.NormSteps to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.NormSteps.fsti.checked instead of cache/Karamel/FStar.NormSteps.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Attributes to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Attributes.fsti.checked instead of cache/Karamel/FStar.Attributes.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Prelude to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Prelude.fsti.checked instead of cache/Karamel/FStar.Prelude.fsti.checked

(321) * Warning 321: - Did not expect module FStar.Mul to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.Mul.fst.checked instead of cache/Karamel/FStar.Mul.fst.checked

(321) * Warning 321: - Did not expect module Prims to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/Prims.fst.checked instead of cache/Karamel/Prims.fst.checked

(321) * Warning 321: - Did not expect module FStar.UInt32 to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/FStar.UInt32.fsti.checked instead of cache/Karamel/FStar.UInt32.fsti.checked

(321) * Warning 321: - Did not expect module LowStar.Buffer to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Buffer.fst.checked instead of cache/Karamel/LowStar.Buffer.fst.checked

(321) * Warning 321: - Did not expect module LowStar.Modifies to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/ulib.checked/LowStar.Modifies.fst.checked instead of cache/Karamel/LowStar.Modifies.fst.checked

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/providers/evercrypt/fst/EverCrypt.Hash.fst(288,6-288,7): - Module not found: M

(285) * Warning 285 at /__w/FStar/FStar/hacl-star/code/streaming/Hacl.Streaming.Blake2.Params.fst(50,11-50,15): - Module not found: Core

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Lemmas.fst(300,6-300,7): - Module not found: B

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Lemmas.fst(50,6-50,7): - Module not found: S

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Crypto.fst(70,21-70,23): - Module not found: U8

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Impl.Crypto.fst(66,14-66,15): - Module not found: B

(321) * Warning 321: - Did not expect module EverCrypt.CTR.Keys to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/hacl-star/obj/EverCrypt.CTR.Keys.fsti.checked instead of /__w/FStar/FStar/everquic-crypto/obj/EverCrypt.CTR.Keys.fsti.checked

(321) * Warning 321: - Did not expect module EverCrypt.CTR.Keys to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/hacl-star/obj/EverCrypt.CTR.Keys.fst.checked instead of /__w/FStar/FStar/everquic-crypto/obj/EverCrypt.CTR.Keys.fst.checked

(274) * Warning 274: - Implicitly opening namespace 'vale.' shadows module 'lib.meta' in file "/__w/FStar/FStar/hacl-star/lib/Lib.Meta.fst". - Rename "/__w/FStar/FStar/hacl-star/lib/Lib.Meta.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'spec.hash.' shadows module 'test' in file "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst". - Rename "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst" to avoid conflicts.

(274) * Warning 274: - Implicitly opening namespace 'model.' shadows module 'quic' in file "src/QUIC.fsti, src/QUIC.fst". - Rename "src/QUIC.fsti, src/QUIC.fst" to avoid conflicts.

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Public.fsti(9,22-9,31): - module not found in search path: lowparse.bitfields

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Public.fsti(4,26-4,30): - module not found in search path: lowparse.spec.base

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Parse.fst(7,21-7,30): - module not found in search path: lowparse.bitfields

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Parse.fst(5,26-5,37): - module not found in search path: lowparse.spec.combinators

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.Parse.fsti(12,21-12,30): - module not found in search path: lowparse.bitfields

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Spec.Header.fst(5,21-5,30): - module not found in search path: lowparse.bitfields

(274) * Warning 274: - Implicitly opening namespace 'spec.hash.' shadows module 'test' in file "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst". - Rename "/__w/FStar/FStar/hacl-star/providers/test/Test.fsti, /__w/FStar/FStar/hacl-star/providers/test/Test.fst" to avoid conflicts.

(285) * Warning 285 at /__w/FStar/FStar/everquic-crypto/src/QUIC.Secret.Int.fsti(9,21-9,30): - module not found in search path: lowparse.bitfields

(274) * Warning 274: - Implicitly opening namespace 'model.' shadows module 'quic' in file "src/QUIC.fsti, src/QUIC.fst". - Rename "src/QUIC.fsti, src/QUIC.fst" to avoid conflicts.