Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 6 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -1339,9 +1339,12 @@ jobs:
run: bash scripts/v4-probe-selector-keystone-gate.sh --perturb-check
# Near-term CI dogfood: the v4.workflow.executor .dag is the batching
# AUTHORITY. claim_executor consumes its plan (batch_runner.dag) and runs the
# claim suite batch-by-batch, claims-in-parallel. --perturb-check proves the
# host CONSUMES the .dag (drop a dependency -> rebatch) and that the
# executor's ordering gates execution (false gating claim -> batch 2 skipped).
# claim suite batch-by-batch, claims-in-parallel. --perturb-check splits along
# the model-vs-orchestration line: the batching AUTHORITY (deps drive batch
# count) is asserted as pure .dag witnesses via ci-claim-gate's uniform perturb
# (bre_authority_rows_tsv), and the run-loop WALK-halt (false gating claim ->
# fail closed + batch 2 skipped) is a claim_executor --perturb-check receipt.
# Both claim_executor and ci-claim-gate are already built above for this job.
- name: v4 executor batch-runner dogfood (must-pass, discriminating)
run: bash scripts/v4-batch-executor-gate.sh --perturb-check
# §11.7.1 Class A safety floor (parallel matrix lane) -- the per-row PERTURB
Expand Down
170 changes: 57 additions & 113 deletions scripts/v4-batch-executor-gate.sh
Original file line number Diff line number Diff line change
Expand Up @@ -3,28 +3,47 @@
# v4.workflow.executor .dag is the BATCHING AUTHORITY for the claim suite.
#
# `claim_executor` evaluates the executor-decided plan
# (batch_runner.dag::bre_claim_batches → List<List<ClaimRef>>) and runs the
# suite batch-by-batch, claims-in-parallel. This gate asserts:
# (batch_runner.dag::bre_claim_batches -> List<List<ClaimRef>>) and runs the
# suite batch-by-batch, claims-in-parallel.
#
# green: the plan yields 2 batches and every claim passes (exit 0). The
# executor places the gating claim in batch 1 and the two derived
# claims in batch 2 (a later readiness layer).
# Model-first dissolution of the former inline-shell perturb scaffold (the awk
# roster projection + the three inline-python perturbs are gone). The gate now
# splits along the model-vs-orchestration line:
#
# green: the plan yields 2 batches and every claim passes (exit 0). The
# executor places the gating claim in batch 1 and the two derived
# claims in batch 2 (a later readiness layer).
#
# --perturb-check adds two discriminating receipts:
# authority: empty the .dag dependency list in a temp tree → the plan must
# collapse to 1 batch. Proves the host CONSUMES the .dag's
# batching (it is not a hand-coded mirror): change the model,
# the batches change, with zero host edit.
# fail-closed: rewrite the batch-1 (gating) witness body to `false` in a temp
# tree → the run must exit 1 AND never reach batch 2. Proves the
# executor's dependency ordering actually gates execution.
#
# [authority + degenerate] = MODEL semantics, run through ci-claim-gate's
# uniform witness-body->false perturb over batch_runner.dag's
# bre_authority_rows_tsv: the dependency input DRIVES the batch count
# (empty deps -> 1 batch, full deps -> 2, empty suite -> 0). The batching is
# computed by the .dag (parallel_executor_plan_from_dependencies); these are
# pure .dag witnesses, not a host re-resolve. Replaces the old inline-python
# "empty the dep list and re-run the host" + "empty the suite" perturbs.
#
# [run-loop walk] = CI-ORCHESTRATION behavior, host-resident in claim_executor
# (--perturb-check): planting the batch-1 gating witness->false must make the
# run fail closed AND halt the walk before batch 2. Tests ONLY the run-loop
# walk-halt; the batch structure/ordering it walks is the .dag's (asserted by
# the model witnesses above). Replaces the old inline-python gating perturb.
#
# [degenerate host] = CI-ORCHESTRATION fail-closed, exercised through a real
# consumer: claim_executor is driven with a deliberately empty plan
# (bre_degenerate_empty_plan -> []) and must exit non-zero — an empty run is
# never a successful run. Replaces the old inline-python "empty the suite and
# re-run the host" perturb; the model side (empty in -> zero out) is the
# bre_empty_suite_yields_no_batches witness above.

set -euo pipefail

root="$(git rev-parse --show-toplevel 2>/dev/null || pwd)"
cd "$root"

bin="${CLAIM_EXECUTOR:-target/release/claim_executor}"
exe="${CLAIM_EXECUTOR:-target/release/claim_executor}"
gate="${CI_CLAIM_GATE:-target/release/ci-claim-gate}"
plan_entry="src/v4/test/claim/workflow/batch_runner.dag"
perturb=0

Expand All @@ -34,13 +53,13 @@ case "${1:-}" in
*) echo "usage: $0 [--perturb-check]" >&2; exit 2 ;;
esac

if [[ ! -x "$bin" ]]; then
echo "error: claim_executor not found at $bin" >&2
if [[ ! -x "$exe" ]]; then
echo "error: claim_executor not found at $exe (build: cargo build -p v2-compiler --release)" >&2
exit 2
fi

echo "== green: executor-decided batches, every claim passes =="
out="$("$bin" --source-root src/v4 --plan-entry "$plan_entry" 2>&1)"
out="$("$exe" --source-root src/v4 --plan-entry "$plan_entry" 2>&1)"
echo "$out"
if ! grep -q "executor plan = 2 batch(es)" <<<"$out"; then
echo "FAIL: expected 2 executor-decided batches" >&2
Expand All @@ -56,107 +75,32 @@ if [[ "$perturb" -eq 0 ]]; then
exit 0
fi

tmp="$(mktemp -d)"
trap 'rm -rf "$tmp"' EXIT

echo "== perturb/authority: emptying the .dag dependency list must rebatch 2 -> 1 =="
cp -r src/v4 "$tmp/v4"
python3 - "$tmp/v4/test/claim/workflow/batch_runner.dag" <<'PY'
import sys
p = sys.argv[1]
s = open(p).read()
needle = """data bre_suite_dependencies: List<DependencyView> = [
bre_core_to_a_dependency,
bre_core_to_b_dependency
]"""
if needle not in s:
raise SystemExit("perturb: dependency-list anchor not found")
open(p, "w").write(s.replace(needle, "data bre_suite_dependencies: List<DependencyView> = []"))
PY
out_auth="$("$bin" --source-root "$tmp/v4" --plan-entry "$tmp/v4/test/claim/workflow/batch_runner.dag" 2>&1)"
echo "$out_auth"
if ! grep -q "executor plan = 1 batch(es)" <<<"$out_auth"; then
echo "FAIL: removing the .dag dependency did NOT rebatch to 1 — host is not consuming the executor" >&2
exit 1
echo "== perturb/authority + degenerate (MODEL): deps drive batch count, via ci-claim-gate =="
if [[ ! -x "$gate" ]]; then
echo "error: ci-claim-gate not found at $gate (build: cargo build -p ci_claim_gate --release)" >&2
exit 2
fi
echo "authority OK (model drives batching)"
"$gate" \
--source-root src/v4 \
--gate-entry "$plan_entry" \
--rows-fn bre_authority_rows_tsv \
--notice-title "batch-executor authority" \
--perturb-check
echo "authority OK (model drives batching; each witness red-under-mutation)"

echo "== perturb/fail-closed: a false batch-1 gating claim must stop before batch 2 =="
# Hermetic like the other two perturbs: work entirely in a tmp/v4 copy. The
# claim entry inside batch_runner.dag is repo-relative, so we also repoint
# bre_suite_entry at the tmp copy — then the host resolves the perturbed file,
# never the tracked one (no in-place mutation of the working tree).
rm -rf "$tmp/v4"
cp -r src/v4 "$tmp/v4"
tmp_gating="$tmp/v4/test/claim/workflow/affected_set_ci_runner.dag"
python3 - "$tmp/v4/test/claim/workflow/batch_runner.dag" "$tmp_gating" <<'PY'
import sys
br, gating = sys.argv[1], sys.argv[2]
# Repoint the suite entry at the tmp copy.
s = open(br).read()
needle = 'data bre_suite_entry: String = "src/v4/test/claim/workflow/affected_set_ci_runner.dag"'
if needle not in s:
raise SystemExit("perturb: bre_suite_entry anchor not found")
open(br, "w").write(s.replace(needle, f'data bre_suite_entry: String = "{gating}"'))
# Rewrite the gating witness body to `false` in the tmp copy.
fn = "ci_runner_narrow_selection_holds"
g = open(gating).read()
start = g.find(f"fn {fn}(")
if start < 0:
raise SystemExit(f"perturb: function {fn} not found")
brace = g.find("{", start)
depth = 0
i = brace
while i < len(g):
if g[i] == "{":
depth += 1
elif g[i] == "}":
depth -= 1
if depth == 0:
break
i += 1
open(gating, "w").write(g[:brace] + "{\n false\n}" + g[i + 1:])
PY
set +e
out_fc="$("$bin" --source-root "$tmp/v4" --plan-entry "$tmp/v4/test/claim/workflow/batch_runner.dag" 2>&1)"
code=$?
set -e
echo "$out_fc"
if [[ "$code" -eq 0 ]]; then
echo "FAIL: a false gating claim still exited 0" >&2
exit 1
fi
if grep -q "batch 2" <<<"$out_fc"; then
echo "FAIL: batch 2 ran despite a failed gating batch 1 (ordering not enforced)" >&2
exit 1
fi
echo "fail-closed OK (executor ordering gates execution)"
echo "== perturb/walk (ORCHESTRATION): false gating batch-1 -> fail closed AND halt before batch 2 =="
"$exe" --source-root src/v4 --plan-entry "$plan_entry" --perturb-check
echo "walk OK (run-loop halts dependents on a failed gate)"

echo "== perturb/degenerate: an empty suite (0 batches) must fail closed, not pass on 0 claims =="
rm -rf "$tmp/v4"
cp -r src/v4 "$tmp/v4"
python3 - "$tmp/v4/test/claim/workflow/batch_runner.dag" <<'PY'
import sys
p = sys.argv[1]
s = open(p).read()
needle = """data bre_suite_nodes: List<Node> = [
bre_core_node,
bre_a_node,
bre_b_node
]"""
if needle not in s:
raise SystemExit("perturb: suite-nodes anchor not found")
open(p, "w").write(s.replace(needle, "data bre_suite_nodes: List<Node> = []"))
PY
set +e
out_empty="$("$bin" --source-root "$tmp/v4" --plan-entry "$tmp/v4/test/claim/workflow/batch_runner.dag" 2>&1)"
code_empty=$?
set -e
echo "$out_empty"
if [[ "$code_empty" -eq 0 ]]; then
echo "FAIL: a 0-batch executor plan exited 0 (vacuous pass)" >&2
echo "== perturb/degenerate (ORCHESTRATION): a 0-batch plan must fail closed, not pass on 0 claims =="
# Drive claim_executor with a deliberately EMPTY plan (bre_degenerate_empty_plan -> [])
# and require a non-zero exit. Exercises the host fail-closed guard (an empty run is never
# a successful run) through a real .dag consumer — no temp-tree, no shell scaffold. Replaces
# the old inline-python "empty the suite nodes and re-run" perturb.
if "$exe" --source-root src/v4 --plan-entry "$plan_entry" --plan-function bre_degenerate_empty_plan; then
echo "FAIL: claim_executor accepted a 0-batch plan (vacuous pass)" >&2
exit 1
fi
echo "degenerate OK (empty plan fails closed)"
echo "degenerate OK (host fails closed on an empty plan)"

echo "ALL OK"
Loading
Loading