diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam index f9ae457ad..a1c46c487 100644 --- a/engine/hax-engine.opam +++ b/engine/hax-engine.opam @@ -1,5 +1,6 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" +version: "0.1.0-alpha.1" synopsis: "The engine of hax, a Rust verification tool" description: "Hax is divided in two: a frontend (written in Rust) and an engine (written in OCaml). This is the engine." diff --git a/frontend/exporter/src/constant_utils.rs b/frontend/exporter/src/constant_utils.rs index 281816af3..cf91501dd 100644 --- a/frontend/exporter/src/constant_utils.rs +++ b/frontend/exporter/src/constant_utils.rs @@ -374,7 +374,7 @@ mod rustc { let name = assoc.name.to_string(); // Retrieve the trait information - let impl_expr = get_trait_info(s, generics, assoc); + let impl_expr = self_clause_for_item(s, assoc, generics).unwrap(); ConstantExprKind::TraitConst { impl_expr, name } } diff --git a/frontend/exporter/src/rustc_utils.rs b/frontend/exporter/src/rustc_utils.rs index c20fb0683..2e8601b86 100644 --- a/frontend/exporter/src/rustc_utils.rs +++ b/frontend/exporter/src/rustc_utils.rs @@ -12,17 +12,6 @@ impl<'tcx, T: ty::TypeFoldable>> ty::Binder<'tcx, T> { } } -// TODO: this seems to be constructing a `Self: Trait` clause. Document what it does exactly. -pub fn poly_trait_ref<'tcx, S: UnderOwnerState<'tcx>>( - s: &S, - assoc: &ty::AssocItem, - generics: ty::GenericArgsRef<'tcx>, -) -> Option> { - let tcx = s.base().tcx; - let r#trait = tcx.trait_of_item(assoc.def_id)?; - Some(ty::Binder::dummy(ty::TraitRef::new(tcx, r#trait, generics))) -} - #[tracing::instrument(skip(s))] pub(crate) fn arrow_of_sig<'tcx, S: UnderOwnerState<'tcx>>(sig: &ty::PolyFnSig<'tcx>, s: &S) -> Ty { Ty::Arrow(Box::new(sig.sinto(s))) diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 6553fe247..a04b6fafa 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -91,29 +91,6 @@ pub mod rustc { use rustc_hir::def_id::DefId; use rustc_middle::ty::*; - /// This is the entrypoint of the solving. - impl<'tcx, S: crate::UnderOwnerState<'tcx>> crate::SInto - for rustc_middle::ty::PolyTraitRef<'tcx> - { - #[tracing::instrument(level = "trace", skip(s))] - fn sinto(&self, s: &S) -> crate::ImplExpr { - tracing::trace!( - "Enters sinto ({})", - stringify!(rustc_middle::ty::PolyTraitRef<'tcx>) - ); - use crate::ParamEnv; - let warn = |msg: &str| { - if !s.base().ty_alias_mode { - crate::warning!(s, "{}", msg) - } - }; - match impl_expr(s.base().tcx, s.owner_id(), s.param_env(), self, &warn) { - Ok(x) => x.sinto(s), - Err(e) => crate::fatal!(s, "{}", e), - } - } - } - /// Items have various predicates in scope. `path_to` uses them as a starting point for trait /// resolution. This tracks where each of them comes from. #[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)] @@ -239,65 +216,59 @@ pub mod rustc { use itertools::Itertools; use rustc_hir::def_id::DefId; use rustc_middle::ty::*; + use std::collections::{hash_map::Entry, HashMap}; - fn erase_and_norm<'tcx>( - tcx: TyCtxt<'tcx>, - param_env: ParamEnv<'tcx>, - x: PolyTraitPredicate<'tcx>, - ) -> PolyTraitPredicate<'tcx> { - tcx.erase_regions(tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x)) + /// Erase all regions. Largely copied from `tcx.erase_regions`. + fn erase_all_regions<'tcx, T>(tcx: TyCtxt<'tcx>, value: T) -> T + where + T: TypeFoldable>, + { + use rustc_middle::ty; + struct RegionEraserVisitor<'tcx> { + tcx: TyCtxt<'tcx>, + } + + impl<'tcx> TypeFolder> for RegionEraserVisitor<'tcx> { + fn cx(&self) -> TyCtxt<'tcx> { + self.tcx + } + + fn fold_ty(&mut self, ty: Ty<'tcx>) -> Ty<'tcx> { + ty.super_fold_with(self) + } + + fn fold_binder(&mut self, t: ty::Binder<'tcx, T>) -> ty::Binder<'tcx, T> + where + T: TypeFoldable>, + { + // Empty the binder + Binder::dummy(t.skip_binder().fold_with(self)) + } + + fn fold_region(&mut self, _r: ty::Region<'tcx>) -> ty::Region<'tcx> { + // We erase bound regions despite it being possibly incorrect. `for<'a> fn(&'a + // ())` and `fn(&'free ())` are different types: they may implement different + // traits and have a different `TypeId`. It's unclear whether this can cause us + // to select the wrong trait reference. + self.tcx.lifetimes.re_erased + } + } + value.fold_with(&mut RegionEraserVisitor { tcx }) } - /// Custom equality on `Predicate`s. - /// - /// Sometimes Rustc inserts extra generic arguments: I noticed - /// some `__H` second argument given to core::hash::Hash for - /// instance. `__H` seems to be inserted in [1]. Such extra - /// arguments seems to be ignored by `default_print_def_path` [2]. - /// - /// Hence, for now, equality is decided by comparing the debug - /// string representations of `Predicate`s. - /// - /// Note there exist also predicates that are different, - /// `Eq`-wise, but whose `sinto` counterpart are equal. - /// - /// TODO: figure out how to implement this function in a sane way. - /// - /// [1]: https://github.com/rust-lang/rust/blob/b0889cb4ed0e6f3ed9f440180678872b02e7052c/compiler/rustc_builtin_macros/src/deriving/hash.rs#L20 - /// [2]: https://github.com/rust-lang/rust/blob/b0889cb4ed0e6f3ed9f440180678872b02e7052c/compiler/rustc_middle/src/ty/print/mod.rs#L141 - fn predicate_equality<'tcx>( + // Lifetimes are irrelevant when resolving instances. + pub(super) fn erase_and_norm<'tcx, T>( tcx: TyCtxt<'tcx>, - x: PolyTraitPredicate<'tcx>, - y: PolyTraitPredicate<'tcx>, - param_env: rustc_middle::ty::ParamEnv<'tcx>, - ) -> bool { - // Lifetime and constantness are irrelevant when resolving instances - let x = erase_and_norm(tcx, param_env, x); - let y = erase_and_norm(tcx, param_env, y); - let x: Predicate = x.upcast(tcx); - let y: Predicate = y.upcast(tcx); - let sx = format!("{:?}", x.kind().skip_binder()); - let sy = format!("{:?}", y.kind().skip_binder()); - - // const DEBUG: bool = false; - // if DEBUG && result { - // use crate::{Predicate, SInto}; - // let xs: Predicate = x.sinto(s); - // let ys: Predicate = y.sinto(s); - // if x != y { - // eprintln!( - // "######################## predicate_equality ########################" - // ); - // eprintln!("x={:#?}", x); - // eprintln!("y={:#?}", y); - // eprintln!( - // "######################## sinto ########################" - // ); - // eprintln!("sinto(x)={:#?}", xs); - // eprintln!("sinto(y)={:#?}", ys); - // } - // } - sx == sy + param_env: ParamEnv<'tcx>, + x: T, + ) -> T + where + T: TypeFoldable> + Copy, + { + erase_all_regions( + tcx, + tcx.try_normalize_erasing_regions(param_env, x).unwrap_or(x), + ) } #[tracing::instrument(level = "trace", skip(tcx))] @@ -329,7 +300,7 @@ pub mod rustc { struct PredicateSearcher<'tcx> { tcx: TyCtxt<'tcx>, param_env: rustc_middle::ty::ParamEnv<'tcx>, - candidates: Vec>, + candidates: HashMap, Candidate<'tcx>>, } impl<'tcx> PredicateSearcher<'tcx> { @@ -361,36 +332,25 @@ pub mod rustc { fn extend(&mut self, candidates: impl IntoIterator>) { let tcx = self.tcx; // Filter out duplicated candidates. - let new_candidates: Vec<_> = candidates - .into_iter() - .filter(|candidate| { - !self - .candidates - .iter() - .any(|seen_candidate: &Candidate<'tcx>| { - predicate_equality( - tcx, - candidate.pred, - seen_candidate.pred, - self.param_env, - ) - }) - }) - .collect(); - if new_candidates.is_empty() { - return; + let mut new_candidates = Vec::new(); + for mut candidate in candidates { + // Normalize and erase all lifetimes. + candidate.pred = erase_and_norm(tcx, self.param_env, candidate.pred); + if let Entry::Vacant(entry) = self.candidates.entry(candidate.pred) { + entry.insert(candidate.clone()); + new_candidates.push(candidate); + } + } + if !new_candidates.is_empty() { + self.extend_parents(new_candidates); } - // Add the candidates and their parents. - self.extend_inner(new_candidates); } - /// Add the given candidates without filtering for duplicates. This is a separate - /// function to avoid polymorphic recursion due to the closures capturing the type - /// parameters of this function. - fn extend_inner(&mut self, new_candidates: Vec>) { + /// Add the parents of these candidates. This is a separate function to avoid + /// polymorphic recursion due to the closures capturing the type parameters of this + /// function. + fn extend_parents(&mut self, new_candidates: Vec>) { let tcx = self.tcx; - // First append all the new candidates. - self.candidates.extend(new_candidates.iter().cloned()); // Then recursively add their parents. This way ensures a breadth-first order, // which means we select the shortest path when looking up predicates. self.extend(new_candidates.into_iter().flat_map(|candidate| { @@ -416,7 +376,8 @@ pub mod rustc { /// add the relevant implied associated type bounds to the set as well. fn lookup(&mut self, target: PolyTraitRef<'tcx>) -> Option<&Candidate<'tcx>> { let tcx = self.tcx; - let target: PolyTraitPredicate = target.upcast(tcx); + let target: PolyTraitPredicate = + erase_and_norm(tcx, self.param_env, target).upcast(tcx); // The predicate is `::Type: OtherTrait`. We look up `T as Trait` in // the current context and add all the bounds on `Trait::Type` to our context. @@ -450,26 +411,18 @@ pub mod rustc { })); } - tracing::trace!( - "Looking for {target:?} in: [\n{}\n]", - self.candidates - .iter() - .map(|c| format!(" {c:?}\n")) - .join("") - ); - for candidate in &self.candidates { - if predicate_equality(tcx, candidate.pred, target, self.param_env) { - return Some(candidate); - } + tracing::trace!("Looking for {target:?}"); + let ret = self.candidates.get(&target); + if ret.is_none() { + tracing::trace!( + "Couldn't find {target:?} in: [\n{}]", + self.candidates + .iter() + .map(|(_, c)| format!(" - {:?}\n", c.pred)) + .join("") + ); } - tracing::trace!( - "Couldn't find {target:?} in: [\n{}\n]", - self.candidates - .iter() - .map(|c| format!(" {c:?}\n")) - .join("") - ); - None + ret } } @@ -560,7 +513,9 @@ pub mod rustc { ) -> Result>, String> { obligations .iter() - .flat_map(|obligation| { + // Only keep depth-1 obligations to avoid duplicate impl exprs. + .filter(|obligation| obligation.recursion_depth == 1) + .filter_map(|obligation| { obligation.predicate.as_trait_clause().map(|trait_ref| { impl_expr( tcx, @@ -575,7 +530,7 @@ pub mod rustc { } #[tracing::instrument(level = "trace", skip(tcx, param_env, warn))] - fn impl_expr<'tcx>( + pub(super) fn impl_expr<'tcx>( tcx: TyCtxt<'tcx>, owner_id: DefId, param_env: rustc_middle::ty::ParamEnv<'tcx>, @@ -676,9 +631,7 @@ pub mod rustc { (param_env, trait_ref): (ty::ParamEnv<'tcx>, ty::PolyTraitRef<'tcx>), ) -> Result, CodegenObligationError> { - let trait_ref = tcx - .try_normalize_erasing_regions(param_env, trait_ref) - .unwrap_or(trait_ref); + let trait_ref = super::search_clause::erase_and_norm(tcx, param_env, trait_ref); // Do the initial selection for the obligation. This yields the // shallow result we are looking for -- that is, what specific impl. @@ -742,16 +695,6 @@ pub mod rustc { } } -#[cfg(feature = "rustc")] -impl<'tcx, S: UnderOwnerState<'tcx>> SInto - for rustc_middle::ty::PolyTraitPredicate<'tcx> -{ - fn sinto(&self, s: &S) -> ImplExpr { - use rustc_middle::ty::ToPolyTraitRef; - self.to_poly_trait_ref().sinto(s) - } -} - /// Given a clause `clause` in the context of some impl block `impl_did`, susbts correctly `Self` /// from `clause` and (1) derive a `Clause` and (2) resolve an `ImplExpr`. #[cfg(feature = "rustc")] @@ -761,6 +704,7 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>( clause: rustc_middle::ty::Clause<'tcx>, span: rustc_span::Span, ) -> Option<(Clause, ImplExpr, Span)> { + use rustc_middle::ty::ToPolyTraitRef; let tcx = s.base().tcx; let impl_trait_ref = tcx .impl_trait_ref(impl_did) @@ -772,8 +716,100 @@ pub fn super_clause_to_clause_and_impl_expr<'tcx, S: UnderOwnerState<'tcx>>( clause.sinto(s).id }; let new_clause = clause.instantiate_supertrait(tcx, impl_trait_ref); - let impl_expr = new_clause.as_predicate().as_trait_clause()?.sinto(s); + let impl_expr = solve_trait( + s, + new_clause + .as_predicate() + .as_trait_clause()? + .to_poly_trait_ref(), + ); let mut new_clause_no_binder = new_clause.sinto(s); new_clause_no_binder.id = original_predicate_id; Some((new_clause_no_binder, impl_expr, span.sinto(s))) } + +/// This is the entrypoint of the solving. +#[cfg(feature = "rustc")] +#[tracing::instrument(level = "trace", skip(s))] +pub fn solve_trait<'tcx, S: BaseState<'tcx> + HasOwnerId>( + s: &S, + trait_ref: rustc_middle::ty::PolyTraitRef<'tcx>, +) -> ImplExpr { + use crate::ParamEnv; + let warn = |msg: &str| { + if !s.base().ty_alias_mode { + crate::warning!(s, "{}", msg) + } + }; + match rustc::impl_expr(s.base().tcx, s.owner_id(), s.param_env(), &trait_ref, &warn) { + Ok(x) => x.sinto(s), + Err(e) => crate::fatal!(s, "{}", e), + } +} + +/// Solve the trait obligations for a specific item use (for example, a method call, an ADT, etc.). +/// +/// [predicates]: optional predicates, in case we want to solve custom predicates (instead of the +/// ones returned by [TyCtxt::predicates_defined_on]. +#[cfg(feature = "rustc")] +#[tracing::instrument(level = "trace", skip(s), ret)] +pub fn solve_item_traits<'tcx, S: UnderOwnerState<'tcx>>( + s: &S, + def_id: rustc_hir::def_id::DefId, + generics: rustc_middle::ty::GenericArgsRef<'tcx>, + predicates: Option>, +) -> Vec { + let tcx = s.base().tcx; + let param_env = s.param_env(); + + let mut impl_exprs = Vec::new(); + + // Lookup the predicates and iter through them: we want to solve all the + // trait requirements. + // IMPORTANT: we use [TyCtxt::predicates_defined_on] and not [TyCtxt::predicated_of] + let predicates = match predicates { + None => tcx.predicates_defined_on(def_id), + Some(preds) => preds, + }; + for (pred, _) in predicates.predicates { + // Explore only the trait predicates + if let Some(trait_clause) = pred.as_trait_clause() { + let poly_trait_ref = trait_clause.map_bound(|clause| clause.trait_ref); + // Apply the substitution + let poly_trait_ref = + rustc_middle::ty::EarlyBinder::bind(poly_trait_ref).instantiate(tcx, generics); + // Warning: this erases regions. We don't really have a way to normalize without + // erasing regions, but this may cause problems in trait solving if there are trait + // impls that include `'static` lifetimes. + let poly_trait_ref = tcx + .try_normalize_erasing_regions(param_env, poly_trait_ref) + .unwrap_or(poly_trait_ref); + let impl_expr = solve_trait(s, poly_trait_ref); + impl_exprs.push(impl_expr); + } + } + impl_exprs +} + +/// Retrieve the `Self: Trait` clause for a trait associated item. +#[cfg(feature = "rustc")] +pub fn self_clause_for_item<'tcx, S: UnderOwnerState<'tcx>>( + s: &S, + assoc: &rustc_middle::ty::AssocItem, + generics: rustc_middle::ty::GenericArgsRef<'tcx>, +) -> Option { + let tcx = s.base().tcx; + + // Retrieve the trait + let tr_def_id = tcx.trait_of_item(assoc.def_id)?; + + // Create the reference to the trait + use rustc_middle::ty::TraitRef; + let tr_generics = tcx.generics_of(tr_def_id); + let generics = generics.truncate_to(tcx, tr_generics); + let tr_ref = TraitRef::new(tcx, tr_def_id, generics); + let tr_ref = rustc_middle::ty::Binder::dummy(tr_ref); + + // Solve + Some(solve_trait(s, tr_ref)) +} diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index e08a0d274..80a5359be 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -1796,10 +1796,9 @@ impl Alias { ); AliasKind::Opaque } else { - let impl_expr = Binder::dummy(trait_ref).sinto(s); AliasKind::Projection { assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s), - impl_expr, + impl_expr: solve_trait(s, Binder::dummy(trait_ref)), } } } @@ -2444,16 +2443,10 @@ pub enum ExprKind { let tcx = gstate.base().tcx; r#trait = (|| { let assoc_item = tcx.opt_associated_item(*def_id)?; - let assoc_trait = tcx.trait_of_item(assoc_item.def_id)?; - let trait_ref = ty::TraitRef::new(tcx, assoc_trait, generics.iter()); - let impl_expr: ImplExpr = { - // TODO: we should not wrap into a dummy binder - let poly_trait_ref = ty::Binder::dummy(trait_ref); - poly_trait_ref.sinto(gstate) - }; + let impl_expr = self_clause_for_item(gstate, &assoc_item, generics)?; let assoc_generics = tcx.generics_of(assoc_item.def_id); - let assoc_generics = translated_generics.drain(0..assoc_generics.parent_count); - Some((impl_expr, assoc_generics.collect())) + let assoc_generics = translated_generics.drain(0..assoc_generics.parent_count).collect(); + Some((impl_expr, assoc_generics)) })(); generic_args = translated_generics; bounds_impls = solve_item_traits(gstate, *def_id, generics, None); @@ -2702,8 +2695,8 @@ pub enum ExprKind { #[value({ let tcx = gstate.base().tcx; tcx.opt_associated_item(*def_id).as_ref().and_then(|assoc| { - poly_trait_ref(gstate, assoc, args) - }).map(|poly_trait_ref| poly_trait_ref.sinto(gstate)) + self_clause_for_item(gstate, assoc, args) + }) })] r#impl: Option, }, @@ -3624,7 +3617,7 @@ impl<'tcx, S: UnderBinderState<'tcx>> SInto unreachable!() }; ProjectionPredicate { - impl_expr: poly_trait_ref.sinto(s), + impl_expr: solve_trait(s, poly_trait_ref), assoc_item: tcx.associated_item(alias_ty.def_id).sinto(s), ty, } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 3a59a398f..8e85f8f51 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -383,7 +383,7 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: BaseState<'tcx> + H match assoc.container { rustc_middle::ty::AssocItemContainer::TraitContainer => { // Retrieve the trait information - let impl_expr = get_trait_info(s, generics, &assoc); + let impl_expr = self_clause_for_item(s, &assoc, generics).unwrap(); // Return only the method generics; the trait generics are included in `impl_expr`. let method_generics = &generics[num_container_generics..]; (method_generics.sinto(s), Option::Some(impl_expr)) diff --git a/frontend/exporter/src/types/mir_traits.rs b/frontend/exporter/src/types/mir_traits.rs index fa7564a62..fa2fa5f1e 100644 --- a/frontend/exporter/src/types/mir_traits.rs +++ b/frontend/exporter/src/types/mir_traits.rs @@ -1,88 +1,5 @@ use crate::prelude::*; -/// Retrieve the trait information, typically for a function call. -/// TODO: rename -pub fn get_trait_info<'tcx, S: UnderOwnerState<'tcx>>( - s: &S, - generics: rustc_middle::ty::GenericArgsRef<'tcx>, - assoc: &rustc_middle::ty::AssocItem, -) -> ImplExpr { - let tcx = s.base().tcx; - - // Retrieve the trait - let tr_def_id = tcx.trait_of_item(assoc.def_id).unwrap(); - - // Create the reference to the trait - use rustc_middle::ty::TraitRef; - let tr_ref = TraitRef::new(tcx, tr_def_id, generics); - let tr_ref = rustc_middle::ty::Binder::dummy(tr_ref); - - // Solve - solve_trait(s, tr_ref) -} - -pub fn solve_trait<'tcx, S: BaseState<'tcx> + HasOwnerId>( - s: &S, - trait_ref: rustc_middle::ty::PolyTraitRef<'tcx>, -) -> ImplExpr { - let mut impl_expr: ImplExpr = trait_ref.sinto(s); - // TODO: this is a bug in hax: in case of method calls, the trait ref - // contains the generics for the trait ref + the generics for the method - let trait_def_id: rustc_hir::def_id::DefId = - (&impl_expr.r#trait.as_ref().hax_skip_binder().def_id).into(); - let params_info = get_params_info(s, trait_def_id); - impl_expr - .r#trait - .inner_mut() - .generic_args - .truncate(params_info.num_generic_params); - impl_expr -} - -/// Solve the trait obligations for a specific item use (for example, a method -/// call, an ADT, etc.). -/// -/// [predicates]: optional predicates, in case we want to solve custom predicates -/// (instead of the ones returned by [TyCtxt::predicates_defined_on]. -#[tracing::instrument(level = "trace", skip(s))] -pub fn solve_item_traits<'tcx, S: UnderOwnerState<'tcx>>( - s: &S, - def_id: rustc_hir::def_id::DefId, - generics: rustc_middle::ty::GenericArgsRef<'tcx>, - predicates: Option>, -) -> Vec { - let tcx = s.base().tcx; - let param_env = s.param_env(); - - let mut impl_exprs = Vec::new(); - - // Lookup the predicates and iter through them: we want to solve all the - // trait requirements. - // IMPORTANT: we use [TyCtxt::predicates_defined_on] and not [TyCtxt::predicated_of] - let predicates = match predicates { - None => tcx.predicates_defined_on(def_id), - Some(preds) => preds, - }; - for (pred, _) in predicates.predicates { - // Explore only the trait predicates - if let Some(trait_clause) = pred.as_trait_clause() { - let poly_trait_ref = trait_clause.map_bound(|clause| clause.trait_ref); - // Apply the substitution - let poly_trait_ref = - rustc_middle::ty::EarlyBinder::bind(poly_trait_ref).instantiate(tcx, generics); - // Warning: this erases regions. We don't really have a way to normalize without - // erasing regions, but this may cause problems in trait solving if there are trait - // impls that include `'static` lifetimes. - let poly_trait_ref = tcx - .try_normalize_erasing_regions(param_env, poly_trait_ref) - .unwrap_or(poly_trait_ref); - let impl_expr = solve_trait(s, poly_trait_ref); - impl_exprs.push(impl_expr); - } - } - impl_exprs -} - /// We use this to store information about the parameters in parent blocks. /// This is necessary because when querying the generics of a definition, /// rustc gives us *all* the generics used in this definition, including diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 79d1a6115..2c6d55fa9 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -314,7 +314,7 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" [[package]] name = "hax-lib" -version = "0.1.0-pre.1" +version = "0.1.0-alpha.1" dependencies = [ "hax-lib-macros", "num-bigint", @@ -323,7 +323,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.1.0-pre.1" +version = "0.1.0-alpha.1" dependencies = [ "hax-lib-macros-types", "paste", @@ -335,7 +335,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.1.0-pre.1" +version = "0.1.0-alpha.1" dependencies = [ "proc-macro2", "quote", @@ -346,14 +346,14 @@ dependencies = [ [[package]] name = "hax-lib-protocol" -version = "0.1.0-pre.1" +version = "0.1.0-alpha.1" dependencies = [ "libcrux", ] [[package]] name = "hax-lib-protocol-macros" -version = "0.1.0-pre.1" +version = "0.1.0-alpha.1" dependencies = [ "proc-macro-error", "proc-macro2",