Introducing LEO: A Ledger-Based Programming Language
LEO is a programming language designed for executing offline computations and producing transactions in a ledger-based system. It prioritizes security and privacy, making it suitable for zero-knowledge applications. In this blog post, we will explore the design of LEO, including its environment, syntax, static and dynamic semantics, and R1CS semantics.
Environment: LEO programs execute in a ledger-based system where users can perform offline computations and generate transactions. The language ensures execution correctness, privacy, and transaction non-malleability. Malicious parties cannot create valid state transitions without the private key and application state of a user, transactions only reveal intended public information, and transactions are protected from modification in transit to the ledger.
Syntax: The syntax of LEO is defined using a context-free grammar. It supports scalar types (booleans, integers, addresses, field elements, and group elements) and aggregate types (tuples, arrays, and circuit types). Circuit types resemble class types in other languages and consist of member variable and member function declarations. Functions can be defined at the top level or as member functions of circuit types.
Expressions: LEO supports various types of expressions, including variables, literals, unary and binary operations, tuples, arrays, circuits, function calls, conditionals, and more. Expressions can refer to function parameters, local variables, and circuit member variables. The language provides convenient syntax for common operations, such as accessing tuple components or array elements.
Statements: Statements in LEO include expression statements, return statements, variable definition statements, assignment statements, conditional statements, loop statements, and console statements. Expression statements are used for side effects, return statements specify values to be returned from functions, and assignment statements modify variable values. Conditional and loop statements control the flow of execution.
Annotations: LEO allows annotations in circuit and function declarations, although their details are omitted in this summary. Currently, LEO supports a limited set of annotations for test functions.
Files, Imports, and Packages: LEO programs are organized into files, which contain function and circuit type declarations. Import declarations enable referencing functions and circuit types from other files or libraries. Packages provide a way to bundle collections of LEO functions and circuit types together.
Static Semantics: LEO’s static semantics ensure compile-time requirements for program compilation. The process involves canonicalization, type checking, type inference, and checking for scope and correctness of expressions and statements. The canonicalization phase simplifies equivalent forms of language constructs, while type checking and inference determine the types of expressions and statements. The static semantics guarantee type correctness and consistency.
LEO is a ledger-based programming language designed for secure and privacy-preserving computations in a zero-knowledge context. With its expressive syntax, support for various types, and emphasis on security, LEO provides a powerful tool for developing applications that require correctness, privacy, and non-malleability.