Aporia DSL

Aporia DSL

The Aporia DSL describes a numerical computation, parameter domains, outputs, and assumptions that APORIA can check. The compiler checks and lowers the model into A-IR before execution. The syntax documented here is the language implemented in software/crates/aporia-dsl; it is not a general-purpose programming language.

Example

model euler_decay "explicit Euler on exponential decay" {
  input dt in [0.001, 0.6]
  let k = 2
  state e = 1.0
  loop 41 {
    advance e = e - k * e * dt
    watch e
  }
  let final = e
  require final > 0
}

This follows the repository's software/benchmarks/ode/euler_decay/model.ap example. The supported forms visible in the parser and corpus include model, bounded input, let, state, counted loop, advance, watch, require, and check declarations.

Inputs and units

An input has a declared domain, either an interval or a finite choice set. An optional unit annotation gives it a physical dimension and scale. The unit checker compares both: km and m share a dimension but not a scale, so they are not silently interchangeable. Unit prefixes are an explicit table rather than generated productively; unsupported or ambiguous units produce diagnostics. Celsius is rejected because affine conversion requires an offset, while the unit representation models multiplicative scale.

Expressions are checked for dimensional compatibility, including function constraints such as dimensionless arguments to trigonometric or exponential functions. The count unit marks an integral quantity. A parameter domain must be constant; it cannot depend on another input.

State, traces, and rules

state declares an evolving quantity, advance assigns its next value inside a counted loop, and watch records a trace. A final let output or watched state can be observed. require encodes a model constraint such as positivity, bounds, finiteness, or an approximate equality with a tolerance. check declares supported behavioural relations such as monotonicity, scaling, symmetry, conservation within tolerance, or a Lipschitz bound. Supported relation forms and operand restrictions are enforced by the compiler; for example, symmetric parameters must have compatible quantity kinds and interchangeable domains for a swap execution to be valid.

Declared rules become evidence only when evaluated. A unit error rejected at compile time is not a runtime detection and is not counted as one in benchmark results.

A-IR

The compiler lowers the checked program into APORIA's three-address intermediate representation. A-IR carries parameters, domains, numeric types, dimensions, instructions, constraints, and relations. Its verifier checks structural invariants before execution, and its canonical text form preserves floating-point literals by their exact bits. The scalar interpreter executes this representation; the campaign itself now calls an Executor interface, but the shipped CLI input path is still .ap DSL.

For how DSL rules are used as evidence, see Evidence Model. For runtime traces and the campaign sequence, see How APORIA Works.

---

Home · Architecture · Evidence Model