diff --git a/.github/workflows/integration-tests.yml b/.github/workflows/integration-tests.yml
index 1afdf305..d8b1b52a 100644
--- a/.github/workflows/integration-tests.yml
+++ b/.github/workflows/integration-tests.yml
@@ -51,15 +51,16 @@ jobs:
sudo chmod +x /usr/local/bin/solc8.29
solc8.29 --version
- - name: async runners
- run: |
- uv pip install pytest-xdist
-
- name: run autoprover integration tests
run: |
uv run pytest -n 3 -m 'expensive' tests
env:
CERTORAKEY: ${{ secrets.CERTORAKEY }}
+ - name: run template fuzz tests
+ run: |
+ uv run pytest -n 2 -m 'fuzz' tests
+ env:
+ HYPOTHESIS_PROFILE: extended
# Fires ONLY if a step above failed. The whole point of the file.
- name: Notify Slack on failure
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/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/foundry/author.py b/composer/foundry/author.py
index f7596455..4b367ec8 100644
--- a/composer/foundry/author.py
+++ b/composer/foundry/author.py
@@ -47,8 +47,7 @@
from composer.spec.gen_types import TypedTemplate
from composer.spec.graph_builder import bind_standard, run_to_completion
from composer.spec.types import PropertyFormulation
-from composer.spec.system_model import ContractComponentInstance
-from composer.spec.tool_env import BasicAgentTools
+from composer.spec.system_model import ContractComponentInstance, component_context
from composer.spec.service_host import ServiceHost
from composer.spec.util import uniq_thread_id
from composer.tools.thinking import RoughDraftState, get_rough_draft_tools
@@ -611,7 +610,7 @@ def get_resume_prompt(self, state: FoundryGenerationState, summary: str) -> str:
# Top-level batch entry
# ---------------------------------------------------------------------------
-
+@component_context
class FoundryPropertyGenParams(TypedDict):
"""Per-batch render variables for ``foundry_property_generation_prompt.j2``.
Mirror of ``PropertyGenParams`` in the CVL author, minus ``resources``
@@ -619,6 +618,7 @@ class FoundryPropertyGenParams(TypedDict):
context: ContractComponentInstance | None
properties: list[PropertyFormulation]
contract_name: str
+ sort: Literal["existing"]
_FoundryPropertyGenTemplate = TypedTemplate[FoundryPropertyGenParams](
@@ -668,6 +668,7 @@ async def batch_foundry_test_generation(
"context": component,
"properties": props,
"contract_name": contract_name,
+ "sort": "existing"
})
titles = [p.title for p in props]
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/pipeline/core.py b/composer/pipeline/core.py
index 3c92a585..4f7ca944 100644
--- a/composer/pipeline/core.py
+++ b/composer/pipeline/core.py
@@ -55,7 +55,7 @@ class Formalizer[FormT: BackendResult](ABC):
state — never set post-hoc. `FormT: ReportableResult` is what makes the report a core step."""
formalized_type: type[FormT]
backend_tag: ReportBackend
-
+
@abstractmethod
async def formalize(
self,
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..b6822a4a 100644
--- a/composer/spec/feedback.py
+++ b/composer/spec/feedback.py
@@ -17,9 +17,9 @@
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.system_model import ContractComponentInstance, component_context
from composer.spec.util import uniq_thread_id
class PropertyFeedback(BaseModel):
@@ -32,6 +32,11 @@ class PropertyFeedback(BaseModel):
class Properties(TypedDict):
properties: list[PropertyFormulation]
+class FeedbackInputs(Properties):
+ rebuttals: Sequence[Rebuttal]
+ skipped: Sequence[SkippedProperty]
+
+@component_context
class FeedbackInherentParams(TypedDict):
context: ContractComponentInstance | None
# Matches the tri-state on the env-level ``sort``:
@@ -42,7 +47,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 +61,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 +93,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 +107,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 +124,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..440b69ea 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, TypedDict
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..b5e59ba0 100644
--- a/composer/spec/natspec/author.py
+++ b/composer/spec/natspec/author.py
@@ -16,23 +16,24 @@
FeedbackToolContext, check_completion, CVLGenerationExtra
)
-
+from composer.spec.service_host import Sort
from composer.spec.context import (
WorkflowContext, CVLGeneration, SystemDoc
)
from composer.spec.types import PropertyFormulation
from composer.spec.feedback import property_feedback_judge, Properties, FeedbackTemplate
from composer.spec.gen_types import TypedTemplate
-from composer.spec.system_model import ContractComponentInstance, ContractName
+from composer.spec.system_model import ContractComponentInstance, ContractName, component_context
from composer.spec.cvl_generation import CVL_JUDGE_KEY, FeedbackToolContext, static_tools, SkippedProperty
from composer.spec.service_host import ServiceHost
from composer.ui.tool_display import tool_display, suppress_ack
from composer.spec.natspec.task_description import Assembler, ConfigurationBuilder
from composer.spec.natspec.typecheck import TypeChecker
+@component_context
class SourceGenerationParams(Properties):
context: ContractComponentInstance
- sort: Literal["greenfield", "existing", "update"]
+ sort: Sort
NoSourceGen = TypedTemplate[SourceGenerationParams]("nosource_property_generation_prompt.j2")
@@ -223,7 +224,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..c899038a 100644
--- a/composer/spec/natspec/interface_gen.py
+++ b/composer/spec/natspec/interface_gen.py
@@ -26,7 +26,7 @@
InterfaceGenCallParams,
resolve_extra_input,
)
-from composer.spec.system_model import NatspecApplication, SolidityIdentifier
+from composer.spec.system_model import NatspecApplication, SolidityIdentifier, ExplicitContract, FromSourceContract, ExistingFromSource
from composer.spec.util import string_hash, uniq_thread_id
from composer.spec.service_host import ServiceHost
@@ -43,7 +43,7 @@ async def generate_interface[I: InterfaceDeclModel](
materializer: Assembler,
description: AgentDescription[InterfaceResult[I], InterfaceGenCallParams],
*,
- target_identifiers: set[SolidityIdentifier] | None = None,
+ target_identifiers: set[SolidityIdentifier],
) -> InterfaceResult[I]:
"""Generate a Solidity interface from component analysis and system document.
@@ -71,12 +71,6 @@ async def generate_interface[I: InterfaceDeclModel](
solc_name = f"solc{solc_version}"
- external_contracts = (
- target_identifiers
- if target_identifiers is not None
- else {c.solidity_identifier for c in summary.contract_components}
- )
-
ST = type("ST", (MessagesState,), {
"__annotations__": {"result": NotRequired[InterfaceResult[I]]}
})
@@ -91,13 +85,13 @@ class ResultTool(AsyncResultTool[result_ty]):
async def validate_result(self, res: InterfaceResult[I]) -> str | None:
seen: set[SolidityIdentifier] = set()
for nm, i in res.name_to_interface.items():
- if nm not in external_contracts:
+ if nm not in target_identifiers:
return f"Invalid entry found; no external contract with solidity identifier {nm} appears in input"
if not i.path.endswith(".sol"):
return f"Interface path '{i.path}' for {nm} must end in '.sol'."
seen.add(nm)
- if seen != external_contracts:
- return f"Missing results for contract(s): {external_contracts - seen}"
+ if seen != target_identifiers:
+ return f"Missing results for contract(s): {target_identifiers - seen}"
compile_inputs = [i.path for i in res.name_to_interface.values()]
try:
@@ -127,13 +121,18 @@ async def validate_result(self, res: InterfaceResult[I]) -> str | None:
return None
target_contracts = [
- c for c in summary.contract_components if c.solidity_identifier in external_contracts
+ c for c in summary.contract_components if c.solidity_identifier in target_identifiers
]
+
+ def assert_is(t: FromSourceContract | ExplicitContract) -> ExistingFromSource:
+ assert isinstance(t, ExistingFromSource)
+ return t
+
existing_contracts = [
- c for c in summary.contract_components if c.solidity_identifier not in external_contracts
+ assert_is(c) for c in summary.contract_components if c.solidity_identifier not in target_identifiers
]
- 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..bb337d6a 100644
--- a/composer/spec/natspec/task_description.py
+++ b/composer/spec/natspec/task_description.py
@@ -5,13 +5,13 @@
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,
StubDeclarationModel,
)
-from composer.spec.system_model import ExplicitContract, NatspecApplication, SolidityIdentifier
+from composer.spec.system_model import ExplicitContract, NatspecApplication, SolidityIdentifier, ExistingFromSource
from composer.spec.util import temp_certora_file
@@ -28,7 +28,7 @@
class InterfaceGenCallParams(TypedDict):
summary: NatspecApplication
target_contracts: list[ExplicitContract]
- existing_contracts: list[ExplicitContract]
+ existing_contracts: list[ExistingFromSource]
solc_version: str
@@ -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/prop_inference.py b/composer/spec/prop_inference.py
index 3edc92c0..008050ef 100644
--- a/composer/spec/prop_inference.py
+++ b/composer/spec/prop_inference.py
@@ -4,7 +4,7 @@
Parameterized by source availability via AnalysisInput tuple.
"""
-from typing import Any, Callable, NotRequired, override, Literal, Sequence
+from typing import Any, Callable, NotRequired, override, Literal, Sequence, TypedDict
import re
from difflib import SequenceMatcher
from pydantic import BaseModel, Field
@@ -18,17 +18,17 @@
from graphcore.tools.schemas import WithImplementation
from composer.input.files import Document
+from composer.spec.gen_types import TypedTemplate
from composer.spec.context import WorkflowContext, CacheKey, ComponentGroup
from composer.spec.graph_builder import bind_standard, run_to_completion
from composer.spec.types import PropertyFormulation
-from composer.spec.system_model import ContractComponentInstance
+from composer.spec.system_model import ContractComponentInstance, component_context
from composer.tools.thinking import RoughDraftState, get_rough_draft_tools
from composer.spec.service_host import Sort, ServiceHost
from composer.io.conversation import ConversationContextProvider
from composer.spec.refinement import refinement_loop, EndConversation, SyncStateUpdateTool
from composer.templates.loader import load_jinja_template
from composer.ui.tool_display import tool_display
-from composer.spec.util import string_hash
from rich.markdown import Markdown
from rich.console import Group
@@ -99,6 +99,14 @@ class RefinementState(MessagesState):
field not exceeding 2^128 - 1, etc.)
"""
+@component_context
+class PropertyAnalysisParams(TypedDict):
+ sort: Sort
+ context: ContractComponentInstance
+ prior_properties: list[_AgentRoundResult]
+ backend_guidance: str
+
+property_analysis_template = TypedTemplate[PropertyAnalysisParams]("property_analysis_prompt.j2")
def _get_initial_prompt(
context: ContractComponentInstance,
@@ -106,13 +114,12 @@ def _get_initial_prompt(
prev_results: list[_AgentRoundResult],
backend_guidance: str,
) -> str:
- return load_jinja_template(
- "property_analysis_prompt.j2",
- context=context,
- backend_guidance=backend_guidance,
- sort=sort,
- prior_properties=prev_results
- )
+ return property_analysis_template.bind({
+ "backend_guidance": backend_guidance,
+ "context": context,
+ "prior_properties": prev_results,
+ "sort": sort
+ }).render_to(load_jinja_template)
@tool_display("Ending conversation...", None)
class Exit(WithImplementation[str]):
diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py
index d0bf3cd3..02f3d954 100644
--- a/composer/spec/source/author.py
+++ b/composer/spec/source/author.py
@@ -19,7 +19,7 @@
from composer.spec.context import WorkflowContext, CVLGeneration, SourceCode
from composer.spec.types import PropertyFormulation
from composer.pipeline.core import GaveUp
-from composer.spec.system_model import ContractComponentInstance, SolidityIdentifier
+from composer.spec.system_model import ContractComponentInstance, SolidityIdentifier, component_context
from composer.spec.source.prover import ProverStateExtra, DELETE_SKIP, VALIDATION_KEY as PROVER_VALIDATION_KEY
from langgraph.graph import MessagesState
from langgraph.runtime import get_runtime
@@ -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
@@ -151,7 +151,9 @@ class ResourceView(TypedDict):
required: bool
import_path: str
+@component_context
class PropertyGenParams(TypedDict):
+ sort: Literal["existing"]
context: ContractComponentInstance | None
resources: list[ResourceView]
properties: list[PropertyFormulation]
@@ -361,7 +363,8 @@ async def batch_cvl_generation(
"resources": resource_views,
"context": component,
"properties": props,
- "contract_name": source.contract_name
+ "contract_name": source.contract_name,
+ "sort": "existing"
})
# use "cache=long" to account for very long prover runs.
@@ -391,7 +394,7 @@ async def batch_cvl_generation(
feedback_env = property_feedback_judge(
ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({
"sort": "existing",
- "context": component
+ "context": component,
}), props
)
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..7a0afee7 100644
--- a/composer/spec/system_model.py
+++ b/composer/spec/system_model.py
@@ -1,8 +1,10 @@
from dataclasses import dataclass
-from typing import Literal
+from typing import Literal, TypedDict
+from typing_extensions import ReadOnly
from pydantic import BaseModel, Field
from functools import cached_property
from composer.spec.util import slugify_filename
+from composer.spec.service_host import Sort
from .types import ComponentName, SolidityIdentifier, ContractName
type ContractSort = Literal["dynamic", "singleton", "multiple"]
@@ -190,7 +192,7 @@ class ContractInstance:
@property
def contract(self) -> ExplicitContract:
return self.app.contract_components[self.ind]
-
+
@cached_property
def sibling_contracts(self) -> list[ExplicitContract]:
to_ret : list[ExplicitContract] = []
@@ -245,3 +247,44 @@ def from_app(
ind=component_index,
_contract=ContractInstance(ind=contract_index, app=app),
)
+
+# The structural shape a template-param TypedDict must have to be marked: a
+# ``sort`` plus a per-component ``context``. Used only as the ``@component_context``
+# bound, so the decorator statically rejects param dicts that don't actually carry
+# these two fields.
+class ComponentContextProtocol(TypedDict):
+ sort: ReadOnly[Sort]
+ context: ReadOnly[ContractComponentInstance | None]
+
+# Dunder attribute stamped on marked classes. A trailing-underscore-pair name so
+# it is never subject to identifier name-mangling.
+_context_marker_attr = "__template_ctxt_params__"
+
+
+def component_context[T: ComponentContextProtocol](t: type[T]) -> type[T]:
+ """Assert a template-param TypedDict conforms to the context-param shape, and
+ mark it for coherent fuzzing. Two roles:
+
+ * **Conformance check.** Python has no native way to declare that a TypedDict
+ "implements" a shape — TypedDict inheritance only *adds* keys, it can't
+ assert that a separately-declared dict (e.g. one that already extends some
+ other params base) matches a protocol. Routing the dict through this
+ decorator, whose parameter is bound ``T: ComponentContextProtocol``, makes
+ the type checker verify at the declaration site that it really carries
+ ``sort: Sort`` and ``context: ContractComponentInstance | None``. The dict is
+ returned unchanged, so this is a purely checked pass-through.
+ * **Runtime marker.** Stamps ``_context_marker_attr`` on the class object (not
+ on instances). The template fuzz test discovers marked classes by this
+ attribute and, for each, draws a ``sort`` and then a ``context`` coherent
+ with it rather than independently — templates read sort-gated,
+ subtype-specific fields off the context, so an incoherent pair renders into a
+ crash (see ``tests/test_fuzzed_templates.py``).
+
+ The marker is an attribute, not an annotation, so it never appears among the
+ TypedDict's keys (``get_type_hints`` / ``__required_keys__`` are untouched).
+ Because TypedDict class attributes are not inherited by derived TypedDicts, each
+ concrete param dict must be decorated directly — marking a base does not
+ propagate.
+ """
+ setattr(t, _context_marker_attr, True)
+ return t
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..2ffe0788 100644
--- a/composer/templates/application_context_new.j2
+++ b/composer/templates/application_context_new.j2
@@ -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 }}