WASM Goblins (0)

Capability-secure actors meet verified WASM sandboxes

Trit: 0 (ERGODIC - mediates capabilities ↔ sandboxes)

Verified WASM Runtime Matrix

Goblins → WASM Interaction Patterns

1. Actor as WASM Module

;; Goblins actor that wraps a WASM module
(define (^wasm-actor bcom wasm-bytes)
  (define instance (wasm-instantiate wasm-bytes))
  
  (define (call method . args)
    (wasm-invoke instance method args))
  
  (methods
   [call call]
   [memory (lambda () (wasm-memory instance))]))

2. WASM Module as Actor

;; WASM module exporting Goblins-compatible interface
;; Compiled from Hoot
(define-module (wasm-counter)
  #:export (spawn-counter))

(define (spawn-counter initial)
  (let ([count initial])
    (lambda (msg)
      (match msg
        ['inc (set! count (+ count 1))]
        ['get count]))))

3. Capability Passing via WASM Handles

┌─────────────────────────────────────────────────────────────┐
│                     Goblins Vat                             │
│  ┌─────────┐     ┌─────────┐     ┌─────────┐               │
│  │ Actor A │────→│ WASM    │────→│ Actor B │               │
│  │ (Scheme)│ cap │ Module  │ cap │ (Scheme)│               │
│  └─────────┘     └─────────┘     └─────────┘               │
│       ↑              ↑               ↑                      │
│       └──────────────┴───────────────┘                      │
│              OCapN / CapTP                                  │
└─────────────────────────────────────────────────────────────┘

WASM Syscall Categories

WASI (Base - All Runtimes)

fd_read

fd_write

clock_time_get

random_get

proc_exit

WASIX (Wasmer Extended)

thread_spawn

proc_fork

sock_connect

tty_get/set

futex_*

WAVEN (SGX Memory Virtualization)

Verified Semantics

Iris-Wasm (Coq Mechanized)

Wasm 1.0 Spec ──→ Coq Mechanization ──→ Iris Separation Logic
                                              ↓
                              Robust Capability Safety Proofs

Key properties verified:

• Memory isolation between modules
• Control flow integrity
• Type safety preservation
• Capability encapsulation (MSWasm extension)

Cranelift Verification

CLIF IR ──→ VeriWasm ──→ Machine Code
              ↓
     SFI guarantee preservation
     Constant-time compilation (ct-wasm)

Hoot Bridge (Native Goblins ↔ WASM)

;; Compile Goblins actor to WASM
(use-modules (hoot compile) (goblins))

(define (^portable-actor bcom)
  (lambda (msg)
    (match msg
      ['ping 'pong]
      [('echo x) x])))

;; Compile to WASM with preserved semantics
(compile-actor ^portable-actor
  #:output "actor.wasm"
  #:tail-calls #t        ; Wasm tail-call proposal
  #:gc #t)               ; Wasm GC proposal

Hoot WASM Features

Runtime Selection Matrix

Use Case                          Runtime          Reason
─────────────────────────────────────────────────────────────
Browser + Goblins                 Hoot             Native Scheme semantics
Server + Multi-tenant             Wasmtime         Verified + fast
TEE / Enclave                     WAMR + WAVEN     SGX memory virtualization
Edge / IoT                        wasm3            Minimal footprint
Full POSIX / Terminal             Wasmer + WASIX   TTY + fork + threads
Kubernetes / Cloud Native         WasmEdge         CNCF ecosystem

GF(3) Triad: WASM Runtime Layer

Hoot (+1)      ⊗ Goblins (0)    ⊗ WAVEN (-1)     = 0 ✓
generative       orchestration    verification
Scheme→WASM      actor dispatch   memory isolation

Interaction Examples

1. Nickel Contract → WASM Module

;; Load Nickel-validated config into WASM actor
(define (^config-actor bcom nickel-json)
  (define config (json->scheme nickel-json))
  (define wasm (compile-config-handler config))
  (define instance (wasm-instantiate wasm))
  
  (lambda (key)
    (wasm-invoke instance 'get key)))

2. Juvix Intent → WASM Execution

;; Execute Juvix-compiled intent in sandboxed WASM
(define (^intent-executor bcom intent-wasm)
  (define instance 
    (wasm-instantiate intent-wasm
      #:imports `((geb . ,geb-morphism-table))))
  
  (lambda (resources)
    (wasm-invoke instance 'execute resources)))

3. WASIX Terminal → Goblins REPL

;; REPL actor with terminal capabilities
(define (^repl-actor bcom tty-cap)
  (define (read-eval-print)
    (define input (<- tty-cap 'read-line))
    (define result (eval (read input)))
    (<- tty-cap 'write (format #f "~a\n" result))
    (read-eval-print))
  
  (methods
   [start read-eval-print]))

Security Properties

End-of-Skill Interface

Related Skills

Trit: 0 (ERGODIC - mediates compilation ↔ execution ↔ verification) Key Property: Verified sandboxes + capability discipline = compositional security

Autopoietic Marginalia

The interaction IS the skill improving itself.

Every use of this skill is an opportunity for worlding:

• MEMORY (-1): Record what was learned
• REMEMBERING (0): Connect patterns to other skills
• WORLDING (+1): Evolve the skill based on use

Add Interaction Exemplars here as the skill is used.