Podlog language v1

[robknight]

This adds a simple DSL for specifying custom predicates and proof requests. It is similar to the language we have been using informally in our docs. The code includes tests, and should be capable of supporting all of our current predicates, with the exception of SetContains/SetNotContains. A language reference is included below.

Example

A proof request for ZuKYC:

REQUEST(
    NotContains(?sanctions["sanctionList"], ?gov["idNumber"]) 
    Lt(?gov["dateOfBirth"], ?SELF_HOLDER_18Y["const_18y"])      
    Equal(?pay["startDate"], ?SELF_HOLDER_1Y["const_1y"])         
    Equal(?gov["socialSecurityNumber"], ?pay["socialSecurityNumber"]) 
    ValueOf(?SELF_HOLDER_18Y["const_18y"], 1169909388)               
    ValueOf(?SELF_HOLDER_1Y["const_1y"], 1706367566)                  
)

Ethdos custom predicates:

eth_friend(src_ori, src_key, dst_ori, dst_key, private: attestation_pod) = AND(
    ValueOf(?attestation_pod["_type"], 1)
    Equal(?attestation_pod["_signer"], ?src_ori[?src_key])
    Equal(?attestation_pod["attestation"], ?dst_ori[?dst_key])
)

eth_dos_distance_base(src_ori, src_key, dst_ori, dst_key, distance_ori, distance_key) = AND(
    Equal(?src_ori[?src_key], ?dst_ori[?dst_key])
    ValueOf(?distance_ori[?distance_key], 0)
)

eth_dos_distance_ind(src_ori, src_key, dst_ori, dst_key, distance_ori, distance_key, private: one_ori, one_key, shorter_distance_ori, shorter_distance_key, intermed_ori, intermed_key) = AND(
    eth_dos_distance(?src_ori, ?src_key, ?intermed_ori, ?intermed_key, ?shorter_distance_ori, ?shorter_distance_key)
    ValueOf(?one_ori[?one_key], 1)
    SumOf(?distance_ori[?distance_key], ?shorter_distance_ori[?shorter_distance_key], ?one_ori[?one_key])
    eth_friend(?intermed_ori, ?intermed_key, ?dst_ori, ?dst_key)
)

eth_dos_distance(src_ori, src_key, dst_ori, dst_key, distance_ori, distance_key) = OR(
    eth_dos_distance_base(?src_ori, ?src_key, ?dst_ori, ?dst_key, ?distance_ori, ?distance_key)
    eth_dos_distance_ind(?src_ori, ?src_key, ?dst_ori, ?dst_key, ?distance_ori, ?distance_key)
)

Code structure

The grammar is implemented using Pest, which is able to derive a basic parser implementation from a grammar file. We have tests for this in parser.rs. The parsed input is then turned into an AST by the code in ast.rs. This closely mirrors the internal POD2 data structures, but may diverge in some ways (for example, by allowing certain pieces of syntactic sugar). Finally the AST is turned into POD2 internal data structures in processor.rs. There are end-to-end tests in mod.rs.

Outstanding issues

Currently SetContains and SetNotContains are unsupported, as de-sugaring these to lower-level templates might require some changes in MainPodBuilder or elsewhere. See #224

Next steps

If we're happy with the grammar here, I will update the code examples in the book to use this syntax.

Possible future features

A few features have been considered and are currently out-of-scope, but could be included in future:

Multiple custom predicate batches

For a given Podlog document, all custom predicates will be included in the same batch. We might want to give the user more control by allowing them to specify separate batches, e.g.:

batch "eth_friend" {
  eth_friend(A, B) = AND ( ... )
}

batch "eth_dos" {
  eth_dos_distance(X, Y) = AND ( eth_friend(X, Y) )
}

In this case, the call to eth_friend would be made via a CustomPredicateRef rather than a BatchSelf.

Import syntax

It might be helpful to be able to import custom predicates from different files. For example:

eth_friend = import("path/to/eth_friend.podlog").eth_friend

Given that each custom predicate has a unique hash, we could also imagine a content-addressable store of custom predicates:

eth_friend = import (0x123456abcdef)

Language reference

Language reference

Podlog Language Syntax

Podlog is a declarative language used for defining custom proof logic and requests within the POD2 ecosystem. It allows for the specification of statement templates that can be evaluated by a prover.

Table of Contents

1. Overview
2. Comments
3. Identifiers
4. Variables
5. Literals
   • Integer
   • String
   • Raw (Bytes)
   • Boolean
   • Array
   • Set
   • Dictionary
6. Anchored Keys
7. Top-Level Definitions
   • Custom Predicate Definition
   • Request Definition
8. Statements
   • Native Predicate Calls
   • Custom Predicate Calls

Overview

A Podlog document consists of zero or more top-level definitions, which can be either custom predicate definitions or a single request definition. The language is designed to be human-readable while providing precise instructions for the POD2 prover.

Comments

Single-line comments begin with //. All text from // to the end of the line is ignored.

// This is a comment.
is_valid(User) = AND( // This is an inline comment
    Equal(?User["status"], "active")
)

Identifiers

Identifiers are used for naming custom predicates and for the non-prefixed part of variable names.

• Must start with an uppercase or lowercase letter (A-Z, a-z) or an underscore (_).
• Subsequent characters can be letters, numbers (0-9), or underscores.
• Keywords like private, REQUEST, AND, OR, and native predicate names (e.g., Equal, ValueOf) cannot be used as predicate identifiers.
• The keyword private cannot be used as an identifier (e.g., for variable names).

Examples:
my_predicate
_internal_check
isValidUser1

Invalid:
123starts_with_digit
has-hyphen
private (as a predicate or variable name component)
Equal (as a predicate name)

Variables

Variables represent placeholders for values that the prover will attempt to bind.

• Variable names always start with a question mark (?).
• The part following the ? must adhere to the rules for Identifiers.

Examples:
?UserPod
?publicKey
?_tempValue

Literals

Literals represent fixed values.

Integer

A sequence of digits, optionally prefixed with a - for negative numbers.
Maps to middleware::Value::Int.

Examples: 123, -45, 0

String

Characters enclosed in double quotes (").
Standard JSON-like escaping rules apply for special characters:

• \" for double quote
• \\ for backslash
• / for forward slash (optional, / can be unescaped)
• \b for backspace
• \f for form feed
• \n for newline
• \r for carriage return
• \t for tab
• \uXXXX for a Unicode character specified by 4 hexadecimal digits.
  Maps to middleware::Value::String.

Examples: "hello", "user:name", "escaped \\\" quote", "\u0041"

Raw (Bytes)

A hexadecimal string prefixed with 0x. Must contain an even number of hex digits (0-9, a-f, A-F) and at least two digits.
Maps to middleware::Value::Raw.

Examples: 0xdeadbeef, 0x00, 0x0102030405060708090a0b0c0d0e0f10

Invalid: 0xabc (odd length), 0x (empty), 0xGG (invalid hex chars)

Boolean

The keywords true or false.
Maps to middleware::Value::Bool.

Examples: true, false

Array

A comma-separated list of literals enclosed in square brackets ([]). Elements can be of mixed types.
Maps to middleware::Value::Array.

Examples: [], [1, "two", true], [ [10, 20], #["a", "b"] ]

Set

A comma-separated list of literals enclosed in square brackets prefixed with a hash (#[]). Elements can be of mixed types. The processor will validate uniqueness if required by the underlying middleware.
Maps to middleware::Value::Set.

Examples: #[], #[1, 2, "apple"], #[ 0x01, 0x02 ]

Dictionary

A comma-separated list of string_key: literal_value pairs enclosed in curly braces ({}). Keys must be string literals.
Maps to middleware::Value::Dictionary.

Examples: {}, { "name": "Alice", "age": 30 }, { "data": [1,2,3], "metadata": { "version": "1.0" } }

Anchored Keys

Anchored keys are used to refer to values within a POD (represented by a variable).
Syntax: ?PodVariable["key_literal"] or ?PodVariable[?KeyVariable]

• ?PodVariable: A Variable representing a POD.
• "key_literal": A String Literal representing a fixed key.
• ?KeyVariable: A Variable representing a key to be resolved at runtime.

Examples:
?UserPod["name"]
?DataPod[?fieldName]

Top-Level Definitions

A Podlog document can contain multiple custom predicate definitions and at most one request definition.

Custom Predicate Definition

Defines a reusable piece of logic.

Syntax:
predicate_name(public_arg1, public_arg2, ..., private: private_arg1, private_arg2, ...) = CONJUNCTION_TYPE( statement1 statement2 ... )

• predicate_name: An Identifier for the predicate.
• Arguments:
  • A comma-separated list of public argument names (which are identifiers).
  • Optionally, followed by , private: and then a comma-separated list of private argument names (identifiers).
  • A predicate can have only public arguments, only private arguments (e.g., pred(private: PrivA) = ...), or no arguments (e.g., pred() = ...).
  • Argument names become Variables (e.g., ?public_arg1) within the predicate's scope.
• CONJUNCTION_TYPE: Either AND or OR.
  • AND: All statements in the body must be true.
  • OR: At least one statement in the body must be true.
• statement_list: One or more Statements enclosed in parentheses.

Examples:

// Predicate with only public arguments
is_equal_on_key(PodA, PodB, KeyName) = AND(
    Equal(?PodA[?KeyName], ?PodB[?KeyName])
)

// Predicate with public and private arguments
check_attestation(SrcOrigin, DstOrigin, private: AttestationPod) = AND(
    ValueOf(?AttestationPod["_type"], "MockSigned")
    Equal(?AttestationPod["_signer"], ?SrcOrigin["publicKey"])
    Equal(?AttestationPod["attestation"], ?DstOrigin["id"])
)

Request Definition

Defines the main set of statements to be proven by the prover. There can be at most one REQUEST block in a document.

Syntax:
REQUEST( statement1 statement2 ... )

• statement_list: Optional. If present, one or more Statements enclosed in parentheses. Variables used here are implicitly defined and their bindings are sought by the prover.

Example:

REQUEST(
    is_adult(?User) // Calling a custom predicate
    Equal(?User["countryCode"], ?X["country"])
    NotContains(?SanctionList["names"], ?User["fullName"])
)

Statements

Statements are the core assertions or operations within custom predicate definitions and request blocks.

Native Predicate Calls

These calls invoke built-in operations provided by the POD2 middleware. Arguments to native predicates are typically Anchored Keys, except for ValueOf which takes an Anchored Key and a Literal.

Core Predicates (Directly map to middleware operations):

• ValueOf(?PodVar["key"], LiteralValue)

  • Asserts that the value at ?PodVar["key"] is equal to LiteralValue.
  • Example: ValueOf(?Config["port"], 8080)

• Equal(?PodVar1["key1"], ?PodVar2["key2"])

  • Asserts that the values at the two anchored keys are equal.
  • Example: Equal(?User["id"], ?Order["userId"])

• NotEqual(?PodVar1["key1"], ?PodVar2["key2"])

  • Asserts that the values at the two anchored keys are not equal.
  • Example: NotEqual(?Account["status"], "suspended")

• Lt(?PodVar1["key1"], ?PodVar2["key2"])

  • Asserts value(?PodVar1["key1"]) < value(?PodVar2["key2"]).
  • Example: Lt(?Event["timestamp"], ?CutoffTime["value"])

• LtEq(?PodVar1["key1"], ?PodVar2["key2"])

  • Asserts value(?PodVar1["key1"]) <= value(?PodVar2["key2"]).
  • Example: LtEq(?User["age"], ?MaxAge["limit"])

• Contains(?PodVar[?Container], ?PodVar2[?Key], ?PodVar2[?Value])

  • A general predicate asserting that a container (e.g., dictionary, array, set) contains ?Value at a location specified by ?Key. In most cases, users should use DictContains, SetContains, or ArrayContains based on the expected type of the container.
  • Example: Contains(?Data["record"], ?User["nameKey"], ?User["expectedName"])

• NotContains(?PodVar[?Container], ?PodVar2[?Key])

  • A general predicate asserting that ?Key is not present in ?Container.
  • Example: NotContains(?Banlist["users"], ?User["id"])

• SumOf(?Target["keyT"], ?Source1["keyS1"], ?Source2["keyS2"])

  • Asserts that the value at ?Target["keyT"] equals the sum of the values at ?Source1["keyS1"] and ?Source2["keyS2"].
  • Example: SumOf(?Totals["all"], ?SubTotals["A"], ?SubTotals["B"])

• ProductOf(?Target["keyT"], ?Source1["keyS1"], ?Source2["keyS2"])

  • Asserts that the value at ?Target["keyT"] equals the product of the values at ?Source1["keyS1"] and ?Source2["keyS2"].
  • Example: ProductOf(?Area["rect"], ?Dimensions["width"], ?Dimensions["height"])

• MaxOf(?Target["keyT"], ?Source1["keyS1"], ?Source2["keyS2"])

  • Asserts that the value at ?Target["keyT"] is equal to either of the values at ?Source1["keyS1"] or ?Source2["keyS2"], whichever is higher.
  • Example: MaxOf(?Score["high"], ?Player1["score"], ?Player2["score"])

• HashOf(?Target["keyT"], ?Source1["keyS1"], ?Source2["keyS2"])

  • Asserts value(?Target["keyT"]) is the hash of value(?Source1["keyS1"]) and value(?Source2["keyS2"]).
  • Example: HashOf(?User["computedId"], ?User["email"], ?User["salt"])

Syntactic Sugar Predicates (Translated by the processor):

These provide more convenient syntax for common operations and are translated into the core middleware predicates.

• Gt(?PodVar1["key1"], ?PodVar2["key2"])

  • Asserts value(?PodVar1["key1"]) > value(?PodVar2["key2"]).
  • Translated to: Lt(?PodVar2["key2"], ?PodVar1["key1"]) (arguments are swapped).
  • Example: Gt(?User["score"], 1000)

• GtEq(?PodVar1["key1"], ?PodVar2["key2"])

  • Asserts value(?PodVar1["key1"]) >= value(?PodVar2["key2"]).
  • Translated to: LtEq(?PodVar2["key2"], ?PodVar1["key1"]) (arguments are swapped).
  • Example: GtEq(?Balance["amount"], ?Minimum["required"])

• DictContains(?DictVar["dict_key"], ?KeyToFind["key_name"], ?ExpectedValue["val_name"])

  • Asserts value(?DictVar["dict_key"][?KeyToFind["key_name"]]) == value(?ExpectedValue["val_name"]).
  • Translated to: Contains(?DictVar["dict_key"], ?KeyToFind["key_name"], ?ExpectedValue["val_name"]) (or similar, depending on exact mapping to generic Contains).
  • Example: DictContains(?UserPod["attributes"], ?_KeyNamePod["name"], ?_ExpectedValuePod["admin"])
    • Where ?_KeyNamePod["name"] might resolve to a literal key like "role" and ?_ExpectedValuePod["admin"] to "admin".

• DictNotContains(?DictVar["dict_key"], ?KeyToFind["key_name"])

  • Asserts that ?KeyToFind["key_name"] is not a key in value(?DictVar["dict_key"]).
  • Translated to: NotContains(?DictVar["dict_key"], ?KeyToFind["key_name"]).
  • Example: DictNotContains(?UserPod["flags"], ?_FlagNamePod["is_banned"])

• ArrayContains(?ArrayVar["array_key"], ?IndexVar["idx_name"], ?ExpectedValue["val_name"])

  • Asserts value(?ArrayVar["array_key"][?IndexVar["idx_name"]]) == value(?ExpectedValue["val_name"]).
  • Translated to: Contains(?ArrayVar["array_key"], ?IndexVar["idx_name"], ?ExpectedValue["val_name"]).
  • Example: ArrayContains(?LogPod["entries"], ?_IndexPod["target_idx"], ?_ValuePod["error_code_X"])

(Note: SetContains and SetNotContains are currently missing, pending an implementation for de-sugaring.)

Custom Predicate Calls

Calls a previously defined custom predicate.

Syntax:
predicate_name(arg1, arg2, ...)

• predicate_name: The Identifier of the custom predicate to call.
• arg_list: A comma-separated list of arguments. Arguments can be Variables or Literals. The number and type of arguments must match the public argument definition of the called predicate.

Example:

has_permission(User, Permission, private: Roles) = AND(
    // ... logic using ?User, ?Permission, ?Roles
)

REQUEST(
    has_permission(?CurrentUser, "edit_document")
    ValueOf(?SystemConfig["audit_level"], 3)
)

[ed255]

Some thoughts after reading the PR description (I haven't reviewed the code yet)

• Being able to define multiple batches in a single file sounds good! It would also make it easier to define the batch name. And I assume the changes needed to have that aren't very big. But maybe that's not necessary depending on the answer to the following question:
  • Do you envision that podlog is written to a file? In that case having a syntax to define batches would be useful
  • Do you envision that podlog is written inline in other code? In that case I don't think it's needed, because then it's easy to define multiple batches by writing multiple "snippets of podlog.
• I notice you call Wildcards as Variables. Is that more intuitive to you? Actually if I think about it "variable" makes a lot of sense: in first order logic the quantifiers are variables https://en.wikipedia.org/wiki/Existential_quantification but we're calling them wildcards because we're thinking about a template and the replacement. This also makes me wonder: should we stop calling them Statement Templates and call them Formulas? Or Quantified Statements?
• For sets, arrays and dictionaries: would it make sense to be able to define a request or a custom predicate in podlog but instead of hardcoding the set/array/dict it's defined externally? Like this (and after parsing, you need to pass a value for sanction_list:

extern sanction_list

REQUEST(
    NotContains(sanction_list, ?gov["idNumber"])                   
)

This would apply in generals to literal values that appear in templates. Another example would be a request that involves a statement to show that someone is over 18 years old. To do that we need to calculate a value that is 18 years in the past from now, and this value will change every time we do a request; so being able to pass this value externally would be useful.

Questions

• Can I use a custom predicate defined in a previous document?

[ed255]

I've finished reviewing this PR and I'm marking request changes because there are significant changes to the approach of this PR that I want to discuss.

[ed255]

This looks over complicated. You don't need to encode the bytes into a hex string to do that.
A RawValue is 4 goldiclocks field elements, which can be represented with 64 bits each.
You just need to build each goldilock field element with 64/8 = 8 bytes from the bytes vector.
Also you need to make a decision on the endianness of the bytes vector (and please document the endianness in the grammar).

Also to simplify things I would change the grammar to force the literal_raw to be 32 bytes (or 64 hex characters).

Finally: the goldilocks field is smaller than 2^64-1. This means that some values have aliases, for example 1 and p-1 fit into 64 bits and are the same value but look different when encoded into bytes. I suggest that the parser checks that each array of bytes corresponding to a field element represents an integer that is smaller than p. The method GoldilocksField::from_canonical_u64 performs this check but only in debug mode, not in release. We should check n < Self::GoldilocksField and return an error if that's not the case.

[ed255]

Here you're doing two checks:
Make sure there's a ? prefix and making sure the identifier is not empty. But the grammar already enforces this!
So by the definition of the grammar, these two errors will never occur.
More over, if they were to happen, it would be a bug in the code because either pest is not returning a parsing error, or the grammar is not well defined. For those cases I strongly suggest that we panic instead, and we can do this cleanly with expect.

Please take a look at this commit where I've made some changes to simplify this following this idea:
b806322

I think there are a few more places where this changes can be applied. The only place where we need to do some checking and do proper error reporting is when handling native predicates because their argument types are not validated by the grammar.

But any time we find a rule defined in the grammar, we know that the tokens defined by the grammar will be there. For example, every time we find the Rule::anchored_key we know for sure that we'll encounter 2 Pairs. The first one will either be self_keyword or wildcard; and the second one will either be wildcard or literal_string. Any other case is not expected to happen on any kind of user input.

[ed255]

I just realized we already had this functionality here:

pod2/src/middleware/basetypes.rs

Lines 209 to 218 in d3fef83

	fn from_hex<T: AsRef<[u8]>>(hex: T) -> Result<Self, Self::Error> {
	// In little endian
	let bytes = <[u8; 32]>::from_hex(hex)?;
	let mut buf: [u8; 8] = [0; 8];
	let mut inner = [F::ZERO; HASH_SIZE];
	for i in 0..HASH_SIZE {
	buf.copy_from_slice(&bytes[8 * i..8 * (i + 1)]);
	inner[i] = F::from_canonical_u64(u64::from_le_bytes(buf));
	}
	Ok(Self(inner))

It's used to deserialize a Hash from a hex string, and internally it creates the 4 field elements, which is the same we need to get a RawValue. Then you can do RawValue::from(h: Hash).

The encoding is different though, and it doesn't use a 0x prefix.
The encoding uses little endian, and taking a little endian hex encoded value and adding a 0x prefix is confusing from my point of view.

[ed255]

LGTM! Thanks for addressing all the requests!