From 591da2b985d7c2e1388c5e1ad595f225c90ab90e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 17 Jan 2025 15:48:45 +0100 Subject: [PATCH 1/5] Fix order of `Call` trait clauses --- frontend/exporter/src/types/mir.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index ffc2535c2..24bf3d8c0 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -398,9 +398,11 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: BaseState<'tcx> + H // Solve the trait constraints of the impl block. let container_generics = tcx.generics_of(container_def_id); let container_generics = generics.truncate_to(tcx, container_generics); - let container_trait_refs = + // Prepend the container trait refs. + let mut combined_trait_refs = solve_item_required_traits(s, container_def_id, container_generics); - trait_refs.extend(container_trait_refs); + combined_trait_refs.extend(std::mem::take(&mut trait_refs)); + trait_refs = combined_trait_refs; (generics.sinto(s), None) } } From 7b86f40acb2f4d5844a9316fd5cc4cc192f8e53b Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 20 Jan 2025 10:38:13 +0100 Subject: [PATCH 2/5] doc: add more information in PUBLISHING.md --- PUBLISHING.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/PUBLISHING.md b/PUBLISHING.md index 8929b334e..857f0b517 100644 --- a/PUBLISHING.md +++ b/PUBLISHING.md @@ -58,3 +58,9 @@ Note: for now, we are not publishing to Opam. Instead, let's just advertise the opam pin hax-engine https://github.com/hacspec/hax.git#the-release-tag opam install hax-engine ``` + +## Notes +`cargo release` reads the `Cargo.toml` of each crates of the workspace. +Some creates are excluded from releasing: in their `Cargo.toml` manifest, they have `package.metadata.release.release` set to `false`. + +Also, `cli/subcommands/Cargo.toml` specifies pre-release replacements for the engine: the version of the engine is bumped automatically by `cargo release`. From 5723687cee67f4f33cc5f2dfbe60c6820144d09a Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 20 Jan 2025 10:29:02 +0100 Subject: [PATCH 3/5] chore: Release --- Cargo.lock | 30 +++++++++++++++--------------- Cargo.toml | 20 ++++++++++---------- engine/dune-project | 2 +- engine/hax-engine.opam | 2 +- 4 files changed, 27 insertions(+), 27 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 265b869ac..c0569f138 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -144,7 +144,7 @@ dependencies = [ [[package]] name = "cargo-hax" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "annotate-snippets", "cargo_metadata", @@ -445,7 +445,7 @@ checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" [[package]] name = "hax-adt-into" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "itertools", "proc-macro2", @@ -456,7 +456,7 @@ dependencies = [ [[package]] name = "hax-bounded-integers" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "duplicate", "hax-lib", @@ -465,7 +465,7 @@ dependencies = [ [[package]] name = "hax-driver" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "clap", "colored", @@ -483,7 +483,7 @@ dependencies = [ [[package]] name = "hax-engine-names" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-lib", "hax-lib-protocol", @@ -491,7 +491,7 @@ dependencies = [ [[package]] name = "hax-engine-names-extract" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-adt-into", "hax-engine-names", @@ -502,7 +502,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "extension-traits", "hax-adt-into", @@ -518,7 +518,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-adt-into", "schemars", @@ -528,7 +528,7 @@ dependencies = [ [[package]] name = "hax-lib" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-lib-macros", "num-bigint", @@ -537,7 +537,7 @@ dependencies = [ [[package]] name = "hax-lib-macros" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "hax-lib", "hax-lib-macros-types", @@ -550,7 +550,7 @@ dependencies = [ [[package]] name = "hax-lib-macros-types" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "proc-macro2", "quote", @@ -562,14 +562,14 @@ dependencies = [ [[package]] name = "hax-lib-protocol" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "libcrux", ] [[package]] name = "hax-lib-protocol-macros" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -579,7 +579,7 @@ dependencies = [ [[package]] name = "hax-test-harness" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "assert_cmd", "cargo_metadata", @@ -595,7 +595,7 @@ dependencies = [ [[package]] name = "hax-types" -version = "0.1.0-rc.1" +version = "0.1.0" dependencies = [ "annotate-snippets", "clap", diff --git a/Cargo.toml b/Cargo.toml index ea7eb8493..787666de0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -32,7 +32,7 @@ default-members = [ resolver = "2" [workspace.package] -version = "0.1.0-rc.1" +version = "0.1.0" authors = ["hax Authors"] license = "Apache-2.0" homepage = "https://github.com/hacspec/hax" @@ -71,14 +71,14 @@ colored = "2" annotate-snippets = "0.11" # Crates in this repository -hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0-rc.1", default-features = false } -hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0-rc.1" } -hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0-rc.1" } -hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0-rc.1" } -hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0-rc.1" } -hax-lib = { path = "hax-lib", version = "=0.1.0-rc.1" } -hax-engine-names = { path = "engine/names", version = "=0.1.0-rc.1" } -hax-types = { path = "hax-types", version = "=0.1.0-rc.1" } +hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0", default-features = false } +hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0" } +hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0" } +hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0" } +hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0" } +hax-lib = { path = "hax-lib", version = "=0.1.0" } +hax-engine-names = { path = "engine/names", version = "=0.1.0" } +hax-types = { path = "hax-types", version = "=0.1.0" } [workspace.metadata.release] -owners = ["github:hacspec:crates"] \ No newline at end of file +owners = ["github:hacspec:crates"] diff --git a/engine/dune-project b/engine/dune-project index 5769b572c..a216f477f 100644 --- a/engine/dune-project +++ b/engine/dune-project @@ -2,7 +2,7 @@ (name hax-engine) -(version 0.1.0-rc.1) +(version 0.1.0) (generate_opam_files true) diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam index 56b671995..af7aeae3e 100644 --- a/engine/hax-engine.opam +++ b/engine/hax-engine.opam @@ -1,6 +1,6 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -version: "0.1.0-rc.1" +version: "0.1.0" 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." From ca7947f6725ba9f463d1b6315f58efaf6f4ef4e0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 15 Jan 2025 20:26:36 +0100 Subject: [PATCH 4/5] Only `ImplExprAtom::Concrete` needs nested `ImplExpr`s --- engine/lib/import_thir.ml | 11 ++++++----- frontend/exporter/src/traits.rs | 4 ++-- frontend/exporter/src/traits/resolution.rs | 23 ++++++---------------- 3 files changed, 14 insertions(+), 24 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 2b265117a..646e43d9e 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1099,11 +1099,12 @@ end) : EXPR = struct and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr = let goal = c_trait_ref span ie.trait.value in let impl = { kind = c_impl_expr_atom span ie.impl; goal } in - match ie.args with - | [] -> impl - | args -> - let args = List.map ~f:(c_impl_expr span) args in + match ie.impl with + | Concrete { impl_exprs = []; _ } -> impl + | Concrete { impl_exprs; _ } -> + let args = List.map ~f:(c_impl_expr span) impl_exprs in { kind = ImplApp { impl; args }; goal } + | _ -> impl and c_trait_ref span (tr : Thir.trait_ref) : trait_goal = let trait = Concrete_ident.of_def_id Trait tr.def_id in @@ -1137,7 +1138,7 @@ end) : EXPR = struct Parent { impl = { kind = item_kind; goal = trait_ref }; ident } in match ie with - | Concrete { id; generics } -> + | Concrete { id; generics; _ } -> let trait = Concrete_ident.of_def_id Impl id in let args = List.map ~f:(c_generic_value span) generics in Concrete { trait; args } diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 9b3175489..2b0804ea2 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -62,6 +62,8 @@ pub enum ImplExprAtom { #[from(def_id)] id: GlobalIdent, generics: Vec, + /// The impl exprs that prove the clauses on the impl. + impl_exprs: Vec, }, /// A context-bound clause like `where T: Trait`. LocalBound { @@ -108,8 +110,6 @@ pub struct ImplExpr { pub r#trait: Binder, /// 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: Vec, } /// Given a clause `clause` in the context of some impl block `impl_did`, susbts correctly `Self` diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index cc5377161..fb949eb1c 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -49,6 +49,8 @@ pub enum ImplExprAtom<'tcx> { Concrete { def_id: DefId, generics: GenericArgsRef<'tcx>, + /// The impl exprs that prove the clauses on the impl. + impl_exprs: Vec>, }, /// A context-bound clause like `where T: Trait`. LocalBound { @@ -83,8 +85,6 @@ pub struct ImplExpr<'tcx> { pub r#trait: PolyTraitRef<'tcx>, /// The kind of implemention of the root of the tree. pub r#impl: ImplExprAtom<'tcx>, - /// A list of `ImplExpr`s required to fully specify the trait references in `impl`. - pub args: Vec, } /// Items have various predicates in scope. `path_to` uses them as a starting point for trait @@ -360,7 +360,6 @@ impl<'tcx> PredicateSearcher<'tcx> { let tcx = self.tcx; let impl_source = shallow_resolve_trait_ref(tcx, self.param_env, erased_tref); - let nested; let atom = match impl_source { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, @@ -368,15 +367,14 @@ impl<'tcx> PredicateSearcher<'tcx> { .. })) => { // Resolve the predicates required by the impl. - nested = self.resolve_item_predicates(impl_def_id, generics, warn)?; + let impl_exprs = self.resolve_item_predicates(impl_def_id, generics, warn)?; ImplExprAtom::Concrete { def_id: impl_def_id, generics, + impl_exprs, } } Ok(ImplSource::Param(_)) => { - // Mentioning a local clause requires no extra predicates to hold. - nested = vec![]; match self.resolve_local(erased_tref.upcast(self.tcx), warn)? { Some(candidate) => { let path = candidate.path; @@ -402,17 +400,9 @@ impl<'tcx> PredicateSearcher<'tcx> { } } } - Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => { - nested = vec![]; - ImplExprAtom::Dyn - } - Ok(ImplSource::Builtin(_, _)) => { - // Builtin impls currently don't need nested predicates. - nested = vec![]; - ImplExprAtom::Builtin { r#trait: *tref } - } + Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn, + Ok(ImplSource::Builtin(_, _)) => ImplExprAtom::Builtin { r#trait: *tref }, Err(e) => { - nested = vec![]; let msg = format!( "Could not find a clause for `{tref:?}` in the current context: `{e:?}`" ); @@ -423,7 +413,6 @@ impl<'tcx> PredicateSearcher<'tcx> { Ok(ImplExpr { r#impl: atom, - args: nested, r#trait: *tref, }) } From 0abb7230317c599ab304906e46e359f6864c9f03 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 16 Jan 2025 14:58:39 +0100 Subject: [PATCH 5/5] Add more info to `ImplExprAtom::Builtin` --- engine/lib/import_thir.ml | 2 +- frontend/exporter/src/traits.rs | 14 ++- frontend/exporter/src/traits/resolution.rs | 86 +++++++++++++++++-- .../toolchain__traits into-fstar.snap | 10 +-- 4 files changed, 97 insertions(+), 15 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 646e43d9e..2a47901ac 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1147,7 +1147,7 @@ end) : EXPR = struct List.fold ~init ~f:browse_path path | Dyn -> Dyn | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path - | Builtin { trait } -> Builtin (c_trait_ref span trait.value) + | Builtin { trait; _ } -> Builtin (c_trait_ref span trait.value) | Error str -> failwith @@ "impl_expr_atom: Error " ^ str and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 2b0804ea2..6cf6d99e1 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -92,8 +92,18 @@ pub enum ImplExprAtom { /// `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: Binder }, + /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This + /// morally points to an invisible `impl` block; as such it contains the information we may + /// need from one. + Builtin { + r#trait: Binder, + /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration. + /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T: + /// FnOnce`. + impl_exprs: Vec, + /// The values of the associated types for this trait. + types: Vec<(DefId, Ty)>, + }, /// An error happened while resolving traits. Error(String), } diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index fb949eb1c..8da38c203 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -73,8 +73,18 @@ pub enum ImplExprAtom<'tcx> { /// `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: PolyTraitRef<'tcx> }, + /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This + /// morally points to an invisible `impl` block; as such it contains the information we may + /// need from one. + Builtin { + r#trait: PolyTraitRef<'tcx>, + /// The `ImplExpr`s required to satisfy the implied predicates on the trait declaration. + /// E.g. since `FnMut: FnOnce`, a built-in `T: FnMut` impl would have an `ImplExpr` for `T: + /// FnOnce`. + impl_exprs: Vec>, + /// The values of the associated types for this trait. + types: Vec<(DefId, Ty<'tcx>)>, + }, /// An error happened while resolving traits. Error(String), } @@ -290,7 +300,7 @@ impl<'tcx> PredicateSearcher<'tcx> { // Resolve predicates required to mention the item. let nested_impl_exprs = - self.resolve_item_predicates(alias_ty.def_id, alias_ty.args, warn)?; + self.resolve_item_required_predicates(alias_ty.def_id, alias_ty.args, warn)?; // Add all the bounds on the corresponding associated item. self.extend(item_bounds.map(|(index, pred)| { @@ -367,7 +377,8 @@ impl<'tcx> PredicateSearcher<'tcx> { .. })) => { // Resolve the predicates required by the impl. - let impl_exprs = self.resolve_item_predicates(impl_def_id, generics, warn)?; + let impl_exprs = + self.resolve_item_required_predicates(impl_def_id, generics, warn)?; ImplExprAtom::Concrete { def_id: impl_def_id, generics, @@ -401,7 +412,43 @@ impl<'tcx> PredicateSearcher<'tcx> { } } Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn, - Ok(ImplSource::Builtin(_, _)) => ImplExprAtom::Builtin { r#trait: *tref }, + Ok(ImplSource::Builtin(_, _)) => { + // Resolve the predicates implied by the trait. + let trait_def_id = erased_tref.skip_binder().def_id; + // If we wanted to not skip this binder, we'd have to instantiate the bound + // regions, solve, then wrap the result in a binder. And track higher-kinded + // clauses better all over. + let impl_exprs = self.resolve_item_implied_predicates( + trait_def_id, + erased_tref.skip_binder().args, + warn, + )?; + let types = tcx + .associated_items(trait_def_id) + .in_definition_order() + .filter(|assoc| matches!(assoc.kind, AssocKind::Type)) + .filter_map(|assoc| { + let ty = AliasTy::new(tcx, assoc.def_id, erased_tref.skip_binder().args) + .to_ty(tcx); + let ty = erase_and_norm(tcx, self.param_env, ty); + if let TyKind::Alias(_, alias_ty) = ty.kind() { + if alias_ty.def_id == assoc.def_id { + warn(&format!("Failed to compute associated type {ty}")); + // We can't return the unnormalized associated type as that would + // make the trait ref contain itself, which would make hax's + // `sinto` infrastructure loop. + return None; + } + } + Some((assoc.def_id, ty)) + }) + .collect(); + ImplExprAtom::Builtin { + r#trait: *tref, + impl_exprs, + types, + } + } Err(e) => { let msg = format!( "Could not find a clause for `{tref:?}` in the current context: `{e:?}`" @@ -418,7 +465,19 @@ impl<'tcx> PredicateSearcher<'tcx> { } /// Resolve the predicates required by the given item. - pub fn resolve_item_predicates( + pub fn resolve_item_required_predicates( + &mut self, + def_id: DefId, + generics: GenericArgsRef<'tcx>, + // Call back into hax-related code to display a nice warning. + warn: &impl Fn(&str), + ) -> Result>, String> { + let tcx = self.tcx; + self.resolve_predicates(generics, required_predicates(tcx, def_id), warn) + } + + /// Resolve the predicates implied by the given item. + pub fn resolve_item_implied_predicates( &mut self, def_id: DefId, generics: GenericArgsRef<'tcx>, @@ -426,7 +485,20 @@ impl<'tcx> PredicateSearcher<'tcx> { warn: &impl Fn(&str), ) -> Result>, String> { let tcx = self.tcx; - required_predicates(tcx, def_id) + self.resolve_predicates(generics, implied_predicates(tcx, def_id), warn) + } + + /// Apply the given generics to the provided clauses and resolve the trait references in the + /// current context. + pub fn resolve_predicates( + &mut self, + generics: GenericArgsRef<'tcx>, + predicates: GenericPredicates<'tcx>, + // Call back into hax-related code to display a nice warning. + warn: &impl Fn(&str), + ) -> Result>, String> { + let tcx = self.tcx; + predicates .predicates .iter() .map(|(clause, _span)| *clause) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 9e505d3a1..6ae14d007 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -55,7 +55,7 @@ open FStar.Mul class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit } class t_Foo (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_16210070100893052778:t_Bar v_Self f_U; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_13496126865352171029:t_Bar v_Self f_U; f_U:Type0 } ''' @@ -408,7 +408,7 @@ class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { v_TypeArg v_ConstArg; f_AssocType:Type0; - f_AssocType_7414800425644916102:t_Trait f_AssocType v_TypeArg v_ConstArg + f_AssocType_13704321474071752218:t_Trait f_AssocType v_TypeArg v_ConstArg } ''' "Traits.Interlaced_consts_types.fst" = ''' @@ -485,7 +485,7 @@ open FStar.Mul class t_Trait1 (v_Self: Type0) = { f_T:Type0; - f_T_2328060197809802853:t_Trait1 f_T + f_T_2186006717281159153:t_Trait1 f_T } class t_Trait2 (v_Self: Type0) = { @@ -630,7 +630,7 @@ let use_impl_trait (_: Prims.unit) : Prims.unit = class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_12248650268031145847:t_SuperTrait f_AssocType; + f_AssocType_16668910951696008497:t_SuperTrait f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> Type0; f_assoc_f_post:Prims.unit -> Prims.unit -> Type0; @@ -667,7 +667,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; - f_AssocType_12248650268031145847 = FStar.Tactics.Typeclasses.solve; + f_AssocType_16668910951696008497 = 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);