From d2994fc6c955f9821ae7043eee3c912255a94b34 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 3 May 2024 14:33:26 +0200 Subject: [PATCH 1/6] Bump rustc version --- frontend/exporter/src/traits.rs | 2 +- rust-toolchain.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 8a4f457f8..f358625e3 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -555,7 +555,7 @@ pub mod copy_paste_from_rustc { // Currently, we use a fulfillment context to completely resolve // all nested obligations. This is because they can inform the // inference of the impl's type parameters. - let mut fulfill_cx = >::new(tcx); + let mut fulfill_cx = >::new(&infcx); let impl_source = selection.map(|predicate| { fulfill_cx.register_predicate_obligation(&infcx, predicate.clone()); predicate diff --git a/rust-toolchain.toml b/rust-toolchain.toml index d358713d6..1e7c30d0f 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-06-02" +channel = "nightly-2023-06-12" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] From 7b6b49cebcfabeaa490a2a5470e90548ab9c0060 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 3 May 2024 18:33:16 +0200 Subject: [PATCH 2/6] Bump rustc version --- engine/lib/ast.ml | 2 +- engine/lib/ast_visitors.ml | 12 +-- engine/lib/import_thir.ml | 3 +- engine/lib/subtype.ml | 2 +- frontend/exporter/src/traits.rs | 74 ++++++++----------- frontend/exporter/src/types/copied.rs | 6 ++ rust-toolchain.toml | 2 +- .../toolchain__traits into-fstar.snap | 6 +- 8 files changed, 49 insertions(+), 58 deletions(-) diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index 992f83007..82c5fb119 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -143,7 +143,7 @@ functor ident : impl_ident; } | ImplApp of { impl : impl_expr; args : impl_expr list } - | Dyn of trait_goal + | Dyn | Builtin of trait_goal | FnPointer of ty (* The `IE` suffix is there because visitors conflicts...... *) diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml index 56dc32317..dcf12c9a1 100644 --- a/engine/lib/ast_visitors.ml +++ b/engine/lib/ast_visitors.ml @@ -172,9 +172,7 @@ functor self#visit_list self#visit_impl_expr env record_payload.args in ImplApp { impl; args } - | Dyn x0 -> - let x0 = self#visit_trait_goal env x0 in - Dyn x0 + | Dyn -> Dyn | Builtin x0 -> let x0 = self#visit_trait_goal env x0 in Builtin x0 @@ -1113,9 +1111,7 @@ functor in let reduce_acc = self#plus reduce_acc reduce_acc' in (ImplApp { impl; args }, reduce_acc) - | Dyn x0 -> - let x0, reduce_acc = self#visit_trait_goal env x0 in - (Dyn x0, reduce_acc) + | Dyn -> (Dyn, self#zero) | Builtin x0 -> let x0, reduce_acc = self#visit_trait_goal env x0 in (Builtin x0, reduce_acc) @@ -2301,9 +2297,7 @@ functor in let reduce_acc = self#plus reduce_acc reduce_acc' in reduce_acc - | Dyn x0 -> - let reduce_acc = self#visit_trait_goal env x0 in - reduce_acc + | Dyn -> self#zero | Builtin x0 -> let reduce_acc = self#visit_trait_goal env x0 in reduce_acc diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 0f746afe3..95b73ccf3 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -938,6 +938,7 @@ end) : EXPR = struct TOpaque (Concrete_ident.of_def_id Type def_id) | Alias { kind = Inherent; _ } -> unimplemented [ span ] "type Alias::Inherent" + | Alias { kind = Weak; _ } -> unimplemented [ span ] "type Alias::Weak" | Param { index; name } -> (* TODO: [id] might not unique *) TParam { name; id = Local_ident.mk_id Typ (MyInt64.to_int_exn index) } @@ -987,7 +988,7 @@ end) : EXPR = struct | LocalBound { clause_id; path; _ } -> let init = LocalBound { id = clause_id } in List.fold ~init ~f:browse_path path - | Dyn { trait } -> Dyn (c_trait_ref span trait) + | Dyn -> Dyn | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path | Builtin { trait } -> Builtin (c_trait_ref span trait) | FnPointer { fn_ty } -> FnPointer (c_ty span fn_ty) diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml index e55925237..835861fda 100644 --- a/engine/lib/subtype.ml +++ b/engine/lib/subtype.ml @@ -70,7 +70,7 @@ struct impl = dimpl_expr span impl; args = List.map ~f:(dimpl_expr span) args; } - | Dyn tr -> Dyn (dtrait_goal span tr) + | Dyn -> Dyn | Builtin tr -> Builtin (dtrait_goal span tr) | ClosureIE todo -> ClosureIE todo | FnPointer ty -> FnPointer (dty span ty) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index f358625e3..1e921c561 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -19,51 +19,66 @@ pub enum ImplExprPathChunk { }, } +/// The source of a particular trait implementation. Most often this is either `Concrete` for a +/// concrete `impl Trait for Type {}` item, or `LocalBound` for a context-bound `where T: Trait`. #[derive( Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, JsonSchema, )] pub enum ImplExprAtom { + /// A concrete `impl Trait for Type {}` item. Concrete { id: GlobalIdent, generics: Vec, }, + /// A context-bound clause like `where T: Trait`. LocalBound { clause_id: u64, r#trait: Binder, path: Vec, }, + /// The automatic clause `Self: Trait` present inside a `impl Trait for Type {}` item. SelfImpl { r#trait: Binder, path: Vec, }, - /// `dyn TRAIT` is a wrapped value with a virtual table for trait - /// `TRAIT`. In other words, a value `dyn TRAIT` is a dependent + /// `dyn Trait` is a wrapped value with a virtual table for trait + /// `Trait`. In other words, a value `dyn Trait` is a dependent /// triple that gathers a type τ, a value of type τ and an - /// instance of type `TRAIT`. - Dyn { - r#trait: TraitRef, - }, - Builtin { - r#trait: TraitRef, - }, - FnPointer { - fn_ty: Box, - }, + /// instance of type `Trait`. + /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that + /// built-in implementation. + Dyn, + /// A built-in trait whose implementation is computed by the compiler, such as `Sync`. + Builtin { r#trait: TraitRef }, + /// Function pointer types (e.g. `fn(bool, u32) -> u32`) automaticlaly implement some traits + /// such as `Copy` and the appropriate `Fn` traits. + /// FIXME: currently unused because rustc no longer identifies those explicitly. + FnPointer { fn_ty: Box }, + /// Closures automatically implement the appropriate `Fn` traits. + /// FIXME: currently unused because rustc no longer identifies those explicitly. Closure { closure_def_id: DefId, parent_substs: Vec, signature: Box, }, + /// Anything else. Currently used for trait upcasting and trait aliases. Todo(String), } +/// An `ImplExpr` describes the full data of a trait implementation. Because of generics, this may +/// need to combine several concrete trait implementation items. For example, `((1u8, 2u8), +/// "hello").clone()` combines the generic implementation of `Clone` for `(A, B)` with the +/// concrete implementations for `u8` and `&str`, represented as a tree. #[derive( Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, JsonSchema, )] pub struct ImplExpr { + /// The trait this is an impl for. + pub r#trait: TraitRef, + /// The kind of implemention of the root of the tree. pub r#impl: ImplExprAtom, + /// A list of `ImplExpr`s required to fully specify the trait references in `impl`. pub args: Box>, - pub r#trait: TraitRef, } mod search_clause { @@ -377,38 +392,13 @@ impl<'tcx> IntoImplExpr<'tcx> for rustc_middle::ty::PolyTraitRef<'tcx> { .with_args(impl_exprs(s, &nested), trait_ref) } } - // Happens when we use a function pointer as an object implementing - // a trait like `FnMut` - ImplSource::FnPointer(rustc_trait_selection::traits::ImplSourceFnPointerData { - fn_ty, - nested, - }) => ImplExprAtom::FnPointer { - fn_ty: fn_ty.sinto(s), + ImplSource::Object(data) => { + ImplExprAtom::Dyn.with_args(impl_exprs(s, &data.nested), trait_ref) } - .with_args(impl_exprs(s, &nested), trait_ref), - ImplSource::Closure(rustc_trait_selection::traits::ImplSourceClosureData { - closure_def_id, - substs, - nested, - }) => { - let substs = substs.as_closure(); - let parent_substs = substs.parent_substs().sinto(s); - let signature = Box::new(substs.sig().sinto(s)); - ImplExprAtom::Closure { - closure_def_id: closure_def_id.sinto(s), - parent_substs, - signature, - } - .with_args(impl_exprs(s, &nested), trait_ref) - } - ImplSource::Object(data) => ImplExprAtom::Dyn { - r#trait: data.upcast_trait_ref.skip_binder().sinto(s), - } - .with_args(impl_exprs(s, &data.nested), trait_ref), - ImplSource::Builtin(x) => ImplExprAtom::Builtin { + ImplSource::Builtin(nested) => ImplExprAtom::Builtin { r#trait: self.skip_binder().sinto(s), } - .with_args(impl_exprs(s, &x.nested), trait_ref), + .with_args(impl_exprs(s, &nested), trait_ref), x => ImplExprAtom::Todo(format!( "ImplExprAtom::Todo(see https://github.com/hacspec/hax/issues/381) {:#?}\n\n{:#?}", x, self diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index cdbe68186..329e488f2 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1546,6 +1546,7 @@ pub struct Alias { pub def_id: DefId, } +/// Reflects [`rustc_middle::ty::AliasKind`] #[derive( Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord, )] @@ -1557,8 +1558,12 @@ pub enum AliasKind { /// The `Type` in `Ty: Trait<..., Type = U>`. assoc_item: AssocItem, }, + /// An associated type in an inherent impl. Inherent, + /// An `impl Trait` opaque type. Opaque, + /// A type alias that references opaque types. Likely to always be normalized away. + Weak, } impl Alias { @@ -1578,6 +1583,7 @@ impl Alias { } RustAliasKind::Inherent => AliasKind::Inherent, RustAliasKind::Opaque => AliasKind::Opaque, + RustAliasKind::Weak => AliasKind::Weak, }; Alias { kind, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 1e7c30d0f..c98b28911 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-06-12" +channel = "nightly-2023-06-18" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 96e9610ce..f73ac375b 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -82,8 +82,8 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 = class t_Foo (v_Self: Type) = { f_AssocType:Type; - f_AssocType_14574884306673035349:t_SuperTrait f_AssocType; - f_AssocType_15671956332092790358:Core.Clone.t_Clone f_AssocType; + f_AssocType_7709027004138830043:t_SuperTrait f_AssocType; + f_AssocType_11415341696577095690:Core.Clone.t_Clone f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> bool; f_assoc_f_post:Prims.unit -> Prims.unit -> bool; @@ -130,7 +130,7 @@ let g (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; - f_AssocType_14574884306673035349 = FStar.Tactics.Typeclasses.solve; + f_AssocType_7709027004138830043 = FStar.Tactics.Typeclasses.solve; f_N = sz 32; f_assoc_f_pre = (fun (_: Prims.unit) -> true); f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true); From ae77c060083e67cf14910bc214d66295d68aa7ad Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 May 2024 11:32:18 +0200 Subject: [PATCH 3/6] `Box>` is silly --- frontend/exporter/src/traits.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 1e921c561..b1e7ce4d8 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -78,7 +78,7 @@ pub struct ImplExpr { /// The kind of implemention of the root of the tree. pub r#impl: ImplExprAtom, /// A list of `ImplExpr`s required to fully specify the trait references in `impl`. - pub args: Box>, + pub args: Vec, } mod search_clause { @@ -280,7 +280,7 @@ impl ImplExprAtom { fn with_args(self, args: Vec, r#trait: TraitRef) -> ImplExpr { ImplExpr { r#impl: self, - args: Box::new(args), + args, r#trait, } } From 122a64ea640776942309796368bd2fcbe998424a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 6 May 2024 13:58:37 +0200 Subject: [PATCH 4/6] Bump rustc version --- frontend/exporter/src/types/copied.rs | 20 ++++++++++++++++++-- rust-toolchain.toml | 2 +- 2 files changed, 19 insertions(+), 3 deletions(-) diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index 329e488f2..aef78cd1c 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -177,15 +177,31 @@ pub enum UnOp { #[derive(AdtInto, Copy, Clone, Debug, Serialize, Deserialize, JsonSchema)] #[args(<'slt, S: UnderOwnerState<'slt>>, from: rustc_middle::mir::BinOp, state: S as _s)] pub enum BinOp { + // We merge the checked and unchecked variants because in either case overflow is failure. + #[custom_arm( + rustc_middle::mir::BinOp::Add | rustc_middle::mir::BinOp::AddUnchecked => BinOp::Add, + )] Add, + #[custom_arm( + rustc_middle::mir::BinOp::Sub | rustc_middle::mir::BinOp::SubUnchecked => BinOp::Sub, + )] Sub, + #[custom_arm( + rustc_middle::mir::BinOp::Mul | rustc_middle::mir::BinOp::MulUnchecked => BinOp::Mul, + )] Mul, Div, Rem, BitXor, BitAnd, BitOr, + #[custom_arm( + rustc_middle::mir::BinOp::Shl | rustc_middle::mir::BinOp::ShlUnchecked => BinOp::Shl, + )] Shl, + #[custom_arm( + rustc_middle::mir::BinOp::Shr | rustc_middle::mir::BinOp::ShrUnchecked => BinOp::Shr, + )] Shr, Eq, Lt, @@ -3240,6 +3256,8 @@ pub enum ClauseKind { TypeOutlives(TypeOutlivesPredicate), Projection(ProjectionPredicate), ConstArgHasType(ConstantExpr, Ty), + WellFormed(GenericArg), + ConstEvaluatable(ConstantExpr), } /// Reflects [`rustc_middle::ty::Clause`] @@ -3368,12 +3386,10 @@ pub enum ClosureKind { )] pub enum PredicateKind { Clause(Clause), - WellFormed(GenericArg), ObjectSafe(DefId), ClosureKind(DefId, Vec, ClosureKind), Subtype(SubtypePredicate), Coerce(CoercePredicate), - ConstEvaluatable(ConstantExpr), ConstEquate(ConstantExpr, ConstantExpr), TypeWellFormedFromEnv(Ty), Ambiguous, diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c98b28911..518fd28cd 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-06-18" +channel = "nightly-2023-06-20" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] From f2e20faac7d35cf035f9797e467aaea8403da862 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 6 May 2024 15:21:02 +0200 Subject: [PATCH 5/6] feat: get rid of `ImplExprAtom::{FnPointer,Closure}` --- engine/lib/ast.ml | 3 --- engine/lib/ast_visitors.ml | 18 ------------------ engine/lib/import_thir.ml | 2 -- engine/lib/subtype.ml | 2 -- frontend/exporter/src/traits.rs | 11 ----------- 5 files changed, 36 deletions(-) diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index 82c5fb119..10cc44808 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -145,9 +145,6 @@ functor | ImplApp of { impl : impl_expr; args : impl_expr list } | Dyn | Builtin of trait_goal - | FnPointer of ty - (* The `IE` suffix is there because visitors conflicts...... *) - | ClosureIE of todo and trait_goal = { trait : concrete_ident; args : generic_value list } (** A fully applied trait: [Foo] (or diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml index dcf12c9a1..1f9ce20f7 100644 --- a/engine/lib/ast_visitors.ml +++ b/engine/lib/ast_visitors.ml @@ -176,12 +176,6 @@ functor | Builtin x0 -> let x0 = self#visit_trait_goal env x0 in Builtin x0 - | FnPointer x0 -> - let x0 = self#visit_ty env x0 in - FnPointer x0 - | ClosureIE x0 -> - let x0 = self#visit_todo env x0 in - ClosureIE x0 method visit_trait_goal (env : 'env) (this : trait_goal) : trait_goal = let trait = self#visit_concrete_ident env this.trait in @@ -1115,12 +1109,6 @@ functor | Builtin x0 -> let x0, reduce_acc = self#visit_trait_goal env x0 in (Builtin x0, reduce_acc) - | FnPointer x0 -> - let x0, reduce_acc = self#visit_ty env x0 in - (FnPointer x0, reduce_acc) - | ClosureIE x0 -> - let x0, reduce_acc = self#visit_todo env x0 in - (ClosureIE x0, reduce_acc) method visit_trait_goal (env : 'env) (this : trait_goal) : trait_goal * 'acc = @@ -2301,12 +2289,6 @@ functor | Builtin x0 -> let reduce_acc = self#visit_trait_goal env x0 in reduce_acc - | FnPointer x0 -> - let reduce_acc = self#visit_ty env x0 in - reduce_acc - | ClosureIE x0 -> - let reduce_acc = self#visit_todo env x0 in - reduce_acc method visit_trait_goal (env : 'env) (this : trait_goal) : 'acc = let reduce_acc = self#visit_concrete_ident env this.trait in diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 95b73ccf3..2a515162b 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -991,8 +991,6 @@ end) : EXPR = struct | Dyn -> Dyn | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path | Builtin { trait } -> Builtin (c_trait_ref span trait) - | FnPointer { fn_ty } -> FnPointer (c_ty span fn_ty) - | Closure _ as x -> ClosureIE ([%show: Thir.impl_expr_atom] x) | Todo str -> failwith @@ "impl_expr_atom: Todo " ^ str and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml index 835861fda..76c2db4b9 100644 --- a/engine/lib/subtype.ml +++ b/engine/lib/subtype.ml @@ -72,8 +72,6 @@ struct } | Dyn -> Dyn | Builtin tr -> Builtin (dtrait_goal span tr) - | ClosureIE todo -> ClosureIE todo - | FnPointer ty -> FnPointer (dty span ty) and dgeneric_value (span : span) (generic_value : A.generic_value) : B.generic_value = diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index b1e7ce4d8..bc6ac4b71 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -50,17 +50,6 @@ pub enum ImplExprAtom { Dyn, /// A built-in trait whose implementation is computed by the compiler, such as `Sync`. Builtin { r#trait: TraitRef }, - /// Function pointer types (e.g. `fn(bool, u32) -> u32`) automaticlaly implement some traits - /// such as `Copy` and the appropriate `Fn` traits. - /// FIXME: currently unused because rustc no longer identifies those explicitly. - FnPointer { fn_ty: Box }, - /// Closures automatically implement the appropriate `Fn` traits. - /// FIXME: currently unused because rustc no longer identifies those explicitly. - Closure { - closure_def_id: DefId, - parent_substs: Vec, - signature: Box, - }, /// Anything else. Currently used for trait upcasting and trait aliases. Todo(String), } From 22177f09d74e3608f09570cfec1882529392c2a4 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 6 May 2024 15:42:29 +0200 Subject: [PATCH 6/6] fix(proof-libs): reflect `alloc` changes --- .../core/Alloc.Collections.Binary_heap.fsti | 31 +++++++++---------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti b/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti index 5c8875782..d925c6db5 100644 --- a/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti +++ b/proof-libs/fstar/core/Alloc.Collections.Binary_heap.fsti @@ -1,28 +1,27 @@ module Alloc.Collections.Binary_heap open Rust_primitives -val t_BinaryHeap: Type -> eqtype +val t_BinaryHeap: Type -> unit -> eqtype -val impl_9__new: #t:Type -> t_BinaryHeap t -val impl_9__push: #t:Type -> t_BinaryHeap t -> t -> t_BinaryHeap t -val impl_10__len: #t:Type -> t_BinaryHeap t -> usize -val impl_10__iter: #t:Type -> t_BinaryHeap t -> t_Slice t +val impl_10__new: #t:Type -> t_BinaryHeap t () +val impl_10__push: #t:Type -> t_BinaryHeap t () -> t -> t_BinaryHeap t () +val impl_11__len: #t:Type -> t_BinaryHeap t () -> usize +val impl_11__iter: #t:Type -> t_BinaryHeap t () -> t_Slice t open Core.Option -val impl_10__peek: #t:Type -> t_BinaryHeap t -> t_Option t -val impl_9__pop: #t:Type -> t_BinaryHeap t -> t_BinaryHeap t & t_Option t +val impl_11__peek: #t:Type -> t_BinaryHeap t () -> t_Option t +val impl_10__pop: #t:Type -> t_BinaryHeap t () -> t_BinaryHeap t () & t_Option t unfold -let nonempty h = v (impl_10__len h) > 0 +let nonempty h = v (impl_11__len h) > 0 -val lemma_peek_len: #t:Type -> h: t_BinaryHeap t - -> Lemma (Option_Some? (impl_10__peek h) <==> nonempty h) +val lemma_peek_len: #t:Type -> h: t_BinaryHeap t () + -> Lemma (Option_Some? (impl_11__peek h) <==> nonempty h) -val lemma_pop_len: #t:Type -> h: t_BinaryHeap t - -> Lemma (Option_Some? (snd (impl_9__pop h)) <==> nonempty h) - -val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t - -> Lemma (impl_10__peek h == snd (impl_9__pop h)) - [SMTPat (impl_10__peek h)] +val lemma_pop_len: #t:Type -> h: t_BinaryHeap t () + -> Lemma (Option_Some? (snd (impl_10__pop h)) <==> nonempty h) +val lemma_peek_pop: #t:Type -> h: t_BinaryHeap t () + -> Lemma (impl_11__peek h == snd (impl_10__pop h)) + [SMTPat (impl_11__peek h)]