flux_rs::defs and extern_spec cannot be imported across crates

[enjhnsn2]

Curently, flux defs like:

flux_rs::defs!{
    fn bv32(x:int) -> bitvec<32> { bv_int_to_bv32(x) }
}

cannot be used across crates, nor can extern_specs like:

#[extern_spec]
impl<T> [T] {
    #[flux_rs::sig(fn(&[T][@n]) -> usize[n])]
    fn len(v: &[T]) -> usize;
}

While this can be worked around by duplicating this code, it is rather inconvenient. For example, we are verifying code in several different crates in Tock. I have all my wrapper types (and would like to have my extern_specs and defs) in one crate called flux-support, which is then imported by all the Tock crates we are verifying. Currently Flux cannot support this pattern.

[nilehmann]

A workaround would be to have an unattached file somewhere in the repo (not inside any crate) and then include it in all the crates that want to use it using the #[path = ..] attribute on a module declaration, e.g.,

// flux-support.rs
flux_rs::defs!{
    fn bv32(x:int) -> bitvec<32> { bv_int_to_bv32(x) }
}

// crate1/src/lib.rs

#[path = "../../flux-support.rs"]
mod flux_support;

// crate2/src/lib.rs

#[path = "../../flux-support.rs"]
mod flux_support;

This would technically still duplicate the file from the perspective of the build system, but at least the content stays in one place.

[nilehmann]

#763 implements the extern spec part of this.

@enjhnsn2 please test and see if there are any issues. It should be enough to add the crate with the extern specs as a dependency with the caveat that you need to "mention" the crate at least once. If the crate doesn't contain any item you are importing you can mention it using extern crate crate_name. Since the metadata format has changed you'll need to rm -rf target/flux.

The flux_rs::defs part requires more planning because flux defs are identified only by a name and they are made globally available within the crate they are defined. This is problematic if we allow to import them from external crates so we must implement some way to qualify flux defs by crate/module.

[enjhnsn2]

Just tested the extern_spec part of this and it works great.