Differential fuzzer for Z3 encoder (decidability Step 2.5)

[rmichaelthomas]

Summary

Property-based differential fuzzer (Trust Infrastructure Addendum v1.0r §88.6) verifying that the Z3 encoder (checker.py, PR #63) produces formulas semantically equivalent to what the interpreter (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.

• Additive only — tests/test_fuzzer.py is new; pyproject.toml gains hypothesis in the dev extra + a fuzzer pytest marker; .gitignore gains .hypothesis/.
• checker.py, interpreter.py, and analyzer.py are byte-identical to main (verified via git diff).
• Vocabulary unchanged at 61 words.

Results

• Suite: 1763 → 1775 passed (net +12), 0 failed, 0 skipped, 0 regressions.
• Standard mode (500 examples/test): 0 disagreements across all 3 property tests.
• Heavy mode (LIMINATE_FUZZ_HEAVY=1, 5000 examples/test): 0 disagreements across all 3 property tests.
• Oracle-level skip rate: ~0.08% (12 of ~15,000 oracle calls in heavy mode — 11 interp_runtime_error, 1 interp_type_error, 0 encoder-side skips). Hypothesis's own "invalid examples" statistic (~13-17%) is a separate, internal choice-budget overrun on the recursive condition strategy, confirmed via debug-verbosity run — not oracle skips.
• 6 deterministic tests + 3 hypothesis-driven property tests, all passing (12 total new tests).

Findings along the way

Two generator-side fixes (not encoder/interpreter changes):

1. interpreter._eval_value has no NameRef branch in condition value position (only BareWord) — the original spec assumed otherwise; generator now uses BareWord only there.
2. Raw-double float generation could produce IEEE-754-vs-exact-rational precision mismatches at epsilon scale (e.g. x - 1.6e-256 == x); floats are now rounded to 2dp (currency-like), matching realistic literal shapes.

Both are documented inline in the test file.

Test plan

• python -m pytest -q — 1775 passed
• python -m pytest tests/test_fuzzer.py -v --tb=short — 12 passed
• LIMINATE_FUZZ_HEAVY=1 python -m pytest tests/test_fuzzer.py -v --hypothesis-show-statistics — 0 disagreements at 5000 examples/test
• git diff main -- src/liminate/checker.py src/liminate/interpreter.py src/liminate/analyzer.py — empty
• Vocabulary count confirmed 61

🤖 Generated with Claude Code