Route SAT and SMT recovery diagnostics through public capabilities - #609
Conversation
47f29df to
075e71e
Compare
yuelgrace1810-ops
changed the title
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 50ff4ca587
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| hint=( | ||
| "Create the assignment with SatArtifactService.put_assignment " | ||
| "against the intended canonical CNF." | ||
| "Use math.find for sat.model.find to produce an assignment " |
There was a problem hiding this comment.
When an invalid assignment URI triggers this diagnostic, following the hint only inspects sat.model.find: math.find is read-only discovery and cannot produce the promised assignment artifact. The same misleading wording appears in the new CNF and SAT/SMT proof hints. Direct callers to the public MCP surface therefore remain unable to complete the stated recovery unless they already know to make a separate math.run call; explicitly say to inspect the producer with math.find and execute it with math.run, or point directly to math.run.
AGENTS.md reference: AGENTS.md:L58-L62
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Addressed in ce16268: recovery hints now say "inspect with math.find and execute with math.run" instead of just "use math.find", so callers can complete the stated artifact recovery.
math.find is read-only discovery and cannot produce assignment or proof artifacts. Update recovery hints to say 'inspect with math.find and execute with math.run' so callers can complete the stated recovery.
2 participants
Summary
math.findcapability routesRoot cause
Verifier and solver diagnostics were exposed through public capability results, but their remediation text instructed agents to call internal Python service methods that are not available through MCP. Evaluation exposed this first for SAT; a repository-wide literal-hint audit then found the same independent pattern in SMT proof verification.
Audit evidence
A combined capability-composition and diagnostic-actionability audit checked:
All 328 installed capability titles were rediscoverable in the top five, all 224 published invocation examples completed, 42 emitted relationships resolved to stored artifacts, and the two packaged skill surfaces were byte-identical. The actionable internal-API references were isolated to SAT and SMT recovery hints.
Overlap review
Validation
git diff --check: passedThis is intentionally a draft PR and does not change SAT/SMT mathematics, assurance, artifact validation, or provider installation policy.