Introduction

Hydronnx is an ONNX onramp for Chelis. It reads an .onnx model file ahead of time and emits a typed Chelis function module. From your Chelis program, the loaded model is an ordinary function: type-checked at every call site, attachable to @property blocks for chelis prove, and composable with hand-written Chelis end to end.

The three-step workflow

# 1. Inspect: see what the model contains and whether it is in scope.
chelis-hydronnx-inspect model.onnx

# 2. Emit: generate a typed Chelis module. Build-time; do this once per model.
chelis-hydronnx-emit model.onnx -o src/mymodel.ch

# 3. Use: import the emitted module and call it like any Chelis function.
#    import Hydronnx.MyModel (forward)
#    def predict(x) = top_class(forward(normalize(x)))
chelis test     # compile, run, check end-to-end
chelis prove src/mymodel.ch --samples 64 --seed 0   # verify @property blocks

See Loading a model for the walkthrough against the worked example.

What Hydronnx is for

Hydronnx delivers type discipline, property verification, and composition. The emitted forward is a typed Chelis function whose input and output shapes are part of its signature, so every call site is checked at compile time. You can attach @property blocks and verify them with chelis prove, and you can thread the model through hand-written Chelis pre- and post-processing with the whole pipeline type-checked end to end.

For raw inference throughput, broad vision models, or hardware reach (GPU, mobile NPU), ONNX Runtime is the right tool. The migration guide covers the trade-off in detail.

Scope, in brief

Hydronnx emits weights as Chelis source literals, so the inline-emit path fits small models: tabular classifiers, small MLPs, small transformer encoders, and windowed pooling and single-Conv image-classifier graphs. A multi-megabyte model does not fit the inline path. The honest, complete account is in Limitations and scope, and the weight story is in Weights and large models.

A separate runtime path runs a model with its real weights without the inline-source ceiling. chelis-hydronnx-run executes a model through the translate and chelis-ir eval path. Weights are an eval-time in-memory map, not source text, so there is no size ceiling: a real ResNet18 reproduces ONNX Runtime's logits to about 1e-6. This is the runtime product, not the typed-source product. Nothing it runs is chelis checked or provable. Verify the architecture with chelis-hydronnx-emit --weights placeholder; run the numbers with chelis-hydronnx-run.

Worked examples

Two complete reef projects ship with the repository and are exercised by the test suite on every build, so the commented commands cannot drift from the code.

• examples/tabular_classifier/ is a small tabular classifier: 4 features map to 3 class probabilities through Gemm, Relu, and Softmax. The example's tests/example.ch checks that the emitted forward matches ONNX Runtime's golden output within 1e-3, and the bundled property snippet verifies that the three softmax outputs always sum to 1.
• examples/image_classifier/ is a small Conv-bearing image classifier covering the inspect, emit, check, test workflow on a Conv to Relu to GlobalAveragePool to Reshape to Gemm to Softmax graph.

License

MIT.