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 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. - This query was retried due to the --proof_recovery option, yet it still failed on all attempts. - Env = (a : Type) (wp : Prims.pure_wp a) (f : _: Prims.unit -> Prims.PURE a) (p : _: a -> Prims.prop) - VC = forall (p: Prims.pure_post a). wp p /\ (forall (pure_result: a). p pure_result ==> p pure_result) ==> (forall (pure_result: Prims.unit). (forall (a: Type0) (wp: Prims.pure_wp a) (p: Prims.pure_post a) (q: Prims.pure_post a). (forall (x: a). p x ==> q x) ==> wp p ==> wp q) ==> wp (fun bind_result_1 -> bind_result_1 == f () ==> (forall (return_val: a). return_val == bind_result_1 ==> p return_val))) - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/Prims.fst(335,38-335,57)

(12) * Error 12 at BeyondCriteria.fst(22,23-22,28): - Expected type Prims.prop but s2 tr has type Type0

(12) * Error 12 at BeyondCriteria.fst(22,13-22,18): - Expected type Prims.prop but s1 tr has type Type0

(12) * Error 12 at ExtraTactics.fst(9,34-9,39): - Expected type Prims.prop but p x has type Type0

(12) * Error 12 at ExtraTactics.fst(8,15-8,18): - Expected type Prims.prop but p x has type Type0

(12) * Error 12 at Hist.fst(24,97-24,104): - Expected type Prims.prop but p2 lt r has type Type0

(12) * Error 12 at Hist.fst(24,85-24,92): - Expected type Prims.prop but p1 lt r has type Type0

(12) * Error 12 at TC.Checkable.fst(4,33-4,36): - Expected type Prims.prop but p x has type Type0

Process completed with exit code 2.

(134) * Error 134 at STLC.fst(501,11-501,13): - Namespace 'FStar.ST' cannot be found.

(34) * Error 34 at BeyondCriteria.fst(66,8-67,154): - Computed type Type0 and effect Tot is not compatible with the annotated type Prims.prop and effect GTot

(12) * Error 12 at BeyondCriteria.fst(67,10-67,154): - Expected type Prims.prop but comp.rel_sem (comp.source.beh (comp.source.link ps cs)) (comp.target.beh (comp.target.link (comp.compile_pprog ps) ct)) has type Type0

(134) * Error 134 at MST.Repr.fst(7,21-7,25): - Namespace 'FStar.Monotonic.Heap' cannot be found.

Process completed with exit code 2.

(12) * Error 12 at /__w/FStar/FStar/steel/lib/steel/Steel.Witnessed.Core.fsti(9,40-9,44): - Expected type Prims.prop but p s1 has type Type0

(12) * Error 12 at /__w/FStar/FStar/steel/lib/steel/Steel.Witnessed.Core.fsti(9,17-9,21): - Expected type Prims.prop but p s0 has type Type0

Process completed with exit code 2.

(19) * Error 19 at src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.Format.Serialize.fst(1376,45-1376,60): - Ill-typed term - Assertion failed - 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. - Env = (xs : CBOR.Pulse.Raw.Type.cbor_serialized) (p : PulseCore.FractionalPermission.perm) (xh0 : xh0: CBOR.Spec.Raw.Base.raw_data_item{Map? xh0}) (n : n: Prims.nat{n == FStar.UInt64.v xh0.len.value}) (res : LowParse.Pulse.Base.with_perm (Pulse.Lib.Slice.slice LowParse.Bytes.byte )) (__ : Prims.squash (res.v == xs.cbor_serialized_payload /\ res.p == CBOR.Pulse.Raw.Util.perm_mul p xs.cbor_serialized_perm)) (__ : Prims.squash (xs.cbor_serialized_header == xh0.len)) (_n7 : FStar.Ghost.erased Prims.nat) (_r'8 : FStar.Ghost.erased (LowParse.Spec.VCList.nlist _n7 (CBOR.Spec.Raw.Base.raw_data_item & CBOR.Spec.Raw.Base.raw_data_item))) (__ : Prims.squash (xh0.v == _r'8)) - VC = CBOR.Spec.Raw.EverParse.parse_raw_data_item_kind.parser_kind_subkind == FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong /\ (LowParse.Spec.Combinators.and_then_kind CBOR.Spec.Raw.EverParse.parse_raw_data_item_kind CBOR.Spec.Raw.EverParse.parse_raw_data_item_kind) .parser_kind_subkind == FStar.Pervasives.Native.Some LowParse.Spec.Base.ParserStrong - See also src/cbor/pulse/raw/everparse/CBOR.Pulse.Raw.Format.Serialize.fst(1375,2-1376,210)

(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

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PIMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.PIMap.t

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.IMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.IMap.t

(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

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(21,5-21,11): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.p_uvar

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Unionfind.fsti(20,5-20,8): - Adding an implicit 'assume new' qualifier on FStarC.Unionfind.puf

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Hash.fsti(4,5-4,14): - Adding an implicit 'assume new' qualifier on FStarC.Hash.hash_code

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/basic/FStarC.Timing.fsti(20,5-20,12): - Adding an implicit 'assume new' qualifier on FStarC.Timing.time_ns

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.SMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.SMap.t

(239) * Warning 239 at /__w/FStar/FStar/FStar/src/data/FStarC.PSMap.fsti(7,5-7,6): - Adding an implicit 'assume new' qualifier on FStarC.PSMap.t

(285) * Warning 285 at Compiler.StlcToFStar.fst(9,11-9,31): - No modules in namespace FStar.StrongExcludedMiddle and no file with that name either

(285) * Warning 285 at Examples.HOC.fst(4,21-4,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at Examples.Autograder.fst(5,21-5,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at STLC.fst(501,11-501,13): - No modules in namespace FStar.ST and no file with that name either

(285) * Warning 285 at LabeledRefs.fsti(6,24-6,28): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at MST.Repr.fst(10,27-10,36): - module not found in search path: fstar.monotonic.witnessed

(285) * Warning 285 at MST.Repr.fst(7,21-7,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at MST.Tot.fst(6,21-6,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at FullGroundType.fst(6,21-6,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at Witnessable.fst(8,21-8,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

(285) * Warning 285 at SpecTree.fst(4,21-4,25): - No modules in namespace FStar.Monotonic.Heap and no file with that name either

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

(288) * Warning 288 at Unsigned_negation.fst(93,32-93,47): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(93,2-93,73)

(288) * Warning 288 at Unsigned_negation.fst(93,32-93,47): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(93,2-93,73)

(288) * Warning 288 at Unsigned_negation.fst(81,32-81,47): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(81,2-81,73)

(288) * Warning 288 at Unsigned_negation.fst(81,32-81,47): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also Unsigned_negation.fst(81,2-81,73)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(25,4-25,19): - FStar.Int.Cast.uint64_to_int64 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(170,4-170,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)

(288) * Warning 288 at Pulse.Lib.C.Casts.fst(21,4-21,19): - FStar.Int.Cast.uint32_to_int32 is deprecated - with care; in C the result is implementation-defined when not representable - See also /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Int.Cast.fst(155,4-155,19)

(321) * Warning 321: - Did not expect module Pulse.Main to be already checked. - Found it in an unexpected location: /__w/FStar/FStar/fstar/lib/fstar/pulse/common.checked/Pulse.Main.fsti.checked instead of _cache/Pulse.Main.fsti.checked

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

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Char.fsti(0,0-0,0): - Interface FStar.Char is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.Attributes.fsti(0,0-0,0): - Interface FStar.Attributes is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/ulib/FStar.All.fsti(0,0-0,0): - Interface FStar.All is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Main.fsti(0,0-0,0): - Interface Pulse.Main is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.NonInformative.fsti(0,0-0,0): - Interface Pulse.Lib.NonInformative is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Loc.fsti(0,0-0,0): - Interface Pulse.Lib.Loc is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Dv.fsti(0,0-0,0): - Interface Pulse.Lib.Dv is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Core.fsti(0,0-0,0): - Interface Pulse.Lib.Core is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Core.Refs.fsti(0,0-0,0): - Interface Pulse.Lib.Core.Refs is admitted without an implementation

(335) * Warning 335 at /__w/FStar/FStar/fstar/lib/fstar/pulse/common/Pulse.Lib.Core.Inv.fsti(0,0-0,0): - Interface Pulse.Lib.Core.Inv is admitted without an implementation

(285) * Warning 285 at src/lowparse/LowParse.Low.Combinators.fsti(5,29-5,35): - module not found in search path: lowstar.monotonic.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.FLData.fst(8,18-8,28): - module not found in search path: fstar.hyperstack

(285) * Warning 285 at src/lowparse/LowParse.Low.FLData.fst(7,30-7,32): - module not found in search path: fstar.hyperstack.st

(285) * Warning 285 at src/lowparse/LowParse.Low.FLData.fst(5,19-5,25): - module not found in search path: lowstar.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.VLData.fst(44,18-44,28): - module not found in search path: fstar.hyperstack

(285) * Warning 285 at src/lowparse/LowParse.Low.VLData.fst(7,30-7,32): - module not found in search path: fstar.hyperstack.st

(285) * Warning 285 at src/lowparse/LowParse.Low.VLData.fst(6,19-6,25): - module not found in search path: lowstar.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.Array.fst(205,18-205,28): - module not found in search path: fstar.hyperstack

(285) * Warning 285 at src/lowparse/LowParse.Low.Array.fst(173,19-173,25): - module not found in search path: lowstar.buffer

(285) * Warning 285 at src/lowparse/LowParse.Low.Array.fst(10,30-10,32): - module not found in search path: fstar.hyperstack.st

(359) * Warning 359 at CLRS.Ch23.MST.Spec.fst(956,4-1046,9): - This query succeeded after increasing its rlimit by 2x - Increase the rlimit in the file or simplify the proof. This is only succeeding due to --proof_recovery being given.