Route SAT diagnostics through public capabilities

Author: Grace Lee Rui Yue

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

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,