A tale of two fixes

.github/workflows/pytest.yml

@@ -23,7 +23,7 @@ jobs:
 
       - name: sync-deps
         run: |
-          uv sync --group test
+          uv sync --group test --extra prover
 
       - name: Run pytest
         run: |

certora_autosetup/setup/summary_resolver.py

@@ -105,6 +105,36 @@ def _vmtype_to_str(vmtype: dict) -> str:
     return base
 
 
+def _parse_ast_payload(stdout: str, returncode: int, stderr: str) -> Optional[dict]:
+    """Parse the JSON AST payload from ``ASTExtraction.jar`` stdout.
+
+    The jar prints ``Warning: …`` / ``Error: …``
+    diagnostic lines to stdout *before* the JSON payload, which it then prints
+    exactly once as the final output (on both the success and syntax-error paths).
+    So we drop the leading diagnostic lines and parse the remainder — rather than
+    ``json.loads`` the whole stream, which fails at char 0 on the first warning.
+    Returns the decoded payload, or ``None`` when the jar produced no AST
+    (``ast`` is null — a hard syntax error left for the TypecheckerLoop backstop).
+    """
+    lines = stdout.splitlines()
+    # Only LEADING diagnostic lines precede the JSON; never strip inside the payload.
+    while lines and lines[0].startswith(("Warning: ", "Error: ")):
+        lines.pop(0)
+    body = "\n".join(lines).strip()
+    # Empty stdout (or stdout that was nothing but diagnostics) means the jar gave us
+    # no payload — surface that with its stderr rather than an opaque JSONDecodeError.
+    if not body:
+        raise RuntimeError(f"{_AST_EXTRACTION_JAR} produced no JSON (exit {returncode}): {stderr.strip()}")
+    try:
+        payload = json.loads(body)
+    except json.JSONDecodeError as exc:
+        raise RuntimeError(
+            f"{_AST_EXTRACTION_JAR} output was not JSON after stripping diagnostics "
+            f"(exit {returncode}): {exc}; stdout_head={stdout!r} stderr={stderr.strip()!r}"
+        )
+    return payload if payload.get("ast") else None
+
+
 def _ast_extraction(blanked_source: str) -> Optional[dict]:
     """Run ``ASTExtraction.jar syntax-check`` on CVL source, return the parsed JSON.
 
@@ -125,15 +155,7 @@ def _ast_extraction(blanked_source: str) -> Optional[dict]:
         capture_output=True,
         text=True,
     )
-    # The jar prints the JSON payload to stdout even for syntax errors (ast=null). Empty
-    # stdout means it crashed before producing anything — surface that, with its stderr,
-    # rather than an opaque JSONDecodeError.
-    if not result.stdout.strip():
-        raise RuntimeError(
-            f"{_AST_EXTRACTION_JAR} produced no output (exit {result.returncode}): {result.stderr.strip()}"
-        )
-    payload = json.loads(result.stdout)
-    return payload if payload.get("ast") else None
+    return _parse_ast_payload(result.stdout, result.returncode, result.stderr)
 
 
 def parse_methods_entries(spec_path: Path, log: Optional[LogFn] = None) -> List[MethodEntry]:

composer/spec/source/summarizer.py

@@ -76,6 +76,19 @@ def _format_types(udts: list[dict]) -> str:
     return "\n".join(to_format)
 
 
+def _types_input(udts: str) -> list[str | dict]:
+    """Initial-prompt fragment advertising the available user-defined types.
+
+    Returns [] when there are none — never a list containing an empty string,
+    which would become an empty Anthropic text content block and get the whole
+    request rejected ("messages: text content blocks must be non-empty"). The
+    return type mirrors ``FlowInput.input`` so it drops straight into ``Input``.
+    """
+    if not udts:
+        return []
+    return ["The following types are available for use in your spec", udts]
+
+
 class SummarizerExtra(TypedDict):
     plan: str | None
     curr_spec: str | None
@@ -251,10 +264,7 @@ def _validator(s: ST, _res: str) -> str | None:
             typechecked="",
             plan=None,
             curr_spec=None,
-            input=[
-                "The following types are available for use in your spec",
-                udts,
-            ],
+            input=_types_input(udts),
         ),
         thread_id=ctx.thread_id,
         recursion_limit=ctx.recursion_limit,

tests/test_summarizer.py

@@ -0,0 +1,24 @@
+"""Unit tests for composer.spec.source.summarizer input construction.
+
+Regression guard: a contract with no user-defined types must not cause an empty
+text content block to be sent to the LLM (Anthropic rejects those with
+"messages: text content blocks must be non-empty").
+"""
+
+from composer.spec.source.summarizer import _format_types, _types_input
+
+
+def test_format_types_empty():
+    assert _format_types([]) == ""
+
+
+def test_types_input_empty_is_omitted():
+    # The bug: an empty udts must yield no input element, never [""].
+    assert _types_input("") == []
+
+
+def test_types_input_nonempty_keeps_preamble():
+    assert _types_input("A struct Foo at the top level: use `Foo`") == [
+        "The following types are available for use in your spec",
+        "A struct Foo at the top level: use `Foo`",
+    ]

tests/test_summary_resolver.py

@@ -0,0 +1,48 @@
+"""Unit tests for ASTExtraction stdout parsing in summary_resolver.
+
+Regression guard: ASTExtraction.jar (EVMVerifier OutPrinter) prints `Warning:`
+diagnostic lines to stdout before the JSON payload, so a raw json.loads of stdout
+fails at char 0. `_parse_ast_payload` must strip those leading lines and parse the
+JSON that follows.
+"""
+
+import json
+
+import pytest
+
+from certora_autosetup.setup.summary_resolver import _parse_ast_payload
+
+_AST = {"ast": {"importedMethods": []}}
+_AST_JSON = json.dumps(_AST)
+
+
+def test_pure_json_no_warnings():
+    assert _parse_ast_payload(_AST_JSON, 0, "") == _AST
+
+
+def test_warning_lines_before_json_are_stripped():
+    stdout = (
+        "Warning: Syntax warning in spec file dummy file:1:1: Registered the contract alias x\n"
+        "Warning: Syntax warning in spec file dummy file:2:1: Registered the contract alias y\n"
+        + _AST_JSON
+    )
+    assert _parse_ast_payload(stdout, 0, "") == _AST
+
+
+def test_ast_null_returns_none():
+    assert _parse_ast_payload(json.dumps({"ast": None}), 1, "") is None
+
+
+def test_empty_stdout_raises_with_exit_and_stderr():
+    with pytest.raises(RuntimeError, match="produced no JSON.*exit 3.*boom"):
+        _parse_ast_payload("", 3, "boom")
+
+
+def test_warnings_only_no_json_raises():
+    with pytest.raises(RuntimeError, match="produced no JSON"):
+        _parse_ast_payload("Warning: something\n", 0, "")
+
+
+def test_non_json_after_stripping_raises_with_context():
+    with pytest.raises(RuntimeError, match="was not JSON after stripping diagnostics"):
+        _parse_ast_payload("Warning: w\nnot json at all", 0, "stderr text")