gatecount

How many states does removing this check admit? An exact count, or an honest refusal.

"We fuzzed it and found zero escapes" is a statement about a search. It tells you what the search did not find, over however many inputs it happened to try, and it is equally consistent with the check being load-bearing, decorative, or holed.

"Removing this check admits exactly 30,240 additional states out of 32,768" is a statement about the system.

Two implementations become directly comparable. A redundant check shows up as a zero. Nobody has to agree on how much fuzzing is enough.

Install

pip install gatecount        # zero runtime dependencies

30-second quickstart

gatecount selftest
gatecount count    domain.json "x < 128 and y < 128"
gatecount removing domain.json "x < 128 and y < 128" "x < 128"    # blast radius
gatecount compare  domain.json "policy_a" "policy_b"              # both directions

Exit codes: 0 the check admits nothing extra · 1 it admits states · 2 no exact count was established. Note that 1 is the ordinary result for a check that does something — this is a measurement, not a pass/fail gate.

Worked example — the blast radius of an ownership check

examples/admission_policy.json declares a 32,768-point domain: 16 tenants, 16 entry owners, 64 token counts, a prefix flag.

$ gatecount removing examples/admission_policy.json \
    "tenant_id == entry_owner and token_count > 0" \
    "token_count > 0"
EXACT — states admitted ONLY when the check is removed
  admitted .......... 30240 of 32768 states (92.2852% of the domain)
  witness ........... entry_owner=0, is_prefix=0, tenant_id=1, token_count=1
  witness ........... entry_owner=0, is_prefix=0, tenant_id=1, token_count=2
  witness ........... entry_owner=0, is_prefix=0, tenant_id=1, token_count=3
  note .............. every point in the declared domain was evaluated
$ echo $?
1

Check it by hand: the guarded policy admits 16 × 63 × 2 = 2,016; the weakened one admits 16 × 16 × 63 × 2 = 32,256; the difference is 30,240. There is a test asserting exactly that.

And a check that turns out to do nothing:

$ gatecount removing examples/admission_policy.json \
    "token_count > 0 and token_count >= 0" "token_count > 0"
EXACT — states admitted ONLY when the check is removed
  admitted .......... 0 of 32768 states (0.0000% of the domain)
  The check admits NOTHING the rest of the policy did not already refuse.
  On this domain it is REDUNDANT — which is a finding, not a pass.
$ echo $?
0

A zero is a finding, not a clean bill of health. A check that admits nothing extra is either implied by another check or dead, and both are worth knowing.

Exact, sampled, or refused

method	when	what you get
exact	the domain is enumerable within the budget (20M points)	a count. Not an estimate
sampled	you passed --sample N explicitly	a fraction with an exact Clopper–Pearson interval, every field prefixed APPROXIMATE_, and no admitted_states field at all
refused	the domain is too large and you did not ask for sampling	an error naming the size and the cap

The tool never silently switches to sampling. An estimate presented as a count is worse than a refusal, so the distinction is carried in the result object and in the JSON — not only in the printout:

{
  "exact": false,
  "APPROXIMATE_admitted_estimate": 499000,
  "fraction_95_ci": [0.4830, 0.5285],
  "WARNING": "SAMPLED, NOT EXACT. `admitted_states` is deliberately absent: a sampled count that
              can be read as an exact one is the failure mode this tool exists to prevent."
}

result.empty — the "this check is redundant" property — is false for any sampled result, however many zeros the sample saw. A sampled zero is not a proof of emptiness.

Library use

from gatecount import Domain, over_accepting, compare

d = Domain.from_dict({"x": {"lo": 0, "hi": 255}, "y": {"lo": 0, "hi": 255}})

r = over_accepting(d, "x < 128 and y < 128", "x < 128")
r.admitted        # 16384
r.exact           # True
r.witnesses       # concrete points the weakened policy lets through

both = compare(d, "x < 128", "x < 200")     # both directions, always

Predicates may be expression strings or plain Python callables. The expression language is < <= > >= == !=, and or not, + - * /, parentheses, variables and numbers; 0 < x < 1 is rejected rather than regrouped.

What is refused

• a variable with an empty domain — the whole space is empty and every count is 0 vacuously;
• a duplicated domain value — the denominator, and every ratio using it, would be wrong;
• a domain with no variables — there is nothing to count over;
• a predicate mentioning an undeclared variable — no declared range means no denominator, so the count would be over a space nobody specified;
• a domain above the cap with no explicit --sample.

Honest scope

An exact count says: over the domain you declared, this many assignments are admitted by one predicate and refused by the other. It does not say:

• that the domain is the real input space. The count is exact for what you declared. If your real system takes a 64-bit integer and you declared 0–255, the number is right and about a different system. Choosing the domain is the analyst's job and the tool cannot check it.
• that the states are equally likely, or equally dangerous. This is a cardinality, not a risk estimate. 30,240 admitted states might all be unreachable in practice; one might be catastrophic.
• that the predicate is the real check. Transcribing your policy into an expression is a modelling step, and a model that omits a conjunct produces a confident count about code you do not run.

What this does not do

gatecount counts and reports. It never admits, refuses, or gates anything on the result. The counter counts; acting on the count is somebody else's decision. See CLAIMS-MAP.md.

Development

pip install -e ".[dev]"
python -m pytest -q          # 34 tests
gatecount selftest

Counts are checked against closed forms and against an independently written brute-force loop; the binomial interval is checked against SciPy when SciPy is installed. stats.py is vendored rather than rewritten, and its header says why: the rewrite was tried first and was silently wrong at one end of the interval.

License

Apache-2.0. See LICENSE and CONTRIBUTING.md.

Citing this? Metadata is in CITATION.cff — GitHub's "Cite this repository" button reads it directly.

---

The rest of the portfolio

25 artifacts, one idea: a measurement you cannot check is a press release. Every tool here reports; none of them gates.

Tools

abstain-bench	how often does a verifier pass input it could not check?
evidence	run the whole portfolio over your repo — the weakest leg, never the mean
floorgen	what must your system remember? an exact lower bound
formal-proof-mcp	a proof kernel for your coding agent
gatecount	exactly how many states does removing this check admit? ← you are here
gridlock	certify a wait-for relation cannot wedge
honestbench	measure your CI's escape rate
kvleak	cross-tenant leak scanner
kvprobe	model-substitution detector with a measured FPR
preregister	refuses to seal a plan whose conclusion is already fixed
proof-carrying-ci	the whole portfolio as one CI check, with SARIF
proof-to-code-drift	fail the build when the proof stops matching
sf-verify	re-derive admission decisions offline
signoff-cert	certificates that carry their own false-pass bound
tokencount	a token count both parties can recompute

Benchmarks — each recomputes one of our own published numbers from its certificate

illusion-bench	how many broken kernels does your oracle admit?
kv-reuse-econ-bench	recompute our economics headline
llm-tenant-isolation-bench	recompute our isolation figures

Datasets

abstain-corpus	32 inputs a verifier must NOT pass
kv-reuse-econ-traces	per-workload reuse accounting + the closed form
kv-tenant-isolation-bench	isolation observations, uninterpretable rows included
llm-precision-fingerprints	precision-labelled logprobs with a negative control

Try it in a browser — no install, no GPU

negative-results-atlas	ten claims we took back
tenant-leak-demo	the residency calculator
wait-for-visualiser	paste a wait-for graph, see the cycle

Documentation

Everything above, explained in one place: https://nickharris808.github.io/evidence-docs/ — the tutorial, what this proves and what it does not, and a CLI reference generated by running --help on every published command.

The commercial edition

Everything above is measure-only and Apache-2.0: it tells you what is true and never acts on it. The enforcement side — binding a partition key at the admission decision, the compiled gate corpus, and the certificate-issuing faucet — is covered by filed patents and licensed separately.

Reading is free. Enforcing is licensed.