Invoking Predicates
If you've worked with imperative smart contract languages like Solidity
in the past, you know that interactions between smart contracts are essential for many applications.
One way to do this is by calling one contract from another contract. Pint has a similar concept
where one predicate can invoke another predicate with some arguments. We use the word "invoke"
here instead of "call" because, unlike imperative languages, predicates in Pint are not called in
the traditional sense since that would imply the existence of a control flow (a "call" followed by a
"return"). Instead, in Pint, predicate A
can invoke predicate B
with some arguments to indicate
that B
has to be present in the solution with this particular set of arguments, if A
is also
present in the solution. If this sounds confusing, don't worry. It will all be clear by the end of
this chapter.
We cover two types of predicate invocations:
- External predicate invocation.
- Sibling predicate invocation.
Invoking External Predicates
Similar to accessing external storage, a predicate in an external contract can be invoked through an
interface
declaration corresponding to the external contract. When invoking the external
predicate, the following are needed:
- The address of the external contract.
- The address of the predicate we want to access in that contract.
- A list of arguments.
Consider the following external smart contract that we would like interact with:
predicate foo(
x: int,
y: bool,
t: { int, bool },
) {
// predicate logic
}
// other predicates
To interact with this contract, we first need to generate its interface:
interface MyInterface {
predicate foo(
x: int,
y: bool,
t: { int, bool },
);
// other predicates
}
Now, we can invoke predicate foo
as follows:
const CONTRACT_ADDR = 0xEB87FCE275A9AB10996D212F39221A56B90E01C37FA9D16EE04A3FE8E17DEED9;
const FOO_ADDR = 0xBA6595C5C75346E6C82BED0CE770D0758ADD1712163FCE45E38E5E8EAC6AA153;
predicate bar(
a: int,
b: bool,
) {
let tuple = { 42, b };
constraint MyInterface[[CONTRACT_ADDR]]::foo[[FOO_ADDR]](a, true, tuple);
}
The predicate invocation expression has three parts separated by ::
:
- The name of the interface
MyInterface
followed by the address of the corresponding deployed contract in between[[..]]
. This is quite similar to what we had to do to access external storage variables. - The name of the predicate
foo
followed by the address of the corresponding predicate in the deployed contract. - A list of arguments that must match the list parameters of
foo
in theinterface
.
In the above, the constraint:
constraint MyInterface[[CONTRACT_ADDR]]::foo[[FOO_ADDR]](a, true, tuple);
can be interpreted as follows: any solution that solves predicate bar
must also contain a solution
for predicate foo
such that:
- The address of
foo
isFOO_ADDR
. - The address of the contract that contains
foo
isCONTRACT_ADDR
. - The arguments provided for
foo
in the solution are equal toa
,true
, andtuple
respectively.
Of course, for foo
to be actually satisfied, the containing contract must exist and be deployed,
the addresses must be correct, and the arguments must match (in number and types) what the deployed
bytecode of foo
actually expects.
Invoking Sibling Predicates
A special case for invoking predicates is when the invoked predicate is in the same contract as the predicate that is invoking it. There is no conceptual difference between this special case and the generalized case above expect that, because we are working in the same contract, there is no need to declare an interface for the contract. There is also no need to specify the address of the invoked predicate because the compiler can figure that out on its own! Here's an example:
predicate A(
a: { bool, int },
b: bool,
c: int[3],
) {
// predicate logic
}
predicate B() {
constraint A[[]]( { true, 42 }, false, [1, 2, 3]);
}
Here, predicate B
invokes sibling predicate A
by using its path (just A
) and empty square
brackets [[]]
to indicate that the address is to be computed by the compiler. The constraint
constraint A[[]](..)
should be interpreted exactly as in the case of external predicate
invocation: any solution that solves B
should also contain a solution for A
with the provided
listed arguments.
One important caveat of the above is that you are not allowed to have cyclical dependencies between predicates. For example:
predicate A(x: int) {
constraint B[[]](0);
}
predicate B(y: int) {
constraint A[[]](0);
}
Here, predicate A
invokes predicate B
and predicate B
invokes predicate A
. This causes a
cycle where the address of a predicate cannot be determined and used by the other. The compiler will
emit the following error to prevent you from proceeding:
Error: dependency cycle detected between predicates
╭─[invoking_predicates_3.pnt:1:1]
│
1 │ predicate A(x: int) {
│ ─────┬─────
│ ╰─────── this predicate is on the dependency cycle
│
7 │ predicate B(y: int) {
│ ─────┬─────
│ ╰─────── this predicate is on the dependency cycle
│
│ Note: dependency between predicates is typically created via predicate instances
───╯
Another caveat is that a predicate cannot reference itself:
predicate C(x: int) {
constraint C[[]](x);
}
The compiler will complain as follows:
Error: self referential predicate `::C`
╭─[invoking_predicates_4.pnt:2:16]
│
2 │ constraint C[[]](x);
│ ────┬───
│ ╰───── this predicate call references the predicate it's declared in
───╯