Add SRDatalog VulReasoner integration

README.md

@@ -9,6 +9,16 @@
 
 An explainable inference software supporting annotated, real valued, graph based and temporal logic.
 
+## SRDatalog VulReasoner integration
+
+This fork includes a reproducible
+[VulReasoner integration](minimal_vulreasoner/README.md) that runs this PyReason
+checkout as the semantic oracle and evaluates the same interval-valued rules
+with SRDatalog. It includes the original rules, annotation callback, default
+GraphML input, exact parity checker, bounded performance harnesses, and an
+executable notebook explaining the non-semiring provenance gap and two-stage
+aggregate lowering.
+
 ## Links
 [📃 Paper](https://arxiv.org/abs/2302.13482)
 

minimal_vulreasoner/.gitignore

@@ -0,0 +1 @@
+output/

minimal_vulreasoner/.python-version

@@ -0,0 +1 @@
+3.10.12

minimal_vulreasoner/README.md

@@ -0,0 +1,223 @@
+# PyReason to SRDatalog VulReasoner integration
+
+A self-contained application that exercises **only** the PyReason features
+VulReasoner depends on, implements the same reasoning in SRDatalog, and checks
+their exact temporal interval parity. This integration lives in the PyReason
+fork so PyReason remains the executable oracle while the accelerated backend is
+versioned independently.
+
+## Contents
+
+| File | Purpose |
+|------|---------|
+| `run_minimal_reasoner.py` | The example. Loads the KG, one ruleset, the annotation fn, facts, and runs the fixpoint. |
+| `run_srdatalog_reasoner.py` | Runs those same inputs through SRDatalog and prints every temporal `AnalystAt` result. |
+| `validate_minimal_parity.py` | Runs both engines and compares their complete temporal result maps. |
+| `graphml_ingest.py` | Streaming, PyReason-compatible GraphML-to-relation adapter. |
+| `analyst_rule_loader.py` | Parser for the constrained six-rule analyst CSV shape. |
+| `srdatalog_query.py` | The same six delayed analyst rules encoded in the SRDatalog DSL. |
+| `stress_workload.py` | Deterministic layered workloads shared by both engines. |
+| `benchmark_pyreason.py` | PyReason oracle and timing harness. |
+| `benchmark_srdatalog.py` | SRDatalog build, GPU timing, and result-digest harness. |
+| `graphml/CWE_121_MVP2.graphml` | VulReasoner's default knowledge graph with label-to-label ontology edges (`can_cause`, `contributes_to`, `manifestation_of`, …). |
+| `rules/analyst_rules.csv` | The six analyst rules whose heads call the annotation function. |
+| `annotation_fn.py` | VulReasoner's `paired_minimum_bounds_ann_fn` reference callback. |
+
+`output/` is created at runtime and holds the rule-trace CSVs (`pr.save_rule_trace`).
+
+## PyReason surface used
+
+`pr.reset` → `pr.load_graphml` → `pr.settings.{atom_trace, allow_ground_rules,
+save_graph_attributes_to_trace}` → `pr.add_annotation_function` →
+`pr.add_rule_from_csv` → `pr.add_closed_world_predicate` → `pr.add_fact` /
+`pr.Fact` (hasLabel, analystAt, stepFrom) → `pr.reason` → `pr.save_rule_trace`.
+
+That is the complete set VulReasoner's reasoning loop touches.
+
+## PyReason terms in database and provenance language
+
+PyReason uses `annotation` for several ideas that database systems normally
+name separately.  The mapping used by the SRDatalog port is:
+
+| PyReason term | Database/provenance term |
+|---|---|
+| satisfied or grounded rule body | join result; one derivation witness for the head |
+| `qualified_nodes` / `qualified_edges` | the supporting input tuples belonging to each witness |
+| body `annotations` | interval-valued payloads carried by those input tuples |
+| head annotation function | user-defined grouped aggregate over the witnesses for one rule and head key |
+| `paired_minimum_bounds_ann_fn` | rule-local `ARG MAX` by lower bound, carrying the winning witness's interval |
+| rule trace | explanation graph / why-provenance trace |
+| world | the current keyed relation state at one logical time, not a probabilistic-database possible world |
+| world update | duplicate-key interval-lattice merge into that state |
+| `<-1` | logical-time shift, represented in SRDatalog by a successor join |
+
+The callback is **provenance-aware** because it compares alternative
+derivation witnesses and returns the interval belonging to the selected
+witness.  It is not full semiring provenance: classical why-provenance retains
+all alternative supporting derivations, whereas the callback deliberately
+keeps one maximum-scoring witness.  The parity encoding retains its stable rank
+and interval, but does not currently materialize a complete provenance
+polynomial.
+
+The compiler-level denotation and the reason for the separate candidate
+relation are specified in SRDatalog's
+[`docs/ir_lowering_semantics.md`, Section 6.2](https://github.com/harp-lab/srdatalog-python/blob/a5ccfdae531c2f321f5746634eb97515def34b90/docs/ir_lowering_semantics.md#62-provenance-aware-witness-selection).
+
+## The example workflow
+
+Four code blocks chained so the analyst's `analystAt` "control" atom propagates
+one hop per timestep, from the first block to the `CWE_121` vulnerability class:
+
+```
+b1 (computed_write_length)
+   --contributes_to-->   b2 (incorrect_length_calculation)   [analyst-rule-2]
+   --can_cause-->        b3 (return_address_overwrite)        [analyst-rule-1]
+   --manifestation_of--> b4 (CWE_121)                         [analyst-rule-5]
+```
+
+## Run
+
+```bash
+uv sync --project minimal_vulreasoner --frozen
+PYTHONHASHSEED=0 uv run --project minimal_vulreasoner --frozen \
+  python minimal_vulreasoner/run_minimal_reasoner.py
+```
+
+The nested uv project pins Python 3.10.12, uses this checkout as its editable
+PyReason oracle, pins the validated SRDatalog Git revision, and locks every
+transitive dependency in `minimal_vulreasoner/uv.lock`. It is intentionally
+independent of any repository-wide development environment.
+
+Expected tail:
+
+```
+Converged at time: 4
+analystAt(b4) reached: True
+```
+
+`PYTHONHASHSEED=0` isn't required for this script, but VulReasoner pins it so its
+on-disk traces are byte-reproducible (ADR 0005).
+
+## Run the existing inputs on SRDatalog
+
+This command consumes the checked-in `CWE_121_MVP2.graphml`,
+`analyst_rules.csv`, and the workflow facts declared in `example_config.py`:
+
+```bash
+uv run --project minimal_vulreasoner --frozen \
+  python minimal_vulreasoner/run_srdatalog_reasoner.py \
+  --jobs "$(nproc)"
+```
+
+The runner streams GraphML edge attributes into ordinary relation columns,
+parses the six PyReason rules into the supported analyst-rule contract, compiles
+the DSL query, loads the relations, runs the GPU fixpoint, and prints one
+`RESULT_JSON=...` line. After the first build, reuse the cached shared library:
+
+```bash
+uv run --project minimal_vulreasoner --frozen \
+  python minimal_vulreasoner/run_srdatalog_reasoner.py \
+  --no-compile
+```
+
+The exact result is:
+
+```json
+{
+  "b1@0": [1.0, 1.0],
+  "b1@1": [1.0, 1.0],
+  "b2@2": [1.0, 1.0],
+  "b3@3": [1.0, 1.0],
+  "b4@4": [1.0, 1.0]
+}
+```
+
+For a fresh differential comparison against this PyReason checkout:
+
+```bash
+uv run --project minimal_vulreasoner --frozen \
+  python minimal_vulreasoner/validate_minimal_parity.py \
+  --no-compile
+```
+
+It compares every `(node,time) -> [lower,upper]` entry and exits nonzero on any
+difference. The validated input contains 188 graph nodes, 403 graph edges, and
+138 edge-attribute facts selected by the six analyst rules. On an RTX 6000 Ada,
+streaming ingestion took about 4 ms, cached GPU execution about 17 ms, and the
+one-time CUDA build about 39 seconds.
+
+## SRDatalog semantics
+
+The PyReason delay `<-1` is source-level data, not a special GPU scheduling
+primitive.  `Successor(t,t1)` connects an `AnalystAt` state at `t` to the state
+produced at `t1`, and ordinary semi-naive evaluation carries the change.
+
+`AnalystAt(node,time,lower,upper)` is a functional lattice relation keyed by
+`(node,time)`.  Duplicate knowledge is joined by interval intersection:
+
+```
+[l1,u1] join [l2,u2] = [max(l1,l2), min(u1,u2)]
+```
+
+Each connector join first emits the raw derivation witnesses for one PyReason
+rule.  A functional candidate relation groups them by `(node,time)` and
+materializes the rule-local `ARG MAX`: maximum lower bound, with stable
+connector rank as the tie-break key.  This is required to reproduce
+`paired_minimum_bounds_ann_fn`; intersecting all raw witnesses is not
+equivalent.
+
+Candidate insertion performs the selection during keyed `NEW -> FULL`
+maintenance.  The following candidate-to-`AnalystAt` rule is only a projection
+of the already-selected witness.  Insertion into `AnalystAt` then applies the
+different, cross-rule interval-intersection operation.  A future head aggregate
+could fuse these stages, but it could not remove their semantic grouping
+boundary.
+
+Bounds are stored in two columns as bit-cast IEEE-754 binary32 words.  All
+generated values are in `[0,1]`, where unsigned word order preserves float
+order.  MIR sees only a generic functional-lattice merge/delta operation;
+sorted-array GPU maintenance is one physical realization of it.
+
+## Stress parity and benchmark
+
+Run the PyReason oracle in one warm process:
+
+```bash
+uv run --project minimal_vulreasoner --frozen \
+  python minimal_vulreasoner/benchmark_pyreason.py \
+  --warmup \
+  --case 4,4,2 \
+  --case 8,32,4 \
+  --case 12,128,8
+```
+
+Build once and run the same shapes on SRDatalog:
+
+```bash
+uv run --project minimal_vulreasoner --frozen \
+  python minimal_vulreasoner/benchmark_srdatalog.py \
+  --case 4,4,2 \
+  --case 8,32,4 \
+  --case 12,128,8 \
+  --repeat 2
+```
+
+Both harnesses print `target_bounds_sha256`, a SHA-256 digest over every final
+target and interval.  Equal digests establish exact target-set parity, while
+`target_bounds_sample` leaves a few decoded bounds visible for diagnosis.
+
+On an NVIDIA RTX 6000 Ada, the exact implementation produced these warm
+measurements:
+
+| Depth × width × fanout | Transitions | PyReason reason | SRDatalog run | Digest parity |
+|---|---:|---:|---:|---|
+| 4 × 4 × 2 | 32 | 8.1 ms | 8.2 ms | exact |
+| 8 × 32 × 4 | 1,024 | 351.8 ms | 32.5 ms | exact |
+| 12 × 128 × 8 | 12,288 | 29.39 s | 32.7 ms | exact |
+| 16 × 256 × 8 | 32,768 | — | 44.8 ms | GPU stress only |
+
+Compilation is intentionally reported separately (about 49 seconds on this
+machine) because generated CUDA is cached and reused.  The GPU harness also
+uses an explicit process exit after database shutdown to avoid a known
+ctypes/CUDA shared-library static-teardown crash; this does not affect query
+results or measured execution time.

minimal_vulreasoner/__init__.py

@@ -0,0 +1 @@
+"""Minimal VulReasoner parity and stress fixtures."""

minimal_vulreasoner/analyst_rule_loader.py

@@ -0,0 +1,141 @@
+'''Parse the constrained PyReason analyst-rule CSV into source-level specs.'''
+
+from __future__ import annotations
+
+import csv
+import re
+from dataclasses import dataclass
+from pathlib import Path
+
+_HEAD = re.compile(
+  r"^analystAt\((?P<target>[A-Za-z_]\w*)\):(?P<annotation>[A-Za-z_]\w*)$"
+)
+_ATOM = re.compile(
+  r"(?P<predicate>[A-Za-z_]\w*)\((?P<arguments>[^)]*)\)"
+  r"(?:\:\[(?P<lower>[0-9.]+),(?P<upper>[0-9.]+)\])?"
+)
+
+
+@dataclass(frozen=True)
+class Bound:
+  lower: float
+  upper: float
+
+  def __post_init__(self) -> None:
+    if not 0.0 <= self.lower <= self.upper <= 1.0:
+      raise ValueError(f"invalid probability interval [{self.lower},{self.upper}]")
+
+
+@dataclass(frozen=True)
+class AnalystRuleSpec:
+  name: str
+  connector_predicate: str
+  annotation_function: str
+  delay: int
+  analyst_bound: Bound
+  cause_label_bound: Bound
+  effect_label_bound: Bound
+  connector_bound: Bound
+
+  @property
+  def relation_name(self) -> str:
+    return "".join(part.title() for part in self.connector_predicate.split("_"))
+
+  @property
+  def input_file(self) -> str:
+    return f"{self.connector_predicate}.csv"
+
+
+@dataclass(frozen=True)
+class _AtomSpec:
+  predicate: str
+  arguments: tuple[str, ...]
+  bound: Bound | None
+
+
+def _atom_specs(body: str) -> tuple[_AtomSpec, ...]:
+  atoms = []
+  for match in _ATOM.finditer(body):
+    lower = match.group("lower")
+    upper = match.group("upper")
+    bound = None if lower is None else Bound(float(lower), float(upper))
+    atoms.append(
+      _AtomSpec(
+        match.group("predicate"),
+        tuple(arg.strip() for arg in match.group("arguments").split(",")),
+        bound,
+      )
+    )
+  return tuple(atoms)
+
+
+def parse_analyst_rule(rule_text: str, name: str) -> AnalystRuleSpec:
+  '''Parse and validate the one connector-rule shape supported by this query.'''
+  pieces = re.split(r"\s+<-(\d+)\s+", rule_text.strip(), maxsplit=1)
+  if len(pieces) != 3:
+    raise ValueError(f"{name}: expected a delayed '<-N' rule")
+  head_text, delay_text, body_text = pieces
+  head = _HEAD.fullmatch(head_text)
+  if head is None or head.group("target") != "CB2":
+    raise ValueError(f"{name}: expected analystAt(CB2):annotation head")
+
+  atoms = _atom_specs(body_text)
+  analyst = [atom for atom in atoms if atom.predicate == "analystAt"]
+  labels = [atom for atom in atoms if atom.predicate == "hasLabel"]
+  steps = [atom for atom in atoms if atom.predicate == "stepFrom"]
+  connectors = [
+    atom
+    for atom in atoms
+    if atom.predicate not in {"analystAt", "hasLabel", "stepFrom"}
+  ]
+  if len(analyst) != 1 or len(labels) != 2 or len(steps) != 1 or len(connectors) != 1:
+    raise ValueError(
+      f"{name}: expected analystAt, two hasLabel clauses, one connector, and stepFrom"
+    )
+  if analyst[0].arguments != ("CB1",) or steps[0].arguments != ("CB1", "CB2"):
+    raise ValueError(f"{name}: unsupported analystAt/stepFrom variables")
+  label_by_block = {atom.arguments[0]: atom for atom in labels}
+  if set(label_by_block) != {"CB1", "CB2"}:
+    raise ValueError(f"{name}: hasLabel clauses must be keyed by CB1 and CB2")
+  connector = connectors[0]
+  expected_connector_args = (
+    label_by_block["CB1"].arguments[1],
+    label_by_block["CB2"].arguments[1],
+  )
+  if connector.arguments != expected_connector_args:
+    raise ValueError(f"{name}: connector variables do not pair the hasLabel clauses")
+  bounded = (analyst[0], label_by_block["CB1"], label_by_block["CB2"], connector)
+  if any(atom.bound is None for atom in bounded):
+    raise ValueError(f"{name}: every bounded body atom requires [lower,upper]")
+
+  return AnalystRuleSpec(
+    name=name,
+    connector_predicate=connector.predicate,
+    annotation_function=head.group("annotation"),
+    delay=int(delay_text),
+    analyst_bound=analyst[0].bound,
+    cause_label_bound=label_by_block["CB1"].bound,
+    effect_label_bound=label_by_block["CB2"].bound,
+    connector_bound=connector.bound,
+  )
+
+
+def load_analyst_rules(path: str | Path) -> tuple[AnalystRuleSpec, ...]:
+  with Path(path).open(newline="") as handle:
+    rows = csv.DictReader(handle)
+    required = {"rule_text", "name", "infer_edges", "set_static"}
+    if rows.fieldnames is None or not required <= set(rows.fieldnames):
+      raise ValueError(f"analyst rule CSV requires columns {sorted(required)}")
+    specs = []
+    for row in rows:
+      if row["infer_edges"].strip().lower() != "true":
+        raise ValueError(f"{row['name']}: analyst connector rule must infer edges")
+      if row["set_static"].strip().lower() != "false":
+        raise ValueError(f"{row['name']}: delayed analyst result must not be static")
+      specs.append(parse_analyst_rule(row["rule_text"], row["name"]))
+  if not specs:
+    raise ValueError(f"analyst rule CSV contains no rules: {path}")
+  predicates = [spec.connector_predicate for spec in specs]
+  if len(predicates) != len(set(predicates)):
+    raise ValueError("analyst rule CSV contains duplicate connector predicates")
+  return tuple(specs)