tin  1.5.9
verification_and_evidence

Purpose

Verification and evidence artifacts make behavior, generated outputs, resource use, and replay coverage inspectable. They give a project a concrete trail from machine definition to generated reviews, host tests, target profiles, and resource manifests.

The evidence path is an engineering review workflow. It records what was checked, what was generated, and which bounded runtime surfaces were selected.

Artifact Types

The current tooling and runtime surfaces use stable schema names for reviewable artifacts:

Artifact Schema Use
Artifact manifest tin.artifacts.v1 target, runtime, transport, evidence, generated artifact, and package metadata index
Machine IR verified-tsm.machine.v1 state, event, transition, runtime, transport, and evidence metadata
Trace replay verified-tsm.trace.v1 finite event traces used by generated conformance tests
Traceability verified-tsm.traceability.v1 requirement-to-test and trace coverage mapping
Resource manifest tsm.resource_manifest.v1 static runtime resource accounting

Resource Manifests

Runtime resource manifests record bounded storage and accounting information in a JSON form that can be checked into an evidence bundle.

#include <cstddef>
#include <sstream>
#include "tsm/runtime.h"
tsm::resource_snapshot snapshot{};
snapshot.queue_slots = 8;
snapshot.max_event_bytes = 32;
snapshot.max_event_alignment = alignof(std::max_align_t);
snapshot.task_count = 2;
snapshot.task_arena_bytes = 1024;
std::ostringstream manifest;
tsm::write_resource_manifest(manifest, "drive-controller", snapshot);
tsm::runtime::write_resource_manifest
void write_resource_manifest(Stream &output, char const *name, resource_snapshot const &snapshot)
Definition: resource_manifest.h:27
tsm::runtime::resource_snapshot
Definition: resources.h:23
tsm::runtime::resource_snapshot::queue_slots
std::size_t queue_slots
Definition: resources.h:26
runtime.h
Convenience include for runtime queue, executor, and topology APIs.

The caller owns the stream and decides where the resulting bytes go.

Trace Replay

Finite traces are the bridge between specifications, generated conformance tests, and runtime behavior checks. Trace generation records expected behavior as data, then emits C++ test cases that replay those traces against the public runtime surface.

The trace path is useful for:

  • regression tests for a machine's accepted event sequences;
  • negative tests for invalid or malformed traces;
  • review of equal-deadline wake ordering and queue behavior;
  • requirement coverage reports that point at generated tests.

The tooling treats traces as finite examples. It does not claim that a trace file proves every possible interleaving.

Quality Commands

Run the quality build and tests before treating the documentation and generated artifacts as current:

cmake --build build/quality
ctest --test-dir build/quality --output-on-failure

The quality suite covers machine tooling smoke tests, generated Python import checks, generated pybind11 skeleton checks, trace generator checks, resource manifest checks, and runtime behavior tests.

Related Pages