Unified agentic spec inference for P: frozen candidate schema, robust validation backbone, ranking (PLAN.md Phases 0-4) - #977
Open
ankushdesai wants to merge 4 commits into
Open
Conversation
…ndidate schema + verdict vocabulary
Phase 0: bring the agentic invariant-mining scripts from pinfer-peasyai-design
onto this branch (invariant_core.py, proposers, prep/diag/check/repair/verify).
Phase 1 (per Src/PInfer/Scripts/PLAN.md v2):
- Candidate/Formula dataclasses with structured formula record (quantifiers,
guards, relations, sc/config_event for quorum, uses_index) + provenance_run
- dedup_key/dedup_candidates: canonical property identity, cluster-and-keep
- Frozen verdict vocabulary: HOLDS-BOUNDED (not "HOLDS"), UNKNOWN-VACUITY for
canary-less passes, HOLDS-PROVEN reserved for PVerifier
- JUDGE_OUTPUT_SCHEMA {verdict, confidence, cex_grounding, development_action}
- build_env deduped into invariant_core (diag_compile/verify_repairs import it)
- propose_templated.js CAND_SCHEMA extended to mirror the Python contract
- test_invariant_core.py: 8 -> 22 tests (schema round-trip, dedup, judge
contract, JS<->Python parity, full mocked verdict-classification matrix)
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ser + hybrid merge Phase 2a (PLAN.md): propose_intent.js — intent-lens proposer Workflow. Derives candidates from design intent (docs + source comments) through the four INTENT_LENSES (agreement/liveness/consistency/validity), complementing propose_templated.js's grammar-scaffold enumeration. Emits the shared CAND_SCHEMA with provenance:"intent" and structured formula records; the validity lens carries the canary convention. Python INTENT_LENSES stays the source of truth (TestProposerParity guards drift). Phase 2b, deterministic half: merge_candidates.py — hybrid merge CLI. Unions candidate sets from any number of proposers (workflow-result or plain-list shape), dedups by invariant_core.dedup_key, clusters-and-keeps representatives (nothing silently dropped), and emits per-provenance in/out stats for the PLAN §8 reduction-ratio metric. The PInfer enumerative adapter plugs in as just another input file. Tests: 22 -> 26 (proposer parity, cross-proposer dedup with cluster/stat assertions, plain-list input). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…aseline-diff attribution The three silent-failure fixes from the PLAN.md multi-agent review: - Auto-canary (M4, §6.1): make_canary derives a <Name>_canary vacuity probe from any candidate by replacing its asserts with `assert false` in place (string-literal-aware scanner, guards preserved). PREP appends canaries for candidates lacking one; validate_candidates does the same. Vacuity detection no longer depends on proposer cooperation; assert-less monitors stay UNKNOWN-VACUITY rather than being overclaimed. - Static name gate (M9, §6.2): static_gate parses the project's event/type declarations and rejects candidates observing undeclared events, handling unobserved events, or accessing phantom payload fields — before any compile cycle, with a REPAIR-ready diagnostic (verdict COMPILE-ERR, detail "static-gate: ..."). Mirrors PeasyAI's EventDeclarationValidator / PayloadFieldValidator semantics without adding a dependency. - Baseline-differential attribution (M5, §6.3): _baseline_failures bounded- checks the unmodified project once; _attribute_owner marks a candidate failure SUT-owned iff its signature pre-exists there. Replaces the brittle '_candidates.p'/'liveness'/'hot state' substring heuristic — a monitor- induced deadlock now correctly attributes to the monitor (regression test). check_candidates.py grows --no-auto-canary/--no-gate/--no-baseline. Tests: 26 -> 37 (canary derivation incl. `;`-in-format-string, attribution matrix incl. the deadlock regression, gate pass/flag/integration). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…oring kernel) Port the scoring kernel from experimental/pinfer's ranking_with_llm.py into the shared core, per PLAN.md Phase 4 / review finding M12: - compute_score: sqrt(gen*crit)*0.8 + dist*0.2 + vis*0.0 (identical formula, RANK_WEIGHTS), plus the 4-metric rubric (generalization / criticality / distinguishability / visibility) as engine-agnostic prompt strings and a RANK_OUTPUT_SCHEMA structured-output contract. - Dropped couplings: Strands agent layer, Bedrock model id, `constants` module, pruned_invariants.txt input — the ranker consumes Candidate/Verdict. - Verdict gating: only HOLDS-BOUNDED/HOLDS-PROVEN candidates are rankable; VACUOUS/FAILS/unvalidated land in an explicit unranked list with reasons (perfect LLM scores cannot rescue a gated candidate). - rank_candidates.py CLI: --emit-prompt (deterministic prompt build for the LLM-owning wrapper) and --apply (combine returned scores + gate + report), completing the wrapper-owns-the-provider seam used by propose/judge. Tests: 37 -> 42 (kernel formula/validation/custom-weights, gating+sort, prompt/schema shape). CLI smoke-tested in both modes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Contributor
There was a problem hiding this comment.
Pull request overview
Implements a unified, engine-agnostic “validate → prune/dedup → rank → judge” backbone for agentic P specification inference (per PLAN.md Phases 0–4), with a frozen candidate/formula schema, deterministic validation improvements (auto-canary vacuity handling, baseline-differential attribution, static name gate), plus two pluggable LLM proposers and supporting CLIs/tests.
Changes:
- Adds
invariant_core.pydefining the frozenCandidate/Formulaschema, dedup key + clustering, static gate, auto-canary derivation, bounded-check verdicting, and ranking kernel + prompt builders. - Adds/updates pipeline tooling: proposers (
propose_templated.js,propose_intent.js), candidate prep/merge/check/diagnose/repair/verify, and rank application. - Adds a comprehensive unit test suite (
test_invariant_core.py) and supporting docs (README_agentic_invariants.md, updatedPLAN.md).
Reviewed changes
Copilot reviewed 13 out of 13 changed files in this pull request and generated 8 comments.
Show a summary per file
| File | Description |
|---|---|
| Src/PInfer/Scripts/invariant_core.py | Core schema + validation/gating/attribution + ranking prompt/kernel utilities. |
| Src/PInfer/Scripts/test_invariant_core.py | Unit tests for schema, dedup, canary, gate, attribution, ranking, proposer parity. |
| Src/PInfer/Scripts/propose_templated.js | Template-scaffold proposer emitting schema-shaped candidates. |
| Src/PInfer/Scripts/propose_intent.js | Intent-lens proposer emitting schema-shaped candidates. |
| Src/PInfer/Scripts/prep_candidates.py | Deterministic candidate cleanup + auto-canary emission into .p files. |
| Src/PInfer/Scripts/merge_candidates.py | Hybrid merge + structured dedup (cluster-and-keep + stats). |
| Src/PInfer/Scripts/check_candidates.py | CLI wrapper over validate_candidates. |
| Src/PInfer/Scripts/diag_compile.py | Per-candidate isolated compile diagnostics for repair. |
| Src/PInfer/Scripts/repair_workflow.js | LLM workflow to repair non-compiling candidates given compiler errors. |
| Src/PInfer/Scripts/verify_repairs.py | Recompile repaired candidates to measure repair success. |
| Src/PInfer/Scripts/rank_candidates.py | Deterministic rank prompt emission + score application/gating/reporting. |
| Src/PInfer/Scripts/README_agentic_invariants.md | User-facing documentation for propose→check→judge and repair loop. |
| Src/PInfer/Scripts/PLAN.md | Updated plan/spec describing architecture, stages, acceptance, and findings map. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
|
|
||
| Return the corrected full \`spec ${f.name} ... { ... }\` source (keep the same spec name and the same intent/property) plus a one-line summary of what you changed. If a property fundamentally cannot be expressed as a P monitor (e.g. it needs the ternary only for a value the property doesn't really need), simplify minimally while preserving the property's meaning.`, | ||
| { label: `repair:${f.name}`, phase: 'Repair', schema: SCHEMA, agentType: 'Explore' } | ||
| ).then(r => ({ benchmark: f.benchmark, name: f.name, changes: r && r.changes, fixedSource: r && r.fixedSource })) |
Comment on lines
+309
to
+324
| handlers = list(_HANDLER_RE.finditer(block)) | ||
| for i, hm in enumerate(handlers): | ||
| ev, param = hm.group(1), hm.group(2) | ||
| if ev not in declared: | ||
| errs.append(f"handles undeclared event '{ev}'") | ||
| continue | ||
| if observed and ev not in observed: | ||
| errs.append(f"handles '{ev}' which is not in the observes list") | ||
| fields = declared[ev] | ||
| if fields is None: | ||
| continue # payload type unresolvable; skip field checks | ||
| body_end = handlers[i + 1].start() if i + 1 < len(handlers) else len(block) | ||
| for fa in re.finditer(rf"\b{re.escape(param)}\.(\w+)", block[hm.end():body_end]): | ||
| if fa.group(1) not in fields: | ||
| errs.append(f"'{param}.{fa.group(1)}' — event '{ev}' payload has no field " | ||
| f"'{fa.group(1)}' (fields: {sorted(fields)})") |
| sys.path.insert(0, str(Path(__file__).resolve().parent)) | ||
| from invariant_core import make_canary # noqa: E402 | ||
|
|
||
| HANDLER_RE = re.compile(r'(on\s+\w+\s+do\s*\([^)]*\)\s*|on\s+\w+\s+goto\s+\w+\s+with\s*\([^)]*\)\s*|entry\s*(?:\([^)]*\))?\s*|exit\s*)\{') |
Comment on lines
+347
to
+349
| out = subprocess.run(["p", "compile"], cwd=project, env=env, | ||
| capture_output=True, text=True).stdout | ||
| return "Compilation succeeded" in out |
| 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 |
| d = r["dir"] | ||
| diag = Path(d) / "PSpec" / "_diag.p" | ||
| diag.write_text(r["fixedSource"]) | ||
| out = subprocess.run(["p", "compile"], cwd=d, env=env, capture_output=True, text=True).stdout |
Comment on lines
+54
to
+55
| args = ap.parse_args() | ||
|
|
Comment on lines
+4
to
+5
| monitors into a P project, compile, bounded model-check, and classify each as | ||
| HOLDS / FAILS(+counterexample) / VACUOUS / INCONCLUSIVE / COMPILE-ERR. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Implements the machine-independent core of the unified P specification-inference plan (
Src/PInfer/Scripts/PLAN.md): a single validate→prune→rank→judge backbone with pluggable proposers, where LLM proposers derive candidatespecmonitors from design intent and PChecker is the sound oracle. Supersedes the scripts in #974 (same lineage, hardened).The plan is v2 — it incorporates a 44-finding multi-agent review of the v1 design; §13 of PLAN.md maps every finding to its resolution. The three silent-failure classes that review surfaced are fixed here:
make_canary): backbone derives a<Name>_canaryprobe from any candidate by replacing its asserts in place; canary-less monitors reportUNKNOWN-VACUITY, never a bare passevent/typedecls; rejects undeclared events, unobserved handlers, phantom payload fields — before any compile cycle, with a repair-ready diagnosticStructure (
Src/PInfer/Scripts/)invariant_core.py— the hub: frozenCandidate/Formulaschema (structured guards/relations/SC/quorum fields), canonical dedup key (cluster-and-keep, nothing silently dropped), honest verdict vocabulary (HOLDS-BOUNDEDvs reservedHOLDS-PROVEN,VACUOUS,UNKNOWN-VACUITY,INCONCLUSIVE), judge contract withdevelopment_action, ranking kernel (compute_score, ported fromexperimental/pinfer'sranking_with_llm.pyminus Strands/Bedrock coupling) — all engine-agnostic; wrappers own the LLM provider.propose_templated.js(grammar-scaffold enumeration) +propose_intent.js(new: design-intent lenses) emitting one schema; JS↔Python parity is unit-tested.merge_candidates.py(hybrid merge + per-provenance stats),prep_candidates.py(P fixups + auto-canaries),check_candidates.py(gate → baseline → wire → bounded-check → classify),diag_compile.py/repair_workflow.js/verify_repairs.py(compile-repair loop),rank_candidates.py(verdict-gated ranking).Testing
test_invariant_core.py), no toolchain needed: schema round-trip, dedup, full mocked verdict-classification matrix, attribution (incl. the deadlock regression), gate, canary derivation (incl.;-inside-format-string), ranking kernel + gating, JS↔Python parity.rank_candidates.py/merge_candidates.pysmoke-tested end-to-end on fixtures.p compile/p checkacceptance on FD/TPC (+ fault-injected variant, N≥3 seeds, §8 metrics) — needs a box with .NET 8 +p install+ an LLM runtime; that is the milestone's remaining exit criterion and is called out in PLAN.md §12.Reviewer notes
experimental/pinferbuilding.🤖 Generated with Claude Code