AOS / Docs

Crucible Reference

This page is the exhaustive reference for the shipped crucible command-line interface and canonical scenario TOML. Use the task-oriented guides for worked procedures and this page to look up exact option names, accepted values, defaults, required fields, and nested kind tables.

Read Support boundaries before inferring packaged operator support from a schema or public Rust type. The guide map routes from each workflow to this catalog.

The Rust types and Clap declarations are the implementation source of truth. Unknown TOML fields and unknown closed-vocabulary values are rejected. Generate a scenario through the Rust builder and to_canonical_toml whenever possible; its content-addressed IDs are computed values, not labels to invent by hand. See the scenario authoring guide and the Nginx/Curl tutorial. For a conceptual walkthrough of causes, bindings, opportunities, and effects, start with Signal-driven faults.

Direct implementation references:

#Value conventions

Notation or valueMeaning
<path>Host path. Relative paths are resolved from the command's working directory.
<hash>Content address in blake3:<64 lowercase hexadecimal digits> form.
<path-or-hash>A local file/path or an object resolvable from --store.
<dur>Positive integer followed by no suffix, tick, ticks, ns, us, ms, or s. No suffix means ticks; one tick is one nanosecond.
*_nanosUnsigned integer duration in virtual nanoseconds.
*_ticksUnsigned integer virtual-time or scheduler coordinate.
*_basis_pointsInteger probability or factor measured in basis points. Probabilities accept 0..=10000, where 10,000 is 100%.
loss_millionthsInteger link probability in 0..=1000000, where 1,000,000 is 100%.
field? in this pageOptional field. The question mark is documentation notation and is not part of the TOML key.

#Command-line interface

#Global options

Global options may appear before or after the subcommand.

OptionAccepted value and defaultPurposeGuide
--seed <u64|hex>Unsigned decimal, 0x hexadecimal, or canonical seed text; otherwise CRUCIBLE_SEED, then scenario seedOverride the root entropy.Seed resolution
--backend <auto|qemu>auto (default), qemuSelect or discover the local backend. Production builds expose QEMU only.Backend discovery
--daemon <addr>Host/port or HTTP endpointSend a supported lifecycle operation to a daemon instead of running locally.Daemon operation
--daemon-ca <path>Requires --daemon and the other client TLS pathsAuthenticate an HTTPS daemon with this CA certificate.Daemon operation
--daemon-cert <path>Requires --daemon and the other client TLS pathsPresent this client certificate chain to an HTTPS daemon.Daemon operation
--daemon-key <path>Requires --daemon and the other client TLS pathsPresent this client private key to an HTTPS daemon.Daemon operation
--trusted-unauthenticated-daemonRequired for cleartext daemon accessExplicitly acknowledge an unauthenticated endpoint on a trusted network. Conflicts with daemon mutual TLS.Daemon operation
--qemu <path>Discovered when omittedOverride the packaged patched-QEMU executable. Must be paired with --plugin.Backend discovery
--plugin <path>Discovered when omittedOverride the matching QEMU plugin. Must be paired with --qemu.Backend discovery
--store <path>Command-specific default below --artifact-dirSet the content-addressed store root.Artifacts and store
--format <jsonl|json|table|markdown>Terminal: table; non-terminal: jsonlSelect report rendering. jsonl and json are stable machine formats.Output formats
--trace <path>Standard outputWrite the canonical event-log stream to a file.Output formats
--artifact-dir <path>./.crucibleSet the failure-artifact and default savepoint/report directory.Artifacts and store
-v, --verboseRepeatable; default count 0Increase diagnostic verbosity.Running
-q, --quietBoolean; default offSuppress non-essential output.Running
-h, --helpBuilt inPrint top-level or subcommand help.This reference
-V, --versionBuilt inPrint the Crucible version.This reference

Backend values:

ValueMeaning
autoDiscover and validate the packaged QEMU/plugin pair.
qemuRequire the local patched-QEMU production backend.

Production QEMU execution also requires CRUCIBLE_RUN_STATE_ROOT to name a writable, durable directory. Crucible creates content-addressed scenario and monotonic run subdirectories beneath it. Each run records exact Linux process identities (PID, start-time ticks, and executable), staged replacements, and the lifecycle transaction phase. A second live owner is rejected; after an interrupted owner disappears, Crucible verifies or contains every recorded process before admitting a new run. Missing, malformed, or version-mismatched recovery records fail closed.

Every QEMU child also receives a nonzero, monotonically increasing process generation before the plugin accepts fault commands. Terminal lifecycle authorization, durable supervision records, and restored fault state must all name that exact generation. A request or checkpoint from an earlier child is rejected rather than being applied to its replacement.

Output-format values:

ValueMeaning
jsonlNewline-delimited canonical JSON records; preferred for streaming programs.
jsonOne JSON document.
tableHuman-readable terminal table.
markdownMarkdown report, especially useful for retained triage output.

#Commands

CommandPurposeDetailed guide
runExecute a scenario to a terminal condition.Running
verifyRepeat a scenario and compare fingerprints and canonical logs, or compare artifacts.Reproduction
selftestRun packaged determinism gates.Self-test
saveStop at a deterministic coordinate and export a savepoint.Savepoints
resumeContinue from a savepoint or checkpoint.Resume
forkContinue from a savepoint with a new seed or decision override.Fork
replayValidate and reduce a recorded reproduction artifact.Replay
searchExplore a bounded schedule space.State-space search
fuzzSample a scenario family using basic-block coverage.Coverage-guided fuzzing
triageCluster, deduplicate, compare, and minimize findings.Findings and triage
debugInspect a live daemon session at a coordinate; local artifact/savepoint execution currently fails closed.Debugging
serveRun the remote lifecycle API.Daemon operation
completionsGenerate shell completion definitions.Shell completions

#run

Argument or optionRequired/defaultMeaning
SCENARIORequiredCanonical scenario TOML path or content hash.
--until <quiescence|virtual-time|property|stopped>Default quiescenceSelect the terminal condition; see terminal values.
--max-virtual-time <dur>Required with --until virtual-timeStop with timeout after this virtual-time budget.
--max-quanta <n>OptionalStop at an exact scheduler-quantum boundary unless another terminal condition occurs first.
--interactiveOffPause at genesis and read interactive commands from standard input.
--save-on <fail|always|never>Default neverMaterialize an outcome savepoint only on failure, for every outcome, or never.
--watchOffCollect live session-status updates alongside run evidence.

--save-on values:

ValueMeaning
failSave only a failing outcome.
alwaysSave passing, failing, and timeout outcomes.
neverDo not create an outcome savepoint.

#verify

Exactly one of SCENARIO and --compare is required.

Argument or optionRequired/defaultMeaning
SCENARIOAlternative to --compareScenario path or content hash to execute repeatedly.
--runs <n>Default 2Number of executions to compare.
--adversarialOffRun under the hostile host-condition matrix.
--bisectOffOn divergence, run deterministic divergence bisection and print its report.
--compare <a> <b>Alternative to SCENARIOCompare two existing reproduction artifacts using their embedded identities, without executing a scenario or generating a seed.

#selftest

OptionRequired/defaultMeaning
--gates <list>All applicable gatesRun a comma-separated gate subset.
--with-qemuHidden production option; offInclude QEMU-backed gates. This is primarily a package/gate surface.

Test-double builds also compile a test-only --corpus <path> fixture-manifest option; it is not part of the shipped production interface.

Self-test honors the global --format, --trace, and --quiet options. JSONL uses selftest_gate, selftest_scenario, and terminal final_outcome records.

#save

Argument or optionRequired/defaultMeaning
SCENARIORequiredScenario path or content hash.
--at <virtual-time|quiescence|property|marker>RequiredSelect the save boundary; see boundary values.
--label <name>OptionalAdd a human-readable savepoint label.
--max-virtual-time <dur>Required with --at virtual-timeExact virtual-time coordinate at which to save; stagnation and overshoot fail closed.
--property <assertion>Required with --at propertyAssertion ID whose violated phase supplies the boundary.
--marker <name>Required with --at markerGuest-marker ID whose observation supplies the boundary.
--out <path>Default below --artifact-dirSelect the exported savepoint-handle path.

Savepoint handle schema v3 records the selected property violation or guest marker, its exact boundary proof, and a content-addressed canonical predicate payload. The reader rejects mismatched selectors, predicates, terminal conditions, frontiers, and undeclared property identities. The canonical trace exposes the same proof as save_boundary_proof, with percent-encoded selector values. Older v2 handles remain readable but lack selector provenance.

A property or marker miss returns exit 3 without a handle. An explicit --trace is still honored and ends with save_boundary_failure, preserving the partial control trail for diagnosis.

#resume

Argument or optionRequired/defaultMeaning
SAVEPOINTRequiredSavepoint-handle path or checkpoint content hash.
--until <quiescence|virtual-time|property|stopped>Default quiescenceSelect the resumed terminal condition.
--max-virtual-time <dur>Required with --until virtual-timeStop with timeout after this virtual-time budget.
--interactiveOffDrive the resumed session from standard input.
--watchOffCollect live session-status updates.

#fork

Argument or optionRequired/defaultMeaning
SAVEPOINTRequiredSavepoint-handle path or checkpoint content hash.
--override <decision=value>Repeatable; conflicts with global --seedPin a scheduler-recorded live World-network choice. The percent-encoded point starts with live-world-network/; the value uses the canonical loss/duplicate/corrupt choice vocabulary.
--until <quiescence|virtual-time|property|stopped>Default quiescenceSelect the child branch's terminal condition.
--max-virtual-time <dur>Required with --until virtual-timeStop with timeout after this virtual-time budget.
--label <name>OptionalLabel the forked branch.
--interactiveOffDrive the forked session from standard input.
--watchOffCollect live session-status updates.

#replay

Argument or optionRequired/defaultMeaning
ARTIFACTRequiredv3 reproduction-artifact path; production replay requires the matching packaged QEMU/plugin identity.
--check <original-log>OptionalAfter live replay succeeds, require byte-identical canonical JSONL output.
--to <savepoint>OptionalLive-replay the artifact, then validate a target savepoint handle or checkpoint hash as its typed prefix. A v3 artifact can resolve its own terminal checkpoint hash without a separate store object.
--bisect <other-artifact>OptionalLive-replay both artifacts, then locate their first evidence divergence.

The v3 artifact's live recipe declares its fingerprint evidence scope. Run, verify, and fuzz use the full execution stream; search and fork use one terminal sample per VM node. Interactive control recipes are rejected until exact command timing can be reproduced.

Argument or optionRequired/defaultMeaning
SCENARIORequiredScenario path or content hash.
--strategy <bfs|dfs|guided>Default bfsExpand breadth-first, depth-first, or by coverage guidance.
--max-depth <n>OptionalBound decision depth.
--max-states <n>Default 1Bound materialized states. Set this explicitly for useful campaigns.
--on-violation <stop|collect>Engine default stop when omittedStop at the first property/timeout finding or continue within the supplied budget.
--findings-out <path>Content-addressed path below --artifact-dirWrite the signed findings ledger here, including an empty ledger when no finding is retained.
--schedule-named-truths <path>OptionalLoad schedule-named assertion truth data.
--retained-evidence <path>Hidden/internalLoad backend-retained assertion evidence for gate workflows.

Search policy values:

Option valueMeaning
--strategy bfsExpand the shallowest frontier first.
--strategy dfsFollow a frontier deeply before returning to siblings.
--strategy guidedUse coverage feedback to prioritize frontiers.
--on-violation stopStop after the first counterexample.
--on-violation collectContinue exploring within the configured budget and retain every distinct property or timeout finding.

#fuzz

Supply the family either positionally or with --family, never both.

Argument or optionRequired/defaultMeaning
FAMILYAlternative to --familyBuilt-in name, family TOML path, or content hash.
--family <path|hash>Alternative to FAMILYExplicit named form of the family input.
--runs <n>Default 1Number of concrete family instances to run.
--coverage <basic-block>Default basic-blockSelect the coverage feedback signal.
--corpus <path>OptionalSeed and regression corpus directory.
--on-violation <stop|collect>Default stopStop at the first property/timeout finding or retain findings through the run budget.
--findings-out <path>Content-addressed path below --artifact-dirWrite the signed findings ledger here, including an empty ledger when no finding is retained.

#triage

Argument or optionRequired/defaultMeaning
FINDINGSRequiredSigned findings ledger emitted by search or fuzz.
--policy <coarse|default|fine|exact>Default defaultSelect how much failure evidence participates in a cluster signature. Finer policies split more findings.
--minimize <none|representative|all>Default representativeSkip minimization, minimize one deterministic representative per cluster, or minimize every selected representative.
--report <dir>Default below --artifact-dirWrite per-cluster reports here.
--recompute-signaturesOffRecompute signatures and fail if discovery-time bytes drift.
--compare <other-triage-result>OptionalCompare against another content-addressed triage result.

Triage policy values:

Option valueMeaning
--policy coarseGroup aggressively using coarse evidence.
--policy defaultUse the normal failure-signature policy.
--policy fineInclude more evidence and split more findings.
--policy exactRequire exact signature evidence.
--minimize noneReport representatives unchanged.
--minimize representativeMinimize the content-address-least representative per cluster.
--minimize allMinimize every selected representative.

#debug

Exactly one target is required: positional ARTIFACT|SAVEPOINT or --session. The four coordinate selectors are mutually exclusive.

Argument or optionRequired/defaultMeaning
ARTIFACT|SAVEPOINTAlternative to --sessionAttach to a retained artifact or savepoint.
--session <id:epoch:seed>Alternative to positional targetAttach to a running daemon session. The seed is exactly 64 lowercase hexadecimal digits.
--at <coord>Optional coordinateOpen at a virtual-time or node-icount coordinate.
--at-event <seq>Optional coordinateOpen at an event-log sequence.
--at-failureOptional coordinateOpen at the recorded failure point.
--at-checkpoint <hash>Optional coordinateOpen at a checkpoint content address.
--node <id>OptionalSelect the node whose gdbstub is attached.
--gdb-listen <addr>OptionalListen for mediated GDB-protocol clients here.
--read-onlyOff; conflicts with --allow-mutatePreserve the canonical run and prohibit mutation.
--allow-mutateOffFork a non-canonical debug branch for mutation.
--checkpoint-stride <n>OptionalBound reverse-step replay distance with opportunistic checkpoints.
--record-transcript <path>OffExclusively create a bounded branch-local guest-channel transcript.
--guest-idle-timeout <dur>30sFail and clean up when a guest agent produces no response for this duration.

Debugger verbs:

VerbArgumentsMeaning
attach-gdbNoneOpen the mediated gdbstub channel.
fork-debugNoneCreate the explicit non-canonical whole-world branch required for guest introspection.
goto<coord>Move to another accepted debug coordinate.
reverse-stepinstruction, quantum, event, assertion, or timerStep backward by one deterministic grain.
reverse-continue<condition>Continue backward to a matching condition.
exec-- <argv...>Execute argv directly through the forked guest agent.
pty[--columns <n>] [--rows <n>] -- <argv...>Bridge a local terminal to a guest PTY.
sshNoneBridge bytes to the SSH server configured in the guest agent.

#serve

OptionRequired/defaultMeaning
--listen <addr>RequiredBind the HTTP/2 lifecycle API. TLS is selected by the server TLS options.
--max-sessions <n>Optional; must be greater than zeroCap concurrent live sessions.
--production-qemuOffHost inline scenarios with the packaged production QEMU lifecycle instead of the quiescent API-test loop.
--qemu-rendezvous-icount <n>Optional positive count; production QEMU onlyCap production-QEMU runs at this deterministic instruction-count rendezvous interval.
--read-onlyOffPermit query/watch calls and reject mutations.
--tls-cert <path>Required with the other server TLS pathsServer certificate chain.
--tls-key <path>Required with the other server TLS pathsServer private key.
--client-ca <path>Required with the other server TLS pathsCA used to authenticate client certificates.
--trusted-unauthenticated-bindRequired for cleartextExplicitly trust an unauthenticated bind; conflicts with TLS.
--debug-role <sha256=capability,...>Repeatable; authenticated serverMap a client leaf-certificate fingerprint to observe, control, mutate, shell, and/or admin.

#completions

completions SHELL writes a completion definition to standard output.

SHELLOutput
bashBash complete definition.
elvishElvish argument completer.
fishFish complete definition.
powershellPowerShell argument completer registration.
zshZsh _crucible completion definition.

#Terminal and save-boundary values

ValueUsed byMeaning
quiescencerun --until, resume --until, fork --until, save --atStop when the scheduler has no immediately runnable work. This is the default terminal condition.
virtual-time--until, save --atStop at the positive --max-virtual-time duration.
property--until, save --atStop on a property verdict; save requires --property and selects that assertion's violated phase.
stopped--until onlyStop only after an explicit stopped state.
markersave --at onlySave after observing the named --marker.

Interactive command keywords and current payload limitations are documented in Interactive control.

#Canonical scenario document

A scenario contains exactly four top-level tables. The id on each top-level table is a validated content address generated from that canonical component; changing its content requires regenerating that ID. Nested node, device, event, and assertion IDs are scenario-local names instead.

TableRequired fieldsContents
[scenario]id, seed, app_random_draw_capScenario identity, deterministic seed material, and maximum guest application-random draws.
[world]idVM nodes, I/O device sub-nodes, and links. node and link arrays default empty.
[plan]id, fault_model, fault_signal_semantic_versionEvent graph plus the sole signal/binding fault representation.
[properties]idNamed assertions. assertion defaults empty.

#[scenario] fields

FieldTypeMeaning
idcontent-address stringHash of the complete scenario definition. Generated and validated.
seedcanonical seed stringRoot deterministic seed, commonly a full 0x byte string.
app_random_draw_capunsigned integer or decimal stringMaximum white-box application-random draws admitted by the scenario. Zero rejects all such draws.

#[[world.node]] VM fields

VM rows are untagged: they do not carry kind.

FieldType/defaultMeaning
idRequired stringUnique scenario-local node name.
archx86_64 (default) or aarch64Guest architecture.
memory_mibDefault 512Guest memory in MiB.
cmdlineDefault empty stringAdditional kernel command line.
smp_vcpusRequired unsigned integerVirtual CPU count.
icount_shiftRequired unsigned integerQEMU instruction-count shift.
kernelOptional content addressPer-node kernel artifact. The production lifecycle may supply a configured artifact when absent.
root_imageOptional content addressPer-node root-image artifact.
initrdOptional content addressPer-node initrd artifact.
ready_pointRequired nested tableDeterministic snapshot point; see below.
white_boxRequired enabled or disabledPermit or prohibit the guest-host white-box channel.

VM enum values:

FieldValueMeaningReference
archx86_64Run an x86-64 guest.TOML schema source
archaarch64Run an AArch64 guest.TOML schema source
white_boxdisabledProhibit the optional guest-host observation/control channel.TOML schema source
white_boxenabledAllow typed guest markers and application-random requests through the white-box doorbell.TOML schema source

[world.node.ready_point] kinds:

kindRequired fieldsMeaningReference
fixed_icountretired: u64Snapshot after exactly this many retired guest instructions.TOML schema source
network_idlewindow_nanos: u64Snapshot after the first network-idle window of this length.TOML schema source
console_markermarker: stringSnapshot when the guest console emits the marker.TOML schema source
agent_signalNoneSnapshot when the optional in-guest agent signals readiness.TOML schema source

#[[world.node]] I/O device fields

I/O rows share the VM node array but carry a kind. Every field listed for the selected kind is required.

kindRequired fieldsMeaningReference
blockid, owner, shift_bits, artifact, artifact_length, read_base_ns, write_base_ns, flush_ns, get_length_ns, per_byte_nsDeterministic block sub-node backed by a content-addressed base image. owner is a VM ID; latency is the operation base plus the per-byte component.TOML schema source
nine_pid, owner, shift_bits, artifact, control_ns, data_ns, per_byte_nsDeterministic read-only 9p filesystem sub-node. owner is a VM ID; control/data bases and the per-byte term model completion latency.TOML schema source

For both kinds, id is the unique device name, shift_bits maps device work to virtual time, and artifact is a content-addressed blob reference.

FieldTypeMeaning
endpoint_a, endpoint_bRequired node IDsThe two distinct VM endpoints. Ordering is canonicalized.
latency_nanosRequired unsigned integerOne-way base latency.
jitter_nanosRequired unsigned integerMaximum subtractive jitter. latency_nanos - jitter_nanos must remain above Crucible's minimum.
loss_millionthsRequired integer 0..=1000000Baseline deterministic link-loss probability.
bandwidth_bpsOptional positive integerBaseline bits-per-virtual-second cap.

Bindings refer to a unique link by its canonical link ID. Generate target IDs through a Rust scenario builder so they remain bound to the admitted World.

#[[world.node_fault_capabilities]] fields

Each VM that accepts node-level faults has one closed capability declaration. The declaration is an admission contract, not a request for best-effort QEMU behavior: the run fails before boot if the realized CPU type or canonical register manifest differs. register_schema is the BLAKE3 content hash of the complete encoded register manifest, represented in TOML as { bytes = [32 decimal byte values] }.

FieldRequired valueMeaning
idUnique stringScenario-local capability declaration ID.
nodeVM node IDVM governed by this declaration.
architecturex86_64 or aarch64Exact guest architecture ABI. It must agree with the VM's arch.
cpu_modelPrintable QOM typenameExact realized QEMU CPU type, including the architecture suffix reported by QEMU.
register_schemaContent hash tableBLAKE3 of the canonical public register-manifest bytes.
registersNonempty arrayExhaustive register rows described below, ordered canonically by numeric_id.
address_spacesNonempty arrayGuest memory ranges which node faults may address.
page_bytesPower-of-two integerGuest page size used by memory-fault contracts.
dram_geometryTableExact QEMU DRAM coordinate mapping described below.
interruptsArrayFully routed interrupt targets. May be empty.
clock_sourcesArrayGuest-visible clock sources. May be empty.
acceleratorsArrayDeclared accelerator devices. May be empty; sensor devices are not accepted.
ready_markersCanonically ordered unique string arrayExact guest event-marker names allowed to complete require_ready; an undeclared marker rejects the run before boot. May be empty.
semantic_version1Capability schema version.

#Register rows

Every guest-visible or implementation-private register in the pinned CPU model appears in [[world.node_fault_capabilities.registers]]. A row with an all-zero writable_mask_hex is reference-only: it must advertise neither impulse nor persistent, has no model phases or side effects, and cannot be selected for a mutation. A writable row advertises at least one mutation mode, has VMState coverage, and lists every safe hook phase. The four masks partition every in-range bit exactly once; padding bits above width_bits are zero. Mask bytes use lowercase hexadecimal in least-significant-byte-first order.

FieldRequired valueMeaning
idUnique stringStable selector ID for this register.
nameCanonical lowercase identifierExact name exported by QEMU.
numeric_idNonzero integerStable private-to-public manifest row ID.
groupRegister-group value belowArchitecture category used by coverage gates.
width_bits1..=65536Architectural value width.
per_vcputrueValues are independently selected by vCPU index.
model_phasesOrdered unique arrayWritable rows use before_instruction, after_instruction, or both; reference-only rows use [].
side_effectsOrdered unique arrayDerived QEMU state recomputed by the architecture setter; reference-only rows use [].
impulseBooleanSupports one exact mutation at a selected occurrence.
persistentBooleanSupports a rule applied at every selected register hook.
vmstateBooleanRegister value and any advertised persistent rule survive save/restore. Required for writable rows.
writable_mask_hexExact-width lowercase hexBits the fault ABI may change.
reserved_mask_hexExact-width lowercase hexArchitecturally reserved bits, always preserved.
ignored_mask_hexExact-width lowercase hexBits whose architectural writes are ignored.
read_only_mask_hexExact-width lowercase hexReadable or implementation-private bits that cannot be mutated.

Register-group values are exhaustive:

ValueContents
general_purposeInteger data and address registers.
control_flowProgram counters and explicit control-flow registers.
flagsInteger condition and status flags.
segmentSegment selectors, bases, limits, and attributes.
controlTranslation and execution-control registers.
systemOther guest-visible architecture system registers.
debugGuest-visible debug registers.
floating_pointFloating-point data, status, and control registers.
vectorSIMD, vector, and predicate registers.
errorArchitecture-defined error status and syndrome registers.

Register side-effect values are exhaustive:

ValueRequired architecture action
tlb_flushFlush affected vCPU translations.
translation_block_flushInvalidate affected translated code.
flags_recomputeRebuild cached flags or execution state.
interrupt_reevaluateRecompute interrupt masking and delivery.
timer_rearmRecompute and arm derived timer deadlines.
control_flow_synchronizeSynchronize the next guest instruction location.

#Memory, interrupt, clock, and accelerator rows

Nested locationRequired fieldsMeaning
[[world.node_fault_capabilities.address_spaces]]id, start_address, positive length_bytesOne non-wrapping guest address range. Address and length accept a TOML integer or canonical decimal/hex string.
[world.node_fault_capabilities.dram_geometry]channels=2, ranks=2, banks=16, interleave_bytes=64, semantic_version=1The only currently implemented GPA-to-DRAM mapping.
[[world.node_fault_capabilities.interrupts]]All interrupt-row fields belowOne exact source-to-controller route and its mutation contract.
[[world.node_fault_capabilities.clock_sources]]id, semantic_version=1, monotonicOne registered guest clock and whether reads must remain monotonic.
[[world.node_fault_capabilities.accelerators]]id, nonempty sorted classes, semantic_version=1, capability_manifestOne realized fault device and its exact content-addressed manifest; classes contains any supported combination of gpu, tpu, and fpga.

ready_markers is part of the content-addressed QEMU launch contract. Each entry names a decoded guest event marker, not an assertion, lifecycle, coverage, or random-request marker. The host carries the exact set admitted by the World through setup and node construction, and rejects a lifecycle or watchdog action whose ready_marker is absent from the selected live node.

Interrupt rows are exhaustive realized-machine contracts. Every field is required; there are no inferred controller defaults. A scenario is rejected before boot if QEMU reports a different family, controller version, electrical mode, route, priority, phase set, replacement range, drop transition, or VMState coverage.

Interrupt fieldRequired valueMeaning
idUnique stringStable manifest-row identity.
controllerController object IDController selected by a fault target.
sourceSource object IDDevice, timer, or vCPU source selected by a fault target.
controller_versionPrintable non-whitespace stringExact realized QEMU controller implementation/version identity.
familyInterrupt-family value belowArchitecture path whose hooks and state semantics are implemented.
vector_startFamily-valid integerInclusive first x86 vector or Arm INTID this source may produce after guest programming.
vector_endFamily-valid integerInclusive last runtime vector or INTID; must be at least vector_start. Each opportunity records the exact observed value.
replacement_vector_startFamily-valid integerInclusive first replacement accepted for this row.
replacement_vector_endFamily-valid integerInclusive last replacement accepted for this row; must be at least replacement_vector_start.
triggeredge or levelElectrical pending-state behavior. Families fixed to edge reject level.
polarityactive_high or active_lowActive line level or edge direction.
target_vcpusSorted unique nonempty integer arrayComplete closed route target set.
model_phasesSorted unique nonempty phase arrayAny subset of raise, route, and interrupt_deliver actually implemented for this row.
priorityInteger 0..=255Controller priority used by deterministic ordering.
delivery_dropDrop-state value belowExact controller transition when a selected delivery is dropped.
vmstatetrueThe controller state and Crucible interrupt overlay survive save/restore.

Interrupt-family values and valid vector domains are exhaustive:

FamilyArchitectureValid vector/INTIDRequired trigger
x86_local_apic_fixedx86-6416..=255edge or level
x86_ipix86-6416..=255edge
x86_io_apicx86-6416..=255edge or level
x86_picx86-640..=255edge or level
x86_msix86-6416..=255edge
x86_msi_xx86-6416..=255edge
x86_nmix86-64exactly 2edge
x86_timerx86-6416..=255edge or level, as realized
arm_gic_sgiAArch640..=15edge
arm_gic_ppiAArch6416..=31edge or level
arm_gic_spiAArch6432..=1019edge or level
arm_gic_lpiAArch648192..=16777215edge
arm_timerAArch6416..=31edge or level, as realized

delivery_drop is constrained by trigger so that dropping cannot silently change controller semantics:

ValueAllowed triggerExact transition
consume_edgeedgeConsume the selected pending edge without creating active guest exception state.
repend_asserted_levellevelConsume the sampled opportunity and re-pend according to the unchanged physical line assertion.

SMI is intentionally absent: the current QEMU contract does not implement the complete SMM state transition. Arm SError is configured as a typed cpu_exception, not as an interrupt-manifest family.

#Plans, signals, bindings, and faults

There is one fault authoring and execution model. A plan combines an ordinary event graph with signal programs and typed bindings. Static, finite, periodic, stochastic, trace-replayed, and stateful behavior all use this same path; there is no separate imperative activation API.

Implementation sources:

#Fault-topology canonical locations

Fault-topology arrays are direct children of [world]. The complete canonical row set is [[world.fault_domain]], [[world.network_interface]], [[world.network_segment]], [[world.network_medium]], [[world.network_forwarder]], [[world.network_queue]], [[world.network_path]], [[world.network_attachment]], [[world.network_contact_plan]], [[world.network_policy_artifact]], [[world.mobile_endpoint]], [[world.storage_device]], [[world.storage_controller]], [[world.storage_array]], [[world.storage_policy_artifact]], and [[world.node_fault_capabilities]]. See the fault topology reference for every top-level and nested field, closed policy payload, constraint, and continuation rule.

#Storage-array declarations

Every [[world.storage_array]] row is a complete logical-device contract. All fields below are required; there are no inferred RAID defaults or legacy fallbacks.

FieldAccepted valueMeaning
idUnique object IDStable array identity used by storage_array targets.
deviceBlock storage-device IDGuest-visible logical block node. It must not be a member.
semantic_version1Exact layout, parity, and rebuild semantics.
layoutmirror, stripe, single_parity, or dual_parityClosed physical layout. Single parity requires at least three members; dual parity requires at least four.
chunk_bytesPositive power of twoData chunk and parity-stripe unit.
read_quorumPositive integer no greater than member countMinimum online member paths before reads are admitted.
write_quorumPositive integer no greater than member countMinimum online members before non-atomic writes are admitted.
membersCanonical nonempty member tableEach row has unique id, unique block device, and contiguous ordinal beginning at zero.
pathsCanonical path tableEach row has id, positive queue_depth, and a policy reference.
member_path_statearray_state artifact IDComplete baseline online state for every declared member and path.
selection_policyarray_selection artifact IDBaseline mirror read selection: lowest healthy, stable hash, or least loaded.
rebuild_servicerebuild artifact IDBaseline positive rebuild chunk, queue depth, and byte rate.
consistency_policyarray_consistency artifact IDBaseline quorum, degraded-commit, or atomic-stripe behavior.
failure_resultNon-success block typed_result artifact IDExact result returned when no legal quorum exists.
fault_domainsCanonical fault-domain ID listShared-cause domains containing the array.

The smallest member capacity, rounded down to chunk_bytes, must cover the logical device after mirror/stripe/parity overhead. The baseline policy always routes logical I/O through the declared members. An active storage.array_state binding replaces all five baseline policy references as one state transition; when it deactivates, the declaration baseline resumes.

#[plan] fields

FieldRequired/defaultMeaning
idRequired generated content addressIdentity of the event graph and complete signal-driven fault layer.
fault_modelRequired; only signal_bindings_v2Selects the sole accepted fault schema. Earlier forms fail before typed lowering.
fault_signal_semantic_versionRequired; only 2Locks signal/binding semantics for canonicalization and replay.
signalEmpty array by defaultClosed signal-program rows described below.
fault_bindingEmpty array by defaultTyped bridges from signal outputs to effects.
resource_limitsAll compiled defaultsScenario-owned limits; every value must be positive and no greater than its compiled ceiling.
eventEmpty array by defaultNon-fault event-graph rows.

#[[plan.event]] fields and actions

FieldRequired/defaultMeaning
idRequired stringUnique event identity.
triggerOptionalPredicate table or DSL string. Omission is unconditional.
actionRequiredOne closed action table.
policyonce by default; repeatableFire once or on later false-to-true transitions.
Action kindFieldsEffect
arm_timername, after_nanosArm or replace a relative timer.
cancel_timernameCancel the timer.
start_nodenodeStart a declared stopped node.
stop_nodenodeStop a declared node.
create_savepointoptional labelMaterialize a savepoint at the firing boundary.
forkoptional labelFork a child execution at the firing boundary.
passnoneProduce an explicit passing terminal verdict.
failreasonProduce an explicit failing terminal verdict.
loglevel, messageEmit deterministic text; level is debug, info, warn, or error.
groupactionsApply nested actions in declared order as one group.

#[[plan.signal]] common fields

FieldRequired/defaultMeaning
idRequiredStable signal identity.
domainRequiredvirtual_time, node_counter, operation, spatial, event, or state.
exportedDefault trueWhether the node is available as a binding input.
value_typeRequiredbool, i64, u64, ratio, duration_nanos, rate_per_second, probability_millionths, enum, event, vector2, vector3, or bytes; parameterized types also carry their schema/scalar type.
unitRequiredOne unit from the table below.
scale_decimal_exponentDefault 0; -18..=18Exact decimal scaling carried in signal shape.
inputsEmpty unless required by an operatorIDs of upstream nodes; order is semantic for noncommutative operators.
kind and kind-specific fieldsRequiredFlattened closed source, pure operator, or stateful operator specification.

Every stateful signal additionally requires positive state_bytes, the exact bounded checkpoint allocation for that node. Source and pure nodes reject that field.

Signal units are exhaustive:

UnitStored quantity
dimensionlessInteger or rational without a physical unit.
virtual_nanosecondsVirtual duration or coordinate.
millimetres, square_millimetres, millimetres_per_secondPosition, squared distance, or velocity.
millidegreesOrientation.
millicelsiusTemperature.
microvolts, microamps, microwatts, microjoulesVoltage, current, power, or energy.
femtowatts, millidecibels, millidecibel_milliwattsExact linear or logarithmic RF/optical quantity.
kilohertzFrequency.
bits_per_second, bytes_per_second, operations_per_secondService rate.
parts_per_million, probability_millionthsRatio or probability; probability is 0..=1_000_000.
micrometres_per_second_squared, micrometres_per_hourAcceleration or precipitation rate.

Signal source kinds are exhaustive:

kindRequired fieldsPurposeConfiguration source
constantvalueEmit one immutable typed literal.signal schema
stepordered points, beforeEmit piecewise-constant values.signal schema
pulsestart, duration, inactive, activeEmit one finite active interval.signal schema
periodic_pulseepoch, period, width, phase, inactive, activeEmit repeating exact active intervals.signal schema
rampstart, end, start_value, end_value, roundingEmit one exact linear transition.signal schema
triangleepoch, period, phase, minimum, maximum, roundingEmit a periodic triangle wave.signal schema
sawtoothepoch, period, phase, minimum, maximum, roundingEmit a periodic sawtooth wave.signal schema
event_sequenceordered eventsEmit typed events with stable same-coordinate order.signal schema
traceartifact, raw_provenance, channel, interpolation, before, after, missing; optional quality channel/threshold and time mappingReplay a normalized recorded channel while retaining its raw provenance.signal schema
telemetryadapter, target, field, boundary_delay=1Read delayed production telemetry without a feedback loop.signal schema
point_setartifact, coordinate_frame, interpolation, outsideSample irregular spatial data.signal schema
regular_gridartifact, coordinate_frame, origin_mm, cell_size_mm, dimensions, interpolation, outsideSample a dense 3-D grid.signal schema
tiled_gridmanifest, coordinate_frame, tile_size_mm, interpolation, outsideSample a bounded tiled grid.signal schema
zone_mapartifact, coordinate_frame, boundary, overlapResolve polygon/polyhedron membership.signal schema
path_profileartifact, path, interpolation, before, afterSample a quantity by distance along a path.signal schema
seeded_fieldfield_seed_domain, coordinate_frame, quantization_mm, correlation_mm, distribution, distribution_parametersGenerate a deterministic correlated field.signal schema
transmitter_fieldtransmitter, coordinate_frame, position_signal, optional orientation_signal, model, lookup, environment_signalsApply calibrated path-loss, antenna, and environment transfer.signal schema
bernoulliprobability_millionths, key_domain, optional opportunity_filterMake a stable-key Boolean draw.signal schema
uniform_integerminimum, maximum, key_domain, optional opportunity_filterMake an unbiased stable-key inclusive integer draw.signal schema
exponential_waitrate, sampler_version, sampler_table, key_domain, optional maximum_nanosSample an exact integer inverse-CDF exponential wait.signal schema
weibull_waitshape, scale_nanos, sampler_version, sampler_table, key_domain, optional maximum_nanosSample an exact integer inverse-CDF Weibull wait.signal schema

Interpolation is exact, hold_previous, nearest, or linear; linear also declares rounding and overflow. Boundary behavior is error, hold, constant, repeat, or inactive. Missing-sample behavior is error, hold, interpolate, or inactive. Rounding is floor, ceiling, toward_zero, away_from_zero, or nearest_ties_to_even; overflow is error or saturate. Stochastic key_domain is opportunity, transition, or coordinate.

Pure specification kinds select the parameter shape:

kindRequired fieldsPurposeConfiguration source
simpleoperator, overflowConfigure a parameter-free arithmetic, comparison, Boolean, selection, or edge operator.pure schemas
ratio_arithmeticoperator, ratio, rounding, overflowMultiply or divide by an exact reduced ratio.pure schemas
clampminimum, maximum, overflowClamp a value to inclusive typed bounds.pure schemas
lookup_stepordered points, before, afterApply a piecewise-constant lookup.pure schemas
piecewise_linearordered points, rounding, overflowApply exact linear interpolation between lookup points.pure schemas
enum_mapexhaustive entriesMap every accepted enum input to a typed output.pure schemas
unit_convertfrom_unit, to_unit, ratio, offset, rounding, overflowConvert compatible units with exact affine arithmetic.pure schemas
delaypositive delay, positive retained_samplesDelay values in their declared domain with a hard history bound.pure schemas
sample_holdpositive cadence, epoch, positive retained_samplesSample and hold at exact domain coordinates.pure schemas
windowoperator, positive window, sampling_cadence, positive retained_samples, rounding, overflowCompute a bounded window minimum, maximum, or mean.pure schemas
distancemetric, roundingCompute spatial distance in one coordinate frame.pure schemas
zone_containszoneTest declared zone membership.pure schemas
field_samplenoneSample a declared spatial field using the input coordinate.pure schemas
orientation_deltaconventionCompute orientation difference using a closed convention.pure schemas
merge_eventspositive source_sequence_limitMerge typed event streams with bounded stable ordering.pure schemas
gate_eventsnonePass typed events only while the Boolean gate input is true.pure schemas

The operator field is exhaustive:

OperatorValid pure specificationResult
addsimpleAdd equal-shaped inputs.
subtractsimpleSubtract the second input from the first.
multiply_ratioratio_arithmeticMultiply by the declared exact ratio.
divide_ratioratio_arithmeticDivide by the declared exact ratio.
absolutesimpleProduce a signed value's absolute magnitude.
negatesimpleNegate a signed value.
minsimpleSelect the minimum input.
maxsimpleSelect the maximum input.
clampclampClamp to explicit inclusive bounds.
equalsimpleTest equality.
not_equalsimpleTest inequality.
lesssimpleTest strict less-than ordering.
less_equalsimpleTest less-than-or-equal ordering.
greatersimpleTest strict greater-than ordering.
greater_equalsimpleTest greater-than-or-equal ordering.
allsimpleCompute Boolean conjunction.
anysimpleCompute Boolean disjunction.
notsimpleCompute Boolean negation.
selectsimpleSelect between equal-shaped branches with a Boolean condition.
lookup_steplookup_stepApply the declared piecewise-constant lookup.
piecewise_linearpiecewise_linearApply the declared interpolating lookup.
enum_mapenum_mapApply the exhaustive enum mapping.
unit_convertunit_convertApply the exact compatible-unit conversion.
delaydelayRead the bounded delayed value.
sample_holdsample_holdRead the fixed-cadence held value.
window_minwindowCompute the bounded window minimum.
window_maxwindowCompute the bounded window maximum.
window_meanwindowCompute the exactly rounded bounded window mean.
distancedistanceCompute spatial distance.
zone_containszone_containsTest zone membership.
field_samplefield_sampleSample a spatial field.
orientation_deltaorientation_deltaCompute orientation difference.
edge_risingsimpleEmit an event on a Boolean rising edge.
edge_fallingsimpleEmit an event on a Boolean falling edge.
merge_eventsmerge_eventsMerge typed events in stable order.
gate_eventsgate_eventsGate a typed event stream.

Stateful specification kinds are exhaustive:

kindRequired fieldsPurposeConfiguration source
hysteresisinitial, set_when, clear_when, minimum_residence_nanosApply Boolean hysteresis with an optional residence interval.stateful schemas
debounceinitial, residence_nanosCommit an input only after it remains stable for the residence interval.stateful schemas
integratorinitial, cadence_nanos, positive time_unit_nanos, rounding, overflowIntegrate exactly at source changes or a declared cadence.stateful schemas
leaky_integratorinitial, positive cadence_nanos, positive time_unit_nanos, decay_ratio, positive maximum_catch_up_steps, rounding, overflowIntegrate at fixed cadence while applying exact rational decay.stateful schemas
finite_state_machinenonempty states, initial, exhaustive transitions, unmatched_eventRun a closed event/guard/timer transition table.stateful schemas
markov_chainnonempty states, initial, opportunity, probability_rowsRun an exact-probability finite Markov chain.stateful schemas
burst_processinitial_bad, transition probabilities, opportunityRun a two-state correlated good/bad process.stateful schemas
counterinitial, maximum, overflow, optional reset_eventCount bounded typed events with explicit overflow/reset behavior.stateful schemas
queue_modelpositive capacity, discipline, overflowModel bounded checkpointed service backlog.stateful schemas

Unknown variants or fields in any table are rejected.

#[[plan.fault_binding]] fields

FieldRequired/defaultMeaning
idRequiredStable binding identity.
signalsRequired nonempty list; signal alias only for one inputCanonical input signals.
samplingDefault at_boundaryString value at_boundary, at_opportunity, at_change, cadence_nanos, or at_event; the latter two use adjacent parameter fields.
mappingRequiredClosed signal-to-effect transfer below.
selectorRequiredexact, target_set, fault_domain, or version-1 dynamic_path.
phasesDefault: every phase in the effect descriptorNonempty exact application-phase set; canonical output always emits it.
effectRequiredOne typed effect specification; semantic_version=1.
opportunity_filterRequired when opportunity sampling cannot be inferredAdapter, operation set, phase set, and optional target-kind constraints.
searchDefault fixedString selecting bounded search behavior; non-fixed parameters use adjacent [plan.fault_binding.search_policy].
observabilityDefault policySample retention, inactive-opportunity retention, and mapped-value retention; canonical output always emits it.
transition_declarationRequired only by state_transition mappingVersioned exhaustive transition-table declaration retained in the binding.
service_declarationRequired only by service_profile mappingVersioned named physical-input service-profile declaration retained in the binding.

transition_declaration has exact fields id, semantic_version = 1, input, effect, singular transition = [{ request, transition }], and default_transition. The input is an event or enum value type; each request is a typed signal value and each transition is a registered adapter-transition ID.

service_declaration has exact fields id, semantic_version = 1, effect, inputs = [{ role, shape }], and parameters. A shape contains value type, unit, and decimal exponent. Parameters are probability, duration_nanos, bits_per_second, bytes_per_second, operations_per_second, capacity_ratio, signed_offset, or unsigned_count and must belong to the declared effect.

Mapping kindFieldsResult
active_when_trueinvertPersistent activation from Boolean input.
active_when_equalvaluePersistent activation for one enum value.
thresholdcomparison, threshold, optional clear_threshold, residence_nanosStateful threshold/hysteresis activation.
map_parameterparameterMap one signal to one registered effect field.
piecewise_parameterparameter, ordered points, rounding, overflowExact finite transfer function.
hazardnoneKeyed probability outcome at matching opportunities.
impulse_on_eventnoneOne impulse per typed event identity.
state_transitiontransition_tableExhaustively registered adapter transition.
service_profileservice_profileRegistered named physical-input service model.

Search policy kinds are fixed, branch_outcome { maximum_branches }, branch_transition { candidates }, branch_parameter { parameter, candidates }, mutate_trace_window { start_nanos, end_nanos, candidates, maximum_mutations }, and mutate_mapping { point_indices, candidates, maximum_mutations }. Mutation candidates are concrete, finite replacement schedules. A trace candidate names trace_node and exact existing sample coordinates with typed replacement values. A mapping candidate names exact point indices and complete typed replacement points. Crucible materializes the bounded Cartesian product into fixed-policy scenarios before starting QEMU; it never guesses mutation values. --max-states is one global budget for that product: every materialized scenario root consumes one state, and every graph frontier expansion consumes another. It is not reset for each candidate. Finding artifacts embed the authenticated transitive signal-object closure and the exact ordered mutation recipe, so replay does not require the search store that produced the candidate.

#Fault opportunity operation values

opportunity_filter.operations is a required, nonempty list when a binding declares an opportunity filter. Every value in one list must belong to the filter's adapter; mixed-adapter lists are rejected. phases is also required and nonempty, while target_kinds may be empty to avoid further restriction. For example:

[plan.fault_binding.opportunity_filter]
adapter = "network"
operations = ["network_transmit", "network_receive"]
phases = ["admit"]
target_kinds = ["network_interface"]

The following table is the complete closed operation vocabulary. The operation enum and adapter mapping and the filter schema and validation are the corresponding code contracts.

Operation valueAdapterOpportunity representedConfiguration
network_transmitnetworkA frame leaves a producer or forwarding interface.Add "network_transmit" to operations.
network_receivenetworkA frame arrives at a selected recipient interface.Add "network_receive" to operations.
network_contendnetworkParticipants contend for a shared-medium resource.Add "network_contend" to operations.
network_allocatenetworkA shared medium allocates service, a slot, or another bounded resource.Add "network_allocate" to operations.
network_enqueuenetworkA frame is admitted to a bounded network queue.Add "network_enqueue" to operations.
network_servenetworkA queued frame consumes modeled link or forwarder service.Add "network_serve" to operations.
network_dequeuenetworkA frame leaves a queue for delivery, forwarding, or disposal.Add "network_dequeue" to operations.
network_learnnetworkA forwarder updates learned forwarding state.Add "network_learn" to operations.
network_lookupnetworkA forwarder consults routing, switching, firewall, or related state.Add "network_lookup" to operations.
network_routenetworkA route is selected or transitions between versioned paths.Add "network_route" to operations.
network_translatenetworkAn address, port, protocol, or control result is translated.Add "network_translate" to operations.
network_encapsulatenetworkA frame or bundle is encapsulated or decapsulated.Add "network_encapsulate" to operations.
network_selectnetworkA path, backend, beam, gateway, channel, or candidate is selected.Add "network_select" to operations.
network_traversenetworkTraffic traverses one segment, medium, path, or scheduled contact.Add "network_traverse" to operations.
network_changenetworkA versioned topology, path, profile, or attachment changes.Add "network_change" to operations.
network_discovernetworkA network, peer, access point, cell, service, or contact is discovered.Add "network_discover" to operations.
network_authenticatenetworkNetwork access or peer identity is authenticated.Add "network_authenticate" to operations.
network_associatenetworkAn interface establishes an attachment or association.Add "network_associate" to operations.
network_handoffnetworkAn attachment moves between access resources or paths.Add "network_handoff" to operations.
network_acquirenetworkA scheduled contact, channel, beam, or link is acquired.Add "network_acquire" to operations.
network_custodynetworkDelay-tolerant traffic changes custody or durable queue ownership.Add "network_custody" to operations.
network_teardownnetworkA contact, association, tunnel, or attachment is torn down.Add "network_teardown" to operations.
storage_readstorageA block or 9p read request is resolved.Add "storage_read" to operations.
storage_writestorageA block or 9p write request is resolved.Add "storage_write" to operations.
storage_flushstorageA guest requests a durability or ordering barrier.Add "storage_flush" to operations.
storage_discardstorageA block range is discarded or deallocated.Add "storage_discard" to operations.
storage_get_lengthstorageGuest-visible device capacity is queried.Add "storage_get_length" to operations.
storage_resetstorageA storage device, controller, namespace, or path is reset.Add "storage_reset" to operations.
storage_erasestorageA flash erase block is erased.Add "storage_erase" to operations.
storage_refreshstorageMedia is refreshed to restore or retain readable state.Add "storage_refresh" to operations.
storage_admitstorageA controller decides whether to admit an operation.Add "storage_admit" to operations.
storage_submitstorageAn admitted operation is submitted to controller service.Add "storage_submit" to operations.
storage_completestorageA block, controller, array, or 9p operation completes.Add "storage_complete" to operations.
storage_enumeratestorageA controller, namespace, path, or 9p device is enumerated.Add "storage_enumerate" to operations.
storage_rebuildstorageAn array performs bounded rebuild work.Add "storage_rebuild" to operations.
node_bootnodeA node enters its boot transition.Add "node_boot" to operations.
node_runnodeA node or vCPU performs scheduled execution.Add "node_run" to operations.
node_pausenodeA node enters a paused state.Add "node_pause" to operations.
node_resetnodeA node performs an architectural reset.Add "node_reset" to operations.
node_stopnodeA node stops or powers off.Add "node_stop" to operations.
node_resumenodeA stopped or paused node resumes execution.Add "node_resume" to operations.
cpu_instructionnodeA vCPU reaches an instruction execution opportunity.Add "cpu_instruction" to operations.
cpu_exceptionnodeA vCPU reaches an architecture exception transition.Add "cpu_exception" to operations.
cpu_haltnodeA vCPU enters or leaves a halted service state.Add "cpu_halt" to operations.
register_accessnodeAn architecture-resolved register is read or written.Add "register_access" to operations.
memory_fetchnodeA vCPU fetches instruction bytes.Add "memory_fetch" to operations.
memory_loadnodeA vCPU loads data from memory.Add "memory_load" to operations.
memory_storenodeA vCPU stores data to memory.Add "memory_store" to operations.
memory_dma_readnodeA device reads guest memory through DMA.Add "memory_dma_read" to operations.
memory_dma_writenodeA device writes guest memory through DMA.Add "memory_dma_write" to operations.
memory_page_table_walknodeA vCPU MMU reads a page-table descriptor.Add "memory_page_table_walk" to operations.
memory_refreshnodeModeled main memory performs a refresh operation.Add "memory_refresh" to operations.
interrupt_raisenodeAn interrupt source raises an interrupt.Add "interrupt_raise" to operations.
interrupt_routenodeAn interrupt controller resolves a route and target.Add "interrupt_route" to operations.
interrupt_acknowledgenodeA target acknowledges an interrupt.Add "interrupt_acknowledge" to operations.
interrupt_delivernodeAn interrupt is delivered to a target vCPU.Add "interrupt_deliver" to operations.
interrupt_returnnodeA vCPU completes an interrupt-return transition.Add "interrupt_return" to operations.
clock_readnodeGuest software reads a registered clock source.Add "clock_read" to operations.
clock_armnodeA guest-visible timer is armed.Add "clock_arm" to operations.
clock_firenodeA guest-visible timer reaches its fire boundary.Add "clock_fire" to operations.
clock_synchronizenodeA clock synchronization update is applied.Add "clock_synchronize" to operations.
clock_source_switchnodeGuest-visible timekeeping switches clock sources.Add "clock_source_switch" to operations.
accelerator_submitnodeA job is submitted to an accelerator queue.Add "accelerator_submit" to operations.
accelerator_executenodeAn accelerator performs modeled job work.Add "accelerator_execute" to operations.
accelerator_completenodeAn accelerator job produces a completion.Add "accelerator_complete" to operations.
accelerator_memory_accessnodeAn accelerator accesses device or guest memory.Add "accelerator_memory_access" to operations.
accelerator_resetnodeAn accelerator performs a reset transition.Add "accelerator_reset" to operations.

#Target selector values

Target kindAdapterWhat it selects
network_interfacenetworkOne endpoint interface.
network_segmentnetworkOne directed physical or logical segment.
network_mediumnetworkOne shared medium/channel resource.
network_queuenetworkOne bounded queue.
network_forwardernetworkSwitch, router, modem, repeater, or gateway.
network_pathnetworkVersioned directed path.
network_attachmentnetworkInterface association/attachment.
network_contactnetworkScheduled or acquired contact.
block_devicestorageOne whole block or flash device.
block_rangestorageOne byte-addressed range of a block or flash device.
storage_controllerstorageOne controller namespace or access path.
storage_arraystorageOne declared array member or path.
ninep_devicestorageOne 9p device.
nodenodeOne whole emulated node.
vcpunodeOne virtual CPU.
registernodeOne architecture-resolved register bit range.
memory_rangenodeOne physical or resolved virtual memory range.
interruptnodeOne exact source, route, target vCPU, and vector/type.
clock_sourcenodeOne registered guest-visible clock source.
acceleratornodeDeclared accelerator device.

Sensor targets are specification-only and are rejected by this schema.

#Exhaustive effect registry

Every row below is executable. Parameters names the primary closed table or fields; follow the linked family source for nested enum fields. Legal targets, phases, lifetimes, composition, capabilities, and replay-evidence keys are enforced by the effect registry.

Effect kindParameters and purposeConfiguration source
network.availabilityDirectional state and queued/in-flight policies; make an interface, segment, path, or contact up, down, receive-only, or transmit-only.network parameters
network.flapDown, training, and recovery durations; model timed link transitions.network parameters
network.negotiated_modeRate, duplex, lanes, FEC, and training duration.network parameters
network.profile_deltaOptional latency/rate/error/technology profile components.network parameters
network.propagation_delayExact delay or a distance/velocity lookup; adds propagation time above the immutable scheduler floor.network parameters
network.access_delayPer-opportunity arbitration or retry delay in virtual nanoseconds.network parameters
network.jitterKeyed bounded delay variation with a closed distribution.network parameters
network.service_curveOrdered piecewise-constant rate segments integrated over virtual time.network parameters
network.token_bucketRate, burst size, and initial tokens for a checkpointed service constraint.network parameters
network.queue_policyByte/frame capacity, discipline/classes, and overflow response.network parameters
network.frame_lossExplicit or millionths-probability frame loss keyed to stable frame identity.network parameters
network.burst_error_stateCorrelated good/bad loss and corruption process with checkpointed transition state.network parameters
network.duplicateProbability, copy count, and inter-copy gap for bounded additional deliveries.network parameters
network.reorderBounded reorder window and keyed selection rule.network parameters
network.payload_transformBit flip, field mutation, truncation, or undetected corruption.network parameters
network.detected_frame_errorCRC/FCS/framing/FEC class and corrected/retry/drop/reset receiver action.network parameters
network.mtuMTU plus drop, fragment, or typed-error oversize policy.network parameters
network.pause_backpressureClass-scoped pause state with an optional exact resume boundary.network parameters
network.recipient_subsetVersioned multicast/broadcast candidate filtering by declared membership.network parameters
network.forwarder_lifecycleRestart/reset/power-loss transition, downtime, and queue/table retention.network parameters
network.forwarding_mutationWrong-port, flood, blackhole, loop, or stale-age lookup mutation.network parameters
network.route_transitionOld/new paths, convergence events, and in-flight policy.network parameters
network.control_plane_serviceBounded control queue, service curve, work size, and overflow.network parameters
network.firewall_dispositionSelector/state machine plus accept, reject, or drop.network parameters
network.connection_stateNAT, conntrack, load-balancer, tunnel, or DNS table and overflow state.network parameters
network.shared_mediumResources, arbitration, contention/collision/capture, and duty cycle.network parameters
network.rf_channelCarrier/bandwidth, signal/noise/gain/attenuation/fading, SINR transfer, and retry outcomes.network parameters
network.associationCandidate set, authentication, selection, hysteresis, timers, handoff, and traffic policy.network parameters
network.control_result_transformTechnology operation plus drop, stale, bias, replace, or typed error result.network parameters
network.contactContact intervals, range delay, and beam/gateway candidates.network parameters
network.custody_queueBundle/byte capacity, priority, expiry, route/contact plan, hop bound, and overflow.network parameters
storage.availabilityOnline/offline/read-only/degraded state.storage parameters
storage.reported_capacityGuest-visible length and affected-range policy.storage parameters
storage.latencyOperation-filtered base delay and keyed jitter at resolve or delivery.storage parameters
storage.serviceIntegrated bandwidth, IOPS, queue, class, and token service constraints.storage parameters
storage.operation_failureOperation set, keyed probability, and referenced typed failure result.storage parameters
storage.stall_timeoutStall, recovery, and modeled timeout coordinates with explicit completion behavior.storage parameters
storage.completion_reorderBounded keyed completion ordering within the declared window.storage parameters
storage.duplicate_completionProtocol-valid additional completions and guest duplicate disposition.storage parameters
storage.read_transformBit corruption, stale-version read, or cross-range/device misdirection.storage parameters
storage.write_dispositionApplied, lost, torn, or misdirected persistence.storage parameters
storage.persistence_orderDeclared durable partial order and violation behavior.storage parameters
storage.volatile_cacheBounded cache admission, eviction, dirty-eviction, and power-loss-protection policy.storage parameters
storage.volatile_cache_lossBoundary impulse selecting the exact eligible cached-write set to lose.storage parameters
storage.flush_dispositionHonest, erroring, lying, or stalled flush result.storage parameters
storage.media_rangePersistent bad, latent, poisoned, or read-only byte range with count/time thresholds.storage parameters
storage.flash_statePer-erase-block wear, program/erase failure, retention, and read-disturb state.storage parameters
storage.controller_lifecycleReset/reconnect/enumeration/namespace/path transition and pending-I/O treatment.storage parameters
storage.array_stateArray member/path state, selection, quorum, rebuild, and partial-update consistency.storage parameters
ninep.resultTyped errno, stale object, or misdirected 9p result.storage parameters
ninep.visibilityCheckpointed committed-versus-visible frontier and lookup behavior.storage parameters
node.lifecycleBoot, crash, reset, power-cycle, stop, and recovery transition with explicit state loss.node parameters
node.hangNode, vCPU-set, or accelerator progress outage with watchdog/recovery policy.node parameters
cpu.serviceExact rational execution capacity, thermal throttling, and vCPU service schedule.node parameters
cpu.vcpu_stateOnline, offline, or stalled vCPU transition with round-robin topology state.node parameters
cpu.register_transformArchitecture-resolved bit flip, stuck mask/value, or replacement.node parameters
cpu.instruction_transformInstruction result corruption, skip, or replay at an exact instruction opportunity.node parameters
cpu.exceptionArchitecture-specific machine check, hardware error, or injected exception.node parameters
interrupt.dispositionDrop, delay, duplicate, or replace one exact interrupt delivery.node parameters
interrupt.stormBounded generated interrupt sequence with exact acknowledgements.node parameters
memory.mutationAtomic GPA/GVA bit flip or byte replacement at a safe boundary.node parameters
memory.access_transformStuck/read-corrupt/lost-write/torn-write/poison transform by access class.node parameters
memory.ecc_eventCorrected or uncorrectable ECC event with a platform error record and acknowledgement.node parameters
memory.region_statePersistent failure, retention decay, or rowhammer disturbance with range counters.node parameters
memory.serviceShared memory-access latency, bandwidth, and page-table-walk service constraints.node parameters
clock.transformGuest-visible offset, rational drift, jump, freeze, jitter, or wander.node parameters
clock.source_stateClock-source failure, fallback, selection, or synchronization state.node parameters
accelerator.lifecycleDevice disappearance, reset, reconnect, enumeration, and queue treatment.node parameters
accelerator.result_transformOrdered accelerator job-field or result-buffer corruption.node parameters
accelerator.memory_eventCorrected, uncorrectable, or transformed device-memory event.node parameters
accelerator.serviceCompute, memory, thermal, or power service cap with queue/job ledgers.node parameters

The registry has 71 distinct keys and exactly one row above for each key. A reference-integrity gate compares this document with the closed registry so a new executable kind cannot ship undocumented.

#Properties and predicates

#[properties] and assertions

LocationRequired fieldsMeaning
[properties]idGenerated content address for the property bundle.
[[properties.assertion]]id, message, propertyStable assertion name, user-facing failure message, and nested temporal property.

#Property kinds

[properties.assertion.property] is tagged by kind. Supplying a field not listed for that kind is an error.

kindRequired fieldsMeaningReference
alwayspredicateInvariant: the predicate must hold at every relevant evaluation point.TOML schema source
sometimespredicateLiveness witness: the predicate must hold at least once.TOML schema source
eventuallytrigger, property, deadline_ticksAfter trigger holds, property must hold within this many virtual-time ticks from the trigger instant.TOML schema source
after_quiescencepredicateCheck the predicate once when the run quiesces or reaches its run limit.TOML schema source
reachablepredicate, expectationCoverage-style reachability or unreachability expectation.TOML schema source

Reachability expectation tables:

kindFields/defaultMeaning
reachableon_unreached: warn|fail, default warnExpect at least one witness; warn or fail if none is observed.
unreachableNoneFail if a witness is observed.

#Predicate kinds

A predicate may be a DSL string or a structured table tagged by kind. The same vocabulary is accepted for assertion predicates and event triggers.

kindRequired/optional fieldsTrue whenReference
atat_ticksVirtual time equals the exact coordinate.TOML schema source
afterduration_nanos, ofThe duration has elapsed since event ID of last fired.TOML schema source
timernameThe named relative timer fires.TOML schema source
network_matchpredicate, link?A delivered frame, optionally restricted to a link ID, matches the nested frame predicate.TOML schema source
console_matchnode, regexThe node's captured serial output matches the regex program.TOML schema source
coverage_pointnode, pointThe node executes the nested address or symbol code point.TOML schema source
memory_predicatenode, place, cmp, valueThe sampled memory/register value satisfies the comparison.TOML schema source
io_patternnode, io_kindAn I/O event of the selected kind is observed for the node.TOML schema source
node_statenode, stateThe node has the selected lifecycle state.TOML schema source
assertion_statename, stateThe named assertion is satisfied or violated.TOML schema source
quiescentNoneThe scheduler has settled with no immediately runnable work.TOML schema source
namedname, nodes?The named predicate DSL entry resolves in the current world/plan context.TOML schema source
guest_markermarkerThe white-box-enabled guest emits the named bare marker or declared assertion marker as applicable.TOML schema source
all_ofpredicates arrayEvery nested predicate is true.TOML schema source
any_ofpredicates arrayAt least one nested predicate is true.TOML schema source
oncepredicateThe nested predicate has become true at least once.TOML schema source
notpredicateThe nested predicate is false.TOML schema source

#Named predicate DSL strings

These strings may appear directly where a predicate is expected. Structured kind = "named" form also accepts name plus an optional nodes array.

DSL valueExpansion
no_crashed_nodesnot(any_of(node_state(node, crashed) for every VM))
quiescentquiescent
node_alive:<node>not(node_state(<node>, crashed))
node_crashed:<node>once(node_state(<node>, crashed))

#Nested predicate value tables

Frame predicates used by network_match:

kindRequired fieldsMatch
anyNoneAny delivered frame.
exactbytes_hexComplete frame bytes equal the hexadecimal sequence.
containsneedle_hexFrame contains the hexadecimal byte sequence.
prefixprefix_hexFrame begins with the hexadecimal byte sequence.

Code points used by coverage_point:

kindRequired fieldsMeaning
guest_addressaddressExact guest virtual address.
symbolnameSymbol resolved by the configured observation backend.

Places used by memory_predicate:

kindRequired fieldsMeaning
physical_addressaddress, widthRead a guest physical address.
virtual_addressaddress, widthRead a guest virtual address.
symbolname, widthRead memory at a symbol.
registername, widthRead a guest register.

Memory widths:

widthRead size
u88 bits
u1616 bits
u3232 bits
u6464 bits

Unsigned memory comparisons:

cmpOperation
eqEqual to value.
neNot equal to value.
ltLess than value.
leLess than or equal to value.
gtGreater than value.
geGreater than or equal to value.

io_pattern.io_kind values:

ValueMatches
anyAny modeled I/O event.
block_readBlock read.
block_writeBlock write.
fsyncFlush/fsync event.
nine_p9p filesystem event.
networkNetwork event.

Node lifecycle states:

node_state.stateMeaning
startedThe declared node is running.
crashedThe node entered its modeled crash state.
hungThe node is running but no longer making modeled progress.
exitedThe guest/runtime exited.

Assertion phases:

assertion_state.stateMeaning
satisfiedThe named assertion reached its satisfied terminal phase.
violatedThe named assertion reached its violated terminal phase.

#Output, artifacts, and exit status

JSON and JSONL are stable programmatic formats. Tables and Markdown are presentation formats. The event trace is distinct from diagnostic output; use --trace and --quiet when a job needs a clean machine stream.

The content-addressed store contains scenario forms, schedules, checkpoints, and related execution objects. A reproduction artifact records inputs and the schedule needed to reproduce a result. Signal-fault reproduction artifacts also embed every reachable normalized trace/spatial/sampler object, authenticate each object while restoring it into an isolated in-memory store, and include mutation provenance when search changed a trace or mapping. A savepoint handle names a checkpoint for resume, fork, and debugger attachment. Preserve every store object referenced by exported handles; reproduction artifacts carry their own signal closure.

StatusClass
0Success
1Property failure, divergence, replay mismatch, counterexample, or triage failure
2Virtual-time or scheduler-quantum timeout
3Crash, daemon failure, replay-oracle failure, or build-identity mismatch
4Backend failure
5Invalid scenario, artifact, store object, or local I/O input
64Command-line usage error

Scripts should branch on the status class and consume JSON/JSONL output. Human diagnostic wording may change. See Troubleshooting for cause-oriented guidance.