diff --git a/projects/passepartout/_index.org b/projects/passepartout/_index.org index 6f75d45..e750d69 100644 --- a/projects/passepartout/_index.org +++ b/projects/passepartout/_index.org @@ -5,8 +5,48 @@ #+title: Passepartout #+filetags: :index: -The staged roadmap and architecture — from conventional computing through verified Lisp machine on custom silicon. +Every layer of the modern computing stack — hardware, firmware, OS, compiler, runtime, network, application — is independently built and independently untrusted. Security today is empirical: "no bugs found in this release" does not mean no bugs exist. We patch, we scan, we monitor, and we accept that zero days are inevitable. The model is probabilistic and the response is reactive. -- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — the full architecture: verification subsystem, environment subsystem, social protocol +Passepartout asks a different question: what if a single system verified everything — from the gate that authorizes an action to the hardware that executes it? + +**One verified memory graph, from silicon to application.** + +The problem with conventional verification is that it operates at one layer. You can verify a microkernel. You can verify a compiler. You can verify a smart contract. But the proofs live in different frameworks, apply to different semantics, and cannot be composed. The gap between any two verified layers is itself an unverified trust boundary — and that gap is where every practical exploit lives. + +The solution is to eliminate the layers. When the entire stack shares one evaluation semantics, there are no boundaries to compose across. The same proof that shows a gate correctly enforces policy also shows that the hardware correctly evaluates the gate. There is nothing between them. + +**Why Lisp specifically.** + +Verification requires a formal semantics closed under evaluation — a specification that says exactly what every possible program does, with no undefined behavior and no implementation-defined escape hatches. C has both. x86 has both. Rust reduces undefined behavior but does not eliminate it, and its intermediate representation is enormous. The only language with a self-contained formal semantics small enough to verify at the metal is Lisp — because the evaluator *is* the specification. There is no gap between what the spec says and what the machine does. A Lisp machine is a Lisp evaluator, and a verified Lisp evaluator is a verified machine by construction. + +This is not about programmer preference. It is the shortest path to a closed, verifiable semantic model at hardware granularity. + +**Three subsystems, one address space.** + +The project decomposes into three subsystems that share one evaluation semantics, one memory graph, and one proof chain: + +- **Verification subsystem** — A gate that evaluates every proposed action against formal policy before allowing it. The same decision procedure checks a shell command, a social protocol contract, or an LLM-generated response. Root as an attack target does not exist because the gate does not depend on OS privilege boundaries — it is in the evaluation loop itself. + +- **Environment subsystem** — The personal computing environment where the user works. One coherent program image, one address space, no IPC boundaries between components, no MMU to attack. The editor, shell, browser, and agent are not separate programs — they are functions in the same evaluated graph. + +- **Social protocol** — Self-sovereign DID identity, encrypted messaging, personal data stores, relay network, compute marketplace, and liquid democracy. The glue between Passepartout instances. Every message is signed, DAG-tracked, and content-addressed. Communication is provable when you choose it to be. + +All three operate in the same Lisp address space. The same gate that authorizes a file write also authorizes a social protocol transaction. The same Merkle chain that proves a DIDComm message's provenance also proves the compiler output matches its source. One semantics, one proof, one machine. + +**Staged delivery, not a cut-over.** + +The full Lisp machine on custom silicon is the destination, but the path is designed so every stage delivers value independently. Stage 0 runs on conventional Linux using Python — exactly where Hermes and gbrain are today. Each subsequent stage eliminates a class of threat and replaces one component with a verified equivalent. The migration is progressive component swap, not a rewrite. + +Stage 7 is what remains when all computational threats are eliminated: physical theft, electronic warfare, logical holes in the specification, and the fallibility of the LLM oracle. No zero days, no viruses, no worms, no malware. The only remaining attack surfaces are physical, oracular, and spec-level — and those are limits of computation itself, not of this design. + +**What it means.** + +When every action is gate-checked, every message is provable, and every computation runs on verified semantics, the security model shifts from empirical to deductive. Compliance becomes executable gate rules instead of annual audits. AI safety becomes a verified gate between the LLM and the action stream instead of probabilistic guardrails. The accumulated verification suite from every deployed instance becomes an industry certification — Underwriters Laboratory for AI. + +Passepartout is a new category. Verified infrastructure. Every existing category — cloud, AI, OS, social, payments, compliance, governance — eventually migrates into it because the alternative becomes indefensible. + +--- + +- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Passepartout Architecture]] — the architecture in detail: verification subsystem, environment, social protocol - [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic Effects]] — how verification cascades across society, economics, and geopolitics -- [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Staged roadmap]] — Stage 0 (Now) through Stage 7 (What Remains) +- [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Staged Roadmap]] — Stage 0 (Now) through Stage 7 (What Remains) diff --git a/projects/passepartout/architecture/architecture.org b/projects/passepartout/architecture/architecture.org index 8968063..3d8d9bb 100644 --- a/projects/passepartout/architecture/architecture.org +++ b/projects/passepartout/architecture/architecture.org @@ -4,37 +4,72 @@ :ID: a1fac32a-47de-5fbd-b67d-29152c851747 :ID: 42c86e6f-4f27-4993-8238-b7bc7d15fb7b :END: -#+title: Passepartout — A Verifiable Personal Intelligence +#+title: Architecture #+filetags: :passepartout:architecture: -Every layer of the modern computing stack — hardware, firmware, OS, compiler, runtime, network, application — is independently built and independently untrusted. Security is empirical: "no bugs found in this release" does not mean no bugs exist. We live with a patching treadmill, with CVEs treated as inevitable, with compliance audits that attest to process rather than proving correctness. +The project index introduces the case for verification and why it requires a uniform semantic model at hardware granularity. This page describes the architecture in detail: how the three subsystems fit together, how the gate works, what the Lisp machine looks like, and why the stack compresses into a single address space. -Passepartout replaces the entire stack with a single coherent architecture where the same gate stack verifies everything and the same prover proves everything consistent. +**The gate as the central primitive.** -**One project, one image, one verified memory graph.** +The verification subsystem is a gate: a function that takes (action, context, policy) and returns (permit | deny). Every action passes through it — a shell command from the user, a proposal from the LLM, a message from the network, a file write by a scheduled job. There is no privileged path around the gate. There is no "run as root" because root is not a concept in the gate model — root is a convention enforced by an OS that the gate replaces. -Three subsystems compose into a single system: +The gate combines two decision layers: -- **Verification subsystem** — A gate that evaluates every proposed action — from the user, the LLM, or a network message — against formal policy before allowing it. Combines ACL2-verified decision procedures for security-critical checks with a probabilistic LLM for natural-language reasoning. The gate checks shell commands, DIDComm messages, and LLM-generated action proposals through the same decision procedure. Root as an attack target does not exist. +1. ACL2-verified decision procedures for security-critical checks — access control, message authentication, capability resolution. These are provably correct for their domain. +2. An LLM for natural-language reasoning — parsing the user's intent, evaluating whether an action falls within policy boundaries that require human judgment. -- **Environment subsystem** — A single Lisp image where editor (Lish), browser (Nyxt), shell (Lish), and agent coexist. No separate daemons, no IPC boundaries, no trust transitions between components. One address space, one evaluated memory graph, no MMU to attack. The distinction between tool and self dissolves. +The LLM layer is probabilistic. The ACL2 layer is deductive. The gate architecture ensures that the deductive layer is authoritative where it applies and the probabilistic layer is bounded by it — the LLM cannot overrule a verified denial. -- **Social protocol** — Self-sovereign DID identity, DIDComm encrypted messaging, personal data store, relay network, compute marketplace, liquid democracy. The protocol that connects Passepartout instances to each other. Every message is signed, DAG-tracked, and content-addressed. Communication becomes provable when you choose it to be. +**The environment subsystem: one address space.** -All three subsystems operate in the same Lisp address space. All three are verified by the same ACL2 prover. The gate that authorizes a file read also authorizes a social protocol contract. The Merkle chain that proves a DIDComm message's provenance also proves the compiler output matches its source. There is one semantics, one proof, one machine. +The environment eliminates the layered trust model of a conventional OS by eliminating the layers. Instead of an editor that sends keystrokes through a terminal emulator to a shell that forks processes that read files through a kernel VFS layer — each boundary a potential vulnerability — the environment subsystem runs everything in a single Lisp address space. -**The staged approach:** +What this means concretely: -The full Lisp machine on custom silicon is the destination. But the path is designed so every stage delivers value independently. +- The editor is a Lisp function that manipulates text buffers in the evaluated memory graph. +- The shell is a Lisp read-eval-print loop that compiles to the same evaluator. +- The browser renders HTML through a Lisp-based rendering engine, not through a separate browser process. +- The agent runtime invokes Lisp functions, not subprocesses. -Stage 0 is where we are — conventional Linux on x86, with Python (Hermes) as the agent runtime and gbrain as the knowledge store. Stage 1 adds message-level authentication with the social protocol. Stage 2 adds the verified gate as a software layer. Stage 3 is the Lisp machine emerging inside the host OS — SBCL image absorbing every interface into one address space. Stages 4 through 6 add in-process LLM inference, plist-native weights, and verified fine-tuning. Stage 7 is what remains when all computational threats are eliminated: physical, oracular, and specification limits that no machine can solve. +(The specific implementations that realize this today use Lish for the shell and editor, Nyxt for the browser, and SBCL as the host Lisp — but the architectural principle is uniform semantics in one address space, not these particular packages.) -Each stage is usable. Each stage eliminates a class of threats that the previous stage could not. The migration from today's Hermes deployment to a full Passepartout machine is a progressive component swap, not a cut-over. +There is no MMU boundary between components because there are no separate processes. There is no IPC because there is nothing to communicate between — everything shares the same memory graph. The distinction between tool and self dissolves: your editor buffer, your shell history, your agent's state, and your social protocol messages all live in the same evaluated object graph, protected by the same gate, verified by the same prover. -**What it means:** +**The social protocol: provable communication.** -When every action is gate-checked, every message is provable, and every computation runs on verified hardware, the security model shifts from empirical to deductive. Memory corruption — the dominant attack vector for decades — is structurally eliminated. Compiler backdoors are impossible because compilation is Lisp-to-Lisp within the verified evaluator. Malware has no execution path that bypasses the gate. +The social protocol extends the verified semantics beyond a single machine. It provides: -The downstream effects cascade: compliance becomes executable gate rules instead of annual audits. AI safety becomes a verified gate between the LLM and the action stream instead of probabilistic guardrails. The accumulated regression suite from every deployed instance becomes an industry certification — Underwriters Laboratory for AI. +- Self-sovereign DID identity (every instance has a cryptographic identity it controls) +- DIDComm encrypted messaging (end-to-end encrypted, signed, DAG-tracked) +- Personal data stores (user-owned, gate-controlled) +- Relay network (asynchronous message delivery across trust boundaries) +- Compute marketplace (provision verified the compute you rent) +- Liquid democracy (delegable voting over protocol governance) -Passepartout is not a product in an existing category. Verified infrastructure is a new category, and every existing category — cloud, AI, OS, social, payments, compliance, governance — eventually migrates into it because the alternative becomes indefensible. +Every message is signed by the sender's DID, tracked in a content-addressed DAG, and optionally notarized. Communication is provable when you choose it to be — you can prove what you sent, to whom, when, without revealing content. + +The social protocol is not a blockchain. It uses DAG-based ordering for causality, not global consensus. Delegable trust replaces proof of work. + +**The staged progression.** + +The full architecture — gate-verified Lisp machine on custom silicon — is the destination. The staged roadmap describes how each successive replacement eliminates a class of threat: + +- Stage 0: Conventional Linux, Python agent (Hermes), SQLite knowledge store (gbrain). The starting point. Zero days exist; patches are manual. +- Stage 1: Message-level authentication via the social protocol. Communication becomes provable. +- Stage 2: The gate operates as a software layer over the host OS. Shell commands, LLM proposals, and network messages all pass through the same decision procedure. Root is eliminated as an attack path. +- Stage 3: The host OS is replaced by a bare-metal SBCL image. The Lisp machine emerges. One address space, one evaluator, no MMU to attack. +- Stage 4: LLM inference moves into the Lisp process. No API calls across a network boundary. The LLM becomes a function in the same evaluated graph. +- Stage 5: Neural weights are stored as plist-native data structures. The gap between symbolic and neural representations closes. +- Stage 6: Verified fine-tuning. Every weight update is gate-checked against policy — the LLM cannot learn to bypass the gate because the gate is not in the LLM's mutable space. +- Stage 7: What remains. Physical theft, electronic warfare, holes in the specification itself, and the fallibility of the LLM oracle. These are limits of computation, not of this design. + +Each stage is independently useful. Stage 0 is running today. The migration is progressive component swap, not a cut-over. + +**Downstream effects.** + +When every action is gate-checked, every message is provable, and every computation runs on verified semantics, the security model shifts from empirical to deductive. The downstream effects cascade beyond personal computing: + +- **Compliance** becomes executable gate rules instead of annual audits. A SOC 2 report is a gate configuration, not a PDF. +- **AI safety** becomes a verified gate between the LLM and the action stream instead of probabilistic guardrails or RLHF. +- **Software certification** becomes the accumulated regression suite of every deployed instance — the Underwriters Laboratory for AI. +- **Operating systems** become obsolete. The gate replaces the kernel, the address space replaces process isolation, and the verified evaluator replaces the entire privilege model.