Skip to content

sync spec & code #107

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

Merged
tideofwords merged 5 commits into from
Mar 5, 2025
Merged

sync spec & code #107

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
2245185
sync spec & code
arnaucube Mar 3, 2025
7c933e8
move primitives (merkletree) into the backend
arnaucube Mar 4, 2025
fac9b7a
comment on the ops spec and link to issue #108
arnaucube Mar 4, 2025
4f7a8ed
typo
arnaucube Mar 4, 2025
7aaf9df
fix github-ci mdbook-publish pages
arnaucube Mar 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/mdbook-publish.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ jobs:
run: |
curl --proto '=https' --tlsv1.2 https://sh.rustup.rs -sSf -y | sh
rustup update
rustup toolchain install nightly-x86_64-unknown-linux-gnu
cargo install --version ${MDBOOK_VERSION} mdbook
cargo install --version ${MDBOOKKATEX_VERSION} mdbook-katex
- name: Setup Pages
Expand Down
2 changes: 1 addition & 1 deletion book/book.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,4 +9,4 @@ title = "POD2-docs"
default-theme = "light"

[preprocessor.katex]
after = ["links"]
after = ["links"]
1 change: 0 additions & 1 deletion book/src/SUMMARY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@
- [POD types](./podtypes.md)
- [SignedPOD](./signedpod.md)
- [MainPOD](./mainpod.md)
- [MockPOD](./mockpod.md)
- [Examples](./examples.md)

# Architecture
Expand Down
1 change: 1 addition & 0 deletions book/src/examples.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
Examples of POD2 use cases

## EthDos
*Check also the [custom statement example](./customexample.md) section.*

Original in prolog https://gist.github.com/ludns/f84b379ec8c53c97b7f95630e16cc39c#file-eth_dos-pl

Expand Down
4 changes: 2 additions & 2 deletions book/src/merklestatements.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
The front end has three compound types
- `Dictionary`
- `Array`
- `Set`,
- `Set`

all of which are represented as `MerkleTree` on the back end.

Expand Down Expand Up @@ -194,4 +194,4 @@ keyhash = hash(key)
```ContainsValue(root, value)``` is deduced from
```
Contains(root, idx, value).
```
```
31 changes: 20 additions & 11 deletions book/src/merkletree.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

/// builds a new `MerkleTree` where the leaves contain the given key-values
fn new(max_depth: usize, kvs: &HashMap<Value, Value>) -> Result<Self>;

/// returns the root of the tree
fn root(&self) -> Hash;

/// returns the max_depth parameter from the tree
fn max_depth(&self) -> usize;

/// returns the value at the given key
fn get(&self, key: &Value) -> Result<Value>;

/// returns a boolean indicating whether the key exists in the tree
fn contains(&self, key: &Value) -> bool;
fn contains(&self, key: &Value) -> Result<bool>;

/// returns a proof of existence, which proves that the given key exists in
/// the tree. It returns the `MerkleProof`.
fn prove(&self, key: &Value) -> Result<MerkleProof>;

/// returns a proof of non-existence, which proves that the given `key`
/// does not exist in the tree
/// the tree. It returns the `value` of the leaf at the given `key`, and the
/// `MerkleProof`.
fn prove(&self, key: &Value) -> Result<(Value, MerkleProof)>;

/// returns a proof of non-existence, which proves that the given
/// `key` does not exist in the tree. The return value specifies
/// the key-value pair in the leaf reached as a result of
/// resolving `key` as well as a `MerkleProof`.
fn prove_nonexistence(&self, key: &Value) -> Result<MerkleProof>;

/// verifies an inclusion proof for the given `key` and `value`
fn verify(root: Hash, proof: &MerkleProof, key: &Value, value: &Value) -> Result<()>;
fn verify(max_depth: usize, root: Hash, proof: &MerkleProof,
key: &Value, value: &Value,) -> Result<()>;

/// verifies a non-inclusion proof for the given `key`, that is, the given
/// `key` does not exist in the tree
fn verify_nonexistence(root: Hash, proof: &MerkleProof, key: &Value) -> Result<()>;
fn verify_nonexistence( max_depth: usize, root: Hash,
proof: &MerkleProof, key: &Value,) -> Result<()>;

/// returns an iterator over the leaves of the tree
fn iter(&self) -> std::collections::hash_map::Iter<Value, Value>;
fn iter(&self) -> Iter;
}
```

## Development plan
- short term: merkle tree as a 'precompile' in POD operations, which allows to directly verify proofs
- initial version: just a wrapper on top of the existing Plonky2's MerkleTree
- second iteration: implement the MerkleTree specified in this document
- long term exploration:
- explore feasibility of using Starky (for lookups) connected to Plonky2, which would allow doing the approach described at [https://hackmd.io/@aardvark/SkJ-wcTDJe](https://hackmd.io/@aardvark/SkJ-wcTDJe)

Expand Down
1 change: 0 additions & 1 deletion book/src/mockpod.md
View file
Open in desktop

This file was deleted.

50 changes: 32 additions & 18 deletions book/src/operations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,23 +9,37 @@ The following table summarises the natively-supported operations:
|------|-----------------------|---------------------|-----------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------|
| 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)` |
| 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)` |
| 10 | `TransitiveGt` | `s1`, `s2` | `s1 = Gt(ak1, ak2)`, `s2 = Gt(ak3, ak4)`, `ak2 = ak3` | `Gt(ak1, ak4)` |
| 11 | `EntryLEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LEq(ak1, ak2)` |
| 12 | `TransitiveLEq` | `s1`, `s2` | `s1 = LEq(ak1, ak2)`, `s2 = LEq(ak3, ak4)`, `ak2 = ak3` | `LEq(ak1, ak4)` |
| 13 | `EntryContains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_includes(value1, value2, proof) = true` | `Contains(ak1, ak2)` |
| 14 | `RenameContains` | `s1`, `s2` | `s1 = Contains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Contains(ak4, ak2)` |
| 15 | `EntrySintains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `Sintains(ak1, ak2)` |
| 16 | `RenameSintains` | `s1`, `s2` | `s1 = Sintains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Sintains(ak4, ak2)` |
| 17 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
| 18 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
| 19 | `MaxOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = max(value2, value3)` | `MaxOf(ak1, ak2, ak3)` |
| 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)` |

<!-- NOTE: should we 'uniformize' the names? eg. currently we have `EntryGt` and `GtToNEq` -->

<br><br>

<span style="color:green"><b>WIP</b>. The following table defines more operations that are not yet [implemented](https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20).<br>
Issue keeping track of the operations: [#108](https://github.com/0xPARC/pod2/issues/108).
</span><br>
| Code | Identifier | Args | Condition | Output |
|------|------------------|------------|----------------------------------------------------------------|----------------------|
| | `SymmetricEq` | `s` | `s = Equal(ak1, ak2)` | `Eq(ak2, ak1)` |
| | `SymmetricNEq` | `s` | `s = NotEqual(ak1, ak2)` | `NEq(ak2, ak1)` |
| | `RenameSintains` | `s1`, `s2` | `s1 = Sintains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Sintains(ak4, ak2)` |
| | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
| | `TransitiveGt` | `s1`, `s2` | `s1 = Gt(ak1, ak2)`, `s2 = Gt(ak3, ak4)`, `ak2 = ak3` | `Gt(ak1, ak4)` |
| | `TransitiveLEq` | `s1`, `s2` | `s1 = LEq(ak1, ak2)`, `s2 = LEq(ak3, ak4)`, `ak2 = ak3` | `LEq(ak1, ak4)` |
| | `LEqToNEq` | `s` | `s = LEq(ak1, ak2)` | `NEq(ak1, ak2)` |


[^newentry]: Since new key-value pairs are not constrained, this operation will have no arguments in-circuit.
33 changes: 17 additions & 16 deletions book/src/statements.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,28 +18,29 @@ The POD system has several builtin statements. These statements are associated t

### Backend statements

<font color="red">TODO: update table of backend statements </font>

A statement is a code (or, in the frontend, string identifier) followed by 0 or more arguments. These arguments may consist of up to three anchored keys and up to one POD value.

The following table summarises the natively-supported statements, where we write `value_of(ak)` for 'the value anchored key `ak` maps to', which is of type `PODValue`, and `key_of(ak)` for the key part of `ak`:

| Code | Identifier | Args | Meaning |
|------|-------------|---------------------|-------------------------------------------------------------------|
| 0 | `None` | | no statement (useful for padding) |
| 1 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` |
| 2 | `Eq` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
| 3 | `NEq` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
| 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 | `Sintains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
| 8 | `SumOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)` |
| 9 | `ProductOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) * value_of(ak3)` |
| 10 | `MaxOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = max(value_of(ak2), value_of(ak3))` |
| Code | Identifier | Args | Meaning |
|------|---------------|---------------------|-------------------------------------------------------------------|
| 0 | `None` | | no statement (useful for padding) |
| 1 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` |
| 2 | `Eq` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
| 3 | `NEq` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
| 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.

| 8 | `SumOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)` |
| 9 | `ProductOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) * value_of(ak3)` |
| 10 | `MaxOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = max(value_of(ak2), value_of(ak3))` |

### Frontend statements

<span style="color:red">TODO: Current implementation frontend Statements reuse the middleware Statements, which:</span><br>
<span style="color:red">- 1: GEq & LEq don't appear in the frontend impl</span><br>
<span style="color:red">- 2: frontend impl has Contains & NotContains, which don't appear at the following block</span>
```
ValueOf(key: AnchoredKey, value: ScalarOrVec)

Expand Down Expand Up @@ -150,4 +151,4 @@ ecdsa_priv_to_pub_of(A.pubkey, B.privkey)

[^builtin]: <font color="red">TODO</font> List of built-in statements is not yet complete.

[^fillsum]: <font color="red">TODO</font> Does sum mean x+y = z or x = y+z?
[^fillsum]: <font color="red">TODO</font> Does sum mean x+y = z or x = y+z?
2 changes: 1 addition & 1 deletion book/src/values.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ In the frontend, this is a simple bool. In the backend, it will have the same e
In the frontend, this type corresponds to the usual `String`. In the backend, the string will be mapped to a sequence of field elements and hashed with the hash function employed there, thus being represented by its hash.

## `Raw`
"Raw" is short for "raw value". A `Raw` exposes a backend value on the frontend.
"Raw" is short for "raw value". A `Raw` exposes a [backend `Value`](./backendtypes.md) on the frontend.

With the plonky2 backend, a `Raw` is a tuple of 4 elements of the Goldilocks field.

Expand Down
2 changes: 1 addition & 1 deletion src/backends/plonky2/mock_signed.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@ use anyhow::Result;
use std::any::Any;
use std::collections::HashMap;

use super::primitives::merkletree::MerkleTree;
use crate::constants::MAX_DEPTH;
use crate::middleware::{
containers::Dictionary, hash_str, AnchoredKey, Hash, Params, Pod, PodId, PodSigner, PodType,
Statement, Value, KEY_SIGNER, KEY_TYPE,
};
use crate::primitives::merkletree::MerkleTree;

pub struct MockSigner {
pub pk: String,
Expand Down
1 change: 1 addition & 0 deletions src/backends/plonky2/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
pub mod basetypes;
pub mod mock_main;
pub mod mock_signed;
pub mod primitives;
3 changes: 2 additions & 1 deletion src/primitives/merkletree.rs → ...backends/plonky2/primitives/merkletree.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ use std::collections::HashMap;
use std::fmt;
use std::iter::IntoIterator;

use crate::middleware::{Hash, Value, F, NULL};
use crate::backends::plonky2::basetypes::{Hash, Value, F, NULL};

/// Implements the MerkleTree specified at
/// https://0xparc.github.io/pod2/merkletree.html
Expand Down Expand Up @@ -37,6 +37,7 @@ impl MerkleTree {
self.root.hash()
}

/// returns the max_depth parameter from the tree
pub fn max_depth(&self) -> usize {
self.max_depth
}
Expand Down
0 src/primitives/mod.rs → src/backends/plonky2/primitives/mod.rs
View file
Open in desktop
File renamed without changes.
Loading
Loading