Числовая модель

Реализованы все восемь целых фиксированной ширины, bool, контекстные литералы, checked/wrapping +, -, *, отрицание signed, сравнения, логика с коротким замыканием, побитовые операции, сдвиги, деление и остаток. Насыщение и преобразования ниже остаются проектами и не входят в доступный синтаксис. Точное работающее подмножество описано в спецификации ядра.

Типы и значения

Доступные целые: u8/u16/u32/u64 и i8/i16/i32/i64. Для ширины N беззнаковый диапазон — от 0 до 2^N − 1, знаковый — от −2^(N−1) до 2^(N−1) − 1. Ширина не зависит от архитектуры. bool остаётся отдельным типом, не числом.

Платформозависимые int и uint в Core не вводятся. Возможный будущий тип индекса требует собственного контракта, а не неявного совпадения с шириной адреса.

Для арифметики фиксируем одинаковый тип обоих типизированных операндов: смешение знаковых и беззнаковых типов и изменение ширины требуют явного преобразования. Неявное расширение запрещено так же, как сужение.

Константы и типизированные вычисления

Компилятор использует произвольную точность математических целых констант на этапе компиляции. При выборе конкретного типа проверяется диапазон. Это не вводит runtime bigint и не делает операции типизированного целого операциями произвольной точности.

Нужно различать три случая:

Случай	Правило
Математическая константа до выбора типа	Точное целое без машинного переполнения
Приведение константы к конкретному типу	Проверка диапазона; непредставимое значение — ошибка компиляции
Вычисление над уже типизированными операндами	Правила checked/wrapping/saturating выбранного типа, даже если входы известны компилятору

Например, MAX + 1 - 1 для уже типизированных checked-операндов не может быть заменено на MAX: первая операция обязана вызвать trap при её исполнении. Свёртка констант сохраняет этот отказ и не превращает trap в ошибку типизации лишь потому, что оптимизатор смог заранее вычислить результат.

Контекстная типизация

Литерал получает конкретный тип из аннотации привязки, объявленного результата функции, параметра вызова или второго, уже типизированного операнда. Контекст распространяется через скобки и арифметические операции. Типы уже типизированных значений не меняются: несовместимые ограничения дают ошибку. Сначала проверяется типизированный операнд, независимо от того, стоит он слева или справа. Литералы не заставляют его расширяться.

Если тип целочисленного выражения нельзя определить из контекста или его типизированных операндов, выбирается u32. Это сохраняет правило текущего прототипа. Минимальный подходящий тип по значению не подбирается. Поэтому голая привязка отрицательного литерала потребует явного знакового контекста, например аннотации i32.

Примеры типизации (строки с ошибкой или trap показаны отдельно для иллюстрации):

a: u8 = 42          // литерал проверяется как u8
b: u8 = 256         // ошибка диапазона литерала
c: i16 = -100       // отрицательный литерал проверяется как единое значение
x: u8 = 255
y = x + 1          // литерал 1 получает u8; checked-сложение вызывает trap
z = 1 + x          // те же типы и тот же trap
plain = 42         // без контекста — u32

Минус непосредственно перед числовым литералом участвует в определении его математического значения до проверки диапазона. Поэтому -128 допустим в контексте i8, без промежуточного положительного 128 типа i8. Отрицание типизированного значения — отдельная checked-операция; отрицание знакового MIN требует trap.

Обычные арифметические выражения сначала типизируются, потом вычисляются по правилам типа, даже если все листья — литералы. Например, привязка x: u8 = 255 + 1 - 1 должна сохранить trap. Произвольная точность служит для представления литералов и независимых математических расчётов компилятора; она не превращает обычное исходное выражение в нетипизированный bigint-расчёт. Отдельный пользовательский режим математических константных выражений пока не вводится.

При сравнении тип результата bool не задаёт тип числовых операндов: он выводится из самих операндов либо выбирается u32 для двух литералов. Проверка обеих веток сохраняется: литерал вне диапазона — ошибка исходника даже в неисполняемой ветке, но корректно типизированное checked-переполнение в такой ветке не исполняется и не превращается в обязательную диагностику.

Три политики арифметики

Политика	Результат	Статус
Checked	Точный математический результат, если он представим; иначе trap	`+`, `-`, `*` для всех целых реализованы
Wrapping	Результат по модулю 2^N	`+%`, `-%`, `*%` для всех целых реализованы
Saturating	Результат ограничивается нижней/верхней границей типа	Запланировано; `+\|` — предложение синтаксиса

Для знакового wrapping фиксируем интерпретацию полученных N бит как дополнительного кода: диапазон результата остаётся знаковым. Это правило значений, а не требование к представлению данных целевым процессором.

Checked-ошибка сейчас завершает программу через trap: не возвращает Result, не допускает продолжения с усечённым значением, не является UB. Фиксированное сообщение, конкретный сигнал и код завершения не гарантируются. Оптимизация не вправе удалять исполняемую потенциально падающую операцию только потому, что её результат не используется. Невыбранная ветка не исполняется.

При расширении целых сохраняем этот контракт, пока отдельное решение не изменит спецификацию. Восстановимая ошибка арифметики должна иметь отдельную операцию с явно возвращаемым результатом после появления Result.

Преобразования

Неявное сужение запрещено. Нужно различать две операции:

Проверяемое преобразование сохраняет математическое значение, если оно представимо в целевом типе; иначе trap, согласованный с checked-арифметикой.
Явно усекающее преобразование задаёт результат по модулю 2^N целевого типа; для знакового назначения результат интерпретируется как дополнительный код.

Такое определение явно покрывает отрицательные значения и смену знаковости. Проверяемое расширение знакового отрицательного значения в беззнаковый тип тоже может завершиться ошибкой, несмотря на увеличение ширины.

as и отдельное обозначение усекающего преобразования пока не утверждены. До реализации нужно выбрать синтаксис, правила литералов и диагностик. Одна операция не должна незаметно переключаться между проверкой и усечением.

Логика, биты и сдвиги

Для && и || реализовано короткое замыкание: правая часть вычисляется только при необходимости. Обе части проверяются статически и имеют тип bool. ! уже определён только для bool.

Побитовые операции работают с N-битным представлением целого. Их результаты не зависят от endian хоста.

Сдвиги реализуют следующие правила:

Операция	Семантика
`x << n`	N-битный сдвиг влево; вышедшие старшие биты отбрасываются
`x >> n`, unsigned	Логический сдвиг вправо с нулевым заполнением
`x >> n`, signed	Арифметический сдвиг вправо со знаковым заполнением
Счётчик `n`	Тип `u32`, независимо от ширины и знаковости `x`
`n >= N`	Trap при исполнении
Отрицательный литерал или signed-счётчик	Ошибка типизации; неявного преобразования в `u32` нет

Нетипизированный литерал счётчика получает u32. Счётчик, уже имеющий другой целый тип, потребует явного проверяемого преобразования после появления такого синтаксиса. Например, 64 — допустимый литерал u32, но для сдвига u64 вызывает runtime trap. Этот случай отличается от отрицательного литерала, который не проходит типизацию счётчика.

Результат имеет тип левого операнда. Знаковый левый сдвиг выполняется над N-битным дополнительным кодом, затем биты интерпретируются в исходном знаковом типе. Арифметического переполнения при таком сдвиге нет. Таким образом, для u8 со значением 128 сдвиг влево на 1 даст 0, а checked-сложение этого значения с самим собой вызовет trap.

Проверка счётчика выполняется до машинного сдвига; маскирование величины конкретным CPU не становится правилом языка. Сдвиг не равен checked-умножению: замена одного другим допустима только с доказательством сохранения семантики.

Деление и остаток

/ и % реализованы для всех восьми целых типов. Операнды имеют одинаковый тип; нетипизированные литералы получают его из контекста. Приоритет совпадает с умножением, ассоциативность — слева направо.

Частное округляется к нулю, ненулевой остаток имеет знак делимого. В математических целых выполняется a = (a / b) * b + (a % b); это тождество не разрешает вводить переполнение в промежуточных операциях.

Случай	Результат
`a / 0`, `a % 0`	Trap при исполнении
Signed `MIN / -1`	Trap: частное не представимо
Signed `MIN % -1`	0: остаток представим, частное не вычисляется
`-7 / 3`, `7 / -3`	−2
`-7 % 3`, `-7 % -3`	−1
`7 % -3`	1

Неисполняемая ветка или короткозамкнутый операнд не вызывает trap. Неиспользуемый результат не разрешает устранять обязательную проверку. Нулевой делитель в корректно типизированном выражении не является ошибкой типизации, даже если он известен компилятору.

Независимость от backend

IR должен сохранять ширину, знаковость, арифметическую политику и вид преобразования. Нельзя восстанавливать их из выбранных LLVM-инструкций или подразумеваемых флагов переполнения. Одинаковый вход должен давать одинаковое значение либо определённый отказ при разных уровнях оптимизации и на поддерживаемых архитектурах.

Checked-операции понижаются через signed/unsigned overflow intrinsics и переход к trap. Wrapping — через обычные операции без nsw/nuw. Проверки делителя и величины сдвига должны предшествовать опасным инструкциям. LLVM srem также имеет UB для MIN % -1. Backend Liza заменяет делитель −1 на +1 перед srem: остаток остаётся нулём, опасная инструкция не исполняется. Эти ограничения следуют из LLVM Language Reference.

Критерий завершения этапа

Каждая доступная операция определена на всех входах: значение, ошибка типизации или предусмотренный runtime trap.
У каждой ширины и знаковости проверены границы, переполнение и преобразования.
Позитивные, негативные и trap-проверки выполняются при O0 и O2; сравниваются полные значения, а не только младшие биты кода завершения.
Неисполняемые ветки и короткозамкнутые операнды не вызывают trap или эффектов.
Исходный LLVM IR не содержит необоснованных nsw, nuw, inbounds и других обещаний, нарушение которых меняет определённое поведение Liza.
Один набор проверок выполняется минимум на двух подтверждённых архитектурах при наличии соответствующей инфраструктуры. Два названия ОС сами по себе не являются подтверждением двух архитектур.

Одной проверки перечисленных флагов недостаточно для отсутствия UB: деление, остаток и сдвиги требуют собственных проверок. Оптимизатор может добавить флаги только после доказательства их предусловий.

Отдельный следующий вопрос — значение, битовое представление и кодирование.