lawref.layers

Слой программы по CLIR — вторая половина law.layers/0.1 в оракуле.

Первая половина (LDC-E8102, слой зависимости выше слоя пакета) живёт в resolver. Здесь — вывод слоя САМОЙ программы и LDC-E8101, когда она требует механики выше объявленного слоя.

Чем этот вывод отличается от вывода компилятора — и почему это не дефект. lawc считает слой по ПОВЕРХНОСТИ: classification в LS §2.3 числится конструкцией L1, и компилятор поднимает слой по ключевому слову. Оракул видит уже CLIR, где классификация — обычное правило своей силы: строгая классификация после lowering-а требует ровно L0-механики.

Это два разных вопроса, и оба законны:

• компилятор отвечает «какого слоя ПОВЕРХНОСТЬ автор написал» — по нему считается заявка пакета и работает LDC-E8101 над исходником;
• оракул отвечает «какой слой МЕХАНИКИ нужен, чтобы это исполнить» — по нему проверяется conservativity LS §2.4 (режим --layer выключает механику выше слоя, и результат обязан не измениться).

Инвариант между ними: семантический слой ≤ поверхностного. Обратное означало бы, что lowering вносит механику, которой в исходнике не было, — это дефект, и его ловит verify/ci/gates/compiler/check_layer_inference.py.

Слой программы — не слой вычисления. Программа T003 состоит из строгих правил и фактов, то есть по механике L0; но дело подаёт P и not P одновременно, а L0 на такой вход обязан остановиться с CONFLICTED_INPUTS (LS §2.3), тогда как L1 сохраняет неоднозначность §112. Слой вычисления считается по паре «программа + дело», и infer отвечает только за первую половину. Поэтому вывод этого модуля — нижняя граница, а не приговор: он говорит «меньше этого не хватит», а не «этого достаточно».

Attributes

Name	Description
LAYER_EXCEEDED	No description.
ORDER	No description.

Functions

Name	Description
check_declared	LDC-E8101: программа требует механики выше объявленного слоя.
findings	Конструкции, поднявшие слой: [(слой, что именно)], тяжёлые первыми.
infer	Слой механики, необходимой для исполнения программы (LS §2.2).

LAYER_EXCEEDEDattributemodule attribute#

View source

LAYER_EXCEEDED = 'LDC-E8101'

ORDERattributemodule attribute#

View source

ORDER = {'L0': 0, 'L1': 1, 'L2': 2, 'L3': 3}

check_declaredfunction#

View source

def check_declared(document: dict, declared: str) -> list[dict]

LDC-E8101: программа требует механики выше объявленного слоя.

Молчание здесь — не «всё хорошо», а «объявленного слоя хватает»: заявка ниже фактической потребности означала бы, что исполнитель слоя вернёт другой результат, чем полный движок, а слой обещает обратное (§2.4).

findingsfunction#

View source

def findings(document: dict) -> list[tuple[str, str]]

Конструкции, поднявшие слой: [(слой, что именно)], тяжёлые первыми.

inferfunction#

View source

def infer(document: dict) -> str

Слой механики, необходимой для исполнения программы (LS §2.2).