Verus internals updates

[elanortang]

Port updates to Verus internals that Travis made on verify-rustlib to main.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[elanortang]

I added some #[cfg(verus_verify_core)] attributes in source/rust_verify/src/driver.rs - let me know if I should add more in other places or remove some of them.

[elanortang]

It looks like the failure of test_opaque_type_assume_spec_ok can be traced to the changes in source/builtin_macros/src/syntax.rs: if I undo them (locally), this test succeeds. Do you have an idea of why those changes would cause type inference to fail?

[parno]

It looks like the failure of test_opaque_type_assume_spec_ok can be traced to the changes in source/builtin_macros/src/syntax.rs: if I undo them (locally), this test succeeds. Do you have an idea of why those changes would cause type inference to fail?

I'm just guessing, but this bit in the syntax macro seems like a plausible culprit:

if self.erase_ghost.erase() {
            Expr::Verbatim(quote! {
                ::core::unimplemented!()
            })

Previously this invoked a function on the arguments, which would add additional type constraints that presumably help type inference do a better job.

[tjhance]

if the body is unimplemented, it won't be able to find a type to instantiate the opaque type.

[tjhance]

possibly better solution: if self.erase_ghost.erase() is true, just erase the entire assume_specification function

[elanortang]

possibly better solution: if self.erase_ghost.erase() is true, just erase the entire assume_specification function

Would that mean that if self.erase_ghost.erase() is true, don't set e to be anything, and don't call stmts.push(Stmt::Expr(e, None)) afterward?

[tjhance]

Why are these cfg options necessary?

This is already a runtime option, we don't need it to be a compile-time option as well. I'd prefer to avoid unnecessary compile-time options.

[elanortang]

The last time we talked about this code, you had said that for merging it into main, it was a kind of hacky way to get around errors about stable attributes, so you felt more comfortable putting it behind verify_core.

But if upon further inspection you think it already has the necessary setup, I can take these cfgs out. (And to clarify, is it correct that you would want either all of them in or none of them?)

[tjhance]

As long as it's behind the runtime check, that's good enough.

[elanortang]

They should all be removed now

[elanortang]

Regarding the changes to source/builtin_macros/src/syntax.rs: according to the commit where @tjhance added them originally, they exist to fix an issue with --compile.

However, it seems like compilation of the Rust stdlib now works fine if I revert these changes - if I run ./compile.sh in the branch rustlib/add-compiler-builtins (which fixes errors in compiling core, among other things), it still goes through.

@tjhance are there any other places I should test compilation before determining that the --compile issue is no longer a problem?

[tjhance]

@tjhance are there any other places I should test compilation before determining that the --compile issue is no longer a problem?

If it works on your rustlib branch, then it's all good.

[elanortang]

@tjhance are there any other places I should test compilation before determining that the --compile issue is no longer a problem?

If it works on your rustlib branch, then it's all good.

It appears that although basic compilation works on rustlib/add-compiler-builtins, this is still a problem on rustlib/vec due to some additional assume_specifications there on core::intrinsics::unchecked_add::<T>. I get this error message:

thread 'rustc' panicked at compiler/rustc_mir_transform/src/validate.rs:80:25:
broken MIR in Item(DefId(0:27316 ~ core[856b]::specs::intrinsics::_verus_external_fn_specification_656_core_32__58__58__32_intrinsics_32__58__58__32_unchecked__add_32__58__58__32__60__32_T_32__62_)) (after phase change to runtime-optimized) at bb0[0]:
Cannot AddUnchecked non-integer type T/#0

I will look into figuring out how to erase the entire assume_specification function.