cindervm

A deterministic bytecode virtual machine for agent execution. Bytecode is verified before it runs, the whole machine is a value you can snapshot, and a run replays exactly from its journal.

• What this is
• Why bytecode instead of a coroutine
• The three invariants
• Toolchain walkthrough
• The instruction set
• The verifier
• Continuations and replay
• Building from source
• Repository layout
• Stability
• License

An agent run is long-lived, effectful, and resumable. Modelled as a host coroutine, its suspended state is a compiler-generated struct with no serializable form: you cannot write it to disk, inspect it, or resume it in a different process.

cindervm models the run as bytecode on a machine built for it. The library crate (cindervm) holds the machine and its toolchain; three binaries drive it:

The crate has no dependencies outside core, alloc, and std. The hash (hash.rs), the heap arena (heap.rs), and the argument parsing in the binaries are all written in-crate, because this is a trust boundary and every dependency is code you would also be trusting. unsafe is denied crate-wide (#![deny(unsafe_code)]).

Three designs were considered and set aside:

Host coroutines (async fn, async def). Suspension points are implicit and the suspended state has no stable representation. Good for I/O concurrency, wrong for a run you want to move or persist.

Replay-based durable execution. Recovery re-runs the whole program and short-circuits completed calls from a log, which makes one unlogged source of non-determinism enough to diverge. cindervm restores state directly rather than re-deriving it, and every source of non-determinism (NOW, RAND, tool answers) is an instruction that reads from the journal.

Interpreting a live object graph. Serialization becomes a graph walk with identity preservation. A flat operand stack over a flat heap arena of tagged values serializes as a copy of two arrays plus a relocation pass.

The VM approach costs an assembler and a verifier. It buys a machine state that is already a byte string.

Most of the codebase falls out of three rules, stated verbatim at the top of src/lib.rs:

1. The interpreter performs no I/O. interp::Vm::step is a pure function of (image, state, answer). When it needs an effect it returns a trap::Trap and stops; the host answers with a trap::Answer. Replay is exact because replay::Host serves answers from a journal and the interpreter cannot tell the difference: there was never a code path that touched the network.
2. Every value is Copy, tagged, and pointer-free. value::Value is 16 bytes with an explicit tag byte and no Drop. Larger payloads live in the arena behind a value::Handle, an arena-relative offset. Snapshot is two copies and a hash; restore relocates by arithmetic.
3. Verification is a precondition, not a mode. An image::Image cannot be constructed except through verify::admit. By the time the interpreter sees an image, stack depth, operand types, pending-value liveness, branch targets, metering on back-edges, and fork balance have been proven. So interp carries no pc bounds check and no stack-depth check.

.cdx is a macro assembler for the bytecode, meant for tests and examples; the production path is asm::Builder driven by a higher-level frontend. A minimal program and the toolchain applied to it:

        .isa      cdx/4
        .image    "triage"
        .fn       main() -> i32
        .maxstack 1
main:
        ldi       0
        ret

$ cinderc build triage.cdx -o triage.cdxb
wrote triage.cdxb (N bytes, checksum 0x...)

$ cinderc dis triage.cdxb          # disassemble the sealed image
$ cinderc run triage.cdxb --trace  # run, tracing traps and the halt code
$ cinder explain E_PENDING_ESCAPE  # look up a diagnostic code

cinderc build assembles, then calls verify::admit, then writes the sealed .cdxb. cinderc run reads an image, constructs a Vm with default limits, and drives the step loop, answering each trap. cinder run delegates to cinderc run; cinder explain <CODE> prints the blurb and phase for a diagnostic code, or lists every known code when the argument is unrecognised.

cdx/4, defined once in src/isa.rs as a const table (opcode, operand shape, stack effect, type rule, effect class). The assembler mnemonics, the disassembler, and the verifier's transfer functions all read from that single table, and cinderc --emit-isa-md renders it. Encoding is fixed 4-byte (INSN_LEN = 4) with a wide prefix (0xFF) promoting the operand field for large constant pools.

The opcode classes, from the ISA table:

Floats, indirect branches, and host pointers are deliberately absent: each would break serializability or the verifier's static control-flow graph.

src/verify.rs is a JVM-style verifier: abstract interpretation over the control-flow graph (src/cfg.rs), iterated to a fixpoint, with merge points unifying the abstract frames. The type lattice is Bottom ⊑ {Int, Str, Bytes, List, Handle, Pending} ⊑ Top, with Top illegal at any use site (isa::Ty). It runs at load and proves, among other properties:

• stack depth at every instruction is single-valued and within maxstack;
• every operand has a type the instruction accepts;
• no Pending value is live at a return or a snapshot boundary, so no snapshot can capture a half-issued effect nobody is awaiting;
• branch targets land on real instructions in the same function;
• every cycle in the CFG contains a metering instruction, so a runaway loop burns budget rather than wall-clock.

Diagnostics carry source spans from the assembler (src/diag.rs), so a verify failure on hand-written .cdx reads like a compiler error with a code such as E_PENDING_ESCAPE, which cinder explain can describe.

A snapshot is the machine flattened to a byte string: a header binding it to an image hash, the call frames, the operand slots, the heap arena, the context ring, and the budget ledger, sealed with a content hash (src/cont.rs). cont::restore validates the hash, the image binding, and every handle's extent before it reconstructs, so a snapshot from a different image fails with an image mismatch rather than a wild jump.

The journal (src/journal.rs) is append-only and hash-chained: each record commits to the previous record's hash, so a truncated or edited journal is detectable. replay::Host (src/replay.rs) serves the interpreter from that journal instead of from a live host; if the interpreter asks for something the journal does not have next, that is a divergence error naming the record.

Requires Rust (pinned in rust-toolchain.toml). The Makefile is the source of truth for what CI runs; .github/workflows/ci.yml calls the same targets.

cargo build --release            # library + cinderc, cinder, cinder-fuzz
cargo test                       # unit tests, including the invariant tests
cargo clippy --all-targets       # lints configured in Cargo.toml
cargo run --bin cinderc -- --emit-isa-md   # regenerate the ISA reference

The release profile uses fat LTO, a single codegen unit, panic = "abort", and stripped symbols (Cargo.toml). The fuzz profile turns on debug assertions and overflow checks so the fuzzer catches arithmetic and arena mistakes.

The Rust core is intentionally flat; module boundaries follow the machine's structure.

cindervm/
├── src/
│   ├── lib.rs        crate root, the three invariants, #![deny(unsafe_code)]
│   ├── isa.rs        opcode table, encoding, stack effects, type rules
│   ├── value.rs      tagged 16-byte Value, arena handles, coercions
│   ├── lex.rs        .cdx tokenizer with span tracking
│   ├── asm.rs        parser, symbol resolution, fixups, encoder
│   ├── image.rs      .cdxb container: sections, header, sealing
│   ├── cfg.rs        basic blocks, dominators, loop headers
│   ├── verify.rs     abstract interpreter, type lattice, CFG fixpoint
│   ├── interp.rs     the dispatch loop and instruction semantics
│   ├── frame.rs      call frames and operand stack windows
│   ├── heap.rs       bump arena, handle validation
│   ├── cont.rs       snapshot / restore, relocation, validation
│   ├── journal.rs    hash-chained record log and cursor
│   ├── replay.rs     journal-backed host, divergence detection
│   ├── budget.rs     two-phase reservation ledger
│   ├── ctx.rs        context ring, windowing, token accounting
│   ├── trap.rs       the interpreter/host boundary type
│   ├── wire.rs       frame protocol codec (behind the `wire` feature)
│   ├── diag.rs       spans, stable error codes, rendered diagnostics
│   ├── disas.rs      disassembler and `cinderc dis` output
│   ├── hash.rs       in-crate content hashing
│   └── bin/
│       ├── cinderc.rs     assembler / runner CLI
│       ├── cinder.rs      version / explain / run
│       └── cinder_fuzz.rs mutation fuzzer
└── docs/
    ├── internal-contract.md   frozen inter-module interface
    └── assets/                the three SVG identity assets

0.x: the library API is not stable. The .cdxb container carries a format version and the ISA is versioned separately (cdx/4, ISA_VERSION = 4); adding opcodes bumps the ISA minor, changing the meaning of one bumps the ISA version. CHANGELOG.md tracks changes.

Apache-2.0. See LICENSE.