mirror of
https://github.com/ProvableHQ/leo.git
synced 2024-09-19 17:57:40 +03:00
Merge branch 'master' into leo-wasm
This commit is contained in:
commit
e42a3186a0
@ -57,6 +57,11 @@ pub fn evaluate_eq<'a, F: PrimeField, G: GroupType<F>, CS: ConstraintSystem<F>>(
|
||||
}
|
||||
(ConstrainedValue::Array(arr_1), ConstrainedValue::Array(arr_2)) => {
|
||||
let mut current = ConstrainedValue::Boolean(Boolean::constant(true));
|
||||
|
||||
if arr_1.len() != arr_2.len() {
|
||||
return Err(CompilerError::array_sizes_must_match_in_eq(arr_1.len(), arr_2.len(), span).into());
|
||||
}
|
||||
|
||||
for (i, (left, right)) in arr_1.into_iter().zip(arr_2.into_iter()).enumerate() {
|
||||
let next = evaluate_eq(&mut cs.ns(|| format!("array[{}]", i)), left, right, span)?;
|
||||
|
||||
|
@ -6,7 +6,7 @@ The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
FINAL
|
||||
IMPLEMENTED
|
||||
|
||||
# Summary
|
||||
|
||||
|
@ -6,7 +6,7 @@ The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
DRAFT
|
||||
IMPLEMENTED
|
||||
|
||||
# Summary
|
||||
|
||||
@ -149,3 +149,7 @@ None.
|
||||
# Alternatives
|
||||
|
||||
None.
|
||||
|
||||
# Implementation Decisions
|
||||
|
||||
For the length of an array, we decided on `<expression>.len()`, where `<expression>` is any expression of array type.
|
||||
|
@ -6,7 +6,7 @@ The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
DRAFT
|
||||
IMPLEMENTED
|
||||
|
||||
# Summary
|
||||
|
||||
|
@ -6,7 +6,7 @@ The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
DRAFT
|
||||
IMPLEMENTED
|
||||
|
||||
## Summary
|
||||
|
||||
|
@ -6,7 +6,7 @@ The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
DRAFT
|
||||
FINAL
|
||||
|
||||
# Summary
|
||||
|
||||
|
@ -6,15 +6,15 @@ The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
DRAFT
|
||||
FINAL
|
||||
|
||||
## Summary
|
||||
|
||||
This RFC proposes two things:
|
||||
This RFC proposes three things:
|
||||
|
||||
1. The scalar types in Leo (integers, fields, etc.) can have static methods.
|
||||
2. The scalar types in Leo (integers, fields, etc.) can have static constants.
|
||||
3. Those values that have a scalar type can have methods directly on them.
|
||||
3. Expressions of scalar type can have instance methods called on them.
|
||||
|
||||
## Motivation
|
||||
|
||||
@ -29,23 +29,20 @@ Firstly we would have to modify both the ABNF and parsing of Leo to allow static
|
||||
The ABNF would look as follows:
|
||||
|
||||
```abnf
|
||||
; This is an existing old rule
|
||||
; This is an existing old rule.
|
||||
scalar-type = boolean-type / arithmetic-type / address-type / character-type
|
||||
|
||||
; This is an existing old rule
|
||||
circuit-type = identifier / self-type
|
||||
|
||||
; Add this rule.
|
||||
named-type = circuit-type / scalar-type ; new rule
|
||||
named-type = identifier / self-type / scalar-type
|
||||
|
||||
; Modify this rule:
|
||||
; Modify this rule.
|
||||
postfix-expression = primary-expression
|
||||
/ postfix-expression "." natural
|
||||
/ postfix-expression "." identifier
|
||||
/ identifier function-arguments
|
||||
/ postfix-expression "." identifier function-arguments
|
||||
/ named-type "::" identifier function-arguments ; this used to be a circuit-type
|
||||
/ named-type "::" identifier ; this is new to allow static members on
|
||||
/ named-type "::" identifier function-arguments ; this used to be identifier-or-self-type
|
||||
/ named-type "::" identifier ; this is new to allow member constants
|
||||
/ postfix-expression "[" expression "]"
|
||||
/ postfix-expression "[" [expression] ".." [expression] "]"
|
||||
```
|
||||
|
284
docs/rfc/012-record-transaction-model.md
Normal file
284
docs/rfc/012-record-transaction-model.md
Normal file
@ -0,0 +1,284 @@
|
||||
# Leo RFC 012: Record and Transaction Model
|
||||
|
||||
## Authors
|
||||
|
||||
The Aleo Team.
|
||||
|
||||
## Status
|
||||
|
||||
DRAFT
|
||||
|
||||
## Summary
|
||||
|
||||
This RFC describes how Leo programs interact with the Aleo blockchain.
|
||||
The description is oriented to the Leo developer:
|
||||
it does not describe the zero-knowledge details,
|
||||
as the whole purpose of Leo is to enable developers
|
||||
to write applications with only a very high-level understanding of zero-knowledge.
|
||||
|
||||
## Motivation
|
||||
|
||||
While Leo can be described as a regular programming language
|
||||
(albeit with certain non-standard restrictions motivated by its compilation to zero-knowledge circuits),
|
||||
its purpose is to build applications for the Aleo blockchain.
|
||||
It is thus important to describe precisely how Leo programs operate in the Aleo blockchain.
|
||||
|
||||
## Design
|
||||
|
||||
### Zexe
|
||||
|
||||
The Aleo blockchain follows the Zexe model, with some variations.
|
||||
It is thus useful to briefly review some aspects of Zexe first.
|
||||
|
||||
In Zexe, there are _records_ that contain application-specific data,
|
||||
and _transactions_ that consume _n_ old records and produce _m_ new records.
|
||||
The computation of the new records from the old records
|
||||
is arbitrary and unknown to the blockchain;
|
||||
the blockchain only enforces that the old records satisfy known _death predicates_
|
||||
and that the new records satisfy known _birth predicates_.
|
||||
|
||||
### Aleo Blockchain
|
||||
|
||||
In the Aleo blockchain, a transaction always consumes 2 old records and produces 2 new records.
|
||||
That is, _n_ = 2 and _m_ = 2 with respect to the Zexe model.
|
||||
Other choices are possible, and may be supported in the future;
|
||||
the current choice of 2 old and 2 new records is motivated by
|
||||
being the minimum to represent certain computations of interest, such as token exchanges,
|
||||
which may involve records owned by different parties
|
||||
(and therefore need to consume more than one record, since each record has a unique owner).
|
||||
|
||||
One or both of the old records may be dummy,
|
||||
if only one old actual record is desired,
|
||||
or if new records are to be created "from nothing".
|
||||
One or both of the new records may be dummy,
|
||||
if only one new actual record is desired,
|
||||
or if old records just have to be consumed.
|
||||
|
||||
Aleo records and transactions have a well-defined structure.
|
||||
They are ordered collections of typed slots.
|
||||
Of particular interest is the _payload_ slot,
|
||||
which contains a fixed number of bytes (currently 128)
|
||||
to store application-specific data.
|
||||
(Note that the developer documentation is out of date at the time of this writing.)
|
||||
|
||||
In the Aleo blockchain, unlike Zexe, there is no separation among
|
||||
computation of new records from old records, death predicates, and birth predicates.
|
||||
Instead, a Leo program plays the role of all three, as described below.
|
||||
|
||||
### Current Leo Program Execution Model
|
||||
|
||||
A Leo program is a collection of files,
|
||||
with `file` as defined in the ABNF grammar,
|
||||
i.e. as a sequence of declarations.
|
||||
A Leo program has one main file,
|
||||
which may contain import declarations,
|
||||
which resolve to other files,
|
||||
which may in turn contain import declarations,
|
||||
and so on until a closed set of files is obtained:
|
||||
that (linked) set of files is the _program_.
|
||||
|
||||
In order to be used in the Aleo blockchain,
|
||||
a Leo program must include a function called `main`, in its aforementioned main file.
|
||||
The processing of a transaction corresponds to an invocation of this `main` function.
|
||||
The word 'corresponds' in the preceding sentence is important:
|
||||
unlike other blockchains like Ethereum,
|
||||
the processing of the transaction does not involve executing the Leo code;
|
||||
rather, it involves checking a zero-knowledge proof
|
||||
of the execution of the Leo program,
|
||||
which was prepared when the Leo program was compiled.
|
||||
This is what 'corresponds' means, in that sentence.
|
||||
However, for the high-level purpose of this RFC, these are zero-knowledge details.
|
||||
|
||||
In general, the `main` function takes some `const` and some non-`const` inputs (declared as parameters),
|
||||
and returns an output (declared as a return type), which may be a tuple to effectively represent multiple outputs.
|
||||
The `const` inputs are compiled into the zero-knowledge circuit,
|
||||
so they can be ignored for our purpose here,
|
||||
leaving the non-`const` inputs and the output for consideration.
|
||||
|
||||
The execution of `main` can be described as a mathematical function
|
||||
```
|
||||
main : Record x Record x Inputs -> Record x Record x Output
|
||||
```
|
||||
where `x` is cartesian product,
|
||||
`Record` is the set of possible records,
|
||||
`Inputs` is the set of possible inputs to `main`, and
|
||||
`Output` is the set of possible outputs from `main`.
|
||||
(These sets can be thought as "types", but mathematically we talk about sets.)
|
||||
That is, this mathematical function
|
||||
takes three inputs (the two old records and the `main` inputs)
|
||||
and returns three outputs (the two new records and the `main` output).
|
||||
While `Record` is fixed, i.e. it is the same for all Leo programs,
|
||||
both `Inputs` and `Output` differ based on the Leo input and output types of `main`.
|
||||
|
||||
In the Leo code, in `main` or in functions called by `main`,
|
||||
the values in `Inputs` are accessed via the `main` parameters,
|
||||
while the old records are accessed via the special `input` variable,
|
||||
which provides access to the two old records and their slots,
|
||||
including the payloads that contain application-specific data.
|
||||
The picture for new records and values in `Output` is less clear from the documentation:
|
||||
experimentation suggests that the new records are obtained
|
||||
by serializing the output value in `Output` (which, recall, may be a tuple).
|
||||
|
||||
It is important to note that the values in `Inputs` do not come from the two old records.
|
||||
Rather, they are private inputs, supplied by the developer
|
||||
when they compile the Leo program and generate the zero-knowledge proof.
|
||||
Indeed, as mentioned above, the processing of the transaction in the blockchain
|
||||
does not execute the Leo code, and thus does not need to know the values in `Inputs`.
|
||||
Rather, the blockchain has to verify a zero-knowledge proof asserting that
|
||||
there exist values in `Input`, known to the creator of the transaction,
|
||||
such that the execution of the Leo program's `main`
|
||||
on those values and on the old records
|
||||
yields the new records, along with some value in `Output`;
|
||||
this is, roughly speaking, the assertion proved in zero-knowledge.
|
||||
|
||||
### Proposed Leo Program Execution Model
|
||||
|
||||
The current model described above seems adequate overall, but we need to:
|
||||
1. Clarify how Leo code reads old records and writes new records.
|
||||
2. Generalize from one entry point (i.e. the `main` function) to multiple entry points, in line with the smart contract paradigm.
|
||||
|
||||
Generalizing from one `main` entry point to multiple ones is conceptually easy.
|
||||
It means that, instead of implicitly designating `main` as the only entry point,
|
||||
we need a mechanism to explicitly designate one or more Leo functions as entry points.
|
||||
|
||||
A simple approach could be to use an annotation like `@entrypoint` to designate _entry point functions_:
|
||||
```
|
||||
@entrypoint
|
||||
function mint(...) -> ... { ... }
|
||||
|
||||
@entrypoint
|
||||
function transfer(...) -> ... { ... }
|
||||
```
|
||||
This has a precedent, in the use of `@test` to designate Leo test functions that are not compiled to circuits.
|
||||
|
||||
Another approach is to use a keyword, e.g.
|
||||
```
|
||||
entrypoint function mint(...) -> ... { ... }
|
||||
|
||||
entrypoint function transfer(...) -> ... { ... }
|
||||
```
|
||||
Yet another approach is to group entrypoint functions inside a new block construct, e.g.
|
||||
```
|
||||
entrypoint {
|
||||
|
||||
function mint(...) -> ... { ... }
|
||||
|
||||
function transfer(...) -> ... { ... }
|
||||
}
|
||||
```
|
||||
|
||||
Now let us turn to the issue of clarifying how the Leo code reads old records and writes new records.
|
||||
|
||||
Given that records have a fixed structure with typed slots,
|
||||
their format could be described by a Leo circuit type,
|
||||
whose member variables correspond to the slots.
|
||||
The types of the slots would be fairly low-level,
|
||||
i.e. byte arrays (e.g. `u8[128]` for the payload)
|
||||
and unsigned integers (e.g. `u64` for the balance),
|
||||
because they must have a clear correspondence with the serialized form of records.
|
||||
This means that the Leo code may have to do
|
||||
its own deserialization of the payload bytes into higher-level Leo values;
|
||||
standard serialization/deserialization libraries for Leo types may be provided for this,
|
||||
as an independent and more generally useful feature.
|
||||
|
||||
It may make sense to have a circuit type for the special `input` variable,
|
||||
which includes two slots for the two old records.
|
||||
All these circuit types should be explicitly documented,
|
||||
and available to the Leo program.
|
||||
|
||||
However, we probably want `input` to be read-only,
|
||||
i.e. disallow assigning to an old record slot.
|
||||
Designating `input` as `const` does not seem right,
|
||||
as that designation normally means that it is compiled into the circuit.
|
||||
Instead, we could provide read-only access via member function (e.g. `payload()`, `balance()`),
|
||||
but we still have to prohibit assignments to member variables (which is currently allowed on any circuit type).
|
||||
As an orthogonal and more generally useful feature,
|
||||
we could consider adding public/private access designations to Leo circuit members.
|
||||
Another approach is to avoid exposing the member variables,
|
||||
and just make the member functions available via an implicit import declaration.
|
||||
All of this needs to be thought through more carefully, in the broader context of the Leo language design;
|
||||
in any case, it should be clear that this can be made to work in some way,
|
||||
and that Leo programs can access the old records through the special `input` variables.
|
||||
|
||||
One issue with the special `input` variable is whether it should be treated as a built-in global variable,
|
||||
or whether it should be explicitly passed to the entry point functions and to the non-entry-point functions called by them.
|
||||
The first approach is more concise, while the second approach is more explicit.
|
||||
Note that, in the second approach, we may want to enforce certain restrictions on the use of `input`,
|
||||
e.g. we may not want to allow a call `f(input, input)` even if the parameters of `f` both have the same circuit type as `input`.
|
||||
There is nothing inherently wrong with `f(input, input)`, i.e. with handling `input` by value,
|
||||
except that perhaps `input` is a relatively large structure,
|
||||
and duplicating it generates a (relatively) large number of R1CS constraints.
|
||||
Another idea is to pass `input` by (immutable) reference behind the scenes,
|
||||
analogously to how we pass `self` by mutable reference to functions with `mut self`.
|
||||
|
||||
The treatment of output records is less clear at this point.
|
||||
As mentioned above, experimentation suggests that currently the output values of `main` are serialized into new records.
|
||||
This is not "symmetric" with the treatment of input records.
|
||||
It may be preferable to require the Leo code to perform its own serialization of high-level data to output records,
|
||||
which would often be the inverse of the deserialization from input records.
|
||||
We could consider, for symmetry, to add a special `output` variable,
|
||||
also with a known circuit type,
|
||||
which contains (at least some of) the data in the output records, most notably the two payloads.
|
||||
(It may not contain all the data of the record because some slots
|
||||
have to be computed by the underlying zero-knowledge mechanisms,
|
||||
outside of the Leo code.)
|
||||
This `output` variable would have to be read/write, unlike `input`.
|
||||
Similarly to `input`, it could be either a built-in global variable
|
||||
or passed around functions by reference, in a single-threaded way.
|
||||
The single-threadedness is a more important requirement here,
|
||||
since the variable is read/write,
|
||||
i.e. it needs to be treated like a global variable,
|
||||
in the sense that there is a single instance of it.
|
||||
|
||||
If we go the `output` variable route, a question is what happens with the outputs of the entry point functions
|
||||
(i.e. the values in `Output`, in the mathematical function described earlier).
|
||||
If all the output data is explicitly written into the output record by the Leo code,
|
||||
then perhaps the Leo entry point functions should always return `()`, i.e. "nothing",
|
||||
or perhaps they should be predicates, i.e. return `bool`,
|
||||
where `true` indicates a successful check (e.g. "yes, this private input yields this commitment when hashed")
|
||||
and `false` indicates a failed check.
|
||||
|
||||
Another possibility is to require entry point functions to return records as outputs.
|
||||
More precisely, these may be smaller structures than records,
|
||||
because some of the slots of the records may only be calculated outside of Leo,
|
||||
but for the present discussion we will assume that Leo can calculate the whole records.
|
||||
As mentioned earlier, a transaction may generate 0, 1, or 2 new records.
|
||||
Correspondingly, we could require entry point functions to return results of one of the following types:
|
||||
```
|
||||
@entrypoint function ...(...) -> () // when no new records are created
|
||||
@entrypoint function ...(...) -> Record // when one new record is created
|
||||
@entrypoint function ...(...) -> (Record, Record) // when two new records are created
|
||||
// using an annotation for concreteness, but the point stands for the other options discussed
|
||||
```
|
||||
In other words, an entry point function can be now seen as a mathematical function
|
||||
```
|
||||
entrypoint : Record x Record x Inputs -> Record x Record
|
||||
```
|
||||
where one or both output records are dummy if the function creates less than two new records.
|
||||
|
||||
The above constrains each entry point to always return the same number of records.
|
||||
Different entry point functions may return different numbers of records.
|
||||
If we want the same entry point function
|
||||
to return different numbers of records in different situations,
|
||||
then it could make sense to have a more general circuit type for the output of a transaction,
|
||||
which may contain 0, 1, or 2 records, and possibly other information as needed,
|
||||
and require entry point functions to uniformly return values of that type:
|
||||
```
|
||||
@entrypoint function ...(...) -> TransactionOutput // contains 0, 1, or 2 records
|
||||
```
|
||||
|
||||
Earlier we discussed having a known and accessible circuit type for the `input` special variable.
|
||||
This type could be called `TransactionInput`, which mirrors `TransactionOutput`.
|
||||
In this case, it seems more natural to treat `input` not as a global variable,
|
||||
but as a parameter of entry functions;
|
||||
it could be the first parameter, required for every entry function that accesses the transaction input:
|
||||
```
|
||||
@entrypoint function ...(input: TransactionInput, ...) -> TransactionOutput
|
||||
```
|
||||
We could even drop `input` as a special keyword/expression altogether,
|
||||
and allow any name (but suggest a convention) for the `TransactionInput` parameter of entry point functions.
|
||||
|
||||
## Alternatives
|
||||
|
||||
The 'Design' section above already outlines several alternatives to consider.
|
||||
Once we make some specific choices, we can move the other options to this section.
|
@ -163,7 +163,7 @@ create_errors!(
|
||||
help: None,
|
||||
}
|
||||
|
||||
/// For when the operation has no implmentation on the type of variable received.
|
||||
/// For when the operation has no implementation on the type of variable received.
|
||||
@formatted
|
||||
incompatible_types {
|
||||
args: (operation: impl Display),
|
||||
@ -841,4 +841,11 @@ create_errors!(
|
||||
msg: "len() can only be called on an array value".to_string(),
|
||||
help: None,
|
||||
}
|
||||
|
||||
@formatted
|
||||
array_sizes_must_match_in_eq {
|
||||
args: (lhs: impl Display, rhs: impl Display),
|
||||
msg: format!("array sizes must match for comparison; left: {}, right: {}", lhs, rhs),
|
||||
help: None,
|
||||
}
|
||||
);
|
||||
|
@ -466,7 +466,7 @@ described above.
|
||||
newline = line-feed / carriage-return / carriage-return line-feed
|
||||
```
|
||||
|
||||
Go to: _[line-feed](#user-content-line-feed), [carriage-return](#user-content-carriage-return)_;
|
||||
Go to: _[carriage-return](#user-content-carriage-return), [line-feed](#user-content-line-feed)_;
|
||||
|
||||
|
||||
Line terminators form whitespace, along with spaces and horizontal tabs.
|
||||
@ -476,7 +476,7 @@ Line terminators form whitespace, along with spaces and horizontal tabs.
|
||||
whitespace = space / horizontal-tab / newline
|
||||
```
|
||||
|
||||
Go to: _[newline](#user-content-newline), [horizontal-tab](#user-content-horizontal-tab), [space](#user-content-space)_;
|
||||
Go to: _[space](#user-content-space), [newline](#user-content-newline), [horizontal-tab](#user-content-horizontal-tab)_;
|
||||
|
||||
|
||||
There are two kinds of comments in Leo, as in other languages.
|
||||
@ -564,7 +564,6 @@ keyword = %s"address"
|
||||
/ %s"Self"
|
||||
/ %s"self"
|
||||
/ %s"static"
|
||||
/ %s"string"
|
||||
/ %s"type"
|
||||
/ %s"u8"
|
||||
/ %s"u16"
|
||||
@ -590,7 +589,7 @@ lowercase-letter = %x61-7A ; a-z
|
||||
letter = uppercase-letter / lowercase-letter
|
||||
```
|
||||
|
||||
Go to: _[uppercase-letter](#user-content-uppercase-letter), [lowercase-letter](#user-content-lowercase-letter)_;
|
||||
Go to: _[lowercase-letter](#user-content-lowercase-letter), [uppercase-letter](#user-content-uppercase-letter)_;
|
||||
|
||||
|
||||
The following rules defines (ASCII) decimal, octal, and hexadecimal digits.
|
||||
@ -763,7 +762,7 @@ and Unicode escapes with one to six hexadecimal digits
|
||||
character-literal = single-quote character-literal-element single-quote
|
||||
```
|
||||
|
||||
Go to: _[single-quote](#user-content-single-quote), [character-literal-element](#user-content-character-literal-element)_;
|
||||
Go to: _[character-literal-element](#user-content-character-literal-element), [single-quote](#user-content-single-quote)_;
|
||||
|
||||
|
||||
<a name="character-literal-element"></a>
|
||||
@ -774,7 +773,7 @@ character-literal-element = not-single-quote-or-backslash
|
||||
/ unicode-character-escape
|
||||
```
|
||||
|
||||
Go to: _[simple-character-escape](#user-content-simple-character-escape), [unicode-character-escape](#user-content-unicode-character-escape), [not-single-quote-or-backslash](#user-content-not-single-quote-or-backslash), [ascii-character-escape](#user-content-ascii-character-escape)_;
|
||||
Go to: _[simple-character-escape](#user-content-simple-character-escape), [not-single-quote-or-backslash](#user-content-not-single-quote-or-backslash), [ascii-character-escape](#user-content-ascii-character-escape), [unicode-character-escape](#user-content-unicode-character-escape)_;
|
||||
|
||||
|
||||
<a name="single-quote-escape"></a>
|
||||
@ -829,7 +828,7 @@ simple-character-escape = single-quote-escape
|
||||
/ null-character-escape
|
||||
```
|
||||
|
||||
Go to: _[carriage-return-escape](#user-content-carriage-return-escape), [backslash-escape](#user-content-backslash-escape), [line-feed-escape](#user-content-line-feed-escape), [horizontal-tab-escape](#user-content-horizontal-tab-escape), [null-character-escape](#user-content-null-character-escape), [single-quote-escape](#user-content-single-quote-escape), [double-quote-escape](#user-content-double-quote-escape)_;
|
||||
Go to: _[single-quote-escape](#user-content-single-quote-escape), [null-character-escape](#user-content-null-character-escape), [line-feed-escape](#user-content-line-feed-escape), [carriage-return-escape](#user-content-carriage-return-escape), [double-quote-escape](#user-content-double-quote-escape), [horizontal-tab-escape](#user-content-horizontal-tab-escape), [backslash-escape](#user-content-backslash-escape)_;
|
||||
|
||||
|
||||
<a name="ascii-character-escape"></a>
|
||||
@ -837,7 +836,7 @@ Go to: _[carriage-return-escape](#user-content-carriage-return-escape), [backsla
|
||||
ascii-character-escape = %s"\x" octal-digit hexadecimal-digit
|
||||
```
|
||||
|
||||
Go to: _[octal-digit](#user-content-octal-digit), [hexadecimal-digit](#user-content-hexadecimal-digit)_;
|
||||
Go to: _[hexadecimal-digit](#user-content-hexadecimal-digit), [octal-digit](#user-content-octal-digit)_;
|
||||
|
||||
|
||||
<a name="unicode-character-escape"></a>
|
||||
@ -865,7 +864,7 @@ string-literal-element = not-double-quote-or-backslash
|
||||
/ unicode-character-escape
|
||||
```
|
||||
|
||||
Go to: _[unicode-character-escape](#user-content-unicode-character-escape), [not-double-quote-or-backslash](#user-content-not-double-quote-or-backslash), [simple-character-escape](#user-content-simple-character-escape), [ascii-character-escape](#user-content-ascii-character-escape)_;
|
||||
Go to: _[not-double-quote-or-backslash](#user-content-not-double-quote-or-backslash), [ascii-character-escape](#user-content-ascii-character-escape), [unicode-character-escape](#user-content-unicode-character-escape), [simple-character-escape](#user-content-simple-character-escape)_;
|
||||
|
||||
|
||||
The ones above are all the atomic literals
|
||||
@ -885,7 +884,7 @@ atomic-literal = untyped-literal
|
||||
/ string-literal
|
||||
```
|
||||
|
||||
Go to: _[untyped-literal](#user-content-untyped-literal), [character-literal](#user-content-character-literal), [unsigned-literal](#user-content-unsigned-literal), [boolean-literal](#user-content-boolean-literal), [signed-literal](#user-content-signed-literal), [address-literal](#user-content-address-literal), [field-literal](#user-content-field-literal), [string-literal](#user-content-string-literal), [product-group-literal](#user-content-product-group-literal)_;
|
||||
Go to: _[boolean-literal](#user-content-boolean-literal), [unsigned-literal](#user-content-unsigned-literal), [signed-literal](#user-content-signed-literal), [untyped-literal](#user-content-untyped-literal), [address-literal](#user-content-address-literal), [field-literal](#user-content-field-literal), [character-literal](#user-content-character-literal), [product-group-literal](#user-content-product-group-literal), [string-literal](#user-content-string-literal)_;
|
||||
|
||||
|
||||
After defining the (mostly) alphanumeric tokens above,
|
||||
@ -929,7 +928,7 @@ token = keyword
|
||||
/ symbol
|
||||
```
|
||||
|
||||
Go to: _[symbol](#user-content-symbol), [keyword](#user-content-keyword), [identifier](#user-content-identifier), [atomic-literal](#user-content-atomic-literal), [package-name](#user-content-package-name), [annotation-name](#user-content-annotation-name)_;
|
||||
Go to: _[atomic-literal](#user-content-atomic-literal), [keyword](#user-content-keyword), [annotation-name](#user-content-annotation-name), [symbol](#user-content-symbol), [package-name](#user-content-package-name), [identifier](#user-content-identifier)_;
|
||||
|
||||
|
||||
Tokens, comments, and whitespace are lexemes, i.e. lexical units.
|
||||
@ -939,7 +938,7 @@ Tokens, comments, and whitespace are lexemes, i.e. lexical units.
|
||||
lexeme = token / comment / whitespace
|
||||
```
|
||||
|
||||
Go to: _[token](#user-content-token), [comment](#user-content-comment), [whitespace](#user-content-whitespace)_;
|
||||
Go to: _[comment](#user-content-comment), [token](#user-content-token), [whitespace](#user-content-whitespace)_;
|
||||
|
||||
|
||||
|
||||
@ -975,7 +974,7 @@ signed-type = %s"i8" / %s"i16" / %s"i32" / %s"i64" / %s"i128"
|
||||
integer-type = unsigned-type / signed-type
|
||||
```
|
||||
|
||||
Go to: _[unsigned-type](#user-content-unsigned-type), [signed-type](#user-content-signed-type)_;
|
||||
Go to: _[signed-type](#user-content-signed-type), [unsigned-type](#user-content-unsigned-type)_;
|
||||
|
||||
|
||||
The integer types, along with the field and group types,
|
||||
@ -1090,7 +1089,7 @@ form all the types.
|
||||
type = scalar-type / tuple-type / array-type / identifier / self-type
|
||||
```
|
||||
|
||||
Go to: _[scalar-type](#user-content-scalar-type), [array-type](#user-content-array-type), [tuple-type](#user-content-tuple-type), [self-type](#user-content-self-type), [identifier](#user-content-identifier)_;
|
||||
Go to: _[tuple-type](#user-content-tuple-type), [identifier](#user-content-identifier), [array-type](#user-content-array-type), [self-type](#user-content-self-type), [scalar-type](#user-content-scalar-type)_;
|
||||
|
||||
|
||||
It is convenient to introduce a rule for types that are
|
||||
@ -1101,7 +1100,7 @@ either identifiers or `Self`, as this is used in other rules.
|
||||
identifier-or-self-type = identifier / self-type
|
||||
```
|
||||
|
||||
Go to: _[self-type](#user-content-self-type), [identifier](#user-content-identifier)_;
|
||||
Go to: _[identifier](#user-content-identifier), [self-type](#user-content-self-type)_;
|
||||
|
||||
|
||||
The lexical grammar given earlier defines product group literals.
|
||||
@ -1150,7 +1149,7 @@ a group literal is either a product group literal or an affine group literal.
|
||||
group-literal = product-group-literal / affine-group-literal
|
||||
```
|
||||
|
||||
Go to: _[product-group-literal](#user-content-product-group-literal), [affine-group-literal](#user-content-affine-group-literal)_;
|
||||
Go to: _[affine-group-literal](#user-content-affine-group-literal), [product-group-literal](#user-content-product-group-literal)_;
|
||||
|
||||
|
||||
As often done in grammatical language syntax specifications,
|
||||
@ -1179,7 +1178,7 @@ primary-expression = identifier
|
||||
/ circuit-expression
|
||||
```
|
||||
|
||||
Go to: _[identifier](#user-content-identifier), [array-expression](#user-content-array-expression), [literal](#user-content-literal), [expression](#user-content-expression), [tuple-expression](#user-content-tuple-expression), [circuit-expression](#user-content-circuit-expression)_;
|
||||
Go to: _[identifier](#user-content-identifier), [circuit-expression](#user-content-circuit-expression), [tuple-expression](#user-content-tuple-expression), [literal](#user-content-literal), [expression](#user-content-expression), [array-expression](#user-content-array-expression)_;
|
||||
|
||||
|
||||
Tuple expressions construct tuples.
|
||||
@ -1232,7 +1231,7 @@ Go to: _[expression](#user-content-expression)_;
|
||||
array-repeat-construction = "[" expression ";" array-expression-dimensions "]"
|
||||
```
|
||||
|
||||
Go to: _[expression](#user-content-expression), [array-expression-dimensions](#user-content-array-expression-dimensions)_;
|
||||
Go to: _[array-expression-dimensions](#user-content-array-expression-dimensions), [expression](#user-content-expression)_;
|
||||
|
||||
|
||||
<a name="array-expression-dimensions"></a>
|
||||
@ -1277,7 +1276,7 @@ circuit-construction = identifier-or-self-type "{"
|
||||
"}"
|
||||
```
|
||||
|
||||
Go to: _[circuit-inline-element](#user-content-circuit-inline-element), [identifier-or-self-type](#user-content-identifier-or-self-type)_;
|
||||
Go to: _[identifier-or-self-type](#user-content-identifier-or-self-type), [circuit-inline-element](#user-content-circuit-inline-element)_;
|
||||
|
||||
|
||||
<a name="circuit-inline-element"></a>
|
||||
@ -1336,7 +1335,7 @@ postfix-expression = primary-expression
|
||||
/ postfix-expression "[" [expression] ".." [expression] "]"
|
||||
```
|
||||
|
||||
Go to: _[identifier](#user-content-identifier), [natural](#user-content-natural), [expression](#user-content-expression), [primary-expression](#user-content-primary-expression), [identifier-or-self-type](#user-content-identifier-or-self-type), [postfix-expression](#user-content-postfix-expression), [function-arguments](#user-content-function-arguments)_;
|
||||
Go to: _[expression](#user-content-expression), [identifier-or-self-type](#user-content-identifier-or-self-type), [postfix-expression](#user-content-postfix-expression), [function-arguments](#user-content-function-arguments), [identifier](#user-content-identifier), [natural](#user-content-natural), [primary-expression](#user-content-primary-expression)_;
|
||||
|
||||
|
||||
Unary operators have the highest operator precedence.
|
||||
@ -1350,7 +1349,7 @@ unary-expression = postfix-expression
|
||||
/ "-" unary-expression
|
||||
```
|
||||
|
||||
Go to: _[postfix-expression](#user-content-postfix-expression), [unary-expression](#user-content-unary-expression)_;
|
||||
Go to: _[unary-expression](#user-content-unary-expression), [postfix-expression](#user-content-postfix-expression)_;
|
||||
|
||||
|
||||
Next in the operator precedence is exponentiation,
|
||||
@ -1427,7 +1426,7 @@ conjunctive-expression = equality-expression
|
||||
/ conjunctive-expression "&&" equality-expression
|
||||
```
|
||||
|
||||
Go to: _[conjunctive-expression](#user-content-conjunctive-expression), [equality-expression](#user-content-equality-expression)_;
|
||||
Go to: _[equality-expression](#user-content-equality-expression), [conjunctive-expression](#user-content-conjunctive-expression)_;
|
||||
|
||||
|
||||
Next come disjunctive expressions, left-associative.
|
||||
@ -1451,7 +1450,7 @@ conditional-expression = disjunctive-expression
|
||||
":" conditional-expression
|
||||
```
|
||||
|
||||
Go to: _[disjunctive-expression](#user-content-disjunctive-expression), [expression](#user-content-expression), [conditional-expression](#user-content-conditional-expression)_;
|
||||
Go to: _[expression](#user-content-expression), [conditional-expression](#user-content-conditional-expression), [disjunctive-expression](#user-content-disjunctive-expression)_;
|
||||
|
||||
|
||||
Those above are all the expressions.
|
||||
@ -1484,7 +1483,7 @@ statement = expression-statement
|
||||
/ block
|
||||
```
|
||||
|
||||
Go to: _[loop-statement](#user-content-loop-statement), [expression-statement](#user-content-expression-statement), [return-statement](#user-content-return-statement), [conditional-statement](#user-content-conditional-statement), [assignment-statement](#user-content-assignment-statement), [variable-declaration](#user-content-variable-declaration), [console-statement](#user-content-console-statement), [constant-declaration](#user-content-constant-declaration), [block](#user-content-block)_;
|
||||
Go to: _[assignment-statement](#user-content-assignment-statement), [return-statement](#user-content-return-statement), [conditional-statement](#user-content-conditional-statement), [expression-statement](#user-content-expression-statement), [variable-declaration](#user-content-variable-declaration), [loop-statement](#user-content-loop-statement), [constant-declaration](#user-content-constant-declaration), [console-statement](#user-content-console-statement), [block](#user-content-block)_;
|
||||
|
||||
|
||||
<a name="block"></a>
|
||||
@ -1536,7 +1535,7 @@ constant-declaration = %s"const" identifier-or-identifiers [ ":" type ]
|
||||
"=" expression ";"
|
||||
```
|
||||
|
||||
Go to: _[identifier-or-identifiers](#user-content-identifier-or-identifiers), [type](#user-content-type), [expression](#user-content-expression)_;
|
||||
Go to: _[identifier-or-identifiers](#user-content-identifier-or-identifiers), [expression](#user-content-expression), [type](#user-content-type)_;
|
||||
|
||||
|
||||
<a name="identifier-or-identifiers"></a>
|
||||
@ -1569,7 +1568,7 @@ conditional-statement = branch
|
||||
/ branch %s"else" conditional-statement
|
||||
```
|
||||
|
||||
Go to: _[branch](#user-content-branch), [block](#user-content-block), [conditional-statement](#user-content-conditional-statement)_;
|
||||
Go to: _[conditional-statement](#user-content-conditional-statement), [branch](#user-content-branch), [block](#user-content-block)_;
|
||||
|
||||
|
||||
A loop statement implicitly defines a loop variable
|
||||
@ -1582,7 +1581,7 @@ loop-statement = %s"for" identifier %s"in" expression ".." [ "=" ] expression
|
||||
block
|
||||
```
|
||||
|
||||
Go to: _[block](#user-content-block), [expression](#user-content-expression), [identifier](#user-content-identifier)_;
|
||||
Go to: _[expression](#user-content-expression), [identifier](#user-content-identifier), [block](#user-content-block)_;
|
||||
|
||||
|
||||
An assignment statement is straightforward.
|
||||
@ -1599,7 +1598,7 @@ assignment-operator = "=" / "+=" / "-=" / "*=" / "/=" / "**="
|
||||
assignment-statement = expression assignment-operator expression ";"
|
||||
```
|
||||
|
||||
Go to: _[assignment-operator](#user-content-assignment-operator), [expression](#user-content-expression)_;
|
||||
Go to: _[expression](#user-content-expression), [assignment-operator](#user-content-assignment-operator)_;
|
||||
|
||||
|
||||
Console statements start with the `console` keyword,
|
||||
@ -1655,7 +1654,7 @@ Go to: _[string-literal](#user-content-string-literal)_;
|
||||
print-call = print-function print-arguments
|
||||
```
|
||||
|
||||
Go to: _[print-function](#user-content-print-function), [print-arguments](#user-content-print-arguments)_;
|
||||
Go to: _[print-arguments](#user-content-print-arguments), [print-function](#user-content-print-function)_;
|
||||
|
||||
|
||||
An annotation consists of an annotation name (which starts with `@`)
|
||||
@ -1685,7 +1684,7 @@ function-declaration = *annotation %s"function" identifier
|
||||
block
|
||||
```
|
||||
|
||||
Go to: _[type](#user-content-type), [identifier](#user-content-identifier), [function-parameters](#user-content-function-parameters), [block](#user-content-block)_;
|
||||
Go to: _[identifier](#user-content-identifier), [function-parameters](#user-content-function-parameters), [type](#user-content-type), [block](#user-content-block)_;
|
||||
|
||||
|
||||
<a name="function-parameters"></a>
|
||||
@ -1695,7 +1694,7 @@ function-parameters = self-parameter
|
||||
/ function-inputs
|
||||
```
|
||||
|
||||
Go to: _[function-inputs](#user-content-function-inputs), [self-parameter](#user-content-self-parameter)_;
|
||||
Go to: _[self-parameter](#user-content-self-parameter), [function-inputs](#user-content-function-inputs)_;
|
||||
|
||||
|
||||
<a name="self-parameter"></a>
|
||||
@ -1716,7 +1715,7 @@ Go to: _[function-input](#user-content-function-input)_;
|
||||
function-input = [ %s"const" ] identifier ":" type
|
||||
```
|
||||
|
||||
Go to: _[identifier](#user-content-identifier), [type](#user-content-type)_;
|
||||
Go to: _[type](#user-content-type), [identifier](#user-content-identifier)_;
|
||||
|
||||
|
||||
A circuit member variable declaration consists of
|
||||
@ -1764,7 +1763,7 @@ circuit-declaration = %s"circuit" identifier
|
||||
*member-function-declaration "}"
|
||||
```
|
||||
|
||||
Go to: _[member-variable-declarations](#user-content-member-variable-declarations), [identifier](#user-content-identifier)_;
|
||||
Go to: _[identifier](#user-content-identifier), [member-variable-declarations](#user-content-member-variable-declarations)_;
|
||||
|
||||
|
||||
An import declaration consists of the `import` keyword
|
||||
@ -1786,7 +1785,7 @@ by using an explicit package name before the package path.
|
||||
import-declaration = %s"import" package-name "." package-path ";"
|
||||
```
|
||||
|
||||
Go to: _[package-path](#user-content-package-path), [package-name](#user-content-package-name)_;
|
||||
Go to: _[package-name](#user-content-package-name), [package-path](#user-content-package-path)_;
|
||||
|
||||
|
||||
<a name="package-path"></a>
|
||||
@ -1797,7 +1796,7 @@ package-path = "*"
|
||||
/ "(" package-path *( "," package-path ) [","] ")"
|
||||
```
|
||||
|
||||
Go to: _[package-name](#user-content-package-name), [package-path](#user-content-package-path), [identifier](#user-content-identifier)_;
|
||||
Go to: _[package-name](#user-content-package-name), [identifier](#user-content-identifier), [package-path](#user-content-package-path)_;
|
||||
|
||||
|
||||
A type alias declaration defines an identifier to stand for a type.
|
||||
|
@ -414,7 +414,6 @@ keyword = %s"address"
|
||||
/ %s"Self"
|
||||
/ %s"self"
|
||||
/ %s"static"
|
||||
/ %s"string"
|
||||
/ %s"type"
|
||||
/ %s"u8"
|
||||
/ %s"u16"
|
||||
|
9
tests/compiler/array_without_size/compare_fail.leo
Normal file
9
tests/compiler/array_without_size/compare_fail.leo
Normal file
@ -0,0 +1,9 @@
|
||||
/*
|
||||
namespace: Compile
|
||||
expectation: Fail
|
||||
*/
|
||||
|
||||
function main() {
|
||||
let x: [u8; _] = [1u8,2];
|
||||
let z: bool = x == [1u8,2,3]; // array size mismatch
|
||||
}
|
@ -0,0 +1,5 @@
|
||||
---
|
||||
namespace: Compile
|
||||
expectation: Fail
|
||||
outputs:
|
||||
- "Error [ECMP0376093]: array sizes must match for comparison; left: 2, right: 3\n --> compiler-test:5:19\n |\n 5 | let z: bool = x == [1u8,2,3]; // array size mismatch\n | ^^^^^^^^^^^^^^"
|
Loading…
Reference in New Issue
Block a user