WireDag format
Beacon operates on WireDag files: the serialized RISC DAG representation produced by the Chelis compiler's lowering pass. This page describes the format and how Beacon interprets it.
Schema versions
Section titled “Schema versions”Beacon parses two schema versions:
- v1: the original WireDag layout.
- v2: extended schema with additional node metadata.
Both versions are accepted transparently. Beacon detects the schema version from the file header.
Integrity checking
Section titled “Integrity checking”Beacon accepts serialized WireDag bytes together with an expected SHA-256 hash. Before parsing, it computes the hash of the raw bytes and rejects the file if the hash does not match. This ensures the DAG has not been modified after compilation.
chelis-beacon check model.wiredag --sha256 <expected-hash> --oracle arb-point --input x=1.5 --output-range '[0.0, 2.0]'Structure
Section titled “Structure”A WireDag file encodes:
| Component | Description |
|---|---|
| Root index | The node index at which Beacon begins backward traversal to determine which nodes contribute to the output. |
| Named scalar input boxes | One or more named inputs, each bound to a scalar value or interval at invocation time. |
| Output range | A single closed interval declaring the property to verify. |
| Node array | The DAG nodes themselves (arithmetic ops, constants, function applications). |
ConstTensor ops
Section titled “ConstTensor ops”ConstTensor literal ops embed tensor data directly in the DAG. Beacon models these by hulling the finite, non-empty tensor data to the interval [min(data), max(data)]. This is sound: any element of the tensor is contained in the hull, so downstream arithmetic that depends on the constant is bounded correctly.
ConstTensor nodes are targetable, meaning the user can inspect their modeled intervals in diagnostic output.