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.
| - 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?
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?
| @@ -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?
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