ITF

ITF is an Elixir library for decoding and inspecting traces emitted by Apalache. It is tested against Apalache 0.58.3.

ITF only consumes .itf.json data. It does not execute Apalache, implement Victoria semantics, replay traces, or encode ITF.

Installation

Add itf to mix.exs:

{:itf, "~> 0.1.0"}

Usage

Load a trace from disk:

{:ok, trace} = ITF.load("counter.itf.json")
trace.vars
trace.states
trace.loop_index

Or decode an existing JSON binary:

{:ok, trace} = ITF.decode(json)

Both functions accept max_bytes: and max_depth: limits. The defaults are 256 MiB and 256 semantic expression levels; use :infinity explicitly to disable either limit. Invalid ITF returns a source-aware, path-aware ITF.Error. Invalid arguments or options raise ArgumentError.

Primitive values use native Elixir booleans, strings, and integers. Sequences are lists and records are maps. Ambiguous ITF forms stay distinct:

case value do
  %ITF.Set{values: values} -> {:set, values}
  %ITF.Map{entries: entries} -> {:map, entries}
  %ITF.Variant{tag: tag, value: payload} -> {:variant, tag, payload}
end

Tuples use ITF.Tuple and unserializable values use ITF.Unserializable. Set elements and map entries retain emitted order for inspection, but that order has no semantic meaning. Metadata and unknown trace/state extensions are preserved as raw JSON and are never expression-decoded.

The Rust code under test/oracle/ pins itf-rs 0.4.0 and is used only as an independent development/CI oracle for the shared subset. No Rust, Apalache execution code, fixtures, or tests are included in the Hex package.

Development

Install asdf 0.16.5 first. The root .tool-versions file is the authority for the exact versions of all project runtimes and command-line tools. On a new machine, bootstrap just once, then let the public setup recipe install the complete toolchain through asdf:

asdf plugin add just https://github.com/olofvndrhr/asdf-just.git
asdf install just
asdf exec just setup

Mix owns Hex and the dependencies locked in mix.lock; Cargo owns the oracle crates locked in test/oracle/itf_rs/Cargo.lock. The setup recipe does not replace either ecosystem's dependency installation.

just setup
just doctor
just deps
just check
just docs
just package-audit
just consumer-smoke
just test-oracle
just test-apalache

Ordinary mix test uses committed fixtures and requires neither Rust nor Apalache. just setup is the only toolchain-mutating workflow. The oracle and real-Apalache recipes are intentionally separate evidence lanes.

CI consumes the same version authority through specialized, commit-pinned Beam and Java setup actions. Its minimum lane is intentionally explicit at Elixir 1.18.4 and OTP 27.0 rather than reading the current Beam versions from .tool-versions. CI uses asdf only for just, Apalache, and Rust, then invokes the same public Justfile recipes used locally. Mix continues to own Hex and Elixir dependencies, and Cargo continues to own the Rust oracle dependencies.

Maintainer release

From a clean, synchronized main, run just release and review the guarded preflight summary before confirming the exact release tag. The command runs all release gates, publishes to Hex, pushes only the tag, and creates the GitHub release; partial failures require manual recovery.

License

MIT License. See LICENSE.