# Aeri
Aeri is a Cardano smart contract language by Knott Dynamics, created by Trevor
Knott. The `aeri` crate is the official Aeri language toolchain: compiler, CLI,
and Rust API. It checks contracts, runs pure tests, formats and lints source,
and compiles the supported language subset to Plutus V2 UPLC/CBOR.
## Aeri Language
Aeri defines its own `.aeri` source language for writing typed validators,
helper functions, custom data types, constants, pattern matches, and pure tests.
The toolchain provides commands to create projects, check types, run tests,
format and lint code, inspect lowering, estimate costs, generate contract docs,
and build preview or UPLC artifacts.
Unsupported Cardano ledger behavior is rejected explicitly. Aeri does not label
preview IR or partially lowered contracts as deployable Cardano scripts.
## Installation
Install the `aeri` CLI from crates.io:
```sh
cargo install aeri
```
Create and verify a project:
```sh
aeri new my-contract
aeri check-project my-contract
aeri test-project my-contract
aeri lint-project my-contract
aeri verify-project my-contract --target preview
```
The official Rust compiler API is documented on
[docs.rs](https://docs.rs/aeri/latest/aeri/).
## Backend Status
Aeri has two output targets:
- `--target preview` emits Aeri textual IR in preview blueprint-shaped JSON with
`target: "aeri-text-ir"` and `cardanoDeployable: false`.
- `--target uplc` emits PlutusScriptV2 JSON and CBOR hex for validators that fit
the current serializable UPLC subset. `verify --target uplc` checks the
generated script hash with `cardano-cli` from `PATH` or `AERI_CARDANO_CLI`.
The UPLC target is intentionally gated. `tx_signed_by` lowers for Plutus V2
`ScriptContext` signatories, and `tx_has_datum` lowers to Plutus V2 `TxInfo`
datum-map value lookup; other transaction-context builtins such as `tx_paid_to`
and `tx_after` still require real Plutus `ScriptContext` decoder lowering and
are rejected with explicit blockers. `tx_spends` also needs a full `TxOutRef`
ABI instead of an unsafe ByteArray-only transaction-id shortcut. Custom
constructor field encoding, unsupported ledger parameter decoders, and general
list encodings are also still blocked; nullary internal constructors, direct
matches/equality, list-literal equality, and list-literal membership on
constructors built in-place whose recursively nested fields end in supported
`Bool`, `Int`, `ByteArray`, `String`, `Data`, `Unit`, or all-nullary custom
values, primitive `list_has_*` /
`list_len_*` helper calls with list
literal inputs or primitive ledger list parameters, generic `list_has` /
`list_len` for supported primitive, `Unit`, and nullary custom list literals,
including `list_has([], item)` when `item` supplies the type, generic
`list_len` for primitive ledger list parameters and direct constructor list
literals whose fields can be evaluated without encoding constructor values,
primitive list-literal equality, and nullary constructor tag equality /
list-literal equality lower in the supported subset.
```sh
aeri check my-contract/validators/main.aeri
aeri fmt --check my-contract/validators/main.aeri
aeri test my-contract/validators/main.aeri
aeri lint my-contract/validators/main.aeri
aeri inspect my-contract/validators/main.aeri --target preview --ir
aeri build-project my-contract --target preview --artifacts build/
```
## Language
Aeri modules contain `type` declarations, `fn` helpers, and `validator` entries.
A validator must take either `(redeemer, ctx)` or `(datum, redeemer, ctx)`
parameters, with `ctx: Tx` as the final parameter, and it must return `Bool`.
```aeri
module vesting;
validator release(datum: Data, redeemer: ByteArray, ctx: Tx) {
let beneficiary = #62a7f38c2dd8d7a2f55b79e8154a7e681ad7e04a08f4fd915f87cdd1;
let deadline: Int = 1000;
let signed = tx_signed_by(ctx, beneficiary);
let matured = tx_after(ctx, deadline);
trace "checking vesting release";
matured && redeemer == #01
}
```
Custom redeemers can be modeled directly and checked exhaustively with `match`:
```aeri
type Action {
Withdraw(to: ByteArray, amount: Int),
Close
}
fn authorized(action: Action, owner: ByteArray, ctx: Tx) -> Bool {
match action {
Withdraw(to, amount) => tx_signed_by(ctx, owner) && tx_paid_to(ctx, to, amount),
Close => tx_signed_by(ctx, owner)
}
}
```
Type and constructor names share the module declaration namespace, so a
constructor cannot reuse a type, function, validator, constant, or test name.
Match catch-all arms (`_` or a variable pattern) must be last, because later arms
would be unreachable. Duplicate constructor, boolean, integer, byte array, and
string match arms are rejected.
Pure `test` blocks can exercise helpers, constants, constructors, lists,
arithmetic, and deterministic transaction fixtures without a ledger node:
```aeri
test snack_menu_has_five {
list_has_int(TREATS, 5)
}
```
Add `fails` after the test name when a pure negative path is expected to reject:
```aeri
test bad_redeemer_rejects fails {
#02 == #01
}
```
Use `test_data` and `test_tx` inside test blocks to exercise transaction-context
builtins deterministically. These are test fixtures only; they are rejected in
constants, functions, and validators.
```aeri
test release_context_passes {
let owner = #aaaaaaaa;
let ctx: Tx = test_tx([owner], [], [], [], [], 1000, 2000, [], []);
tx_signed_by(ctx, owner) && tx_after(ctx, 1000)
}
```
Use `fail` when a branch should explicitly reject. It type-checks in any result
position and lowers to script error output.
```aeri
fn must_be_true(flag: Bool) -> Bool {
if flag {
true
} else {
fail
}
}
```
`aeri lint` catches suspicious contract patterns, including placeholder zero byte
arrays, tautological comparisons, self-comparisons through `datum_equals`, and
literal zero divisors, plus validators that do not contain a non-trivial
`require` guard.
Add `--deny-warnings` in CI to turn warnings into failures.
`aeri verify` and `aeri verify-project` run type checking, pure tests, and linting
as one release-readiness gate. Verification fails on lint warnings unless
`--allow-warnings` is passed. With `--target uplc`, verification also requires
successful UPLC lowering, flat encoding, CBOR script generation, and a matching
`cardano-cli transaction policyid` hash.
`aeri docs` and `aeri docs-project` generate Markdown summaries of modules,
types, constants, functions, validators, and pure tests.
`aeri cost` and `aeri cost-project` report generated script size, IR node count,
and a deterministic static budget score for quick comparison.
`aeri inspect <file>` and `aeri inspect-project <root>` render ASCII terminal
inspectors that deconstruct contracts into module items, validator parameters,
lowered IR stats, builtin use, and backend readiness. Use `--json` for
machine-readable output, `--ir` to show the full preview IR, and
`--target uplc --check` to fail CI when contracts still have UPLC emission
blockers. Use `--target uplc --check-core` to check whether a textual UPLC-core
candidate can be produced and structurally validated for scope and supported
builtin arity/version.
The current UPLC-core inspection subset covers pure lambdas, lets, constants,
conditionals, `trace`, primitive matches including `Unit`, integer arithmetic/comparisons,
primitive equality, `sha2_256`, `blake2b_256`, `append_bytes`, and
primitive `List<T>` helper/equality calls with list literal inputs, plus nullary
constructor tag equality / list-literal equality and direct matches/equality plus
list-literal equality and membership on constructors built in-place with
recursively nested direct constructor fields ending in supported `Bool`, `Int`,
`ByteArray`, `String`, `Data`, `Unit`, or all-nullary custom values, plus
primitive ledger list parameter decoding for runtime `list_has_*` / `list_len*`
helpers, generic `list_has`, and generic `list_len`, including `list_has_unit`
and `list_len_unit`,
primitive ledger list equality including `List<Unit>`, all-nullary custom ledger
list membership/length/equality by constructor tag, and mixed primitive
runtime/literal list equality.
Transaction context builtins other than `tx_signed_by` and `tx_has_datum`,
constructor field encoding, unsupported ledger parameter decoders, nested or
fieldful custom list parameters, general list values, non-primitive mixed
literal/runtime list equality outside all-nullary custom tags, and non-primitive
non-list-literal equality inputs remain blockers for UPLC emission.
Blueprint schemas include constructor titles and nested `items` metadata for
`List<T>` parameters and fields so generated JSON remains useful to downstream
tools.
## Types
Aeri supports `Bool`, `Int`, `ByteArray`, `Data`, `Tx`, `String`, `Unit`,
`List<T>`, and module-defined constructor types. Integer arithmetic, boolean
logic, comparison, `if`, `match`, `let`, `require`, `trace`, and `return` are
checked before IR is emitted.
The `Unit` literal is written as `()`, so non-empty `List<Unit>` literals can be
written as `[()]` or `[(), ()]`.
The same `()` spelling can be used as a `match` pattern for `Unit` subjects.
Local `let` bindings can be inferred or annotated, such as
`let deadline: Int = 1000;`.
Local and pattern bindings cannot shadow an existing binding in the same scope,
which keeps parameter use explicit in validators and helpers.
## Builtins
The current Cardano-oriented builtins are:
- `tx_signed_by(ctx: Tx, signer: ByteArray) -> Bool`
- `tx_paid_to(ctx: Tx, address: ByteArray, amount: Int) -> Bool`
- `tx_mints(ctx: Tx, asset: ByteArray, amount: Int) -> Bool`
- `tx_after(ctx: Tx, slot: Int) -> Bool`
- `tx_before(ctx: Tx, slot: Int) -> Bool`
- `tx_spends(ctx: Tx, output_ref: ByteArray) -> Bool`
- `tx_has_datum(ctx: Tx, datum: Data) -> Bool`
- `datum_equals(left: Data, right: Data) -> Bool`
- `sha2_256(bytes: ByteArray) -> ByteArray`
- `blake2b_256(bytes: ByteArray) -> ByteArray`
- `append_bytes(left: ByteArray, right: ByteArray) -> ByteArray`
- `list_has_bytes(items: List<ByteArray>, item: ByteArray) -> Bool`
- `list_has_int(items: List<Int>, item: Int) -> Bool`
- `list_has_bool(items: List<Bool>, item: Bool) -> Bool`
- `list_has_string(items: List<String>, item: String) -> Bool`
- `list_has_data(items: List<Data>, item: Data) -> Bool`
- `list_has_unit(items: List<Unit>, item: Unit) -> Bool`
- `list_has(items: List<T>, item: T) -> Bool`
- `list_len_bytes(items: List<ByteArray>) -> Int`
- `list_len_int(items: List<Int>) -> Int`
- `list_len_bool(items: List<Bool>) -> Int`
- `list_len_string(items: List<String>) -> Int`
- `list_len_data(items: List<Data>) -> Int`
- `list_len_unit(items: List<Unit>) -> Int`
- `list_len(items: List<T>) -> Int`
The test-only fixture builtins are:
- `test_data(bytes: ByteArray) -> Data`
- `test_tx(signers: List<ByteArray>, paid_to: List<ByteArray>, paid_amounts: List<Int>, minted_assets: List<ByteArray>, minted_amounts: List<Int>, valid_from: Int, valid_until: Int, spends: List<ByteArray>, datums: List<Data>) -> Tx`
`test_tx` evaluates `tx_paid_to` against aggregate payments to an address,
`tx_mints` against exact aggregate minted amounts, `tx_after` against
`valid_from >= slot`, and `tx_before` against `valid_until <= slot`. These
fixtures are not ledger emulation and are never deployable script output.
Constants and lists are available for common allowlist-style contracts:
```aeri
const ADMINS: List<ByteArray> = [
#11111111111111111111111111111111111111111111111111111111,
#22222222222222222222222222222222222222222222222222222222,
];
const EMPTY_ADMINS: List<ByteArray> = [];
```
Empty list literals are accepted when a `List<T>` type is known from a constant,
typed `let`, function return, `if` branch, `match` arm, call argument, or
constructor field context. They also work in equality expressions when the other
operand has a known `List<T>` type. `list_has([], item)` is allowed when `item`
has a supported primitive, `Unit`, all-nullary custom type, or direct constructor
value whose nested direct fields have supported leaves; `list_len([])` and bare
`[] == []` / `[] != []` are allowed because their results do not depend on the
item type.
## Projects
Use `aeri new <name>` to create a project skeleton with `aeri.toml` and a
starter validator under `validators/`. Use `aeri check-project <root>` to type
check a whole project, `aeri fmt-project --write <root>` to format it, and
`aeri verify-project <root> --target preview` before shipping to run checks,
pure tests, and lints together. `aeri build-project <root> --target preview`
scans a project tree for `.aeri` files and merges all validators and type
definitions into one preview blueprint JSON document.
Project scans skip generated and vendor directories such as `.git`, `.aeri`,
`target`, `build`, `dist`, and `node_modules`.
Pass `--artifacts <dir>` to write `blueprint.preview.json` plus one `.aeri.ir`
textual IR file per validator under `<dir>/scripts/`. These artifacts are not
serialized Cardano scripts.
When `aeri.toml` contains `name` and `version`, project builds use those values
in the blueprint preamble.
## Author And License
Aeri is authored by Trevor Knott of Knott Dynamics and distributed under the
MIT License.