Add Flux tool description and CI workflow #403
Conversation
| @@ -109,7 +111,7 @@ impl_from!(u8 => u16, #[stable(feature = "lossless_int_conv", since = "1.5.0")]) | |||
| impl_from!(u8 => u32, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); | |||
| impl_from!(u8 => u64, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); | |||
| impl_from!(u8 => u128, #[stable(feature = "i128", since = "1.26.0")]); | |||
| impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")]); | |||
| impl_from!(u8 => usize, #[stable(feature = "lossless_int_conv", since = "1.5.0")], #[cfg_attr(flux, flux::spec(fn(x:u8) -> usize[x]))]); | |||
There was a problem hiding this comment.
Can you outline a path on how this might eventually get integrated upstream?
There was a problem hiding this comment.
Could you clarify whether you're referring to specs in general or just the spec in this macro?
There was a problem hiding this comment.
Actually just this one: to me (and I could be wrong!) it looks like a change that, if we were to try to do more proofs using Flux, would require changes in lots of places. For other specs/contracts there is a path in that Rust upstream has experimental contracts support. But tool-specific annotations seem a lot less likely to be merged upstream.
There was a problem hiding this comment.
You are not wrong in that more proofs will require more annotations. We've thought about this, and one option is to provide signatures in a separate file (à la ocaml .mli files), but this is something we have not implemented yet (we have something similar for extern specs).
There was a problem hiding this comment.
With this specific case: wouldn't it be possible to move the spec into the macro_rules so that all generated implementations feature a flux_spec?
There was a problem hiding this comment.
Sadly, no, we try that first, but the macro is also used to convert from bool to integers, and we can't use the same signature for that, i.e., the following is ill-formed when $Small is bool.
#[cfg_attr(flux, flux::spec(fn(x: $Small) -> $Large[x]))]
There was a problem hiding this comment.
Yes, the catch here is that we want to branch on the $Small and $Large and only put different specs depending on their values.
There is perhaps some way to do this with the macros but we couldn't quite work it out, unfortunately.
Would be great if you have any suggestions.
| - arithmetic overflows | ||
| - division by zero |
There was a problem hiding this comment.
For these, does Flux distinguish between ones causing a panic vs ones deemed undefined behaviour?
There was a problem hiding this comment.
No, we currently don't distinguish between those.
There was a problem hiding this comment.
Would you mind including some documentation to this effect?
There was a problem hiding this comment.
I added a sentence at the end of the section explaining this.
nilehmann
force-pushed
the
flux-submission
branch
from
54e5d36 to
57edee9
Compare
| - name: Install Z3 | ||
| uses: cda-tum/setup-z3@v1.6.1 | ||
| with: | ||
| version: 4.12.1 |
There was a problem hiding this comment.
Do we have to stick with this particular version of Z3? Would it be conceivable to just install Ubuntu's version of Z3?
There was a problem hiding this comment.
This is the version we use in our CI. I had problems in the past with Ubuntu's version being too old, and that's why I pinned it. That being said, I see that now they are in 4.13, so we should be fine with that. We may need to update in the future, though.
There was a problem hiding this comment.
Could you please add a comment denoting the minimum version of Z3 required? I am worried about being stuck with a particular version of Z3 when soundness issue in that version of the solver may eventually be found.
There was a problem hiding this comment.
@tautschnig, I'm unsure about what to do here. There's nothing special about this version; it's just the one we actively use in CI, so we have a bit more confidence with it. We (mostly) use standard smtlib, so newer and some older versions should also work.
There was a problem hiding this comment.
Should I add a comment explaining exactly that?
| @@ -0,0 +1,239 @@ | |||
| # Flux | |||
|
|
|||
| [Flux](https://flux-rs.github.io/flux) is a refinement type checker | |||
There was a problem hiding this comment.
Can you please include a section on (current) limitations or caveats?
There was a problem hiding this comment.
I added a section at the end of the document.
This PR introduces Flux to the list of tools used in the book and adds a corresponding CI workflow.
The CI workflow runs Flux on a subset of
core(specifically, files undersrc/ascii) to verify the absence of array out-of-bounds errors. It demonstrates how to annotate the code with refinement types to specify the pre- and post-conditions necessary to prove safety on the subset that Flux is enabled.The Flux tool and necessary dependencies are built from source on CI (pinning specific commits).
Resolves #362