# Aeri
Aeri is the official 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 deterministic pure tests, formats and lints source,
and compiles the supported language subset to Plutus V2 UPLC/CBOR.
## Aeri Language
`Aeri` defines its own `.aeri` language for writing typed validators,
helpers, custom data types, constants, pattern matches, and pure tests.
The toolchain provides the core flow for every project:
- create projects
- check types
- run tests
- format and lint sources
- inspect lowering and readiness
- estimate costs and generate docs
- 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 textual Aeri IR in preview-blueprint JSON
- sets `target: "aeri-text-ir"`
- sets `cardanoDeployable: false`
- `--target uplc`
- emits Plutus Script V2 JSON and CBOR hex for supported validators
- verifies generated script hashes with `cardano-cli transaction policyid`
when available from `PATH` or `AERI_CARDANO_CLI`
The UPLC path is intentionally gated.
- Supported today: `tx_signed_by`, `tx_has_datum`
- Explicit blockers remain for most transaction context decoders (`tx_paid_to`,
`tx_after`, etc.), constructor field encoding, unsafe shortcut forms, and
several list-value edge cases
- Nullary constructors and direct pattern matches are supported when all nested
fields remain in the supported value set.
```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.