Custom statements and custom operations

Users of the POD system can introduce custom predicates (previously called custom statements) to express complex logical relations not available in the built-in predicates. Every custom predicate is defined as the conjunction (AND) or disjunction (OR) of a small number of other statements.

When a custom predicate is introduced in a MainPod, it becomes available for use in that POD and all PODs that inherit¹ from it.

On the frontend, a custom predicate is defined as a collection of conjunctions and disjunctions of statements. The definition can be recursive: the definition of a predicate can involve the predicate itself, or the definitions of several predicates can depend on each other.

At the backend level, every definition of a predicate is either a conjunction or a disjunction of statements. To convert a frontend custom predicate to the backend, the middleware may need to introduce sub-predicates.

On the backend, custom predicates are defined in groups. A group can contain one or more custom predicates and their associated sub-predicates. Recursive definition is only possible within a group: the definition of a predicate in a group can only depend on previously existing predicates, itself, and other predicates in the same group.

Arguments of custom predicates

The definition of a custom predicate might also be called an operation or deduction rule. It includes two (or, potentially, say, five) statement templates as conditions. The arguments to the statement templates are decomposed as (origin, key) pairs: if statements are allowed to have arity at most 4, then the statement templates in a deduction rule will have at most 8 arguments (4 origins and 4 keys). The same holds for the output statement.

Each argument (origin or key) to an statement template is either a wildcard or a literal. In the backend, the wildcard arguments will be identified as *1, *2, *3, ....

Examples

See examples

Hashing and predicate IDs

Each custom predicate is defined as part of a group of predicates. The definitions of all statements in the group are laid out consecutively (see examples) and hashed. For more details, see the pages on hashing custom statements and custom predicates.

How to prove an application of an operation

The POD proof format is inspired by "two-column proofs" (for an example, see Wikipedia). A POD contains a "tabular proof", in which each row includes a "statement" and an "operation". The "operation" is the "reason" that justifies the statement: it is everything the circuit needs as a witness to verify the statement.

For a custom statement, the "reason" includes the following witnesses and verifications:

• the definition of the statement, serialized (see examples)
  • if the statement is part of a group, the definition of the full group, serialized
• verify that the hash of the definition is the statement ID
• the definition will have some number of "wildcards" (*1, *2, ...) as arguments to statement templates; a value for each wildcard must be provided as a witness (each will be either an origin ID or key)
• the circuit must substitute the claimed values for the wildcards, and the resulting statements (true statements with origins and keys) will appear as witnesses
• the circuit must verify that all the input statement templates (with origins and keys) appear in the previous statements (in higher rows of the table)
• the circuit also substitutes the claimed values for the wildcards in the output statement, and verifies that it matches the claimed output statement