aeri 0.2.4

Aeri is a Cardano smart contract language by Knott Dynamics, created by Trevor Knott, with its official compiler and CLI.
Documentation

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:

cargo install aeri

Create and verify a project:

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.

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.
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.

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";
  require signed || datum_equals(datum, datum);

  matured && redeemer == #01
}

Custom redeemers can be modeled directly and checked exhaustively with match:

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:

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:

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.

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.

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:

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.