index.cast

← index dialect

Explicit integer conversion at an address boundary. Index uses a signed target-selected carrier and offset uses an independently selected unsigned carrier. Entering either address domain maps i1 false and true to 0 and 1. Entering index interprets other fixed-width payloads as signed. Entering offset zero-extends the raw bits of narrower fixed-width payloads; an i64 payload must already be nonnegative because offset's source fact domain is [0, INT64_MAX]. A range proof must describe the input; an assumption on the cast result cannot justify the conversion. A target requiring a narrower address carrier accepts only values proven representable in that carrier. Leaving an address domain follows its signedness and preserves the low destination-width bits when narrowing, including casts to i1. Conversion between index and offset requires the numeric value to be representable in the destination domain. Pure fixed-width integer changes use scalar.extsi, scalar.extui, or scalar.trunci.

Operation contract

Property	Value
Semantic phase	executable
Traits	Pure, DistributionTransfer

Signature

Kind	Name	Type	Cardinality	Description
Operand	input	scalar	required	—
Result	result	scalar	required	—

Examples

%i = index.cast %n : i64 to index

%bytes = index.cast %raw : i64 to offset

%n = index.cast %i : index to i64