Skip to main content
Glama

Setup, run dynamic proof, refresh report

orangepro_prove_loop

Runs trusted-local repository setup, then executes the unchanged targeted proof oracle and refreshes the behavior report; setup failures return unrunnable without touching the proof ledger.

Instructions

Product wrapper around orangepro_prove: run trusted-local setup_commands in the source checkout, then the UNCHANGED dynamic targeted-proof oracle, then refresh the behavior report. Setup is non-secret repo prep only (build/install/shim); a setup failure returns unrunnable, does not run the oracle, and leaves the ledger untouched (never Proven). Public Proven still closes only through the unchanged certificate.

Input Schema

NameRequiredDescriptionDefault
methodNoOptional consistency check. If provided, must match the member derived from target_symbol.
run_idNoOptional caller-supplied run id. Defaults to a local monotonic id.
runnerNoTest runner override. Default auto.
sourceNoSource checkout containing the test and target files. Setup runs here. Defaults to workspace.
test_envNoExplicit non-secret KEY=value env entries for the test run.
test_runNoGo: fully-anchored test name for `go test -run`, e.g. '^TestCompute$' (required for Go targets). Java: 'TestClass#testMethod', e.g. 'CalculatorTest#addsTwoNumbers' (required for Java targets).
target_idNoOptional graph target id that must resolve to exactly one hard-linked CodeSymbol.
test_pathNoTS/JS: repo-relative test file to run (required for TS/JS targets).
workspaceNoLocal workspace root. Defaults to the current directory.
timeout_msNoPer baseline/mutant test timeout.
jest_configNoRepo-relative Jest config path.
replacementNoTS/JS: inert sentinel body, e.g. 'return null;' or 'return {"ok":false};'. Must be JSON-only per the oracle (required for TS/JS targets). Go derives its own sentinel.
target_fileNoOptional consistency check. If provided, must match the file derived from target_symbol.
target_symbolNoExact CodeSymbol external id, e.g. sym:src/service.ts#OrderService.createOrder. Preferred.
vitest_configNoRepo-relative Vitest config path.
setup_commandsNoTrusted-local repo prep run in the source checkout before the oracle. Non-secret only (build/install/shim). First non-zero exit returns unrunnable.
replacement_modeNoSentinel wrapping mode. Default return-json.
setup_timeout_msNoDefault per-setup-command timeout (ms). Default 30000.
link_node_modulesNoTrusted-repo speed mode: symlink node_modules into temp copies.

Schema Changelog

Changes observed during successful MCP inspections.

  1. Changed3 schema fields changed
    • removedInput schema / additionalProperties
      Removed value: -false
    • removedInput schema / properties / setup_commands / items / additionalProperties
      Removed value: -false
    • addedInput schema / properties / setup_commands / items / properties / timeout_ms / maximum
      Added value: +9007199254740991
  2. Addedv0.2.59

TDQS

A4.2/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Annotations already declare non-readonly, open-world, non-idempotent, and non-destructive behavior. The description adds important semantics: setup commands are non-secret repo prep only, setup failure returns unrunnable and skips the oracle while leaving the ledger untouched, and Proven status still requires the unchanged certificate. It does not cover permissions, rate limits, or every mutation effect.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Three dense sentences are front-loaded with the workflow, safety constraint, and failure behavior. There is no filler, and every sentence carries useful information for invoking the tool correctly.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The description explains the workflow and key failure states, and the schema fully documents all 19 parameters. Since there is no output schema, normal success return details and report-refresh output shape are not fully described, but the critical safety and proof semantics are present.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%, and the schema already explains test_path, test_run, replacement, setup_commands, and the other parameters in detail. The description reinforces setup_commands semantics but adds little parameter meaning beyond what the schema provides.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

It names the specific workflow sequence: setup_commands in the source checkout, then the unchanged dynamic targeted-proof oracle, then refresh the behavior report. It also explicitly identifies itself as a wrapper around orangepro_prove, making it distinguishable from that sibling.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The use case is clear: this tool is for when trusted-local repo prep is needed before running the proof oracle and refreshing the report. It names orangepro_prove as the underlying alternative but does not explicitly state when to call that sibling directly instead of this wrapper.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.