From 9de6fd28ffa28fde6e8a17cc0ecf925b6292316f Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 11:32:33 -0700 Subject: [PATCH 1/7] Add Z3 checker packaging: check extra, lazy import, CheckerUnavailable Adds the check optional-dependency extra (z3-solver>=4.12) and the checker.py module skeleton: CheckerUnavailable/UnencodableConstruct/ NonlinearArithmetic exceptions, the lazy _import_z3() helper, and the Finding/CheckResult dataclasses. z3 is never imported at module scope, so `import liminate.checker` succeeds with zero third-party runtime dependencies whether or not z3 is installed. Co-Authored-By: Claude Sonnet 5 --- pyproject.toml | 1 + src/liminate/checker.py | 77 ++++++++++++++++++++++++++++++++++ tests/test_checker.py | 93 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 171 insertions(+) create mode 100644 src/liminate/checker.py create mode 100644 tests/test_checker.py diff --git a/pyproject.toml b/pyproject.toml index 074079f..b54c09b 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -25,6 +25,7 @@ liminate = "liminate.cli:main" [project.optional-dependencies] dev = ["pytest>=7.0"] build = ["pyinstaller>=6.0"] +check = ["z3-solver>=4.12"] [tool.pytest.ini_options] testpaths = ["tests"] diff --git a/src/liminate/checker.py b/src/liminate/checker.py new file mode 100644 index 0000000..a8d23f8 --- /dev/null +++ b/src/liminate/checker.py @@ -0,0 +1,77 @@ +"""Z3 satisfiability checker for Liminate's enforcement fragment. + +Decidability Step 2 (Trust Infrastructure Addendum v1.0s §91/§92.6). +Encodes an Agreement's deontic statements (require/forbid/permit/expect +and the define predicates they reference) into SMT constraints over +QF_UFLIRA and runs seven authoring-time checks that a human reading the +file would miss. + +Scope: the enforcement fragment only. No temporal encoding (starting_date +/ until_date are ignored — v1.0s §91.6), no trace semantics, no CLI verb. +This module sits alongside analyzer.detect_contradictions; it does not +replace or modify it. + +z3 is an optional dependency (the `check` extra). This module never +imports z3 at top level — `import liminate.checker` must always succeed. +The import happens lazily inside the public entry point. +""" + + +from __future__ import annotations + +import time +from dataclasses import dataclass + + +class CheckerUnavailable(Exception): + """Raised when the z3 solver is not installed.""" + + +class UnencodableConstruct(Exception): + """Raised when an AST node falls outside the encodable fragment.""" + + +class NonlinearArithmetic(Exception): + """Raised when multiplied_by/divided_by has no compile-time-constant + operand after definition inlining.""" + + +def _import_z3(): + try: + import z3 + except ImportError: + raise CheckerUnavailable( + "Satisfiability checking needs the z3 solver. " + "Install it with: pip install liminate[check]" + ) from None + return z3 + + +@dataclass +class Finding: + kind: str + severity: str + statements: list[str] + explanation: str + + +@dataclass +class CheckResult: + findings: list[Finding] + checked: int + elapsed_ms: float + encodable: bool + skipped_reason: str | None = None + + + +def check_agreement(statements, symbol_table) -> CheckResult: + """Encode `statements` and run the seven core checks. + + Input mirrors analyzer.detect_contradictions(statements): a list of + top-level statement ASTs. Never raises for out-of-fragment input — + UnencodableConstruct is caught at this boundary and reported via + CheckResult(encodable=False, skipped_reason=...). + """ + _import_z3() + raise NotImplementedError diff --git a/tests/test_checker.py b/tests/test_checker.py new file mode 100644 index 0000000..e29c3bd --- /dev/null +++ b/tests/test_checker.py @@ -0,0 +1,93 @@ +"""Tests for the Z3 satisfiability checker (src/liminate/checker.py). + +Decidability Step 2 — encodes Liminate's enforcement fragment (require/ +forbid/permit/expect + define predicates) into SMT constraints and runs +seven authoring-time checks. See src/liminate/checker.py for the design +notes; this file mirrors its phase structure. +""" + +from __future__ import annotations + +import subprocess +import sys + +import pytest + +from liminate.cli import Session +from liminate.lexer import tokenize +from liminate.parser import parse +from liminate.analyzer import SymbolEntry +from liminate.reorderer import reorder +from liminate.result import LiminateResult + + +def _parse_line(line, predicate_names=None): + reordered = reorder(tokenize(line)) + assert not isinstance(reordered, LiminateResult), line + ast = parse(reordered, predicate_names=predicate_names) + assert not isinstance(ast, LiminateResult), line + return ast + + +def _condition_of(line, predicate_names=None): + """Parse a require/forbid/permit/expect/define line and return the + condition AST (the `.condition` field for deontic verbs).""" + return _parse_line(line, predicate_names=predicate_names).condition + + +def run_lines(lines): + session = Session() + results = [session.run_line(line) for line in lines] + return session, results + + +# --------------------------------------------------------------------------- +# Phase 1 — packaging: lazy z3 import +# --------------------------------------------------------------------------- + + +def test_checker_module_importable_without_z3(): + """`import liminate.checker` must succeed even when z3 cannot be + imported at all — the module must not import z3 at top level.""" + script = ( + "import sys, builtins\n" + "_orig_import = builtins.__import__\n" + "def _blocked(name, *a, **k):\n" + " if name == 'z3' or name.startswith('z3.'):\n" + " raise ImportError('z3 not installed (simulated)')\n" + " return _orig_import(name, *a, **k)\n" + "builtins.__import__ = _blocked\n" + "import liminate.checker\n" + "print('IMPORT_OK')\n" + ) + result = subprocess.run( + [sys.executable, "-c", script], capture_output=True, text=True + ) + assert result.returncode == 0, result.stderr + assert "IMPORT_OK" in result.stdout + + +def test_check_agreement_raises_checker_unavailable_without_z3(): + """Calling the public entry point without z3 installed raises + CheckerUnavailable, not an ImportError or traceback.""" + script = ( + "import sys, builtins\n" + "_orig_import = builtins.__import__\n" + "def _blocked(name, *a, **k):\n" + " if name == 'z3' or name.startswith('z3.'):\n" + " raise ImportError('z3 not installed (simulated)')\n" + " return _orig_import(name, *a, **k)\n" + "builtins.__import__ = _blocked\n" + "import liminate.checker as checker\n" + "try:\n" + " checker.check_agreement([], {})\n" + "except checker.CheckerUnavailable as e:\n" + " print('RAISED_CHECKER_UNAVAILABLE')\n" + " print(str(e))\n" + ) + result = subprocess.run( + [sys.executable, "-c", script], capture_output=True, text=True + ) + assert result.returncode == 0, result.stderr + assert "RAISED_CHECKER_UNAVAILABLE" in result.stdout + assert "pip install liminate[check]" in result.stdout From 9336ee00a115c88e9a6d69ad443dc5c3194cd22a Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 11:32:45 -0700 Subject: [PATCH 2/7] Add Z3 encoder sort model and constant allocation _Encoder allocates Z3 constants from the symbol table: number->Real, string->String, date->Int (epoch-day ordinals), one constant per record field named {record}__{field}. list_of_* entries get no constant -- membership expands to a disjunction at encode time instead (Phase 3). Names are sanitized to legal SMT identifiers with a reverse map for diagnostics, since Liminate allows hyphens. Co-Authored-By: Claude Sonnet 5 --- src/liminate/checker.py | 113 ++++++++++++++++++++++++++++++++++++++++ tests/test_checker.py | 62 ++++++++++++++++++++++ 2 files changed, 175 insertions(+) diff --git a/src/liminate/checker.py b/src/liminate/checker.py index a8d23f8..572b753 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -19,8 +19,32 @@ from __future__ import annotations +import re import time from dataclasses import dataclass +from datetime import date + +from .parser import ( + ArithmeticNode, + BareWord, + CompoundConditionNode, + ConditionNode, + DateLiteral, + DefineNode, + EachPronoun, + ExpectNode, + FieldAccessNode, + ForbidNode, + NameRef, + NumberLiteral, + PermitNode, + PredicateApplicationNode, + QuotedString, + RememberValueNode, + RequireNode, + SequenceNode, +) +from .renderer import render class CheckerUnavailable(Exception): @@ -65,6 +89,95 @@ class CheckResult: +# --------------------------------------------------------------------------- +# Phase 2 — sort model and constant allocation +# --------------------------------------------------------------------------- + +# Liminate names may contain hyphens (e.g. "actor-teams") and other +# characters that are not legal SMT identifiers. Sanitization is +# deterministic; the encoder keeps a reverse map so diagnostics can name +# the original Liminate identifier instead of the sanitized one. +_SANITIZE_RE = re.compile(r"[^A-Za-z0-9_]") + +# SymbolEntry.type / SymbolEntry.schema[field] values that map onto a +# scalar Z3 sort. Dates encode as Int via epoch-day ordinals (§9 fact 9 — +# never mixed with number's Real sort). +_LIST_TYPES = frozenset({"list_of_strings", "list_of_numbers", "list_of_dates"}) + + +def _sanitize_base(name: str) -> str: + sanitized = _SANITIZE_RE.sub("_", name) + if sanitized and sanitized[0].isdigit(): + sanitized = f"_{sanitized}" + return sanitized or "_" + + +def _date_ordinal(d: date) -> int: + return d.toordinal() + + +class _Encoder: + """Holds the Z3 constant map for one check_agreement() call plus the + definitions map (Phase 4) needed for value-position name inlining.""" + + def __init__(self, z3mod, symbol_table, definitions): + self.z3 = z3mod + self.symtab = symbol_table + self.definitions = definitions # name -> defining ASTNode (Phase 4) + self.constants: dict[str, object] = {} + self.reverse: dict[str, str] = {} + self.lists: dict[str, list] = {} + self._sanitized_cache: dict[str, str] = {} + self._inlining_visited: set[str] = set() + self._predicate_depth = 0 + self._build_constants() + + def _sanitize(self, name: str) -> str: + """Deterministic name -> SMT identifier, disambiguated against + collisions from distinct original names sanitizing identically.""" + cached = self._sanitized_cache.get(name) + if cached is not None: + return cached + base = _sanitize_base(name) + candidate = base + suffix = 0 + while candidate in self.reverse and self.reverse[candidate] != name: + suffix += 1 + candidate = f"{base}__{suffix}" + self._sanitized_cache[name] = candidate + self.reverse[candidate] = name + return candidate + + def _build_constants(self) -> None: + for name, entry in self.symtab.items(): + if entry.type == "number": + self.constants[name] = self.z3.Real(self._sanitize(name)) + elif entry.type == "string": + self.constants[name] = self.z3.String(self._sanitize(name)) + elif entry.type == "date": + self.constants[name] = self.z3.Int(self._sanitize(name)) + elif entry.type == "record": + for field_name, field_type in (entry.schema or {}).items(): + key = f"{name}__{field_name}" + ident = self._sanitize(key) + if field_type == "number": + self.constants[key] = self.z3.Real(ident) + elif field_type == "string": + self.constants[key] = self.z3.String(ident) + elif field_type == "date": + self.constants[key] = self.z3.Int(ident) + # Any other field scalar type is left unallocated; + # UnencodableConstruct is raised lazily if a condition + # actually references it (§10 boundary contract). + elif entry.type in _LIST_TYPES: + # No constant — §6 "includes"/"not_includes" expand to a + # finite disjunction over these literal values instead. + self.lists[name] = list(entry.value) + # list_of_records, composition, predicate, and anything else + # get no constant here; predicates are handled by body + # inlining (§6), not by constant allocation. + + def check_agreement(statements, symbol_table) -> CheckResult: """Encode `statements` and run the seven core checks. diff --git a/tests/test_checker.py b/tests/test_checker.py index e29c3bd..9594223 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -91,3 +91,65 @@ def test_check_agreement_raises_checker_unavailable_without_z3(): assert result.returncode == 0, result.stderr assert "RAISED_CHECKER_UNAVAILABLE" in result.stdout assert "pip install liminate[check]" in result.stdout + + +# --------------------------------------------------------------------------- +# Phase 2 — sort model and constant allocation +# --------------------------------------------------------------------------- + +z3 = pytest.importorskip("z3") + +from liminate import checker # noqa: E402 (after importorskip) + + +def test_constant_map_number_string_date_record_and_string_list(): + symtab = { + "amount": SymbolEntry(name="amount", value=10, type="number"), + "status": SymbolEntry(name="status", value="open", type="string"), + "due": SymbolEntry( + name="due", value=__import__("datetime").date(2026, 1, 1), type="date" + ), + "order1": SymbolEntry( + name="order1", + value={"total": 50, "label": "x"}, + type="record", + schema={"total": "number", "label": "string"}, + ), + "tags": SymbolEntry( + name="tags", value=["a", "b"], type="list_of_strings" + ), + } + enc = checker._Encoder(z3, symtab, {}) + + assert enc.constants["amount"].sort() == z3.RealSort() + assert enc.constants["status"].sort() == z3.StringSort() + assert enc.constants["due"].sort() == z3.IntSort() + assert enc.constants["order1__total"].sort() == z3.RealSort() + assert enc.constants["order1__label"].sort() == z3.StringSort() + + # No constant is allocated for a list — membership expands to a + # disjunction at encode time instead. + assert "tags" not in enc.constants + + # Reverse map round-trips for every allocated constant. + for original in ("amount", "status", "due", "order1__total", "order1__label"): + sanitized = enc._sanitize(original) + assert enc.reverse[sanitized] == original + + +def test_constant_map_sanitizes_hyphenated_names(): + symtab = { + "actor-teams": SymbolEntry(name="actor-teams", value=1, type="number"), + } + enc = checker._Encoder(z3, symtab, {}) + const = enc.constants["actor-teams"] + # Must be a legal Z3/SMT identifier — no raw hyphen survives. + assert "-" not in str(const) + assert enc.reverse[enc._sanitize("actor-teams")] == "actor-teams" + + +def test_date_ordinal_helper_matches_toordinal(): + import datetime + + d = datetime.date(2026, 7, 20) + assert checker._date_ordinal(d) == d.toordinal() From e3ce84ba372ad01f5d89da6f9efddcb1683526a1 Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 11:32:57 -0700 Subject: [PATCH 3/7] Add Z3 condition encoder: operators, within, includes, predicates encode_condition mirrors interpreter._eval_condition/_apply_op exactly: is/equal_to/not_equal_to/above/below, not_above/not_below as fused <=/>= (never a structural Not() wrapper), within with value=tolerance and value2=target (the counter-intuitive operand order verified against the parser), includes/not_includes over a statically-known list with the empty-list edge case special-cased before splatting. PredicateApplicationNode substitutes EachPronoun with the application's subject (never by name) and encodes the body recursively, with a depth guard mirroring the interpreter's own defensive posture. Every other name in a predicate body resolves normally. Co-Authored-By: Claude Sonnet 5 --- src/liminate/checker.py | 185 +++++++++++++++++++++++++++++++++++ tests/test_checker.py | 208 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 393 insertions(+) diff --git a/src/liminate/checker.py b/src/liminate/checker.py index 572b753..487eaa6 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -177,6 +177,191 @@ def _build_constants(self) -> None: # get no constant here; predicates are handled by body # inlining (§6), not by constant allocation. + # ----------------------------------------------------------------- + # Phase 3 — condition encoder (mirrors interpreter._eval_condition) + # ----------------------------------------------------------------- + + def encode_condition(self, cond): + if isinstance(cond, CompoundConditionNode): + left = self.encode_condition(cond.left) + right = self.encode_condition(cond.right) + if cond.connector == "and": + return self.z3.And(left, right) + return self.z3.Or(left, right) + if isinstance(cond, PredicateApplicationNode): + return self._encode_predicate_application(cond) + if isinstance(cond, ConditionNode): + return self._encode_condition_leaf(cond) + raise UnencodableConstruct( + f"Can't encode condition {type(cond).__name__}." + ) + + def _encode_predicate_application(self, cond): + entry = self.symtab.get(cond.predicate_name) + if entry is None or entry.type != "predicate": + raise UnencodableConstruct( + f"No predicate definition found for '{cond.predicate_name}'." + ) + if self._predicate_depth >= _MAX_PREDICATE_ENCODE_DEPTH: + raise UnencodableConstruct( + f"Predicate '{cond.predicate_name}' is nested more than " + f"{_MAX_PREDICATE_ENCODE_DEPTH} levels deep — this usually " + f"means two or more definitions refer back to each other." + ) + substituted = _substitute_each_pronoun(entry.value, cond.subject) + self._predicate_depth += 1 + try: + result = self.encode_condition(substituted) + finally: + self._predicate_depth -= 1 + return self.z3.Not(result) if cond.negated else result + + def _encode_condition_leaf(self, cond): + if cond.op == "within": + # §3 correction (1): value is the tolerance, value2 is the + # target — mirrors interpreter._eval_condition exactly. + field_val = self.encode_field(cond.field) + tolerance = self.encode_value(cond.value) + target = self.encode_value(cond.value2) + return self.z3.And( + field_val - target <= tolerance, + target - field_val <= tolerance, + ) + if cond.op in ("includes", "not_includes"): + return self._encode_membership(cond) + field_val = self.encode_field(cond.field) + value_val = self.encode_value(cond.value) + return _encode_comparison(self.z3, cond.op, field_val, value_val) + + def _encode_membership(self, cond): + if not isinstance(cond.field, NameRef) or cond.field.name not in self.lists: + label = cond.field.name if isinstance(cond.field, NameRef) else type(cond.field).__name__ + raise UnencodableConstruct( + f"'{cond.op}' needs a statically known list; '{label}' isn't one." + ) + items = self.lists[cond.field.name] + elem = self.encode_value(cond.value) + if not items: + # §6 empty-list edge case: z3.Or()/z3.And() with no arguments + # is invalid, so this is special-cased before splatting. + return self.z3.BoolVal(cond.op == "not_includes") + literals = [self._python_literal(v) for v in items] + if cond.op == "includes": + return self.z3.Or(*[elem == lit for lit in literals]) + return self.z3.And(*[elem != lit for lit in literals]) + + def _python_literal(self, value): + if isinstance(value, bool): + raise UnencodableConstruct("Boolean list elements can't be encoded.") + if isinstance(value, (int, float)): + return self.z3.RealVal(value) + if isinstance(value, str): + return self.z3.StringVal(value) + if isinstance(value, date): + return self.z3.IntVal(_date_ordinal(value)) + raise UnencodableConstruct(f"Can't encode list element {value!r}.") + + def encode_field(self, node): + if isinstance(node, NameRef): + if node.name in self.constants: + return self.constants[node.name] + raise UnencodableConstruct(f"'{node.name}' isn't an encodable fact.") + if isinstance(node, FieldAccessNode): + key = f"{node.record_name}__{node.field}" + if key in self.constants: + return self.constants[key] + raise UnencodableConstruct( + f"'{node.field} of {node.record_name}' isn't an encodable fact." + ) + # EachPronoun (outside a predicate body it should already have + # been substituted out of) and ExtremaNode (§6: out of scope + # this build) both fall through to this generic branch. + raise UnencodableConstruct( + f"Can't encode field reference {type(node).__name__}." + ) + + def encode_value(self, node, origin_name=None): + if isinstance(node, NumberLiteral): + return self.z3.RealVal(node.value) + if isinstance(node, DateLiteral): + return self.z3.IntVal(_date_ordinal(node.value)) + if isinstance(node, QuotedString): + return self.z3.StringVal(node.content) + if isinstance(node, (BareWord, NameRef)): + return self._resolve_name_value(node) + if isinstance(node, FieldAccessNode): + return self.encode_field(node) + raise UnencodableConstruct(f"Can't encode value {type(node).__name__}.") + + def _resolve_name_value(self, node): + name = node.word if isinstance(node, BareWord) else node.name + if name in self.constants: + return self.constants[name] + if isinstance(node, BareWord): + return self.z3.StringVal(node.word) + raise UnencodableConstruct(f"'{name}' isn't defined.") + + +# Mirrors interpreter._MAX_PREDICATE_EVAL_DEPTH — belt-and-braces defense +# against a hand-built symbol table, since PRs #60/#61 already guarantee +# acyclicity for any program that reached the encoder via the analyzer. +_MAX_PREDICATE_ENCODE_DEPTH = 64 + + +def _substitute_each_pronoun(node, replacement): + """Deep-substitute every EachPronoun in a predicate body with the + application's subject node (§3 correction 2) — never by name.""" + if isinstance(node, EachPronoun): + return replacement + if isinstance(node, CompoundConditionNode): + return CompoundConditionNode( + left=_substitute_each_pronoun(node.left, replacement), + right=_substitute_each_pronoun(node.right, replacement), + connector=node.connector, + ) + if isinstance(node, ConditionNode): + return ConditionNode( + field=_substitute_each_pronoun(node.field, replacement), + op=node.op, + value=_substitute_each_pronoun(node.value, replacement), + value2=( + _substitute_each_pronoun(node.value2, replacement) + if node.value2 is not None + else None + ), + ) + if isinstance(node, PredicateApplicationNode): + return PredicateApplicationNode( + subject=_substitute_each_pronoun(node.subject, replacement), + predicate_name=node.predicate_name, + negated=node.negated, + ) + if isinstance(node, ArithmeticNode): + return ArithmeticNode( + left=_substitute_each_pronoun(node.left, replacement), + right=_substitute_each_pronoun(node.right, replacement), + op=node.op, + ) + return node + + +def _encode_comparison(z3mod, op, lhs, rhs): + """Mirrors interpreter._apply_op exactly. not_above/not_below are + fused negations (<=/>=), never a structural Not(above)/Not(below) + wrapper — §12 failure mode 6.""" + if op in ("is", "equal_to"): + return lhs == rhs + if op == "not_equal_to": + return lhs != rhs + if op == "above": + return lhs > rhs + if op == "below": + return lhs < rhs + if op == "not_above": + return lhs <= rhs + if op == "not_below": + return lhs >= rhs + raise UnencodableConstruct(f"Unknown comparison operator '{op}'.") def check_agreement(statements, symbol_table) -> CheckResult: """Encode `statements` and run the seven core checks. diff --git a/tests/test_checker.py b/tests/test_checker.py index 9594223..0e9b053 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -153,3 +153,211 @@ def test_date_ordinal_helper_matches_toordinal(): d = datetime.date(2026, 7, 20) assert checker._date_ordinal(d) == d.toordinal() + + +# --------------------------------------------------------------------------- +# Phase 3 — condition encoder +# --------------------------------------------------------------------------- + + +def _pinned(enc, name, value): + """A solver assumption pinning a free constant to a concrete value, + so a structurally-free condition formula gets a definite sat/unsat + verdict for a specific fact assignment.""" + return enc.constants[name] == value + + +def _check_with(formula, *assumptions): + s = z3.Solver() + for a in assumptions: + s.add(a) + s.add(formula) + return s.check() + + +def _number_symtab(**facts): + return {name: SymbolEntry(name=name, value=v, type="number") for name, v in facts.items()} + + +def test_op_is_and_equal_to(): + for line in ("require amount is 50", "require amount is equal to 50"): + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + formula = enc.encode_condition(_condition_of(line)) + assert _check_with(formula, _pinned(enc, "amount", 50)) == z3.sat + assert _check_with(formula, _pinned(enc, "amount", 51)) == z3.unsat + + +def test_op_not_equal_to(): + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + formula = enc.encode_condition(_parse_line("require amount is not equal to 50").condition) + assert _check_with(formula, _pinned(enc, "amount", 51)) == z3.sat + assert _check_with(formula, _pinned(enc, "amount", 50)) == z3.unsat + + +def test_op_above(): + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + formula = enc.encode_condition(_condition_of("require amount is above 50")) + assert _check_with(formula, _pinned(enc, "amount", 60)) == z3.sat + assert _check_with(formula, _pinned(enc, "amount", 40)) == z3.unsat + + +def test_op_below(): + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + formula = enc.encode_condition(_condition_of("require amount is below 50")) + assert _check_with(formula, _pinned(enc, "amount", 40)) == z3.sat + assert _check_with(formula, _pinned(enc, "amount", 60)) == z3.unsat + + +def test_op_not_above(): + """not_above is a fused <=, not a structural Not(above) wrapper.""" + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + formula = enc.encode_condition(_parse_line("require amount is not above 50").condition) + assert _check_with(formula, _pinned(enc, "amount", 50)) == z3.sat # boundary included + assert _check_with(formula, _pinned(enc, "amount", 51)) == z3.unsat + + +def test_op_not_below(): + """not_below is a fused >=, not a structural Not(below) wrapper.""" + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + formula = enc.encode_condition(_parse_line("require amount is not below 50").condition) + assert _check_with(formula, _pinned(enc, "amount", 50)) == z3.sat # boundary included + assert _check_with(formula, _pinned(enc, "amount", 49)) == z3.unsat + + +def test_op_within_operand_order_not_swapped(): + """§3 correction (1): value is tolerance, value2 is target. A swap + would make amount=50 satisfiable; the correct encoding must not.""" + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + cond = _parse_line("require amount is within 5 of 100").condition + formula = enc.encode_condition(cond) + assert _check_with(formula, _pinned(enc, "amount", 100)) == z3.sat + assert _check_with(formula, _pinned(enc, "amount", 105)) == z3.sat # boundary + assert _check_with(formula, _pinned(enc, "amount", 106)) == z3.unsat + assert _check_with(formula, _pinned(enc, "amount", 50)) == z3.unsat # would be sat if swapped + + +def test_op_includes_present_value_is_satisfiable(): + symtab = { + "tags": SymbolEntry(name="tags", value=["urgent", "normal"], type="list_of_strings"), + } + enc = checker._Encoder(z3, symtab, {}) + cond = _parse_line('require tags includes "urgent"').condition + formula = enc.encode_condition(cond) + assert _check_with(formula) == z3.sat + + +def test_op_includes_absent_value_is_unsatisfiable(): + symtab = { + "tags": SymbolEntry(name="tags", value=["urgent", "normal"], type="list_of_strings"), + } + enc = checker._Encoder(z3, symtab, {}) + cond = _parse_line('require tags includes "missing"').condition + formula = enc.encode_condition(cond) + assert _check_with(formula) == z3.unsat + + +def test_op_not_includes_mirrors_includes(): + symtab = { + "tags": SymbolEntry(name="tags", value=["urgent", "normal"], type="list_of_strings"), + } + enc = checker._Encoder(z3, symtab, {}) + present = _parse_line('require tags not includes "urgent"').condition + absent = _parse_line('require tags not includes "missing"').condition + assert _check_with(enc.encode_condition(present)) == z3.unsat + assert _check_with(enc.encode_condition(absent)) == z3.sat + + +def test_op_includes_empty_list_special_case(): + symtab = { + "tags": SymbolEntry(name="tags", value=[], type="list_of_strings"), + } + enc = checker._Encoder(z3, symtab, {}) + includes_cond = _parse_line('require tags includes "x"').condition + not_includes_cond = _parse_line('require tags not includes "x"').condition + assert _check_with(enc.encode_condition(includes_cond)) == z3.unsat + assert _check_with(enc.encode_condition(not_includes_cond)) == z3.sat + + +def test_compound_and_or(): + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + and_cond = _parse_line("require amount is above 10 and amount is below 20").condition + or_cond = _parse_line("require amount is above 100 or amount is below 5").condition + and_formula = enc.encode_condition(and_cond) + or_formula = enc.encode_condition(or_cond) + assert _check_with(and_formula, _pinned(enc, "amount", 15)) == z3.sat + assert _check_with(and_formula, _pinned(enc, "amount", 30)) == z3.unsat + assert _check_with(or_formula, _pinned(enc, "amount", 200)) == z3.sat + assert _check_with(or_formula, _pinned(enc, "amount", 50)) == z3.unsat + + +def test_predicate_application_substitutes_each_pronoun_and_resolves_outer_symbols(): + """§3 corrections (2) and (3): the predicate body's implicit field + binds to EachPronoun, substituted with the application's subject; + every other name in the body (cutoff) resolves normally.""" + session, results = run_lines([ + "remember a number called cutoff with 100", + "define big: is above cutoff", + ]) + for r in results: + assert r.status.name == "SUCCESS", r.message + symtab = dict(session.symtab) + symtab["amount"] = SymbolEntry(name="amount", value=0, type="number") + enc = checker._Encoder(z3, symtab, {}) + cond = _condition_of("forbid amount is big", predicate_names={"big"}) + formula = enc.encode_condition(cond) + cutoff = _pinned(enc, "cutoff", 100) + assert _check_with(formula, cutoff, _pinned(enc, "amount", 150)) == z3.sat + assert _check_with(formula, cutoff, _pinned(enc, "amount", 50)) == z3.unsat + + +def test_predicate_application_negated(): + session, results = run_lines([ + "remember a number called cutoff with 100", + "define big: is above cutoff", + ]) + for r in results: + assert r.status.name == "SUCCESS", r.message + symtab = dict(session.symtab) + symtab["amount"] = SymbolEntry(name="amount", value=0, type="number") + enc = checker._Encoder(z3, symtab, {}) + cond = _condition_of("forbid amount is not big", predicate_names={"big"}) + formula = enc.encode_condition(cond) + cutoff = _pinned(enc, "cutoff", 100) + assert _check_with(formula, cutoff, _pinned(enc, "amount", 150)) == z3.unsat + assert _check_with(formula, cutoff, _pinned(enc, "amount", 50)) == z3.sat + + +def test_predicate_application_missing_definition_is_unencodable(): + symtab = _number_symtab(amount=0) + enc = checker._Encoder(z3, symtab, {}) + cond = checker.PredicateApplicationNode( + subject=checker.NameRef(name="amount"), predicate_name="ghost", negated=False, + ) + with pytest.raises(checker.UnencodableConstruct): + enc.encode_condition(cond) + + +def test_predicate_depth_guard_on_hand_built_cycle(): + """Belt-and-braces defense (§6) mirroring interpreter's + _MAX_PREDICATE_EVAL_DEPTH, exercised via a hand-built symbol table + since the analyzer (PR #60/#61) already rejects real self-reference.""" + symtab = _number_symtab(amount=0) + cyclic_body = checker.PredicateApplicationNode( + subject=checker.EachPronoun(), predicate_name="loopy", negated=False, + ) + symtab["loopy"] = SymbolEntry(name="loopy", value=cyclic_body, type="predicate") + enc = checker._Encoder(z3, symtab, {}) + cond = checker.PredicateApplicationNode( + subject=checker.NameRef(name="amount"), predicate_name="loopy", negated=False, + ) + with pytest.raises(checker.UnencodableConstruct): + enc.encode_condition(cond) + + +def test_extrema_and_top_level_each_pronoun_are_unencodable(): + symtab = _number_symtab(amount=0, cap=0) + enc = checker._Encoder(z3, symtab, {}) + with pytest.raises(checker.UnencodableConstruct): + enc.encode_field(checker.EachPronoun()) + with pytest.raises(checker.UnencodableConstruct): + enc.encode_value(checker.EachPronoun()) From da9d57d2ec76c45c1aef5e0ad282304854eed020 Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 11:33:07 -0700 Subject: [PATCH 4/7] Add arithmetic encoding, name inlining, and nonlinearity detection Closes TI-Q13. The symbol table only stores computed values, never the defining expression, so check_agreement scans RememberValueNode in the program AST into a definitions map. Value-position name resolution now inlines a name's defining expression when it contains an ArithmeticNode anywhere, guarded by a visited-set against self-reference. After inlining, multiplied_by/divided_by raise NonlinearArithmetic when neither operand is a compile-time constant -- a name reference never counts as one here, even when its own value happens to be a literal, because it is a free Z3 constant to the solver regardless. This is the case PR #62's syntactic linearity check provably misses: remember a number called beta with 4 remember a number called z from beta multiplied by beta forbid alpha is above z The analyzer sees only a bare name in the condition and passes it (tests/test_arithmetic.py's test_KNOWN_GAP_value_indirection_bypasses_ the_linearity_restriction pins this, unmodified). The encoder inlines z to beta*beta and rejects it. Co-Authored-By: Claude Sonnet 5 --- src/liminate/checker.py | 106 +++++++++++++++++++++++++++++ tests/test_checker.py | 146 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 252 insertions(+) diff --git a/src/liminate/checker.py b/src/liminate/checker.py index 487eaa6..bf42803 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -280,6 +280,11 @@ def encode_field(self, node): f"Can't encode field reference {type(node).__name__}." ) + # ----------------------------------------------------------------- + # Phase 4 — value position: literals, name resolution + inlining, + # arithmetic + nonlinearity detection (TI-Q13 closure) + # ----------------------------------------------------------------- + def encode_value(self, node, origin_name=None): if isinstance(node, NumberLiteral): return self.z3.RealVal(node.value) @@ -288,19 +293,95 @@ def encode_value(self, node, origin_name=None): if isinstance(node, QuotedString): return self.z3.StringVal(node.content) if isinstance(node, (BareWord, NameRef)): + # §3 correction (4): both shapes must be handled — the parser + # emits BareWord for names in value position, but the AST + # comment allows NameRef too. return self._resolve_name_value(node) if isinstance(node, FieldAccessNode): return self.encode_field(node) + if isinstance(node, ArithmeticNode): + return self._encode_arithmetic(node, origin_name) + # EachPronoun at top level and ExtremaNode (§6: out of scope + # this build) both fall through to this generic branch. raise UnencodableConstruct(f"Can't encode value {type(node).__name__}.") def _resolve_name_value(self, node): name = node.word if isinstance(node, BareWord) else node.name + defining = self.definitions.get(name) + if ( + defining is not None + and self._contains_arithmetic(defining) + and name not in self._inlining_visited + ): + # §7 inlining rule: the symbol table only stores computed + # values, not defining expressions, so a name whose defining + # `remember` involves arithmetic is inlined — the recursive + # encode below is what lets nonlinearity be caught at all. + self._inlining_visited.add(name) + try: + return self.encode_value(defining, origin_name=name) + finally: + self._inlining_visited.discard(name) if name in self.constants: return self.constants[name] if isinstance(node, BareWord): + # Matches interpreter._eval_value: an unresolved BareWord is + # a string literal, not an error. return self.z3.StringVal(node.word) raise UnencodableConstruct(f"'{name}' isn't defined.") + def _contains_arithmetic(self, node) -> bool: + return isinstance(node, ArithmeticNode) + + def _is_compile_time_constant(self, node) -> bool: + """A numeral literal, or an arithmetic tree of literals only — + deliberately NOT resolved through name indirection. A BareWord/ + NameRef operand (e.g. `beta` in `beta multiplied by beta`) is + always treated as an opaque runtime symbol here, even if its own + defining value happens to be a literal — that symbol is a free + Z3 constant to the solver, so multiplying it by itself is + genuinely nonlinear regardless of what the interpreter would + compute it to be at run time.""" + if isinstance(node, NumberLiteral): + return True + if isinstance(node, ArithmeticNode): + return ( + self._is_compile_time_constant(node.left) + and self._is_compile_time_constant(node.right) + ) + return False + + def _encode_arithmetic(self, node, origin_name=None): + if node.op in ("multiplied_by", "divided_by"): + if not self._is_compile_time_constant( + node.left + ) and not self._is_compile_time_constant(node.right): + raise NonlinearArithmetic(self._nonlinear_message(node, origin_name)) + left = self.encode_value(node.left, origin_name=origin_name) + right = self.encode_value(node.right, origin_name=origin_name) + if node.op == "plus": + return left + right + if node.op == "minus": + return left - right + if node.op == "multiplied_by": + return left * right + if node.op == "divided_by": + return left / right + raise UnencodableConstruct(f"Unknown arithmetic operator '{node.op}'.") + + def _nonlinear_message(self, node, origin_name) -> str: + op_word = "multiplied by" if node.op == "multiplied_by" else "divided by" + msg = ( + f"'{render(node.left)} {op_word} {render(node.right)}' is nonlinear " + f"— neither side is a compile-time constant." + ) + if origin_name is not None: + msg += ( + f" This came from inlining '{origin_name}', defined by a " + f"'remember' statement." + ) + return msg + # Mirrors interpreter._MAX_PREDICATE_EVAL_DEPTH — belt-and-braces defense # against a hand-built symbol table, since PRs #60/#61 already guarantee @@ -345,6 +426,31 @@ def _substitute_each_pronoun(node, replacement): return node +def _iter_statements(statements): + """Descend into SequenceNode, mirroring the walking convention + analyzer._iter_deontic_nodes uses — the shared pattern §10 asks the + checker to reuse, applied here to the broader set of statement types + check_agreement needs (not just Require/Forbid).""" + for stmt in statements: + if isinstance(stmt, SequenceNode): + yield from _iter_statements(stmt.operations) + else: + yield stmt + + +def _build_definitions(statements): + """§7 — name -> defining ASTNode, scanned from the program AST. The + symbol table only stores computed values (RememberValueNode.value is + gone by execution time), so this is the only place the defining + expression survives. Later definitions overwrite earlier ones, + matching _store's overwrite semantics (v1d §58).""" + definitions: dict[str, object] = {} + for stmt in _iter_statements(statements): + if isinstance(stmt, RememberValueNode): + definitions[stmt.name] = stmt.value + return definitions + + def _encode_comparison(z3mod, op, lhs, rhs): """Mirrors interpreter._apply_op exactly. not_above/not_below are fused negations (<=/>=), never a structural Not(above)/Not(below) diff --git a/tests/test_checker.py b/tests/test_checker.py index 0e9b053..19cc985 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -361,3 +361,149 @@ def test_extrema_and_top_level_each_pronoun_are_unencodable(): enc.encode_field(checker.EachPronoun()) with pytest.raises(checker.UnencodableConstruct): enc.encode_value(checker.EachPronoun()) + + +# --------------------------------------------------------------------------- +# Phase 4 — arithmetic, name inlining, TI-Q13 closure +# --------------------------------------------------------------------------- + + +def test_build_definitions_from_remember_value_nodes(): + statements = [_parse_line(l) for l in [ + "remember a number called beta with 4", + "remember a number called z from beta multiplied by beta", + "forbid alpha is above z", + ]] + definitions = checker._build_definitions(statements) + assert set(definitions) == {"beta", "z"} + assert isinstance(definitions["z"], checker.ArithmeticNode) + + +def test_build_definitions_later_overwrites_earlier(): + statements = [_parse_line(l) for l in [ + "remember a number called w with 1", + "remember a number called w with 2", + ]] + definitions = checker._build_definitions(statements) + assert isinstance(definitions["w"], checker.NumberLiteral) + assert definitions["w"].value == 2 + + +def test_build_definitions_descends_into_sequence_node(): + seq = checker.SequenceNode( + operations=[ + _parse_line("remember a number called w with 1"), + _parse_line("remember a number called v with 2"), + ], + connectors=["and"], + ) + definitions = checker._build_definitions([seq]) + assert set(definitions) == {"w", "v"} + + +def test_inlining_applies_when_defining_expression_has_arithmetic(): + definitions = { + "beta": checker.NumberLiteral(value=4), + "z": checker.ArithmeticNode( + left=checker.BareWord(word="beta"), + right=checker.BareWord(word="beta"), + op="multiplied_by", + ), + } + symtab = _number_symtab(beta=4, alpha=0) + enc = checker._Encoder(z3, symtab, definitions) + with pytest.raises(checker.NonlinearArithmetic): + enc.encode_value(checker.BareWord(word="z")) + + +def test_inlining_skipped_when_defining_expression_has_no_arithmetic(): + """A plain `remember ... with 4` (no ArithmeticNode in its defining + expression) is NOT inlined — it resolves to its opaque constant.""" + definitions = {"w": checker.NumberLiteral(value=4)} + symtab = _number_symtab(w=4) + enc = checker._Encoder(z3, symtab, definitions) + result = enc.encode_value(checker.BareWord(word="w")) + assert result is enc.constants["w"] + + +def test_self_reference_guard_falls_back_to_opaque_constant(): + """`remember a number called x from x plus 1` — inlining must not + recurse infinitely; on revisit it falls back to the opaque constant.""" + definitions = { + "x": checker.ArithmeticNode( + left=checker.BareWord(word="x"), + right=checker.NumberLiteral(value=1), + op="plus", + ), + } + symtab = _number_symtab(x=0) + enc = checker._Encoder(z3, symtab, definitions) + result = enc.encode_value(checker.BareWord(word="x")) # must not raise / hang + assert result is not None + + +def test_multiplied_by_nonlinear_when_neither_operand_constant(): + definitions = { + "beta": checker.NumberLiteral(value=4), + } + symtab = _number_symtab(beta=4) + enc = checker._Encoder(z3, symtab, definitions) + node = checker.ArithmeticNode( + left=checker.BareWord(word="beta"), + right=checker.BareWord(word="beta"), + op="multiplied_by", + ) + with pytest.raises(checker.NonlinearArithmetic): + enc.encode_value(node) + + +def test_multiplied_by_linear_when_one_operand_is_a_literal(): + symtab = _number_symtab(beta=4) + enc = checker._Encoder(z3, symtab, {}) + node = checker.ArithmeticNode( + left=checker.BareWord(word="beta"), + right=checker.NumberLiteral(value=2), + op="multiplied_by", + ) + result = enc.encode_value(node) # must not raise + assert result is not None + + +def test_divided_by_nonlinear_when_neither_operand_constant(): + symtab = _number_symtab(beta=4, gamma=2) + enc = checker._Encoder(z3, symtab, {}) + node = checker.ArithmeticNode( + left=checker.BareWord(word="beta"), + right=checker.BareWord(word="gamma"), + op="divided_by", + ) + with pytest.raises(checker.NonlinearArithmetic): + enc.encode_value(node) + + +def test_TI_Q13_checker_rejects_value_indirection_the_analyzer_permits(): + """Matched pair with tests/test_arithmetic.py's + test_KNOWN_GAP_value_indirection_bypasses_the_linearity_restriction, + which deliberately pins that liminate.run()/the analyzer PASS this + program: PR #62's syntactic linearity check sees only a bare + NameRef/BareWord in the condition, never the ArithmeticNode that + produced it. The checker closes that gap by inlining the value at + encode time and rejecting the nonlinear multiplication it exposes.""" + lines = [ + "remember a number called alpha with 10", + "remember a number called beta with 2", + "remember a value called doubled from beta multiplied by beta", + "forbid alpha is above doubled", + ] + session, results = run_lines(lines) + for r in results[:-1]: + assert r.status.name == "SUCCESS", r.message + assert results[-1].status.name == "PROHIBITION_VIOLATED" # liminate.run() accepts + enforces it + + statements = [_parse_line(l) for l in lines] + definitions = checker._build_definitions(statements) + enc = checker._Encoder(z3, session.symtab, definitions) + cond = statements[-1].condition + with pytest.raises(checker.NonlinearArithmetic) as excinfo: + enc.encode_condition(cond) + assert "doubled" in str(excinfo.value) From dbc84c99b34b25a8fc23d113d04c40e512ad4439 Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 11:33:18 -0700 Subject: [PATCH 5/7] Add deontic statement effect formulas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit encode_deontic reduces a Require/Forbid/Permit/Expect node to (effect, allowed): require fires on ¬C∧¬E (allowed C∨E); forbid fires on C∧¬E (allowed ¬C∨E); permit and expect fire on C∧¬E / ¬C∧¬E respectively but are non-blocking and get no allowed-space, since they never participate in the require/forbid contradiction check (locked DT-Q3: permit never contradicts). exception=None collapses to BoolVal(False) uniformly across all four verbs. Co-Authored-By: Claude Sonnet 5 --- src/liminate/checker.py | 38 ++++++++++ tests/test_checker.py | 151 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 189 insertions(+) diff --git a/src/liminate/checker.py b/src/liminate/checker.py index bf42803..f5a658e 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -382,6 +382,44 @@ def _nonlinear_message(self, node, origin_name) -> str: ) return msg + # ----------------------------------------------------------------- + # Phase 5 — deontic statement effect formulas (§8) + # ----------------------------------------------------------------- + + def encode_deontic(self, node): + """Returns (effect, allowed) for a Require/Forbid/Permit/Expect + node. `effect` is the condition under which the statement fires + (halts for require/forbid, emits for permit, reports for + expect). `allowed` is the allowed-state space (require/forbid + only — None for permit/expect, which never participate in the + require/forbid contradiction check per the locked DT-Q3 + decision: permit never contradicts).""" + condition = self.encode_condition(node.condition) + exception = ( + self.encode_condition(node.exception) + if node.exception is not None + else self.z3.BoolVal(False) + ) + not_condition = self.z3.Not(condition) + not_exception = self.z3.Not(exception) + if isinstance(node, RequireNode): + effect = self.z3.And(not_condition, not_exception) + allowed = self.z3.Or(condition, exception) + return effect, allowed + if isinstance(node, ForbidNode): + effect = self.z3.And(condition, not_exception) + allowed = self.z3.Or(not_condition, exception) + return effect, allowed + if isinstance(node, PermitNode): + effect = self.z3.And(condition, not_exception) + return effect, None + if isinstance(node, ExpectNode): + effect = self.z3.And(not_condition, not_exception) + return effect, None + raise UnencodableConstruct( + f"Can't encode deontic statement {type(node).__name__}." + ) + # Mirrors interpreter._MAX_PREDICATE_EVAL_DEPTH — belt-and-braces defense # against a hand-built symbol table, since PRs #60/#61 already guarantee diff --git a/tests/test_checker.py b/tests/test_checker.py index 19cc985..4fe62c2 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -507,3 +507,154 @@ def test_TI_Q13_checker_rejects_value_indirection_the_analyzer_permits(): with pytest.raises(checker.NonlinearArithmetic) as excinfo: enc.encode_condition(cond) assert "doubled" in str(excinfo.value) + + +# --------------------------------------------------------------------------- +# Phase 5 — deontic statement effect formulas +# --------------------------------------------------------------------------- + + +def _pin_all(enc, symtab): + """Pin every scalar fact the encoder allocated a constant for to its + real interpreter value, so a formula referencing only those facts + collapses to a concrete, closed boolean.""" + assumptions = [] + for name, entry in symtab.items(): + if name not in enc.constants: + continue + if entry.type == "date": + assumptions.append(enc.constants[name] == checker._date_ordinal(entry.value)) + elif entry.type in ("number", "string"): + assumptions.append(enc.constants[name] == entry.value) + return assumptions + + +def _run_last_and_encode(lines): + session, results = run_lines(lines) + for r in results[:-1]: + assert r.status.name == "SUCCESS", r.message + last_ast = _parse_line(lines[-1]) + enc = checker._Encoder(z3, session.symtab, {}) + effect, allowed = enc.encode_deontic(last_ast) + assumptions = _pin_all(enc, session.symtab) + return results[-1], effect, allowed, assumptions + + +def test_require_effect_fires_iff_interpreter_halts(): + r, effect, _, assumptions = _run_last_and_encode([ + "remember a number called amount with 40", + "require amount is above 50", + ]) + assert r.status.name == "REQUIREMENT_NOT_MET" + assert _check_with(effect, *assumptions) == z3.sat + + r2, effect2, _, assumptions2 = _run_last_and_encode([ + "remember a number called amount with 60", + "require amount is above 50", + ]) + assert r2.status.name == "SUCCESS" + assert _check_with(effect2, *assumptions2) == z3.unsat + + +def test_require_unless_excuses_matches_interpreter(): + r, effect, _, assumptions = _run_last_and_encode([ + "remember a number called amount with 40", + 'remember a string called override with "yes"', + "require amount is above 50 unless override is yes", + ]) + assert r.status.name == "SUCCESS" # excused + assert _check_with(effect, *assumptions) == z3.unsat + + +def test_forbid_effect_fires_iff_interpreter_halts(): + r, effect, _, assumptions = _run_last_and_encode([ + "remember a number called amount with 60", + "forbid amount is above 50", + ]) + assert r.status.name == "PROHIBITION_VIOLATED" + assert _check_with(effect, *assumptions) == z3.sat + + r2, effect2, _, assumptions2 = _run_last_and_encode([ + "remember a number called amount with 40", + "forbid amount is above 50", + ]) + assert r2.status.name == "SUCCESS" + assert _check_with(effect2, *assumptions2) == z3.unsat + + +def test_forbid_unless_excuses_matches_interpreter(): + r, effect, _, assumptions = _run_last_and_encode([ + "remember a number called amount with 60", + 'remember a string called override with "yes"', + "forbid amount is above 50 unless override is yes", + ]) + assert r.status.name == "SUCCESS" # excused + assert _check_with(effect, *assumptions) == z3.unsat + + +def test_permit_effect_fires_iff_interpreter_emits(): + session, results = run_lines([ + "remember a number called amount with 60", + "permit amount is above 50", + ]) + assert results[-1].output is not None # fired + enc = checker._Encoder(z3, session.symtab, {}) + effect, allowed = enc.encode_deontic(_parse_line("permit amount is above 50")) + assert allowed is None # §8: permit never participates in allowed-space checks + assumptions = _pin_all(enc, session.symtab) + assert _check_with(effect, *assumptions) == z3.sat + + session2, results2 = run_lines([ + "remember a number called amount with 40", + "permit amount is above 50", + ]) + assert results2[-1].output is None # did not fire + enc2 = checker._Encoder(z3, session2.symtab, {}) + effect2, _ = enc2.encode_deontic(_parse_line("permit amount is above 50")) + assumptions2 = _pin_all(enc2, session2.symtab) + assert _check_with(effect2, *assumptions2) == z3.unsat + + +def test_expect_effect_fires_iff_interpreter_reports_divergence(): + session, results = run_lines([ + "remember a number called amount with 40", + "expect amount is above 50", + ]) + assert results[-1].output is not None # divergence reported + enc = checker._Encoder(z3, session.symtab, {}) + effect, allowed = enc.encode_deontic(_parse_line("expect amount is above 50")) + assert allowed is None + assumptions = _pin_all(enc, session.symtab) + assert _check_with(effect, *assumptions) == z3.sat + + session2, results2 = run_lines([ + "remember a number called amount with 60", + "expect amount is above 50", + ]) + assert results2[-1].output is None # met expectation, no report + enc2 = checker._Encoder(z3, session2.symtab, {}) + effect2, _ = enc2.encode_deontic(_parse_line("expect amount is above 50")) + assumptions2 = _pin_all(enc2, session2.symtab) + assert _check_with(effect2, *assumptions2) == z3.unsat + + +def test_require_forbid_effect_and_allowed_are_logical_complements(): + for line in ("require amount is above 50", "forbid amount is above 50"): + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + effect, allowed = enc.encode_deontic(_parse_line(line)) + s = z3.Solver() + s.add(effect != enc.z3.Not(allowed)) + assert s.check() == z3.unsat # no assignment breaks the complement + + +def test_exception_none_collapses_to_false(): + """When `exception` is None, E must behave as BoolVal(False) so the + require/forbid formulas collapse to the unguarded shape.""" + enc = checker._Encoder(z3, _number_symtab(amount=0), {}) + node = _parse_line("require amount is above 50") + assert node.exception is None + effect, allowed = enc.encode_deontic(node) + plain_condition = enc.encode_condition(node.condition) + s = z3.Solver() + s.add(allowed != plain_condition) + assert s.check() == z3.unsat From f3da2091f30691d6d15c6ca4e77021d2cd1b603c Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 11:33:28 -0700 Subject: [PATCH 6/7] Add the seven core satisfiability checks Each check is a separate assert_and_track solver query (tracked names stmt_{index}_{verb}, 5000ms timeout -> an "inconclusive" info finding rather than hanging): (1) always-deny / vacuous require, (2) dead forbid, (3) require-forbid contradiction, (4) unless-swallows-the-rule (the highest-value finding -- runs first and suppresses check 2 for the same statement since the two share a query shape for forbid), (5) redundant forbid, (6) dead permit, (7) constant predicate bodies (contradiction or tautology), which needs a fresh Z3 constant standing in for a predicate's implicit subject, sorted by inferring how the body compares it. Checks 3 and 5 are pairwise (O(n^2)); above 200 deontic statements they're skipped with an informational finding while the per-statement checks still run. Co-Authored-By: Claude Sonnet 5 --- src/liminate/checker.py | 372 ++++++++++++++++++++++++++++++++++++++++ tests/test_checker.py | 257 +++++++++++++++++++++++++++ 2 files changed, 629 insertions(+) diff --git a/src/liminate/checker.py b/src/liminate/checker.py index f5a658e..3497da6 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -420,6 +420,79 @@ def encode_deontic(self, node): f"Can't encode deontic statement {type(node).__name__}." ) + # ----------------------------------------------------------------- + # Phase 6, check 7 — a predicate's own body, standing alone + # ----------------------------------------------------------------- + # + # A `define` body is normally only ever encoded through an + # application site (§6), where EachPronoun substitutes to a concrete + # subject expression with a known sort. Check 7 asks whether the + # body is constant *for any possible subject* — so it needs a fresh, + # unconstrained Z3 constant standing in for "any subject," sorted by + # how the body actually compares it. Reuses the same substitution + + # encode_condition machinery as a real application by registering + # the placeholder under a synthetic name in `self.constants`, rather + # than inventing a second code path. + + def encode_predicate_body_standalone(self, predicate_name, body): + sort = self._infer_subject_sort(body, set()) + if sort is None: + raise UnencodableConstruct( + f"Can't infer a subject type for predicate " + f"'{predicate_name}' — its body never compares the " + f"implicit subject against anything with a known sort." + ) + placeholder = f"__subject__{predicate_name}" + ident = self._sanitize(placeholder) + if sort == "number": + self.constants[placeholder] = self.z3.Real(ident) + elif sort == "string": + self.constants[placeholder] = self.z3.String(ident) + else: + self.constants[placeholder] = self.z3.Int(ident) + substituted = _substitute_each_pronoun(body, NameRef(name=placeholder)) + return self.encode_condition(substituted) + + def _infer_subject_sort(self, node, visited): + if isinstance(node, CompoundConditionNode): + return self._infer_subject_sort( + node.left, visited + ) or self._infer_subject_sort(node.right, visited) + if isinstance(node, ConditionNode): + if isinstance(node.field, EachPronoun): + hint = self._value_sort_hint(node.value) + if hint is None and node.value2 is not None: + hint = self._value_sort_hint(node.value2) + return hint + return None + if isinstance(node, PredicateApplicationNode): + if isinstance(node.subject, EachPronoun): + if node.predicate_name in visited: + return None + entry = self.symtab.get(node.predicate_name) + if entry is None or entry.type != "predicate": + return None + return self._infer_subject_sort( + entry.value, visited | {node.predicate_name} + ) + return None + return None + + def _value_sort_hint(self, node): + if isinstance(node, (NumberLiteral, ArithmeticNode)): + return "number" + if isinstance(node, DateLiteral): + return "date" + if isinstance(node, QuotedString): + return "string" + if isinstance(node, (BareWord, NameRef)): + name = node.word if isinstance(node, BareWord) else node.name + entry = self.symtab.get(name) + if entry is not None and entry.type in ("number", "string", "date"): + return entry.type + return None + return None + # Mirrors interpreter._MAX_PREDICATE_EVAL_DEPTH — belt-and-braces defense # against a hand-built symbol table, since PRs #60/#61 already guarantee @@ -507,6 +580,305 @@ def _encode_comparison(z3mod, op, lhs, rhs): return lhs >= rhs raise UnencodableConstruct(f"Unknown comparison operator '{op}'.") + +# --------------------------------------------------------------------------- +# Phase 6 — the seven core checks (§9) +# --------------------------------------------------------------------------- + +_SOLVER_TIMEOUT_MS = 5000 +_PAIRWISE_CAP = 200 + +_VERB_NAMES = { + RequireNode: "require", + ForbidNode: "forbid", + PermitNode: "permit", + ExpectNode: "expect", +} + + +@dataclass +class _DeonticEntry: + index: int + verb: str + node: object + effect: object + allowed: object | None + text: str + + +def _collect_deontic_entries(enc, statements) -> list[_DeonticEntry]: + entries = [] + for stmt in _iter_statements(statements): + verb = _VERB_NAMES.get(type(stmt)) + if verb is None: + continue + effect, allowed = enc.encode_deontic(stmt) + entries.append(_DeonticEntry( + index=len(entries), verb=verb, node=stmt, + effect=effect, allowed=allowed, text=render(stmt), + )) + return entries + + +def _tracked_name(index, verb) -> str: + return f"stmt_{index}_{verb}" + + +def _interpret_check_result(z3mod, result) -> str: + if result == z3mod.unsat: + return "unsat" + if result == z3mod.sat: + return "sat" + return "unknown" + + +def _run_query(enc, tracked): + """tracked: list[(formula, name)]. Every assertion is tracked (§9) + so unsat_core() can map a finding back to its source statement(s). + A per-query timeout means a hard query surfaces as 'unknown' rather + than hanging the whole run.""" + s = enc.z3.Solver() + s.set("timeout", _SOLVER_TIMEOUT_MS) + for formula, name in tracked: + s.assert_and_track(formula, name) + status = _interpret_check_result(enc.z3, s.check()) + core = s.unsat_core() if status == "unsat" else None + return status, core + + +def _inconclusive(check_name, statements) -> Finding: + return Finding( + kind="inconclusive", severity="info", statements=list(statements), + explanation=( + f"Check '{check_name}' timed out and is inconclusive for: " + f"{', '.join(statements)}." + ), + ) + + +def _cap_finding(count) -> Finding | None: + if count <= _PAIRWISE_CAP: + return None + return Finding( + kind="inconclusive", severity="info", statements=[], + explanation=( + f"{count} deontic statements exceeds the pairwise-check cap of " + f"{_PAIRWISE_CAP} — require/forbid contradiction (check 3) and " + f"redundant-forbid (check 5) were skipped. Per-statement checks " + f"still ran." + ), + ) + + +def _check_always_deny(enc, entries) -> list[Finding]: + """Check 1 — a require whose allowed-space (C ∨ E) is UNSAT can + never be satisfied: it always halts execution.""" + findings = [] + for e in entries: + if e.verb != "require": + continue + status, _ = _run_query(enc, [(e.allowed, _tracked_name(e.index, e.verb))]) + if status == "unsat": + findings.append(Finding( + kind="always_deny", severity="error", statements=[e.text], + explanation=( + f"'{e.text}' can never be satisfied — every possible " + f"state violates it, so this requirement always halts " + f"execution." + ), + )) + elif status == "unknown": + findings.append(_inconclusive("always_deny", [e.text])) + return findings + + +def _check_dead_forbid(enc, entries, swallowed) -> list[Finding]: + """Check 2 — a forbid whose effect (C ∧ ¬E) is UNSAT never fires. + Suppressed for a statement check 4 already flagged (§9: run check 4 + first, report the more specific diagnosis, not both).""" + findings = [] + for e in entries: + if e.verb != "forbid" or e.index in swallowed: + continue + status, _ = _run_query(enc, [(e.effect, _tracked_name(e.index, e.verb))]) + if status == "unsat": + findings.append(Finding( + kind="dead_forbid", severity="warning", statements=[e.text], + explanation=( + f"'{e.text}' can never trigger — no possible state " + f"satisfies its condition, so this prohibition never " + f"fires." + ), + )) + elif status == "unknown": + findings.append(_inconclusive("dead_forbid", [e.text])) + return findings + + +def _check_require_forbid_conflict(enc, entries, capped) -> list[Finding]: + """Check 3 — a require and a forbid whose allowed-spaces are jointly + UNSAT can never both be satisfied.""" + if capped: + return [] + findings = [] + requires = [e for e in entries if e.verb == "require"] + forbids = [e for e in entries if e.verb == "forbid"] + for r in requires: + for f in forbids: + status, _ = _run_query(enc, [ + (r.allowed, _tracked_name(r.index, r.verb)), + (f.allowed, _tracked_name(f.index, f.verb)), + ]) + if status == "unsat": + findings.append(Finding( + kind="require_forbid_conflict", severity="error", + statements=[r.text, f.text], + explanation=( + f"'{r.text}' and '{f.text}' can never both hold — " + f"any state satisfying one violates the other." + ), + )) + elif status == "unknown": + findings.append( + _inconclusive("require_forbid_conflict", [r.text, f.text]) + ) + return findings + + +def _check_unless_swallows_rule(enc, entries): + """Check 4 — a statement whose own effect (given its own exception) + is UNSAT reads as protection while providing none: the exception + fires whenever the rule would. Highest-value finding in the + taxonomy; runs before check 2 so its statement is suppressed there. + Returns (findings, swallowed_indices).""" + findings = [] + swallowed = set() + for e in entries: + if e.node.exception is None: + continue + status, _ = _run_query(enc, [(e.effect, _tracked_name(e.index, e.verb))]) + if status == "unsat": + swallowed.add(e.index) + findings.append(Finding( + kind="unless_swallows_rule", severity="error", statements=[e.text], + explanation=( + f"'{e.text}' can never fire — its own 'unless' exception " + f"holds in every state where the base condition does, so " + f"this rule can never actually enforce anything." + ), + )) + elif status == "unknown": + findings.append(_inconclusive("unless_swallows_rule", [e.text])) + return findings, swallowed + + +def _check_redundant_forbid(enc, entries, capped) -> list[Finding]: + """Check 5 — forbid_1 ∧ ¬forbid_2 UNSAT means forbid_1 is subsumed + by forbid_2: whenever the narrower one would fire, the broader one + already does.""" + if capped: + return [] + findings = [] + forbids = [e for e in entries if e.verb == "forbid"] + for e1 in forbids: + for e2 in forbids: + if e1.index == e2.index: + continue + status, _ = _run_query(enc, [ + (e1.effect, _tracked_name(e1.index, e1.verb)), + (enc.z3.Not(e2.effect), f"not_{_tracked_name(e2.index, e2.verb)}"), + ]) + if status == "unsat": + findings.append(Finding( + kind="redundant_forbid", severity="warning", + statements=[e1.text, e2.text], + explanation=( + f"'{e1.text}' is redundant — whenever it would fire, " + f"'{e2.text}' already fires too." + ), + )) + elif status == "unknown": + findings.append( + _inconclusive("redundant_forbid", [e1.text, e2.text]) + ) + return findings + + +def _check_dead_permit(enc, entries) -> list[Finding]: + """Check 6 — a permit whose effect can't co-occur with the allowed + space of every require/forbid can only ever apply to a state some + other rule already blocks.""" + findings = [] + permits = [e for e in entries if e.verb == "permit"] + if not permits: + return findings + guards = [e for e in entries if e.verb in ("require", "forbid")] + for p in permits: + tracked = [(p.effect, _tracked_name(p.index, p.verb))] + tracked.extend((g.allowed, _tracked_name(g.index, g.verb)) for g in guards) + status, _ = _run_query(enc, tracked) + if status == "unsat": + findings.append(Finding( + kind="dead_permit", severity="warning", statements=[p.text], + explanation=( + f"'{p.text}' can never actually apply — every state " + f"where it would grant permission is already blocked " + f"by another require/forbid rule." + ), + )) + elif status == "unknown": + findings.append(_inconclusive("dead_permit", [p.text])) + return findings + + +def _check_constant_predicate(enc, statements) -> list[Finding]: + """Check 7 — for each `define`, is its body a contradiction (always + false) or a tautology (always true) for any possible subject?""" + findings = [] + for stmt in _iter_statements(statements): + if not isinstance(stmt, DefineNode): + continue + text = render(stmt) + try: + body_formula = enc.encode_predicate_body_standalone( + stmt.name, stmt.condition + ) + except UnencodableConstruct: + findings.append(Finding( + kind="inconclusive", severity="info", statements=[text], + explanation=( + f"Couldn't determine a subject type for predicate " + f"'{stmt.name}' — check 7 (constant predicate) skipped " + f"for it." + ), + )) + continue + + contradiction, _ = _run_query( + enc, [(body_formula, f"predicate_{stmt.name}_body")] + ) + if contradiction == "unsat": + findings.append(Finding( + kind="constant_predicate", severity="warning", statements=[text], + explanation=f"'{text}' is always false — no subject can ever satisfy it.", + )) + continue + if contradiction == "unknown": + findings.append(_inconclusive("constant_predicate", [text])) + continue + + tautology, _ = _run_query( + enc, [(enc.z3.Not(body_formula), f"predicate_{stmt.name}_not_body")] + ) + if tautology == "unsat": + findings.append(Finding( + kind="constant_predicate", severity="warning", statements=[text], + explanation=f"'{text}' is always true — every subject satisfies it.", + )) + elif tautology == "unknown": + findings.append(_inconclusive("constant_predicate", [text])) + return findings + def check_agreement(statements, symbol_table) -> CheckResult: """Encode `statements` and run the seven core checks. diff --git a/tests/test_checker.py b/tests/test_checker.py index 4fe62c2..04921ab 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -658,3 +658,260 @@ def test_exception_none_collapses_to_false(): s = z3.Solver() s.add(allowed != plain_condition) assert s.check() == z3.unsat + + +# --------------------------------------------------------------------------- +# Phase 6 — the seven core checks +# --------------------------------------------------------------------------- + + +def _build_checker_context(lines, predicate_names=None): + session, results = run_lines(lines) + for r in results: + assert r.status.name in ( + "SUCCESS", "REQUIREMENT_NOT_MET", "PROHIBITION_VIOLATED", + ), r.message + statements = [_parse_line(l, predicate_names=predicate_names) for l in lines] + definitions = checker._build_definitions(statements) + enc = checker._Encoder(z3, session.symtab, definitions) + return enc, statements + + +def _findings_of_kind(findings, kind): + return [f for f in findings if f.kind == kind] + + +def test_check1_always_deny_positive(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "require amount is above 50 and amount is below 10", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_always_deny(enc, entries) + assert len(findings) == 1 + assert findings[0].severity == "error" + + +def test_check1_always_deny_negative(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "require amount is above 5", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_always_deny(enc, entries) + assert findings == [] + + +def test_check2_dead_forbid_positive(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "forbid amount is above 50 and amount is below 10", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_dead_forbid(enc, entries, swallowed=set()) + assert len(findings) == 1 + assert findings[0].severity == "warning" + + +def test_check2_dead_forbid_negative(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "forbid amount is above 50", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_dead_forbid(enc, entries, swallowed=set()) + assert findings == [] + + +def test_check3_require_forbid_conflict_positive(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "require amount is above 100", + "forbid amount is above 50", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_require_forbid_conflict(enc, entries, capped=False) + assert len(findings) == 1 + assert findings[0].severity == "error" + + +def test_check3_require_forbid_conflict_negative(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "require amount is above 100", + "forbid amount is above 200", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_require_forbid_conflict(enc, entries, capped=False) + assert findings == [] + + +def test_check3_skipped_when_capped(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "require amount is above 100", + "forbid amount is above 50", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_require_forbid_conflict(enc, entries, capped=True) + assert findings == [] + + +def test_check4_unless_swallows_rule_positive_forbid(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "forbid amount is above 1000 unless amount is above 0", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings, swallowed = checker._check_unless_swallows_rule(enc, entries) + assert len(findings) == 1 + assert findings[0].severity == "error" + assert swallowed == {entries[0].index} + + +def test_check4_unless_swallows_rule_positive_require(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "require amount is above 5 unless amount is below 1000", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings, swallowed = checker._check_unless_swallows_rule(enc, entries) + assert len(findings) == 1 + assert swallowed == {entries[0].index} + + +def test_check4_unless_swallows_rule_negative(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "forbid amount is above 1000 unless amount is above 2000", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings, swallowed = checker._check_unless_swallows_rule(enc, entries) + assert findings == [] + assert swallowed == set() + + +def test_check4_suppresses_check2_for_same_statement(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "forbid amount is above 1000 unless amount is above 0", + ]) + entries = checker._collect_deontic_entries(enc, statements) + unless_findings, swallowed = checker._check_unless_swallows_rule(enc, entries) + dead_forbid_findings = checker._check_dead_forbid(enc, entries, swallowed) + assert _findings_of_kind(unless_findings, "unless_swallows_rule") + assert dead_forbid_findings == [] # suppressed, not double-reported + + +def test_check5_redundant_forbid_positive(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "forbid amount is above 100", + "forbid amount is above 50", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_redundant_forbid(enc, entries, capped=False) + assert len(findings) == 1 + assert findings[0].severity == "warning" + assert findings[0].statements[0] == entries[0].text # the narrower one + + +def test_check5_redundant_forbid_negative(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + 'remember a string called status with "open"', + "forbid amount is above 50", + 'forbid status is equal to "blocked"', + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_redundant_forbid(enc, entries, capped=False) + assert findings == [] + + +def test_check5_skipped_when_capped(): + enc, statements = _build_checker_context([ + "remember a number called amount with 10", + "forbid amount is above 100", + "forbid amount is above 50", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_redundant_forbid(enc, entries, capped=True) + assert findings == [] + + +def test_check6_dead_permit_positive(): + enc, statements = _build_checker_context([ + "remember a number called amount with 5", + "require amount is below 10", + "permit amount is above 50", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_dead_permit(enc, entries) + assert len(findings) == 1 + assert findings[0].severity == "warning" + + +def test_check6_dead_permit_negative(): + enc, statements = _build_checker_context([ + "remember a number called amount with 5", + "require amount is below 100", + "permit amount is above 50", + ]) + entries = checker._collect_deontic_entries(enc, statements) + findings = checker._check_dead_permit(enc, entries) + assert findings == [] + + +def test_check7_constant_predicate_contradiction(): + enc, statements = _build_checker_context([ + "define impossible: is above 100 and is below 50", + ]) + findings = checker._check_constant_predicate(enc, statements) + assert len(findings) == 1 + assert findings[0].severity == "warning" + assert "never" in findings[0].explanation or "always false" in findings[0].explanation + + +def test_check7_constant_predicate_tautology(): + enc, statements = _build_checker_context([ + "define always_big_or_small: is above 0 or is below 1000000", + ]) + findings = checker._check_constant_predicate(enc, statements) + assert len(findings) == 1 + assert findings[0].severity == "warning" + + +def test_check7_constant_predicate_negative_resolves_outer_symbol(): + enc, statements = _build_checker_context([ + "remember a number called cutoff with 100", + "define big: is above cutoff", + ]) + findings = checker._check_constant_predicate(enc, statements) + assert findings == [] + + +def test_pairwise_cap_finding_helper(): + assert checker._cap_finding(200) is None + finding = checker._cap_finding(201) + assert finding is not None + assert finding.severity == "info" + assert finding.kind == "inconclusive" + + +def test_run_query_interprets_sat_unsat_unknown(): + enc, _ = _build_checker_context(["remember a number called amount with 5"]) + sat_status, _ = checker._run_query(enc, [(z3.BoolVal(True), "t")]) + assert sat_status == "sat" + unsat_status, core = checker._run_query(enc, [(z3.BoolVal(False), "f")]) + assert unsat_status == "unsat" + assert len(core) >= 1 + + +def test_interpret_check_result_maps_unknown_to_inconclusive(): + assert checker._interpret_check_result(z3, z3.sat) == "sat" + assert checker._interpret_check_result(z3, z3.unsat) == "unsat" + assert checker._interpret_check_result(z3, z3.unknown) == "unknown" + + +def test_solver_timeout_configured_at_5000ms(): + assert checker._SOLVER_TIMEOUT_MS == 5000 From eaa8e6df99e7c2880d1753918d0efc669340a48e Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 11:33:37 -0700 Subject: [PATCH 7/7] Add check_agreement public API check_agreement(statements, symbol_table) -> CheckResult ties the encoder and the seven checks together. Input mirrors analyzer.detect_contradictions(statements) -- a list of top-level statement ASTs; the checker implements its own SequenceNode-descending walk (_iter_statements) rather than reusing detect_contradictions' _iter_deontic_nodes, which only yields Require/ForbidNode and would silently drop Permit/Expect/Define. UnencodableConstruct and NonlinearArithmetic are caught at this boundary and reported as CheckResult(encodable=False, skipped_reason=...); so is any other exception (invariant 8 -- no unhandled exception escapes check_agreement for any input, malformed or out-of-fragment). Every statement rendering in a Finding goes through renderer.render() so checker output matches canonical form everywhere else in the system. Co-Authored-By: Claude Sonnet 5 --- src/liminate/checker.py | 50 ++++++++++++++++++++--- tests/test_checker.py | 87 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 131 insertions(+), 6 deletions(-) diff --git a/src/liminate/checker.py b/src/liminate/checker.py index 3497da6..b79564e 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -16,7 +16,6 @@ The import happens lazily inside the public entry point. """ - from __future__ import annotations import re @@ -88,7 +87,6 @@ class CheckResult: skipped_reason: str | None = None - # --------------------------------------------------------------------------- # Phase 2 — sort model and constant allocation # --------------------------------------------------------------------------- @@ -879,13 +877,53 @@ def _check_constant_predicate(enc, statements) -> list[Finding]: findings.append(_inconclusive("constant_predicate", [text])) return findings + def check_agreement(statements, symbol_table) -> CheckResult: """Encode `statements` and run the seven core checks. Input mirrors analyzer.detect_contradictions(statements): a list of top-level statement ASTs. Never raises for out-of-fragment input — - UnencodableConstruct is caught at this boundary and reported via - CheckResult(encodable=False, skipped_reason=...). + UnencodableConstruct (and any other encoding failure — invariant 8) + is caught at this boundary and reported via + CheckResult(encodable=False, skipped_reason=...) rather than a + traceback or a false clean bill of health. """ - _import_z3() - raise NotImplementedError + z3mod = _import_z3() + start = time.monotonic() + try: + definitions = _build_definitions(statements) + enc = _Encoder(z3mod, symbol_table, definitions) + entries = _collect_deontic_entries(enc, statements) + + findings: list[Finding] = [] + cap = _cap_finding(len(entries)) + capped = cap is not None + if cap is not None: + findings.append(cap) + + unless_findings, swallowed = _check_unless_swallows_rule(enc, entries) + findings.extend(unless_findings) + findings.extend(_check_always_deny(enc, entries)) + findings.extend(_check_dead_forbid(enc, entries, swallowed)) + findings.extend(_check_require_forbid_conflict(enc, entries, capped)) + findings.extend(_check_redundant_forbid(enc, entries, capped)) + findings.extend(_check_dead_permit(enc, entries)) + findings.extend(_check_constant_predicate(enc, statements)) + except (UnencodableConstruct, NonlinearArithmetic) as exc: + return CheckResult( + findings=[], checked=0, + elapsed_ms=(time.monotonic() - start) * 1000, + encodable=False, skipped_reason=str(exc), + ) + except Exception as exc: # invariant 8 — never let anything escape + return CheckResult( + findings=[], checked=0, + elapsed_ms=(time.monotonic() - start) * 1000, + encodable=False, skipped_reason=f"{type(exc).__name__}: {exc}", + ) + + return CheckResult( + findings=findings, checked=len(entries), + elapsed_ms=(time.monotonic() - start) * 1000, + encodable=True, skipped_reason=None, + ) diff --git a/tests/test_checker.py b/tests/test_checker.py index 04921ab..9516955 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -915,3 +915,90 @@ def test_interpret_check_result_maps_unknown_to_inconclusive(): def test_solver_timeout_configured_at_5000ms(): assert checker._SOLVER_TIMEOUT_MS == 5000 + + +# --------------------------------------------------------------------------- +# Phase 7 — public API (Finding / CheckResult / check_agreement) +# --------------------------------------------------------------------------- + + +def test_check_agreement_clean_program_zero_findings(): + lines = [ + "remember a number called amount with 60", + "require amount is above 50", + "forbid amount is above 1000", + ] + session, results = run_lines(lines) + for r in results: + assert r.status.name == "SUCCESS", r.message + statements = [_parse_line(l) for l in lines] + result = checker.check_agreement(statements, session.symtab) + assert result.encodable is True + assert result.findings == [] + assert result.checked == 2 + assert result.skipped_reason is None + + +def test_check_agreement_out_of_fragment_is_reported_not_crashed(): + node = checker.RequireNode( + condition=checker.ConditionNode( + field=checker.EachPronoun(), op="above", value=checker.NumberLiteral(value=5), + ), + exception=None, + ) + result = checker.check_agreement([node], {}) + assert result.encodable is False + assert result.skipped_reason is not None + assert result.findings == [] + + +def test_check_agreement_never_raises_for_malformed_symbol_table(): + result = checker.check_agreement([], None) + assert result.encodable is False + assert result.skipped_reason is not None + + +def test_check_agreement_ti_q13_integration_rejects_via_encodable_false(): + """The manual-gate pairing: liminate.run() accepts and enforces this + program (see test_KNOWN_GAP_value_indirection_bypasses_the_linearity + _restriction in tests/test_arithmetic.py); check_agreement rejects it.""" + lines = [ + "remember a number called alpha with 10", + "remember a number called beta with 2", + "remember a value called doubled from beta multiplied by beta", + "forbid alpha is above doubled", + ] + session, results = run_lines(lines) + assert results[-1].status.name == "PROHIBITION_VIOLATED" + statements = [_parse_line(l) for l in lines] + result = checker.check_agreement(statements, session.symtab) + assert result.encodable is False + assert "doubled" in result.skipped_reason + + +def test_check_agreement_finds_unless_swallows_rule_end_to_end(): + lines = [ + "remember a number called amount with 10", + "forbid amount is above 1000 unless amount is above 0", + ] + session, results = run_lines(lines) + statements = [_parse_line(l) for l in lines] + result = checker.check_agreement(statements, session.symtab) + assert result.encodable is True + kinds = [f.kind for f in result.findings] + assert "unless_swallows_rule" in kinds + assert "dead_forbid" not in kinds # suppressed by check 4 + + +def test_check_agreement_descends_into_sequence_node(): + seq = checker.SequenceNode( + operations=[ + _parse_line("remember a number called amount with 10"), + _parse_line("require amount is above 5 and amount is below 3"), + ], + connectors=["and"], + ) + symtab = {"amount": SymbolEntry(name="amount", value=10, type="number")} + result = checker.check_agreement([seq], symtab) + assert result.encodable is True + assert any(f.kind == "always_deny" for f in result.findings)