Module chiplet 

Independent AIR Chiplet definitions.

A ChipletDef snapshots a chiplet’s full AIR (constraints, layout, bus specs) into an owned struct. The prover runs an independent ZeroCheck per chiplet. The bus (GPA) reconnects chiplets to the main trace.

Structs

ChipletDef

Pre-computed chiplet AIR definition.

CompositeChiplet

Build-time composition of peer chiplets into a single unit.

CompositeChipletBuilder

Builder for CompositeChiplet.

Functions

compose_chiplet_defs

Flatten multiple composites into a single chiplet def list.

compose_external_buses

Collect external buses from multiple composites.

unconstrained_bit_selectors

Non-paired Bit selectors with no direct s·s + s boolean root, each tagged with the declaring bus_id. Advisory only: booleanness can hold indirectly (one-hot, disjoint products), callers warn rather than reject.

validate_paired_bus_mutex

Without the mutex root, both selectors high collapse the bus numerator to zero in char-2; without the boolean roots, the mutex admits non-zero field-element selectors that bypass binary on/off semantics.