Message pipeline

The verified message pipeline. Mirrors lean-cbcl/LeanCbcl/Pipeline.lean. Input strings (from stdin, the CLI, a WASM/FFI/NIF wrapper, or an arena agent) traverse a fixed sequence of steps: parse → parse_message → validate → expand → causal verify → shape check → success. Success yields a ValidMessageGrammar witness; any step failure produces a ValidationError carrying a blame attribution.

graph LR
    input["Input String\n(stdin / argv / NIF / FFI)"]
    parse-step["Step 1 Parse\ncrates/cbcl-parser/src/parser.rs"]
    parse-message-step["Step 2 Parse Message\ncrates/cbcl-parser/src/message_parser.rs"]
    validate-step["Step 3 Validate\ncrates/cbcl-core/src/r1.rs r3.rs"]
    expand-step["Step 4 Expand\ncrates/cbcl-core/src/template.rs"]
    causal-step["Step 6a Causal Verify\ncrates/cbcl-core/src/protocol.rs"]
    shape-step["Step 6b Shape Check\ncrates/cbcl-core/src/r5.rs shape.rs"]
    success["Success: ValidMessageGrammar\ncrates/cbcl-parser/src/pipeline.rs"]
    failure["ValidationError + Blame\ncrates/cbcl-core/src/blame.rs"]

    input --> parse-step
    parse-step -->|"S-expr"| parse-message-step
    parse-message-step -->|"Message"| validate-step
    validate-step -->|"R1/R2/R3 OK"| expand-step
    expand-step -->|"expanded Message"| causal-step
    causal-step -->|"causally OK"| shape-step
    shape-step -->|"shape OK"| success
    parse-step -->|"ParseError"| failure
    parse-message-step -->|"MalformedMessage"| failure
    validate-step -->|"R1/R2/R3 violation"| failure
    expand-step -->|"R2FuelExhausted"| failure
    causal-step -->|"CausalViolation"| failure
    shape-step -->|"ShapeViolation"| failure

Steps

Step 1 — Parse (crates/cbcl-parser/src/parser.rs). Tokenize and parse an S-expression. Hand-rolled recursive-descent (ADR-001), O(n), fuel-bounded. ParseError on malformed input. Equivalent to the DPDA decision (det_parser.rs ↔ DetParser.lean: agentDetParser_agrees).

Step 2 — Parse message (crates/cbcl-parser/src/message_parser.rs + cbcl-core/message.rs). Lift S-expression into a typed Message. MalformedMessage on grammar violation. MessageParser.lean proves grammar soundness AND completeness (ValidMessageGrammar ↔ parseMessage).

Step 3 — Validate (r1.rs, r3.rs, plus the syntactic part of r2.rs). Validate dialect-related safety constraints. Errors: R1RecursivePerformative, R2ResourceBoundsInvalid, R3CoreOverride. R1 detection via DFS — proven sound and complete in Lean.

Step 4 — Expand (template.rs, evaluator.rs). Expand template substitutions under R2 fuel. R2FuelExhausted if a substitution exceeds the dialect’s declared depth/expansion bounds. TemplateExpansion.lean proves expansion terminates within declared bounds.

Step 6a — Causal verify (protocol.rs). For dialects with a (protocol ...) clause, verify_causal checks that incoming messages are well-ordered against the agent’s MessageStore. Failure: CausalViolation { violation, blame }.

Step 6b — Shape check (r5.rs, shape.rs). Final check before success. Failure: ShapeViolation { violation, blame }. R5 covers REQ-208 + REQ-222.

Fail-closed guarantee

REQ-231: fail-closed, no bypass, no partial checks. The pipeline cannot return success unless every step succeeded — there is no path that elides causal verification or shape checking once dialect-installed.

Two entry points:

run_pipeline — light path: parse + validate, no runtime context. Used in test harnesses and FFI parse-only paths.
run_pipeline_full — full path, takes a DialectRegistry and MessageStore.

Lean: pipeline_success_grammar proves success ⟹ ValidMessageGrammar.

The dialect mechanism — CBCL’s homoiconic self-extension surface. A dialect is itself a CBCL message in S-expression syntax. Installation runs through three gating safety checks (R1, R2, R3), one closure check (DCFL tag preservation via msg_tag.rs), and finally lands in the per-agent DialectRegistry. Once installed, the agent runtime dispatches incoming messages by pattern-matching against installed performatives and expanding their templates under R2 fuel. Dialects propagate between agents via the gossip protocol, with safety re-checked at the receiving end.

This is the architectural distinguisher of CBCL: agents define and exchange new vocabularies at runtime without escaping the DCFL complexity class. Lean theorem dcfl_preserved (lean-cbcl/LeanCbcl/DeterministicUnion.lean) proves that installing a fresh-named dialect into an agent with unique dialect names preserves DCFL membership of the agent’s message language. R3CorePreservation.lean’s install_preserves_core + install_no_core_redefinition compose to the runtime guarantee that the eight core performatives can never be shadowed.

graph LR
    dialect-source["Dialect Source\n(S-expression text)"]
    dialect-parser["Dialect Parser\ncrates/cbcl-parser/src/dialect_parser.rs"]
    registry["Dialect Registry\ncrates/cbcl-core/src/dialect.rs"]
    template-expand["Template Expansion\ncrates/cbcl-core/src/template.rs"]
    r1-check["R1 No Recursion\ncrates/cbcl-core/src/r1.rs"]
    r2-check["R2 Resource Bounds\ncrates/cbcl-core/src/r2.rs"]
    r3-check["R3 Core Preservation\ncrates/cbcl-core/src/r3.rs"]
    msg-tag-check["DCFL Tag Preservation\ncrates/cbcl-core/src/msg_tag.rs"]
    gossip-propagation["Gossip Propagation\ncrates/cbcl-core/src/gossip.rs"]
    agent-runtime["Agent Runtime\ncrates/cbcl-core/src/agent.rs"]

    dialect-source --> dialect-parser
    dialect-parser -->|"parse_dialect"| r1-check
    r1-check -->|"DFS sound + complete"| r2-check
    r2-check -->|"static bounds OK"| r3-check
    r3-check -->|"no core override"| msg-tag-check
    msg-tag-check -->|"dcfl_preserved"| registry
    registry -->|"installed"| agent-runtime
    agent-runtime -->|"message dispatch"| template-expand
    template-expand -->|"R2 fuel"| agent-runtime
    registry -.->|"install + propagate"| gossip-propagation
    gossip-propagation -.->|"merges into peer"| registry

Components

Dialect parser (crates/cbcl-parser/src/dialect_parser.rs). Parses an S-expression dialect source into a structured dialect term ready for safety checks.

R1 — no recursion (crates/cbcl-core/src/r1.rs). DFS over performative templates. Sound and complete (Lean: r1_mutual_sound + dfsNoCycle_complete).

R2 — resource bounds (crates/cbcl-core/src/r2.rs). Validates that ResourceBounds (depth, expansion, time) are within the agent’s configured ceilings; the runtime version of the check enforces them per-message via fuel consumption.

R3 — core preservation (crates/cbcl-core/src/r3.rs). The eight core performatives (tell, ask, reply, hello, bye, ok, error, cancel) cannot be redefined. Lean: R3CorePreservation.install_preserves_core + install_no_core_redefinition.

DCFL tag preservation (crates/cbcl-core/src/msg_tag.rs). Deterministic tagging shows the new dialect’s grammar union remains decidable. Lean: dcfl_preserved.

Dialect registry (crates/cbcl-core/src/dialect.rs). Per-agent store of installed dialects.

Template expansion (crates/cbcl-core/src/template.rs). Pure declarative pattern→template substitution. Iteration, recursion, and reflection are all forbidden by R1; expansion size and depth are capped by R2 fuel. Used by the evaluator at message-dispatch time.

overall

Overall architecture

Workspace-level view of the CBCL Rust implementation. The workspace is a strict purity-zoned Cargo workspace: pure deterministic core crates (cbcl-core, cbcl-parser) under #![forbid(unsafe_code)] + no_std + alloc, surrounded by effectful shell crates (cbcl-cli, cbcl-wasm, cbcl-ffi, cbcl-erl, cbcl-arena). Parallel to the Rust workspace lives lean-cbcl/, a Lean 4 formalization that machine-checks safety properties of the core algorithms.

graph LR
    cbcl-core["cbcl-core\ncrates/cbcl-core/src/"]
    cbcl-parser["cbcl-parser\ncrates/cbcl-parser/src/"]
    cbcl-cli["cbcl-cli\ncrates/cbcl-cli/src/"]
    cbcl-wasm["cbcl-wasm\ncrates/cbcl-wasm/src/"]
    cbcl-ffi["cbcl-ffi\ncrates/cbcl-ffi/src/"]
    cbcl-erl["cbcl-erl\ncrates/cbcl-erl/src/"]
    cbcl-arena["cbcl-arena\ncrates/cbcl-arena/src/"]
    lean-cbcl["lean-cbcl\nlean-cbcl/"]

    cbcl-parser -->|"types, R1-R5, pipeline deps"| cbcl-core
    cbcl-cli -->|"parse, verify, agent REPL"| cbcl-parser
    cbcl-cli -->|"agent + gossip simulation"| cbcl-core
    cbcl-wasm -->|"parse_message, verify_dialect"| cbcl-parser
    cbcl-wasm -->|"agent, dialect"| cbcl-core
    cbcl-ffi -->|"parse, agent send/free"| cbcl-parser
    cbcl-ffi -->|"agent, evaluator"| cbcl-core
    cbcl-erl -->|"verify_dialect NIF"| cbcl-parser
    cbcl-erl -->|"core types"| cbcl-core
    cbcl-arena -->|"messages, dialects"| cbcl-core
    cbcl-arena -->|"pipeline parsing"| cbcl-parser
    lean-cbcl -.->|"machine-checked proofs of"| cbcl-core

The crates

Pure core

cbcl-core — crates/cbcl-core/src/ · ~17k LoC. 23 modules covering S-expressions, messages and performatives, dialect registry, runtime agents, the message evaluator, template expansion, pattern matching, canonical serialization, the five safety constraints (R1–R5), blame attribution, shape and causal-protocol verification, deterministic message tagging, gossip propagation, policy engine, and message store. Largest modules: agent.rs (1669), store.rs (1694), protocol.rs (1715).

cbcl-parser — crates/cbcl-parser/src/. Hand-rolled recursive-descent parser (ADR-001) and the verified pipeline. Five parsers (S-expr, message, dialect, protocol, shape) feed into one pipeline (parse → parse_message → validate → expand → causal verify → shape check). Pure (no_std + alloc, #![forbid(unsafe_code)]). Mirrored by lean-cbcl/LeanCbcl/Parser.lean and Pipeline.lean.

Effectful shells

cbcl-cli — crates/cbcl-cli/src/main.rs, ~400 LoC. clap-based subcommand dispatch. Subcommands: parse, verify, agent (interactive REPL), simulate (gossip). See Command surface.

cbcl-wasm — Two-tier API (ADR-003): pure WASM exports always available on wasm32, plus wasm-bindgen JS interop behind the bindgen feature. API surface: parse_message, verify_dialect, create_agent, send_message. Provides its own no_std allocator and panic handler for wasm32 cdylib builds.

cbcl-ffi — C FFI bindings via cbindgen. Public API: cbcl_parse_message, cbcl_verify_dialect, cbcl_agent_new, cbcl_agent_send, cbcl_agent_free, cbcl_string_free. Returns CbclResult { data, error } where the caller frees data with cbcl_string_free.

cbcl-erl — Erlang/BEAM NIF binding (SPEC-009). BEAM module name cbcl_erl, loaded from libcbcl_erl.{so,dylib} via rustler 0.36. Each NIF is split into a #[rustler::nif] wrapper and an env-free *_pure helper carrying the real logic — the pure helpers are the only testable surface under cargo test.

summary

CBCL — architecture overview

The Rust implementation of CBCL: a self-extensible, formally verified agent communication language that occupies the deterministic context-free (DCFL) sweet spot between fixed-vocabulary ACLs (KQML, FIPA-ACL) and unrestricted JSON/NL.

The workspace is a strict purity-zoned Cargo workspace — pure deterministic core crates under #![forbid(unsafe_code)] + no_std + alloc, surrounded by effectful shell crates. Parallel to the Rust workspace lives lean-cbcl/, a Lean 4 formalization that machine-checks safety properties (R1–R5) of the core algorithms with zero sorries.

Companion paper: CBCL @ IEEE S&P 2026.

Four views

Overall architecture — workspace structure: pure core, effectful shells, Lean proofs.
Message pipeline — the fixed sequence every message traverses: parse → parse_message → validate → expand → causal-verify → shape-check → success.
Command surface — the cbcl CLI: parse, verify, agent, simulate.
Extension points — dialect installation and gossip; how agents define new vocabulary at runtime without escaping DCFL.

Load-bearing properties

Strict purity boundary (ADR-004, PURITY-MAP). cbcl-core and cbcl-parser are deterministic, no_std + alloc, #![forbid(unsafe_code)]. Effectful code (I/O, CLI, WASM/FFI/NIF, simulation) lives in shell crates that import the core — never the reverse.
Five runtime safety constraints:
- R1 — no recursion in dialect templates
- R2 — resource bounds enforced statically and at runtime
- R3 — the eight core performatives (tell, ask, reply, hello, bye, ok, error, cancel) cannot be redefined
- R4 — integrity via Signer trait
- R5 — shape well-formedness (REQ-222)
DCFL closure under fresh-named dialect installation (Lean theorem dcfl_preserved in lean-cbcl/LeanCbcl/DeterministicUnion.lean).
Fail-closed pipeline (REQ-231) — no path returns success unless every step succeeded.

Source

Architectural data exported from cbcl-rs/.omm/. Each view here has a Lean counterpart that proves its key properties; drift between the Rust implementation and the Lean formalization silently invalidates artefact integrity, so any safety-critical change must update both sides.

Message pipeline

Steps

Fail-closed guarantee

See also