Constants are immutable values that are assigned to a variable at compile time. Constants are declared using the const keyword and must be initialized with a value or with an expression that can be evaluated at compile time. The value of a constant cannot be changed once it is assigned. Technically, a constant is a substitute for an underlying literal value which is replaced by the constant's value during compilation.
const MAX_SIZE: u32 = 100;
Functions in Inference are used to define a block of code that can be executed multiple times with different inputs. Functions are defined using the fn keyword followed by the function name, type parameters, parameters, return type, and body. Functions can have multiple parameters and can return a single value or a tuple of values.
For detailed information about functions, see the Functions section.
fn sum(a: u32, b: u32) -> u32 {
return a + b;
}
External functions are functions that are not defined within the current module or spec but in fact are host calls. Such functions may simulate the host (blockchain) behavior as a description about the external environment.
For detailed information about external functions, see the Functions section.
external fn external_function(a: u32, b: u32) -> u32;
Types in Inference are used to define the structure of data. Inference provides a set of built-in types, such as integers, booleans, and arrays, as well as the ability to define custom types using structs and enums.
For detailed information about embedded types, see the Types section.
type Address = u32;
A spec is an abstract module representation. By module, we mean a scoped set of imports, definitions, and functions. Specs are used to group related definitions and functions together and provide a way to organize the program specification as a whole. Technically, in proof mode a spec is translated into a theory of propositions and theorems alongside its module; in compile mode the spec is stripped from the output entirely. See §3.2 Compiler Design.
Specs may contain definitions of constants, structs, enums, and functions. Nested specs are not allowed and are rejected at parse time.
spec AuctionSpec {
const MAX_BID: u64 = 1000;
const MIN_BID: u64 = 100;
struct Bid {
bidder: Address;
amount: u64;
}
enum AuctionState {
Open,
Closed
}
fn is_valid_bid(bid: Bid) -> bool {
return bid.amount >= MIN_BID && bid.amount <= MAX_BID;
}
fn is_auction_open(state: AuctionState) -> bool {
return state == AuctionState::Open;
}
}
Enums, short for enumerations, are a user-defined data type in Inference that consists of a set of named integral constants. They provide a way to assign symbolic names to integral values, enhancing code readability and maintainability.
During compilation, the compiler replaces the enum constants with their corresponding integral values, making enums a compile-time construct. Technically, enums are very similar to C-style "macro enums".
enum Arch {
WASM,
EVM,
}
enum ContextType {
Program,
Contract,
}
A struct in Inference is a user-defined algebraic data type that allows defining a group of variables under a single name. The underlying data structure of a struct is a record (or a tuple), which is a collection of fields or members. Each field can have a different type, and the fields are accessed using the dot operator.
Along with the fields, a struct can also have methods that define the behavior of the struct. These methods can be used to manipulate the fields of the struct or perform some operations on them. The methods are defined inside the struct block and must take either self or mut self as the first parameter. A method which takes self can read the value of any field of the instance it was invoked on by accessing it using the self keyword. However, it may neither mutate any data in the struct, nor call other methods which take mut self. Methods which take mut self can additionally change data and call other mut self methods, but they may only be invoked on a mutable instance of the struct.
Declared structs will automatically have a new function in their namespace for creating instances of the struct. The parameters of the new function are the values to be assigned to each field in the new instance. They must be explicitly named with name: value syntax, and the order of the parameters does not matter.
Declaring an Account struct:
struct Account {
address: Address;
balance: u64;
fn can_withdraw(self, amount: u64) -> bool {
return self.balance >= amount;
}
fn transfer(mut self, amount: u64, mut receiver : Account) -> bool {
if !self.can_withdraw(amount) {return false;}
self.balance = self.balance - amount;
receiver.balance = receiver.balance + amount;
return true;
}
}
Creating an instance of Account:
// Suppose we already have some address we would like to use...
let addr : Address = ... ;
// Create the new account with that address, and a balance of 0.
let acc : Account = Account::new(address: addr, balance: 0);
The type signature of the constructor is
Account::new(Address,u64) -> Account
It is possible to pass named arguments rather than relying on the order they are declared in:
let acc : Account = Account::new(balance: 0, address: addr);
Invoking methods:
let mut account1 : Account = Account::new(address: addr1, balance: 10)
let mut account2 : Account = Account::new(address: addr2, balance: 0);
let account3 : Account = Account::new(address: addr3, balance: 5);
// Works because account1 and account2 are mutable, so we can change
// both of the balances.
account1.transfer(5, account2);
// Results in error: account2 is mutable, but account3 is not, so we cannot
// change its balance.
account2.transfer(2, account3);
// Results in error: account1 is mutable, but account3 is not.
account3.transfer(1, account1);
// This is OK. can_withdraw takes a regular reference, so we can invoke
// it on immutable account instances, as it does not change any information.
let my_bool : bool = account3.can_withdraw(10);