# lawref.layers

*module*

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

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

**Чем этот вывод отличается от вывода компилятора — и почему это не дефект.**
`lawc` считает слой по ПОВЕРХНОСТИ: `classification` в LS [§2.3](https://github.com/arxohq/law/blob/master/spec/LAYERS-SURFACES.ru.md#23-точные-составы) числится
конструкцией L1, и компилятор поднимает слой по ключевому слову. Оракул
видит уже CLIR, где классификация — обычное правило своей силы: строгая
классификация после lowering-а требует ровно L0-механики.

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

* компилятор отвечает «какого слоя ПОВЕРХНОСТЬ автор написал» — по нему
  считается заявка пакета и работает `LDC-E8101` над исходником;
* оракул отвечает «какой слой МЕХАНИКИ нужен, чтобы это исполнить» — по
  нему проверяется conservativity LS [§2.4](https://github.com/arxohq/law/blob/master/spec/LAYERS-SURFACES.ru.md#24-слой--это-conservative-fragment-а-не-диалект) (режим `--layer` выключает
  механику выше слоя, и результат обязан не измениться).

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

**Слой программы — не слой вычисления.** Программа T003 состоит из строгих
правил и фактов, то есть по механике L0; но дело подаёт `P` и `not P`
одновременно, а L0 на такой вход обязан остановиться с `CONFLICTED_INPUTS`
(LS [§2.3](https://github.com/arxohq/law/blob/master/spec/LAYERS-SURFACES.ru.md#23-точные-составы)), тогда как L1 сохраняет неоднозначность [§112](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/16-part-xv-defeasible-semantics-and-conflict-resolution.ru.md#112-ambiguity-policy). Слой вычисления
считается по паре «программа + дело», и `infer` отвечает только за первую
половину. Поэтому вывод этого модуля — нижняя граница, а не приговор: он
говорит «меньше этого не хватит», а не «этого достаточно».

## lawref.layers.LAYER_EXCEEDED

*attribute* · *module attribute*

```python
LAYER_EXCEEDED = 'LDC-E8101'
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/layers.py#L38-L38)

## lawref.layers.ORDER

*attribute* · *module attribute*

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/layers.py#L36-L36)

## lawref.layers.check_declared

*function*

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

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

Молчание здесь — не «всё хорошо», а «объявленного слоя хватает»: заявка
ниже фактической потребности означала бы, что исполнитель слоя вернёт
другой результат, чем полный движок, а слой обещает обратное ([§2.4](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/01-part-i-audit.ru.md#24-не-была-определена-точная-модель-defeasible-вывода)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/layers.py#L143-L163)

## lawref.layers.findings

*function*

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

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/layers.py#L108-L134)

## lawref.layers.infer

*function*

```python
def infer(document: dict) -> str
```

Слой механики, необходимой для исполнения программы (LS [§2.2](https://github.com/arxohq/law/blob/master/spec/LAYERS-SURFACES.ru.md#22-определение-слоёв)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/layers.py#L137-L140)