Anulum Overview Host analysis AMP simulation Validation Python API Rust API C/C++ API

Dedicated-hart ISA capture

The public tools/capture_amp_simulation.py command executes an admitted RV64 firmware image on actual Spike harts against the production AXI RTL plugin. The selected hart runs the selected C or Rust fixed-point controller and publishes observations to its reserved telemetry ring. Other original harts park in firmware. The host logger drains that ring and the actual fabric event FIFO separately. This verifies functional execution; it does not run Linux on the parked harts or establish physical U54 instruction timing.

Original firmware inputs

tools/prepare_amp_image.py requires an original complete DTB, native configuration, actual RV64 compiler and explicit resource selections. It copies the admitted source and generates a strict freestanding compiler Makefile. Run that Makefile to compile, link and verify the firmware. --isa selects the target HTIF exit after logger acknowledgement; without it the target parks, and the ISA capture command refuses that completion mode. The default arithmetic backend is C. Add --rust-compiler rustc to select the original installed Rust compiler and the RV64 Rust arithmetic archive. Both selections use the same startup assembly, interrupt service, reserved memory, telemetry ring and target completion.

The same resource arguments are required by preparation, image verification and capture:

Argument Meaning
--ram-node Original RAM node containing both reserved regions
--firmware-node Dedicated reserved firmware region
--telemetry-node Disjoint reserved shared telemetry region
--device-node Original versioned Witness AXI device
--plic-node, --plic-layout Original interrupt controller and concrete context layout
--hart, --interrupt Dedicated original hart and retained interrupt source
--stack-bytes Explicit reserved firmware stack size

Paths, memory ranges, hart topology and interrupt ownership must agree with the original DTB and linked firmware. The native configuration contains all 24 fields, including reference and fault settings. A modeled controller latency is refused: the target executes instructions. Each firmware or telemetry reservation must fit one selected RAM bank without overlapping another declared RAM node, including a partial alias. The Spike command explicitly allocates every enabled original DTB RAM bank with -m. Banks must have page-aligned addresses and lengths and must not overlap; the command refuses absent or disabled memory instead of inheriting the simulator default allocation. Prepared sources, configuration, platform, compiler and actual compiler dependencies are hash-bound by the verified image. The image also retains its actual compiler frontend, collect2, assembler and linker identities and driver version, frozen before compilation and reconciled again during verification. Each actual compiler program's ELF interpreter resolves its native runtime libraries before preparation. Their paths, hashes and copied bytes are retained in runtime_source_index.json and runtime_sources/ inside the prepared image. Verification requires the original live compiler/library identities and the captured library bytes to agree. When a cross-toolchain is installed in a private prefix, its actual host library directory must be available to the dynamic loader for preparation and capture (for example through LD_LIBRARY_PATH). A compiler executable on PATH alone is insufficient if its assembler cannot load the matching shared libopcodes and libbfd libraries. The generated verifier retains the selected Python environment's executable path. Preparation also copies the original loop_timing_witness Python modules, JSON contracts and typing marker into source/tools/loop_timing_witness/. The preparation receipt hashes those files alongside the standalone verifier commands. The captured verifier therefore imports its captured implementation rather than the current checkout's installed package. Changing any captured module, schema or typing marker makes verify-inputs refuse the build. Subprogram, version or library drift is refused. Altered originals require a fresh preparation and build.

Preparation also runs the actual compiler's -M preprocessing for all five C-backend translation units (or all four platform translation units with explicit Rust arithmetic) with their original strict compile flags before any object exists. precompile/ retains the actual GCC dependency records and diagnostics. compiler_sources/ and compiler_source_index.json preserve the complete source/header bytes, including external compiler headers. Image-local names are relative, allowing byte-preserving image relocation; external header identities remain absolute. build_commands.json retains exact compile, link, verification and original-input check vectors.

The generated Makefile runs the public tools/verify_amp_preparation.py admission before any object or link recipe. Changed original records, sources, headers or captured indexes refuse before objects are created. Final image verification requires post-compilation GCC records to match the entire original preprocessing closure; new, omitted or changed dependencies refuse.

The Rust selection additionally captures the original safe-core and ABI-adapter source files, Cargo metadata, paired installed target .rlib archives and .rmeta metadata files, and native compiler runtime libraries. Fixed direct rustc vectors bind the original sysroot, RV64IMAC target, external core library, release flags and strict diagnostics. Ambient Cargo configuration does not select the firmware compiler. Each original Rust source must be a regular file contained in the selected checkout; symlinked source paths that escape it are refused before a build receipt is created. Actual metadata compilation precedes objects; both metadata dependency records and source closure are frozen in rust_preparation.json. Final compilation must reproduce that closure. The image receipt binds the actual safe-core Rlib, ABI static archive and both compiler records. Capture preserves these outputs as well as the original sources and library snapshots; offline analysis reconciles their captured bytes without needing the former host compiler installation. Transient Make jobserver descriptors are excluded from compiler identity queries. Make retains valid descriptors for actual Rust compilation. Source, compiler, target-library or archive drift requires a fresh preparation; it cannot be admitted by changing the declared backend. The Rust toolchain test links an isolated Rustup home to an owned copy of the real compiler and its host libraries. It verifies refusal when Cargo is absent, when the RV64 target libraries are absent, and when their metadata partners are missing. The portable receipt also requires both members of every target-library pair. Owned symlink cases verify that neither a target file nor the target directory can escape the selected compiler sysroot. The test also changes an owned archive during actual metadata compilation and requires refusal before a preparation receipt is written. It leaves the installed toolchain unchanged.

tests/test_amp_rust_snapshot_drift.py changes an owned original source or an owned installed target archive exactly at its second real filesystem read, after hashing and before snapshot copying. Its test-only native interposer forwards opens to the kernel; it does not replace Rust source data, hash functions or compiler output with a mock. Preparation must refuse the changed bytes before writing a receipt. The global Rustup installation and canonical checkout remain unchanged.

CI simulator setup

The reusable test workflow installs pinned RV64 GCC, device-tree compiler and Boost packages. It fetches Spike commit 7ab2efd6785e847c6d13d810c0b25b7c9c26bd21 and builds the actual simulator and generated SDK headers. That source needs socketif.h included before decode_macros.h in riscv/interactive.cc: the latter defines yield(), which conflicts with Boost's yield(unsigned) declaration. The workflow verifies the complete file's SHA-256 before and after this include-order change. The existing source receipts retain the Git revision and patch, so the change is part of capture provenance.

CI compiles tests/platforms/spike_multihart.dts, prepares and verifies the dedicated-hart firmware, and builds the mechanical and thermal plugins through make amp-spike-plugin. The test job exports their original paths through WITNESS_RV64_CC, WITNESS_SPIKE_SOURCE, WITNESS_SPIKE_BUILD, WITNESS_SPIKE, WITNESS_SPIKE_PLUGIN, WITNESS_SPIKE_THERMAL_PLUGIN and WITNESS_AMP_IMAGE. The source build and tests have a 90-minute job limit. These artifacts support functional ISA and RTL tests; they retain the simulation_only evidence status.

Production plugin build

Build against the source and generated headers matching the actual Spike executable. Supply both directories explicitly; absent original headers are refused before compilation.

make amp-spike-plugin AMP_SPIKE_SOURCE="$SPIKE_SOURCE" AMP_SPIKE_BUILD="$SPIKE_BUILD" \
  SIMULATION_THERMAL=0

The target compiles the production RTL, the current C controller, native configuration parser, actual Spike AXI adapter and Verilator runtime. Its output is build/amp_spike_0/witness_spike_axi.so. Use SIMULATION_THERMAL=1 for the thermal plant and build/amp_spike_1/witness_spike_axi.so. AMP_PLUGIN_DIRECTORY selects an explicit build directory. The handwritten C and C++ inputs use -O2 with strict warnings. The Verilator runtime objects also use -O2, with matching dependency-preparation and compilation flags. Host compiler optimisation keeps long functional captures within their wall-clock budget; it does not change the RTL sample period or establish physical processor latency. Native coverage variants retain their explicit compiler flags and are reported separately from the admitted production capture. Before Verilator generation, the target writes an exclusive generation.json with original RTL, handwritten code, SDK source/header hashes, Git revision and tracked patch. It records the actual compiler frontend, collect2, assembler and linker, Verilator wrapper and native backend, runtime root, Make, archive tool and interpreter hashes and versions. The native executables must be dynamically linked little-endian Linux ELF64 programs. Each executable's own ELF interpreter resolves its libraries with a bounded --list invocation under the actual build environment. Original interpreter and resolved filesystem library hashes are retained in runtime_libraries and in the captured dependency closure. This covers the C/C++ drivers and subprograms, native Verilator backend, Make, archive tool, Python and Perl. Kernel-provided vDSO mappings have no filesystem bytes and are excluded. The compiled plant and FIFO address width are explicit; SIMULATION_FIFO_ADDRESS_BITS accepts the RTL's range of 1–14. Ambient VERILATOR_ROOT or VERILATOR_BIN substitutions are refused.

The generated model uses the explicitly selected LINUX_CXX. Actual compiler preprocessing then records all native/model dependencies, including system headers, before any object is compiled. compilation.json freezes those hashes and the generated build files. Successful compilation must preserve the original generation inputs and match the entire preprocessor source/header closure. Loader-resolved library paths and bytes must also remain unchanged through both preparation stages and final receipt creation. The model build uses -MD without -MMD, retaining system headers.

The final exclusive plugin.json binds both original stages, compiler records, sources, link-input hashes and the actual library. Existing generation or final receipts stop Make before generation; select a fresh directory. A preparation attempted after objects, archives or a library exist is refused. Generation also requires an empty directory: existing compiler records, hidden files, nested contents and symbolic directory aliases are preserved and refused. An explicitly selected AMP_VERILATOR_ROOT must match the actual generator's runtime root. make amp-spike-plugin-prepare exposes the same generation and preprocessor stages without compiling native objects. These identities do not authenticate a compromised build host or establish physical performance.

The plugin is tied to the selected Spike API and ABI; rebuilding against a different SDK does not establish compatibility with an older executable. Capture records the actual executed executable/plugin hashes; retain the original build log and matching SDK separately.

Public capture arguments

Pass --image for the verified image directory, --dtb and --configuration for that image's retained originals, and the complete resource arguments above. Select the actual installed --spike executable and --plugin library explicitly. --output must be a new directory outside the image. Existing output is preserved and refused.

--rtc-nanoseconds maps Spike RTC progress to the functional RTL clock. --time-limit bounds simulated nanoseconds; --timeout bounds the host process in seconds. Neither bound is a physical execution-time measurement. The production plugin's compiled thermal parameter, read through the real RTL register, determines the declared plant.

The selected library must have its original plugin.json beside it, conforming to the plugin build schema. Capture requires all actual native/model build roles and checks original preparation, source/header, compiler-record, link-object and tool and build-library hashes. Declared final identities must agree with the original pre-compilation receipt. It also reconciles the declared dependency set with the original compiler records, refusing omissions. Original build inputs must remain available for acquisition; an old receipt whose inputs changed requires a fresh build.

The command snapshots the verified inputs before execution and rejects input or tool byte drift after execution. Spike's actual version header comes from its supported --help output. The simulator's own ELF interpreter lists the libraries selected for both Spike and the admitted plugin under the actual execution environment. The capture freezes their paths, hashes and bytes separately from the plugin's original build libraries. After execution it repeats version and loader resolution, checks the captured copies and refuses drift. Failure retains acquired raw files and simulator diagnostics. Success writes a capture receipt, the normal public run manifest and the normal analysis report.

Artifact Contract
image/ Snapshot of original verified firmware, platform, configuration and sources
image/precompile/, image/compiler_sources/, image/compiler_source_index.json Original GCC records and exact pre-compilation source/header bytes
image/build_commands.json Original complete compiler, linker and verification vectors
command.json Exact executed argument vector, simulator/plugin SHA-256 and actual runtime identity
runtime_source_index.json, runtime_sources/ Original simulator/plugin loader libraries and captured bytes
plugin_build.json Original admitted native build receipt
plugin_source_index.json Original absolute source/header names mapped to stable local path/hash pairs
plugin_sources/ Exact copied compiler/source/header bytes under portable numerical paths
spike.log Actual target diagnostics and one final logger completion receipt
events.bin Original 16-byte fabric event records
tracking_raw.csv Original native integer controller observations
capture.json AMP capture schema, artifact hashes and final counters
tracking.csv Exact Q8.24 conversion of observed reference/output rows
manifest.json Public run schema, placement bare_metal_amp
reports/ Standard report JSON, interval CSVs and plot

Analysis and limits

The same telemetry ABI 2 startup is used by the Linux collector. Firmware initialises and publishes the complete mailbox and its actual run constants before waiting for logger readiness. The logger checks all fifteen published run words before releasing firmware startup; the fabric starts only after the dedicated hart arms. The producer does not assume that Linux has already configured the fabric when firmware boots. Final acknowledgement still follows complete stream drain and close.

tests/test_amp_architectural_refusals.py deliberately damages constants in owned copies of the actual cross-compiled ELF and executes those copies directly in Spike. These copies are outside the admitted capture workflow: they exercise native defence in depth and never produce a completed capture. The logger observes exact native refusal causes for invalid resources and run bounds, plus real load-access-fault causes and addresses for unmapped MMIO and PLIC accesses. An invalid compiled hart owner never enters C: the unchanged startup assembly parks every simulated hart, and the bounded run expires without publishing mailbox or stream data. tests/test_amp_logger_api.py links public API calls into the actual Spike adapter, retaining the production RTL and native objects after verifying their hashes. It exercises both plants' arming waits, delayed consumer batches, acquisition callbacks and lifecycle/address/contract refusals, transport ownership and alignment, public AXI loads and stores, and the SDK device-factory tree interface. Public Spike RAM stores damage actual initial and arming fields for admission checks. An owned ELF copy selects its real LQR kernel with a matching configuration and retained hashes. The transport and firmware remain unchanged. Successful diagnostic executions retain ten samples and forty events; these clients do not publish capture or measurement manifests. tests/test_amp_spike_runtime.py executes original production plugins with actual native argument, memory and device-tree failures. Both plants also complete a run backed by a real 1 MiB DTB RAM allocation. Device-tree checks compare properties after an actual dtc round trip; they do not infer a factory callback from the SDK dump command. A missing PLIC is refused by the pinned SDK assertion, and an actual UART overlapping the Witness aperture is refused by the adapter. These diagnostics do not publish admitted captures. tests/test_amp_consumer_fault.py links a diagnostic Spike plugin from the hash-verified production RTL and native objects, but makes its real logger violate one consumer-owned transition. The unchanged RV64 firmware refuses an invalid startup status with cause 0x108, refuses READY-state reserved-field corruption with cause 0x107, and refuses an invalid final acknowledgement with cause 0x108. Startup faults occur before a sample or completion receipt. The final-acknowledgement fault occurs after the logger has drained both streams, but the failed process still prevents a capture or manifest. These diagnostic plugins are fault-injection evidence and are never admitted as production captures. tests/test_amp_cycle_fault.py preserves each actual AXI register transaction but changes the cycle word returned to the CPU in a source-anchored diagnostic plugin. The unchanged firmware refuses a first cycle equal to the configured run length and a repeated second cycle with cause 0x101. Raw output retains only events and telemetry observed before refusal; neither case can publish completion or enter capture admission. tests/test_amp_kernel_fault.py releases validated startup through the real logger and then changes the actual first coefficient word in target RAM before the first interrupt. The unchanged firmware kernel revalidates its input, refuses with cause 0x102, and retains only the fabric event observed before computation. The diagnostic RAM write is outside capture admission. tests/test_amp_interrupt_fault.py waits until the firmware has armed real PLIC source 2, then changes only the expected source word in target RAM to 3. The unchanged trap handler claims the actual source 2 and refuses the mismatch with cause 0x103. The diagnostic run retains the one pre-refusal fabric event and cannot enter capture admission. tests/test_amp_spurious_claim.py links a source-bound RV64 prelude around the original firmware entry. It calls the unchanged machine-external trap handler before startup, when the actual PLIC claim is zero, and requires the handler to return before the complete original ten-cycle run. This covers the non-terminal empty-claim path through the real PLIC rather than a substituted claim value. tests/test_amp_startup_admission_fault.py releases the unchanged target through the real logger, then changes one CPU observation at a time. Its source-anchored diagnostic plugin retains the production RTL and Spike objects. The mechanical/thermal matrix covers every startup MMIO short circuit, every firmware-owned mailbox word, the command-submission guard and a zero-iteration real overload. A source-bound post-entry wrapper changes the already admitted hart word before calling the unchanged C main function, so the C range guard is exercised without bypassing the assembly owner gate. Refusal cases retain empty pre-start streams and cannot publish a capture or manifest; command blocking completes only after the independent hardware safe state. With an unserviced interrupt, the real fabric records every sample and deadline and enters the safe state on the third consecutive miss. The run times out without a target completion; its actual drained raw events remain available. These checks establish functional architectural behaviour, not Linux/HSS/PMP isolation or physical timing.

tests/test_amp_rust_capture_parity.py builds current Rust firmware and both production plant plugins, then runs the public capture command for C and Rust on each plant. It requires ten completed samples, 40 events and exact event/tracking stream equality per plant. It also compares interval rows after excluding the capture-specific run identifier. This establishes functional simulator parity, not physical timing or board acceptance.

tests/test_amp_rust_panic.py builds a separate source-bound RV64 image with a deliberate panic at the public Rust PID reset entry point. Both production plant plugins execute the image through the public capture command. The original Rust panic handler calls the shared firmware refusal path; the logger observes cause 0x109 before any sample and no completion, manifest or report is admitted. The fault is confined to the test-owned source copy; the production Rust adapter is unchanged.

tests/test_amp_rust_branch_coverage.py separately instruments the unchanged host safe core and C ABI adapter. Real C API/PID/LQR clients, public Rust core tests and a test-owned genuine panic producer must cover every reported source line and branch. That host profile does not substitute for the target refusal or physical coverage.

tests/test_amp_consumer_stall.py exercises actual telemetry starvation with a diagnostic scheduling variant built by tests/amp_stall_plugin.py from the current original Spike plugin. The fixture verifies the production plugin, original C++ compiler and every original link input against the selected build receipt before compiling its exclusive diagnostic source. It uses the normal WITNESS_SPIKE_PLUGIN and WITNESS_SPIKE_THERMAL_PLUGIN inputs and records the actual compile/link commands, source hashes and raw build output. After the first real sample is consumed, that variant suspends logger polling while continuing actual fabric event draining, target instruction execution and interrupt delivery. It never writes firmware-owned RAM. The unchanged firmware fills all 256 retained slots, then refuses the next publication with cause 0x100 and the attempted cycle. The test checks the actual RAM dump, every retained cycle and IRQ generation, the unchanged consumer position and the withheld final acknowledgement. Both mechanical and thermal variants are built and exercised by the parametrized fixture. These diagnostic plugins and altered run images remain outside capture admission. This test is distinct from forcing the full-ring arithmetic predicate through deliberate target RAM corruption.

The optional hash-bound amp_capture run field is distinct from native_metadata. It requires CONTROL, bare_metal_amp and rtl_simulation and forbids native_metadata in the same run. Capture repeats live build admission after execution and refuses receipt changes. Reanalysis requires the captured original build receipt and source index, including every original dependency. It verifies library identity, original captured bytes and the plant parameter read from the running RTL. Reanalysis uses the captured closure and does not require the original installed SDK/toolchain. It also verifies both image/compiler and execution/runtime library indexes against their original receipts, checks captured library bytes and reconciles the image's original preparation hash. Captured compiler metadata must include the original driver, all selected C subprograms, version and runtime libraries. Missing or incomplete metadata is refused before library lookup. Original preparation input hashes and preprocessing record hashes must agree with captured artifacts. The firmware compiler source index and captured bytes must still match the original preprocessing identities, even if outer capture and manifest hashes are recomputed. Offline analysis decodes the original verification argument vector without executing it, rebinds the captured DTB resource selection and re-admits the captured ELF contract and HTIF channel. The declared platform, run constants, stack, load segments, source inputs, compiler driver and simulation mode must agree with those original inputs. Rehashing contradictory image declarations does not make them admissible.

The analysis verifies the original receipt and artifacts, agrees with the executed tool and verified firmware identities, and reconciles controller coefficients, period, fault schedule, plant and exact converted tracking with the original run. Actual final sample, record, miss, overflow and safe-state counts must agree with the full event history, including warm-up. The logger acknowledges completion only after both streams drain and output closes.

Reports remain simulation_only. Board acceptance flags are false; there is no physical power series. Missing power keeps the normal validity gate false. Missing sample observations remain missing and can additionally invalidate tracking coverage. No interpolation or completion counter repairs a lost event. Reanalysis uses the normal command:

python tools/analyze_run.py capture/manifest.json --output-dir capture/reanalysis

The captured directory must remain intact. SHA-256 establishes byte identity, not trust in a compromised simulator, compiler, plugin or host. Physical deployment additionally needs verified Linux/HSS/PMP ownership, hardware acquisition and the same-bitstream acceptance procedure in the measurement protocol.