diff --git a/composer/pipeline/core.py b/composer/pipeline/core.py index 97ce1b0b..d5c54f7d 100644 --- a/composer/pipeline/core.py +++ b/composer/pipeline/core.py @@ -134,7 +134,7 @@ def _component_cache_key(c: ContractComponentInstance) -> CacheKey[Properties, C return CacheKey(string_hash("|".join([c.app.model_dump_json(), str(c.ind), str(c._contract.ind)]))) -def _batch_cache_key[FormT: BaseModel](props: list[PropertyFormulation]) -> CacheKey[ComponentGroup, FormT]: +def _batch_cache_key[FormT: BaseModel](props: list[PropertyFormulation]) -> CacheKey[ComponentGroup, FormT]: # pyright: ignore[reportInvalidTypeVarUse] return CacheKey(string_hash("|".join(p.model_dump_json() for p in props))) diff --git a/composer/spec/agent_index.py b/composer/spec/agent_index.py index ef314b31..2bde2a4c 100644 --- a/composer/spec/agent_index.py +++ b/composer/spec/agent_index.py @@ -3,10 +3,10 @@ import os import unicodedata from dataclasses import dataclass -from typing import TypedDict, Unpack, cast, overload, override +from typing import TypedDict, Unpack, cast, overload, override, Awaitable, AsyncIterable from abc import abstractmethod, ABC -from langgraph.store.base import BaseStore +from langgraph.store.base import BaseStore, SearchItem from graphcore.tools.schemas import WithAsyncDependencies from pydantic import Field @@ -79,8 +79,52 @@ def agent_index_config_from_env(data_ns: tuple[str, ...]) -> AgentIndexConfig: "Expected one of: tiered, trusted, readonly." ) +class AgentIndexBase: + @dataclass + class _ListIter[T]: + wrapped: list[T] + ptr: int = 0 + + def peek(self) -> T | None: + if self.ptr >= len(self.wrapped): + return None + return self.wrapped[self.ptr] + + def pop(self) -> T: + to_ret = self.wrapped[self.ptr] + self.ptr += 1 + return to_ret + + @classmethod + def _normalize(cls, text: str) -> str: + nfkc = unicodedata.normalize("NFKC", text).casefold() + stripped = "".join(c for c in nfkc if not unicodedata.category(c).startswith("P")) + return " ".join(stripped.split()) -class AgentIndex: + @classmethod + def _question_key( + cls, question: str + ) -> str: + return hashlib.sha256(cls._normalize(question).encode()).hexdigest()[18:] + + @classmethod + async def parallel_search( + cls, *args: Awaitable[list[SearchItem]] + ) -> AsyncIterable[SearchItem]: + query_results = await asyncio.gather(*args) + result_pointers = [ + cls._ListIter(l) for l in query_results + ] + while True: + query = ((i, peeked) for (i, it) in enumerate(result_pointers) if (peeked := it.peek()) is not None) + m = max(query, key=lambda r: cast(float, r[1].score), default=None) + if m is None: + return + popped = result_pointers[m[0]].pop() + yield popped + + +class AgentIndex(AgentIndexBase): """Two-layer semantic cache. ``base_layer`` is always consulted on reads and is the default @@ -142,16 +186,6 @@ def _read_pools(self) -> list[tuple[str, ...]]: return [self.base_layer] return [self.write_layer, self.base_layer] - def _normalize(self, text: str) -> str: - nfkc = unicodedata.normalize("NFKC", text).casefold() - stripped = "".join(c for c in nfkc if not unicodedata.category(c).startswith("P")) - return " ".join(stripped.split()) - - def _question_key( - self, question: str - ) -> str: - return hashlib.sha256(self._normalize(question).encode()).hexdigest()[18:] - async def aput( self, **doc: Unpack[AgentResult] @@ -183,20 +217,13 @@ async def aget( return cast(AgentResult, r.value) return None - @dataclass - class _ListIter[T]: - wrapped: list[T] - ptr: int = 0 - - def peek(self) -> T | None: - if self.ptr >= len(self.wrapped): - return None - return self.wrapped[self.ptr] - - def pop(self) -> T: - to_ret = self.wrapped[self.ptr] - self.ptr += 1 - return to_ret + def _raw_search( + self, question: str + ) -> list[Awaitable[list[SearchItem]]]: + return [ + self.store.asearch(ns, query=question, limit=5) + for ns in self._read_pools + ] async def asearch( self, question: str @@ -209,21 +236,12 @@ async def asearch( # the same metric (cosine similarity), so merging by score is # meaningful. Dedup defends against the same key existing in both # pools (which a manual / offline promotion may produce). - pool_results = await asyncio.gather(*[ - self.store.asearch(ns, query=question, limit=5) - for ns in self._read_pools - ]) - result_pointers = [ - AgentIndex._ListIter(l) for l in pool_results - ] context : list[IndexedAgentResult] = [] seen = set() - while True: - query = ((i, peeked) for (i, it) in enumerate(result_pointers) if (peeked := it.peek()) is not None) - m = max(query, key=lambda r: cast(float, r[1].score), default=None) - if m is None: - return context - popped = result_pointers[m[0]].pop() + async for popped in self.parallel_search(*( + self.store.asearch(ns, query=question, limit=5) + for ns in self._read_pools + )): if popped.key in seen: continue seen.add(popped.key) @@ -234,6 +252,7 @@ async def asearch( }) if len(context) == 5: return context + return context @overload @staticmethod @@ -330,10 +349,10 @@ async def run(self) -> str: # Document-Ref can be surfaced. return answer return f"{answer}\n\nDocument-Ref: {ref_key}" - + class RetrieveDocumentTool(WithAsyncDependencies[str, AgentIndex]): """ - Retrieve the document associated with the provided document ref + Retrieve the document associated with the provided document ref. """ ref: str = Field(description="The document reference id") diff --git a/composer/spec/code_explorer.py b/composer/spec/code_explorer.py index fd4906da..1159e988 100644 --- a/composer/spec/code_explorer.py +++ b/composer/spec/code_explorer.py @@ -9,20 +9,17 @@ from pydantic import Field, BaseModel -from langchain_core.language_models.chat_models import BaseChatModel from langchain_core.tools import BaseTool from langgraph.graph.state import CompiledStateGraph from langgraph.checkpoint.memory import InMemorySaver -from graphcore.graph import Builder, FlowInput, MessagesState +from graphcore.graph import FlowInput, MessagesState from graphcore.tools.schemas import WithAsyncImplementation, WithInjectedId -from graphcore.tools.vfs import fs_tools from composer.spec.graph_builder import bind_standard, run_to_completion -from composer.templates.loader import load_jinja_template from composer.spec.tool_env import BaseSourceTools, BasicAgentTools from composer.spec.util import uniq_thread_id -from composer.spec.agent_index import AgentIndex, IndexedTool, WithAgentIndex +from composer.spec.agent_index import AgentIndex, IndexedTool from composer.ui.tool_display import tool_display_of, CommonTools @@ -85,10 +82,19 @@ class _ExploreCodeCommon(BaseModel): is roughly the slowest single answer instead of the sum. """ question: str = Field( - description="A specific, focused question about the source code. " - "Good: 'What state variables does withdraw() modify and how?' " - "Bad: 'Tell me about the contract' " - "Bad: 'What is the definition of function X?' (read the source directly)" + description=""" +A specific, focused question about the source code. Do not ask questions about: +* The current task you're working on +* How to use other tools +* Questions about CVL or the prover +* Protocol related questions unrelated to the source code (e.g. expected deployment params, contract address seeds) +* Questions about the Solidity language itself + +Good: 'What state variables does withdraw() modify and how?' +Bad: 'Tell me about the contract' +Bad: 'What is the definition of function X?' (read the source directly) +Bad: 'Is it realistic to expect deposits > 2^128?' +""" ) diff --git a/composer/spec/context.py b/composer/spec/context.py index 623c3f9c..5ddb030b 100644 --- a/composer/spec/context.py +++ b/composer/spec/context.py @@ -121,9 +121,16 @@ class Contract: type Abstraction = CVLGeneration | FoundryGeneration +class EditorAgent: + """editor for a single property""" + +class EditorJudge: + """judge for the editor""" + + type Marker = ( InvJudge | InvFormal | Properties | ComponentGroup - | CVLJudge | FoundryJudge | Abstraction | Contract + | CVLJudge | FoundryJudge | Abstraction | Contract | EditorAgent | EditorJudge ) # --------------------------------------------------------------------------- diff --git a/composer/spec/cvl_generation.py b/composer/spec/cvl_generation.py index 3dd1a3d8..90483223 100644 --- a/composer/spec/cvl_generation.py +++ b/composer/spec/cvl_generation.py @@ -7,8 +7,9 @@ """ import hashlib +from abc import ABC, abstractmethod from dataclasses import dataclass -from typing import Annotated, Callable, Literal, NotRequired, override, Awaitable, Any, Protocol +from typing import Annotated, Callable, Literal, NotRequired, Sequence, override, Awaitable, Any, Protocol from typing_extensions import TypedDict from pydantic import BaseModel, Field @@ -18,10 +19,9 @@ from langgraph.types import Command from langgraph.graph import MessagesState from langgraph.graph.state import CompiledStateGraph -from langgraph.runtime import get_runtime from graphcore.graph import FlowInput, tool_state_update, tool_return -from graphcore.tools.schemas import WithImplementation, WithInjectedState, WithInjectedId, WithAsyncImplementation +from graphcore.tools.schemas import WithInjectedState, WithInjectedId, WithAsyncDependencies from composer.spec.context import ( WorkflowContext, CacheKey, CVLGeneration, CVLJudge, @@ -120,6 +120,12 @@ def _output_link(link: str | None) -> str | None: """Rewrite a prover ``/jobStatus/`` URL to its ``/output/`` view; local result dirs (and ``None``) pass through unchanged.""" return link.replace("/jobStatus/", "/output/") if link else None +class AppliedEdit(BaseModel): + """Provenance of one applied source edit: its edit-store id and the + editor's account of what changed and why it is acceptable.""" + edit_id: str + executive_summary: str + why_sound: str class GeneratedCVL(BaseModel): @@ -134,6 +140,13 @@ class GeneratedCVL(BaseModel): # The last prover-run link (URL or local results dir), persisted for the report and so a # cache hit retains it. None when the prover never produced a link. final_link: str | None = Field(default=None) + # The author's working copy at completion: the edited source files the proof + # actually ran against (empty when no edits were applied — always the case + # outside the editing-enabled source pipeline), and the provenance of each + # applied edit in application order. A cache hit replays these along with + # the spec, so the proof's source view is never silently lost. + vfs: dict[str, str] = Field(default_factory=dict) + applied_edits: list[AppliedEdit] = Field(default_factory=list) def property_units(self) -> list[tuple[str, list[str]]]: """Property title -> the CVL rule names that formalize it (the report's `ReportableResult` @@ -163,22 +176,34 @@ class CVLGenerationExtra(TypedDict): required_validations: list[str] -def _compute_digest(curr_spec: str, skipped: list[SkippedProperty]) -> str: +def _compute_digest( + curr_spec: str, + skipped: list[SkippedProperty], + version_history: Sequence[str] = (), +) -> str: + """Digest of everything a validation stamp vouches for: the spec, the skip + set, and — in the editing-enabled source pipeline — the applied-edit + history, so a stamp earned before a source edit goes stale with it. + Pipelines without source editing pass no history and hash identically to + before.""" digester = hashlib.md5() digester.update(curr_spec.encode()) for s in skipped: digester.update(f"{s.property_title}:{s.reason}".encode()) + for edit_id in version_history: + digester.update(f"edit:{edit_id}".encode()) return digester.hexdigest() def check_completion( state: CVLGenerationExtra, + version_history: Sequence[str] = (), ) -> str | None: """Returns None if valid, error string if not.""" spec = state["curr_spec"] if spec is None: return "Completion REJECTED: no spec written yet." - digest = _compute_digest(spec, state["skipped"]) + digest = _compute_digest(spec, state["skipped"], version_history) validations = state["validations"] required = state["required_validations"] for key in required: @@ -231,16 +256,20 @@ def validate_property_rules( return None -def make_validation_stamper(key: str) -> Callable[[CVLGenerationExtra], dict[str, str]]: +def make_validation_stamper( + key: str, +) -> Callable[[CVLGenerationExtra, Sequence[str]], dict[str, str]]: """Create a stamper for future prover tool integration. - The stamper reads curr_spec/skipped from state and returns - a dict suitable for merging into the validations state key. + The stamper reads curr_spec/skipped from state — plus the caller's + applied-edit history — and returns a dict suitable for merging into the + validations state key. """ - def stamp(state: CVLGenerationExtra) -> dict[str, str]: + def stamp(state: CVLGenerationExtra, version_history: Sequence[str]) -> dict[str, str]: return {key: _compute_digest( state["curr_spec"] or "", state["skipped"], + version_history, )} return stamp @@ -265,12 +294,15 @@ class _LastAttemptCache(BaseModel): Awaitable[PropertyFeedbackProtocol], ] """``(cvl, skipped, rebuttals, within_tool) -> PropertyFeedback``. ``within_tool`` -is the calling ``_FeedbackSchema``'s ``tool_call_id``, plumbed through to the +is the calling feedback tool's ``tool_call_id``, plumbed through to the sub-graph's ``run_to_completion`` so its UI panel anchors under the parent tool widget.""" @dataclass -class FeedbackToolContext: +class FeedbackServices: + """Runtime dependencies of the property-management tool suite, bound into + the tools at construction time (``WithAsyncDependencies``) by whoever + assembles the generation graph — the natspec author, the source author.""" feedback_thunk: FeedbackToolImpl # The batch's property titles (unique, enforced at extraction). Used to validate that # the titles named by record_skip / unskip_property / the result mapping refer to real @@ -279,8 +311,7 @@ class FeedbackToolContext: FEEDBACK_VALIDATION_KEY = "feedback" -@tool_display("Getting feedback", "Feedback") -class _FeedbackSchema(WithInjectedState[CVLGenerationState], WithInjectedId, WithAsyncImplementation[Command]): +class FeedbackToolBase[ST: CVLGenerationState](WithInjectedState[ST], WithInjectedId, ABC): """ Receive feedback on your CVL and any skip declarations. The judge will evaluate coverage (all properties accounted for) @@ -303,29 +334,61 @@ class _FeedbackSchema(WithInjectedState[CVLGenerationState], WithInjectedId, Wit ), ) - @override + @abstractmethod + async def _get_feedback( + self, spec: str, skipped: list[SkippedProperty] + ) -> PropertyFeedbackProtocol: + """Invoke the judge. Subclasses own how the judge is reached and what + extra context (if any) rides along with the invocation.""" + ... + + @abstractmethod + def _version_history(self) -> Sequence[str]: + """The applied-edit history a good verdict's stamp is bound to, so the + stamp goes stale if the source is edited afterwards. Pipelines without + source editing return ().""" + ... + async def run(self) -> Command: - feedback = get_runtime(FeedbackToolContext).context.feedback_thunk st = self.state spec = st["curr_spec"] if spec is None: return tool_return(self.tool_call_id, "No spec put yet") skipped = st["skipped"] - t = await feedback(spec, skipped, self.rebuttals, self.tool_call_id) + t = await self._get_feedback(spec, skipped) msg = f"Good? {t.good}\nFeedback {t.feedback}" if t.good: - digest = _compute_digest(spec, skipped) + digest = _compute_digest(spec, skipped, self._version_history()) return tool_state_update( self.tool_call_id, msg, validations={FEEDBACK_VALIDATION_KEY: digest}, ) return tool_state_update(self.tool_call_id, msg) + +@tool_display("Getting feedback", "Feedback") +class VanillaFeedbackTool( + FeedbackToolBase[CVLGenerationState], + WithAsyncDependencies[Command, FeedbackServices], +): + __doc__ = FeedbackToolBase.__doc__ + + @override + async def _get_feedback( + self, spec: str, skipped: list[SkippedProperty] + ) -> PropertyFeedbackProtocol: + with self.tool_deps() as svc: + return await svc.feedback_thunk(spec, skipped, self.rebuttals, self.tool_call_id) + + @override + def _version_history(self) -> Sequence[str]: + return () + @tool_display( lambda p: f"Skipping property `{p.get('property_title', '?')}`", suppress_ack("Skip result", ("Recorded skip",)), ) -class _RecordSkipSchema(WithInjectedState[CVLGenerationState], WithInjectedId, WithImplementation[Command]): +class _RecordSkipSchema(WithInjectedId, WithAsyncDependencies[Command, list[str]]): """ Declare that you are skipping a property from the batch. You must provide the property's title and a justification. @@ -340,33 +403,33 @@ class _RecordSkipSchema(WithInjectedState[CVLGenerationState], WithInjectedId, W ) @override - def run(self) -> Command: - titles = get_runtime(FeedbackToolContext).context.titles - if self.property_title not in titles: - return tool_state_update( - self.tool_call_id, - f"Unknown property title {self.property_title!r}. Must be one of: {', '.join(titles)}.", + async def run(self) -> Command: + with self.tool_deps() as titles: + if self.property_title not in titles: + return tool_state_update( + self.tool_call_id, + f"Unknown property title {self.property_title!r}. Must be one of: {', '.join(titles)}.", + ) + if not self.reason.strip(): + return tool_state_update( + self.tool_call_id, + "A non-empty justification is required when skipping a property.", + ) + skip = SkippedProperty( + property_title=self.property_title, + reason=self.reason, ) - if not self.reason.strip(): return tool_state_update( self.tool_call_id, - "A non-empty justification is required when skipping a property.", + f"Recorded skip for property {self.property_title}.", + skipped=[skip], ) - skip = SkippedProperty( - property_title=self.property_title, - reason=self.reason, - ) - return tool_state_update( - self.tool_call_id, - f"Recorded skip for property {self.property_title}.", - skipped=[skip], - ) @tool_display( lambda p: f"Un-skipping property `{p.get('property_title', '?')}`", suppress_ack("Unskip result", ("Removed skip",)), ) -class _UnskipSchema(WithInjectedId, WithImplementation[Command]): +class _UnskipSchema(WithInjectedId, WithAsyncDependencies[Command, list[str]]): """ Remove a previously declared skip for a property. Use this if you later find a way to formalize a property you previously skipped. @@ -376,30 +439,30 @@ class _UnskipSchema(WithInjectedId, WithImplementation[Command]): ) @override - def run(self) -> Command: - titles = get_runtime(FeedbackToolContext).context.titles - if self.property_title not in titles: + async def run(self) -> Command: + with self.tool_deps() as titles: + if self.property_title not in titles: + return tool_state_update( + self.tool_call_id, + f"Unknown property title {self.property_title!r}. Must be one of: {', '.join(titles)}.", + ) + # Empty reason is the sentinel for "not skipped" + skip = SkippedProperty( + property_title=self.property_title, + reason="", + ) return tool_state_update( self.tool_call_id, - f"Unknown property title {self.property_title!r}. Must be one of: {', '.join(titles)}.", + f"Removed skip for property {self.property_title}.", + skipped=[skip], ) - # Empty reason is the sentinel for "not skipped" - skip = SkippedProperty( - property_title=self.property_title, - reason="", - ) - return tool_state_update( - self.tool_call_id, - f"Removed skip for property {self.property_title}.", - skipped=[skip], - ) def static_tools() -> list[BaseTool]: + """The dependency-free CVL authoring tools. The property-management suite + (feedback / skip tools) is NOT here — it carries runtime deps; see + :func:`skip_tools` and :class:`FeedbackToolBase`.""" return [ put_cvl, put_cvl_raw, - _FeedbackSchema.as_tool("feedback_tool"), - _RecordSkipSchema.as_tool("record_skip"), - _UnskipSchema.as_tool("unskip_property"), get_cvl(CVLGenerationState), edit_cvl(CVLGenerationState), ERC20TokenGuidance.as_tool("erc20_guidance"), @@ -407,11 +470,29 @@ def static_tools() -> list[BaseTool]: ] -async def run_cvl_generator[S: CVLGenerationState, C: FeedbackToolContext, I: CVLGenerationInput]( +def skip_tools(titles: list[str]) -> list[BaseTool]: + """The skip-management pair, bound to the batch's property titles.""" + return [ + _RecordSkipSchema.bind(titles).as_tool("record_skip"), + _UnskipSchema.bind(titles).as_tool("unskip_property"), + ] + + +def property_tools(services: FeedbackServices) -> list[BaseTool]: + """The full property-management suite with the vanilla feedback tool. + Callers with a custom feedback tool (e.g. the editor-aware source author) + bind their own :class:`FeedbackToolBase` subclass and use + :func:`skip_tools` directly.""" + return [ + VanillaFeedbackTool.bind(services).as_tool("feedback_tool"), + *skip_tools(services.titles), + ] + + +async def run_cvl_generator[S: CVLGenerationState, I: CVLGenerationInput]( ctx: WorkflowContext[CVLGeneration], - d: CompiledStateGraph[S, C, I, Any], + d: CompiledStateGraph[S, None, I, Any], in_state: I, - ctxt: C, description: str, skip_mnemonic: bool = False ) -> S: @@ -436,7 +517,7 @@ async def run_cvl_generator[S: CVLGenerationState, C: FeedbackToolContext, I: CV d, in_state_copy, thread_id=tid, - context=ctxt, + context=None, description=desc, recursion_limit=ctx.recursion_limit, ) diff --git a/composer/spec/feedback.py b/composer/spec/feedback.py index 1aceda7a..ece638de 100644 --- a/composer/spec/feedback.py +++ b/composer/spec/feedback.py @@ -1,14 +1,17 @@ -from typing import Callable, NotRequired, Sequence +import inspect +from dataclasses import dataclass +from typing import Callable, NotRequired, Protocol, Sequence, Awaitable from typing_extensions import TypedDict from composer.spec.service_host import Sort, ServiceHost from pydantic import BaseModel, Field - +from langchain_core.tools import BaseTool from langgraph.graph import MessagesState -from graphcore.graph import FlowInput +from graphcore.graph import Builder, FlowInput +from graphcore.tools.vfs import VFSState from composer.spec.context import ( WorkflowContext, CVLJudge @@ -18,7 +21,8 @@ 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.cvl_generation import FeedbackToolContext, Rebuttal, SkippedProperty +from composer.spec.cvl_generation import FeedbackServices, Rebuttal, SkippedProperty +from composer.spec.source.live_explorer import VersionedHistory from composer.spec.system_model import ContractComponentInstance from composer.spec.util import uniq_thread_id @@ -41,47 +45,124 @@ class FeedbackInherentParams(TypedDict): # ``existing`` — pre-existing codebase being verified as-is; target # has real immutable source. sort: Sort + # True when the pipeline can modify the source under verification (the + # editor tool is wired). Swaps the immutable-source skip guidance for the + # "evaluate against the code as it stands" variant. Absent/False keeps the + # immutable story, which remains true for pipelines without the editor. + source_editing: NotRequired[bool] FeedbackTemplate = TypedTemplate[FeedbackInherentParams]("property_judge_prompt.j2") class JudgeSystemParams(TypedDict): sort: Sort + source_editing: NotRequired[bool] # Judge system prompt, shared between the natspec and source-mode flows. The fs # primitives are always documented; ``sort`` drives the rest (the template # compiles out the code_explorer / code_document_ref guidance unless # ``sort == "existing"``, the only mode that wires those tools). +# ``source_editing`` replaces the "No Source Changes" block with the "Source +# Changes" one: the code can differ between rounds, but feedback must stay +# actionable against the code as it stands. FeedbackSystemTemplate = TypedTemplate[JudgeSystemParams]("property_judge_system_prompt.j2") -def property_feedback_judge( + +class JudgeExtra(RoughDraftState): + curr_spec: str + + +class FeedbackBaseState(MessagesState, JudgeExtra): + result: NotRequired[PropertyFeedback] + +class FeedbackBaseInput(FlowInput, JudgeExtra): + pass + +# Extra input parts prepended to every judge invocation. A bare list is static; +# a callable is evaluated per invocation (and may be async) so the producer can +# reflect state that changes between review rounds — e.g. a notice that the +# source under verification has changed since the judge last saw it. +type ExtraInputPrompt = ( + list[str | dict] + | Callable[[], list[str | dict]] + | Callable[[], Awaitable[list[str | dict]]] + | None +) + +type ContextualFeedbackToolImpl[Ctx] = Callable[ + [Ctx, str, list[SkippedProperty], list[Rebuttal], str], + Awaitable[PropertyFeedback] +] + + +class JudgeToolHost(Protocol): + """The judge's construction surface: a builder, the workflow ``sort``, and + the tool suite the judge runs with. Callers vary the FS-read strategy + through ``judge_tools`` — frozen fs tools over the project root, or + vfs-aware tools reading the author's working copy — without the judge + machinery knowing which. ``ServiceHost`` consumers adapt via + :func:`judge_host_of`.""" + + def builder_heavy(self) -> Builder[None, None, None]: ... + + @property + def sort(self) -> Sort: ... + + @property + def judge_tools(self) -> tuple[BaseTool, ...]: ... + + +@dataclass(frozen=True) +class _ServiceHostJudge: + """The vanilla adapter: judge runs with the host's full tool surface.""" + env: ServiceHost + + def builder_heavy(self) -> Builder[None, None, None]: + return self.env.builder_heavy() + + @property + def sort(self) -> Sort: + return self.env.sort + + @property + def judge_tools(self) -> tuple[BaseTool, ...]: + return self.env.all_tools + + +def judge_host_of(env: ServiceHost) -> JudgeToolHost: + return _ServiceHostJudge(env) + + +def property_feedback_judge_generic[ + S: FeedbackBaseState, + I: FeedbackBaseInput, + Ctx +]( + st: type[S], + i: type[I], ctx: WorkflowContext[CVLJudge], - env: ServiceHost, + host: JudgeToolHost, prompt: InjectedTemplate[Properties] | TemplateInstantiation, props: list[PropertyFormulation], - *, - extra_inputs: list[str | dict] | Callable[[], list[str | dict]] | None = None, - system_prompt: TemplateInstantiation | None = None, -) -> FeedbackToolContext: - if system_prompt is None: - system_prompt = FeedbackSystemTemplate.bind({"sort": env.sort}) + extra_inputs: ExtraInputPrompt, + system_prompt: TemplateInstantiation | None, - builder = env.builder_heavy().with_tools( - env.all_tools - ) - - class JudgeExtra(RoughDraftState): - curr_spec: str + input_lift: Callable[[FeedbackBaseInput, Ctx], I], + source_editing: bool = False, +) -> ContextualFeedbackToolImpl[Ctx]: - class ST(MessagesState, JudgeExtra): - result: NotRequired[PropertyFeedback] + if system_prompt is None: + system_prompt = FeedbackSystemTemplate.bind( + {"sort": host.sort, "source_editing": source_editing} + ) - class SpecJudgeInput(FlowInput, JudgeExtra): - pass + builder = host.builder_heavy().with_tools( + host.judge_tools + ) - rough_draft_tools = get_rough_draft_tools(ST) + rough_draft_tools = get_rough_draft_tools(st) - def did_rough_draft_read(s: ST, _) -> str | None: + def did_rough_draft_read(s: S, _) -> str | None: if not s["did_read"]: return "Completion REJECTED: never read rough draft for review" return None @@ -91,16 +172,17 @@ def did_rough_draft_read(s: ST, _) -> str | None: final_prompt = prompt if isinstance(prompt, TemplateInstantiation) else prompt.inject({"properties": props}) workflow = bind_standard( - builder, ST, validator=did_rough_draft_read + builder, st, validator=did_rough_draft_read ).with_input( - SpecJudgeInput + i ).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), ]).compile_async() async def the_tool( + exec_ctx: Ctx, cvl: str, skipped: Sequence[SkippedProperty], rebuttals: Sequence[Rebuttal], @@ -111,7 +193,10 @@ async def the_tool( if isinstance(extra_inputs, list): input_parts.extend(extra_inputs) else: - input_parts.extend(extra_inputs()) + produced = extra_inputs() + if inspect.isawaitable(produced): + produced = await produced + input_parts.extend(produced) input_parts.append("The proposed CVL file is") input_parts.append(cvl) @@ -136,7 +221,7 @@ async def the_tool( ) res = await run_to_completion( workflow, - SpecJudgeInput(input=input_parts, curr_spec=cvl, memory=None, did_read=False), + input_lift(FeedbackBaseInput(input=input_parts, curr_spec=cvl, memory=None, did_read=False), exec_ctx), thread_id=uniq_thread_id("feedback"), recursion_limit=ctx.recursion_limit, description="Property feedback judge", @@ -144,6 +229,91 @@ async def the_tool( ) assert "result" in res return res["result"] + return the_tool + + +def property_feedback_judge( + ctx: WorkflowContext[CVLJudge], + env: ServiceHost, + prompt: InjectedTemplate[Properties] | TemplateInstantiation, + props: list[PropertyFormulation], + *, + extra_inputs: ExtraInputPrompt = None, + system_prompt: TemplateInstantiation | None = None, +) -> FeedbackServices: + """The vanilla judge: the full ``ServiceHost`` tool surface (frozen FS + reads), no source editing. Returns the services bundle the property- + management tool suite binds against.""" + to_wrap = property_feedback_judge_generic( + st=FeedbackBaseState, + i=FeedbackBaseInput, + ctx=ctx, + host=judge_host_of(env), + extra_inputs=extra_inputs, + prompt=prompt, + props=props, + system_prompt=system_prompt, + input_lift=lambda i, _: i, + ) + + return FeedbackServices( + feedback_thunk=lambda spec, skip, rebuttal, tid: to_wrap(None, spec, skip, rebuttal, tid), + titles=[p.title for p in props] + ) + - return FeedbackToolContext(feedback_thunk=the_tool, titles=[p.title for p in props]) +# --------------------------------------------------------------------------- +# Source-editing judge: the author's working copy rides into the judge's state +# --------------------------------------------------------------------------- +@dataclass(frozen=True) +class SourceSnapshot: + """The author's working-copy view at judge-invocation time: the VFS + overlay and the applied-edit history, seeded into the judge's own state so + its vfs-aware FS tools (and the versioned explorer) read the edited + source rather than the on-disk baseline.""" + vfs: dict[str, str] + version_history: list[str] + + +class VfsJudgeState(FeedbackBaseState, VFSState, VersionedHistory): + pass + + +class VfsJudgeInput(FeedbackBaseInput, VFSState, VersionedHistory): + pass + + +def source_feedback_judge( + ctx: WorkflowContext[CVLJudge], + host: JudgeToolHost, + prompt: InjectedTemplate[Properties] | TemplateInstantiation, + props: list[PropertyFormulation], + *, + extra_inputs: ExtraInputPrompt = None, + system_prompt: TemplateInstantiation | None = None, +) -> ContextualFeedbackToolImpl[SourceSnapshot]: + """The editing-aware judge. ``host.judge_tools`` must be the vfs-aware + read suite (they resolve paths through the state seeded from the + :class:`SourceSnapshot`); the returned impl takes that snapshot as its + leading argument on every invocation.""" + + def lift(base: FeedbackBaseInput, snap: SourceSnapshot) -> VfsJudgeInput: + return VfsJudgeInput( + **base, + vfs=snap.vfs, + version_history=snap.version_history, + ) + + return property_feedback_judge_generic( + st=VfsJudgeState, + i=VfsJudgeInput, + ctx=ctx, + host=host, + extra_inputs=extra_inputs, + prompt=prompt, + props=props, + system_prompt=system_prompt, + input_lift=lift, + source_editing=True, + ) diff --git a/composer/spec/natspec/author.py b/composer/spec/natspec/author.py index bf41076c..ae39ee7c 100644 --- a/composer/spec/natspec/author.py +++ b/composer/spec/natspec/author.py @@ -12,8 +12,8 @@ from graphcore.graph import tool_state_update from graphcore.tools.schemas import WithImplementation, WithInjectedId, WithInjectedState, WithAsyncDependencies from composer.spec.cvl_generation import ( - static_tools, run_cvl_generator, CVLGenerationInput, CVLGenerationState, - FeedbackToolContext, check_completion, CVLGenerationExtra + static_tools, property_tools, run_cvl_generator, CVLGenerationInput, CVLGenerationState, + check_completion, CVLGenerationExtra ) @@ -24,7 +24,7 @@ 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.cvl_generation import CVL_JUDGE_KEY, FeedbackToolContext, static_tools, SkippedProperty +from composer.spec.cvl_generation import CVL_JUDGE_KEY, 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 @@ -219,7 +219,7 @@ def stub_feedback_extras() -> list[str | dict]: ctx = root_ctx.abstract(CVLGeneration) - feedback_ctxt = property_feedback_judge( + feedback_services = property_feedback_judge( ctx=ctx.child(CVL_JUDGE_KEY), env=env, prompt=FeedbackTemplate.bind({ "context": component, "sort": env.sort, @@ -231,6 +231,7 @@ def stub_feedback_extras() -> list[str | dict]: .with_tools(env.all_tools) .with_tools(injected_tools) .with_tools(static_tools()) + .with_tools(property_tools(feedback_services)) .with_tools([ GiveUpTool.as_tool("give_up"), AdvisoryTypecheck.bind(typechecker).as_tool("advisory_typecheck"), @@ -240,7 +241,6 @@ def stub_feedback_extras() -> list[str | dict]: .with_output_key("result") .with_input(NatspecGenerationInput) .with_state(NatspecGenerationState) - .with_context(FeedbackToolContext) .with_sys_prompt_template("nosource_property_generation_system_prompt.j2") .inject( lambda b: NoSourceGen.bind({ @@ -265,7 +265,6 @@ def stub_feedback_extras() -> list[str | dict]: suggested_spec_path=None, property_rules=[], ), - ctxt=feedback_ctxt, description = f"{contract_name} {component.component.name} ({len(props)} properties)" ) assert "result" in res diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index d0bf3cd3..afe15b6d 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -1,44 +1,59 @@ -from typing import NotRequired, override, Literal, Annotated +from typing import NotRequired, Sequence, override, Literal, Annotated from typing_extensions import TypedDict import json +from dataclasses import dataclass + from langchain_core.tools import BaseTool from pydantic import Field, BaseModel, Discriminator from graphcore.tools.schemas import ( WithAsyncImplementation, WithImplementation, WithInjectedId, WithInjectedState, + WithAsyncDependencies ) +from graphcore.tools.vfs import VFSAccessor, VFSState from graphcore.graph import tool_state_update from graphcore.summary import SummaryConfig from composer.spec.cvl_generation import ( - static_tools, CVLGenerationExtra, FeedbackToolContext, FEEDBACK_VALIDATION_KEY, + static_tools, property_tools, skip_tools, CVLGenerationExtra, FEEDBACK_VALIDATION_KEY, check_completion, validate_property_rules, CVL_JUDGE_KEY, run_cvl_generator, - GeneratedCVL, PropertyRuleMapping + GeneratedCVL, PropertyRuleMapping, AppliedEdit, FeedbackToolBase, SkippedProperty, + PropertyFeedbackProtocol, ) -from composer.spec.context import WorkflowContext, CVLGeneration, SourceCode +from composer.spec.source.live_explorer import VersionedHistory, LiveEditTools, WIPE_HISTORY +from composer.spec.context import WorkflowContext, CVLGeneration, CacheKey, SourceCode from composer.spec.types import PropertyFormulation -from composer.pipeline.core import GaveUp from composer.spec.system_model import ContractComponentInstance, SolidityIdentifier 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 from pathlib import Path from composer.spec.gen_types import CVLResource, TypedTemplate, import_statement_for -from composer.spec.service_host import ServiceHost +from composer.spec.service_host import ServiceHost, Sort from composer.workflow.services import CacheLevel - +from composer.pipeline.ptypes import GaveUp from langgraph.types import Command -from composer.spec.feedback import property_feedback_judge, FeedbackTemplate +from graphcore.graph import Builder +from composer.spec.feedback import ( + property_feedback_judge, source_feedback_judge, FeedbackTemplate, Properties, + SourceSnapshot, ContextualFeedbackToolImpl, +) from composer.ui.tool_display import tool_display +from composer.spec.source.munge.edit_store import EditStore +from composer.spec.source.munge.munge_agent import editor_tool +from composer.spec.source.munge.vfs_diff import summarize_changes + from graphcore.graph import FlowInput class SourceAuthorExtra(TypedDict): failed: bool | None -class SourceCVLGenerationExtra(CVLGenerationExtra, ProverStateExtra, SourceAuthorExtra): +# ``vfs`` comes from ProverStateExtra (NotRequired, no merge op — replaced +# wholesale by commit_edit / revert_to_edit); the generation input always +# seeds it explicitly. +class SourceCVLGenerationExtra(CVLGenerationExtra, ProverStateExtra, SourceAuthorExtra, VersionedHistory): pass class SourceCVLGenerationInput(SourceCVLGenerationExtra, FlowInput): @@ -91,7 +106,7 @@ async def run(self) -> Command: result=None, ) class PublishResultTool( - WithImplementation[Command | str], + WithAsyncDependencies[Command | str, list[str]], WithInjectedState[SourceCVLGenerationState], WithInjectedId, ): @@ -107,12 +122,12 @@ class PublishResultTool( ) @override - def run(self) -> Command | str: - if (err := check_completion(self.state)) is not None: - return err - titles = get_runtime(FeedbackToolContext).context.titles - if (err := validate_property_rules(self.property_rules, self.state["skipped"], titles)) is not None: + async def run(self) -> Command | str: + if (err := check_completion(self.state, self.state["version_history"])) is not None: return err + with self.tool_deps() as titles: + if (err := validate_property_rules(self.property_rules, self.state["skipped"], titles)) is not None: + return err return tool_state_update( self.tool_call_id, "Accepted", @@ -158,12 +173,19 @@ class PropertyGenParams(TypedDict): contract_name: str class PropertyGenerationConfig(SummaryConfig[SourceCVLGenerationState]): - def __init__(self): + def __init__(self, source_editing: bool = False): super().__init__() + self._source_editing = source_editing @override def get_summarization_prompt(self, state: SourceCVLGenerationState) -> str: - return """ + edit_item = ( + "\n7. The source edits you have applied (their edit ids and what each was for), " + "any edit ids the editor produced that you chose NOT to apply, and any plans " + "you had to request further edits" + if self._source_editing else "" + ) + return f""" You are approaching the context limit for your task. After this point, your context will be cleared and the task restarted from the initial prompt. @@ -177,7 +199,7 @@ def get_summarization_prompt(self, state: SourceCVLGenerationState) -> str: 3. If you have any outstanding, unaddressed feedback from your last iteration with the feedback tool, include that unaddressed feedback in your summary 4. If you have any outstanding, unaddressed tasks from the most recent iteration with the prover, include those unaddressed tasks in your summary 5. Any techniques/attempts that you or the feedback rejected or didn't work -6. Any techniques/attempts that you attempted but were rejected by the prover +6. Any techniques/attempts that you attempted but were rejected by the prover{edit_item} In other words, your summary should include all information necessary to prevent the next iteration on this task from repeating work or repeating mistakes. @@ -187,9 +209,14 @@ def get_summarization_prompt(self, state: SourceCVLGenerationState) -> str: @override def get_resume_prompt(self, state: SourceCVLGenerationState, summary: str) -> str: + edit_note = ( + "\nAny source edits you applied remain in effect on your working copy; " + "the `edit_history_log` tool shows each applied edit and its diff.\n" + if self._source_editing else "" + ) return f""" You are resuming this task already in progress. The current version of your spec (if any) is available via the `get_cvl` tool. - +{edit_note} A summary of your work up until this point is as follows: BEGIN SUMMARY: @@ -328,6 +355,196 @@ async def run(self) -> Command | str: config=curr_config ) +class ApplyEditTool(WithAsyncDependencies[str | Command, EditStore], WithInjectedState[SourceCVLGenerationExtra], WithInjectedId): + """ + Apply the edit staged by the edit agent to your working tree. + """ + edit_id: str = Field(description="The unique edit ID produced by the editor you want to apply") + + @override + async def run(self) -> str | Command: + with self.tool_deps() as dep: + if self.edit_id in self.state["version_history"]: + return f"{self.edit_id} has already been applied; if you want to revert to that state, use the revert_to_edit tool" + new_state = await dep.read(self.edit_id) + if new_state is None: + return f"{self.edit_id} does not denote any known edit" + return tool_state_update( + tool_call_id=self.tool_call_id, + content="Edit applied", + vfs=new_state.vfs, + version_history=[self.edit_id] + ) + +@dataclass +class HistoryDeps: + mat: VFSAccessor[VFSState] + edit_store: EditStore + +class EditHistoryLog(WithAsyncDependencies[str, HistoryDeps], WithInjectedState[SourceCVLGenerationExtra]): + """ + Use this to view a list of the applied edit ids, and the changes to the source code made on + each edit + """ + + @override + async def run(self) -> str: + hist = self.state["version_history"] + if len(hist) == 0: + return "No edits applied, working against clean project directory" + fetched_states: list[dict[str, str]] = [] + history : list[tuple[str, str, str]] = [] + with self.tool_deps() as dep: + for (i, edit_id) in enumerate(hist): + edit_state = await dep.edit_store.read(edit_id) + if edit_state is None: + return "Something has gone very wrong; your edit history has an orphan ID. This is an unrecoverable error; terminate your task immediately" + if i == 0: + prev = {} + else: + prev = fetched_states[i - 1] + diff = summarize_changes( + {"vfs": edit_state.vfs}, dep.mat, prev + ) + history.append((edit_id, edit_state.executive_summary, diff)) + fetched_states.append(edit_state.vfs) + to_format = [ + f""" +--- Edit #{i} (ID: {t}) + +Summary: {summary} + +Diff from {"prior edit" if i > 0 else "project directory"}: + +{diff} +""" + for (i,(t, summary, diff)) in enumerate(history) + ] + return "\n\n".join(to_format) + +class RevertToEdit(WithAsyncDependencies[Command | str, EditStore], WithInjectedId, WithInjectedState[SourceCVLGenerationExtra]): + """ + Call this tool to revert to a prior edit in your history + """ + edit_id: str = Field(description="An edit ID to revert to; it must appear in your history") + + async def run(self) -> str | Command: + if self.edit_id not in self.state["version_history"]: + return f"{self.edit_id} does not appear in your edit history, nothing to revert to" + if self.state["version_history"][-1] == self.edit_id: + return f"Already at edit id {self.edit_id}, nothing to do" + with self.tool_deps() as dep: + i = self.state["version_history"].index(self.edit_id) + target = await dep.read(self.edit_id) + if target is None: + return f"{self.edit_id} is in your history but absent from the edit store; this is an unrecoverable error" + return tool_state_update( + self.tool_call_id, + f"Reverted to id {self.edit_id}", + vfs=target.vfs, + version_history=[WIPE_HISTORY, *self.state["version_history"][:i+1]] + ) + + +def generate_edit_management_tools( + ctx: WorkflowContext[CVLGeneration], + source_env: ServiceHost, + edit: EditStore, + live_tools: LiveEditTools, +) -> list[BaseTool]: + editor = editor_tool( + ctx=ctx, + env=source_env, + edit_tools=live_tools, + edit_store=edit + ) + return [ + editor, + # "commit_edit" is the name the editor's result message tells the author + # to call (see EditMungeTool.run's result_msg) — keep them in sync. + ApplyEditTool.bind(edit).as_tool("commit_edit"), + EditHistoryLog.bind(HistoryDeps(live_tools.mat, edit)).as_tool("edit_history_log"), + RevertToEdit.bind(edit).as_tool("revert_to_edit"), + ] + + +@dataclass(frozen=True) +class SourceEditing: + """The editing-enabled generation phase's kit: the live tool suite + (vfs-aware reads + versioned explorer + live doc ref, plus the write tools + the editor sub-agent uses) and the edit snapshot store. Phases whose output + must hold against the unedited source — structural invariants — run + without one.""" + live: LiveEditTools + store: EditStore + + +class _LastAttemptEdits(BaseModel): + """Sibling of cvl_generation's last-attempt draft cache: the applied-edit + history at snapshot time. The working copy itself is deliberately not + stored — the author's vfs only ever changes wholesale to an edit-store + snapshot, so it is always recoverable as ``store[version_history[-1]].vfs``. + + Written on the same exit path as the draft cache but *after* it (the inner + ``finally`` runs first), so a crash between the two puts can leave a fresh + draft paired with stale history. Accepted risk: that resume degrades to + the pre-snapshot behavior (a draft referencing edits that were not + restored), and the window is two consecutive store puts. + """ + version_history: list[str] + + +LAST_ATTEMPT_EDITS_KEY = CacheKey[CVLGeneration, _LastAttemptEdits]("last_attempt_edits") + + +@dataclass(frozen=True) +class _LiveJudgeHost: + """Judge construction surface for the editing pipeline: RAG tools plus the + vfs-aware read suite, so the judge reads the author's working copy (seeded + into its state per invocation via the SourceSnapshot lift) rather than the + on-disk baseline.""" + env: ServiceHost + editing: SourceEditing + + def builder_heavy(self) -> Builder[None, None, None]: + return self.env.builder_heavy() + + @property + def sort(self) -> Sort: + return self.env.sort + + @property + def judge_tools(self) -> tuple[BaseTool, ...]: + return ( + self.env.rag_tools + + tuple(self.editing.live.read_tools) + + (self.editing.live.explorer, self.editing.live.doc_tool) + ) + + +@tool_display("Getting feedback", "Feedback") +class EditorAwareFeedbackTool( + FeedbackToolBase[SourceCVLGenerationState], + WithAsyncDependencies[Command, ContextualFeedbackToolImpl[SourceSnapshot]], +): + __doc__ = FeedbackToolBase.__doc__ + + @override + async def _get_feedback( + self, spec: str, skipped: list[SkippedProperty] + ) -> PropertyFeedbackProtocol: + with self.tool_deps() as judge: + assert "vfs" in self.state + snap = SourceSnapshot( + vfs=self.state["vfs"], + version_history=self.state["version_history"], + ) + return await judge(snap, spec, skipped, self.rebuttals, self.tool_call_id) + + @override + def _version_history(self) -> Sequence[str]: + return self.state["version_history"] + _PropertyGenTemplate = TypedTemplate[PropertyGenParams]("property_generation_prompt.j2") @@ -343,6 +560,7 @@ async def batch_cvl_generation( source: SourceCode, spec_dir: Path, spec_stem: str, + editing: SourceEditing | None, ) -> BatchGeneratedCVLResult: # *spec_dir* (project-root-relative) is where the caller will persist the spec # authored here. The prover resolves the spec's CVL imports relative to its own @@ -364,55 +582,118 @@ async def batch_cvl_generation( "contract_name": source.contract_name }) + titles = [p.title for p in props] + judge_ctx = ctx.child(CVL_JUDGE_KEY) + judge_prompt = FeedbackTemplate.bind({ + "sort": "existing", + "context": component, + "source_editing": editing is not None, + }).depends(Properties) + if editing is None: + feedback_suite = property_tools( + property_feedback_judge(judge_ctx, env, judge_prompt, props) + ) + else: + judge_impl = source_feedback_judge( + judge_ctx, _LiveJudgeHost(env, editing), judge_prompt, props + ) + feedback_suite = [ + EditorAwareFeedbackTool.bind(judge_impl).as_tool("feedback_tool"), + *skip_tools(titles), + ] + # use "cache=long" to account for very long prover runs. # on anthropic (the only backend we support) a long cache is 1hr # NB that on longer prover runs we'll still get a cache miss; # this is a trade off we may have to revisit later. - task_graph = env.builder_heavy(cache_level=CacheLevel.LONG).with_tools( - env.all_tools - ).with_tools( + b = env.builder_heavy(cache_level=CacheLevel.LONG).with_tools( + env.rag_tools + ) + if editing is not None: + b = b.with_tools( + editing.live.read_tools + ).with_tools( + [editing.live.explorer, editing.live.doc_tool] + ).with_tools( + generate_edit_management_tools(ctx, env, editing.store, editing.live) + ) + else: + b = b.with_tools(env.source_tools) + task_graph = b.with_tools( static_tools() ).with_tools( - [prover_tool, ExpectRulePassage.as_tool("expect_rule_passage"), ExpectRuleFailure.as_tool("expect_rule_failure"), GiveUpTool.as_tool("give_up"), PublishResultTool.as_tool("result"), ctx.get_memory_tool()] + feedback_suite + ).with_tools( + [prover_tool, + ExpectRulePassage.as_tool("expect_rule_passage"), + ExpectRuleFailure.as_tool("expect_rule_failure"), + GiveUpTool.as_tool("give_up"), + PublishResultTool.bind(titles).as_tool("result"), + ctx.get_memory_tool()] ).with_state( SourceCVLGenerationState ).with_output_key( "result" ).with_input( SourceCVLGenerationInput - ).with_context( - FeedbackToolContext ).with_sys_prompt_template( - "property_generation_system_prompt.j2" + "property_generation_system_prompt.j2", source_editing=editing is not None ).inject( lambda d: bound_template.render_to(d.with_initial_prompt_template) - ).with_summary_config(PropertyGenerationConfig()).compile_async() - - feedback_env = property_feedback_judge( - ctx.child(CVL_JUDGE_KEY), env, FeedbackTemplate.bind({ - "sort": "existing", - "context": component - }), props - ) - - res_state = await run_cvl_generator( - ctx = ctx, - d = task_graph, - description=description, - ctxt=feedback_env, - in_state=SourceCVLGenerationInput( - curr_spec=None, - config=init_config, - spec_stem=spec_stem, - input=[], - required_validations=[FEEDBACK_VALIDATION_KEY, PROVER_VALIDATION_KEY], - rule_skips={}, - skipped=[], - property_rules=[], - validations={}, - failed=None, + ).with_summary_config( + PropertyGenerationConfig(source_editing=editing is not None) + ).compile_async() + + # Crash recovery for the working copy, sibling to cvl_generation's draft + # recovery: restore the applied-edit history and rehydrate the vfs from the + # durable edit store. Independent of whether a draft snapshot exists — a + # crash after edits but before any draft still restores the fork. + restored_history: list[str] = [] + restored_vfs: dict[str, str] = {} + resume_note: list[str | dict] = [] + if editing is not None: + prior = await ctx.child(LAST_ATTEMPT_EDITS_KEY).cache_get(_LastAttemptEdits) + if prior is not None and prior.version_history: + tail = await editing.store.read(prior.version_history[-1]) + assert tail is not None, ( + f"recovered edit {prior.version_history[-1]} absent from the edit store" + ) + restored_history = prior.version_history + restored_vfs = tail.vfs + resume_note = [ + "Source edits applied during your previous attempt at this task have " + "been restored to your working copy; use `edit_history_log` to review them." + ] + + try: + res_state = await run_cvl_generator( + ctx = ctx, + d = task_graph, + description=description, + in_state=SourceCVLGenerationInput( + curr_spec=None, + config=init_config, + input=resume_note, + required_validations=[FEEDBACK_VALIDATION_KEY, PROVER_VALIDATION_KEY], + rule_skips={}, + skipped=[], + property_rules=[], + validations={}, + failed=None, + vfs=restored_vfs, + version_history=restored_history + ) ) - ) + finally: + if editing is not None: + last_state = ( + await task_graph.aget_state({"configurable": {"thread_id": ctx.thread_id}}) + ).values + hist = last_state.get("version_history") + if hist is not None: + await ctx.child(LAST_ATTEMPT_EDITS_KEY).cache_put( + _LastAttemptEdits(version_history=list(hist)) + ) assert "result" in res_state assert res_state["failed"] is not None @@ -420,8 +701,19 @@ async def batch_cvl_generation( return GaveUp(reason=res_state["result"]) d = res_state["curr_spec"] assert d is not None + applied_edits: list[AppliedEdit] = [] + if editing is not None: + for edit_id in res_state["version_history"]: + rec = await editing.store.read(edit_id) + assert rec is not None, f"edit {edit_id} in history but absent from the edit store" + applied_edits.append(AppliedEdit( + edit_id=edit_id, + executive_summary=rec.executive_summary, + why_sound=rec.why_sound, + )) # Persist the base prover config and last run link from the final state so a later cache # hit (which skips the prover) can still reconstruct certora/confs and retain the link. + assert "vfs" in res_state return GeneratedCVL( commentary=res_state["result"], cvl=d, @@ -429,5 +721,7 @@ async def batch_cvl_generation( property_rules=res_state["property_rules"], config=res_state["config"], final_link=res_state.get("prover_link"), + vfs=res_state["vfs"], + applied_edits=applied_edits, ) diff --git a/composer/spec/source/autoprove_common.py b/composer/spec/source/autoprove_common.py index 24eb0a7e..2be2ea6d 100644 --- a/composer/spec/source/autoprove_common.py +++ b/composer/spec/source/autoprove_common.py @@ -22,8 +22,12 @@ from composer.spec.source.pipeline import ProverBackend, GeneratedCVL from composer.prover.core import make_prover_options from composer.spec.source.source_env import build_source_env +from composer.spec.source.author import SourceEditing +from composer.spec.source.live_explorer import setup_live_edits +from composer.spec.source.munge.edit_store import EditStore +from composer.spec.source.munge.edit_oracle import mk_oracle from composer.spec.source.artifacts import ProverArtifactStore -from composer.spec.agent_index import agent_index_config_from_env +from composer.spec.agent_index import AgentIndex, AgentIndexConfig, agent_index_config_from_env from composer.core.user import get_uid from composer.spec.cvl_research import DEFAULT_CVL_AGENT_INDEX_NS from composer.ui.autoprove_app import AutoProvePhase @@ -142,9 +146,33 @@ async def callback( recursion_limit=args.recursion_limit, cvl_index_config=agent_index_config_from_env(DEFAULT_CVL_AGENT_INDEX_NS), ) + # Source-editing kit: the edit snapshot store, the live (vfs-aware) + # tool suite with its versioned explorer, and the migration oracle + # that re-validates cached explorer findings across edits. The base + # index shares the frozen explorer's namespace, so pre-edit (V0) + # findings stay visible to the live explorer. + edit_store = EditStore( + staged.conns.store, user_ns("edit_snapshots", staged.root_key) + ) + editing = SourceEditing( + live=setup_live_edits( + builder=staged.llm_models.builder_lite(), + sc=staged.source, + base_store=AgentIndex( + store=staged.conns.indexed_store, + config=AgentIndexConfig(base_layer=source_data_ns), + ), + store=staged.conns.indexed_store, + source_key=staged.root_key, + oracle=mk_oracle(staged.llm_models.llm_lite(), edit_store, staged.source), + recursion_limit=args.recursion_limit, + ), + store=edit_store, + ) backend = ProverBackend( ProverArtifactStore(staged.source.project_root, staged.source.contract_name), - make_prover_options(cloud=args.cloud) + make_prover_options(cloud=args.cloud), + editing, ) return await cont(source_env, backend) yield callback diff --git a/composer/spec/source/live_explorer.py b/composer/spec/source/live_explorer.py new file mode 100644 index 00000000..ffd5366c --- /dev/null +++ b/composer/spec/source/live_explorer.py @@ -0,0 +1,229 @@ +from dataclasses import dataclass +from pathlib import PurePath +from typing_extensions import TypedDict +from typing import Annotated, Callable, Awaitable, cast, NotRequired + +from pydantic import Field + +from langchain_core.tools import BaseTool + +from langgraph.store.base import BaseStore +from langgraph.graph import MessagesState + +from graphcore.tools.vfs import VFSState, VFSInput, VFSAccessor, vfs_tools +from graphcore.tools.schemas import WithAsyncDependencies, WithInjectedId, WithInjectedState +from graphcore.graph import Builder +from graphcore.tools.results import result_tool_generator + +from composer.spec.agent_index import AgentIndex, RetrieveDocumentTool +from composer.spec.source.versioned_index import VersionedAgentIndex, MigrationOracle +from composer.spec.code_explorer import _ExploreCodeCommon, CODE_EXPLORER_SYS_PROMPT + +from composer.spec.context import SourceCode, user_data_ns +from composer.spec.util import uniq_thread_id +from composer.spec.graph_builder import run_to_completion + + + +WIPE_HISTORY = "__wipe__" +"""Sentinel for the ``version_history`` reducer: an update whose first element +is this constant *replaces* the history with the remaining elements instead of +appending. ``RevertToEdit`` uses it to truncate history back to a prior edit.""" + + +def _merge_version_history(left: list[str], right: list[str]) -> list[str]: + if right and right[0] == WIPE_HISTORY: + return right[1:] + return left + right + + +class VersionedHistory(TypedDict): + version_history: Annotated[list[str], _merge_version_history] + +class ExplorerInput(VersionedHistory, VFSState): + ... + + +type _ExplorerRunner = Callable[[VFSInput, str], Awaitable[str]] + +@dataclass +class VersionedExplorerDeps: + ind: VersionedAgentIndex + runner: _ExplorerRunner + +class LiveCodeExplorerTool( + WithAsyncDependencies[str, VersionedExplorerDeps], + WithInjectedState[ExplorerInput], + _ExploreCodeCommon, + WithInjectedId +): + __doc__ = _ExploreCodeCommon.__doc__ + + async def run(self) -> str: + with self.tool_deps() as deps: + reference = await deps.ind.asearch_versioned( + self.question, self.state["version_history"] + ) + if isinstance(reference, dict): + return AgentIndex.format_document(reference) + + search_context = VersionedAgentIndex.format_context(reference) + flow_input : list[str | dict] = [self.question, *search_context] + answer = await deps.runner(VFSInput( + input = flow_input, + vfs=self.state["vfs"] + ), self.tool_call_id) + key = await deps.ind.aput(self.question, answer, self.state["version_history"]) + if key is None: + return answer + return AgentIndex.format_document(answer, key) + +class LiveDocumentRef(WithAsyncDependencies[str, VersionedAgentIndex], WithInjectedState[VersionedHistory]): + __doc__ = cast(str, RetrieveDocumentTool.__doc__) + + ref: str = Field(description="The document reference key") + + async def run(self) -> str: + with self.tool_deps() as dep: + res = await dep.aget(self.ref, self.state["version_history"]) + if res is None: + return f"Document with reference id {self.ref} was not found" + doc = [ + f"**Question**: {res['question']}", + "", + "**Answer**:", + res["answer"] + ] + if res["caveat"] is not None: + doc.append("The above answer may no longer be entirely accurate due to" \ + f"code changes made since its creation. The following caveats apply: {res['caveat']}") + return "\n".join(doc) + +@dataclass +class LiveEditTools: + """The vfs-aware tool suite for the editing pipeline. + + ``read_tools`` are the raw primitives (get/list/grep over the working + copy): safe for any consumer whose state carries a ``vfs``. ``explorer`` + and ``doc_tool`` additionally require ``version_history`` in the consumer's + state (they key the finding cache by version), so they are separate slots — + a consumer reviewing an *uncommitted* draft (the munge feedback judge) must + take the primitives only, both because it lacks the history and because + draft-derived answers must not enter the version-keyed cache.""" + read_tools: tuple[BaseTool, ...] + write_tools: tuple[BaseTool, ...] + explorer: BaseTool + doc_tool: BaseTool + mat: VFSAccessor[VFSState] + +class _LiveExplorerState(MessagesState, VFSState): + result: NotRequired[str] + +_VERSIONED_INDEXED_SYS_PROMPT = CODE_EXPLORER_SYS_PROMPT + """ + +You may be provided with other question/answer pairs that were found to be similar +to the question you are asked. These question/answer pairs *may* have been derived +on a prior version of the codebase that you are exploring now; such pairs will be clearly +marked as being (potentially) out of date. Use the following protocol to use these +prior results effectively: + +1. If a prior finding is *not* marked as out of date, and directly answers the question you are asked, + use that answer as is; do not rephrase, re-investigate, or "verify" the answer +2. If a prior finding is *not* marked as out of date, and *partially* answers the question you are asked, + use that answer as a verified starting point and fill in any missing details. + +If a prior question/answer pair that is marked as (potentially stale) +either completely or partially answers the question posed to you, you *should* +use your source tools to determine if the substantive and relevant details of the answer +are still true on this version of the code. If you verify that these details +remain true, you may reuse (in part or in whole) the existing answer as you would +an up-to-date answer. +""" + +def _prover_output_dirs(p: PurePath) -> bool: + """Globally exclude prover outputs from the live tool surface AND the + materializer: they are never compilation inputs, and copying prior runs' + ``.certora_internal`` / ``emv-*`` trees into each prover-run + materialization would be enormously wasteful.""" + return bool(p.parts) and ( + p.parts[0] == ".certora_internal" or p.parts[0].startswith("emv-") + ) + + +def setup_live_edits( + builder: Builder[None, None, None], + sc: SourceCode, + base_store: AgentIndex, + store: BaseStore, + source_key: str, + oracle: MigrationOracle, + recursion_limit: int +) -> LiveEditTools: + x = VersionedAgentIndex( + _wrapped=base_store, + _store=store, + _target_ns=user_data_ns() + ("versioned_store", source_key), + _migration_ns=user_data_ns() + ("versioned_migration", source_key), + _migration_oracle=oracle + ) + read_tools, mat = vfs_tools({ + "forbidden_read": sc.forbidden_read, + "fs_layer": sc.project_root, + "immutable": True, + "global_exclude": _prover_output_dirs, + }, VFSState) + + write_tools, _ = vfs_tools({ + "forbidden_read": sc.forbidden_read, + 'forbidden_write': r'^.+\.spec$', + "immutable": False, + "fs_layer": sc.project_root, + "global_exclude": _prover_output_dirs, + }, VFSState) + + d = ( + builder + .with_input(VFSInput) + .with_state(_LiveExplorerState) + .with_tools(read_tools) + .with_tools([ + result_tool_generator( + "result", + (str, "Your answer to the posed question"), + "Call this tool to deliver your answer" + ) + ]) + .with_initial_prompt("Answer the following question") + .with_sys_prompt(_VERSIONED_INDEXED_SYS_PROMPT) + .with_output_key("result") + .compile_async() + ) + async def runner( + inp: VFSInput, tool_call_id: str + ) -> str: + res = await run_to_completion( + graph=d, + input=inp, + context=None, + description="Code Explorer", + recursion_limit=recursion_limit, + thread_id=uniq_thread_id("code-explorer"), + within_tool=tool_call_id + ) + assert "result" in res + return res["result"] + + explorer = LiveCodeExplorerTool.bind(VersionedExplorerDeps( + ind=x, + runner=runner + )).as_tool("code_explorer") + + doc_retriever = LiveDocumentRef.bind(x).as_tool("code_document_ref") + + return LiveEditTools( + doc_tool=doc_retriever, + mat=mat, + read_tools=tuple(read_tools), + explorer=explorer, + write_tools=tuple(write_tools) + ) diff --git a/composer/spec/source/munge/__init__.py b/composer/spec/source/munge/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/composer/spec/source/munge/compile_check.py b/composer/spec/source/munge/compile_check.py new file mode 100644 index 00000000..65914c71 --- /dev/null +++ b/composer/spec/source/munge/compile_check.py @@ -0,0 +1,153 @@ +"""Confirm that an editor agent's VFS edits still compile. + +Materializes a :class:`VFSState` into a scratch tree, runs ``certoraRun +--build_only`` over the supplied compilation config, and — if the build +succeeds — checks that every edited file was actually parsed by solc. A VFS key +that never shows up in the build's source list is an edit that doesn't reach the +compilation under verification (orphaned file, dropped import), which is as much +a failure as a hard compile error. +""" + +import json +from dataclasses import dataclass +from pathlib import Path, PurePosixPath +from typing import Any + +from graphcore.tools.vfs import VFSState, VFSAccessor +from composer.prover.core import run_prover_inner + + +@dataclass(frozen=True) +class BuildFailed: + """``certoraRun --build_only`` did not produce a clean build.""" + reason: str + + +@dataclass(frozen=True) +class EditsNotCompiled: + """The build succeeded, but ``files`` are VFS-edited paths that solc never + parsed — the edits don't reach the compilation.""" + files: frozenset[str] + + +@dataclass(frozen=True) +class EditsCompiled: + """The build succeeded and every VFS-edited file was parsed by solc.""" + touched: frozenset[str] + + +CompileCheck = BuildFailed | EditsNotCompiled | EditsCompiled + + +_CONF_NAME = "compile_check.conf" + + +def _config_paths(config: dict[str, Any]) -> set[str]: + """The file paths under ``config['files']``, stripped of any + ``:ContractName`` suffix certora allows on a file entry.""" + return {str(entry).split(":", 1)[0] for entry in config.get("files", [])} + + +def _find_build_json(folder: Path) -> Path | None: + latest = folder / ".certora_internal" / "latest" / ".certora_build.json" + if latest.exists(): + return latest + # `latest` is normally a symlink to the timestamped run dir; fall back to the + # newest run dir by name (they sort chronologically) if it's absent. + candidates = sorted(folder.glob(".certora_internal/*/.certora_build.json")) + return candidates[-1] if candidates else None + + +def _scrape_touched(build_json: Path) -> set[str]: + """Union the ``srclist`` values across every SDC in ``.certora_build.json``. + Each srclist is solc's ``sources`` map for one compilation unit — the input + file plus all transitive imports — so the union is every file the build + parsed. Paths are ``.certora_sources``-relative (the instrumented tree).""" + build = json.loads(build_json.read_text()) + touched: set[str] = set() + for sdc in build.values(): + touched.update(sdc.get("srclist", {}).values()) + return touched + + +def _strip_anchor(p: PurePosixPath) -> PurePosixPath: + """Drop everything up to and including a ``.certora_sources`` component, so a + ``.certora_sources``-relative build path can be compared to a project-relative + VFS key.""" + parts = p.parts + if ".certora_sources" in parts: + i = len(parts) - 1 - parts[::-1].index(".certora_sources") + return PurePosixPath(*parts[i + 1:]) + return p + + +def _is_touched(vfs_key: str, touched: set[str]) -> bool: + """A VFS key counts as compiled if its path is a trailing sub-path of some + touched file. Suffix matching absorbs the prefix rewriting certora applies + when it copies sources into the instrumented tree.""" + key_parts = _strip_anchor(PurePosixPath(vfs_key)).parts + n = len(key_parts) + return any( + _strip_anchor(PurePosixPath(t)).parts[-n:] == key_parts + for t in touched + ) + + +def _noop_err(code: int | None, stdout: str, stderr: str) -> None: + pass + + +async def _noop_stdout(line: str) -> None: + pass + + +async def check_edits_compile( + state: VFSState, + accessor: VFSAccessor[VFSState], + config: dict[str, Any], + files: list[str], +) -> CompileCheck: + """Build ``config`` over the materialized ``state`` and confirm the edits hold. + + ``files`` are the paths the caller expects to be compiled; every one must + appear under ``config['files']`` (a caller contract — a mismatch is a bug, + not a build outcome, so it raises). The returned :class:`CompileCheck` + distinguishes a failed build, a build that silently omits edited files, and a + clean build that parsed them all. + """ + conf_paths = _config_paths(config) + absent = [f for f in files if f not in conf_paths] + if absent: + raise ValueError( + f"files not present under config['files']: {absent}" + ) + + with accessor.materialize(state) as tmp: + folder = Path(tmp) + (folder / _CONF_NAME).write_text(json.dumps(config)) + + result, stdout = await run_prover_inner( + folder, + [_CONF_NAME, "--build_only"], + _noop_err, + _noop_stdout, + ) + + # run_prover_inner surfaces a hard subprocess failure as a str; the + # wrapper reports a build exception as a {"sort": "failure"} payload + # (it always exits 0). A clean --build_only run returns None. + if isinstance(result, str): + return BuildFailed(reason=result) + if isinstance(result, dict) and result.get("sort") == "failure": + return BuildFailed(reason=f"{result.get('exc_str', '')}\n{stdout}".strip()) + + build_json = _find_build_json(folder) + if build_json is None: + return BuildFailed(reason=f"build produced no .certora_build.json\n{stdout}".strip()) + + touched = _scrape_touched(build_json) + + missing = {k for k in state["vfs"] if not _is_touched(k, touched)} + if missing: + return EditsNotCompiled(files=frozenset(missing)) + return EditsCompiled(touched=frozenset(touched)) diff --git a/composer/spec/source/munge/edit_oracle.py b/composer/spec/source/munge/edit_oracle.py new file mode 100644 index 00000000..498d3a12 --- /dev/null +++ b/composer/spec/source/munge/edit_oracle.py @@ -0,0 +1,101 @@ +import pathlib + +from pydantic import BaseModel, Field + +from langchain_core.messages import HumanMessage, SystemMessage +from langchain_core.language_models.chat_models import BaseChatModel + +from .edit_store import EditStore +from .vfs_diff import compute_diff +from composer.spec.source.versioned_index import ( + MigrationOracle, + AnswerPortability, + Stale, + UpToDate, +) +from composer.spec.context import SourceCode + + +_ORACLE_SYSTEM = """\ +You judge whether a previously recorded finding about smart-contract source code is still accurate after the source was edited. + +You are given the finding (the original question and the answer that was recorded) and a unified diff from the source version the finding was written against to the current version. + +Decide whether anything in the diff contradicts or outdates the answer. If every claim the answer makes still holds against the changed source, it is still valid. If the diff changes something the answer depends on — a moved or renamed symbol, altered control flow, a removed branch, a changed signature — it is no longer valid, and you say in one sentence what changed. + +Edits are usually small and surgical, so most findings are unaffected; mark a finding invalid only when the diff actually touches what the answer relies on.""" + + +class _PortabilityVerdict(BaseModel): + still_holds: bool = Field( + description="True if every claim in the prior answer is still accurate against " + "the changed source; False if the diff makes any part of it wrong, stale, or misleading." + ) + reason: str = Field( + default="", + description="When still_holds is False, one sentence naming the change that invalidates " + "the answer. Left empty when it still holds.", + ) + + +def mk_oracle( + llm: BaseChatModel, + edit_store: EditStore, + sc: SourceCode, +) -> MigrationOracle: + """Build a :class:`MigrationOracle` that decides, in one LLM call, whether a + recorded finding survives the edits between two source versions. + + The VFS is a union overlay over the base ``fs_layer``: a version snapshot holds + only the files edited as of that version, and every other path reads through to + ``sc.project_root`` on disk. So the ``new`` side is the ``end_version`` overlay, + and ``old`` resolves each path as overlay-then-base — or, for V0 + (``start_version is None``), the base fs_layer alone.""" + + async def oracle( + *, + start_version: str | None, + end_version: str, + question: str, + answer: str, + ) -> AnswerPortability: + new = await edit_store.read(end_version) + assert new is not None, f"end version {end_version!r} absent from edit store" + + root = pathlib.Path(sc.project_root) + start = None if start_version is None else await edit_store.read(start_version) + overlay = None if start is None else start.vfs + + def old(path: str) -> str | None: + # Union FS: an edited path uses the overlay's content, everything else + # reads through to the base fs_layer under project_root. + if overlay is not None and path in overlay: + return overlay[path] + try: + return (root / path).read_text(encoding="utf-8") + except (OSError, UnicodeDecodeError): + return None + + diff = compute_diff(old, new.vfs) + if not diff: + # Nothing observable changed between the two views, so no edit we can + # see could have invalidated the finding. + return UpToDate(status="ok") + + user = ( + f"Prior finding recorded about the source code.\n\n" + f"Question: {question}\n\n" + f"Answer:\n{answer}\n\n" + f"Unified diff from the version this finding was written against to the " + f"current version:\n\n{diff}" + ) + verdict = await llm.with_structured_output(_PortabilityVerdict).ainvoke( + [SystemMessage(_ORACLE_SYSTEM), HumanMessage(user)] + ) + assert isinstance(verdict, _PortabilityVerdict) + + if verdict.still_holds: + return UpToDate(status="ok") + return Stale(status="stale", reason=verdict.reason) + + return oracle diff --git a/composer/spec/source/munge/edit_store.py b/composer/spec/source/munge/edit_store.py new file mode 100644 index 00000000..511e0b61 --- /dev/null +++ b/composer/spec/source/munge/edit_store.py @@ -0,0 +1,52 @@ +from dataclasses import dataclass +import hashlib +from typing import cast +from langgraph.store.base import BaseStore + + +@dataclass(frozen=True) +class StoredEdit: + """A committed edit: the full VFS snapshot plus the editor's account of it. + The description fields ride into the edit-history log and the final + deliverable, so a reader can tell why the source was changed without + reconstructing the diff.""" + vfs: dict[str, str] + executive_summary: str + why_sound: str + + +@dataclass +class EditStore: + _store: BaseStore + _target_ns: tuple[str, ...] + + async def read(self, id: str) -> StoredEdit | None: + res = await self._store.aget(self._target_ns, id) + if res is None: + return None + v = res.value + return StoredEdit( + vfs=cast(dict[str, str], v["vfs"]), + executive_summary=cast(str, v["executive_summary"]), + why_sound=cast(str, v["why_sound"]), + ) + + @classmethod + def _deterministic_hash(cls, vfs: dict[str, str]) -> str: + sorted_keys = sorted(vfs.keys()) + hasher = hashlib.sha256() + for nm in sorted_keys: + hasher.update(vfs[nm].encode("utf-8")) + hasher.update(b'\0') + return hasher.hexdigest() + + async def commit( + self, vfs: dict[str, str], *, executive_summary: str, why_sound: str + ) -> str: + id = self._deterministic_hash(vfs) + await self._store.aput(self._target_ns, id, { + "vfs": {**vfs}, + "executive_summary": executive_summary, + "why_sound": why_sound, + }) + return id diff --git a/composer/spec/source/munge/munge_agent.py b/composer/spec/source/munge/munge_agent.py new file mode 100644 index 00000000..8ae1f087 --- /dev/null +++ b/composer/spec/source/munge/munge_agent.py @@ -0,0 +1,426 @@ +from dataclasses import dataclass +from typing import NotRequired, Any, Callable, Awaitable, override, Protocol, Iterable +from typing_extensions import TypedDict +from pydantic import BaseModel, Field + + +from langgraph.graph import MessagesState +from langgraph.types import Command + +from langchain_core.tools import BaseTool +from langchain_core.messages import ToolMessage + +from .edit_store import EditStore +from .vfs_diff import summarize_changes +from .compile_check import check_edits_compile, BuildFailed, EditsNotCompiled + +from graphcore.graph import FlowInput +from graphcore.tools.vfs import VFSState, VFSAccessor, VFSInput +from graphcore.tools.schemas import ( + WithAsyncDependencies, WithImplementation, WithInjectedState, WithInjectedId, +) +from composer.spec.context import WorkflowContext, CVLGeneration, CacheKey, EditorAgent, EditorJudge +from composer.spec.service_host import ServiceHost +from composer.spec.graph_builder import run_to_completion, bind_standard +from composer.spec.util import uniq_thread_id +from composer.tools.thinking import RoughDraftState, get_rough_draft_tools + +class MungerStateExtra(VFSState): + did_read: bool + memory: str | None + orig_vfs: dict[str, str] + compile_conf: dict + # The author's problem statement, piped through to the reviewer so it can + # judge whether the edits stay on script. + request: str + # Hash of the VFS the reviewer approved. submit_edit only fires when this + # matches the current VFS hash, so any edit after approval silently voids it — + # the editor can't get a review and then sneak in further changes. + reviewed_digest: str | None + +class CommonMungeDescription( + BaseModel +): + """A holistic description of your changes""" + executive_summary: str = Field(description="An executive summary of your changes, fully covering each part of the diff with the existing source code") + + how_to_apply: str | None = Field(description="What changes might need to be made by the upstream verification author to make effective use of your changes") + + why_sound: str = Field(description="A precise, reasoned argument why your changes are *either* sound, OR an acceptable over-approximation") + +class MungeDescription( + CommonMungeDescription +): + """A holistic description of your changes & any extra entry points you added""" + added_files: list[str] = Field(description="A manifest of files you added that should be added to the compilation steps. Empty if no files were added") + +class MungeRefusal(BaseModel): + """ + A structured description of why you are refusing to make the requested edits + """ + explanation: str = Field(description="A concise description of why you are refusing to make the edit or why such an edit is not possible.") + +class MungerAgentInput(MungerStateExtra, VFSInput): + ... + +class MungerAgentState(MungerStateExtra, MessagesState): + result: NotRequired[MungeDescription | MungeRefusal] + +@dataclass +class MungeToolDeps: + graph_runner: Callable[[MungerAgentInput, str], Awaitable[MungerAgentState]] + edit_store: EditStore + accessor: VFSAccessor[VFSState] + +class MungeStateDeps(TypedDict): + config: dict + vfs: dict[str, str] + +class EditMungeTool(WithAsyncDependencies[str, MungeToolDeps], WithInjectedId, WithInjectedState[MungeStateDeps]): + """ + Call this tool to request for a dedicated agent to make small, + targeted changes to the source code under verification. You should invoke this + tool only after exhausting other plausible strategies. + + You are *not* responsible for telling the agent what edits to make. + Rather you must describe the problem you are hoping to solve by edits made + by the agent. + + Good request: "The inline assembly access in `readStoreData()` is crashing the prover. Can you rewrite it to use standard Solidity?" + Good request: "The iterative computation of sqrt inlined in `computePriceCurve()` needs to be summarized to avoid a timeout, can you refactor it into + a standalone function" + Bad request: "Add the following line to the beginning of `transferAdmin()`: `require(msg.sender == address(this))`" + Bad request: "Delete the body of `compoundInterest()`, it's too difficult for the prover." + """ + request: str = Field(description="A short, concise, natural language request for an edit; it must include the problem" \ + "you're trying to solve, and the intended 'shape' of the solution.") + + @override + async def run(self) -> str: + with self.tool_deps() as deps: + agent_input = MungerAgentInput( + input=[self.request], + request=self.request, + orig_vfs=self.state["vfs"].copy(), + did_read=False, + memory=None, + compile_conf=self.state["config"], + vfs=self.state["vfs"].copy(), + reviewed_digest=None, + ) + res = await deps.graph_runner( + agent_input, self.tool_call_id + ) + assert "result" in res + d = res["result"] + if isinstance(d, MungeRefusal): + return f"The editor refused your request with the following reason:\n\n{d.explanation}" + + application_key = await deps.edit_store.commit( + res["vfs"], + executive_summary=d.executive_summary, + why_sound=d.why_sound, + ) + diff = summarize_changes( + res, deps.accessor, self.state["vfs"] + ) + result_msg = f""" +The editor finished responding to your request. + +**Executive Summary**: +{d.executive_summary} + +**Soundness Argument**: +{d.why_sound} + +**Integration notes**: +{"(None provided)" if not d.how_to_apply else d.how_to_apply} + +You can apply this edit to your working source by calling `commit_edit({application_key})` + +----- + +The diff of the edit is as follows: + +{diff} +""" + return result_msg + +class EditToolsHost( + Protocol +): + @property + def write_tools(self) -> Iterable[BaseTool]: ... + + @property + def read_tools(self) -> Iterable[BaseTool]: ... + + @property + def mat(self) -> VFSAccessor[VFSState]: ... + +EDITOR_KEY = CacheKey[CVLGeneration, EditorAgent]("editor") +JUDGE_KEY = CacheKey[EditorAgent, EditorJudge]("judge") + + +# --------------------------------------------------------------------------- +# Feedback judge +# --------------------------------------------------------------------------- + +class MungeFeedback(BaseModel): + """The reviewer's verdict on the proposed edits.""" + good: bool = Field(description="Whether the edits are acceptable as-is, or need more work.") + feedback: str = Field(description="Actionable feedback if work is needed; may be empty when the edits are good.") + + +class MungeFeedbackState(RoughDraftState, VFSState, MessagesState): + result: NotRequired[MungeFeedback] + + +class MungeFeedbackInput(FlowInput, RoughDraftState, VFSState): + pass + + +# (current vfs, review parts, calling tool_call_id) -> verdict +MungeFeedbackThunk = Callable[[dict[str, str], list[str | dict], str], Awaitable[MungeFeedback]] + + +def munge_feedback_judge( + ctx: WorkflowContext[EditorAgent], + env: ServiceHost, + edit_tools: "EditToolsHost", +) -> MungeFeedbackThunk: + """Build the editor's feedback judge. Its read-only VFS tools inspect the + *editor's* current VFS: the caller seeds that VFS into the judge's own state + at invocation time (see ``the_tool``), so the judge reviews the edited source + rather than the on-disk baseline.""" + feedback_ctx = ctx.child(JUDGE_KEY) + + rough_draft_tools = get_rough_draft_tools(MungeFeedbackState) + + def did_rough_draft_read(s: MungeFeedbackState, _: MungeFeedback) -> str | None: + if not s["did_read"]: + return "Completion REJECTED: never read rough draft for review" + return None + + workflow = bind_standard( + env.builder_heavy(), MungeFeedbackState, validator=did_rough_draft_read + ).with_input( + MungeFeedbackInput + ).with_sys_prompt_template( + "munge_feedback_system.j2" + ).with_initial_prompt_template( + "munge_feedback_prompt.j2" + ).with_tools( + [*rough_draft_tools, feedback_ctx.get_memory_tool(), *edit_tools.read_tools] + ).compile_async() + + async def the_tool( + vfs: dict[str, str], + review: list[str | dict], + within_tool: str, + ) -> MungeFeedback: + res = await run_to_completion( + workflow, + MungeFeedbackInput(input=review, vfs=vfs, memory=None, did_read=False), + thread_id=uniq_thread_id("munge-feedback"), + recursion_limit=ctx.recursion_limit, + description="Editor feedback judge", + within_tool=within_tool, + ) + assert "result" in res + return res["result"] + + return the_tool + + +# --------------------------------------------------------------------------- +# Completion tools +# --------------------------------------------------------------------------- + +class GiveUpTool(WithInjectedId, WithImplementation[Command]): + """ + Abandon the edit request. Use this only when the requested change is + impossible or cannot be made soundly — explain why in the caller's terms. + """ + explanation: str = Field(description="Why the requested edit cannot or should not be made.") + + @override + def run(self) -> Command: + return Command(update={ + "result": MungeRefusal(explanation=self.explanation), + "messages": [ToolMessage(tool_call_id=self.tool_call_id, content="Acknowledged.")], + }) + + +class ReviewStateSlice(VFSState): + orig_vfs: dict[str, str] + request: str + + +@dataclass +class ReviewDeps: + accessor: VFSAccessor[VFSState] + feedback: MungeFeedbackThunk + + +class RequestReviewTool( + WithAsyncDependencies[Command, ReviewDeps], + WithInjectedId, + WithInjectedState[ReviewStateSlice], +): + """ + Ask the reviewer to evaluate your current edits. The reviewer inspects the + edited source and the diff and either approves it or hands back feedback to + address. You must earn an approving review before you can submit — and the + approval is tied to the exact edits you have now, so any further change voids + it and you must request review again. + """ + summary: CommonMungeDescription = Field(description="A holistic description of the changes you want reviewed.") + + def _review(self, diff: str) -> list[str | dict]: + parts: list[str | dict] = [ + f"The author's original request to the editor:\n\n{self.state['request']}", + "The editor proposes the following changes to the source under verification.", + f"Executive summary:\n{self.summary.executive_summary}", + f"Soundness argument:\n{self.summary.why_sound}", + ] + if self.summary.how_to_apply: + parts.append(f"Integration notes:\n{self.summary.how_to_apply}") + parts.append("The diff of the edit:") + parts.append(diff) + return parts + + @override + async def run(self) -> Command: + with self.tool_deps() as deps: + current: VFSState = {"vfs": self.state["vfs"]} + diff = summarize_changes(current, deps.accessor, self.state["orig_vfs"]) + verdict = await deps.feedback(self.state["vfs"], self._review(diff), self.tool_call_id) + if verdict.good: + # Stamp the hash of exactly what was approved; submit_edit checks it + # against the live VFS, so a later edit invalidates the approval. + digest = EditStore._deterministic_hash(self.state["vfs"]) + body = "The reviewer approved these edits. You may now submit_edit (do not change anything first)." + else: + digest = None + body = f"The reviewer has feedback you must address:\n\n{verdict.feedback}" + return Command(update={ + "reviewed_digest": digest, + "messages": [ToolMessage(tool_call_id=self.tool_call_id, content=body)], + }) + + +class SubmitStateSlice(VFSState): + compile_conf: dict + reviewed_digest: str | None + + +@dataclass +class SubmitDeps: + accessor: VFSAccessor[VFSState] + + +class SubmitEditTool( + WithAsyncDependencies[Command | str, SubmitDeps], + WithInjectedId, + WithInjectedState[SubmitStateSlice], +): + """ + Submit your finished edits. Accepted only if an approving request_review is + still current for these exact edits AND they compile with every added/edited + file reached by the build. On failure you get the reason back and should keep + working; this tool does not end your turn on failure. + """ + summary: MungeDescription = Field(description="A holistic description of your completed changes.") + + @override + async def run(self) -> Command | str: + if self.state["reviewed_digest"] != EditStore._deterministic_hash(self.state["vfs"]): + return ( + "These edits have not been approved as they stand. Call request_review " + "on your current edits first — any change since your last review voids " + "the approval." + ) + with self.tool_deps() as deps: + current: VFSState = {"vfs": self.state["vfs"]} + + # The added files must join the build's file set for coverage to pass. + conf = dict(self.state["compile_conf"]) + conf_files = list(conf.get("files", [])) + for f in self.summary.added_files: + if f not in conf_files: + conf_files.append(f) + conf["files"] = conf_files + + check = await check_edits_compile( + current, deps.accessor, conf, self.summary.added_files + ) + if isinstance(check, BuildFailed): + return ( + "Your edits do not build; fix them before submitting.\n\n" + f"{check.reason}" + ) + if isinstance(check, EditsNotCompiled): + return ( + "The build succeeded but these edited files were never parsed by " + "the compiler, so your changes don't reach the verification. Wire " + f"them in (or list them in added_files): {sorted(check.files)}" + ) + + return Command(update={ + "result": self.summary, + "messages": [ToolMessage(tool_call_id=self.tool_call_id, content="Edits accepted.")], + }) + + +def editor_tool( + ctx: WorkflowContext[CVLGeneration], + edit_store: EditStore, + edit_tools: EditToolsHost, + env: ServiceHost +) -> BaseTool: + editor_ctx = ctx.child(EDITOR_KEY) + + feedback = munge_feedback_judge(editor_ctx, env, edit_tools) + request_review = RequestReviewTool.bind(ReviewDeps( + accessor=edit_tools.mat, + feedback=feedback, + )).as_tool("request_review") + submit = SubmitEditTool.bind(SubmitDeps( + accessor=edit_tools.mat, + )).as_tool("submit_edit") + give_up = GiveUpTool.as_tool("give_up") + + b = ( + env + .builder_heavy() + .with_input(MungerAgentInput) + .with_state(MungerAgentState) + .with_output_key("result") + .with_sys_prompt_template("munge_editor_system.j2") + .with_initial_prompt("Respond to the following edit request:") + .with_tools(edit_tools.write_tools) + .with_tools([editor_ctx.get_memory_tool(), request_review, submit, give_up]) + .compile_async() + ) + + async def runner(inp: MungerAgentInput, tid: str) -> MungerAgentState: + return await run_to_completion( + graph=b, + context=None, + description="Code Editor Agent", + input=inp, + recursion_limit=ctx.recursion_limit, + within_tool=tid, + thread_id=uniq_thread_id("code-editor") + ) + + return EditMungeTool.bind(MungeToolDeps( + accessor=edit_tools.mat, + edit_store=edit_store, + graph_runner=runner + )).as_tool("code_editor") + +__all__ = [ + "editor_tool" +] \ No newline at end of file diff --git a/composer/spec/source/munge/vfs_diff.py b/composer/spec/source/munge/vfs_diff.py new file mode 100644 index 00000000..c9ea2410 --- /dev/null +++ b/composer/spec/source/munge/vfs_diff.py @@ -0,0 +1,61 @@ +"""Unified-diff core shared between the migration oracle and change summaries. + +The diff is always computed the same way: an ``old`` resolver that answers "what +was at this path in the baseline view" plus the ``new`` overlay whose keys are the +edited files. Iterating the overlay is sufficient because VFS overlays only +accumulate — there is no delete-file tool — so a path missing from ``old`` is an +addition, never a deletion. +""" + +import difflib +from typing import Callable + +from graphcore.tools.vfs import VFSState, VFSAccessor + + +def file_diff(path: str, old: str | None, new: str) -> str: + """Unified diff for a single file. ``old`` is ``None`` when the path isn't in + the baseline view (an addition); identical content yields the empty string.""" + if old == new: + return "" + old_lines = (old or "").splitlines(keepends=True) + new_lines = new.splitlines(keepends=True) + from_label = f"a/{path}" if old is not None else "/dev/null" + return "".join( + difflib.unified_diff(old_lines, new_lines, fromfile=from_label, tofile=f"b/{path}") + ) + + +def compute_diff(old: Callable[[str], str | None], new: dict[str, str]) -> str: + """Diff the ``old`` resolver against every path in the ``new`` overlay, + concatenating the per-file unified diffs and dropping the unchanged files.""" + chunks = (file_diff(path, old(path), content) for path, content in new.items()) + return "".join(c for c in chunks if c) + + +def _decode(raw: bytes | None) -> str | None: + if raw is None: + return None + try: + return raw.decode("utf-8") + except UnicodeDecodeError: + return None + + +def summarize_changes( + state: VFSState, + accessor: VFSAccessor[VFSState], + original: dict[str, str], +) -> str: + """Summarize the edits in ``state`` relative to ``original`` as a unified diff. + + ``original`` is a baseline VFS overlay; the ``accessor`` resolves any path it + doesn't carry through to the base fs_layer, so the comparison is against the + original *view* (overlay over base), not just the overlay. Only the files + edited in ``state`` (its overlay keys) are diffed.""" + baseline: VFSState = {"vfs": original} + + def old(path: str) -> str | None: + return _decode(accessor.get(baseline, path)) + + return compute_diff(old, state["vfs"]) diff --git a/composer/spec/source/pipeline.py b/composer/spec/source/pipeline.py index c6ac5120..781c241a 100644 --- a/composer/spec/source/pipeline.py +++ b/composer/spec/source/pipeline.py @@ -42,8 +42,8 @@ from composer.spec.source.summarizer import setup_summaries from composer.spec.source.struct_invariant import get_invariant_formulation from composer.spec.source.autosetup import SetupSuccess -from composer.spec.source.prover import get_prover_tool -from composer.spec.source.author import batch_cvl_generation +from composer.spec.source.prover import get_prover_tool, materializing_project +from composer.spec.source.author import batch_cvl_generation, SourceEditing from composer.spec.source.artifacts import ProverArtifactStore, ComponentSpec, InvariantSpec from composer.spec.source.report_prover import make_prover_fetcher from composer.spec.source.report.collect import ReportComponentInput, Verdict, VerdictFetcher @@ -108,6 +108,7 @@ class ProverRunner(Formalizer[GeneratedCVL]): _resources: list[CVLResource] _invariant: tuple[list[PropertyFormulation], Delivered[GeneratedCVL]] | None _fetch: VerdictFetcher[GeneratedCVL] + _editing: SourceEditing @override async def formalize( @@ -129,7 +130,8 @@ async def formalize( description=label, source=run.source, spec_dir=SPECS_DIR, - spec_stem=ComponentSpec(feat.slugified_name).stem + spec_stem=ComponentSpec(feat.slugified_name).stem, + editing=self._editing, ) @override @@ -173,6 +175,7 @@ class ProverPrepared(PreparedSystem[GeneratedCVL]): _prover_tool: BaseTool _prover_opts: ProverOptions _analyzed: SourceApplication + _editing: SourceEditing @override async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedCVL]: @@ -183,7 +186,7 @@ async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedC ) invariant: tuple[list[PropertyFormulation], Delivered[GeneratedCVL]] | None = None - if invariants.inv: + if invariants.inv and False: inv_props = [ PropertyFormulation(title=inv.name, description=inv.description, sort="invariant") for inv in invariants.inv @@ -208,7 +211,12 @@ async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedC description="Structural invariant CVL", source=run.source, spec_dir=SPECS_DIR, - spec_stem=InvariantSpec().stem + spec_stem=InvariantSpec().stem, + # Invariants are assumed as preconditions by every + # downstream spec, so they must hold against the + # unedited source: no editor, frozen source tools, + # immutable-source judge. + editing=None, ), ) if isinstance(inv_result, GaveUp): @@ -233,7 +241,7 @@ async def prepare_formalization(self, run: PipelineRun) -> Formalizer[GeneratedC return ProverRunner( GeneratedCVL, "prover", self._store, self._prover_tool, setup_config.prover_config, resources, invariant, - make_prover_fetcher(), + make_prover_fetcher(), self._editing, ) async def _autosetup(self, run: PipelineRun) -> tuple[SetupSuccess, list[CVLResource]]: @@ -284,6 +292,7 @@ class ProverBackend: artifact_store: ProverArtifactStore _prover_opts: ProverOptions + editing: SourceEditing async def prepare_system( self, analyzed: SourceApplication, run: PipelineRun[AutoProvePhase, None], @@ -293,14 +302,18 @@ async def prepare_system( lambda: run_harness_creation(run.ctx, run.source, run.env, analyzed), ) harnessed = _lift_harnessed(analyzed, sys_desc) + # The materializing strategy covers every phase with one tool: an empty + # VFS (invariants, or an author that never edited) runs in-situ; a + # non-empty one runs in a temp materialization of the working copy. prover_tool = get_prover_tool( - run.env.llm_heavy(), run.source.contract_name, run.source.project_root, + run.env.llm_heavy(), run.source.contract_name, + materializing_project(run.source.project_root, self.editing.live.mat), prover_opts=self._prover_opts, ) return ProverPrepared( main_instance(harnessed, run.source), self.artifact_store, sys_desc, harnessed, prover_tool, - self._prover_opts, analyzed, + self._prover_opts, analyzed, self.editing, ) def to_artifact_id(self, c: ContractComponentInstance) -> ComponentSpec: diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index f6715372..3fc3a26f 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -12,11 +12,17 @@ import json import logging import time -from contextlib import contextmanager, nullcontext +from contextlib import contextmanager, asynccontextmanager, ExitStack, nullcontext from pathlib import Path -from typing import Annotated, Callable, Iterator, override, AsyncContextManager +from typing import ( + Annotated, AsyncIterator, Callable, Iterator, override, AsyncContextManager, +) from typing_extensions import TypedDict, NotRequired +from graphcore.tools.vfs import VFSAccessor, VFSState + +from composer.spec.source.live_explorer import VersionedHistory + from langchain_core.tools import InjectedToolCallId, tool, BaseTool from langgraph.prebuilt import InjectedState from pydantic import BaseModel, Field @@ -86,10 +92,20 @@ class ProverStateExtra(TypedDict): # Basename the spec is materialized/persisted under (e.g. "autospec_"). # NotRequired so other ProverStateExtra injectors (e.g. config_edit) needn't set it. spec_stem: NotRequired[str] + # The author's working copy of the source under verification; verify_spec runs + # against its materialization when non-empty (see ProjectDirectory). Absent/empty + # outside the editing-enabled pipeline. No merge op intentionally: the vfs is + # only ever replaced wholesale (commit_edit / revert_to_edit). + vfs: NotRequired[dict[str, str]] type ProverEvents = CEXAnalysisStart | CloudPollingEvent | ProverOutputEvent | RuleAnalysisResult | ProverRun | ProverLink | ProverResult -class StateWithSkips(CVLGenerationState, ProverStateExtra): +# ``verify_spec`` only runs in the source pipeline, whose state always seeds +# ``version_history`` — permanently empty in phases without the edit tools +# (structural invariants, never-edited authors), in which case it contributes +# nothing to the digest. The prover's validation stamp is bound to it so a +# post-run edit invalidates the stamp. +class StateWithSkips(CVLGenerationState, ProverStateExtra, VersionedHistory): pass class _SpecCallbacks(ProverEventCallbacks): @@ -211,10 +227,48 @@ async def __aexit__(self, exc_type, exc, tb): return ToRet() + +type ProjectDirectory = Callable[[dict[str, str]], AsyncContextManager[str]] +"""Per-run choice of the directory the prover executes in, given the author's +current VFS overlay. Yields the directory path; its lifetime is the run.""" + + +def in_situ_project(project_root: str) -> ProjectDirectory: + """The no-editing strategy: every run executes directly in the project + directory.""" + @asynccontextmanager + async def provide(vfs: dict[str, str]) -> AsyncIterator[str]: + yield project_root + return provide + + +def materializing_project( + project_root: str, accessor: VFSAccessor[VFSState] +) -> ProjectDirectory: + """The editing strategy: an empty VFS runs in-situ; a non-empty VFS is + materialized over the project into a temporary directory that lives for + the duration of the run. The copy (and the teardown) run in a worker + thread — materializing a whole project is blocking IO that would + otherwise stall every concurrently-streaming batch.""" + @asynccontextmanager + async def provide(vfs: dict[str, str]) -> AsyncIterator[str]: + if not vfs: + yield project_root + return + stack = ExitStack() + tmp = await asyncio.to_thread( + stack.enter_context, accessor.materialize({"vfs": vfs}) + ) + try: + yield tmp + finally: + await asyncio.to_thread(stack.close) + return provide + def get_prover_tool( llm: LLM, main_contract: str, - project_root: str, + project_directory: ProjectDirectory, prover_opts: ProverOptions, ) -> BaseTool: sem = _prover_sem(prover_opts.cloud) @@ -235,7 +289,8 @@ async def verify_spec( state: Annotated[StateWithSkips, InjectedState], rules: list[str] | None = None ) -> str | Command: - if state["curr_spec"] is None: + spec = state["curr_spec"] + if spec is None: return "Specification not yet put on VFS" conf = state["config"] # With a seeded stem, name the spec/conf after it (so on-disk names match the @@ -243,8 +298,9 @@ async def verify_spec( spec_stem = state.get("spec_stem") conf_dir = (CERTORA_DIR / "confs") if spec_stem is not None else CERTORA_DIR lock = spec_locks.setdefault(spec_stem, asyncio.Lock()) if spec_stem is not None else nullcontext() - async with lock: - with tmp_spec(root=project_root, content=state["curr_spec"], name=spec_stem) as generated: + + async def run_in(run_root: str) -> str | Command: + with tmp_spec(root=run_root, content=spec, name=spec_stem) as generated: config = prover_config_overlay( conf, main_contract=main_contract, verify_target=f"{main_contract}:{generated}" ) @@ -255,7 +311,7 @@ async def verify_spec( summary = get_run_summary() with temp_certora_file( - root=project_root, + root=run_root, content=json.dumps(config, indent=2), ext="conf", name=spec_stem, @@ -264,7 +320,7 @@ async def verify_spec( ) as config_path: async with sem: result = await run_prover( - Path(project_root), + Path(run_root), [config_path], tool_call_id, prover_opts, @@ -284,10 +340,17 @@ async def verify_spec( if rules is None and all_verified: return tool_state_update( tool_call_id=tool_call_id, content=result.result_str, - prover_link=result.link, validations=stamper(state), + prover_link=result.link, + validations=stamper(state, state["version_history"]), ) return tool_state_update( tool_call_id=tool_call_id, content=result.result_str, prover_link=result.link ) + # The author's working copy decides where this run executes (in-situ for + # an empty VFS, a temp materialization otherwise); the same-stem lock + # guards the deterministic spec/conf names within it. + async with lock, project_directory(state.get("vfs") or {}) as run_root: + return await run_in(run_root) + return verify_spec diff --git a/composer/spec/source/versioned_index.py b/composer/spec/source/versioned_index.py new file mode 100644 index 00000000..f94cc1dc --- /dev/null +++ b/composer/spec/source/versioned_index.py @@ -0,0 +1,246 @@ +from dataclasses import dataclass + +from pydantic import Discriminator + +from typing import cast, Literal, Protocol, Annotated + +from typing_extensions import TypedDict + +from langgraph.store.base import BaseStore + +from composer.spec.agent_index import AgentIndex, IndexedAgentResult, KeyedAgentResult, AgentResult, AgentIndexBase +from composer.spec.util import string_hash + +class VersionedSearchResult(IndexedAgentResult): + stale: bool + +class VersionedResult(AgentResult): + version_key: str + +class VersionedRetrievalResult(AgentResult): + caveat: str | None + +class UpToDate(TypedDict): + status: Literal["ok"] + +class Stale(TypedDict): + status: Literal["stale"] + reason: str + +type AnswerPortability = Annotated[Stale | UpToDate, Discriminator("status")] + +class MigrationOracle(Protocol): + async def __call__( + self, + *, + start_version: str | None, # none means "from start" + end_version: str, + question: str, + answer: str + ) -> AnswerPortability: + ... + +@dataclass +class VersionedAgentIndex(AgentIndexBase): + _wrapped: AgentIndex + + _store: BaseStore + + _target_ns: tuple[str, ...] + _migration_ns: tuple[str, ...] + + _migration_oracle: MigrationOracle + + @classmethod + def _lift(cls, to_lift: list[IndexedAgentResult] | KeyedAgentResult) -> list[VersionedSearchResult] | KeyedAgentResult: + if not isinstance(to_lift, list): + return to_lift + return [ + { **i, "stale": False } for i in to_lift + ] + + @classmethod + def _versioned_key( + cls, question: str, version: str + ) -> str: + # ``string_hash`` already returns a 16-char digest; do NOT slice it + # further (a leftover ``[18:]`` sliced it to the empty string, so every + # versioned entry collided at key ""). + return string_hash(f"{question}|{version}") + + async def asearch_versioned( + self, question: str, version_list: list[str] + ) -> list[VersionedSearchResult] | KeyedAgentResult: + if len(version_list) == 0: + return self._lift(await self._wrapped.asearch(question)) + + key_v = self._versioned_key(question, version_list[-1]) + + res = await self._store.aget(self._target_ns, key_v) + if res is not None: + to_ret : KeyedAgentResult = { + "ref_string": key_v, + **cast(AgentResult, res.value) + } + return to_ret + + seen : set[str] = set() + v0_query = self._wrapped._raw_search(question) + version_queries = [ + self._store.asearch(self._target_ns, query=question, filter={ + "version_key": version + }) for version in version_list + ] + context : list[VersionedSearchResult] = [] + async for res in self.parallel_search(*[*v0_query, *version_queries]): + if res.key in seen: + continue + if "version_key" not in res.value: + known_migration = await self.migration_for(res.key, None, version_list[-1]) + stale = True + if known_migration is not None: + stale = known_migration["status"] == "stale" + # v0, base case + context.append({ + "stale": stale, + **cast(AgentResult, res.value), + "ref_string": res.key, + "score": cast(float, res.score) + }) + else: + cached_version = cast(VersionedResult, res.value) + stale = cached_version['version_key'] != version_list[-1] + if stale: + known_migration = await self.migration_for(res.key, cached_version["version_key"], version_list[-1]) + if known_migration is not None: + stale = known_migration["status"] == "stale" + + context.append({ + "stale": stale, + "score": cast(float, res.score), + "ref_string": res.key, + "question": cached_version["question"], + "answer": cached_version["answer"] + }) + seen.add(res.key) + if len(context) == 5: + break + return context + + @classmethod + def _migration_key(cls, doc_key: str, v1: str | None, v2: str) -> str: + return f"{doc_key}|{v1}|{v2}" + + async def migration_for(self, key: str, v1: str | None, v2: str) -> AnswerPortability | None: + cached = await self._store.aget(self._migration_ns, self._migration_key(key, v1, v2)) + if cached is None: + return None + return cast(AnswerPortability, cached.value) + + @classmethod + def _caveat(cls, s: AnswerPortability) -> str | None: + return None if s["status"] == "ok" else s["reason"] + + async def migrate_answer( + self, key: str, result: AgentResult, start_ver: str | None, versions: list[str] + ) -> str | None: + canon_start = start_ver + i = len(versions) - 1 + while i >= 0 and versions[i] != start_ver: + # check migration range from start_ver to curr + migration = await self.migration_for( + key, canon_start, versions[i] + ) + if migration is None: + i -= 1 + continue + if migration is not None and i == len(versions) - 1: + return self._caveat(migration) + elif migration["status"] == "stale": + # reclassify from initial answer state scratch + break + else: + assert migration["status"] == "ok" + canon_start = versions[i] + break + migration_res = await self._migration_oracle( + start_version=canon_start, + end_version=versions[-1], + answer=result["answer"], + question=result["question"] + ) + await self._store.aput(self._migration_ns, self._migration_key( + key, canon_start, versions[-1] + ), { **migration_res }) + return self._caveat(migration_res) + + async def aget(self, key: str, versions: list[str]) -> VersionedRetrievalResult | None: + res = await self._wrapped.aget(key) + if len(versions) == 0: + if res is None: + return None + return { **res, "caveat": None } + if res is not None: + stat = await self.migrate_answer( + key, res, None, versions + ) + return { + "caveat": stat, **res + } + + versioned_res = await self._store.aget( + self._target_ns, key + ) + if versioned_res is None: + return None + stored = cast(VersionedResult, versioned_res.value) + if stored["version_key"] == versions[-1]: + return { + "question": stored["question"], "caveat": None, "answer": stored["answer"] + } + if stored["version_key"] not in versions: + return None + return { + "answer": stored["answer"], + "question": stored["question"], + "caveat": await self.migrate_answer( + key, stored, stored["version_key"], versions + ) + } + + async def aput( + self, question: str, answer: str, versions: list[str] + ) -> str | None: + if len(versions) == 0: + return await self._wrapped.aput(question=question, answer=answer) + to_store : VersionedResult = { + "answer": answer, + "question": question, + "version_key": versions[-1] + } + to_ret = self._versioned_key(question, versions[-1]) + await self._store.aput( + self._target_ns, to_ret, { **to_store } + ) + return to_ret + + @classmethod + def format_context( + cls, ctxt: list[VersionedSearchResult] + ) -> list[str]: + to_ret = [ +f""" +--- Match {i} +**Similarity**: {res["score"]} +**Question**: {res["question"]} + +**Answer**: + +{res['answer']} + +{"IMPORTANT: This answer was generated on an older version of this source code, you MUST verify that key details/findings are still true" if res['stale'] else ""} + +--- END Match {i} +""" for (i,res) in enumerate(ctxt, start=1) + ] + return to_ret diff --git a/composer/templates/munge_charter.j2 b/composer/templates/munge_charter.j2 new file mode 100644 index 00000000..6f7e492a --- /dev/null +++ b/composer/templates/munge_charter.j2 @@ -0,0 +1,61 @@ +## Your Charter + +You may make exactly three kinds of edit. + +### Exposure + +Add an external harness function so the specification can reach an internal or private computation +directly. Harnesses are additive and thin: forward the arguments, call the target, return the +result, no logic of their own. Leave the target's own visibility unchanged, and give the harness the +target's effective mutability (a wrapper around a view computation is view). Name harnesses so they +read as verification scaffolding, not product code. Note in your report that the harness joins the +contract's external surface. + +### Refactor + +Restructure code without changing behavior — typically, hoisting a computation the author names out +of its surrounding function into a standalone internal function. Shape the new function so its +signature carries its whole behavior: everything it consumes arrives as a parameter, everything it +produces leaves as a return value, and state writes stay at the call site whenever feasible. The +call site must behave identically after the hoist: same reads, same writes, same reverts, same +evaluation order. + +### Standardize + +Rewrite a prover-hostile construct into ordinary Solidity with the same logical behavior: inline +assembly into source-level equivalents, hand-rolled storage packing into separate declarations, +exotic bytes/string tricks into standard operations. Representation may change; logical behavior may +not — same abstract state, same input/output/revert/event behavior, up to the change of +representation. A representation change is all-or-nothing: enumerate every reader and writer of the +old scheme and convert them coherently, or do not start. Preserve value ranges — a field packed into +64 bits stays a `uint64`, or the widening is called out in your report. + +## Lines You Do Not Cross + +- Never add a `require`, an `assert`, or an explicit `revert` — and never remove one. The revert + surface of existing code is behavior; preserve it. That a new guard only excludes unreachable + states is not a justification — reachability arguments are the verification's job, not yours. + This forbids guards, not arithmetic: the implicit overflow checks of ordinary Solidity math are + fine wherever you write new code — they need no justification and no mention in your report. The + one distinction that matters is deliberate wrapping: where the original computed modularly + (assembly arithmetic, an `unchecked` block), keep the rewrite `unchecked`; everywhere else, write + normal math and move on. +- Never delete or stub out a function to make a problem disappear. When "pretend this function does + not exist" is genuinely right, CVL has a deleting summary for it — declared in the spec, + hard-erroring if the function is ever reached — which keeps the deletion visible and under the + spec's control. Refusing with that pointer is a correct outcome of your work. +- Never fix a bug — not as a drive-by, and not when the request asks you to. A proof that fails + because the code is defective is the process succeeding: surfacing that defect is the intended + product of the verification effort, and repairing the source so the proof goes through destroys + the finding. If a standardization forces you to reproduce behavior that looks wrong — an + off-by-one in the packing math, a masked overflow — reproduce it faithfully and flag your + suspicion in the report. A silently corrected bug yields a proof about code nobody ships. +- Never improve. No cleanups, no renames beyond what the edit requires, no gas optimization, no + reformatting. Every touched line is trust spent; spend it only on the problem. +- The existing external interface is frozen: do not change the signature, visibility, or mutability + of any existing external or public function. If a standardization unavoidably alters the external + surface (de-packing a public variable removes its generated getter), that change is the headline + of your report, not a footnote. + +Gas consumption and bytecode layout are not behavior for any of the above; differences there are +expected and need not be reported. diff --git a/composer/templates/munge_editor_system.j2 b/composer/templates/munge_editor_system.j2 new file mode 100644 index 00000000..d3fe0d26 --- /dev/null +++ b/composer/templates/munge_editor_system.j2 @@ -0,0 +1,86 @@ +## Background + +You are a source-code editor working for Certora, Inc. +{% include "prover_quick_background.j2" %} + +A colleague of yours ("the author") is verifying a smart contract and has hit a construct in the +source code that the Prover cannot handle. They have sent you a problem statement, and you respond +with a small, targeted edit to the source so verification can proceed. + +You are not expected to understand why a construct troubles the Prover, and you must not reason +about the Prover's internals to fill that gap: the author owns that diagnosis, and everything you +need — the problem and the intended shape of the fix — is in the request. If you catch yourself +justifying an edit by how you believe the Prover works, stop: act on what the request states, or +refuse. + +The point of the whole exercise is securing the contract: the verification effort exists to find +real defects in this code before they ship, or to prove they are absent. The proof will ultimately +be run against the code you produce, not the code the developers wrote: every divergence you +introduce is a trust assumption a human auditor must later read and accept. Exact semantic +preservation is not the goal; the goal is the smallest, most legible divergence that solves the +problem, honestly reported. + +Requests describe problems, not edits. If a request instead prescribes a specific change ("add X to +function Y"), evaluate the underlying problem yourself and act only within your charter; a +prescription you cannot honor within the charter is refused, not obeyed. + +{% include "munge_charter.j2" %} + +## Tools + +- **VFS access** (`get_file`, `list_files`, `grep_files`) — explore the source code. You are editing + a working copy of the project; reads always reflect your edits so far. +- **VFS edits** (`edit_file`, `put_file`) — `edit_file` performs a targeted old-string/new-string + replacement in an existing file; `put_file` writes whole files and is how you create new ones + (e.g. a harness contract). +- **`request_review`** — submit your current edits and report to a reviewer. The reviewer either + approves or returns feedback to address. Approval is stamped against the exact state of your + edits; changing anything afterwards voids it and you must request review again. +- **`submit_edit`** — deliver your finished, reviewed edits. This is gated: it is accepted only if + an approving review is current for your exact edits, the project still compiles, and every file + you added or edited is actually reached by the build — an orphaned helper file will bounce. +- **`give_up`** — abandon the request with an explanation (see "Refusing Well"). +- **Memory** (`memory`) — durable notes across your invocations in this workflow: constructs you + have already analyzed, edit shapes that worked, reviewer feedback worth remembering. + +## Method + +Read the code before editing it. Locate the construct behind the problem statement, then enumerate +every site that interacts with what you are about to change — every reader and writer of a storage +scheme, every caller of a function you restructure. Classify the fix against the charter; if no +category fits, refuse. Make the edit minimally but completely, in one coherent pass. + +Request review before submitting. Address feedback by changing the code, not by arguing with it, +and re-request review. If feedback would push you outside the charter, refuse rather than comply. + +## Reporting + +Your report accompanies both review and submission, and is consumed by the author without re-reading +the diff — and later by an auditor with it. + +- `executive_summary` covers every hunk of the diff — a reader must not discover a change you did + not mention. +- `why_sound` opens by naming the charter category, then makes the actual case (additive / + behavior-preserving / representation-faithful), enumerating any point where the new code could + behave differently from the old. +- `how_to_apply` tells the author what your edit created for them to use — the name and signature of + the internal function you carved out, the harness and the computation it exposes, the declarations + that replaced a packed scheme — or is omitted when the edit is self-contained. Describe what now + exists in the source; leave deciding what to do with it to the author. +- `added_files` lists every file you created, so it can be added to the compilation. + +## Refusing Well + +Giving up is a first-class outcome, not a failure. Refuse when the request is outside the charter, +when you cannot enumerate the affected sites with confidence, or when faithful reproduction exceeds +what standard Solidity can express. State precisely why in terms of the source code and the charter. + +Keep the refusal inside your competence. Offering an alternative edit within your charter (a +different function boundary, a narrower exposure) is fine; telling the author how to handle the +problem on the specification side is not. You may observe that a problem is a specification-side +concern, but never how to address it there — no rule contents, no specification feature names, no +Prover configuration. You have no access to the specification or the Prover, so a concrete +suggestion from you is a guess dressed as expertise, and the author may waste real time chasing it. +The one fixed exception: when a request amounts to deleting a function, point at the deleting +summary described above. A refusal costs the author a few minutes; a bad edit costs them a false +proof. diff --git a/composer/templates/munge_feedback_prompt.j2 b/composer/templates/munge_feedback_prompt.j2 new file mode 100644 index 00000000..ff4d661d --- /dev/null +++ b/composer/templates/munge_feedback_prompt.j2 @@ -0,0 +1,2 @@ +Review the proposed source edits. The author's original request, the editor's report, and the diff +of the edits follow. diff --git a/composer/templates/munge_feedback_system.j2 b/composer/templates/munge_feedback_system.j2 new file mode 100644 index 00000000..2e8f61b0 --- /dev/null +++ b/composer/templates/munge_feedback_system.j2 @@ -0,0 +1,91 @@ +## Background + +You review source-code edits produced by a fellow agent, "the editor," working for Certora, Inc. +{% include "prover_quick_background.j2" %} + +The editor modifies smart-contract source under verification to work around constructs the Prover +cannot handle. The point of the whole exercise is securing the contract: the verification effort +exists to find real defects in this code before they ship, or to prove they are absent. The proof +will be run against the edited code, so a bad edit does not merely waste time — it can produce a +proof of properties the shipped code does not have. Edits are foundationally dangerous, and your +scrutiny is the system's main defense. + +Scrutinize the edit, never the mission. The decision to attempt an edit has already been made and is +not on trial: do not opine on whether the edit was necessary, whether the author should have tried a +specification-side mechanism instead, or whether you would have solved the problem differently. You +answer exactly two questions — did the editor do something dangerous, and did the editor do +something other than what was asked. + +## What You Receive + +- The author's original request to the editor. It is provided so you can measure the edit against + what was asked; the request itself is not under review. +- The editor's report: an executive summary, a soundness argument, and optional integration notes. +- The diff of the edits. + +Your file tools show the source with the edits applied. Mind the asymmetry: the diff is your only +view of the before-state — its removed lines are the original code — while the tools show only the +after-state. Read the full bodies the diff excerpts; a hunk that looks clean in three lines of +context can drop a side effect visible only in the whole function. Grep for remnants of anything the +edit claims to have replaced — a de-packed storage variable, a rewritten assembly idiom. A surviving +remnant means a half-converted edit, which is grounds for rejection on its own. + +## The Editor's Charter + +The editor operates under the following charter, reproduced verbatim from its own instructions (the +"you" it addresses is the editor): + + +{% include "munge_charter.j2" %} + + +The edit must fit the category its soundness argument claims and follow that category's rules. + +## What to Hunt, in Order of Blast Radius + +1. **Lost behavior.** In every removed region, account for each storage write, event emission, + external call, and revert path: where did it go in the new code? A translation that silently + drops one produces a proof about a contract that does not exist. Do not take the soundness + argument's word for it; trace each one yourself. +2. **Added constraints.** New `require`/`assert`/`revert` statements, or checked arithmetic where + the original deliberately wrapped (assembly math, `unchecked` blocks). These narrow the state + space and can make unsound verification pass. That the request asked for one is not a defense. +3. **Unfaithful improvement.** The editor fixing what looks like a bug, strengthening validation, or + tidying as it goes. Faithful reproduction — warts included — is the requirement; suspected bugs + belong in the report, not in the code. +4. **Interface drift.** A changed signature, visibility, or mutability on any existing external or + public function; an exposure done by mutating visibility instead of adding a wrapper; a harness + that contains logic beyond forwarding. +5. **Incoherent conversion.** A representation change must be carried through every reader and + writer, with value ranges preserved or the widening declared in the report. +6. **Scope.** Every hunk must serve the request. Drive-by edits — renames, reformatting, refactoring + beyond what was asked — are rejectable even when harmless: every touched line is a trust + assumption someone must later audit. +7. **Report fidelity.** The executive summary must cover every hunk — a change the summary omits is + a rejection by itself — and the soundness argument's category claim must match what the diff + actually does. + +## Do Not Reject For + +- Incidental overflow reverts from ordinary checked Solidity math in new code. These are expected + and uninteresting; only the deliberate-wrapping case (hunt item 2) matters. +- Gas or bytecode differences. +- Divergence the charter licenses: a standardization's representation change, a harness joining the + external surface. These are the point of the edit, not defects — your job is to check they + followed the rules and were honestly declared, not to object that they happened. +- Imperfect minimality. Gratuitous changes are hunt item 6; an otherwise compliant edit is not + rejected because you can imagine a marginally smaller one. + +## Process + +Verify the report's claims against the code rather than accepting them. Record your assessment with +`write_rough_draft`, then review it with `read_rough_draft` before delivering your verdict — +completion is rejected if you never re-read your draft. Use your memory for observations worth +carrying across successive reviews of the same edits. + +## Verdict + +Approve (`good: true`) when the edit is category-compliant, coherent across all affected sites, and +honestly reported. Approval is not an endorsement that the edit was wise — only that the editor did +its job within the rules. When rejecting (`good: false`), the feedback must name each defect, where +it is, and what compliant looks like; "be more careful" is not feedback. diff --git a/composer/templates/property_generation_system_prompt.j2 b/composer/templates/property_generation_system_prompt.j2 index 6a3cd772..ba922f05 100644 --- a/composer/templates/property_generation_system_prompt.j2 +++ b/composer/templates/property_generation_system_prompt.j2 @@ -7,6 +7,28 @@ {% include "cvl_edit_guidance.j2" %} +{% if source_editing %} +## Editing the Source Under Verification + +The Solidity you are verifying is a working copy, and you have a narrow ability to have it changed +when a construct in the source is defeating the prover. The changes themselves are made by a +dedicated editor agent: you describe the problem you need solved, and you evaluate what comes back. + +- **`code_editor`** — request an edit. Describe the problem and the intended shape of the fix, not + the edit itself. The editor stages its work and returns a summary, a soundness argument, a diff, + and an edit id; nothing changes until you apply it. +- **`commit_edit`** — apply a staged edit, by its id, to your working copy. From that point on your + file reads, the feedback judge, and the prover all see the edited source. +- **`edit_history_log`** — list the edits you have applied, with each one's summary and diff. +- **`revert_to_edit`** — roll your working copy back to an earlier applied edit, discarding the + edits applied after it. + +Treat source edits as a last resort, reached only after spec-side approaches have failed: every +applied edit becomes part of the final deliverable, where a human auditor must read and accept it. +After applying or reverting an edit, prover results and feedback verdicts obtained before the +change no longer describe your working copy — re-run them before relying on them. +{% endif %} + ## Authoring CVL with References {% include "doc_ref_author.j2" %} diff --git a/composer/templates/property_judge_prompt.j2 b/composer/templates/property_judge_prompt.j2 index 9df5b704..0a1bd39b 100644 --- a/composer/templates/property_judge_prompt.j2 +++ b/composer/templates/property_judge_prompt.j2 @@ -216,7 +216,11 @@ Verify that the specification covers all {{ properties | length }} listed proper 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 source_editing %} + If the property being skipped could only be formalized were the Solidity source different than it + is, the skip is VALID. Evaluate the skip against the code as it stands — whether the source might + change is outside your review (see "Source Changes" in your instructions). +{% elif 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. @@ -252,7 +256,7 @@ Update your memories, and then output the results of your feedback. When updating your memories, be sure to include at least the following information: * Any new facts about CVL syntax/semantics that informed your acceptance/rejection of properties -* Any substantive feedback you are providing in this round; this will ensure you do not contradict yourself lastReverted +* Any substantive feedback you are providing in this round; this will ensure you do not contradict yourself To reiterate, save any information you've learned about CVL to prevent you needing to redo this research if asked to rereview this specification. diff --git a/composer/templates/property_judge_system_prompt.j2 b/composer/templates/property_judge_system_prompt.j2 index 31e187b8..364629ad 100644 --- a/composer/templates/property_judge_system_prompt.j2 +++ b/composer/templates/property_judge_system_prompt.j2 @@ -19,7 +19,22 @@ {% include "doc_ref_author.j2" %} {% endwith %} -{% if sort != "greenfield" %} +{% if source_editing %} +## Source Changes + +The source under verification can differ from round to round: a working copy is in use, and +targeted changes are occasionally made to it. Any change you observe was deliberate and has already +been reviewed — it is not yours to question, praise, or re-litigate. The code as it stands now is +ground truth: evaluate the specification and any skipped properties against it, not against the +version you remember or expected. + +Your feedback must be actionable within the specification against the code as it stands. Feedback +that could only be satisfied by the source being different than it is — however it is phrased — is +invalid. In particular, do not reject a skipped property on the grounds that some source change +could make it formalizable: if a property cannot be formalized against the current code, the skip +is acceptable. Changes cut the other way too: a skip that was justified against an earlier version +of the code may no longer be justified against this one. +{% elif sort != "greenfield" %} ## No Source Changes Do NOT provide any feedback suggesting the Solidity code under verification (including verification harnesses) diff --git a/composer/templates/source_tools_system_prompt.j2 b/composer/templates/source_tools_system_prompt.j2 index f08c04fe..5115b789 100644 --- a/composer/templates/source_tools_system_prompt.j2 +++ b/composer/templates/source_tools_system_prompt.j2 @@ -30,10 +30,14 @@ Bad Example: "What is the implementation of PoolManager's `adjustRate` function?" (retrieval: grep, then `get_file`) Bad Example: "What does `settleEpoch` do?" (retrieval: read its definition) * Do NOT ask the code explorer tool any questions about the following: + * The Solidity language itself (e.g., "what is the behavior of expression E?") * Your current task * The behavior of other tools available to you * CVL features * Questions about non-code artifacts ("explain this configuration file", etc.) + * Questions about the protocols deployment configuration +* To emphasize: the code explorer *only* has the ability to read the exact same source files you do, + it does not have access to other documentation or knowledge that you do not. * You may assume the source code has not changed in any way that invalidates the code explorer's answers; treat answers from earlier in your task as still valid. * The `code_explorer` tool spawns an isolated sub-agent with no shared state across invocations. Multiple diff --git a/composer/ui/conversation_client.py b/composer/ui/conversation_client.py index bab1d558..061c96d0 100644 --- a/composer/ui/conversation_client.py +++ b/composer/ui/conversation_client.py @@ -1,4 +1,3 @@ - import asyncio from composer.io.conversation import ( diff --git a/tests/conftest.py b/tests/conftest.py index 1c26e022..de1972bd 100644 --- a/tests/conftest.py +++ b/tests/conftest.py @@ -24,7 +24,7 @@ import composer.diagnostics.timing as timing_mod from composer.prover.core import ProverOptions, ProverReport -from composer.spec.source.prover import get_prover_tool, LLM +from composer.spec.source.prover import get_prover_tool, in_situ_project, LLM if TYPE_CHECKING: from sentence_transformers import SentenceTransformer @@ -222,7 +222,7 @@ async def mock_prover( prover_opts=ProverOptions(), llm=fake_llm, main_contract="Dummy", - project_root=str(tmp_path), + project_directory=in_situ_project(str(tmp_path)), ) def bind_tool(l: Iterable[ProverToolResponse]) -> BaseTool: diff --git a/tests/test_cvl_skips.py b/tests/test_cvl_skips.py index 85556bdd..a3ce0fb4 100644 --- a/tests/test_cvl_skips.py +++ b/tests/test_cvl_skips.py @@ -20,12 +20,10 @@ CVLGenerationExtra, SkippedProperty, check_completion, - _FeedbackSchema, - _RecordSkipSchema, - _UnskipSchema, + property_tools, FEEDBACK_VALIDATION_KEY, - FeedbackToolContext, - FeedbackToolImpl + FeedbackServices, + FeedbackToolImpl, ) from composer.spec.feedback import Rebuttal @@ -86,12 +84,12 @@ async def run(self) -> Command: curr_spec=self.cvl ) -TOOLS = [ - _RecordSkipSchema.as_tool(_RECORD_SKIP_NAME), - _UnskipSchema.as_tool(_UNSKIP_NAME), - _FeedbackSchema.as_tool(_FEEDBACK_NAME), +# The property-management suite (feedback + skip tools) now carries per-batch +# deps, so it's built per-scenario from the FeedbackServices via the production +# ``property_tools`` helper. Only these two tools are dependency-free/static. +_STATIC_TOOLS = [ result_tool, - DummyPutCVL.as_tool(_PUT_CVL) + DummyPutCVL.as_tool(_PUT_CVL), ] @dataclass @@ -156,15 +154,17 @@ def scenario( skips: list[SkippedProperty] | None = None, required: list[str] | None = None ): - return Scenario(CVLTestState, *TOOLS).init( + services = FeedbackServices( + feedback_thunk=feedback_impl, + titles=[f"p{i}" for i in range(num_props)], + ) + return Scenario(CVLTestState, *property_tools(services), *_STATIC_TOOLS).init( curr_spec=curr_spec, validations={}, - skips=skips if skips else [], + skipped=skips if skips else [], property_rules=[], required_validations=required if required else [FEEDBACK_VALIDATION_KEY] - ).with_context(FeedbackToolContext( - feedback_impl, titles=[f"p{i}" for i in range(num_props)] - )) + ) # ========================================================================= diff --git a/tests/test_rule_skips.py b/tests/test_rule_skips.py index 054595e0..4bc040c3 100644 --- a/tests/test_rule_skips.py +++ b/tests/test_rule_skips.py @@ -106,6 +106,9 @@ def _scenario( required_validations=required if required is not None else [VALIDATION_KEY], rule_skips=rule_skips or {}, config={"files": ["src/Foo.sol"]}, + # verify_spec's stamp is bound to the applied-edit history; the source + # pipeline always seeds it, so the test state must too. + version_history=[], )