David Ewert
David Ewert
Example: ```rust use creusot_contracts::*; fn test() { let c = { #[requires(@x + @y < @u32::MAX)] #[ensures(@result == @x + @y)] |x: u32, y: u32| x + y }; let...
Triggers
It would probably be useful to allow uses to manually specify triggers for laws and quantifiers to help avoid matching loops. Note: Why3 already supports this https://why3.lri.fr/doc/syntaxref.html#grammar-token-triggers
The following code: ```rust #[requires(i == Int::new(2))] fn test(i: Int) {} #[requires(s.lookup(3) == 5)] fn test2(s: Seq) {} #[requires(m.lookup(7) == 11)] fn test3(m: Map) {} ``` gives the following errors:...
The following code verifies successfully even though it calls an impure function from a predicate: ```rust use prusti_contracts::*; fn impure() -> u32 { 5 } predicate! { fn pred(x: u32)...
Trying to verify the program: ```rust use prusti_contracts::*; trait Fn { type Output; #[pure] fn postcondition(&self, arg: &A, res: &Self::Output) -> bool; #[ensures(self.postcondition(&arg, &result))] fn call(&self, arg: A) -> Self::Output;...
`PartialEq::eq` currently has the postcondition `result == (@self == @rhs)` and `Vec::::ModelTy` is `Seq` which implies that `Vec::eq` should return true iff both vectors have exactly the same elements. `Vec::eq`...
I added an experimental `--why3 ` flag to to `cargo creusot` which cause Creusot to run Why3 on the generated mlcfg (automatically including the mlcfg file). Example usages: `cargo creusot...
Currently mutable references are extensional (`forall *x == *y && ^x == ^y ==> x == y`) I don't think many of the proofs should require this extensionality axiom. Would...
In trying to come up with a good way to handle #869 and #902, most of the trouble seems to come from unnecessary reborrowing in the MIR. If it wasn't...
In order to continue trying to avoid matching loops/timeouts I am trying to avoid Why3's `encoding_smt_if_poly` and `eliminate_algebraic_if_poly` transformations. I created the driver `z3_no_poly.drv` which is mostly a copy of...