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
16 changes: 12 additions & 4 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -671,14 +671,22 @@ jobs:
key: cargo-ci-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('**/Cargo.lock', 'rust-toolchain.toml') }}
restore-keys: |
cargo-ci-${{ runner.os }}-${{ runner.arch }}-
- name: Cache gunbc binary (v4 lens CI)
- name: Cache gunbc + claim_batch binaries (v4 lens CI)
id: v4-v2-bin
uses: actions/cache@v5
with:
path: target/release/gunbc
key: gunbc-bin-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('src/v2/stage0/src/**', 'src/v2/stage0/Cargo.toml', 'Cargo.toml', '**/Cargo.lock', 'rust-toolchain.toml') }}
# This job runs the node-frontier gate, which needs BOTH gunbc and the
# claim_batch batch runner. Distinct key namespace ('gunbc-lens-bin-')
# from the gunbc-only jobs (ci_floor / ci_floor_emit / v4_lens_gate,
# key 'gunbc-bin-') so we never restore a gunbc-only cache and skip the
# build with claim_batch absent — both binaries are produced by the same
# `cargo build -p v2-compiler --release` and cached together.
path: |
target/release/gunbc
target/release/claim_batch
key: gunbc-lens-bin-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('src/v2/stage0/src/**', 'src/v2/stage0/Cargo.toml', 'Cargo.toml', '**/Cargo.lock', 'rust-toolchain.toml') }}
restore-keys: |
gunbc-bin-${{ runner.os }}-${{ runner.arch }}-
gunbc-lens-bin-${{ runner.os }}-${{ runner.arch }}-
- name: Build v2 compiler (v4 lens CI)
if: steps.v4-v2-bin.outputs.cache-hit != 'true'
run: bash .github/ci-floor/with-sccache-retry.sh cargo build -p v2-compiler --release
Expand Down
91 changes: 71 additions & 20 deletions scripts/v4-affected-set-node-frontier-gate.sh
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,10 @@ root="$(git rev-parse --show-toplevel 2>/dev/null || pwd)"
cd "$root"

bin="${V2_COMPILER:-target/release/gunbc}"
# Batch witness runner: resolves one shared --entry closure once and runs many
# witnesses in a single process. Used for the GREEN pass only; the perturb pass
# stays per-row through `$bin` (each row mutates a different function).
bin_batch="${CLAIM_BATCH:-target/release/claim_batch}"
perturb=0

case "${1:-}" in
Expand All @@ -30,6 +34,11 @@ if [[ ! -x "$bin" ]]; then
exit 2
fi

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

gate_model="src/v4/test/claim/workflow/affected_set_ci_runner.dag"
affected_testgen_gate_model="src/v4/test/claim/workflow/affected_testgen_ci_runner.dag"

Expand Down Expand Up @@ -89,6 +98,32 @@ run_row() {
"$bin" run --source-root "$source_root" --entry "$entry" --function "$function" --claim-run
}

# GREEN pass for a stream of "<entry>\t<function>" lines on stdin: group the
# functions by their shared --entry and resolve each entry's import closure ONCE
# (via claim_batch), running all of that entry's witnesses in a single process.
# This collapses the N-rows-share-one-entry green pass from N full-tree resolves
# to one. Fail-closed: a non-zero claim_batch exit (any witness red) aborts.
batch_green_pass() {
local title="$1"
local -A entry_fns=()
local -a entry_order=()
local entry function
while IFS=$'\t' read -r entry function; do
[[ -z "$entry" ]] && continue
if [[ -z "${entry_fns[$entry]+x}" ]]; then
entry_order+=("$entry")
fi
entry_fns[$entry]+="${function},"
done
local e fns
for e in "${entry_order[@]}"; do
fns="${entry_fns[$e]%,}"
echo "::group::${title} (batch green): ${e}"
"$bin_batch" --source-root src/v4 --entry "$e" --functions "$fns" --claim-run
echo "::endgroup::"
done
}

perturb_function_to_false() {
local file="$1" function="$2"
python3 - "$file" "$function" <<'PY'
Expand Down Expand Up @@ -128,18 +163,31 @@ if [[ -z "$expected_count" ]]; then
exit 2
fi

row_count=0
# Collect every row first so the GREEN pass can resolve each shared entry once.
node_frontier_rows=()
while IFS= read -r member; do
[[ -z "$member" ]] && continue
row="$(project_list_member_row "$member")"
if [[ -z "$row" ]]; then
echo "error: list member $member missing AffectedSetNodeFrontierClaimRunRow binding in $gate_model" >&2
exit 2
fi
node_frontier_rows+=("$row")
done < <(list_claim_run_row_members)

if [[ "${#node_frontier_rows[@]}" -eq 0 ]]; then
echo "error: ci_runner_node_frontier_claim_run_rows has no members in $gate_model" >&2
exit 2
fi

# GREEN pass: one resolve per shared entry, all that entry's witnesses in it.
printf '%s\n' "${node_frontier_rows[@]}" | cut -f2,3 \
| batch_green_pass "affected-set node-frontier"

# PERTURB pass + count: one mutated resolve per row (each mutates a different fn).
row_count=0
for row in "${node_frontier_rows[@]}"; do
IFS=$'\t' read -r label entry function <<< "$row"
echo "::group::affected-set node-frontier: ${label}"
run_row "src/v4" "$entry" "$function"
echo "::endgroup::"

if [[ "$perturb" -eq 1 ]]; then
tmp="$(mktemp -d)"
Expand All @@ -158,12 +206,7 @@ while IFS= read -r member; do
trap - EXIT
fi
row_count=$((row_count + 1))
done < <(list_claim_run_row_members)

if [[ "$row_count" -eq 0 ]]; then
echo "error: ci_runner_node_frontier_claim_run_rows has no members in $gate_model" >&2
exit 2
fi
done

if [[ "$row_count" -ne "$expected_count" ]]; then
echo "error: node-frontier gate projected ${row_count} rows; modeled count is ${expected_count}" >&2
Expand Down Expand Up @@ -286,18 +329,31 @@ if [[ -z "$expected_affected_testgen_count" ]]; then
exit 2
fi

affected_testgen_count=0
# Collect every row first so the GREEN pass can resolve each shared entry once.
affected_testgen_rows=()
while IFS= read -r member; do
[[ -z "$member" ]] && continue
row="$(project_affected_testgen_row "$member")"
if [[ -z "$row" ]]; then
echo "error: list member $member missing AffectedTestgenClaimRunRow binding in $affected_testgen_gate_model" >&2
exit 2
fi
affected_testgen_rows+=("$row")
done < <(list_affected_testgen_row_members)

if [[ "${#affected_testgen_rows[@]}" -eq 0 ]]; then
echo "error: affected_testgen_claim_run_rows has no members in $affected_testgen_gate_model" >&2
exit 2
fi

# GREEN pass: one resolve per shared entry, all that entry's witnesses in it.
printf '%s\n' "${affected_testgen_rows[@]}" | cut -f2,3 \
| batch_green_pass "affected-testgen"

# PERTURB pass + count: one mutated resolve per row (each mutates a different fn).
affected_testgen_count=0
for row in "${affected_testgen_rows[@]}"; do
IFS=$'\t' read -r label entry function <<< "$row"
echo "::group::affected-testgen: ${label}"
run_row "src/v4" "$entry" "$function"
echo "::endgroup::"

if [[ "$perturb" -eq 1 ]]; then
tmp="$(mktemp -d)"
Expand All @@ -316,12 +372,7 @@ while IFS= read -r member; do
trap - EXIT
fi
affected_testgen_count=$((affected_testgen_count + 1))
done < <(list_affected_testgen_row_members)

if [[ "$affected_testgen_count" -eq 0 ]]; then
echo "error: affected_testgen_claim_run_rows has no members in $affected_testgen_gate_model" >&2
exit 2
fi
done

if [[ "$affected_testgen_count" -ne "$expected_affected_testgen_count" ]]; then
echo "error: affected-testgen gate projected ${affected_testgen_count} rows; modeled count is ${expected_affected_testgen_count}" >&2
Expand Down
8 changes: 8 additions & 0 deletions src/v2/stage0/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -23,3 +23,11 @@ path = "src/main.rs"
name = "regen_stage0"
path = "src/bin/regen_stage0.rs"
# cache-bust-v2-binary-20260526

# Batch claim runner: resolve one --entry closure once, run many witnesses.
# Hand-written CI tool (like regen_stage0); reuses the v2-compiler lib, does NOT
# go through the generated main.rs / emit stage. Amortizes the per-row full-tree
# resolve in the v4 node-frontier CI gate's green pass.
[[bin]]
name = "claim_batch"
path = "src/bin/claim_batch.rs"
158 changes: 158 additions & 0 deletions src/v2/stage0/src/bin/claim_batch.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
//! Batch Bool-witness runner: resolve ONE entry's import closure once, then run
//! many witness functions against the shared resolved graph.
//!
//! Motivation. The v4 node-frontier CI gate
//! (`scripts/v4-affected-set-node-frontier-gate.sh`) runs N Bool witnesses that
//! ALL share a single `--entry` file, differing only in `--function`. Invoking
//! `gunbc run --entry <E> --function <F> --claim-run` once per row re-resolves
//! the entire `src/v4` module closure N times (~5-13s each — the
//! `build_module_index` + closure-compile cost dominates; the witness eval
//! itself is sub-second). This bin walks that resolve ONCE and loops the
//! functions, collapsing N resolves to 1 for the green pass.
//!
//! The gate's perturb pass still runs per-row through `gunbc run`: each row
//! mutates a DIFFERENT function to `false` in its own temp source-root, so those
//! resolves are genuinely distinct and cannot share an index.
//!
//! This is a hand-written CLI bin (like `regen_stage0`), deliberately NOT routed
//! through the generated `main.rs` / emit stage — so adding this capability
//! touches no load-bearing pipeline stage. It reuses the same resolve/run
//! primitives the `gunbc run --claim-run` path uses (see
//! `cli_run::resolve_entry_graph` / `cli_run::run_claim`).
//!
//! Usage:
//! claim_batch --source-root <dir> [--source-root <dir> ...] \
//! --entry <file.dag> \
//! --functions f1,f2,... [--function f3 ...] [--claim-run]
//!
//! Exit codes: 0 = all witnesses returned Bool(true); 1 = any witness failed,
//! returned non-Bool, raised a runtime error, or resolve failed; 2 = usage error.

// Binary entrypoint: it reports witness results directly on stdout/stderr, so
// println!/eprintln! are appropriate here (the disallowed-macros lint is aimed
// at library crates that should return structured errors). The generated main.rs
// carries the same allow.
#![allow(clippy::disallowed_macros)]

use std::process::ExitCode;

use v2_compiler::cli_run::{resolve_entry_graph, run_claim, ClaimOutcome};

fn require_value(args: &[String], idx: usize, flag: &str) -> Result<String, ExitCode> {
match args.get(idx) {
Some(v) => Ok(v.clone()),
None => {
eprintln!("claim_batch: {} requires a value", flag);
Err(ExitCode::from(2))
}
}
}

fn run() -> Result<ExitCode, ExitCode> {
let args: Vec<String> = std::env::args().collect();
let mut source_roots: Vec<String> = Vec::new();
let mut entry: Option<String> = None;
let mut functions: Vec<String> = Vec::new();

let mut i = 1;
while i < args.len() {
match args[i].as_str() {
"--source-root" => {
i += 1;
source_roots.push(require_value(&args, i, "--source-root")?);
}
"--entry" => {
i += 1;
entry = Some(require_value(&args, i, "--entry")?);
}
"--function" => {
i += 1;
functions.push(require_value(&args, i, "--function")?);
}
"--functions" => {
i += 1;
let csv = require_value(&args, i, "--functions")?;
functions.extend(
csv.split(',')
.map(|s| s.trim())
.filter(|s| !s.is_empty())
.map(|s| s.to_string()),
);
}
// Accepted for call-site parity with `gunbc run`; this bin is always
// claim-run (Bool witnesses).
"--claim-run" => {}
other => {
eprintln!("claim_batch: unknown argument: {}", other);
return Err(ExitCode::from(2));
}
}
i += 1;
}

if source_roots.is_empty() {
eprintln!("claim_batch: provide at least one --source-root");
return Err(ExitCode::from(2));
}
let entry = match entry {
Some(e) => e,
None => {
eprintln!("claim_batch: --entry <file.dag> is required");
return Err(ExitCode::from(2));
}
};
if functions.is_empty() {
eprintln!("claim_batch: provide at least one --function or --functions");
return Err(ExitCode::from(2));
}

// Resolve the entry's import closure ONCE.
let (graph, source_indices) = match resolve_entry_graph(&source_roots, &entry) {
Ok(pair) => pair,
Err(msg) => {
eprintln!("claim_batch: resolve failed for {}:\n{}", entry, msg);
return Err(ExitCode::from(1));
}
};
eprintln!(
"claim_batch: resolved {} once; running {} witness(es)",
entry,
functions.len()
);

// Run each witness against the shared graph.
let mut any_failed = false;
for function in &functions {
match run_claim(&graph, source_indices.clone(), function) {
ClaimOutcome::Pass => println!("PASS {}", function),
ClaimOutcome::Fail => {
println!("FAIL {}", function);
any_failed = true;
}
ClaimOutcome::NotBool { got } => {
println!(
"FAIL {} (returned `{}`, not Bool; --claim-run entries must return Bool)",
function, got
);
any_failed = true;
}
ClaimOutcome::RuntimeError { message } => {
println!("FAIL {} (runtime error: {})", function, message);
any_failed = true;
}
}
}

if any_failed {
Ok(ExitCode::from(1))
} else {
Ok(ExitCode::SUCCESS)
}
}

fn main() -> ExitCode {
match run() {
Ok(code) => code,
Err(code) => code,
}
}
Loading
Loading