(72) * Error 72 at /__w/FStar/FStar/karamel/runtime/WasmSupport.fst(64,10-64,13): - Identifier not found: [C.Loops.for] - Could not resolve module name C.Loops

Process completed with exit code 2.

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(448,0-448,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

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

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

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

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

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

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

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

(288) * Warning 288 at /__w/FStar/FStar/karamel/krmllib/FStar.Krml.Endianness.fst(57,56-57,63): - FStar.Krml.Endianness.le_to_n is deprecated - FStar.Endianness.le_to_n - See also /__w/FStar/FStar/karamel/krmllib/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

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

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(802,9-802,20): - 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(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(1612,18-1612,29): - 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(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(1632,7-1632,18): - 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(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(1638,7-1638,18): - 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(448,0-448,42)

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

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2204,11-2204,22): - 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(448,0-448,42)

(288) * Warning 288 at /__w/FStar/FStar/steel/lib/steel/Steel.Effect.Common.fsti(2782,10-2782,21): - 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(448,0-448,42)

(352) * Warning 352 at /__w/FStar/FStar/steel/lib/steel/Steel.ST.Effect.fsti(170,16-170,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(171,19-171,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

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 /__w/FStar/FStar/pulse/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 /__w/FStar/FStar/pulse/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 /__w/FStar/FStar/pulse/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 /__w/FStar/FStar/pulse/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 /__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 '@'.

(328) * Warning 328 at /__w/FStar/FStar/pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst(781,4-781,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.fst(125,20-125,22): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of p1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(125,20-125,22)) and pb1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(141,16-141,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(141,16-141,19): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of pb1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(141,16-141,19)) and p1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(125,20-125,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 /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17)) and t1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(173,20-173,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.

(290) * Warning 290 at /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17): - In the decreases clause for this function, the SMT solver may not be able to prove that the types of b1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(295,15-295,17)) and q1 (bound in /__w/FStar/FStar/pulse/src/checker/Pulse.Syntax.Base.fst(301,14-301,16)) 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.qualifier - 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