Unable to authenticate to FlakeHub. Individuals must register at FlakeHub.com; Organizations must create an organization at FlakeHub.com.

Unable to authenticate to FlakeHub. Individuals must register at FlakeHub.com; Organizations must create an organization at FlakeHub.com.

Process completed with exit code 1.

Unable to authenticate to FlakeHub. Individuals must register at FlakeHub.com; Organizations must create an organization at FlakeHub.com.

Process completed with exit code 1.

Unable to authenticate to FlakeHub. Individuals must register at FlakeHub.com; Organizations must create an organization at FlakeHub.com.

Process completed with exit code 2.

(19) * Error 19 at CommonUtils.fst(37,3-38,7): - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/Prims.fst(377,38-377,57)

(72) * Error 72 at ExtraTactics.fst(78,13-78,23): - Identifier not found: nth_binder

(19) * Error 19 at Hist.fst(71,13-71,21): - Subtyping check failed - Expected type wp: hist0 'a {hist_wp_monotonic wp} got type p: (_: Prims.list event_type -> Prims.pure_post 'a) -> _: Prims.list event_type -> Prims.pure_pre - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts.

Process completed with exit code 2.

(19) * Error 19 at MST.Tot.fst(74,13-74,31): - Subtyping check failed - Expected type wp: FStar.Pervasives.st_wp_h FStar.Monotonic.Heap.heap 'a {MST.Repr.st_wp_monotonic FStar.Monotonic.Heap.heap wp} got type p: ( _: _: 'a{Prims.l_True} -> _: _: FStar.Monotonic.Heap.heap{Prims.l_True} -> Type0) -> h: _: FStar.Monotonic.Heap.heap{Prims.l_True} -> Prims.pure_pre - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts.

Process completed with exit code 2.

(37) * Error 37 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Printing.fst(95,15-95,21): - Constructor A.LitDoc not found

Process completed with exit code 137.

(72) * Error 72 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(237,18-237,32): - Identifier not found: lookup_lb_view

(72) * Error 72 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(237,18-237,32): - Identifier not found: lookup_lb_view

(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4): - Could not prove post-condition - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - Also see: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4) - Other related locations: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(243,11-243,96)

(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4): - Could not prove post-condition - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - Also see: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(245,2-257,4) - Other related locations: /__w/FStar/FStar/hacl-star/vale/code/crypto/aes/Vale.AES.GCM_helpers.fst(243,11-243,96)

(72) * Error 72 at /__w/FStar/FStar/hacl-star/vale/code/lib/util/Vale.Lib.Tactics.fst(34,32-34,44): - Identifier not found: bv_of_binder

(72) * Error 72 at /__w/FStar/FStar/hacl-star/vale/code/lib/util/Vale.Lib.Tactics.fst(34,32-34,44): - Identifier not found: bv_of_binder

(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(161,2-163,64): - Subtyping check failed - Expected type Type got type n_arrow dom Type - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - Also see: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(162,10-162,15) - Other related locations: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(160,35-160,40)

(19) * Error 19 at /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(161,2-163,64): - Subtyping check failed - Expected type Type got type n_arrow dom Type - The SMT solver could not prove the query. Use --query_stats for more details. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - Also see: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(162,10-162,15) - Other related locations: /__w/FStar/FStar/hacl-star/vale/specs/interop/Vale.Interop.Base.fst(160,35-160,40)

(19) * Error 19 at /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(263,52-279,5): - Subtyping check failed - Expected type map_blocks_a 0 got type s: FStar.Seq.Base.seq a {FStar.Seq.Base.length s = 0} - Try with --query_stats to get more details - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - Also see: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(267,50-267,54) - Other related locations: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(266,6-266,10)

(19) * Error 19 at /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(263,52-279,5): - Subtyping check failed - Expected type map_blocks_a 0 got type s: FStar.Seq.Base.seq a {FStar.Seq.Base.length s = 0} - Try with --query_stats to get more details - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - Also see: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(267,50-267,54) - Other related locations: /__w/FStar/FStar/hacl-star/lib/Lib.Sequence.fst(266,6-266,10)

(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/stage0/out/lib/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

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

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

(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 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

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(289,14-289,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(289,14-289,16)) and t1 (bound in Pulse.Syntax.Base.fst(173,20-173,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(882,4-882,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(601,47-601,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(600,47-600,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(497,8-497,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(359,8-359,15): - Global binding 'PulseSyntaxExtension.Sugar.eq_decl' is recursive but not used in its body

(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 '@'.

(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.

(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 "/__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 "./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

(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