Prove registry key unambiguity in Lean; evidence five more core laws

[0thernet]

The provider-plugin registry's route key (<transport>:<surfaceId>) and exact-contract key (<transport>:<surfaceId>/<operation>@<contractVersion>) are now proven unambiguous in Lean — each key parses back to its parts and no two valid coordinate tuples share a key — with a seeded unseparated-key defect refuted and differential tests binding the Lean model to the TypeScript grammars. The lane also evidences five more core laws: injected clocks in the approval broker, serialized plugin lifecycle, CAS no-rollback, no-writes-on-read-paths, and local-CLI post-spawn indeterminate.

Claims moved (6)

Claim	Layer	Evidence
identifier-roundtrip	lean	RouteKey.lean: parse_routeKey, routeKey_injective, parse_operationKey, operationKey_injective, plus the operationKeyUnseparated defect refutation; differential rsurf/rop/rkey/okey against isProviderPluginSurfaceId, isProviderPluginOperationName, routeKey, operationKey
lifecycle-injected-clocks	stateful-model	approval-broker two-clock model (src/control/approval-broker-clock.model.test.ts)
plugin-lifecycle-serialized	stateful-model	src/provider-plugin-lifecycle-kernel.test.ts (+310)
state-cas-no-rollback	stateful-model	src/storage-cas.model.test.ts (+242)
no-writes-on-read-paths	example	D14 admission-claim example; gap narrowed to the fingerprinted examples
local-cli-post-spawn-indeterminate	quint	local-cli.qnt (Apalache length 8, 2,000 × 8-step samples) + 628-line production replay

Evidence and how the evidence fails when broken

• Lean. lake build --wfail compiles the new module with warnings as errors; the axiom audit counts all 66 required theorems with their recorded statement digests; proofs.json registers the RouteKey theorems and the operationKeyUnseparated seeded defect, which the audit proves refutes operationKey_injective.
• Differential. scripts/verification-lean-encodings.test.ts generates identifier candidates heavy in key separators and near the length bounds and asserts the Lean validSurface/validOperation/routeKey/operationKey agree with the TypeScript; the seeded defect's counterexample is rejected by production.
• Local-CLI model. local-cli.qnt checks postSpawnIndeterminate/noRespawn; stepRetryTimeout and stepTrustNotStarted mutants must violate them; scripts/verification-local-cli-replay.test.ts replays 1,000 seeded traces through production.
• Honest scope. identifier-roundtrip's notVerified records that the grammars are modelled by hand from their regular expressions, that the differential test samples generated inputs, and that the registry's positive-safe-integer check on contract versions is not modelled.

Defects found

• None new in production; the lane narrowed two notVerified gaps to their measured extent (smuggled-key, read-path writes) so the claims describe exactly what the examples fingerprint.

Package budget

Only src/provider-plugin-registry.ts ships (+6 lines: routeKey/operationKey exported with doc references to the proofs). Lean files, proofs.json, models, and tests stay out of the package.

CI cost

Lean build time grows by one 277-line module plus differential property runs; local-cli.qnt adds an Apalache length-8 check and a 1,000-trace replay to the Required verification job.

Not covered

• Registry keys for identifier grammars other than surface IDs and operation names (adapter, auth, run IDs, portable operation identities, cursor tokens, platform catalog IDs) remain example/property-tested only.
• The Lean model is hand-derived from the regexes; the differential test samples generated inputs rather than proving the regex itself.
• Local validation on this host: bun run verify:lean passed fully (build --wfail, axiom audit, all seeded defects, differential tests); typecheck and claims render/check pass post-merge. Helper-heavy stateful suites are delegated to the Required CI run on this head.

🤖 Generated with Claude Code

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated
ghostget	Ready	Preview	Sep 25, 2026 4:15am UTC