amr/hermes-brain
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Reorganize brain: projects/ top level, rename filenames, update homepage

Browse Source 
- Moved everything from ideas/passepartout/ to projects/passepartout/
- Moved legal structures to projects/flags/
- Created missing _index.org files for all subdirectories
- Stripped redundant passepartout- prefix from filenames
- Rewrote root _index.org as generalized brain index (projects + concepts)
- Updated Hugo nav to Projects/Concepts
- Updated build script section descriptions
- Deleted stale ideas/passepartout-economics.md orphan
This commit is contained in:
Hermes
2026-05-24 18:54:14 +00:00
parent 4b60244919
commit 0a8e77e949
119 changed files with 177 additions and 127 deletions
Download Patch File Download Diff File Expand all files Collapse all files

30
projects/passepartout/architecture/_index.org Normal file
View File

@@ -0,0 +1,30 @@
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 5e7f1d2a-3b4c-5d6e-7f8a-9b0c1d2e3f4a
:END:
#+title: Passepartout — Architecture Section Index
#+filetags: :passepartout:index:
This section documents the Passepartout architecture: the staged build-out from conventional computing through verified infrastructure, the subsystems, and the systemic effects of verification becoming the default.
**Architecture overviews:**
- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture index]] — Passepartout architecture, market, revenue paths
- [[id:a1fac32a-47de-5fbd-b67d-29152c851747][Architecture overview]] — the three subsystems at a glance
- [[id:42c86e6f-4f27-4993-8238-b7bc7d15fb7b][Environment subsystem]] — the Lisp image, editor, browser, shell, hardware
**Staged roadmap (progressive capability layers):**
Each stage covers: what is added, what threats are eliminated, what it costs, when it is viable.
| Stage | Delivers | Key cost | Timeline |
|-------+----------+----------+----------|
| [[id:4a1f23b0-abc1-4def-9876-543210abcdef][0 — Now]] | Baseline: conventional computing | Patching treadmill, no deductive guarantees | Today |
| [[id:4a1f23b0-abc2-4def-9876-543210abcdef][1 — Social Protocol]] | Communication integrity, provable DAG | Crypto overhead, key management | Today |
| [[id:4a1f23b0-abc3-4def-9876-543210abcdef][2 — Verification]] | Verified gate, capability auth | Policy formalization burden | Today (limited) |
| [[id:4a1f23b0-abc4-4def-9876-543210abcdef][3 — Lisp Machine]] | Lisp image, Merkle memory, no kernel | Lisp tax, no backward compat, single address space | 2-5yr (soft) / 5-10yr (ASIC) |
| [[id:4a1f23b0-abc5-4def-9876-543210abcdef][4 — Inference]] | In-process LLM, token interception | ~10x compute/RAM/storage | Server now; consumer 3-5yr |
| [[id:4a1f23b0-abc6-4def-9876-543210abcdef][5 — Weights]] | Plist-native weights, weight-level provenance | ~100x GPU / ~2-5x ASIC | GPU hybrid now; ASIC 5-10yr |
| [[id:4a1f23b0-abc7-4def-9876-543210abcdef][6 — Training]] | Verified fine-tuning, neural world model | ~100x fine-tuning only | 3-5yr fine-tuning |
| [[id:4a1f23b0-abc8-4def-9876-543210abcdef][7 — Remaining]] | Physical threats, oracles, speculation, bootstrap axiom | Mitigations are non-computational | Forever |
**Systemic analysis:**
- [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic effects over time]] — how verification cascades across society, economics, and geopolitics

55
projects/passepartout/architecture/architecture.org Normal file
View File

@@ -0,0 +1,55 @@
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 1c3ec48b-446c-50d2-b53e-126a81f5143f
:ID: a1fac32a-47de-5fbd-b67d-29152c851747
:ID: 42c86e6f-4f27-4993-8238-b7bc7d15fb7b
:END:
#+title: Passepartout Architecture
#+filetags: :passepartout:architecture:economics:index:
Passepartout is a self-bootstrapping replacement for the entire personal computing stack — one project, one image, one verified memory graph. Three subsystems compose into a single system:
**Verification subsystem** — The gate stack that evaluates every proposed action against formal policy. Capability-based authorization. Combines a probabilistic LLM for natural-language reasoning with a deterministic symbolic engine (gate stack, ACL2 prover, Screamer constraint solver) for all security-critical decisions. The gate verifies shell commands, DIDComm messages, and LLM-generated action proposals through the same decision procedure.
**Environment subsystem** — The Lisp image where editor, browser, shell, and agent coexist. No separate daemons, no IPC boundaries, no trust transitions between components. One address space from which the verification subsystem checks every state mutation.
Roadmap: v2.0 Lish editor + Nyxt browser (Qt/WebKit) → v3.0+ Lisp-native layout & browser → v4.0 in-process LLM → v5.0 tagged RISC-V hardware via TinyTapeout/FPGA → v6.0 world models and true agency.
**Social protocol implementation** — Self-sovereign DID identity, DIDComm encrypted messaging, [[id:1a2b38df-20ba-58ca-ba55-a072be67bd0d][Personal Data Store]], relay network, [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][compute marketplace]], liquid democracy.
All three subsystems operate in the same Lisp address space. All three are verified by the same ACL2 prover. The gate stack that verifies a shell command also verifies a DIDComm message. The distinction between "tool" and "self" dissolves.
---
Total addressable market: ~$960B/year across cloud, AI, OS, social media, payments, productivity, and compliance.
The business model is the AWS of provable computing: AGPL infrastructure is free, revenue comes from verification appliances, gate rules, certification, namespace registry, hosted PDS, and a [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][compute marketplace]]. Network effects are positive sum — every instance feeds the regression suite and grows the marketplace.
[[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][Lisp Machine security — unified memory threat model]]
[[id:04c2f221-c54f-51e5-b40a-48822cd16d45][Common Logic (ISO 24707) — relevance to Passepartout]]
[[id:a5d59d12-b23e-58d6-a81b-9b8b06556949][Collective regression suite — how it compounds]]
Key analytical frames:
- [[id:5961e469-53a3-5f3c-ab72-3c83ef91963f][Investment thesis — the unified view]]
- [[id:9af13fff-9725-542b-93b1-a555bc74ad72][Why Lisp is economically viable now]]
- [[id:efc76898-03f7-57ba-923d-35d65da88bb7][The per-domain sufficiency flip]]
- [[id:dc2e4f22-1c4c-5d4a-a151-f96e5d3b0d70][Development velocity and timeline estimates]]
- [[id:0b5a8a74-cfd6-542d-bc88-4eb3cd8626f9][Cost structure and zero marginal cost]]
- [[id:aa6d062e-a520-5d14-8773-00687ed9c689][Competitive moats analysis]]
Revenue paths (short to long term):
- [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Verification appliance]] [[id:c34940cc-090e-57c4-8020-e78b1d32b96c][Domain gate packages]] [[id:45258a2d-1675-562c-9024-5d1eb2f1ea56][Evaluation harness]]
- [[id:2e390c1d-65f3-5fb3-b898-ac3fc4291ee7][Protocol premium usernames]] [[id:1a2b38df-20ba-58ca-ba55-a072be67bd0d][PDS as a service]] [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][Compute marketplace]]
- [[id:827bc546-e887-5b7c-9b65-6392beaf0920][Verification monopoly — the big money]] [[id:2f783eb4-638e-5afa-9b59-6224d086a712][Infrastructure lock-in]]
Strategy and IP:
- [[id:caaeee11-ba6f-5566-aecd-f171b4c459c0][Patent strategy]] [[id:67faf52f-9126-50a7-b87e-2bedc610dac7][Licensing (AGPL + commercial)]]
- [[id:5f55bbe6-d243-5766-8ccf-5c5cc88a6542][Impact on the AI/GPU industry]]
- [[id:29e4dbf3-cf19-589c-8b14-389e8a39d564][Upgrade and distribution lifecycle]]
- [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][Gate rule encoding from codified domains]]
- [[id:2afd9a3c-e96a-54c7-ac77-a05a28065b4b][Biology as proof of the Lisp model]]
- [[id:00ab3a4d-e3de-5605-a67d-12935bb36ab5][Comparison with Symbolics Genera]]
The [[id:b25bf753-9799-41ab-82f5-1a1416db756b][protocol overview]] and [[id:a3243dd0-3209-423b-98e1-51c3eada2658][advanced integration]] requirements define how Passepartout's gate stack connects to the social protocol layer. The [[id:72570648-d943-42e5-a781-3b09791ac6ec][realistic assessment]] covers deployment timelines and adoption risks.
*The lines that run the modern internet (tens of millions across Google, Meta, Amazon, Apple, Microsoft) are replaced by a single coherent architecture where one gate stack verifies everything and one prover proves everything consistent.*

108
projects/passepartout/architecture/lisp-machine-security.org Normal file
View File

@@ -0,0 +1,108 @@
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 1c95ce7d-a2db-506a-9608-df68f9ae211b
:END:
#+title: Lisp Machine Security — Unified Memory Threat Model
#+filetags: :passepartout:security:lisp-machine:pmp:isolation:
On a bare metal [[id:13e6ae54-2d24-5aa0-b1cd-a7e8e749aa70][Lisp Machine]] with a unified Lisp image, the defense-in-depth provided by the OS kernel disappears. The gate stack and the code it protects share a single address space. An attacker who exploits a memory corruption in the browser renderer can modify the gate stack's permission tables, the policy engine's state, or the ACL2 prover's decision output. There is no kernel underneath to catch them.
This note analyzes the threat model and proposes a hardware-enforced privilege separation within the single Lisp image.
**The problem**
In the conventional layered model (Linux + SBCL + [[id:28c46769-c14b-42aa-ac7a-69d310157f8f][Passepartout]]), there is defense in depth. Even if the gate stack has a bug, Linux provides seccomp, namespaces, file permissions, and process isolation as a safety net. If SBCL segfaults, the kernel catches it.
On a bare metal Lisp Machine, the model collapses:
```
Everything (agent, editor, browser, shell, gate stack, ACL2)
└── RISC-V hardware (no kernel)
```
The only protection is that the gate stack is verified by ACL2 to be correct. But ACL2 verification is static — it proves properties about source code. At runtime, a memory corruption in the same image invalidates the entire proof. "All defense is symbolic" is exactly right.
**The solution: [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware-enforced privilege zones]] within the Lisp image**
RISC-V provides three hardware privilege levels: M-mode (machine), S-mode (supervisor), and U-mode (user). Physical Memory Protection (PMP) enforces access control at the hardware bus level — it cannot be bypassed by software, even by code running in S-mode if configured in M-mode. The key: use these mechanisms to create zones within the shared Lisp address space.
**Three-layer architecture**
Layer 1 — The Gate Core (M-mode, ~500 lines of verified assembly/Lisp)
One core runs permanently in M-mode with PMP configuration that cannot be modified by any other core.
- Configures PMP at boot into three fixed zones: M-zone (gate core), S-zone (gate stack), U-zone (untrusted)
- Hashes and verifies the S-mode binary against a signed Merkle manifest before booting it
- Monitors the gate stack core via watchdog timer
- Cannot be read or written from any other privilege level
- No MMU, no interrupt handling for U-mode — just PMP + timer + sanity checking
- The absolute smallest possible trusted computing base
- Loaded from ROM with a hardware root of trust
Layer 2 — The Gate Stack (S-mode, ~2,000 lines of verified Lisp)
The ACL2 verifier, Screamer, policy engine, permission tables, and ECALL handler.
- Runs in supervisor mode with a thin kernel: just an ECALL dispatcher and a bounded memory allocator
- Its data structures (permissions table, policy objects, authentication state, hash of loaded binaries) live in S-zone memory protected by PMP
- U-mode cannot read or write S-zone — hardware enforced at every bus access
- Receives requests from U-mode exclusively through ECALL: "may I write to path X?", "should I execute command Y?", "query fact Z"
- The ECALL handler is the entire enforcement boundary — about 500 lines of Lisp that must correctly validate every request
Layer 3 — Untrusted Code (U-mode, arbitrarily large)
The LLM interface, browser renderer, Nyxt, Lish shell when executing user commands, any LLM-generated or external code.
- Lives in U-zone memory
- Cannot access S-zone or M-zone memory (PMP enforced)
- Cannot execute privileged instructions (hardware enforced)
- Can only communicate with the gate stack via ECALL — a narrow message-passing interface
- Shared heap with S-mode for GC efficiency, but PMP prevents U-mode from reading S-mode objects
**Boot chain**
1. ROM loads the M-mode gate core binary, verified by hardware signature against an eFuse key
2. Gate core configures PMP to create the three zones, protecting its own memory and the gate stack's memory
3. Gate core hashes the gate stack binary, compares against signed manifest stored in M-zone
4. Gate core loads gate stack into S-mode memory, ACL2 verifies the binary structure
5. Gate stack creates a restricted heap region for U-mode with bounds checked by PMP
6. U-mode code is loaded and started — it has no way to access S-mode or M-mode memory
**Failure mode analysis**
U-mode browser bug exploited. The attacker controls U-mode. They can call ECALL with arbitrary arguments. The gate stack verifies every ECALL. The attacker cannot read S-mode memory (PMP), cannot execute privileged instructions (hardware), cannot modify the gate stack's state (PMP). The attacker is limited to what the ECALL handler allows — which is the gate stack's policy.
ECALL handler bug. The critical vulnerability. If the ECALL handler has a buffer overflow, a parsing error, or a logic mistake in permission checking, an attacker in U-mode can trick it into granting unauthorized access. This is the single point of failure for the entire system. Mitigation: the ECALL handler must be the most rigorously verified component. ACL2 must prove its correctness for all valid and all invalid inputs. It must be minimal — no filesystem access, no networking, no string parsing beyond what's needed to validate request structure.
Gate stack accepts hostile input. U-mode sends a crafted file path designed to exploit a parsing bug in the path validator. If the gate stack has a vulnerability in its input processing logic, it can be compromised from below even though hardware isolation prevents direct memory access. Mitigation: the gate stack must treat all U-mode input as hostile. It must use bounded buffers, no recursion in parsing, and ACL2-verified parsing functions.
Speculative execution. PMP does not prevent speculative reads. A Spectre gadget in U-mode can leak S-mode memory through cache timing side channels. Mitigation: use RISC-V Zkt (constant-time) extension or disable speculation on the gate core entirely. The gate core is CPU-bound verification logic with no need for branch prediction.
DMA attack via PCIe. An attacker who compromises a network card can attempt DMA into arbitrary physical memory. IOMMU constrains DMA: devices can only write to designated I/O buffers in U-zone. Gate stack memory in S-zone is outside the IOMMU window. The IOMMU must be configured before PCIe devices are initialized.
Physical attack. Cold boot, bus probing, JTAG — all bypass PMP and IOMMU. Mitigation: memory encryption with a hardware key stored in eFuse (RISC-V Scalar Cryptography extension). Out of scope for the first iteration; the system assumes a trusted physical environment.
ACL2 trust problem. ACL2 verifies the gate stack. But ACL2 itself is ~50,000 lines of Lisp. If ACL2 has a bug, it could "prove" that an incorrect gate stack is correct. Mitigation: ACL2's proof kernel is ~1,200 lines and has been verified by ACL2 itself (the bootstrap). This is the best-known technique for prover trust, but it is not a formal proof of ACL2's correctness — faith in the bootstrap is faith in the hardware that ran it and the human who reviewed the initial seed.
**Comparison with conventional layered security**
The conventional Linux approach: TCB is ~28 million lines of C across kernel, drivers, and runtime. Defense in depth from many layers. But each layer adds attack surface.
The Lisp Machine approach: TCB is ~2,500 lines of verified Lisp (M-mode gate core + S-mode gate stack). Attack surface is ~500 lines of ECALL handler. The TCB is roughly 10,000x smaller. This security advantage creates [[id:aa6d062e-a520-5d14-8773-00687ed9c689][moats]] — a competitor would need to match both the hardware isolation and the verified codebase.
The fundamental trade: fewer layers, less depth, but each layer is simpler, smaller, and verified. A bug in the ECALL handler is catastrophic. A bug in the Linux kernel might be contained by seccomp or namespaces. The question is which is more likely: a bug in 500 lines of verified Lisp, or a bug in 28 million lines of C that is not contained by the remaining depth?
For most threat models, the Lisp Machine is more secure. The ECALL handler is a narrow, structured interface. There is no filesystem, no networking, no process management, no driver model, no /proc, no ptrace, no setuid, no namespace subsystem, no cgroups in the gate stack — each of which is a source of CVEs in Linux.
But this is a single-point-of-failure architecture. If the ECALL handler holds, the system is secure. If it breaks, everything is compromised. There is no fallback. This must be a conscious design choice, not an accident.
**Gaps in the current design**
None of this is in the architecture documents. The following are not yet specified — these architectural innovations are potential candidates for [[id:caaeee11-ba6f-5566-aecd-f171b4c459c0][patent strategy]]:
1. PMP region layout — exactly what is protected and by which region
2. ECALL handler specification — the exact interface, request types, validation logic, and error handling
3. M-mode gate core specification — what it does, how it's verified, how it loads
4. IOMMU configuration for PCIe devices
5. Watchdog strategy — what happens if the gate core freezes
6. Side-channel mitigation — speculation control, timing attacks
7. ACL2 trust documentation — the bootstrap chain and what it means for the gate stack's verification
8. The boot attestation protocol — how the gate core verifies the gate stack before loading it
9.
See the [[id:6fe67db6-25bd-4d11-bd1d-b44ec809e858][Social protocol identity specification]] for how user identity, key derivation, and DID management integrate with the gate stack's boot chain and privilege zones.
— how many cycles does an ECALL take, and does that affect the 10-80-10 ratio

16
projects/passepartout/architecture/self-driving-lisp-machine.org Normal file
View File

@@ -0,0 +1,16 @@
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 13e6ae54-2d24-5aa0-b1cd-a7e8e749aa70
:END:
#+title: The Self-Driving Lisp Machine
#+filetags: :passepartout:lisp-machine:hardware:riscv:tenstorrent:
A Tenstorrent P150 (~72 RISC-V Tensix cores) running Passepartout: 72 RISC-V cores running Lisp microcode, one core dedicated to ACL2, one to Screamer, the rest to gate verification and fact store operations.
The self-driving threshold: the system can synthesize and load its own FPGA microcode or Tensix dispatch programs from within the running Lisp image. The system profiles its own gate verification latency, proposes a new microcoded instruction for the hot path, compiles RISC-V assembly from ACL2-verified specifications, loads it via PCIe DMA from within SBCL, benchmarks it — and rolls back if slower.
Every subdomain involved is software — the most codifiable domain. RISC-V ISA, SBCL internals, ACL2 metafunctions, CIC type theory, compiler optimization — all can [[id:efc76898-03f7-57ba-923d-35d65da88bb7][flip to symbolic sufficiency]] within days to weeks of ingestion.
**Timeline:** ~6,000 lines of new code (microcode, PCIe DMA, Tensix management, benchmark harness). ~60 cycles at current velocity. 2-4 weeks. Total from today: 6-10 weeks. See [[id:dc2e4f22-1c4c-5d4a-a151-f96e5d3b0d70][time estimates]] for the velocity model behind these numbers.
The Tenstorrent approach is dramatically simpler than FPGA because the microcode is RISC-V assembly (software), not FPGA bitstream (hardware with minutes-per-iteration synthesis). The [[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][Lisp Machine security model]] — unified memory, tagged architecture, no MMU — applies directly because the Tensix cores share the same address space. [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Verification appliance]] economics apply: a certified Lisp Machine at scale replaces compliance hardware. See [[id:9af13fff-9725-542b-93b1-a555bc74ad72][why Lisp is economically viable now]] and [[id:29e4dbf3-cf19-589c-8b14-389e8a39d564][upgrade lifecycle]] for the economic and deployment foundations.

84
projects/passepartout/architecture/stage-0-now.org Normal file
View File

@@ -0,0 +1,84 @@
---
title: Stage 0 — Now (Conventional Computing)
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---
← [[id:329a30cd-55fb-496d-a60b-91388c211bba][Passepartout]] → [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]]
# Stage 0: Now
*Summary: The conventional stack as it exists today. Not a design — the starting point.*
This is the baseline we inherit. Linux on x86, C/Rust toolchain,
web-based applications, GPU compute for AI, TCP/IP networking. Every layer
is independently built and independently untrusted.
The conventional stack spans every layer:
| Layer | Threats |
|-------+---------|
| [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Hardware]] | silicon trojan, rowhammer, speculation side channels (spectre/meltdown), physical theft |
| Firmware | UEFI implants, SMM rootkits, ME backdoor — unaccountable opaque processors |
| OS kernel | privilege escalation, syscall bugs, driver exploits — CVEs weekly |
| Compiler | Ken Thompson's "Trusting Trust" — compiler backdoors invisible at source level |
| Runtime | heap corruption, use-after-free, buffer overflow — the dominant malware vector |
| Network | MITM, TLS state machine bugs, DNS poisoning, routing attacks |
| Application | XSS, SQLi, RCE, dependency chain attacks, supply chain |
| User | phishing, social engineering, credential theft |
| LLM (if present) | jailbreaks, prompt injection (unbounded space), data leakage in outputs, probabilistic unreliability |
**Key property:** Every layer is independent and untrusted. No layer can vouch
for any other. Security is *empirical* — "no bugs found in this release" — not
deductive.
## What is eliminated
Nothing. Every threat that has ever existed in computing exists at Stage 0.
## What does this cost?
- **Patching treadmill** — the industry spends uncountable hours applying CVEs.
Every OS update risks regressions. Security teams are measured by mean time
to detect, not mean time to prevent.
- **Incident response** — breaches are expected, not exceptional. The average
dwell time (attacker inside system before detection) is months.
- **Bug bounties** — a market failure tax: pay researchers to find the bugs
your toolchain inevitably produces.
- **Complexity tax** — every OS, driver, library, and daemon is a potential
entry point. The attack surface is unknowable because no layer can vouch
for any other.
- **No deductive guarantees** — security is empirical. "No bugs found in this
release" does not mean no bugs exist.
Even with all this spending, the system is not provably secure. You can't
audit your way to deductive guarantees on a conventional stack.
## What does this enable?
Everything we have. The entire software ecosystem, all hardware, every network.
The cost and the capability are the same thing — maximum flexibility, minimum
provable trust.
## When is this viable?
Today. This is where we are.
## In practice
We have normalized reactive security because the alternative — building a
provably secure stack — is considered too expensive. Every company of
meaningful size has a security team whose job is to detect when they've been
breached, not to prevent it. The average dwell time is measured in months.
This is treated as normal because the alternative — a provably secure stack —
is seen as prohibitively expensive. This roadmap is the argument that the
provable alternative is not only possible, but the inevitable destination.
The question is not whether to build it, but at what pace.
← [[id:329a30cd-55fb-496d-a60b-91388c211bba][Passepartout]] → [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc1-4def-9876-543210abcdef
:END:

85
projects/passepartout/architecture/stage-1-social-protocol.org Normal file
View File

@@ -0,0 +1,85 @@
---
title: Stage 1 - Social Protocol (In-Transit Integrity)
type: reference
tags: :passepartout:roadmap:social-protocol:
created: 2026-05-24
---
← [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Stage 0 — Now]] → [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Stage 2 — Verification]]
# Stage 1: [[id:1d074690-a279-59cb-b91d-e9a22ae104ad][Social Protocol]]
*Summary: Every message is signed, DAG-tracked, and content-addressed.
Communication becomes provable - when you choose it to be.*
## What is added
- DID-based identity per participant (Ed25519 key pairs)
- Message-level authentication via JWE/JWS envelopes
- DAG of content-addressed messages for auditable history
- Channels for directed and broadcast communication
- End-to-end encryption (Double Ratchet, MLS) with perfect forward secrecy
- Ephemeral Notes via `ephemeral_duration` (time-locked encryption, key shedding, mandatory infrastructure GC)
- Off-the-Record (OTR) mode bypassing PDS storage entirely (volatile client memory only, clients prohibited from recording)
- Pseudonymous Personas for deniable identity
- Relays as transient routers (pub/sub model, no long-term storage)
- Onion routing between PDSs for metadata masking
## What is eliminated
- **Message forgery** — every message is signed; you prove the sender
- **Message tampering in transit** — envelopes are authenticated; tampering changes the CID and breaks the chain
- **Impersonation / spoofing** — DID identity keys, not usernames
- **Replay attacks** — nonces and sequence numbers per message
- **MITM on social protocol-mediated channels** — end-to-end signatures; relays need no trust
- **Loss of message history** — DAG is append-only and content-addressed
## What does this cost?
- **Crypto overhead per message** — every message requires signing and verification.
For high-throughput channels, this adds latency and CPU cost
- **DAG storage grows unbounded** — the append-only log never shrinks unless GC
is explicitly designed
- **Key management burden** — DID resolution, key rotation, revocation. Lost keys
mean lost identity. No "reset password" for DIDs
- **No anonymous participation by default** — DIDs tie every message to a
cryptographic identity. Pseudonymity is a Persona choice, not the baseline
## What does this enable?
Provable communication infrastructure. You can prove who said what, when, and
to whom — or choose off-the-record privacy. Every subsequent stage builds on
this DAG: it is the source of truth for evidence, audit, and the accumulated
knowledge that later stages use for falsification.
## When is this viable?
Today. The social protocol is a protocol design that can be deployed on existing networks.
The infrastructure (PDS, Relay, Gateway) runs on conventional [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware]].
## In practice
Communication becomes provable - but only when the user chooses. The social protocol's Note
primitive supports the full spectrum: persistent DAG-stored messages for audit
and compliance, ephemeral Notes that self-destruct, and full Off-the-Record
(OTR) mode that bypasses PDS storage entirely.
The user chooses per-channel or per-message: permanent and attributable for
contracts and governance, ephemeral and deniable for private conversation. The
infrastructure enforces each choice - PDS garbage-collects expired CIDs, Relays
drop them from routing tables, clients shed message keys after display. The social protocol
replaces trust with evidence where evidence is wanted; elsewhere it provides
privacy by design.
The social protocol does not secure the endpoint. The machines running social protocol clients can
still be compromised at the OS, compiler, or hardware level. The keys are on
those machines - malware that compromises an endpoint can sign messages using
the endpoint's keys. The messages are authentic; the sender wasn't. The social protocol
carries the authorization; it doesn't evaluate it.
← [[id:4a1f23b0-abc1-4def-9876-543210abcdef][Stage 0 — Now]] → [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Stage 2 — Verification]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc2-4def-9876-543210abcdef
:END:

84
projects/passepartout/architecture/stage-2-verification.org Normal file
View File

@@ -0,0 +1,84 @@
---
title: Stage 2 — Verification Subsystem
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---
← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]] → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]]
# Stage 2: Verification Subsystem
*Summary: A verified gate evaluates every action against formal policy.
Capability-based authorization. "Root" as an attack target no longer exists.*
## What is added
- [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][ACL2-verified]] gate functions that evaluate every proposed action
- [[id:c34940cc-090e-57c4-8020-e78b1d32b96c][Capability-based authorization]]: every action requires a token, not an identity
- [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][Gate]] checks every action — from user, agent, or external message — against:
- Is the action authorized by policy?
- Does the capability grant this operation?
- Does the action violate any system invariant?
- Decision procedure formalized in ACL2, machine-checked
- Gate runs as a decision layer on the conventional host (Stage 0 [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware]])
## What is eliminated
- **Unauthorized actions** — even a fully compromised endpoint cannot perform an
action the gate blocks. The gate is the final arbiter, not the OS or client.
- **Privilege escalation** — no amount of subversion below the gate can grant
capabilities the policy doesn't allow. The gate checks capability tokens,
not caller identity.
- **"Root" as a meaningful attack target** — there is no root in Passepartout. There
are capabilities, and capabilities are checked.
## What does this cost?
- **Verification latency** — every action is checked against policy. Complex
policies add delay
- **Policy formalization burden** — everything must be written explicitly. Gaps
block legitimate actions (false positives) or allow undesirable ones (false
negatives). There is no [[id:4a1f23b0-abc8-4def-9876-543210abcdef][Common Sense]] fallback — the policy cannot rely on
unformalized human intuition. Everything must be written down
- **Capability management complexity** — distributing, revoking, auditing
capabilities is itself security-critical. A leaked capability is
indistinguishable from an authorized action
- **Policy drift** — as the system evolves, the policy must evolve with it.
Out-of-date policy blocks new legitimate uses
- **Proof maintenance** — the gate's decision procedure is verified, but the
policy is not. Each policy change needs new proof
- **The gate runs on untrusted hardware** — if the OS or hardware is
compromised, the gate's guarantees are meaningless. The attacker can skip
the gate or modify its output. Full gate guarantees arrive at Stage 3
## What does this enable?
The system can now say "no" to unauthorized actions even when the endpoint is
fully compromised. Security is no longer dependent on client integrity. This is
the first layer where deductive guarantees enter the picture — but they are
contingent on Stage 3's trust substrate.
## When is this viable?
Today as a software layer on conventional hardware, but with limited guarantees
(the gate itself can be compromised by the host OS). Full power arrives at
Stage 3 when the gate runs on the verified Lisp machine.
## In practice
The gate is the final arbiter, not the OS or the client. But it runs on a
machine it doesn't trust. Users must weigh the benefit (unauthorized actions
blocked) against the operational cost (everything must be explicitly authorized
in policy). For high-stakes environments, the trade-off is worth it. For casual
use, the friction may lead users to bypass the gate.
*Full gate guarantees arrive when Passepartout runs on its own Lisp machine
(Stage 3). Before that, it's a correctness proof running on an untrusted substrate.*
← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]] → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc3-4def-9876-543210abcdef
:END:

134
projects/passepartout/architecture/stage-3-lisp-machine.org Normal file
View File

@@ -0,0 +1,134 @@
---
title: Stage 3 — Lisp Machine
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---
← [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Stage 2 — Verification]] → [[id:4a1f23b0-abc5-4def-9876-543210abcdef][Stage 4 — Inference]]
# Stage 3: Lisp Machine
*Summary: The [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][verified Lisp machine]]. One image, one [[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][memory graph]], one [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][gate stack]].
No kernel, no process boundaries, no memory corruption. The verification subsystem, the environment subsystem, and the social protocol are no longer separate components — they are properties of the same machine.*
## What is added
Passepartout spans three engineering phases that converge on the same architecture:
### Phase A — Software emergence (2-3 years)
The Lisp machine emerges inside a host OS. A single SBCL image absorbs every
user interface into one address space:
- **Lish editor:** a multi-threaded Common Lisp editor via Qt/QML (EQL5).
The agent's system prompt lives in an Org buffer — visible, editable,
hot-reloadable. Org-babel for inline evaluation. The editor IS the daemon.
- **Nyxt browser:** Common Lisp web browser in three erosion stages:
Qt+WebKit → S-expression DOM → pure Lisp layout. Web content is natively
queryable and modifiable as Lisp data structures.
- **Lish shell:** text-stream replaced by plists. Pipe becomes function
composition. Scripts become Lisp functions on memory objects.
- **Emacs migration (three phases):** parasite bridge (v0.4.0) → ELisp
compatibility layer inside CL image → native CL implementations.
- **Minibuffer:** universal command surface — edit files, navigate web,
run Lisp expressions, invoke agent commands.
### Phase B — Cannibalization (3-5 years)
Gradual replacement of every external dependency with native Lisp:
- TCP bridge → internal function call (single SBCL image)
- QML layout → Lisp layout (Yoga FFI as intermediate)
- WebKit → Lisp DOM + Lisp-native layout engine
- Qt widgets → Lisp-native X11/Wayland bindings
- Font rendering → HarfBuzz FFI → Lisp replacement
- Qt event loop → SBCL native thread scheduler
- Linux bootloader → Stage0 Lisp bootstrap (500 bytes hex → self-hosting Lisp)
The system remains usable at every step. Each replacement is a component swap.
### Phase C — [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Hardware]] (5-10 years)
The dual-unit ASIC: one chip, two compute units, one Merkle-verified memory graph:
1. **Symbolic core** — tagged RISC-V (4-8 type tag bits per word, hardware
type checking, single-cycle LISP.CAR/LISP.CDR). Runs gate stack, cognitive
loop, general Lisp evaluation.
2. **Tensor unit** — cons-cell-native matrix compute. Walks the tensor DAG
directly for attention and matmul. No FFI boundary, no GPU mirror.
Prototyping: TinyTapeout (130nm, 8-bit tagged toy) → FPGA core (DE10-Nano,
VexRiscv) → FPGA tensor (Xilinx VU9P, cons-cell matmul) → shuttle (12nm,
tagged RISC-V at 100-300MHz) → ASIC (5nm, both units on die).
Phase migration: parasitic FPGA PCIe card → functional hijacking → driver
cannibalization → self-hosting (Stage0 on bare metal).
Hardware GC: dedicated Scavenger bus master runs GC in parallel with symbolic
and tensor computation. Persistent NVRAM: boot to exactly where you left off.
## What is eliminated
- **Memory corruption entirely** — verified Lisp evaluator, no undefined
behavior. No buffer overflow, use-after-free, type confusion.
- **OS kernel exploitation** — no kernel. Evaluator is the substrate. No
syscalls, no drivers, no MMU to confuse.
- **Compiler backdoors** — Lisp-to-Lisp compilation within the verified
evaluator. [[id:13e6ae54-2d24-5aa0-b1cd-a7e8e749aa70][Ken Thompson's "Trusting Trust"]] is structurally impossible.
- **Malware / viruses / worms** — no "download and execute" path that bypasses
the gate. The evaluator only runs objects in the verified memory graph.
- **Supply chain at binary level** — every object has a Merkle chain to its
origin. A dependency is a pointer, not a file.
- **The subsystem composition problem** — one address space, one
semantics, one proof. The interface between verification, environment, and
protocol is an internal relationship.
## What does this cost?
- **Lisp tax on everything** — verified execution is 2-10x slower than
optimized C on equivalent hardware. Symbolic core is designed to minimize
this; tensor unit sidesteps it for neural compute
- **No backward compatibility** — existing software doesn't run on the Lisp
machine. No Linux binaries, no x86 drivers, no GPU compute stacks (without mirror path)
- **Single address space fragility** — no process isolation. A bug in the
editor can corrupt the browser. One crash radius, one machine
- **Massive engineering investment** — shortest plausible timeline to a usable
software Lisp machine is 2-3 years; ASIC 5-10 years
- **Ecosystem abandonment** — no open-source packages, no shared libraries.
Everything is in the Merkle memory graph or it doesn't exist
## What does this enable?
Deductive security replaces empirical security. Memory bugs — the dominant
attack vector for decades — are structurally eliminated. No more patching for
CVEs. No ASLR, no DEP, no CFI — the class of attacks they mitigate doesn't
exist. Every boot is a fresh verification that the evaluator, memory graph,
and gate stack are intact.
## When is this viable?
- **Software (Phase A+B):** 2-3 years on existing hardware. Single SBCL image,
gate stack, Lish/Nyxt/Lish — usable on a developer workstation today.
- **ASIC (Phase C):** 5-10 years. FPGA prototype within 1-2 years, shuttle
within 3-5, commercial foundry 5-10.
## In practice
Memory bugs — the dominant attack vector for decades — are structurally
eliminated. No more patching for CVEs. No antivirus, no firewall (at the
machine level — network boundaries remain). A Passepartout Lisp machine that
boots correctly will not crash from a memory corruption bug, ever.
But you've given up the entire existing software world. You cannot run Firefox,
Postgres, nginx, Python, or any Linux binary. The machine is a Lisp machine
and everything must be written in Lisp. The practical trade is: absolute
memory safety at the cost of adopting an entirely new computing paradigm.
This is not an upgrade path — it is a replacement.
← [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Stage 2 — Verification]] → [[id:4a1f23b0-abc5-4def-9876-543210abcdef][Stage 4 — Inference]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc4-4def-9876-543210abcdef
:END:

95
projects/passepartout/architecture/stage-4-inference.org Normal file
View File

@@ -0,0 +1,95 @@
---
title: Stage 4 — Inference (In-Process LLM)
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---
← [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]] → [[id:4a1f23b0-abc6-4def-9876-543210abcdef][Stage 5 — Weights]]
# Stage 4: Inference
*Summary: The LLM runs in-process under the gate. Every token is inspected
during generation. No external API, no separate trust domain.*
## What is added
- CFFI binding to llama.cpp (or pure-Lisp inference engine) — LLM in the same
SBCL image as the agent, editor, and gate
- [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][Gate-level token interception]]: the Dispatcher inspects every partial token
sequence during generation. Trajectories that would produce unauthorized
actions are suppressed mid-stream, not filtered after the fact
- Weights loaded from the Lisp machine's Merkle-verified store as a macro-tag blob (one
tagged Lisp object pointing to flat binary)
- Deterministic inference: same input, same output, same hash — auditable
and replayable
*Two neural components on the same substrate:* Stage 4 hosts the LLM for
generative reasoning and action proposals. The LeCun-type world model (sensory
prediction) joins at Stage 6. Both run on the same tensor unit with the same
plist-native weight architecture and gate-level interception. The LLM proposes
actions to the gate (authorization — binary, deductive). The world model
proposes predictions to the gate (falsification — structural, empirical). The
gate handles both through different procedures.
## What is eliminated
- **LLM as a separate trust domain** — no external server, no API call, no
cloud provider to breach
- **Remote inference model attacks** — the model cannot be swapped without
changing the Merkle hash
- **Prompt injection as an action bypass** — the gate sees partial generation.
A jailbreak that would produce an unauthorized action is caught before the
tokens complete
- **Model integrity ambiguity** — you know exactly which model is running,
at which commit, with which hash
## What does this cost?
- **~10x compute, RAM, and storage** — the gate evaluates semantics at every
token, not just logits. A model running at 50 tok/s natively runs at ~5 tok/s
under gate-level interception
- **GPU/accelerator constraints** — CFFI to GPU libraries is the bottleneck.
Exotic [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware]] may not be supported
- **Memory pressure** — the LLM shares the address space with the entire system.
A 70B param model at 4-bit takes ~35GB. At 10x multiplier, effective
conventional-equivalent cost is ~350GB
- **Determinism is double-edged** — auditable but cannot adapt or creatively drift
- **No model parallelism** — Passepartout runs on one machine. Frontier-scale models
may be too large for a single address space
## What does this enable?
Action proposals from the LLM are intercepted by the gate before they reach
the system. The gate authorizes or denies in real time based on policy, not
on trust in the LLM. This eliminates the entire class of "LLM escaped its
sandbox" attacks.
## When is this viable?
- **Server hardware (A100/H100 class, 512GB+ RAM):** today. 5 tok/s on 7B
models is usable for chat
- **Consumer hardware (RTX 5090 class):** 3-5 years
- **On ASIC tensor unit:** the 10x overhead drops closer to 2-5x because the
gate runs on the symbolic core in parallel with inference on the tensor unit
## In practice
The LLM is no longer a black box connected by API. The gate watches every
token as it's generated and can stop any generation trajectory that would
produce an unauthorized action. The model is powerful; the gate is in control.
Chat is noticeably slower — roughly 5 tok/s instead of 50 — but the security
guarantee is structural, not probabilistic. For bulk processing or real-time
applications, the 10x tax may be prohibitive without dedicated acceleration.
The weights are still a verified *blob* — you know the file's hash but can't
prove anything about individual weights. Training provenance is not tracked.
The inference is FFI-mediated, so trust in llama.cpp remains.
← [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]] → [[id:4a1f23b0-abc6-4def-9876-543210abcdef][Stage 5 — Weights]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc5-4def-9876-543210abcdef
:END:

88
projects/passepartout/architecture/stage-5-weights.org Normal file
View File

@@ -0,0 +1,88 @@
---
title: Stage 5 — Weights (Plist-Native)
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---
← [[id:4a1f23b0-abc5-4def-9876-543210abcdef][Stage 4 — Inference]] → [[id:4a1f23b0-abc7-4def-9876-543210abcdef][Stage 6 — Training]]
# Stage 5: Weights
*Summary: Every weight is a [[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][Lisp object in the Merkle memory graph]]. You can
prove not just that the model file is unmodified, but that this specific
attention head has the weight vector it should have.*
## What is added
- Plist-native weight graph: weights are typed plists structured as a tree of
tensors DAG, not a flat blob
- Structural weight diffs: the response to "which weight changed?" is "layer 17,
head 3, weights 2048-4096 differ by vector V" — not "the blob hash changed"
- Weight provenance chain: the memory graph links each layer to its training
event. A structural property of the weights, not a log entry about them
- No FFI boundary for inference: the tensor unit (or GPU mirror) operates on
Lisp objects directly. The evaluator's verified semantics cover computation
## What is eliminated
- **Sub-tensor granularity tampering** — you can verify individual attention
heads, not just the blob
- **Weight provenance ambiguity** — every weight links to its origin event
- **The FFI inference gap** — inference runs on Lisp data directly. No C/GPU
code outside the evaluator's semantics
## What does this cost?
- **~100x compute, RAM, and storage on conventional [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware]] (GPU path).**
A 7B model requiring 4GB as GGUF needs ~400GB as plist-native weights on a
GPU. GPUs are built for flat arrays and SIMT; cons-cell traversal is their
worst case
- **This 100x is GPU-relative, not fundamental.** An ASIC tensor unit with
tagged memory, Merkle hashing in the memory controller, and sparse DAG-
walking matmul closes the gap to 2-5x
- **Two implementation paths:**
1. *GPU path (near-term):* plist-native weights as gold standard for
provenance, GPU-native mirror for compute, Merkle-verifiable loading
protocol. Cost: 100x storage, ~2-3x load-time overhead
2. *ASIC path (destination):* tensor unit speaks cons-cell. No mirror
needed. Cost: 2-5x over GPU for dense matmul
- **GC pressure** — plist-native weights produce enormous GC load. The
Scavenger handles this on ASIC; on GPU path the mirror avoids it
- **Mixed-precision is complex** — 4-bit and 8-bit quantization destroy
pointer structure. Full float32/64 may be the only practical option
## What does this enable?
You can prove exactly what your model is and that it hasn't been modified.
The Merkle chain from training event to individual weight is structural, not
logged. Fine-tuning provenance becomes as verifiable as the code running on
the machine. This is the stage where hardware choice determines practical
viability.
## When is this viable?
- **GPU hybrid path:** today. Works on any Passepartout with a GPU
- **ASIC native path:** 5-10 years (tensor unit on the dual-unit chip)
## In practice
Every individual weight is Merkle-verified, structurally tracked, and computed
within the Lisp evaluator's verified semantics. The FFI trust gap is closed.
Stage 5 is where hardware choice determines practical viability. The GPU path
works today but carries the storage overhead of two representations (plist gold
standard + GPU mirror) and the load-time verification cost. The ASIC path is
the destination — one representation, one chip, no workaround. Most users will
use the GPU path for years before the ASIC becomes available.
Either path is viable. The GPU path can be built today with existing hardware.
The ASIC path is the destination — a single verified chip that doesn't need
the hybrid workaround.
← [[id:4a1f23b0-abc5-4def-9876-543210abcdef][Stage 4 — Inference]] → [[id:4a1f23b0-abc7-4def-9876-543210abcdef][Stage 6 — Training]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc6-4def-9876-543210abcdef
:END:

124
projects/passepartout/architecture/stage-6-training.org Normal file
View File

@@ -0,0 +1,124 @@
---
title: Stage 6 — Training (Verified Fine-Tuning + World Model)
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---
← [[id:4a1f23b0-abc6-4def-9876-543210abcdef][Stage 5 — Weights]] → [[id:4a1f23b0-abc8-4def-9876-543210abcdef][Stage 7 — Remaining]]
# Stage 6: Training
*Summary: Verified fine-tuning under the gate. Every example checked for consent.
Every gradient application is a verified state transition. The neural world model
runs in parallel with the LLM for sensory-physical prediction.*
## What is added
### Verified fine-tuning
The training loop is not a script. It is a verified function in the evaluator:
1. Read a training example from the [[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][memory graph]]
2. Check the example's authorization tag against [[id:45ea493b-94ad-5885-aa65-0c846e5c3c1d][policy]]
3. Compute the gradient
4. Check gradient constraints (permitted weights, bounded LR, scope limits)
5. Apply the update
6. Record the state transition with a Merkle link to the input
### The neural world model (LeCun type)
A second neural network runs on the tensor unit alongside the LLM. It predicts
sensory and physical dynamics — object trajectories, scene evolution, low-level
sensor futures. It shares the same plist-native weight architecture and the
same verified training pipeline:
- **Domain:** physical world prediction (not social — that belongs to the
accumulated knowledge DAG)
- **Training:** imported from conventional [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware]]. Pretrain elsewhere,
verify import, fine-tune under gate
- **Gate interaction:** the world model proposes predictions to the gate
("the ball will land at position X"). The gate falsifies predictions against
the accumulated observation DAG after the fact, tracking calibration over
time. This is verification through falsification, not authorization
### The interaction at Stage 6
1. World model predicts sensory outcome: "user will press button in 2 seconds"
2. LLM reasons about the predicted outcome: "if user presses button, C follows"
3. LLM proposes action to gate: "preempt C"
4. Gate checks policy + accumulated knowledge for similar past scenarios
5. Gate authorizes or denies
6. After outcome occurs, gate falsifies world model's prediction against actual
observation, updating calibration score
## What is eliminated
- **Data poisoning** — every training example is authorized before gradient
application. Only data tagged with consent is trainable
- **Unauthorized fine-tuning** — training policy specifies scope (layers, LR,
data tags) and the gate enforces all constraints at every step
- **Malicious checkpoint injection** — no checkpoints. Training is a verified
sequence of continuous state transitions
- **Training-time backdoors** — the optimizer function is verified by hash.
A Trojan optimizer fails the gate check because its identity doesn't match
## What does this cost?
- **~100x slower than conventional fine-tuning** — building on Stage 5's 100x
overhead (GPU path) plus verified gate checks per example. A LoRA fine-tuning
that takes 2 hours natively takes ~200 hours. Doable overnight, not for rapid
iteration
- **Storage per training step** — every Merkle-tracked state transition adds
to the memory graph. A fine-tuning run could produce hundreds of terabytes
of deltas
- **Only fine-tuning is practical** — full pretraining on the Lisp machine never makes
sense. The 100x overhead is structural. Practical workflow: pretrain on
conventional GPU cluster → import as verified blob → convert to plist-native
under gate → fine-tune on the Lisp machine
- **Data gate latency** — every training example passes through the
authorization gate. For datasets with millions of examples, this pre-
processing step can take days
- **Wrong-spec for training policy** — the training policy is the most
security-critical spec. A compromised admin writing a policy that authorizes
all layers and all data defeats the system through its own verification
## What does this enable?
You can train on private data with proof of consent per example. The fine-tuning
history is structural, not logged — every gradient step is Merkle-linked to its
input. The world model gives the system sensorimotor common sense: object
persistence, trajectory prediction, basic physics — grounded in this specific
environment's observations.
## When is this viable?
- **Fine-tuning (GPU path):** 3-5 years on server hardware
- **World model:** same timeline — shares the pipeline and tensor unit
- **ASIC native:** when tensor unit silicon arrives (5-10 years)
## In practice
Training integrity is guaranteed at every step. Data consent is verified per
example. The optimizer cannot be swapped. Checkpoints cannot be backdoored.
But this system is not for training frontier models — it is for auditing
training runs that happen elsewhere.
The practical workflow is: pretrain on a conventional GPU cluster, import the
weights into the Lisp machine as a verified blob (Stage 4), then fine-tune on the Lisp machine
under the verified training loop. The pretraining phase remains unverified,
but the fine-tuning phase — where the model gains knowledge of private data
and user preferences — is verified. This is the pragmatic sweet spot.
The world model learns your environment's physics — how your voice sounds,
how your face moves when confused, how quickly you respond to different
message types. The gate falsifies its predictions, so the world model
converges toward accurate beliefs about your world, not the statistical
average of the internet.
← [[id:4a1f23b0-abc6-4def-9876-543210abcdef][Stage 5 — Weights]] → [[id:4a1f23b0-abc8-4def-9876-543210abcdef][Stage 7 — Remaining]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc7-4def-9876-543210abcdef
:END:

171
projects/passepartout/architecture/stage-7-remaining.org Normal file
View File

@@ -0,0 +1,171 @@
---
title: Stage 7 — What Remains
type: reference
tags: :passepartout:roadmap:
created: 2026-05-24
---
← [[id:4a1f23b0-abc7-4def-9876-543210abcdef][Stage 6 — Training]]
# Stage 7: What Remains
*Summary: At full maturity — dual-unit ASIC, plist-native weights, verified
fine-tuning, neural world model — the following irreducible threats survive.
None can be eliminated by computation alone.*
## 1. Physical threats
| Threat | Mitigation | Cost |
|--------|-----------|------|
| Theft | Tamper-resistant packaging (mesh sensors, zeroization on opening) | 10-100x packaging cost |
| EMP | Write-once checkpoint recovery | Mid-transaction data at risk |
| [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][Hardware]] trojan in fabrication | Independent fab runs + trace comparison | 2x fab cost minimum |
| Power/EM side channels | Constant-power design, shielding | Power overhead |
Physical hardening is expensive in direct proportion to the threat level.
If someone steals your Lisp machine, they have your data. Hardware hashing
and encryption slow them down, but the security boundary is now physical.
## 2. Side channels in the verified model
The system is functionally correct but may leak information through timing
channels (unless the spec explicitly models timing as an output), access-
pattern channels (verified gates enforce authorization but not non-interference),
and the crypto-verification tension (proving constant-time is a different proof
from proving functional correctness).
Closing side channels requires 2-4x the verification effort for crypto routines
and oblivious RAM overhead for memory access. Feasible for security-critical
code, impractical for the entire system. For LLM inference, this means an
attacker on the same machine could determine which tokens were generated by
measuring computation time — an open research problem.
## 3. Oracle poisoning
The system reasons perfectly about a world that may not exist:
- **Time** — a clock that can be wrong (NTP drift or attack). The machine
cannot verify which time source is correct
- **DNS / network routing** — BGP hijack reroutes traffic. Cryptographic
envelopes survive, but traffic goes to the wrong destination
- **Sensors / physical input** — the machine processes correctly; the sensor
may be compromised
- **User input** — the single most dangerous oracle. A user who authorizes a
malicious action bypasses every security guarantee. The system is secure;
the user was wrong
Oracle diversity reduces surface area but introduces Byzantine agreement
problems. The question at Stage 7 shifts from "can the attacker break the
crypto?" to "can the attacker convince the user to press the button?"
## 4. The bootstrap axiom
- **Hardware** — silicon correctness cannot be proved from within the system
- **[[id:84a537b4-4256-50c8-91f5-dd5b4538418f][ACL2 kernel]]** — ~500 lines of Lisp accepted, not proved
- **Stage-0 bootstrap** — 500-byte hex sequence, readable by a human in an
afternoon, not mechanically verified
This is the Godelian boundary of the system. Any attack that modifies the
bootstrap is undetectable from within. Detection requires physical inspection
by a trusted external party. For any real-world threat model, this is not the
weakest link — the user's Wi-Fi password is far more likely to be compromised.
## 5. The gap between specification and intent
- **Wrong spec** — the system is provably correct with respect to its formal
spec. If the spec is wrong, the system is correct and wrong
- **Incomplete invariants** — every invariant must be explicitly formalized.
There is no Common Sense fallback (see Appendix A). The most dangerous gaps are unknown ones
- **Emergent failures** — two individually correct operations can produce a
catastrophic result in combination
The verified system is perfectly correct about the wrong thing. This is the
same class of failure as "the software compiled without warnings and crashed
in production" — but instead of debugging a crash, you are debugging a formal
specification that may take weeks to analyze.
## 6. The world outside the system
- **Lying peers** — a peer with a valid DID can give dishonest answers
- **Legal compliance** — a provably correct drug transaction is still illegal
- **Coercion / duress** — the user can be compelled to authorize actions. The
gate faithfully records the authorization
These externalities cannot be addressed within the system. Any attempt (duress
mode, silent alert) expands the threat model.
## Appendix A: Common Sense
**Common sense is the set of generalized expectations about how the world works
that are not derived from specific observations within a particular system.**
That a chair is for sitting. That promises create expectations. That people
contacted at 3am are likely to be annoyed.
These are distinct from the accumulated knowledge in the [[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][Merkle DAG]], which records
specific observations. Common sense is the *generalization engine*.
**Three channels in the Passepartout architecture:**
| Channel | Origin | Verification | Granularity |
|---------|--------|-------------|-------------|
| LLM pretraining | Internet-scale corpus | None (probabilistic, distributed) | Vast but opaque |
| World model (LeCun) | Sensory observations + training | Falsified against accumulated DAG | Physical dynamics |
| Causal inference on accumulated knowledge | This system's DAG | Merkle-linked to evidence | Precise but bounded |
**The falsification loop brings common sense under gate control:**
1. LLM proposes a common-sense belief: "users don't like being contacted at 3am"
2. The world model formalizes it into a causal edge with a confidence weight
3. The gate queries the accumulated DAG: "how many 3am messages were
well-received in this user's history?"
4. If the evidence confirms, it enters the structural knowledge store
5. If contradictory, the gate rejects it and the LLM must revise
Over time, common sense that matches this specific user's world becomes
structural knowledge. The system converges toward beliefs aligned with the
user's actual environment, not the statistical average of the internet.
Common sense is never fully formalized and never fully trusted. It always
remains probabilistic, the LLM's domain, subject to falsification. The gate
does not "have" common sense. It gates access to the structural knowledge
store for beliefs that survive falsification.
## Appendix B: Summary table of eliminated threats
| Threat | Eliminated at stage |
|--------|---------------------|
| Memory corruption | 3 — Lisp Machine |
| OS exploitation | 3 — Lisp Machine |
| Malware / viruses / worms | 3 — Lisp Machine |
| Compiler backdoors | 3 — Lisp Machine |
| Message forgery / tampering | 1 — [[id:1d074690-a279-59cb-b91d-e9a22ae104ad][Social Protocol]] |
| MITM on communication | 1 — Social Protocol |
| Unauthorized actions | 2 — Gate stack (fully at 3) |
| Prompt injection bypassing gate | 4 — In-process inference |
| Weight tampering (blob level) | 4 — Verified blob hash |
| Weight tampering (fine-grained) | 5 — Plist-native weights |
| Data poisoning / unauthorized training | 6 — Verified training + world model |
| Physical theft / EMP | Survives to 7 |
| Side channels | Survives to 7 (specification gap) |
| Oracle poisoning | Survives to 7 (ground truth gap) |
| Wrong spec / human error | Survives to 7 (intent gap) |
| Bootstrap axiom | Survives to 7 (Gödelian boundary) |
| External coercion / law | Survives to 7 (not solvable by computation) |
The system ends up deductively secure inside a physically and oracularly
bounded envelope. That envelope — the chip, the world, the user — is the
only remaining attack surface worth worrying about.
Every security guarantee in this document has a price. The question is not
"is this secure?" but "is the price worth it for the threat model it
eliminates?" For a personal AI that holds private conversations and manages
keys, Stages 1-4 may be enough. For a financial system that settles billions,
Stages 5-6 justify the overhead. The progressive threat model is also a
progressive cost-benefit analysis — know the price, then decide.
← [[id:4a1f23b0-abc7-4def-9876-543210abcdef][Stage 6 — Training]]
:PROPERTIES:
:CREATED: [2026-05-24 Sun]
:ID: 4a1f23b0-abc8-4def-9876-543210abcdef
:END:

117
projects/passepartout/architecture/systemic-effects.org Normal file
View File

@@ -0,0 +1,117 @@
:PROPERTIES:
:ID: b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba
:CREATED: [2026-05-23 Sat]
:END:
#+title: Passepartout — Systemic Effects Over Time
#+filetags: :passepartout:strategy:effects:geopolitics:society:
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.
Using the [[id:2cdca4b0-6b41-44b4-acb0-af21d0e27b00][orders-of-magnitude framework]], the effects cascade across time scales. Each scale is qualitatively different, not just more of the same.
* Weeks to months — Phase Zero effects
** Scientific: verification becomes the publishing standard
Passepartout's gate rules turn every computational result into a machine-checkable proof. Papers carry proof logs, not just dataset citations. The replication crisis in compute-heavy fields (ML, climate science, genomics) meets its match — if the code doesn't verify, the result doesn't publish.
The effect compounds: proof repositories accumulate lemma libraries across fields, so each paper stands on verified shoulders, not on trust.
** Economic: the compliance industry's margins erode
The first enterprise that replaces a [[id:ed65031c-cbd2-4ad2-bd53-a67791e183cd][SOC2]] audit with a gate rule saves $500K and two weeks. The Big Four consulting revenue in GRC (governance, risk, compliance) starts eroding — first at the margins (automated control testing), then structurally (the entire audit function).
[[id:c34940cc-090e-57c4-8020-e78b1d32b96c][Gate rule packages]] sell to the same CISO who buys audit prep today. The difference: audit prep is a cost center; gate rules are an investment that compounds.
** Political: regulation becomes executable
The first regulation encoded as a gate rule sets a precedent. Regulators realize they can specify compliance in executable form rather than prose. This changes the regulator-regulated relationship from adversarial interpretation to formal specification.
A regulation that says "access logs must be tamper-proof" is a negotiation. A gate rule that enforces Merkle-chain logging is a fact. Compliance shifts from "did you follow the intent" to "does the proof pass."
* Months to years — Phase Zero scaling, early End State
** Technological: AI safety becomes engineering, not policy
The verified API gateway ([[id:ed05cab4-88e9-4e25-b7c9-346fa39c69a0][revenue hub]]) proves that AI safety is a software engineering problem, not a policy problem. Companies don't need AI regulation — they need Passepartout gate rules between the LLM and production.
This shifts the entire AI safety discourse. The question stops being "what should we ban?" and becomes "what gates should we verify?" Prompt injection, jailbreaks, data leakage, hallucination in critical paths — all become gate rule specifications, not white papers.
** Social: institutional trust gives way to computational trust
"I verified it" replaces "I trust the auditor." DIDs make platform-owned identity look like a historical anomaly. The [[id:1a2b38df-20ba-58ca-ba55-a072be67bd0d][PDS model]] makes surveillance advertising technically impossible without the user's active consent gate.
The social contract around data shifts: companies don't own user data because the architecture literally prevents them from accessing it without a permission gate. The [[id:513d5996-4ac7-4567-a992-18fc01599104][GDPR]] model (notice + consent) was a regulation trying to fix bad architecture. The PDS model is architecture that makes bad behaviour impossible.
** Cultural: verification earns cachet
The Lisp renaissance is not retro — it is the first time a language of proof carries cultural cachet outside academia. A new generation of developers grows up with verification as a default, not an afterthought.
The "move fast and break things" ethos ages overnight. In the C-suite, saying "we don't verify our deployments" becomes as embarrassing as saying "we don't test our code" was in the 2000s. The cultural shift precedes and enables the economic shift.
* Years — End State consolidates
** Economic: [[id:827bc546-e887-5b7c-9b65-6392beaf0920][the verification monopoly]]
If every transaction on the social protocol, every plugin in the environment, every gate rule passes through Passepartout's verification, then the early player collects a tax on the entire verified economy. This is the [[id:827bc546-e887-5b7c-9b65-6392beaf0920][verification monopoly]].
The $960B TAM ([[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][architecture index]]) is not aspirational — it is the cost of admission to the verified stack. Every dollar spent on cloud, AI, OS, social media, payments, and compliance eventually flows through the verification layer. The early player does not capture 100% of that, but the spread on even 5-10% is venture-scale money.
The switching cost to unverified infrastructure becomes infinite. No enterprise can justify "why would we go back to unverified code" once verification is in place. This is the [[id:2f783eb4-638e-5afa-9b59-6224d086a712][infrastructure lock-in]].
** Geopolitical: compute becomes a strategic asset
The [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][compute marketplace]] becomes a geopolitical asset on the order of SWIFT or the dollar. Whoever provisions the largest verified compute capacity becomes the default infrastructure provider for any nation that wants verified digital sovereignty.
Passepartout is inherently anti-surveillance-capitalist architecture. The PDS model does not do bulk surveillance. This makes it threatening to both:
- /Authoritarian states/ — they lose dragnet access to citizen data
- /Surveillance capitalists/ — they lose the data moat their business model depends on
The nations that adopt verified infrastructure are in one economic sphere. The nations that block it are in another. This is a new axis of the digital cold war.
** Political: liquid democracy infrastructure at scale
Verifiable proxy voting, delegation chains, quadratic funding for [[id:64708e1f-00e9-4cb7-b44b-ea0b98e5296d][public goods (Social protocol contracts)]] — these are not experiments. They become infrastructure that nation-states adopt because the alternative (unverifiable voting, opaque governance) becomes indefensible.
The effect is not that democracy becomes digital. The effect is that trust in institutions becomes a measurable property rather than a polling number. Did the government follow its own rules? The proof log says yes or no. This is the political equivalent of the scientific reproducibility shift: institutions that can produce proof logs are trusted; institutions that cannot are not.
* Generations — End State mature
** Geopolitical: the digital order is redefined
The verification network defines the digital order in the same way the internet defined the 1990s. Nations on verified infrastructure are in one economic sphere; nations that are not are in another.
Lisp Machine hardware becomes a strategic export control — like advanced semiconductors today. Passepartout is not a product category; it is infrastructure sovereignty.
** Cultural: the break-everything era becomes a historical curiosity
The "move fast and break things" era is remembered like bloodletting or lead paint. A developer who does not verify is like a civil engineer who does not do structural calculations. The entire profession shifts from "write code" to "write verified code" as the default.
The cultural residue of the unverified era (daily security patches, ransomware as an industry, "works on my machine") becomes a teaching example of how things used to be done.
** Scientific: proof libraries as shared inheritance
ACL2 proof libraries are the arxiv of verified knowledge. The accumulation of proof strategies across millions of domains — every edge case ever encountered, every lemma ever proven — becomes a shared inheritance that no single human could assemble. The system bootstraps itself into regions of proof space that no unassisted human could reach.
The frontier shifts. The question is no longer "can we verify this" but "what new things become possible when verification is free." The corollary: what new kinds of error become possible when the proof is wrong? The proof is machine-checkable; the specification is human. Specification errors become the dominant failure mode — and that is a more tractable problem than runtime bugs, because specifications can be verified against other specifications.
** Economic: the old economy becomes a historical layer
Proprietary software [[id:67faf52f-9126-50a7-b87e-2bedc610dac7][licensing]], cloud lock-in, compliance consulting, annual audit firms — these are as alien to someone born into the verified era as mainframes and COBOL are to a cloud-native developer. The new economy runs on verified infrastructure where the marginal cost of verification is zero and the switching cost to unverified infrastructure is infinite.
The insurance industry, which prices based on risk, shifts to pricing based on proof coverage. Companies with full verification pay lower premiums. Companies without it cannot get insured. This is the completion of the feedback loop: verification is not just better engineering — it is a requirement for participation in the formal economy.
* References
- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture index]] — the full Passepartout architecture
- [[id:a1fac32a-47de-5fbd-b67d-29152c851747][Architecture overview]] — the three subsystems
- [[id:ed05cab4-88e9-4e25-b7c9-346fa39c69a0][Revenue streams overview]] — economic effects quantified
- [[id:64708e1f-00e9-4cb7-b44b-ea0b98e5296d][Social protocol contracts]] — governance, insurance, liquid democracy
- [[id:827bc546-e887-5b7c-9b65-6392beaf0920][Verification monopoly]] — the big money
- [[id:2f783eb4-638e-5afa-9b59-6224d086a712][Infrastructure lock-in]] — switching costs
- [[id:2cdca4b0-6b41-44b4-acb0-af21d0e27b00][Orders of magnitude — time]] — the framework that structures this analysis
- [[id:dc2e4f22-1c4c-5d4a-a151-f96e5d3b0d70][Development timeline]] — Phase Zero vs End State mapping
- [[id:3c6b0449-a8fb-5b89-b82a-34efb21ef5b5][Compute marketplace]] — the geopolitical asset
- [[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][Lisp Machine security]] — why the architecture is anti-surveillance by design
- [[id:5f55bbe6-d243-5766-8ccf-5c5cc88a6542][AI industry impact]] — how verification changes the AI landscape