Skip to content

test: property tests for the naming and encoding invariants#157

Open
ojhermann wants to merge 1 commit into
cachix:mainfrom
ojhermann:test/property-invariants
Open

test: property tests for the naming and encoding invariants#157
ojhermann wants to merge 1 commit into
cachix:mainfrom
ojhermann:test/property-invariants

Conversation

@ojhermann

Copy link
Copy Markdown
Contributor

Closes #156.

Adds proptest as a dev-dependency and quantifies the two invariants from the issue: akv name injectivity, and the encode_query inverse. Seven properties, 0.59s.

I checked both against the real pre-fix implementations rather than trusting that they work. That turned out to matter — see the second section.

What they catch

akv name injectivity. Restoring the old _- mapping in encode_name_component:

Test failed: name "secretspec--A--A--a" did not decode back to its triple
minimal failing input: (project, profile, key) = ("A", "A", "a")

Query encoding. Restoring the plain URI encoder that QUERY_ENCODE_SET replaced:

Test failed: value "#" did not survive the round-trip through "keyring://?v=#"
minimal failing input: value = "#"

Both fail on essentially the first case and shrink to something minimal.

The design bit worth reviewing

Injectivity stated over pairs is the honest phrasing, but a bad test. My first attempt was the obvious one:

fn distinct_triples_never_collide(a in triple(), b in triple()) {
    prop_assume!(a != b);
    prop_assert_ne!(format_secret_name(&a.0, ..)?, format_secret_name(&b.0, ..)?);
}

Run against the old _- scheme, it passes. Two independently generated triples essentially never collide by chance — finding ("a","b__c","d") vs ("a","b","c__d") that way is a needle in a haystack. It looks like a test of injectivity and is close to vacuous.

So the load-bearing property here is a left inverse instead: a name decodes back to exactly the triple that built it. If every name decodes to one triple, no two triples can share a name — same guarantee, but every single generated case exercises it, and it's linear rather than quadratic to sample.

I kept the pairwise form too, because it states the guarantee in the shape the module actually claims ("injective") and would catch a collision introduced somewhere other than the encoding. But it only earns its place with a generator biased toward the _/- region where every historical collision has lived:

prop_oneof!["[A-Za-z0-9_-]{1,8}", "[_-]{1,3}"]

So biased, against the old scheme it finds one immediately:

distinct triples ("_", "-", "---") and ("_", "_-_", "-")
  both produced "secretspec-----------"

That bias is commented in the source, since it looks arbitrary otherwise and is the difference between a real test and a decorative one.

Cost

  • 8 new lockfile entries, all dev-only: proptest, bit-set, bit-vec, quick-error, rand_xorshift, rusty-fork, unarray, wait-timeout. Nothing reaches anyone depending on secretspec.
  • 0.59s for the seven properties. Default 256 cases; happy to lower it.
  • No proptest-regressions files yet. If you'd rather those weren't committed when a failure is found, that's a one-line .gitignore — tell me which you prefer.

Not included

The third item from #156parse(uri(cfg)) == parse(spec) across every provider — isn't here. The trait object only exposes uri(), so what's reachable generically is idempotence (uri(parse(uri(parse(s)))) == uri(parse(s))), which is strictly weaker: it wouldn't catch a dropped field, because the loss happens in the first render and is stable after. Doing it properly needs per-provider config generators and PartialEq on the config types. Worth its own PR if you want it; I didn't want to smuggle that scope in here.

No CHANGELOG entry: test-only, no behaviour change, and the CHANGELOG asks for user-facing entries.

Two invariants the provider layer states in prose, claims over an infinite
domain, and has broken before. Adds `proptest` as a dev-dependency and
quantifies them.

akv name injectivity. `Fix Azure Key Vault name collisions` rewrote the naming
scheme onto Base32 because `_`->`-` let distinct triples collide; what guards
the rewrite is `assert_ne!` over one hand-picked pair per case. These sample the
whole component domain instead.

The load-bearing property is a left inverse — a name decodes back to exactly the
triple that built it — not the pairwise "no two collide". Injectivity stated over
pairs is the honest phrasing but a poor test: two independently generated triples
almost never collide, and sampled against the old `_`->`-` mapping the pairwise
property reports no collision at all while the left inverse fails on the first
case and shrinks to ("A", "A", "a"). The pairwise form is kept, with a generator
weighted toward the `_`/`-` region every historical collision has lived in; so
biased, it finds one immediately.

Query encoding. `QUERY_ENCODE_SET` states its own contract — it "makes
`encode_query` a true inverse of that parsing, so query values round-trip" — and
that claim about every string is checked today against one hand-written value in
one provider's tests. Sampled against the plain URI encoder it replaced, the
property fails and shrinks to "#". This is shared machinery: every provider's
`uri()` renders through it, and `uri()` names the store in audit records.

Both properties were checked against the real pre-fix implementations rather than
assumed to work.

Test-only; no behaviour change. The eight new lockfile entries are dev-only and
do not reach anyone depending on `secretspec`. The suite grows by 0.59s.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@ojhermann
ojhermann force-pushed the test/property-invariants branch from a6aae96 to 8380950 Compare July 17, 2026 00:28
@ojhermann

Copy link
Copy Markdown
Contributor Author

Force-pushed to drop two proptest-regressions/ files I had committed by accident (git add -A swept them up). They were seeds from failures of code I had temporarily broken to check the properties actually bite — not failures of anything in this PR, so they would have read as "what went wrong here?" for no reason.

Removing them also makes the note at the bottom of the description true again: there are no regression files, and the choice of whether to commit them or .gitignore them when a real failure turns up is still yours.

Now 5 files, +268/−2. Properties unchanged and still passing.

@domenkozar

Copy link
Copy Markdown
Member

Could we somehow write the property test once and run it through all registered providers?

@ojhermann

Copy link
Copy Markdown
Contributor Author

Could we somehow write the property test once and run it through all registered providers?

I'll look into this

@ojhermann

Copy link
Copy Markdown
Contributor Author

@domenkozar — yes, prototyped it. One property test now enumerates PROVIDER_REGISTRY, constructs each provider offline (URL parsing only, no client/network), and asserts the naming invariants across all 14 registered providers in a single body.

What made it shareable: two small, pure trait methods —

  • is_valid_native_name(item) — what names a store accepts (default: any non-empty; akv overrides with its letters/digits/hyphens rule).
  • convention_collapses_scope() — whether a store drops project/profile (dotenv, env, bws).

With those, one test covers determinism, charset-legality (the invariant akv's Base32 scheme exists to satisfy — now free for every current and future provider), and injectivity (skipping the scope-collapsing stores). akv keeps its own Base32 round-trip proptest, since decodability needs knowledge of its scheme and doesn't generalize.

It also surfaced a real thing: bws collapses project/profile like dotenv/env but wasn't classified as flat (FLAT_PROVIDERS listed only those two). Worth a look regardless of the test question.

Your call on scope:

  1. Take the generic test — the two trait methods + the shared proptest; one test across all providers for determinism/charset/injectivity, akv round-trip stays local. Prototyped and green; I can push it here.
  2. Keep naming tests provider-local — the shared encoding test already covers the one truly shared function (encode_query); leave naming per-provider.

I lean 1 — charset coverage for every future provider is the real win — but the two methods are an API addition, so your call.

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.

Property-based tests for the injectivity and round-trip invariants the provider layer already states

2 participants