Static-semantics
Static semantics of Leo.
The static semantics of Leo defines
the requirements that must be satisfied
by the constructs defined in the abstract syntax in order for the Leo code
to execute without certain kinds of errors
(such as accessing variables not in scope,
applying operators to operands of the wrong types,
and so on)
and to be flattened to zero-knowledge circuits.
The static semantics is formalized via
predicates to check that the constructs satisfy the requirements.
Subtopics
- Type-checking
- Type checking of Leo.
- Static-environments
- Static environments of Leo.
- Curve-parameterization
- Curve parameterization in Leo.
- Function-recursion
- Function recursion checks in Leo.
- Struct-recursion
- Struct type recursion checks in Leo.
- Input-checking
- Static checks on input files.
- Program-checking
- Static checks on Leo programs.
- Type-maps-for-struct-components
- Maps from identifiers to types
for struct type components.
- Program-and-input-checking
- Static checks on Leo programs and inputs.
- Output-checking
- Static checks on output files.
