search-with-proof: pilot driver (6.2)

One side per run over selected pilot pairs: board, brain on the VM with the
project DeepSeek client, executor tasks on kube-ax, verification on the VM lane
(AX verify lane switchable). Hard run ceiling with reservation before every call,
per-search and step caps; fixed side never sees the vulnerable revision; records
carry digests only. Dry run with the stub model reaches demonstrated.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
This commit is contained in:
Marius Ciepluch
2026-10-05 18:58:24 +02:00
co-authored by Claude Opus 5.5
parent 941fbb5fb0
commit 87b82564b4
4 changed files with 881 additions and 1 deletions
+77 -1
View File
@@ -1,6 +1,8 @@
# Search feasibility tools
These host-side tools make no model calls. Run them from the repository root.
Run these host-side tools from the repository root. Selection and executor smoke
make no model calls; the pilot driver calls the configured model unless `--dry-run`
is specified.
## Executor smoke
@@ -55,3 +57,77 @@ The default identity-bearing manifest is
counts, selection biases, input instrumentation, and digests only. Neither output
is overwritten. A successful selection is feasibility input, not evidence of
buildability, oracle operation, unseen performance, or BLOCK eligibility.
## One-sided pilot driver (task 6.2)
The shared virtualenv may be installed against another worktree; `PYTHONPATH`
below explicitly selects this worktree's source.
Offline probe, using a scripted model and in-process repository executor with real
host verification (no network or provider calls):
```sh
PYTHONPATH="$PWD/src" /home/mc/Source/OpenUltraSAST/.venv/bin/python -m benchmarks.search.pilot_run \
--dry-run --side vulnerable --pairs 0 --ceiling-usd 0.50 \
--out /tmp/search-pilot-dry.jsonl
```
For three **live** searches, after the oracle infrastructure probe and budget
approval, set `SEARCH_TASK_IMAGE` to the tested search image's complete
`REGISTRY/IMAGE@sha256:DIGEST` reference, then run:
```sh
PYTHONPATH="$PWD/src" /home/mc/Source/OpenUltraSAST/.venv/bin/python -m benchmarks.search.pilot_run \
--manifest benchmarks/search/private/pilot.json \
--side vulnerable --pairs 0,1,2 --ceiling-usd 1.50 \
--verify-lane vm --image "${SEARCH_TASK_IMAGE:?Set the tested digest-pinned search image}" \
--out benchmarks/measurements/2026-10-05-search-pilot-vulnerable.jsonl
```
This command spends money and contacts AX and the store. The ceiling shown is an
example for the three $0.50 searches, not evidence that a live run was approved or
performed. Use a fresh output path; output files are never overwritten.
The existing DeepSeek key/base URL environment variables and provider model/prices
are reused (`deepseek-flash` by default). `.env` does not override exported values.
Retries are disabled. Unknown models require both `--usd-per-mtok-in` and
`--usd-per-mtok-out`. Every call reserves its conservative input-token bound plus
`--max-tokens` output allowance against the task allowance and shared run ceiling;
failed calls and calls with missing usage settle the maximum. Reservations in the
record are cumulative admitted maxima, not outstanding spend. Their sum can exceed
the ceiling when usage settlements release unused allowances. Settled spend remains
bounded by the run ceiling and $0.50/search. Search defaults also cap reason rounds
at 4, intents at 3 per round, explore at 15 minutes including acquisition, and demos
at 3. Physical AX submissions and coordinator steps have separate 32-task caps.
The board defaults to a private local FileStore under a fresh directory in
`benchmarks/search/private/runs/`; `--board-memory` selects another board store URI.
The AX mailbox still requires the existing `OUSAST_MEMORY=s3://bucket/prefix`, public
HTTPS `S3_ENDPOINT`, and host store credentials. Board storage does not replace the
mailbox. Executors receive only presigned object URLs. The brain runs on the VM;
repository tools and build/export run in key-free AX executors. VM verification
requires working user namespaces and consumes executor-built archives. `--verify-lane
ax` switches to the existing dispatcher, with three fresh verifier tasks per side
and no executor holding a worker slot during those repetitions.
Each selected index produces a JSON line followed by one run summary: Req 3.4
outcome, reserved/settled spend, calls, tokens, physical tasks, coordinator steps,
phase timings, failure codes, input bytes, board bytes, end reason, and hashed
repository/revision identities. The private board and checkouts contain identity-bearing
data. The public JSONL omits raw model/executor diagnostics. Selection advantages
are explicit in the summary; this is feasibility evidence, not BLOCK qualification.
A fixed invocation creates a fresh board/demo and retains only the fixed revision.
Its verifier runs two independent sets of repetitions on that same fixed revision;
no vulnerable checkout or previously generated vulnerable demo is passed in.
`fixed_effect_observed` reports a consistent owned effect on the first three fixed
runs (`null` when unavailable or inconsistent). Such an effect requires adjudication;
it is not promoted to a differential `demonstrated` outcome. The normal safe probe
therefore ends `inconclusive`, never “not vulnerable”.
Generic `injection` needs an `oracle` value of `sql` or `command` in the private
manifest; without a subtype verification returns `no_oracle`. No subtype is guessed
from repository names. The selected manifest's pair 1 currently lacks this metadata.
Live transport, provider authentication/cost, real project buildability, and AX
oracle operation must still be measured; an offline probe cannot establish them.