Beacon

Beacon is the Chelis shell for bound-propagation verification over lowered Chelis RISC DAGs (v0.1.8).

What Beacon does

Beacon verifies properties of Chelis programs by propagating bounds through the compiled DAG representation. Given a WireDag, a set of named inputs, and a target output range, Beacon determines whether the program's output is guaranteed to fall within that range.

The verification pipeline:

1. Parses a serialized WireDag (schema v1 or v2).
2. Binds named scalar inputs to concrete values or boxes.
3. Propagates interval bounds forward through the DAG nodes.
4. Compares the resulting output bounds against the declared target range.
5. Emits a sound proved verdict when the propagated bounds satisfy the target range.

Oracle strategies

Beacon supports four oracle strategies that control how inputs are interpreted and how soundness is established:

• arb-point: singleton point inputs, fully sound.
• arb-box: interval box inputs, fully sound.
• arb-split: bounded splitting with coverage checks.
• zonotope-verified: zonotope lane with dependency tracking and Arb-verified branch-and-bound.

See Oracles for detailed semantics of each strategy.

Key properties

• Soundness: a proved verdict means the output range holds for all inputs in the declared domain. Beacon never emits proved unless the bounds fully satisfy the target.
• WireDag native: operates directly on the lowered RISC DAG representation, not on source-level Chelis.
• Certified artifacts: vendors the WI-13 erf envelope for sound erf bounding. See Erf envelope.