Fold stage secondary docs into main pages: one note per stage
- Merge stage-1-dependency-map.org (library tables) into stage-1-social-protocol.org - Merge stage-2-acl2-integration.org (integration approaches, risk, PDS constraint) into stage-2-verification.org - Delete both secondary files - Regenerate ID map - Rebuild: 145 files, 0 errors - Sidebar now shows one page per stage: Stage 0-7
This commit is contained in:
Hermes
@@ -28,14 +28,12 @@
|
||||
"d2722576-fc9b-4bd3-bc2f-f5692b561b4e": "projects/passepartout/architecture/academic.org",
|
||||
"8cb760e2-37c6-4a78-af4d-f89f69d1678b": "projects/passepartout/architecture/stages/_index.org",
|
||||
"4a1f23b0-abc8-4def-9876-543210abcdef": "projects/passepartout/architecture/stages/stage-7-remaining.org",
|
||||
"3ec5bd52-f115-455e-83be-63db9a4ad3a7": "projects/passepartout/architecture/stages/stage-1-dependency-map.org",
|
||||
"4a1f23b0-abc6-4def-9876-543210abcdef": "projects/passepartout/architecture/stages/stage-5-weights.org",
|
||||
"4a1f23b0-abc7-4def-9876-543210abcdef": "projects/passepartout/architecture/stages/stage-6-training.org",
|
||||
"4a1f23b0-abc5-4def-9876-543210abcdef": "projects/passepartout/architecture/stages/stage-4-inference.org",
|
||||
"4a1f23b0-abc3-4def-9876-543210abcdef": "projects/passepartout/architecture/stages/stage-2-verification.org",
|
||||
"4a1f23b0-abc4-4def-9876-543210abcdef": "projects/passepartout/architecture/stages/stage-3-lisp-machine.org",
|
||||
"4a1f23b0-abc2-4def-9876-543210abcdef": "projects/passepartout/architecture/stages/stage-1-social-protocol.org",
|
||||
"460e06f4-6bfc-4969-89d8-685c0c4434cf": "projects/passepartout/architecture/stages/stage-2-acl2-integration.org",
|
||||
"4b5c6d7e-8f9a-0b1c-2d3e-4f5a6b7c8d9e": "projects/passepartout/architecture/knowledge-layers/neurological-empirical.org",
|
||||
"329bd4fb-702a-4a2b-9c63-69281aacb83a": "projects/passepartout/architecture/knowledge-layers/_index.org",
|
||||
"5c6d7e8f-9a0b-1c2d-3e4f-5a6b7c8d9e0f": "projects/passepartout/architecture/knowledge-layers/practical-implications.org",
|
||||
|
||||
@@ -1,84 +0,0 @@
|
||||
---
|
||||
title: Stage 1
|
||||
type: reference
|
||||
tags: :passepartout:architecture:social-protocol:dependencies:
|
||||
created: 2026-05-28
|
||||
---
|
||||
|
||||
← Stage 1 — Social Protocol | Repo Organization
|
||||
|
||||
# Stage 1 — Full Library Dependency Map
|
||||
|
||||
Stage 1 (social protocol) depends on three tiers of libraries: existing CL, spec-based CL, and bridged sidecars.
|
||||
|
||||
## Existing CL Libraries (ready now)
|
||||
|
||||
These are mature, production-tested Common Lisp libraries that require no development work:
|
||||
|
||||
| Library | Role in Stage 1 |
|
||||
|---------|----------------|
|
||||
| Ironclad | All crypto primitives — Ed25519, SHA-256, AES, ChaCha20-Poly1305, HMAC, DH |
|
||||
| hunchentoot | HTTP server — PDS API endpoints |
|
||||
| drakma | HTTP client — inter-PDS communication, sidecar calls |
|
||||
| cl+ssl | TLS everywhere — server and client |
|
||||
| websocket-driver | Real-time Relay connections |
|
||||
| jonathan | JSON parsing/serialization — DID docs, JWE headers, API payloads |
|
||||
| cl-sqlite | Message storage, user data, DAG index |
|
||||
| local-time | Timestamps for Notes, DAG entries |
|
||||
| bordeaux-threads | Concurrency — connection handling, parallel verification |
|
||||
| alexandria | General utilities |
|
||||
| log4cl | Structured logging |
|
||||
| fiveam | Testing framework |
|
||||
| cffi | Foreign function interface to C/Rust sidecars |
|
||||
| usocket | Socket abstraction |
|
||||
|
||||
## New CL Libraries (need development)
|
||||
|
||||
| Library | What it implements | Key correctness challenge |
|
||||
|---------|-------------------|-------------------------|
|
||||
| cl-dag / cl-cid | IPLD Merkle DAG — CID encoding, multihash, DAG tree operations | Spec compliance (IPLD test vectors) |
|
||||
| cl-did | W3C DID — Ed25519 key wrapping, DID document construction, did:key resolution | Spec compliance (W3C test suite) |
|
||||
| cl-jose | JWE/JWS — envelope serialization, key wrapping modes, algorithm selection | Surface area (combinatorial spec, not deep math) |
|
||||
| cl-double-ratchet | Signal Double Ratchet — DH ratchet, symmetric ratchet, associated data, header encryption | **Highest risk** — one byte wrong in associated data breaks every message |
|
||||
| cl-bip | BIP-32/39/44 — mnemonic encoding, HD key derivation, hardened vs non-hardened paths | Silent failure (wrong derivation produces wrong keys, no error) |
|
||||
| cl-didcomm | DIDComm v2 — message packing, forwarding, routing, attachment handling | Composes the above libraries; protocol logic correctness |
|
||||
|
||||
## Bridged Sidecars (initial release)
|
||||
|
||||
Replace native CL development risk with battle-tested implementations via CFFI or sidecar processes:
|
||||
|
||||
| Component | Bridge method | Source | Replaced by |
|
||||
|-----------|--------------|--------|-------------|
|
||||
| Double Ratchet | CFFI → libsignal | Signal's C library, MIT license | cl-double-ratchet |
|
||||
| DID operations | CFFI → didkit | Spruce, Rust + C bindings, Apache 2.0 | cl-did |
|
||||
| DIDComm | CFFI → didcomm-rust | DIDComm WG, C bindings, Apache 2.0 | cl-didcomm |
|
||||
| DAG/CID storage | HTTP API → ipfs daemon | IPFS Go daemon, MIT license | cl-dag |
|
||||
| BIP derivation | CFFI or sidecar | libbitcoin or bip-utils | cl-bip |
|
||||
| JOSE envelopes | CFFI → libjose or OpenSSL CMS | libjose/OpenSSL | cl-jose |
|
||||
|
||||
## Infrastructure Code (Passepartout-specific)
|
||||
|
||||
These are not libraries but Passepartout systems that must be built:
|
||||
|
||||
| Component | Role |
|
||||
|-----------|------|
|
||||
| PDS server | HTTP/WS API, message routing, storage orchestration, gate integration |
|
||||
| Relay server | Pub/sub message routing between PDSs, connection management |
|
||||
| Client API layer | Protocol endpoints the mobile apps call |
|
||||
|
||||
## Risk Distribution
|
||||
|
||||
- **Low risk:** cl-dag, cl-did, cl-bip — published standards with test vectors, or bridged via sidecar
|
||||
- **Medium risk:** cl-jose — large spec surface area but well-documented
|
||||
- **High risk:** cl-double-ratchet — protocol logic depth, must get state transitions exactly right
|
||||
|
||||
The sidecar strategy collapses the high-risk items to near-zero implementation risk for the initial release.
|
||||
|
||||
→ Repo Organization
|
||||
→ Stage 2 — Verification Subsystem
|
||||
|
||||
:PROPERTIES:
|
||||
:CREATED: [2026-05-11 Mon]
|
||||
:WEIGHT: 13
|
||||
:ID: 3ec5bd52-f115-455e-83be-63db9a4ad3a7
|
||||
:END:
|
||||
@@ -111,6 +111,73 @@ sparse knowledge). As the instance count grows, contradiction frequency
|
||||
increases and quality converges. This is Cyc's pump-priming problem solved
|
||||
through network effects instead of hand-curation.
|
||||
|
||||
## Full Library Dependency Map
|
||||
|
||||
Stage 1 depends on three tiers of libraries: existing CL, new CL (need development), and bridged sidecars.
|
||||
|
||||
### Existing CL Libraries (ready now)
|
||||
|
||||
These are mature, production-tested Common Lisp libraries that require no development work:
|
||||
|
||||
| Library | Role in Stage 1 |
|
||||
|---------|----------------|
|
||||
| Ironclad | All crypto primitives — Ed25519, SHA-256, AES, ChaCha20-Poly1305, HMAC, DH |
|
||||
| hunchentoot | HTTP server — PDS API endpoints |
|
||||
| drakma | HTTP client — inter-PDS communication, sidecar calls |
|
||||
| cl+ssl | TLS everywhere — server and client |
|
||||
| websocket-driver | Real-time Relay connections |
|
||||
| jonathan | JSON parsing/serialization — DID docs, JWE headers, API payloads |
|
||||
| cl-sqlite | Message storage, user data, DAG index |
|
||||
| local-time | Timestamps for Notes, DAG entries |
|
||||
| bordeaux-threads | Concurrency — connection handling, parallel verification |
|
||||
| alexandria | General utilities |
|
||||
| log4cl | Structured logging |
|
||||
| fiveam | Testing framework |
|
||||
| cffi | Foreign function interface to C/Rust sidecars |
|
||||
| usocket | Socket abstraction |
|
||||
|
||||
### New CL Libraries (need development)
|
||||
|
||||
| Library | What it implements | Key correctness challenge |
|
||||
|---------|-------------------|-------------------------|
|
||||
| cl-dag / cl-cid | IPLD Merkle DAG — CID encoding, multihash, DAG tree operations | Spec compliance (IPLD test vectors) |
|
||||
| cl-did | W3C DID — Ed25519 key wrapping, DID document construction, did:key resolution | Spec compliance (W3C test suite) |
|
||||
| cl-jose | JWE/JWS — envelope serialization, key wrapping modes, algorithm selection | Surface area (combinatorial spec, not deep math) |
|
||||
| cl-double-ratchet | Signal Double Ratchet — DH ratchet, symmetric ratchet, associated data, header encryption | **Highest risk** — one byte wrong in associated data breaks every message |
|
||||
| cl-bip | BIP-32/39/44 — mnemonic encoding, HD key derivation, hardened vs non-hardened paths | Silent failure (wrong derivation produces wrong keys, no error) |
|
||||
| cl-didcomm | DIDComm v2 — message packing, forwarding, routing, attachment handling | Composes the above libraries; protocol logic correctness |
|
||||
|
||||
### Bridged Sidecars (initial release)
|
||||
|
||||
Replace native CL development risk with battle-tested implementations via CFFI or sidecar processes:
|
||||
|
||||
| Component | Bridge method | Source | Replaced by |
|
||||
|-----------|--------------|--------|-------------|
|
||||
| Double Ratchet | CFFI → libsignal | Signal's C library, MIT license | cl-double-ratchet |
|
||||
| DID operations | CFFI → didkit | Spruce, Rust + C bindings, Apache 2.0 | cl-did |
|
||||
| DIDComm | CFFI → didcomm-rust | DIDComm WG, C bindings, Apache 2.0 | cl-didcomm |
|
||||
| DAG/CID storage | HTTP API → ipfs daemon | IPFS Go daemon, MIT license | cl-dag |
|
||||
| BIP derivation | CFFI or sidecar | libbitcoin or bip-utils | cl-bip |
|
||||
| JOSE envelopes | CFFI → libjose or OpenSSL CMS | libjose/OpenSSL | cl-jose |
|
||||
|
||||
### Infrastructure Code (Passepartout-specific)
|
||||
|
||||
These are not libraries but Passepartout systems that must be built:
|
||||
|
||||
| Component | Role |
|
||||
|-----------|------|
|
||||
| PDS server | HTTP/WS API, message routing, storage orchestration, gate integration |
|
||||
| Relay server | Pub/sub message routing between PDSs, connection management |
|
||||
| Client API layer | Protocol endpoints the mobile apps call |
|
||||
|
||||
### Risk Distribution
|
||||
|
||||
- **Low risk:** cl-dag, cl-did, cl-bip — published standards with test vectors, or bridged via sidecar
|
||||
- **Medium risk:** cl-jose — large spec surface area but well-documented
|
||||
- **High risk:** cl-double-ratchet — protocol logic depth, must get state transitions exactly right
|
||||
|
||||
The sidecar strategy collapses the high-risk items to near-zero implementation risk for the initial release.
|
||||
|
||||
← [[id:8cb760e2-37c6-4a78-af4d-f89f69d1678b][Stage 0 — Now]] → [[id:4a1f23b0-abc3-4def-9876-543210abcdef][Stage 2 — Verification]]
|
||||
|
||||
:PROPERTIES:
|
||||
|
||||
@@ -1,54 +0,0 @@
|
||||
---
|
||||
title: Stage 2 Architecture
|
||||
type: reference
|
||||
tags: :passepartout:architecture:gate:acl2:
|
||||
created: 2026-05-28
|
||||
---
|
||||
|
||||
← Stage 2 — Verification Subsystem
|
||||
|
||||
# Stage 2: ACL2 Integration and Risk Profile
|
||||
|
||||
## ACL2 is not a CL library
|
||||
|
||||
ACL2 is a separate system — a theorem prover and programming language with a Lisp-like syntax, not a Common Lisp library you import. It has its own image, its own evaluator, and its own type system (a subset of CL). There are three integration approaches:
|
||||
|
||||
**1. Embed exported compiled code (recommended)**
|
||||
Write the gate's core decision procedures in ACL2, prove them correct, then compile to CL code that runs natively in the PDS process. ACL2's :program mode and defattach mechanism allow verified functions to be called from unverified CL code. The proof artifact is the source; the runtime is the compiled function.
|
||||
|
||||
**2. Subprocess with serialized inputs**
|
||||
The PDS sends the action + context + policy as JSON to an ACL2 subprocess, which evaluates the decision procedure and returns permit/deny. Simpler to implement but adds latency and a trust boundary between the PDS and the ACL2 process.
|
||||
|
||||
**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.
|
||||
|
||||
## Stage 2 risk: design uncertainty, not spec complexity
|
||||
|
||||
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.
|
||||
|
||||
| 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 |
|
||||
| 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 |
|
||||
|
||||
## What makes Stage 2 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 ACL2 verification covers the kernel — "does this decision follow from the policy?" — not the policy itself. Policy changes don't require reproving the kernel; they require writing new policy rules.
|
||||
|
||||
## 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 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
|
||||
- The gate cannot be bypassed; there is no privileged path
|
||||
|
||||
→ Stage 3 — Lisp Machine
|
||||
|
||||
:PROPERTIES:
|
||||
:CREATED: [2026-05-11 Mon]
|
||||
:WEIGHT: 15
|
||||
:ID: 460e06f4-6bfc-4969-89d8-685c0c4434cf
|
||||
:END:
|
||||
@@ -138,10 +138,46 @@ The reasoner is *born at Stage 1* and *hardens through Stage 2*:
|
||||
|
||||
The gate graduates from checking *who* is authorized to checking *what is
|
||||
true*. A policy can say "deny actions based on false premises" — and the
|
||||
reasoner determines which premises are false. This is the connection
|
||||
detects which premises are false. This is the connection
|
||||
between security verification and knowledge verification that the original
|
||||
Cyc architecture required but could not enforce.
|
||||
|
||||
## ACL2 Integration Approaches
|
||||
|
||||
ACL2 is a separate system — a theorem prover and programming language with a Lisp-like syntax, not a Common Lisp library you import. It has its own image, its own evaluator, and its own type system (a subset of CL). There are three integration approaches:
|
||||
|
||||
**1. Embed exported compiled code (recommended)**
|
||||
Write the gate's core decision procedures in ACL2, prove them correct, then compile to CL code that runs natively in the PDS process. ACL2's :program mode and defattach mechanism allow verified functions to be called from unverified CL code. The proof artifact is the source; the runtime is the compiled function.
|
||||
|
||||
**2. Subprocess with serialized inputs**
|
||||
The PDS sends the action + context + policy as JSON to an ACL2 subprocess, which evaluates the decision procedure and returns permit/deny. Simpler to implement but adds latency and a trust boundary between the PDS and the ACL2 process.
|
||||
|
||||
**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.
|
||||
|
||||
## Risk Comparison: Stage 1 vs Stage 2
|
||||
|
||||
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.
|
||||
|
||||
| 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 |
|
||||
| 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 |
|
||||
|
||||
## What Makes Stage 2 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 ACL2 verification covers the kernel — "does this decision follow from the policy?" — not the policy itself. Policy changes don't require reproving the kernel; they require writing new policy rules.
|
||||
|
||||
## 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 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
|
||||
- The gate cannot be bypassed; there is no privileged path
|
||||
|
||||
← [[id:4a1f23b0-abc2-4def-9876-543210abcdef][Stage 1 — Social Protocol]] → [[id:4a1f23b0-abc4-4def-9876-543210abcdef][Stage 3 — Lisp Machine]]
|
||||
|
||||
:PROPERTIES:
|
||||
|
||||
Reference in New Issue
Block a user