Process completed with exit code 1.

Process completed with exit code 1.

Process completed with exit code 1.

(12) * Error 12 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(597,2-597,37): - Expected type Type but vdep_payload v p _ has type Type0

(34) * Error 34 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(597,2-597,37): - Computed type Type0 and effect Prims.PURE is not compatible with the annotated type Type and effect GTot

Process completed with exit code 2.

(189) * Error 189 at src/checker/Pulse.Common.fst(63,0-68,16): - Expected expression of type f: (_: (*?u95*) _ -> FStar.Pervasives.Native.option (*?u90*) _) -> Type got expression fun _ -> (*?u95*) _ of type f: (_: (*?u95*) _ -> FStar.Pervasives.Native.option (*?u90*) _) -> Prims.GTot Type

(54) * Error 54 at lib/core/Pulse.Lib.NonInformative.fst(32,21-33,62): - (*?u42*) _ is not equal to the expected type y: a{y == FStar.Ghost.elift1 (fun _ -> _._1) p} & (*?u12*) _

(54) * Error 54 at lib/core/PulseCore.PartialNondeterministicHoareStateMonad.fsti(20,52-20,53): - _: Prims.unit -> Prims.nat is not a subtype of the expected type _: Prims.unit -> FStar.Pervasives.Dv (k: Prims.nat{k == n}) - See also lib/core/PulseCore.PartialNondeterministicHoareStateMonad.fsti(20,14-20,15)

(66) * Error 66 at lib/core/PulseCore.HeapExtension.fsti(291,25-291,32): - Failed to resolve implicit argument ?24 of type Type introduced for Instantiating implicit argument

(66) * Error 66 at lib/core/PulseCore.BaseHeapSig.fsti(300,25-300,32): - Failed to resolve implicit argument ?21 of type Type introduced for Instantiating implicit argument

Process completed with exit code 2.

(66) * Error 66 at LowParse.Spec.Base.fsti(369,26-369,42): - Failed to resolve implicit argument ?5 of type Type introduced for Instantiating implicit argument

Process completed with exit code 2.

(189) * Error 189 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,12-193,16): - Expected expression of type _: FStar.Pervasives.Native.option (*?u23*) _ -> Type got expression fun _ -> (*?u23*) _ of type _: FStar.Pervasives.Native.option (*?u23*) _ -> Prims.GTot Type - See also /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,4-193,8)

(189) * Error 189 at /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,12-193,16): - Expected expression of type _: FStar.Pervasives.Native.option (*?u23*) _ -> Type got expression fun _ -> (*?u23*) _ of type _: FStar.Pervasives.Native.option (*?u23*) _ -> Prims.GTot Type - See also /__w/FStar/FStar/hacl-star/code/meta/Meta.Interface.fst(193,4-193,8)

(66) * Error 66 at /__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17): - Failed to resolve implicit argument ?33 of type Type introduced for user-provided implicit term at /__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17)

(66) * Error 66 at /__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17): - Failed to resolve implicit argument ?33 of type Type introduced for user-provided implicit term at /__w/FStar/FStar/hacl-star/lib/Lib.Buffer.fst(452,16-452,17)

(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17): - Failed to resolve implicit argument ?48 of type Type introduced for user-provided implicit term at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17)

(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17): - Failed to resolve implicit argument ?48 of type Type introduced for user-provided implicit term at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Bignum.ModInvLimb.fst(44,16-44,17)

(19) * Error 19 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,6-501,12): - Assertion failed - See also /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,13-501,26)

(19) * Error 19 at /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,6-501,12): - Assertion failed - See also /__w/FStar/FStar/hacl-star/code/bignum/Hacl.Spec.Bignum.Lib.fst(501,13-501,26)

(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17): - Failed to resolve implicit argument ?29 of type Type introduced for user-provided implicit term at /__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17)

(66) * Error 66 at /__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17): - Failed to resolve implicit argument ?29 of type Type introduced for user-provided implicit term at /__w/FStar/FStar/hacl-star/code/frodo/Hacl.Impl.Frodo.Encode.fst(178,16-178,17)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

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

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

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

(288) * Warning 288 at /__w/FStar/FStar/FStar/ulib/FStar.Reflection.V2.Arith.fst(116,20-116,31): - FStar.Stubs.Tactics.V2.Builtins.term_eq_old is deprecated - Use Reflection.term_eq instead - See also /__w/FStar/FStar/FStar/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti(446,0-446,42)

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

(337) * Warning 337 at /__w/FStar/FStar/FStar/src/data/FStarC.RBSet.fst(105,30-105,31): - 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/data/FStarC.RBSet.fst(105,36-105,37): - 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(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(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 '@'.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

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

(337) * Warning 337 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2068,65-2068,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 '@'.

(361) * Warning 361 at /__w/FStar/FStar/steel/lib/steel/Steel.Semantics.Hoare.MST.fst(1351,0-1372,15): - Some #push-options have not been popped. Current depth is 1.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(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

(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(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(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(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(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(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(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(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(59,11-59,18): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also FStar.Krml.Endianness.fst(21,8-21,15)

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

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

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

(337) * Warning 337 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(621,47-621,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 src/syntax_extension/PulseSyntaxExtension.Sugar.fst(622,47-622,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 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 '@'.

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

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fsti(372,16-372,18): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of t1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fsti(372,16-372,18)) and b1 (bound in src/checker/Pulse.Syntax.Base.fst(291,15-291,17)) are equal. - The type of the first term is: Pulse.Syntax.Base.st_term - The type of the second term is: Pulse.Syntax.Base.pattern & Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

(290) * Warning 290 at src/checker/Pulse.Syntax.Base.fst(121,20-121,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in src/checker/Pulse.Syntax.Base.fst(121,20-121,22)) and pb1 (bound in src/checker/Pulse.Syntax.Base.fst(137,16-137,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 src/checker/Pulse.Syntax.Base.fst(137,16-137,19): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in src/checker/Pulse.Syntax.Base.fst(137,16-137,19)) and p1 (bound in src/checker/Pulse.Syntax.Base.fst(121,20-121,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.

(290) * Warning 290 at src/checker/Pulse.Syntax.Base.fst(291,15-291,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in src/checker/Pulse.Syntax.Base.fst(291,15-291,17)) and t1 (bound in src/checker/Pulse.Syntax.Base.fst(169,20-169,22)) are equal. - The type of the first term is: Pulse.Syntax.Base.pattern & Pulse.Syntax.Base.st_term - The type of the second term is: Pulse.Syntax.Base.st_term - If the proof fails, try annotating these with the same type.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

(361) * Warning 361 at LowParse.BitFields.fst(1276,0-1276,29): - Some #push-options have not been popped. Current depth is 1.

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

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

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

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

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

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

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

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

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

(333) * Warning 333: - Unable to open hints file: .hints/Rust2.fst.hints; ran without hints

(333) * Warning 333: - Unable to open hints file: .hints/Rust3.fst.hints; ran without hints

ubuntu-latest pipelines will use ubuntu-24.04 soon. For more details, see https://github.com/actions/runner-images/issues/10636

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

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

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

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

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

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

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

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

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