Rustc 1.79.0

[utaal]

This has taken a while but I think it's almost there.

After merging main there's this issue which I think is related to treating the marker trait specially for erasure:
(solved, see below)

trait T3254_Pointee {
    type A3255_Metadata : T3256_Freeze+T3249_Debug+T3176_Hash+T3253_Ord+T3252_PartialOrd<<Self as T3254_Pointee>::A3255_Metadata, >+T3251_PartialEq<<Self as T3254_Pointee>::A3255_Metadata, >+T3175_Eq+T3245_Clone+?Sized;
}

error[E0405]: cannot find trait `T3256_Freeze` in this scope
   --> dummyrs.rs:263:27
    |
263 |     type A3255_Metadata : T3256_Freeze+T3249_Debug+T3176_Hash+T3253_Ord+T3252_PartialOrd<<Self as T3254_Pointee>::A3255_Metadata, >+T3251...
    |                           ^^^^^^^^^^^^ not found in this scope

[ziqiaozhou]

This has taken a while but I think it's almost there.

After merging main there's this issue which I think is related to treating the marker trait specially for erasure:

trait T3254_Pointee {
    type A3255_Metadata : T3256_Freeze+T3249_Debug+T3176_Hash+T3253_Ord+T3252_PartialOrd<<Self as T3254_Pointee>::A3255_Metadata, >+T3251_PartialEq<<Self as T3254_Pointee>::A3255_Metadata, >+T3175_Eq+T3245_Clone+?Sized;
}

error[E0405]: cannot find trait `T3256_Freeze` in this scope
   --> dummyrs.rs:263:27
    |
263 |     type A3255_Metadata : T3256_Freeze+T3249_Debug+T3176_Hash+T3253_Ord+T3252_PartialOrd<<Self as T3254_Pointee>::A3255_Metadata, >+T3251...
    |                           ^^^^^^^^^^^^ not found in this scope

@utaal, the freeze issue could be fixed by adding the external specification for Freeze trait in vstd. ziqiaozhou@7e824a2

[utaal]

Thank you for the pointer @ziqiaozhou!

[ziqiaozhou]

I deleted my prior comment since I was thinking that error was due to other reasons, since the error only happens in a large project where the code may use some new features. The error disappears if I extract that specific chunk of code out. Later on, I realized that it is fixable by const_header_wrapper.

To support that in the new macro, I need to change the rewrite similar to the change in syntax.rs. I just lazily set that const_header_wrapper for all spec function calls. I think we can just set it by default no matter whether the function is const or non-const. I also noticed that some macros rely on syntax::rewrite_expr or proof_block or others will need to set is_const: true as default.

ziqiaozhou@ae239c6

[utaal]

@Chris-Hawblitzel ran veritas and found that my fixes for the new const rules are not sufficient, specifically for this case, from https://github.com/utaal/verified-nrkernel

pub exec const x86_arch_exec: ArchExec ensures x86_arch_exec@ == x86_arch_spec {
    let layers = [
        ArchLayerExec { entry_size: L0_ENTRY_SIZE, num_entries: 512 },
        ArchLayerExec { entry_size: L1_ENTRY_SIZE, num_entries: 512 },
        ArchLayerExec { entry_size: L2_ENTRY_SIZE, num_entries: 512 },
        ArchLayerExec { entry_size: L3_ENTRY_SIZE, num_entries: 512 },
    ];
    assert(x86_arch_spec.layers =~= layers@.map(|n,e:ArchLayerExec| e@));
    ArchExec { layers }
}

where there is a mix of proof code, which should be allowed to call anything, and exec code which should conform to the const rules. At the moment I don't know how we can address this.

[utaal]

@Chris-Hawblitzel I did this, which is quite heavy-handed, but seems to work.