wip: almost onto Grants now

Author: CMCDragonkai

docs/reference/specifications/PSP-1 - Capability Model and Grammar.mdx

@@ -89,17 +89,18 @@ Capability evaluation depends on small, versioned rulebooks ("registries"):
 - Resource Schemes: normalization and subset comparators per scheme.
 - Channel Lattices: partial order used by channel_geq.
 - Builtins: the available operations (opcodes), their types, and tightening rules.
+- PSP-4 MAY also define domain verb/resource registries (e.g., energy verbs; asset:/bacnet:/ocpp: schemes) and TAP-referenced trust registries (e.g., notary key lists, DKIM selector archives, origin key policies). CEPs do not consume these artifacts directly; if used, their outputs appear as environment facts and are asserted in Programs (e.g., via ctx_eq).
 
 A registry ID is a content-addressed identifier (e.g., a CID/multihash) for a specific, immutable entry or snapshot in one of these registries.
 
 ### Definitions
 
-Channel lattice and channel_lattice_id
+Channel `lattice` and `channel_lattice_id`:
 
 - A channel lattice defines a partial order over channel profiles (e.g., mtls:v1 ≥ tls_exporter:v1 ≥ dpop:v1 ≥ bearer:v1). It is the rulebook used by the builtin channel_geq(channel, floor).
 - channel_lattice_id is the content-addressed ID of the specific lattice used to interpret "≥". It is required whenever a Program uses channel_geq.
 
-Builtins and builtins_id
+Builtins and `builtins_id`:
 
 - The builtins registry defines each opcode's semantics, types, and attenuation tightening rules (e.g., within_time, ttl_ok, in_pairset, channel_geq, ctx_eq, presenter_is).
 - builtins_id is the content-addressed ID of the exact builtin set the Program uses.
@@ -108,7 +109,7 @@ Resource schemes:
 
 - Each resource scheme (vault:, net:, k8s:, …) has a registry entry that defines normalization and a decidable subset comparator. In PSP-1, comparators are selected by scheme name; no per-scheme ID is pinned.
 
-Verbs
+Verbs:
 
 - Verbs are namespaced strings (e.g., secret:read). Evaluation treats them as strings for equality. TAP may govern allowlists; PSP-1 does not require pinning a verbs set.
 
@@ -196,23 +197,26 @@ At verification, the CEP supplies an environment of facts. Builtins may referenc
   - enforcer: Str — DID/identifier of the enforcing CEP (audience).
   - channel: Str — profile representing the live session's binding.
   - ctx: `Map<Str, Term>` - runtime context (e.g., `{"ns":"prod","pod":"runner-42"}`).
-- Optional environment facts (TAP‑gated)
+- Optional environment facts (TAP-gated)
   - lease_status - opaque assurance/freshness input for lease checks (no I/O in the builtin).
+  - 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., ctx_eq).
 - Missing facts (normative)
   - If a builtin present in the Program requires an environment fact that is missing, evaluation MUST fail closed.
 
-#### Bultins and registries
+#### Builtins and registries
 
 - Each builtin op_id, its type signature, and its tightening rule are defined in the Builtins registry (PSP-4). The exact set in use is pinned by builtins_id in the Grant.
 - Channel comparisons (e.g., channel_geq) consult a pinned channel_lattice_id when present.
 - Resource subset checks in declaration-aware builtins (e.g., in_pairset) consult the scheme comparator selected by the resource's scheme name.
 - If a builtin, lattice, or comparator required by the Program is unknown or unavailable, evaluation MUST fail closed.
+- Programs may constrain the live session's profile using `channel_geq(channel, "…")` as defined by the pinned channel lattice. Programs may also assert runtime or provenance context via equality over environment facts (e.g., ctx_eq("k","v")). How those environment facts are obtained or validated — including the presentation binding to a live session - is outside the CPL/0 language and governed by TAP and PSP-2.
 
 #### Typing, totality and failure modes
 
 - Builtins MUST validate argument types at evaluation time. Ill-typed invocations MUST fail closed.
 - Strings MUST be considered in NFC for comparison purposes; Bytes are compared as exact octets.
 - Evaluation MUST be performed under CEP-enforced limits (CPU/steps/memory). Exceeding limits MUST result in deny.
+- The `now: Int` fact is CEP-provided and subject to TAP time-discipline; PSP-1 is agnostic to the time source.
 
 #### Relationship with Biscuit Datalog (Informative)
 
@@ -225,9 +229,147 @@ At verification, the CEP supplies an environment of facts. Builtins may referenc
 
 ### 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.
+
+#### PairSet
+
+- Definition: PairSet is a finite set of (action: Str, resource: Str) pairs.
+- Purpose: express an allowlist of "what actions on which resources" a capability can authorize.
+- 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.
+
+#### 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
+  - in_actionset(action, Actions#CID) evaluates to true if and only if action ∈ ActionSet(CID).
+- Attenuation
+  - For a derived Grant, the child ActionSet MUST be a subset of the parent ActionSet.
+
+#### 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
+  - in_resourceset(resource, Resources#CID) evaluates to true if and only if there exists r_sel ∈ ResourceSet(CID) with resource ⊆ 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.
+
+#### Program Use
+
+- Declarations are data sources invoked via builtins; Programs combine these with other literals (within_time, ttl_ok, channel_geq, ctx_eq, presenter_is).
+- Actions appear as strings; resources are scheme-qualified strings; subset relations are defined per scheme in the registry (no unbounded regex/globs; selectors MUST be finite or safely bounded with a decidable comparator).
+- Unknown declaration kinds, schemes, or comparators MUST cause deny.
+
+#### Attenuation over Declarations
+
+- Delegation MUST NOT broaden Declarations.
+  - PairSet_child ⊆ PairSet_parent.
+  - ActionSet_child ⊆ ActionSet_parent.
+  - ResourceSet_child ⊆ 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.
+
+#### Profiles
+
+- This specification standardizes exactly three Declaration kinds: PairSet, ActionSet, ResourceSet. Profiles MAY further constrain their usage (e.g., disallow ResourceSet for certain verbs) or prescribe default comparators per scheme. A CEP MUST deny if a Program references a declaration kind not supported by the active profile or if a required comparator is not available.
+
 ### Program Canonical Format (PCF) & Digest
 
-### Verbs & Resources
+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).
+
+#### 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.
+
+#### Normalization rules
+
+- Literals within a Query MUST be sorted by a total order over:
+  - literal kind (e.g., Builtin before Atom if Atoms are present),
+  - 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.
+
+#### 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.
+
+#### Prohibited/non-canonical forms
+
+- Floating-point numbers MUST NOT appear in Programs.
+- Indefinite-length encodings and non-normalized strings MUST NOT appear in canonical bytes (see PSP-3 for encoding constraints).
+- Any literal or term introducing non-determinism or network I/O MUST NOT be part of a Program.
+
+#### Deterministic encoding and identity
+
+- program_bytes = ENCODE(PCF(Program)) as specified by PSP-3.
+- program_id = multihash(program_bytes) as specified by PSP-3.
+- A Grant carrying program_bytes and program_id MUST be rejected if recomputation does not match.
+
+#### 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 their presence prevents deterministic term encodings, identity derivation MUST fail.
+
+#### 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 program_bytes and program_id across platforms and versions.
+
+#### Informative guidance
+
+Keep operator identifiers stable and registry-pinned to avoid PCF instability from renaming.
+When referencing Declarations by content address (e.g., “Pairs#CID”), ensure the reference syntax and encoding are deterministic and consistent.
+
+### Verbs & Resources (Reader Guidance)
+
+Verbs are namespaced strings (e.g., “secret:read”, “deploy:to_env”, “energy:curtail”). They appear as the action fact and as elements inside Declarations (PairSet/ActionSet). Verb semantics MUST be documented in a registry with versioned definitions. Registry entries SHOULD declare expected resource scheme(s) and any required constraints (e.g., time window, channel profile, mediated surface references). A CEP MUST deny if a required constraint is not asserted by the Program. TAP MAY whitelist verbs per domain; unknown verbs default to non‑permitted unless TAP specifies otherwise.
+
+Resources are scheme‑qualified identifiers (URI‑like) that denote targets (e.g., “vault:secret://org/team/key”, “k8s://ns/prod”, “asset:building‑12:rtu‑3”, “api:https://vendor.com/path”). They appear as the resource fact and as elements inside Declarations (PairSet/ResourceSet). Each resource scheme MUST have a registry entry defining normalization and a decidable subset comparator. Grants SHOULD use specific resources. If a scheme permits selectors, their use MUST be finite or safely bounded with a defined subset proof. Unknown schemes or unavailable comparators MUST cause deny. TAP MAY restrict acceptable schemes or forms per domain and verb.
+
+Delegation subset: For derived Grants, resource.child MUST be a subset of resource.parent under the scheme’s comparator; for Declarations, child sets MUST be subsets of parent sets.
+
+Programs consult finite allowlists via Declarations and evaluate constraints using builtins. Verb and scheme registries define documentation and comparators; unknowns fail closed.
+
+---
+
+## Grants
+
+## Presentations
+
+## Delegation && Attenuation
+
+## Verification Algorithm
+
+## Security Considerations
+
+
+
 
 
 

docs/reference/specifications/PSP-4 - Registries.mdx

@@ -0,0 +1 @@
+# PSP-4 - Registries

docs/reference/specifications/PSP-5 - Attestations.mdx

@@ -0,0 +1 @@
+# PSP-5 - Attestations

docs/reference/specifications/PSP-6 - TAP and RAM.mdx

@@ -0,0 +1 @@
+# PSP-6 - TAP and RAM

docs/reference/specifications/PSP-6 - TAP.mdx

@@ -0,0 +1 @@
+# PSP-7 - CEP and Bridge Adapter Profiles