Per-statement encodability in check_agreement

[rmichaelthomas]

Summary

check_agreement() previously aborted the entire contract when any single statement failed to encode — the abort happened inside _collect_deontic_entries, before any of the seven checks ran, so findings was never computed rather than computed-and-discarded. This makes encodability per-statement: a statement that fails to encode is recorded (text/reason/verb) in a new CheckResult.unencodable list and excluded; every remaining statement still proceeds through all seven checks.

• UnencodableStatement dataclass (text, reason, verb) added alongside Finding.
• CheckResult gains unencodable: list[UnencodableStatement] = field(default_factory=list) — last, defaulted, so existing positional construction sites keep working.
• _collect_deontic_entries and _check_constant_predicate (check 7) now each return (results, unencodable) tuples, catching UnencodableConstruct/NonlinearArithmetic per statement instead of letting them propagate to the outer contract-level catch.
• Field semantics (TI-Q15, LOCKED): checked counts statements that actually encoded; encodable is False only when zero statements encoded; skipped_reason is set only when encodable is False; unencodable may be non-empty while encodable is True.
• Version bump 0.17.1 → 0.18.0 (additive field, no breaking change).

Consistency invariants satisfied

1. encodable === (checked > 0) holds in every CheckResult path, including both outer except branches (unencodable=[] added to each).
2. unencodable is always a list, never null.
3. UnencodableStatement.text is render(node) — the same canonical rendering used elsewhere, untouched, so the join with Observatory's node.canonical holds.
4. _DeonticEntry.index stays dense — index=len(entries) evaluated after skipping unencodable statements, so Z3 tracked-assertion names never collide.
5. All seven check functions are unchanged; they just receive a shorter entries list.
6. No reserved words added — vocabulary stays at 61.

A real edge case this surfaced

A contract containing only a define (no require/forbid/permit/expect) and zero deontic statements now reports encodable=False/checked=0 even when that one define's own check-7 encoding succeeds and produces a finding — because checked/encodable are scoped strictly to deontic entries per the locked spec's literal implementation, and findings is never gated on checked. Updated test_check_source_finds_constant_predicate_regression_for_define_node to match (previously this combination — checked=0 yet encodable=True — was only possible because encodable was hardcoded True on any non-exceptional path).

Test plan

• pytest tests/ — 1851 passed, 0 failed, 0 skipped.
• pytest tests/test_vocabulary.py — 18 passed; reserved-word count unchanged at 61.
• pytest tests/test_checker.py — 137 passed, including 6 new tests covering: partial encodability, total failure, clean-contract regression (unencodable == []), nonlinear exclusion alongside a clean statement, index density across a mid-list exclusion, and an unencodable define that still emits its inconclusive finding.
• Two pre-existing tests updated for the locked, intentional behavior change (tuple-returning _collect_deontic_entries/_check_constant_predicate call sites bulk-fixed; two assertions moved from skipped_reason content to unencodable[].reason since skipped_reason is now a generic string for the all-unencodable case).

🤖 Generated with Claude Code