rewrite project _index.org broader intro (Environment, Knowledge, Verification); add Knowledge subsystem to architecture page

projects/passepartout/_index.org

@@ -5,48 +5,36 @@
 #+title: Passepartout
 #+filetags: :index:
 
-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.
+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.
 
-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?
+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.
 
-**One verified memory graph, from silicon to application.**
+Three subsystems compose into one system:
 
-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.
+- **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.
 
-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.
+- **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.
 
-**Why Lisp specifically.**
+- **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.
 
-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.
+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.
 
-This is not about programmer preference. It is the shortest path to a closed, verifiable semantic model at hardware granularity.
+**Why Lisp.**
 
-**Three subsystems, one address space.**
+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.
 
-The project decomposes into three subsystems that share one evaluation semantics, one memory graph, and one proof chain:
+**Why staged.**
 
-- **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.
+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.
-
-- **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.
+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.
 
-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.
+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.
 
 ---
 
-- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture]] — the architecture: verification subsystem, environment, social protocol
+- [[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)

projects/passepartout/architecture/architecture.org

@@ -7,33 +7,58 @@
 #+title: Architecture
 #+filetags: :passepartout:architecture:
 
-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.
+The project index introduces Passepartout as a personal computing environment. This page describes the architecture in detail: the four subsystems, how they compose, how the gate works, how the memex is structured, and why the stack compresses into a single address space.
 
-**The gate as the central primitive.**
+**The four subsystems, one address space.**
 
-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.
+Passepartout is one system built from four subsystems that share one evaluation semantics, one memory graph, and one proof chain:
+
+- **Environment** — the personal computing environment
+- **Knowledge** — the unified memex
+- **Verification** — the gate
+- **Social Protocol** — provable communication between instances
+
+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 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.)
+
+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. 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.
+
+**The knowledge subsystem: Org-mode as unified memex.**
+
+The knowledge subsystem makes a bet that most systems consider too expensive: that humans and machines should share the same file format. That bet is Org-mode.
+
+Most systems separate human-readable notes from machine-readable data. The user writes Markdown. The system stores it, indexes it, searches it. But the system maintains its own internal model — a database, a knowledge graph — disconnected from the Markdown. When the user leaves, the Markdown survives but the model must be reconstructed.
+
+Passepartout refuses this separation. The Org file is not a representation of the data; the Org file IS the data. The same text the user reads and edits is what the system parses and operates on. There is no translation layer between human and machine — no schema, no import/export, no API boundary between what you write and what the system knows.
+
+Sparse tree retrieval makes this efficient at scale. Org-mode's headline hierarchy is a semantic structure the system can query. When the agent needs information about a specific function, it retrieves exactly the subtree under that heading — not the entire file. Context stays lean (2,000 to 4,000 tokens) while the full knowledge base remains accessible through structural retrieval. This is fundamentally different from Markdown, where retrieval is either imprecise (grep) or entire-file (expensive).
+
+The knowledge subsystem maintains two indices over the Org prose:
+
+1. A neural index using vector embeddings for semantic search — the gateway to the full richness of natural language.
+2. A symbolic index storing formal assertions about what the prose says — predicates, relations, constraints — each grounded to a specific heading or block.
+
+The prose is always ground truth. Both indices are derived views that can be rebuilt from scratch. Nothing is lost in the indices that was not already in the Org files.
+
+This is what sovereignty means in technical terms: the user owns the data in a format they can access, and the system operates on the data in the same format they own. The format is stable — Org-mode has been in active development since 2003. There is no schema migration, no database upgrade, no vendor lock-in. Your notes survive the system.
+
+**The verification subsystem: the gate.**
+
+The gate is 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. Root is not a concept in the gate model — root is a convention enforced by an OS that the gate replaces.
 
 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.
 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 that the deductive layer is authoritative where it applies and the probabilistic layer is bounded by it — the LLM cannot overrule a verified denial.
+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.
 
-**The environment subsystem: one address space.**
+The gate does not depend on OS privilege boundaries because it is in the evaluation loop itself. This is the architectural reason for the Lisp machine: a conventional OS interposes between the gate and the hardware. A Lisp machine eliminates that interposition by making the gate part of the evaluator.
-
-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.
-
-What this means concretely:
-
-- 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.
-
-(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.)
-
-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.
 
 **The social protocol: provable communication.**
 
@@ -43,12 +68,12 @@ The social protocol extends the verified semantics beyond a single machine. It p
 - 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)
+- Compute marketplace (provision verified compute you rent)
 - Liquid democracy (delegable voting over protocol governance)
 
 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 social protocol is not a blockchain. DAG-based ordering handles causality; delegable trust replaces proof of work.
 
 **The staged progression.**
 
@@ -57,11 +82,11 @@ The full architecture — gate-verified Lisp machine on custom silicon — is th
 - 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 3: The host OS is replaced by a bare-metal Lisp image. 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 4: LLM inference moves into the Lisp process. No API calls across network boundaries. 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 5: Neural weights 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 6: Verified fine-tuning. Every weight update is gate-checked against policy.
-- 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.
+- Stage 7: What remains. Physical theft, electronic warfare, holes in the specification itself, and the fallibility of the LLM oracle. 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.
 
@@ -72,4 +97,4 @@ When every action is gate-checked, every message is provable, and every computat
 - **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.
+- **Operating systems** become obsolete. The gate replaces the kernel, the address space replaces process isolation, and the verified evaluator replaces the privilege model.