-
Notifications
You must be signed in to change notification settings - Fork 598
feat: Add public data read gadget #13138
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
Changes from all commits
6157356
55a8ddd
169acb1
4484452
301f3fc
85a891f
951fa2a
6c6d0de
b9dca21
765a697
b78da93
a2ab083
f1802f6
659e77f
f2a5bf5
4798808
46cff64
24bce68
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,100 @@ | ||
| include "merkle_check.pil"; | ||
| include "ff_gt.pil"; | ||
| include "poseidon2_hash.pil"; | ||
| include "constants_gen.pil"; | ||
| include "precomputed.pil"; | ||
|
|
||
| // This gadget checks reads in the public data tree. The public data tree is an indexed tree where leaves | ||
| // have slot and value. Slot is the "key" and value is the stored data. When we read from the public data tree, | ||
| // we assume that a slot that has not been written before has value zero. | ||
| // For this we perform a low leaf membership proof and: | ||
| // - if the low leaf slot is equal to the slot, that means that slot has been written before, and we assert that | ||
| // the low leaf value is equal to the value we are reading. | ||
| // - if the low leaf slot is not equal to the slot, we assert that the low leaf is indeed a valid low leaf for the | ||
| // requested slot, proving non existence of the slot in the tree. In that case we check value to be zero. | ||
| // In order to validate that a leaf is a low leaf of the slot, we need to check that the low_leaf.slot is < slot | ||
| // and that low_leaf.next_slot is > slot. However, we need to consider the case where next_slot is zero, which | ||
| // means "infinity". The highest slot inserted in the tree will point to infinity as the "next_slot". | ||
| // | ||
| // Usage: | ||
| // sel { value, leaf_slot, public_data_tree_root } | ||
| // in public_data_read.sel { public_data_read.value, public_data_read.slot, public_data_read.root }; | ||
| // | ||
| namespace public_data_read; | ||
| pol commit sel; | ||
| sel * (1 - sel) = 0; | ||
|
|
||
| #[skippable_if] | ||
| sel = 0; | ||
|
|
||
| // Inputs to the gadget | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Usage of this gagdet is not clear at first sight. |
||
| pol commit value; | ||
| pol commit slot; | ||
| pol commit root; | ||
|
|
||
| // Hints | ||
| pol commit low_leaf_slot; | ||
| pol commit low_leaf_value; | ||
| pol commit low_leaf_next_index; | ||
| pol commit low_leaf_next_slot; | ||
|
|
||
| pol commit low_leaf_index; | ||
|
|
||
| // ========= LOW LEAF MEMBERSHIP ========= | ||
| pol commit low_leaf_hash; | ||
| // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple | ||
| pol commit tree_height; | ||
| sel * (tree_height - constants.PUBLIC_DATA_TREE_HEIGHT) = 0; | ||
|
|
||
| #[LOW_LEAF_POSEIDON2_0] | ||
| sel { low_leaf_slot, low_leaf_value, low_leaf_next_index, low_leaf_hash } | ||
| in poseidon2_hash.start { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output }; | ||
|
|
||
| #[LOW_LEAF_POSEIDON2_1] | ||
| sel { low_leaf_next_slot, precomputed.zero, precomputed.zero, low_leaf_hash } | ||
| in poseidon2_hash.end { poseidon2_hash.input_0, poseidon2_hash.input_1, poseidon2_hash.input_2, poseidon2_hash.output }; | ||
|
|
||
| #[LOW_LEAF_MEMBERSHIP] | ||
| sel { low_leaf_hash, low_leaf_index, tree_height, root } | ||
| in merkle_check.start { merkle_check.read_node, merkle_check.index, merkle_check.path_len, merkle_check.read_root }; | ||
|
|
||
| // ========= LOW LEAF VALIDATION ========= | ||
| // We commit leaf not exists instead of leaf exists since it'll be used as a selector for a lookup | ||
| pol commit leaf_not_exists; | ||
| leaf_not_exists * (1 - leaf_not_exists) = 0; | ||
| pol LEAF_EXISTS = 1 - leaf_not_exists; | ||
|
|
||
| pol commit slot_low_leaf_slot_diff_inv; | ||
| pol SLOT_LOW_LEAF_SLOT_DIFF = slot - low_leaf_slot; | ||
|
|
||
| // SLOT_LOW_LEAF_SLOT_DIFF == 0 <==> LEAF_EXISTS == 1 | ||
| #[EXISTS_FLAG_CHECK] | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Add a comment like: SLOT_LOW_LEAF_SLOT_DIFF == 0 <==> LEAF_EXISTS == 0 |
||
| sel * (SLOT_LOW_LEAF_SLOT_DIFF * (LEAF_EXISTS * (1 - slot_low_leaf_slot_diff_inv) + slot_low_leaf_slot_diff_inv) - 1 + LEAF_EXISTS) = 0; | ||
|
|
||
| // value = LEAF_EXISTS ? low_leaf_value : 0 | ||
| #[VALUE_IS_CORRECT] | ||
| low_leaf_value * LEAF_EXISTS - value = 0; | ||
|
|
||
| // If the leaf doesn't exist, we need to validate that the slot is greater than the low leaf slot | ||
|
|
||
| // TODO: We need this temporarily while we do not allow for aliases in the lookup tuple | ||
| pol commit one; | ||
| sel * (1 - one) = 0; | ||
|
|
||
| #[LOW_LEAF_SLOT_VALIDATION] | ||
| leaf_not_exists { slot, low_leaf_slot, one } | ||
| in ff_gt.sel_gt { ff_gt.a, ff_gt.b, ff_gt.result }; | ||
|
|
||
| // If next slot is not zero (which would be infinity), it has to be greater than the slot. | ||
| // We commit next_slot_is_nonzero instead of next_slot_is_zero since it'll be used as a selector for a lookup | ||
| pol commit next_slot_is_nonzero; | ||
| next_slot_is_nonzero * (1 - next_slot_is_nonzero) = 0; | ||
| pol NEXT_SLOT_IS_ZERO = 1 - next_slot_is_nonzero; | ||
|
|
||
| pol commit next_slot_inv; | ||
| #[NEXT_SLOT_IS_ZERO_CHECK] | ||
| leaf_not_exists * (low_leaf_next_slot * (NEXT_SLOT_IS_ZERO * (1 - next_slot_inv) + next_slot_inv) - 1 + NEXT_SLOT_IS_ZERO) = 0; | ||
|
|
||
| #[LOW_LEAF_NEXT_SLOT_VALIDATION] | ||
| next_slot_is_nonzero { low_leaf_next_slot, slot, one } | ||
| in ff_gt.sel_gt { ff_gt.a, ff_gt.b, ff_gt.result }; | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -70,9 +70,9 @@ std::vector<TestParams> comparison_tests = { | |
| TestParams{ 0, -1, false } | ||
| }; | ||
|
|
||
| class BasicTest : public TestWithParam<TestParams> {}; | ||
| class FieldGreaterThanBasicTest : public TestWithParam<TestParams> {}; | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think we were actually calling them SomethingConstrainingTest?
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes but this class name is appended to INSTANTIATE_TEST_SUITE_P(FieldGreaterThanConstrainingTest,
FieldGreaterThanBasicTest,
::testing::ValuesIn(comparison_tests));results in something like this |
||
|
|
||
| TEST_P(BasicTest, BasicComparison) | ||
| TEST_P(FieldGreaterThanBasicTest, BasicComparison) | ||
| { | ||
| const auto& param = GetParam(); | ||
|
|
||
|
|
@@ -92,11 +92,13 @@ TEST_P(BasicTest, BasicComparison) | |
| check_relation<ff_gt>(trace); | ||
| } | ||
|
|
||
| INSTANTIATE_TEST_SUITE_P(FieldGreaterThanConstrainingTest, BasicTest, ::testing::ValuesIn(comparison_tests)); | ||
| INSTANTIATE_TEST_SUITE_P(FieldGreaterThanConstrainingTest, | ||
| FieldGreaterThanBasicTest, | ||
| ::testing::ValuesIn(comparison_tests)); | ||
|
|
||
| class InteractionsTests : public TestWithParam<TestParams> {}; | ||
| class FieldGreaterThanInteractionsTests : public TestWithParam<TestParams> {}; | ||
|
|
||
| TEST_P(InteractionsTests, InteractionsWithRangeCheck) | ||
| TEST_P(FieldGreaterThanInteractionsTests, InteractionsWithRangeCheck) | ||
| { | ||
| const auto& param = GetParam(); | ||
|
|
||
|
|
@@ -123,7 +125,9 @@ TEST_P(InteractionsTests, InteractionsWithRangeCheck) | |
| check_relation<ff_gt>(trace); | ||
| } | ||
|
|
||
| INSTANTIATE_TEST_SUITE_P(FieldGreaterThanConstrainingTest, InteractionsTests, ::testing::ValuesIn(comparison_tests)); | ||
| INSTANTIATE_TEST_SUITE_P(FieldGreaterThanConstrainingTest, | ||
| FieldGreaterThanInteractionsTests, | ||
| ::testing::ValuesIn(comparison_tests)); | ||
|
|
||
| TEST(FieldGreaterThanConstrainingTest, NegativeManipulatedDecompositions) | ||
| { | ||
|
|
||
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.
@sirasistant We certainly can add a skippable condition.
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.
oh yes pleaaase! I didn't pay attention but basically we shouldn't merge any gadget without skippable
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.
Ugh, my bad, forgot about the skippable condition