diff --git a/projects/passepartout/biology-parallels.org b/ideas/biology-parallels.org similarity index 100% rename from projects/passepartout/biology-parallels.org rename to ideas/biology-parallels.org diff --git a/projects/passepartout/_index.org b/projects/passepartout/_index.org index e0933fa..98af7a6 100644 --- a/projects/passepartout/_index.org +++ b/projects/passepartout/_index.org @@ -5,36 +5,55 @@ #+title: Passepartout #+filetags: :index: -Passepartout is a project whose product does not yet exist in any category. It builds toward a personal computing environment where one machine — a verified Lisp Machine — is your editor, browser, shell, agent, knowledge base, and social identity all in one address space, all verified by the same prover, all owned and controlled by you. +**What Passepartout is.** -It answers a question most systems have stopped asking: what kind of computing environment would you build if you did not assume that every layer is a potential attack surface? Not an operating system with better security — an operating system that eliminates the need for security boundaries by eliminating the layers between components. +Passepartout is a project that builds toward a personal computing environment where you own your computation, your data, and your agency — and the architecture proves it, not promises it. -Three subsystems compose into one system: +It is a single system that is simultaneously: -- **Environment** — Your personal computing environment. Editor, browser, shell, and AI agent coexist as functions in one Lisp image, not separate processes. No daemons to manage, no IPC to trust, no MMU to attack. The tool and the self share one memory graph. +- Your editor, browser, shell, and AI agent — not separate programs but a single environment where everything works together because everything shares the same structure. +- Your knowledge base — a living [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][memex]] of everything you read, write, and decide, stored in a format you can read and your machine can read, with no translation layer between them. +- Your gatekeeper — a system that checks every action against your rules before taking it, whether the action comes from you, from the AI, or from the network. +- Your identity and communication protocol — cryptographic identity, encrypted messaging, and provable exchanges between instances. -- **Knowledge** — A memex where humans and machines share the same file format. Org-mode is the universal representation: prose the human writes, code the machine runs, metadata the system queries, and links the graph navigates — all in one structure. The Org file is not a representation of your data; it is your data. No database to maintain, no schema to migrate, no lock-in to outlive. +These are not separate products. They are one project, one architecture, one machine. -- **Verification** — A gate that evaluates every action — from the user, the LLM, or a network message — against formal policy before allowing it. The same decision procedure checks a file write, a DIDComm contract, and an LLM-generated proposal. Root does not exist. Privilege escalation is structurally impossible because there are no privilege levels to escalate through. +**Why it exists.** -All three operate in the same Lisp address space, verified by the same ACL2 prover. The gate that authorizes a file read also authorizes a social protocol transaction. The Merkle chain that proves a DIDComm message's provenance also proves the compiler output matches its source. One semantics, one proof, one machine. +The modern computing stack is built from independently built, independently untrusted layers: hardware, firmware, operating system, compilers, runtime, network protocols, applications. Each layer assumes the layers below it are either trusted or someone else's problem. The gaps between layers are where exploits live. -**Why Lisp.** +Security is reactive. We find bugs, we patch them, we run antivirus, we monitor logs. The model is probabilistic: "no known vulnerabilities" does not mean none exist, only that none have been found. The patching treadmill has been running for forty years and shows no sign of slowing. -Because verification requires closed formal semantics — a specification that says exactly what every program does, with no undefined behavior. Lisp is the only language where the evaluator is the spec. A Lisp machine has no spec-interpretation gap. This is not about programmer preference; it is about the shortest path to a verifiable machine. +Passepartout asks a different question: what if you eliminated the boundaries between layers instead of trying to secure them? What if the entire stack shared one structure, one verification, one proof — from the rules that authorize an action to the hardware that executes it? -**Why staged.** +This eliminates entire categories of threats by structural design, not by patching. Memory corruption exploits, compiler backdoors, malware with execution paths that bypass the rules — these are not mitigations you add on top of an unsafe system. They are classes of threat that cannot exist in a system built on this principle. -The full Lisp machine on custom silicon is the destination, but every stage delivers value independently. Stage 0 runs on conventional Linux using Python — Hermes as agent, gbrain as knowledge store. Stage 1 adds the social protocol (DID identity, encrypted messaging). Stage 2 adds the verified gate as a software layer. Stage 3 replaces the host OS with a bare-metal Lisp image. Each subsequent stage eliminates another class of threat: network API calls, the gap between symbolic and neural weights, unverified fine-tuning. Stage 7 is what remains when all computational threats are eliminated — physical theft, electronic warfare, holes in the specification itself, and the fallibility of the LLM oracle. +**What it replaces.** + +| Current approach | Passepartout | +|---|---| +| Separate editor, browser, shell, agent — each a different program with different trust assumptions | One environment where all are functions in the same memory space | +| Knowledge stored in a database you cannot inspect | Knowledge stored in a file format you read and edit directly | +| Security through permissions, firewalls, antivirus, audits | Security through a rule system that checks every action before it executes | +| Separate identity systems for every service (Google login, GitHub, Slack) | One cryptographic identity you control | +| Vulnerabilities found and patched reactively | Categories of threat eliminated by architecture | + +**How we get there.** + +The full system is the destination, but every intermediate stage delivers value on its own. The project is designed as a staged migration from conventional hardware to the full architecture, with no rewrite required between stages. Stage 0 is running today. **What it means.** -When every action is gate-checked, every message is provable, and every computation runs on verified semantics, security 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. +A system built this way shifts computing from an empirical trust model — "this has passed our tests" — to a deductive one: "this is structurally impossible for the following reasons." The downstream effects cascade beyond any single user: -But this is what the architecture makes possible, not what it is. What it is: a personal computing environment built on the premise that you should own your computation, your data, and your agency — and that the architecture should prove it, not promise it. +- A company's compliance obligations become a set of rules the system enforces by construction, not a binder of documents an auditor reviews once a year. +- AI safety becomes a rule system between the AI and the actions it can take, not a set of probabilities and guardrails. +- Software certification becomes a shared suite of proofs from every deployed instance — a public attestation that a system behaves as specified. + +Passepartout creates a new category: verified infrastructure. Not a safer operating system, not a better AI agent, not another social network — but the foundation beneath all three, built on a principle that the current approach cannot offer: that the system, by its structure, is trustworthy. --- -- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture]] — the architecture: environment, knowledge, verification, and their staged build-out -- [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic Effects]] — how verification cascades across society and economics -- [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Staged Roadmap]] — Stage 0 (Now) through Stage 7 (What Remains) +- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture]] — the system in detail +- [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic Effects]] — what verification cascades into +- [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Staged Roadmap]] — from today to Stage 7 diff --git a/projects/passepartout/architecture/architecture.org b/projects/passepartout/architecture/architecture.org index 1cb8dce..47b7ac6 100644 --- a/projects/passepartout/architecture/architecture.org +++ b/projects/passepartout/architecture/architecture.org @@ -22,7 +22,7 @@ Each is described below. **The environment: one address space.** -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 runs everything in a single Lisp address space. +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 runs everything in a single Lisp address space. (Lisp is a family of programming languages where code and data share the same representation. This property means the machine can verify what code does and modify itself without restarting. It is the foundation that makes the entire architecture possible.) 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 a separate process. The agent runtime invokes Lisp functions, not subprocesses. (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.) @@ -53,7 +53,7 @@ The gate is a function that takes (action, context, policy) and returns (permit The gate combines two decision layers: -1. ACL2-verified decision procedures for security-critical checks — access control, message authentication, capability resolution. These are provably correct for their domain. +1. ACL2-verified decision procedures for security-critical checks — access control, message authentication, capability resolution. (ACL2 is a theorem prover and programming language for formal verification. It proves that code behaves correctly for all possible inputs, not just the ones tested.) 2. An LLM for natural-language reasoning — parsing the user's intent, evaluating whether an action falls within policy boundaries that require human judgment. The LLM layer is probabilistic. The ACL2 layer is deductive. The gate architecture ensures the deductive layer is authoritative where it applies and the probabilistic layer is bounded by it — the LLM cannot overrule a verified denial.