search

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.12k stars 50 forks source link

Identifer names are unstable #1134

Open xldenis opened 6 hours ago

xldenis commented 6 hours ago

Since @lysxia has moved us to hash based identifiers, they have become unstable, locally every proof regenerates at least one identifier causing proofs to be marked as obsolete / having detached goals. I don't know why this occurs though, perhaps StableHash is not stable enough? Or we're too aggressively caching metadata?

Lysxia commented 5 hours ago

Looking at the hash changes in #1133, do you know where the empty modules at the end of type_invariants/borrows.coma come from?

EDIT: Found it. They come from the impl Invariant blocks.

xldenis commented 4 hours ago

You can also look at #1132, there are some failures due to Invariant but locally I observed some for other traits like Clone, Eq etc...

xldenis commented 4 hours ago

Right now all I can think of is that StableHash is somehow platform dependent but the docs explicitly say it shouldn't be. Alternatively, I notice you hash a usize, I suppose that could hypothetically b diff on 32 bit, but GH actions aren't 32 bit anyways...

EDIT: the impl of usize hash always treats it as 64 bits to enable platform independence.

I will note this is 100% deterministic as well, which is somewhat reassuring.