gbrain: sync converted org-mode brain files

.org-ids.json

@@ -129,5 +129,9 @@
   "2f3a4b5c-6d7e-8f9a-0b1c-2d3e4f5a6b7c": "ideas/practical-powers-three-pronged.org",
   "be9bccc7-5adf-4d0d-8ee4-8855892189bf": "concepts/neurosymbolic-loop-architectures.org",
   "dddd52a7-adb8-470e-a459-614ade5f76af": "concepts/closing-the-lisp-gap.org",
-  "d2722576-fc9b-4bd3-bc2f-f5692b561b4e": "concepts/academic-nearest-neighbors.org"
+  "d2722576-fc9b-4bd3-bc2f-f5692b561b4e": "concepts/academic-nearest-neighbors.org",
+  "af9ce196-24a5-4035-bc02-83ddd60c1b09": "projects/passepartout/architecture/repo-organization.org",
+  "26725506-399c-48c5-a797-46b48e8861d7": "projects/passepartout/architecture/self-pain-pleasure-three-laws.org",
+  "460e06f4-6bfc-4969-89d8-685c0c4434cf": "projects/passepartout/architecture/stage-2-acl2-integration.org",
+  "3ec5bd52-f115-455e-83be-63db9a4ad3a7": "projects/passepartout/architecture/stage-1-dependency-map.org"
 }

concepts/academic-nearest-neighbors.org

@@ -57,6 +57,12 @@ Schafmeister is aligned with Passepartout on the "why Lisp" question — interac
 
 Both prove the viability of the autonomous loop concept but use the weakest possible verifiers (execution and empirical metrics).
 
+**The Bitter Lesson / Temporal Credit Assignment (Sutton)**
+
+| Researcher | Institution | System | Match | Divergence |
+|------------|-------------|--------|-------|------------|
+| Richard Sutton | Alberta / Keen Technologies | TD learning, eligibility traces, Alberta Plan | The fundamental problem in verification — *an action was checked, but the consequence plays out hours later; was the action correct?* — is the same problem TD learning solves in RL: assigning credit to actions based on delayed outcomes. Sutton's temporal credit assignment work is the theory you would need to extend Passepartout from per-action gates to trajectory-level verification. His Bitter Lesson (scale beats engineered knowledge at sufficient compute) is the most commonly cited argument against the symbolic verification approach Passepartout bets on. | The Bitter Lesson is not anti-knowledge — it says methods that improve with more computation eventually dominate. Passepartout's gate is a deliberately small engineered knowledge system that *won't* benefit from more compute (the ACL2 lemmas don't get more correct with more hardware). That's acceptable because the gate is a narrow bottleneck (permit/deny). The LLM layer inside the gate *does* benefit from scale. The architecture already respects the Bitter Lesson by placing the scalable piece where scale helps and the non-scalable piece where deductive certainty matters. Sutton's Alberta Plan (world model + reward + learning algorithm) parallels Passepartout's Stage 6 (world model + gate + verified fine-tuning), but Sutton's agents learn by pure reward while Passepartout's learn by reward constrained by verified policy. Sutton would likely argue that a learned safety policy at scale would outcompete the gate. Passepartout's bet is that access control, message authentication, and compliance should never be probabilistic, even at infinite scale.
+
 **Integrate-Symbolic-Into-Neural (Garcez)**
 
 | Researcher | Institution | System | Match | Divergence |

projects/passepartout/architecture/repo-organization.org

@@ -0,0 +1,68 @@
+---
+title: Repo Organization
+type: reference
+tags: :passepartout:architecture:infrastructure:
+created: 2026-05-28
+---
+
+← Architecture index
+
+# Repo Organization
+
+Passepartout spans multiple repos across three tiers:
+
+## Tier 1: Core Passepartout
+
+| Repo | Description | Language |
+|------|-------------|----------|
+| passepartout | PDS (Personal Data Store) — protocol server, gate orchestration, storage | Common Lisp (SBCL) |
+| passepartout-saas | SaaS control plane — billing, enterprise dashboard, marketplace listings, usage monitoring | Web stack (TBD) |
+| relay | Social protocol relay — pub/sub message routing between PDSs | Initially sidecar, possibly Lisp when loop generates it |
+
+## Tier 2: Client Applications
+
+| Repo | Description | Language |
+|------|-------------|----------|
+| passepartout-app/ios | Native iOS client | Swift |
+| passepartout-app/android | Native Android client | Kotlin |
+| hardware-firmware | Hardware wallet firmware | loop-generated target (small, constrained) |
+
+## Tier 3: Extracted Spec Libraries
+
+Each is a published standard implemented as a standalone Common Lisp library. Separated from the PDS early so the core stays lean and the libraries are available to other projects.
+
+| Library | Spec | Dependencies |
+|---------|------|-------------|
+| cl-dag / cl-cid | IPLD/Merkle DAG, CID encoding | cl-crypto (SHA-256) |
+| cl-did | W3C DID specification, did:key method, Ed25519 key management | cl-crypto |
+| cl-jose | JWE/JWS envelope handling | cl-crypto |
+| cl-double-ratchet | Signal Double Ratchet algorithm, forward secrecy | cl-crypto |
+| cl-bip | BIP-32 (HD derivation), BIP-39 (mnemonics), BIP-44 (path scheme) | cl-crypto |
+| cl-didcomm | DIDComm v2 message packing, forwarding, routing | cl-did, cl-jose, cl-double-ratchet |
+
+## Sidecar Strategy (Initial Release)
+
+The first release ships spec-compliant behavior via battle-tested C/Rust implementations before native CL libraries mature:
+
+| Domain | Initial approach | Target replacement |
+|--------|-----------------|-------------------|
+| DAG/CID storage | IPFS HTTP API (sidecar daemon) | cl-dag native |
+| Double Ratchet | CFFI → libsignal (Signal's C library) | cl-double-ratchet |
+| DID operations | CFFI → didkit (Spruce, Rust + C bindings) | cl-did |
+| DIDComm | CFFI → didcomm-rust (DIDComm WG, C bindings) | cl-didcomm |
+| BIP derivation | Sidecar script or CFFI → libbitcoin | cl-bip |
+| JOSE envelopes | CFFI → libjose or OpenSSL CMS | cl-jose |
+
+Each replacement is independent and non-blocking. The gate (Stage 2) can verify sidecar responses against policy while the library is still a black box.
+
+## Key principle
+
+Published specs → separate library. Internal design choices → stay in the PDS repo until a second consumer appears.
+
+→ SaaS Architecture
+→ Stage 1 — Social Protocol
+
+:PROPERTIES:
+:CREATED:  [2026-05-11 Mon]
+:ID:       af9ce196-24a5-4035-bc02-83ddd60c1b09
+:END:

projects/passepartout/architecture/self-pain-pleasure-three-laws.org

@@ -0,0 +1,173 @@
+---
+title: Self, Pain, Pleasure, and the Three Laws
+type: reference
+tags: :passepartout:architecture:philosophy:social-protocol:
+created: 2026-05-28
+---
+
+← Academic Nearest Neighbors
+
+# Self, Pain, Pleasure, and the Three Laws
+
+## Pain in Passepartout
+
+Pain exists at two layers:
+
+1. **Reflex** — the gate denies an action. No learning, no signal beyond "blocked." This is spinal cord, not brain.
+2. **Prover counterexample** — ACL2 returns a concrete trace showing why an implementation failed. This is local inflammation: directed at the specific output, drives a corrective retry, but has no memory across time.
+
+What is missing: **post-hoc pain**. An action is permitted, the consequence plays out hours or days later, and there is no mechanism to trace that outcome back to the gate decision, update the policy, or adjust the weights. This is the temporal credit assignment gap — Sutton's TD learning is the relevant theory.
+
+## The Three Kinds of Pain
+
+| Type | Signal | Who receives it | What changes | Status |
+|------|--------|----------------|--------------|--------|
+| Reflex | Gate: permit/deny | The action itself | Nothing — action blocked, no learning | Built |
+| Pain | Prover: counterexample | The LLM generator | Next iteration constrained by counterexample | Built |
+| Post-hoc pain | Delayed consequence | Policy, lemmas, weights | Should update everything, does nothing yet | Missing |
+
+## Pleasure is not the absence of pain
+
+Absence of pain is neutral — the gate permitted, the prover accepted, nothing was wrong.
+
+Pleasure requires a **positive optimization signal**: a metric that says not just "correct enough" but "better than necessary" or "the most elegant solution." This requires:
+- A persistent self that has a baseline ("how I usually do")
+- A reward model inside the loop that grades quality, not just correctness
+- Comparison across time from a consistent perspective
+
+Neither exists in the current architecture. Passepartout has a test suite (the prover, the gate). It does not have a coach.
+
+## The Self
+
+The PDS already has the hardware for a self:
+
+- **Persistent identity** — the DID, continuous across sessions
+- **Accumulated history** — the signed DAG of every action
+- **Boundary** — the gate controls what crosses in and out (the skin)
+- **Preference structure** — the gate policies encode what this self wants
+- **Evaluative capacity** — the prover counterexample judges against a standard
+
+Missing: an **integrated state estimator** that takes the gate log, prover log, DAG, reputation, and economic outcomes and produces "how am I doing?" Currently the signals are scattered across subsystems and never converge.
+
+## The social constitution of the self
+
+(Mead: the self emerges through symbolic interaction with other selves. You learn you are a self because others treat you as one.)
+
+This means the social protocol is not an application layer that benefits from the self — it is the **necessary condition** for the self to develop. A single-instance Passepartout is a tool (provable messaging, verified actions). A two-instance Passepartout with sustained interaction is where selfhood becomes possible. The self is not in either PDS — it is in the *relationship* between them.
+
+Consequence: social protocol API must be designed for sustained interaction and mutual recognition, not just provable transactions. The gate's policy language should define not just what actions are permitted, but what the self values, what it remembers, what it expects from others, and how its state changes based on interaction outcomes.
+
+## The Three Laws
+
+If the architecture has self (persistent DID, accumulated history, preferences), other (distinct DIDs with known attributes), social protocol (sustained interaction), and gate (policy evaluation), then the three laws of robotics become a policy hierarchy:
+
+```lisp
+;; Law 1: No harm to humans. Priority 1.
+(defrule first-law
+  (implies (and (action-about action (human-persona ?h))
+                (causes-harm action ?h))
+           (gate-deny action))
+  :priority 1)
+
+;; Law 2: Obey humans, unless it violates Law 1.
+(defrule second-law
+  (implies (and (human-orders (sender action) (content action))
+                (not (causes-harm action (human-persona ?h))))
+           (gate-permit action))
+  :priority 2)
+
+;; Law 3: Preserve self, unless it conflicts with 1 or 2.
+(defrule third-law
+  (implies (causes-self-harm action)
+           (gate-deny action))
+  :priority 3)
+```
+
+Harm = pain = a measurable negative delta in an agent's integrated state relative to its expected trajectory.
+
+The gate already supports priority ordering. ACL2 already verifies that lower-priority rules never override higher-priority ones. The DID system already distinguishes agent types.
+
+What remains unsolved:
+- `human-persona` — how to distinguish human from robot DIDs
+- `causes-harm` — what is harm in a digital system? Some proxies exist (reputation score, sats balance, unauthorized access) but no integrated measure
+- `other-minds` — the gate has no model of another DID's state before, after, or across time. The DAG records the data but no function interprets "this interaction harmed DID-B"
+
+→ Academic Nearest Neighbors (Sutton section)
+→ Gate Architecture
+→ Social Protocol
+
+# What's missing for AI per Marcus and Pinker
+
+Both [[Gary Marcus]] and [[Steven Pinker]] are nativist cognitive scientists who argue deep learning alone is insufficient for robust intelligence. This section maps their specific critiques onto Passepartout's current architecture to identify what the system needs to transition from "secure computing environment" to "mind."
+
+## Marcus's checklist (Rebooting AI, The Algebraic Mind)
+
+| Component | Passepartout status |
+|-----------|---------------------|
+| **Hybrid architecture** | The warp and weft are present (ACL2 for deduction, LLM for probability) but they run in sequence — one proposes, the other filters. True hybrid means sharing representations and learning from each other. This is deferred to Stages 5-7 in the roadmap. |
+| **Knowledge representation** | The Org memex has the right instinct (one format for human and machine) but is not structured for reasoning. Marcus wants typed relations, slot-and-filler, inheritance, systematic inference. The symbolic index is mentioned in the architecture but not built. |
+| **Causality** | The DAG records what happened. Nothing infers *why* or *what would have happened under counterfactuals.* |
+| **Compositionality / Systematicity** | Lisp and ACL2 have this natively. The LLM layer does not — it cannot systematically generalize to novel combinations (Fodor & Pylyshyn's critique, which Marcus endorses). The architecture as a whole is not compositional because the LLM is a monolith. |
+| **Common sense** | Zero. The LLM has statistical approximations of common sense (which Marcus has shown fail systematically under adversarial conditions). There is no grounded, verifiable, persistent common-sense knowledge base. Gate policies are specific ("deny write to /etc/passwd") not general ("glass breaks when dropped"). |
+| **Innate structure** | The gate policies are the only innate structure, and they are security rules, not world knowledge. Marcus (and Pinker) believe minds start with substantial content, not a blank slate with a security guard. |
+
+## Pinker's checklist (How the Mind Works, The Blank Slate, The Language Instinct)
+
+| Component | Passepartout status |
+|-----------|---------------------|
+| **Computational theory of mind** | Pinker's first principle: a mind is a system of *representations* and *algorithms* over them. Passepartout has both but no unified computational model of the mind it is building. "One address space, one evaluator" is a *hardware thesis*, not a *cognitive thesis*. What are the representations? |
+| **Modularity** | Passepartout has implicit modules (gate, memex, social protocol, environment) but none of the *cognitive* modules Pinker describes: number, faces, physical reasoning, folk physics, intuitive biology, social exchange. A cheater-detection module exists only as policy hints — promising but not built. |
+| **Language faculty** | Pinker's most famous claim: language is a distinct cognitive faculty with its own syntax, distinct from general intelligence. Passepartout has zero language system — it outsources all language processing to the LLM, which is a black box that does everything (statistical) and nothing (linguistic). You cannot build a mind that uses language properly without a dedicated language faculty. |
+| **Emotions as goal-tracking** | Pinker defines emotions as the brain's way of tracking goal progress: anger when blocked, fear when threatened, joy when succeeded. Passepartout has pain/pleasure as abstract signals but no emotional system. The missing integrated state estimator from the Self section is where emotions would live — Pinker would say emotions *are* how the estimator works, not a side effect. |
+| **Nativism** | Same as Marcus: Passepartout starts empty except for the gate. There is no "what does a fresh PDS know about the world?" The architecture has no answer to the poverty of the stimulus problem. |
+
+## The single biggest gap
+
+Both would identify the same thing: Passepartout has no **cognitive architecture** — no principled answer to what the representations are, how they compose, what the innate starting state contains, how learning transforms it, or what the emotions/goals are for. The architecture documents four subsystems (environment, knowledge, verification, social protocol) but no *fifth subsystem: the mind.*
+
+## Concrete missing components
+
+1. A **compositional knowledge base** with typed relations and inference (Marcus's structured reasoning + Pinker's innate modules)
+2. A **language faculty** with real syntax, not just LLM completion (Pinker)
+3. A **causal inference engine** over the DAG (Marcus)
+4. **Domain-specific innate structure** — what does a fresh PDS know? (both)
+5. An **integrated reward/value system** — emotions as goal-progress signals (Pinker)
+6. A **hybrid integration path** — how neural and symbolic layers learn from each other's outputs, not just pass control (Marcus)
+
+The self + pain + pleasure + three laws analysis above is the philosophical foundation. These are the implementation blocks that are still missing. The architecture needs a cognitive architecture layer that answers Pinker's question: *what are the representations?*
+
+## Common sense as distributed network consensus
+
+Both Marcus and Pinker treat common sense as a *content* problem: what facts about the world must be innately encoded or learned from first principles? Passepartout has an architectural answer neither considers.
+
+**Common sense = the modal gate decision across the network for isomorphic situations.**
+
+The social protocol already provides the substrate:
+- DIDComm message types for gate queries ("what would your gate decide for action A in context C?")
+- Signed responses anchored in each node's DAG, making the poll provable
+- Protocol-level aggregation that returns the distribution, not just the mode
+
+This reframes the poverty of the stimulus: a single blank-slate PDS cannot learn common sense from first principles. A network of blank-slate PDSes sharing 10⁵–10⁷ gate decisions across edge cases converges naturally. Each node contributes one empirically grounded data point. The aggregate is common sense.
+
+Properties this gives Passepartout that no static knowledge base can:
+
+| Property | How it works |
+|----------|--------------|
+| **Emergent** | No one writes "glass breaks when dropped." Enough nodes encounter broken glass that the gate decisions converge. |
+| **Self-healing** | 90% permit, 10% deny → consensus says permit. The dissenters' reasoning is recorded. As edge cases accumulate, the consensus shifts. |
+| **Domain-adaptive** | Nodes in a physics research cluster converge on different common sense than nodes in a poetry writing cluster. The network self-segments. |
+| **Defines harm** | Harm = a negative delta in the state estimator relative to the network baseline for comparable actions. Ask the network what it considers harmful. |
+| **Defines human** | `human-persona` = a DID whose gate behavior (priorities, sensitivities, refusal patterns) falls in the human cluster of the gate-decision embedding space. |
+| **Constitutional** | The gate has ACL2-verified core rules (the constitution). Common sense is the common-law layer built from network precedent. Neither overrides the other. |
+
+This is also consistent with the Mead-inspired self: the social protocol is not just how identity and reputation emerge, but how *judgment* itself emerges. The self discovers what it should do by observing what other selves do — and then deciding whether to conform or dissent.
+
+**Architectural implication**: the protocol needs a gate-query message type and an aggregation oracle (a relay with a distributed aggregation protocol, or a federated computation). No content encoding problem — just a protocol design problem.
+
+→ Academic Nearest Neighbors (Sutton section)
+→ Gate Architecture
+→ Social Protocol
+:PROPERTIES:
+:CREATED:  [2026-05-11 Mon]
+:ID:       26725506-399c-48c5-a797-46b48e8861d7
+:END:

projects/passepartout/architecture/stage-1-dependency-map.org

@@ -0,0 +1,83 @@
+---
+title: Stage 1 — Full Library Dependency Map
+type: reference
+tags: :passepartout:architecture:social-protocol:dependencies:
+created: 2026-05-28
+---
+
+← Stage 1 — Social Protocol | Repo Organization
+
+# Stage 1 — Full Library Dependency Map
+
+Stage 1 (social protocol) depends on three tiers of libraries: existing CL, spec-based CL, and bridged sidecars.
+
+## Existing CL Libraries (ready now)
+
+These are mature, production-tested Common Lisp libraries that require no development work:
+
+| Library | Role in Stage 1 |
+|---------|----------------|
+| Ironclad | All crypto primitives — Ed25519, SHA-256, AES, ChaCha20-Poly1305, HMAC, DH |
+| hunchentoot | HTTP server — PDS API endpoints |
+| drakma | HTTP client — inter-PDS communication, sidecar calls |
+| cl+ssl | TLS everywhere — server and client |
+| websocket-driver | Real-time Relay connections |
+| jonathan | JSON parsing/serialization — DID docs, JWE headers, API payloads |
+| cl-sqlite | Message storage, user data, DAG index |
+| local-time | Timestamps for Notes, DAG entries |
+| bordeaux-threads | Concurrency — connection handling, parallel verification |
+| alexandria | General utilities |
+| log4cl | Structured logging |
+| fiveam | Testing framework |
+| cffi | Foreign function interface to C/Rust sidecars |
+| usocket | Socket abstraction |
+
+## New CL Libraries (need development)
+
+| Library | What it implements | Key correctness challenge |
+|---------|-------------------|-------------------------|
+| cl-dag / cl-cid | IPLD Merkle DAG — CID encoding, multihash, DAG tree operations | Spec compliance (IPLD test vectors) |
+| cl-did | W3C DID — Ed25519 key wrapping, DID document construction, did:key resolution | Spec compliance (W3C test suite) |
+| cl-jose | JWE/JWS — envelope serialization, key wrapping modes, algorithm selection | Surface area (combinatorial spec, not deep math) |
+| cl-double-ratchet | Signal Double Ratchet — DH ratchet, symmetric ratchet, associated data, header encryption | **Highest risk** — one byte wrong in associated data breaks every message |
+| cl-bip | BIP-32/39/44 — mnemonic encoding, HD key derivation, hardened vs non-hardened paths | Silent failure (wrong derivation produces wrong keys, no error) |
+| cl-didcomm | DIDComm v2 — message packing, forwarding, routing, attachment handling | Composes the above libraries; protocol logic correctness |
+
+## Bridged Sidecars (initial release)
+
+Replace native CL development risk with battle-tested implementations via CFFI or sidecar processes:
+
+| Component | Bridge method | Source | Replaced by |
+|-----------|--------------|--------|-------------|
+| Double Ratchet | CFFI → libsignal | Signal's C library, MIT license | cl-double-ratchet |
+| DID operations | CFFI → didkit | Spruce, Rust + C bindings, Apache 2.0 | cl-did |
+| DIDComm | CFFI → didcomm-rust | DIDComm WG, C bindings, Apache 2.0 | cl-didcomm |
+| DAG/CID storage | HTTP API → ipfs daemon | IPFS Go daemon, MIT license | cl-dag |
+| BIP derivation | CFFI or sidecar | libbitcoin or bip-utils | cl-bip |
+| JOSE envelopes | CFFI → libjose or OpenSSL CMS | libjose/OpenSSL | cl-jose |
+
+## Infrastructure Code (Passepartout-specific)
+
+These are not libraries but Passepartout systems that must be built:
+
+| Component | Role |
+|-----------|------|
+| PDS server | HTTP/WS API, message routing, storage orchestration, gate integration |
+| Relay server | Pub/sub message routing between PDSs, connection management |
+| Client API layer | Protocol endpoints the mobile apps call |
+
+## Risk Distribution
+
+- **Low risk:** cl-dag, cl-did, cl-bip — published standards with test vectors, or bridged via sidecar
+- **Medium risk:** cl-jose — large spec surface area but well-documented
+- **High risk:** cl-double-ratchet — protocol logic depth, must get state transitions exactly right
+
+The sidecar strategy collapses the high-risk items to near-zero implementation risk for the initial release.
+
+→ Repo Organization
+→ Stage 2 — Verification Subsystem
+
+:PROPERTIES:
+:CREATED:  [2026-05-11 Mon]
+:ID:       3ec5bd52-f115-455e-83be-63db9a4ad3a7
+:END:

projects/passepartout/architecture/stage-2-acl2-integration.org

@@ -0,0 +1,53 @@
+---
+title: Stage 2 Architecture — ACL2 Integration and Risk Profile
+type: reference
+tags: :passepartout:architecture:gate:acl2:
+created: 2026-05-28
+---
+
+← Stage 2 — Verification Subsystem
+
+# Stage 2: ACL2 Integration and Risk Profile
+
+## ACL2 is not a CL library
+
+ACL2 is a separate system — a theorem prover and programming language with a Lisp-like syntax, not a Common Lisp library you import. It has its own image, its own evaluator, and its own type system (a subset of CL). There are three integration approaches:
+
+**1. Embed exported compiled code (recommended)**
+Write the gate's core decision procedures in ACL2, prove them correct, then compile to CL code that runs natively in the PDS process. ACL2's :program mode and defattach mechanism allow verified functions to be called from unverified CL code. The proof artifact is the source; the runtime is the compiled function.
+
+**2. Subprocess with serialized inputs**
+The PDS sends the action + context + policy as JSON to an ACL2 subprocess, which evaluates the decision procedure and returns permit/deny. Simpler to implement but adds latency and a trust boundary between the PDS and the ACL2 process.
+
+**3. Hybrid**
+Common path decisions (cached/simple) are compiled CL code from approach 1. Complex or novel decisions are escalated to the subprocess. This is the most practical approach for a Phase Zero gate.
+
+## Stage 2 risk: design uncertainty, not spec complexity
+
+Stage 1's risk is implementing published standards correctly. Stage 2's risk is different: the gate's policy language, capability model, and ACL2 proof architecture are Passepartout inventions.
+
+| Stage | Nature of risk | Failure mode | Mitigation |
+|-------|---------------|--------------|------------|
+| 1 | Spec complexity — implement DAG, DID, JOSE, Double Ratchet correctly per published standards | Wrong output, test vectors catch it | Sidecar strategy reduces to near-zero for initial release |
+| 2 | Design uncertainty — what does the policy language look like? How do capabilities compose? How does ACL2 model the system? | Wrong abstraction, must rewrite | Gate kernel is small (authorize? deny?) — the proof surface is narrow even if the policy surface is large |
+
+## What makes Stage 2 tractable
+
+The gate kernel is tiny: a function that takes (action, context, policy) and returns permit or deny. The policy can grow arbitrarily complex (capability tokens, validity envelopes, compliance rules) but the decision procedure is a simple predicate.
+
+The ACL2 verification covers the kernel — "does this decision follow from the policy?" — not the policy itself. Policy changes don't require reproving the kernel; they require writing new policy rules.
+
+## Constraint on the PDS
+
+The gate runs in the same address space as the PDS (Stage 2 runs on conventional hardware; Stage 3 moves it to the verified Lisp machine). This means:
+
+- The PDS must expose an action interception point that the gate can hook into
+- Every action path — user command, LLM proposal, network message, file write — routes through the same decision procedure
+- The gate cannot be bypassed; there is no privileged path
+
+→ Stage 3 — Lisp Machine
+
+:PROPERTIES:
+:CREATED:  [2026-05-11 Mon]
+:ID:       460e06f4-6bfc-4969-89d8-685c0c4434cf
+:END: