itf

# 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`:

```elixir
{:itf, "~> 0.1.0"}
```

## Usage

Load a trace from disk:

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

Or decode an existing JSON binary:

```elixir
{: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:

```elixir
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:

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

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