New trait encoding scheme and add support for more specific trait impls

Co-authored-by: Lennard Gäher <l.gaeher@posteo.de>

case_studies/minivec/src/lib.rs

@@ -394,6 +394,7 @@ impl<T> Vec<T> {
     #[rr::args("(#(<#> xs), γ)", "Z.of_nat i")]
     #[rr::requires("i < length xs")]
     #[rr::observe("γ": "delete i (<#> xs)")]
+    #[rr::returns("xs !!! i")]
     pub fn remove(&mut self, index: usize) -> T {
         // index out of bounds?
         assert!(index < self.len);

case_studies/tests/output/tests/proofs/proof_traits_foo_call_foobar.v

@@ -7,20 +7,21 @@ Set Default Proof Using "Type".
 Section proof.
 Context `{!refinedrustGS Σ}.
 
-
 Lemma traits_foo_call_foobar_proof (π : thread_id) :
   traits_foo_call_foobar_lemma π.
 Proof.
   traits_foo_call_foobar_prelude.
 
   repeat liRStep; liShow.
-  liInst Hevar1 (int i32).
-  liInst Hevar0 (int u32).
-  rep liRStep.
 
   all: print_remaining_goal.
-  Unshelve. all: sidecond_solver.
+  Unshelve. 
+  all: sidecond_solver.
   Unshelve. all: sidecond_hammer.
+  { unshelve_sidecond.
+    (* TODO improve solver *)
+    intros. prepare_initial_coq_context.
+    simpl. done. }
   Unshelve. all: print_remaining_sidecond.
 Qed.
 End proof.

case_studies/tests/output/tests/proofs/proof_traits_foo_call_foobar2.v

@@ -4,6 +4,7 @@ From refinedrust.examples.tests.generated Require Import generated_code_tests ge
 
 Set Default Proof Using "Type".
 
+
 Section proof.
 Context `{!refinedrustGS Σ}.
 
@@ -12,10 +13,6 @@ Lemma traits_foo_call_foobar2_proof (π : thread_id) :
 Proof.
   traits_foo_call_foobar2_prelude.
 
-  repeat liRStep; liShow.
-  liInst Hevar0 (int i32).
-  repeat liRStep; liShow.
-  liInst Hevar1 (traits_foo_Foo_W_i32_Output_ty).
   repeat liRStep; liShow.
 
   all: print_remaining_goal.

case_studies/tests/output/tests/proofs/proof_traits_foo_foobar.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.tests.generated Require Import generated_code_tests generated_specs_tests generated_template_traits_foo_foobar.
+
+Set Default Proof Using "Type".
+
+
+Section proof.
+Context `{!refinedrustGS Σ}.
+
+Lemma traits_foo_foobar_proof (π : thread_id) :
+  traits_foo_foobar_lemma π.
+Proof.
+  traits_foo_foobar_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/tests/output/tests/proofs/proof_traits_foo_foobar_ref.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.tests.generated Require Import generated_code_tests generated_specs_tests generated_template_traits_foo_foobar_ref.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{RRGS : !refinedrustGS Σ}.
+
+Lemma traits_foo_foobar_ref_proof (π : thread_id) :
+  traits_foo_foobar_ref_lemma π.
+Proof.
+  traits_foo_foobar_ref_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/tests/output/tests/proofs/proof_traits_foo_foobar_ref2.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.tests.generated Require Import generated_code_tests generated_specs_tests generated_template_traits_foo_foobar_ref2.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{RRGS : !refinedrustGS Σ}.
+
+Ltac multirepeat tac :=
+  match goal with
+  | |- _ => tac
+  | _ => fail 1000
+  end.
+
+Lemma traits_foo_foobar_ref2_proof (π : thread_id) :
+  traits_foo_foobar_ref2_lemma π.
+Proof.
+  traits_foo_foobar_ref2_prelude.
+
+  rep <-! liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  { (* TODO: augment the lft alive solver to handle symbolic cases *)
+    admit.
+    }
+  { solve_elctx_sat.
+  notypeclasses refine (tac_elctx_app_ty_outlives_E _ _ _ _ _ _).
+         solve_elctx_submseteq. 
+    refine (tac_lctx_lft_incl_init_list _ _ _ _ _).
+
+  (*Ltac multirepeat tac ::=*)
+  (*lazymatch goal with*)
+  (*| |- ?H => idtac H; tac; tac; first [solve [fail] | multirepeat tac]*)
+  (*| |- _ => fail*)
+  (*end.*)
+
+
+    (* TODO: 
+       problem here:
+       - see the notes on the elctx rule in the inclusion solver.
+       - the same lifetime can appear multiple times on the LHS of the elctx
+       - there may be cycles
+       - So expanding/following an inclusion isn't always safe and may get us into cycles or deadlocks.
+
+
+       Can we normalize the context before to fix this?
+       Can we convert to multiinclusions that are always safe? e.g. left-ro-right or right-to-left?
+
+       In principle, we could follow inclusions on both sides, but always include all candidates.
+       Then we use an exists- exists interpretation, i.e., we need to find a match on both sides.
+       Problem: this can quickly explode
+     *)
+
+    (*list_find_tac*)
+    (*
+    Ltac list_find_tac_noindex' cont l ::=
+  multimatch l with
+  | [] => fail
+  | ?h :: ?l => (cont h)
+  | ?h :: ?l => (list_find_tac_noindex' cont l)
+  | _ ++ ?l => list_find_tac_noindex' cont l
+  end.
+multimatch goal with
+| |- lctx_lft_incl_list ?E ?L ?κs1 ?κs2 =>
+        let find_in_elctx j κ :=
+         list_find_tac_noindex
+          ltac:(fun el =>
+                  multimatch el with
+                  | κ ⊑ₑ ?κ' =>
+                      notypeclasses refine
+                       (tac_lctx_lft_incl_list_augment_external E L κ κ' κs1
+                          κs2 j _ _ _);
+                       [ elctx_list_elem_solver | reflexivity | simpl;
+                           match goal with 
+                           | |- ?H2 => idtac H2
+                            end ]
+                  | _ => fail
+                  end) E
+        in
+        list_find_tac find_in_elctx κs1;
+        solve_lft_incl_list_step
+
+end.
+notypeclasses refine (tac_lctx_lft_incl_list_augment_external _ _ ϝ0 κ _ _ 0 _ _ _);
+                    [ elctx_list_elem_solver | reflexivity | simpl ];
+                        solve_lft_incl_list_step.
+
+solve_lft_incl_list_step;
+solve_lft_incl_list_step; solve[fail].
+  multirepeat solve_lft_incl_list_step.
+
+    match goal with
+         first [ solve_lft_incl_list_step | done].
+      (* TODO: here, the solver gets misled and should backtrack *)
+    solve_elctx_sat_step.
+     *)
+
+  (* TODO look at these *)
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/tests/output/tests/proofs/proof_traits_foo_foobar_ref3.v

+From caesium Require Import lang notation.
+From refinedrust Require Import typing shims.
+From refinedrust.examples.tests.generated Require Import generated_code_tests generated_specs_tests generated_template_traits_foo_foobar_ref3.
+
+Set Default Proof Using "Type".
+
+Section proof.
+Context `{RRGS : !refinedrustGS Σ}.
+
+Lemma traits_foo_foobar_ref3_proof (π : thread_id) :
+  traits_foo_foobar_ref3_lemma π.
+Proof.
+  traits_foo_foobar_ref3_prelude.
+
+  repeat liRStep; liShow.
+
+  all: print_remaining_goal.
+  Unshelve. all: sidecond_solver.
+  Unshelve. all: sidecond_hammer.
+  (* TODO: look at these *)
+  Unshelve. all: print_remaining_sidecond.
+Qed.
+End proof.

case_studies/tests/src/generics.rs

+
+#[rr::params("x")]
+#[rr::args("x")]
+fn generic1<T>(x: T) {
+
+}
+
+#[rr::verify]
+fn call_generic1_1() {
+    generic1(42);
+}
+
+#[rr::verify]
+fn call_generic1_2() {
+    let x = 1;
+    generic1(&x);
+}
+
+// TODO missing annotations to generate
+#[rr::skip]
+fn call_generic1_3() {
+    let x = 1;
+    let y = 2;
+    generic1((&x, &y));
+}
+
+#[rr::params("x")]
+#[rr::args("#x")]
+fn generic2<'a, T>(x : &'a T) {
+
+}
+
+#[rr::verify]
+fn call_generic2_1() {
+    let x = 1;
+    generic2(&x);
+}
+
+#[rr::params("x")]
+#[rr::args("#x")]
+fn generic3<'a>(x : &'a i32) {
+
+}
+
+#[rr::verify]
+fn call_generic3_1() {
+    let x = 1;
+    generic3(&x);
+}

case_studies/tests/src/lib.rs

@@ -6,7 +6,9 @@
 mod enums;
 mod structs;
 mod char;
+
 mod traits;
+
 mod statics;
 
 mod vec_client;
@@ -15,3 +17,5 @@ mod closures;
 mod references;
 mod option;
 mod consts;
+
+mod generics;

case_studies/tests/src/traits.rs

@@ -108,6 +108,16 @@ trait FooB<T>
 }
 */
 
+trait Bar<'a> {
+    fn bar(x : &'a i32);
+}
+
+impl<'a> Bar<'a> for i32 {
+    fn bar(x : &'a i32) {
+
+    }
+}
+
 
 // TODO: support skip for modules
 //#[rr::skip]
@@ -136,18 +146,39 @@ mod foo {
         }
     }
 
-    // So, I can also do requirements which might only be fulfilled later.
-    // (i.e. the requirement on T might be fulfilled by another instance).
-    impl<T> Foo<i32> for T 
-        where T : Foo<i32>
+    /* TODO
+    impl<'a, T> Foo<i32> for &'a T
+    {
+        type Output = i32;
+
+        #[rr::verify]
+        fn bar<U>(&self, x: U) -> (Self::Output, i32, U) {
+            (534, 54, x)
+        }
+    }
+    */
+
+
+    impl Foo<i32> for u32
     {
         type Output = i32;
 
-        // TODO
-        fn bar<U>(&self, x : U ) -> (Self::Output, i32, U) {
+        #[rr::verify]
+        fn bar<U>(&self, x: U) -> (Self::Output, i32, U) {
+            (64, 54, x)
+        }
+    }
+
+    /*
+    impl<'a, T> Foo<&'a mut T> for u32
+    {
+        type Output = i32;
+
+        fn bar<U>(&self, x : U) -> (Self::Output, &'a mut T, U) {
             unimplemented!();
         }
     }
+    */
 
     #[rr::params("w")]
     #[rr::args("#w")]
@@ -166,6 +197,65 @@ mod foo {
         let a = 0;
         foobar(&a);
     }
+
+    #[rr::skip]
+    #[rr::params("w")]
+    #[rr::args("w")]
+    fn foobar_ref<'a, W>(x: W) where W: Foo<&'a mut i32> {
+        // TODO: fails because of lifetime annotation, look into this
+
+        x.bar(32); 
+    }
+
+    #[rr::skip]
+    #[rr::params("w")]
+    #[rr::args("w")]
+    fn foobar_ref3<'a, W>(x: W) where W: Foo<&'a mut i32, Output=i32> {
+        // TODO fails because of sidecondition solver
+        x.bar(32); 
+    }
+
+    /*
+    #[rr::verify]
+    fn call_foobar_ref<'a>(x: &'a u32) {
+        foobar_ref::<'a, u32>(*x);
+    }
+
+    fn call_call_foobar_ref() {
+        let x = 42;
+        call_foobar_ref(&x);
+    }
+    */
+
+    #[rr::skip]
+    #[rr::params("w", "v")]
+    #[rr::args("w", "v")]
+    fn foobar_ref2<W, T>(x: W, a: T) where W: Foo<T> {
+        // TODO fails because of sidecondition solver
+        x.bar(32); 
+    }
+
+    /*
+    fn call_foobar_ref2() {
+        let mut x = 43;
+        foobar_ref2::<u32, &'_ mut i32>(43, &mut x);
+    }
+
+    fn call_foobar_ref2_2() {
+        let mut x = 43;
+
+        foobar_ref2::<u32, (&'_ i32, &'_ i32)>(43, (&x, &x));
+    }
+
+    impl<T> Foo<(T, T)> for u32
+    {
+        type Output = i32;
+
+        fn bar<U>(&self, x : U) -> (Self::Output, (T, T), U) {
+            unimplemented!();
+        }
+    }
+    */
 }
 
 /*

rr_frontend/.cargo/config.toml

@@ -30,6 +30,7 @@ rustflags = [
     "-Aclippy::non_ascii_literal",
     "-Aclippy::panic_in_result_fn",
     "-Aclippy::unwrap_in_result",
+    "-Aclippy::separated_literal_suffix",
 
     # clippy::style
     "-Aclippy::new_without_default",

rr_frontend/Cargo.lock

@@ -399,6 +399,7 @@ dependencies = [
  "indoc",
  "itertools",
  "log",
+ "typed-arena",
 ]
 
 [[package]]

rr_frontend/radium/Cargo.toml

@@ -8,6 +8,7 @@ repository.workspace = true
 version.workspace = true
 
 [dependencies]
+typed-arena.workspace = true
 derive_more.workspace = true
 indent_write.workspace = true
 indoc.workspace = true

rr_frontend/radium/src/coq.rs

@@ -432,6 +432,14 @@ impl Param {
         Self::new(Name::Named(name), self.ty.clone(), self.implicit)
     }
 
+    #[must_use]
+    pub fn get_name(&self) -> Option<&str> {
+        match &self.name {
+            Name::Named(s) => Some(s),
+            Name::Unnamed => None,
+        }
+    }
+
     #[allow(clippy::collapsible_else_if)]
     #[must_use]
     pub fn format(&self, make_implicits: bool) -> String {
@@ -470,6 +478,10 @@ impl ParamList {
         Self(vec![])
     }
 
+    pub fn append(&mut self, params: Vec<Param>) {
+        self.0.extend(params);
+    }
+
     /// Make using terms for this list of binders
     #[must_use]
     pub fn make_using_terms(&self) -> Vec<GallinaTerm> {
@@ -736,7 +748,7 @@ impl ContextDecl {
     pub fn refinedrust() -> Self {
         Self {
             items: ParamList::new(vec![Param::new(
-                Name::Unnamed,
+                Name::Named("RRGS".to_owned()),
                 Type::Literal("refinedrustGS Σ".to_owned()),
                 true,
             )]),

rr_frontend/translation/src/lib.rs

@@ -82,6 +82,7 @@ pub struct VerificationCtxt<'tcx, 'rcx> {
     type_translator: &'rcx TypeTranslator<'rcx, 'tcx>,
     trait_registry: &'rcx TraitRegistry<'tcx, 'rcx>,
     functions: &'rcx [LocalDefId],
+    fn_arena: &'rcx Arena<radium::FunctionSpec<radium::InnerFunctionSpec<'rcx>>>,
 
     /// the second component determines whether to include it in the code file as well
     extra_exports: HashSet<(coq::Export, bool)>,
@@ -222,8 +223,10 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
             let a = shim_registry::TraitShim {
                 path: interned_path,
                 name: decl.name.clone(),
+                spec_param_record: decl.spec_params_record.clone(),
                 spec_record: decl.spec_record.clone(),
                 base_spec: decl.base_spec.clone(),
+                base_spec_params: decl.base_spec_params.clone(),
                 spec_subsumption: decl.spec_subsumption.clone(),
             };
             return Some(a);
@@ -294,7 +297,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
                 info!("found impl method: {:?}", did);
                 if self.env.tcx().trait_id_of_impl(impl_did).is_some() {
                     info!("found trait method: {:?}", did);
-                    trait_methods.push((did, &fun.spec));
+                    trait_methods.push((did, fun.spec));
                     continue;
                 }
             }
@@ -435,7 +438,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
         // write translated source code of functions
         {
             writeln!(code_file, "Section code.").unwrap();
-            writeln!(code_file, "Context `{{!refinedrustGS Σ}}.").unwrap();
+            writeln!(code_file, "Context `{{RRGS : !refinedrustGS Σ}}.").unwrap();
             writeln!(code_file, "Open Scope printing_sugar.").unwrap();
             writeln!(code_file).unwrap();
 
@@ -450,14 +453,14 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
         // write function specs
         {
             writeln!(spec_file, "Section specs.").unwrap();
-            writeln!(spec_file, "Context `{{!refinedrustGS Σ}}.").unwrap();
+            writeln!(spec_file, "Context `{{RRGS : !refinedrustGS Σ}}.").unwrap();
             writeln!(spec_file).unwrap();
 
             for (_, fun) in self.procedure_registry.iter_code() {
-                if fun.spec.has_spec {
-                    if fun.spec.args.len() != fun.code.get_argument_count() {
-                        warn!("Function specification for {} is missing arguments", fun.name());
-                    }
+                if fun.spec.is_complete() {
+                    //if fun.spec.spec.args.len() != fun.code.get_argument_count() {
+                    //warn!("Function specification for {} is missing arguments", fun.name());
+                    //}
 
                     writeln!(spec_file, "{}", fun.spec).unwrap();
                 } else {
@@ -472,7 +475,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
         // also write only-spec functions specs
         {
             for (_, spec) in self.procedure_registry.iter_only_spec() {
-                if spec.has_spec {
+                if spec.is_complete() {
                     writeln!(spec_file, "{spec}").unwrap();
                 } else {
                     writeln!(spec_file, "(* No specification provided for {} *)", spec.function_name)
@@ -530,7 +533,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
 
             let mode = self.procedure_registry.lookup_function_mode(*did).unwrap();
 
-            if fun.spec.has_spec && mode.needs_proof() {
+            if fun.spec.is_complete() && mode.needs_proof() {
                 let mut imports = common_imports.clone();
 
                 imports.append(&mut vec![
@@ -555,7 +558,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
                     template_file,
                     "\
                     Section proof.\n\
-                    Context `{{!refinedrustGS Σ}}.\n"
+                    Context `{{RRGS : !refinedrustGS Σ}}.\n"
                 )
                 .unwrap();
 
@@ -564,7 +567,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
                 write!(template_file, "End proof.\n\n").unwrap();
 
                 fun.generate_proof_prelude(&mut template_file).unwrap();
-            } else if !fun.spec.has_spec {
+            } else if !fun.spec.is_complete() {
                 write!(template_file, "(* No specification provided *)").unwrap();
             } else {
                 write!(template_file, "(* Function is trusted *)").unwrap();
@@ -574,7 +577,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
 
     fn check_function_needs_proof(&self, did: DefId, fun: &radium::Function) -> bool {
         let mode = self.procedure_registry.lookup_function_mode(did).unwrap();
-        fun.spec.has_spec && mode.needs_proof()
+        fun.spec.is_complete() && mode.needs_proof()
     }
 
     /// Write proofs for a verification unit.
@@ -634,7 +637,7 @@ impl<'tcx, 'rcx> VerificationCtxt<'tcx, 'rcx> {
             writeln!(proof_file).unwrap();
 
             writeln!(proof_file, "Section proof.").unwrap();
-            writeln!(proof_file, "Context `{{!refinedrustGS Σ}}.").unwrap();
+            writeln!(proof_file, "Context `{{RRGS : !refinedrustGS Σ}}.").unwrap();
             writeln!(proof_file).unwrap();
 
             fun.generate_proof(&mut proof_file, rrconfig::admit_proofs()).unwrap();
@@ -887,10 +890,14 @@ fn register_shims<'tcx>(vcx: &mut VerificationCtxt<'tcx, '_>) -> Result<(), base
 
     for shim in vcx.shim_registry.get_trait_shims() {
         if let Some(did) = utils::try_resolve_did(vcx.env.tcx(), &shim.path) {
+            let assoc_tys = vcx.trait_registry.get_associated_type_names(did);
             let spec = radium::LiteralTraitSpec {
+                assoc_tys,
                 name: shim.name.clone(),
+                spec_params_record: shim.spec_param_record.clone(),
                 spec_record: shim.spec_record.clone(),
                 base_spec: shim.base_spec.clone(),
+                base_spec_params: shim.base_spec_params.clone(),
                 spec_subsumption: shim.spec_subsumption.clone(),
             };
 
@@ -1082,10 +1089,11 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
 
         if mode.is_only_spec() {
             // Only generate a spec
-            match translator.map(FunctionTranslator::generate_spec) {
+            match translator.and_then(FunctionTranslator::generate_spec) {
                 Ok(spec) => {
                     println!("Successfully generated spec for {}", fname);
-                    vcx.procedure_registry.provide_specced_function(f.to_def_id(), spec);
+                    let spec_ref = vcx.fn_arena.alloc(spec);
+                    vcx.procedure_registry.provide_specced_function(f.to_def_id(), spec_ref);
                 },
                 Err(base::TranslationError::FatalError(err)) => {
                     println!("Encountered fatal cross-function error in translation: {:?}", err);
@@ -1105,7 +1113,7 @@ fn translate_functions<'rcx, 'tcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
             }
         } else {
             // Fully translate the function
-            match translator.and_then(FunctionTranslator::translate) {
+            match translator.and_then(|x| x.translate(vcx.fn_arena)) {
                 Ok(fun) => {
                     println!("Successfully translated {}", fname);
                     vcx.procedure_registry.provide_translated_function(f.to_def_id(), fun);
@@ -1286,10 +1294,12 @@ fn register_trait_impls(vcx: &VerificationCtxt<'_, '_>) -> Result<(), String> {
             // make names for the spec and inclusion proof
             let base_name = type_translator::strip_coq_ident(&vcx.env.get_item_name(did));
             let spec_name = format!("{base_name}_spec");
+            let spec_params_name = format!("{base_name}_spec_params");
             let proof_name = format!("{base_name}_spec_subsumption");
 
             let impl_lit = radium::LiteralTraitImpl {
                 spec_record: spec_name,
+                spec_params_record: spec_params_name,
                 spec_subsumption_proof: proof_name,
             };
             vcx.trait_registry
@@ -1302,7 +1312,9 @@ fn register_trait_impls(vcx: &VerificationCtxt<'_, '_>) -> Result<(), String> {
 }
 
 /// Generate trait instances
-fn assemble_trait_impls<'tcx, 'rcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
+fn assemble_trait_impls<'tcx, 'rcx>(
+    vcx: &mut VerificationCtxt<'tcx, 'rcx>,
+) -> Result<(), base::TranslationError<'tcx>> {
     let trait_impl_ids = vcx.env.get_trait_impls();
 
     for trait_impl_id in trait_impl_ids {
@@ -1311,66 +1323,18 @@ fn assemble_trait_impls<'tcx, 'rcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
 
         // check if we registered this impl previously
         if let Some(lit) = vcx.trait_registry.lookup_impl(did) {
-            let trait_spec_ref = vcx.trait_registry.lookup_trait(trait_did).unwrap();
-
-            let param_env: ty::ParamEnv<'tcx> = vcx.env.tcx().param_env(trait_impl_id.to_def_id());
-
-            // get all associated items
+            let impl_info = vcx.trait_registry.get_trait_impl_info(did)?;
             let assoc_items: &'tcx ty::AssocItems = vcx.env.tcx().associated_items(did);
             let trait_assoc_items: &'tcx ty::AssocItems = vcx.env.tcx().associated_items(trait_did);
-
-            // figure out the parameters this impl gets
-            let impl_generics: &'tcx ty::Generics = vcx.env.tcx().generics_of(did);
-            let mut typarams = Vec::new();
-            for param in &impl_generics.params {
-                if let ty::GenericParamDefKind::Type { .. } = param.kind {
-                    let name = param.name.as_str();
-                    let lit = radium::LiteralTyParam::new(name, name);
-                    typarams.push(lit);
-                }
-            }
-
-            // figure out the trait ref for this
             let subject = vcx.env.tcx().impl_subject(did).skip_binder();
             if let ty::ImplSubject::Trait(trait_ref) = subject {
-                // get instantiation for the trait's parameters
-                let self_ty = trait_ref.args.type_at(0);
-                // TODO: get rid of unwrap
-                let self_inst = vcx.type_translator.translate_type_in_empty_scope(self_ty).unwrap();
-                let mut params_inst = Vec::new();
-                for arg in &trait_ref.args[1..] {
-                    let ty = vcx.type_translator.translate_type_in_empty_scope(self_ty).unwrap();
-                    params_inst.push(ty);
-                }
-
-                // get instantiation for the associated types
-                // and go over all methods
-                let mut assoc_types_inst = Vec::new();
                 let mut methods = HashMap::new();
 
                 // TODO don't rely on definition order
-
                 // maybe instead iterate over the assoc items of the trait
-                //assoc_items.find_by_name_and_kind(
+
                 for x in trait_assoc_items.in_definition_order() {
-                    if x.kind == ty::AssocKind::Type {
-                        let ty_item = assoc_items.find_by_name_and_kind(
-                            vcx.env.tcx(),
-                            x.ident(vcx.env.tcx()),
-                            ty::AssocKind::Type,
-                            did,
-                        );
-                        if let Some(ty_item) = ty_item {
-                            let ty_did = ty_item.def_id;
-                            let ty = vcx.env.tcx().type_of(ty_did);
-                            // TODO unwrap
-                            let translated_ty =
-                                vcx.type_translator.translate_type_in_empty_scope(ty.skip_binder()).unwrap();
-                            assoc_types_inst.push(translated_ty);
-                        } else {
-                            unreachable!("trait impl does not have required item");
-                        }
-                    } else if x.kind == ty::AssocKind::Fn {
+                    if x.kind == ty::AssocKind::Fn {
                         let fn_item = assoc_items.find_by_name_and_kind(
                             vcx.env.tcx(),
                             x.ident(vcx.env.tcx()),
@@ -1379,15 +1343,7 @@ fn assemble_trait_impls<'tcx, 'rcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
                         );
                         if let Some(fn_item) = fn_item {
                             if let Some(spec) = vcx.procedure_registry.lookup_function_spec(fn_item.def_id) {
-                                // TODO: make sure that for unannotated functions we use the
-                                // default spec
-                                let ty_params = &spec.ty_params;
-                                let spec_name = &spec.spec_name;
-
-                                methods.insert(
-                                    x.name.as_str().to_owned(),
-                                    Some((spec_name.to_owned(), ty_params.to_owned())),
-                                );
+                                methods.insert(x.name.as_str().to_owned(), spec);
                             } else {
                                 // TODO should handle this case
                                 unreachable!("");
@@ -1398,21 +1354,15 @@ fn assemble_trait_impls<'tcx, 'rcx>(vcx: &mut VerificationCtxt<'tcx, 'rcx>) {
                         }
                     }
                 }
+                let instance_spec = radium::TraitInstanceSpec::new(methods);
 
                 // assemble the spec and register it
-                let spec = radium::TraitImplSpec::new(
-                    lit,
-                    trait_spec_ref,
-                    typarams,
-                    self_inst,
-                    params_inst,
-                    assoc_types_inst,
-                    methods,
-                );
+                let spec = radium::TraitImplSpec::new(lit, impl_info, instance_spec);
                 vcx.trait_impls.insert(did, spec);
             }
         }
     }
+    Ok(())
 }
 
 /// Get and parse all module attributes.
@@ -1519,8 +1469,10 @@ where
     let shim_arena = Arena::new();
     let trait_arena = Arena::new();
     let trait_impl_arena = Arena::new();
+    let fn_spec_arena = Arena::new();
     let type_translator = TypeTranslator::new(env, &struct_arena, &enum_arena, &shim_arena);
-    let trait_registry = TraitRegistry::new(env, &type_translator, &trait_arena, &trait_impl_arena);
+    let trait_registry =
+        TraitRegistry::new(env, &type_translator, &trait_arena, &trait_impl_arena, &fn_spec_arena);
     let procedure_registry = ProcedureScope::new();
     let shim_string_arena = Arena::new();
     let mut shim_registry = shim_registry::ShimRegistry::empty(&shim_string_arena);
@@ -1564,6 +1516,7 @@ where
         dune_package: package,
         const_registry: ConstScope::empty(),
         trait_impls: HashMap::new(),
+        fn_arena: &fn_spec_arena,
     };
 
     register_functions(&mut vcx).map_err(|x| x.to_string())?;
@@ -1580,7 +1533,7 @@ where
 
     // important: happens after all functions have been translated, as this uses the translated
     // function specs
-    assemble_trait_impls(&mut vcx);
+    assemble_trait_impls(&mut vcx).map_err(|x| x.to_string())?;
 
     continuation(vcx);
 

rr_frontend/translation/src/shim_registry.rs

@@ -41,10 +41,14 @@ struct ShimTraitEntry {
     kind: String,
     /// name of the trait
     name: String,
+    /// the Coq def name of the spec param record
+    spec_param_record: String,
     /// the Coq def name of the spec record
     spec_record: String,
     /// the Coq def name of the base spec
     base_spec: String,
+    /// the Coq def name of the base spec params
+    base_spec_params: String,
     /// the Coq def name of spec subsumption relation
     spec_subsumption: String,
 }
@@ -136,8 +140,10 @@ impl From<TraitMethodImplShim> for ShimTraitMethodImplEntry {
 pub struct TraitShim<'a> {
     pub path: Path<'a>,
     pub name: String,
+    pub spec_param_record: String,
     pub spec_record: String,
     pub base_spec: String,
+    pub base_spec_params: String,
     pub spec_subsumption: String,
 }
 
@@ -147,8 +153,10 @@ impl<'a> From<TraitShim<'a>> for ShimTraitEntry {
             path: shim.path.iter().map(|x| (*x).to_owned()).collect(),
             kind: "trait".to_owned(),
             name: shim.name,
+            spec_param_record: shim.spec_param_record,
             spec_record: shim.spec_record,
             base_spec: shim.base_spec,
+            base_spec_params: shim.base_spec_params,
             spec_subsumption: shim.spec_subsumption,
         }
     }
@@ -355,8 +363,10 @@ impl<'a> ShimRegistry<'a> {
                     let entry = TraitShim {
                         path: self.intern_path(b.path),
                         name: b.name,
+                        spec_param_record: b.spec_param_record,
                         spec_record: b.spec_record,
                         base_spec: b.base_spec,
+                        base_spec_params: b.base_spec_params,
                         spec_subsumption: b.spec_subsumption,
                     };
 

rr_frontend/translation/src/spec_parsers/enum_spec_parser.rs

@@ -4,6 +4,8 @@
 // If a copy of the BSD-3-clause license was not distributed with this
 // file, You can obtain one at https://opensource.org/license/bsd-3-clause/.
 
+use std::collections::HashMap;
+
 use attribute_parse::{parse, MToken};
 use parse::{Parse, Peek};
 use radium::{coq, specs};
@@ -27,8 +29,6 @@ pub trait EnumSpecParser {
         ty_name: &str,
         attrs: &'a [&'a AttrItem],
         variant_attrs: &[Vec<&'a AttrItem>],
-        params: &'a [specs::LiteralTyParam],
-        lfts: &'a [(Option<String>, specs::Lft)],
     ) -> Result<specs::EnumSpec, String>;
 }
 
@@ -42,7 +42,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for EnumPattern {
     fn parse(input: parse::Stream, meta: &ParseMeta) -> parse::Result<Self> {
         // parse the pattern
         let pat: parse::LitStr = input.parse(meta)?;
-        let (pat, _) = process_coq_literal(&pat.value(), *meta);
+        let (pat, _) = process_coq_literal(&pat.value(), meta);
 
         let args: Vec<String> = if parse::Dollar::peek(input) {
             // optionally parse args
@@ -55,7 +55,7 @@ impl<'a> parse::Parse<ParseMeta<'a>> for EnumPattern {
             parsed_args
                 .into_iter()
                 .map(|s| {
-                    let (arg, _) = process_coq_literal(&s.value(), *meta);
+                    let (arg, _) = process_coq_literal(&s.value(), meta);
                     arg
                 })
                 .collect()
@@ -68,24 +68,24 @@ impl<'a> parse::Parse<ParseMeta<'a>> for EnumPattern {
 }
 
 #[allow(clippy::module_name_repetitions)]
-pub struct VerboseEnumSpecParser;
+pub struct VerboseEnumSpecParser<'a> {
+    scope: &'a LiteralScope,
+}
 
-impl VerboseEnumSpecParser {
-    pub const fn new() -> Self {
-        Self {}
+impl<'a> VerboseEnumSpecParser<'a> {
+    pub const fn new(scope: &'a LiteralScope) -> Self {
+        Self { scope }
     }
 }
 
-impl EnumSpecParser for VerboseEnumSpecParser {
+impl<'b> EnumSpecParser for VerboseEnumSpecParser<'b> {
     fn parse_enum_spec<'a>(
         &'a mut self,
         ty_name: &str,
         attrs: &'a [&'a AttrItem],
         variant_attrs: &[Vec<&'a AttrItem>],
-        params: &'a [specs::LiteralTyParam],
-        lfts: &'a [(Option<String>, specs::Lft)],
     ) -> Result<specs::EnumSpec, String> {
-        let meta = (params, lfts);
+        let meta = self.scope;
 
         let mut variant_patterns: Vec<(String, Vec<String>, String)> = Vec::new();
         let mut rfn_type = None;