Skip to content

Add VulReasoner interval parity workflow#87

Draft
StarGazerM wants to merge 8 commits into
mainfrom
pyreason-parity
Draft

Add VulReasoner interval parity workflow#87
StarGazerM wants to merge 8 commits into
mainfrom
pyreason-parity

Conversation

@StarGazerM

@StarGazerM StarGazerM commented Jul 17, 2026

Copy link
Copy Markdown
Collaborator

Summary

  • add interval-valued functional relation semantics, including float32-bit bounds, rule-local max-lower witness selection, and cross-rule interval intersection
  • add the minimal VulReasoner PyReason oracle, GraphML ingestion, SRDatalog lowering, exact parity validation, and deterministic stress benchmarks
  • add an executed notebook explaining the semantic gap, why the callback is provenance-aware but not traditional semiring provenance, the two-rule lowering, exact default-input bytes, and bounded scaling results
  • split dependency management into a Python 3.12 SRDatalog development project and an independently locked, uv-managed Python 3.10.12 VulReasoner application

Why

VulReasoner's annotation callback does two context-dependent reductions: it selects one derivation witness within each source rule, then intersects the selected intervals contributed by different rules. Treating all duplicates uniformly either intersects losing witnesses or makes different rules compete. The new candidate relations and lattice maintenance preserve that semantic boundary through CUDA execution.

The PyReason oracle also requires a different interpreter and dependency stack from normal SRDatalog development. The nested project pins the validated PyReason Git revision and removes the previous dependency on a dirty sibling checkout.

Impact

The repository now has a reproducible end-to-end path from the supplied PyReason rules and GraphML input to exact SRDatalog results, plus executable documentation and larger shared workloads for correctness and performance analysis. Contributors can use the root lock for SRDatalog work while the notebook and parity harness use minimal_vulreasoner/uv.lock without changing the root environment.

Validation

  • uv run --frozen pytest -q tests/test_cuda_orchestrator_lattice.py tests/test_integration_vulreasoner_minimal_optional.py tests/test_lattice_value_semantics.py tests/test_vulreasoner_analyst_rule_loader.py tests/test_vulreasoner_graphml_ingest.py tests/test_vulreasoner_srdatalog_query.py tests/test_vulreasoner_stress_workload.py — 29 passed, 1 skipped
  • uv run --frozen --group jupyter-test pytest -q tests/test_viz_jupyter.py tests/test_viz_doop_jupyter.py — 10 passed
  • uv run --project minimal_vulreasoner --frozen python minimal_vulreasoner/validate_minimal_parity.py --no-compile --jobs 8 — complete temporal PyReason/SRDatalog parity passed
  • full live notebook execution under minimal_vulreasoner/.venv completed without cell errors; the PyReason scaling suite completed within its 120-second timeout
  • default GraphML PyReason/SRDatalog canonical result bytes match exactly with SHA-256 ae3d94e59f1417f1f7ab264f4bf5146e9e511a4b35c1a351bcc24cb4039d4b2d
  • shared stress-workload target digests match exactly through 12,288 transitions
  • uv run --frozen --no-default-groups --group docs sphinx-build -W --keep-going -b html docs docs/_build/html — passed
  • both uv lockfiles pass uv lock --check

StarGazerM and others added 8 commits June 10, 2026 10:44
Demonstrates that PyReason's minimal_example (delay-0, [1,1] bounds) is the
degenerate, fully-covered case of srdatalog's plain-Datalog semantics: runs
PyReason live and matches the program's least model {Mary, Justin, John}.
Surveys the real PyReason example files to show <-N delay changes the
fixpoint only under non-monotonicity (negation/closed-world); positive
programs are delay-invariant.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
# Conflicts:
#	src/srdatalog/ir/codegen/cuda/main_file.py
#	src/srdatalog/ir/hir/__init__.py
#	src/srdatalog/ir/mir/print.py
#	src/srdatalog/ir/mir/types.py
#	tests/fixtures/integration/doop.mir.sexpr
#	tests/fixtures/tc.mir.sexpr
#	tests/fixtures/tc_with_plan.mir.sexpr
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant