Skip to content
Chelis docs

Scope and limitations

WI-B4 linear-relaxation groundwork

Section titled “WI-B4 linear-relaxation groundwork”

The WI-B4 linear-relaxation subsystem is internal only. It contains:

  • Affine and backward relaxation forms.
  • A correlation-preserving join scorecard.
  • Opt-in transformer tests for Exp, Log, Sqrt, Recip, and Div.

However, WI-B4 has no public CLI domain, no oracle selector, no dispatch surface, and no trusted proof lane. It is not accessible through the chelis-beacon command.

arb-oracle feature flag

Section titled “arb-oracle feature flag”

The arb-oracle feature is optional. It requires the arb-oracle feature flag at build time. Builds without this flag omit the arb-point, arb-box, and arb-split oracles entirely, leaving only zonotope-verified.

If you installed via chelis reef install, the default binary includes the arb-oracle feature. Custom builds must opt in explicitly.

Model size

Section titled “Model size”

Beacon uses an inline DAG representation. Models stay small: the entire WireDag is loaded into memory as a flat node array. This is appropriate for the verification targets Beacon is designed for (individual functions and small subgraphs), not for whole-program DAGs with millions of nodes.