Generate our own impl block names for consistency between ghost/erased runs of rustc

[Chris-Hawblitzel]

Previously, our VIR paths contained rustc-generated segments like "impl%0" and "impl%1", using rustc's numbering for the "impl%n" names. Unfortunately, this numbering is not necessarily consistent between the keep-ghost-code run of rustc and the erased-ghost-code run of rustc. Therefore, this pull request generates our own unique names for impl blocks independent of rustc's numbering.

The generated unique names include abbreviations of the datatype and (optionally) trait name for each impl block, so this pull request also has the side effect of making the VIR names more readable.

[Chris-Hawblitzel]

Example:

struct Cat;

impl Cat {
    spec fn f() -> int { 5 }
}

old SMT:

;; Function-Decl test::Cat::f
(declare-fun test!impl&%0.f.? (Poly) Int)

new SMT:

;; Function-Decl test::Cat::f
(declare-fun test!&%Cat.f.? (Poly) Int)

[tjhance]

Unfortunately, this numbering is not necessarily consistent between the keep-ghost-code run of rustc and the erased-ghost-code run of rustc.

Why is this important?

[tjhance]

why do FnDef and FnPtr not include type arguments?

[Chris-Hawblitzel]

These should probably be unsupported_err!, as in mid_ty_to_vir_ghost. I just have to set up the spans and Result return types so that these errors would get reported properly.

[Chris-Hawblitzel]

Ok, I updated the pull request to use unsupported_err!

[Chris-Hawblitzel]

Why is this important?

If this issue happens while compiling vstd, the compiled rust library will have different names from the serialized VIR (in the persisted .vir file). This causes Verus to fail to find the expected names in the .vir file in code that uses vstd. We never saw this before because it happened that the names always matched up, but in recent experiments on the https://github.com/verus-lang/verus/tree/rustc_build branch this has actually happened (before using the fix in this PR).

[tjhance]

Is it OK for the IMPL_SEPARATOR to be the same as the PATHS_SEPARATOR? the impl name can be part of a path, right?

[Chris-Hawblitzel]

Good point. I changed IMPL_SEPARATOR to "&/".

[tjhance]

I don't understand the function of ImplNameId. As I understand it, the ImplFingerprint is the thing that remains constant across the ghost/erased runs. The ImplNameState maps those to Idents, which I presume are the idents that end up in the VIR Path names. So what does ImplNameId do?

[Chris-Hawblitzel]

what does ImplNameId do?

I renamed this to RustcLocalImplId and added comments:

// rustc's internal name in a particular run of rustc.
// It consists of TypPath data, which is stable across runs of rustc,
// and numeric disambiguators, which can vary between runs of rustc.
// Our goal is to remap RustcLocalImplId to completely stable names.
pub(crate) type RustcLocalImplId = (TypPath, Vec<u32>);

[tjhance]

So it's just a stringified version of the DefPath? Is it not possible to use the DefPath or DefId as the key?

[Chris-Hawblitzel]

So it's just a stringified version of the DefPath? Is it not possible to use the DefPath or DefId as the key?

I took a closer look at this. RustcLocalImplId = (TypPath, Vec<u32>) is a stringified, hashable, serializable version of a prefix of a DefPath. I tried using RustcLocalImplId = DefPath or RustcLocalImplId = (CrateNum, Vec<DisambiguatedDefPathData>). However, these didn't implement Serialize and Deserialize.

Also, the code for def_path_to_rustc_id has a second purpose. It's used for def_path_to_path, which strips off the disambiguators to get a path that can be used in the fingerprints.

[tjhance]

Hm, ok, there's still something I'm missing here. Why does RustcLocalImplId need to be serializable? If the whole point is that it's not stable, what good does that do?

[Chris-Hawblitzel]

Hm, ok, there's still something I'm missing here. Why does RustcLocalImplId need to be serializable? If the whole point is that it's not stable, what good does that do?

This was also confusing for me while I was writing the code, so it's probably good to document the approach better. I added more comments describing a typical scenario:

    // Example:
    // - when compiling vstd (both with erase_ghost and !erase_ghost):
    //   - rustc creates its own internal names for impls in vstd
    //     - these names may be different in erase_ghost and !erase_ghost
    //     - example:
    //       - in erase_ghost: impl%2
    //       - in !erase_ghost: impl%3
    //   - we represent these rustc internal names with RustcLocalImplId
    //     - example:
    //       - in erase_ghost: ("impl", [2])
    //       - in !erase_ghost: ("impl", [3])
    //   - we map the RustcLocalImplId to our own Ident in map_to_stable_name
    //     - we create a mapping for erase_ghost and another mapping for !erase_ghost
    //     - the Ident values are the same in erase_ghost and !erase_ghost
    //     - example:
    //       - in erase_ghost: ("impl", [2]) -> impl_Vec7
    //       - in !erase_ghost: ("impl", [3]) -> impl_Vec7
    //   - in our own VIR AST for the vstd library (created with !erase_ghost),
    //     we use the stable Ident values
    //     - impl_Vec7
    //   - rustc emits a library file on disk using its erase_ghost internal names
    //       - in erase_ghost: impl%2
    //   - we serialize and emit our VIR AST in CrateWithMetadata
    //     - the serialized VIR AST contains impl_Vec7
    //   - we also serialize the erase_ghost mapping in CrateWithMetadata
    //     - ("impl", [2]) -> impl_Vec7
    //     - see the export_impls function below and see import_export.rs
    // - when a client application imports vstd:
    //   - rustc reads in the erase_ghost-compiled vstd library from disk
    //     - this file contains the *same* erase_ghost rustc internal names
    //       created while compiling vstd
    //       - in erase_ghost: impl%2
    //     - we again represent these internal names with the same RustcLocalImplId
    //       as we did while compiling vstd
    //       - in erase_ghost: ("impl", [2])
    //   - we read in the serialized mapping from CrateWithMetadata created when compiling vstd
    //     - in erase_ghost: ("impl", [2]) -> impl_Vec7
    //   - we use the RustcLocalImplId and deserialized map_to_stable_name to recover the same
    //     Ident values that were used while compiling vstd
    //     - impl_Vec7
    //   - the key result is that these Ident values will match the !erase_ghost Ident values
    //     that are present in the rest of the deserialized VIR AST for the vstd library
    //     (whereas if we hadn't done the remapping, we would have seen inconsistent names,
    //     impl%2 from the !erase_ghost rustc-emitted library, and impl%3 in our deserialized
    //     VIR AST)

[tjhance]

OK, I think I get it now. Just to check, we use the fingerprinting in order to make sure these two things map to the same Ident:

    //       - in erase_ghost: ("impl", [2]) -> impl_Vec7
    //       - in !erase_ghost: ("impl", [3]) -> impl_Vec7

But the fingerprints don't get serialized, the thing we serialize is the erase_ghost mapping, which matches the rlib file?

[tjhance]

Can we add an assert here that the disambiguator list we're ignoring is empty?

[Chris-Hawblitzel]

Can we add an assert here that the disambiguator list we're ignoring is empty?

I just tried this:

fn def_path_to_path<'tcx>(tcx: TyCtxt<'tcx>, def_path: DefPath) -> TypPath {
    let (path, disambiguators) = def_path_to_rustc_id(tcx, def_path, usize::MAX);
    assert!(disambiguators.len() == 0);
    path
}

However, this assertion fails for nested impls (which, admittedly, we don't support yet, but we could in the future, and names.rs is intended to account for this):

struct S;
impl S {
    fn f() {
        struct Q;
        impl Q {
            fn g() {}
        }
    }
}

[tjhance]

Oh, I... had no idea nested impls were a thing.

Can you give a rough argument why the fingerprinting is sound even when disambiguators are thrown away?

[Chris-Hawblitzel]

we use the fingerprinting in order to make sure these two things map to the same Ident:

yes

[Chris-Hawblitzel]

the thing we serialize is the erase_ghost mapping, which matches the rlib file?

yes

[Chris-Hawblitzel]

But the fingerprints don't get serialized

Good point. The fingerprints had been unnecessarily marked Serialize, Deserialize. I just removed that.