New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Verify The Jackbot 10684 #251
Conversation
Could you remove the |
Done. |
prusti-tests/tests/verify_overflow/pass/competitve_programming/dp/TheJackpot_10684.rs
Show resolved
Hide resolved
prusti-tests/tests/verify_overflow/pass/competitve_programming/dp/TheJackpot_10684.rs
Show resolved
Hide resolved
#[requires (i >= 0)] | ||
#[requires (i < seq.len())] | ||
#[requires (seq.len() > 0)] | ||
fn solve_rec(seq: &VecWrapperI32, i: usize) -> i32 { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would say that it is not obvious that this function is computing the result we want it to compute. Therefore, we need to prove that this is indeed the case. One idea would be to do this as follows:
- Write a function
solve_naive(seq: &VecWrapperI32) -> i32
that solves the problem by using two nested loops (one loop checks all possible start positions of the subsequence, and the second one computes all possible sums that start at that position). - Prove that
solve_rec(seq, seq.len()) >= solve_naive(seq)
(it should be much easier to prove>=
than==
).
Is it clear how to do that?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I will try to do it and see if I manage.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you get any questions, please let me know.
I have changed it but I am facing overflow problems now. Is there a way to avoid that or should I also verify the overflow won’t happen?
|
I think the final version should be verified to be overflow free. Please let me know if you get problems with this. |
The final version gives me overflow problems |
The task description says that each number is not larger than 1000. Adding this to the precondition and propagating down should allow convincing Prusti that there are no overflows. |
I am trying to add this condition #[ensures (result >= -1000 && result <= i * 10000)] , but i is usize and result is i32. it. gives me the error expected i32 found usize. is there a way to do the multiplication in the condition? |
Have you tried |
Prusti complains without reporting the error. It gives an error at the beginning of the file whenever I use casting. |
Uh, thanks for reporting that. PR #253 should fix the error reporting. We actually don't support casting between usize and other integer types, because Rust gives no guarantee about the range of usize. I didn't remember that. The issue #252 that you opened mentions the proper solution. |
@kammola |
@kammola I have added instructions on how to use a locally built version in Prusti Assistant: https://viperproject.github.io/prusti-dev/dev-guide/development/setup.html#using-locally-built-version-in-prusti-assistant |
pub struct VecWrapperI32 { | ||
v: Vec<i32>, | ||
} | ||
|
||
impl VecWrapperI32 { | ||
#[trusted] | ||
#[pure] | ||
#[ensures (0 <= result)] | ||
pub fn len(&self) -> usize { | ||
self.v.len() | ||
} | ||
|
||
#[trusted] | ||
#[ensures (result.len() == 0)] | ||
pub fn new() -> Self { | ||
VecWrapperI32 { v: Vec::new() } | ||
} | ||
|
||
#[trusted] | ||
#[pure] | ||
#[requires (0 <= index && index < self.len())] | ||
pub fn lookup(&self, index: usize) -> i32 { | ||
self.v[index] | ||
} | ||
|
||
#[trusted] | ||
#[ensures (self.len() == old(self.len()) + 1)] | ||
#[ensures (self.lookup(old(self.len())) == value)] | ||
#[ensures (forall(|i: usize| (0 <= i && i < old(self.len())) ==> | ||
self.lookup(i) == old(self.lookup(i))))] | ||
pub fn push(&mut self, value: i32) { | ||
self.v.push(value); | ||
} | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does this work with an #[extern_spec]
implementation, like here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does #[extern_spec]
allow adding a pure lookup
function? (As far as I remember there were some serious problems with supporting the Index
and IndexMut
traits.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried but I also couldn't find a way to support lookup.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah yes, you're right, the encoding panics when trying to call such a function. I suppose you could write a trusted wrapper only for the lookup function but then it's more messy.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
Only noticed this now unfortunately; there is a typo in the folder name, should be "competitive". |
No description provided.