PSP1 Review via GPT-5 Pro, Grok 4, Gemini 2.5 Pro, Claude Sonnet 4.5 - Semantics, Syntax and Structure

[CMCDragonkai]

Description

PSP-1 draft was created in #160, and we actually got an initial GPT5-pro review. This GPT5-pro review was a "failure-seeking" review.

Below is a failure‑seeking review of PSP‑1 with concrete edits. I’ve grouped feedback into: (A) critical inconsistencies and correctness bugs, (B) structural/style changes to make this feel like an RFC/EIP/BIP‑grade spec, (C) oversights and attack surfaces you haven’t addressed, and (D) a clean, regularized ToC plus redlines you can drop in.

Overall it was about making sure our spec does what it says it will do and ensure that CEPs will all behave the same and eliminating any ambiguity. No significant semantic changes was in it.

The GPT5-pro review was then passed to 3 separate AI agents each providing their synthesis on the required changes.

• claude-1.md
• gemini25-1.md
• grok4-1.md

This was brought back into GPT5-pro in order to further clean up with iterative diffs.

Synthesis of the cross review was done.

Details

V = 4

Below is a synthesis of the three external assessments of the failure‑seeking review you ran on PSP‑1. I start with the consensus picture, then the differences and why they diverge, and finally a Bayesian scoring of options with concrete, semantic‑first recommendations. Inline I point to each model’s write‑ups.

---

1) High‑level alignment (what all three agreed on)

All three reviewers independently converged on the same semantic hardening moves. In short:

• Eliminate Atoms/Symbols/Variables; Builtins‑only + ground terms. This removes internal contradictions and stabilizes PCF and evaluation semantics.

• Standardize time boundaries and precedence. Use a single captured now; make windows half‑open [start, end); define exp ∧ ttl_ok as an intersection (both must pass).

• Make attenuation mechanically checkable (purely syntactic). Child must keep all parent checks (by PCF identity); may drop queries (narrows OR); any retained query’s literals are a superset; literal constants may only tighten per builtin rules.

• Pin semantics to kill drift. Beyond builtins_id and (when used) channel_lattice_id, add a schemes_snapshot_id (or equivalent) so resource comparator semantics are content‑addressed and chain‑stable.

• Scope boundaries across PSP‑1/‑2/‑3. Keep PSP‑1 abstract/semantic; move wire encodings and receipt fields to PSP‑3 and PSP‑2 respectively; make the doc read like an RFC (clean ToC; fewer “(normative)” markers).

• Channel‑binding profiles & lattice. Name the exact profiles (e.g., TLS exporter, DPoP), cite standards, and put the partial order in the pinned lattice snapshot.

• Environment normalization timing. Normalize resource under the same comparator semantics before evaluation; fail‑closed on any normalization failure.

Implication: The above are semantic changes: they alter the meaning of evaluation, the outcome at edges, or the trust/determinism envelope—not just editorial polish.

---

2) Where they differ (and why)

Topic	Claude	Gemini	Grok	Why they diverged / trade‑off
Comparator pinning form	Proposes two options: (A) require schemes_snapshot_id (recommended) or (B) record comparator fingerprints in PoAR only.	Treats schemes_snapshot_id as REQUIRED in pins.	Integrates schemes_snapshot_id into pins and chain compatibility; leans mandatory.	Claude leaves an audit‑only path (lower friction, weaker determinism). Gemini/Grok optimize for determinism and replayability even if governance overhead rises.
Rollout strategy	Iterative plan in 4–5 passes (core semantics → pinning → structure → tests → polish).	Presents high‑level diffs and structure, less on phasing.	Similar to Gemini: high‑level diff with concrete section moves.	Difference is procedural, not semantic. Claude optimizes for change management risk.
How prescriptive to be in PSP‑1 vs PSP‑2/‑3	Strong push to purge receipt/transport from PSP‑1; leave only pointers.	Same, plus explicit references to RFCs for encodings in PSP‑3.	Same; provides a concrete RFC‑style ToC.	All agree on separation; Grok/Gemini add more editorial specificity (ToC) while Claude focuses on boundary hygiene.
Emphasis on test vectors	Strong emphasis: PCF stability, attenuation valid/invalid, time edges, normalization traps.	Same.	Same, with ToC slot for interop.	No real divergence—only where to house them and sequencing.

---

5) Deep‑dive on the top semantic deltas

5.1 Comparator semantics pinning

• Agreement: All three argue for pinning comparator semantics; divergence is whether to also accept an audit‑only path (PoAR fingerprints) when operators resist governance friction.

• Why it matters: Without pinning, two CEPs may reach different decisions as comparators evolve—non‑replayable security.

• Call: In PSP‑1 core, require schemes_snapshot_id across a delegation chain; allow PoAR fingerprints as additional evidence, not a substitute. (Posterior ≈ 0.85–0.90 in favor of mandatory pinning.)

5.2 Time semantics & precedence

• Agreement: Single captured now; half‑open windows; both envelope [iat, exp) and ttl_ok must pass.

• Why it matters: Prevents edge‑case discrepancies (e.g., off‑by‑one at expiry).

• Call: Adopt spec‑wide half‑open semantics; rewrite within_time and the CEP algorithm accordingly. (Posterior ≈ 0.92.)

5.3 Syntactic attenuation

• Agreement: Make attenuation mechanical, eliminating “controls authority” subjectivity.

• Why it matters: Verifiers must decide with no judgment calls; delegation proofs become predictable.

• Call: Replace the prose with the precise rules; update chain checks accordingly. (Posterior ≈ 0.95.)

5.4 Channel binding profiles & lattice

• Agreement: Name profiles (e.g., tls-exporter:v1, dpop:v1, mtls:v1, bearer:v1), cite the underlying RFCs, and pin the lattice snapshot used for >=.

• Why it matters: Avoids accidental weakening via ambiguous profile strings; supports deterministic evaluation of channel_geq.

• Call: Treat these as registry artifacts subject to the same pinning discipline as builtins.

5.5 Environment normalization

• Agreement: The CEP must normalize resource under the same comparator semantics as declaration canonicalization before evaluation; failure is deny.

• Why it matters: Prevents “different normalization at input vs declaration” bugs.

• Call: Promote this to a single normative rule in “Evaluation Environment.”

---

6) Concrete edit outcomes (semantic first, then structure)

1. Pins: Add schemes_snapshot_id to Grant.pins; require equality across delegation hops; update fail‑closed list to include unknown/mismatched snapshot; keep PoAR comparator fingerprints as additional audit material.

2. Time model: Add a short section “Time Model & Boundaries”; redefine within_time(now, nbf, exp) as nbf ≤ now < exp; in CEP algorithm use now ∈ [iat, exp) ∧ ttl_ok.

3. Attenuation: Replace the ambiguous rule with the check/query/literal tightening rules; update delegation verification to require exact PCF identity for checks retained.

4. Language model: Remove all mentions of Atoms/Symbols/Variables; keep Builtins‑only literals; update Appendix A grammar and PCF sorting (no “Atom” kind).

5. Channel binding: Add a registry subsection for profile identifiers and pin their lattice via channel_lattice_id; cite profiles where they’re standardized; treat unknown profile in lattice as deny.

6. Normalization rule: In “Evaluation Environment,” require normalization of resource prior to any builtin evaluation; failure denies.

7. Structure: Move all on‑wire encodings to PSP‑3 and all receipt fields/reason codes to PSP‑2; adopt the RFC‑like ToC; add a Test Vectors & Interop section.

---

7) Final recommendations (ordered by semantic criticality)

1. Adopt mandatory comparator pinning (schemes_snapshot_id) in PSP‑1; allow PoAR fingerprints only as supplemental audit. (Posterior: ~0.88)

2. Lock the time model to half‑open windows and explicit exp ∧ ttl_ok intersection; rewrite builtin + algorithm text accordingly. (~0.92)

3. Replace attenuation prose with the syntactic rules; require PCF identity for parent checks; allow query dropping; enforce literal‑constant tightening per builtin rules. (~0.95)

4. Purge Atoms/Vars entirely; Builtins‑only. (~0.93)

5. Define and pin the channel‑profile lattice; treat unknown profile or lattice mismatch as deny. (~0.88)

6. Normative normalization rule for resource, pre‑eval; deny on failure. (~0.90)

7. Restructure PSP‑1 (ToC, boundaries, tests). (~0.90)

---

Notes on your stated concern (“semantic” over “syntactic”)

Every recommendation above in §5/§7 materially changes evaluation outcomes or replayability (determinism), i.e., they are semantic. The purely syntactic/editorial suggestions (ToC, moving sections, naming consistency) are useful but subordinated here; they won’t make or break enforcement outcomes.

---

If you want, I can transform these into precise diff blocks for PSP‑1 (one pass per semantic item), starting with time semantics and attenuation (the two lowest‑risk, highest‑impact edits).

Tasks

• 1. GPT5-pro high level review
• 2. Cross Review by 3 additional agents
• 3. Diff applied changes from the synthesized cross review
• 4. Check that changes abide by the original cross review
• 5. Complete syntactic and spinal changes

Prototype implementation will be the stage after review. We will need to figure out the right governance process for the specifications. I suspect PSP1,2,3,4 will all be in "review" to while prototype implementation is achieved.

Final checklist

• Domain specific tests
• Full tests
• Updated inline-comment documentation
• Lint fixed
• Squash and rebased
• Sanity check the final build

[CMCDragonkai]

Initial set of changes done in 3b0fc51

• Removes the Atom/Sym/Var contradiction in the current Terminology and introduces the official name for TAP to avoid "profile" overload later.
• PCF must not refer to literal kinds that the language forbids; we keep the ordering rules purely over builtin operator id and arguments.
• Without pinning, comparator evolution can change allow/deny decisions over time. We make the snapshot mandatory and chain-stable; this is the single biggest determinism hardener.
• The spec mentions normalization in multiple places; this consolidates a single, normative rule where evaluators look first. (The "Grants -> Determinism and normalization invariants" bullet remains consistent.)
• Edge-consistent timing: half-open [iat,exp) is already used in the algorithm; this makes precedence explicit so independent CEPs agree on acceptance at the boundary.
• Aligns all time semantics to half-open windows, preventing "double-counting the endpoint" and making ttl_ok consistent with the Presentation lifetime check.
• Replaces "controls authority" (subjective) with a mechanical, verifier-checkable rule. This is the cornerstone of safe delegation.
• Keeps comparator fingerprints as additional evidence even with mandatory pinning; also makes snapshot equality a first-class chain condition.
• Eliminates ambiguity about where profile strings come from, and ties their interpretation to the pinned lattice snapshot.
• Aligns terminology with "Threat and Acceptance Policy"; avoids overloading "profile" in TAP contexts while preserving the separate concept of PSP-level "Profiles" elsewhere in the doc.
• Makes the same syntactic rule explicit in both delegation sections to avoid reader confusion and implementation drift.
• Codifies your note about keeping PoAR fingerprints for fast replay/audit while keeping snapshot pinning as the source of truth.
• Disambiguates "Profiles" here as specification profiles, so it doesn't collide with the TAP policy concept.

[CMCDragonkai]

Additional changes are getting more syntactic and clarifying material as well spine changes and reference material.

Cross review 2 to assess whether initial cross reviews were correct.

• claude-2.md
• gemini25-2.md
• grok4-2.md

[CMCDragonkai]

It's expected that sometimes with multiagent interactions that there maybe an interaction rollback to fork from another point in the conversation.

[CMCDragonkai]

Using agent mode is pretty useful as way to do long form turn by turn editing, it does however make mistakes, and it would easier if I could HITL update the text from the system it's operating on. I think I need embedded agent mode directly on my workstation to reduce latency of feedback.

[CMCDragonkai]

In the most recent update, we removed a few things.

1. Attenuation by Derivation
2. Appendix D - Suggested Reason Codes

This was suggested through restructuring and eliminating duplicate information. However I don't think all "references" are updated. In particular Appendix D by being removed, there are some times still references to reason codes. That should be updated accordingly. I also need another check done on the Attenuation by Derivation to see if the restructuring is concise without repetitive information and we're not missing anything.

[CMCDragonkai]

Alright we're reaching the finish line of this review. By which we will move on to prototype implementation and/or PSP-2,3 and so on. Probably updating some of the market loop documents to explain this spec.

The final changes seem to be small. Things like langVersion should just always be cpl/0. There still feels like there's some duplication of information that can be tightened up.

There's a bunch of "notes" that make the spec not super tight. They provide some interesting information that's probably not easy to understand without everything else being understood.

I realise that some of the names of receipts like PoAR and DenyReceipt seems a big a strange. Maybe we need a ActionReceipt and DenyReceipt and UseReceipt? Rather than PoAR. The PoAR is a bit long and legacy.

---

1) Unify decision/receipts + remove duplication/reason‑codes

Intent: PSP‑1 should only (a) require the enforcing CEP to record a decision event, and (b) say that if PSP‑2 receipts are implemented, emit the appropriate receipt. PSP‑1 must not define what a DenyReceipt/PoAR contains or require reason codes—that belongs to PSP‑2.

A. Replace §13.2 “Step 8” with a single authoritative rule

Find the block beginning with:

8. Decision and receipts (placement-agnostic)
  - On success:
    - Allow enforcement …
    - The enforcing CEP MUST record …
    - emit an Access PoAR …
    - PoARs MUST include programId … comparator fingerprints …
  - On failure:
  - The enforcing CEP MUST record …
    a DenyReceipt. DenyReceipts MUST include …

Replace it with:

8. Decision recording (placement-agnostic)

- 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.

B. Trim §13.2 “Step 7” (no receipt talk)

Find in Step 7:

Enforce resource bounds (CPU/steps/memory). Exceeding limits MUST result in deny. (The enforcing CEP SHOULD … receipts/reason code …)

Replace with:

Enforce resource bounds (CPU/steps/memory). Exceeding limits MUST result in deny.

C. Clean §13.3 “Execution Constraints” (no receipt talk)

Find the bullets under “Deadlines and budgets”:

… MUST abort and deny when the deadline is reached. The enforcing CEP SHOULD log an appropriate reason code … PSP‑2 …

Replace with:

… MUST abort and deny when the deadline is reached.

D. Clean §14.4 “Bounded Evaluation and DoS”

Find:

limits MUST result in deny. The enforcing CEP SHOULD log an appropriate reason code … PSP‑2 …

Replace with:

limits MUST result in deny.

E. Clean §14.9 “Side‑Channels and Error Signaling”

Find the “Error reporting” bullet that mentions “machine‑readable denial reason” (or any receipt content).

Replace the whole error‑reporting bullet with:

- Error reporting
  - Avoid leaking sensitive details in free‑form error messages. PSP‑1 does not define receipt formats; if receipts are used, their structure is defined by PSP‑2.

F. Remove any remaining references to “reason code(s)”

Search for reason code, reason codes, or “machine‑readable denial reason” and delete those phrases/sentences. (They’re no longer mentioned in PSP‑1 after the changes above.)

---

2) Lease freshness: placement + naming

You’re right: putting lease freshness under “12.2 Rotation” was the wrong place, and lease_status + “surfaced” was sloppy. This belongs in the verification algorithm (closed‑world, TAP‑governed), and any environment fact should use lower‑camel.

A. Rename the optional env fact in §4.5

Find under “Optional environment facts (TAP‑gated)”:

- lease_status - opaque assurance/freshness input for lease checks (no I/O in the builtin).

Replace with:

- leaseStatus — optional TAP‑provided evidence used to assess upstream lease/credential freshness. Semantics are TAP‑defined; no network I/O occurs during evaluation.

B. Fix the env list in §13.2 Step 5

Find in “5. Build evaluation environment (facts)”:

- Optional TAP-approved freshness facts (e.g., lease_status), if present

Replace with:

- Optional TAP-approved freshness facts (e.g., leaseStatus), if present

C. Move the normative lease‑freshness check into the algorithm; remove it from §12.2

Delete the lease‑freshness paragraph that was added under §12.2 Rotation (the one referencing non‑native SoA, local evidence, and lease_status).

Add the following bullet under §13.2 Step 3 (Resolve and verify the leaf Grant (local)), immediately after the revocation bullet:

- Lease freshness (when applicable): 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.

This keeps the check in the closed‑world, TAP‑governed algorithm where it belongs, avoids format creep, and uses lower‑camel consistently.

---

3) Remove the “buildChain” implementation note; fold the substance into §11.3

You’re right: introducing a buildChain helper that isn’t defined elsewhere is distracting. The spec already says “simple path leaf→root; reject cycles; max depth via TAP”. Let’s delete the note and make the normative bullets explicit.

A. Delete the entire “Implementation note (Informative): chain assembly” under §11.3.

B. Ensure the normative bullets in §11.3 explicitly cover the same ground:

If not already explicit, augment §11.3 as follows (these are short normative refinements, not a new helper):

- prev linkage MUST form a simple path from leaf to root; the CEP MUST deny if any digest repeats (cycle detection).
- All required parent Grants MUST be locally available at enforcement; otherwise the CEP MUST deny. (Pre‑enforcement acquisition is TAP‑governed.)

(You already state depth caps and anchors; these two bullets make availability + cycles unmistakable without adding a pseudo‑API.)

---

4) What I did not change (because it’s outside PSP‑1’s scope)

• No references to DenyReceipt contents or reason codes remain; those are PSP‑2’s job.
• No new helper semantics are introduced (no buildChain function, no receipt fields).
• Rotation (§12.2) remains TAP‑governed and receipt‑agnostic.

---

Sanity check (net effect)

• One source of truth for decision/receipt behavior lives in §13.2 Step 8.
• No normative recursion into PSP‑2 fields/reason codes.
• Lease freshness is evaluated where it belongs (the algorithm), and the env fact name is consistent (leaseStatus).
• Cycle detection & parent availability are crisp, normative bullets; no undefined helpers.

If you’re aligned with this, I can produce a consolidated patch file that applies these edits in one shot.

---

I think also that the lease_status and stuff is unclear to me how it works. After all PSP-1... should it even engage in details of lease rotation, it was said it should be in the TAP policy and it seems repeated as well.

Again lots of notes/structural/normative details are repeated we should do a cross-review of duplication and where things can be tightened up rather than "adding" more to the spec.

[CMCDragonkai]

I'm going to do one more pass over this and then change the cross review to focus on "tightening up" - reducing duplication - making the spec resilient to inconsistencies... after fixing up the above.

Spec reviews are like programming, the main problem is you don't have a compiler to check your work. It's entirely based on socio-technical review. There's something I want to compare with say EIP-1.

[CMCDragonkai]

We are now in the tightening phase. This is interesting because we can use 4 different models to do independent evaluation.

This is the psp-1 finalization step before we get to prototyping implementation.

I want this current review to focus on "tightening up" - reducing duplication - making the spec resilient to inconsistencies....

Spec reviews are like programming, the main problem is you don't have a compiler to check your work. It's entirely based on socio-technical review. There's something I want to compare with say EIP-1 production readiness.

So identify if there's inconsistencies or things that are being needlessly duplicated and be delicate with our tightening process.

Then from gpt5 pro it indicates that the ranking of reviews are:

Details

Here’s a concise ranking with unitless scores (0–10) and rationale across coverage, actionability, and risk of inconsistency.

1. claude-6 — 9.5

• Strengths:
  • Most comprehensive and actionable: concrete diffs, single-source-of-truth (SSOT) consolidation, execution plan with effort estimates.
  • Catches systemic duplication: pins, environment facts, time-window intersection, projection warnings.
  • Introduces a master fail-closed table with IDs; consistent terminology (channel binding profile, CID, Unix seconds).
  • Addresses lease freshness placement and receipt obligations; adds EIP-grade polish (Backwards Compatibility, Implementation Status).
• Weaknesses:
  • Slightly heavy; some steps could be combined.
• Net:
  • Best overall balance of coverage, specificity, and low-risk edits.

2. grok4-6 — 8.8

• Strengths:
  • Strong SSOT framing (Section 13 as canonical), EIP-1 comparison, and “compiler pass” mindset.
  • Provides tightened replacement text, new sections (Motivation, Backwards Compatibility), and small diffs you can paste.
  • Calls out duplication hotspots and suggests minimal, targeted cuts.
• Weaknesses:
  • One or two recommendations conflict with other reviews (e.g., whether to house “Local Availability” primarily in §2.2 or §11.6).
  • Slightly more narrative; fewer exact line targets than claude-6.
• Net:
  • Very good big-picture refactor with usable edits; second-best.

3. gemini25-6 — 7.8

• Strengths:
  • Clear SSOT principle: move all verification logic into Section 13; refactor other sections to descriptive formation rules.
  • Elevates lease freshness to a core invariant; simplifies algorithm step 8.
  • Good at reducing future inconsistency risk conceptually.
• Weaknesses:
  • Less actionable at the line-edit level; few exact diffs.
  • Omits some duplication hotspots (projection warnings, CID naming, time-window duplication in multiple sections).
• Net:
  • Strong conceptual guidance; needs complementary concrete edits to execute.

4. deepseek-6 — 7.5

• Strengths:
  • Identifies key duplications: Local Availability redefinition, fail-closed repetition, time-window wording, channel binding profile lists, implementer notes.
  • Sensible structural cleanups (rename 11.9, consolidate builtins detail to Appendix B, standardize program notation).
• Weaknesses:
  • Overlaps heavily with claude-6 but with fewer precise edits; most redundant of the four.
  • Some suggested moves (e.g., moving builtins earlier) may be unnecessary churn.
• Net:
  • Useful checklist of redundancies; least comprehensive and most redundant relative to others.

Summary

• Best comprehensive review: claude-6 (9.5) — covers everything with exact, low-risk edits and a plan.
• Most redundant/least actionable: deepseek-6 (7.5) — good points but largely overlaps with others without the same precision.
• If you adopt one reviewer’s plan verbatim, take claude-6; augment with grok4-6’s EIP-1 polish and gemini25-6’s SSOT emphasis (Section 13 as the canonical verifier).

So we can say that deepseek is the weakest, and I could see gemini2.5 is the best "conceptual" model that has the best human-level explanation of things, but it is not as analytical. I wonder how gpt5 pro would evaluate it self.

[CMCDragonkai]

Ok so while we are now in the tightening consolidation making it more cohesive phase, we realised we have alot of repetition and we need to start factoring out aspects of the spec into more modular parts, to collapse the information entropy that exists here.

[CMCDragonkai]

Cohesion means changing some of the information architecture which I've done in the psp-1-new.mdx here. However there's a few remaining things to fix up in terms of internal referencing. So right now I'm trying to do that.

[CMCDragonkai]

Alright I think restructuring is done. Cohesion is sort of done. It's not perfect, but we should proceed with prototyping phase.