Skip to content

Custom statements arguments can't be AnchoredKey #434

@ed255

Description

@ed255

Currently we can write this:

my_pred(d) = AND(
  Equal(d.foo, 1)
  Lt(d.bar, 100)
)

But I can't write this:

my_pred(d) = AND(
  Equal(d.foo, 1)
  Lt(d.bar, 100)
  my_other_pred(d.baz)
)

That's because arguments to custom statements can only be literals in the current implementation. That feels quite inconvenient.

The same happens with introduction statements.

What would be needed to support AnchoredKeys as arguments to custom statements?
Currently the circuit resolves 4 AnchoredKeys for each statement slot. This is because native predicates use up to 4 arguments (DictContains(new_root, old_root, key, value).
We would need to change that to Params::max_statement_args which is 5 in Params::default(). Then in the circuit that verifies custom predicate operations we could use the resolved AnchoredKeys.
Note that if we bump the number of resolved AnchoredKeys to 5 we could add a new argument to the DictionaryUpdate to include the old value which is currently missing.

The circuit cost of this is adding an extra AnchoredKey resolution for each statement slot that is unused most of the time

Metadata

Metadata

Assignees

No one assigned

    Labels

    backendTopics: Encoding, Arithmetic constraints, Verification, LayoutingenhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions