Expand description
Static plan verification as an admission gate.
car-verify could already reject a bad plan before any tool ran — but the
only call site that did so lived inside the executor’s replan loop
(ReplanConfig::verify_before_execute). That loop needs a registered
crate::ReplanCallback, and it is bounded by max_replans, which defaults
to 0. No production path registered a callback, so the check never fired on
real work: the README promised verification before execution and the runtime
delivered it only for a replan that never happened.
StaticVerificationGate moves the same check to the seam that does run on
every proposal — crate::admission::AdmissionGate, the same place the
information-flow gate already sits.
What this is worth, precisely. validate_action already checks tool
existence, parameter schemas, preconditions, and state dependencies — per
action, and with a stronger schema validator than car-verify’s (the full
jsonschema crate versus a hand-rolled required+type subset). So on a
single-action proposal this gate adds no coverage at all: rejecting “the
whole proposal” and rejecting “the one action” are the same thing, and the
validator gets there anyway.
The value is entirely on multi-action proposals, and it is about timing,
not coverage. validate_action runs as execution reaches each action, so a bad
tool name in action 5 is discovered after actions 1–4 have already had their
side effects. This gate sees the whole proposal up front and refuses it before
the first dispatch, so nothing partial happens. Register it on any runtime that
accepts externally-authored multi-action proposals; on a runtime that only ever
submits one action at a time it is close to inert.
What blocks, and what is only advisory. Blocking is limited to
state-independent findings: an unregistered tool, parameters that violate the
registered schema, and a tool_call with no tool. Those are exact — they
cannot be wrong about a plan that would in fact have run.
Everything state-dependent is advisory, because the forward model is
incomplete: it applies only the effects an action declares in
expected_effects. An action that really writes a key without declaring it is
invisible, so a downstream precondition or state_dependency reading that key
is reported as failing even though execution would have succeeded. Blocking a
whole proposal on that would be a false rejection, and StaticState::is_unknown
does not save us — nothing in the workspace ever populates unknown_keys, so it
is always false. The loop heuristic (count >= 3) is advisory for the same
reason: three legitimate polls are indistinguishable from a runaway loop.
Preconditions still get enforced — by validate_action, at execution time,
against live state, where the answer is accurate. Write conflicts are warnings
upstream and never blocked. Dependency cycles cannot occur at all (car-ir’s
DAG edges only point to lower indices).
Structs§
- Static
Verification Gate - An admission gate that statically verifies a proposal before any action runs.
Functions§
- blocking_
errors - Run static verification and return the blocking errors, if any.
- is_
blocking_ issue - Whether a verification issue is exact enough to refuse a whole proposal on.