Add VeriFast CI #239
Add VeriFast CI #239
Conversation
There was a problem hiding this comment.
@btj do you think you could add a simple proof example in ./verifast-proofs and implement the diff and tool invocation logic in check-verifast-proofs.mysh ? We'd like to be able to check that the action runs/fails/succeeds at least once. A positive and a negative example would be great
|
|
||
| unsafe fn reverse(mut n: *mut Node) -> *mut Node | ||
| //@ req Nodes(n, ?nodes); | ||
| //@ ens Nodes(result, reverse(nodes)); |
There was a problem hiding this comment.
Would it be possible to use a different name for the mathematical list reverse function and the rust reverse method ? This could be confusing for some novice users (myself included). By the way does ghost code live in a separate namespace ? I'm guessing not since you can refer to Rust function parameters in the spec. How does overloading work between Rust code and verifast ghost code for function symbols ?
There was a problem hiding this comment.
Real functions and lemmas share the same namespace. No two functions can have the same name. But in this example the real function is called Node::reverse and the lemma is called reverse, so there's no clash.
| } | ||
| ``` | ||
| A lemma is like a regular Rust function, except that it is declared inside an annotation. VeriFast checks that it has no side effects and that it terminates. | ||
|
|
There was a problem hiding this comment.
Can we say that the general methodology/mental model for proving some Rust code implementing some data structure would be to: first, formalize the data structure layout, its invariants and functions in in Verifast's own separation logic language, and then prove that the Rust code and the abstract specification compute the same thing by adding annotations explaining how both compute in lockstep (you are essentially weaving the spec and the program's executions together) ?
There was a problem hiding this comment.
That's not quite how I think of it. The specification (the req clause and the ens clause) is not computational/imperative; it's declarative. The lemmas are imperative but they are proofs of their specification; I think of them as mathematical lemmas stating that the precondition implies the postcondition.
| ``` | ||
| The Rust compiler accepts it just fine, but VeriFast complains that it cannot prove that when this function returns, the ownership of the value pointed to by `dest` is *separate* from the ownership of the return value. If we replace the final line by `result`, VeriFast accepts the code. | ||
|
|
||
| For a function not marked as `unsafe`, VeriFast generates a specification expressing that the function is *semantically well-typed* per [RustBelt](https://research.ralfj.de/thesis.html)'s definition of what Rust's types mean in separation logic. If no specification clause annotations are provided for the function, VeriFast verifies the function against the generated specification; otherwise, VeriFast first verifies that the provided specification implies the generated one, and then verifies the function against the provided specification. |
There was a problem hiding this comment.
Precision the "generated specification" is the default specification derived automatically by Verifast, according to RustBelts separation logic model of rust types, from the function signature.
|
|
||
| For a function not marked as `unsafe`, VeriFast generates a specification expressing that the function is *semantically well-typed* per [RustBelt](https://research.ralfj.de/thesis.html)'s definition of what Rust's types mean in separation logic. If no specification clause annotations are provided for the function, VeriFast verifies the function against the generated specification; otherwise, VeriFast first verifies that the provided specification implies the generated one, and then verifies the function against the provided specification. | ||
|
|
||
| The generated specification for `replace` is as follows: |
There was a problem hiding this comment.
Can we call this the default specification ? Or automatically generated ?
| //@ ens thread_token(_t) &*& *dest |-> ?dest1 &*& <T>.own(_t, dest1) &*& <T>.own(_t, result); | ||
| ``` | ||
| `<T>.own(t, v)` expresses ownership of the T value `v` accessible to thread `t` (in case T is not [Send](https://doc.rust-lang.org/nomicon/send-and-sync.html)). | ||
| `thread_token(t)` represents permission to open *nonatomic invariants* and *nonatomic borrows* at thread `t`; these contain resources shared in a non-thread-safe way at thread `t`. |
There was a problem hiding this comment.
I don't think the concept of opening predicates has been explained so far in this doc, a link to a definition would be useful.
There was a problem hiding this comment.
This sentence is not about opening predicates, it's about opening invariants and borrows; I wanted to briefly motivate thread_token but I'm not sure it makes sense to try and explain those concepts here.
There was a problem hiding this comment.
Could you also add a README file to this folder that describes the intended puprpose and organisation guidelines ?
From side discussions it seems that the folder will contain copies of standard library files extended with verifast ghost code, and that check-verifast-proofs.mysh will run all the diff logic and verifast analyses, but this needs to be explained here
There was a problem hiding this comment.
It would really be awsome to have an actual example of a working proof as part of this PR too, so that we can check the action is working.
|
I'm developing a "refinement checker", a simple tool that checks that one |
Adds a GitHub Actions workflow that downloads VeriFast and runs
verifast-proofs/check-verifast-proofs.mysh. (myshis a simple tool that ships with VeriFast for running simple scripts. It is optimized for running test suites (and used to run VeriFast's test suite. Works on Linux, Mac, and Windows.)See #238 to see how this can be used to verify the
linked_list.rs(Challenge 5) solution.Resolves #213
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.