feat(guarantee): calls-resolution-is-a-function (severity:error)#479
Merged
Conversation
…ck resolver soundness A new datalog guarantee: a CALL must not resolve to two distinct targets under the same resolvedVia tag — resolution must be a function. Carves out the two resolvers that are one-to-many BY DESIGN: rust-dyn-dispatch (trait-object semantic dispatch) and rust-cross-method (the heuristic parity ceiling; precise resolution = the team-server SCIP tier). This is the enforcement layer for the #23 rust_calls rework (#466 + #467): with rust-calls now a true function, the guarantee locks the property and catches regressions. Verified on a fresh rust graph via the derive engine (backend.checkGuarantee): 0 violations WITH the carve-outs, 561 WITHOUT them (= rust-cross-method 237 + rust-dyn-dispatch 324 — exactly the two excluded one-to-many resolvers, nothing else over-resolves). Uses the derive builtin edge_attr to read the CALLS edge's resolvedVia; the edge() generator legs lead so the planner binds before the edge_attr point-probes (E-PLAN-002 otherwise). severity:error. `grafema check` is NOT wired into CI, so this is opt-in enforcement (grafema check → process.exit(1) on violation), not a per-PR CI blocker. Known scope: the JS resolvers (runtime-globals residual, cross-file-calls, same-file-calls) have their own over-resolution not yet closed — the JS analogue of the #23 rust work; on a graph where they fire, this rule reports them (correctly, as real over-resolutions to fix). Supersedes the stale vm #431 branch (which carried no actual rule). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
1 participant
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
A new
grafema checkdatalog guarantee: a CALL must not resolve to two distinct targets under the sameresolvedViatag — resolution must be a function. This is the enforcement layer for the #23rust_callsrework (#466 + #467) — withrust-callsnow a true function, this locks the property and catches regressions.Supersedes the stale vm
#431branch (which carried no actual rule — it only removed a guarantee main has since added).Carve-outs (one-to-many BY DESIGN, not bugs)
rust-dyn-dispatch— trait-object method call dispatches to every impl by design.rust-cross-method— cross-implx.len()with no local receiver type fans to everylenimpl; the heuristic parity ceiling (precise = team-server SCIP tier).Verification (fresh rust graph, derive engine via
checkGuarantee)The rule uses the derive builtin
edge_attrto read the CALLS edgeresolvedVia; theedge()generator legs lead so the planner binds before theedge_attrpoint-probes (otherwise E-PLAN-002). YAML validated; rule follows the schema of the 50 existing guarantees.Gate semantics
severity:error, butgrafema checkis not wired into CI — so this is opt-in enforcement (grafema check→exit 1on violation), not a per-PR CI blocker.Known scope (follow-up)
The JS resolvers (
runtime-globalsresidual,cross-file-calls,same-file-calls) have their own over-resolution not yet closed — the JS analogue of the #23 rust work. On a graph where they fire, this rule reports them (correctly — they are real over-resolutions to fix). Closing them is a separate effort before this gate is green JS-wide.🤖 Generated with Claude Code