Skip to content

Manuscript guard for the journal version, and the ten pre-registered studies behind it - #55

Open
MohammadThabetHassan wants to merge 74 commits into
mainfrom
paper/stvr-pins
Open

MohammadThabetHassan wants to merge 74 commits into
mainfrom
paper/stvr-pins

Conversation

@MohammadThabetHassan

@MohammadThabetHassan MohammadThabetHassan commented Oct 3, 2026 •

Copy link
Copy Markdown
Owner

The manuscript guard (scripts/check_manuscript.py) follows the paper's journal rewrite. Ten
pre-registered studies are added:

  • the Gatekeeper suites' surviving mutants decided exactly;
  • the paper's suite-strategy result replicated on the same real Rego policy;
  • the strategies scored against faults two Rego libraries' maintainers fixed;
  • the Cedar study's equivalence verdicts checked by Cedar's own symbolic analyser;
  • Xu et al.'s XACML coverage criteria against the quotient, on Xu et al.'s own benchmark;
  • established combination and structural criteria against the quotient, at matched size;
  • a census that certifies the inside verdicts call by call;
  • the Rego equivalences decided again under every Constraint the library ships;
  • the payoff studies' suites rescored over subsumption-minimal mutants;
  • the Kyverno library's suites decided exactly, as the Gatekeeper suites were.

Questions raised in a pre-submission review are answered from artifacts already written,
post hoc and labelled as such: the exclusions crossed with every reason they carry, line coverage
against adequacy, clustered intervals, and the guard families behind the inside verdicts.

A reproduction image runs the fast checks in CI.

The guard

  • Reads supplement.tex beside the manuscript, and the pins are re-anchored to the rewritten
    abstract and sections.

  • Accepts a decomposition stated in both files: every statement must carry the same counts and
    one copy must sum to the artifact's figure.

  • Checks every copy of each data figure by the pgfplots axis it draws (taxonomy, payoff),
    and the graphical abstract's bars (axis abstract); a renamed axis is reported, not skipped.
    The payoff figure plots three populations (generated, real Cedar, real Rego); the graphical
    abstract keeps two.

  • Pins every study as the paper states it: 477 pinned claims in all. Two kinds of statement
    are asserted against the artifacts:

    • fractions the prose rounds ("two thirds", "three quarters");
    • sentences with no number ("the ordering is the same", "on every policy", "none refuted").

    The 10-page article restates the results in the full version's own phrases, so each pin
    reaches both texts.

  • Holds the paper to the strength of its evidence.

    • The Rego equivalences are stated as relative to the parameter settings each suite tests.
    • The guard pins the worst cases: 76.7%, giving the range [76.7, 89.5]. For the schemas it pins
      63.3%, asserted equal to the raw rate over compiling mutants.
    • It pins the exclusions crossed with every reason they carry, not counted schema-first,
      and checks the taxonomy figure against the cross-tabulation's bands.
  • Scopes each table's rows to that table. The XACML criteria rows had matched their labels
    anywhere in the text; the minimal-mutant table has a row of the same name.

  • Rounds tables once. Per-module rows are checked against their counts, rounded half up: a
    stored score is already rounded, and rounding it again printed 15/19 as 79.0.

The exact Rego study (scripts/rego_exact_study.py, scripts/rego_witness_space.py)

Inside the fragment equivalence is decidable, so the kill rates of the Gatekeeper library's
author-written suites are decided exactly, under protocols committed and hashed before each run:

  • docs/EXACT_ADEQUACY_PROTOCOL_REGO.md covers the 18 suite-study modules inside the
    fragment. Result (docs/rego-exact-adequacy-v1.json): 13 modules pass the completeness
    check.
    • 54 of their 81 surviving mutants are equivalent.
    • The exact score is 89.5% pooled, against a raw 75.3%.
    • Each of the 27 real gaps comes with an input that kills it.
    • Four modules are excluded by name.
  • docs/EXACT_ADEQUACY_PROTOCOL_REGO_SCHEMAS.md covers the 26 policy schemas, each
    instantiated by its suite's parameters, as a secondary population. Result
    (docs/rego-exact-adequacy-schemas-v1.json):
    ten are measured.
    • 62 of their 103 surviving mutants are equivalent.
    • The exact score is 81.3% pooled, against a raw 65.9%.
  • stillborn (docs/rego-suite-stillborn-v1.json): 154 of 2,984 mutants do not compile,
    yet were counted as kills.
  • gaps (docs/rego-exact-gaps-v1.json, post hoc): every gap is also killed by a review
    shaped like the authors' own.

The suite-strategy study on real Rego (scripts/rego_payoff_study.py)

docs/EXACT_EVALUATION_PROTOCOL_REGO.md replicates the payoff study. The population is the 13
measured modules, each under every parameter setting its suite tests: 34 policies. Every decision
is OPA's.

Result (docs/rego-suite-strategy-study-v1.json), as expected detection:

Strategy Detection
Quotient 99.9%
Random suite of the quotient's size 97.6%
Decision proxy 42.5%
Random suite of the proxy's size 19.7%
  • The quotient beats the proxy on all 34 policies: 0.573 [0.528, 0.614].
  • It beats random testing by a small 0.022 [0.011, 0.036].

Real faults (scripts/rego_real_faults_study.py)

docs/REAL_FAULTS_PROTOCOL_REGO.md fixes 72 candidate fixes from the histories of the Gatekeeper
and Config Validator libraries and classifies them before analysis: 34 behaviour fixes form the
population. P is the policy at the fix's parent, and the fix is the single "mutant". The study
measures whether a suite built from P would have exposed the change.

Result (docs/rego-real-faults-v1.json): 20 faults are scored.

  • 14 of them are unions of P's quotient classes.
  • Mean exposure: quotient 95.9%, random suite of the same size 85.7%, decision proxy 35.8%.
  • H1: 0.102 [0.037, 0.182], p = .0009. H2: 0.601 [0.433, 0.759], p = .0001.
  • Every fix that reads only paths P already read is a union of classes. Five of the six fixes
    that read a new field are exposed only by chance.

SymCC's check of the Cedar verdicts (scripts/cedar_symcc_crosscheck.py)

The Cedar study calls a mutant equivalent when no cell of its witness space separates it, and it
checks completeness by sampling.

How it was checked.

  • docs/CEDAR_SYMCC_CROSSCHECK_PROTOCOL.md puts the same question to SymCC, through
    cedar symcc equivalent (cedar-policy-cli 4.12.0, with cvc5 1.3.1).
  • It uses the schemas the files' own authors wrote. Those schemas were found by
    scripts/cedar_schema_candidates.py and frozen in docs/cedar-schema-candidates-v1.json
    before the run.
  • Every counterexample is decided again by cedarpy, through the study's own evaluation
    function.

Result (docs/cedar-symcc-crosscheck-v1.json) — 71 files with a schema (the development
file is reported apart):

  • Equivalent verdicts, 173.
    • None is refuted.
    • 161 are verified in every request environment.
    • 12 are ill typed under the schema in some environment.
  • Live verdicts, 830.
    • 743 are confirmed live.
    • 72 (8.7%) are equivalent under the authors' schema, mostly scope widenings.
  • Engine agreement: all 743 counterexamples are confirmed by cedarpy.

A first run's parser could not read datetime counterexamples. That deviation is recorded and the
population was run again.

Xu et al.'s criteria on their own benchmark (scripts/xacml_criteria_study.py)

The paper said Xu, Shrestha and Shen's criteria were not compared. docs/XACML_CRITERIA_PROTOCOL.md
compares them on their own terms:

  • Policies: XPA's benchmark policies (11 of 20 eligible).
  • Mutants: XPA's own operators.
  • Suites: what XPA's seven generators produce, built from XPA's source and run with the Z3
    release nearest the one it pins.
  • Decisions: every one Balana's. The harness agrees with all 372 conformance cases Balana's
    own suite runs.

Result (docs/xacml-criteria-study-v1.json), stated with both halves:

  • Over the ten policies where XPA built an MC/DC suite, the quotient detects every live mutant.
    On this equality-heavy benchmark almost every cell is its own class, so it needs 584 requests
    on average (681 over all eleven).
  • XPA's MC/DC detects 94.6% with 37 requests over those same ten.
  • The quotient still beats every criterion: MC/DC by 5.4 points [1.6, 9.7], Holm p = 0.031.
  • Only MC/DC and its variant beat random suites of their own size after Holm. The rule-pair
    criteria do no better than random.

Deviation. A first run stopped on XPA's PTT mutants, which lack the Target XACML 3.0
requires. They now get the empty Target XPA describes, and the artifact records the deviation.

Post hoc re-analyses

These read only committed artifacts and are post hoc, not pre-registered.

  • exclusion_taxonomy.py --crosstab-json writes docs/exclusion-crosstab-v1.json: every
    exclusion against every reason it carries. 1,621 of the 1,790 have a guard the request does
    not determine; 169 are schemas and nothing else. The schema-first count (exclusion-taxonomy-v1)
    is unchanged and still reproduces byte for byte.
  • scripts/review_round_analyses.py writes docs/review-round-analyses-v1.json:
    • Kendall's tau-b of line coverage against the kill rate (0.51, permutation p 0.0001, 48
      modules) and against the exact score (0.31, p 0.18, 13 modules);
    • cluster bootstrap and exact cluster sign-flip, the Rego payoff by module and the real faults
      by commit and by module (every interval stays above zero);
    • the two faults the protocol reports rather than scores, counted as unexposed;
    • each scored population's equivalent share;
    • the inside verdicts of Azure, XACML and IAM sorted by whether their guard families are
      decidable whatever fills the operands (4,615 with Cedar) or only with a literal operand (148).
  • Tests (tests/test_review_round_analyses.py) recompute both artifacts and compare them with
    the committed files.

Established criteria at matched size (scripts/combination_criteria_study.py)

The quotient is all-combinations coverage over a policy's guard atoms. This study scores the
cheaper strategies under docs/COMBINATION_CRITERIA_PROTOCOL.md, fixed before the run.

  • Strategies and populations:
    • each choice, base choice, pairwise and three-wise coverage, as greedy covers over the
      classes, 100 seeded constructions per policy;
    • rule coverage, decision coverage and MC/DC over each rule's atoms, on the generated policies.
  • How scores are computed: every suite's detection is computed exactly, and each strategy is
    set beside a random suite of its own size. The quotient's own figures reproduce the payoff
    studies' exactly.

Result (docs/combination-criteria-study-v1.json):

  • Generated policies: MC/DC detects 73.4% with a median of 8 tests and three-wise coverage 69.6%
    with 14, against the quotient's 91.0% with 48.
  • Cedar: three-wise coverage detects 83.5% with 21, against 99.3% with 36.
  • The quotient beats every criterion (Holm-adjusted p at most 0.0014 and 0.0008).
  • Per test, MC/DC and rule and decision coverage gain far more over random suites of their size
    than the quotient does. Base choice does worse than random.
  • Certain detection, the share every choice of witnesses detects, is 74.2% and 98.4%.

The inside verdicts, certified call by call (scripts/guard_certification.py)

The membership adapters accept a guard family by name. For patterns, products and some string
operations, finite refinement needs a literal operand, which no adapter checks.

  • What the census does (under docs/GUARD_CERTIFICATION_PROTOCOL.md, fixed before it read
    any corpus):
    • reads every guard call of every artifact judged inside, except Cedar's 22, which rest on its
      designers' encoding;
    • records each operand as a literal (a parameter read counts as one), a read of the request,
      or computed;
    • certifies a verdict only when every call has the operand its family needs.
  • Reproduction first: before reading a corpus, the census re-measures it from the pinned
    clone and checks every subject's verdict, not only the counts.

Result (docs/guard-certification-v1.json): 5,030 of the 5,175 inside verdicts (97.2%) are
certified.

Corpus Certified
IAM 1,635 of 1,651
Azure Policy 2,119 of 2,137
XACML 952 of 953
Cedar 22, by design
Kyverno 209 of 243
Rego 93 of 169

A post hoc reading, not fixed before the run, follows a helper function's arguments to their
calls. It certifies 146 of the 169 Rego modules, and is reported beside the protocol's count.

Corrections after the first run (4,984 certified). The artifact keeps the first run's counts
and names each correction:

  • the Google library's subjects are named from the directory above its checkout, so its 54
    modules had not been read;
  • two third-party files are hashed with line endings normalised, as the measurement hashed them;
  • parameter reads written through object.get or some … in are recognised;
  • calls in else branches, comprehensions and function heads are read;
  • a function's arguments are no longer taken for output;
  • get_default counts as a parameter read only when it reads the parameters.

Only the Google library and those two files rose. The four Rego corpora lost one module.

Under every Constraint the library ships (scripts/rego_shipped_constraints_study.py)

The exact study's 54 equivalents hold under the settings each suite tests. 43 of them are in
modules that read parameters, so the paper gave the Rego score as a range, [76.7, 89.5].

  • What the study does (under docs/SHIPPED_CONSTRAINTS_PROTOCOL_REGO.md, which froze every
    sample Constraint before any module was decided under one): it decides the same mutants
    again under every Constraint the Gatekeeper library ships for each template.
  • Reproduction first: on the tested settings, every one of the 14 modules reproduces its
    exact-study record: mutants, kills, equivalents, survivors and cells per setting.

Result (docs/rego-shipped-constraints-v1.json):

  • Five of the 13 modules gain a setting no test uses (wildcard image exemptions, the full
    wildcard "*"). They hold 26 of the 43 parameter-relative equivalents.
  • Every new setting is decided without a missing cell. None separates an equivalent; each
    separates only distinguishable mutants.
  • The score under every shipped Constraint is therefore 89.5%. 76.7% stays the bound for
    settings the library does not ship.

Portability (3793243): running the Rego instruments on Windows needed two fixes, neither of
which changes a result on Linux.

  • opa parse now reads a temporary file instead of /dev/stdin.
  • The mutation operator writes that file with LF line endings. With CRLF, every multi-line
    mutant had been silently dropped.

First run. It compared the tested settings with the record as an ordered list. OPA's test
runner prints a suite's inputs in an order that varies from run to run, so four modules failed
on order alone. The gate now compares each setting's cells, and the artifact's notes keep that
run's account.

Over subsumption-minimal mutants (scripts/minimal_mutant_study.py)

Redundant mutants can inflate scores and the gaps between strategies. Inside the fragment every
mutant is constant on each witness cell, so its difference set is exact and subsumption is
inclusion between difference sets: the minimal set is computed, not estimated over a pool of
tests.

  • What the study does (under docs/MINIMAL_MUTANTS_PROTOCOL.md, fixed before it ran): it
    scores the payoff studies' and the criteria study's suites, unchanged and with the same seeds,
    over each policy's minimal mutants, on the 300 generated policies and the 96 Cedar files.
  • Reproduction first: over every live mutant, it reproduces all three earlier studies at
    their stored precision.

Result (docs/minimal-mutant-study-v1.json): 5,516 live mutants are 3,018 minimal ones on
the generated policies, and 1,935 are 812 on Cedar.

Strategy Generated, all Generated, minimal Cedar, all Cedar, minimal
Quotient 91.0% 83.7% 99.3% 98.6%
Random suite of the quotient's size 78.9% 72.2% 90.5% 88.3%
Decision proxy 44.4% 24.5% 28.5% 17.3%
MC/DC 73.4% 57.5% — —
  • Every score falls, and the quotient's advantage survives. It beats a random suite of its size,
    the proxy and every established criterion on both populations (Holm-adjusted p at most 0.0009).
  • Its lead over the proxy and the criteria widens. Over random suites of its size it is 11.6
    points on the generated policies (12.1 over all mutants) and 10.3 on Cedar (8.9).
  • Per policy, it falls below a random suite of its size on 25 of 300 and 4 of 96, against 15 and
    2 over all mutants.
  • Rego is not rescored: its payoff study kept no difference set per mutant.

First run. It looked decision coverage up among the payoff strategies, where "decision" names
the proxy, and compared criteria with the quotient's exact score rather than its six-decimal one.
Both are fixed in 7e4d828, and the artifact's notes (aee8cc5) record that no other mean, interval
or p value changed.

The Kyverno suites, decided exactly (scripts/kyverno_exact_study.py)

The Gatekeeper study's question, asked of a second admission library under
docs/EXACT_ADEQUACY_PROTOCOL_KYVERNO.md, which was committed before the instrument existed:
which survivors of the Kyverno library's own suites are equivalent to their policies.

  • Population: of the 206 inside policies, 86 have rules the witness construction
    (scripts/kyverno_witness_space.py) models: pattern, anyPattern and deny-condition rules over
    request fields and the operation. 28 have no mutant, 10 exceed the 20,000-cell cap and one names a
    kind with no known API version, leaving 44 scored beside three development policies.
  • Engine: every decision is Kyverno 1.19.1's, on 13,685 cells and 29,267 completeness inputs.
    No policy fails the completeness check.

Result (docs/kyverno-exact-adequacy-v1.json):

  • The suites kill 95 of 129 mutants. Only 2 of the 34 survivors are equivalent, so the exact score
    is 74.8% against a raw 73.6%: unlike Gatekeeper's, these suites' misses are almost all real.
  • The 32 real gaps fall in 11 policies: 16 non-empty patterns weakened to accept the empty string,
    and 16 equality anchors made conditional. Each comes with a resource that kills it, and adding
    those resources to the suites kills all 32 and no equivalent mutant.

Reproduction (reproduce/)

  • The image. reproduce/Dockerfile pins OPA 1.20.2, Kyverno CLI 1.19.1, the Cedar CLI's
    experimental build 4.12.0, cvc5 1.3.1 and cedarpy 4.12.1. Each binary is checked against its
    release's SHA-256.
  • The modes. reproduce/run.sh has five: verify, corpora, membership, symcc and
    xacml.
  • The README. reproduce/README.md maps every artifact to the command that writes it, and
    names what does not reproduce exactly.
  • CI. .github/workflows/reproduce.yml builds the image and runs verify.
  • The pre-registration check. scripts/check_protocols.py checks that all 17 pre-registered
    artifacts name a protocol the repository holds.

Checks

  • With TRUSTWEAVE_PAPER set, these tests pass: the guard's, the witness space's, the payoff
    study's, the real-faults study's, the SymCC check's, the schema list's, the post hoc
    re-analyses', the criteria study's, the census's, the shipped-Constraints study's, the minimal-mutant study's, the Kyverno study's and the protocol check's. Without the paper, as in CI, the guard tests skip and the others still run.
  • The guard reports 477 pinned claims agreeing for the full-length paper, the 10-page article
    and its Springer Nature build.
  • Lint: ruff check . and ruff format --check . are clean.
  • What changed: README.md, CHANGELOG.md, scripts/, tests/, docs/, reproduce/,
    the reproduction workflow and .zenodo.json.

…r the pins to the STVR rewrite

The manuscript is now a main file and a supporting-information file. The guard reads the
supplement's body after the main text (dropping the cross-file S-/M- label prefixes), so the
documented command is unchanged and a figure moved to the supplement is still checked. Pins
that restated the old abstract and introduction are re-anchored or removed with no number
changed; restatements in the new wording of the abstract, introduction, membership and threats
sections are pinned. New test: a figure changed only in the supplement is caught.
… its supplement

A paper that has a short version and an extended version states the worked example's mechanism
counts twice. Every statement must carry the same counts and one copy must sum to the artifact's
figure; a changed count in either still fails.
…ical abstract

Find a data figure by the pgfplots axis it draws (name=taxonomy, name=payoff) rather than by
its label, and compare every copy with its artifact: the 10-page article draws both as panels
of one figure and the full-length version as two figures, and each copy has to agree. The
payoff figure, which restates the two suite-strategy tables on one scale, is now pinned too,
and an axis that is renamed is reported rather than silently skipped.

When a graphical-abstract.tex sits beside the manuscript, compare its bars (the axis named
abstract) with the same artifacts: a table-of-contents figure is read away from the paper,
where no table can contradict it.

Drop the third-party schema count, which the rewritten paper no longer states.
The suite study scored the Gatekeeper library suites by the share of mutants they kill, which
counts mutants no test could kill. Inside the fragment equivalence is decidable, so this adds
the study that decides it: a witness space per module and instantiation, built from the guards
of the module and of every mutant, every decision taken by OPA, completeness checked against
drawn reviews and against the authors own test inputs, and an input that kills every
surviving mutant that is not equivalent.

The protocol, docs/EXACT_ADEQUACY_PROTOCOL_REGO.md, is committed and hashed into the script
before the study runs on its population; only the development module, src/general/httpsonly,
was run while the harness was written.
Comment thread tests/test_rego_witness_space.py Fixed
…y schemas

Twenty-six of the suite study's modules are policy schemas, outside the fragment until a
Constraint supplies their parameters; their suites always supply them, so each test runs an
instantiated policy. The primary protocol already decides equivalence per instantiation of a
module's own suite, so the same procedure scores these suites exactly. This adds that second
population under its own protocol, written while the primary study runs and before any of its
results were read, reported beside the primary population and never pooled into its headline.

The new protocol also records an erratum to the primary one: it counts the excluded modules as
25 schemas and 6 that read data.inventory, where the membership artifact says 26 and 5.
Forking while the executor's own threads held a lock left all six workers waiting on it, so the first population run stopped before it decided anything; spawned workers start clean. Each finished module is now logged as it completes.
…rn kills counted

The pre-registered study (docs/EXACT_ADEQUACY_PROTOCOL_REGO.md) ran on the 18 suite-study modules
judged inside the fragment. Thirteen pass, besides the development module: three exceed the cell
cap and one fails completeness, the drawn reviews finding a rule combination no cell held. On the
thirteen, 54 of the 81 mutants the suites leave alive are equivalent under every instantiation the
suites test, the exact score is 89.5% pooled against a raw 75.3%, and each of the other 27
survivors comes with an input that kills it; adding those inputs as tests kills every
distinguishable mutant. docs/rego-exact-adequacy-v1.json records it.

A stillborn census of the suite study's 2,984 mutants (docs/rego-suite-stillborn-v1.json) finds
154 that do not compile, all counted as kills; over the mutants that load the suites kill 69.0%,
not 70.6%. The test's sample pattern now escapes its dots, which CodeQL read as a hostname.
The paper now reports the Gatekeeper suites decided exactly: the stillborn kills of the suite
study, the 18 modules inside the fragment and the 13 that pass, the equivalent survivors, the
exact score against the raw one, line coverage against exact adequacy, the gaps and the table
of modules. Each figure is recomputed from rego-exact-adequacy-v1, rego-suite-stillborn-v1 and
rego-exact-gaps-v1; the fractions the prose rounds (two thirds, three quarters) are asserted
against the artifacts, so a re-run that moves them fails here first. 224 pins in all.

rego_exact_study.py gaps is a post-hoc reading of the finished study, outside its protocol: it
finds every one of the 27 real gaps killed by a review whose fields and types all occur in the
authors' own inputs, so none depends on an object an API server would reject.
@MohammadThabetHassan MohammadThabetHassan changed the title check_manuscript: read the supplement, check every figure copy and the graphical abstract Manuscript guard for the journal version, and the Gatekeeper suites decided exactly Oct 4, 2026
The second suite-strategy study replicated the first on Cedar only, because a replication on
Rego needed a cell enumerator. The exact-adequacy study built and checked one, so this adds the
replication: the measured Gatekeeper modules under every instantiation their suites test, the
five strategies of the first protocol scored in closed form, every decision OPA's.

The quotient classes are the cells grouped by what OPA says each of the module's atoms is at the
cell's values. rego_witness_space now records those atoms -- operator, operand order, constant --
beside the hints it already kept, without changing the hints, so the witness spaces are those the
exact-adequacy study built. A policy whose decision varies inside a class is excluded. The
protocol, docs/EXACT_EVALUATION_PROTOCOL_REGO.md, is hashed into the script before the study runs
on any module but the development one.
Run under docs/EXACT_EVALUATION_PROTOCOL_REGO.md (the artifact records its hash) on the 13
Gatekeeper modules the exact study measured, each under every parameter setting its suite tests:
34 policies, every decision OPA's. All 34 pass the constancy check with no unmerged path, and
all are scored.

Expected score: quotient 99.9%, random at the quotient's size 97.6%, decision proxy 42.5%,
random at the proxy's size 19.7%, refinement 100.0%. H1 0.022 [0.011, 0.036], 29 wins, 3 ties,
2 losses (both disallowinteractive); H2 0.573 [0.528, 0.614], 34/0/0; H3 0.228 [0.196, 0.262];
each p = 0.0001, Holm 0.0003. By module: 99.9 / 96.3 / 47.5 / 22.7, Holm p = 0.0006 for each.
…abstract's new wording

The payoff figure now plots three populations; the graphical abstract keeps its two. A new
claim set pins the Rego replication wherever the paper states it: the abstract, the
contribution, the population and the engine, the read-across table (its rows are anchored by
their own shape, so they cannot collide with the two tables before it), the three comparisons,
the two losses, the module reading, the development module, the threats and the conclusion.
The 10-page article restates the result in the full version's own phrases, so each pin reaches
both texts.

The abstract's sample, Cedar and Rego sentences were reworded to make room for the replication,
and their pins follow. The tests cover a drifted Rego bar and a drifted Rego table entry.
…uotient

The study scores with two closed forms and groups reviews by the truth values of the module's
atoms; neither had a test. The closed forms are now checked against enumerating what they
summarise, Holm's correction and the permutation floor against known values, and the
signature on reviews that agree or differ in one respect at a time: one class for reviews that
agree on every atom, a collection read as the set of its elements' classes, an unmerged path
making every value its own class.

One fix, found by the last test: values_to_decide iterated the elements of a scalar met where a
collection was expected, which raises; signature already treats such a value as having none,
and now both do. The study's results cannot have depended on it: the error is not caught, and
the run finished with every policy scored.
@MohammadThabetHassan MohammadThabetHassan changed the title Manuscript guard for the journal version, and the Gatekeeper suites decided exactly Manuscript guard for the journal version, the Gatekeeper suites decided exactly, and the payoff study on real Rego Oct 4, 2026
…inal

The paper now names five protocols, and the exact-adequacy one is no longer the third of them;
the contribution calls it a further protocol, and the pin follows.
… results

Run under docs/EXACT_ADEQUACY_PROTOCOL_REGO_SCHEMAS.md (the artifact records its hash): the 26
Gatekeeper policy schemas, each instantiated by the parameters its own suite supplies. This is the
second run; the first was lost to a subprocess timeout that fired while the process group was
paused for memory on the shared server, and it wrote no artifact.

Seven schemas exceed the 250,000-cell cap and nine fail the completeness check, so ten are
measured. On them 62 of the 103 surviving mutants are equivalent (60%); the suites kill 178 of
219 distinguishable mutants, 81.3% exactly against a raw 65.9% (mean 75.0 vs 61.2, a difference
of 13.8 [9.1, 18.7]); each of the 41 real gaps comes with a killing input, and the inputs, added
as tests, kill every distinguishable mutant and no equivalent one. Reported beside the primary
population, never pooled with it, as the protocol requires.
The shared sentence of both versions, the supplement's paragraph and its table row by row. The
result is worded in a template of its own: the primary study's pins would otherwise reach it,
which is how this was caught. 272 pinned claims agree on all three builds.
…round tables once

A referee-style review of the paper found statements that outran the evidence; the paper now
says what was shown, and the guard pins the new statements:

- the Rego equivalences hold under the parameter settings each suite tests: the worst case if
  every equivalent in a module that reads parameters were separable by an untested setting
  (76.7%, the range [76.7, 89.5]), the 43 such equivalents, and for the schemas, where none is
  outright, the worst case 63.3% asserted equal to the raw rate over the mutants that compile;
- the abstract's reworded sentences (the samples sit at or below their vendors' shares, which
  the guard already asserted; "two thirds of what the suites miss");
- the taxonomy: the 1,790 exclusions a careless reading would call expressiveness, with the
  expressive share asserted to be about half, and the expressiveness band asserted under a
  quarter of every corpus.

The per-module table pins now divide the counts and round once, half up: an artifact's stored
score is already rounded, and rounding it again printed 15/19 as 79.0 rather than 78.9.
278 pinned claims agree on all three builds.
…histories

Every payoff result so far scores suites against the authors' own mutation operators. This
protocol scores the same strategies against faults nobody seeded: the behaviour fixes the
maintainers of the Gatekeeper library and Google's Config Validator library made to their own
policies. The policy in use before a fix is the policy, the fix is the single "mutant", and the
question is whether a suite built from the policy in use would have exposed the change.

The 72 candidate module changes (fix-labelled commits touching one to three modules) were
listed and classified from their messages and diffs before any was analysed; the
classification is part of the protocol, so its hash fixes it: 34 behaviour fixes in the two
corpora studied, 5 more in Red Hat's library excluded by name (its suites run under conftest).
Primary outcomes: the share of fixes whose difference set is a union of the old policy's
quotient classes, and the strategies' exposure probabilities with two pre-registered
comparisons.
…velopment faults

scripts/rego_real_faults_study.py runs the protocol fixed in docs/REAL_FAULTS_PROTOCOL_REGO.md:
for each behaviour fix in the Gatekeeper and Config Validator histories, the module at the fix's
parent (the policy in use) and at the fix, each with its own commit's libraries; both suites'
inputs and settings; the exact study's witness space from the two versions together, its
completeness check, and OPA's decisions; the policy's own quotient as the Rego payoff study
builds it; and each strategy's exposure probability in closed form, the settings' misses
multiplied. Membership is the paper's procedure, run on the corpus as it stood at each commit.

Config Validator passes the asset at input.asset and the Constraint at input.constraint, and
decides with deny; the analysis reads a renamed copy of the syntax tree, while OPA decides on
the module as written. Only the fixtures a test reads are loaded: one malformed fixture
elsewhere in a 2019 tree stopped the whole suite, which is how the Config Validator
development fault first came back with no inputs.

The two development faults the protocol names (Gatekeeper #2, Config Validator #34) are the
only ones run so far.
Run under docs/REAL_FAULTS_PROTOCOL_REGO.md (the artifact records its hash) on the 34 behaviour
fixes the protocol froze, two of them its development faults. Twenty are scored; ten are
excluded by name (three read data.inventory and one reads the clock, so the policy in use is
outside the fragment; four fail the completeness check; one exceeds the cell cap; one fix does
not compile under OPA 1.20.2), and in two the versions agree on every cell under the settings
the suites test.

Of the 20, the difference set is a union of the policy's own quotient classes in 14, so one
witness per class exposes them with certainty, and 15 are exposed with certainty; 6 fixes read
a path the policy in use never read. Mean exposure: refinement 100%, quotient 95.9%, random at
the quotient's size 85.7%, the decision proxy 35.8%, random at its size 11.7%. H1 (quotient >
random, same size) 0.102 [0.037, 0.182], 15 wins, 3 ties, 2 losses, p = 0.0009; H2 (quotient >
proxy) 0.601 [0.433, 0.759], 17/3/0, p = 0.0001 (Holm 0.0002).
…CI, and Zenodo metadata

reproduce/Dockerfile builds the environment the artifacts were produced in: the package and its
research scripts, OPA 1.20.2 and the Kyverno CLI 1.19.1 (each checked against the release's
published SHA-256), cedarpy 4.12.1 and Z3. reproduce/run.sh runs three modes: verify (tool
versions, the pre-registration check, the study scripts' tests, the solver check of the witness
construction; minutes, no network), corpora (every corpus at the commit its artifact records)
and membership (re-measure every corpus and diff the counts).

reproduce/check_protocols.py makes the pre-registrations checkable after the fact: every
artifact that records a protocol hash must name a protocol file the repository still holds, so
a protocol edited after its study ran is reported. All ten pre-registered artifacts pass.

A workflow builds the image and runs verify on pull requests that touch the instruments, the
artifacts or the protocols. .zenodo.json carries the archive's metadata for the GitHub-Zenodo
integration; minting the DOI is the maintainers' step.
The abstract's closing sentence, the sentence both main texts share, the full version's
paragraph, contribution and conclusion, and the supporting information's record: the candidate
counts, read from the protocol's own frozen table; the exclusions by fault number; the means and
both comparisons; and each scored fault's table row. Three facts the prose states without a
number are asserted against the artifact: every fault whose fix reads only what the policy in use
read is a union of its classes, the proxy never beats the quotient, and both development faults
are exposed with certainty. The abstract's re-worded Cedar, Rego and corpus sentences are
re-anchored. The test workspace copies the protocols beside the artifacts. 318 pinned claims
agree on all three builds.
…e reads package versions from metadata

The mutation gate copies src, scripts and tests into its sandbox, so a test that loaded the
checker from reproduce/ could not import it there. cedarpy has no __version__ attribute; the
image's verify step now reads both versions through importlib.metadata.
…alence verdicts

The Cedar exact study calls a mutant equivalent when no cell of its witness space separates
it, and checks completeness by drawing 200 requests per file. This protocol puts the same
question to Cedar's symbolic compiler (cedar-policy-cli 4.12.0 `symcc equivalent`, cvc5
1.3.1), under the schemas the files' own authors wrote.

scripts/cedar_schema_candidates.py lists each scored file's schema candidates at the corpus
commit, nearest first, and takes the first that strictly validates the file. The frozen list,
docs/cedar-schema-candidates-v1.json, gives 72 of the 153 scored files a schema (41 in the
file's directory, 18 in an ancestor, 13 elsewhere; 53 repositories, 1,718 environments).
Outside the one development file, 71 files hold 173 equivalent and 830 live verdicts.

Primary outcome: equivalent verdicts refuted by a counterexample that cedarpy confirms;
the prediction is zero. The check is one-directional, and a refutation whose principal is
its resource is flagged, because the study's witness space omits such requests.
…file

scripts/cedar_symcc_crosscheck.py reproduces each file's verdicts with the Cedar exact
study's own code and seed, checks that SymCC reads the file's JSON form as its text, then
runs `cedar symcc equivalent` for every mutant in every environment of the authors' schema.
Every counterexample is parsed and decided again by cedarpy through the study's evaluation
function; only a confirmed one refutes an equivalent verdict.

The parser is pinned to what the CLI printed for a synthetic schema and policy covering
sets, records, entity references, extension values, ancestors, tags and escapes. On the
development file (promptfence forbid-support-delete) the 8 verdicts reproduce, the control
verifies in all 3 environments, the 7 equivalent verdicts verify in every environment, and
the one live mutant's counterexample is confirmed (Deny against Allow).
The sentence the article and the full version share, the uncertified count, the
contributions' count, the post-hoc reading, the supplement's per-language counts, the
first run, and every row of the census table, tied to its own table. Before pinning,
the guard checks that the census read the verdicts the membership artifacts record,
that every corpus reproduced and every text was recovered, and that the corrections
raised only the Google library and the two recovered Kyverno files. The two family
pins whose sentences the census replaced are retired, and the families table's total
row is tied to its table.
@MohammadThabetHassan MohammadThabetHassan changed the title Manuscript guard for the journal version; exact Rego studies, real faults, SymCC's check of the Cedar verdicts, and Xu et al.'s criteria Manuscript guard for the journal version, and the seven pre-registered studies behind it Oct 4, 2026
The shared sentence, the contributions and the supplement's result now say that Cedar's
22 rest on its designers' encoding and the rest were certified call by call; the pins
follow them and assert the Cedar count.
opa parse now reads a temporary file instead of /dev/stdin, and the mutation operator
writes that file with LF line endings: on a platform that translates newlines, every
multi-line location text carried a carriage return the source had not got, and those
mutants were silently dropped. Neither change alters a result on Linux; on Windows the
exact study now reproduces its committed record for privileged-containers exactly (13
mutants, 3 equivalent, the same survivor, the same 330 and 930 cells).
…y ships

The exact study decides equivalence under the settings each suite tests, so 43 of its 54
equivalents are relative and the paper gives a range, [76.7, 89.5]. This study decides
them again under every Constraint the library ships for the template, frozen here: five
of the 13 headline modules gain a new setting, holding 26 of the 43. The tested settings
must reproduce the exact study's record module by module before anything is scored;
a module undecided under a new setting is reported both ways.
…straint

Step for step the exact study's: the same mutants, kills, witness space and engine
decisions, on the same seeded generator. On the tested settings each module must
reproduce its committed record (counts, survivors by index, settings, cells per
setting) or it is reported and not scored. Each new shipped setting is then decided,
with every review the suite's inputs carry paired with the new parameters among the
off-cell checks; a module whose witness space cannot be built, or that shows a missing
cell, under a new setting is undecided there and pooled both ways. The shipped
Constraints are frozen in the script as in the protocol and recomputed before a run.

Tests check the protocol's hash and table, reading samples, and, on a synthetic
template whose suite tests only an exact exemption, that a wildcard Constraint
separates a mutant the tested settings leave equivalent. The development module
reproduces its record exactly.
…er the order

OPA's test runner prints a suite's inputs in an order that differs from run to run, and
the tested settings are read in that order. The first population run compared them with
the committed record as an ordered list, and four modules failed on order alone, with
every count, survivor and setting's cells the same; it separated no equivalent under any
shipped Constraint. The artifact's notes keep that run's account.
…results

Every one of the 14 modules reproduces its exact-study record on the tested settings.
Five of the 13 headline modules gain a shipped setting no test uses (wildcard image
exemptions, the full wildcard "*", a new allowedRoles and disallowAuthenticated shape),
holding 26 of the 43 parameter-relative equivalents. Every new setting is decided with
no missing cell and separates distinguishable mutants only: none of the 54 equivalents
is separated, so the pooled exact score under every shipped Constraint is 89.5%, the
tested score; 76.7% remains the bound for settings the library does not ship.
The abstract's score under every shipped Constraint, the full version's sentence (43
equivalents, 26 under a new setting, 89.5%), the supplement's counts and every row of
its table. Before pinning, the guard checks that every module reproduced, that the
tested figures are the exact study's, that no equivalent was separated (the article's
sentence), and that the shipped score lies between the worst case and the tested score,
as it must when a separated equivalent can never be a kill. The abstract's range pin
and its corpus-size pin move with the abstract's new wording.
@MohammadThabetHassan MohammadThabetHassan changed the title Manuscript guard for the journal version, and the seven pre-registered studies behind it Manuscript guard for the journal version, and the eight pre-registered studies behind it Oct 4, 2026
"Equivalents that depend on parameters" said what the study found false: none of
them moved. The supplement now says "in modules that read parameters", as the full
version does, and the pin follows it.
Inside the fragment every mutant is constant on each witness cell, so a mutant's
difference set is exact and subsumption is inclusion between difference sets: the
minimal set is computed, not estimated over a pool of tests. The study rescores the
payoff studies' and the criteria study's suites, unchanged, over minimal mutants on
the generated and Cedar populations, after reproducing all three artifacts over every
live mutant. Directions only are fixed, and what the paper says in each outcome.
Minimal mutants are computed exactly from each live mutant's difference set over the
witness cells: identical sets once, none with a strict subset among the others. The
payoff studies' four strategies and the criteria study's suites, with the same seeds
and constructions, are scored over every live mutant (which must reproduce all three
artifacts at their stored precision before anything is tested) and over the minimal
ones; H1m, H2m and each Q_s^m are tested one-sided with one Holm family per population.
Tests cover the definition, overlap that is not inclusion, the four strategies on a
small space, and the reference policy.
The first run looked the criteria study's decision coverage up among the payoff
studies' strategies, where "decision" names the proxy, so Q_decision^m tested the
quotient against the proxy twice, and the per-policy record let the proxy's score
overwrite decision coverage's. Each strategy is now named with the study it comes from;
a test pins the distinction. Every other figure of that run is unchanged.
…anged

Comparing a criterion with the quotient's score from the same study makes a tie at six
decimals a tie; the first run counted rounding differences as wins and losses. Every
other mean, interval and p value is that run's.
Run at aee8cc5 on the 300 generated policies and the 96 Cedar files of the primary
analysis, after reproducing both payoff studies and the criteria study over every live
mutant. 5,516 live mutants are 3,018 minimal ones, and 1,935 are 812. Every score falls
and the quotient's lead holds: 83.7% against 72.2% for a random suite of its size and
24.5% for the proxy on the generated policies, 98.6/88.3/17.3 on Cedar; it beats a
random suite of its size, the proxy and every established criterion on both
populations (Holm p at most 0.0009). Per policy it falls below a random suite of its
size on 25 of 300 and 4 of 96, against 15 and 2 over all mutants.
Seven sentences and eleven table rows of the new supplement section, and the full
version's threats sentence, are pinned to docs/minimal-mutant-study-v1.json; the
per-policy losses over all mutants come from the two payoff artifacts it reproduces.
The XACML criteria table's row pins matched their labels anywhere in the text, and the
new table has a row of the same name, so they now match only inside their own table.
459 claims hold on all three builds.
@MohammadThabetHassan MohammadThabetHassan changed the title Manuscript guard for the journal version, and the eight pre-registered studies behind it Manuscript guard for the journal version, and the nine pre-registered studies behind it Oct 4, 2026
The README states each limit once, drops the duplicated decision table in favour of one
that names the deciding rule, and lists the quality evidence plainly; every marker the
reality check requires is kept. The site's overview, installation, walkthrough and
research pages are rewritten to the same standard, with all commands unchanged. The
0.3.1 changelog gains a highlights section, describes the branch audit by what it
covered rather than how it was run, and no longer cites an audit report the repository
does not hold.
The Rego study's question, asked of a second admission language: which surviving
mutants of the Kyverno library's own suites are equivalent to their policies, the
suites' exact scores, and a resource that kills every real survivor. Fixed before
the instrument exists: the population (inside ClusterPolicies whose rules are pattern
or deny validate rules over request fields and the operation; 86 by static inspection),
the development set, the witness space and its candidates, every decision made by
kyverno apply, completeness checked three ways with a missing cell failing the policy,
the kill definition, the measures, closing the gaps, and what the paper says in each
outcome.
…y's suites

kyverno_witness_space.py builds, per rule, the observables the protocol names (pattern
leaves with anchors stripped, anchored keys' presence, condition paths, the operation,
and the names and namespaces selectors read) and their candidates, from the policy and
every mutant; cells are the product, one resource each. kyverno_exact_study.py computes
the population, runs every kill as kyverno_mutation runs it, has kyverno apply decide
the policy and every mutant on every cell and on the completeness inputs, splits any
batch the engine cannot load, and closes the gaps by adding each kill resource to the
suite. Developed on the three development policies only, where a namespace written
neither way had left every decision unread until the killed-but-equivalent count
exposed it.
Run at b7616ff under the protocol of c51346f. Of the 206 inside policies, 86 meet the
protocol's conditions on their guards; 28 have no mutant, 10 exceed the cell cap and one
names a kind with no known API version, leaving 44 scored beside the three development
policies. Every decision is Kyverno 1.19.1's, on 13,685 cells and 29,267 completeness
inputs; no policy fails the completeness check. The suites kill 95 of 129 mutants; only
2 of the 34 survivors are equivalent, so the exact score is 74.8% against a raw 73.6%.
The other 32 are real gaps in 11 policies, each with a resource that kills it, and adding
those resources to the suites kills all 32 and no equivalent mutant.
Eighteen claims tie the paper to docs/kyverno-exact-adequacy-v1.json: the sentence both
main texts share, the abstract's exact and raw scores, the full version's contribution,
every figure of the supplement section and each row of its table. The guard also asserts
what the prose rounds or implies: one survivor in seventeen equivalent, no stillborn
mutant, no kill of an equivalent one, no missing cell and no exception in closing the
gaps. 477 claims hold on all three builds. The post hoc analyses are described as such.
@MohammadThabetHassan MohammadThabetHassan changed the title Manuscript guard for the journal version, and the nine pre-registered studies behind it Manuscript guard for the journal version, and the ten pre-registered studies behind it Oct 4, 2026
The abstract now gives each population's three scores before the population, and a few
sentences gained a comma, a verb or a parenthesis; the pins follow the new phrasing. No
expected value changes, and all 477 claims pass on the three builds.
The abstract now starts a sentence with the generated-policies figures, so the pin accepts a
capital On. No expected value changes; all 477 claims pass on the three builds.
The supplement now names the schema category of the exclusion taxonomy
as a column rather than a row. The pin accepts either word; the expected
count (743 definitions) is unchanged.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants