Aard custom #49

tideofwords · 2025-02-10T16:35:05Z

initial PR for custom deduction docs

Make syntax and notation consistent with Rust source code.

Co-authored-by: Ahmad Afuni <[email protected]>

ed255 · 2025-02-17T14:27:55Z

book/src/custom.md

+
+When a custom predicate is introduced in a MainPod, it becomes available for use in that POD and all PODs that inherit[^inherit] from it.
+
+A custom predicate can be defined either _nonrecursively_ or _recursively_ (as part of a "batch"). A nonrecursive custom predicate is defined in terms of previously defined predicates (whether custom or native).  A "batch" of custom predicates can be defined _recursively_: the definition of any custom predicate in the batch can use both previously defined predicates and all the predicates in the batch.


About the "batch" term. Can we discuss alternatives?
I've thought about "group" or "unit".

We could also use the terminology: a custom predicate is defined with conjunctions and disjunctions of statements. At the backend level this is achieved with sub-predicates that are either conjunctions or disjunctions. So with this naming there's no "batch", it's either a custom predicate (high level view) or sub-predicate (what you call a custom predicate that belongs to a batch).

Also, could we agree that a list of predicates that form a batch have a single top level predicate, which is the one that the user cares about?

Changing to "group".

In general, will the frontend allow combinations of conjunction and disjunction in a single custom predicate? As in
pred1:
AND(OR(pred2, pred3), pred4)?
This looks like a good idea.

In this case, of course we would also allow a recursive definition, like
pred1:
AND(OR(pred2, pred3), pred1).

If we require a single top-level predicate for each group, the user won't be able to make multiple predicates depend on each other recursively. I can't think of a natural use case where you would want that, but if the backend allows it, why disable it on the frontend?

Changing to "group".

In general, will the frontend allow combinations of conjunction and disjunction in a single custom predicate? As in pred1: AND(OR(pred2, pred3), pred4)? This looks like a good idea.

In this case, of course we would also allow a recursive definition, like pred1: AND(OR(pred2, pred3), pred1).

I also think this is a good idea for the frontend. Nevertheless I also think it's OK to start with a simpler version where we don't implement it yet and leave it as a TODO for later.

If we require a single top-level predicate for each group, the user won't be able to make multiple predicates depend on each other recursively. I can't think of a natural use case where you would want that, but if the backend allows it, why disable it on the frontend?

Why having a single top-level predicate in a group doesn't allow the user to have multiple predicates depend on each other recursively? Is it because those internal predicates don't have names that the user can refer to? If that's the case, I think the user could still give names to internal predicates during the build process to reference them, and still end up with a single top-level predicate in the group. Or is there any other reason?

I thought about assuming a single top-level predicate for each group because then we could say the top-level (entry-point) predicate always takes the same index in the group (let's say: 0). This would be a convention that could facilitate debugging.

ed255 · 2025-02-17T14:30:20Z

book/src/custom.md

+
+## Custom predicates and their IDs
+
+A custom predicate, like a built-in predicate, is identified by a _name_ on the front end and an _identifier_ on the back end.  In the non-recursive case, the back-end identifier is defined as a hash of the definition of the custom predicate.


I would propose that in the backend we don't distinguish recursive and non-recursive cases (or batched / non-batched). Instead all custom predicates have the recursivity capability. And if we don't need recursion we just make a batch of a single predicate.

Implementation wise that may mean that we make a merkle tree out of a single custom predicate and identify it with mt_root.0

Sounds good to me

ed255 · 2025-02-17T14:41:37Z

book/src/custom1.md

+you have to provide the following witnesses in-circuit.
+
+- Copy of the deduction rule
+- Values for *1, *2, *3, *4, *5.  (*1, *2, *4 should be OriginIDs for the three origins; *3 and *5 should be key names.)


I wonder if we could skip the type checking in the circuit, considering that all of these values are encoded as 4 field elements in plonky2.

That's right, you don't have to enforce type checking in-circuit (I think you can't anyway?), because the conditions can only be satisfied if the types are right.

ed255 · 2025-02-17T14:59:02Z

book/src/custom1b.md

+
+The definition of a custom predicate might also be called an _operation_ or _deduction rule_.  It includes two (or, potentially, say, five) input statements.  The arguments to the input statements are decomposed as (origin, key) pairs: if statements are allowed to have arity at most 4, then the input statements 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 input statement is either a wildcard or a literal.  In the backend, the wildcard arguments will be identified as *1, *2, *3, ....


I would propose using the name "statement template" for statements we use to build a custom predicate.
The template would include the Predicate and the list of "template arguments" which would be what you call "wildcard".

I looked at two famous template libraries and they call this "wildcards" "tags"

http://mustache.github.io/mustache.5.html

https://jinja.palletsprojects.com/en/stable/templates/

But I think I like the term "wildcard" better than "tag".

"Statement templates" is good

book/src/custom2.md

ed255 · 2025-02-17T15:12:08Z

book/src/custom2.md

+Equal(name_from_pod1, friend_from_pod2)
+```
+
+## How to inherit local variables from a previous POD


I would appreciate an example use-case to be added here https://github.com/0xPARC/pod2/blob/main/book/src/examples.md
which requires propagating keys from PODs, because I believe there are different ways to approach this propagation / inheritance of keys but I find it hard to reason if a particular way is good or not because I don't have a use-case to validate it.

Cool, I'm adding "attested great boy pod", which reveals the names of the friends who have good boy pods.

ed255 · 2025-02-17T15:15:10Z

book/src/notes

@@ -0,0 +1,6 @@
+Ethdos(x, y, d) = OR ( EthdosBase(x, y, d), EthdosInd(x, y, d) )


Maybe this file was committed by mistake?

Yep, removed it

ed255 · 2025-02-17T15:17:34Z

book/src/customexample.md

+>
+
+On the backend, this is converted to a rule where all the arguments are either wildcards or literals:
+eth_friend(*1, *2, *3, *4) = and<


This is a very interesting example to discuss the topic of arities in custom predicates.
This custom predicate has:

The predicate has 4 arguments (that's what I was calling public in [Custom Statements] Custom Predicates with binary AND, OR #54)

The predicate has 5 wildcards

The predicate has 1 wildcard that doesn't come from a predicate argument (that's what I was calling private in [Custom Statements] Custom Predicates with binary AND, OR #54)

book/src/custom1.md

Co-authored-by: Eduard S. <[email protected]>

arnaucube · 2025-02-21T11:55:03Z

Since @ed255 is off for the next few weeks, is it ok @tideofwords if we merge this PR as a consolidation of the current spec that we're already implementing?
And when @ed255 comes back can check your answers and we can iterate if needed.

book/src/customexample.md

arnaucube · 2025-02-24T10:42:38Z

book/src/customexample.md

+```
+eth_friend(src_or, src_key, dst_or, dst_key) = and<
+    // there is an attestation pod that's a SIGNATURE POD
+    ValueOf(attestation_pod, "type", SIGNATURE)     


question, is the attestation_pod a 'private' argument? if so, should it need to be defined in some way at the predicate definition, something like
eth_friend(src_or, src_key, dst_or, dst_key, priv attestation_pod) = and<...?
(probably not with this syntax, but specifying somehow that the attestation_pod is an input to the template)

attestation_pod is an argument to the operation, but not an argument to the predicate.

In other words:
When you do the operation in-circuit, you need to provide attestation_pod as a witness.
But in the list of statements, when you have an eth_friend statement, you don't show the attestation_pod there.

oh I see, thanks!

tideofwords · 2025-02-24T15:09:57Z

Since @ed255 is off for the next few weeks, is it ok @tideofwords if we merge this PR as a consolidation of the current spec that we're already implementing? And when @ed255 comes back can check your answers and we can iterate if needed.

Yep, this is good

tideofwords and others added 9 commits February 6, 2025 14:19

Merge changes to docs

0cdb5e8

Fix typo

f6cf70c

Correct SUMMARY so it compiles; update .gitignore

02478c6

Clean up statements.md

d5c7bea

Make syntax and notation consistent with Rust source code.

Fix statements for Merkle trees and compound types

b9d8c58

First draft of custom statements and small updates to signedpod.md

5e203f7

Update book/src/merkletree.md

3e2498e

Co-authored-by: Ahmad Afuni <[email protected]>

merklestatements correct typo

a5afb20

Co-authored-by: Ahmad Afuni <[email protected]>

add todo for gadget ids

84fcdf4

Co-authored-by: Ahmad Afuni <[email protected]>

arnaucube added the deductions [tmp while we're specifying] deduction-related issues label Feb 12, 2025

tideofwords added 7 commits February 12, 2025 15:45

Merge branch 'main' into aard_custom

5d45c79

Separate out custom statements version 1

b6f98e9

More details on custom statements version 1

84e93ec

new file custom2

e498bb1

Partial draft of version 2

af56b90

First draft of version 2 spec, it's kind of a mess

46a569e

Another version of the custom predicates spec

1845724

ed255 reviewed Feb 17, 2025

View reviewed changes

ed255 mentioned this pull request Feb 18, 2025

Prototype custom predicates #74

Merged

Update book/src/custom2.md

6e55ed8

Co-authored-by: Eduard S. <[email protected]>

arnaucube added this to the Milestone 2 milestone Feb 19, 2025

tideofwords added 5 commits February 19, 2025 09:33

Simple example of deduction rule applied in circuit

b38c699

Implement Edu's comments on custom predicates

2aaa6f0

Backend predicates must be defined in groups

c7ab9bf

Add more examples

a88656a

Two diff statements using same constant

d85a216

arnaucube reviewed Feb 21, 2025

View reviewed changes

book/src/customexample.md Outdated Show resolved Hide resolved

arnaucube reviewed Feb 24, 2025

View reviewed changes

Remove deprecated example

97f012c

arnaucube approved these changes Feb 24, 2025

View reviewed changes

tideofwords merged commit d3bc892 into main Feb 24, 2025
4 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Aard custom #49

Aard custom #49

tideofwords commented Feb 10, 2025

ed255 Feb 17, 2025

tideofwords Feb 19, 2025

ed255 Feb 22, 2025

ed255 Feb 17, 2025

tideofwords Feb 19, 2025

ed255 Feb 17, 2025

tideofwords Feb 19, 2025

ed255 Feb 17, 2025

ed255 Feb 17, 2025

tideofwords Feb 19, 2025

ed255 Feb 17, 2025

tideofwords Feb 19, 2025

ed255 Feb 17, 2025

tideofwords Feb 19, 2025

ed255 Feb 17, 2025

arnaucube commented Feb 21, 2025

arnaucube Feb 24, 2025 •

edited

Loading

tideofwords Feb 24, 2025

arnaucube Feb 24, 2025

tideofwords commented Feb 24, 2025


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

		A custom predicate can be defined either _nonrecursively_ or _recursively_ (as part of a "batch"). A nonrecursive custom predicate is defined in terms of previously defined predicates (whether custom or native). A "batch" of custom predicates can be defined _recursively_: the definition of any custom predicate in the batch can use both previously defined predicates and all the predicates in the batch.


		## Custom predicates and their IDs

		A custom predicate, like a built-in predicate, is identified by a _name_ on the front end and an _identifier_ on the back end. In the non-recursive case, the back-end identifier is defined as a hash of the definition of the custom predicate.


		The definition of a custom predicate might also be called an _operation_ or _deduction rule_. It includes two (or, potentially, say, five) input statements. The arguments to the input statements are decomposed as (origin, key) pairs: if statements are allowed to have arity at most 4, then the input statements 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 input statement is either a wildcard or a literal. In the backend, the wildcard arguments will be identified as 1, 2, *3, ....

		@@ -0,0 +1,6 @@
		Ethdos(x, y, d) = OR ( EthdosBase(x, y, d), EthdosInd(x, y, d) )

Aard custom #49

Aard custom #49

Conversation

tideofwords commented Feb 10, 2025

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

arnaucube commented Feb 21, 2025

arnaucube Feb 24, 2025 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tideofwords commented Feb 24, 2025

arnaucube Feb 24, 2025 •

edited

Loading