← Church Machine

Figure 1 — Dual-Gate Trusted Security Base Architecture

The complete TSB consists of exactly two hardware gates: mLoad (read path) and mSave (write path). Every capability operation in the entire machine must pass through one or both gates. Any validation failure at any stage routes to the single FAULT handler. ~329 lines of synthesizable Amaranth HDL.

TRUSTED SECURITY BASE (TSB) ~329 lines Amaranth HDL — 5 orders of magnitude smaller than Linux, 2 orders smaller than seL4 mLoad — Read Gate Read-Side Instructions Permission Gate Table R→DREAD W→DWRITE X→LAMBDA L→LOAD S→SAVE E→CALL 1 Permission Check 2 Bounds Check 3 Version Match 4 MAC / Seal Validation 5 G-bit Reset (GC liveness) 6 CR Write (capability register update) 7 Thread Shadow Update ✓ Valid Read Complete FAIL FAIL FAIL FAIL mSave — Write Gate Write to C-List (SAVE) 1 Source GT Version Match 2 Source GT Seal Validation 3 Target C-List Bounds Check 4 B-bit Check (B=1 required) 5 F-bit Detection on Target Slot F=1 → HTTP/tunnel route 6 Seal Recompute (FNV hash) 7 G-bit Reset (GC liveness) 8 Commit to C-List ✓ Valid Write Complete FAIL FAIL FAIL FAIL FAULT Single handler No recovery No fallback Turing Domain DREAD(R) DWRITE(W) LAMBDA(X) Church Domain LOAD(L) SAVE(S) CALL(E) C-List Write SAVE instruction Namespace commit path M-Elevation Bypasses permission check Symmetric Design: mLoad guards every read (7 stages), mSave guards every write (8 stages) Together they form the complete TSB. No capability operation bypasses both gates. G-bit integrated into both paths — every namespace access contributes to GC liveness tracking.
mLoad validation stages
mSave validation stages
B-bit / F-bit propagation control
GC integration / success path
Failure → FAULT
M-elevation (microcode bypass)