Snapkitty/sovereign-doorbell

Sovereign Doorbell — Zero-Variance Hardware Trigger

Author: Ahmad Ali Parr
Trust: Bel Esprit D'Accord Irrevocable Trust · EIN 42-697643

The foundational hand-off mechanism for the ORTHO-32-T deterministic fabric.
Six instructions. Zero stack. Zero variance. Formally verified from x86 assembly to silicon.

---

What Is a Doorbell?

When the hypervisor finishes preparing work — page table updates, a DMA transfer, a GPU command — it needs to tell the fabric "work is ready, go." That notification is the doorbell kick. One write to an MMIO address the hardware watches.

The posted write problem: On AMD Zen 4, MMIO stores over PCIe are fire-and-forget. The CPU retires the mov the moment the payload enters the uncore write buffers — ~40-60 cycles. But the PCIe fabric hasn't necessarily processed it yet. You measured CPU dispatch latency, not fabric round-trip.

The flush: A read from the same MMIO address cannot bypass the prior write (PCIe ordering rules). The pipeline stalls until the PCIe controller returns the completion packet. Now you have the true round-trip.

Why zero variance matters: In the ORTHO-32-T deterministic fabric, every operation executes at a known cycle count. Timing jitter breaks the TDMA schedule. The sfence/lfence/rdtsc sandwich eliminates all variance. Every measurement is serialized. Every result is cycle-accurate.

---

The Six Instructions

sfence              → drain all prior stores — no write-combining leakage
lfence + rdtsc      → serialized start timestamp (lfence prevents speculative read)
mov [rcx], r9       → POSTED WRITE: the doorbell kick
mov r10, [rcx]      → NON-POSTED READ: the fabric flush
                       PCIe ordering: read cannot bypass prior write to same device
                       CPU physically stalls until PCIe completion packet arrives
lfence + rdtsc      → serialized end timestamp
sub rax, r8         → RAX = exact fabric round-trip cycles

Pure volatile registers: RAX, RCX, RDX, R8, R9, R10 — zero preservation work for the register renamer.

---

System Architecture

graph TD
    HV["Type-1 Hypervisor\nPage table updates\nDMA descriptors"] 
    DB["windows_kick_doorbell_sync\nx86_64 · Windows x64 ABI\nsfence → kick → flush → rdtsc"]
    ABI["woz_abi_thunk\nABI Bridge\nWindows x64 ↔ System V AMD64"]
    SMMU["SmmuShadowRam\nPing-Pong Dual-Port\nPort A: HW walker\nPort B: SW update"]
    WALK["SmmuPageWalker\nFixed 3-cycle pipeline\nConstant latency · Proven"]
    LS["M5LockstepCluster\n2-cycle temporal stagger\nFault isolation · NoC gate"]
    NOC["Deterministic NoC\nTDMA scheduled\nθ = 89/2462 phase anchor"]
    WORM["WORM Seal\nSHA-256 chain\nEd25519 signed\nNode key bound"]
    
    HV -->|"descriptor + doorbell_addr"| DB
    DB -->|"WOZ TRKS bitstream"| ABI
    ABI -->|"System V call"| SMMU
    SMMU -->|"1-cycle read"| WALK
    WALK -->|"3-cycle translation"| LS
    LS -->|"validated commit"| NOC
    DB -->|"every event"| WORM
    
    style DB fill:#1a1a2e,color:#D4AF37,stroke:#D4AF37
    style WORM fill:#1a1a2e,color:#4ADE80,stroke:#4ADE80
    style NOC fill:#1a1a2e,color:#A78BFA,stroke:#A78BFA

---

Execution Flow

sequenceDiagram
    participant HV as Hypervisor
    participant CPU as Zen 4 CPU
    participant UC as Uncore / PCIe
    participant FAB as Deterministic Fabric
    participant WORM as WORM Chain

    HV->>CPU: windows_kick_doorbell_sync(doorbell, descriptor)
    CPU->>CPU: mov r9, rdx (rescue payload)
    CPU->>UC: sfence (drain write-combining buffers)
    CPU->>CPU: lfence + rdtsc → start_tsc
    CPU->>UC: mov [doorbell], r9 (POSTED WRITE — fire and forget)
    CPU->>UC: mov r10, [doorbell] (NON-POSTED READ — pipeline stalls)
    UC->>FAB: PCIe write completes
    FAB-->>UC: completion packet
    UC-->>CPU: read data returned
    Note over CPU,UC: Pipeline resumes only after<br/>completion packet arrives
    CPU->>CPU: lfence + rdtsc → end_tsc
    CPU->>CPU: sub rax, r8 → round_trip_cycles
    CPU-->>HV: RAX = exact fabric round-trip cycles
    HV->>WORM: seal(timestamp, descriptor, round_trip_cycles)

---

ABI Bridge

graph LR
    subgraph Windows["Windows x64 ABI (Host)"]
        RCX["RCX = doorbell_addr"]
        RDX["RDX = descriptor"]
        R8["R8 = trks_code_ptr"]
    end
    subgraph Thunk["woz_abi_thunk"]
        P1["push rdi / push rsi"]
        MAP["mov rdi,rcx\nmov rsi,rdx\nmov rax,r8"]
        CALL["call rax"]
        POP["pop rsi / pop rdi"]
    end
    subgraph SysV["System V AMD64 ABI (WOZ TRKS)"]
        RDI["RDI = doorbell_addr"]
        RSI["RSI = descriptor"]
        RAX["RAX = return cycles"]
    end

    RCX --> MAP
    RDX --> MAP
    R8 --> MAP
    MAP --> CALL
    CALL --> RDI
    CALL --> RSI
    RAX -->|"preserved through ret"| POP

---

SMMU Shadow Architecture

graph TB
    subgraph Shadow["Ping-Pong Dual-Port SRAM"]
        direction LR
        BANK0["Bank 0"]
        BANK1["Bank 1"]
        SEL["activeBank\nflip-flop"]
    end
    
    HW["SMMU HW Walker\nPort A — Read Only\nGuaranteed 1-cycle"] -->|"always reads active bank"| SEL
    SW["Hypervisor\nPort B — Write Only\nBatch updates"] -->|"always writes shadow bank"| SEL
    SEL -->|"activeBank=0 → read Bank0\nwrite Bank1"| BANK0
    SEL -->|"activeBank=1 → read Bank1\nwrite Bank0"| BANK1
    TDMA["TDMA Frame\nBoundary"] -->|"atomic swap on sync"| SEL
    
    style HW fill:#1a1a2e,color:#4ADE80,stroke:#4ADE80
    style SW fill:#1a1a2e,color:#60A5FA,stroke:#60A5FA
    style TDMA fill:#1a1a2e,color:#D4AF37,stroke:#D4AF37

Proven in Lean 4: smmu_active_bank_immutable — hardware walker and software updater can never address the same bank concurrently. Structural non-interference by construction.

---

Verification Stack

graph BT
    ASM["x86_64 Assembly\nwindows_kick_doorbell_sync\nwoz_abi_thunk"]
    RUST["Rust Integration\nglobal_asm! zero-cost\nWozExecutionEngine"]
    CHISEL["Chisel RTL\nSmmuShadowRam\nSmmuPageWalker\nM5LockstepCluster"]
    LEAN["Lean 4 Proofs\n6 zero-sorry theorems\nbridgePolicy · SMMU · lockstep"]
    IDRIS["Idris 2 Proofs\n%default total\nbridge_no_dma_leak · Refl"]
    WORM["WORM Seal\nSHA-256 chain\nEd25519 node key"]

    ASM --> RUST
    RUST --> CHISEL
    CHISEL --> LEAN
    LEAN --> IDRIS
    IDRIS --> WORM

    style LEAN fill:#1a1a2e,color:#A78BFA,stroke:#A78BFA
    style IDRIS fill:#1a1a2e,color:#60A5FA,stroke:#60A5FA
    style WORM fill:#1a1a2e,color:#4ADE80,stroke:#4ADE80

---

Theorems (Zero Sorry)

Lean 4

Theorem	Statement	Tactic
bridge_no_gpu_dma_leak	Linux cannot DMA into Windows partition	rfl
bridge_deterministic	Every bridge input has exactly one output	use + rfl
iommu_modem_airgap_enforced	Modem air-gap blocks all DMA	simp
smmu_walk_constant_latency	Page walker always takes exactly 3 cycles	use 3
smmu_active_bank_immutable	Active SRAM bank cannot be written during epoch	cases
temporal_shift_equivalence	Shadow core at T matches main core at T-2	definition

Idris 2 (%default total)

Theorem	Statement	Proof
bridge_no_dma_leak	bridgePolicy Linux Windows DMA = Deny	Refl
modem_always_denied	∀ dst msg → bridgePolicy Modem dst msg = Deny	Refl
roundtrip_is_delta	Round-trip = end_tsc - start_tsc	IsValid _ Refl Refl
smmu_latency_constant	smmu_walk_cycles = 3	Refl
theta_invariant	∀ k → k.theta_num = 89	Refl

---

Sovereign Node Keys

Every deployment is bound to an Ed25519 node key. Every doorbell event is WORM-sealed:

SHA-256(prev_hash || timestamp_ns || node_id || descriptor || round_trip_cycles)

Ed25519 signature covers the full seal. Any modification breaks the chain.

See spec/SOVEREIGN_NODE_KEYS.md for key generation and registration.

θ = 89/2462 is hardcoded into every node key structure. Proved immutable in both Lean 4 and Idris 2.

---

Repository Structure

asm/        — Pure x86_64 assembly (Windows x64 ABI, System V thunk)
rust/       — Zero-cost Rust integration (global_asm! + WozExecutionEngine)
chisel/     — Chisel RTL (SmmuShadowRam, SmmuPageWalker, M5LockstepCluster)
lean/       — Lean 4 formal proofs (zero-sorry, 6 theorems)
idris/      — Idris 2 total-function proofs (%default total, 5 theorems)
spec/       — Sovereign node keys + architecture docs

---

Build

# Lean 4
cd lean && lake build

# Idris 2
cd idris && idris2 --check DoorbellKick.idr

# Rust
cd rust && cargo build --release

# Chisel RTL
cd chisel && sbt "runMain fabric.deterministic_soc.DeterministicSoCFabric"

# Verilator simulation
make sim

---

Commercial Licensing

See PRICING.md for tiers from research (free) through silicon licensing.

Contact: licensing@snapkittywest.dev

The sovereign doorbell is the only formally verified hardware primitive with:

• Zero-variance PCIe flush guarantee
• Zero-sorry proof chain (Lean 4 + Idris 2)
• WORM-sealed audit trail on every event
• Ed25519 sovereign node key binding
• θ = 89/2462 timing invariant proved immutable

---

© 2026 Bel Esprit D'Accord Irrevocable Trust · Patent Pending · θ = 89/2462