lawref.evaluator.procedures

Свёртка истории процедур — SPEC §160.1–§164.2, §180.2, §201.1 (DECISION-0156).

Фаза стоит ОДНОЙ стратой §111 между strict-замыканием входных фактов и правилами-потребителями §164: автомат перестал быть записью правил и стал данными узла procedure §201.1, а порядок по времени со «строго более ранними» событиями §110.1 правилами не выражается.

Свёртка ОДНА на документ (§161.2): все процедуры программы и все их экземпляры лежат в одном глобальном порядке по началу канонического time носителей §79.1. Носители с равным началом образуют ГРУППУ и каждый читает состояние ДО группы — отсюда требование §161.2, которое эта реализация держит по построению: порядок обхода внутри группы не влияет ни на один опубликованный факт и ни на один узел proof-графа.

Программа без узла procedure через модуль не проходит вовсе: байты её документов обязаны остаться прежними (инвариант 3 CLAUDE.md).

Attributes

Name	Description
CARRIER_REUSED	No description.
INVALID_JOIN	No description.
NORM_STATUS_PREDICATES	No description.
REASONS	No description.
SIMULTANEOUS	No description.

Classes

Name	Description
Automaton	Разбор узла procedure в таблицы, которыми пользуется свёртка.
FoldRefusal	Отказ свёртки §161.1: документ не вычисляется целиком (§181.2).

Functions

Name	Description
above_rules	Предикат → правила НАД свёрткой, его производящие (§161.2).
automaton_subtype	§160.1: тип носителя есть on E либо его подтип §79.
check_guard_stratification	§161.2: гард перехода не может читать вывод, произведённый ВЫШЕ свёртки.
effect_predicates	Предикат → ЧТО его производит выше свёртки, кроме правил (§161.2).
fold	Одна глобальная свёртка §161.1–§164.2 над всеми процедурами документа.
fold_plan	§161.2/§111: план страт относительно свёртки истории.
fold_predicates	Предикаты §164.1, ПРОИЗВОДИМЫЕ свёрткой (не читаемые ею).
needs_event_world	Нужен ли документу мир событий §79.1.
rule_reads	ВСЕ предикаты, читаемые правилом (§161.2, барьер свёртки).
split_closure_groups	Замыкания §70 НИЖЕ и ВЫШЕ свёртки (§161.2, §231.1).
split_defeasible	Слой L1 §104–§115 НИЖЕ и ВЫШЕ свёртки (§161.2, §111).
split_strict	Строгий слой НИЖЕ свёртки (§161.2): правила, чьи головы транзитивно не
validate_joins	§162.2: соединение, которое не сработает никогда, есть тупик.

CARRIER_REUSEDattributemodule attribute#

View source

CARRIER_REUSED = _fatal(
  'CARRIER_REUSED',
  'одно событие предъявлено носителем двух переходов одной области либо вложенных областей одного экземпляра; такие переходы не образуют одного шага истории, и состояние после события не определено, свёртка не выполнялась (§161.1, §162.1)'
)

INVALID_JOINattributemodule attribute#

View source

INVALID_JOIN = _fatal(
  'INVALID_JOIN_POLICY',
  'политика соединения области недостижима: quorum(n) при n вне 1..m либо соединение без областей; автомат не исполняется (§162.2)'
)

NORM_STATUS_PREDICATESattributemodule attribute#

View source

NORM_STATUS_PREDICATES = (
  'urn:law:std#active',
  'urn:law:std#bearer_of',
  'urn:law:std#beneficiary_of',
  'urn:law:std#conflicts',
  'urn:law:std#created',
  'urn:law:std#instance_of',
  'urn:law:std#rule_of',
  'urn:law:std#satisfied',
  'urn:law:std#undetermined',
  'urn:law:std#violated'
)

Show moreShow less

REASONSattributemodule attribute#

View source

REASONS = ('from', 'on', 'guard', 'requires', 'join')

SIMULTANEOUSattributemodule attribute#

View source

SIMULTANEOUS = _fatal(
  'SIMULTANEOUS_EVENTS',
  'два события экземпляра процедуры имеют равное начало канонического интервала; порядок истории не определён, свёртка не выполнялась (§79.1, §161.1)'
)

Automatonclass#

View source

class Automaton(node: dict, lattice: Any = None)

Разбор узла procedure в таблицы, которыми пользуется свёртка.

constantsattributeinstance attribute#

View source

constants: dict[str, dict] = {}

idattributeinstance attribute#

View source

id = str(node['id'])

latticeattributeinstance attribute#

View source

lattice = lattice

nodeattributeinstance attribute#

View source

node = node

regionsattributeinstance attribute#

View source

regions: dict[str, dict] = {}

state_pathattributeinstance attribute#

View source

state_path: dict[str, tuple[str, ...]] = {}

statesattributeinstance attribute#

View source

states: dict[str, dict] = {}

transition_pathattributeinstance attribute#

View source

transition_path: dict[str, tuple[str, ...]] = {}

transitionsattributeinstance attribute#

View source

transitions: dict[str, dict] = {}

active_statesmethodstaticmethod#

View source

def active_states(config: dict | None) -> list[str]

Все активные состояния конфигурации — рекурсивно по областям.

entermethod#

View source

def enter(state_id: str) -> dict

Конфигурация после входа в state_id: у составного состояния токены ставятся в initial КАЖДОЙ области (§162.1).

initial_configmethod#

View source

def initial_config() -> dict | None

initial_state_idmethod#

View source

def initial_state_id() -> str | None

is_terminal_in_regionmethod#

View source

def is_terminal_in_region(state_id: str) -> bool

join_ofmethod#

View source

def join_of(state_id: str) -> dict | None

navigatemethod#

View source

def navigate(config: dict | None, path: tuple[str, ...]) -> dict | None

Под-конфигурация области по пути; None — область не активна.

predicatemethod#

View source

def predicate(field: str) -> str

region_of_statemethod#

View source

def region_of_state(state_id: str) -> tuple[str, ...]

regions_ofmethod#

View source

def regions_of(state_id: str) -> list[dict]

replacemethod#

View source

def replace(config: dict, path: tuple[str, ...], new_sub: dict) -> dict

Копия конфигурации с заменённой под-конфигурацией по пути.

termmethod#

View source

def term(name: str) -> dict

Терм имени профиля §164.1 (состояние, переход, сама процедура) в форме ПОСЛЕ предпрохода §54.1. Имя без декларации константы остаётся const_ref — так устроены и корпусная конвенция, и ручные векторы; имя, объявленное const S: PState = …, публикуется значением.

FoldRefusalclass#

View source

class FoldRefusal(issue: dict)

Bases: Exception

Отказ свёртки §161.1: документ не вычисляется целиком (§181.2).

issueattributeinstance attribute#

View source

issue = issue

above_rulesfunction#

View source

def above_rules(nodes: list[dict]) -> dict[str, list[str]]

Предикат → правила НАД свёрткой, его производящие (§161.2).

automaton_subtypefunction#

View source

def automaton_subtype(automaton: Automaton, carrier_type: str, on: str) -> bool

§160.1: тип носителя есть on E либо его подтип §79.

check_guard_stratificationfunction#

View source

def check_guard_stratification(nodes: list[dict], plan: dict | None = None) -> None

§161.2: гард перехода не может читать вывод, произведённый ВЫШЕ свёртки.

Статически это LDC-E1348 у компилятора; у оракула, которому CLIR подан собранным вручную, тот же случай есть fatal до исполнения. Переносить такое правило вниз нельзя: оно само (либо его группа §111) зависит от свёртки, и перенос означал бы чтение невычисленного вывода (§110).

Отказ предъявляется по ПОТЕНЦИАЛЬНОМУ графу: дефитер, неприменимый в ЭТОМ деле, положения группы не меняет — положение фазы есть свойство программы, а не дела.

effect_predicatesfunction#

View source

def effect_predicates(nodes: list[dict]) -> dict[str, str]

Предикат → ЧТО его производит выше свёртки, кроме правил (§161.2).

Два класса сверх правил: эффект полномочия §127 (payload.effect.after) и статус-атом §140. Оба производятся фазами L2/L3, которые стоят выше свёртки ЦЕЛИКОМ, а не «выше по зависимости»: норм-цикл §143 и defeasible §104 на страты не разделимы, и гард, читающий такой предикат, не увидит его ни при каком порядке фаз (E-0148, сверка №4 п. 8).

Значение — id шаблона полномочия; у статус-атома §140 его нет, и значение пусто: производитель там — сам движок.

foldfunction#

View source

def fold(store: SupportStore, nodes: list[dict], registry: ProofRegistry, issues: list[dict], world: EventWorld, env: Any = None, plan: dict | None = None) -> None

Одна глобальная свёртка §161.1–§164.2 над всеми процедурами документа.

fold_planfunction#

View source

def fold_plan(nodes: list[dict]) -> dict[str, Any] | None

§161.2/§111: план страт относительно свёртки истории.

«Ниже свёртки» — не «строгое правило». Вход внешних по отношению к префиксу предикатов замораживается после завершения ВСЕХ их производителей, включая defeasible-кандидатов, их оппозицию, дефитеры и применимые приоритеты; сила правила сама по себе положения не определяет. Независимые завершённые ГРУППЫ L1 §111 идут ниже свёртки; группа, зависящая от свёртки либо от закреплённых выше производителей, идёт выше ЦЕЛИКОМ — часть кандидатов внизу, а часть наверху означала бы разрешение конфликта по недособранному множеству, то есть нарушение predicate completion barrier §111.

Расчёт — одна неподвижная точка по четырём правилам:

1. правило (любой силы), читающее предикат из above, — выше;
2. группа L1 предиката, у которого ХОТЬ ОДИН производитель выше (своё поражаемое правило, strict-оппозиция, атакующий дефитер), — выше целиком;
3. условие приоритета §120, читающее предикат из above, поднимает правила, которых касается ребро;
4. подъём добавляет ГОЛОВУ правила в above, и расчёт повторяется — подъём группы поднимает её потребителей.

Безусловный транзитивный путь приоритета §106 планом не трогается вовсе: замыкание считается по ПОЛНОЙ программе (prepare_defeasible), и ребро A > C через правило B выше свёртки действует в нижней части, не требуя исполнения B.

None — узла procedure в программе нет: план не строится, порядок фаз прежний, байты прежних документов целы (инвариант 3 CLAUDE.md).

fold_predicatesfunction#

View source

def fold_predicates(nodes: list[dict]) -> set[str]

Предикаты §164.1, ПРОИЗВОДИМЫЕ свёрткой (не читаемые ею).

needs_event_worldfunction#

View source

def needs_event_world(nodes: list[dict]) -> bool

Нужен ли документу мир событий §79.1.

Программа без процедур, без политики §82.1, без типа-события и без расписания recurring его не строит вовсе — и остаётся байтово той же, какой была до DECISION-0156 (инвариант 3 CLAUDE.md).

rule_readsfunction#

View source

def rule_reads(rule: dict) -> set[str]

ВСЕ предикаты, читаемые правилом (§161.2, барьер свёртки).

«Читает» здесь — не «стоит положительным конъюнктом тела». Барьер §161.2 строится по ПОЛНОМУ графу чтений, иначе он пропускает ровно те формы, в которых чтение и прячется: not_known §113, агрегат §59 и квантор §52 внутри гарда, сравнение §57, scope §92 и — главное — термы САМОЙ ГОЛОВЫ (count { s | current_state(x, s) } в аргументе вывода читает свёртку, а конъюнктом тела не является).

Собственный предикат головы в чтения не входит: он производится, а не читается; но аргументы головы обходятся наравне с телом.

split_closure_groupsfunction#

View source

def split_closure_groups(level_groups, nodes: list[dict], plan: dict | None = None)

Замыкания §70 НИЖЕ и ВЫШЕ свёртки (§161.2, §231.1).

Замыкание над предикатом свёртки материализуется ПОСЛЕ неё: закрытый current_state §164.2 иначе получил бы explicit negative на каждый кандидат раньше, чем свёртка опубликовала бы положительную опору, и текущее состояние дела стало бы BOTH — то есть спорным — на ровном месте. Правила, замыкания и свёртка стратифицируются ВМЕСТЕ (§111: «strict-замыкания и замыкания §70 согласуются с тем же планом»), поэтому подъём группы L1 поднимает и замыкание над её предикатом.

split_defeasiblefunction#

View source

def split_defeasible(prepared: dict, plan: dict | None)

Слой L1 §104–§115 НИЖЕ и ВЫШЕ свёртки (§161.2, §111).

Возвращает пару установок с ТЕМИ ЖЕ замыканием приоритетов §106, рангами §110 и статическими issues, что и полная: подготовка считается по ПОЛНОЙ программе, а планом отбираются лишь ИСПОЛНЯЕМЫЕ кандидаты. Иначе транзитивное ребро приоритета, проходящее через правило выше свёртки, исчезло бы в нижней части, и положение фазы изменило бы решётку §106 — свойство программы, а не порядка вычисления.

Нижняя часть пуста — возвращается (None, prepared): прежний единственный вызов, прежние байты.

split_strictfunction#

View source

def split_strict(prepared, nodes: list[dict], plan: dict | None = None)

Строгий слой НИЖЕ свёртки (§161.2): правила, чьи головы транзитивно не зависят ни от предикатов §164.1, ни от групп L1, закреплённых выше.

Свёртка есть одна страта §111, и её вход заморожен на входе: правила, читающие valid_transition / entered_state / left_state / current_state, стоят СТРОГО ВЫШЕ и до свёртки не применяются — иначе not_known(valid_transition(…)) §113 у потребителя §164 сработал бы на НЕВЫЧИСЛЕННОМ выводе (§161.1). Программа без узла procedure этой функции не видит и идёт прежним порядком байт в байт.

validate_joinsfunction#

View source

def validate_joins(automata: list[Automaton]) -> None

§162.2: соединение, которое не сработает никогда, есть тупик.

Тот же класс, что статический LDC-E1345, предъявленный собранным вручную CLIR, — fatal INVALID_JOIN_POLICY до вывода. LDC-E1345 называет ЧЕТЫРЕ формы, а не одну: quorum(n) вне диапазона, join без областей и — обе проверялись раньше — область без initial либо без терминального состояния. Область без начального состояния не получает токена вовсе, а область без терминала не завершается ни при какой истории: и то, и другое делает соединение недостижимым ровно так же, как quorum(0).