aleohq / leo Goto Github PK

Overview

Currently a function containing multiple return statements will short circuit upon evaluating the first one.
This is incorrect behavior because we need to evaluate the entirety of each function to satisfy R1CS constraints.

Changes

function main(cond: bool) -> u32 {
    if cond {
        return 1u32
    } else {
        return 0u32
    }
}

In the above function there are two return statements whose results depend on a cond input boolean.
We can conditionally select the desired result from the conditional by passing this cond as an indicator to the function main when it is ready to return.
As expected, return arguments will no longer terminate a function early. Instead, they will pass their result along with their indicator to the function main when it is ready to return.

Issue Overview:

The leo-compiler directory structure is a mess after adding several individual features. It should be simplified to improve readability and further development.

Current directory structure

leo
|- compiler/
    |- src/
        |- address/
        |- constraints/
            |- definitions/
            |- mod.rs
            |- boolean.rs
            |- comparator.rs
            |- expression.rs
            |- field.rs
            |- function.rs
            |- generate_constraints.rs
            |- group.rs
            |- integer.rs
            |- program.rs
            |- statement.rs
            |- value.rs
        |- errors/
        |- field/
        |- group/
        |- imports/
        |- compiler.rs
        |- lib.rs
    |- tests/
    |- Cargo.toml
    |- README.md

New directory structure

leo
|- compiler/
    |- src/
        |- constraints/
            |- generate_constraints.rs
        |- definition/
        |- errors/
        |- expression/
        |- function/
        |- import/
        |- program/
        |- statement/
        |- value/
            |- address/
            |- boolean/
            |- field/
            |- group/
            |- integer/
            |- comparator.rs
            |- value.rs
        |- compiler.rs
        |- lib.rs
    |- tests/
    |- Cargo.toml
    |- README.md

All files in the previous structure will be moved into a module folder with the same name where appropriate.
Files with conflicting names will be renamed according to their function within the new module.

Inputs

token_withdraw.in

[main]
data: u8[32] = [0u8; 32];

[registers]
token_id: u8[32] = [0u8; 32];
value_balance: u64 = 0;

token_withdraw.state

[[public]]

[state]
leaf_index: u32 = 0;
root: u8[32] = [0u8; 32];

[[private]]

[record]
serial_number: u8[32] = [0u8; 32];
commitment: u8[32] = [0u8; 32];
owner: address = aleo1...;
value: u64 = 5;
payload: u8[32] = [0u8; 32]; // TBD
birth_program_id: u8[32] = [0u8; 32];
death_program_id: u8[32] = [0u8; 32];
serial_number_nonce: u8[32] = [0u8; 32];
commitment_randomness: u8[32] = [0u8; 32];

[state_leaf]
path: u8[32][2] = [ [0u8; 32], [0u8; 32] ];
memo: u8[32] = [0u8; 32];
network_id: u8 = 0;
leaf_randomness: u8[32] = [0u8; 32];

Outputs

token_withdraw.out

[registers]
token_id: u8[32] = [0u8; 32];
value_balance: u64 = 5;

For integration tests, one can invoke these files to load the correct input and state as follows:

#[({USER_DEFINED_1}.in, {USER_DEFINED_2}.state, {USER_DEFINED_3}.out)]
test function token_withdraw() {
    ...
}

For example, one could invoke it as any of the following examples:

#[(token_withdraw.in, token_withdraw.state, token_withdraw.out)]
test function token_withdraw() {
    ...
}

#[(test_input.in, test_state.state, test_output.out)]
test function token_withdraw() {
    ...
}

#[
    mainnet.in,
    mainnet.state,
    mainnet.out
]
test function token_withdraw() {
    ...
}

Issue Scope

Currently the GroupElement enum holds only constant values that implement the Group trait.

Proposed Changes

First, the GroupElement will be renamed to GroupAffine to make it more clear that this data type should generically represent an affine point (x, y) on the given elliptic curve.

Second, a new data type will be created to hold both constant and allocated representations of an affine point.
This data type will be implemented similar to https://github.com/AleoHQ/snarkOS/tree/master/models/src/gadgets/utilities

The following gadget trait implementations will be required: ToBytesGadget, EqGadget, ConditionalEqGadget, CondSelectGadget, AllocGadget.
There should also be methods constant(), add(), add_constant(), sub(), sub_constant() where a constraint system over a given field can be passed into the method signature.
As a result, the final GroupAffine type will not have any additional trait arguments. This will help to keep the overall compiler clean and free of additional trait dependencies.

Currently import files are compiled when their functions are called. Not when the main file is compiled.
This should be changed so that all files care compiled at the same time.

🚀 Describe the Feature

Adding support for floats (f8, f16, f32, f64)

Motivation

Floating-type values are important for ML and data science applications.

🚀 Describe the Feature

During the build phase, Leo should generate the local data commitment opening to ensure the program will verify that the provided record to the program is indeed legitimate inputs.

🐛 Describe the Bug

Integer variable != integer value

Steps to Reproduce

Code snippet to reproduce

function mean(inputs: u32[10]) -> u32 {
    let mut output = 0u32;
    for i in 0..10 {
        output += inputs[i];
    }
    return output/10
}

function calculate_coefficients(y_array: u32[10], x_array: u32[10]) -> (u32, u32) {
    let x_mean = mean(x_array);
    let y_mean = mean(y_array);

    let mut numerator = 0u32;
    let mut denominator = 0u32;

    for i in 0..10 {
        numerator += (x_array[i] - x_mean) * (y_array[i] - y_mean);
        denominator += (x_array[i] - x_mean) ** 2;
    }

    let b1 = numerator / denominator;
    let b0 = y_mean - (b1 * x_mean);

    return (b1, b0)
}

// 1 != 1, and 0 != 0
test function test_calculate_coefficients() {
    let x_array: u32[10] = [0,1,2,3,4,5,6,7,8,9];
    let y_array: u32[10] = [0,1,2,3,4,5,6,7,8,9];

    print!("{}", x_array);
    print!("{}", y_array);

    let (b1, b0) = calculate_coefficients(y_array, x_array);

    assert_eq!(b1, 1);
    assert_eq!(b0, 0);
}

Currently integer >=, >, <=, < is only supported at the evaluation level for leo primitives.
This means that these operators are not enforced in the constraint system.

This introduces const in the Leo input file.

[main]
const a: bool = true;
b: u8 = 2;
c: field = 0;
d: group = (0, 1)group;

Note that in main.leo this is unchanged.

function main(a: bool, b: u8, c: field, d: group) {
}

Overview

For syntax errors that do not match the style guide we should output warnings to console.

Changes

Use the warn! macro from the log crate.
Try to catch candidates as early as possible in compiler.

Currently private and public keywords represent allocated public and private inputs that are passed to the constraint system when a leo program is executed.
We will be removing these visibility keywords altogether and restricting all program variables to private. This will remove visual confusion and code conflict when integrating Leo with snarkOS down the line.

println!()
debug!()
error!()

I don't believe we are using these two methods in leo-typed/common/span.rs:
https://github.com/AleoHQ/leo/blob/master/types/src/common/span.rs#L33
https://github.com/AleoHQ/leo/blob/master/types/src/common/span.rs#L51

In addition, I believe the conversion from AstSpan<'ast> can be done much cleaner, as Pest already has this logic built-in. e.g. span.as_str() should be able to replace our logic of span.start_pos().line_of().trim_end() and would be a more reliable impl then as semantically, we just want the affected string.

@collinc97 if you can confirm, I can impl these changes in PR #120

The field tests for leo in compiler/tests/field do not test the full length of field elements.

Leo will parse a number in decimal format into a field element. However, there is currently no way to convert a field element into decimal format.

This makes it difficult to test because we can generate random field elements but cannot pass them into the Leo compiler.

A conversion between the field element's BigInteger format into decimal is needed to resolve this issue.

🐛 Describe the Bug

When initializing a new Leo repository, we are missing files to run Leo.
Missing .state file causes leo commands to fail.

Refactor all errors to follow the following example:

leo error: expected `;` found `EOF`
--> src/main.leo:3:19
   |
 3 |     let a: u32 = 1␊
   |                   ^---
   |
 = expected `;`
leo error: could not compile src/main.leo

🚀 Describe the Feature

We should investigate the Pest parses_to convention for leo-ast and leo-input testing.
https://docs.rs/pest/2.1.3/pest/macro.parses_to.html

Motivation

Currently, we are checking inputs via higher level testing and this could be a clean way to implement direct checks on the Pest generated AST, rather than waiting until a later stage to verify correctness.

Issue Scope

Currently the FieldElement enum does not take advantage of FpGadget and directly holds the value and variable for an allocated field.

As a result, the following gadgets need to be manually implemented: AllocGadget, EqGadget, ConditionalEqGadget, CondSelectGadget, ToBitsGadget, ToBytesGadget
In addition, relying on Field as a trait parameter in types.rs bloats the code significantly. We can optimize by passing the string down to a FieldType module. Similar to the changes from #37

Proposed Changes

FieldElement will be refactored to Field which will contain a string in /compiler/src/types.rs.
A new FieldType module will be defined at /compiler/src/field.

pub enum FieldType<F: Field + PrimeField> {
  Constant(F),
  Allocated(FpGadget<F>),
}

The FieldType module will implement the following methods: constant(), add(), sub(), mul(), div(), pow().

and traits: AllocGadget, EqGadget, ConditionalEqGadget, CondSelectGadget, ToBitsGadget, ToBytesGadget.

🐛 Describe the Bug

Tests are not run in isolation. Running two tests on the same method produces error if expected outputs differ.

Steps to Reproduce

Code snippet to reproduce

function mean(inputs: u32[10]) -> u32 {
    let mut output = 0u32;
    for i in 0..10 {
        output += inputs[i];
    }
    return output/10
}

test function test_mean() {
    let inputs = [1u32; 10];
    assert_eq!(1, mean(inputs));
}

// Should equal 2, mean(inputs) outputs 1.
test function test_mean2() {
    let inputs = [2u32; 10];
    assert_eq!(2, mean(inputs));
}

🚀 Describe the Feature

Rename leo-inputs folder to input and rename the leo-inputs package to leo-input.

Motivation

As we migrate to the main(input) convention, we should maintain consistency in naming of our modules to maintain cleanliness.

let will indicate an allocated program variable.
const will indicate a constant program variable.

Allocated program variables must be passed in as private inputs to the constraint system upon program execution.

Constant program variables are static values which do not need to passed in as inputs to the constraint system.

Currently in the README, tuple are returned without a clear declaration: https://github.com/AleoHQ/leo/blame/master/README.md#L267.

Shouldn't it be return (1, [2, 3]) instead of return 1, [2, 3]?

Not sure if this is a typo in the README or intended behavior

Currently running leo prove will load the inputs file and parse it. These actions should be done by the compiler prior to program execution.

🐛 Describe the Bug

The pow exponentiation function for signed integers fails on negative bases, large powers, and some large bases.

Steps to Reproduce

// src/main.leo
function main() {
    let a = 11i8 ** 2i8;
}

Stack trace & error message

Result::unwrap()` on an `Err` value: Overflow

Expected Behavior

The function should compile and run without error.

We will need a gadget of 2 constraints with the following logic to handle assertions in a conditional branch.

D = A * B
indicator * (D - C) == 0

🐛 Describe the Bug

There are unnecessary parenthesis on line:

They do not enforce any special ordering on different statements so they should be removed.

Currently assigning multiple returns from a function:

let (a, b) = double();

With explicit types:

let (u32 a, u32 b) = double();

The explicit type assignment should be changed to:

let (a, b): (u32, u32) = double();

Overview

Currently ConstraintSystem is a parameter for ConstrainedProgram. ConstraintSystem is used in some but not all methods and is not used by ConstrainedProgram directly. This should be changed so that ConstraintSystem is only passed into methods that need it.

The current ConstrainedProgram struct:

pub struct ConstrainedProgram<F: Field + PrimeField, G: GroupType<F>, CS: ConstraintSystem<F>> {
    pub identifiers: HashMap<String, ConstrainedValue<F, G>>,
    pub _cs: PhantomData<CS>,
}

The new struct:

pub struct ConstrainedProgram<F: Field + PrimeField, G: GroupType<F>> {
    pub identifiers: HashMap<String, ConstrainedValue<F, G>>,
}

The current enforce_add_expression() method:

fn enforce_add_expression(
        &mut self,
        cs: &mut CS,
        left: ConstrainedValue<F, G>,
        right: ConstrainedValue<F, G>,
    ) -> Result<ConstrainedValue<F, G>, ExpressionError>

The new method:

fn enforce_add_expression<CS: ConstraintSystem<F>>(
        &mut self,
        cs: &mut CS,
        left: ConstrainedValue<F, G>,
        right: ConstrainedValue<F, G>,
    ) -> Result<ConstrainedValue<F, G>, ExpressionError>

Dependabot couldn't fetch one or more of your project's path-based Rust dependencies. The affected dependencies were ../snarkOS/algorithms/Cargo.toml, ../snarkOS/curves/Cargo.toml, ../snarkOS/errors/Cargo.toml, ../snarkOS/gadgets/Cargo.toml, ../snarkOS/models/Cargo.toml and ../snarkOS/utilities/Cargo.toml.

To use path-based dependencies with Dependabot the paths must be relative and resolve to a directory in this project's source code.

View the update logs.

u8 integers test overflows it's stack sometimes when being run

To simplify file types, I propose the following file formats to transition to.

{package_name}.leo.pk -> {package_name}.lpk
{package_name}.leo.vk -> {package_name}.lvk
{package_name}.leo.proof -> {package_name}.proof
{package_name}.leo.checksum -> {package_name}.sum

In addition, inputs will be changed as follows:

inputs.leo -> {package_name}.in

Issue Scope

Currently, unique name spaces are not created for statements or expressions in a program.

function main() {
  let mut a = 0;
  a += 1;
  a += 1; // <- gives conflicting namespace error
}

This makes iterative code like for loops fail as well.

Proposed Changes

refactor the Types module to include Span details such as line number which can be used to create a unique namespace.