From 0632100a4b38afd30f3ba5118467aed0ee8802a4 Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Tue, 21 Jul 2026 11:57:40 -0700 Subject: [PATCH] Make check_source work on unbound rule templates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit check_source (shipped in PR #65) passed run()'s symbol table straight to check_agreement, so any referenced-but-unbound evidence field raised UnencodableConstruct and every unbound rule template — every Translate draft, and every shipped agreement template in liminate-dev's app/agreement_templates.py — reported encodable=False (Halverson dry run, PR #89, finding 1). Adds a type-inference pre-pass inside check_source only: for each referenced-but-unbound field, infer a scalar type from a literal comparison or a defined predicate's own body, and synthesize a type-only placeholder SymbolEntry (value=None) for it. A real remember/define binding always wins. A field typed by neither path stays unresolved and still correctly reports encodable=False — invariant 8 unchanged. check_agreement, the encoder, and the seven checks are untouched. Ported from case-studies/halverson/check-output/check_harness.py in liminate-dev, the working prototype this stage productionizes. Co-Authored-By: Claude Sonnet 5 --- src/liminate/checker.py | 148 ++++++++++++++++++++++++++++++++++++++-- tests/test_checker.py | 99 +++++++++++++++++++++++++++ 2 files changed, 243 insertions(+), 4 deletions(-) diff --git a/src/liminate/checker.py b/src/liminate/checker.py index 6ba0d16..e8cbfa8 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -23,6 +23,7 @@ from dataclasses import dataclass from datetime import date +from .analyzer import SymbolEntry from .lexer import LexError, leading_indent, tokenize from .parser import ( ArithmeticNode, @@ -1028,6 +1029,129 @@ def _collect_checkable_statements(source: str) -> list: return statements +# --------------------------------------------------------------------------- +# check_source's type-inference pre-pass — unbound rule templates +# --------------------------------------------------------------------------- +# +# A Translate draft — and every shipped agreement template in +# liminate-dev's app/agreement_templates.py — is an *unbound rule +# template* by design: it references evidence fields (amount, +# manager-approval, ...) that no `remember` binds, so run()'s symbol table +# has no entry for them. _build_constants then allocates nothing for the +# missing name, and encode_field raises UnencodableConstruct the first +# time a condition actually touches it, so check_source reported +# encodable=False for every such template (Halverson dry run, liminate-dev +# PR #89, finding 1). +# +# This pass synthesizes type-only placeholder SymbolEntry objects +# (value=None — the Z3 encoder only reads the type, in _build_constants, +# to allocate a free constant) for referenced-but-unbound fields, inferred +# from how each field is used: a literal it's directly compared against, +# or, for ` is `, the predicate's own body. A field +# typed by neither path stays unresolved and still raises +# UnencodableConstruct at check time — that is invariant 8 working +# correctly, not a gap to paper over. A real `remember`/`define` binding +# always wins over an inferred placeholder (see the `name not in +# symbol_table` guard in check_source below). +# +# Ported from case-studies/halverson/check-output/check_harness.py in +# liminate-dev (the working prototype), adapted to checker.py's naming. +# +# Known limit: the heuristic below is exercised against the Halverson +# corpus's condition shapes only. FieldAccessNode on records, and the +# `within` / `includes` operators, were never hit by that corpus and are +# not covered here — a field reached only through one of those shapes +# stays unresolved. Generalizing beyond what that corpus proved is +# separate work. + + +def _condition_leaves(node): + """Yield every ConditionNode/PredicateApplicationNode leaf inside a + condition tree, descending CompoundConditionNode's and/or shape.""" + if isinstance(node, CompoundConditionNode): + yield from _condition_leaves(node.left) + yield from _condition_leaves(node.right) + elif isinstance(node, (ConditionNode, PredicateApplicationNode)): + yield node + + +def _literal_type(value_node) -> str | None: + if isinstance(value_node, NumberLiteral): + return "number" + if isinstance(value_node, DateLiteral): + return "date" + if isinstance(value_node, (QuotedString, BareWord)): + return "string" + return None + + +def _predicate_subject_types(statements: list) -> dict[str, str]: + """For each `define : `, infer the scalar type a + subject must have to be applied to it via ` is ` — + mirrors _Encoder._value_sort_hint / _infer_subject_sort (used by check + 7's standalone predicate-body encoding), but runs pre-encoding on raw + ASTs rather than during Z3 constant allocation. E.g. `define large: is + above 5000` implies a number subject.""" + subject_types: dict[str, str] = {} + + def hint(cond) -> str | None: + if isinstance(cond, CompoundConditionNode): + return hint(cond.left) or hint(cond.right) + if isinstance(cond, ConditionNode) and isinstance(cond.field, EachPronoun): + t = _literal_type(cond.value) + if t is None and cond.value2 is not None: + t = _literal_type(cond.value2) + return t + return None + + for stmt in statements: + if isinstance(stmt, DefineNode): + t = hint(stmt.condition) + if t is not None: + subject_types[stmt.name] = t + return subject_types + + +_INFERABLE_DEONTIC_TYPES = (RequireNode, ForbidNode, PermitNode, ExpectNode) + + +def _infer_field_types(statements: list) -> dict[str, str]: + """Walk every deontic condition, exception, and define body for a bare + NameRef field and infer a scalar type — from the literal it's directly + compared against, or, for a predicate application (` is + `), from the predicate's own body via `_predicate_subject_types`. + First inference wins; a field typed by neither path is simply absent + from the result and stays unresolved (raises UnencodableConstruct at + check time, same as any other out-of-fragment reference).""" + types: dict[str, str] = {} + subject_types = _predicate_subject_types(statements) + + def note(name: str, scalar_type: str | None) -> None: + if scalar_type is not None: + types.setdefault(name, scalar_type) + + def walk_condition(cond) -> None: + for leaf in _condition_leaves(cond): + if isinstance(leaf, ConditionNode) and isinstance(leaf.field, NameRef): + note(leaf.field.name, _literal_type(leaf.value)) + if leaf.value2 is not None: + note(leaf.field.name, _literal_type(leaf.value2)) + elif isinstance(leaf, PredicateApplicationNode) and isinstance( + leaf.subject, NameRef + ): + note(leaf.subject.name, subject_types.get(leaf.predicate_name)) + + for stmt in statements: + if isinstance(stmt, DefineNode): + walk_condition(stmt.condition) + elif isinstance(stmt, _INFERABLE_DEONTIC_TYPES): + walk_condition(stmt.condition) + if stmt.exception is not None: + walk_condition(stmt.exception) + + return types + + 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. @@ -1040,9 +1164,21 @@ def check_source(source: str, *, domain_packs=None) -> CheckResult: 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. + + A contract source is very often an *unbound rule template* — it + references evidence fields no `remember` in the source ever binds, so + run()'s symbol table has no entry for them. Before handing off to + check_agreement, this function adds a type-only placeholder + SymbolEntry (see `_infer_field_types`) for every referenced-but-unbound + field it can infer a scalar type for; a real binding from `run()` + always takes precedence. A field neither bound nor inferable is left + alone and still surfaces as `encodable=False` from check_agreement's + own UnencodableConstruct boundary. + + Hands the (possibly widened) symbol table and the collected statements + to `check_agreement` and returns its `CheckResult` unchanged — no + wrapping, no extra fields. A caller that also needs the real symbol + table calls `run()` directly instead. Never catches `CheckerUnavailable` — it propagates exactly as `check_agreement` raises it (z3 not installed). An out-of-fragment @@ -1059,4 +1195,8 @@ def check_source(source: str, *, domain_packs=None) -> CheckResult: auto_confirm_amber=True, ) statements = _collect_checkable_statements(source) - return check_agreement(statements, contract_result.symbol_table) + symbol_table = dict(contract_result.symbol_table) + for name, scalar_type in _infer_field_types(statements).items(): + if name not in symbol_table: + symbol_table[name] = SymbolEntry(name=name, value=None, type=scalar_type) + return check_agreement(statements, symbol_table) diff --git a/tests/test_checker.py b/tests/test_checker.py index 9ed92d7..bbd566c 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -1144,3 +1144,102 @@ def test_check_source_unparseable_source_returns_checked_zero_no_raise(): assert isinstance(result, checker.CheckResult) assert result.checked == 0 assert result.findings == [] + + +# --------------------------------------------------------------------------- +# Phase 9 — check_source's type-inference pre-pass for unbound rule +# templates (Halverson dry run, liminate-dev PR #89, finding 1) +# --------------------------------------------------------------------------- + + +def test_check_source_encodes_unbound_template_and_finds_violation(): + """Regression test for the whole stage: before the type-inference + pre-pass, check_source(source) passed run()'s symbol table straight to + check_agreement, and a field no `remember` ever bound (here, `amount`) + raised UnencodableConstruct at encode_field, reported as + encodable=False. `amount` is only ever referenced, never bound — the + inference pass must type it from the literal `5000` and the check must + still find the genuine unless_swallows_rule violation.""" + source = 'forbid amount is above 5000 unless amount is above 0 because "policy"' + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is True + assert result.skipped_reason is None + kinds = [f.kind for f in result.findings] + assert "unless_swallows_rule" in kinds + + +def test_check_source_encodes_real_shipped_vendor_invoice_review_template(): + """The exact template shipped in liminate-dev's + app/agreement_templates.py (AGREEMENT_TEMPLATES, id + 'vendor_invoice_review'), copied verbatim rather than imported across + repos. Every evidence field it references — amount, manager-approval, + purchase-order, approval-status — has no `remember` binding it + anywhere in the source; this is the exact document finding 1 verified + against and must be encodable now.""" + source = "\n".join([ + 'remember a string called agreement-purpose with "vendor invoice review"', + "define large: is above 5000", + 'require amount is above 0 because "an invoice must have a positive amount"', + 'forbid amount is large unless manager-approval is equal to "yes" ' + 'because "large invoices need manager sign-off"', + 'require purchase-order is equal to "matched" because ' + '"every invoice must match a PO"', + 'permit approval-status is equal to "ready" because ' + '"all invoice criteria are met"', + ]) + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is True + assert result.skipped_reason is None + + +def test_check_source_real_remember_not_overwritten_by_inference(): + """A field bound by a real `remember` (here, `amount` as a number) + must win over the inference pass, even when the inferred type from a + literal comparison elsewhere in the source would disagree (here, + comparing `amount` against a quoted string would infer 'string'). If + the placeholder ever overwrote the real binding, this program would + encode cleanly as a same-sort string comparison; because the real + number binding takes precedence, comparing a Real constant against a + StringVal is a genuine sort mismatch and must be reported as + encodable=False, not silently swallowed (invariant 8).""" + source = "\n".join([ + "remember a number called amount with 3000", + 'forbid amount is equal to "five thousand" because "policy"', + ]) + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is False + assert result.skipped_reason is not None + + +def test_check_source_field_typed_only_via_predicate_application(): + """`amount` is never compared against a literal directly — its only + appearance is `amount is large`, a PredicateApplicationNode. The type + must be resolved through `large`'s own body (`is above 5000`, a number + comparison) via `_predicate_subject_types`, not left unresolved.""" + source = "\n".join([ + "define large: is above 5000", + 'forbid amount is large because "policy"', + ]) + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is True + assert result.skipped_reason is None + assert result.checked == 1 + + +def test_check_source_untypeable_field_stays_encodable_false_no_raise(): + """`category` is referenced only via `includes`, whose target must be + a statically known list (a real list_of_* symbol-table entry) — the + inference pass only ever produces scalar (number/string/date) + placeholders, so `category` stays untypeable for this purpose and the + program must still surface as encodable=False through check_agreement's + normal UnencodableConstruct boundary, never raise.""" + source = 'forbid category includes "restricted" because "policy"' + result = checker.check_source(source) + assert isinstance(result, checker.CheckResult) + assert result.encodable is False + assert result.skipped_reason is not None + assert result.findings == []