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
62 changes: 8 additions & 54 deletions .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -45,37 +45,14 @@ jobs:
if [ -x "$CARGO_HOME/bin/cargo" ]; then CARGO_BIN="$CARGO_HOME/bin/cargo"; else CARGO_BIN="$(command -v cargo || true)"; fi
if [ -z "$CARGO_BIN" ]; then echo "::error::no cargo binary: neither the isolated $CARGO_HOME/bin/cargo shim nor PATH carries one"; exit 1; fi
echo "CARGO_BIN=$CARGO_BIN" >> "$GITHUB_ENV"
- name: Discriminate private homes from a hostile legacy writer
run: |
# dissolve-on: ci_hostile_legacy_writer_discriminator_script -- foreign-executor concurrency control proving readers sharing a mutable toolchain path are disrupted by a hostile reinstall while readers bound to the job-private CARGO_HOME are unaffected. Its process synchronization, executable replacement, and observations remain shell until a typed concurrent filesystem/tool-execution interference probe effect lands on host_effect_apply (shell-to-intent Phase 2); neither the environment-binding effect nor the toolchain-selection effect can replace this observation
set -eu
ROOT="$RUNNER_TEMP/gunbc-hostile-toolchain-writer"
rm -rf "$ROOT"
mkdir -p "$ROOT"
await_barrier() { WAIT_PATH=$1; WAIT_LABEL=$2; I=0; while [ ! -e "$WAIT_PATH" ]; do I=$((I + 1)); if [ "$I" -gt 3000 ]; then echo "::error::hostile-writer $WAIT_LABEL barrier not reached: $WAIT_PATH" >&2; return 1; fi; sleep 0.01; done; }
run_arm() {
ARM=$1; READER_HOME=$2; LEGACY_HOME=$3
mkdir -p "$READER_HOME/bin" "$LEGACY_HOME/bin" "$ARM"
printf '#!/bin/sh\nprintf safe\n' > "$READER_HOME/bin/toolchain-probe"
chmod +x "$READER_HOME/bin/toolchain-probe"
( await_barrier "$ARM/writer-ready" reader-a-writer-ready && touch "$ARM/reader-a-observed" && [ "$("$READER_HOME/bin/toolchain-probe")" = safe ] ) & A=$!
( await_barrier "$ARM/writer-ready" reader-b-writer-ready && touch "$ARM/reader-b-observed" && [ "$("$READER_HOME/bin/toolchain-probe")" = safe ] ) & B=$!
( printf '#!/bin/sh\nprintf hostile\n' > "$ARM/reinstall" && chmod +x "$ARM/reinstall" && mv -f "$ARM/reinstall" "$LEGACY_HOME/bin/toolchain-probe" && touch "$ARM/writer-ready" && await_barrier "$ARM/readers-done" writer-readers-done ) & C=$!
if wait "$A"; then AS=0; else AS=$?; fi; if wait "$B"; then BS=0; else BS=$?; fi; touch "$ARM/readers-done"; if wait "$C"; then CS=0; else CS=$?; fi
if [ "$CS" -ne 0 ] || [ ! -e "$ARM/reader-a-observed" ] || [ ! -e "$ARM/reader-b-observed" ]; then echo "::error::hostile-writer control failed before reader comparison in $ARM" >&2; return 2; fi
if [ "$AS" -eq 0 ] && [ "$BS" -eq 0 ]; then return 0; else return 1; fi
}
SHARED="$ROOT/shared"
if run_arm "$ROOT/shared-arm" "$SHARED" "$SHARED"; then SHARED_STATUS=0; else SHARED_STATUS=$?; fi
if [ "$SHARED_STATUS" -ne 1 ]; then echo "::error::hostile writer shared-arm expected reader interference, status=$SHARED_STATUS" >&2; exit 1; fi
LEGACY="$ROOT/legacy"
case "${CARGO_HOME:-}" in "$RUNNER_TEMP/cargo") PRIVATE_READER="$CARGO_HOME" ;; *) PRIVATE_READER="$LEGACY" ;; esac
if run_arm "$ROOT/private-arm" "$PRIVATE_READER" "$LEGACY"; then PRIVATE_STATUS=0; else PRIVATE_STATUS=$?; fi
if [ "$PRIVATE_STATUS" -ne 0 ]; then echo "::error::hostile legacy writer affected private-home readers, status=$PRIVATE_STATUS" >&2; exit 1; fi
- name: Build the witness fold
id: build_witness_fold
run: |
cargo build --release -p v1-compiler --bins
- name: Discriminate private homes from a hostile legacy writer
run: |
ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd)
"$ROOT/target/release/gunbc" run --source-root "$ROOT/dag" --source-root "$ROOT/src/v2" --entry dag/gunbc/toolchain_home_interference_probe.dag --function toolchain_home_interference_probe_wet
- name: Record the toolchain environment
run: |
echo "host=$(hostname) runner=${RUNNER_NAME:-unset}"
Expand Down Expand Up @@ -121,37 +98,14 @@ jobs:
if [ -x "$CARGO_HOME/bin/cargo" ]; then CARGO_BIN="$CARGO_HOME/bin/cargo"; else CARGO_BIN="$(command -v cargo || true)"; fi
if [ -z "$CARGO_BIN" ]; then echo "::error::no cargo binary: neither the isolated $CARGO_HOME/bin/cargo shim nor PATH carries one"; exit 1; fi
echo "CARGO_BIN=$CARGO_BIN" >> "$GITHUB_ENV"
- name: Discriminate private homes from a hostile legacy writer
run: |
# dissolve-on: ci_hostile_legacy_writer_discriminator_script -- foreign-executor concurrency control proving readers sharing a mutable toolchain path are disrupted by a hostile reinstall while readers bound to the job-private CARGO_HOME are unaffected. Its process synchronization, executable replacement, and observations remain shell until a typed concurrent filesystem/tool-execution interference probe effect lands on host_effect_apply (shell-to-intent Phase 2); neither the environment-binding effect nor the toolchain-selection effect can replace this observation
set -eu
ROOT="$RUNNER_TEMP/gunbc-hostile-toolchain-writer"
rm -rf "$ROOT"
mkdir -p "$ROOT"
await_barrier() { WAIT_PATH=$1; WAIT_LABEL=$2; I=0; while [ ! -e "$WAIT_PATH" ]; do I=$((I + 1)); if [ "$I" -gt 3000 ]; then echo "::error::hostile-writer $WAIT_LABEL barrier not reached: $WAIT_PATH" >&2; return 1; fi; sleep 0.01; done; }
run_arm() {
ARM=$1; READER_HOME=$2; LEGACY_HOME=$3
mkdir -p "$READER_HOME/bin" "$LEGACY_HOME/bin" "$ARM"
printf '#!/bin/sh\nprintf safe\n' > "$READER_HOME/bin/toolchain-probe"
chmod +x "$READER_HOME/bin/toolchain-probe"
( await_barrier "$ARM/writer-ready" reader-a-writer-ready && touch "$ARM/reader-a-observed" && [ "$("$READER_HOME/bin/toolchain-probe")" = safe ] ) & A=$!
( await_barrier "$ARM/writer-ready" reader-b-writer-ready && touch "$ARM/reader-b-observed" && [ "$("$READER_HOME/bin/toolchain-probe")" = safe ] ) & B=$!
( printf '#!/bin/sh\nprintf hostile\n' > "$ARM/reinstall" && chmod +x "$ARM/reinstall" && mv -f "$ARM/reinstall" "$LEGACY_HOME/bin/toolchain-probe" && touch "$ARM/writer-ready" && await_barrier "$ARM/readers-done" writer-readers-done ) & C=$!
if wait "$A"; then AS=0; else AS=$?; fi; if wait "$B"; then BS=0; else BS=$?; fi; touch "$ARM/readers-done"; if wait "$C"; then CS=0; else CS=$?; fi
if [ "$CS" -ne 0 ] || [ ! -e "$ARM/reader-a-observed" ] || [ ! -e "$ARM/reader-b-observed" ]; then echo "::error::hostile-writer control failed before reader comparison in $ARM" >&2; return 2; fi
if [ "$AS" -eq 0 ] && [ "$BS" -eq 0 ]; then return 0; else return 1; fi
}
SHARED="$ROOT/shared"
if run_arm "$ROOT/shared-arm" "$SHARED" "$SHARED"; then SHARED_STATUS=0; else SHARED_STATUS=$?; fi
if [ "$SHARED_STATUS" -ne 1 ]; then echo "::error::hostile writer shared-arm expected reader interference, status=$SHARED_STATUS" >&2; exit 1; fi
LEGACY="$ROOT/legacy"
case "${CARGO_HOME:-}" in "$RUNNER_TEMP/cargo") PRIVATE_READER="$CARGO_HOME" ;; *) PRIVATE_READER="$LEGACY" ;; esac
if run_arm "$ROOT/private-arm" "$PRIVATE_READER" "$LEGACY"; then PRIVATE_STATUS=0; else PRIVATE_STATUS=$?; fi
if [ "$PRIVATE_STATUS" -ne 0 ]; then echo "::error::hostile legacy writer affected private-home readers, status=$PRIVATE_STATUS" >&2; exit 1; fi
- name: Build the witness fold
id: build_witness_fold
run: |
cargo build --release -p v1-compiler --bin claim_executor --bin gunbc
- name: Discriminate private homes from a hostile legacy writer
run: |
ROOT=$(git rev-parse --show-toplevel 2>/dev/null || pwd)
"$ROOT/target/release/gunbc" run --source-root "$ROOT/dag" --source-root "$ROOT/src/v2" --entry dag/gunbc/toolchain_home_interference_probe.dag --function toolchain_home_interference_probe_wet
- name: Record the toolchain environment
run: |
echo "host=$(hostname) runner=${RUNNER_NAME:-unset}"
Expand Down
8 changes: 5 additions & 3 deletions dag/gunbc/auth/materialized_secret.dag
Original file line number Diff line number Diff line change
Expand Up @@ -275,11 +275,13 @@ fn with_materialized_ssh_key_file<R>(
// agent alive across several steps of its own job, authenticating nothing
// about a fleet host. That case cannot bind to HostEffectTransport at
// all: gunbc.host_effect HostEffectIntent.target is a NodeControlPlane,
// and both NodeControlPlane arms (HostOs, BmcController) require a
// and both fleet-addressed NodeControlPlane arms (HostOs, BmcController) require a
// gunbc.fleet_intent.ComputeHost — a full enrolled hardware identity a
// transient runner does not have and should not fabricate.
// gunbc.ci_deploy_target_host already refuses the identical conflation
// for LocalShell apply ("runner identity does not prove target host"). A
// RunnerLocalHost now provides an honest target only for effects explicitly modeled as
// runner-local; it does not make fleet-targeted secret materialization admissible.
// gunbc.ci_deploy_target_host already refuses the identical conflation for LocalShell apply
// ("runner identity does not prove target host"). A
// future EnvVar or StdinPassword binding written to solve that case would
// materialize correctly and then have nowhere honest to dissolve to — the
// module would look reused when the subject had actually changed
Expand Down
3 changes: 2 additions & 1 deletion dag/gunbc/ci_spec.dag
Original file line number Diff line number Diff line change
Expand Up @@ -651,7 +651,8 @@ fn gunbc_ci_multi_principal_probe_invoke() -> String {
// THE MARKER'S ORIGINAL TRIGGER WAS UNFALSIFIABLE, AND THIS ROW RECORDS WHY BEFORE
// DELETING IT (parent-session finding, 2026-08-21). It read "DISSOLVES WHEN the typed
// secret-materialization effect... lands on host_effect_apply" — but host_effect_apply's
// HostEffectIntent.target is a NodeControlPlane, and both its arms require a ComputeHost.
// HostEffectIntent.target is a NodeControlPlane. Fleet effects use arms carrying ComputeHost;
// explicitly runner-local effects use RunnerLocalHost without fabricating a fleet identity.
// An ephemeral GitHub Actions runner is not a ComputeHost the fleet models; there was no
// host_effect_apply arm this step could ever land on, so the condition named could never
// occur. That is the same defect class as the trigger corrected alongside it this session
Expand Down
4 changes: 4 additions & 0 deletions dag/gunbc/codex_supervised_turn_run.dag
Original file line number Diff line number Diff line change
Expand Up @@ -100,6 +100,10 @@ fn codex_supervised_worker_turn_apply(
CodexSupervisedTurnRefused {
reason: "Codex supervised worker turn returned unexpected ConvergePlanApplied evidence" as NonEmptyStr,
}
ToolchainHomeInterferenceDiscriminated =>
CodexSupervisedTurnRefused {
reason: "Codex supervised worker turn returned unexpected ToolchainHomeInterferenceDiscriminated evidence" as NonEmptyStr,
}
}
NotConverged { reason: why, applied: _ } =>
CodexSupervisedTurnRefused { reason: why as NonEmptyStr }
Expand Down
3 changes: 3 additions & 0 deletions dag/gunbc/host_effect.dag
Original file line number Diff line number Diff line change
Expand Up @@ -77,10 +77,12 @@ type HostEffect =
| ReplaceRunnerIncarnation { from: LocalRunnerSlotIncarnation, cause: RunnerReplacementCause }
| ObserveRunnerLocalState { slot: RunnerSlotIdentity }
| ObserveGitHubRunnerRegistration { slot: RunnerSlotIdentity, organization: NonEmptyStr }
| ProbeToolchainHomeInterference {}

type NodeControlPlane =
HostOs { node: ComputeHost }
| BmcController { node: ComputeHost }
| RunnerLocalHost

type Drive = OneShot | ConvergeLoop

Expand Down Expand Up @@ -190,6 +192,7 @@ type HostEffectIntent {
type HostEffectEvidence =
ShellEffectApplied { exit_code: Int, stdout: String, stderr: String }
| ConvergePlanApplied { exit_code: Int, stdout: String }
| ToolchainHomeInterferenceDiscriminated

fn host_effect_drive_from_evidence(evidence: IdempotencyEvidence) -> Drive {
if host_effect_is_converge_loop_evidence(evidence: evidence) {
Expand Down
Loading
Loading