-
Notifications
You must be signed in to change notification settings - Fork 204
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: Enable dynamic indices on slices (#2446)
Co-authored-by: Jake Fecher <[email protected]>
- Loading branch information
Showing
16 changed files
with
678 additions
and
122 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
7 changes: 7 additions & 0 deletions
7
crates/nargo_cli/tests/execution_success/slice_dynamic_index/Nargo.toml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
[package] | ||
name = "slice_dynamic_index" | ||
type = "bin" | ||
authors = [""] | ||
compiler_version = "0.10.3" | ||
|
||
[dependencies] |
1 change: 1 addition & 0 deletions
1
crates/nargo_cli/tests/execution_success/slice_dynamic_index/Prover.toml
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
x = "5" |
222 changes: 222 additions & 0 deletions
222
crates/nargo_cli/tests/execution_success/slice_dynamic_index/src/main.nr
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,222 @@ | ||
fn main(x : Field) { | ||
// The parameters to this function must come directly from witness values (inputs to main). | ||
regression_dynamic_slice_index(x - 1, x - 4); | ||
} | ||
|
||
fn regression_dynamic_slice_index(x: Field, y: Field) { | ||
let mut slice = []; | ||
for i in 0..5 { | ||
slice = slice.push_back(i); | ||
} | ||
assert(slice.len() == 5); | ||
|
||
dynamic_slice_index_set_if(slice, x, y); | ||
dynamic_slice_index_set_else(slice, x, y); | ||
dynamic_slice_index_set_nested_if_else_else(slice, x, y); | ||
dynamic_slice_index_set_nested_if_else_if(slice, x, y + 1); | ||
dynamic_slice_index_if(slice, x); | ||
dynamic_array_index_if([0, 1, 2, 3, 4], x); | ||
dynamic_slice_index_else(slice, x); | ||
|
||
dynamic_slice_merge_if(slice, x); | ||
dynamic_slice_merge_else(slice, x); | ||
} | ||
|
||
fn dynamic_slice_index_set_if(mut slice: [Field], x: Field, y: Field) { | ||
assert(slice[x] == 4); | ||
assert(slice[y] == 1); | ||
slice[y] = 0; | ||
assert(slice[x] == 4); | ||
assert(slice[1] == 0); | ||
if x as u32 < 10 { | ||
assert(slice[x] == 4); | ||
slice[x] = slice[x] - 2; | ||
slice[x - 1] = slice[x]; | ||
} else { | ||
slice[x] = 0; | ||
} | ||
assert(slice[3] == 2); | ||
assert(slice[4] == 2); | ||
} | ||
|
||
fn dynamic_slice_index_set_else(mut slice: [Field], x: Field, y: Field) { | ||
assert(slice[x] == 4); | ||
assert(slice[y] == 1); | ||
slice[y] = 0; | ||
assert(slice[x] == 4); | ||
assert(slice[1] == 0); | ||
if x as u32 > 10 { | ||
assert(slice[x] == 4); | ||
slice[x] = slice[x] - 2; | ||
slice[x - 1] = slice[x]; | ||
} else { | ||
slice[x] = 0; | ||
} | ||
assert(slice[4] == 0); | ||
} | ||
|
||
// This tests the case of missing a store instruction in the else branch | ||
// of merging slices | ||
fn dynamic_slice_index_if(mut slice: [Field], x: Field) { | ||
if x as u32 < 10 { | ||
assert(slice[x] == 4); | ||
slice[x] = slice[x] - 2; | ||
} else { | ||
assert(slice[x] == 0); | ||
} | ||
assert(slice[4] == 2); | ||
} | ||
|
||
fn dynamic_array_index_if(mut array: [Field; 5], x: Field) { | ||
if x as u32 < 10 { | ||
assert(array[x] == 4); | ||
array[x] = array[x] - 2; | ||
} else { | ||
assert(array[x] == 0); | ||
} | ||
assert(array[4] == 2); | ||
} | ||
|
||
// This tests the case of missing a store instruction in the then branch | ||
// of merging slices | ||
fn dynamic_slice_index_else(mut slice: [Field], x: Field) { | ||
if x as u32 > 10 { | ||
assert(slice[x] == 0); | ||
} else { | ||
assert(slice[x] == 4); | ||
slice[x] = slice[x] - 2; | ||
} | ||
assert(slice[4] == 2); | ||
} | ||
|
||
|
||
fn dynamic_slice_merge_if(mut slice: [Field], x: Field) { | ||
if x as u32 < 10 { | ||
assert(slice[x] == 4); | ||
slice[x] = slice[x] - 2; | ||
|
||
slice = slice.push_back(10); | ||
// Having an array set here checks whether we appropriately | ||
// handle a slice length that is not yet resolving to a constant | ||
// during flattening | ||
slice[x] = 10; | ||
assert(slice[slice.len() - 1] == 10); | ||
assert(slice.len() == 6); | ||
|
||
slice[x] = 20; | ||
slice[x] = slice[x] + 10; | ||
|
||
slice = slice.push_front(11); | ||
assert(slice[0] == 11); | ||
assert(slice.len() == 7); | ||
assert(slice[5] == 30); | ||
|
||
slice = slice.push_front(12); | ||
assert(slice[0] == 12); | ||
assert(slice.len() == 8); | ||
assert(slice[6] == 30); | ||
|
||
let (popped_slice, last_elem) = slice.pop_back(); | ||
assert(last_elem == 10); | ||
assert(popped_slice.len() == 7); | ||
|
||
let (first_elem, rest_of_slice) = popped_slice.pop_front(); | ||
assert(first_elem == 12); | ||
assert(rest_of_slice.len() == 6); | ||
|
||
// TODO(#2462): SliceInsert and SliceRemove with a dynamic index are not yet implemented in ACIR gen | ||
slice = rest_of_slice.insert(2, 20); | ||
assert(slice[2] == 20); | ||
assert(slice[6] == 30); | ||
assert(slice.len() == 7); | ||
|
||
// TODO(#2462): SliceInsert and SliceRemove with a dynamic index are not yet implemented in ACIR gen | ||
let (removed_slice, removed_elem) = slice.remove(3); | ||
// The deconstructed tuple assigns to the slice but is not seen outside of the if statement | ||
// without a direct assignment | ||
slice = removed_slice; | ||
|
||
assert(removed_elem == 1); | ||
assert(slice.len() == 6); | ||
} else { | ||
assert(slice[x] == 0); | ||
slice = slice.push_back(20); | ||
} | ||
|
||
assert(slice.len() == 6); | ||
assert(slice[slice.len() - 1] == 30); | ||
} | ||
|
||
fn dynamic_slice_merge_else(mut slice: [Field], x: Field) { | ||
if x as u32 > 10 { | ||
assert(slice[x] == 0); | ||
slice[x] = 2; | ||
} else { | ||
assert(slice[x] == 4); | ||
slice[x] = slice[x] - 2; | ||
slice = slice.push_back(10); | ||
} | ||
assert(slice.len() == 6); | ||
assert(slice[slice.len() - 1] == 10); | ||
|
||
slice = slice.push_back(20); | ||
assert(slice.len() == 7); | ||
assert(slice[slice.len() - 1] == 20); | ||
} | ||
|
||
fn dynamic_slice_index_set_nested_if_else_else(mut slice: [Field], x: Field, y: Field) { | ||
assert(slice[x] == 4); | ||
assert(slice[y] == 1); | ||
slice[y] = 0; | ||
assert(slice[x] == 4); | ||
assert(slice[1] == 0); | ||
if x as u32 < 10 { | ||
slice[x] = slice[x] - 2; | ||
if y != 1 { | ||
slice[x] = slice[x] + 20; | ||
} else { | ||
if x == 5 { | ||
// We should not hit this case | ||
assert(slice[x] == 22); | ||
} else { | ||
slice[x] = 10; | ||
slice = slice.push_back(15); | ||
assert(slice.len() == 6); | ||
} | ||
assert(slice[4] == 10); | ||
} | ||
} else { | ||
slice[x] = 0; | ||
} | ||
assert(slice[4] == 10); | ||
assert(slice.len() == 6); | ||
assert(slice[slice.len() - 1] == 15); | ||
|
||
slice = slice.push_back(20); | ||
assert(slice.len() == 7); | ||
assert(slice[slice.len() - 1] == 20); | ||
} | ||
|
||
fn dynamic_slice_index_set_nested_if_else_if(mut slice: [Field], x: Field, y: Field) { | ||
assert(slice[x] == 4); | ||
assert(slice[y] == 2); | ||
slice[y] = 0; | ||
assert(slice[x] == 4); | ||
assert(slice[2] == 0); | ||
if x as u32 < 10 { | ||
slice[x] = slice[x] - 2; | ||
// TODO: this panics as we have a load for the slice in flattening | ||
if y == 1 { | ||
slice[x] = slice[x] + 20; | ||
} else { | ||
if x == 4 { | ||
slice[x] = 5; | ||
} | ||
assert(slice[4] == 5); | ||
} | ||
} else { | ||
slice[x] = 0; | ||
} | ||
assert(slice[4] == 5); | ||
} | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.