Finished task129 #24
Finished task129 #24
Conversation
tasks/human_eval_129.rs
Outdated
| forall|i: int| (0 <= i < N ==> #[trigger] grid[i].len() == N), | ||
| { | ||
| &&& (forall|i: int, j: int| (0 <= i < N && 0 <= j < N) ==> 1 <= #[trigger] grid[i][j] <= N * N) | ||
| &&& (forall|n: int| #[trigger] exists_a_square_with_value::<N>(grid, n)) |
There was a problem hiding this comment.
This seems to be assuming false. I think you need to bound n to be between 1 and N*N, right?
There was a problem hiding this comment.
Yes, good catch. I have made the change, I have also added a guard to the other condition on line 72. The body of no_repeats_in_grid is now:
&&& (forall|i: int, j: int| (0 <= i < N && 0 <= j < N) ==> 1 <= #[trigger] grid[i][j] <= N * N)
&&& (forall|n: int| 1 <= (n + 0) <= N*N ==> #[trigger] exists_a_cell_with_value::<N>(grid, n))
&&& (forall|i1: int, j1: int, i2: int, j2: int|
(0 <= i1 < N && 0 <= j1 < N && 0 <= i2 < N && 0 <= j2 < N)
==> (grid[i1][j1] == grid[i2][j2]) ==> i1 == i2 && j1 == j2)
This also required me to slightly modify the proof in find_smallest_adjacent_to_one
There was a problem hiding this comment.
The proof in find_smallest_adjacent_to_one is a little longer and uses some weird triggering stuff now. I played around with it a bit and this was the nicest I could make it in the time I was willing to spend on it.
If you would like a nicer proof, I can try to play around with it some more
| == alternate_path))); | ||
|
|
||
| while k_counter > 0 | ||
| invariant |
There was a problem hiding this comment.
As a rule of thumb, if your invariant clause list grows this large, it's probably worth trying to factor out some of the components, if only to document what the intent of each bundle is.
There was a problem hiding this comment.
I am not 100% sure what the correct way to do this is. I factored out all of the invariants that are not dependent on things that change at each loop iteration:
pub closed spec fn facts_passed_into_loop<const N: usize>(grid: [[u8; N]; N], ones_coordinates : (usize, usize), smallest_coordinates : (usize, usize), smallest : u8) -> bool {
&&& no_repeats_in_grid::<N>([email protected]_values(|row: [u8; N]| [email protected]_values(|item| item as int)))
&&& 1 <= smallest <= N * N
&&& ones_coordinates.0 < N - 1 ==> grid[ones_coordinates.0 + 1][ones_coordinates.1 as int]
>= smallest
&&& ones_coordinates.0 > 0 ==> grid[ones_coordinates.0 - 1][ones_coordinates.1 as int]
>= smallest
&&& ones_coordinates.1 < N - 1 ==> grid[ones_coordinates.0 as int][ones_coordinates.1 + 1]
>= smallest
&&& ones_coordinates.1 > 0 ==> grid[ones_coordinates.0 as int][ones_coordinates.1 - 1]
>= smallest
&&& ((ones_coordinates.0 < N + 1 && ones_coordinates.0 + 1 == smallest_coordinates.0
&& ones_coordinates.1 == smallest_coordinates.1) || (ones_coordinates.0 > 0
&& ones_coordinates.0 - 1 == smallest_coordinates.0 && ones_coordinates.1
== smallest_coordinates.1) || (ones_coordinates.1 < N + 1 && ones_coordinates.0
== smallest_coordinates.0 && ones_coordinates.1 + 1 == smallest_coordinates.1) || (
ones_coordinates.1 > 0 && ones_coordinates.0 == smallest_coordinates.0
&& ones_coordinates.1 - 1 == smallest_coordinates.1))
&&& 0 <= smallest_coordinates.0 < N
&&& 0 <= smallest_coordinates.1 < N
&&& 0 <= ones_coordinates.0 < N
&&& 0 <= ones_coordinates.1 < N
&&& grid[smallest_coordinates.0 as int][smallest_coordinates.1 as int] == smallest
&&& grid[ones_coordinates.0 as int][ones_coordinates.1 as int] == 1u8
}
This is a majority of invariants and the other ones are somewhat important. Is this alright?
There was a problem hiding this comment.
For small/simple loops, if you want the body to automatically inherit the ambient facts, you can use #[verifier::loop_isolation(false)] (see docs for details).
It might be overkill for a one-off function like this, but in general, I'd be inclined to define a coordinate struct, and then have some of these invariants be collected in a well-formed condition, possibly w.r.t. a grid that's passed into the condition. That can help avoid repetition and also convey intent.
|
I have made the changes you requested. Thanks for the comments, especially the completeness issue |
| &&& ((coords.0 < N - 1 && grid[coords.0 + 1][coords.1] == n) | ||
| || (coords.0 > 0 && grid[coords.0 - 1][coords.1] == n) | ||
| || (coords.1 < N - 1 && grid[coords.0][coords.1 + 1] == n) | ||
| || (coords.1 > 0 && grid[coords.0][coords.1 - 1] == n)) |
There was a problem hiding this comment.
I may be overly fussy here, but I was imagining something like:
&&& ( (coords.0 < N - 1 && grid[coords.0 + 1][coords.1] == n)
|| (coords.0 > 0 && grid[coords.0 - 1][coords.1] == n)
|| (coords.1 < N - 1 && grid[coords.0][coords.1 + 1] == n)
|| (coords.1 > 0 && grid[coords.0][coords.1 - 1] == n))
which makes it very transparent what's happening with the grid coordinates.
You could also consider starting the entire function body with a
let (x, y) = coords;
...
so that the rest of the body isn't cluttered with coords.0 and coords.1
| smallest as int, | ||
| 1, | ||
| (#[trigger] (i + 0), #[trigger] (j + 0)), | ||
| ))); | ||
|
|
||
| // assert (false); |
There was a problem hiding this comment.
You can probably delete this.
| == alternate_path))); | ||
|
|
||
| while k_counter > 0 | ||
| invariant |
There was a problem hiding this comment.
For small/simple loops, if you want the body to automatically inherit the ambient facts, you can use #[verifier::loop_isolation(false)] (see docs for details).
It might be overkill for a one-off function like this, but in general, I'd be inclined to define a coordinate struct, and then have some of these invariants be collected in a well-formed condition, possibly w.r.t. a grid that's passed into the condition. That can help avoid repetition and also convey intent.
Tried to simplify this as much as I could. Let me know if you have any suggestions.
This could potentially be a good candidate for instability. It was not too bad, but would be interesting to see what happens if we ran Mariposa on this with a timeout of like 2 seconds