Hedronite · Ops Lesson · Kubernetes track · Thu 2026-10-15

Fail-closed pull request gates name parity, regenerate-and-diff, and nix flake check for a policy-law catalog

A weakened law passed two gates. Only the generator noticed.

Lesson Class: Ops (T2 · phase B)
Track: Kubernetes track · day 85
Referent: bend-gate.sh · checks.law-catalog · git diff --exit-code
Not a repeat: not 10-12 flake packages · 10-13 Nickel · 10-14 Key Vault
Paired Cert: CKS RBAC escalate, bind, aggregation
Count the Names
Parity catches drift, not weakness.
Seal the Inputs
The Nix check sees only what it is handed.
Regenerate, Then Diff
A hand edit is drift.
Two files that agree can both be wrong.

A catalog of 53 rules can pass every consistency check while one rule is quietly flipped from Refuse to Allow. Three gate layers, run against three simulated pull requests, show which layer catches which change.

The problem

A reviewer opens a pull request that touches one file in a policy catalog. The diff shows Refuse{} turning into Allow{} in two places, and the two edits agree with each other, so the change reads as a consistent tidy-up. The continuous integration (CI) run is green, the reviewer approves, and a rule that used to forbid a case now permits it. Nothing complained, because nothing was checking the one property that mattered.

The example repository is an open-source Rust policy kit with 53 rules, which it calls laws. Each law lives in three files that must agree. laws/NAMES lists one law name per line. laws/LAWS.bend writes each law in Bend, a programming language, as a verdict function plus a law statement that pins the forbidden case to Refuse. laws/PROOF.bend is a proof file that must name every law. A pull request gate is the set of automated checks that must pass before a change can merge. The question is what that gate needs so that a change which breaks or weakens a law cannot merge.

The DevOps Handbook states the stance a gate should take: "Whenever someone introduces a change that causes our build or automated tests to fail, no new work is allowed to enter the system until the problem is fixed." It adds that teams may even configure version control to prevent further commits until the first stage of the pipeline is green again. It also warns that ignoring a broken pipeline makes it "ever more difficult to bring our applications and environment back into a deployable state." (The DevOps Handbook, PDF pp. 201 to 203.) That stance only helps if the gate can actually fail on the changes that matter. The kit's own documentation adds a rule for this catalog: "Do not weaken a law to make a proof pass."

The idea, in plain words

A catalog like this needs three gate layers, and each one catches a different class of change. The first is name parity: a small shell script checks that the three files list the same 53 names, so it catches files that drifted apart. The second runs that same script inside nix flake check, in a clean build environment, so it also catches a gate that only passes because of something on one developer's machine. The third is regenerate-and-diff: a generator rebuilds all three files from one table, and the pull request is refused if the committed files differ from the regenerated ones, so it catches hand edits that keep the files consistent with each other. Every layer has to be fail-closed, meaning a missing file or a mismatch is an error and never a pass. The lab results below show why the third layer is needed. A weakened law passed the first two layers and was refused only by the third.

Concept A: name parity, the cheapest gate

A check is fail-closed when every situation it cannot confirm as good ends in a failure, such as a missing file, a count that does not match, or an absent tool. The opposite is fail-open, where the unknown case is waved through. A gate protects you in the cases nobody predicted, and nobody writes a deliberate passing branch for a case they did not predict. Otherwise, deleting PROOF.bend would be the easiest way to turn a proof check green.

Name parity means the same set of names appears in every file that must mention them. It is the cheapest layer because it only counts lines and runs grep. Here is the first part of the kit's gate script, scripts/bend-gate.sh, with its header comment trimmed:

...
set -eu
export BEND_NO_TELEMETRY="${BEND_NO_TELEMETRY:-1}"

root=$(CDPATH= cd -- "$(dirname "$0")/.." && pwd)
laws_dir=${RUST_TOPS_LAWS:-"$root/laws"}
laws="$laws_dir/LAWS.bend"
proof=${1:-"$laws_dir/PROOF.bend"}
names="$laws_dir/NAMES"

if [ ! -f "$laws" ] || [ ! -f "$proof" ] || [ ! -f "$names" ]; then
  printf 'bend-gate: missing laws pack under %s\n' "$laws_dir" >&2
  exit 2
fi

expected=$(grep -c . "$names")
got=$(grep -c '^law ' "$laws" || true)
if [ "$got" -ne "$expected" ]; then
  printf 'bend-gate: LAWS.bend has %s law statements, expected %s\n' "$got" "$expected" >&2
  exit 1
fi

while IFS= read -r law; do
  [ -n "$law" ] || continue
  if ! grep -q "^law ${law}:" "$laws"; then
    printf 'bend-gate: LAWS.bend does not state %s\n' "$law" >&2
    exit 1
  fi
  if ! grep -q "$law" "$proof"; then
    printf 'bend-gate: proof does not name %s\n' "$law" >&2
    exit 1
  fi
done < "$names"

The line set -eu makes the shell stop when a command fails (-e) and treat an unset variable as an error (-u). That is the fail-closed foundation, because a typo in a variable name cannot silently become an empty string. The next line exports BEND_NO_TELEMETRY for the Bend tool, defaulting it to 1. This lesson does not depend on it, and no Bend tool was run in the lab. The variable laws_dir takes its value from the environment variable RUST_TOPS_LAWS if set, and otherwise from the laws directory next to the script. The Nix check in the next section uses that override. The proof path can also be given as the first argument, which is how a copy of the proof with one law removed can be tested.

The first real test is the missing-file branch. If any of the three files is absent, the script prints a message to standard error and exits with code 2, a different code from the mismatch cases so a log reader can tell "nothing to check" from "checked and wrong". The count check then compares expected, the number of non-empty lines in NAMES, with got, the number of lines in LAWS.bend that start with law . The || true after the second grep keeps the script alive when grep reports no match, so the mismatch message prints instead of the script stopping early. The loop then reads each name and requires two things: a line starting law <name>: in LAWS.bend, and the name appearing somewhere in PROOF.bend.

The second half of the script decides what happens after name parity succeeds:

if [ "${BEND_GATE_NAMES_ONLY:-0}" = "1" ]; then
  printf 'bend-gate: %s laws named\n' "$expected"
  exit 0
fi

if ! command -v bend >/dev/null 2>&1; then
  printf 'bend-gate: %s laws named; bend not on PATH (names-only)\n' "$expected"
  exit 0
fi

dir=$(CDPATH= cd -- "$(dirname "$proof")" && pwd)
name=$(basename "$proof")
cd "$dir"
exec bend "$name"

If BEND_GATE_NAMES_ONLY is set to 1, the script reports success right after name parity and never looks for the Bend tool. Otherwise it asks the shell whether bend is on the PATH, the list of directories searched for commands. If bend is missing it still exits 0 and says so in its message. If bend is present, the script changes into the proof's directory and replaces itself with bend PROOF.bend, which the kit's README says "exits 0" when the proof holds. That final step is the only place a Bend proof is evaluated. It never ran in the lab, because the lab machine had no bend binary.

The lab simulated two pull requests against these checks. PR A appended mutants_skip_needs_reason to NAMES without writing the law. PR B changed PROOF.bend so that Laws.single_deny_site() became Laws.single_deny(). The real output for each, from the names-only gate:

== PR A: add a law name to NAMES, no law written ==
-- names-only gate
bend-gate: LAWS.bend has 53 law statements, expected 54
exit=1
== PR B: proof stops naming a law ==
-- names-only gate
bend-gate: proof does not name single_deny_site
exit=1

Both are caught by name parity alone. PR A fails on the count because NAMES now lists 54 laws while LAWS.bend states 53. PR B fails in the loop, because the only place PROOF.bend mentioned single_deny_site was the call that the edit renamed.

The pitfall is that this gate can exit 0 having done less than its name suggests. When a developer runs it with no bend installed, the baseline lab output reads:

-- gate as a developer runs it
bend-gate: 53 laws named; bend not on PATH (names-only)
exit=0

A green result here means the names agree, not that any proof ran. The diagnostic is to read the last line of the log, which says "names-only" when the proof was skipped. This reads against the catalog's own content. One of the 53 laws is missing_tool_not_green, whose generated statement is {tool_verdict(ToolMissing{}) == Refuse{} : Verdict}: a missing tool must be refused, not passed. The script is honest in its message but generous in its exit code, so a CI job that wants the proof itself, and not just names, should fail when the gate fails or when its output contains names-only, for example with out=$(sh scripts/bend-gate.sh) && ! printf '%s\n' "$out" | grep -q names-only on a runner that is supposed to have bend. The obvious shorter form, ! sh scripts/bend-gate.sh | grep -q names-only, is itself fail-open: when the gate fails it prints its error to standard error, grep finds nothing, and the ! turns that into success. (The longer form was checked against three stand-in scripts, one names-only, one failing and one passing, and exited 1, 1 and 0. It was not run against a real bend.) The Nix check sets BEND_GATE_NAMES_ONLY=1 on purpose, which is a different and openly declared choice.

A second limit is that the grep calls only look for names. The check that the proof names a law is a plain substring search, so it confirms the name appears and says nothing about whether the law inside is strong.

Concept B: the same gate inside nix flake check

A flake is a directory with a flake.nix file that declares its inputs (other flakes it depends on) and its outputs (packages, development shells, checks, and so on). A derivation is a description of a build that Nix can run to produce a result in the Nix store, the directory where Nix keeps its build results. The Nix manual says nix flake check "verifies that the flake specified by flake reference flake-url can be evaluated successfully ... and that the derivations specified by the flake's checks output can be built successfully." A check, then, is a derivation listed under checks.<system>.<name>, and it passes when it builds.

The reason to run the gate this way is that a build runs in a controlled environment, so the result does not depend on what happens to be installed or checked out on one person's machine. Otherwise a gate can pass on the author's laptop for reasons that are not true on the CI runner. Here is the checks output from the kit's flake.nix:

checks = forAllSystems (
  system:
  let
    pkgs = pkgsFor system;
  in
  {
    cargo-tops = self.packages.${system}.cargo-tops;
    rust-tops-laws = self.packages.${system}.rust-tops-laws;

    # Names-only: does not require bend in the sandbox.
    # Host `scripts/bend-gate.sh` runs the Bend proof when bend is on PATH.
    law-catalog = pkgs.runCommand "rust-tops-law-catalog" { } ''
      set -eu
      export BEND_GATE_NAMES_ONLY=1
      export RUST_TOPS_LAWS=${./laws}
      bash ${./scripts/bend-gate.sh}
      echo ok >"$out"
    '';
  }
);

The forAllSystems helper produces one set of checks for each of four listed systems (aarch64-darwin, x86_64-darwin, aarch64-linux, x86_64-linux). The first two entries reuse packages as checks, so they pass if the packages build. The interesting entry is law-catalog. The Nixpkgs manual says runCommand "returns a derivation built using the specified command(s), in the stdenvNoCC environment", and its arguments are a name, an attribute set of extra settings (empty here), and the build command. The command sets BEND_GATE_NAMES_ONLY=1 because, as the comment says, the check does not require bend in the sandbox. It points RUST_TOPS_LAWS at ${./laws}, which makes Nix copy the whole laws directory into the store and substitute the store path. The check is therefore hermetic: it reads only the copied files, not whatever is on the machine. Finally it runs the same script, here under bash rather than sh, and writes ok to $out, the path where a derivation must leave its result. If the script exits non-zero, the build fails and so does the check.

The lab built this one check with nix build on the attribute law-catalog, and filtered the output to the interesting lines. For PR A it printed:

-- nix check law-catalog
error: Cannot build '/nix/store/…-rust-tops-law-catalog.drv'.
       > bend-gate: LAWS.bend has 53 law statements, expected 54
exit=1

The failure message from the script appears inside Nix's "Cannot build" error, so a reader of the CI log sees the same sentence they would see running the script by hand. The lab script replaced the store hashes with an ellipsis, and the output above is that real, filtered output.

The pitfall is that a check only sees what the flake hands it. The command above receives ./laws and ./scripts/bend-gate.sh and nothing else. In particular, the generator file's comment says it is "never pulled by the Nix law-catalog check", so this layer cannot tell whether the laws still match the generator's table. A second pitfall concerns systems. The manual describes --all-systems as the option that checks the outputs for all systems. The workflow in this lesson does not pass it, and the lab ran on one system, an aarch64-darwin machine, so the Nix result here was verified for that system only.

Concept C: regenerate and diff, the gate that catches a weakened law

A source of truth is the single place where a fact is written by hand. A generated artifact is a file produced from that source by a program, so nobody should edit it directly. In this kit the source of truth is a table in scripts/gen-laws.rs, and laws/LAWS.bend, laws/PROOF.bend and laws/NAMES are artifacts. The reason this works as a gate is that a generator is deterministic. If you rerun it and the output differs from what is committed, then someone changed an artifact by hand, and a hand edit is exactly how a law gets weakened without anyone touching the table. Otherwise two files that were each edited by hand can agree with each other and still disagree with the intent.

The generator is a std-only Rust program, which means it uses only Rust's standard library. This is the table's row type and the first row, for the law the lab weakens:

struct Row {
    law: &'static str,
    typ: &'static str,
    fun: &'static str,
    bad: &'static str,
    good: &'static str,
    bad_verdict: &'static str,
}
...
const BINARY: &[Row] = &[
    Row { law: "evidence_not_self_served", typ: "Evidence", fun: "evidence_verdict", bad: "FromImpl", good: "FromContract", bad_verdict: "Refuse" },
    ...
    Row { law: "single_deny_site", typ: "DenySite", fun: "deny_verdict", bad: "DenyDouble", good: "DenySingle", bad_verdict: "Refuse" },
];

Each row describes one law: its name (law), the Bend type (typ), the verdict function (fun), the forbidden case (bad), the acceptable case (good), and the verdict the forbidden case must receive (bad_verdict). For evidence_not_self_served, evidence that comes from the implementation itself (FromImpl) must be refused. The table holds 52 of these binary laws. The generator inserts a 53rd, fuzz_untrusted_ingress, from a separate block, and it exits with an error if the total is not exactly 53 (the constant EXPECTED_LAWS). That guard is another fail-closed behavior: a table with a row missing stops the generator instead of producing a smaller catalog.

One function turns a row into Bend code:

fn emit_binary_block(row: &Row) -> String {
    format!(
        "type {typ} is Data:\n  {bad}{{}}\n  {good}{{}}\n\ndef {fun}(x: {typ}) -> Verdict:\n  match x:\n    case {bad}{{}}:\n      {verdict}{{}}\n    case {good}{{}}:\n      Allow{{}}\n\nlaw {law}:\n  {{{fun}({bad}{{}}) == {verdict}{{}} : Verdict}}\n\ndef {law}():\n  {{==}}\n",
        typ = row.typ,
        bad = row.bad,
        good = row.good,
        fun = row.fun,
        verdict = row.bad_verdict,
        law = row.law,
    )
}

The important detail is that {verdict} is filled in twice from the same field, once in the match arm for the bad case and once in the law statement. The generator can only produce the verdict function and its law statement in agreement, which is what a law needs. For the first row, the first lines of the generated LAWS.bend read:

type Evidence is Data:
  FromImpl{}
  FromContract{}

def evidence_verdict(x: Evidence) -> Verdict:
  match x:
    case FromImpl{}:
      Refuse{}
    case FromContract{}:
      Allow{}

law evidence_not_self_served:
  {evidence_verdict(FromImpl{}) == Refuse{} : Verdict}

def evidence_not_self_served():
  {==}

A hand edit has to change both the match arm and the law line to keep the file self-consistent, and that is what PR C did. The generator then writes all three files from the same table:

write_or_exit(&laws_dir.join("LAWS.bend"), &laws_body);
...
write_or_exit(&laws_dir.join("PROOF.bend"), &proof);
...
let names = format!("{}\n", law_names.join("\n"));
write_or_exit(&laws_dir.join("NAMES"), &names);

The directory comes from laws_dir(), which takes the parent of the directory holding the script and appends laws. The generator therefore always overwrites the repository's own laws/ directory, which is where the next command looks.

The script runs as a Cargo script. The Cargo unstable book describes single-file packages, run with cargo +nightly -Zscript file.rs, where the .rs file carries its package settings in a frontmatter block, here ---cargo followed by a [package] table. Its default build directory is $CARGO_HOME/target/<hash>, so running it does not litter the repository. The diff step is then git diff --exit-code -- laws/. Git documents --exit-code as making the command exit with 1 if there were differences and 0 if there were none, and the path after -- limits the comparison to that directory. The lab used --stat as well, which adds a diffstat summary.

PR C is the pull request that matters. It changed FromImpl{} from Refuse{} to Allow{} in the match arm, and changed the law statement from Refuse{} to Allow{} to match. The pull request's own diffstat was laws/LAWS.bend | 4 ++--, four lines in one file. Here is what each layer reported:

-- names-only gate
bend-gate: 53 laws named
exit=0
-- nix check law-catalog
exit=0
-- regenerate and diff
...
 laws/LAWS.bend | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)
exit=1

The first two layers passed. The count is still 53, every name is still stated, and PROOF.bend still names every law, so name parity has nothing to object to. The generator's wrote 53 laws line, which prints a temporary path, is shown as .... The real diff shows exactly what the weakening was:

diff --git a/laws/LAWS.bend b/laws/LAWS.bend
index db47c2a..cc9ed7e 100644
--- a/laws/LAWS.bend
+++ b/laws/LAWS.bend
@@ -12,12 +12,12 @@ type Evidence is Data:
 def evidence_verdict(x: Evidence) -> Verdict:
   match x:
     case FromImpl{}:
-      Allow{}
+      Refuse{}
     case FromContract{}:
       Allow{}
 
 law evidence_not_self_served:
-  {evidence_verdict(FromImpl{}) == Allow{} : Verdict}
+  {evidence_verdict(FromImpl{}) == Refuse{} : Verdict}
 
 def evidence_not_self_served():
   {==}

The minus lines are the pull request's content and the plus lines are what the generator wrote, so the diff restores Refuse. A reviewer reading this output sees the weakened law spelled out, instead of having to spot it inside a larger change.

The pitfall is that this gate trusts the generator. If a pull request edits the table in gen-laws.rs and also commits the regenerated outputs, the generated files match the new table, and regenerate-and-diff passes. The gate has only moved the question from the three law files to the generator file, so the generator file itself needs careful review. A change to scripts/gen-laws.rs should be treated as a change to the policy.

Putting it together: a required check on GitHub

The workflow below runs all three layers on GitHub Actions. It was written for this lesson. It parses as YAML but has not been run on GitHub, so treat it as a starting point and not as tested configuration.

# Pull request gate for the law catalog. Lesson file: not run on GitHub.
name: laws-gate

on:
  pull_request:
  merge_group:

permissions:
  contents: read

jobs:
  law-gate:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: cachix/install-nix-action@v25
      # Layer 1 and 2: name parity inside the Nix sandbox, plus every other check.
      - run: nix flake check -L
      # Layer 3: the generator is the source of truth; a hand edit is drift.
      - run: rustup toolchain install nightly --profile minimal
      - run: cargo +nightly -Zscript scripts/gen-laws.rs
      - run: git diff --exit-code -- laws/

The on: block lists two triggers. GitHub documents that by default a workflow on pull_request runs only for the activity types opened, synchronize and reopened, which covers a new pull request and every push to it. For open, mergeable pull requests the workflow gets the merge branch, and because actions/checkout checks out that branch by default, the tests run against the merged result and not the head branch alone. The same page warns that workflows will not run on pull request activity if the pull request has a merge conflict, so a conflicted pull request needs its conflict resolved before the gate will run at all. The second trigger, merge_group, is for merge queues. A merge queue is GitHub's mechanism for merging approved pull requests in order, and the documentation says that if your repository uses Actions for required checks you must add the merge_group event, "Otherwise, status checks will not be triggered when you add a pull request to a merge queue."

The permissions key limits the workflow's token to reading repository contents. The job is named law-gate and runs on ubuntu-latest. The two uses steps check out the code and install Nix, following the sample on nix.dev, which uses actions/checkout@v4 and then cachix/install-nix-action@v25 before running Nix commands. The version tags come from that sample, and newer releases may exist, so check them before use. The first run step is nix flake check -L, which builds every check, including law-catalog. The -L flag is the short form of --print-build-logs, which prints full build logs to standard error. That is how the "Cannot build" message from the lab would reach the CI log. According to the Nix manual, without the keep-going option set to true Nix stops at the first error.

The last three steps are layer three. The workflow assumes rustup is already on the runner. The step rustup toolchain install nightly --profile minimal installs the nightly toolchain with the minimal profile, which the rustup book describes as including "as few components as possible to get a working compiler (rustc, rust-std, and cargo)" and recommends for CI. The cargo +nightly -Zscript step regenerates the three files in place, and git diff --exit-code -- laws/ fails the job if anything changed. That is the PR C failure from the lab, now at the last step of the job.

A workflow only blocks a merge if the repository requires it. A required status check is a check that a branch protection rule demands before changes can merge into the protected branch. GitHub's documentation says that "all required status checks must pass before collaborators can merge changes into the protected branch", and that a required check must have a "successful, skipped, or neutral status". A skipped job therefore counts as passing, which is why this job has no condition that could skip it. The same page advises that job names be unique across all workflows, since the same name in several workflows "can cause ambiguous status check results and block pull requests from being merged", so law-gate should not be reused elsewhere. It also notes that by default the restrictions "don't apply to people with admin permissions", unless you optionally apply them to administrators. A gate that an administrator can bypass without noticing is open for that person.

Here is the complete lab picture, with "not run" for layers the lab did not execute on that pull request:

ChangeName-parity scriptNix checkRegenerate and diff
main (baseline)exit 0exit 0exit 0
PR A: name added, no lawexit 1exit 1not run
PR B: proof stops naming a lawexit 1not runnot run
PR C: law weakened, verdict and law flipped togetherexit 0exit 0exit 1

Three limits apply to these results. The lab ran on an aarch64-darwin machine with Determinate Nix 3.22.3 (nix 2.35.2) and cargo 1.101.0-nightly, so the Nix result covers one of the four systems the flake lists. The lab built the law-catalog derivation directly with nix build, while the workflow runs nix flake check, which the manual says builds the derivations in the checks output. No bend binary existed on that machine, so no Bend proof was run and nothing here says how Bend evaluates a proof. Finally, the workflow was not run on GitHub.

Check yourself

**1. A pull request adds a line to laws/NAMES but writes no matching law. Which script message fails it, and with what exit code?**

The count check fails it with bend-gate: LAWS.bend has 53 law statements, expected 54 and exit code 1. The Nix check fails with the same line inside "Cannot build".

**2. A developer runs scripts/bend-gate.sh on a machine without bend and sees exit 0. What did the gate actually verify?**

Only name parity. The last line of the log says bend not on PATH (names-only), which means no Bend proof was run.

3. Why did PR C pass both the name-parity script and the Nix check?

PR C flipped the verdict and the law statement from Refuse to Allow together. The count stayed at 53, every name was still stated, and PROOF.bend still named every law, and both checks only look at names and counts.

**4. What does git diff --exit-code -- laws/ return after the generator runs on PR C, and why?**

It returns 1, because the regenerated LAWS.bend differs from the committed one. The generator writes Refuse from its table, and the diff shows that change.

**5. A pull request edits the bad_verdict field in gen-laws.rs and commits the regenerated files. Does regenerate-and-diff catch it?**

No. The regenerated files match the edited table, so the diff is empty. The generator file needs its own review.

Sources