Route SAT and SMT recovery diagnostics through public capabilities

src/jacobian/sat_smt/cadical.py

@@ -544,8 +544,9 @@ def _resolve_request(
                 schema_uri=sat.installation.cnf_schema_uri,
                 expected="one valid canonical CNF artifact and enforceable budget",
                 hint=(
-                    "Create the instance with SatArtifactService.put_cnf and use "
-                    "only the advertised wall-time and conflict limits."
+                    "Use math.find for sat.cnf.materialize to create the canonical "
+                    "CNF, then pass its cnf_uri with only the advertised wall-time "
+                    "and conflict limits."
                 ),
             )
         ) from exc

src/jacobian/sat_smt/sat_capabilities.py

@@ -417,8 +417,10 @@ def invoke(self, request: CapabilityRequest) -> CapabilityResult:
                         "to one canonical CNF"
                     ),
                     hint=(
-                        "Create the assignment with SatArtifactService.put_assignment "
-                        "against the intended canonical CNF."
+                        "Use math.find for sat.model.find to produce an assignment "
+                        "artifact for the intended canonical CNF. If that optional "
+                        "producer is unavailable, install the CaDiCaL provider; do "
+                        "not invent an assignment URI."
                     ),
                 )
             ) from exc
@@ -630,8 +632,10 @@ def invoke(self, request: CapabilityRequest) -> CapabilityResult:
                         "lineage to one canonical CNF"
                     ),
                     hint=(
-                        "Create the proof with SatArtifactService.put_proof against "
-                        "the intended canonical CNF."
+                        "Use math.find for sat.unsat_proof.find to produce a proof "
+                        "artifact for the intended canonical CNF. If that optional "
+                        "producer is unavailable, install the CaDiCaL provider; do "
+                        "not invent a proof URI."
                     ),
                 )
             ) from exc

src/jacobian/sat_smt/smt_capabilities.py

@@ -180,8 +180,10 @@ def invoke(self, request: CapabilityRequest) -> CapabilityResult:
                         "lineage to one exact pinned-profile SMT query"
                     ),
                     hint=(
-                        "Create the proof with smt.unsat_proof.find or "
-                        "SmtArtifactService.put_proof against the intended query."
+                        "Use math.find for smt.unsat_proof.find to produce a proof "
+                        "artifact for the intended query. If that optional producer "
+                        "is unavailable, install the cvc5 provider; do not invent a "
+                        "proof URI."
                     ),
                 )
             ) from exc

tests/boundary/providers/external_sat/startup/test_smt_unsat_proof_verification.py

@@ -167,6 +167,27 @@ def _verify(runtime: JacobianRuntime, proof_uri: str):
     )
 
 
+def test_invalid_proof_diagnostic_routes_through_public_capabilities(
+    tmp_path: Path,
+    monkeypatch: pytest.MonkeyPatch,
+) -> None:
+    executable = _fake_carcara(
+        tmp_path,
+        "print('valid')\nraise SystemExit(0)",
+    )
+    runtime = _runtime_with_runtime(tmp_path, monkeypatch, executable)
+
+    result = _verify(runtime, "artifact://sha256/" + "0" * 64)
+
+    assert result.execution.status is ExecutionStatus.ERROR
+    assert result.diagnostics[0].code == "INVALID_SMT_UNSAT_PROOF"
+    hint = result.diagnostics[0].hint or ""
+    assert "math.find" in hint
+    assert "smt.unsat_proof.find" in hint
+    assert "cvc5" in hint
+    assert "SmtArtifactService" not in hint
+
+
 def test_unsat_proof_is_verified_by_authorized_strict_carcara(
     tmp_path: Path,
     monkeypatch: pytest.MonkeyPatch,

tests/composition/runtime/test_sat_assignment_verification.py

@@ -79,6 +79,23 @@ def test_sat_assignment_verifier_declares_its_typed_artifact_route(
     )
 
 
+def test_invalid_assignment_diagnostic_routes_through_public_capabilities(
+    authorized_complete_runtime,
+) -> None:
+    result = _verify(
+        authorized_complete_runtime,
+        "artifact://sha256/" + "0" * 64,
+    )
+
+    assert result.execution.status is ExecutionStatus.ERROR
+    assert result.diagnostics[0].code == "INVALID_SAT_ASSIGNMENT"
+    hint = result.diagnostics[0].hint or ""
+    assert "math.find" in hint
+    assert "sat.model.find" in hint
+    assert "CaDiCaL" in hint
+    assert "SatArtifactService" not in hint
+
+
 def test_sat_assignment_is_verified_by_an_authorized_clean_process(
     authorized_complete_runtime,
     monkeypatch: pytest.MonkeyPatch,