Update for Creusot 0.7.0

[Lysxia]

This currently only updates the .rs sources. I haven't tried fixing the proofs yet.

BTW Is there a reason for checking in .why3find and target?

[sarsko]

Thanks, Xia!

I’ll have a look tomorrow (aka later today)

Regarding .why3find: workflow may have changed, but originally it is so that one can check out the repo an open it in why3 and have the proof be finished already.

Regarding target: This maybe should not be checked in, but it is also generated and having it checked in means less work when checking out the repo.

[sarsko]

I'll just be stupid and ask my questions here. What happened to predicate? It's now all logic? That looks to be the only change

[Lysxia]

Yes, that's the only change to make it compilable with Creusot again! It's all #[logic] on Rust's side and Creusot makes it a Why3 predicate if it returns bool. There's a handful of broken proofs, and my hope is that they can be fixed by adding some lemmas, but that's a bit of tedious work so it will take a while.

[sarsko]

Thanks.

Partly out of curiosity, partly because I have had logic functions which return bools (such as a function which negates a boolean, I think due to lack of support in Creusot at the time): is there any limitations in how predicates can be used? Can I ever get burned by a logic function which inadvertently has become a predicate?

Also how come the proofs now need more stuff to pass? Has what is exposed to the smt-solvers been changed?

[jhjourdan]

In theory, predicates can be used everywhere a logic function can be used, and conversely. So there should not be any regression because of that.

In practice, the goals sent to SMT solvers are slightly different, which may turn a unstable VC from unsat to unknown, just because it's unstable. So it's difficult to tell whether there can be "true" regressions, but, at least in Creusot's test suite, there has not been any.

[jhjourdan]

Regarding .why3find: workflow may have changed, but originally it is so that one can check out the repo an open it in why3 and have the proof be finished already.

Agreed.

Regarding target: This maybe should not be checked in, but it is also generated and having it checked in means less work when checking out the repo.

That's usually a bad idea, even if I agreee that rebuilding may take some time. The reason is that it contains large files that change a lot, so that your repo can grow quickly.

[sarsko]

That's usually a bad idea, even if I agreee that rebuilding may take some time. The reason is that it contains large files that change a lot, so that your repo can grow quickly.

Yeah, probably a good idea to remove it.

[Lysxia]

• I found the issue blocking the proofs: clone for Vec, whose spec changed in the past year, was missing a postcondition (Fix spec of Vec::clone creusot-rs/creusot#1794). So this update will have to wait for the 0.7.0 release. In the meantime I commited updates to depend on 0.7.0-dev here.
• I updated Friday too, here the diffs are more extensive due Creusot being stricter about respecting visibility modifiers (pub + logic(open))
• All the proofs pass again on my machine!
• I moved all the proof.json into a toplevel verif directory instead of separate CreuSAT/verif, Robinson/verif, Friday/verif. I'm not using Makefile.toml, just cargo creusot -- -p CreuSAT -p Robinson -p Friday. But if you prefer I can revert this.
• I removed the coma files, target dirs, and refreshed the .why3find cache, which results in a massive diff.

[sarsko]

Thanks, Xia!

I don't care much about makefiles and directory structure. It became like it is due to a mix of limitations with Creusot and limitations in how much I care. Probably the makefile stuff will get removed.

I think it'd be better to do the deletions and moves in a separate PR, whichever PR does that is going to be unreadable.

I see that creusot-rs/creusot#987 is still a thing. That's unfortunate.

[Lysxia]

I just released Creusot 0.7.0, and the proofs succeed with cargo creusot prove --replay -- -p CreuSAT -p Robinson -p Friday.

I also updated NewDB to compile with Creusot but I'm not sure what the status of its proofs was supposed to be.

[sarsko]

Thanks! How come it fails build if it passes proofs?

I'll deal with NewDB if I ever pick it back up in the future

[Lysxia]

The build fails with Scratch which is yet another subdirectory I overlooked...

[Lysxia]

Scratch should build again now.

[sarsko]

Excellent, thanks! I appreciate that you put in the effort to update the repository for current Creusot!

Looks like the only thing failing is fmt. I'll have a look over the PR and run fmt once I'm home.

[Lysxia]

Fixed formatting!