Z3 encoder and seven core satisfiability checks (decidability Step 2)

[rmichaelthomas]

Summary

Step 2 of the decidability path (Trust Infrastructure Addendum v1.0s §91/§92.6). Adds src/liminate/checker.py: a satisfiability checker for Liminate's enforcement fragment — the four deontic verbs (require/forbid/permit/expect), their conditions, and the define predicates they reference — encoded into SMT constraints (QF_UFLIRA via Z3) with seven authoring-time checks.

Phases completed (one commit each)

1. Packaging — check optional-dependency extra (z3-solver>=4.12), lazy z3 import, CheckerUnavailable/UnencodableConstruct/NonlinearArithmetic exceptions, Finding/CheckResult dataclasses.
2. Sort model & constant allocation — number→Real, string→String, date→Int (epoch-day ordinals), per-field record constants, name sanitization with a reverse map.
3. Condition encoder — mirrors interpreter._eval_condition/_apply_op exactly: all comparison operators, within (value=tolerance, value2=target), includes/not_includes, predicate application with EachPronoun substitution and a depth guard.
4. Arithmetic, name inlining, TI-Q13 closure — a definitions map scanned from RememberValueNodes, inlining of arithmetic-containing defining expressions, and NonlinearArithmetic detection when neither operand of multiplied_by/divided_by is a compile-time constant.
5. Deontic effect formulas — encode_deontic reduces each verb to (effect, allowed) per the locked semantics table.
6. Seven core checks — always-deny, dead-forbid, require/forbid conflict, unless-swallows-the-rule, redundant-forbid, dead-permit, constant-predicate, each a tracked assert_and_track solver query with a 5000ms timeout and a 200-statement pairwise cap.
7. Public API — check_agreement(statements, symbol_table) -> CheckResult, with every encoding failure (including unexpected ones) caught at the boundary — never a traceback.

Files created / modified

• src/liminate/checker.py (new)
• tests/test_checker.py (new, 69 tests)
• pyproject.toml (+1 line: the check extra)

interpreter.py, analyzer.py, tests/test_arithmetic.py, tests/test_contradiction_detection.py, tests/test_vocabulary.py are untouched (confirmed via git diff — empty).

Suite

1763 passed / 0 failed / 0 skipped — up from the 1694 baseline on main@95daaf5, +69 new tests, zero regressions.

Vocabulary

Confirmed still 61 words — tests/test_vocabulary.py (18/18) unchanged and passing.

TI-Q13 (value-provenance indirection) — closed

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

• liminate.run() / the analyzer: accepts and enforces it (PROHIBITION_VIOLATED) — PR Accept bare dates in temporal prefixes; restrict arithmetic to linear forms #62's syntactic linearity check only sees a bare name in the condition, never the ArithmeticNode behind it.
• check_agreement(): rejects it — encodable=False, skipped_reason names 'doubled' and the nonlinear beta multiplied by beta term, by inlining the defining expression at encode time.

Design decisions beyond literal spec text

Five points were genuinely ambiguous in the build prompt; each is backed by a dedicated test:

1. Constant allocation skips (doesn't raise on) non-scalar symbol-table entries eagerly — UnencodableConstruct fires lazily only when a condition actually references one.
2. _is_compile_time_constant never resolves through name indirection, even when a name's own value is a literal — it's a free Z3 constant to the solver regardless.
3. divided_by uses the same uniform "neither operand constant" rule as multiplied_by (no asymmetric divisor-only rule).
4. Check 4 (unless-swallows-the-rule) is verb-adjusted — it tests each statement's own effect formula, not the literal C∧¬E notation applied invariantly (which is meaningless for require).
5. Check 7 infers a fresh subject's Z3 sort from how the predicate body compares it, falling back to an "inconclusive" finding if inference fails.

Invariants exercised by tests

All nine consistency invariants from the build prompt are covered: vocabulary frozen at 61 (§11.1), zero new runtime deps behind a lazy import (§11.2), operator semantics matching the interpreter (§11.3, throughout test_op_*), unless uniformly condition ∧ ¬exception (test_exception_none_collapses_to_false), interpreter.py/detect_contradictions untouched (§11.5–6, confirmed via git diff), the pinned KNOWN_GAP test unmodified (§11.7), no unhandled exception escapes check_agreement (§11.8, test_check_agreement_never_raises_for_malformed_symbol_table), and the suite growing monotonically with zero regressions (§11.9).

Manual gate

Reviewed and passed by Rob — full suite diff and check-4 CheckResult output confirmed clear before this PR was opened.

🤖 Generated with Claude Code

Co-Authored-By: Claude Sonnet 5 noreply@anthropic.com