Unified agentic spec inference for P: frozen candidate schema, robust validation backbone, ranking (PLAN.md Phases 0-4)

Src/PInfer/Scripts/README_agentic_invariants.md

@@ -0,0 +1,91 @@
+# Agentic invariant mining (propose → check → judge)
+
+A lightweight, agent-driven alternative to brute-force trace mining. Instead of
+enumerating predicates over traces, an LLM agent **proposes** the invariants a
+protocol *should* satisfy by reading the P **source + design-intent comments**,
+those candidates are **model-checked** by PChecker (the sound oracle), and the
+agent then **judges** each result. PChecker — not the agent — is the source of truth.
+
+```
+  ┌─────────────────────────────┐   reads PSrc/*.p + design comments
+  │ ① PROPOSE  (LLM agent)      │   emits intent-level `spec` monitors
+  │   derive from INTENT, not    │   → a candidates .p file
+  │   from the implementation    │
+  └──────────────┬──────────────┘
+                 ▼
+  ┌─────────────────────────────┐   check_candidates.py:
+  │ ② CHECK  (this tool)        │   wire monitors in, generate one test each,
+  │   PChecker on EVERY candidate│   compile, model-check, classify,
+  │   + vacuity canaries         │   extract counterexamples
+  └──────────────┬──────────────┘
+                 ▼  HOLDS / FAILS(+cex) / VACUOUS
+  ┌─────────────────────────────┐   for each FAILS: required property → BUG,
+  │ ③ JUDGE  (LLM agent)        │   else over-strong → SPURIOUS (repair/drop).
+  │   grounded in the cex        │   for each HOLDS: meaningful vs vacuous.
+  └─────────────────────────────┘
+```
+
+## Why this shape
+
+* **Propose from intent, never from the implementation.** If candidates merely
+  paraphrase the code, a bug becomes a "correct" invariant and is never found.
+  Deriving from the protocol's *contract* lets PChecker measure the gap between
+  intent and implementation — and that gap is where bugs live.
+* **No trace pre-filter.** A failing candidate is *information*, not garbage: it
+  is either a real bug (a required property the system violates) or an over-strong
+  candidate. Only a sound check + judgment over the concrete counterexample can
+  tell them apart, so every candidate goes to PChecker.
+* **Vacuity is checked.** "HOLDS" can be a lie if the assertion's guard never
+  fires. A `<Name>_canary` companion (`assert false` in the same guarded branch)
+  reveals it: if the canary never trips, `<Name>` verified nothing.
+
+## Using the checker
+
+```bash
+python3 Src/PInfer/Scripts/check_candidates.py \
+  --project   Tutorial/4_FailureDetector \
+  --candidates /path/to/candidates.p \
+  --main      TestMultipleClients \
+  --assert-in "union { TestMultipleClients }, FailureDetector, FailureInjector" \
+  --iters     3000
+```
+
+* `--candidates` is a `.p` file containing one or more `spec <Name> observes ... { ... }`
+  blocks (the proposer agent's output). A `spec <Name>_canary` block is treated as a
+  vacuity probe for `<Name>`.
+* `--assert-in` is the module expression that appears after `in` in the project's
+  existing test (copy it from `PTst/TestScript.p`).
+* The tool resolves `dotnet`/`DOTNET_ROOT` automatically and cleans up the files it
+  generates (`PSpec/_candidates.p`, `PTst/_candidate_tests.p`) unless `--keep`.
+
+Steps ① and ③ are LLM steps (run them with Claude Code / any agent); this script is
+the deterministic middle. Validated on Two-Phase Commit, where the loop surfaced a
+real read-your-writes consistency violation and correctly separated it from an
+over-strong "all vote SUCCESS ⇒ commit" candidate that fails only due to benign timeouts.
+
+## Compile-repair stage (recovers candidates that don't compile)
+
+LLM-written spec monitors fail to compile ~28% of the time (concentrated in multi-state
+liveness monitors): inline `var` init, `?:` ternary, `not`/`not in`, `{x}` string
+interpolation, duplicate state names, seq-vs-set, invented event names. A two-script
+loop recovers them by feeding the *exact compiler error* back to an LLM:
+
+```bash
+# 1. Diagnose: compile each candidate alone, capture its first compiler error.
+python3 Src/PInfer/Scripts/diag_compile.py --out fails.json \
+    FailureDetector=Tutorial/4_FailureDetector=fd_candidates.p
+# 2. Repair (LLM): an agent per failing spec rewrites it given the error + P syntax rules.
+#    repair_workflow.js is a Workflow; pass `fails.json` as its args; it returns fixed sources.
+# 3. Verify: recompile each fixed spec.
+python3 Src/PInfer/Scripts/verify_repairs.py repairs.json
+```
+
+Iterate steps 2-3: round 1 fixes the shallow errors; round 2 gets the deeper ones the
+first fix exposes (e.g. an invented `eSpec_..._Init` event, a residual seq/set mismatch).
+On the 4-benchmark sweep this recovered **all 23** previously-uncompilable candidates in
+two rounds (15 then 8) — compile yield ~72% → ~100%. The repair agent must read the real
+PSrc/PTst to avoid hallucinating event names, and is told to preserve the property, fixing
+only syntax/encoding. Place repair AFTER deterministic `prep_candidates.py` (which already
+unescapes entities, hoists `var` decls, and rewrites `!in`/`for`) so the LLM only handles
+the genuinely diverse long tail.
+```

Src/PInfer/Scripts/check_candidates.py

@@ -0,0 +1,57 @@
+#!/usr/bin/env python3
+"""
+check_candidates.py — CLI over the shared `invariant_core` engine: wire candidate spec
+monitors into a P project, compile, bounded model-check, and classify each as
+HOLDS / FAILS(+counterexample) / VACUOUS / INCONCLUSIVE / COMPILE-ERR.
+
+A `<Name>_canary` companion spec (assert false in the same guarded branch) drives vacuity
+detection; a failure owned by a pre-existing SUT assertion is reported INCONCLUSIVE.
+
+    python3 check_candidates.py --project Tutorial/4_FailureDetector \
+        --candidates fd_candidates.p --main TestMultipleClients \
+        --assert-in "union { TestMultipleClients }, FailureDetector, FailureInjector" --iters 3000
+
+This is the deterministic middle of the agentic loop (propose → check → judge). See
+README_agentic_invariants.md; the engine lives in invariant_core.py.
+"""
+import argparse
+import json
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+from invariant_core import validate_candidates  # noqa: E402
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--project", required=True, help="P project dir (contains the .pproj)")
+    ap.add_argument("--candidates", required=True, help=".p file of candidate spec monitors")
+    ap.add_argument("--main", required=True, help="test main machine name")
+    ap.add_argument("--assert-in", required=True, help="module expression after 'in' (no trailing ';')")
+    ap.add_argument("--iters", type=int, default=3000, help="schedules per candidate")
+    ap.add_argument("--keep", action="store_true", help="leave generated files in place")
+    ap.add_argument("--no-auto-canary", action="store_true",
+                    help="don't derive vacuity canaries for canary-less candidates")
+    ap.add_argument("--no-gate", action="store_true",
+                    help="skip the static event/field name gate")
+    ap.add_argument("--no-baseline", action="store_true",
+                    help="skip the baseline run (monitor-vs-SUT attribution degrades)")
+    args = ap.parse_args()
+
+    src = Path(args.candidates).read_text()
+    verdicts = validate_candidates(args.project, src, args.main, args.assert_in, args.iters, args.keep,
+                                   auto_canary=not args.no_auto_canary,
+                                   gate=not args.no_gate, baseline=not args.no_baseline)
+
+    print(f"{'CANDIDATE':<42}{'VERDICT':<17}DETAIL")
+    print("-" * 100)
+    for v in verdicts:
+        print(f"{v.name:<42}{v.verdict:<17}{v.detail}")
+    print("\nNext: an agent judges each FAILS as `bug` (required property) or `spurious` "
+          "(over-strong), and each HOLDS-BOUNDED for vacuity/interestingness.")
+    print(json.dumps([{"name": v.name, "verdict": v.verdict, "detail": v.detail} for v in verdicts]))
+
+
+if __name__ == "__main__":
+    main()

Src/PInfer/Scripts/diag_compile.py

@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+"""Diagnose WHY candidate spec monitors fail to compile.
+
+Wires each `spec` block (from a candidates .p file) ALONE into its P project and
+captures the compiler's first error, so the repair stage can fix each given the
+exact diagnostic. Emits a JSON list [{benchmark,dir,name,source,error}].
+
+Usage:
+    python3 diag_compile.py --out fails.json \
+        ClientServer=Tutorial/1_ClientServer=cand_ClientServer.p \
+        FailureDetector=Tutorial/4_FailureDetector=cand_FailureDetector.p
+each positional arg is  <label>=<projectDir>=<candidateFile>.
+"""
+import argparse, json, re, subprocess, sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+from invariant_core import build_env  # noqa: E402  (single source of the dotnet/`p` resolver)
+
+SPEC_RE = re.compile(r'^\s*spec\s+([A-Za-z_]\w*)', re.MULTILINE)
+ERR_RE = re.compile(r'(error:|\[.*Error.*\]|Error:|expecting|mismatched|no viable|cannot|'
+                    r'undeclared|not declared|Expected|duplicates|could not find)', re.IGNORECASE)
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument("--out", default="compile_fails.json")
+    ap.add_argument("targets", nargs="+", help="<label>=<projectDir>=<candidateFile> ...")
+    args = ap.parse_args()
+    env = build_env()
+
+    fails = []
+    for t in args.targets:
+        label, d, candfile = t.split("=", 2)
+        src = Path(candfile).read_text()
+        spans = [(m.start(), m.group(1)) for m in SPEC_RE.finditer(src)] + [(len(src), None)]
+        diag = Path(d) / "PSpec" / "_diag.p"
+        for i in range(len(spans) - 1):
+            name, block = spans[i][1], src[spans[i][0]:spans[i + 1][0]].strip()
+            diag.write_text(block)
+            out = subprocess.run(["p", "compile"], cwd=d, env=env, capture_output=True, text=True).stdout
+            if "Compilation succeeded" not in out:
+                errs = [l.strip() for l in out.splitlines() if ERR_RE.search(l)]
+                first = next((l for l in errs if "0 Error" not in l and "Build succeeded" not in l), "")
+                print(f"[{label}] {name}: {first[:150]}")
+                fails.append({"benchmark": label, "dir": d, "name": name, "source": block, "error": first[:300]})
+        diag.unlink(missing_ok=True)
+
+    Path(args.out).write_text(json.dumps(fails, indent=2))
+    print(f"\n{len(fails)} failing specs -> {args.out}")
+
+
+if __name__ == "__main__":
+    main()