Skip to content

sync spec & code#107

Merged
tideofwords merged 5 commits intomainfrom
sync-spec-and-code
Mar 5, 2025
Merged

sync spec & code#107
tideofwords merged 5 commits intomainfrom
sync-spec-and-code

Conversation

@arnaucube
Copy link
Collaborator

@arnaucube arnaucube commented Mar 3, 2025 •
edited
Loading

resolves #103

@arnaucube arnaucube added this to the Milestone 2 milestone Mar 3, 2025
arnaucube
arnaucube commented Mar 3, 2025
View reviewed changes
book/src/operations.md Outdated
Comment on lines +29 to +37
<span style="color:red">WIP, the following ones were appearing at the docs table but not at the implementation ([src/middleware/operation.rs](https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20)):</span><br>
<span style="color:red">TODO rm?</span>
| Code | Identifier | Args | Condition | Output |
|------|-----------------------|---------------------|-----------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------|
| 3 | `SymmetricEq` | `s` | `s = Equal(ak1, ak2)` | `Eq(ak2, ak1)` |
| 4 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
| 5 | `EntryNEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NEq(ak1, ak2)` |
| 6 | `SymmetricNEq` | `s` | `s = NotEqual(ak1, ak2)` | `NEq(ak2, ak1)` |
| 7 | `GtToNEq` | `s` | `s = Gt(ak1, ak2)` | `NEq(ak1, ak2)` |
| 8 | `LEqToNEq` | `s` | `s = LEq(ak1, ak2)` | `NEq(ak1, ak2)` |
| 9 | `EntryGt` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2` | `Gt(ak1, ak2)` |
| 16 | `RenameSintains` | `s1`, `s2` | `s1 = Sintains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Sintains(ak4, ak2)` |
| 7 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
| 6 | `LEqToNEq` | `s` | `s = LEq(ak1, ak2)` | `NEq(ak1, ak2)` |
Copy link
Collaborator Author

@arnaucube arnaucube Mar 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ax0 @tideofwords , question: the table from lines 8 to 25 contains the same ops that are implemented at https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20 ; the table from lines 31 to 39 contains the ops that were at the table previous to this commit, but that don't appear at the rust impl. Should those ops be added to the implementation? or we should remove them from the spec?

Copy link
Collaborator Author

@arnaucube arnaucube Mar 4, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

After seeing #108 , thought about keeping the ones that appear in the 2nd table, with a comment remarking that those are not yet implemented. The changes can be seen at the commit fac9b7a .

Copy link
Collaborator

@tideofwords tideofwords Mar 5, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, this sounds good to me. I think we'll have to refine the list of operations anyway...

arnaucube
arnaucube commented Mar 3, 2025
View reviewed changes
book/src/operations.md
Comment on lines 10 to +25
| 0 | `None` | | | `None` |
| 1 | `NewEntry`[^newentry] | `(key, value)` | | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 |
| 2 | `EntryEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Eq(ak1, ak2)` |
| 2 | `CopyStatement` | `s` | | |
| 3 | `EntryEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Eq(ak1, ak2)` |
| 4 | `EntryNEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NEq(ak1, ak2)` |
| 5 | `EntryGt` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2` | `Gt(ak1, ak2)` |
| 6 | `EntryLEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LEq(ak1, ak2)` |
| 7 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
| 8 | `GtToNEq` | `s` | `s = Gt(ak1, ak2)` | `NEq(ak1, ak2)` |
| 9 | `LtToNEq` | `s` | `s = Lt(ak1, ak2)` | `NEq(ak1, ak2)` |
| 10 | `EntryContains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_includes(value1, value2, proof) = true` | `Contains(ak1, ak2)` |
| 11 | `EntrySintains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `Sintains(ak1, ak2)` |
| 12 | `RenameContains` | `s1`, `s2` | `s1 = Contains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Contains(ak4, ak2)` |
| 13 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
| 14 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
| 15 | `MaxOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = max(value2, value3)` | `MaxOf(ak1, ak2, ak3)` |
Copy link
Collaborator Author

@arnaucube arnaucube Mar 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(this table is updated to match the same enumeration as in https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20 )

@arnaucube arnaucube force-pushed the sync-spec-and-code branch 2 times, most recently from 65564ab to 8387f8b Compare March 3, 2025 21:46
arnaucube
arnaucube commented Mar 3, 2025
View reviewed changes
book/src/statements.md
| 4 | `Gt` | `ak1`, `ak2` | `value_of(ak1) > value_of(ak2)` |
| 5 | `LEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
| 6 | `Contains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
| 7 | `NotContains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
Copy link
Collaborator Author

@arnaucube arnaucube Mar 3, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

did this change to make it match the implementation naming, but later realized that other sections of the spec use Sintains. Maybe we should stick to either Sintains or NotContains everywhere (code & spec).

Copy link
Collaborator

@ax0 ax0 Mar 5, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apparently Sintains has fallen out of favour, so we'll have to go with NotContains.

Copy link
Collaborator Author

@arnaucube arnaucube Mar 5, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

well in this specific line I changed it to NotContains but because is what I saw on other parts of the code, but later saw other sections of the spec that still use Sintains and left those with that. So even after this current PR we'll keep having both Sintains and NotContains at different places.
I think it's not a deal breaker for now, so not 'urgent' to fix, but something to have in mind and maybe over the next days we can agree on one of them.

@arnaucube arnaucube force-pushed the sync-spec-and-code branch from 8387f8b to 2245185 Compare March 3, 2025 23:20
@arnaucube arnaucube force-pushed the sync-spec-and-code branch from 66696cd to 7c933e8 Compare March 4, 2025 13:30
@arnaucube arnaucube force-pushed the sync-spec-and-code branch from 7f37322 to fac9b7a Compare March 4, 2025 17:48
@arnaucube arnaucube marked this pull request as ready for review March 4, 2025 17:49
@arnaucube arnaucube requested review from ax0 and tideofwords March 4, 2025 17:49
arnaucube
arnaucube commented Mar 4, 2025
View reviewed changes
book/src/merkletree.md
@@ -145,39 +145,48 @@ For the current use cases, we don't need to prove that the key exists but the va

```rust
impl MerkleTree {
Copy link
Collaborator Author

@arnaucube arnaucube Mar 4, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(the changes in this file are just to update the merkletree.md#Interface to match the rust implementation interface)

@arnaucube arnaucube force-pushed the sync-spec-and-code branch from 1c5dccd to 4f7a8ed Compare March 4, 2025 17:53
ax0
ax0 approved these changes Mar 5, 2025
View reviewed changes
Copy link
Collaborator

@ax0 ax0 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM!

book/src/statements.md
| 4 | `Gt` | `ak1`, `ak2` | `value_of(ak1) > value_of(ak2)` |
| 5 | `LEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
| 6 | `Contains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
| 7 | `NotContains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
Copy link
Collaborator

@ax0 ax0 Mar 5, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Apparently Sintains has fallen out of favour, so we'll have to go with NotContains.

@tideofwords tideofwords merged commit 02ec7c3 into main Mar 5, 2025
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ax0 ax0 ax0 approved these changes

@tideofwords tideofwords Awaiting requested review from tideofwords

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

Milestone 2

Development

Successfully merging this pull request may close these issues.

Sync spec & code

3 participants

@arnaucube @ax0 @tideofwords