Plugin tool contribution

[jtoman]

Allows plugins to contribute tools to the formalizers of individual backends.

This accomplished in two places. First, the formalizers (not the backend) declares a tool_provider_type field. This field names a particular subclass of PipelinePlugin which provide tools for the formalizer to use. This information is used by the pipeline to construct a formalization cache key that includes the plugins that contributed to that formalization.

The actual binding of tools is accomplished by pushing a ToolBinder object through to the formalizer. The ToolBinder takes ToolExtension type and the "injected parameters" and returns a sequence of ProvidedTools. Each ProvidedTools object encapsulates the Langchain tools that may be bound directly on the graph plus the system prompt blurb describing to the agent how to use said tool.

Tool Discovery Details

The ToolBinder type is a polymorphic function with (roughly) the following signature:

(ToolExtension[TP, U, P], **P) -> Sequence[ProvidedTool]

where U is the usual FeatureUnit bound type parameter for the backend. **P is a param spec type parameter; it defines the protocol for how the formalizer communicates with its plugins in a way that is opaque to the pipeline core. ToolExtension itself is defined as a class with two fields:

provider: type[TP]
project: (TP) -> ((U, list[PropertyFormulation], PluginToolContext, **P) -> Sequence[ProvidedTools])

project takes an instance of TP (the tool provider) and projects out a member function which takes, as arguments: the feature unit being formalized (represented by U), the list of properties being formalized, the "plugin tool context" (see below), and "whatever arguments are represented by P". The fixed argument prefix (U, list[PropertyFormulation], and PluginToolContext) are all injected automatically by the tool binder implementation; all the arguments represented by P are passed through from the call to the ToolBinder. [1]

Behind the scenes, the ToolBinder constructed by the pipeline core iterates all of the plugins loaded for a run, and finds those that are subclasses of provider, it injects the fixed prefix arguments alongside the formalization specific arguments represented by P. In addition, a special class AnyBackend allows a plugin to define tools used by anybackend; it only has the fixed prefix injected, formalization specific parameters are never passed through.

The PluginToolContext type is the existing PluginContext type without the runner field; the plugin is expected to provide its functionality through tools, which should not be spawned as top-level multi-job tasks. In addition, we provide a register field of type ArtifactRegistrar. This lets plugins communicate unstructured "verification artifacts" back to the main pipeline. These artifacts are included in the main report as side information.

Tool Usage

In practice, the expected shape of communication between a plugin and the formalizer are two parameters, the actual runtime representation of the author's state type, and a projector function, which takes an instance of the state and yields a slice of the state used by the author.

For example, the CertoraProverTool api provides the plugin tools with type[SourceCVLGenerationState] and (SourceCVLGenerationState) -> AsyncContextManager[CVLAuthorState]. CVLAuthorState contains, among other things:

1. The current configuration
2. A materialized copy of the VFS state of the author
3. An edit store for proposing edits to the author's VFS
4. A "prover runner" which handles provisioning and running the prover

It is strongly recommended (but not enforced) that formalizers handle provisioning of abstractions for accessing the utilities they themselves access through tools (e.g., running the prover) instead of passing through the raw building blocks to access those utilities themselves. For example, in the prover runner case above, passing through the data necessary for the plugin to run the prover "from scratch" would require passing the ProverOptions the "config overlay" (the basic config elaboration performed by the author's prover tool), the current configuration (already passed), and require the plugin to know how to piece all that together. All of this together would create a far greater API surface with which to maintain BC for the plugins (e.g., don't rename the prover_config_overlay function because some random plugin might need it). In other words, use this projector function pattern to push functionality to the plugins, instead of making them pull in random pieces of code from the rest of the AP codebase.

Parallelization

To support long running tools, we've added a TaskHost abstraction, which can be used to launch background tasks that run in parallel with the main agent. It is expected this will be used to allow plugins to doe their work as background tasks. The main formalization agent can use the task management tools to query background task state and to wait for/retrieve results.

Prover Tools

The other "big" piece of this PR is enabling plugins for the Certora Prover tool to propose edits to the source code under verification. This could be useful to, e.g., write a plugin that addresses PTA failures due to inline assembly, or to use Concord to make verified large scale rewrites beyond what the code editor agent is empowered to do. These edits are proposed and committed using the existing edit store infrastructure. However, we extend the edit store to record the provenance of edits; the existing editor is called "MungeAgent", edits from plugins are tagged with their id (this tagging is handled automatically; the plugins cannot lie about their id).

On Testing

I have proven this code correct, but I haven't yet tested it [2]. I am sharing it here because its in its mostly final state; I plan to do a big test run in parallel with the review process.

[1] There is a second form which takes an InjectedToolExtension, which allows the P part of the plugin to know about the plugin id it is requesting. Don't think too hard about it, it makes your head hurt.

[2] I haven't actually proved it correct either

[ericeil]

Does the for r in r.children modify the existing r, or create a new scope? (You use r again on the next line)

[ericeil]

Remove?

[ericeil]

Remove?