Stages: rename titles, fix execution order, remove all numbered references
This commit is contained in:
@@ -40,7 +40,7 @@ This eliminates entire categories of threats by structural design, not by patchi
|
|||||||
|
|
||||||
**How we get there.**
|
**How we get there.**
|
||||||
|
|
||||||
The full system is the destination, but every intermediate stage delivers value on its own. The project is designed as a staged migration from conventional hardware to the full architecture, with no rewrite required between stages. Stage 0 is running today.
|
The full system is the destination, but every intermediate stage delivers value on its own. The project is designed as a staged migration from conventional hardware to the full architecture, with no rewrite required between stages. Development is running today.
|
||||||
|
|
||||||
**What it means.**
|
**What it means.**
|
||||||
|
|
||||||
@@ -56,4 +56,4 @@ Passepartout creates a new category: verified infrastructure. Not a safer operat
|
|||||||
|
|
||||||
- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture]] — the system in detail
|
- [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][Architecture]] — the system in detail
|
||||||
- [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic Effects]] — what verification cascades into
|
- [[id:b9fa4b7b-bc61-4d7f-918d-ff687b80f2ba][Systemic Effects]] — what verification cascades into
|
||||||
- [[id:8cb760e2-37c6-4a78-af4d-f89f69d1678b][Staged Roadmap]] — from today to Stage 7
|
- [[id:8cb760e2-37c6-4a78-af4d-f89f69d1678b][Staged Roadmap]] — from today to What Remains
|
||||||
|
|||||||
@@ -84,7 +84,7 @@ Blind spot 2 — the kernel prevents the action before the gate sees it. If the
|
|||||||
|
|
||||||
Without these mitigations, the gate's coverage converges to a plateau determined only by what has already broken, leaving large regions permanently dependent on the LLM's probabilistic reliability.
|
Without these mitigations, the gate's coverage converges to a plateau determined only by what has already broken, leaving large regions permanently dependent on the LLM's probabilistic reliability.
|
||||||
|
|
||||||
**Gate decision flow (Stage 2):** An action arrives carrying a domain tag. First, the gate checks the deductive layer — does this domain have registered ACL2-verified boundary procedures? If any denies, reject instantly. The LLM cannot overrule. If no verified procedure denies, the gate checks with Screamer — a constraint network built from rules extracted by the LLM and corrected by humans. Screamer resolves domain-specific constraints, rights, and prohibitions. If Screamer finds a resolution, apply it. If not, the gate asks the LLM. The LLM proposes permit or deny, and the gate re-checks against the deductive boundaries (defense in depth). Every decision is logged to the decision log.
|
**Gate decision flow (Neurosymbolic Agent stage):** An action arrives carrying a domain tag. First, the gate checks the deductive layer — does this domain have registered ACL2-verified boundary procedures? If any denies, reject instantly. The LLM cannot overrule. If no verified procedure denies, the gate checks with Screamer — a constraint network built from rules extracted by the LLM and corrected by humans. Screamer resolves domain-specific constraints, rights, and prohibitions. If Screamer finds a resolution, apply it. If not, the gate asks the LLM. The LLM proposes permit or deny, and the gate re-checks against the deductive boundaries (defense in depth). Every decision is logged to the decision log.
|
||||||
|
|
||||||
**How domains emerge:** Domain tags are not assigned upfront. The user writes notes in Org. The symbolic index extracts entities and relationships. Screamer's constraint network connects them. Over time, clusters form — entities that mention each other frequently and mention outside entities rarely. The gate notices clusters where LLM utilization is high. It asks the LLM to label them: "This cluster deals with financial records. Shall I create a domain called accounting?" If the user confirms, the procedure registry gets a new tag. New domains start empty — no verified boundaries — and fill as mistakes accumulate.
|
**How domains emerge:** Domain tags are not assigned upfront. The user writes notes in Org. The symbolic index extracts entities and relationships. Screamer's constraint network connects them. Over time, clusters form — entities that mention each other frequently and mention outside entities rarely. The gate notices clusters where LLM utilization is high. It asks the LLM to label them: "This cluster deals with financial records. Shall I create a domain called accounting?" If the user confirms, the procedure registry gets a new tag. New domains start empty — no verified boundaries — and fill as mistakes accumulate.
|
||||||
|
|
||||||
@@ -132,11 +132,11 @@ The social protocol is not a blockchain. DAG-based ordering handles causality; d
|
|||||||
|
|
||||||
The full architecture — gate-verified Lisp machine on custom silicon — is the destination. The staged roadmap (see the [[file:/stages.org][stages]] directory for full detail) describes how each successive replacement eliminates a class of threat:
|
The full architecture — gate-verified Lisp machine on custom silicon — is the destination. The staged roadmap (see the [[file:/stages.org][stages]] directory for full detail) describes how each successive replacement eliminates a class of threat:
|
||||||
|
|
||||||
Stage 0 (Now: Linux + Python agent + SQLite), Stage 1 (Neurosymbolic Agent: the gate — root eliminated, provenance store operational), Stage 2 (Lisp Machine: bare-metal — no MMU), Stage 3 (AI Inference: in-process LLM), Stage 4 (Social Protocol: provable communication), Stage 5 (AI Weights: plist-native neural data), Stage 6 (AI Training: verified fine-tuning), Stage 7 (What Remains — physical, political, oracular limits).
|
Development (baseline: Linux + Python agent + SQLite), Neurosymbolic Agent (the gate — root eliminated, provenance store operational), Social Protocol (provable communication), Lisp Machine (bare-metal — no MMU), AI Inference (in-process LLM), AI Weights (plist-native neural data), AI Training (verified fine-tuning), What Remains (physical, political, oracular limits).
|
||||||
|
|
||||||
Each stage is independently useful. Stage 0 is running today. The migration is progressive component swap, not a cut-over.
|
Each stage is independently useful. Development is running today. The migration is progressive component swap, not a cut-over.
|
||||||
|
|
||||||
**Self-developing hardware (Stage 3+):** The hardware side of the Lisp Machine self-improves by synthesizing its own microcode. A Tenstorrent P150 (~72 RISC-V Tensix cores) runs Lisp microcode with one core dedicated to ACL2, one to Screamer, and the rest to gate verification and fact store operations. 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. The self-driving threshold: every subdomain involved (RISC-V ISA, SBCL internals, ACL2 metafunctions, compiler optimization) is software — the most codifiable domain — and can flip to symbolic sufficiency within days of ingestion.
|
**Self-developing hardware (Lisp Machine onwards):** The hardware side of the Lisp Machine self-improves by synthesizing its own microcode. A Tenstorrent P150 (~72 RISC-V Tensix cores) runs Lisp microcode with one core dedicated to ACL2, one to Screamer, and the rest to gate verification and fact store operations. 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. The self-driving threshold: every subdomain involved (RISC-V ISA, SBCL internals, ACL2 metafunctions, compiler optimization) is software — the most codifiable domain — and can flip to symbolic sufficiency within days of ingestion.
|
||||||
|
|
||||||
**Downstream effects.**
|
**Downstream effects.**
|
||||||
|
|
||||||
|
|||||||
@@ -62,7 +62,7 @@ Both prove the viability of the autonomous loop concept but use the weakest poss
|
|||||||
|
|
||||||
| Researcher | Institution | System | Match | Divergence |
|
| Researcher | Institution | System | Match | Divergence |
|
||||||
|------------|-------------|--------|-------|------------|
|
|------------|-------------|--------|-------|------------|
|
||||||
| Richard Sutton | Alberta / Keen Technologies | TD learning, eligibility traces, Alberta Plan | The fundamental problem in verification — *an action was checked, but the consequence plays out hours later; was the action correct?* — is the same problem TD learning solves in RL: assigning credit to actions based on delayed outcomes. Sutton's temporal credit assignment work is the theory you would need to extend Passepartout from per-action gates to trajectory-level verification. His Bitter Lesson (scale beats engineered knowledge at sufficient compute) is the most commonly cited argument against the symbolic verification approach Passepartout bets on. | The Bitter Lesson is not anti-knowledge — it says methods that improve with more computation eventually dominate. Passepartout's gate is a deliberately small engineered knowledge system that *won't* benefit from more compute (the ACL2 lemmas don't get more correct with more hardware). That's acceptable because the gate is a narrow bottleneck (permit/deny). The LLM layer inside the gate *does* benefit from scale. The architecture already respects the Bitter Lesson by placing the scalable piece where scale helps and the non-scalable piece where deductive certainty matters. Sutton's Alberta Plan (world model + reward + learning algorithm) parallels Passepartout's Stage 6 (world model + gate + verified fine-tuning), but Sutton's agents learn by pure reward while Passepartout's learn by reward constrained by verified policy. Sutton would likely argue that a learned safety policy at scale would outcompete the gate. Passepartout's bet is that access control, message authentication, and compliance should never be probabilistic, even at infinite scale.
|
| Richard Sutton | Alberta / Keen Technologies | TD learning, eligibility traces, Alberta Plan | The fundamental problem in verification — *an action was checked, but the consequence plays out hours later; was the action correct?* — is the same problem TD learning solves in RL: assigning credit to actions based on delayed outcomes. Sutton's temporal credit assignment work is the theory you would need to extend Passepartout from per-action gates to trajectory-level verification. His Bitter Lesson (scale beats engineered knowledge at sufficient compute) is the most commonly cited argument against the symbolic verification approach Passepartout bets on. | The Bitter Lesson is not anti-knowledge — it says methods that improve with more computation eventually dominate. Passepartout's gate is a deliberately small engineered knowledge system that *won't* benefit from more compute (the ACL2 lemmas don't get more correct with more hardware). That's acceptable because the gate is a narrow bottleneck (permit/deny). The LLM layer inside the gate *does* benefit from scale. The architecture already respects the Bitter Lesson by placing the scalable piece where scale helps and the non-scalable piece where deductive certainty matters. Sutton's Alberta Plan (world model + reward + learning algorithm) parallels Passepartout's AI Training stage (world model + gate + verified fine-tuning), but Sutton's agents learn by pure reward while Passepartout's learn by reward constrained by verified policy. Sutton would likely argue that a learned safety policy at scale would outcompete the gate. Passepartout's bet is that access control, message authentication, and compliance should never be probabilistic, even at infinite scale.
|
||||||
|
|
||||||
**Integrate-Symbolic-Into-Neural (Garcez)**
|
**Integrate-Symbolic-Into-Neural (Garcez)**
|
||||||
|
|
||||||
|
|||||||
@@ -98,7 +98,7 @@ The P150 is the system's peripheral nervous system — always-on monitoring behi
|
|||||||
| 2x RTX 3090 | Fast LLM inference |
|
| 2x RTX 3090 | Fast LLM inference |
|
||||||
| EPYC (main cores) | ACL2, Screamer, PDS, Gate orchestration |
|
| EPYC (main cores) | ACL2, Screamer, PDS, Gate orchestration |
|
||||||
| P150 | Always-on temporal awareness, parallel constraint search, fact store indexing, anomaly detection |
|
| P150 | Always-on temporal awareness, parallel constraint search, fact store indexing, anomaly detection |
|
||||||
| FPGA (future) | Stage 3 Lisp Machine (tagged memory, hardware GC) |
|
| FPGA (future) | Lisp Machine (tagged memory, hardware GC) |
|
||||||
|
|
||||||
**Temporal awareness: explicit vs ambient**
|
**Temporal awareness: explicit vs ambient**
|
||||||
|
|
||||||
|
|||||||
@@ -43,7 +43,7 @@ A single primitive — the Note — serves as message, document, contract, vote,
|
|||||||
|
|
||||||
**9. Staged progression 0→7**
|
**9. Staged progression 0→7**
|
||||||
|
|
||||||
Each stage is independently useful and fully functional. Stage 0 (current) runs conventional Linux with Hermes and gbrain. Stage 7 is custom silicon with the full verified stack. The migration is progressive component swap, not a cut-over. See [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][architecture.org]] and [[id:5e7f1d2a-3b4c-5d6e-7f8a-9b0c1d2e3f4a][_index.org]] for the full roadmap.
|
Each stage is independently useful and fully functional. Development (current) runs conventional Linux with Hermes and gbrain. What Remains is custom silicon with the full verified stack. The migration is progressive component swap, not a cut-over. See [[id:1c3ec48b-446c-50d2-b53e-126a81f5143f][architecture.org]] and [[id:5e7f1d2a-3b4c-5d6e-7f8a-9b0c1d2e3f4a][_index.org]] for the full roadmap.
|
||||||
|
|
||||||
**10. Self-modification / hot-reload (the autodidactic loop)**
|
**10. Self-modification / hot-reload (the autodidactic loop)**
|
||||||
|
|
||||||
@@ -53,9 +53,9 @@ Because code and data share the same representation in a Lisp address space, the
|
|||||||
|
|
||||||
Symbolic reasoning is typically expensive (knowledge engineering, ontology maintenance). Passepartout inverts this: the LLM generates symbolic assertions cheaply, the Gate verifies them deductively, and the Org source stores them as a human-readable byproduct. The expensive part becomes the verification, which compounds with every use. See [[id:0a33bd83-ff3c-4eac-bc97-83eb6702051a][design-decisions.org]] for the token economics analysis.
|
Symbolic reasoning is typically expensive (knowledge engineering, ontology maintenance). Passepartout inverts this: the LLM generates symbolic assertions cheaply, the Gate verifies them deductively, and the Org source stores them as a human-readable byproduct. The expensive part becomes the verification, which compounds with every use. See [[id:0a33bd83-ff3c-4eac-bc97-83eb6702051a][design-decisions.org]] for the token economics analysis.
|
||||||
|
|
||||||
**12. Potential revenue streams from Stage 1**
|
**12. Potential revenue streams from the Social Protocol**
|
||||||
|
|
||||||
The social protocol (Stage 1) enables paid services before the full stack is built — DID registration, relay node operation, PDS hosting, compute marketplace fees. Revenue starts flowing before the Gate exists as a software layer. See [[id:5e7f1d2a-3b4c-5d6e-7f8a-9b0c1d2e3f4a][_index.org]] for the full TAM analysis.
|
The social protocol enables paid services before the full stack is built — DID registration, relay node operation, PDS hosting, compute marketplace fees. Revenue starts flowing before the Gate exists as a software layer. See [[id:5e7f1d2a-3b4c-5d6e-7f8a-9b0c1d2e3f4a][_index.org]] for the full TAM analysis.
|
||||||
|
|
||||||
**13. Dual growth strategies: social + institutional**
|
**13. Dual growth strategies: social + institutional**
|
||||||
|
|
||||||
|
|||||||
@@ -124,7 +124,7 @@ The provenance store must be populated with validated data before it can enforce
|
|||||||
|
|
||||||
3. **Validation through use.** Every time the system runs a computation and receives experimental feedback (or the user provides a measurement), the comparison is recorded. Disagreements between prediction and measurement trigger parameter updates. Over hundreds of comparisons, the provenance store's confidence intervals tighten.
|
3. **Validation through use.** Every time the system runs a computation and receives experimental feedback (or the user provides a measurement), the comparison is recorded. Disagreements between prediction and measurement trigger parameter updates. Over hundreds of comparisons, the provenance store's confidence intervals tighten.
|
||||||
|
|
||||||
4. **Community amplification (Stage 1+).** Through the social protocol, instances share validated parameter sets with provenance chains. A force field validated by one instance for ethanol and another for DMSO accumulates a broader validity envelope than either alone. The network effect compounds the cold-start investment.
|
4. **Community amplification (Social Protocol onwards).** Through the social protocol, instances share validated parameter sets with provenance chains. A force field validated by one instance for ethanol and another for DMSO accumulates a broader validity envelope than either alone. The network effect compounds the cold-start investment.
|
||||||
|
|
||||||
The cold start never reaches the same confidence as a mature instance with years of experimental feedback. But even a seeded provenance store with provisional parameters is strictly better than a system with no provenance — because the provisional parameters are explicitly tagged as provisional, and the user can see the confidence for every result rather than trusting a single unmarked number.
|
The cold start never reaches the same confidence as a mature instance with years of experimental feedback. But even a seeded provenance store with provisional parameters is strictly better than a system with no provenance — because the provisional parameters are explicitly tagged as provisional, and the user can see the confidence for every result rather than trusting a single unmarked number.
|
||||||
|
|
||||||
@@ -132,15 +132,15 @@ The cold start never reaches the same confidence as a mature instance with years
|
|||||||
|
|
||||||
The knowledge-layers infrastructure is staged, not all-at-once:
|
The knowledge-layers infrastructure is staged, not all-at-once:
|
||||||
|
|
||||||
- **Stage 0 (current).** The probabilistic oracle exists (the LLM). The provenance store does not. The deductive engine partially exists through Hermes skills (symbolic gate rules as Python, not ACL2). The empirical layer is invisible — the LLM reasons about chemistry, biology, and engineering using training data alone, without systematic provenance.
|
- **Development (current).** The probabilistic oracle exists (the LLM). The provenance store does not. The deductive engine partially exists through Hermes skills (symbolic gate rules as Python, not ACL2). The empirical layer is invisible — the LLM reasons about chemistry, biology, and engineering using training data alone, without systematic provenance.
|
||||||
|
|
||||||
- **Stage 1 (social protocol).** The provenance store prototype can be introduced as a side effect of signed messages and data exchange. When instances share a validated parameter set, the message carries a signature and source. The receiving instance stores it with provenance. Natural crawl before full infrastructure.
|
- **Social Protocol (social protocol).** The provenance store prototype can be introduced as a side effect of signed messages and data exchange. When instances share a validated parameter set, the message carries a signature and source. The receiving instance stores it with provenance. Natural crawl before full infrastructure.
|
||||||
|
|
||||||
- **Stage 2 (gate as software).** The provenance store becomes operational infrastructure. The gate checks scientific validity alongside security policy. The provenance store integrates with the Knowledge subsystem as a structured data store — the symbolic index holds formal facts; the provenance store holds empirical parameters. Same storage mechanism, different data type.
|
- **Neurosymbolic Agent (gate as software).** The provenance store becomes operational infrastructure. The gate checks scientific validity alongside security policy. The provenance store integrates with the Knowledge subsystem as a structured data store — the symbolic index holds formal facts; the provenance store holds empirical parameters. Same storage mechanism, different data type.
|
||||||
|
|
||||||
- **Stage 3 (Lisp machine).** The symbolic engine is native in one address space. ACL2 runs at hardware level. The provenance store becomes a native Lisp hash table with persistence. The gate checks validity predicates in the evaluation loop itself. The LLM proposes model selections; every proposal is verified against the provenance store before execution. All three layers in one address space.
|
- **Lisp Machine (Lisp machine).** The symbolic engine is native in one address space. ACL2 runs at hardware level. The provenance store becomes a native Lisp hash table with persistence. The gate checks validity predicates in the evaluation loop itself. The LLM proposes model selections; every proposal is verified against the provenance store before execution. All three layers in one address space.
|
||||||
|
|
||||||
- **Stage 4+ (in-process inference).** The LLM moves in-process. All three components share one address space. No IPC between them. The query cycle is: LLM proposes → symbolic engine checks against provenance store → if valid, execute → if invalid, return to LLM with diagnostic. This loop runs at native speed.
|
- **AI Inference onwards (in-process inference).** The LLM moves in-process. All three components share one address space. No IPC between them. The query cycle is: LLM proposes → symbolic engine checks against provenance store → if valid, execute → if invalid, return to LLM with diagnostic. This loop runs at native speed.
|
||||||
|
|
||||||
* What This Changes in the Architecture
|
* What This Changes in the Architecture
|
||||||
|
|
||||||
|
|||||||
@@ -109,13 +109,13 @@ All three are handled by the same provenance store, the same gate predicates, an
|
|||||||
|
|
||||||
**Where this fits in the stage plan.**
|
**Where this fits in the stage plan.**
|
||||||
|
|
||||||
- **Stage 0-1**: The provenance store does not exist. Neural network models are loaded as black boxes with no systematic validity checking. This is current practice in computational science — the user is responsible for knowing whether a model applies to their problem.
|
- **Development to Neurosymbolic Agent**: The provenance store does not exist. Neural network models are loaded as black boxes with no systematic validity checking. This is current practice in computational science — the user is responsible for knowing whether a model applies to their problem.
|
||||||
|
|
||||||
- **Stage 2**: The provenance store begins operation. Initially it handles traditional symbolic-fitted models because they have clear provenance chains and validity envelopes. Neural network models require the distribution match infrastructure, which is a separate development track.
|
- **Social Protocol**: The provenance store begins operation. Initially it handles traditional symbolic-fitted models because they have clear provenance chains and validity envelopes. Neural network models require the distribution match infrastructure, which is a separate development track.
|
||||||
|
|
||||||
- **Stage 3**: The distribution match infrastructure is operational. The gate can check whether an input is within a neural network's training distribution. The provenance store holds training dataset descriptions, validation benchmarks, and distribution summary statistics for each supported neural network model.
|
- **Lisp Machine**: The distribution match infrastructure is operational. The gate can check whether an input is within a neural network's training distribution. The provenance store holds training dataset descriptions, validation benchmarks, and distribution summary statistics for each supported neural network model.
|
||||||
|
|
||||||
- **Stage 4+**: Neural network models are loaded into the same address space as the symbolic engine and the provenance store. The distribution match check runs at the level of the evaluation loop itself. The gate's validity check becomes a fast native predicate — no querying a separate data store, just reading a hash table and computing a distance in the same process.
|
- **AI Inference onwards**: Neural network models are loaded into the same address space as the symbolic engine and the provenance store. The distribution match check runs at the level of the evaluation loop itself. The gate's validity check becomes a fast native predicate — no querying a separate data store, just reading a hash table and computing a distance in the same process.
|
||||||
|
|
||||||
**The summary.**
|
**The summary.**
|
||||||
|
|
||||||
|
|||||||
@@ -53,14 +53,14 @@ The first release ships spec-compliant behavior via battle-tested C/Rust impleme
|
|||||||
| BIP derivation | Sidecar script or CFFI → libbitcoin | cl-bip |
|
| BIP derivation | Sidecar script or CFFI → libbitcoin | cl-bip |
|
||||||
| JOSE envelopes | CFFI → libjose or OpenSSL CMS | cl-jose |
|
| JOSE envelopes | CFFI → libjose or OpenSSL CMS | cl-jose |
|
||||||
|
|
||||||
Each replacement is independent and non-blocking. The gate (Stage 2) can verify sidecar responses against policy while the library is still a black box.
|
Each replacement is independent and non-blocking. The gate (Neurosymbolic Agent stage) can verify sidecar responses against policy while the library is still a black box.
|
||||||
|
|
||||||
## Key principle
|
## Key principle
|
||||||
|
|
||||||
Published specs → separate library. Internal design choices → stay in the PDS repo until a second consumer appears.
|
Published specs → separate library. Internal design choices → stay in the PDS repo until a second consumer appears.
|
||||||
|
|
||||||
→ SaaS Architecture
|
→ SaaS Architecture
|
||||||
→ Stage 1 — Social Protocol
|
→ Social Protocol
|
||||||
|
|
||||||
:PROPERTIES:
|
:PROPERTIES:
|
||||||
:CREATED: [2026-05-11 Mon]
|
:CREATED: [2026-05-11 Mon]
|
||||||
|
|||||||
@@ -3,7 +3,7 @@
|
|||||||
:WEIGHT: 10
|
:WEIGHT: 10
|
||||||
:ID: 8cb760e2-37c6-4a78-af4d-f89f69d1678b
|
:ID: 8cb760e2-37c6-4a78-af4d-f89f69d1678b
|
||||||
:END:
|
:END:
|
||||||
#+title: Stage 0: Now
|
#+title: Development
|
||||||
#+filetags: :passepartout:architecture:stages:roadmap:
|
#+filetags: :passepartout:architecture:stages:roadmap:
|
||||||
|
|
||||||
The staged roadmap for Passepartout — from current conventional computing through the full self-improving Lisp machine vision. Each stage is independently useful and the migration is progressive component swap, not a cut-over.
|
The staged roadmap for Passepartout — from current conventional computing through the full self-improving Lisp machine vision. Each stage is independently useful and the migration is progressive component swap, not a cut-over.
|
||||||
@@ -11,15 +11,15 @@ The staged roadmap for Passepartout — from current conventional computing thro
|
|||||||
**The stages at a glance:**
|
**The stages at a glance:**
|
||||||
|
|
||||||
| Stage | What changes | Threat eliminated |
|
| Stage | What changes | Threat eliminated |
|
||||||
|---|---|---|
|
|---|----------|-------------------|
|
||||||
| 0: Now | Linux + Python agent + SQLite (current) | None — starting point |
|
| Development | Linux + Python agent + SQLite (current) | None — starting point |
|
||||||
| 1: Neurosymbolic Agent | The gate — ACL2-verified decision procedures, provenance store, validity envelope predicates | Root as attack path, unverified empirical claims |
|
| Neurosymbolic Agent | The gate — ACL2-verified decision procedures, provenance store, validity envelope predicates | Root as attack path, unverified empirical claims |
|
||||||
| 2: Lisp Machine | Bare-metal Lisp image, one address space | MMU boundary, process isolation |
|
| Social Protocol | DID identity, encrypted messaging, data stores | Unauthenticated communication |
|
||||||
| 3: AI Inference | In-process LLM inference | API call interception |
|
| Lisp Machine | Bare-metal Lisp image, one address space | MMU boundary, process isolation |
|
||||||
| 4: Social Protocol | DID identity, encrypted messaging, data stores | Unauthenticated communication |
|
| AI Inference | In-process LLM inference | API call interception |
|
||||||
| 5: AI Weights | Neural weights as plist-native data | Symbolic/neural representation gap |
|
| AI Weights | Neural weights as plist-native data | Symbolic/neural representation gap |
|
||||||
| 6: AI Training | Verified fine-tuning, gate-checked weight updates | Unsanctioned model mutation |
|
| AI Training | Verified fine-tuning, gate-checked weight updates | Unsanctioned model mutation |
|
||||||
| 7: What Remains | Physical, political, oracular limits | (No computational threat remains) |
|
| What Remains | Physical, political, oracular limits | (No computational threat remains) |
|
||||||
|
|
||||||
*Summary: The conventional stack as it exists today. Not a design — the starting point.*
|
*Summary: The conventional stack as it exists today. Not a design — the starting point.*
|
||||||
|
|
||||||
@@ -46,7 +46,7 @@ The conventional stack spans every layer:
|
|||||||
for any other. Security is *empirical* — "no bugs found in this release" — not
|
for any other. Security is *empirical* — "no bugs found in this release" — not
|
||||||
deductive.
|
deductive.
|
||||||
|
|
||||||
**What is eliminated:** Nothing. Every threat that has ever existed in computing exists at Stage 0.
|
**What is eliminated:** Nothing. Every threat that has ever existed in computing exists at this stage.
|
||||||
|
|
||||||
**What does this cost:**
|
**What does this cost:**
|
||||||
- Patching treadmill — the industry spends uncountable hours applying CVEs. Every OS update risks regressions.
|
- Patching treadmill — the industry spends uncountable hours applying CVEs. Every OS update risks regressions.
|
||||||
|
|||||||
@@ -5,8 +5,8 @@ tags: :passepartout:roadmap:
|
|||||||
created: 2026-05-24
|
created: 2026-05-24
|
||||||
---
|
---
|
||||||
|
|
||||||
← [[id:8cb760e2-37c6-4a78-af4d-f89f69d1678b][Stage 0: Now]] → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]]
|
← [[id:8cb760e2-37c6-4a78-af4d-f89f69d1678b][Development]] → [[id:1d074690-a279-59cb-b91d-e9a22ae104ad][Social Protocol]]
|
||||||
# Stage 2: Verification Subsystem
|
# Neurosymbolic Agent
|
||||||
|
|
||||||
*Summary: A verified gate evaluates every action against formal policy.
|
*Summary: A verified gate evaluates every action against formal policy.
|
||||||
Capability-based authorization. "Root" as an attack target no longer exists.*
|
Capability-based authorization. "Root" as an attack target no longer exists.*
|
||||||
@@ -20,7 +20,7 @@ Capability-based authorization. "Root" as an attack target no longer exists.*
|
|||||||
- Does the capability grant this operation?
|
- Does the capability grant this operation?
|
||||||
- Does the action violate any system invariant?
|
- Does the action violate any system invariant?
|
||||||
- Decision procedure formalized in ACL2, machine-checked
|
- 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]])
|
- Gate runs as a decision layer on the conventional Development-stage host [[id:84a537b4-4256-50c8-91f5-dd5b4538418f][hardware]]
|
||||||
- **Provenance store becomes operational infrastructure:** a structured data extension of the Knowledge subsystem storing empirical parameters, validity envelopes, and benchmark results with full provenance chains
|
- **Provenance store becomes operational infrastructure:** a structured data extension of the Knowledge subsystem storing empirical parameters, validity envelopes, and benchmark results with full provenance chains
|
||||||
- **Validity envelope predicates as gate vectors:** the gate checks not only security policy but also scientific validity — is this model valid in this context? Are the parameters within their validated range? Does the input fall within the model's training distribution?
|
- **Validity envelope predicates as gate vectors:** the gate checks not only security policy but also scientific validity — is this model valid in this context? Are the parameters within their validated range? Does the input fall within the model's training distribution?
|
||||||
|
|
||||||
@@ -51,20 +51,20 @@ Capability-based authorization. "Root" as an attack target no longer exists.*
|
|||||||
policy is not. Each policy change needs new proof
|
policy is not. Each policy change needs new proof
|
||||||
- **The gate runs on untrusted hardware** — if the OS or hardware is
|
- **The gate runs on untrusted hardware** — if the OS or hardware is
|
||||||
compromised, the gate's guarantees are meaningless. The attacker can skip
|
compromised, the gate's guarantees are meaningless. The attacker can skip
|
||||||
the gate or modify its output. Full gate guarantees arrive at Stage 3
|
the gate or modify its output. Full gate guarantees arrive at the Lisp Machine
|
||||||
|
|
||||||
## What does this enable?
|
## What does this enable?
|
||||||
|
|
||||||
The system can now say "no" to unauthorized actions even when the endpoint is
|
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
|
fully compromised. Security is no longer dependent on client integrity. This is
|
||||||
the first layer where deductive guarantees enter the picture — but they are
|
the first layer where deductive guarantees enter the picture — but they are
|
||||||
contingent on Stage 3's trust substrate.
|
contingent on the Lisp Machine's trust substrate.
|
||||||
|
|
||||||
## When is this viable?
|
## When is this viable?
|
||||||
|
|
||||||
Today as a software layer on conventional hardware, but with limited guarantees
|
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
|
(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.
|
the Lisp Machine stage when the gate runs on the verified Lisp machine.
|
||||||
|
|
||||||
## In practice
|
## In practice
|
||||||
|
|
||||||
@@ -75,51 +75,51 @@ in policy). For high-stakes environments, the trade-off is worth it. For casual
|
|||||||
use, the friction may lead users to bypass the gate.
|
use, the friction may lead users to bypass the gate.
|
||||||
|
|
||||||
*Full gate guarantees arrive when Passepartout runs on its own Lisp machine
|
*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.*
|
(the Lisp Machine stage). Before that, it's a correctness proof running on an untrusted substrate.*
|
||||||
|
|
||||||
### Symbolic Reasoner — CL-Native Higher-Order Logic Engine
|
### Symbolic Reasoner — CL-Native Higher-Order Logic Engine
|
||||||
|
|
||||||
The gate needs to evaluate not just *security policy* but *epistemic
|
The gate needs to evaluate not just *security policy* but *epistemic
|
||||||
validity*: is this action consistent with what the system knows about the
|
validity*: is this action consistent with what the system knows about the
|
||||||
world? The provenance store (Stage 1) provides quality-scored assertions,
|
world? The provenance store provides quality-scored assertions,
|
||||||
but there is no engine to **reason over them** — to combine assertions,
|
but there is no engine to **reason over them** — to combine assertions,
|
||||||
prove entailments, detect contradictions, or generate causal explanations.
|
prove entailments, detect contradictions, or generate causal explanations.
|
||||||
|
|
||||||
**A CL-native symbolic reasoner** fills this gap. It operates over the
|
**A CL-native symbolic reasoner** fills this gap. It operates over the
|
||||||
symbolic index of the Knowledge subsystem (predicates, relations,
|
symbolic index of the Knowledge subsystem (predicates, relations,
|
||||||
constraints extracted from Org prose) and returns (entailed | contradicted
|
constraints extracted from Org prose) and returns (entailed | contradicted
|
||||||
| undetermined) for any query.
|
|| undetermined) for any query.
|
||||||
|
|
||||||
### Architecture
|
### Architecture
|
||||||
|
|
||||||
| Layer | What it does | Implementation |
|
| Layer | What it does | Implementation |
|
||||||
|-------|-------------|----------------|
|
|-------|-------------|----------------|
|
||||||
| Assertion store | Quality-scored formal claims from Stage 1's truth layer | Provenance store hash table (Stage 2) |
|
| Assertion store | Quality-scored formal claims from this stage's truth layer | Provenance store hash table |
|
||||||
| Constraint solver | SAT/SMT-style search over bounded problem spaces | Screamer (CL, existing) |
|
| Constraint solver | SAT/SMT-style search over bounded problem spaces | Screamer (CL, existing) |
|
||||||
| Deduction engine | Forward/backward chaining over first-order subset of assertions | CL-native, starts as Screamer extension |
|
| Deduction engine | Forward/backward chaining over first-order subset of assertions | CL-native, starts as Screamer extension |
|
||||||
| Higher-order layer | Nested modalities — belief, intention, causation, temporal |
|
| Higher-order layer | Nested modalities — belief, intention, causation, temporal |
|
||||||
> Screamer cannot express these natively | CL macros + custom proof search |
|
> Screamer cannot express these natively | CL macros + custom proof search |
|
||||||
| Gate interface | (action, context) → (permit \| deny \| needs-evidence) | ACL2 FFI across the Lisp boundary |
|
| Gate interface | (action, context) → (permit | deny | needs-evidence) | ACL2 FFI across the Lisp boundary |
|
||||||
|
|
||||||
### Why not Lean directly
|
### Why not Lean directly
|
||||||
|
|
||||||
Lean 4 is C++ at its core — a separate trust domain that breaks the single
|
Lean 4 is C++ at its core — a separate trust domain that breaks the single
|
||||||
address space. The reasoner must be CL-native for the Stage 3 Lisp machine
|
address space. The reasoner must be CL-native for the Lisp Machine
|
||||||
model. Lean is the *reference* design: its tactics, elaboration, and type
|
model. Lean is the *reference* design: its tactics, elaboration, and type
|
||||||
theory inspire the CL implementation, but the engine itself is written in
|
theory inspire the CL implementation, but the engine itself is written in
|
||||||
Common Lisp and lives in the same memory graph as the evaluator and gate.
|
Common Lisp and lives in the same memory graph as the evaluator and gate.
|
||||||
|
|
||||||
### Development path across stages
|
### Development path across stages
|
||||||
|
|
||||||
The reasoner is *born at Stage 1* and *hardens through Stage 2*:
|
The reasoner is *born at the Neurosymbolic Agent stage* and *hardens through the Social Protocol stage*:
|
||||||
|
|
||||||
| Stage | Reasoner state | How it gets there |
|
| Stage | Reasoner state | How it gets there |
|
||||||
|-------|---------------|-------------------|
|
|-------|---------------|-------------------|
|
||||||
| 1 | CL prototype (Screamer-based, first-order) | Shared via social protocol's Reasoner Code Exchange. Users test against local symbolic indices, share patches |
|
| Neurosymbolic Agent | CL prototype (Screamer-based, first-order) | Shared via social protocol's Reasoner Code Exchange. Users test against local symbolic indices, share patches |
|
||||||
| 1 | Higher-order extensions sketched | CL macros for modal logic, causal chains — tested on small assertion sets |
|
| Neurosymbolic Agent | Higher-order extensions sketched | CL macros for modal logic, causal chains — tested on small assertion sets |
|
||||||
| 2 | Reasoner feeds gate decisions | Gate delegates knowledge-dependent checks: "is this action valid given what we know?" Works on quality-scored assertions from Stage 1's truth layer |
|
| Social Protocol | Reasoner feeds gate decisions | Gate delegates knowledge-dependent checks: "is this action valid given what we know?" Works on quality-scored assertions from the Neurosymbolic Agent stage's truth layer |
|
||||||
| 3 | Reasoner absorbed into address space | Same memory graph as evaluator, gate, LLM. No FFI, no IPC |
|
| Lisp Machine | Reasoner absorbed into address space | Same memory graph as evaluator, gate, LLM. No FFI, no IPC |
|
||||||
| 4 | Reasoner enters self-improvement loop | In-process LLM reads reasoner code, proposes improvements, gate checks policy |
|
| AI Inference | Reasoner enters self-improvement loop | In-process LLM reads reasoner code, proposes improvements, gate checks policy |
|
||||||
|
|
||||||
### Cost
|
### Cost
|
||||||
|
|
||||||
@@ -154,16 +154,16 @@ The PDS sends the action + context + policy as JSON to an ACL2 subprocess, which
|
|||||||
**3. Hybrid**
|
**3. Hybrid**
|
||||||
Common path decisions (cached/simple) are compiled CL code from approach 1. Complex or novel decisions are escalated to the subprocess. This is the most practical approach for a Phase Zero gate.
|
Common path decisions (cached/simple) are compiled CL code from approach 1. Complex or novel decisions are escalated to the subprocess. This is the most practical approach for a Phase Zero gate.
|
||||||
|
|
||||||
## Risk Comparison: Stage 1 vs Stage 2
|
## Risk Comparison: Neurosymbolic Agent vs Social Protocol
|
||||||
|
|
||||||
Stage 1's risk is implementing published standards correctly. Stage 2's risk is different: the gate's policy language, capability model, and ACL2 proof architecture are Passepartout inventions.
|
The Social Protocol stage's risk is implementing published standards correctly. The Neurosymbolic Agent stage's risk is different: the gate's policy language, capability model, and ACL2 proof architecture are Passepartout inventions.
|
||||||
|
|
||||||
| Stage | Nature of risk | Failure mode | Mitigation |
|
| Stage | Nature of risk | Failure mode | Mitigation |
|
||||||
|-------|---------------|--------------|------------|
|
|-------|---------------|--------------|------------|
|
||||||
| 1 | Spec complexity — implement DAG, DID, JOSE, Double Ratchet correctly per published standards | Wrong output, test vectors catch it | Sidecar strategy reduces to near-zero for initial release |
|
| Social Protocol | Spec complexity — implement DAG, DID, JOSE, Double Ratchet correctly per published standards | Wrong output, test vectors catch it | Sidecar strategy reduces to near-zero for initial release |
|
||||||
| 2 | Design uncertainty — what does the policy language look like? How do capabilities compose? How does ACL2 model the system? | Wrong abstraction, must rewrite | Gate kernel is small (authorize? deny?) — the proof surface is narrow even if the policy surface is large |
|
| Neurosymbolic Agent | Design uncertainty — what does the policy language look like? How do capabilities compose? How does ACL2 model the system? | Wrong abstraction, must rewrite | Gate kernel is small (authorize? deny?) — the proof surface is narrow even if the policy surface is large |
|
||||||
|
|
||||||
## What Makes Stage 2 Tractable
|
## What Makes the Gate Tractable
|
||||||
|
|
||||||
The gate kernel is tiny: a function that takes (action, context, policy) and returns permit or deny. The policy can grow arbitrarily complex (capability tokens, validity envelopes, compliance rules) but the decision procedure is a simple predicate.
|
The gate kernel is tiny: a function that takes (action, context, policy) and returns permit or deny. The policy can grow arbitrarily complex (capability tokens, validity envelopes, compliance rules) but the decision procedure is a simple predicate.
|
||||||
|
|
||||||
@@ -171,13 +171,13 @@ The ACL2 verification covers the kernel — "does this decision follow from the
|
|||||||
|
|
||||||
## Constraint on the PDS
|
## Constraint on the PDS
|
||||||
|
|
||||||
The gate runs in the same address space as the PDS (Stage 2 runs on conventional hardware; Stage 3 moves it to the verified Lisp machine). This means:
|
The gate runs in the same address space as the PDS (at the Neurosymbolic Agent stage, on conventional hardware; the Lisp Machine stage moves it to the verified Lisp machine). This means:
|
||||||
|
|
||||||
- The PDS must expose an action interception point that the gate can hook into
|
- The PDS must expose an action interception point that the gate can hook into
|
||||||
- Every action path — user command, LLM proposal, network message, file write — routes through the same decision procedure
|
- Every action path — user command, LLM proposal, network message, file write — routes through the same decision procedure
|
||||||
- The gate cannot be bypassed; there is no privileged path
|
- The gate cannot be bypassed; there is no privileged path
|
||||||
|
|
||||||
← [[id:8cb760e2-37c6-4a78-af4d-f89f69d1678b][Stage 0: Now]] → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]]
|
← [[id:8cb760e2-37c6-4a78-af4d-f89f69d1678b][Development]] → [[id:1d074690-a279-59cb-b91d-e9a22ae104ad][Social Protocol]]
|
||||||
:PROPERTIES:
|
:PROPERTIES:
|
||||||
:CREATED: [2026-05-24 Sun]
|
:CREATED: [2026-05-24 Sun]
|
||||||
:WEIGHT: 11
|
:WEIGHT: 11
|
||||||
|
|||||||
@@ -5,8 +5,8 @@ tags: :passepartout:roadmap:social-protocol:
|
|||||||
created: 2026-05-24
|
created: 2026-05-24
|
||||||
---
|
---
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc5-4def-9876-543210abcdef][AI Inference]] → [[id:4a1f23b0-abc6-4def-9876-543210abcdef][AI Weights]]
|
← [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Neurosymbolic Agent]] → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]]
|
||||||
# Stage 1: [[id:1d074690-a279-59cb-b91d-e9a22ae104ad][Social Protocol]]
|
# Social Protocol
|
||||||
|
|
||||||
*Summary: Every message is signed, DAG-tracked, and content-addressed.
|
*Summary: Every message is signed, DAG-tracked, and content-addressed.
|
||||||
Communication becomes provable - when you choose it to be.*
|
Communication becomes provable - when you choose it to be.*
|
||||||
@@ -90,7 +90,7 @@ from Org prose by the LLM — is a signed, DAG-tracked message.
|
|||||||
| Contradiction detection | The DAG flags when instance A asserts P and instance B asserts ¬P. Conflicts are protocol events, not bugs | Signed assertions, DAG query |
|
| Contradiction detection | The DAG flags when instance A asserts P and instance B asserts ¬P. Conflicts are protocol events, not bugs | Signed assertions, DAG query |
|
||||||
| Verification staking | Instances vouch for assertions with reputation or compute stake. Surviving challenges accumulate confidence; false assertions degrade the issuer's weight | Contradiction detection |
|
| Verification staking | Instances vouch for assertions with reputation or compute stake. Surviving challenges accumulate confidence; false assertions degrade the issuer's weight | Contradiction detection |
|
||||||
| Truth scoring | Every assertion carries a confidence tier: (1) extracted/LLM-guess → (2) locally consistent → (3) corroborated by N independent instances → (4) gate-enforced | Staking, corroboration count |
|
| Truth scoring | Every assertion carries a confidence tier: (1) extracted/LLM-guess → (2) locally consistent → (3) corroborated by N independent instances → (4) gate-enforced | Staking, corroboration count |
|
||||||
| Reasoner code exchange | The same protocol distributes CL reasoner prototypes. Users collaborate on the symbolic reasoner (Stage 2) before it enters the gate | Signed code, DAG versioning |
|
| Reasoner code exchange | The same protocol distributes CL reasoner prototypes. Users collaborate on the symbolic reasoner (the Lisp Machine stage) before it enters the gate | Signed code, DAG versioning |
|
||||||
|
|
||||||
**The verification economy emerges naturally.** Instances that contribute
|
**The verification economy emerges naturally.** Instances that contribute
|
||||||
verified assertions gain reputation. Instances that propagate falsehoods
|
verified assertions gain reputation. Instances that propagate falsehoods
|
||||||
@@ -112,13 +112,13 @@ through network effects instead of hand-curation.
|
|||||||
|
|
||||||
## Full Library Dependency Map
|
## Full Library Dependency Map
|
||||||
|
|
||||||
Stage 1 depends on three tiers of libraries: existing CL, new CL (need development), and bridged sidecars.
|
This stage depends on three tiers of libraries: existing CL, new CL (need development), and bridged sidecars.
|
||||||
|
|
||||||
### Existing CL Libraries (ready now)
|
### Existing CL Libraries (ready now)
|
||||||
|
|
||||||
These are mature, production-tested Common Lisp libraries that require no development work:
|
These are mature, production-tested Common Lisp libraries that require no development work:
|
||||||
|
|
||||||
| Library | Role in Stage 1 |
|
| Library | Role in this stage |
|
||||||
|---------|----------------|
|
|---------|----------------|
|
||||||
| Ironclad | All crypto primitives — Ed25519, SHA-256, AES, ChaCha20-Poly1305, HMAC, DH |
|
| Ironclad | All crypto primitives — Ed25519, SHA-256, AES, ChaCha20-Poly1305, HMAC, DH |
|
||||||
| hunchentoot | HTTP server — PDS API endpoints |
|
| hunchentoot | HTTP server — PDS API endpoints |
|
||||||
@@ -177,9 +177,9 @@ These are not libraries but Passepartout systems that must be built:
|
|||||||
|
|
||||||
The sidecar strategy collapses the high-risk items to near-zero implementation risk for the initial release.
|
The sidecar strategy collapses the high-risk items to near-zero implementation risk for the initial release.
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc5-4def-9876-543210abcdef][AI Inference]] → [[id:4a1f23b0-abc6-4def-9876-543210abcdef][AI Weights]]
|
← [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Neurosymbolic Agent]] → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]]
|
||||||
:PROPERTIES:
|
:PROPERTIES:
|
||||||
:CREATED: [2026-05-24 Sun]
|
:CREATED: [2026-05-24 Sun]
|
||||||
:WEIGHT: 14
|
:WEIGHT: 12
|
||||||
:ID: 4a1f23b0-abc2-4def-9876-543210abcdef
|
:ID: 4a1f23b0-abc2-4def-9876-543210abcdef
|
||||||
:END:
|
:END:
|
||||||
@@ -5,8 +5,8 @@ tags: :passepartout:roadmap:
|
|||||||
created: 2026-05-24
|
created: 2026-05-24
|
||||||
---
|
---
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Neurosymbolic Agent]] → [[id:4a1f23b0-abc5-4def-9876-543210abcdef][AI Inference]]
|
← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Social Protocol]] → [[id:4a1f23b0-abc5-4def-9876-543210abcdef][AI Inference]]
|
||||||
# Stage 3: Lisp Machine
|
# 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]].
|
*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.*
|
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.*
|
||||||
@@ -129,9 +129,9 @@ and everything must be written in Lisp. The practical trade is: absolute
|
|||||||
memory safety at the cost of adopting an entirely new computing paradigm.
|
memory safety at the cost of adopting an entirely new computing paradigm.
|
||||||
This is not an upgrade path — it is a replacement.
|
This is not an upgrade path — it is a replacement.
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Neurosymbolic Agent]] → [[id:4a1f23b0-abc5-4def-9876-543210abcdef][AI Inference]]
|
← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Social Protocol]] → [[id:4a1f23b0-abc5-4def-9876-543210abcdef][AI Inference]]
|
||||||
:PROPERTIES:
|
:PROPERTIES:
|
||||||
:CREATED: [2026-05-24 Sun]
|
:CREATED: [2026-05-24 Sun]
|
||||||
:WEIGHT: 12
|
:WEIGHT: 14
|
||||||
:ID: 4a1f23b0-abc4-4def-9876-543210abcdef
|
:ID: 4a1f23b0-abc4-4def-9876-543210abcdef
|
||||||
:END:
|
:END:
|
||||||
@@ -5,8 +5,8 @@ tags: :passepartout:roadmap:
|
|||||||
created: 2026-05-24
|
created: 2026-05-24
|
||||||
---
|
---
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]] → [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Social Protocol]]
|
← [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]] → [[id:4a1f23b0-abc6-4def-9876-543210abcdef][AI Weights]]
|
||||||
# Stage 4: Inference
|
# AI Inference
|
||||||
|
|
||||||
*Summary: The LLM runs in-process under the gate. Every token is inspected
|
*Summary: The LLM runs in-process under the gate. Every token is inspected
|
||||||
during generation. No external API, no separate trust domain.*
|
during generation. No external API, no separate trust domain.*
|
||||||
@@ -24,9 +24,9 @@ during generation. No external API, no separate trust domain.*
|
|||||||
and replayable
|
and replayable
|
||||||
- **Distribution match check runs at evaluation loop speed:** the gate's validity predicate for neural network models becomes a fast native function — compute distance to training distribution and compare against threshold in the same process, no IPC
|
- **Distribution match check runs at evaluation loop speed:** the gate's validity predicate for neural network models becomes a fast native function — compute distance to training distribution and compare against threshold in the same process, no IPC
|
||||||
|
|
||||||
*Two neural components on the same substrate:* Stage 4 hosts the LLM for
|
*Two neural components on the same substrate:* this stage hosts the LLM for
|
||||||
generative reasoning and action proposals. The LeCun-type world model (sensory
|
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
|
prediction) joins at AI Training. Both run on the same tensor unit with the same
|
||||||
plist-native weight architecture and gate-level interception. The LLM proposes
|
plist-native weight architecture and gate-level interception. The LLM proposes
|
||||||
actions to the gate (authorization — binary, deductive). The world model
|
actions to the gate (authorization — binary, deductive). The world model
|
||||||
proposes predictions to the gate (falsification — structural, empirical). The
|
proposes predictions to the gate (falsification — structural, empirical). The
|
||||||
@@ -87,7 +87,7 @@ 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.
|
prove anything about individual weights. Training provenance is not tracked.
|
||||||
The inference is FFI-mediated, so trust in llama.cpp remains.
|
The inference is FFI-mediated, so trust in llama.cpp remains.
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]] → [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Social Protocol]]
|
← [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Lisp Machine]] → [[id:4a1f23b0-abc6-4def-9876-543210abcdef][AI Weights]]
|
||||||
:PROPERTIES:
|
:PROPERTIES:
|
||||||
:CREATED: [2026-05-24 Sun]
|
:CREATED: [2026-05-24 Sun]
|
||||||
:WEIGHT: 13
|
:WEIGHT: 13
|
||||||
@@ -6,7 +6,7 @@ created: 2026-05-24
|
|||||||
---
|
---
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Social Protocol]] → [[id:4a1f23b0-abc7-4def-9876-543210abcdef][AI Training]]
|
← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Social Protocol]] → [[id:4a1f23b0-abc7-4def-9876-543210abcdef][AI Training]]
|
||||||
# Stage 5: Weights
|
# AI Weights
|
||||||
|
|
||||||
*Summary: Every weight is a [[id:1c95ce7d-a2db-506a-9608-df68f9ae211b][Lisp object in the Merkle memory graph]]. You can
|
*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
|
prove not just that the model file is unmodified, but that this specific
|
||||||
@@ -69,7 +69,7 @@ viability.
|
|||||||
Every individual weight is Merkle-verified, structurally tracked, and computed
|
Every individual weight is Merkle-verified, structurally tracked, and computed
|
||||||
within the Lisp evaluator's verified semantics. The FFI trust gap is closed.
|
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
|
This stage is where hardware choice determines practical viability. The GPU path
|
||||||
works today but carries the storage overhead of two representations (plist gold
|
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
|
standard + GPU mirror) and the load-time verification cost. The ASIC path is
|
||||||
the destination — one representation, one chip, no workaround. Most users will
|
the destination — one representation, one chip, no workaround. Most users will
|
||||||
|
|||||||
@@ -6,7 +6,7 @@ created: 2026-05-24
|
|||||||
---
|
---
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc6-4def-9876-543210abcdef][AI Weights]] → [[id:4a1f23b0-abc8-4def-9876-543210abcdef][What Remains]]
|
← [[id:4a1f23b0-abc6-4def-9876-543210abcdef][AI Weights]] → [[id:4a1f23b0-abc8-4def-9876-543210abcdef][What Remains]]
|
||||||
# Stage 6: Training
|
# AI Training
|
||||||
|
|
||||||
*Summary: Verified fine-tuning under the gate. Every example checked for consent.
|
*Summary: Verified fine-tuning under the gate. Every example checked for consent.
|
||||||
Every gradient application is a verified state transition. The neural world model
|
Every gradient application is a verified state transition. The neural world model
|
||||||
@@ -41,7 +41,7 @@ same verified training pipeline:
|
|||||||
the accumulated observation DAG after the fact, tracking calibration over
|
the accumulated observation DAG after the fact, tracking calibration over
|
||||||
time. This is verification through falsification, not authorization
|
time. This is verification through falsification, not authorization
|
||||||
|
|
||||||
### The interaction at Stage 6
|
### The interaction at this stage
|
||||||
|
|
||||||
1. World model predicts sensory outcome: "user will press button in 2 seconds"
|
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"
|
2. LLM reasons about the predicted outcome: "if user presses button, C follows"
|
||||||
@@ -64,7 +64,7 @@ same verified training pipeline:
|
|||||||
|
|
||||||
## What does this cost?
|
## What does this cost?
|
||||||
|
|
||||||
- **~100x slower than conventional fine-tuning** — building on Stage 5's 100x
|
- **~100x slower than conventional fine-tuning** — building on AI Weights' 100x
|
||||||
overhead (GPU path) plus verified gate checks per example. A LoRA fine-tuning
|
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
|
that takes 2 hours natively takes ~200 hours. Doable overnight, not for rapid
|
||||||
iteration
|
iteration
|
||||||
@@ -104,7 +104,7 @@ But this system is not for training frontier models — it is for auditing
|
|||||||
training runs that happen elsewhere.
|
training runs that happen elsewhere.
|
||||||
|
|
||||||
The practical workflow is: pretrain on a conventional GPU cluster, import the
|
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
|
weights into the Lisp machine as a verified blob (AI Inference stage), then fine-tune on the Lisp machine
|
||||||
under the verified training loop. The pretraining phase remains unverified,
|
under the verified training loop. The pretraining phase remains unverified,
|
||||||
but the fine-tuning phase — where the model gains knowledge of private data
|
but the fine-tuning phase — where the model gains knowledge of private data
|
||||||
and user preferences — is verified. This is the pragmatic sweet spot.
|
and user preferences — is verified. This is the pragmatic sweet spot.
|
||||||
|
|||||||
@@ -6,7 +6,7 @@ created: 2026-05-24
|
|||||||
---
|
---
|
||||||
|
|
||||||
← [[id:4a1f23b0-abc7-4def-9876-543210abcdef][AI Training]]
|
← [[id:4a1f23b0-abc7-4def-9876-543210abcdef][AI Training]]
|
||||||
# Stage 7: What Remains
|
# What Remains
|
||||||
|
|
||||||
*Summary: At full maturity — dual-unit ASIC, plist-native weights, verified
|
*Summary: At full maturity — dual-unit ASIC, plist-native weights, verified
|
||||||
fine-tuning, neural world model — the following irreducible threats survive.
|
fine-tuning, neural world model — the following irreducible threats survive.
|
||||||
@@ -54,7 +54,7 @@ The system reasons perfectly about a world that may not exist:
|
|||||||
the user was wrong
|
the user was wrong
|
||||||
|
|
||||||
Oracle diversity reduces surface area but introduces Byzantine agreement
|
Oracle diversity reduces surface area but introduces Byzantine agreement
|
||||||
problems. The question at Stage 7 shifts from "can the attacker break the
|
problems. The question at this stage shifts from "can the attacker break the
|
||||||
crypto?" to "can the attacker convince the user to press the button?"
|
crypto?" to "can the attacker convince the user to press the button?"
|
||||||
|
|
||||||
## 4. The bootstrap axiom
|
## 4. The bootstrap axiom
|
||||||
|
|||||||
@@ -70,9 +70,9 @@ Alternative: start with 4×64GB to get half bandwidth without crippling storage
|
|||||||
|
|
||||||
* Strategic framing
|
* Strategic framing
|
||||||
|
|
||||||
This node is a bootstrap between Stage 0 (current, conventional) and Stages 3-4 (Lisp machine, bare-metal, in-process LLM on dedicated silicon). DDR4's bandwidth ceiling won't matter because:
|
This node is a bootstrap between Development (current, conventional) and Lisp Machine and AI Inference. DDR4's bandwidth ceiling won't matter because:
|
||||||
|
|
||||||
- Proxmox + ZFS + the Gate (Stage 2) don't stress 8-channel DDR4-3200
|
- Proxmox + ZFS + the Gate (Neurosymbolic Agent stage) don't stress 8-channel DDR4-3200
|
||||||
- GPU inference uses its own VRAM, not system memory
|
- GPU inference uses its own VRAM, not system memory
|
||||||
- By the time the Lisp machine arrives (different hardware entirely), this node graduates to NAS / Proxmox host duty
|
- By the time the Lisp machine arrives (different hardware entirely), this node graduates to NAS / Proxmox host duty
|
||||||
|
|
||||||
|
|||||||
@@ -18,10 +18,10 @@ independent dynamics. Each has its own phases, defined by different
|
|||||||
metrics. They run concurrently and reinforce each other, but neither is a
|
metrics. They run concurrently and reinforce each other, but neither is a
|
||||||
precondition for the other. Each section below defines its own phases.
|
precondition for the other. Each section below defines its own phases.
|
||||||
|
|
||||||
Phases are distinct from the architecture's development Stages (Stage 0
|
Phases are distinct from the architecture's development Stages (Development
|
||||||
= now/Linux-hosted, Stage 1 = social protocol, Stage 2 = verification
|
= now/Linux-hosted, Social Protocol = social protocol, Neurosymbolic Agent = verification
|
||||||
TUI, Stage 3 = Lisp machine, Stage 4 = inference ASIC). The clock for
|
TUI, Lisp Machine = Lisp machine, AI Inference = inference ASIC). The clock for
|
||||||
both adoptions starts when Stage 2 ships (TUI complete). See
|
both adoptions starts when Neurosymbolic Agent ships (TUI complete). See
|
||||||
[[id:dc2e4f22-1c4c-5d4a-a151-f96e5d3b0d70][Development timeline]] for the Stage breakdown.
|
[[id:dc2e4f22-1c4c-5d4a-a151-f96e5d3b0d70][Development timeline]] for the Stage breakdown.
|
||||||
|
|
||||||
* Social adoption
|
* Social adoption
|
||||||
|
|||||||
@@ -79,7 +79,7 @@ Because the LLM never makes a decision — it only translates — there are zero
|
|||||||
| Graph growth | Manual — human experts build and update in Studio | Automatic — autodidactic loop hardens from Gate decisions |
|
| Graph growth | Manual — human experts build and update in Studio | Automatic — autodidactic loop hardens from Gate decisions |
|
||||||
| LLM role | Natural language translation only | Proposes actions, facts, interpretations; cannot overrule Gate |
|
| LLM role | Natural language translation only | Proposes actions, facts, interpretations; cannot overrule Gate |
|
||||||
| Audit trail | Proof trees from reasoning engine | Full decision log from every Gate action |
|
| Audit trail | Proof trees from reasoning engine | Full decision log from every Gate action |
|
||||||
| Execution environment | Conventional cloud/SaaS | Lisp address space, bare metal at Stage 3+ |
|
| Execution environment | Conventional cloud/SaaS | Lisp address space, bare metal at Lisp Machine onwards |
|
||||||
| Identity | User accounts in SaaS | Self-sovereign DID |
|
| Identity | User accounts in SaaS | Self-sovereign DID |
|
||||||
| Social protocol | None | DIDComm, PDS, relay, compute marketplace, liquid democracy |
|
| Social protocol | None | DIDComm, PDS, relay, compute marketplace, liquid democracy |
|
||||||
| Openness | Proprietary, closed source | Designed to be open and self-hosted |
|
| Openness | Proprietary, closed source | Designed to be open and self-hosted |
|
||||||
@@ -102,7 +102,7 @@ Because the LLM never makes a decision — it only translates — there are zero
|
|||||||
|
|
||||||
* Implications for Passepartout
|
* Implications for Passepartout
|
||||||
|
|
||||||
**Validation.** Rainbird proves the market exists. Enterprises will pay significant sums for deterministic symbolic AI over a natural language interface. Every Rainbird case study — especially in regulated industries — validates the revenue model Passepartout targets for Stage 2.
|
**Validation.** Rainbird proves the market exists. Enterprises will pay significant sums for deterministic symbolic AI over a natural language interface. Every Rainbird case study — especially in regulated industries — validates the revenue model Passepartout targets for the Neurosymbolic Agent stage.
|
||||||
|
|
||||||
**Differentiation.** Rainbird's weaknesses are Passepartout's strengths. The autodidactic loop, the evaluation loop interposition, the social protocol, the Lisp address space, the self-hosted pricing — these are gaps in Rainbird's offering that Passepartout can exploit.
|
**Differentiation.** Rainbird's weaknesses are Passepartout's strengths. The autodidactic loop, the evaluation loop interposition, the social protocol, the Lisp address space, the self-hosted pricing — these are gaps in Rainbird's offering that Passepartout can exploit.
|
||||||
|
|
||||||
|
|||||||
@@ -17,7 +17,7 @@ This is the bootstrap — the system must build itself before it can build anyth
|
|||||||
|
|
||||||
- The gate stack seeds 50-70 entity classes from its own code (files, commands, processes, networks, dependencies)
|
- The gate stack seeds 50-70 entity classes from its own code (files, commands, processes, networks, dependencies)
|
||||||
- Every git commit, build error, test failure, and shell command is a gate outcome — accumulating toward sufficiency without manual curation
|
- Every git commit, build error, test failure, and shell command is a gate outcome — accumulating toward sufficiency without manual curation
|
||||||
- The reasoner is born as a Screamer-based CL prototype shared via the social protocol at Stage 1, hardens into the gate at Stage 2, and enters self-improvement under the in-process LLM at Stage 4
|
- The reasoner is born as a Screamer-based CL prototype shared via the social protocol at the Social Protocol stage, hardens into the gate at the Neurosymbolic Agent stage, and enters self-improvement under the in-process LLM at the AI Inference stage
|
||||||
- The social protocol itself is software — its correctness is verified by the same gate that software engineering produces
|
- The social protocol itself is software — its correctness is verified by the same gate that software engineering produces
|
||||||
|
|
||||||
Sufficiency in software engineering means the system can propose, verify, and apply changes to its own codebase under gate supervision. This is the bootstrap completion signal.
|
Sufficiency in software engineering means the system can propose, verify, and apply changes to its own codebase under gate supervision. This is the bootstrap completion signal.
|
||||||
@@ -43,7 +43,7 @@ This is where the verification economy produces real revenue, not just knowledge
|
|||||||
|
|
||||||
4. **First-mover advantage is real.** The first gate configuration for HIPAA risk assessments becomes the template. Every audit that passes against it is a data point. Late entrants must either replicate years of accumulated gate outcomes or buy access to the commons. A proprietary compliance vendor cannot compete with a commons that improves with every customer.
|
4. **First-mover advantage is real.** The first gate configuration for HIPAA risk assessments becomes the template. Every audit that passes against it is a data point. Late entrants must either replicate years of accumulated gate outcomes or buy access to the commons. A proprietary compliance vendor cannot compete with a commons that improves with every customer.
|
||||||
|
|
||||||
5. **The ontology work can happen in parallel with hardware maturation.** Encoding HIPAA rules as gate predicates is a Stage 2 activity (software layer on conventional hardware). Enforcement at scale — passing a SOC 2 Type II audit — waits for Stage 3 (Lisp machine). But the encoding, testing, and network convergence happen years before the silicon is ready.
|
5. **The ontology work can happen in parallel with hardware maturation.** Encoding HIPAA rules as gate predicates is a Neurosymbolic Agent activity (software layer on conventional hardware). Enforcement at scale — passing a SOC 2 Type II audit — waits for the Lisp Machine. But the encoding, testing, and network convergence happen years before the silicon is ready.
|
||||||
|
|
||||||
**Fourth: Physics, chemistry, and the rest of science can wait.**
|
**Fourth: Physics, chemistry, and the rest of science can wait.**
|
||||||
|
|
||||||
|
|||||||
@@ -498,7 +498,7 @@ but connected through resource flows:
|
|||||||
|
|
||||||
- **Institutional → Social:** Compliance revenue would accelerate the
|
- **Institutional → Social:** Compliance revenue would accelerate the
|
||||||
social protocol's development timeline, but the architecture is
|
social protocol's development timeline, but the architecture is
|
||||||
self-developing after Stage 2 — the bootstrap loop means engineering
|
self-developing after the Neurosymbolic Agent stage — the bootstrap loop means engineering
|
||||||
does not depend on external funding. Revenue is amplificatory, not
|
does not depend on external funding. Revenue is amplificatory, not
|
||||||
necessary.
|
necessary.
|
||||||
- **Social → Institutional (late stage):** At Phase 3+, the social
|
- **Social → Institutional (late stage):** At Phase 3+, the social
|
||||||
@@ -515,7 +515,7 @@ directions. Institutional success can exist without social success
|
|||||||
without institutional success — the social protocol reaches critical
|
without institutional success — the social protocol reaches critical
|
||||||
mass through pure platform competition, and its development is not
|
mass through pure platform competition, and its development is not
|
||||||
blocked by lack of institutional revenue because the architecture is
|
blocked by lack of institutional revenue because the architecture is
|
||||||
self-developing after Stage 2 (the agent writes its own code; the
|
self-developing after the Neurosymbolic Agent stage (the agent writes its own code; the
|
||||||
bootstrap loop makes engineering self-sustaining). The coupling is
|
bootstrap loop makes engineering self-sustaining). The coupling is
|
||||||
amplificatory, not foundational: each side's success makes the other
|
amplificatory, not foundational: each side's success makes the other
|
||||||
more valuable, but neither depends on the other to survive.
|
more valuable, but neither depends on the other to survive.
|
||||||
|
|||||||
@@ -8,7 +8,7 @@
|
|||||||
|
|
||||||
* Assumptions
|
* Assumptions
|
||||||
|
|
||||||
- Stage 2 instance: one SBCL Lisp process with Gate + PDS + environment in one address space
|
- Neurosymbolic Agent instance: one SBCL Lisp process with Gate + PDS + environment in one address space
|
||||||
- User brings own LLM API key — no AI token cost to the provider
|
- User brings own LLM API key — no AI token cost to the provider
|
||||||
- Containerized: Docker image running on cloud VMs (AWS spot instances)
|
- Containerized: Docker image running on cloud VMs (AWS spot instances)
|
||||||
- Instances are embarrassingly parallel — no cross-instance coordination
|
- Instances are embarrassingly parallel — no cross-instance coordination
|
||||||
|
|||||||
Reference in New Issue
Block a user