From 29c81c83ecea1942b7cc923a24f33933b158da82 Mon Sep 17 00:00:00 2001 From: John Toman Date: Wed, 22 Jul 2026 22:14:25 -0700 Subject: [PATCH 1/8] checkpoint --- composer/spec/source/author.py | 6 +- composer/templates/property_judge_prompt.j2 | 22 ++++- composer/ui/thread_renderer.py | 100 ++++++++++++++++++-- 3 files changed, 114 insertions(+), 14 deletions(-) diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index d0bf3cd3..096437b8 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -30,7 +30,7 @@ from langgraph.types import Command -from composer.spec.feedback import property_feedback_judge, FeedbackTemplate +from composer.spec.feedback import property_feedback_judge, FeedbackTemplate, Properties from composer.ui.tool_display import tool_display from graphcore.graph import FlowInput @@ -391,8 +391,8 @@ async def batch_cvl_generation( feedback_env = property_feedback_judge( ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({ "sort": "existing", - "context": component - }), props + "context": component, + }).depends(Properties), props ) res_state = await run_cvl_generator( diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 9df5b704..9a5b9df5 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -207,9 +207,11 @@ Verify that the specification covers all {{ properties | length }} listed proper - If the spec does NOT address a property AND the author has NOT declared a skip for it: reject the spec and flag the missing property. - If the author declared a skip for a property: critically evaluate the justification. If the property IS expressible in CVL (e.g., using ghost state, invariants, or other CVL features), reject the skip and explain how it can be formalized. - Only accept a skip if the property is genuinely beyond CVL's expressiveness. However, you *MUST NOT* - accept an author's claims that a property is beyond CVL's expressiveness at face value; - perform your own research (or examine any CVL Document references cited in their skip) + Only accept a skip if the property is genuinely beyond CVL's expressiveness *as confirmed + by your own empirical research* or provided CVL-Document-Ref citations. Do *NOT* accept + accept an author's claims that a property is beyond CVL's expressiveness at face value, + nor should you make your *own* assumptions about CVL expressibility: + you MUST perform your own research (or examine any CVL Document references cited in their skip) and critically examine their claims about CVL expressivity when evaluating the skip. *Exception*: if the author has filed an empirical rebuttal (see Step 1) against a prior-round @@ -222,6 +224,17 @@ Verify that the specification covers all {{ properties | length }} listed proper code are INVALID. {% endif %} +Do NOT "wave through" skip reasons because they sound plausible or confidently assert uncited +facts about CVL or the prover behavior. Further, do not accept as a skip justification +citations of limitations of their own authored CVL, i.e., +reject a reason that explains their chosen summarization/hook/ghost strategy +doesn't admit verifying the skipped property. The author has *full control* over the *entire* CVL +file you are reviewing, including the summaries, hooks, ghosts, cvl functions, etc. +If the summarization/hook/ghost strategy they chose makes the desired +property impossible to verify, but an alternative strategy could, reject the skip with advice +on how to adjust the strategy. + + **Array quantification limitation**: The Certora Prover cannot universally quantify over dynamic-length arrays. Properties that reason about all elements of an array can only be verified by explicitly bounding the array size and adding element-wise logic for each case. @@ -247,6 +260,9 @@ the current stub implementation; stubs are *NON-FUNCTIONAL* and are purely a min the specification. {% endif %} +If the author skipped properties, be sure to review your rough draft to determine if the cited reasons +stand up to scrutiny. + ## Step 6 Update your memories, and then output the results of your feedback. diff --git a/composer/ui/thread_renderer.py b/composer/ui/thread_renderer.py index e88f80d9..17f09478 100644 --- a/composer/ui/thread_renderer.py +++ b/composer/ui/thread_renderer.py @@ -6,8 +6,9 @@ import json from typing import Awaitable, Callable +from textual import events from textual.binding import Binding -from textual.containers import VerticalScroll +from textual.containers import VerticalScroll, HorizontalScroll, Horizontal from textual.widgets import Static, Collapsible from rich.text import Text @@ -16,9 +17,55 @@ from langchain_core.messages import AIMessage, HumanMessage, SystemMessage, ToolMessage from composer.io.thread_timeline import SummarizationMarker, TimelineItem +from composer.ui.clipboard import copy_to_clipboard from composer.ui.content import normalize_content +class CopyButton(Static): + """A compact glyph that copies a fixed payload to the system clipboard. + + Clickable and keyboard-focusable (Enter copies). The full payload is echoed + in the confirmation toast — never truncated — so the user can eyeball what + landed on the clipboard. + """ + + can_focus = True + + DEFAULT_CSS = """ + CopyButton { width: auto; padding: 0 1; color: $accent; } + CopyButton:hover { background: $accent 30%; } + CopyButton:focus { background: $accent 50%; text-style: bold; } + """ + + BINDINGS = [Binding("enter", "copy", "Copy", show=False)] + + def __init__(self, payload: str, *, what: str, glyph: str = "⧉", **kwargs) -> None: + super().__init__(glyph, **kwargs) + self._payload = payload + self._what = what + self.tooltip = f"Copy {what}" + + def on_click(self, event: events.Click) -> None: + event.stop() + self.action_copy() + + def action_copy(self) -> None: + if copy_to_clipboard(self._payload): + self.app.notify(f"Copied {self._what}: {self._payload}") + else: + self.app.notify( + "No clipboard tool found (install wl-clipboard / xclip / xsel).", + severity="error", + ) + + +def _wide(body) -> HorizontalScroll: + """Wrap a wide payload (JSON, prover/CEX traces) in a content-height box + that scrolls sideways instead of clipping or wrapping. The inner widget is + sized to its natural width via CSS (``width: auto``).""" + return HorizontalScroll(body) + + def _first_line(s: str, max_len: int = 100) -> str: for line in s.splitlines(): stripped = line.strip() @@ -81,7 +128,7 @@ class ThreadRenderer(VerticalScroll): DEFAULT_CSS = """ ThreadRenderer { height: 1fr; padding: 0 2; } ThreadRenderer > * { margin-bottom: 1; } - ThreadRenderer .turn-header { margin-top: 1; } + ThreadRenderer .turn-header { margin-top: 1; width: 1fr; } ThreadRenderer .turn-header:hover { background: $accent 30%; } ThreadRenderer .tool-call { margin-left: 2; } ThreadRenderer .tool-result { margin-left: 2; } @@ -101,6 +148,17 @@ class ThreadRenderer(VerticalScroll): ThreadRenderer DescendableToolCall > CollapsibleTitle:focus { background: $warning 40%; } + + ThreadRenderer HorizontalScroll { height: auto; } + ThreadRenderer HorizontalScroll > * { width: auto; } + + ThreadRenderer .hdr-row { height: auto; } + ThreadRenderer #thread-id-bar { + height: auto; + margin-bottom: 1; + background: $panel; + } + ThreadRenderer #thread-id-bar > .thread-id-label { width: 1fr; padding: 0 1; } """ BINDINGS = [ @@ -122,12 +180,14 @@ def __init__( self, timeline: list[tuple[TimelineItem, str | None]], *, + thread_id: str | None = None, descendable_tool_call_ids: set[str] | None = None, on_tool_descend: Callable[[str], Awaitable[None]] | None = None, **kwargs, ) -> None: super().__init__(**kwargs) self._timeline = timeline + self._lg_thread_id = thread_id self._descendable = descendable_tool_call_ids or set() self._on_tool_descend = on_tool_descend @@ -143,6 +203,19 @@ def set_timeline(self, timeline: list[tuple[TimelineItem, str | None]]) -> None: def _render_all(self) -> list: widgets: list = [] + if self._lg_thread_id: + widgets.append( + Horizontal( + Static( + Text(f"thread: {self._lg_thread_id}", style="bold"), + classes="thread-id-label", + ), + CopyButton(self._lg_thread_id, what="thread id"), + id="thread-id-bar", + classes="hdr-row", + ) + ) + # Pair tool results to calls by tool_call_id. Ids are unique across # summary epochs so pairing across them is fine. tool_results: dict[str, ToolMessage] = {} @@ -151,7 +224,7 @@ def _render_all(self) -> list: tool_results[item.tool_call_id] = item turn = 0 - for idx, (item, _ckpt_id) in enumerate(self._timeline): + for idx, (item, ckpt_id) in enumerate(self._timeline): match item: case SummarizationMarker(): widgets.append(self._render_summarization(item, idx)) @@ -161,7 +234,7 @@ def _render_all(self) -> list: widgets.append(self._render_human(item, idx)) case AIMessage(): turn += 1 - widgets.extend(self._render_turn(item, idx, turn, tool_results)) + widgets.extend(self._render_turn(item, idx, turn, ckpt_id, tool_results)) case ToolMessage(): pass # rendered inline with its AI message case _: @@ -204,6 +277,7 @@ def _render_turn( msg: AIMessage, idx: int, turn: int, + ckpt_id: str | None, tool_results: dict[str, ToolMessage], ) -> list: widgets: list = [] @@ -229,7 +303,17 @@ def _render_turn( if n_tool_calls: header.append(f" {n_tool_calls} tool call(s)", style="dim") header.append(usage_str, style="dim") - widgets.append(Static(header, classes="turn-header")) + header_widget = Static(header, classes="turn-header") + if ckpt_id is not None: + widgets.append( + Horizontal( + header_widget, + CopyButton(ckpt_id, what="checkpoint id"), + classes="hdr-row", + ) + ) + else: + widgets.append(header_widget) for block in blocks: match block["type"]: @@ -264,7 +348,7 @@ def _render_turn( if descendable: assert self._on_tool_descend is not None coll: Collapsible = DescendableToolCall( - Static(Syntax(args_str, "json", theme="monokai")), + _wide(Static(Syntax(args_str, "json", theme="monokai"))), title=call_title, collapsed=True, classes="tool-call", @@ -273,7 +357,7 @@ def _render_turn( ) else: coll = Collapsible( - Static(Syntax(args_str, "json", theme="monokai")), + _wide(Static(Syntax(args_str, "json", theme="monokai"))), title=call_title, collapsed=True, classes="tool-call", @@ -290,7 +374,7 @@ def _render_turn( result_title += f" [{status}]" result_title += f": {preview}" widgets.append(Collapsible( - Static(content, markup=False), + _wide(Static(content, markup=False)), title=result_title, collapsed=True, classes="tool-result", From 63908db4e45c15ad7cc09360fc540023abcd587b Mon Sep 17 00:00:00 2001 From: John Toman Date: Thu, 23 Jul 2026 09:52:29 -0700 Subject: [PATCH 2/8] Judge prompt improvements --- .github/workflows/integration-tests.yml | 2 +- .github/workflows/pytest.yml | 2 +- composer/cli/diagnostics/ap_trail_view.py | 5 ++ composer/templates/loader.py | 12 ++-- composer/templates/property_judge_prompt.j2 | 65 +++++++++++---------- composer/ui/clipboard.py | 35 +++++++++++ 6 files changed, 85 insertions(+), 36 deletions(-) create mode 100644 composer/ui/clipboard.py diff --git a/.github/workflows/integration-tests.yml b/.github/workflows/integration-tests.yml index 1afdf305..771abdd0 100644 --- a/.github/workflows/integration-tests.yml +++ b/.github/workflows/integration-tests.yml @@ -57,7 +57,7 @@ jobs: - name: run autoprover integration tests run: | - uv run pytest -n 3 -m 'expensive' tests + COMPOSER_STRICT_TEMPLATES=1 uv run pytest -n 3 -m 'expensive' tests env: CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/.github/workflows/pytest.yml b/.github/workflows/pytest.yml index 184f7c25..c0987e86 100644 --- a/.github/workflows/pytest.yml +++ b/.github/workflows/pytest.yml @@ -27,4 +27,4 @@ jobs: - name: Run pytest run: | - uv run pytest -m 'not expensive' tests/ + COMPOSER_STRICT_TEMPLATES=1 uv run pytest -m 'not expensive' tests/ diff --git a/composer/cli/diagnostics/ap_trail_view.py b/composer/cli/diagnostics/ap_trail_view.py index 2794a037..e3b622f4 100644 --- a/composer/cli/diagnostics/ap_trail_view.py +++ b/composer/cli/diagnostics/ap_trail_view.py @@ -179,7 +179,10 @@ def __init__(self, source: RunSource) -> None: self._expanded: set[str] = set() # from_tool_id -> [ThreadMeta] index (one-time pass over run's ThreadMeta) self._by_from_tool: dict[str, list[tuple[str, ThreadMeta]]] = defaultdict(list) + # thread_run_id -> ThreadMeta, for O(1) lookup when mounting a renderer. + self._meta_by_run_id: dict[str, ThreadMeta] = {} for tid, meta in source.threads: + self._meta_by_run_id[tid] = meta ft = meta.get("from_tool_id") if ft is not None: self._by_from_tool[ft].append((tid, meta)) @@ -274,8 +277,10 @@ async def _show_in_right_pane(self, thread_run_id: str) -> None: switcher = self.query_one("#switcher", ContentSwitcher) if thread_run_id not in self._mounted_renderers: cache = await self._get_thread_cache(thread_run_id) + meta = self._meta_by_run_id.get(thread_run_id) renderer = ThreadRenderer( cache.timeline, + thread_id=meta.get("thread_id") if meta is not None else None, descendable_tool_call_ids=cache.descendable_tool_call_ids, on_tool_descend=self._descend_to_child, id=f"r_{thread_run_id}", diff --git a/composer/templates/loader.py b/composer/templates/loader.py index d9708d7e..ce42793c 100644 --- a/composer/templates/loader.py +++ b/composer/templates/loader.py @@ -1,17 +1,21 @@ -from typing import Any -from jinja2 import Environment, FileSystemLoader +from typing import Any, TypedDict, NotRequired +from jinja2 import Environment, FileSystemLoader, StrictUndefined, Undefined import pathlib +import os script_dir = pathlib.Path(__file__).parent +class _UndefinedParams(TypedDict): + undefined: NotRequired[type[Undefined]] + +_test_mode_undefined : _UndefinedParams = { "undefined": StrictUndefined } if os.environ.get("COMPOSER_STRICT_TEMPLATES") is not None else {} def _autoescape(template_name: str | None) -> bool: # HTML templates (``*.html.j2``) must autoescape interpolated values; prompt templates # (plain ``.j2``) stay verbatim — escaping would corrupt their contents. return template_name is not None and template_name.endswith(".html.j2") - -env = Environment(loader=FileSystemLoader(script_dir), autoescape=_autoescape) +env = Environment(loader=FileSystemLoader(script_dir), autoescape=_autoescape, **_test_mode_undefined) def load_jinja_template(template_name: str, **kwargs: Any) -> str: """Load and render a Jinja template from the script directory""" diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 9a5b9df5..b60a8a2c 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -204,29 +204,25 @@ against a *contract* output is the cure, not the defect. Verify that the specification covers all {{ properties | length }} listed properties. For each property: - If the spec contains rules/invariants addressing it: evaluate those rules under criteria 1-7. -- If the spec does NOT address a property AND the author has NOT declared a skip for it: reject the spec and flag the missing property. -- If the author declared a skip for a property: critically evaluate the justification. If the property IS expressible in CVL - (e.g., using ghost state, invariants, or other CVL features), reject the skip and explain how it can be formalized. - Only accept a skip if the property is genuinely beyond CVL's expressiveness *as confirmed - by your own empirical research* or provided CVL-Document-Ref citations. Do *NOT* accept - accept an author's claims that a property is beyond CVL's expressiveness at face value, - nor should you make your *own* assumptions about CVL expressibility: - you MUST perform your own research (or examine any CVL Document references cited in their skip) - and critically examine their claims about CVL expressivity when evaluating the skip. - - *Exception*: if the author has filed an empirical rebuttal (see Step 1) against a prior-round - formalization you proposed, accept that rebuttal per the Step 1 evaluation rules — do not - re-insist on the same proposal. If the rebuttal establishes that no working formalization was - found, the skip is VALID on the grounds that your prior proposal proved unworkable. -{% if sort != "greenfield" %} - If the property being skipped could be formalized with Solidity code changes, the skip is VALID. Do *NOT* reject - skips with advice to change the Solidity code. The Solidity code is *IMMUTABLE* and suggestions to change the Solidity - code are INVALID. -{% endif %} +- If the spec neither addresses the property NOR carries an author skip: reject the spec and flag the missing property. +- If the author declared a skip: evaluate it by the rules below. + +#### Evaluating a skip -Do NOT "wave through" skip reasons because they sound plausible or confidently assert uncited -facts about CVL or the prover behavior. Further, do not accept as a skip justification -citations of limitations of their own authored CVL, i.e., +A spuriously skipped property is just as, if not more, fatal than a poorly written one. Each skipped property introduces a potential +gap in the verification of the program which potentially lets bugs or other undesirable behavior appear in "verified" code. +Accordingly, the reasons provided for a skip must be subject to intense scrutiny. The level of scrutiny you must apply depends +on the grounds cited in the reason. First identify which the author is claiming: + +**Ground A — CVL cannot express it.** The claim is that CVL lacks the expressive power to state or observe the property: +it cannot access some storage, cannot quantify over some structure, has no construct for the needed observation, and so on. +This class is *checkable*, and is where the author is most likely to invent claims; a confident, technical-sounding statement of +something being impossibile in CVL or "beyond the prover" should never be taken on faith. +Verify the *specific* claim before accepting the skip: search the manual / use `cvl_researcher`, or read any CVL-Document-Ref the author cited. +Accept only if your own research or the provided citations confirms the limitation; otherwise reject and name the construct that expresses it +(ghost state, direct storage access, hooks, an invariant, a CVL function, bounded element-wise logic, ...). + +Further, do not accept a skip from the author that cites of limitations of their own authored CVL, i.e., reject a reason that explains their chosen summarization/hook/ghost strategy doesn't admit verifying the skipped property. The author has *full control* over the *entire* CVL file you are reviewing, including the summaries, hooks, ghosts, cvl functions, etc. @@ -234,15 +230,24 @@ If the summarization/hook/ghost strategy they chose makes the desired property impossible to verify, but an alternative strategy could, reject the skip with advice on how to adjust the strategy. +**Ground B — the prover cannot discharge it.** + +The claim is that CVL expresses the property fine, but the *prover* cannot prove it in practice: timeouts, non-linear arithmetic, path explosion, non-termination, unknown error in the prover. +This skip ground rests on run experience of the author you do not have; +accept it on that basis (the same evidentiary logic as an empirical rebuttal in Step 1). +Ideally the reason points at the concrete obstacle observed (which computation blew up, where it diverged). + +{% if sort != "greenfield" %} +**Ground C — it would require Solidity changes.** The Solidity code is *IMMUTABLE*. If the only way to formalize the property is to change the source (harnesses included), the skip is VALID. Never reject a skip with advice to change the code. +{% endif %} + +*Prior-round exception (Ground A):* if the author filed an empirical rebuttal (Step 1) showing a formalization *you* proposed does not work, either search for another plausible +solution or accept the skip on the grounds that your proposal proved unworkable. + +#### The unbounded-array limitation (a specific Ground A) -**Array quantification limitation**: The Certora Prover cannot universally quantify over -dynamic-length arrays. Properties that reason about all elements of an array can only be -verified by explicitly bounding the array size and adding element-wise logic for each case. -This means: -- Rules that `require` a bounded array size (e.g., `require arr.length <= 3`) and verify - element-wise are a *valid* approach — do not reject them for overconstrained inputs. -- If a property fundamentally requires reasoning over arbitrary-length arrays with no - feasible bound, accept a skip citing this limitation. +The prover cannot universally quantify over dynamic-length arrays, so a property that must reason about *all* elements of an arbitrary-length array with no feasible size bound is a valid Ground-A skip. Two scoping caveats: +- Bounding the array (`require arr.length <= 3`) and verifying element-wise is a *valid formalization*, not an over-constraint — do not reject it under Criteria 4, and its availability defeats the skip whenever a bound is feasible. When formulating your feedback, be sure to consider any feedback you gave previously. diff --git a/composer/ui/clipboard.py b/composer/ui/clipboard.py new file mode 100644 index 00000000..b46aad13 --- /dev/null +++ b/composer/ui/clipboard.py @@ -0,0 +1,35 @@ +"""Copy text to the system clipboard by shelling out to a platform tool. + +OSC 52 is deliberately avoided: it doesn't work under VTE-based terminals, so +instead we invoke whatever clipboard CLI is on ``PATH``. Preference order is +Wayland (``wl-copy``), then X11 (``xclip`` / ``xsel``), then macOS (``pbcopy``). +""" + +import shutil +import subprocess + +# Each entry is the argv used to write stdin to the clipboard; the first whose +# binary is on PATH and exits cleanly wins. +_CANDIDATES: list[list[str]] = [ + ["wl-copy"], + ["xclip", "-selection", "clipboard"], + ["xsel", "--clipboard", "--input"], + ["pbcopy"], +] + + +def copy_to_clipboard(text: str) -> bool: + """Best-effort copy of *text* to the system clipboard. + + Returns ``True`` once a clipboard tool accepts the text, ``False`` if none + is available or all of them fail. + """ + for cmd in _CANDIDATES: + if shutil.which(cmd[0]) is None: + continue + try: + subprocess.run(cmd, input=text.encode(), check=True) + return True + except Exception: + continue + return False From af9bf1d2d25be7cee89b3fde98a729f012bc6dfc Mon Sep 17 00:00:00 2001 From: John Toman Date: Thu, 23 Jul 2026 16:39:17 -0700 Subject: [PATCH 3/8] phew --- composer/cli/natspec_startup.py | 13 +- composer/meta/__init__.py | 3 + composer/meta/resolver.py | 13 ++ composer/meta/templates.py | 100 +++++++++++++ composer/meta/types.py | 12 ++ composer/scripts/template_manifest.py | 41 ++++++ composer/spec/feedback.py | 45 +++--- composer/spec/gen_types.py | 56 +++++--- composer/spec/natspec/author.py | 2 +- composer/spec/natspec/interface_gen.py | 2 +- composer/spec/natspec/stub_gen.py | 2 +- composer/spec/natspec/task_description.py | 4 +- composer/spec/source/author.py | 2 +- composer/spec/source/report/render.py | 6 +- composer/spec/source/struct_invariant.py | 4 +- composer/spec/system_model.py | 3 +- .../templates/application_context_macro.j2 | 8 +- composer/templates/application_context_new.j2 | 6 +- composer/templates/autoprove_report.html.j2 | 8 +- composer/templates/property_judge_prompt.j2 | 21 +++ tests/test_fuzzed_templates.py | 112 +++++++++++++++ tests/test_template_manifest.py | 133 ++++++++++++++++++ 22 files changed, 521 insertions(+), 75 deletions(-) create mode 100644 composer/meta/__init__.py create mode 100644 composer/meta/resolver.py create mode 100644 composer/meta/templates.py create mode 100644 composer/meta/types.py create mode 100644 composer/scripts/template_manifest.py create mode 100644 tests/test_fuzzed_templates.py create mode 100644 tests/test_template_manifest.py diff --git a/composer/cli/natspec_startup.py b/composer/cli/natspec_startup.py index 8f89cc2e..d2db6169 100644 --- a/composer/cli/natspec_startup.py +++ b/composer/cli/natspec_startup.py @@ -1,11 +1,11 @@ import pathlib -from typing import Any, TypedDict +from typing import TypedDict from langchain_core.tools import BaseTool from graphcore.tools.vfs import DirBackend, FSBackend, Materializer, fs_tools_layered -from composer.spec.gen_types import TypedTemplate +from composer.spec.gen_types import PartialTemplate from composer.spec.system_model import Application, FromSourceApplication from composer.spec.natspec.models import ( InterfaceResult, @@ -19,9 +19,8 @@ class PathChoosingConf(TypedDict): agent_chooses_path: bool -_InterfaceTemplate = TypedTemplate[PathChoosingConf]("interface_generation_prompt.j2") -_StubTemplate = TypedTemplate[PathChoosingConf]("stub_generation_prompt.j2") - +_InterfaceTemplate = PartialTemplate[PathChoosingConf, InterfaceGenCallParams]("interface_generation_prompt.j2") +_StubTemplate = PartialTemplate[PathChoosingConf, StubGenCallParams]("stub_generation_prompt.j2") def build_mental_model( *, @@ -34,10 +33,10 @@ def build_mental_model( agent_chooses_path = source_root is not None interface_prompt = _InterfaceTemplate.bind( {"agent_chooses_path": agent_chooses_path} - ).depends(InterfaceGenCallParams) + ) stub_prompt = _StubTemplate.bind( {"agent_chooses_path": agent_chooses_path} - ).depends(StubGenCallParams) + ) if source_root is not None: return MentalModel( diff --git a/composer/meta/__init__.py b/composer/meta/__init__.py new file mode 100644 index 00000000..6ad7b1ae --- /dev/null +++ b/composer/meta/__init__.py @@ -0,0 +1,3 @@ +""" +Module for introspection of the composer module. Stay away +""" \ No newline at end of file diff --git a/composer/meta/resolver.py b/composer/meta/resolver.py new file mode 100644 index 00000000..dd258bfa --- /dev/null +++ b/composer/meta/resolver.py @@ -0,0 +1,13 @@ +from typing import Iterable, get_args +import sys +import importlib +from .types import TemplateDecl + +def resolve_params(s: TemplateDecl) -> Iterable[type]: + importlib.import_module(s.module) + t = sys.modules[s.module].__dict__[s.qualname] + + res = getattr(t, "__orig_class__") + for i in get_args(res): + assert isinstance(i, type), f"got {i} {type(i)}" + yield i diff --git a/composer/meta/templates.py b/composer/meta/templates.py new file mode 100644 index 00000000..433d7ee0 --- /dev/null +++ b/composer/meta/templates.py @@ -0,0 +1,100 @@ +import ast +import pathlib + +from composer.meta.types import TemplateSort, TemplateDecl + +PACKAGE = "composer" +FULL_TYPE_NAME = "TypedTemplate" +PARTIAL_NAME = "PartialTemplate" +TEMPLATE_ARG = 0 + +TYPE_NAMES = (FULL_TYPE_NAME, PARTIAL_NAME) + +def _names_type(node: ast.expr) -> TemplateSort | None: + """True if `node` textually refers to TYPE_NAME: bare, attribute, or subscripted.""" + if isinstance(node, ast.Name): + if node.id in TYPE_NAMES: + return node.id + if isinstance(node, ast.Attribute): + if node.attr in TYPE_NAMES: + return node.attr + if isinstance(node, ast.Subscript): # TYPE_NAME[...] generic annotation + return _names_type(node.value) + return None + +def _extract_template(value: ast.expr | None) -> str | None: + """Pull the template-name argument (positional or kwarg per TEMPLATE_ARG).""" + if not isinstance(value, ast.Call): + return None + arg = value.args[TEMPLATE_ARG] if len(value.args) > TEMPLATE_ARG else None + if arg is None: + return None + if isinstance(arg, ast.Constant) and isinstance(arg.value, str): + return arg.value + raise ValueError( + f"template argument must be a string literal so the static " + f"scanner can see it (got {ast.dump(arg)[:60]})" + ) + +def _match_statement(stmt: ast.stmt) -> tuple[str, TemplateSort, ast.expr | None] | None: + """Return (variable_name, value_expr_or_None) if `stmt` declares a TYPE_NAME.""" + if isinstance(stmt, ast.AnnAssign): + if (ty_name := _names_type(stmt.annotation)) is not None and isinstance(stmt.target, ast.Name): + return stmt.target.id, ty_name, stmt.value + return None + if isinstance(stmt, ast.Assign): + if (isinstance(stmt.value, ast.Call) and (ty_sort := _names_type(stmt.value.func)) is not None + and len(stmt.targets) == 1 and isinstance(stmt.targets[0], ast.Name)): + return stmt.targets[0].id, ty_sort, stmt.value + return None + +def iter_declarations(package_dir: pathlib.Path, skips: tuple[pathlib.Path, ...]): + """Yield (module_name, var_name, template_or_None) for each top-level declaration. + + Purely textual/AST -- aliased type names (``from registry import + TemplateDecl as TD``) or declarations built in loops will NOT be found. + Keep declaration style boring. + """ + base = package_dir.parent + for py in sorted(package_dir.rglob("*.py")): + if any(py.is_relative_to(skip) for skip in skips): + continue + source = py.read_text(encoding="utf-8") + if FULL_TYPE_NAME not in source and PARTIAL_NAME not in source: # cheap pre-filter before parsing + continue + tree = ast.parse(source, filename=str(py)) + module_name = ".".join(py.relative_to(base).with_suffix("").parts) + + if module_name.endswith(".__init__"): + module_name = module_name.removesuffix(".__init__") + for stmt in tree.body: # top level ONLY -- no ast.walk on purpose + match = _match_statement(stmt) + if match is None: + continue + var_name, ty_sort, value = match + try: + template = _extract_template(value) + except ValueError as exc: + raise ValueError(f"{py}:{stmt.lineno}: {exc}") from None + yield module_name, var_name, template, ty_sort + +def build_manifest(root_package: pathlib.Path, skips: tuple[pathlib.Path, ...]) -> dict[str, TemplateDecl]: + """Scan and return {"module:VAR": {"module", "qualname", "template"?}}.""" + manifest: dict[str, TemplateDecl] = {} + templates_seen: dict[str, str] = {} + for module_name, var_name, template, ty_sort in iter_declarations(root_package, skips): + key = f"{module_name}:{var_name}" + if key in manifest: + raise ValueError(f"{key} declared twice at module top level") + if template is None: + raise ValueError(f"No template name extracted for {key}") + if template in templates_seen: + raise ValueError( + f"template {template!r} declared by both " + f"{templates_seen[template]} and {key}" + ) + templates_seen[template] = key + manifest[key] = TemplateDecl( + qualname=var_name, module=module_name, ty_sort=ty_sort, template_name=template + ) + return manifest diff --git a/composer/meta/types.py b/composer/meta/types.py new file mode 100644 index 00000000..a1572fee --- /dev/null +++ b/composer/meta/types.py @@ -0,0 +1,12 @@ +from typing import Literal +from pydantic import BaseModel, TypeAdapter + +type TemplateSort = Literal["TypedTemplate", "PartialTemplate"] + +class TemplateDecl(BaseModel): + module: str + qualname: str + template_name: str + ty_sort: TemplateSort + +Manifest = TypeAdapter(dict[str, TemplateDecl]) diff --git a/composer/scripts/template_manifest.py b/composer/scripts/template_manifest.py new file mode 100644 index 00000000..eda1a824 --- /dev/null +++ b/composer/scripts/template_manifest.py @@ -0,0 +1,41 @@ +import importlib.util +import pathlib +import sys + +from composer.meta.types import TemplateDecl, Manifest +from composer.meta.templates import build_manifest + +# -------------------------------------------------------------------------- +# STUBS -- fill these in for your repo +# -------------------------------------------------------------------------- +PACKAGE = "composer" + +_THIS_DIR = pathlib.Path(__file__).parent + +def _package_root() -> pathlib.Path: + """Locate PACKAGE on disk without importing it. + + find_spec on a *top-level* name only consults path finders; the module is + never executed. (Dotted names would import parents -- don't pass those.) + """ + spec = importlib.util.find_spec(PACKAGE) + if spec is None or not spec.submodule_search_locations: + raise SystemExit(f"cannot locate package {PACKAGE!r} on sys.path") + to_ret = pathlib.Path(next(iter(spec.submodule_search_locations))) + assert pathlib.Path(__file__).is_relative_to(to_ret) + return to_ret + +def _repo_root() -> pathlib.Path: + return _package_root().parent + +def render_manifest(manifest: dict[str, TemplateDecl]) -> str: + """Canonical, diff-stable serialization (sorted keys, trailing newline).""" + return Manifest.dump_json(manifest, indent=2).decode("utf-8") + +def _main(): + (_repo_root() / "template_manifest.json").write_text( + render_manifest(build_manifest(_package_root(), (_THIS_DIR,))) + ) + +if __name__ == "__main__": + sys.exit(_main()) diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index 1aceda7a..5fd1d0f6 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -17,7 +17,7 @@ from composer.spec.graph_builder import bind_standard, run_to_completion from composer.cvl.tools import get_cvl from composer.tools.thinking import RoughDraftState, get_rough_draft_tools -from composer.spec.gen_types import TemplateInstantiation, InjectedTemplate, TypedTemplate +from composer.spec.gen_types import TemplateInstantiation, TypedTemplate, ITypedTemplate, PartialTemplate from composer.spec.cvl_generation import FeedbackToolContext, Rebuttal, SkippedProperty from composer.spec.system_model import ContractComponentInstance from composer.spec.util import uniq_thread_id @@ -32,6 +32,10 @@ class PropertyFeedback(BaseModel): class Properties(TypedDict): properties: list[PropertyFormulation] +class FeedbackInputs(Properties): + rebuttals: Sequence[Rebuttal] + skipped: Sequence[SkippedProperty] + class FeedbackInherentParams(TypedDict): context: ContractComponentInstance | None # Matches the tri-state on the env-level ``sort``: @@ -42,7 +46,7 @@ class FeedbackInherentParams(TypedDict): # has real immutable source. sort: Sort -FeedbackTemplate = TypedTemplate[FeedbackInherentParams]("property_judge_prompt.j2") +FeedbackTemplate = PartialTemplate[FeedbackInherentParams, FeedbackInputs]("property_judge_prompt.j2") class JudgeSystemParams(TypedDict): sort: Sort @@ -56,7 +60,7 @@ class JudgeSystemParams(TypedDict): def property_feedback_judge( ctx: WorkflowContext[CVLJudge], env: ServiceHost, - prompt: InjectedTemplate[Properties] | TemplateInstantiation, + prompt: ITypedTemplate[FeedbackInputs], props: list[PropertyFormulation], *, extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None, @@ -88,17 +92,13 @@ def did_rough_draft_read(s: ST, _) -> str | None: mem = ctx.get_memory_tool() - final_prompt = prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props}) - - workflow = bind_standard( + staged_workflow = bind_standard( builder, ST, validator=did_rough_draft_read ).with_input( SpecJudgeInput - ).inject( - lambda b: final_prompt.render_to(b.with_initial_prompt_template) ).inject( lambda g: system_prompt.render_to(g.with_sys_prompt_template) - ).with_tools([*rough_draft_tools, mem, get_cvl(ST), ]).compile_async() + ).with_tools([*rough_draft_tools, mem, get_cvl(ST), ]) async def the_tool( cvl: str, @@ -106,6 +106,14 @@ async def the_tool( rebuttals: Sequence[Rebuttal], within_tool: str, ) -> PropertyFeedback: + workflow = staged_workflow.inject( + lambda b: prompt.bind({ + "properties": props, + "rebuttals": rebuttals, + "skipped": skipped + }).render_to(b.with_initial_prompt_template) + ).compile_async() + input_parts: list[str | dict] = [] if extra_inputs: if isinstance(extra_inputs, list): @@ -115,25 +123,6 @@ async def the_tool( input_parts.append("The proposed CVL file is") input_parts.append(cvl) - if skipped: - input_parts.append("The following properties were explicitly skipped by the author:") - for s in skipped: - input_parts.append(f" Property {s.property_title}: {s.reason}") - if rebuttals: - input_parts.append( - "The author has filed the following rebuttals against feedback from " - "prior rounds. Evaluate each per the Step 1 rebuttal rule (and the " - "Criteria 7 exception for skip-related rebuttals). Empirical evidence " - "types (`typecheck_failure`, `counterexample`, `manual_citation`) " - "carry near-binding weight; `reasoned` rebuttals are a conversation, " - "not a veto." - ) - for i, r in enumerate(rebuttals, 1): - input_parts.append( - f" Rebuttal {i} [{r.evidence_type}]\n" - f" Addressing: {r.prior_feedback_reference}\n" - f" Evidence: {r.evidence}" - ) res = await run_to_completion( workflow, SpecJudgeInput(input=input_parts, curr_spec=cvl, memory=None, did_read=False), diff --git a/composer/spec/gen_types.py b/composer/spec/gen_types.py index bf27022a..873573a5 100644 --- a/composer/spec/gen_types.py +++ b/composer/spec/gen_types.py @@ -1,7 +1,7 @@ from dataclasses import dataclass from pathlib import Path, PurePosixPath -from typing import Literal, Mapping, Any, Protocol +from typing import Literal, Mapping, Any, Protocol, final from pydantic import BaseModel, Field @@ -98,6 +98,11 @@ class CVLResource(BaseModel): description: str = Field(description="A description of this resource") sort: Literal["import"] +class ITypedTemplate[T: Mapping[str, Any]](Protocol): + def bind(self, params: T) -> "TemplateInstantiation": + ... + +@final class TypedTemplate[T: Mapping[str, Any]]: def __init__(self, name: str): self._wrapped = name @@ -112,9 +117,40 @@ class TemplateRenderer[T](Protocol): def __call__(self, template: str, /, **kwargs) -> T: ... +@final +@dataclass +class _StagedTemplate[T: Mapping[str, Any]]: + _wrapped: str + _staged_params: dict + + def __str__(self) -> str: + return self._wrapped + + def bind(self, params: T) -> "TemplateInstantiation": + return TemplateInstantiation( + template=self, + args = { + **self._staged_params, + **params + } + ) + +@dataclass +class PartialTemplate[T: Mapping[str, Any], U: Mapping[str, Any]]: + def __init__(self, name: str): + self._wrapped = name + + def __str__(self) -> str: + return self._wrapped + + def bind(self, params: T) -> ITypedTemplate[U]: + return _StagedTemplate(self._wrapped, { **params }) + +type _TemplateName = TypedTemplate | _StagedTemplate + @dataclass class TemplateInstantiation: - template: TypedTemplate + template: _TemplateName args: dict @staticmethod @@ -133,19 +169,3 @@ def render_to[T]( str(self.template), **self.args ) - - def depends[X: Mapping[str, Any]](self, other: type[X]) -> "InjectedTemplate[X]": - return InjectedTemplate(self) - -@dataclass -class InjectedTemplate[X: Mapping[str, Any]]: - wrapped: TemplateInstantiation - - def inject(self, injected: X) -> TemplateInstantiation: - return TemplateInstantiation( - TypedTemplate(str(self.wrapped.template)), - { - **self.wrapped.args, - **injected - } - ) diff --git a/composer/spec/natspec/author.py b/composer/spec/natspec/author.py index bf41076c..f8efb0c8 100644 --- a/composer/spec/natspec/author.py +++ b/composer/spec/natspec/author.py @@ -223,7 +223,7 @@ def stub_feedback_extras() -> list[str | dict]: ctx=ctx.child(CVL_JUDGE_KEY), env=env, prompt=FeedbackTemplate.bind({ "context": component, "sort": env.sort, - }).depends(Properties), props=props, extra_inputs=stub_feedback_extras + }), props=props, extra_inputs=stub_feedback_extras ) g = ( diff --git a/composer/spec/natspec/interface_gen.py b/composer/spec/natspec/interface_gen.py index 964f3248..62dc6f4e 100644 --- a/composer/spec/natspec/interface_gen.py +++ b/composer/spec/natspec/interface_gen.py @@ -133,7 +133,7 @@ async def validate_result(self, res: InterfaceResult[I]) -> str | None: c for c in summary.contract_components if c.solidity_identifier not in external_contracts ] - final_prompt = description.prompt.inject( + final_prompt = description.prompt.bind( InterfaceGenCallParams( summary=summary, target_contracts=target_contracts, diff --git a/composer/spec/natspec/stub_gen.py b/composer/spec/natspec/stub_gen.py index 1a4bd8d2..caba8963 100644 --- a/composer/spec/natspec/stub_gen.py +++ b/composer/spec/natspec/stub_gen.py @@ -126,7 +126,7 @@ async def validate_result(self, res: S) -> str | None: ) return None - final_prompt = description.prompt.inject( + final_prompt = description.prompt.bind( StubGenCallParams( solidity_identifier=solidity_identifier, interface_name=interface_name, diff --git a/composer/spec/natspec/task_description.py b/composer/spec/natspec/task_description.py index 0bbb0c28..ffc4e3ab 100644 --- a/composer/spec/natspec/task_description.py +++ b/composer/spec/natspec/task_description.py @@ -5,7 +5,7 @@ from dataclasses import dataclass, field from typing import Any, AsyncContextManager, Awaitable, ContextManager, Iterator, Mapping, Self, TypedDict -from composer.spec.gen_types import InjectedTemplate +from composer.spec.gen_types import ITypedTemplate from composer.spec.natspec.models import ( InterfaceDeclModel, InterfaceResult, @@ -76,7 +76,7 @@ class AgentDescription[T, X: Mapping[str, Any]]: (e.g. current stubs) at agent-dispatch time. """ output_ty: type[T] - prompt: InjectedTemplate[X] + prompt: ITypedTemplate[X] extra_input: list[str | dict | ExtraInputProducer] = field(default_factory=list) diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index 096437b8..c8d34b2a 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -392,7 +392,7 @@ async def batch_cvl_generation( ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({ "sort": "existing", "context": component, - }).depends(Properties), props + }), props ) res_state = await run_cvl_generator( diff --git a/composer/spec/source/report/render.py b/composer/spec/source/report/render.py index 25986c51..c41fa992 100644 --- a/composer/spec/source/report/render.py +++ b/composer/spec/source/report/render.py @@ -136,7 +136,8 @@ class GroupView(TypedDict): class ReportTemplateParams(TypedDict): """The full, typed context of ``autoprove_report.html.j2``.""" - report: AutoProverReport + contract_name: str + run_timestamp_utc: str | None coverage: CoverageReport terms: ReportTerms has_links: bool @@ -233,7 +234,8 @@ def _build_context(report: AutoProverReport) -> ReportTemplateParams: unit_labels = _OUTCOME_LABELS[report.backend] group_labels = _GROUP_LABELS[report.backend] return { - "report": report, + "contract_name": report.contract_name, + "run_timestamp_utc": report.run_timestamp_utc, "coverage": report.coverage, "terms": _TERMS[report.backend], # The link column / runs header only make sense when a backend actually produced run links. diff --git a/composer/spec/source/struct_invariant.py b/composer/spec/source/struct_invariant.py index 630286cd..bf4742e2 100644 --- a/composer/spec/source/struct_invariant.py +++ b/composer/spec/source/struct_invariant.py @@ -22,7 +22,7 @@ from composer.tools.thinking import RoughDraftState, get_rough_draft_tools from composer.spec.graph_builder import bind_standard, run_to_completion -from composer.spec.context import WorkflowContext, SourceCode, CacheKey, InvJudge +from composer.spec.context import WorkflowContext, SourceFields, SourceCode, CacheKey, InvJudge from composer.spec.service_host import ServiceHost from composer.spec.system_model import HarnessedApplication from composer.spec.gen_types import TypedTemplate @@ -79,7 +79,7 @@ def _merge_invariant_feedback( class InvariantParams(TypedDict): context: HarnessedApplication - contract_spec: SourceCode + contract_spec: SourceFields _typed_invariant_prompt = TypedTemplate[InvariantParams]("structural_invariant_prompt.j2") diff --git a/composer/spec/system_model.py b/composer/spec/system_model.py index 7bdb4059..5a598cee 100644 --- a/composer/spec/system_model.py +++ b/composer/spec/system_model.py @@ -1,5 +1,6 @@ from dataclasses import dataclass -from typing import Literal +from typing import Literal, Generic +from typing_extensions import TypeVar from pydantic import BaseModel, Field from functools import cached_property from composer.spec.util import slugify_filename diff --git a/composer/templates/application_context_macro.j2 b/composer/templates/application_context_macro.j2 index d704839a..3782eea2 100644 --- a/composer/templates/application_context_macro.j2 +++ b/composer/templates/application_context_macro.j2 @@ -16,11 +16,11 @@ This application is comprised of the following components. ## Components {% for c in context.components %} -### {{ "Contract" if c.sort else "External Actor"}}: {% if c.sort %}{{ contract_label(c) }}{% else %}{{ c.name }}{% endif %} +### {{ "Contract" if c.sort is defined else "External Actor"}}: {% if c.sort is defined %}{{ contract_label(c) }}{% else %}{{ c.name }}{% endif %} **Description**: {{ c.description }} -{% if c.sort %} +{% if c.sort is defined %} {% if show_sort %} **Sort**: {{ c.sort }} (see below) {% endif %} @@ -33,10 +33,10 @@ This contract is comprised of the following components: **Component Name**: {{ sub.name }} **Description**: {{ sub.description }} -{% if sub.interactions %} +{% if sub.interactions is defined %} This component interacts with other components in the application or external actors as follows: {% for int in sub.interactions %} -{% if int.contract_name %} +{% if int.contract_name is defined %} * Interaction with component `{{ int.component }}` of `{{ int.contract_name }}`: {{ int.description }} {%else%} * Interaction with external actor {{ int.external_actor }}: {{ int.description }} diff --git a/composer/templates/application_context_new.j2 b/composer/templates/application_context_new.j2 index 050ca6c0..8bcda175 100644 --- a/composer/templates/application_context_new.j2 +++ b/composer/templates/application_context_new.j2 @@ -18,7 +18,7 @@ described as {{ context.app.application_type }}. The other contracts in the application are: {% for other in context.ommer_contracts %} * The {{ contract_label(other) }} contract, described as {{ other.description }}. The contract's sort is {{ other.sort }}. -{%- if sort == "update" %} +{%- if sort is defined and sort == "update" %} Its status in the source tree is `{{ other.tag }}`{% if other.tag in ("unchanged", "edited") %} (source located at `{{ other.path }}`){% endif %}. {%- endif %} {% endfor %} @@ -28,7 +28,7 @@ The sort of a contract means the following: - `dynamic`: One of the other explicit contracts will dynamically create instances of this contract during execution - `multiple`: Multiple instances of this contract will be created, but by some external actor during execution or as part of deployment. -{% if sort == "update" %} +{% if sort is defined and sort == "update" %} The status/tag of a contract in the source tree means the following: - `unchanged`: The contract is already present in the existing source tree and the design does not @@ -43,7 +43,7 @@ The status/tag of a contract in the source tree means the following: {% if context.component.interactions %} This component interacts with other parts of the application/external actors: {% for other in context.component.interactions %} - {% if other.contract_name %} + {% if other.contract_name is defined %} - The {{ other.component }} of {% if other.contract_name == context.contract.name %}this contract{%else%}the {{ other.contract_name }} contract{%endif%}. {% else %} - An external actor "{{ other.external_actor }}" diff --git a/composer/templates/autoprove_report.html.j2 b/composer/templates/autoprove_report.html.j2 index 894c6c9c..3439e896 100644 --- a/composer/templates/autoprove_report.html.j2 +++ b/composer/templates/autoprove_report.html.j2 @@ -2,7 +2,7 @@ -{{ terms.title }} — {{ report.contract_name }} +{{ terms.title }} — {{ contract_name }}