wip(psp-1)

Author: CMCDragonkai

docs/reference/specifications/psp-1-new.mdx

@@ -350,7 +350,7 @@ Registry pinning details are defined in
 - 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).
+    in [Section 4.4, \_Semantic Pinning](#44-semantic-pinning)).
   - Terms are ground: Str | Int | Bool | Bytes. No variables. No user-defined
     atoms.
   - Int is arbitrary-precision. Floats are not permitted.
@@ -367,16 +367,20 @@ Registry pinning details are defined in
 - 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; PSP-4).
+    ([Section 4.4, \_Semantic Pinning](#44-semantic-pinning); PSP-4).
   - Channel-related literals (e.g., `channelGeq`) interpret identifiers using
-    the pinned channel lattice (`channelLatticeId`) (Section 4.4).
+    the pinned channel lattice (`channelLatticeId`)
+    ([Section 4.4, \_Semantic Pinning](#44-semantic-pinning)).
   - Declaration-aware literals (`inPairSet`, `inActionSet`, `inResourceSet`)
-    rely on scheme comparators selected by resource scheme name (Section 4.4).
+    rely on scheme comparators selected by resource scheme name
+    ([Section 4.4, \_Semantic Pinning](#44-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 for the time model).
+    used consistently (see
+    [Section 4.7, _Time Model and Boundaries_](#47-time-model-and-boundaries)
+    for the time model).
 
 ### 4.2 Evaluation Environment
 
@@ -1121,24 +1125,15 @@ Grants and transient proof-of-use.
     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_](#47-time-model-and-boundaries).
-
-  - Effective lifetime: The CEP MUST enforce the intersection of all applicable
-    time windows at the captured `now`. Specifically, the Presentation window
-    `[iat, exp)`, any Grant envelope validity window (`not_before`/`not_after`
-    per PSP-3), and any Program time literals such as `ttlOk` or `withinTime`
-    MUST all succeed. If any one of these constraints fails at `now`,
-    enforcement MUST deny.
   - 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.

docs/reference/specifications/psp-1.mdx

@@ -230,9 +230,8 @@ What PSP-1 defines:
 
 ### 3.3 Threat Model Pointers
 
-PSP-1 addresses a set of well-understood threat vectors. This subsection
-highlights those scenarios and points to TAP for policy controls and
-mitigations.
+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
@@ -283,7 +282,7 @@ Comparators) appear in PSP-4.
 
 ### 4.1 Language Model
 
-This subsection defines the capability language evaluated by CEPs. It specifies
+This section defines the capability language evaluated by CEPs. It specifies
 abstract structure and semantics only. Builtins, channel lattices, and scheme
 comparators are referenced via registry pins (see Semantic Pinning for
 Deterministic Evaluation and PSP-4).