diff --git a/pyproject.toml b/pyproject.toml index ff97329..e4f8398 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,6 @@ [project] name = "liminate" -version = "0.17.1" +version = "0.18.0" description = "A prose-as-syntax language designed from the human end." requires-python = ">=3.10" license = "Apache-2.0" diff --git a/src/liminate/checker.py b/src/liminate/checker.py index c3d2487..81a12e2 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -20,7 +20,7 @@ import re import time -from dataclasses import dataclass +from dataclasses import dataclass, field from datetime import date from .analyzer import SymbolEntry @@ -84,6 +84,13 @@ class Finding: explanation: str +@dataclass +class UnencodableStatement: + text: str # render(node) — the canonical rendering + reason: str # str(exc) from the caught exception + verb: str # "require" | "forbid" | "permit" | "expect" | "define" + + @dataclass class CheckResult: findings: list[Finding] @@ -91,6 +98,7 @@ class CheckResult: elapsed_ms: float encodable: bool skipped_reason: str | None = None + unencodable: list[UnencodableStatement] = field(default_factory=list) # --------------------------------------------------------------------------- @@ -610,18 +618,27 @@ class _DeonticEntry: text: str -def _collect_deontic_entries(enc, statements) -> list[_DeonticEntry]: +def _collect_deontic_entries( + enc, statements +) -> tuple[list[_DeonticEntry], list[UnencodableStatement]]: entries = [] + unencodable = [] for stmt in _iter_statements(statements): verb = _VERB_NAMES.get(type(stmt)) if verb is None: continue - effect, allowed = enc.encode_deontic(stmt) + try: + effect, allowed = enc.encode_deontic(stmt) + except (UnencodableConstruct, NonlinearArithmetic) as exc: + unencodable.append(UnencodableStatement( + text=render(stmt), reason=str(exc), verb=verb, + )) + continue entries.append(_DeonticEntry( index=len(entries), verb=verb, node=stmt, effect=effect, allowed=allowed, text=render(stmt), )) - return entries + return entries, unencodable def _tracked_name(index, verb) -> str: @@ -835,10 +852,13 @@ def _check_dead_permit(enc, entries) -> list[Finding]: return findings -def _check_constant_predicate(enc, statements) -> list[Finding]: +def _check_constant_predicate( + enc, statements +) -> tuple[list[Finding], list[UnencodableStatement]]: """Check 7 — for each `define`, is its body a contradiction (always false) or a tautology (always true) for any possible subject?""" findings = [] + unencodable = [] for stmt in _iter_statements(statements): if not isinstance(stmt, DefineNode): continue @@ -847,7 +867,7 @@ def _check_constant_predicate(enc, statements) -> list[Finding]: body_formula = enc.encode_predicate_body_standalone( stmt.name, stmt.condition ) - except UnencodableConstruct: + except UnencodableConstruct as exc: findings.append(Finding( kind="inconclusive", severity="info", statements=[text], explanation=( @@ -856,6 +876,9 @@ def _check_constant_predicate(enc, statements) -> list[Finding]: f"for it." ), )) + unencodable.append(UnencodableStatement( + text=text, reason=str(exc), verb="define", + )) continue contradiction, _ = _run_query( @@ -881,7 +904,7 @@ def _check_constant_predicate(enc, statements) -> list[Finding]: )) elif tautology == "unknown": findings.append(_inconclusive("constant_predicate", [text])) - return findings + return findings, unencodable def check_agreement(statements, symbol_table) -> CheckResult: @@ -899,7 +922,7 @@ def check_agreement(statements, symbol_table) -> CheckResult: try: definitions = _build_definitions(statements) enc = _Encoder(z3mod, symbol_table, definitions) - entries = _collect_deontic_entries(enc, statements) + entries, unencodable = _collect_deontic_entries(enc, statements) findings: list[Finding] = [] cap = _cap_finding(len(entries)) @@ -914,24 +937,34 @@ def check_agreement(statements, symbol_table) -> CheckResult: 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)) + predicate_findings, predicate_unencodable = _check_constant_predicate( + enc, statements + ) + findings.extend(predicate_findings) + unencodable.extend(predicate_unencodable) except (UnencodableConstruct, NonlinearArithmetic) as exc: return CheckResult( findings=[], checked=0, elapsed_ms=(time.monotonic() - start) * 1000, - encodable=False, skipped_reason=str(exc), + encodable=False, skipped_reason=str(exc), unencodable=[], ) 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}", + unencodable=[], ) return CheckResult( - findings=findings, checked=len(entries), + findings=findings, + checked=len(entries), elapsed_ms=(time.monotonic() - start) * 1000, - encodable=True, skipped_reason=None, + encodable=len(entries) > 0, + skipped_reason=( + None if entries else "No statement in this contract could be encoded." + ), + unencodable=unencodable, ) diff --git a/tests/test_checker.py b/tests/test_checker.py index 34a203a..b190b49 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -694,7 +694,7 @@ def test_check1_always_deny_positive(): "remember a number called amount with 10", "require amount is above 50 and amount is below 10", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_always_deny(enc, entries) assert len(findings) == 1 assert findings[0].severity == "error" @@ -705,7 +705,7 @@ def test_check1_always_deny_negative(): "remember a number called amount with 10", "require amount is above 5", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_always_deny(enc, entries) assert findings == [] @@ -715,7 +715,7 @@ def test_check2_dead_forbid_positive(): "remember a number called amount with 10", "forbid amount is above 50 and amount is below 10", ]) - entries = checker._collect_deontic_entries(enc, statements) + 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" @@ -726,7 +726,7 @@ def test_check2_dead_forbid_negative(): "remember a number called amount with 10", "forbid amount is above 50", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_dead_forbid(enc, entries, swallowed=set()) assert findings == [] @@ -737,7 +737,7 @@ def test_check3_require_forbid_conflict_positive(): "require amount is above 100", "forbid amount is above 50", ]) - entries = checker._collect_deontic_entries(enc, statements) + 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" @@ -749,7 +749,7 @@ def test_check3_require_forbid_conflict_negative(): "require amount is above 100", "forbid amount is above 200", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_require_forbid_conflict(enc, entries, capped=False) assert findings == [] @@ -760,7 +760,7 @@ def test_check3_skipped_when_capped(): "require amount is above 100", "forbid amount is above 50", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_require_forbid_conflict(enc, entries, capped=True) assert findings == [] @@ -770,7 +770,7 @@ def test_check4_unless_swallows_rule_positive_forbid(): "remember a number called amount with 10", "forbid amount is above 1000 unless amount is above 0", ]) - entries = checker._collect_deontic_entries(enc, statements) + 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" @@ -782,7 +782,7 @@ def test_check4_unless_swallows_rule_positive_require(): "remember a number called amount with 10", "require amount is above 5 unless amount is below 1000", ]) - entries = checker._collect_deontic_entries(enc, statements) + 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} @@ -793,7 +793,7 @@ def test_check4_unless_swallows_rule_negative(): "remember a number called amount with 10", "forbid amount is above 1000 unless amount is above 2000", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings, swallowed = checker._check_unless_swallows_rule(enc, entries) assert findings == [] assert swallowed == set() @@ -804,7 +804,7 @@ def test_check4_suppresses_check2_for_same_statement(): "remember a number called amount with 10", "forbid amount is above 1000 unless amount is above 0", ]) - entries = checker._collect_deontic_entries(enc, statements) + 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") @@ -817,7 +817,7 @@ def test_check5_redundant_forbid_positive(): "forbid amount is above 100", "forbid amount is above 50", ]) - entries = checker._collect_deontic_entries(enc, statements) + 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" @@ -831,7 +831,7 @@ def test_check5_redundant_forbid_negative(): "forbid amount is above 50", 'forbid status is equal to "blocked"', ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_redundant_forbid(enc, entries, capped=False) assert findings == [] @@ -842,7 +842,7 @@ def test_check5_skipped_when_capped(): "forbid amount is above 100", "forbid amount is above 50", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_redundant_forbid(enc, entries, capped=True) assert findings == [] @@ -853,7 +853,7 @@ def test_check6_dead_permit_positive(): "require amount is below 10", "permit amount is above 50", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_dead_permit(enc, entries) assert len(findings) == 1 assert findings[0].severity == "warning" @@ -865,7 +865,7 @@ def test_check6_dead_permit_negative(): "require amount is below 100", "permit amount is above 50", ]) - entries = checker._collect_deontic_entries(enc, statements) + entries, _ = checker._collect_deontic_entries(enc, statements) findings = checker._check_dead_permit(enc, entries) assert findings == [] @@ -874,7 +874,7 @@ 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) + 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 @@ -884,7 +884,7 @@ 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) + findings, _ = checker._check_constant_predicate(enc, statements) assert len(findings) == 1 assert findings[0].severity == "warning" @@ -894,7 +894,7 @@ def test_check7_constant_predicate_negative_resolves_outer_symbol(): "remember a number called cutoff with 100", "define big: is above cutoff", ]) - findings = checker._check_constant_predicate(enc, statements) + findings, _ = checker._check_constant_predicate(enc, statements) assert findings == [] @@ -981,7 +981,9 @@ def test_check_agreement_ti_q13_integration_rejects_via_encodable_false(): 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 + assert result.checked == 0 + assert len(result.unencodable) == 1 + assert "doubled" in result.unencodable[0].reason def test_check_agreement_finds_unless_swallows_rule_end_to_end(): @@ -1012,6 +1014,128 @@ def test_check_agreement_descends_into_sequence_node(): assert any(f.kind == "always_deny" for f in result.findings) +# --------------------------------------------------------------------------- +# Phase 7b — per-statement encodability (TI-Q15, LOCKED): a statement that +# fails to encode is recorded in CheckResult.unencodable and excluded, while +# every remaining statement still proceeds through all seven checks. +# --------------------------------------------------------------------------- + + +def test_check_agreement_clean_contract_regression_unencodable_empty(): + """A fully encodable contract behaves byte-identically to pre-change + output, plus the new field defaults to empty.""" + 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 + assert result.unencodable == [] + + +def test_check_source_partial_encodability_excludes_one_checks_the_rest(): + """Three encodable deontics plus one referencing an unresolvable field + ('category' is only ever compared via 'includes', which the + type-inference pass can't type) — the unresolvable one is excluded, + the other three still run through all seven checks.""" + source = "\n".join([ + "remember a number called amount with 60", + 'require amount is above 5000 and amount is below 10 because "policy"', + 'forbid amount is above 100000 because "policy"', + 'permit amount is below 200 because "policy"', + 'forbid category includes "restricted" because "policy"', + ]) + result = checker.check_source(source) + assert result.encodable is True + assert result.checked == 3 + assert len(result.unencodable) == 1 + assert result.unencodable[0].verb == "forbid" + assert any(f.kind == "always_deny" for f in result.findings) + + +def test_check_source_total_failure_all_unencodable(): + """Every statement unencodable: encodable is False, checked is 0, and + skipped_reason is set — but unencodable is populated per statement + rather than the whole contract going dark with zero information.""" + source = "\n".join([ + 'forbid category includes "restricted" because "policy"', + 'require flavor includes "premium" because "policy"', + ]) + result = checker.check_source(source) + assert result.encodable is False + assert result.checked == 0 + assert result.skipped_reason is not None + assert len(result.unencodable) == 2 + + +def test_check_agreement_nonlinear_excluded_clean_forbid_still_checks(): + """The nonlinear statement (doubled = beta * beta, both runtime names) + lands in unencodable with a reason mentioning nonlinearity; a separate + clean forbid alongside it still gets checked.""" + 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", + "forbid alpha is above 1000", + ] + 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 + assert result.checked == 1 + assert len(result.unencodable) == 1 + assert result.unencodable[0].verb == "forbid" + assert "nonlinear" in result.unencodable[0].reason.lower() + + +def test_check_source_index_density_middle_exclusion_no_tracked_name_collision(): + """The second of four deontics is unencodable — the three surviving + entries must still produce findings without a Z3 tracked-name + collision (a collision would surface as a solver error, not a + silently wrong result).""" + source = "\n".join([ + "remember a number called amount with 60", + 'require amount is above 5000 and amount is below 10 because "policy"', + 'forbid category includes "restricted" because "policy"', + 'forbid amount is above 100000 because "policy"', + 'permit amount is below 200 because "policy"', + ]) + result = checker.check_source(source) + assert result.encodable is True + assert result.checked == 3 + assert len(result.unencodable) == 1 + assert any(f.kind == "always_deny" for f in result.findings) + + +def test_check_source_unencodable_define_lands_in_unencodable_and_still_emits_inconclusive(): + """A `define` whose subject type can't be inferred (its body compares + the implicit subject to a name that resolves to no known scalar type) + appears in unencodable with verb == 'define', and check 7 still emits + its existing inconclusive finding — the new field is additive.""" + source = "\n".join([ + "remember a number called amount with 60", + "define weird: is equal to placeholder", + 'require amount is above 10 because "policy"', + ]) + result = checker.check_source(source) + assert result.encodable is True + assert any( + f.kind == "inconclusive" and f.severity == "info" for f in result.findings + ) + define_entries = [u for u in result.unencodable if u.verb == "define"] + assert len(define_entries) == 1 + assert "subject type" in define_entries[0].reason + + # --------------------------------------------------------------------------- # Phase 8 — check_source: public export + text-in, CheckResult-out # --------------------------------------------------------------------------- @@ -1074,13 +1198,15 @@ def test_check_source_finds_constant_predicate_regression_for_define_node(): 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`.""" + require/forbid/permit/expect statements — checked (a count of encoded + deontic entries) stays 0, and per TI-Q15's encodable === (checked > 0) + invariant, encodable is therefore False even though the define's own + check still ran and found its finding — findings is not gated on + encodable/checked, only on what the seven checks actually produced.""" 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.encodable is False assert result.checked == 0 kinds = [f.kind for f in result.findings] assert "constant_predicate" in kinds @@ -1144,7 +1270,8 @@ def test_check_source_out_of_fragment_nonlinear_via_remembered_name(): assert isinstance(result, checker.CheckResult) assert result.encodable is False assert result.skipped_reason is not None - assert "doubled" in result.skipped_reason + assert len(result.unencodable) == 1 + assert "doubled" in result.unencodable[0].reason def test_check_source_unparseable_source_returns_checked_zero_no_raise():