mirror of
https://github.com/ProvableHQ/leo.git
synced 2024-10-26 07:00:35 +03:00
[RFC] Add an RFC for const functions.
The purpose of this RFC is to: - Provide user documentation for this feature in a more accessible way than in the text for https://github.com/AleoHQ/leo/pull/1410, particularly after that PR is closed. - Record the discussion in a recent meeting about broadening the notion of const function to map const arguments to const results rather than requiring const arguments, as a possible future extension.
This commit is contained in:
parent
2a7298b873
commit
ae26d4c7d4
119
docs/rfc/013-const-functions.md
Normal file
119
docs/rfc/013-const-functions.md
Normal file
@ -0,0 +1,119 @@
|
||||
# Leo RFC 013: Constant Functions
|
||||
|
||||
## Author(s)
|
||||
|
||||
The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
IMPLEMENTED
|
||||
|
||||
## Summary
|
||||
|
||||
This RFC proposes the additional of an optional `const` modifier to function declarations
|
||||
to explicitly designate functions that return constant values that can be calculated at compile time.
|
||||
|
||||
## Motivation
|
||||
|
||||
Explicitly designating constant functions makes user intention explicit
|
||||
and simplifies the Leo compiler's checks, as explained below.
|
||||
|
||||
## Background
|
||||
|
||||
Leo code is partially evaluated on its `const` inputs prior to being translated to R1CS.
|
||||
A function that returns a value that only depends on `const` inputs directly or indirectly,
|
||||
can be partially evaluated away, without having to be inlined during flattening.
|
||||
|
||||
## Design
|
||||
|
||||
### Syntax
|
||||
|
||||
The ABNF grammar is extended by adding an optional `const` modifier to function declarations:
|
||||
```
|
||||
function-declaration = *annotation [ %s"const" ] %s"function" identifier
|
||||
"(" [ function-parameters ] ")" [ "->" type ]
|
||||
block
|
||||
```
|
||||
|
||||
This applies to both top-level and member functions.
|
||||
|
||||
### Static Semantics
|
||||
|
||||
A `const` function declaration must satisfy the following conditions:
|
||||
* All its parameters are `const`, including the `self` parameter for instance circuit member functions.
|
||||
* The body does not reference the special `input` variable.
|
||||
* The body only calls other `const` functions.
|
||||
|
||||
### Dynamic Semantics
|
||||
|
||||
This has no impact on the dynamic semantics of Leo, viewed as a traditional programming language.
|
||||
|
||||
### Flattening
|
||||
|
||||
Given that `const` expressions are evaluated completely during flattening,
|
||||
the values of the arguments of a `const` function call are known during flattening,
|
||||
and therefore the function call can be completely evaluated as well.
|
||||
|
||||
If the function is recursive (individually or with others),
|
||||
the evaluation involves the bounded recursion analysis described in a separate RFC.
|
||||
|
||||
### Implementation Considerations
|
||||
|
||||
ASTs for function declarations are extended with a boolean flag `const_`.
|
||||
|
||||
If a `const` function has a non-`const` parameter,
|
||||
an AST error occurs.
|
||||
|
||||
If the body of a `const` function references the `input` variable or calls a non-`const` function,
|
||||
an ASG error occurs.
|
||||
|
||||
The description of static semantics, dynamic semantics, and flattening given above
|
||||
are expressed in terms of Leo, because that is the user's view of the language.
|
||||
In the implementation, flattening occurs after the Leo code is translated to the IR.
|
||||
|
||||
### Examples
|
||||
|
||||
```ts
|
||||
const function len(const arr: [u8; _]) -> u32 {
|
||||
return arr.len();
|
||||
}
|
||||
|
||||
circuit Sample {
|
||||
x: [char; 5]
|
||||
const function say_hi(const self) -> [char; 5] {
|
||||
return self.x;
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
## Drawbacks
|
||||
|
||||
This extension does not appear to bring any drawbacks.
|
||||
|
||||
## Effect on Ecosystem
|
||||
|
||||
None.
|
||||
|
||||
## Alternatives
|
||||
|
||||
### No Constant Designation
|
||||
|
||||
Without an explicit designation of constant functions,
|
||||
the Leo compiler needs to perform an inter-procedural analysis:
|
||||
if `f` calls `g`, in order for `f` to be constant, also `g` must be constant.
|
||||
In other words, the call graph must be taken into account.
|
||||
|
||||
In contrast, with the `const` designation,
|
||||
an intra-procedural analysis suffices,
|
||||
as discussed in the static semantics section above.
|
||||
|
||||
## Future Extensions
|
||||
|
||||
In other languages like Rust, `const` functions are not required to have all constant parameters.
|
||||
They are just required to return constant results for constant arguments,
|
||||
i.e. they must not access global variables and they must only call other `const` functions.
|
||||
In other words, these `const` functions are polymorphic over "constancy".
|
||||
|
||||
This could be also realized in Leo, because type inference/checking determines `const` and non-`const` expressions.
|
||||
This tells the compiler which function calls have all `const` arguments and which ones do not.
|
||||
Therefore, the compiler can selectively evaluate, during flattening, only the calls of `const` functions on `const` arguments.
|
Loading…
Reference in New Issue
Block a user