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.

(72) * Error 72 at src/syntax_extension/PulseSyntaxExtension.Sugar.fst(25,23-25,28): - Identifier not found: [FStarC.Range.range] - Could not resolve module name FStarC.Range

(128) * Error 128 at src/syntax_extension/PulseSyntaxExtension.Err.fst(19,18-19,23): - Module FStarC.Range cannot be found

(72) * Error 72 at src/syntax_extension/PulseSyntaxExtension.SyntaxWrapper.fsti(20,25-20,30): - Identifier not found: [FStarC.Range.range] - Could not resolve module name FStarC.Range

(134) * Error 134 at src/extraction/ExtractPulseOCaml.fst(10,12-10,18): - Namespace FStarC.Effect cannot be found

(134) * Error 134 at src/extraction/ExtractPulseC.fst(5,12-5,18): - Namespace FStarC.Effect cannot be found

(134) * Error 134 at src/extraction/ExtractPulse.fst(5,12-5,18): - Namespace FStarC.Effect cannot be found

(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

(189) * Error 189 at LowParse.Spec.Base.fsti(369,45-369,46): - Expected expression of type bare_parser (*?u5*) _ got expression f of type tot_bare_parser t - See also LowParse.Spec.Base.fsti(369,3-369,4)

Process completed with exit code 2.

(12) * Error 12 at Layered.fst(35,28-35,36): - Expected type _: pair -> Type0 but wp_g x p has type pre_t

(34) * Error 34 at Layered.fst(35,28-35,36): - Computed type pre_t and effect Tot is not compatible with the annotated type _: pair -> Type0 and effect Tot

Process completed with exit code 2.

(189) * Error 189 at /__w/FStar/FStar/hacl-star/vale/code/arch/x64/Vale.X64.QuickCodes.fsti(66,102-66,105): - Expected expression of type Prims.pure_wp' (*?u110*) _ got expression pre of type _: (_: Prims.unit -> Prims.GTot Type0) -> Prims.GTot Type0 - See also /__w/FStar/FStar/hacl-star/vale/code/arch/x64/Vale.X64.QuickCodes.fsti(66,48-66,51)

(189) * Error 189 at /__w/FStar/FStar/hacl-star/vale/code/arch/x64/Vale.X64.QuickCodes.fsti(66,102-66,105): - Expected expression of type Prims.pure_wp' (*?u110*) _ got expression pre of type _: (_: Prims.unit -> Prims.GTot Type0) -> Prims.GTot Type0 - See also /__w/FStar/FStar/hacl-star/vale/code/arch/x64/Vale.X64.QuickCodes.fsti(66,48-66,51)

(189) * Error 189 at /__w/FStar/FStar/hacl-star/vale/code/arch/ppc64le/Vale.PPC64LE.QuickCodes.fsti(66,102-66,105): - Expected expression of type Prims.pure_wp' (*?u110*) _ got expression pre of type _: (_: Prims.unit -> Prims.GTot Type0) -> Prims.GTot Type0 - See also /__w/FStar/FStar/hacl-star/vale/code/arch/ppc64le/Vale.PPC64LE.QuickCodes.fsti(66,48-66,51)

(189) * Error 189 at /__w/FStar/FStar/hacl-star/vale/code/arch/ppc64le/Vale.PPC64LE.QuickCodes.fsti(66,102-66,105): - Expected expression of type Prims.pure_wp' (*?u110*) _ got expression pre of type _: (_: Prims.unit -> Prims.GTot Type0) -> Prims.GTot Type0 - See also /__w/FStar/FStar/hacl-star/vale/code/arch/ppc64le/Vale.PPC64LE.QuickCodes.fsti(66,48-66,51)

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

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

(285) * Warning 285 at src/extraction/ExtractPulse.fst(5,12-5,18): - No modules in namespace FStarC.Effect and no file with that name either

(285) * Warning 285 at src/extraction/ExtractPulse.fst(6,12-6,16): - No modules in namespace FStarC.List and no file with that name either

(285) * Warning 285 at src/extraction/ExtractPulse.fst(7,12-7,16): - No modules in namespace FStarC.Util and no file with that name either

(285) * Warning 285 at src/extraction/ExtractPulse.fst(14,19-14,23): - module not found in search path: fstarc.util

(285) * Warning 285 at src/extraction/ExtractPulseC.fst(5,12-5,18): - No modules in namespace FStarC.Effect and no file with that name either

(285) * Warning 285 at src/extraction/ExtractPulseC.fst(6,12-6,16): - No modules in namespace FStarC.List and no file with that name either

(285) * Warning 285 at src/extraction/ExtractPulseC.fst(7,12-7,16): - No modules in namespace FStarC.Util and no file with that name either

(285) * Warning 285 at src/extraction/ExtractPulseC.fst(15,19-15,23): - module not found in search path: fstarc.util

(285) * Warning 285 at src/extraction/ExtractPulseOCaml.fst(10,12-10,18): - No modules in namespace FStarC.Effect and no file with that name either

(285) * Warning 285 at src/extraction/ExtractPulseOCaml.fst(11,12-11,16): - No modules in namespace FStarC.List and no file with that name either

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.