gbrain: sync converted org-mode brain files

projects/passepartout/architecture/architecture.org

@@ -62,6 +62,34 @@ The LLM layer is probabilistic. The ACL2 layer is deductive. The gate architectu
 
 The gate does not depend on OS privilege boundaries because it is in the evaluation loop itself. This is the architectural reason for the Lisp machine: a conventional OS interposes between the gate and the hardware. A Lisp machine eliminates that interposition by making the gate part of the evaluator.
 
+**How the gate knows which procedure belongs to which domain.**
+
+Every action entering the gate carries a domain tag. The tag is set by context — a file write under /home/user/documents/ gets the "documents" domain, a network call to an approved registry gets "network", a shell command running a compiler gets "software-engineering". The domain tags form a tree: "files" has children "documents", "code", "config", "system", each with its own rule set.
+
+The gate maintains a procedure registry mapping domain tags to ACL2-verified boundary functions. When an action arrives, the gate looks up the most specific domain tag that has a registered procedure. If "documents" has one, it uses that. If not, it walks up to "files". If no domain in the tree has a procedure, the action falls under LLM authority bounded only by the generic outer fence.
+
+Domain tags are defined in the policy configuration — a hierarchy of Org headings or YAML that maps path patterns, network destinations, and command prefixes to domain names. New domains can be added at any time with no code changes, just a policy edit. New domains start with no verified procedures and rely entirely on the LLM until experience accumulates and ACL2 boundaries are written.
+
+**How the verified procedure registry grows.**
+
+Verified procedures are not all written upfront. The initial gate ships with a minimal set of obviously correct outer boundaries — three to five rules that prevent catastrophic, irreversible actions. The registry grows through two mechanisms:
+
+1. Mistake-driven hardening: when the LLM's provisional authority causes harm, that action is logged, a human or automated process writes an ACL2 conjecture to prevent it, the Prover verifies it, and the resulting boundary function is added to the registry under the relevant domain tag.
+
+2. Adversarial probing: the gate randomly injects probe actions that would violate known desirable boundaries but are caught before execution. These probes generate the same hardening signal even when no mistake occurred. They cover the blind spot where the LLM always gets it right and no error is ever logged.
+
+3. Syscall wrappers: every action that crosses from the Lisp image into the host OS passes through a gate wrapper that records the kernel's response. When the kernel denies an action (permissions, seccomp, namespaces) that the gate had no rule for, the wrapper translates that kernel denial into a hardening signal — "the kernel prevented this. Consider codifying it as an ACL2 boundary." This covers the blind spot where the kernel catches the problem first and the gate never sees the danger.
+
+These three channels feed a queue. The autodidactic loop (or a human reviewer) periodically processes the queue, drafts ACL2 conjectures, runs the Prover, and deploys new verified boundaries. The gate's procedure registry grows transaction by transaction, domain by domain, from three rules to hundreds to thousands over the lifetime of the system.
+
+**The two blind spots and their mitigations.**
+
+Blind spot 1 — the LLM always gets it right. If the LLM never attempts a dangerous action in a domain, no mistake is logged, and no ACL2 boundary is proposed. Mitigation: adversarial probing. The gate regularly tests the LLM with actions that would violate known safety properties, logged before execution. These probes generate hardening signals regardless of the LLM's accuracy.
+
+Blind spot 2 — the kernel prevents the action before the gate sees it. If the LLM tries to write to /etc/shadow and the kernel's DAC permissions reject it, the LLM sees a permission error, the gate sees a failed action, but neither knows a safety boundary was enforced. Mitigation: syscall wrappers. The gate wraps every kernel transition and records the reason for denial. A kernel EACCES on /etc/shadow becomes a hardening signal: "the kernel has a rule about /etc/shadow that the gate doesn't. Codify it."
+
+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.
+
 **The social protocol: provable communication.**
 
 The social protocol extends the verified semantics beyond a single machine. It provides: