Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Verify The Jackbot 10684 #251

Merged
merged 8 commits into from
Nov 26, 2020
Merged

Verify The Jackbot 10684 #251

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
889a2e1
Verify The Jackbot 10684
kammola Nov 18, 2020
1733020
Remove .DS_Store files
kammola Nov 18, 2020
bd16997
Fix bug
kammola Nov 18, 2020
c62420e
Specify solution functions
kammola Nov 18, 2020
11cca76
Fix typo
kammola Nov 18, 2020
a1d3045
Add failing iterative solution
kammola Nov 24, 2020
90ad9dd
Add naive solution and check for overflows
kammola Nov 24, 2020
d7c78db
Add iterative naive method
kammola Nov 25, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
123 changes: 123 additions & 0 deletions prusti-tests/tests/verify_overflow/pass/competitve_programming/dp/TheJackpot_10684.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,123 @@
//https://onlinejudge.org/index.php?option=com_onlinejudge&Itemid=8&category=24&page=show_problem&problem=1625
vakaras marked this conversation as resolved.
Show resolved Hide resolved
use prusti_contracts::*;

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);
}
}

#[pure]
#[ensures (result >= a && result >= b)]
#[ensures (result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
if a < b {
b
} else {
a
}
}

#[pure]
#[requires (i >= 0)]
#[requires (i < seq.len())]
#[requires (seq.len() > 0)]
fn solve_rec(seq: &VecWrapperI32, i: usize) -> i32 {
Copy link
Contributor

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:

  1. 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).
  2. 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?

Copy link
Contributor Author

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.

Copy link
Contributor

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.

if i == 0 {
seq.lookup(0)
} else {
let prev = solve_rec(seq, i - 1);
if prev > 0 {
prev + seq.lookup(i)
} else {
seq.lookup(i)
}
}
}

#[pure]
#[requires (seq.len() > 0)]
#[requires (idx >= 0)]
#[requires (idx < seq.len())]
fn the_jackpot_rec(seq: &VecWrapperI32, idx: usize) -> i32 {
if idx == 0 {
max(0, solve_rec(seq, idx))
}else {
max(solve_rec(seq, idx), the_jackpot_rec(seq, idx - 1))
}
}

// Solution >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>

#[requires (seq.len() > 0)]
#[ensures (forall(|k:usize| (k >= 0 && k < seq.len()) ==> (seq.len() == result.len() && result.lookup(k) == solve_rec(seq, k))))]
#[ensures (result.len() == seq.len())]
fn solve(seq: &VecWrapperI32) -> VecWrapperI32 {
let mut dp = VecWrapperI32::new();
dp.push(seq.lookup(0));
let mut i = 1usize;
let len = seq.len();
while i < len {
body_invariant!(i >= 1);
body_invariant!(i < seq.len());
body_invariant!(dp.len() == i);
body_invariant!(forall(|k: usize| (k < i && k >= 0) ==> dp.lookup(k) == solve_rec(seq, k)));
let prev = dp.lookup(i - 1);
if prev > 0 {
dp.push(prev + seq.lookup(i));
} else {
dp.push(seq.lookup(i));
}
i += 1;
}
dp
}

#[requires (seq.len() > 0)]
#[ensures (result == the_jackpot_rec(seq, seq.len() - 1))]
fn the_jackpot(seq: &VecWrapperI32) -> i32 {
let dp = solve(seq);
vakaras marked this conversation as resolved.
Show resolved Hide resolved
let mut answer = max(seq.lookup(0), 0i32);
let len = seq.len();
let mut idx = 1;
while idx < len {
body_invariant!(idx >= 1);
body_invariant!(idx < len);
body_invariant!(answer == the_jackpot_rec(seq, idx - 1));
answer = max(answer, dp.lookup(idx));
idx+=1;
}
answer
}

pub fn main() {
}
223 changes: 223 additions & 0 deletions ...ti-tests/tests/verify_overflow/pass/competitve_programming/dp/TheJackpot_10684_failing.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,223 @@
//https://onlinejudge.org/index.php?option=com_onlinejudge&Itemid=8&category=24&page=show_problem&problem=1625
use prusti_contracts::*;

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);
}
}
Copy link
Member

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?

Copy link
Contributor

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.)

Copy link
Contributor Author

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.

Copy link
Member

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.



#[pure]
#[ensures (result >= a && result >= b)]
#[ensures (result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
if a < b {
b
} else {
a
}
}

// Recursive solution

#[pure]
#[requires (i >= 0)]
#[requires (i < seq.len())]
#[requires (seq.len() > 0)]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
fn max_seq_sum_rec(seq: &VecWrapperI32, i: usize) -> i32 {
if i == 0 {
seq.lookup(0)
} else {
let prev = max_seq_sum_rec(seq, i - 1);
if prev > 0 {
prev + seq.lookup(i)
} else {
seq.lookup(i)
}
}
}

#[pure]
#[requires (seq.len() > 0)]
#[requires (idx >= 0)]
#[requires (idx < seq.len())]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
fn solve_rec(seq: &VecWrapperI32, idx: usize) -> i32 {
if idx == 0 {
max_seq_sum_rec(seq, idx)
}else {
max(max_seq_sum_rec(seq, idx), solve_rec(seq, idx - 1))
}
}

#[pure]
#[requires (seq.len() > 0)]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
fn the_jackpot_rec(seq: &VecWrapperI32) -> i32 {
max(0, solve_rec(seq, seq.len() - 1))
}

// Naive Solution

#[requires (seq.len() > 0)]
#[requires (start >= 0)]
#[requires (start <= end)]
#[requires (end < seq.len())]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
#[ensures (result <= max_seq_sum_rec(seq, end))]
fn seq_sum(seq: &VecWrapperI32, start: usize, end: usize) -> i32 {
if end == start {
seq.lookup(end)
} else {
seq.lookup(end) + seq_sum(seq, start, end - 1)
}
}

#[requires (seq.len() > 0)]
#[requires (start >= 0)]
#[requires (start <= end)]
#[requires (end < seq.len())]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
fn seq_sum_iter(seq: &VecWrapperI32, start: usize, end: usize) -> i32 {
let mut sum = seq.lookup(start);
let mut i = start + 1;
let mut dp = VecWrapperI32::new();
dp.push(sum);

while i <= end {
body_invariant!(i > start);
body_invariant!(i <= end);
body_invariant!(dp.len() == i - start);
body_invariant!(forall(|k: usize| (k >= start && k < i) ==> dp.lookup(k - start) <= max_seq_sum_rec(seq, k)));
sum += seq.lookup(i);
dp.push(sum);
i+=1;
}

sum
}



#[requires (seq.len() > 0)]
#[requires (start >= 0)]
#[requires (start <= end)]
#[requires (end < seq.len())]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
#[ensures (result <= solve_rec(seq, end))]
fn max_seq_sum(seq: &VecWrapperI32, start: usize, end: usize) -> i32 {
if start == end {
seq_sum(seq, start, end)
}else {
max(max_seq_sum(seq, start + 1, end), seq_sum(seq, start, end))
}
}

#[requires (seq.len() > 0)]
#[requires (end >= 0)]
#[requires (end < seq.len())]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
#[ensures (result <= solve_rec(seq, end))]
fn solve_naive(seq: &VecWrapperI32, end: usize) -> i32 {
if end == 0 {
max_seq_sum(seq, 0, end)
} else {
max(solve_naive(seq, end - 1), max_seq_sum(seq, 0, end))
}
}

#[requires (seq.len() > 0)]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
#[ensures (result <= the_jackpot_rec(seq))]
fn the_jackpot_naive(seq: &VecWrapperI32) -> i32 {
max(0, solve_naive(seq, seq.len() - 1))
}

// Solution >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>

#[requires (seq.len() > 0)]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
#[ensures (result.len() == seq.len())]
#[ensures (forall(|k:usize| (k >= 0 && k < seq.len()) ==> (result.lookup(k) == max_seq_sum_rec(seq, k))))]
fn solve(seq: &VecWrapperI32) -> VecWrapperI32 {
let mut dp = VecWrapperI32::new();
dp.push(seq.lookup(0));
let mut i = 1usize;
let len = seq.len();
while i < len {
body_invariant!(i >= 1);
body_invariant!(i < seq.len());
body_invariant!(dp.len() == i);
body_invariant!(forall(|k: usize| (k < i && k >= 0) ==> dp.lookup(k) == max_seq_sum_rec(seq, k)));
let prev = dp.lookup(i - 1);
if prev > 0 {
dp.push(prev + seq.lookup(i));
} else {
dp.push(seq.lookup(i));
}
i += 1;
}
dp
}

#[requires (seq.len() > 0)]
#[requires (forall(|k: usize| (k >= 0 && k < seq.len()) ==> (seq.lookup(k) >= -1000 && seq.lookup(k) <= 1000)))]
#[requires (seq.len() <= 10000)]
#[ensures (result == the_jackpot_rec(seq))]
fn the_jackpot(seq: &VecWrapperI32) -> i32 {
let dp = solve(seq);
let mut answer = seq.lookup(0);
let len = seq.len();
let mut idx = 1;
while idx < len {
body_invariant!(idx >= 1);
body_invariant!(idx < len);
body_invariant!(answer == solve_rec(seq, idx - 1));
answer = max(answer, dp.lookup(idx));
idx+=1;
}
max(0, answer)
}

pub fn main() {
}