PSP-1 - Capability Model and Grammar

Metadata

Status:

Review

Edition:

2025-09-04

Extends:

-

Updates:

-

Obsoletes:

-

Depends on:

PSP-3, PSP-4

Informative references:

PSP-2

1. Abstract

PSP-1 defines the portable, verifiable capability model used by Polykey to express delegated authority. It specifies the structure and semantics of identity-bound authority Grants and Presentations which are ephemeral proofs of capability. In this model, capabilities are canonical, monotone programs evaluated by Capability Enforcement Points (CEPs). Delegation is achieved by syntactic attenuation along a delegation chain: derived Grants may only add checks or shrink finite action/resource scopes and never broaden authority. Programs are normalized into a Program Canonical Form (PCF) and deterministically encoded to derive stable content identifiers, enabling portable verification and anchored delegation chains. PSP-1 specifies the capability program model, multi-scope declarations (finite action/resource sets), delegation/attenuation semantics, revocation checks, and CEP verification behavior. Transport/envelope bindings and sigchain framing are defined in PSP-3; receipt formats and proof traces are defined in PSP-2; enforcement placement/modes are defined in the CEP/BA specification; acceptance and governance live in TAP/RAM.

2. Conventions and Terminology

2.1 Requirements Language

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals, as shown here.

2.2 Core Terminology

• Principal (P): Originator of authority; issues a Grant to a Subject.
• Subject (S): Holder of a Grant that exercises the capability by creating a Presentation.
• Resource (R): Target of the action; may host a native CEP (CEP(R)).
• Capability Enforcement Point (CEP): An agent at P/S/R that verifies Presentations and enforces capabilities.
• Grant (G): A durable, signed statement on a sigchain that carries a capability program; issued by P to S.
• Presentation (Π): An ephemeral proof-of-possession (PoP) token created by S that references a Grant by its canonical digest (grantRef, per PSP-3). It is bound to a live channel and runtime context and is NOT stored on sigchains.
• Channel binding: A cryptographic binding of a Presentation to the live transport/session per a declared binding profile (e.g., TLS exporter, DPoP). It proves the Presentation was minted for, and presented on, the specific session being enforced.
• Verification (Σ): The CEP's verification event; it validates PoP and channel binding, verifies custody and syntactic attenuation along any delegation chain (and anchoring where required), and evaluates the capability program under bounded resources. On success, enforcement MAY proceed and, in derive-style enforcement variants, MAY result in creation of a session-scoped authority.
• Lease: The upstream authority relationship to a non-native Source of Authority (SoA). If a Grant touches a non-native SoA, the enforcing CEP MUST verify Lease freshness per TAP policy.
• CPL: Capability Programming Language.
• Program (CPL/0): A monotone policy evaluated by CEPs, composed of Checks (OR of Queries), Queries (AND of Literals), and Literals that are pure, bounded Builtins over ground Terms (Str/Int/Bytes/Bool). CPL/0 has no user-defined atoms, symbols, or variables. The "/0" suffix denotes the first generation of the Capability Programming Language; future families (e.g., CPL/1) may extend the language without altering the semantics of CPL/0.
• Declarations: Finite sets/relations used by programs: PairSet of (action, resource), ActionSet, and ResourceSet.
• Program Canonical Form (PCF): The normalized, deterministically encoded representation of a Program used for hashing/signing.
• Attenuation: Delegation that only adds checks/tightens literals and shrinks declared sets; never broadens authority.
• Builtins Registry: Versioned, content-addressed set of pure, bounded builtins (time/ttl, channel lattice, resource subset, etc.).
• Pin: A self-describing, content-addressed identifier (e.g., multihash/CID) that refers to an immutable artifact (of any kind). Pins may be expressed as URIs when a scheme/protocol is defined (e.g., cid://..., ipfs://..., https:// with immutable digest parameters). In PSP-1, pins are used to fix semantics; typical examples include the pinned builtins set (builtinsId), the pinned channel lattice (channelLatticeId), and the pinned schemes manifest (schemesSnapshotId). CEPs MUST recognize required pins and, across delegation chains, matching pins are REQUIRED where they affect evaluation.
• Anchoring: A TAP-approved method that binds the root issuer of a delegation chain to a resource domain.
• Access PoAR: The Proof-of-Action receipt written by the enforcing CEP (defined in PSP-2).
• Local Availability: An artifact (Grant, revocation state, lattice snapshot, comparator or other evaluation input) is "locally available" at enforcement if it can be accessed by the CEP without network I/O, within TAP-defined resource bounds, at the moment verification begins. Pre-enforcement resolution (governed by TAP) MAY populate local storage before verification starts. During Program evaluation, any missing required input MUST cause denial.
• TAP (Threat and Acceptance Policy): The acceptance policy that governs time discipline, chain depth and anchoring requirements, resolver/mirroring allowances, replay defenses, and other deployment-specific constraints used by CEPs during verification.
• CEP Placement Variants: A CEP may operate in different trust domains depending on where verification occurs. These placements are defined in the CEP/BA specification and referenced throughout PSP-1.
  • CEP(R) (Resource-side CEP): A CEP embedded in or colocated with the target Resource. It verifies Presentations natively within the Resource's trust domain. No bridging or long-lived upstream lease is involved.
  • CEP(P) (Principal-side CEP): A CEP operated within the Principal's trust domain. When a CEP(P) bridges to a non-PK-native Source of Authority, it acts as a Principal-Side Bridge Adapter (PS-BA) and holds the upstream lease; it must enforce exposure modes (mediate, derive, reveal) and verify lease freshness per TAP.
  • CEP(S) (Subject-side CEP): A CEP operated within the Subject's trust domain. The common pattern is the Subject Session Authority (SSA), where the Subject derives short-scope tokens from a PK-native resource. When a CEP(S) bridges a non-PK-native Source of Authority, it acts as a Subject-Side Bridge Adapter (SS-BA) and enforces exposure modes under TAP guardrails.
• Bridge Adapter (BA): A specialized role of a CEP(P) or CEP(S) that bridges to a non-PK-native Source of Authority (SoA) using a long-lived upstream lease. Bridge Adapters are not a separate placement; they are sub-roles of existing CEP placements. When bridging, a Principal-side CEP is called a PS-BA, and a Subject-side CEP is called an SS-BA. Bridge Adapters enforce exposure modes-mediate, derive, and reveal-as defined in the CEP/BA specification and must verify lease freshness per TAP. Exposure modes dictate how secrets or tokens are handled when interacting with legacy systems.

2.3 Identifier & casing convention

To ensure unambiguous interoperation across implementations, PSP-1 adopts a uniform lower-camelCase naming convention for all specification identifiers. Unless explicitly noted otherwise:

• Builtin operator identifiers (op strings) MUST be lower-camelCase ASCII. For example: withinTime, ttlOk, channelGeq, inPairSet, inActionSet, inResourceSet, ctxEq, presenterIs, and enforcerEq.
• Registry pins and metadata fields MUST use lower-camelCase. Examples include programId, programBytes, langVersion, builtinsId, channelLatticeId, and schemesSnapshotId.
• Environment fact names and illustrative example fields SHOULD use lower-camelCase (e.g., grantRef, channelBinding, presenter, enforcer, ctx).

Registered claims imported from other standards (such as JWT claims iat, exp, jti) retain their original names and are not subject to this convention. Scheme names (e.g., vault:, k8s:) and content identifiers (e.g., cid:...) are treated as data, not identifiers, and therefore remain unchanged.

These canonical names appear in the textual specification and in the non-normative JSON projections. PSP-3 defines the on-wire field names and encodings.

2.4 Interpretation of JSON Projections

This specification includes JSON examples to illustrate semantic structure. Field names and encodings in these examples are non-normative. The authoritative wire format, field bindings, and canonical bytes are defined in PSP-3. Implementers MUST NOT rely on example field names or encodings for interoperability.

3. Motivation and Rationale

3.1 Motivation

PSP-1 is Polykey's core capability model: a minimal, verifiable program model and enforcement semantics that let independent parties mint, hold, present, and verify capabilities across boundaries without centralized Policy Decision Points. By constraining policies to monotone programs with syntactic attenuation and pinned semantics, PSP-1 guarantees deterministic, portable enforcement across independently operated CEPs. Together with PCF identity, registry pinning, and closed-world evaluation, decisions become portable and auditable (via PSP-2) while remaining resilient to semantic drift (via PSP-4).

What PSP-1 defines:

• Capability Program (CPL/0): a monotone program with finite Declarations (PairSet/ActionSet/ResourceSet), normalized into a Program Canonical Form (PCF) for stable digests.
• Grants and Presentations: Grants are signed, durable sigchain statements that carry the Program; Presentations are ephemeral PoP tokens bound to a live channel/context that reference a Grant.
• Delegation & attenuation: syntactic attenuation along a delegation chain (add checks, shrink finite sets; never broaden authority).
• CEP verification (high level): validate PoP and channel binding, verify custody/attenuation (and anchoring where required), then evaluate the Program under bounded resources.

3.2 Design Principles

• Portable: Grants and Presentations are verifiable across organizational and network boundaries.
• Minimal: monotone fragment; finite, subset-checkable declarations; versioned content-addressed registries.
• Attenuable: Derived Grants MUST be subsets of their parents; attenuation is verifiable at enforcement.
• Secure by default: Holder-of-key (PoP) + channel binding; short TTLs for Presentations; pure, bounded builtins only.
• Receipt-ready: CEPs can emit Access PoARs with program projection/proof traces (see PSP-2).

3.3 Threat Model Pointers

PSP-1 addresses a set of well-understood threat vectors. This section highlights those scenarios and points to TAP for policy controls and mitigations.

• Replay and session hijacking: Attackers may replay previously issued Presentations or intercept tokens to impersonate a Subject. PSP-1 defends against replay by requiring holder-of-key PoP signatures, strong channel bindings, per-presentation nonces (jti), and short presentation TTLs. TAP further governs nonce reuse, replay caches, and session invalidation.
• Semantic drift and comparator drift: Changing definitions of builtins, channel lattices, or scheme comparators can alter the meaning of Grants over time. PSP-1 mitigates this by pinning the exact rulebooks in every Grant (builtinsId, channelLatticeId, schemesSnapshotId); mismatched or unknown pins cause a fail-closed deny.
• Resource explosion and unbounded selectors: Unconstrained wildcards or regex patterns could broaden authority or make subset checks undecidable. PSP-1 requires declarations to be finite and safely bounded. Scheme comparators MUST provide decidable subset relations, and unbounded selectors are forbidden unless the comparator defines a safe, bounded proof strategy.
• Lease compromise and bridging attacks: When a CEP acts as a Bridge Adapter to a non-PK-native Source of Authority (SoA), the upstream lease or secret may be stolen or tampered with. PSP-1 enforces PoP and channel binding but leaves the lease lifecycle and exposure mode policies to TAP and the CEP/BA specification. TAP specifies mediate/derive/reveal modes, lease freshness checks, and dual-control requirements.
• Time skew and clock tampering: Inaccurate clocks can circumvent TTL and time windows. PSP-1 mandates a single captured now per enforcement and requires half-open time windows. TAP governs time sources and skew tolerances; enforcement MUST deny if time discipline cannot be satisfied.
• Revocation and chain freshness: Stale or revoked Grants must not be honored. PSP-1 requires revocation state for the leaf and any required parents to be locally available; unknown or stale revocation data causes a fail-closed deny. TAP defines freshness policies and revocation distribution.
• Denial of service: Malicious inputs may include large declarations or complex Programs to exhaust CEP resources. PSP-1 bounds declaration size and enforces pure, deterministic builtins with bounded evaluation. TAP may impose additional CPU/memory budgets and per-request deadlines.
• Confidentiality and context exposure: Excessive context in ctx or declarations may leak personal or operational data. PSP-1 encourages minimal, non-PII context, and PSP-2 defines receipt redaction and selective disclosure mechanisms.

3.4 Rationale

PSP-1's design choices aim to make verification deterministic, portable, and mechanically checkable.

• Monotone CPL/0
  • The checks-only fragment (no variables, rules, recursion, or negation) keeps evaluation decidable and fast and reduces the trusted computing base. Programs are ANDs of checks; checks are ORs of queries; queries are ANDs of ground builtin literals. This aligns with the “checks” fragment of Biscuit.
• Syntactic attenuation (delegation)
  • Syntactic attenuation is a deliberate restriction that makes delegation mechanically checkable and removes subjective interpretations of what "controls authority." A child preserves all parent Checks, may drop Queries to narrow ORs, and may only tighten literal constants and shrink finite Declarations. Under these constraints the CEP can verify attenuation purely through structural subset relations (no inference required).
  • This mirrors the checks-only fragment of Biscuit tokens and ensures independent implementations make identical decisions when verifying a delegation chain. Without syntactic rules, issuers could embed logic that ambiguously broadens or narrows authority, making it difficult or impossible for a CEP to decide whether a child has overstepped the parent.
  • The syntactic approach dovetails with PCF canonicalization: reordering checks or literals does not affect identity, and monotonicity is explicit in the Program structure. See Section 6, Security Considerations for risks mitigated by syntactic attenuation.
• PCF identity
  • Canonicalization (PCF) yields stable program identity (programId) across platforms by sorting/deduplicating literals/queries/checks and enforcing deterministic term encodings. Cosmetic permutations never change identity.
• Pinned semantics
  • Builtins, channel lattices, and scheme comparators are content-addressed snapshots (CIDs). Pinning prevents "semantic drift," and compatibility is enforced across delegation hops to keep meaning consistent across time and deployments.
• Closed-world evaluation
  • The CEP evaluates with locally available inputs only (no network I/O), under bounded resources and a single captured time (now). This ensures reproducibility and supports real-time and offline/segmented deployments.
• Declarations
  • Finite sets (PairSet/ActionSet/ResourceSet) capture scope compactly and make attenuation checks efficient; scheme comparators provide normalization and subset relations.

These choices keep the kernel small and auditable, facilitate receipts, and allow domain-specific TAP policies to govern acceptance without changing core semantics.

3.5 Out of Scope

• Enforcement placement/modes: CEP/BA placements (P/S/R) and mediate/derive/reveal semantics are specified in the CEP/BA spec.
• Lease lifecycle/rotation: Lease issuance and rotation policies are defined elsewhere; PSP-1 only requires Lease freshness to be verified when Grants touch non-native SoA (enforced by CEP per TAP).
• Receipt schemas: All receipt formats (PoAR/VOR/View) are specified in PSP-2.
• Transport/envelope and sigchain framing (JOSE/COSE/DSSE, canonical bytes): specified in PSP-3.
• Channel binding profiles: Concrete channel binding mechanisms (e.g., TLS exporter, DPoP) are defined elsewhere; PSP-1 only requires a verified binding.
• Global time/ordering: PSP-1 does not require a global clock or total order. Acceptance (TAP) specifies clock sources and tolerances.
• Secret issuance/derivation/aggregation crypto and interactive evaluation flows.
• No ZK/succinct delegation proofs in core; no signature aggregation (e.g., BLS).
• No recursion or negation-as-failure in the Program (monotone only).
• No geo polygons beyond finite region sets; no policy graph solvers.
• No regex/unbounded wildcards in resource comparators (prefix/finite models only).
• No network I/O in builtins; all builtins MUST be pure, deterministic, and bounded.

4. Normative Kernel

This section defines the single sources of truth (SSOT) for verification: CPL/0 language model, evaluation environment, declarations, semantic pinning, program canonical form, verification algorithm, time model, and fail-closed catalogue

4.1 CPL/0 Language Model

This section defines the CPL/0 language evaluated by CEPs: abstract structure, term discipline, builtin model (by reference), and evaluation constraints. Registry pinning details are defined in Section 4.4, Semantic Pinning and PSP-4.

• Structure
  • Program = all(Check*)
  • Check = any(Query+)
  • Query = and(Literal+)
  • A Program succeeds iff every Check succeeds.
  • A Check succeeds iff at least one of its Queries succeeds.
  • A Query succeeds iff all of its Literals succeed.
• Literals and Terms
  • Literals are builtin predicates: Builtin(op, [args...]). op is a string identifier of a registered builtin (see Appendix B for the catalog; pinning in Section 4.4, Semantic Pinning).
  • Terms are ground: Str | Int | Bool | Bytes. No variables. No user-defined atoms.
  • Int is arbitrary-precision. Floats are not permitted.
• Monotonicity and purity
  • Programs MUST be monotone. Adding Checks or adding Literals can only narrow authority.
  • Builtins MUST be pure, deterministic, and resource-bounded (CPU/steps/memory). No network I/O or ambient mutable state.
• Typing and comparison
  • Builtins MUST validate argument types at evaluation; ill-typed invocations MUST result in deny.
  • Strings are interpreted in NFC for equality; Bytes are compared as exact octets.
• Builtins and external registries
  • The builtin operator set (identifiers, signatures, semantics, tightening rules) is defined in the Builtins registry and pinned by builtinsId (Section 4.4, _Semantic Pinning; PSP-4).
  • Channel-related literals (e.g., channelGeq) interpret identifiers using the pinned channel lattice (channelLatticeId) (Section 4.4, _Semantic Pinning).
  • Declaration-aware literals (inPairSet, inActionSet, inResourceSet) rely on scheme comparators selected by resource scheme name (Section 4.4, _Semantic Pinning).
• Evaluation discipline
  • Evaluation MUST be performed under CEP-enforced limits (CPU/steps/memory); exceeding limits MUST result in deny.
  • A single logical now: Int (Unix seconds) is captured per enforcement and used consistently (see Section 4.7, Time Model and Boundaries for the time model).

4.2 Evaluation Environment

At verification, the CEP supplies an environment of facts. Builtins may reference these facts by name.

• Required environment facts
  • action: Str - action being attempted (e.g., "secret:read").
  • resource: Str - target resource identifier (scheme-normalized).
  • now: Int - Unix seconds at enforcement.
  • iat: Int - Unix seconds carried by the Presentation.
  • presenter: Str - DID of the presenting Subject.
  • enforcer: Str - DID/identifier of the enforcing CEP (audience).
  • channel: Str - the live session's channel binding profile identifier.
  • ctx: Map<Str, Term> - runtime context (e.g., {"ns":"prod","pod":"runner-42"}).
• Optional environment facts (TAP-gated)
  • leaseStatus - optional TAP-provided evidence used to assess upstream lease/credential freshness. Semantics are TAP-defined; no network I/O occurs during evaluation.
  • TAP MAY require additional environment facts (e.g., provenance labels, jurisdiction tags, or digest references) and define how they are obtained and verified. PSP-1 does not enumerate these; Programs assert them via equality (e.g., ctxEq).
• Missing facts
  • If a builtin present in the Program requires an environment fact that is missing, evaluation MUST fail closed.
  • The CEP MUST normalize resource using the same comparator semantics used to canonicalize declarations before any literal evaluation. Normalization failure MUST cause deny.

4.3 Declarations

Declarations are finite, canonical datasets that a Grant carries alongside the Program. Programs consult Declarations via builtins under pure, bounded evaluation (no network I/O). Declarations exist to express scope allowlists compactly and to make attenuation (subset) checks mechanical and fast.

• Declarations MUST be finite, deterministically canonicalized (normalize, sort, deduplicate), and content-addressed (e.g., with a content identifier).
• Declarations referenced by a Program MUST be bundled in the Grant so CEPs can evaluate without external fetches.
• A CEP MUST deny if a Program references an unknown declaration kind or if a required scheme comparator is unavailable.

There are 2 kinds of literals in declarations: actions and resources.

4.3.1 Actions

Actions are namespaced strings. They appear as elements inside PairSet/ActionSet.

• deploy:to_env
• access:open
• energy:curtail
• secret:read
• secret:derive
• data:export
• model:infer

Actions are plain strings compared for equality. Governance over action names (e.g., allow-lists, required prefixes/constraints) is out of scope for PSP-1 and is defined by TAP policy.

4.3.2 Resources

Resources identify targets and SHOULD be expressed as URIs (or URI-like identifiers) with scheme-specific rules. They appear as elements inside PairSet/ResourceSet.

• k8s://ns/prod
• door:building-12:lock-3
• meter:utility:site-42
• api:https://api.vendor.com/path
• vault:secret://org/team/service/key-id
• asset:building-12:rtu-3

Normative requirements

• Scheme comparator: Each resource scheme MUST have a registry entry that defines normalization and a decidable subset comparator. Registry artifacts SHOULD be content-addressed.
• Specificity: Grants SHOULD use specific resources. If a scheme permits selectors or wildcards, their use MUST be constrained by Program constraints and the scheme's registry rules.
• Attenuation check: For a derived Grant, resource.child MUST be a subset of resource.parent under the scheme's registered subset relation.
• Unknown schemes: If a CEP cannot resolve a scheme or its comparator, it MUST deny.
• Bounded selectors: Patterns/selectors (when allowed) MUST be finite or safely bounded (e.g., explicit sets, bounded prefixes/namespaces) with a defined subset proof. Unbounded globs/regex MUST NOT be permitted unless the registry specifies a safe comparator and proof strategy.
• TAP scoping: TAP policies MAY restrict acceptable schemes per domain and MAY further constrain resource forms (e.g., disallow selectors).

4.3.3 PairSet

PairSet is a finite set of (action: Str, resource: Str) pairs. It enumerates exactly which action/resource combinations are authorized.

• Canonicalization:
  • Normalize each resource string per its scheme's registry entry (PSP-4).
  • Sort pairs lexicographically (e.g., by action, then by normalized resource bytes).
  • Deduplicate exact duplicates.
  • Content-address the canonical bytes to get a stable identifier (CID).
• Portability: PairSets are bundled in the Grant payload (PSP-3 binds bytes) so a CEP can evaluate without network I/O.

Use PairSet when the allowlist is irregular (different actions per resource) and a simple factorization would be incorrect.

4.3.4 ActionSet

ActionSet is a finite set of actions. It factorizes "what" independently of "where."

• Canonicalization:
  • Actions MUST be normalized as strings, sorted deterministically, and deduplicated.
  • The canonical bytes MUST be content-addressed; the content address identifies the ActionSet.
• Program use
  • inActionSet(action, Actions#CID) evaluates to true if and only if action $\in$ ActionSet(CID).
• Attenuation
  • For a derived Grant, the child ActionSet MUST be a subset of the parent ActionSet.

4.3.5 ResourceSet

ResourceSet is a finite set of resources (scheme-qualified strings) with scheme-defined subset semantics.

• Canonicalization
  • Each resource MUST be normalized per its scheme's registry entry.
  • The set MUST be sorted deterministically and deduplicated.
  • The canonical bytes MUST be content-addressed; the content address identifies the ResourceSet.
• Program use
  • inResourceSet(resource, Resources#CID) evaluates to true if and only if there exists r_sel $\in$ ResourceSet(CID) with resource $\subseteq$ r_sel under the scheme's registered subset comparator.
• Attenuation
  • For a derived Grant, the child ResourceSet MUST be a subset of the parent ResourceSet (under set inclusion, using the same normalization and comparator).

Use ActionSet * ResourceSet when the policy is truly a cross-product ("any action in A over any resource in R"). Use PairSet when the matrix is irregular.

4.3.6 Program Use

• Programs consult Declarations via builtins (inPairSet, inActionSet, inResourceSet) using the environment's action and resource facts, combined with other literals (withinTime, ttlOk, channelGeq, ctxEq, presenterIs).
• Actions appear as strings; resources are scheme-qualified strings; subset relations are defined by the scheme comparator (no unbounded regex/globs; selectors MUST be finite or safely bounded with a decidable comparator).
• Unknown declaration kinds, schemes, or comparators MUST cause deny.

4.3.7 Attenuation over Declarations

• Delegation MUST NOT broaden Declarations.
  • PairSet_child $\subseteq$ PairSet_parent.
  • ActionSet_child $\subseteq$ ActionSet_parent.
  • ResourceSet_child $\subseteq$ ResourceSet_parent.
• CEPs MUST verify subset relations hop-by-hop along the delegation chain using the same normalization and comparators; failures or unknowns MUST cause deny.

4.3.8 TAP constraints

PSP-1 standardizes exactly three declaration kinds: PairSet, ActionSet and ResourceSet. Deployments may impose additional acceptance rules via their Threat & Acceptance Policy (TAP). For example, a TAP MAY disallow certain declaration kinds for particular actions or restrict which resource schemes are acceptable. When TAP forbids a declaration kind or a required scheme comparator is unavailable, the CEP MUST deny. These TAP constraints do not alter the semantics defined in this specification.

4.4 Semantic Pinning

This section establishes the minimal, versioned dependencies that capability evaluation relies on, and what a Grant MUST pin so Capability Enforcement Points (CEPs) reach the same decision everywhere. The purpose of semantic pinning is to prevent "semantic drift" - where the meaning of a capability could change over time or across implementations - by fixing the exact rulebooks used for evaluation. PSP-4 defines the actual registry artifacts; PSP-3 defines the on-wire fields and canonical bytes.

4.4.1 Purpose

Capability evaluation depends on a few small, versioned "rulebooks". A Grant MUST pin identifiers for these rulebooks so that independent CEPs evaluating the same Program can arrive at identical decisions at different times and in different deployments. Without pinning, the meaning of a capability could silently change if, for example, a builtin operator's semantics were tightened or a scheme comparator evolved.

4.4.2 What MUST be pinned

A Grant MUST include the following identifiers in its pins map. Each identifier references an immutable snapshot in a registry (see PSP-4):

• langVersion - the CPL/0 language generation. For this specification the value MUST be cpl/0.
• builtinsId - a content-addressed snapshot of the builtin operators in use (including each opcode's semantics, type signatures, tightening rules, and resource bounds).
• schemesSnapshotId - a content-addressed manifest that maps each scheme name referenced by this Grant's declarations to the exact comparator snapshot used for normalization and subset comparison. It MUST be present even if only one scheme is referenced.
• channelLatticeId - REQUIRED only if the Program uses the channelGeq builtin. It is a content-addressed snapshot of the channel lattice used to interpret >= between channel binding profile identifiers. It MUST be omitted if the Program does not call channelGeq.

A Grant does not pin any action registry; actions are plain strings compared for equality. Governance over action names lives in TAP and MAY be enforced by requiring corresponding Program literals.

4.4.3 Snapshot formats

Each pinned identifier refers to a snapshot whose structure is defined in PSP-4. This specification only requires that CEPs treat these snapshots as opaque rulebooks when evaluating Programs.

• Builtins snapshot - Contains a unique ID, version string, and a list of builtin operators. Each operator entry defines the operator's identifier, argument types, semantics, tightening rules for attenuation, and resource bounds (time/memory). Unknown operators MUST cause denial at verification.
• Channel lattice snapshot - Contains a unique ID, a set of channel binding profile identifiers, and a partial order over those identifiers. The partial order defines the result of channelGeq(channel, floor). The precise meaning of each label (e.g., mtls:v1, tls-exporter:v1, dpop:v1, bearer:v1) is defined outside this spec in the registry; only the ordering matters here.
• Schemes manifest (schemesSnapshotId) - Contains a unique ID and a map from scheme names to comparator snapshot IDs. Each comparator snapshot defines normalization and subset decision rules for one scheme (e.g., vault, k8s, door). Unknown or unavailable comparators MUST cause denial. The manifest MUST list every scheme referenced by the Grant's declarations.

4.4.4 Delegation compatibility

In a delegation chain, a child Grant MUST pin exactly the same rulebooks as its parent. For each parent->child hop:

• langVersion(child) == langVersion(parent).
• builtinsId(child) == builtinsId(parent).
• If either Program uses channelGeq, then channelLatticeId(child) == channelLatticeId(parent). If neither uses channelGeq, neither Grant may specify a lattice ID.
• schemesSnapshotId(child) == schemesSnapshotId(parent). The same comparator semantics MUST apply consistently across the chain.

Any mismatch in these identifiers MUST cause denial at verification. Unknown or unavailable builtins, lattices, or comparators at any hop MUST also cause denial.

4.4.5 Fail-closed conditions

A CEP MUST deny if any of the following holds:

• builtinsId is missing, unknown, or cannot be loaded.
• The Program uses channelGeq but channelLatticeId is missing or unknown.
• The Program uses channelGeq but the pinned channelLatticeId does not match across delegation hops.
• schemesSnapshotId is missing, unknown, or mismatched across delegation hops.
• Any resource string's scheme lacks a comparator in the pinned schemesSnapshotId.
• The Program references a builtin not present in the pinned builtinsId.
• Any required registry entry cannot be loaded or applied at verification time.

4.4.6 Interpreting channelGeq

The literal channelGeq(channel, floor) compares the verified channel binding profile identifier (from the Presentation's channel binding) against the floor value under the pinned channel lattice. Common channel binding profiles include:

• mtls:v1 - Mutually authenticated TLS 1.3 (see RFC 8446).
• tls-exporter:v1 - TLS exporter-based channel binding (see RFC 9266).
• dpop:v1 - Demonstrating Proof-of-Possession (DPoP) (see RFC 9449).
• bearer:v1 - No sender-constraining (Bearer tokens).

The pinned lattice defines the partial order between these labels (for example: mtls:v1 >= tls-exporter:v1 >= dpop:v1 >= bearer:v1). This section is informative; the authoritative ordering and the set of recognized profiles are defined by the snapshot referenced by channelLatticeId.

4.4.7 Registry artifacts are defined in PSP-4

The structure and encoding of the builtins snapshot, channel lattice snapshot, and schemes manifest are defined in PSP-4. This specification does not redefine those schemas; it only specifies which identifiers MUST be present in a Grant and how they are enforced.

4.5 Program Canonical Form

Programs MUST be normalized to a canonical tree and deterministically encoded before deriving identity. Canonicalization ensures portable, stable program identifiers across implementations and platforms. The canonical bytes and multihash parameters are specified by PSP-3; this section defines the abstract normalization rules (PCF).

4.5.1 Purpose

• PCF yields a unique representation for a Program so syntactic permutations or duplicate literals do not change identity.
• Canonicalization applies to the abstract Program (Checks, Queries, Literals and their arguments), independent of transport/envelope.

4.5.2 Normalization rules

• Literals within a Query MUST be sorted by a total order over:
  • operator/predicate identifier (text in NFC, bytewise),
  • arguments tuple under canonical term order.
• Duplicate Literals within a Query MUST be removed.
• Queries within a Check MUST be sorted lexicographically by their canonical literal lists and duplicates removed.
• Checks within a Program MUST be sorted lexicographically by their canonical query lists and duplicates removed.

4.5.3 Canonical term order

• Strings MUST be NFC-normalized and compared/encoded as exact bytes.
• Integers MUST be arbitrary-precision, with no float encodings.
• Bytes MUST be exact octets, ordered lexicographically.
• Booleans MUST use canonical forms, with false < true for ordering.
• Environment and declaration references (e.g., "action", "resource", "Pairs#CID") MUST be encoded deterministically and consistently wherever they appear.

4.5.4 Prohibited and Non-Canonical Forms

Certain forms are incompatible with deterministic canonicalization and MUST NOT appear in a CPL/0 Program or its canonical representation:

• Floating-point numbers: Programs MUST NOT contain floating-point values. CPL/0 supports only arbitrary-precision integers.
• Indefinite-length encodings and non-normalized strings: All strings MUST be NFC-normalized and encoded with definite lengths. Indefinite-length encodings and non-normalized strings MUST NOT appear in the canonical bytes (see PSP-3 for encoding constraints).
• Non-determinism or network I/O: Any literal or term that would introduce non-determinism (e.g., entropy, randomness) or perform network/external I/O MUST NOT be part of a Program. Builtins are pure and deterministic by construction; user-defined or environment-sourced non-deterministic operations are out of scope for CPL/0.

4.5.5 Deterministic encoding and identity

• programBytes = ENCODE(PCF(Program)) as specified by PSP-3.
• programId = multihash(programBytes) as specified by PSP-3.
• A Grant carrying programBytes and programId MUST be rejected if recomputation does not match.
• ENCODE is defined in PSP-3; PCF is defined here in PSP-1.

4.5.6 Failure handling

• Canonicalization MUST fail, and verification MUST deny, if a Program contains an unknown operator, ill-typed arguments under a builtin's signature, non-normalized strings, prohibited numbers, or otherwise cannot be normalized.
• Unknown builtins, schemes, or comparators referenced by the Program MUST cause deny during evaluation. If such references prevent deterministic term encodings, identity derivation MUST fail.

4.5.7 Stability and tests

• Canonicalization is part of the trusted computing base. Implementations SHOULD cross-test that semantically identical Programs (after literal reordering, duplicate removal, and string normalization) yield identical programBytes and programId across platforms and versions.

4.6 Verification Algorithm

4.6.1 Algorithm

1. Parse Presentation
   • Validate required conceptual fields: presenter, grantRef, iat, exp, jti, channelBinding, and ctx (these field names are conceptual; on-wire names are defined in PSP-3).
   • Capture a single logical now at the start of enforcement. Enforce the Presentation lifetime window using this now: require iat <= now < exp (subject to TAP clock discipline); else deny.
2. Verify PoP and channel binding
   • Verify the presenter's proof-of-possession signature over the Presentation payload; else deny.
   • Verify channelBinding matches the live session per the declared profile (e.g., TLS exporter, DPoP); else deny.
3. Resolve and verify the leaf Grant (local)
   • Locate the leaf Grant by grantRef in local storage; if unavailable, deny.
   • Verify signatures and envelope framing per PSP-3 (issuer, subject, prev, created_at/nbf/exp as applicable).
   • Enforce the Grant's envelope validity window (if present). Where both Grant and Presentation windows apply, enforce their intersection; else deny.
   • Check revocation state for the leaf Grant per PSP-3/TAP (locally available). If revoked or indeterminate per TAP freshness policy, deny.
   • If enforcement relies on an upstream lease, credential, or secret from a non-native Source of Authority (e.g., a Bridge/Adapter flow), the CEP MUST evaluate freshness per TAP using only locally available evidence (e.g., a TAP-approved environment fact such as leaseStatus). If freshness cannot be established per TAP policy, the CEP MUST deny. PSP-1 does not define the format or acquisition of such evidence.
4. Verify delegation chain (if applicable)
   • Ensure all required parent Grants are locally available; else deny.
   • For each hop child -> parent:
     • Custody and placement: issuer(child) == subject(parent); signatures valid; prev linkage correct; else deny.
     • Depth and cycles: no cycles; deny if TAP depth cap exceeded.
     • Pinned semantics compatibility: langVersion matches; builtinsId matches; channelLatticeId matches whenever channelGeq is used by either hop; schemesSnapshotId matches; else deny.
     • Scheme comparator availability: comparators required by referenced schemes are known/available; else deny.
     • Syntactic attenuation:
       • Program: child MAY add Checks; MUST NOT remove parent Checks. For each retained parent Query, child Literals $\supseteq$ parent Literals; literal constants only tighten per Builtins tightening rules (PSP-4); equality permitted.
       • Declarations: PairSet_child $\subseteq$ PairSet_parent; ActionSet_child $\subseteq$ ActionSet_parent; ResourceSet_child $\subseteq$ ResourceSet_parent (under the scheme comparator).
   • Anchoring: if TAP requires anchoring the root issuer for the resource domain and no applicable method is satisfied, deny.
5. Build evaluation environment (facts)
   • Construct environment facts per Section 4.2, Evaluation Environment from the Presentation, live session, and TAP-approved inputs.
   • Capture a single logical now and use it consistently.
   • Normalize env.resource using the same scheme comparator semantics used for declaration canonicalization; normalization failure -> deny.
6. Load Program and Declarations from the leaf Grant
   • Parse programBytes; recompute programId and require match; else deny.
   • Ensure all Declarations referenced by the Program are present as bundled canonical bytes; else deny.
   • Confirm pinned semantics are usable: builtinsId known; if the Program uses channelGeq, channelLatticeId present and known; schemesSnapshotId present and known; else deny.
7. Evaluate Program (closed-world, bounded)
   • Evaluate the CPL/0 Program against the environment facts and bundled Declarations with pinned semantics:
     • inPairSet / inActionSet / inResourceSet
     • withinTime / ttlOk
     • channelGeq
     • ctxEq
     • presenterIs (if used)
   • Enforce type checks; ill-typed literals -> deny.
   • Enforce resource bounds (CPU/steps/memory). Exceeding limits MUST result in deny.
   • Unknown builtin, unknown lattice, or unknown scheme comparator required by the Program -> deny.
   • Context superset: ctx MUST include all required ctxEq(k, v) literals with equal values; else deny.
8. Decision and receipts (placement-agnostic)
   • Allow enforcement per placement/mode (mediate/derive/reveal are defined outside PSP-1).
   • The enforcing CEP MUST record a decision event (allow or deny) for every enforcement.
   • If the implementation supports PSP-2 receipts, it MUST additionally emit the appropriate receipt:
     • Access PoAR on allow.
     • DenyReceipt on deny.
   • The structure and required fields of these receipts are defined in PSP-2. PSP-1 does not define receipt contents.

4.6.2 Execution Constraints

• Single time capture
  • The CEP MUST capture a single logical now at the start of enforcement and use it consistently for withinTime, ttlOk, envelope window checks, and receipt timestamps.
• Time discipline
  • TAP governs clock source and skew tolerance; the CEP MUST apply TAP's discipline to all time comparisons. If time discipline cannot be satisfied (e.g., clock indeterminate), the CEP MUST deny.
• Deadlines and budgets
  • The CEP MUST enforce bounded evaluation (CPU/steps/memory). If TAP sets a per-request deadline, the CEP MUST abort and deny when the deadline is reached.
• Closed-world inputs
  • All required inputs (leaf Grant, parent Grants, revocation state) MUST be locally available at the start of enforcement; otherwise the CEP MUST deny. No network I/O

4.6.3 Invariants

• Closed-world: The CEP MUST evaluate using only { programBytes/programId, bundled Declarations, builtinsId, channelLatticeId when used, schemesSnapshotId, and the scheme comparator selected by scheme name }. No other registry artifacts may change the decision at enforcement.
• No network I/O during evaluation: If required Grants or revocation state are not locally available at enforcement, the CEP MUST deny.
• Fail-closed: Any ambiguity, unknown, or unevaluable condition in the steps above MUST result in deny.

4.7 Time Model and Boundaries

• Single time capture: The CEP MUST capture a single logical now : Int (Unix seconds) at the start of enforcement. All time comparisons in this algorithm and in builtins evaluation use this same now.
• Half-open windows: Unless a builtin's pinned definition states otherwise, all time windows are half-open intervals [start, end), i.e., inclusive of start, exclusive of end.
  • Presentation validity window: [iat, exp) - accept iff iat <= now < exp.
  • Grant envelope windows (e.g., not_before, not_after per PSP-3) are also treated as half-open and MUST be intersected with the Presentation window.
  • withinTime(now, nbf, exp) succeeds iff nbf <= now < exp under the pinned builtins set.
  • ttlOk(iat, now, ttlMax) succeeds iff now < iat + ttlMax.
• Precedence / intersection: When multiple constraints apply (Presentation window, Grant envelope, and time-based builtins such as withinTime and ttlOk), the effective acceptance condition is the intersection of all applicable constraints at the captured now. If any one fails, enforcement MUST deny.
• Time discipline: Clock source and skew tolerance are governed by TAP policy; all time comparisons MUST follow TAP's time discipline. If time discipline cannot be satisfied (e.g., clock indeterminate), enforcement MUST deny.

4.8 Fail-Closed Catalogue

A CEP MUST deny enforcement if any of the following conditions hold.

Category	Condition
Cryptographic	Proof-of-possession signature invalid
Cryptographic	Channel binding mismatch with the live session
Cryptographic	Grant signature invalid
Temporal	Presentation expired or not yet valid (iat <= now < exp violated)
Temporal	Grant envelope validity window violated
Temporal	Time discipline unsatisfied per TAP
Registry/Pins	Unknown or missing langVersion
Registry/Pins	Unknown or missing builtinsId
Registry/Pins	Unknown or missing channelLatticeId when channelGeq is used
Registry/Pins	schemesSnapshotId mismatch across delegation hops
Registry/Pins	Unknown or unavailable scheme comparator
Chain Structure	grantRef unresolvable to a valid Grant
Chain Structure	issuer(child) != subject(parent)
Chain Structure	Cycle detected in delegation chain
Chain Structure	TAP maximum delegation depth exceeded
Attenuation	Child removes any parent Check
Attenuation	Retained child Query omits any parent Literal
Attenuation	Child broadens a literal constant against tightening rules
Attenuation	Child Declarations are not subsets of parent Declarations
Evaluation	Program references unknown builtin op
Evaluation	Ill-typed literal arguments
Evaluation	Resource normalization failure
Evaluation	Missing required ctx key/value (ctxEq)
Evaluation	CPU/memory/step budgets exceeded
Revocation	Leaf or required parent Grant revoked
Revocation	Revocation state unavailable or indeterminate per TAP freshness
Availability	Required parent Grants not locally available at enforcement
Availability	Declaration bytes missing or malformed
Integrity	programId mismatch on recomputation

5. Artifacts

5.1 Grants

A Grant is a durable, signed statement on an issuer's (P's) sigchain that authorizes a Subject (S) to exercise authority as defined by its embedded capability Program (CPL/0) and the finite Declarations. Verification is deterministic and portable via Program Canonical Form (PCF) identity and registry pinning. Transport framing, canonical bytes, signatures, and revocation claims are specified in PSP-3.

5.1.1 Purpose and Role

• Grants are the unit of durable, identity-bound authority. They encode:
  • The capability Program (CPL/0) as canonical bytes.
  • The Declarations (PairSet, ActionSet, ResourceSet) the Program consults.
  • The registry pins that fix semantics (language version, builtins, and, when used, channel lattice).
• Grants are issued by a Principal (P) to a Subject (S). The Subject later creates Presentations that reference a specific Grant by its canonical digest for enforcement.
• Grants can be delegated: a Subject may issue a derived Grant to a new Subject, under strict syntactic attenuation and pin compatibility (see Delegation & Attenuation).

5.1.2 Normative Requirements

A conforming Grant MUST satisfy all of the following.

1. Payload contents
   • programBytes: The deterministic encoding of PCF(Program) as specified by PSP-3.
   • programId: The multihash of programBytes (PSP-3). CEPs MUST recompute and match.
   • declarations: A finite map from declaration identifiers to bundled canonical bytes:
     • Each identifier MUST be a content address (e.g., CID) derived from canonicalized declaration bytes.
     • Canonicalization of declarations MUST follow PSP-1 rules for the specific kind (PairSet, ActionSet, ResourceSet).
     • The bytes for every referenced declaration MUST be bundled in the Grant payload; no network fetches at evaluation.
   • pins: Registry pins that fix semantics across CEPs and time (see Section 4.4.2, What MUST be pinned).
2. Envelope and framing
   • The envelope (issuer, subject, issuance/validity timestamps, prev linkage, signatures, canonical bytes for the entire claim) is defined in PSP-3.
   • Grants MUST be written on the issuer's sigchain with at least one valid signature per PSP-3.
   • A canonical digest for the entire Grant claim MUST be derivable per PSP-3; Presentations reference this digest as grantRef.
   • CEPs MUST check revocation per PSP-3/TAP before enforcement.
3. Program identity and integrity
   • Implementations MUST construct PCF(Program) prior to deriving programId.
   • At verification, the CEP MUST recompute programId from programBytes. Any mismatch MUST cause deny.
   • If the Program references any declaration identifier (e.g., Pairs#CID, Actions#CID, Resources#CID), the corresponding canonical bytes MUST be included in declarations; missing entries MUST cause deny.
4. Registry pinning and compatibility
   • The Program's semantics MUST be interpreted under the pinned langVersion and builtinsId. If unknown or unavailable, verification MUST deny.
   • If the Program contains channelGeq, channelLatticeId MUST be present and recognized. Unknown lattices MUST cause deny.
   • Resource scheme semantics are selected by the scheme name present in resource strings and MUST match the Scheme registry known to the CEP. Unknown schemes or unavailable comparators MUST cause deny.
   • In a delegation chain, a child Grant's langVersion and builtinsId MUST equal the parent's values. If channelGeq is used in either parent or child, channelLatticeId (when present) MUST be equal across the chain. Any mismatch MUST cause deny.
5. Declarations and bundling
   • Only the standardized declaration kinds are recognized in PSP-1: PairSet, ActionSet, ResourceSet.
   • Declarations MUST be finite, normalized per scheme rules (for resources), sorted, and deduplicated prior to content addressing.
   • Programs MUST reference declarations by content identifier (CID). CEPs MUST resolve references to the bundled bytes; string aliases or labels are non-normative and ignored during verification.
   • Unknown declaration kinds or inability to apply required scheme comparators MUST cause deny.
6. Fail-closed behavior
   • If the Program references a builtin not present in builtinsId, verification MUST deny.
   • If the Program uses channelGeq but channelLatticeId is missing or unknown, verification MUST deny.
   • If any declaration reference is missing from declarations, is malformed, or fails canonical checks, verification MUST deny.
   • If any resource string in a declaration cannot be normalized under its scheme's rules, verification MUST deny.
   • If programBytes cannot be parsed into a valid CPL/0 Program per PSP-1 (e.g., type errors, prohibited terms), verification MUST deny.
7. Determinism and normalization invariants
   • The CEP MUST evaluate using only {programBytes/programId, bundled Declarations, builtinsId, channelLatticeId when used, and the scheme comparator selected by scheme name}. No other registry artifacts may change the decision at verification.
   • At verification time the CEP MUST normalize the environment resource using the same scheme comparator semantics as those used during declaration canonicalization; normalization failure MUST cause deny.

5.1.3 Relationship to Presentations and Enforcement

• Presentations are ephemeral proofs that reference a Grant by its canonical digest (grantRef). They carry PoP, channel binding, iat/exp, and ctx facts. Presentations are NOT recorded on sigchains.
• CEPs verify the Grant (signatures, revocation per PSP-3), verify custody and syntactic attenuation along any delegation chain under the pinned registries, then evaluate the leaf Program against CEP-provided environment facts and the Grant's bundled Declarations.
• On success, enforcement MAY proceed, and the CEP SHOULD emit an Access PoAR containing programId, declaration CIDs, registry pins, and a minimal evaluation trace per PSP-2.
• CEPs MUST deny if grantRef cannot be resolved to a valid Grant under PSP-3 framing and signatures.

5.1.4 Illustrative Projection

The following illustrates only the Grant payload structure relevant to PSP-1. Envelope fields, signatures, canonical claim bytes, and multihash details are defined in PSP-3. Field names in the JSON projection use camelCase for readability. These labels are illustrative only; the normative field names and encodings are defined in PSP-3. Implementers MUST NOT rely on these example names.

{
  "programId": "mh:...", // multihash(programBytes) per PSP-3
  "programBytes": "...", // ENCODE(PCF(Program)) per PSP-3
  "declarations": {
    "pairs:cid:Qm...": "...", // canonical bytes of PairSet
    "actions:cid:Qn...": "...", // canonical bytes of ActionSet (if used)
    "resources:cid:Qr...": "..." // canonical bytes of ResourceSet (if used)
  },
  "pins": {
    "langVersion": "cpl/0",
    "builtinsId": "cid:builtins@YYYYMMDD",
    "channelLatticeId": "cid:lattice@1", // REQUIRED iff Program uses `channelGeq`
    "schemesSnapshotId": "cid:schemes@YYYYMMDD" // REQUIRED: pinned manifest of scheme comparators
  }
}

Implementers MUST NOT rely on this projection for wire encoding; the normative transport and encoding are specified in PSP-3.

5.2 Presentations

A Presentation is an ephemeral, on-path proof by the Subject (S) that it possesses a specific Grant and is exercising it now, on this live channel, in this runtime context. Presentations are NOT written to sigchains. They reference a Grant by its canonical digest (grantRef, per PSP-3), are proof-of-possession (PoP) bound to the holder's key, and are cryptographically bound to the live session via a channel binding profile. PSP-1 defines the semantic components a CEP must verify and evaluate. PSP-3 defines the on-wire signature container and field mappings; Presentations have no durable sigchain envelope and MUST remain small and referential in PSP-1 core.

5.2.1 Purpose and Role

• Ephemeral proof: Demonstrates holder-of-key (PoP) and binds use to the current session.
• Grant reference: Points to the leaf Grant (grantRef per PSP-3) that carries the Program and bundled Declarations.
• Runtime facts: Conveys ctx and timing (iat/exp) the CEP uses to evaluate the Program's literals (e.g., ctxEq, ttlOk, withinTime).

5.2.2 Rationale

Presentations are intentionally ephemeral. Unlike Grants, which are durable and recorded on sigchains, a Presentation conveys proof-of-possession only for the duration of a single live session. Short-lived tokens dramatically reduce the window in which an attacker could replay or steal a capability. They also allow time-bounded constraints (e.g., ttlOk, withinTime) and context-dependent predicates (channelBinding, ctxEq) to be enforced on each invocation without recording sensitive per-use context on a public ledger. Persisting Presentations or allowing them to be reused indefinitely would undermine these protections, enable unauthorized redistribution, and blur the distinction between durable Grants and transient proof-of-use.

5.2.3 Normative Requirements

A conforming Presentation MUST satisfy all of the following.

• Proof-of-possession and channel binding
  • The Presentation MUST be signed by the presenter (PoP). The CEP MUST verify PoP.
  • The Presentation MUST be bound to the live session per the declared channelBinding profile. The CEP MUST verify that the binding matches the live session and deny on mismatch.
• Lifetime and timing
  • The CEP MUST reject if the Presentation is expired (now >= exp) or used too early (now < iat), subject to TAP clock discipline.
  • If the Program contains ttlOk or withinTime literals, the CEP MUST enforce them using iat/now/exp as appropriate.
  • Effective lifetime: Enforce the intersection of all applicable time windows at the captured now. See Section 4.7, Time Model and Boundaries.
  • If the Program does not constrain Presentation lifetime via ttlOk, TAP MAY impose a default maximum Presentation TTL.
• Context
  • ctx MUST be a superset of the required ctxEq(k, v) literals in the Program. Missing keys or unequal values MUST cause deny.
• Grant reference and custody
  • grantRef MUST resolve to a valid leaf Grant under PSP-3 framing and signatures; failure MUST cause deny.
  • If delegation is present, the Presentation MUST carry (or, per TAP, make resolvable by a pre-enforcement resolver) sufficient delegation material to verify:
    • custody hop-by-hop (issuer(child) == subject(parent)),
    • prev linkage (per PSP-3),
    • pins compatibility (langVersion, builtinsId, and channelLatticeId when channelGeq is used),
    • syntactic attenuation (checks/literals tightening and declarations subset).
  • How parent Grants are made available is TAP-governed (e.g., local cache, pre-enforcement resolver, or a TAP required stapled chain proof / zk chain proof). At enforcement, if required parent Grants are not locally available, the CEP MUST deny.
  • Any failure in the above MUST cause deny.
• Storage
  • Presentations MUST NOT be recorded on sigchains.

5.2.4 Fail-Closed Conditions

A CEP MUST deny if any of the following holds:

• PoP signature invalid or channel binding does not match the live session.
• Presentation lifetime invalid or violates ttlOk/withinTime literals.
• grantRef cannot be resolved to a valid Grant (PSP-3).
• Custody/attenuation verification fails (missing parents; signature or prev linkage failure; cycle; TAP depth exceeded; pins mismatch; non-attenuating child).
• Unknown or unavailable builtin referenced by the Program; unknown channelLatticeId when channelGeq is present.
• Unknown or unavailable scheme comparator required for declaration evaluation; env.resource normalization failure under the active comparator.
• Missing required ctx keys or mismatched ctxEq values.
• Grant envelope validity window is violated (now outside not_before/not_after per PSP-3).
• Required parent Grants are not locally available at enforcement (e.g., TAP forbids resolution or resolution failed).

5.2.5 Illustrative Projection

• presenter: DID of the holder (Subject).
• grantRef: canonical digest of the leaf Grant (per PSP-3).
• iat: Int (Unix seconds) - mint time.
• exp: Int (Unix seconds) - expiry; exp - iat SHOULD be short; MAY be bounded by the Program via ttlOk.
• jti: nonce (unique) for replay resistance.
• channelBinding: { profile: Str, value: BytesOrB64 } - binding to the live session (e.g., TLS exporter, DPoP).
• ctx: Map<Str, Term> - runtime context; MUST include at least the key/value pairs required by the Program's ctxEq literals.
• Delegation material (TAP-governed):
  • Presentations in PSP-1 core MUST carry only grantRef (leaf digest). They MAY include grantRefs: an ordered list of parent digests (leaf->root) as resolution hints. Resolution, if allowed, is a TAP-governed, pre-enforcement step outside CPL/0 evaluation. At enforcement, if required parent Grants are not locally available, the CEP MUST deny.
  • A TAP policy (with PSP-3 bindings) MAY define alternate, bounded chain attestation artifacts (e.g., a stapled chain proof or a zero-knowledge chain proof). PSP-1 core does not define or require such artifacts and forbids embedding raw Grant bodies in Presentations.

The following illustrates the Presentation structure relevant to PSP-1. Names and encodings are illustrative only; the normative specification of on-wire fields is defined in PSP-3.

{
  "jti": "uuid-1234",
  "iss": "did:pk:S",
  "iat": 1768099200,
  "exp": 1768099320,
  "channelBinding": {
    "profile": "tls-exporter:v1",
    "value": "base64url(exporter)"
  },
  "ctx": { "ns": "ci", "pod": "runner-xyz" },
  "grantRef": "cid://G_leaf",
  "grantRefs": ["cid://G_parent", "cid://G_root"] // OPTIONAL: ordered leaf->root digests (resolution hints)
}

5.3 Delegation & Attenuation

Delegation allows a Subject (S) that holds a Grant to issue a derived Grant to a new Subject (S2) while never broadening authority (narrower or equal). PSP-1 defines delegation as a mechanical, syntactic subset relation over Programs and Declarations, verified hop-by-hop under pinned semantics. Custody (issuer/subject lineage), chain structure, and any anchoring requirements are enforced by the CEP with no network I/O during Program evaluation.

5.3.1 Purpose and Scope

• Custody: Each derived Grant is authored by the delegator and written on the delegator's sigchain; custody is the hop-by-hop relationship issuer(child) == subject(parent).
• Syntactic attenuation: A child Grant can only narrow or preserve authority (never broaden) by adding checks, tightening literal constants, and shrinking finite Declarations.
• Pinned semantics: All Grants in a chain are interpreted under identical language/builtin sets (and channel lattice when used). Mismatches cause deny.
• Determinism: Unknown or unavailable semantics (builtins, lattice, scheme comparator) fail-closed; CEP decisions are reproducible across independent deployments.
• TAP MAY disallow equal-scope delegation (co-equal grants) by policy (e.g., depth/fan-out caps or strict attenuation requirements). PSP-1 permits equality by default.

5.3.2 Chain Structure and Custody

• Hop custody
  • issuer(child) MUST equal subject(parent).
  • Each Grant in the chain MUST be written on its issuer's sigchain with valid signatures per PSP-3.
  • All required parent Grants MUST be locally available at enforcement; otherwise the CEP MUST deny. (Pre-enforcement acquisition is TAP-governed.)
  • prev linkage MUST form a simple path from leaf to root; the CEP MUST deny if any digest repeats (cycle detection).
• Depth and anchors (TAP-governed)
  • TAP MAY set a maximum delegation depth H; the CEP MUST deny when exceeded.
  • Anchoring of the root issuer for the target resource domain (when applicable) is governed by TAP; if an applicable anchoring method is required but not satisfied, the CEP MUST deny.

5.3.3 Pinned Semantics Compatibility Across Hops

For each parent->child hop:

• langVersion_child MUST equal langVersion_parent.
• builtinsId_child MUST equal builtinsId_parent.
• If channelGeq appears in either parent or child, channelLatticeId_child MUST equal channelLatticeId_parent.
• Scheme comparator consistency: For each resource scheme name referenced by Declarations, the same comparator semantics MUST be applicable across the chain. If a scheme comparator is unknown or unavailable at enforcement, the CEP MUST deny.

Any mismatch in the above MUST cause the CEP to deny chain acceptance.

5.3.4 Syntactic Attenuation

PSP-1 defines attenuation as a purely syntactic subset relation checked hop-by-hop. Children MAY only narrow or preserve authority.

• Program (checks/queries/literals)
  • Checks (Program is AND of Checks):
    • A child Program MUST include all parent Checks (by PCF identity) and MAY add additional Checks.
  • Queries (each Check is OR of Queries):
    • The child MAY remove any subset of the parent's Queries (narrowing the OR). For any retained parent Query, the child Query MUST include all parent Literals (L_child $\supseteq$ L_parent) and MAY add additional Literals.
  • Literal tightening (constants only narrow):
    • Literal constants MAY only be tightened according to the Builtins tightening rules pinned by builtinsId (see PSP-4). Examples:
      • withinTime: child interval $\subseteq$ parent interval.
      • ttlOk: child ttlMax <= parent ttlMax.
      • channelGeq: child floor >= parent floor under the pinned lattice.
      • ctxEq: parent ctxEq(k,v) MUST be preserved; the child MAY add more ctxEq constraints.
    • Equality is permitted: a child may preserve the parent's constants and literals. TAP MAY require strict attenuation (child < parent) in some domains.
  • Context preservation:
    • Any ctxEq(k,v) required by the parent MUST be preserved or further constrained by the child. At enforcement, Presentation.ctx MUST be a superset of the required keys with equal values (see Presentations).
    • Issuers that wish to prevent redistribution SHOULD include presenterIs(...) in the Program; because ctx/literal constraints must be preserved or tightened, re-delegation to a different Subject becomes impossible.
• Declarations (finite sets; multi-scope)
  • PairSet_child $\subseteq$ PairSet_parent.
  • ActionSet_child $\subseteq$ ActionSet_parent.
  • ResourceSet_child $\subseteq$ ResourceSet_parent (under set inclusion defined by the scheme comparator).
  • Declarations MUST remain finite and canonical (normalize, sort, deduplicate) under the same comparator semantics.
• Actions vs resources
  • Actions are plain strings compared for equality (no registry semantics in PSP-1).
  • Resource subset checks MUST use the scheme's registered comparator; unknown/unavailable comparators MUST cause deny.

5.3.5 Closed-World Enforcement and Availability

• Evaluation inputs only:
  • The CEP MUST evaluate using only { programBytes/programId, bundled Declarations, builtinsId, channelLatticeId when used, schemesSnapshotId, and the scheme comparator selected by scheme name }. No other registry artifacts may change the decision at enforcement.
• No network I/O in evaluation:
  • Program evaluation and attenuation checks MUST NOT perform network I/O. Required parent Grants MUST be locally available at enforcement (e.g., via cache, pre-enforcement resolver permitted by TAP, or a TAP-defined stapled artifact). If not locally available, the CEP MUST deny.

5.3.6 Fail-Closed Conditions

A CEP MUST deny if any of the following holds:

• Custody/placement failures:
  • issuer(child) != subject(parent), invalid signatures, missing prev linkage, cycle detected, or TAP depth exceeded.
• Pins incompatibility:
• langVersion mismatch; builtinsId mismatch; channelLatticeId mismatch when channelGeq is used by parent or child.
• Unknown or unavailable semantics:
• Program references a builtin not present in builtinsId; Program uses channelGeq but channelLatticeId is missing or unknown; any resource scheme comparator is unknown or unavailable.
• Attenuation violations:
  • Child removes parent Checks; a retained Query in the child omits any parent Literal; child widens literal constants contrary to Builtins tightening rules; Declarations are not subsets of the parent's.
• Local availability:
  • Required parent Grants are not locally available at enforcement (e.g., TAP forbids resolution or resolution failed pre-enforcement).

5.3.7 Informative Examples

• Time window:
  • Parent withinTime(now, 1000, 2000) -> Child withinTime(now, 1200, 1800) (valid).
• TTL:
  • Parent ttlOk(iat, now, 300) -> Child ttlOk(iat, now, 120) (valid).
• Channel floor:
  • Parent channelGeq(channel, "tls-exporter:v1") -> Child channelGeq(channel, "mtls:v1") (valid; equal or stronger only).
• Context:
  • Parent ctxEq("ns","prod") -> Child ctxEq("ns","prod") $\land$ ctxEq("pod","runner-42") (valid).
• Declarations:
  • Parent PairSet = { ("secret:read","vault:.../team/*"), ("secret:derive","vault:.../svcX") }
  • Child PairSet = { ("secret:read","vault:.../team/appA") } (valid subset).

5.3.8 Extensibility

Future Polykey Standard Proposals MAY introduce additional declaration kinds or builtins. Such extensions MUST preserve the core invariants of PSP-1: monotonicity, purity, bounded evaluation and pinned semantics (builtinsId) with chain-wide compatibility. When a new specification introduces a declaration kind (for example, a policy bundle), derived grants MUST ensure that child bundles are subsets of parent bundles under the registry-defined comparator for that kind. Anchoring mechanics and acceptance policies remain TAP-governed; this specification remains agnostic to how anchors are established, and CEPs enforce anchoring only when TAP declares an applicable method for the resource domain.

5.4 Revocation & Rotation

5.4.1 Revocation

• Grants MAY be revoked by their issuer with a signed revocation claim on the issuer's sigchain (format and framing per PSP-3).
• The CEP MUST check revocation state for the leaf Grant and any required parents before enforcement. If any required Grant is revoked, the CEP MUST deny.
• Closed-world rule
  • Revocation checking MUST NOT introduce network I/O during Program evaluation.
  • Required revocation state MUST be locally available at enforcement; how it becomes available (e.g., mirrors, watchers, stapled freshness tokens) is TAP-governed.
  • If revocation state is unavailable or indeterminate per TAP freshness policy, the CEP MUST deny.
• Receipts (PSP-2): Access PoAR and/or ViewReceipts SHOULD record the revocation decision context (e.g., time/source used, revocation snapshot/fingerprint). Exact fields are defined in PSP-2.

If a domain uses an external delegation or revocation registry (e.g., an on-chain registry such as delegate.cash), its outputs MUST be surfaced as attested inputs (e.g., via TAP-approved processes or ctx facts). Builtins MUST remain pure; no network I/O occurs during Program evaluation.

5.4.2 Rotation

• For secret-bound flows and other upstream SoA freshness requirements (e.g., lease rotation), upstream rotation (leases, credentials, keys) is governed by TAP.
• The CEP MUST enforce any time/freshness constraints asserted by the Program (e.g., withinTime, ttlOk) and any TAP-approved environment facts (e.g., leaseStatus) presented at enforcement.
• An Access PoAR MAY include a leaseRef/freshness pointer or similar evidence as defined by PSP-2. PSP-1 does not mandate an on-wire format for rotation artifacts.

5.5 Framing and Canonical Bytes

PSP-1 defines abstract, semantic objects (Program, Declarations) and their canonicalization (PCF). PSP-3 specifies how these appear on the wire (canonical binary encoding, envelope framing, and multihash identity).

• Envelope and bindings: Mappings for issuer, subject, created_at, not_before, not_after, statement_id, prev, and signatures to JOSE/COSE/DSSE are defined in PSP-3. PSP-1 does not mandate field name representations.
• Identity of the Program is derived from canonical bytes defined in PSP-3:
  • programBytes = ENCODE(PCF(Program))
  • programId = multihash(programBytes)
• Normative integrity requirement: Implementations MUST construct PCF(Program) before deriving identity. At verification, the CEP MUST recompute programId from programBytes; any mismatch between the carried programId and the recomputed value MUST cause verification failure.
• Presentations are signed on-wire messages (not stored on sigchains); PSP-3 defines their signature container and field placements. PSP-1 specifies only the semantic components a CEP MUST verify.

5.6 Relationship to Biscuit (Informative)

• Fragment alignment. CPL/0 defines the checks-only, monotone fragment (no user atoms, variables, rules, recursion, or negation). This corresponds to the Biscuit checks fragment without rules, where each check is an OR of queries, and each query is an AND of ground predicates.
• Structural mapping (CPL/0 -> Biscuit):
  • Program (ALL of Checks) $\cong$ a set of Biscuit check blocks, all of which need to pass.
  • Check (ANY of Queries) $\cong$ a Biscuit check containing multiple queries (OR).
  • Query (AND of Literals) $\cong$ a Biscuit query whose predicates match CPL/0 literals 1:1.
  • Literal (Builtin(op, args...)) $\cong$ a ground predicate recognized by the verifier as the corresponding builtin; arguments are ground terms (Str/Int/Bool/Bytes).
• Conversion constraints (Biscuit -> CPL/0 normalizer):
  1. No rules or user facts are consumed during conversion; only checks are considered. If rules, variables, non-ground terms, or unsupported predicates are present, conversion fails (out of scope for CPL/0 interop).
  2. Predicate identifiers should correspond to recognized builtin operations (op strings) in the pinned builtinsId; argument arity and types should match; strings are NFC; Bytes are exact octets.
  3. The resulting CPL/0 Program is constructed as all(check_i); each Biscuit check yields one CPL/0 Check; each Biscuit query yields one CPL/0 Query; each recognized predicate yields one CPL/0 Literal.
• Equivalence goal: For tokens inside this fragment and under identical pinned semantics (builtins/channel lattice/scheme comparators), verification outcomes are expected to coincide between Biscuit's check evaluation and CPL/0 Program evaluation over the same environment facts. Outside this fragment, issuers can precompute finite sets and ship a CPL/0 guard, or use a TAP-gated policy that provides an approved CEP runtime.

Because CPL/0 is checks-only over ground terms with pure, bounded builtins, CEPs evaluate Programs deterministically and can emit minimal proof traces (which check, which query, which literals). This keeps receipts auditable without a general Datalog engine. If richer inference is required in a domain, issuers or attestors can precompute finite sets (content-addressed) and reference them from the Program; alternative extensions that carry ruleful logic should remain TAP-gated with either a compiled CPL/0 guard or an approved CEP runtime.

6. Security Considerations

This section highlights core security principles, common pitfalls, and recommended operational practices. PSP-1's kernel is intentionally small; strong security emerges from a combination of: (a) a deterministic, closed-world verifier (the CEP), (b) canonicalization and pinning, (c) syntactic attenuation across delegation, and (d) TAP-governed acceptance and deployment hygiene.

6.1 Core Invariants

• Holder-of-key + channel binding
  • Presentations MUST be signed by the presenter (PoP) and MUST be bound to the live session; CEPs MUST verify both and deny on mismatch.
• Closed-world evaluation
  • Program evaluation MUST NOT perform network I/O. Required inputs (leaf/parent Grants, revocation state) MUST be locally available at enforcement; otherwise deny.
• Fail-closed
  • Unknown, missing, or ambiguous inputs (unknown builtin, unknown channelLatticeId when channelGeq is used, unknown scheme comparator, ill-typed literal, normalization failure, indeterminate revocation) MUST result in deny.
• Canonicalization and pinning
  • CEPs MUST recompute programId from programBytes and deny on mismatch.
  • Pins affecting semantics (builtinsId, and channelLatticeId when channelGeq is used) MUST match across delegation hops; mismatches MUST deny.
  • Scheme comparators MUST be selected by scheme name and be available locally; otherwise deny.
• Syntactic attenuation
  • Delegation MUST NOT broaden authority. Children MAY add Checks and tighten constants; Declarations MUST be subsets. Equality is permitted unless TAP requires strict attenuation.

6.2 Time, Replay, and Freshness

• Single logical time
  • CEPs MUST capture a single logical now at enforcement start and use it consistently across withinTime, ttlOk, envelope windows, and receipts.
• Presentation lifetimes
  • Presentations MUST be short-lived (iat/exp). CEPs MUST enforce the Presentation window and any Program time constraints. TAP MAY require nonce replay defenses.
• Revocation freshness
  • CEPs MUST check revocation for the leaf and any required parents using locally available state. If unavailable or indeterminate per TAP freshness policy, deny.

6.3 Resource & String Handling

• Resource normalization
  • CEPs MUST normalize env.resource using the same comparator semantics used for declaration canonicalization; normalization failure MUST deny.
• String canonical form
  • Strings MUST be interpreted in NFC; Bytes MUST be exact octets.

6.4 Bounded Evaluation and DoS

• Resource budgets
• CEPs MUST enforce CPU/steps/memory limits for Program evaluation. Exceeding limits MUST result in deny.
• Input bounds
  • Programs and Declarations MUST remain finite. CEPs SHOULD bound sizes of programBytes, declaration tables, and ctx to mitigate memory/CPU pressure.

6.5 Privacy and Minimal Exposure

• Minimal ctx and PII
  • Presentations and Grants SHOULD avoid raw PII; prefer DIDs and contextual claims. CEPs MUST only require ctx keys needed by the Program's ctxEq literals.
• Receipts
  • Access PoARs SHOULD include minimal evaluation traces (e.g., which check/query passed) and program identifiers (programId, declaration CIDs, pins). Detailed evidence, redactions, and selective disclosure are governed by PSP-2 and TAP.

6.6 Delegation & Distribution

• Equality and redistribution
  • PSP-1 permits equality (child == parent). TAP MAY forbid co-equal grants (fan-out) or require strict attenuation. Issuers who wish to prevent redistribution SHOULD include presenterIs(...) in the Program.
• Anchoring
  • Root anchoring for a resource domain is TAP-governed. Where required and unsatisfied, CEPs MUST deny.

6.7 Exposure modes

• Reveal is high-risk. If TAP permits reveal in a domain, it MUST impose strict guardrails: tiny ttl/scope, dual-control, strong audit correlation, and immediate revoke/rotate of exposed material after use. CEPs MUST deny reveal when not authorized by TAP for the placement/mode in use.
• Mediate/derive/reveal are defined outside PSP-1 (CEP/BA placement/mode and Receipt Rails). This note captures only the security stance.
• Receipts (PSP-2) SHOULD record exposureMode and any immediate rotation/revocation references to preserve auditability.

6.8 Registry and Supply-Chain Trust

• builtinsId and (if used) channelLatticeId MUST reference trusted, content-addressed snapshots. Operators SHOULD monitor and pin approved versions via TAP; deny unknown pins.
• Comparator drift
  • Scheme comparator semantics MUST be stable. The schemesSnapshotId pins the exact comparator set; CEPs MUST deny on unknown or mismatched snapshots. For audit acceleration, PoARs SHOULD record the snapshot id and comparator fingerprints actually used by the enforcer.

6.9 Side-Channels and Error Signaling

• Timing behavior
  • CEPs SHOULD aim for consistent-time checks and minimize data-dependent timing variations in hot paths (especially channelBinding and signature checks).
• Error reporting
  • Free-form error messages SHOULD NOT leak sensitive details. PSP-1 does not define receipt formats; if receipts are used, their structure is defined by PSP-2.

6.10 Conformance and Testing

• PCF stability
  • Implementers SHOULD cross-test PCF canonicalization and ensure semantically equivalent Programs yield identical programId across platforms/versions.
• Deny vectors
  • Test unknown builtin/lattice/comparator, programId mismatch, missing declaration bytes, ill-typed literals, normalization failures, pins mismatches, attenuation violations, and parents_unavailable conditions.

7. Backwards Compatibility

PSP-1 defines CPL/0 as the initial language generation. Future specifications MUST NOT alter CPL/0 semantics in ways that change verification outcomes for existing Grants. Breaking changes require a new language generation (e.g., cpl/1) with a distinct langVersion. Deployments integrating legacy systems SHOULD use TAP to gate interoperability or provide compiled CPL/0 guards.

8. Appendices

This section provides compact, implementation-ready annexes that support PSP-1's kernel: a minimal grammar for CPL/0, the builtin operators and their tightening rules, and the requirements for resource scheme comparators. Wire encodings (e.g., CBOR/COSE/JOSE) remain in PSP-3; registry artifacts (builtins snapshots, lattices, comparators) remain in PSP-4.

8.1 Appendix A - CPL/0 Grammar (CDDL)

This Concise Data Definition Language (CDDL) describes the abstract shape of Programs and Declarations. It is not the on-wire format. Deterministic encoding for programBytes is defined in PSP-3.

; Core terms
Term = Str / Int / Bool / Bytes

Str = tstr  ; NFC-normalized at canonicalization/evaluation
Int = int   ; arbitrary-precision integer
Bool = bool
Bytes = bstr

; Program = AND of Checks
Program = {
  checks: [* Check]        ; length >= 0
}

; Check = OR of Queries
Check = {
  queries: [1* Query]
}

; Query = AND of Literals
Query = {
  literals: [1* Literal]
}

; Literal = Builtin(op, args...)
Literal = {
  op: tstr,     ; operator string (op) (e.g., "withinTime", "inPairSet")
  args: [* Term]
}

; Declaration references inside Programs are by content id (string)
; Example literal: { op: "inPairSet", args: [action, resource, "bafy..."] }

; Declarations are finite, canonical datasets carried alongside the Program
DeclarationMap = {
  ; Keys are content ids (strings or PSP-3-defined identifiers); values are canonical bytes
  * tstr => bstr
}

; Builtins used (see Appendix B for semantics and tightening rules):
; - withinTime(now:Int, nbf:Int, exp:Int)
; - ttlOk(iat:Int, now:Int, ttlMax:Int)
; - channelGeq(channel:Str, floor:Str)
; - inPairSet(action:Str, resource:Str, pairsCid:Str)
; - inActionSet(action:Str, actionsCid:Str)
; - inResourceSet(resource:Str, resourcesCid:Str)
; - ctxEq(key:Str, value:Term)
; - presenterIs(did:Str) [optional; if present, in pinned builtins set]
; - enforcerEq(id:Str)   [optional; if present, in pinned builtins set]

Conformance notes:

• Strings are interpreted in NFC. Bytes are exact octets. No floats.
• Programs MUST be monotone; builtins MUST be pure, deterministic, and bounded.
• Canonicalization (PCF) includes sorting/dedup rules (see main text).
• Unknown operators or ill-typed arguments MUST cause deny.

8.2 Appendix B - Builtins and Tightening Rules

This appendix enumerates the builtin operators assumed by PSP-1 and the tightening rules used for syntactic attenuation. The authoritative registry of operators (op strings, types, and semantics) is modeled in PSP-4; Grants pin the exact set via builtinsId.

Builtin operations (what & how). CPL/0 Programs are conjunctions of builtin literals. Each literal is an op string plus arguments (e.g., withinTime(now, nbf, exp) or inPairSet(action, resource, "cid")). Builtins are pure, deterministic, and resource-bounded; they perform no network I/O and return Booleans. A Grant's builtinsId pins a content-addressed snapshot of the builtin catalog. CEPs MUST deny on unknown operators or ill-typed invocations.

Builtin operations summary

op	type signature	returns	semantics (informative shorthand)	tightening (child vs parent)	fail-closed
withinTime	(now:Int, nbf:Int, exp:Int)	Bool	nbf <= now < exp	[nbf_child >= nbf_parent $\land$ exp_child <= exp_parent]	ill-typed => deny; else boolean result
ttlOk	(iat:Int, now:Int, ttlMax:Int)	Bool	now < iat + ttlMax	ttlMax_child <= ttlMax_parent	ill-typed => deny; else boolean result
channelGeq	(channel:Str, floor:Str)	Bool	channel >= floor in the pinned lattice	floor_child >= floor_parent	unknown lattice or channel binding profile => deny
inPairSet	(action:Str, resource:Str, pairsCid:Str)	Bool	(action, resource) $\in$ PairSet(pairsCid) (resource normalized via comparator)	PairSet_child $\subseteq$ PairSet_parent	missing/malformed declaration or comparator failure => deny
inActionSet	(action:Str, actionsCid:Str)	Bool	action $\in$ ActionSet(actionsCid)	ActionSet_child $\subseteq$ ActionSet_parent	missing/malformed declaration => deny
inResourceSet	(resource:Str, resourcesCid:Str)	Bool	$\exists$ selector $\in$ ResourceSet(resourcesCid) such that resource $\subseteq$ selector under comparator	ResourceSet_child $\subseteq$ ResourceSet_parent	comparator or normalization failure => deny
ctxEq	(key:Str, value:Term)	Bool	environment ctx[key] == value	parent constraints preserved; child may add more	missing key or unequal value => false; ill-typed => deny
presenterIs*	(did:Str)	Bool	presenter == did	equality preserved	ill-typed => deny
enforcerEq*	(id:Str)	Bool	enforcer == id	equality preserved	ill-typed => deny

*Optional operators: present only if included by the pinned builtinsId.

• withinTime(now:Int, nbf:Int, exp:Int)
  • Semantics: true iff nbf <= now < exp.
  • Types: all Int.
  • Tightening: child interval $\subseteq$ parent interval (i.e., nbf_child >= nbf_parent and exp_child <= exp_parent).
  • Fail-closed: ill-typed or now outside the half-open interval [nbf, exp) results in false; unknown => deny.
• ttlOk(iat:Int, now:Int, ttlMax:Int)
• Semantics: true iff now < iat + ttlMax.
• Types: all Int.
• Tightening: ttlMax_child <= ttlMax_parent.
• Fail-closed: ill-typed => deny; else boolean result.
• channelGeq(channel:Str, floor:Str)
  • Semantics: true iff channel >= floor in the pinned channel lattice.
  • Types: Str, Str.
  • Tightening: floor_child >= floor_parent (equal or stronger).
  • Fail-closed: unknown lattice or channel/floor not in lattice => deny.
• inPairSet(action:Str, resource:Str, pairsCid:Str)
• Semantics: true iff (action, resource) $\in$ PairSet(pairsCid), after normalizing resource per its scheme comparator. When selectors are used in the PairSet, the scheme comparator defines matching/subset semantics for resource.
• Types: Str, Str, Str.
• Tightening (delegation): PairSet_child $\subseteq$ PairSet_parent under the same normalization/comparator; equality permitted.
• Fail-closed: missing declaration, malformed bytes, unknown comparator, or normalization failure => deny.
• inActionSet(action:Str, actionsCid:Str)
• Semantics: true iff action $\in$ ActionSet(actionsCid).
• Types: Str, Str.
• Tightening: ActionSet_child $\subseteq$ ActionSet_parent; equality permitted.
• Fail-closed: missing/malformed declaration => deny.
• inResourceSet(resource:Str, resourcesCid:Str)
• Semantics: true iff $\exists$ selector $\in$ ResourceSet(resourcesCid) such that resource $\subseteq$ selector under the scheme comparator.
• Types: Str, Str.
• Tightening: ResourceSet_child $\subseteq$ ResourceSet_parent under the same normalization/comparator; equality permitted.
• Fail-closed: unknown comparator, normalization failure, missing/malformed declaration => deny.
• ctxEq(key:Str, value:Term)
  • Semantics: true iff the evaluation environment ctx contains key with equal value (string comparison in NFC; bytewise equality for Bytes; exact equality for Int/Bool).
  • Types: Str, Term.
  • Tightening: parent ctxEq(k,v) MUST be preserved; child MAY add additional ctxEq constraints.
  • Fail-closed: missing key or unequal value => false; ill-typed => deny.
• presenterIs(did:Str) [optional in builtins set]
  • Semantics: true iff presenter DID equals did.
  • Tightening: equality preserved.
  • Fail-closed: ill-typed => deny.
• enforcerEq(id:Str) [optional in builtins set]
  • Semantics: true iff enforcer identifier equals id.
  • Tightening: equality preserved.
  • Fail-closed: ill-typed => deny.

General rules:

• Unknown builtin op referenced by a Program under the pinned builtinsId MUST cause deny.
• Types are enforced at evaluation; ill-typed invocations MUST cause deny.
• Equality of strings uses NFC; comparator logic never performs network I/O.

8.3 Appendix C - Scheme Comparator Requirements

Resource strings are scheme-qualified identifiers (e.g., vault://..., k8s://..., door:..., eth://...). Each scheme MUST define normalization and a decidable subset comparator in PSP-4. CEPs select comparator semantics by scheme name; unknown/unavailable comparators MUST cause deny.

Required properties for every scheme comparator:

• Normalization (deterministic, pure)
  • Strings are NFC-normalized.
  • Percent-decoding and case policy defined (scheme-specific).
  • Path rules defined (dot-segment collapse, single leading slash, trailing slash policy).
  • Authority/host normalization (if applicable) defined.
  • Any scheme-specific canonical forms clearly specified (e.g., chain id formats for eth://).
• Subset comparator (decidable, bounded)
  • Define selector forms (e.g., equality; bounded prefixes/namespaces).
  • Unbounded regex/globs MUST NOT be permitted in v0.1. Any patterning MUST be finite or have a decidable, bounded proof strategy.
  • Comparison MUST be pure and bounded (time/memory).
• Equality/ordering
  • Equality of normalized forms MUST be byte-exact.
• Cross-chain consistency
  • The same comparator semantics MUST apply consistently across delegation hops; mismatch or unavailability => deny.
• Resource normalization at enforcement
  • CEPs MUST normalize env.resource using the same comparator semantics used for declaration canonicalization; normalization failure => deny.
• No network I/O
  • Comparator logic MUST NOT perform network I/O; any external facts MUST be supplied via the evaluation environment (ctx) and governed by TAP.

Illustrative examples of comparator semantics (defined in PSP-4):

• vault://<vaultName>/<path> - path-prefix subset on normalized paths; no unbounded globs; finite "/*" only if comparator defines a safe, decidable interpretation.
• k8s://ns/<namespace>[/...] - namespace containment; normalized identifiers.
• door:<building>:<lock> - equality comparator.
• eth://<chain>/<contract>[/tokenId] - equality on chain/contract; optional tokenId equality; any richer matching MUST be finite and decidable.

9. Examples and Conformance Test Vectors

9.1 Narrative Examples

This section provides end-to-end, program-first examples. Each example includes:

• A human-readable CPL/0 Program (AST form)
• Declarations (PairSet) with illustrative content addresses (CIDs)
• A non-normative Grant payload projection (payload only)
• A non-normative Presentation projection (conceptual fields)
• A concise CEP evaluation trace outline

9.1.1 Example DevOps - Read a secret from Vault

Scenario

• Allow a CI/CD runner to read secrets under vault:secret://org/app/prod/*.
• Constraints (Program literals): mTLS channel, 1-hour window, 120-second Presentation TTL, and ctx must include ns=prod and app=web.

Program (CPL/0, AST)

(all
  (any
    (and
      (inPairSet action resource Pairs#bafyPairsDev1)
      (channelGeq channel "mtls:v1")
      (withinTime now 1768100000 1768103600)
      (ttlOk iat now 120)
      (ctxEq "ns" "prod")
      (ctxEq "app" "web")
    )
  )
)

Declarations (PairSet; canonicalized and content-addressed)

• PairSet (Pairs#bafyPairsDev1)
  • ("secret:read", "vault㊙️//org/app/prod/*")

Pins

• langVersion: "cpl/0"
• builtinsId: "cid:builtins@2025-09-01"
• channelLatticeId: "cid:channel-lattice@v1" (required because channelGeq is used)
• schemesSnapshotId: "cid:schemes@2025-09-01"

Grant (payload only, non-normative)

{
  "programId": "mh:QmProgDev1",
  "programBytes": "<PCF-bytes>",
  "declarations": {
    "pairs:bafyPairsDev1": "<PairSet-bytes>"
  },
  "pins": {
    "langVersion": "cpl/0",
    "builtinsId": "cid:builtins@2025-09-01",
    "channelLatticeId": "cid:channel-lattice@v1",
    "schemesSnapshotId": "cid:schemes@2025-09-01"
  }
}

Presentation (conceptual fields; non-normative)

{
  "presenter": "did:pk:ci-runner-01",
  "grantRef": "cid://G_leaf_devops",
  "iat": 1768100050,
  "exp": 1768100170,
  "jti": "uuid-1234",
  "channelBinding": { "profile": "mtls:v1", "value": "base64url(exporter)" },
  "ctx": { "ns": "prod", "app": "web", "pod": "runner-xyz" }
}

CEP evaluation outline

1. PoP and channel: presenter's signature valid; channelBinding matches mTLS session.
2. Leaf Grant located locally by grantRef; signatures valid; Grant envelope window intersects with Presentation window.
3. Revocation check (local): not revoked.
4. Delegation chain (if present): custody, prev linkage; pins match; scheme comparator for vault:secret is available; child is subset: PairSet_child $\subseteq$ parent; literals tightened/equal.
5. Build env facts; normalize resource (env.resource) per vault comparator; ok.
6. Program evaluation (closed-world):
   • inPairSet(action,resource,Pairs#bafyPairsDev1): true for "secret:read" and "vault㊙️//org/app/prod/kms-key"
   • channelGeq(channel,"mtls:v1"): true under pinned lattice
   • withinTime(now,1768100000,1768103600): true
   • ttlOk(iat,now,120): true
   • ctxEq("ns","prod"), ctxEq("app","web"): true
7. Allow; emit PoAR (PSP-2) with programId, declaration CIDs, pins, minimal evaluation trace, and revocation snapshot context.

Delegated child (illustrative)

• Parent PairSet: ("secret:read","vault㊙️//org/app/prod/*")
• Child PairSet: ("secret:read","vault㊙️//org/app/prod/appA")
• Parent withinTime(..., 1768100000, 1768103600); Child withinTime(..., 1768100500, 1768103300)
• Parent ttlOk(..., 120); Child ttlOk(..., 60)
• Pins equal; attenuation passes (subset + tightened literals).

9.1.2 Example 2: DevOps - Derive a Short Lived DB Token

Scenario

• Goal: Let a CI/CD runner obtain a short-lived, channel-bound database token to access app-prod.
• Pattern: Derive (preferred over reveal). The enforcer (CEP/adapter) mints a 60-120s DB token on allow. No raw secret is exposed.

Program (CPL/0, AST)

(all
  (any
    (and
      (inPairSet action resource Pairs#bafyPairsDbMint1)
      (channelGeq channel "mtls:v1")
      (withinTime now 1768100000 1768103600)
      (ttlOk iat now 120)
      (ctxEq "ns" "prod")
      (ctxEq "app" "web")
      (ctxEq "purpose" "sha256:artifact-H")
    )
  )
)

Declarations (PairSet; canonicalized and content-addressed)

• PairSet (Pairs#bafyPairsDbMint1)
  • ("token:mint", "db://cluster/app-prod")

Pins

• langVersion: "cpl/0"
• builtinsId: "cid:builtins@2025-09-01"
• channelLatticeId: "cid:channel-lattice@v1"
• schemesSnapshotId: "cid:schemes@2025-09-01"

Grant (payload only, non-normative)

{
  "programId": "mh:QmProgDbMint1",
  "programBytes": "<PCF-bytes>",
  "declarations": {
    "pairs:bafyPairsDbMint1": "<PairSet-bytes>"
  },
  "pins": {
    "langVersion": "cpl/0",
    "builtinsId": "cid:builtins@2025-09-01",
    "channelLatticeId": "cid:channel-lattice@v1",
    "schemesSnapshotId": "cid:schemes@2025-09-01"
  }
}

Presentation (conceptual fields; non-normative)

{
  "presenter": "did:pk:ci-runner-prod-01",
  "grantRef": "cid://G_leaf_dbmint",
  "iat": 1768100050,
  "exp": 1768100170,
  "jti": "uuid-9a7b",
  "channelBinding": { "profile": "mtls:v1", "value": "base64url(exporter)" },
  "ctx": { "ns": "prod", "app": "web", "purpose": "sha256:artifact-H", "pod": "runner-xyz" }
}

CEP evaluation outline

1. Verify PoP + channelBinding (mTLS exporter).
2. Load leaf Grant locally by grantRef; verify signatures + envelope; enforce envelope $\land$ presentation time intersection; check revocation (local).
3. If delegated: verify custody, prev linkage; pins compatibility; scheme comparator available; attenuation (program literals equal/tighter; PairSet_child $\subseteq$ parent).
4. Build env; normalize env.resource per "db://" comparator (equality/prefix per PSP-4 rules).
5. Evaluate Program:
   • inPairSet("token:mint","db://cluster/app-prod",Pairs#bafyPairsDbMint1) -> true
   • channelGeq(channel,"mtls:v1") -> true (equal/stronger under lattice)
   • withinTime(now,1768100000,1768103600) -> true
   • ttlOk(iat,now,120) -> true
   • ctxEq("ns","prod"), ctxEq("app","web"), ctxEq("purpose","sha256:artifact-H") -> true
6. Allow. Enforcement (outside PSP-1): Adapter mints a DB token (e.g., 60-120s TTL), channel-bound/session-scoped; returns token to the Subject or mediates the downstream call.
7. Emit PoAR (PSP-2): include programId, declaration CIDs, pins, minimal evaluation trace (which check/query passed), and any derivation metadata (e.g., tokenRef). No raw secret is exposed.

9.1.3 Example 3: Physical Access - Open a door lock

Scenario

• Allow a mobile app to open a specific lock: door:building-12:lock-3.
• Constraints (Program literals): TLS exporter channel, 10-minute window, 60-second Presentation TTL, and ctx must include visitorId = "door-visit-123".

Program (CPL/0, AST)

(all
  (any
    (and
      (inPairSet action resource Pairs#bafyPairsDoor1)
      (channelGeq channel "tls-exporter:v1")
      (withinTime now 1768102000 1768102600)
      (ttlOk iat now 60)
      (ctxEq "visitorId" "door-visit-123")
    )
  )
)

Declarations (PairSet; canonicalized and content-addressed)

• PairSet (Pairs#bafyPairsDoor1)
  • ("access:open", "door:building-12:lock-3")

Pins

• langVersion: "cpl/0"
• builtinsId: "cid:builtins@2025-09-01"
• channelLatticeId: "cid:channel-lattice@v1"
• schemesSnapshotId: "cid:schemes@2025-09-01"

Grant (payload only, non-normative)

{
  "programId": "mh:QmProgDoor1",
  "programBytes": "<PCF-bytes>",
  "declarations": {
    "pairs:bafyPairsDoor1": "<PairSet-bytes>"
  },
  "pins": {
    "langVersion": "cpl/0",
    "builtinsId": "cid:builtins@2025-09-01",
    "channelLatticeId": "cid:channel-lattice@v1",
    "schemesSnapshotId": "cid:schemes@2025-09-01"
  }
}

Presentation (conceptual fields; non-normative)

{
  "presenter": "did:pk:mobile-app-42",
  "grantRef": "cid://G_leaf_door",
  "iat": 1768102050,
  "exp": 1768102100,
  "jti": "uuid-5678",
  "channelBinding": { "profile": "tls-exporter:v1", "value": "base64url(exporter)" },
  "ctx": { "visitorId": "door-visit-123", "device": "ios" }
}

CEP evaluation outline (resource-side CEP, OT-aware)

1. PoP and channel: valid; tls-exporter bound to the session.
2. Leaf Grant found locally; signatures ok; Grant envelope (if present) $\land$ Presentation window ok.
3. Revocation: not revoked.
4. No delegation chain (single-hop) -> no parent checks.
5. Build env facts; normalize resource with door: comparator; ok.
6. Program evaluation:
   • inPairSet("access:open","door:building-12:lock-3",Pairs#bafyPairsDoor1): true
   • channelGeq("tls-exporter:v1","tls-exporter:v1"): true (equal under lattice)
   • withinTime(now,1768102000,1768102600): true (10-minute window)
   • ttlOk(iat,now,60): true
   • ctxEq("visitorId","door-visit-123"): true
7. Allow within tight deadline; emit a PoAR if receipts are used (see PSP-2). If a TAP-imposed deadline is exceeded, deny.

Delegated child (illustrative; equality permitted)

• Parent PairSet: ("access:open","door:building-12:lock-3")
• Child PairSet: ("access:open","door:building-12:lock-3") (equal set)
• Parent ttlOk(..., 60); Child ttlOk(..., 30) (tightened)
• Equality on scope is permitted by PSP-1 (never broaden). TAP MAY require strictly narrower scopes in some domains.

9.2 Conformance Test Vectors

The following vectors exercise PCF stability, syntactic attenuation, time boundaries, and resource normalization. Each vector specifies inputs and the expected decision. Implementations SHOULD include these (or stricter) cases in their conformance suites.

9.2.1 PCF Identity Stability - literal reordering

Setup: Two Programs differ only by literal order within the same Query.

Expect: programId is identical after PCF; evaluation results coincide.

Inputs (sketch):

P1: (all (any (and (ctxEq "ns" "prod") (ttlOk iat now 120))))
P2: (all (any (and (ttlOk iat now 120) (ctxEq "ns" "prod"))))

Expected: multihash(ENCODE(PCF(P1))) == multihash(ENCODE(PCF(P2))); both allow when ctx.ns="prod" and now < iat+120.

9.2.2 Syntactic Attenuation - valid child (tightened)

Setup: Parent Check with Query Q; Child retains the Check, drops no Queries, and adds a Literal; Declarations child $\subseteq$ parent.

Expect: Chain accepted; evaluation allows when both parent and added child literals hold.

Inputs (sketch):

Parent: (all (any (and (inPairSet action resource Pairs#P) (ttlOk iat now 120))))
Child:  (all (any (and (inPairSet action resource Pairs#C) (ttlOk iat now 60) (ctxEq "ns" "prod"))))
Pairs#C $\subseteq$ Pairs#P

Expected: Chain acceptance; allow only if now < iat+60 and ctx.ns="prod".

9.2.3 Syntactic Attenuation - invalid child (removed Check)

Setup: Parent has two Checks (AND); Child omits one parent Check.

Expect: Chain verification MUST fail due to a syntactic attenuation violation.

Inputs (sketch):

Parent: (all ( (any (and (ctxEq "ns" "prod")))  (any (and (channelGeq channel "mtls:v1"))) ))
Child:  (all ( (any (and (ctxEq "ns" "prod"))) )) ; second Check missing

Expected: Deny.

9.2.4 Time Boundaries - half-open edges

Setup: iat=100, exp=200. ttlOk(iat, now, 100).

Expect: Allow for now $\in$ {100,...,199}, deny for now=200 (Presentation window) and now=200 (TTL boundary).

Inputs: now=199 => allow; now=200 => deny.

Expected: At now=200, both now < exp and now < iat+ttlMax fail.

9.2.5 Resource Normalization - percent-encoding equivalence

Setup: Declaration contains api:https://api.example.com/a%2Fb; env.resource is api:https://api.example.com/a/b. Comparator defines canonical normalization collapsing these to the same normalized form.

Expect: After normalization, inPairSet(action, resource, Pairs#X) is true.

Expected: Allow (assuming other literals hold); deny if normalization fails.

9.2.6 Comparator Snapshot Pinning - mismatch across chain

Setup: Parent pins schemesSnapshotId = S1; Child pins schemesSnapshotId = S2 where S2 != S1.

Expect: Deny at chain verification due to a pin mismatch.

10. Implementation Considerations

• Resource-side CEPs (physics-bound)
  • Keep Programs/ctx minimal; pre-normalize resources; precompile program plans; pre-mirror chains/revocation; enforce microsecond/millisecond budgets with deterministic scheduling. If deadlines cannot be met, fail-closed and apply domain-safe fallback per TAP.
• Principal-/Subject-side CEPs
  • Preload and cache Grants and revocation state; amortize verification with sessions (outside PSP-1) and avoid unbounded ctx. Keep long-lived upstream leases only at the Principal side when bridging legacy (PS-BA); Subject-side should handle only session/short-scope credentials (SSA).
• Receipts: "the enforcer mints the proof." Write the PoAR on the enforcer's sigchain (P/R/S per placement) and deliver to the Subject; structure per PSP-2.

11. References

This specification references the following key standards.

• [RFC2119] Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels," BCP 14, March 1997. This Best Current Practice defines how the terms "MUST", "SHALL", "SHOULD", "MAY" and other capitalized keywords are to be interpreted in IETF specifications.
• [RFC8174] Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words," BCP 14, May 2017. This document clarifies that only uppercase usage of the RFC 2119 keywords carries the special meaning.
• [RFC9266] Whited, S., "Channel Bindings for TLS 1.3," July 2022. Defines the tls-exporter channel binding type for TLS 1.3 and updates other RFCs accordingly.
• [RFC9449] Fett, D., Campbell, B., Bradley, J., Lodderstedt, T., Jones, M., Waite, D., "OAuth 2.0 Demonstrating Proof of Possession (DPoP)," September 2023. Describes a mechanism for sender-constraining OAuth 2.0 tokens via a proof-of-possession mechanism that allows detection of replay attacks.

12. Copyright and License

Copyright and related rights for this specification are waived via CC0 1.0.

Note: This applies to the specification text. Reference implementations or example code MAY use a different license as indicated in their respective repositories.

13. Citation

Please cite this document as:

Roger Qiu (@cmcdragonkai), "PSP-1 - Capability Model and Grammar," Polykey Standard Proposals, no. 1, October 2025. [Online serial]. Available: https://polykey.com/docs/reference/specifications/psp-1.