From 9a3fed66042fdd8a302dd1f5cb9d2b2a637a6318 Mon Sep 17 00:00:00 2001 From: rmichaelthomas Date: Mon, 20 Jul 2026 12:43:29 -0700 Subject: [PATCH] Add differential fuzzer for the Z3 encoder (decidability Step 2.5) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Property-based fuzzer (hypothesis) verifying checker.py's encoder produces formulas semantically equivalent to what interpreter.py computes at runtime. Generates random condition ASTs and deontic statements paired with concrete fact bindings, evaluates both paths via a round-trip oracle, and asserts agreement. - Oracle catches the full exception surface on both sides ((_RuntimeError, TypeError) interpreter-side; (UnencodableConstruct, NonlinearArithmetic, z3.Z3Exception) encoder-side) as skips, never as failures. - Generators respect operator-type compatibility to keep the skip rate low (~0.1% oracle-level skips; hypothesis's own internal choice-budget overrun on the recursive condition strategy accounts for the rest of its "invalid examples" statistic). - Zero disagreements found in standard (500 examples) or heavy (LIMINATE_FUZZ_HEAVY=1, 5000 examples) mode across all three property tests. - Along the way: found interpreter._eval_value has no NameRef branch in condition value position (BareWord only) and that raw-double float generation could manufacture IEEE-754-vs-exact-rational precision mismatches at epsilon scale — both fixed in the generator rather than the frozen encoder/interpreter. checker.py, interpreter.py, and analyzer.py are untouched. Vocabulary unchanged at 61 words. Suite: 1763 -> 1775 (net +12), zero regressions. Co-Authored-By: Claude Sonnet 5 --- .gitignore | 1 + pyproject.toml | 5 +- tests/test_fuzzer.py | 756 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 761 insertions(+), 1 deletion(-) create mode 100644 tests/test_fuzzer.py diff --git a/.gitignore b/.gitignore index 28ca6ef..59dece8 100644 --- a/.gitignore +++ b/.gitignore @@ -2,6 +2,7 @@ __pycache__/ *.py[cod] *.egg-info/ .pytest_cache/ +.hypothesis/ venv/ .venv/ diff --git a/pyproject.toml b/pyproject.toml index b54c09b..82a3f91 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -23,9 +23,12 @@ Repository = "https://github.com/rmichaelthomas/liminate" liminate = "liminate.cli:main" [project.optional-dependencies] -dev = ["pytest>=7.0"] +dev = ["pytest>=7.0", "hypothesis>=6.0"] build = ["pyinstaller>=6.0"] check = ["z3-solver>=4.12"] [tool.pytest.ini_options] testpaths = ["tests"] +markers = [ + "fuzzer: property-based differential fuzzer tests (may be slow)", +] diff --git a/tests/test_fuzzer.py b/tests/test_fuzzer.py new file mode 100644 index 0000000..1c79b7f --- /dev/null +++ b/tests/test_fuzzer.py @@ -0,0 +1,756 @@ +"""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. + +Read-only against checker.py / interpreter.py / analyzer.py — this file +is purely additive. See checker.py's module docstring for the encoder's +design notes; this file exercises it rather than modifying it. +""" + +from __future__ import annotations + +import os +from collections import Counter +from dataclasses import dataclass, field as dc_field +from datetime import date, timedelta + +import pytest + +z3 = pytest.importorskip("z3") + +from hypothesis import assume, given, settings, strategies as st + +from liminate.analyzer import SymbolEntry +from liminate.checker import _Encoder, NonlinearArithmetic, UnencodableConstruct +from liminate.interpreter import _RuntimeError as _InterpRuntimeError +from liminate.interpreter import _eval_condition +from liminate.parser import ( + ArithmeticNode, + BareWord, + CompoundConditionNode, + ConditionNode, + DateLiteral, + DefineNode, + EachPronoun, + ExpectNode, + FieldAccessNode, + ForbidNode, + NameRef, + NumberLiteral, + PermitNode, + PredicateApplicationNode, + QuotedString, + RequireNode, +) +from liminate.renderer import render + +pytestmark = pytest.mark.fuzzer + +_HEAVY = os.environ.get("LIMINATE_FUZZ_HEAVY", "") +_MAX_EXAMPLES = 5000 if _HEAVY else 500 + + +# --------------------------------------------------------------------------- +# Phase 2 — the round-trip oracle +# --------------------------------------------------------------------------- + +# Sentinel distinguishing "the interpreter/encoder declined this input" from +# a real (bool, bool) result. `_oracle` returns a value (not an exception) on +# skip so it stays usable from both plain deterministic tests and hypothesis +# property tests — the property test is the one place that turns a skip into +# `assume(False)`, since `hypothesis.assume`/`event` raise InvalidArgument +# when called outside an active `@given` run, and Phase 2's own acceptance +# check (a hand-crafted skip case) is a plain test, not a `@given` one. +SKIPPED = object() + +# Skip-cause counters (§10 manual-gate reporting): incremented on every +# skip so the breakdown by cause can be read back after a run. +skip_counts: Counter = Counter() + + +def _pin_constants(enc, symbol_table): + """Equality constraints pinning every allocated Z3 constant to its + concrete value from `symbol_table` (§4 sort-matching table). List-type + entries need no pin — membership is expanded from the literal values + already captured in `enc.lists` at encode time.""" + pins = [] + for name, entry in symbol_table.items(): + if entry.type == "number": + const = enc.constants.get(name) + if const is not None: + pins.append(const == z3.RealVal(entry.value)) + elif entry.type == "string": + const = enc.constants.get(name) + if const is not None: + pins.append(const == z3.StringVal(entry.value)) + elif entry.type == "date": + const = enc.constants.get(name) + if const is not None: + pins.append(const == z3.IntVal(entry.value.toordinal())) + elif entry.type == "record": + for field_name, field_value in entry.value.items(): + const = enc.constants.get(f"{name}__{field_name}") + if const is None: + continue + field_type = (entry.schema or {}).get(field_name) + if field_type == "number": + pins.append(const == z3.RealVal(field_value)) + elif field_type == "string": + pins.append(const == z3.StringVal(field_value)) + elif field_type == "date": + pins.append(const == z3.IntVal(field_value.toordinal())) + return pins + + +def _oracle(condition_ast, symbol_table): + """Compare the interpreter's verdict on `condition_ast` against the + encoder's, both evaluated over the concrete values in `symbol_table`. + + Returns `(interp_result, encoder_agrees)` — both real bools — when + both sides accept the input. Returns `(SKIPPED, reason)` when either + side declines: the interpreter rejecting or the encoder refusing to + encode is not an encoder disagreement (§8 invariants 6/7). + """ + try: + interp_result = _eval_condition(condition_ast, None, symbol_table) + except _InterpRuntimeError: + skip_counts["interp_runtime_error"] += 1 + return SKIPPED, "interp_runtime_error" + except TypeError: + 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" + + 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 + return interp_result, agrees + + +def _entries(**by_name): + """Build a symbol table from name=value pairs, inferring the + SymbolEntry.type the same way the interpreter's own `_store` would + for these scalar shapes.""" + symtab = {} + for name, value in by_name.items(): + if isinstance(value, bool): + raise ValueError("bool facts aren't part of v1's value model") + if isinstance(value, (int, float)): + symtab[name] = SymbolEntry(name=name, value=value, type="number") + elif isinstance(value, str): + symtab[name] = SymbolEntry(name=name, value=value, type="string") + elif isinstance(value, date): + symtab[name] = SymbolEntry(name=name, value=value, type="date") + elif isinstance(value, list): + symtab[name] = SymbolEntry(name=name, value=value, type="list_of_strings") + else: + raise ValueError(f"unhandled fact value {value!r}") + return symtab + + +def test_oracle_equality_agrees(): + symtab = _entries(amount=10) + cond = ConditionNode(field=NameRef("amount"), op="is", value=NumberLiteral(10)) + interp_result, agrees = _oracle(cond, symtab) + assert interp_result is True + assert agrees + + +def test_oracle_ordered_comparison_agrees(): + symtab = _entries(amount=10) + cond = ConditionNode(field=NameRef("amount"), op="above", value=NumberLiteral(5)) + interp_result, agrees = _oracle(cond, symtab) + assert interp_result is True + assert agrees + + +def test_oracle_within_agrees(): + symtab = _entries(amount=100) + cond = ConditionNode( + field=NameRef("amount"), op="within", + value=NumberLiteral(5), value2=NumberLiteral(106), + ) + interp_result, agrees = _oracle(cond, symtab) + assert interp_result is False # |100-106|=6 > 5 + assert agrees + + +def test_oracle_includes_agrees(): + symtab = _entries(tags=["red", "green"]) + cond = ConditionNode( + field=NameRef("tags"), op="includes", value=QuotedString("green"), + ) + interp_result, agrees = _oracle(cond, symtab) + assert interp_result is True + assert agrees + + +def test_oracle_compound_and_or_agrees(): + symtab = _entries(amount=10, status="open") + left = ConditionNode(field=NameRef("amount"), op="above", value=NumberLiteral(5)) + right = ConditionNode(field=NameRef("status"), op="is", value=QuotedString("open")) + and_cond = CompoundConditionNode(left=left, right=right, connector="and") + or_cond = CompoundConditionNode( + left=left, + right=ConditionNode(field=NameRef("status"), op="is", value=QuotedString("closed")), + connector="or", + ) + interp_and, agrees_and = _oracle(and_cond, symtab) + interp_or, agrees_or = _oracle(or_cond, symtab) + assert interp_and is True and agrees_and + assert interp_or is True and agrees_or + + +def test_oracle_skips_on_string_above_number(): + symtab = _entries(status="open") + cond = ConditionNode(field=NameRef("status"), op="above", value=NumberLiteral(50)) + interp_result, reason = _oracle(cond, symtab) + assert interp_result is SKIPPED + assert reason == "interp_type_error" + + +# --------------------------------------------------------------------------- +# Phase 3 — hypothesis strategies +# --------------------------------------------------------------------------- + +_STRING_ALPHABET = [ + "alpha", "beta", "gamma", "west", "east", "sre", "oncall", "admin", +] +_DATE_CENTER = date(2025, 7, 1) + + +@dataclass +class FactSchema: + """A random symbol table (§5) plus the name pools the condition + generator needs to respect operator-type compatibility.""" + symtab: dict + numeric_names: list + string_names: list + date_names: list + list_name: object # str | None + record_name: object # str | None + record_fields: dict # field_name -> "number" | "string" | "date" + _predicate_seq: list = dc_field(default_factory=lambda: [0]) + + def next_predicate_name(self) -> str: + self._predicate_seq[0] += 1 + return f"__pred_{self._predicate_seq[0]}" + + +def _names_for_kind(schema: FactSchema, kind: str) -> list: + return { + "number": schema.numeric_names, + "string": schema.string_names, + "date": schema.date_names, + }[kind] + + +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)), + ) + + +def _date_strategy(): + return st.dates( + min_value=_DATE_CENTER - timedelta(days=182), + max_value=_DATE_CENTER + timedelta(days=182), + ) + + +@st.composite +def fact_schema(draw): + """§5 — 2-6 scalar facts, an optional string list, an optional + record. At least one scalar is always present, so every schema has + at least one usable field for equality-family operators.""" + symtab: dict = {} + numeric_names: list = [] + string_names: list = [] + date_names: list = [] + + n_scalars = draw(st.integers(min_value=2, max_value=6)) + for i in range(n_scalars): + kind = draw(st.sampled_from(["number", "string", "date"])) + if kind == "number": + name = f"number_{i}" + symtab[name] = SymbolEntry( + name=name, value=draw(_number_strategy()), type="number", + ) + numeric_names.append(name) + elif kind == "string": + name = f"string_{i}" + symtab[name] = SymbolEntry( + name=name, value=draw(st.sampled_from(_STRING_ALPHABET)), + type="string", + ) + string_names.append(name) + else: + name = f"date_{i}" + symtab[name] = SymbolEntry( + name=name, value=draw(_date_strategy()), type="date", + ) + date_names.append(name) + + list_name = None + if draw(st.booleans()): + list_name = "tags" + items = draw( + st.lists(st.sampled_from(_STRING_ALPHABET), min_size=0, max_size=5) + ) + symtab[list_name] = SymbolEntry( + name=list_name, value=items, type="list_of_strings", + ) + + record_name = None + record_fields: dict = {} + if draw(st.booleans()): + record_name = "rec" + n_fields = draw(st.integers(min_value=1, max_value=3)) + fields: dict = {} + schema_types: dict = {} + for i in range(n_fields): + fkind = draw(st.sampled_from(["number", "string", "date"])) + fname = f"f{i}" + if fkind == "number": + fields[fname] = draw(_number_strategy()) + elif fkind == "string": + fields[fname] = draw(st.sampled_from(_STRING_ALPHABET)) + else: + fields[fname] = draw(_date_strategy()) + schema_types[fname] = fkind + symtab[record_name] = SymbolEntry( + name=record_name, value=fields, type="record", schema=schema_types, + ) + record_fields = schema_types + + return FactSchema( + symtab=symtab, + numeric_names=numeric_names, + string_names=string_names, + date_names=date_names, + list_name=list_name, + record_name=record_name, + record_fields=record_fields, + ) + + +@st.composite +def _arithmetic_value(draw, schema: FactSchema): + """Linear-only arithmetic (TI-Q13 closure): multiplied_by/divided_by + always keep at least one compile-time-constant (NumberLiteral) + operand, and divided_by never uses a literal-zero divisor (failure + mode #7).""" + op = draw(st.sampled_from(["plus", "minus", "multiplied_by", "divided_by"])) + + def _operand(): + if schema.numeric_names and draw(st.booleans()): + name = draw(st.sampled_from(schema.numeric_names)) + return draw(st.sampled_from([NameRef(name), BareWord(name)])) + return NumberLiteral(draw(_number_strategy())) + + if op in ("multiplied_by", "divided_by"): + literal_value = draw(_number_strategy()) + if op == "divided_by" and literal_value == 0: + literal_value = 1 + literal_on_left = draw(st.booleans()) + other = _operand() + left, right = ( + (NumberLiteral(literal_value), other) if literal_on_left + else (other, NumberLiteral(literal_value)) + ) + else: + left, right = _operand(), _operand() + return ArithmeticNode(left=left, right=right, op=op) + + +@st.composite +def _typed_value(draw, schema: FactSchema, kind: str): + """A value AST matching `kind`'s type — a literal, a name reference + (NameRef or BareWord, per failure mode #6 both encode identically), + a record FieldAccessNode when available, or (numeric only) linear + arithmetic.""" + names = _names_for_kind(schema, kind) + r = draw(st.integers(min_value=0, max_value=99)) + + if kind == "number" and r < 15: + return draw(_arithmetic_value(schema)) + + record_fields_of_kind = [ + f for f, t in schema.record_fields.items() if t == kind + ] + if 15 <= r < 30 and record_fields_of_kind: + fname = draw(st.sampled_from(record_fields_of_kind)) + return FieldAccessNode(field=fname, record_name=schema.record_name) + + if 30 <= r < 65 and names: + # BareWord only: interpreter._eval_value has no NameRef branch (it + # only resolves BareWord in value position — verified against + # main@2c628e1). A bare NameRef here raises _RuntimeError + # ("Unexpected value NameRef."), which is a pure skip-budget waste, + # not useful coverage — arithmetic operands are a different code + # path (_evaluate_expression) and do support NameRef; see + # `_arithmetic_value` above. + return BareWord(draw(st.sampled_from(names))) + + if kind == "number": + return NumberLiteral(draw(_number_strategy())) + if kind == "string": + return QuotedString(draw(st.sampled_from(_STRING_ALPHABET))) + return DateLiteral(draw(_date_strategy())) + + +@st.composite +def _predicate_application(draw, schema: FactSchema): + """§5 — a `define`-backed predicate applied to a subject whose type + matches the body's implicit (EachPronoun) parameter type.""" + pools = [k for k in ("number", "string", "date") if _names_for_kind(schema, k)] + if not pools: + return draw(_condition_leaf(schema)) + + kind = draw(st.sampled_from(pools)) + op_pool = ( + ["is", "equal_to", "not_equal_to"] if kind == "string" + else ["above", "below", "not_above", "not_below", "is", "equal_to", "not_equal_to"] + ) + op = draw(st.sampled_from(op_pool)) + value = draw(_typed_value(schema, kind)) + body = ConditionNode(field=EachPronoun(), op=op, value=value) + + pred_name = schema.next_predicate_name() + schema.symtab[pred_name] = SymbolEntry( + name=pred_name, value=body, type="predicate", + ) + + subject_name = draw(st.sampled_from(_names_for_kind(schema, kind))) + negated = draw(st.booleans()) + return PredicateApplicationNode( + subject=NameRef(subject_name), predicate_name=pred_name, negated=negated, + ) + + +@st.composite +def _condition_leaf(draw, schema: FactSchema): + """A single ConditionNode, respecting operator-type compatibility + (§5) so the interpreter/encoder skip rate stays low.""" + op_pool = [] + if schema.numeric_names or schema.date_names: + op_pool += ["above", "below", "not_above", "not_below", "within"] + if schema.list_name is not None: + op_pool += ["includes", "not_includes"] + op_pool += ["is", "equal_to", "not_equal_to"] + + op = draw(st.sampled_from(op_pool)) + + if op in ("includes", "not_includes"): + value = QuotedString(draw(st.sampled_from(_STRING_ALPHABET))) + return ConditionNode(field=NameRef(schema.list_name), op=op, value=value) + + if op in ("above", "below", "not_above", "not_below", "within"): + ordered_kinds = [ + k for k in ("number", "date") if _names_for_kind(schema, k) + ] + kind = draw(st.sampled_from(ordered_kinds)) + field_name = draw(st.sampled_from(_names_for_kind(schema, kind))) + field = NameRef(field_name) + if op == "within": + # Tolerance is always numeric, even for a date field (day count) — + # _within_tolerance requires it regardless of field kind. + tolerance = draw(_typed_value(schema, "number")) + target = draw(_typed_value(schema, kind)) + return ConditionNode(field=field, op=op, value=tolerance, value2=target) + value = draw(_typed_value(schema, kind)) + return ConditionNode(field=field, op=op, value=value) + + # Equality family: any scalar type, including a record field. + pools = [k for k in ("number", "string", "date") if _names_for_kind(schema, k)] + if schema.record_name is not None: + pools.append("record") + kind = draw(st.sampled_from(pools)) + if kind == "record": + field_name = draw(st.sampled_from(list(schema.record_fields))) + field = FieldAccessNode(field=field_name, record_name=schema.record_name) + value = draw(_typed_value(schema, schema.record_fields[field_name])) + else: + field_name = draw(st.sampled_from(_names_for_kind(schema, kind))) + field = NameRef(field_name) + value = draw(_typed_value(schema, kind)) + return ConditionNode(field=field, op=op, value=value) + + +@st.composite +def _leaf(draw, schema: FactSchema): + r = draw(st.integers(min_value=0, max_value=99)) + if r < 15: + return draw(_predicate_application(schema)) + return draw(_condition_leaf(schema)) + + +@st.composite +def condition_ast(draw, schema: FactSchema, depth: int = 0): + """§5 — recursive condition AST, depth-capped at 3, referencing only + facts present in `schema`.""" + if depth < 3 and draw(st.booleans()): + connector = draw(st.sampled_from(["and", "or"])) + left = draw(condition_ast(schema, depth=depth + 1)) + right = draw(condition_ast(schema, depth=depth + 1)) + return CompoundConditionNode(left=left, right=right, connector=connector) + return draw(_leaf(schema)) + + +@st.composite +def deontic_statement(draw, schema: FactSchema): + """§5 — a Require/Forbid/Permit/Expect wrapping a generated + condition, with a 50% chance of an independently generated `unless` + exception.""" + node_cls = draw(st.sampled_from([RequireNode, ForbidNode, PermitNode, ExpectNode])) + condition = draw(condition_ast(schema)) + exception = draw(condition_ast(schema)) if draw(st.booleans()) else None + return node_cls(condition=condition, exception=exception) + + +# --------------------------------------------------------------------------- +# Phase 4 — the deontic-statement oracle (verb-level encoding) +# --------------------------------------------------------------------------- + +def _deontic_fires(node, condition_result: bool, exception_result: bool) -> bool: + """Mirrors _exec_require/_exec_forbid/_exec_permit/_exec_expect's + fire condition exactly (verified against interpreter.py at + main@2c628e1) — require/expect fire on ¬condition ∧ ¬exception, + forbid/permit fire on condition ∧ ¬exception.""" + if isinstance(node, (RequireNode, ExpectNode)): + return (not condition_result) and (not exception_result) + if isinstance(node, (ForbidNode, PermitNode)): + return condition_result and (not exception_result) + raise TypeError(f"not a deontic node: {type(node).__name__}") + + +def _deontic_allowed(node, condition_result: bool, exception_result: bool): + """Mirrors checker.encode_deontic's `allowed` space — None for + permit/expect (DT-Q3: they never participate in the require/forbid + contradiction check).""" + if isinstance(node, RequireNode): + return condition_result or exception_result + if isinstance(node, ForbidNode): + return (not condition_result) or exception_result + return None + + +def _deontic_oracle(node, symbol_table): + """Verb-level counterpart to `_oracle`: compares the interpreter's + fire/allowed verdicts against the encoder's effect/allowed formulas. + Same skip semantics and exception surface as `_oracle`.""" + try: + condition_result = _eval_condition(node.condition, None, symbol_table) + exception_result = ( + _eval_condition(node.exception, None, symbol_table) + if node.exception is not None else False + ) + except _InterpRuntimeError: + skip_counts["interp_runtime_error"] += 1 + return SKIPPED, "interp_runtime_error" + except TypeError: + skip_counts["interp_type_error"] += 1 + return SKIPPED, "interp_type_error" + + fires = _deontic_fires(node, condition_result, exception_result) + allowed = _deontic_allowed(node, condition_result, exception_result) + + enc = _Encoder(z3, symbol_table, {}) + try: + effect_formula, allowed_formula = enc.encode_deontic(node) + 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" + + pins = _pin_constants(enc, symbol_table) + + effect_solver = z3.Solver() + 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 + + allowed_agrees = True + if allowed_formula is not None: + allowed_solver = z3.Solver() + 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 + + return (fires, allowed), (effect_agrees and allowed_agrees) + + +# --------------------------------------------------------------------------- +# Phase 4 — property tests +# --------------------------------------------------------------------------- + + +@given(data=st.data()) +@settings(max_examples=_MAX_EXAMPLES, deadline=None) +def test_condition_round_trip(data): + schema = data.draw(fact_schema()) + cond = data.draw(condition_ast(schema)) + interp_result, agrees = _oracle(cond, schema.symtab) + if interp_result is SKIPPED: + assume(False) + assert agrees, f"Encoder disagrees on {render(cond)}: interpreter={interp_result}" + + +@given(data=st.data()) +@settings(max_examples=_MAX_EXAMPLES, deadline=None) +def test_deontic_effect_round_trip(data): + schema = data.draw(fact_schema()) + stmt = data.draw(deontic_statement(schema)) + outcome, agrees = _deontic_oracle(stmt, schema.symtab) + if outcome is SKIPPED: + assume(False) + assert agrees, f"Encoder disagrees on {render(stmt)}: interpreter={outcome}" + + +@given(data=st.data()) +@settings(max_examples=_MAX_EXAMPLES, deadline=None) +def test_predicate_round_trip(data): + schema = data.draw(fact_schema()) + application = data.draw(_predicate_application(schema)) + interp_result, agrees = _oracle(application, schema.symtab) + if interp_result is SKIPPED: + assume(False) + assert agrees, ( + f"Encoder disagrees on predicate application {render(application)}: " + f"interpreter={interp_result}" + ) + + +# --------------------------------------------------------------------------- +# Phase 4 — regression anchors (deterministic) +# --------------------------------------------------------------------------- + + +def test_within_operand_order(): + """value=tolerance, value2=target — pins the operand order verified + during the Step 2 design (§3 correction 1).""" + for amount, tolerance, target, expected in [ + (100, 5, 103, True), # |100-103|=3 <= 5 + (100, 5, 106, False), # |100-106|=6 > 5 + (100, 0, 100, True), # |100-100|=0 <= 0 + (100, 0, 101, False), # |100-101|=1 > 0 + ]: + symtab = _entries(amount=amount) + cond = ConditionNode( + field=NameRef("amount"), op="within", + value=NumberLiteral(tolerance), value2=NumberLiteral(target), + ) + interp_result, agrees = _oracle(cond, symtab) + assert interp_result == expected + assert agrees + + +def test_includes_empty_list(): + symtab = {"tags": SymbolEntry(name="tags", value=[], type="list_of_strings")} + includes_cond = ConditionNode( + field=NameRef("tags"), op="includes", value=QuotedString("x"), + ) + not_includes_cond = ConditionNode( + field=NameRef("tags"), op="not_includes", value=QuotedString("x"), + ) + interp_result, agrees = _oracle(includes_cond, symtab) + assert interp_result is False + assert agrees + interp_result, agrees = _oracle(not_includes_cond, symtab) + assert interp_result is True + assert agrees + + +def test_KNOWN_interpreter_type_mismatch_surface(): + """Pins the exception-surface map from v1.0r §88.3's latent + _apply_op hole — reachable only by direct AST construction bypassing + the analyzer, exactly how this fuzzer builds conditions (verified + against interpreter.py at main@2c628e1). + + If this starts failing because a mismatch now raises _RuntimeError + instead of TypeError, that is an interpreter improvement: update + this test and narrow the oracle's catch, do not revert the + interpreter. + """ + string_symtab = _entries(status="open") + number_symtab = _entries(amount=10) + date_symtab = _entries(due=date(2026, 1, 1)) + + with pytest.raises(TypeError): + _eval_condition( + ConditionNode(field=NameRef("status"), op="above", value=NumberLiteral(50)), + None, string_symtab, + ) + with pytest.raises(TypeError): + _eval_condition( + ConditionNode(field=NameRef("amount"), op="above", value=QuotedString("x")), + None, number_symtab, + ) + with pytest.raises(_InterpRuntimeError): + _eval_condition( + ConditionNode(field=NameRef("due"), op="above", value=NumberLiteral(5)), + None, date_symtab, + ) + with pytest.raises(_InterpRuntimeError): + _eval_condition( + ConditionNode( + field=NameRef("status"), op="within", + value=NumberLiteral(5), value2=NumberLiteral(10), + ), + None, string_symtab, + ) + assert _eval_condition( + ConditionNode(field=NameRef("amount"), op="includes", value=QuotedString("x")), + None, number_symtab, + ) is False + assert _eval_condition( + ConditionNode(field=NameRef("status"), op="is", value=NumberLiteral(1)), + None, string_symtab, + ) is False + + +# --------------------------------------------------------------------------- +# Phase 5 — skip-rate reporting (manual-gate instrumentation) +# --------------------------------------------------------------------------- + + +@pytest.fixture(scope="module", autouse=True) +def _report_skip_counts(): + yield + if skip_counts: + total = sum(skip_counts.values()) + print(f"\n[fuzzer] {total} skipped examples by cause:") + for reason, count in skip_counts.most_common(): + print(f"[fuzzer] {reason}: {count}")