Целочисленное деление не даёт ядру нат — границу приходится называть постусловием
Выражение (х минус (х остаток от 4)) делить на 4 при х: нат даёт неотрицательное целое, но объявить такой функции возвращает нат нельзя: ядро отвечает «объявлена как нат, а тело даёт число». Значит там, где биты режутся делением (любой кодировщик — основание 64, проценты, шестнадцатеричное), тип неотрицательность не несёт, и границу надо называть постусловием руками: обеспечивает «шестёрка неотрицательна» результат не меньше 0.
Это меняет цену выбора. Общее правило «объявляй нат там, где значение неотрицательно» здесь не срабатывает не по невнимательности, а потому что вывод через деление ядру недоступен. Не тратьте время на попытки убедить объявлением — пишите два постусловия (нижняя граница и верхняя) и идите дальше.
Чем подтверждено. Ветка work/biblioteka, модуль flang/stdlib/base64.flang. Три функции подряд («Первая шестёрка», «Вторая шестёрка», «Третья шестёрка») отвергнуты этой диагностикой при объявлении возвращает нат; после смены на возвращает число и добавления восьми постусловий о границах модуль проверяется без диагностик, все 19 функций тотальны композицией, сторожей в напечатанном коде ноль.
Чем ограничено. Про остаток от без деления ничего не сказано — там неотрицательность на нат ядро выводит. Речь именно про деление.