sync spec & code (#107)

* sync spec & code

* move primitives (merkletree) into the backend

* comment on the ops spec and link to issue #108

* typo

* fix github-ci mdbook-publish pages
This commit is contained in:
arnaucube 2025-03-05 20:35:23 +01:00 committed by GitHub
parent 77f3f347e0
commit 02ec7c311b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
17 changed files with 90 additions and 64 deletions

View file

@ -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

View file

@ -22,7 +22,6 @@
- [POD types](./podtypes.md)
- [SignedPOD](./signedpod.md)
- [MainPOD](./mainpod.md)
- [MockPOD](./mockpod.md)
- [Examples](./examples.md)
# Architecture

View file

@ -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

View file

@ -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.

View file

@ -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 {
/// 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>;
/// 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
/// 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)

View file

@ -1 +0,0 @@
# MockPOD

View file

@ -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.

View file

@ -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) |
| 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)

View file

@ -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.

View file

@ -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,

View file

@ -1,3 +1,4 @@
pub mod basetypes;
pub mod mock_main;
pub mod mock_signed;
pub mod primitives;

View file

@ -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
@ -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
}

View file

@ -1,7 +1,7 @@
//! The frontend includes the user-level abstractions and user-friendly types to define and work
//! with Pods.
use anyhow::{anyhow, Error, Result};
use anyhow::{anyhow, Result};
use itertools::Itertools;
use std::collections::HashMap;
use std::convert::From;
@ -689,13 +689,12 @@ pub mod tests {
let sanction_list = sanction_list.sign(&mut signer)?;
println!("{}", sanction_list);
let kyc = zu_kyc_pod_builder(&params, &gov_id, &pay_stub, &sanction_list)?;
println!("{}", kyc);
let kyc_builder = zu_kyc_pod_builder(&params, &gov_id, &pay_stub, &sanction_list)?;
println!("{}", kyc_builder);
let mut prover = MockProver {};
let kyc = kyc.prove(&mut prover, &params)?;
let kyc = kyc_builder.prove(&mut prover, &params)?;
// TODO: prove kyc with MockProver and print it
println!("{}", kyc);
Ok(())
@ -735,7 +734,7 @@ pub mod tests {
let great_boy = great_boy_pod_full_flow()?;
println!("{}", great_boy);
// TODO: prove kyc with MockProver and print it
// TODO: prove great_boy with MockProver and print it
Ok(())
}

View file

@ -2,7 +2,6 @@ pub mod backends;
pub mod constants;
pub mod frontend;
pub mod middleware;
pub mod primitives;
mod util;
#[cfg(test)]

View file

@ -4,7 +4,9 @@ use anyhow::Result;
use std::collections::HashMap;
use crate::constants::MAX_DEPTH;
use crate::primitives::merkletree::{MerkleProof, MerkleTree};
#[cfg(feature = "backend_plonky2")]
use crate::backends::plonky2::primitives::merkletree::{Iter as TreeIter, MerkleProof, MerkleTree};
use super::basetypes::{hash_value, Hash, Value, EMPTY};
@ -42,13 +44,13 @@ impl Dictionary {
pub fn verify_nonexistence(root: Hash, proof: &MerkleProof, key: &Value) -> Result<()> {
MerkleTree::verify_nonexistence(MAX_DEPTH, root, proof, key)
}
pub fn iter(&self) -> crate::primitives::merkletree::Iter {
pub fn iter(&self) -> TreeIter {
self.mt.iter()
}
}
impl<'a> IntoIterator for &'a Dictionary {
type Item = (&'a Value, &'a Value);
type IntoIter = crate::primitives::merkletree::Iter<'a>;
type IntoIter = TreeIter<'a>;
fn into_iter(self) -> Self::IntoIter {
self.mt.iter()
@ -102,7 +104,7 @@ impl Set {
pub fn verify_nonexistence(root: Hash, proof: &MerkleProof, value: &Value) -> Result<()> {
MerkleTree::verify_nonexistence(MAX_DEPTH, root, proof, value)
}
pub fn iter(&self) -> crate::primitives::merkletree::Iter {
pub fn iter(&self) -> TreeIter {
self.mt.iter()
}
}
@ -147,7 +149,7 @@ impl Array {
pub fn verify(root: Hash, proof: &MerkleProof, i: usize, value: &Value) -> Result<()> {
MerkleTree::verify(MAX_DEPTH, root, proof, &Value::from(i as i64), value)
}
pub fn iter(&self) -> crate::primitives::merkletree::Iter {
pub fn iter(&self) -> TreeIter {
self.mt.iter()
}
}