Skip to content
Arxo Law

lawref.lawtest

Исполнение теста §267 оракулом.

Оракул не разбирает .lawtest — парсер живёт в компиляторе, и второго фронтенда здесь не заводится. На вход приходит УЖЕ ПОНИЖЕННЫЙ тест-документ (lawc lower-test): title + case + query + expectations.

Зачем оракулу свой раннер, если документ вычисления уже под байтовым контрактом. Байты сравнивает check_differential; здесь сравнивается ВЕРДИКТ — то есть ещё одно место, где реализации могут разойтись: сопоставление ожидания §267 с полем результата §174. Оно короткое, но своё у каждой стороны, и молчаливое расхождение здесь означало бы, что один и тот же тест на двух тулчейнах даёт разные ответы. §269 объявляет обмен тестами между независимыми реализациями — значит вердикт обязан быть предметом differential, а не доверия.

Attributes

NameDescription
EXPECT_FIELDSNo description.
EXPECT_VOCABULARIESNo description.
SEVERITY_ORDERNo description.

Functions

NameDescription
check_expectationsСопоставление ожиданий §267 с документом вычисления §174.
declared_idsОбъявленные символы программы: id узлов плюс id параметров отношения
expect_vocabularyСловарь перечислимого поля §174.1; None — словаря у поля нет.
free_generator_refs(id переменной comprehension, id const_ref) для каждой ссылки на
run_propertyВердикт по свойству §270: {"name", "domain", "counterexamples", "skipped"}.
run_testВердикт по тест-документу: {"title", "passed", "failures"}.

EXPECT_FIELDSattributemodule attribute#

View source
EXPECT_FIELDS = {
  'applicability_status': 'applicabilityStatus',
  'evaluation_status': 'evaluationStatus',
  'normative_status': 'normativeStatus',
  'result_kind': 'resultKind',
  'trigger_status': 'triggerStatus',
  'truth_status': 'truthStatus',
  'value': 'value'
}

EXPECT_VOCABULARIESattributemodule attribute#

View source
EXPECT_VOCABULARIES = {
  'applicability_status': 'ApplicabilityStatus',
  'evaluation_status': 'EvaluationStatus',
  'normative_status': 'NormativeStatus',
  'result_kind': 'ResultKind',
  'trigger_status': 'TriggerStatus',
  'truth_status': 'TruthStatus'
}

SEVERITY_ORDERattributemodule attribute#

View source
SEVERITY_ORDER = {'none': -1, 'info': 0, 'warning': 1, 'error': 2, 'fatal': 3}

check_expectationsfunction#

View source
def check_expectations(expectations: list[dict], evaluation: dict, ir: dict) -> list[str]

Сопоставление ожиданий §267 с документом вычисления §174.

Вынесено из run_test отдельной функцией: её зовёт и раннер, и сверка переноса сценариев, которой нужно применить ожидания к ПОДМЕНЁННОМУ документу без запуска движка.

declared_idsfunction#

View source
def declared_ids(ir: dict) -> set[str]

Объявленные символы программы: id узлов плюс id параметров отношения §45.1. Список тот же, что строит unresolved_refs в law-hir/src/lower/mod.rs, — и он ОБЯЗАН быть тем же: иначе одно и то же имя было бы свободной переменной у одной реализации и константой у другой.

expect_vocabularyfunction#

View source
def expect_vocabulary(field: str) -> list[str] | None

Словарь перечислимого поля §174.1; None — словаря у поля нет.

free_generator_refsfunction#

View source
def free_generator_refs(query: dict, ir: dict) -> list[tuple[str, str]]

(id переменной comprehension, id const_ref) для каждой ссылки на константу внутри generator-а §52.1 терма ЗАПРОСА.

Почему это отказ, а не законная ссылка. Компилятор объявил ровно этот запрет для тела правила: LDC-E1317 (law-hir/src/lower/mod.rs) говорит, что имя в generator-е comprehension, не связанное ни биндером правила, ни let, ни переменной самого comprehension, есть свободная переменная §188, и молчаливая подстановка константы дала бы норму, которая не срабатывает никогда. До 01.09.2026 та же формула, поставленная в ТЕРМ ЗАПРОСА теста §267, проходила молча: lower-test понижает файл теста отдельно от программы, и голое имя становилось const_ref на символ, которого в пакете нет. Ответом была пустая коллекция, а ожидания result_kind == COLLECTION пустую коллекцию принимают — тест оставался бы зелёным при удалённой норме (DECISION-0085, случай FNMA-14).

Почему проверяется generator, а не всякий const_ref запроса. Замерено 01.09.2026 по всем 8675 понижённым тестам репозитория: ссылок на НЕОБЪЯВЛЕННУЮ константу в термах запроса 373 на 163 различных имени, и это рабочая идиома, а не долг — непрозрачная константа (FixedBaseIncome у us.fnma.selling_income) нигде не объявлена и работает тем, что одно и то же имя стоит и в факте, и в теле правила. Сверять const_ref со списком объявленных символов значило бы отвергнуть 453 имени корпуса. Отдельно отвергнуть «имя, которого в программе нет вовсе» тоже нельзя: открытый мир делает вопрос о неизвестной константе законным, и корпус такие вопросы задаёт намеренно (ind-44/ind-47, «unchecked … open world»). Generator же измерен отдельно: const_ref внутри него — НОЛЬ на весь репозиторий, то есть запрет E1317 корпус уже соблюдает, и перенос его на запрос ничего не отнимает.

Критерий тот же, что у E1317, а не строже. Имя отвергается, только если оно НЕ объявлено символом предъявленной программы (declared_ids). Ссылка на объявленную константу в generator-е законна и здесь, и в теле правила. Именно поэтому проверка живёт в раннере, а не в lower-test: состав символов приносит --program, и без него отличить объявленную константу от свободной переменной нечем.

Имя ЧУЖОГО namespace пропускается по той же причине, по какой его пропускает компилятор: состав экспортов зависимости предъявляет резолвер, а пустой список означает «предъявить нечем», а не «символа нет».

Границы, оставленные сознательно. (1) Тело квантора §52 не проверяется: E1317 говорит про generator comprehension, и расширять запрет шире прозы значило бы вводить своё правило. (2) Дело §71 не проверяется: assertion ВВОДИТ факт, и непрозрачная константа в нём законна по построению. (3) Свойства §270 не проверяются: их domain и violations строит компилятор из биндеров forall, автор их не пишет.

run_propertyfunction#

View source
def run_property(document: dict, ir: dict, case: dict, resource_root=None, *, evaluator: Callable[[EvaluationRequest], dict] | None = None) -> dict

Вердикт по свойству §270: {"name", "domain", "counterexamples", "skipped"}.

Понижение свойства — работа компилятора (lawc lower-property); здесь только складывается мир и задаются два запроса. Зачем оракулу своя половина: вердикт свойства иначе приходит от ОДНОЙ реализации, а весь контур корректности здесь стоит на том, что их две. Составленная программа (закон + наблюдающие правила) ни в один differential не входит по построению — она собирается на время исполнения свойства, — значит сверять её ответы больше негде.

skipped — наблюдающие правила, которых движок не исполнил. Пустой список есть условие того, что «контрпримеров нет» вообще что-то значит: NON_EXECUTABLE_RULE приходит ПРЕДУПРЕЖДЕНИЕМ, то есть молча для того, кто читает только results (DECISION-0035 §7.1).

run_testfunction#

View source
def run_test(document: dict, ir: dict, resource_root=None, *, evaluator: Callable[[EvaluationRequest], dict] | None = None, calendar: Callable[[dict, dict], bytes | None] | None = None, builder: Callable[..., EvaluationRequest] | None = None) -> dict

Вердикт по тест-документу: {"title", "passed", "failures"}.

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

evaluator позволяет корпусу сохранить перехват вызовов для differential и сертификатов. По умолчанию исполняется независимый оракул.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.