diff --git a/grammar/encodability.json b/grammar/encodability.json index 91b44c3..188a927 100644 --- a/grammar/encodability.json +++ b/grammar/encodability.json @@ -5,82 +5,95 @@ "finding_kinds": [ { "kind": "inconclusive", - "source": "checker.py:671" + "source": "checker.py:808" }, { "kind": "inconclusive", - "source": "checker.py:683" + "source": "checker.py:820" }, { "kind": "always_deny", - "source": "checker.py:703" + "source": "checker.py:840" }, { "kind": "dead_forbid", - "source": "checker.py:726" + "source": "checker.py:863" }, { "kind": "require_forbid_conflict", - "source": "checker.py:754" + "source": "checker.py:891" }, { "kind": "unless_swallows_rule", - "source": "checker.py:783" + "source": "checker.py:920" }, { "kind": "redundant_forbid", - "source": "checker.py:813" + "source": "checker.py:950" }, { "kind": "dead_permit", - "source": "checker.py:842" + "source": "checker.py:979" }, { "kind": "inconclusive", - "source": "checker.py:871" + "source": "checker.py:1011" }, { "kind": "constant_predicate", - "source": "checker.py:888" + "source": "checker.py:1024" }, { "kind": "constant_predicate", - "source": "checker.py:901" + "source": "checker.py:1046" + }, + { + "kind": "inconclusive", + "source": "checker.py:1062" } ], "finding_kinds_missing_from_source": [], "encoder_exceptions": [ { "class": "UnencodableConstruct", - "defined_at": "checker.py:59", + "defined_at": "checker.py:67", "raised_at": [ - "checker.py:207", - "checker.py:214", - "checker.py:218", - "checker.py:251", - "checker.py:267", - "checker.py:274", - "checker.py:280", - "checker.py:285", - "checker.py:291", + "checker.py:220", + "checker.py:227", + "checker.py:231", + "checker.py:252", + "checker.py:270", + "checker.py:286", + "checker.py:293", + "checker.py:302", "checker.py:318", - "checker.py:343", - "checker.py:382", - "checker.py:431", - "checker.py:452", - "checker.py:593" + "checker.py:324", + "checker.py:351", + "checker.py:383", + "checker.py:437", + "checker.py:446", + "checker.py:450", + "checker.py:469", + "checker.py:475", + "checker.py:482", + "checker.py:500", + "checker.py:507", + "checker.py:519", + "checker.py:568", + "checker.py:589", + "checker.py:730" ] }, { "class": "NonlinearArithmetic", - "defined_at": "checker.py:63", + "defined_at": "checker.py:71", "raised_at": [ - "checker.py:371" + "checker.py:495" ] } ], "unencodable_reason_is_not_a_bounded_vocabulary": { - "source": "checker.py:90", + "source": "checker.py:98", "explanation": "checker.py's own UnencodableStatement.reason field is declared `reason: str # str(exc) from the caught exception` -- the reason recorded for a statement the checker could not encode is a stringified Python exception message, not a value drawn from a fixed set. This file cannot enumerate the possible reasons because the source does not define a bounded set of them: every `raised_at` site below constructs its message from an f-string built at the point of failure (interpolating the actual node, name, or operator involved), so the same raise site produces a different reason string for every different unencodable construct it sees. An agent consuming this file should treat `reason` as free text to display, never as a value to match against a known list." } } diff --git a/src/liminate/checker.py b/src/liminate/checker.py index 81a12e2..5a69f9f 100644 --- a/src/liminate/checker.py +++ b/src/liminate/checker.py @@ -2,9 +2,8 @@ Decidability Step 2 (Trust Infrastructure Addendum v1.0s §91/§92.6). Encodes an Agreement's deontic statements (require/forbid/permit/expect -and the define predicates they reference) into SMT constraints over -QF_UFLIRA and runs seven authoring-time checks that a human reading the -file would miss. +and the define predicates they reference) into SMT constraints and runs +seven authoring-time checks that a human reading the file would miss. Scope: the enforcement fragment only. No temporal encoding (starting_date / until_date are ignored — v1.0s §91.6), no trace semantics, no CLI verb. @@ -14,6 +13,14 @@ z3 is an optional dependency (the `check` extra). This module never imports z3 at top level — `import liminate.checker` must always succeed. The import happens lazily inside the public entry point. + +Numeric support is deliberately narrower than the interpreter's full +`int | float` value domain. Symbolic numeric facts must be known Python +integers. Finite decimal literals are encoded as their exact binary64 +values, and arithmetic made entirely from literals or literal arithmetic +definitions is evaluated with Python before encoding. Symbolic operations +that can round a float, and unknown or float-valued numeric facts, are +reported as unencodable. """ from __future__ import annotations @@ -22,6 +29,7 @@ import time from dataclasses import dataclass, field from datetime import date +from math import isfinite from .analyzer import SymbolEntry from .lexer import LexError, leading_indent, tokenize @@ -112,9 +120,9 @@ class CheckResult: _SANITIZE_RE = re.compile(r"[^A-Za-z0-9_]") # SymbolEntry.type / SymbolEntry.schema[field] values that map onto a -# scalar Z3 sort. Dates encode as Int via epoch-day ordinals (§9 fact 9 — -# never mixed with number's Real sort). +# scalar Z3 sort. Dates and supported integer-valued numbers encode as Int. _LIST_TYPES = frozenset({"list_of_strings", "list_of_numbers", "list_of_dates"}) +_NOT_CONSTANT = object() def _sanitize_base(name: str) -> str: @@ -162,8 +170,8 @@ def _sanitize(self, name: str) -> str: def _build_constants(self) -> None: for name, entry in self.symtab.items(): - if entry.type == "number": - self.constants[name] = self.z3.Real(self._sanitize(name)) + if entry.type == "number" and type(entry.value) is int: + self.constants[name] = self.z3.Int(self._sanitize(name)) elif entry.type == "string": self.constants[name] = self.z3.String(self._sanitize(name)) elif entry.type == "date": @@ -172,8 +180,13 @@ def _build_constants(self) -> None: for field_name, field_type in (entry.schema or {}).items(): key = f"{name}__{field_name}" ident = self._sanitize(key) - if field_type == "number": - self.constants[key] = self.z3.Real(ident) + field_value = ( + entry.value.get(field_name) + if isinstance(entry.value, dict) + else None + ) + if field_type == "number" and type(field_value) is int: + self.constants[key] = self.z3.Int(ident) elif field_type == "string": self.constants[key] = self.z3.String(ident) elif field_type == "date": @@ -233,8 +246,14 @@ def _encode_condition_leaf(self, cond): # §3 correction (1): value is the tolerance, value2 is the # target — mirrors interpreter._eval_condition exactly. field_val = self.encode_field(cond.field) - tolerance = self.encode_value(cond.value) target = self.encode_value(cond.value2) + tolerance = self.encode_value(cond.value) + if not self._is_int_sort(field_val) or not self._is_int_sort(target): + raise UnencodableConstruct( + "'within' needs an integer-valued field and target for " + "exact subtraction; a floating-point operand can round " + "in the interpreter." + ) return self.z3.And( field_val - target <= tolerance, target - field_val <= tolerance, @@ -266,7 +285,7 @@ def _python_literal(self, value): if isinstance(value, bool): raise UnencodableConstruct("Boolean list elements can't be encoded.") if isinstance(value, (int, float)): - return self.z3.RealVal(value) + return self._encode_number_literal(value) if isinstance(value, str): return self.z3.StringVal(value) if isinstance(value, date): @@ -277,11 +296,25 @@ def encode_field(self, node): if isinstance(node, NameRef): if node.name in self.constants: return self.constants[node.name] + entry = self.symtab.get(node.name) + if entry is not None and entry.type == "number": + raise self._unsupported_number_fact(node.name, entry.value) raise UnencodableConstruct(f"'{node.name}' isn't an encodable fact.") if isinstance(node, FieldAccessNode): key = f"{node.record_name}__{node.field}" if key in self.constants: return self.constants[key] + entry = self.symtab.get(node.record_name) + if ( + entry is not None + and entry.type == "record" + and (entry.schema or {}).get(node.field) == "number" + ): + values = entry.value if isinstance(entry.value, dict) else {} + raise self._unsupported_number_fact( + f"{node.field} of {node.record_name}", + values.get(node.field), + ) raise UnencodableConstruct( f"'{node.field} of {node.record_name}' isn't an encodable fact." ) @@ -299,7 +332,7 @@ def encode_field(self, node): def encode_value(self, node, origin_name=None): if isinstance(node, NumberLiteral): - return self.z3.RealVal(node.value) + return self._encode_number_literal(node.value) if isinstance(node, DateLiteral): return self.z3.IntVal(_date_ordinal(node.value)) if isinstance(node, QuotedString): @@ -320,6 +353,10 @@ def encode_value(self, node, origin_name=None): def _resolve_name_value(self, node): name = node.word if isinstance(node, BareWord) else node.name defining = self.definitions.get(name) + if defining is not None and self._contains_arithmetic(defining): + folded = self._evaluate_constant_value(node) + if folded is not _NOT_CONSTANT: + return self._encode_number_literal(folded) if ( defining is not None and self._contains_arithmetic(defining) @@ -336,6 +373,9 @@ def _resolve_name_value(self, node): self._inlining_visited.discard(name) if name in self.constants: return self.constants[name] + entry = self.symtab.get(name) + if entry is not None and entry.type == "number": + raise self._unsupported_number_fact(name, entry.value) if isinstance(node, BareWord): # Matches interpreter._eval_value: an unresolved BareWord is # a string literal, not an error. @@ -363,14 +403,111 @@ def _is_compile_time_constant(self, node) -> bool: ) return False + def _evaluate_constant_value(self, node, visited=None): + """Evaluate literal-only arithmetic with the interpreter's Python + operators, including its division result conversion. Arithmetic + definitions may be followed, but a name bound directly to a + literal remains a symbolic fact for the existing checker model. + """ + if visited is None: + visited = set() + if isinstance(node, NumberLiteral): + return node.value + if isinstance(node, ArithmeticNode): + left = self._evaluate_constant_value(node.left, visited) + right = self._evaluate_constant_value(node.right, visited) + if left is _NOT_CONSTANT or right is _NOT_CONSTANT: + return _NOT_CONSTANT + if ( + isinstance(left, bool) + or not isinstance(left, (int, float)) + or isinstance(right, bool) + or not isinstance(right, (int, float)) + ): + return _NOT_CONSTANT + try: + if node.op == "plus": + return left + right + if node.op == "minus": + return left - right + if node.op == "multiplied_by": + return left * right + if node.op == "divided_by": + if right == 0: + raise UnencodableConstruct( + "Literal division by zero is a runtime error and " + "cannot be verified." + ) + result = left / right + if isinstance(result, float) and result.is_integer(): + return int(result) + return result + except OverflowError as exc: + raise UnencodableConstruct( + "Literal arithmetic overflows the interpreter's " + "floating-point conversion." + ) from exc + raise UnencodableConstruct( + f"Unknown arithmetic operator '{node.op}'." + ) + if isinstance(node, (BareWord, NameRef)): + name = node.word if isinstance(node, BareWord) else node.name + if name in visited: + return _NOT_CONSTANT + defining = self.definitions.get(name) + if isinstance(defining, ArithmeticNode): + return self._evaluate_constant_value( + defining, visited | {name}, + ) + return _NOT_CONSTANT + + def _encode_number_literal(self, value): + if type(value) is int: + return self.z3.IntVal(value) + if isinstance(value, float): + if not isfinite(value): + raise UnencodableConstruct( + "Non-finite floating-point values aren't supported by " + "the mathematical checker." + ) + numerator, denominator = value.as_integer_ratio() + return self.z3.RealVal(f"{numerator}/{denominator}") + raise UnencodableConstruct(f"Can't encode numeric value {value!r}.") + + def _unsupported_number_fact(self, name, value): + if isinstance(value, float): + detail = "a floating-point runtime value" + else: + detail = "an unknown integer or floating-point runtime value" + return UnencodableConstruct( + f"'{name}' has {detail}; the mathematical checker supports " + "only integer-valued symbolic numeric facts." + ) + + def _is_int_sort(self, expression): + return expression.sort().kind() == self.z3.Z3_INT_SORT + def _encode_arithmetic(self, node, origin_name=None): if node.op in ("multiplied_by", "divided_by"): if not self._is_compile_time_constant( node.left ) and not self._is_compile_time_constant(node.right): raise NonlinearArithmetic(self._nonlinear_message(node, origin_name)) + folded = self._evaluate_constant_value(node) + if folded is not _NOT_CONSTANT: + return self._encode_number_literal(folded) + if node.op == "divided_by": + raise UnencodableConstruct( + "Division involving a symbolic number is unsupported because " + "the interpreter uses floating-point division." + ) left = self.encode_value(node.left, origin_name=origin_name) right = self.encode_value(node.right, origin_name=origin_name) + if not self._is_int_sort(left) or not self._is_int_sort(right): + raise UnencodableConstruct( + "Symbolic arithmetic with a floating-point operand is " + "unsupported because the interpreter rounds the result." + ) if node.op == "plus": return left + right if node.op == "minus": @@ -863,6 +1000,9 @@ def _check_constant_predicate( if not isinstance(stmt, DefineNode): continue text = render(stmt) + numeric_subject = ( + enc._infer_subject_sort(stmt.condition, set()) == "number" + ) try: body_formula = enc.encode_predicate_body_standalone( stmt.name, stmt.condition @@ -870,11 +1010,7 @@ def _check_constant_predicate( except UnencodableConstruct as exc: findings.append(Finding( kind="inconclusive", severity="info", statements=[text], - explanation=( - f"Couldn't determine a subject type for predicate " - f"'{stmt.name}' — check 7 (constant predicate) skipped " - f"for it." - ), + explanation=f"Check 7 couldn't encode predicate '{stmt.name}': {exc}", )) unencodable.append(UnencodableStatement( text=text, reason=str(exc), verb="define", @@ -892,6 +1028,15 @@ def _check_constant_predicate( continue if contradiction == "unknown": findings.append(_inconclusive("constant_predicate", [text])) + unencodable.append(UnencodableStatement( + text=text, + reason=( + "Z3 returned unknown while checking the numeric predicate." + if numeric_subject + else "Z3 returned unknown while checking the predicate." + ), + verb="define", + )) continue tautology, _ = _run_query( @@ -904,6 +1049,33 @@ def _check_constant_predicate( )) elif tautology == "unknown": findings.append(_inconclusive("constant_predicate", [text])) + unencodable.append(UnencodableStatement( + text=text, + reason=( + "Z3 returned unknown while checking the numeric predicate." + if numeric_subject + else "Z3 returned unknown while checking the predicate." + ), + verb="define", + )) + elif numeric_subject: + findings.append(Finding( + kind="inconclusive", severity="info", statements=[text], + explanation=( + f"Predicate '{stmt.name}' varies over mathematical reals; " + "the checker can't determine whether it is constant over " + "Liminate's integer and floating-point number values." + ), + )) + unencodable.append(UnencodableStatement( + text=text, + reason=( + "Numeric predicate subject may be an integer or a " + "floating-point value; a nonconstant real formula does " + "not establish its runtime behavior." + ), + verb="define", + )) return findings, unencodable diff --git a/tests/test_checker.py b/tests/test_checker.py index b190b49..fbac3d8 100644 --- a/tests/test_checker.py +++ b/tests/test_checker.py @@ -129,10 +129,10 @@ def test_constant_map_number_string_date_record_and_string_list(): } enc = checker._Encoder(z3, symtab, {}) - assert enc.constants["amount"].sort() == z3.RealSort() + assert enc.constants["amount"].sort() == z3.IntSort() assert enc.constants["status"].sort() == z3.StringSort() assert enc.constants["due"].sort() == z3.IntSort() - assert enc.constants["order1__total"].sort() == z3.RealSort() + assert enc.constants["order1__total"].sort() == z3.IntSort() assert enc.constants["order1__label"].sort() == z3.StringSort() # No constant is allocated for a list — membership expands to a @@ -895,7 +895,9 @@ def test_check7_constant_predicate_negative_resolves_outer_symbol(): "define big: is above cutoff", ]) findings, _ = checker._check_constant_predicate(enc, statements) - assert findings == [] + assert len(findings) == 1 + assert findings[0].kind == "inconclusive" + assert findings[0].severity == "info" def test_pairwise_cap_finding_helper(): @@ -1247,7 +1249,11 @@ def test_check_source_threads_predicate_names_matches_hand_built_ast(): 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"] + assert [f.kind for f in actual.findings] == [ + "require_forbid_conflict", "inconclusive", + ] + assert actual.unencodable + assert any(item.verb == "define" for item in actual.unencodable) def test_check_source_out_of_fragment_nonlinear_via_remembered_name(): @@ -1287,31 +1293,25 @@ def test_check_source_unparseable_source_returns_checked_zero_no_raise(): # --------------------------------------------------------------------------- -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.""" +def test_check_source_declines_unbound_numeric_template(): + """An unbound numeric field may be a Python int or float at runtime. + The mathematical checker must decline rather than treating it as an + unconstrained exact Real and certifying a result over the wrong domain.""" 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 + assert result.encodable is False + assert result.checked == 0 + assert result.unencodable + assert any("integer-valued symbolic" in item.reason for item in result.unencodable) -def test_check_source_encodes_real_shipped_vendor_invoice_review_template(): +def test_check_source_partially_checks_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.""" + repos. Its unbound numeric `amount` evidence must now be explicitly + declined; the remaining string-valued rules can still be checked.""" source = "\n".join([ 'remember a string called agreement-purpose with "vendor invoice review"', "define large: is above 5000", @@ -1327,6 +1327,8 @@ def test_check_source_encodes_real_shipped_vendor_invoice_review_template(): assert isinstance(result, checker.CheckResult) assert result.encodable is True assert result.skipped_reason is None + assert result.unencodable + assert any("integer-valued symbolic" in item.reason for item in result.unencodable) def test_check_source_real_remember_not_overwritten_by_inference(): @@ -1336,7 +1338,7 @@ def test_check_source_real_remember_not_overwritten_by_inference(): 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 + number binding takes precedence, comparing an Int constant against a StringVal is a genuine sort mismatch and must be reported as encodable=False, not silently swallowed (invariant 8).""" source = "\n".join([ @@ -1360,9 +1362,155 @@ def test_check_source_field_typed_only_via_predicate_application(): ]) result = checker.check_source(source) assert isinstance(result, checker.CheckResult) + assert result.encodable is False + assert result.checked == 0 + assert result.unencodable + assert any("integer-valued symbolic" in item.reason for item in result.unencodable) + + +def _assert_integer_numeric_support_declined(result): + assert result.encodable is False + assert result.checked == 0 + assert result.unencodable + assert all( + "integer" in item.reason.lower() + or "floating-point" in item.reason.lower() + for item in result.unencodable + ) + + +def test_check_source_declines_float_result_from_decimal_arithmetic(): + """The interpreter rounds 0.1 + 0.2 to 0.30000000000000004. The + checker must not analyze the resulting float-valued field as an + unconstrained mathematical Real.""" + source = "\n".join([ + "remember a value called total from 0.1 plus 0.2", + "require total is equal to 0.3", + ]) + session, runtime = run_lines(source.splitlines()) + + assert runtime[0].status.name == "SUCCESS" + assert runtime[1].status.name == "REQUIREMENT_NOT_MET" + assert session.symtab["total"].value == 0.30000000000000004 + + result = checker.check_source(source) + _assert_integer_numeric_support_declined(result) + + +def test_check_source_folds_repeated_float_intermediate_arithmetic(): + """Constant arithmetic definitions are evaluated in sequence with + Python's float rounding before the checker reasons about the final + integer comparison.""" + source = "\n".join([ + "remember a value called first from 0.1 plus 0.2", + "remember a value called second from first minus 0.3", + "remember a number called total with 0", + "require total is equal to second", + ]) + session, runtime = run_lines(source.splitlines()) + + assert [result.status.name for result in runtime] == [ + "SUCCESS", "SUCCESS", "SUCCESS", "REQUIREMENT_NOT_MET", + ] + assert session.symtab["first"].value == 0.30000000000000004 + assert session.symtab["second"].value == 5.551115123125783e-17 + + result = checker.check_source(source) assert result.encodable is True - assert result.skipped_reason is None - assert result.checked == 1 + assert result.unencodable == [] + assert any(f.kind == "always_deny" for f in result.findings) + + +@pytest.mark.parametrize(("definitions", "total"), [ + ([ + "remember a value called first from 2 plus 3", + "remember a value called second from 4 plus 5", + "remember a value called combined from first multiplied by second", + "require total is equal to combined", + ], 45), + ([ + "remember a value called numerator from 6 multiplied by 3", + "remember a value called denominator from 2 plus 1", + "remember a value called quotient from numerator divided by denominator", + "require total is equal to quotient", + ], 6), +]) +def test_check_source_folds_named_integer_arithmetic_intermediates( + definitions, total, +): + source = "\n".join([ + *definitions[:-1], + f"remember a number called total with {total}", + definitions[-1], + ]) + _, runtime = run_lines(source.splitlines()) + + assert all(result.status.name == "SUCCESS" for result in runtime) + result = checker.check_source(source) + assert result.encodable is True + assert result.unencodable == [] + + +def test_check_source_declines_float_domain_that_hides_runtime_conflict(): + """The two runtime conditions name the same float value. A Real model + admits exact decimal 0.3 as a witness that is not a Python int or + float, so the checker must decline rather than miss the conflict.""" + source = "\n".join([ + "remember a number called total with 0.30000000000000004", + "require total is equal to 0.1 plus 0.2", + "forbid total is equal to 0.30000000000000004", + ]) + session, runtime = run_lines(source.splitlines()) + + assert [result.status.name for result in runtime] == [ + "SUCCESS", "SUCCESS", "PROHIBITION_VIOLATED", + ] + assert session.symtab["total"].value == 0.30000000000000004 + + result = checker.check_source(source) + _assert_integer_numeric_support_declined(result) + assert not any(f.kind == "require_forbid_conflict" for f in result.findings) + + +def test_check_source_preserves_integer_arithmetic_and_float_thresholds(): + """Integer arithmetic remains exact, and direct int-vs-float + comparisons use the exact binary value of the decimal literal.""" + source = "\n".join([ + "remember a number called total with 1", + "require total is equal to 1 plus 0.00000000000000011102230246251565", + "require total is above 0.1", + ]) + session, runtime = run_lines(source.splitlines()) + + assert [result.status.name for result in runtime] == [ + "SUCCESS", "SUCCESS", "SUCCESS", + ] + result = checker.check_source(source) + assert result.encodable is True + assert result.unencodable == [] + assert not any(f.kind == "always_deny" for f in result.findings) + + +@pytest.mark.parametrize("source", [ + "\n".join([ + "remember a number called amount with 1", + "require amount is equal to amount plus 0.1", + ]), + "\n".join([ + "remember a number called amount with 1", + "require amount is equal to amount divided by 3", + ]), + "\n".join([ + "remember a number called amount with 1", + "require amount is within 0.1 of 0.9", + ]), +]) +def test_check_source_declines_symbolic_float_rounding_operations(source): + """Mixed int/decimal arithmetic, variable division, and within with a + floating target need IEEE-754 behavior that the Real encoder does not + model.""" + result = checker.check_source(source) + _assert_integer_numeric_support_declined(result) def test_check_source_untypeable_field_stays_encodable_false_no_raise(): @@ -1391,14 +1539,20 @@ def test_check_source_untypeable_field_stays_encodable_false_no_raise(): def test_check_source_starting_prefixed_forbid_is_checked(): """The regression test for the whole stage: before the fix, checked was 0, not 1 — the statement never reached check_agreement at all.""" - source = 'starting "2025-01-01" forbid amount is above 5000 because "policy"' + source = '\n'.join([ + "remember a number called amount with 6000", + 'starting "2025-01-01" forbid amount is above 5000 because "policy"', + ]) result = checker.check_source(source) assert result.encodable is True assert result.checked == 1 def test_check_source_until_prefixed_forbid_is_checked(): - source = 'until "2025-12-31" forbid amount is above 5000 because "policy"' + source = '\n'.join([ + "remember a number called amount with 6000", + 'until "2025-12-31" forbid amount is above 5000 because "policy"', + ]) result = checker.check_source(source) assert result.encodable is True assert result.checked == 1 @@ -1407,6 +1561,7 @@ def test_check_source_until_prefixed_forbid_is_checked(): def test_check_source_starting_until_prefixed_forbid_is_checked(): """Canonical order: starting before until, both before the verb.""" source = ( + "remember a number called amount with 6000\n" 'starting "2025-01-01" until "2025-12-31" ' 'forbid amount is above 5000 because "policy"' ) @@ -1419,7 +1574,10 @@ def test_check_source_inherited_prefixed_forbid_is_checked(): """The untested sibling: `inherited` is TokenType.OPERATOR, consumed statement-initial exactly like starting/until, and shared the same first-token-dispatch defect — never exercised by any corpus.""" - source = 'inherited forbid amount is above 5000 because "policy"' + source = '\n'.join([ + "remember a number called amount with 6000", + 'inherited forbid amount is above 5000 because "policy"', + ]) result = checker.check_source(source) assert result.encodable is True assert result.checked == 1 @@ -1428,6 +1586,7 @@ def test_check_source_inherited_prefixed_forbid_is_checked(): def test_check_source_full_canonical_prefix_stack_is_checked(): """starting ... until ... inherited ... — the full stack.""" source = ( + "remember a number called amount with 6000\n" 'starting "2025-01-01" until "2025-12-31" inherited ' 'forbid amount is above 5000 because "policy"' ) @@ -1441,6 +1600,7 @@ def test_check_source_temporally_prefixed_statement_reaches_findings(): list: a starting-prefixed forbid whose own unless swallows it must still produce unless_swallows_rule.""" source = ( + "remember a number called amount with 6000\n" 'starting "2025-01-01" forbid amount is above 5000 ' 'unless amount is above 0 because "policy"' ) @@ -1456,7 +1616,8 @@ def test_check_source_define_on_temporally_prefixed_line_registers_predicate(): next line misparses as a string-equality comparison against the bareword "large" instead of a PredicateApplicationNode.""" source = "\n".join([ - 'starting "2025-01-01" define large: is above 5000', + "remember a number called amount with 6000", + 'starting "2025-01-01" define large: is above 0 or is below 1000000', 'forbid amount is large because "policy"', ]) result = checker.check_source(source) diff --git a/tests/test_fuzzer.py b/tests/test_fuzzer.py index 1c79b7f..7d6ef0c 100644 --- a/tests/test_fuzzer.py +++ b/tests/test_fuzzer.py @@ -1,11 +1,12 @@ """Differential fuzzer for the Z3 encoder (src/liminate/checker.py). Decidability Step 2.5 (Trust Infrastructure Addendum v1.0r §88.6) — a -property-based fuzzer that verifies the encoder produces formulas -semantically equivalent to what the interpreter computes at runtime. -Generates random condition ASTs paired with random concrete fact -bindings, evaluates each through both paths via `_oracle`, and asserts -they agree. +property-based fuzzer for the checker's supported symbolic-integer +fragment. It generates random condition ASTs paired with concrete facts, +evaluates each through both paths via `_oracle`, and asserts they agree. +A deterministic numeric corpus separately exercises decimal arithmetic +and rounding boundaries, requiring either a match or an explicit checker +refusal. Read-only against checker.py / interpreter.py / analyzer.py — this file is purely additive. See checker.py's module docstring for the encoder's @@ -18,6 +19,7 @@ from collections import Counter from dataclasses import dataclass, field as dc_field from datetime import date, timedelta +from math import isfinite import pytest @@ -83,7 +85,7 @@ def _pin_constants(enc, symbol_table): if entry.type == "number": const = enc.constants.get(name) if const is not None: - pins.append(const == z3.RealVal(entry.value)) + pins.append(const == _z3_numeric_value(entry.value)) elif entry.type == "string": const = enc.constants.get(name) if const is not None: @@ -99,7 +101,7 @@ def _pin_constants(enc, symbol_table): continue field_type = (entry.schema or {}).get(field_name) if field_type == "number": - pins.append(const == z3.RealVal(field_value)) + pins.append(const == _z3_numeric_value(field_value)) elif field_type == "string": pins.append(const == z3.StringVal(field_value)) elif field_type == "date": @@ -107,7 +109,23 @@ def _pin_constants(enc, symbol_table): return pins -def _oracle(condition_ast, symbol_table): +def _z3_numeric_value(value): + """Encode the concrete runtime number exactly for oracle pins. + + Python floats represent binary fractions. Passing a float directly to + RealVal converts its shortest decimal spelling, which is not the exact + runtime value and can hide the very rounding differences this oracle + needs to find. + """ + if type(value) is int: + return z3.IntVal(value) + if isinstance(value, float) and isfinite(value): + numerator, denominator = value.as_integer_ratio() + return z3.RealVal(f"{numerator}/{denominator}") + raise ValueError(f"unsupported numeric pin {value!r}") + + +def _oracle(condition_ast, symbol_table, *, record_skip=True): """Compare the interpreter's verdict on `condition_ast` against the encoder's, both evaluated over the concrete values in `symbol_table`. @@ -119,28 +137,37 @@ def _oracle(condition_ast, symbol_table): try: interp_result = _eval_condition(condition_ast, None, symbol_table) except _InterpRuntimeError: - skip_counts["interp_runtime_error"] += 1 + if record_skip: + skip_counts["interp_runtime_error"] += 1 return SKIPPED, "interp_runtime_error" except TypeError: - skip_counts["interp_type_error"] += 1 + if record_skip: + skip_counts["interp_type_error"] += 1 return SKIPPED, "interp_type_error" enc = _Encoder(z3, symbol_table, {}) try: formula = enc.encode_condition(condition_ast) - except (UnencodableConstruct, NonlinearArithmetic): - skip_counts["encoder_unencodable"] += 1 - return SKIPPED, "encoder_unencodable" - except z3.Z3Exception: - skip_counts["encoder_z3_exception"] += 1 - return SKIPPED, "encoder_z3_exception" + except (UnencodableConstruct, NonlinearArithmetic) as exc: + if record_skip: + skip_counts["encoder_unencodable"] += 1 + return SKIPPED, f"encoder_unencodable: {exc}" + except z3.Z3Exception as exc: + if record_skip: + skip_counts["encoder_z3_exception"] += 1 + return SKIPPED, f"encoder_z3_exception: {exc}" solver = z3.Solver() solver.add(formula if interp_result else z3.Not(formula)) for pin in _pin_constants(enc, symbol_table): solver.add(pin) - agrees = solver.check() == z3.sat + outcome = solver.check() + if outcome == z3.unknown: + if record_skip: + skip_counts["z3_unknown"] += 1 + return SKIPPED, f"z3_unknown: {solver.reason_unknown()}" + agrees = outcome == z3.sat return interp_result, agrees @@ -263,20 +290,11 @@ def _names_for_kind(schema: FactSchema, kind: str) -> list: def _number_strategy(): - # Rounded to 2dp (currency-like), not raw doubles: hypothesis's float - # strategy otherwise happily generates values like 1.6e-256, and - # `x - 1.6e-256 == x` is True under IEEE-754 double rounding but False - # under Z3 Real's exact rational arithmetic — a genuine representation - # gap between the two arithmetic models, not a bug in either side, and - # not a shape any real Liminate program's literals take. Confirmed via - # a 2000-example probe before this fix; zero disagreements after it. - return st.one_of( - st.integers(min_value=-1000, max_value=1000), - st.floats( - min_value=-1000.0, max_value=1000.0, - allow_nan=False, allow_infinity=False, - ).map(lambda x: round(x, 2)), - ) + # The symbolic checker subset uses integer-valued numeric facts. Decimal + # literals and float arithmetic are exercised by the deterministic + # differential corpus below, where each case is either matched or + # explicitly classified as unsupported. + return st.integers(min_value=-1000, max_value=1000) def _date_strategy(): @@ -599,7 +617,11 @@ def _deontic_oracle(node, symbol_table): effect_solver.add(effect_formula if fires else z3.Not(effect_formula)) for pin in pins: effect_solver.add(pin) - effect_agrees = effect_solver.check() == z3.sat + effect_outcome = effect_solver.check() + if effect_outcome == z3.unknown: + skip_counts["z3_unknown"] += 1 + return SKIPPED, f"z3_unknown: {effect_solver.reason_unknown()}" + effect_agrees = effect_outcome == z3.sat allowed_agrees = True if allowed_formula is not None: @@ -607,7 +629,11 @@ def _deontic_oracle(node, symbol_table): allowed_solver.add(allowed_formula if allowed else z3.Not(allowed_formula)) for pin in pins: allowed_solver.add(pin) - allowed_agrees = allowed_solver.check() == z3.sat + allowed_outcome = allowed_solver.check() + if allowed_outcome == z3.unknown: + skip_counts["z3_unknown"] += 1 + return SKIPPED, f"z3_unknown: {allowed_solver.reason_unknown()}" + allowed_agrees = allowed_outcome == z3.sat return (fires, allowed), (effect_agrees and allowed_agrees) @@ -658,6 +684,115 @@ def test_predicate_round_trip(data): # --------------------------------------------------------------------------- +def test_numeric_differential_corpus_records_mismatches_and_unsupported(): + """Exercise source-shaped decimal arithmetic and keep mismatches + distinct from checker refusals. A mismatch is accumulated and asserted + with both verdicts; it is never sent through Hypothesis assume().""" + def arithmetic(left, op, right): + return ArithmeticNode(left=left, right=right, op=op) + + cases = [ + # Python evaluates each of these to a specific binary64 result. + ("decimal addition", 0.30000000000000004, "equal_to", + arithmetic(NumberLiteral(0.1), "plus", NumberLiteral(0.2)), True, "unsupported"), + ("decimal subtraction", 0.19999999999999998, "equal_to", + arithmetic(NumberLiteral(0.3), "minus", NumberLiteral(0.1)), True, "unsupported"), + ("decimal multiplication", 0.020000000000000004, "equal_to", + arithmetic(NumberLiteral(0.1), "multiplied_by", NumberLiteral(0.2)), True, "unsupported"), + ("nonterminating division", 0.3333333333333333, "equal_to", + arithmetic(NumberLiteral(1), "divided_by", NumberLiteral(3)), True, "unsupported"), + ("decimal inequality", 0.3, "not_equal_to", + arithmetic(NumberLiteral(0.1), "plus", NumberLiteral(0.2)), True, "unsupported"), + ("decimal ordered comparison", 0.3, "below", + arithmetic(NumberLiteral(0.1), "plus", NumberLiteral(0.2)), True, "unsupported"), + # Integer facts retain exact reasoning, including direct comparison + # with decimal thresholds and constant-only floating arithmetic. + ("integer equality", 3, "equal_to", + arithmetic(NumberLiteral(1), "plus", NumberLiteral(2)), True, "match"), + ("decimal threshold", 1, "above", NumberLiteral(0.1), True, "match"), + ("decimal sum threshold", 1, "above", + arithmetic(NumberLiteral(0.1), "plus", NumberLiteral(0.2)), True, "match"), + ("rounding midpoint", 1, "equal_to", + arithmetic(NumberLiteral(1), "plus", NumberLiteral(1.1102230246251565e-16)), True, "match"), + ("above rounding midpoint", 1, "below", + arithmetic(NumberLiteral(1), "plus", NumberLiteral(1.1102230246251567e-16)), True, "match"), + # Python compares large ints to floats without first rounding the + # integer to binary64. The checker must retain that boundary too. + ("integer float precision boundary", 9007199254740993, "equal_to", + NumberLiteral(9007199254740992.0), False, "match"), + ("division threshold", 1, "above", + arithmetic(NumberLiteral(1), "divided_by", NumberLiteral(3)), True, "match"), + # Operations that can round a symbolic runtime number are declined. + ("mixed int decimal arithmetic", 1, "equal_to", + arithmetic(NameRef("amount"), "plus", NumberLiteral(0.1)), False, "unsupported"), + ("symbolic division", 1, "above", + arithmetic(NameRef("amount"), "divided_by", NumberLiteral(3)), True, "unsupported"), + ("within with float target", 1, "within", + None, True, "unsupported"), + ] + observations = [] + mismatches = [] + unexpected_statuses = [] + + for name, amount, op, rhs, expected_interpreter, expected_status in cases: + symbol_table = _entries(amount=amount) + if op == "within": + condition = ConditionNode( + field=NameRef("amount"), op=op, + value=NumberLiteral(0.1), value2=NumberLiteral(0.9), + ) + else: + condition = ConditionNode( + field=NameRef("amount"), op=op, value=rhs, + ) + interpreter_result = _eval_condition(condition, None, symbol_table) + oracle_result, checker_agrees = _oracle( + condition, symbol_table, record_skip=False, + ) + + if oracle_result is SKIPPED: + status = "unsupported" + observations.append({ + "case": name, "status": status, + "interpreter": interpreter_result, "reason": checker_agrees, + }) + elif checker_agrees: + status = "match" + observations.append({ + "case": name, "status": status, + "interpreter": interpreter_result, + "checker": interpreter_result, + }) + else: + status = "mismatch" + checker_result = not interpreter_result + observations.append({ + "case": name, "status": status, + "interpreter": interpreter_result, + "checker": checker_result, + }) + mismatches.append(observations[-1]) + + if interpreter_result is not expected_interpreter: + unexpected_statuses.append({ + "case": name, + "expected_interpreter": expected_interpreter, + "actual_interpreter": interpreter_result, + }) + if status != expected_status: + unexpected_statuses.append({ + "case": name, + "expected_checker_status": expected_status, + "actual_checker_status": status, + }) + + assert not mismatches, f"Actual numerical mismatches: {mismatches!r}" + assert not unexpected_statuses, ( + f"Unexpected numerical classifications: {unexpected_statuses!r}; " + f"all observations: {observations!r}" + ) + + def test_within_operand_order(): """value=tolerance, value2=target — pins the operand order verified during the Step 2 design (§3 correction 1)."""