wip

Author: CMCDragonkai

docs/reference/specifications/psp-1.mdx

@@ -1118,6 +1118,8 @@ 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.
@@ -1177,12 +1179,7 @@ A CEP MUST deny if any of the following holds:
 - Required parent Grants are not locally available at enforcement (e.g., TAP
   forbids resolution or resolution failed).
 
-#### 5.2.5 Structure and Informative Projection
-
-Note: The names below are non-normative conceptual labels used by PSP-1. The
-normative on-wire field names and encodings are defined in PSP-3. This list of
-fields and the subsequent JSON example are informative; deployments MAY map to
-alternative encodings but MUST preserve the semantics.
+#### 5.2.5 Illustrative Projection
 
 - **presenter**: DID of the holder (Subject).
 - **grantRef**: canonical digest of the leaf Grant (per PSP-3).
@@ -1205,9 +1202,9 @@ alternative encodings but MUST preserve the semantics.
     proof). PSP-1 core does not define or require such artifacts and forbids
     embedding raw Grant bodies in Presentations.
 
-**Example:** The following JSON projection illustrates one possible mapping of
-the conceptual fields. Names and encodings are illustrative only; the normative
-specification of on-wire fields is defined in PSP-3.
+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.
 
 ```json
 {
@@ -1458,7 +1455,7 @@ binary encoding, envelope framing, and multihash identity).
   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
-    MUST pass.
+    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
@@ -1468,29 +1465,28 @@ binary encoding, envelope framing, and multihash identity).
     (Str/Int/Bool/Bytes).
 - Conversion constraints (Biscuit -> CPL/0 normalizer):
   1. No rules or user facts are consumed during conversion; only checks are
-     considered. Any presence of rules, variables, non-ground terms, or
-     unsupported predicates MUST cause conversion to fail (out of scope for
-     CPL/0 interop).
-  2. All predicate identifiers MUST correspond to recognized builtin operations
-     (`op` strings) in the pinned `builtinsId`; argument arity and types MUST
+     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 (informative): For tokens inside this fragment and under
-  identical pinned semantics (builtins/channel lattice/scheme comparators),
-  verification outcomes SHOULD coincide between Biscuit's check evaluation and
-  CPL/0 Program evaluation over the same environment facts. Outside this
-  fragment, issuers SHOULD precompute finite sets and ship a CPL/0 guard, or use
-  a TAP-gated policy that provides an approved CEP runtime.
+- 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 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 SHOULD precompute finite sets (content-addressed) and reference them
-from the Program; alternative extensions that carry ruleful logic MUST remain
-TAP-gated and provide either a compiled CPL/0 guard or an approved CEP runtime.
+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
 
@@ -2230,59 +2226,19 @@ Expect: Deny at chain verification due to a pin mismatch.
 
 ## 10. Implementation Considerations
 
-### 10.1 Placement and operational considerations
-
-### 10.2 Placement-Specific Guidance
-
 - 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
+- Principal-/Subject-side CEPs
   - Preload and cache Grants and revocation state; amortize verification with
-    sessions (outside PSP-1) and avoid unbounded ctx.
-
-### 10.3 Example implementation notes
-
-- PSP-1 does not mandate exact Presentation field names or encodings; those
-  appear in PSP-3. The CEP's obligations here are limited to PoP verification,
-  channel binding verification, custody/attenuation verification, and Program
-  evaluation under the pinned semantics and bundled declarations.
-- Per-use narrowing is achieved by the Program's literals (e.g., ctxEq, ttlOk)
-  evaluated against Presentation-supplied ctx and iat/exp. TAP policy MAY
-  introduce presentation overlays with strict attenuation and receipt
-  requirements.
-
-- db:// scheme: register a PSP-4 comparator (normalization + subset semantics).
-  Often equality on cluster/app, or bounded prefix if you expose sub-scopes.
-- If the Resource is PK-native, use Resource-side CEP; otherwise bridge at
-  Principal-side (as shown).
-- Presentations remain small; do not embed Grant bodies in PSP-1 core. If
-  parents aren't local at enforcement, deny (TAP defines pre-enforcement
-  hydration or stapling chain proof).
-- Receipts: PoAR should capture enough to audit the decision (`programId`,
-  declaration CIDs, pins, minimal trace), plus derivation metadata (tokenRef),
-  but never the token itself.
-
-- Resource normalization: ensure env.resource is normalized using the scheme
-  comparator (vault:, door:) that was used to canonicalize Declarations;
-  failures must deny.
-- Pins must match across delegation hops: `langVersion`, `builtinsId`, and, when
-  used, `channelLatticeId`. Mismatches deny.
-- Presentations remain small and referential; do not embed Grant bodies in PSP-1
-  core. If parents are required and not locally available at enforcement, deny
-  (TAP governs pre-enforcement hydration or profile-level stapling).
-- Receipts (PSP-2): PoARs SHOULD record `programId`, declaration CIDs, pins,
-  minimal evaluation trace, and revocation/freshness context; redactions and
-  selective disclosure are TAP/PSP-2 concerns.
-
-### 10.4 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.
+    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