From 0956711af4b5246b6fffc6fb96e0b1627f8fcf19 Mon Sep 17 00:00:00 2001 From: Hermes Date: Thu, 4 Jun 2026 19:43:56 +0000 Subject: [PATCH] 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 --- .org-ids.json | 2 - .../stages/stage-1-dependency-map.org | 84 ------------------- .../stages/stage-1-social-protocol.org | 67 +++++++++++++++ .../stages/stage-2-acl2-integration.org | 54 ------------ .../stages/stage-2-verification.org | 38 ++++++++- 5 files changed, 104 insertions(+), 141 deletions(-) delete mode 100644 projects/passepartout/architecture/stages/stage-1-dependency-map.org delete mode 100644 projects/passepartout/architecture/stages/stage-2-acl2-integration.org diff --git a/.org-ids.json b/.org-ids.json index 1c17100..636f755 100644 --- a/.org-ids.json +++ b/.org-ids.json @@ -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", diff --git a/projects/passepartout/architecture/stages/stage-1-dependency-map.org b/projects/passepartout/architecture/stages/stage-1-dependency-map.org deleted file mode 100644 index 8066cc9..0000000 --- a/projects/passepartout/architecture/stages/stage-1-dependency-map.org +++ /dev/null @@ -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: \ No newline at end of file diff --git a/projects/passepartout/architecture/stages/stage-1-social-protocol.org b/projects/passepartout/architecture/stages/stage-1-social-protocol.org index 40c50d2..88b4dff 100644 --- a/projects/passepartout/architecture/stages/stage-1-social-protocol.org +++ b/projects/passepartout/architecture/stages/stage-1-social-protocol.org @@ -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: diff --git a/projects/passepartout/architecture/stages/stage-2-acl2-integration.org b/projects/passepartout/architecture/stages/stage-2-acl2-integration.org deleted file mode 100644 index e2dcd5e..0000000 --- a/projects/passepartout/architecture/stages/stage-2-acl2-integration.org +++ /dev/null @@ -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: \ No newline at end of file diff --git a/projects/passepartout/architecture/stages/stage-2-verification.org b/projects/passepartout/architecture/stages/stage-2-verification.org index 2c9e9a8..32184b8 100644 --- a/projects/passepartout/architecture/stages/stage-2-verification.org +++ b/projects/passepartout/architecture/stages/stage-2-verification.org @@ -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: