tpt-embedded-tools

Host-side verification, simulation, and analysis suite for tpt-embedded-core.

Overview

tpt-embedded-tools provides CLI-native, CI-first tooling for the tpt-embedded-core no_std ESP32 firmware. While tpt-basestation serves end-users and tpt-embedded-core provides mathematically verified firmware, this suite enforces safety guarantees from the first line of code to deployment.

Architecture

tpt-embedded-tools/
├── libs/
│   ├── tpt-e-elf-parser/        # ELF/DWARF parsing for both Xtensa & RISC-V
│   ├── tpt-e-trace-codec/       # Binary wire schema for structured runtime traces
│   └── tpt-e-esp32-model/       # ESP32 peripheral/register data models
├── crates/
│   ├── tpt-e-simulator/         # Instruction-accurate ESP32 simulator
│   ├── tpt-e-probe/             # Host-side structured trace viewer/verifier
│   ├── tpt-e-stack-analyzer/    # Worst-case stack depth verifier
│   ├── tpt-e-hil-framework/     # Automated hardware-in-the-loop testing
│   ├── tpt-e-peripheral-prover/ # TRM-based register access verifier
│   ├── tpt-e-power-profiler/    # Code-to-physical-power correlator
│   └── tpt-e-invariant-checker/ # Cross-crate invariant static analyzer
└── .github/workflows/           # CI pipelines

Current Status

Status key: 🟢 MVP-complete (real logic, exercised by tests) · 🟡 partially functional (a real code path exists but with known, documented gaps) · 🔴 scaffold/stub only (no functional implementation yet).

Crate	Status	Description
tpt-e-elf-parser	🟢	ELF/header/symbol parsing + DWARF extraction + disassembly-based call-graph edges (direct calls) for Xtensa + RISC-V; on-disk ELF corpus under fixtures/elf; indirect-call detection is not yet implemented
tpt-e-trace-codec	🟢	Binary wire schema for runtime traces, with round-trip encode/decode
tpt-e-esp32-model	🟢	ESP32 peripheral/register models (timer, GPIO, UART)
tpt-e-simulator	🟢	Real RV32IMC + Xtensa call0 (16/24-bit) decode/execute via Cpu::step, deterministic trace recording, fault-injection hooks; full ISA coverage pending
tpt-e-probe	🟢	File + serial trace ingestion (StreamDecoder incremental decode), invariant verification against checked-in fixtures, text/JSON viewer; hardware serial streaming pending
tpt-e-stack-analyzer	🟢	Worst-case stack depth analysis over a call graph, incl. recursion/ISR handling — most-tested crate; dynamic-dispatch detection is not yet implemented (see crate docs)
tpt-e-hil-framework	🟡	Step-based HIL orchestration (flash/reset/expect/inject/wait) over real serial transport (serialport) + espflash CLI, with mock mode for CI; real-hardware validation pending
tpt-e-peripheral-prover	🟢	TRM register-access verifier: constraint model (access bits, preserve masks, sequencing), JSON model overlay, typed + MMIO source checks; integration with tpt-e-invariant-checker and real tpt-embedded-core HAL pending
tpt-e-power-profiler	🟢	Power CSV ingestion, trace/power timestamp alignment, per-state energy integration + report (text/JSON); physical-hardware validation pending
tpt-e-invariant-checker	🟢	Syn-based AST parsing with per-function call-graph reachability analysis (falls back to token-based pattern matching if a target file fails to parse); catches violations across function calls, not just within one function
tpt-e-types	🟢	Shared Invariant/Violation/TraceEvent types across the suite

Quick Start

# Build all crates
cargo build --workspace

# Run all tests
cargo test --workspace

# Run clippy
cargo clippy --workspace -- -D warnings

# Check formatting
cargo fmt --all -- --check

# Run any workspace tool binary through the meta-CLI
cargo xtask run stack-analyzer -- --elf fixtures/elf/riscv_simple_call.elf --limit 8192

# Walk through the whole pipeline end-to-end on checked-in fixtures
bash examples/walkthrough.sh                                    # Linux/macOS
powershell -ExecutionPolicy Bypass -File examples/walkthrough.ps1 # Windows

# Scaffold a new cross-crate invariant rule + fixture + test
bash scripts/new-invariant.sh <name> <source_crate> <target_crate> <resource> <constraint>

See examples/README.md for a step-by-step walkthrough, docs/cross-repo-integration.md for how tpt-embedded-core adopts this suite, and .pre-commit-config.yaml (pre-commit install) to run the fmt/clippy/test/deny bundle before each commit.

Design Decisions

Simulator Backend

The simulator uses a pure-Rust interpreter behind an ExecutionBackend trait, enabling a future QEMU-FFI backend to be added without rearchitecting trace consumers.

Dual-ISA Strategy

Both Xtensa and RISC-V (RV32IMC) are supported via a shared Isa trait/enum used by tpt-e-elf-parser, tpt-e-simulator, and tpt-e-stack-analyzer.

ELF/DWARF Parsing

We use the goblin crate for ELF parsing, providing robust support for both EM_XTENSA and EM_RISCV architectures.

HIL Framework

Hardware-in-the-loop testing uses espflash for flash/reset orchestration, mirroring tpt-basestation's existing serial transport pattern.

License

Licensed under either of:

• Apache License, Version 2.0 (LICENSE-APACHE)
• MIT License (LICENSE-MIT)

at your option.