[RFC] Use header levels consistent with (new) template.

This commit is contained in:
Alessandro Coglio 2021-09-30 09:55:52 -07:00
parent 43c1b29a52
commit d633f93f6f

View File

@ -8,7 +8,7 @@ The Aleo Team.
FINAL
# Summary
## Summary
This proposal provides support for recursion in Leo,
via a user-configurable limit to the allowed depth of the recursion.
@ -26,7 +26,7 @@ User-configurable limits may be also appropriate for
other compiler transformations that are known to terminate
but could result in a very large number of R1CS constraints.
# Motivation
## Motivation
Leo currently allows functions to call other functions,
but recursion is disallowed:
@ -34,9 +34,9 @@ a function cannot call itself, directly or indirectly.
However, recursion is a natural programming idiom in some cases,
compared to iteration (i.e. loops).
# Background
## Background
## Function Inlining
### Function Inlining
Since R1CS are flat collections of constraints,
compiling Leo to R1CS involves _flattening_ the Leo code:
@ -71,7 +71,7 @@ function main(a: u32) -> u32 {
}
```
## Constants and Variables
### Constants and Variables
A Leo program has two kinds of inputs: constants and variables;
both come from input files (which represent blockchain records).
@ -125,7 +125,7 @@ it is the case that, due to the aforementioned partial evaluation,
the `const` arguments of function calls have known values
when the flattening transformations are carried out.
# Design
## Design
After exemplifying how inlining of recursive functions may terminate or not,
we discuss our approach to avoid non-termination.
@ -133,7 +133,7 @@ Then we discuss future optimizations,
and how the approach to avoid non-termination of recursion
may be used for other features of the Leo language.
## Inlining Recursive Functions
### Inlining Recursive Functions
In the presence of recursion,
attempting to exhaustively inline function calls does not terminate in general.
@ -340,7 +340,7 @@ function main() {
...
```
## Configurable Limit
### Configurable Limit
Our proposed approach to avoid non-termination
when inlining recursive functions is to
@ -388,7 +388,7 @@ as discussed later.
In Aleo Studio, this compiler option is presumably specified
via GUI preferences and build configurations.
## Circularity Detection
### Circularity Detection
Besides the depth of the inlining call stack,
the compiler could also keep track of
@ -401,7 +401,7 @@ and the compiler can show to the user the trace of circular calls.
This approach would readily reject the `forever` example given earlier.
## Termination Analysis
### Termination Analysis
In general, a recursive function
(a generic kind of function, not necessarily a Leo function)
@ -460,7 +460,7 @@ If the recognition fails,
the compiler falls back to inlining until
either inlining terminates or the limit is reached.
## Application to Loops
### Application to Loops
Loops are conceptually not different from recursion.
Loops and recursion are two ways to repeat computations,
@ -483,7 +483,7 @@ which in particular would readily recognize
the currently allowed loop forms to terminate.
All of this should be the topic of a separate RFC.
## Application to Potentially Slow Transformations
### Application to Potentially Slow Transformations
Some flattening transformations in the Leo compiler are known to terminate,
but they may take an excessively long time to do so.
@ -496,18 +496,18 @@ not only for flattening transformations that may not otherwise terminate,
but also for ones that may take a long time to do so.
This is a broader topic that should be discussed in a separate RFC.
# Drawbacks
## Drawbacks
This proposal does not appear to bring any real drawbacks,
other than making the compiler inevitably more complex.
But the benefits to support recursion justifies the extra complexity.
# Effect on Ecosystem
## Effect on Ecosystem
This proposal does not appear to have any direct effects on the ecosystem.
It simply enables certain Leo programs to be written in a more natural style.
# Alternatives
## Alternatives
An alternative approach, hinted at in the above discussion about loops,
is to take a similar approach to the current one for loops.