2.4 KiB
Development and verification
The Cargo workspace separates shared production logic from process entry points. lazaret-core is the initial library boundary. The lazaret Client, lazaret-host-coordinator, lazaret-runtime-supervisor, lazaret-network-sidecar, and lazaret-escalation-client executables are thin binary packages; process behavior belongs in libraries so it can be verified without invoking private binary internals.
support/work-packages.toml is the dependency authority. support/model-refinements.toml assigns every modeled action and configured property to production packages and verification levels. support/external-tools.toml fixes the baseline host and tool contracts, including exact kernel qualification records and whether an unavailable capability fails or skips a level. support/process-safety.toml pins dependency source identities, features, and reviewed process APIs and registers the compiler and exercised-path syscall checks for the exclusive spawn/reap broker boundary. docs/implementation-dependencies.md, docs/host-support.md, and .clippy.toml are generated registry outputs.
Run tools/verify-v1, tools/verify-v2, tools/verify-v3, tools/verify-v4, or tools/verify-v5. Each higher level includes the lower levels. V1 is host-local and includes format, Clippy, tests, dependency policy, registry drift, and both TLC models. Physical suites register commands in support/integration-tests.toml; an empty level is an explicit skip. A registered scenario may skip only when every missing capability has policy = "skip" in the external-tool manifest.
Normal verification is offline: Cargo receives --offline and cargo-deny receives --frozen. tools/dev refresh-advisories is the explicit online operation that updates the local RustSec database and then verifies advisories offline. Every level audits the all-feature dependency source checksums, versions, enabled features, reviewed process APIs, generated compiler policy, and unauthorized lint exemptions. V2 registers optional strace cases for exact exercised binary paths; a missing tracer skips those cases, while an observed extra exec, process creation, wait, or SIGCHLD mutation fails. Dynamic tracing does not claim coverage of unexercised paths.
Run tools/dev generate after changing the work-package, external-tool, or process-safety registry. tools/dev generate --check fails when either committed generated view differs.