From f632a99aedd687dabe0f4f3e8444214d151ff65c Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Tue, 21 Jul 2026 10:16:56 -0700 Subject: [PATCH] Add public check_source() and export the checker API check_agreement requires (statements, symbol_table); nothing public produced both, so external callers (the Halverson dry run against liminate-dev PR #89) had to reimplement the statement collector. Doing so on top of run._collect_deontic_statements silently breaks two of the seven checks: it drops DefineNode entirely (check 7 finds nothing) and never collects value-form remember lines (nonlinearity reached through a name goes undetected). check_source wires run() + a corrected collector together as one public entry point so that trap isn't there to walk into a second time. Co-Authored-By: Claude Sonnet 5 --- src/liminate/__init__.py | 6 ++ src/liminate/checker.py | 133 ++++++++++++++++++++++++++++++++++++ tests/test_checker.py | 142 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 281 insertions(+) diff --git a/src/liminate/__init__.py b/src/liminate/__init__.py index 8081120..c97ae8d 100644 --- a/src/liminate/__init__.py +++ b/src/liminate/__init__.py @@ -13,6 +13,7 @@ TestDomainPack, ) from .analyzer import SymbolEntry, analyze +from .checker import CheckerUnavailable, CheckResult, Finding, check_agreement, check_source from .interpreter import execute from .listener import listen from .lexer import leading_indent, tokenize @@ -27,8 +28,11 @@ "AdapterDone", "AdapterFailure", "AdapterUpdate", + "CheckResult", + "CheckerUnavailable", "ContractResult", "DomainPack", + "Finding", "LiminateResult", "LiveValueDeclaration", "LiveValueEntry", @@ -39,6 +43,8 @@ "TestAdapter", "TestDomainPack", "analyze", + "check_agreement", + "check_source", "execute", "leading_indent", "listen", diff --git a/src/liminate/checker.py b/src/liminate/checker.py index b79564e..6ba0d16 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -23,6 +23,7 @@ from dataclasses import dataclass from datetime import date +from .lexer import LexError, leading_indent, tokenize from .parser import ( ArithmeticNode, BareWord, @@ -42,8 +43,13 @@ RememberValueNode, RequireNode, SequenceNode, + parse, ) from .renderer import render +from .reorderer import reorder +from .result import LiminateResult +from .run import run +from .vocabulary import TokenType class CheckerUnavailable(Exception): @@ -927,3 +933,130 @@ def check_agreement(statements, symbol_table) -> CheckResult: elapsed_ms=(time.monotonic() - start) * 1000, encodable=True, skipped_reason=None, ) + + +# --------------------------------------------------------------------------- +# check_source — static inspection from contract text (Halverson dry run, +# liminate-dev PR #89, product findings 1/2) +# --------------------------------------------------------------------------- + +# check_agreement's _VERB_NAMES covers all four deontic verbs — widened +# from run._collect_deontic_statements's ("require", "forbid"), which only +# needs two for its narrower contradiction-detection use case. +_CHECK_DEONTIC_VERBS = ("require", "forbid", "permit", "expect") + + +def _collect_checkable_statements(source: str) -> list: + """Best-effort pre-pass collecting the top-level statement ASTs + check_agreement needs from raw contract text: every `define`, + `require`, `forbid`, `permit`, `expect`, and value-form `remember` + line at indent 0. + + Deliberately NOT a thin wrapper around run._collect_deontic_statements + — reusing that collector as-is silently breaks two of check_agreement's + seven checks: + + 1. `define` lines: run._collect_deontic_statements accumulates the + name into a local predicate_names set (so later require/forbid + applications parse correctly) and then `continue`s WITHOUT + appending the DefineNode. check_agreement's check 7 + (_check_constant_predicate) iterates DefineNode from the statement + list — a collector that drops it yields a silent zero-finding + result for check 7, not an error. + 2. `remember ... with/from ` lines that parse to a + RememberValueNode: _build_definitions scans the statement list for + these to build the name -> defining-expression map that + value-position name inlining (TI-Q13 closure) depends on. Without + them, nonlinear arithmetic reached through a name (e.g. `remember + a value called doubled from beta multiplied by beta`, then + `forbid x is above doubled`) is silently never caught. + + run._collect_deontic_statements itself is untouched — its output feeds + detect_contradictions in the live run() path, and changing what it + returns would alter contradiction-detection behavior for every + program. This is a deliberate duplicate of its scan structure, not a + shared helper, for exactly that reason. + + Anything that fails to tokenize/reorder/parse is silently skipped — + this pass is advisory and must never introduce an error check_source's + own run() call wouldn't also produce. Indented lines (when-block + action lines) are excluded, matching the forward-declaration rule for + predicate names run._collect_deontic_statements also follows. + """ + statements: list = [] + predicate_names: set[str] = set() + for line in source.splitlines(): + stripped = line.lstrip() + if not stripped or stripped.startswith("--"): + continue + try: + if leading_indent(line) != 0: + continue + toks = tokenize(line) + except LexError: + continue + + if toks and toks[0].type is TokenType.DECLARATION and toks[0].value == "define": + reordered = reorder(toks) + if isinstance(reordered, LiminateResult): + continue + node = parse(reordered, predicate_names=predicate_names) + if isinstance(node, DefineNode): + predicate_names.add(node.name) + statements.append(node) + continue + + if not (toks and toks[0].type is TokenType.VERB): + continue + verb = toks[0].value + if verb not in _CHECK_DEONTIC_VERBS and verb != "remember": + continue + + reordered = reorder(toks) + if isinstance(reordered, LiminateResult): + continue + node = parse(reordered, predicate_names=predicate_names) + if isinstance(node, LiminateResult): + continue + + if verb == "remember": + if isinstance(node, RememberValueNode): + statements.append(node) + continue + + statements.append(node) + return statements + + +def check_source(source: str, *, domain_packs=None) -> CheckResult: + """Static inspection of contract text: check_agreement, wired up from + source instead of hand-built statements + a symbol table. + + Runs `run(source, domain_packs=domain_packs, enter_phase2=False, + auto_confirm_amber=True)` to populate a symbol table without entering + Phase 2 (this is static inspection, not execution — no listener, no + I/O) and without leaving an amber outcome unresolved. Collects the + top-level define/require/forbid/permit/expect/remember statement ASTs + from the same source text — see `_collect_checkable_statements`; in + particular, `define` and value-form `remember` lines must both be + collected, or check 7 and nonlinearity detection silently go inert. + Hands both to `check_agreement` and returns its `CheckResult` + unchanged — no wrapping, no extra fields. A caller that also needs + the symbol table calls `run()` directly instead. + + Never catches `CheckerUnavailable` — it propagates exactly as + `check_agreement` raises it (z3 not installed). An out-of-fragment + program is not an error either: `check_agreement` reports it as + `CheckResult(encodable=False, skipped_reason=...)`, passed through + unchanged. A program that fails to parse entirely collects zero + statements and reports `checked=0` with no findings — also not an + error; a caller wanting parse diagnostics should call `run()`. + """ + contract_result = run( + source, + domain_packs=domain_packs, + enter_phase2=False, + auto_confirm_amber=True, + ) + statements = _collect_checkable_statements(source) + return check_agreement(statements, contract_result.symbol_table) diff --git a/tests/test_checker.py b/tests/test_checker.py index 9516955..9ed92d7 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -1002,3 +1002,145 @@ def test_check_agreement_descends_into_sequence_node(): result = checker.check_agreement([seq], symtab) assert result.encodable is True assert any(f.kind == "always_deny" for f in result.findings) + + +# --------------------------------------------------------------------------- +# Phase 8 — check_source: public export + text-in, CheckResult-out +# --------------------------------------------------------------------------- + + +def test_liminate_package_importable_without_z3(): + """`import liminate` must succeed even when z3 cannot be imported at + all — mirrors test_checker_module_importable_without_z3 above, but for + the package root now that it re-exports names from checker.py.""" + 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\n" + "assert callable(liminate.check_agreement)\n" + "assert callable(liminate.check_source)\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_and_friends_exported_from_package(): + import liminate + + assert liminate.check_agreement is checker.check_agreement + assert liminate.CheckResult is checker.CheckResult + assert liminate.Finding is checker.Finding + assert liminate.CheckerUnavailable is checker.CheckerUnavailable + assert liminate.check_source is checker.check_source + for name in ( + "CheckerUnavailable", "CheckResult", "Finding", + "check_agreement", "check_source", + ): + assert name in liminate.__all__ + + +def test_check_source_finds_unless_swallows_rule(): + source = "\n".join([ + "remember a number called amount with 10", + "forbid amount is above 1000 unless amount is above 0", + ]) + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is True + kinds = [f.kind for f in result.findings] + assert "unless_swallows_rule" in kinds + + +def test_check_source_finds_constant_predicate_regression_for_define_node(): + """Regression test for the DefineNode trap: a naive collector built on + run._collect_deontic_statements tracks `define` names into + predicate_names but never appends the DefineNode itself, so check 7 + (_check_constant_predicate, which iterates DefineNode from the + statement list) silently finds nothing. This program has zero + require/forbid/permit/expect statements — checked stays 0 — but must + still surface the constant_predicate finding for the tautological + `define`.""" + source = "define always_big_or_small: is above 0 or is below 1000000" + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is True + assert result.checked == 0 + kinds = [f.kind for f in result.findings] + assert "constant_predicate" in kinds + + +def test_check_source_threads_predicate_names_matches_hand_built_ast(): + """Both require and forbid apply the named predicate `big` to the same + field — proves check_source's collector threads predicate_names the + same way a hand-built AST list (built exactly like the rest of this + file's tests do, via _parse_line with predicate_names threaded by + hand) would, rather than misparsing `is big` as string equality.""" + lines = [ + "remember a number called cutoff with 100", + "define big: is above cutoff", + "remember a number called amount with 150", + "require amount is big", + "forbid amount is big", + ] + source = "\n".join(lines) + session, results = run_lines(lines) + for r in results: + assert r.status.name in ("SUCCESS", "PROHIBITION_VIOLATED"), r.message + + predicate_names = set() + define_ast = _parse_line(lines[1], predicate_names=predicate_names) + predicate_names.add(define_ast.name) + hand_built = [ + define_ast, + _parse_line(lines[3], predicate_names=predicate_names), + _parse_line(lines[4], predicate_names=predicate_names), + ] + + expected = checker.check_agreement(hand_built, session.symtab) + actual = checker.check_source(source) + + assert actual.encodable == expected.encodable + assert actual.checked == expected.checked + assert [(f.kind, f.severity, f.statements) for f in actual.findings] == [ + (f.kind, f.severity, f.statements) for f in expected.findings + ] + assert [f.kind for f in actual.findings] == ["require_forbid_conflict"] + + +def test_check_source_out_of_fragment_nonlinear_via_remembered_name(): + """Doubles as the RememberValueNode-collection regression test: the + nonlinearity in `doubled`'s definition (beta multiplied by beta, both + runtime names) is only visible to check_agreement if the collector + appended `doubled`'s RememberValueNode into the statement list for + _build_definitions to find. A collector that only gathers deontic + verbs (dropping value-form remember lines) would hand check_agreement + a `doubled` that resolves to an opaque, already-allocated constant — + missing the nonlinear multiplication entirely and reporting a clean + (wrong) bill of health instead of encodable=False.""" + source = "\n".join([ + "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", + ]) + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is False + assert result.skipped_reason is not None + assert "doubled" in result.skipped_reason + + +def test_check_source_unparseable_source_returns_checked_zero_no_raise(): + result = checker.check_source("gibberish nonsense flarn blorp") + assert isinstance(result, checker.CheckResult) + assert result.checked == 0 + assert result.findings == []