Skip to content

Run the code the verification is about #65

Description

@daniel-kindl

Problem

Most of the verification asserts that a string appears in a tracked file. It does not run
the code the assertion is about.

All 19 numbered modules in verify/ grep the tracked tree. Counted by assertion kind:

Module check (runs something) check_contains / check_not_contains of those, against source text
verify/80-sandcastle.sh 27 130 112
verify/85-agentq.sh 27 102 44

The import validator

bin/agentbox:872-937 (import_result) is the only path by which model output enters a
real repository. On a machine with no Podman it is checked like this:

# verify/80-sandcastle.sh:287-288
check_contains 'F2 the number of imported commits is bounded' \
    'and the limit is $max' "$AB_CODE"

The code it names:

# bin/agentbox:892-894
[ "$count" -le "$max" ] ||
    { import_refuse "the result has $count commits, and the limit is $max" \
        'Raise it with --max-commits if this is expected.'; return 1; }

Change -le "$max" to -le 9999 and F2 still passes. F1, F3, F13, F14, F16, H3b and G4
have the same shape.

A check that a comment satisfies

# verify/85-agentq.sh:195-196
check_contains 'E10 a merge is followed by a rescan' \
    'a merge can unblock' "$(cat "$AQ_LIB/coordinator.py")"

The needle occurs once in the file, at lib/agentqueue/coordinator.py:15, inside the module
docstring. Delete the wave loop at coordinator.py:252-299 and E10 still passes.
docs/agentq.md:68-70 states that the rescan is not an optimisation.

The helper aq_code_of does not fix this. It deletes lines that start with #, """ or
*. It does not delete a docstring body, so the needle survives it. Every check that uses
aq_code_of can also be satisfied by prose inside a docstring.

E1, E3 and E7 pin user-facing English sentences, for example the issue closed while the run was in progress. The repository writing policy asks for ASD-STE100 rewrites, so a reword
breaks them. A gate that was commented out but whose message string survives still passes
them. E8 pins the private method name _require_clean_diff.

The harness already exists

verify/probes/clone-identity.sh:70-92 sources bin/agentbox as a library, sets
AGENTBOX_STATE_DIR, and calls make_run_dir, create_clone and sanitize_clone against
real Git repositories, with no container. bin/agentbox:237 documents AGENTBOX_STATE_DIR
as existing for the host-side tests. One concern uses it.

Secondary: verify reads a doctor's column widths

# verify/80-sandcastle.sh:638-644
case $doctor_out in
    *'podman client      NOT FOUND'*|*'podman reachable   NO'*)  skip ... ;;

It matches bin/agentbox:1148, which is a printf with fixed column spacing. Realign one
column and every correctly unconfigured machine reports a hard failure instead of a skip.

Secondary: a verification module has no identity

A module's identity lives in four unlinked places: the filename prefix, the section string
it prints, the --only argument, and the verify field in component.json. The filter is
a string comparison:

# verify.sh:53-56
if [ -n "$ONLY" ] && [ "${base%%-*}" != "${ONLY}0" ] && [ "${base%%-*}" != "$ONLY" ]; then
    continue
fi
  • Two files print a section named 1b: verify/10-host.sh:40 ("Host package manifests") and
    verify/15-components.sh:3 ("Toolkit components"). AGENTS.md rules 10 and 12 both say
    "verify.sh module 1b checks that". The reference is ambiguous.
  • verify/85-agentq.sh prints sections 8b and 8c. Neither is selectable. --only 8b
    matches no file and exits with a clean summary.
  • Modules share one shell namespace. out= is assigned in 15 places across modules, and 3
    of 23 modules unset anything.

Secondary: a manifest value copied into a verification module

# verify/45-pi.sh:28-34
else
    PI_RUNTIME_DIR_REL=.local/share/pi-node
    ...
    PI_NODE_MIN_VERSION=22.19.0
fi

manifests/pi.env:26 is the source of truth for 22.19.0. A missing manifest is a failure,
not a reason to guess.

Goal

Let the verification run the code it is about. Keep source queries for the claims that only
a source query can make.

Proposed direction

Separate the two kinds of assertion, and treat them differently.

Behavioural gates run the code. Name the host-side interface of bin/agentbox
create_clone, sanitize_clone, repo_snapshot, diff_snapshot, import_result,
lock_is_stale, load_secrets, redact — and state the globals each one reads and writes.
Extend verify/probes/ with import-validation.sh and lock.sh, built on the scratch
directory adapter that clone-identity.sh already uses. Move the behavioural agentq gates
into verify/probes/agentqueue-unit.test.py, where they can assert on a gate result.

Structural claims stay as source queries. A negative shape claim is sound as a source
query: no --force in gitops.py, no write path outside the lock, no GH_TOKEN in the
coordinator, no second routing mapping in the Pi component. Prefer an AST query, as the lock
check at verify/85-agentq.sh:242-260 already does.

Also:

  • Give agentbox doctor stable exit codes or a --json output, and let
    verify/80-sandcastle.sh read that instead of the display columns.
  • Let a verification module declare its own identifier, so --only can select 8b, and so
    a component.json verify field names an identifier that is guaranteed to resolve.
  • Run each module in a subshell, so its variables and functions do not leak.
  • Delete the fallback block in verify/45-pi.sh:28-34.

Acceptance criteria

  • A probe proves that import_result refuses a history that does not descend from the base commit.
  • A probe proves that import_result refuses a commit count over the bound.
  • A probe proves that import_result refuses an unexpected merge, and accepts one with --allow-merges.
  • A probe proves that import_result refuses a target ref that moved between the check and the write.
  • Those probes pass with no Podman and no built image.
  • Changing -le "$max" to a wrong bound fails the suite.
  • Deleting the rescan loop fails the suite.
  • No check is satisfied by a comment or a docstring.
  • The remaining source queries state a structural claim, not a user-facing sentence.
  • verify/80-sandcastle.sh reads a machine-readable result from agentbox doctor, not its column layout.
  • Every verification module declares one identifier, and every identifier is unique.
  • --only selects a declared identifier, including a lettered one.
  • Every verify field in components/*/component.json resolves to exactly one module, and a test asserts it.
  • verify/45-pi.sh reads manifests/pi.env and fails when it is absent.
  • ./verify.sh remains green.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    verificationVerification gates, probes, self-tests, validation, or support evidence

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions