Step 4 PR 1: permit decision + revocation + scope-faithful absence (contract, v1.4.0)

[sftimeless]

Summary

Step 4 PR 1 — public contract for revocation evidence + scope-faithful absence adjudication. Ships three new verifier claims as additive entries on keel-permit's v0 claim registry. Server-side emission (PR 2 on keel-api) and verifier adjudication (PR 3 on keel-verifier) follow as separate dispatches.

This is contract-only. No emission code, no adjudication code. The pinned semantics + JSON Schema + spec docs + baseline corpus + failure codes lock the public interface for the downstream work.

New claims (additive to claim_registry/v0.json)

Claim	Adjudicates
permit.decision.v1	Signed issuance decision (allow/deny/challenge) via existing binding_signature canonical payload. Issuance-only — never adjudicates mutated row state.
permit.revoked.v1	Signed permit.revoked event bound to both permit_id and project_id. New-only post-cutover. v1 immediate-effect semantics (effective_at == revoked_at).
permit.dispatch_absence_after_revocation.v1	Scope-faithful absence of dispatch.egress_bound events after the revocation effective_at, within a declared signed scope-faithful export segment anchored to signed checkpoint state.

Doctrine framing (locked, in-spec)

The verifier's trust model is falsifiability-oriented, not omniscience-oriented.

This PR uses "scope-faithful absence adjudication" throughout. The phrase "cryptographic non-membership" is reserved for future SMT/NMT/accumulator-backed primitives and never used to describe current Step 4 capability.

Reserved future term: `non_membership_profile` — registered as a reserved semantic-registry namespace for future SMT/NMT/accumulator-backed native non-membership work. Not implemented here. Same reserved-name discipline as `signature_v2` / `counter_signature` in `permit-v1.md` §11.

Standards anchors (cited in spec/dispatch-absence-after-revocation-v1.md)

• RFC 9162 (CT) — inclusion + consistency, no non-inclusion proof type
• draft-ietf-cose-merkle-tree-proofs — registers only inclusion (-1) + consistency (-2); non-membership explicitly out of scope
• draft-ietf-scitt-architecture — VDS-specific proof semantics

Multi-model design pass (§XII change process)

Design locked via 4-model convergence 2026-05-21 over ~2 hours:

• Claude — initial design + cryptographic pressure-test + independent verification (Alin Tomescu sorted-Merkle critique, Crosby/Wallach 2009 tamper-evident logging, RFC 9162, COSE Merkle proofs draft, SCITT architecture, Dahlberg/Pulls 2016 Sparse Merkle Trees)
• Codex — full Phase 1 audit + 6 contract-tightening corrections + local grammar verification
• ChatGPT — terminology lock + falsifiability framing + reserved-future-term recommendation
• Perplexity — standards research across CT/SCITT/COSE/SMT literature + audit framework guidance (SOC 2 SSAE 18, ISO 27001, NIST 800-53, PCAOB AS 1105, ISA 500)

Three soundness bugs prevented from shipping by this design pass

1. Challenge→deny mutation without binding refresh. Current code path mutates `decision` on challenge rejection/expiry without refreshing the signed binding — fixed via new signed state-transition events (PR 2 emission work).
2. Closure-absent overclaiming as "no execution happened." Closure can legitimately fire after revocation if dispatch fired BEFORE revocation. The absence claim now narrows to `dispatch.egress_bound` (initiation) only; downstream events are corroborating, not primary.
3. Plain Merkle absence overclaim. Naive "no matching events in scope" claims over plain Merkle commitments have weak soundness against a malicious prover. Locked terminology + checkpoint anchor + falsifiability framing keep doctrine honest. Native cryptographic non-membership reserved for future SMT/NMT work.

Files (35 changed, +2719 / -8)

• `claim_registry/v0.json` — 3 additive entries (existing entries unchanged per v0 immutability)
• `semantics/permit/{decision_v1,revoked_event_v1,dispatch_absence_after_revocation_v1}.json` — 3 pinned semantics
• `schemas/permit-revoked-event.schema.json` — new event schema (strict, `additionalProperties: false`)
• `spec/{permit-revoked-event-v1,dispatch-absence-after-revocation-v1}.md` — 2 new spec docs
• `spec/failure-codes.md` — new codes incl. `EXPORT_SCOPE_BRIDGE_RECORD_MATCHES_PREDICATE` (verdict: `disproved`, not `unverifiable_scope` — classification conflict, not unverifiability)
• `test-vectors/verifier_claims/v0/fixtures/` — 6 baseline corpus fixtures (negatives + edges land in PR 3)
• `CHANGELOG.md` — 1.4.0 entry

Out of scope (deferred to separate dispatches)

• keel-api server-side emission of `permit.revoked` events (= PR 2)
• keel-api closure-flow revocation guards (= PR 2)
• keel-api signed challenge state-transition events (= PR 2 or follow-on)
• keel-verifier adjudication code for any of the three claims (= PR 3)
• Verifier corpus negatives + edges (= PR 3)
• SMT / NMT / accumulator-backed native non-membership (= future Phase 2.x / Step 6+)
• Counter-signature work (separate dispatch; currently deferred pending PERMIT_V2 §4.3 multi-model design pass — NOT a Step 4 dependency)

Verification performed

• `python3 tools/check_repo_integrity.py` ✅ (jsonschema skipped — not installed locally)
• `python3 tools/check_public_hygiene.py` ✅
• `git diff --check origin/main..HEAD` ✅
• 6 fixture packs re-verified via `node scripts/build_step4_permit_claim_fixtures.mjs` ✅
• Doctrine prose greps:
  • 4× "scope-faithful absence" in absence-claim spec ✅
  • "falsifiability" in absence-claim spec ✅
  • `non_membership_profile` reserved term present ✅
  • Zero "cryptographic non-membership" matches in committed material describing current capability ✅

Next dispatches after merge

1. PR 2 on keel-api — server-side emission of `permit.revoked` events + closure-flow revocation guards + signed challenge state-transition events
2. PR 3 on keel-verifier — adjudication code for the 3 claims + full corpus (negatives + edges) + PyPI publish keel-verifier 2.3.0
3. PR 4 (cross-repo integration) — parity guards, capability inventory finalization, corpus path coordination, coordinated publication

Related

• keel-verifier v2.1.0 PyPI (Step 2 closure, 2026-05-21) — supplies the scope_state primitive that Step 4 builds on
• keel-verifier v2.2.0 PyPI (Trust Stack A.1, 2026-05-21) — supplies the release-authenticity substrate

🤖 Generated via §XII multi-model design pass

Co-Authored-By: Claude noreply@anthropic.com
Co-Authored-By: Codex noreply@openai.com