Weights and large models

Hydronnx emits every ONNX initializer as a Chelis source literal: every weight value becomes a cast(<float>, f32) inside a to_tensor([...]) call. That keeps the generated module self-contained, and it is exactly the right form for small models. It does not scale: a model with millions of parameters would become hundreds of megabytes of .ch before the compiler could type-check it.

This chapter explains the inline-emit ceiling, what is and is not blocked by it, and the two paths that work around it: the placeholder-weight emit mode and the runtime path. It also documents the .hnw sidecar archive, the binary weight format used by the runtime path.

Types versus values: what each operation needs

The inline-weight ceiling is a source-text artifact, not a runtime limit, and it blocks less than it appears. Most of Hydronnx's value (type discipline, composition, structural proofs) needs only the declared types of the weights, not their values.

Operation	Needs weight values?	Why
chelis check (shape, dim, rank, dtype discipline; composition)	No, types only	Type inference reads the sig and structure; it never computes weight values.
chelis prove, SMT tier (output shape, softmax sums to 1, activation bounds)	No	These discharge symbolically; the prover runs nothing.
AD lowering (does grad lower for this op surface)	No	Structural: it differentiates the graph, not specific numbers.
chelis prove, sampling tier (fallback when SMT cannot close)	Some, not necessarily real	The prover zero-fills unbound weights, so weight-independent properties run on placeholder zeros.
chelis test / numeric parity against an ONNX Runtime golden	Yes, real	The whole point is the actual numbers.
Weight-dependent proofs ("this trained net predicts class 0 on region R")	Yes, real	Truth depends on the specific trained weights.

So "weights are inline only" is narrowly true: only the numeric-fidelity source path is bound by the ceiling. The type-discipline and structural-provability value does not need the weight values at all.

Inline literals: the default path

Inline emit is the default and the right choice for small models: tabular models, small MLPs, small transformer encoders, and small Conv-bearing image classifiers. The generated module is one self-contained .ch file with no external dependency, browsable and diffable.

The growth is linear in parameter count, so the inline path fits models whose largest weight stays small. The emitter enforces this with a per-weight element cap; a weight over the cap rejects with WeightTooLarge (WeightConversionFailure at the CLI). Real vision-scale and NLP-scale models exceed the cap, so for those models you reach for one of the paths below.

The f64 precision caveat applies to inline mode: chelis lexes every float literal at f32 precision, so an f64 weight initializer is emitted at f32 precision regardless of the original tensor's dtype. The fixtures are f32, so this rarely bites; an f64 model declares the problem in its weight emit.

Placeholder mode: type discipline at any size

chelis-hydronnx-emit --weights placeholder writes the real graph and signatures but emits each weight as a compact shaped placeholder (one literal element expanded and reshaped to the declared shape) instead of per-element literals. The .ch stays proportional to the graph structure, not the parameter count, so it type-checks, composes, and discharges SMT-tier @property proofs for any model size.

• Gains: the type-discipline and structural-provability value, the core of Hydronnx, delivered for large models with no extra Chelis feature. You can check that your forward composes and prove shape and structural invariants without loading weights.
• Loses: the numbers are placeholders, so chelis test parity and any weight-dependent proof are meaningless in this mode.

A worked illustration: a real ResNet18 is operator-complete and runnable in placeholder mode. With Flatten and MaxPool padding implemented, every one of its nodes emits; --weights placeholder turns its over-ceiling weights into shaped zeros, and the result chelis checks clean and executes end to end (a [1, 3, 224, 224] input runs through to [1, 1000] logits via chelis test). The numbers are placeholder zeros: this confirms the emit, compile, execute pipeline carries a real CNN's full structure, not numeric correctness.

The runtime path: real weights, no source ceiling

chelis-hydronnx-run executes a model with its real weights through the translate and chelis-ir eval path. translate_model lowers ONNX to a chelis-ir Dag and carries the initializers as in-memory tensor values of any size; the interpreter runs the DAG with the weights handed in at eval time. There is no inline-source weight ceiling. A real ResNet18 reproduces ONNX Runtime's logits to about 1e-6 this way.

This is the runtime product, not the typed-source product. There is no emitted .ch, so no chelis check, no chelis prove, and no composition with hand-written Chelis. It is Hydronnx as an ONNX runtime on chelis-ir, a different surface from the "emit a typed forward" promise. Verify the architecture with chelis-hydronnx-emit --weights placeholder; run the numbers with chelis-hydronnx-run. See its CLI reference.

The numeric-source path

The remaining goal is numeric parity (chelis test) and weight-dependent proofs as typed Chelis source: real weight bytes inside a compiled module. This needs a Chelis language feature that does not exist: typed external constants. A compiled .ch module currently has no way to reference weight values from an external file; inline literals are the only way to get the actual numbers into compiled Chelis source, which is the entire reason for the size ceiling.

The intended source form binds each weight to a typed external constant, for example:

sig w1: tensor[4, 6, f32]
extern weight w1 from "irisclassifier.hnw" tensor "w1" sha256 "<tensor-sha256>"

The value would be materialized as an immutable compile-time constant, so the type checker, chelis prove, AD, and lowering all treat it exactly like a to_tensor literal. This preserves the entire typed-source value (a typed forward, chelis prove, composition, deterministic build-time validation, and exact f64 bytes) for large models. It depends on the upstream Chelis feature landing.

The .hnw sidecar archive

Hydronnx has a deterministic .hnw archive writer and reader as an internal Rust library module, and chelis-hydronnx-run exercises it end to end: --export-weights writes every initializer to an archive at its native dtype, and --weights runs a model with the archive's values as the eval-time weight source (checksum-verified, shape-checked, bit-identical round-trip). The archive is not wired into chelis-hydronnx-emit: generated Chelis does not emit typed external constants, so this is a validation surface for the archive core, not an inline-replacing emit path. The emitted .ch cannot reference an archive.

Format goals

• Emitted source size proportional to graph structure, not parameter count.
• Shape and dtype checking stay in Chelis source. The sidecar stores bytes; it is not a dynamic shape authority.
• Exact initializer values preserved, including f64 precision that inline Chelis float literals lose.
• Deterministic build and runtime failures: wrong sidecar, missing tensor, checksum mismatch, shape mismatch, and dtype mismatch all fail before inference silently runs.
• Simple enough to inspect and test without ONNX Runtime.

Archive layout

The sidecar is one packed binary file, not a directory of tensor files. One file is easier to copy, attach to releases, and checksum atomically.

offset  size  field
0       8     magic: "HNXWGT\0\1"
8       4     header_len_le, including this fixed header
12      4     manifest_len_le
16      32    sha256(manifest_json_bytes)
48      32    sha256(payload_region_bytes)
80      n     reserved header extension bytes, zero
...     m     UTF-8 manifest JSON
...     p     payload region, tensor bytes at manifest offsets

All integers are little-endian. The payload region begins immediately after the manifest and is padded to a 64-byte boundary. Each tensor payload is also 64-byte aligned. Alignment is not semantically visible; it exists for mmap and backend loaders. The magic byte includes the major format version; minor feature versioning lives in the manifest so old loaders can reject unknown required features before touching tensor bytes.

Manifest

The manifest is canonical JSON: UTF-8, object keys sorted lexicographically, no insignificant whitespace, integers as JSON numbers, checksums as lowercase hex. Canonical encoding keeps archive generation byte-stable. It records the format version, the producer and source provenance, the module name and a digest of the generated source, the payload length and checksum, and a per-tensor list. Each tensor entry carries:

• id: deterministic Hydronnx identifier used by generated Chelis, stable across machines for the same model and emit options.
• onnx_name: original ONNX initializer name, for diagnostics.
• dtype: f32, f64, i32, i64, or bool.
• shape: logical ONNX tensor shape after parser normalization.
• layout: onnx-row-major. Operator-specific transposes stay in generated graph code, not hidden in the sidecar.
• encoding: raw-le.
• offset and byte_len: position and exact length in the payload region.
• sha256: checksum of this tensor's encoded bytes.
• consumer: generated Chelis definition expected to load this tensor.

A loader rejects unknown values in the format major version, tensor dtype, layout, or encoding.

Tensor encoding

Dense tensors are stored exactly once, in ONNX initializer element order:

Hydronnx dtype	Encoding
f32	IEEE-754 binary32, little-endian
f64	IEEE-754 binary64, little-endian
i32	two's-complement signed 32-bit, little-endian
i64	two's-complement signed 64-bit, little-endian
bool	one byte per element, 0 or 1 only

The expected byte length is num_elements(shape) * dtype_width(dtype). The writer fails if the ONNX initializer data length disagrees, and the reader verifies the same equation before constructing a tensor.

Error model

Sidecar failures surface as distinct errors instead of generic IO: archive missing, archive malformed, archive version unsupported, archive checksum mismatch, tensor missing, tensor metadata mismatch, and tensor checksum mismatch. Diagnostics include both the generated module name and the ONNX initializer name when available.

Choosing a path

• Small model, want a typed forward with real numbers: inline emit (the default).
• Large model, want type discipline, composition, and structural proofs: --weights placeholder.
• Large model, want to run it with real numbers: chelis-hydronnx-run (the runtime path, optionally backed by a .hnw archive).
• Want real numbers as typed source for a large model: this awaits the upstream Chelis typed-external-constant feature.
• Cannot wait and must use inline: shrink, distill, or quantize the model so its largest weight fits under the inline ceiling. This is an escape hatch, not a fix; most real models cannot be shrunk that far without retraining.