PRODUCT.md owns behavior and acceptance. UI_GUIDELINES.md
owns terminal behavior and UI cases. CODING_STYLE.md owns implementation,
safety, allocation, and gate constraints. This document owns verification.
Design
Test production boundaries directly:
input bytes/time → input events;
state/events → state and typed effects;
state/dimensions → bounded cell grid;
grid differences → terminal operations;
filesystem, process, logging, worker, and terminal effects.
No parallel implementation, generic mocking framework, or general-purpose scenario language. Tests
stay ordinary Zig, deterministic, bounded, and offline by default. They never modify operator data
or real package state.
Tests use synthetic trees, fixed clocks, deterministic ordering, fake executables, injected metadata,
and isolated fixtures. Hard-link tests use injected metadata or a probed capable filesystem. Network
tests require an explicit build option and are off by default.
Synchronization
Tests advance a fixed logical clock. They coordinate through injected completions, bounded queues,
readiness events, and test-owned barriers/latches. Use run_one_turn, drain_ready, or
advance_until(predicate, bound) only with a finite registered bound; failures report predicate,
queue state, and trace.
Use pipes/readiness for child processes, PTY readiness/events for terminal tests, and injected
scheduler completions for workers. Release setup/effect barriers only on observed events. Never use
host wall time for ordering.
std.Thread.sleep, timer polling, busy-wait loops, arbitrary retry delays, and time-derived seeds
are forbidden. A real timeout may bound a hung external or capable-platform operation; expiry is a
failure or not_admitted, never successful synchronization. Every wait has a finite event, byte,
iteration, or logical-time bound.
Suites
U — policy/unit: manual-only policy, preselection, accounting, ordering, bounds, positive and
negative cases.
SM — state machine: fixed clocks, events, completions, failures, cancellation, queue saturation,
stale generations; assert invariants and forbidden effects after every event.
R — rendering: semantic content and bounded grids at required dimensions, ASCII/no-color,
invalid text, partial writes, unchanged frames; check structure independently of golden text.
A — filesystem/adapters: synthetic trees and fake executables; identities, ancestry, manifests,
argv, output bounds, dry-run traces, and fixture differences.
PTY: real input decoding, resize, backpressure, signals, cancellation, restoration, confirmation.
SIM: bounded seeded schedules; failures retain seed and replay trace.
M — manual/capable platform: evidence only for the recorded environment and scope.
Simulation corpus: per registered SIM specification, local zig build test runs 256 schedules
(seed indexes 0..255); CI zig build ci runs 4096 (0..4095). Seed is
0x544A53494D000000 + index, evaluated ascending without randomization or wall time. Every schedule
uses registered event, queue, and work bounds. A failure stops that invocation and retains seed,
complete bounded trace, first failing invariant, and forbidden effect. A passing corpus attempts every
index. Each specification owns an independent corpus.
Adapter capability evidence
Read-only planning evidence is scoped to one manager operation, manager/runtime version, effective
configuration, executable, argv, allowlisted environment, network policy, and fixture. Repeat it when
any input changes.
Run in a fresh fixture with dedicated HOME, temporary, XDG, cache, log, configuration, prefix, and
project paths. Compare bounded before/after manifests; trace filesystem, process, and network effects
where possible; include manager/runtime startup and shutdown. Any requested write outside the run log
fails read-only capability. If the operation cannot be observed or prohibited, mark it unavailable.
Default tests use fakes. Evidence never reads or modifies operator package state, HOME, shared storage,
credentials, or repositories.
Capable-platform admission
Each capable-platform test declares one key:
filesystem/mount identity;
allocated blocks;
descriptor-relative access with beneath/no-symlink constraints;
no-follow metadata/open;
regular-file, symlink, and directory mutation sequence;
exact package-manager read-only planning tuple;
logging append, partial-write, and flush;
terminal input, resize, restoration, and output transport.
A probe records key, filesystem/manager identity, kernel interface/version, mount/configuration tuple,
fixture, setup/cleanup, result, confidence, evidence revision/date, and artifact. Record raw paths,
argv, environment allowlist, and network policy where relevant. Keep records bounded and reproducible;
never use operator data.
Admission requires supported plus evidenced for the same scope. unknown, unsupported,
contradicted, stale/mismatched evidence, missing isolation, or missing fixture yields not_admitted,
not pass or silent skip. Transient failure remains unknown for the current filesystem generation.
Mutation tests additionally prove the exact isolated operation trace. Package tests require exact
executable identity, manager/runtime versions, configuration, plugin/hook policy, operation, network
policy, and refreshed effect-set scope.
Manual evidence
Suite M records operator, date, device/OS, application revision, configuration, steps, expected
and observed result, artifacts, and limitations. It excludes credentials, payloads, and unrelated
personal data. It proves only its recorded environment; it never replaces an automated invariant.
Residual race: isolated same-permission replacement and ancestor-move cases; final checks,
mutation order, observed target/location, disclosure, reproduction status. Never claim prevention;
non-reproduction proves nothing.
Accessibility: phone and large terminal, documented assistive technology; focus, selection,
warning, incomplete, confirmation, resize, cancellation, and error comprehension without color or
Unicode-only cues; record unsupported features.
Android confirmation: one allowlisted add-on per run through system confirmation; package,
request, choice, outcome, refreshed state, unobservable interval. Base and non-allowlisted IDs are
negative cases.
Package manager: exact tuple, local/network policy, startup/shutdown, read-only result, effect
set, execution, hooks, cache scope, refreshed state. Any write outside the run log fails purity;
unobservable effects are unavailable/uncertain.
Evidence expires when platform, filesystem/manager, kernel interface, terminal, executable,
configuration, hook policy, or operation changes.
Evidence
Every record contains requirement + revision, suite, case, result, and limitation.
Failure evidence includes invariant, initial state, event trace, transitions, effect ledger, expected/
actual grids, terminal bytes, fixture difference, and replay seed where applicable.
Suite-specific fields:
U: inputs, expected invariant, actual value, forbidden effects;
Non-applicable fields are explicit not_applicable. Evidence is bounded; only diagnostics may
truncate, with truncated: true. Cell grids are the screen oracle, but never replace dimension,
width, clipping, and initialization checks. Screenshots/recordings are supplementary.
The build graph additionally writes one bounded, transient suite-execution record per suite after a
fresh successful run (spec-tool evidence joins it to the current graph). It records suite
execution only, per spec/ENGINE.md suite evidence records; it never replaces the per-case evidence
fields above and never constitutes requirement acceptance.
Deterministic formats
A replay trace is framed canonical JSON, one object per line, fixed key order, no insignificant
whitespace:
Header: schema, case, requirement, revision, suite, seed. Events: increasing sequence,
actor, event, bounded inputs, effects, result. Raw bytes use lowercase hex plus byte length;
optional absence is null; authority/state/effect fields never truncate. Exclude timestamps, addresses,
pointers, PIDs, discovery order, and host-specific temporary paths. Failed simulations retain the
complete bounded trace and seed.
A fixture difference is sorted by raw relative path bytes, then operation. Each record has path_hex,
path_length, operation (added, removed, changed, unchanged), and bounded before/after
metadata: type, identity, size, modification timestamp/resolution, link state, and content digest
when observable. Unknown is explicit. Header: fixture identity/revision, root label, record count.
Duplicate paths, unsorted records, invalid lengths, missing operation tags, and unbounded fields fail.
Compare canonical artifacts as bytes; human reports are projections only.
Requirement manifest
Generated REQUIREMENTS.md projects canonical spec/model/requirements.zon:
required suites, invariant status, registered verification obligations, platform-evidence status/
references, and limitation status/references. unassessed is a gap, never a pass. mapped means a
claimed verification path exists; it does not mean implementation or suite success. Evidence statuses
not_required, required_missing, and recorded do not establish coverage. References resolve to
authoritative paths/anchors; descriptions stay with their owners. Atomic obligations belong to
spec/model/verification.zon.
Consistency classes:
missing:mapped requirement has no claimed verification path;
duplicated: requirement, obligation, claim, or reference repeats;
obsolete: owner/evidence/limitation/requirement/obligation reference fails to resolve at its
revision;
conflicting: claim polarity disagrees with obligation, or status conflicts with references.
Checks prove structure and relationships only, not invariant sufficiency, evidence strength, or
product completeness. Semantic mapping remains human-owned until assessed.
Source and test manifests
spec/model/implementation.zon owns production src/**/*.zig paths, revisions, SHA-256 fingerprints,
and realized obligations. spec/model/tests.zon owns test specs; tests/implementations.zon binds
fixtures to executable tests/**/*.zig sources, fixture revisions, modules, and fingerprints.
The lint/spec gate walks src/ and tests/ recursively. Every Zig source has exactly one applicable
owner. It rejects unregistered sources, duplicate ownership, stale fingerprints/revisions, skipped or
unfinished bound tests, handwritten product tests outside the fixture graph, and unknown bindings.
Generated fixture tests are derived from bindings, not exceptions. Move/delete = manifest change.
Lint policy
Lint hard-fails with file, span, policy, and remediation. Use Zig AST where syntax matters; bounded
source scans only for literal policy tokens.
Skipped tests: reject error.SkipZigTest; suite status must be executable.
Recursion: AST call graph detects direct self-recursion and bounded strongly connected components;
no recursion exception exists. Function-pointer/indirect gaps remain explicit limitations.
Shell: inspect process-call args/literals for interpreters, shell evaluation, command-string
construction, and package/path interpolation. Only registered process boundaries are allowed.
Telemetry/cache: reject telemetry endpoints, analytics/event clients, unregistered network sinks,
scan-index persistence, metadata caches, and resume stores. Run logs and configured user config are
owner-approved.
Dependencies: compare imports/build manifests with the first-party allowlist; undeclared or
vendored third-party code fails.
Bounds: every capacity, timeout, queue, output, path, depth, and retry bound resolves to
spec/model/limits.zon or a documented language/ABI constant; new product bounds need registry and
boundary tests.
Processes: every spawn/execute/signal/reap/manager-process call resolves to one ADAPTERS.md
registry entry with location, role, argv/output bounds, timeout, cancellation, network scope,
capability evidence, and owning tests.
Generated code is checked from canonical registries. Detector blind spots are evidence limitations,
not compliance.
Negative-space coverage
Cancellation and stale generations
Inject cancellation at every legal checkpoint: traversal root/enumeration/metadata/mount/capability/
depth-capacity; planning discovery/adapter/network/dependency/serialization/manifest; logging frame,
write/retry/flush; revalidation root/ancestor/leaf/child-set/final check; mutation/manager admission
and reconciliation. No checkpoint exists between final revalidation and adjacent mutation request.
Assert stop of new admission, reconciliation of admitted effects, durability, remaining-plan
invalidation, no rollback/continuation, and generation release. Indivisible syscall/transaction
completion is observed, never classified by event order.
Deliver every completion class before and after an effect: traversal, metadata, process, network,
logging, filesystem, manager, revalidation, reconciliation. Before effect: discard stale presentation
with no state/authority/accounting change. After effect: reconcile normally, retain result/audit,
update accounting, invalidate remaining plan. Reuse no old storage, handle, buffer, plan, or ID.
Queues and accounting
Fill ordinary capacity while reserved completion, cancellation, resize, failure, shutdown, audit, and
control paths remain. Assert reserved capacity, deterministic mandatory processing, progress coalescing/
drop accounting, no silent required loss, admission stop, optional redraw suppression, live input/status/
quit, and pre-admission unavailability when authority/effect reserve cannot fit.
Inject overflow/unknown at block conversion, file, directory, hard-link, package, filesystem, unified,
selected, filtered, per-filesystem, and reclaim levels. Unknown/incomplete affected aggregate + one
warning + bounded evidence; independent values survive. No wrap, clamp, storage saturation, apparent-byte
substitution. Diagnostic counters may saturate only as at least N.
Bytes and processes
Use invalid UTF-8, C0/DEL/C1/bidi controls, noncharacters, tabs/newlines/CR, separators, quotes,
option-like prefixes, shell metacharacters, leading hyphens, empty components, and post-sanitization
collisions in paths, targets, package names, and argv. Assert strict escaping, bounded width,
collision-safe deterministic labels, explicit unknowns, unchanged authority/argv bytes, and no shell
interpretation. Distinct raw identities never share an actionable display key.
Fake processes cover startup failure, timeout, ignored interrupt, escalation, stalled pipes, closure,
oversized stdout/stderr/required output, nonzero/signal exit, malformed output, detached descendants,
and outliving groups. Assert concurrent drain, bounded explicit truncation, cancellation/reaping,
uncertain classification, no deadlock/shell/unbounded allocation, and no mutation with incomplete
authority. Detached/unobservable = uncertain, never success.
Logging
Fail open/create/parent flush, frame allocation, intent/result writes and partial writes, bounded
EINTR, flushes, audit/payload capacity, disk-full, quota, read-only remount, disconnect, and
descriptor operations independently. Intent failure blocks admission and future mutation. Result
failure after mutation pauses, marks observed/audit state uncertain, disables mutation, and offers
review/quit only. Never repair/truncate partial frames; authority/effect fields never truncate. Exactly
one intent precedes each admitted action; exactly one result follows it, including cancellation,
partial, uncertain, and signal outcomes.
Plans, effects, and directories
Change each material plan field → review; each presentation field → same identity. Cover every action/
field tag, unknown/zero/max lengths, raw bytes, endianness, padding, version, dry-run byte identity,
mutable-storage aliasing, action keys/ties/dependencies/duplicates, discovery-order permutations,
group headers/collapse/cross-group edges, and common/filesystem/symlink/directory/package applicability.
Cover dependency edges/cycles, exact/missing/additional/ambiguous effects, failed/cancelled/skipped/
partial/uncertain outcomes, manager-level expectations, direct authority non-expansion, and independent
continuation only after revalidation.
For manifests cover every field, parent chains, empty/manual-only descendants, bulk prohibition,
deepest-first/raw-byte order, symlinks, capacity ±1, enumeration/metadata/cancellation failures,
and new/missing/moved/duplicate/changed/cross-mount entries. Revalidation changes every root/ancestor/
leaf field; traces assert root reconstruction, validation before descent, child-set comparison, final
check, immediate unlinkat/AT_REMOVEDIR, and no-follow behavior. Unsupported checks and special
types follow TJ-EXEC-03 and TJ-EXEC-05. Revalidation drift covers ancestor replacement, leaf
replacement, mount change on any reviewed path, link-count change against reviewed metadata, new or
removed children, and exactly recorded prior-dependency effects, each asserted with the owner-defined
fail-before-mutation and expected-effect behavior (TJ-EXEC-01, TJ-EXEC-02, TJ-EXEC-04, TJ-EXEC-05).
UI, package, and classification
Confirmation covers every prefix, case, overflow, Backspace, mismatch, Escape/Ctrl-C, buffered input,
paste/mouse/escape input, repeated keys, stale generation, and partial plan change. Render every action,
manifest count, estimate state, counter state, and destructive-effect value; unknown estimate confirmable,
unknown authority not. Ordering covers every tier/key/threshold and discovery permutation.
Package ranking covers 0–11 known sizes, tenth ties, fewer-than-ten known plus unknown, unknown counts,
capacity exhaustion, and show-all without scan/allocation effects. Identity covers aliases, roots, native
keys, versions/slots, domains, unknown/conflicting ownership, provenance, and no executable action.
Package drift covers direct, indirect, and dependency-level additions and removals, manager-level
operation reorderings, declared hook identity, invocation-phase, and policy changes, cache-scope
changes, and manager-version, runtime-version, and effective-configuration changes outside the
evidenced tuple. Every changed effect returns the action to review and no manager operation is
admitted against it; every changed tuple demotes the operation to discovery-only until evidence is
repeated; a prior confirmation never authorizes a changed plan. A reordering that canonicalizes to
identical plan bytes preserves plan identity.
Set shapes are named per surface: empty, maximum, all-hidden, all-unknown, equal-rank, and exact
threshold-boundary sets, each asserted with the owner-defined inclusive boundary, review-list,
empty-result, and bulk-scope semantics (TJ-CLASS-14, TJ-UI-03, TJ-UI-04).
Terminal lifecycle covers normal exit, startup error, runtime error, handled signals, suspension,
resize below the required minimum, and disconnect, each asserted with the owner-defined restoration,
diagnostic, suspend/resume, bounded disconnect, and clamp behavior (TJ-TERM-09, TJ-TERM-02).
Input decoding covers buffered and bracketed-paste confirmation, key auto-repeat, legacy
unmarked-input disclosure, fragmented multibyte input, malformed mouse input, and keyboard recovery,
each asserted with the owner-defined generation discard, non-contribution, disclosure, and
ground-state recovery behavior (TJ-PLAN-10, TJ-TERM-07).
Focus/refresh/browser/filter/key-map tests cover reorder/insert/remove/hide/clear, empty state, generation
slots/exhaustion, stale effects, browser states/navigation, AND/OR/unknown/search, summaries, every key,
help, unavailable reasons, ASCII/no-color, and forbidden effects.
Thresholds use fixed realtime references below/at/above all bounds plus future/missing/invalid/
unrepresentable/coarse timestamps and refresh/wall-clock changes. Accounting covers every conversion,
aggregate, identity generation, overlap, hard-link combination, partial execution, and eventual-release
uncertainty. Symlink resolution covers host/proot relative/absolute roots, namespace boundaries, 39/40/41
links, loops, missing/untrusted namespaces, disagreement, separate identities, unknown-not-broken, and
no target authority.
Normative inventory
Every limit in LIMITS.md has a named boundary test, reserved-capacity invariant, and
limit - 1, limit, limit + 1 coverage:
Scalar limits test below/at/above with checked conversion and no negative case. Dimensions test each
axis independently and together. Alternatives test each component and mixed boundary pairs. Counts/
bytes also test empty input, exact capacity, omission accounting, and reserved capacity where required.
A registered limit without a named test fails the manifest.
Cover every traversal attempt outcome, root normalization, shared-storage alias, mount boundary,
capability/confidence transition, and display collision from FILESYSTEM_CAPABILITIES.md;
every classification rule from CLASSIFICATION.md; every adapter row/state,
version/configuration tuple, effect field, binding/result status, Android ID, and process role from
ADAPTERS.md; every configuration invalid class and CLI option/conflict/stream/terminal
case from CONFIGURATION.md and model/cli.zon; and every required terminal
size, status field, Unicode class, input protocol, restoration, write/backpressure, and unchanged frame.
Gates
Suite matrix
The build graph is authoritative:
Gate
Runs
zig build test
engine/synthetic/tool/generated-registry tests, generated format, spec validation, and locally enabled U, SM, R, A, SIM;
zig build check
test plus source format and lint/spec validation;
zig build ci
check plus registered non-local PTY/M suites and admitted capable-platform lanes.
A suite requires a test spec and executable binding. Missing binding = validation failure, not skip.
-Dsuite=NAME narrows fixture execution only; base generation, formatting, manifest, and spec checks
remain. Unavailable platform = not_admitted, never pass or silent skip.
Tracked-file immutability
check and ci compare pre/post manifests of every tracked path: raw path, kind, byte length, and
SHA-256, sorted by raw bytes. The pre-gate snapshot includes existing dirty work; a clean tree is not
required. Any add/remove/rename/change fails with both records. The gate never repairs, restores,
stages, or deletes. Temporary outputs are outside the manifest; tracked projections must remain equal.
CI also records commit identity from a clean checkout. No warning or environment bypass.
Tests are deterministic, bounded, offline by default, and never modify operator data or real package
state.
Deferred verification directions
These directions are explicitly rejected for version 1 gates and revisited only through a
specification change.
Agent-driven acceptance QA: deferred. Repository gates must stay deterministic and mechanical;
an agent report is advisory observation, never gate evidence or a semantic authority (TJ-GOV-12).
Human-readable agent reports may accompany a release only as unregistered side material.
Native Zig fuzzing: the pinned toolchain provides fuzz instrumentation and a continuous search
mode. Deferred for version 1 gates because the deterministic seeded negative-space suites own v1
coverage; admission requires a capable platform lane with a bounded corpus and failure retention
under the evidence rules above.
Sanitizer runtimes: thread-sanitizer and C undefined-behavior instrumentation exist in the
toolchain but are not gates on this host. They are admitted only through capable-platform evidence
with the same admission rules as any platform lane.
# Testing strategy
[`PRODUCT.md`](PRODUCT.md) owns behavior and acceptance. [`UI_GUIDELINES.md`](UI_GUIDELINES.md)
owns terminal behavior and UI cases. [`CODING_STYLE.md`](CODING_STYLE.md) owns implementation,
safety, allocation, and gate constraints. This document owns verification.
## Design
Test production boundaries directly:
- input bytes/time → input events;
- state/events → state and typed effects;
- state/dimensions → bounded cell grid;
- grid differences → terminal operations;
- filesystem, process, logging, worker, and terminal effects.
No parallel implementation, generic mocking framework, or general-purpose scenario language. Tests
stay ordinary Zig, deterministic, bounded, and offline by default. They never modify operator data
or real package state.
Tests use synthetic trees, fixed clocks, deterministic ordering, fake executables, injected metadata,
and isolated fixtures. Hard-link tests use injected metadata or a probed capable filesystem. Network
tests require an explicit build option and are off by default.
### Synchronization
Tests advance a fixed logical clock. They coordinate through injected completions, bounded queues,
readiness events, and test-owned barriers/latches. Use `run_one_turn`, `drain_ready`, or
`advance_until(predicate, bound)` only with a finite registered bound; failures report predicate,
queue state, and trace.
Use pipes/readiness for child processes, PTY readiness/events for terminal tests, and injected
scheduler completions for workers. Release setup/effect barriers only on observed events. Never use
host wall time for ordering.
`std.Thread.sleep`, timer polling, busy-wait loops, arbitrary retry delays, and time-derived seeds
are forbidden. A real timeout may bound a hung external or capable-platform operation; expiry is a
failure or `not_admitted`, never successful synchronization. Every wait has a finite event, byte,
iteration, or logical-time bound.
## Suites
1. **U — policy/unit:** manual-only policy, preselection, accounting, ordering, bounds, positive and
negative cases.
2. **SM — state machine:** fixed clocks, events, completions, failures, cancellation, queue saturation,
stale generations; assert invariants and forbidden effects after every event.
3. **R — rendering:** semantic content and bounded grids at required dimensions, ASCII/no-color,
invalid text, partial writes, unchanged frames; check structure independently of golden text.
4. **A — filesystem/adapters:** synthetic trees and fake executables; identities, ancestry, manifests,
argv, output bounds, dry-run traces, and fixture differences.
5. **PTY:** real input decoding, resize, backpressure, signals, cancellation, restoration, confirmation.
6. **SIM:** bounded seeded schedules; failures retain seed and replay trace.
7. **M — manual/capable platform:** evidence only for the recorded environment and scope.
Simulation corpus: per registered `SIM` specification, local `zig build test` runs 256 schedules
(seed indexes `0..255`); CI `zig build ci` runs 4096 (`0..4095`). Seed is
`0x544A53494D000000 + index`, evaluated ascending without randomization or wall time. Every schedule
uses registered event, queue, and work bounds. A failure stops that invocation and retains seed,
complete bounded trace, first failing invariant, and forbidden effect. A passing corpus attempts every
index. Each specification owns an independent corpus.
## Adapter capability evidence
Read-only planning evidence is scoped to one manager operation, manager/runtime version, effective
configuration, executable, argv, allowlisted environment, network policy, and fixture. Repeat it when
any input changes.
Run in a fresh fixture with dedicated HOME, temporary, XDG, cache, log, configuration, prefix, and
project paths. Compare bounded before/after manifests; trace filesystem, process, and network effects
where possible; include manager/runtime startup and shutdown. Any requested write outside the run log
fails read-only capability. If the operation cannot be observed or prohibited, mark it unavailable.
Default tests use fakes. Evidence never reads or modifies operator package state, HOME, shared storage,
credentials, or repositories.
### Capable-platform admission
Each capable-platform test declares one key:
- filesystem/mount identity;
- allocated blocks;
- descriptor-relative access with beneath/no-symlink constraints;
- no-follow metadata/open;
- regular-file, symlink, and directory mutation sequence;
- exact package-manager read-only planning tuple;
- logging append, partial-write, and flush;
- terminal input, resize, restoration, and output transport.
A probe records key, filesystem/manager identity, kernel interface/version, mount/configuration tuple,
fixture, setup/cleanup, result, confidence, evidence revision/date, and artifact. Record raw paths,
argv, environment allowlist, and network policy where relevant. Keep records bounded and reproducible;
never use operator data.
Admission requires `supported` plus `evidenced` for the same scope. `unknown`, `unsupported`,
`contradicted`, stale/mismatched evidence, missing isolation, or missing fixture yields `not_admitted`,
not pass or silent skip. Transient failure remains `unknown` for the current filesystem generation.
Mutation tests additionally prove the exact isolated operation trace. Package tests require exact
executable identity, manager/runtime versions, configuration, plugin/hook policy, operation, network
policy, and refreshed effect-set scope.
### Manual evidence
Suite `M` records operator, date, device/OS, application revision, configuration, steps, expected
and observed result, artifacts, and limitations. It excludes credentials, payloads, and unrelated
personal data. It proves only its recorded environment; it never replaces an automated invariant.
- **Residual race:** isolated same-permission replacement and ancestor-move cases; final checks,
mutation order, observed target/location, disclosure, reproduction status. Never claim prevention;
non-reproduction proves nothing.
- **Accessibility:** phone and large terminal, documented assistive technology; focus, selection,
warning, incomplete, confirmation, resize, cancellation, and error comprehension without color or
Unicode-only cues; record unsupported features.
- **Android confirmation:** one allowlisted add-on per run through system confirmation; package,
request, choice, outcome, refreshed state, unobservable interval. Base and non-allowlisted IDs are
negative cases.
- **Package manager:** exact tuple, local/network policy, startup/shutdown, read-only result, effect
set, execution, hooks, cache scope, refreshed state. Any write outside the run log fails purity;
unobservable effects are unavailable/uncertain.
Evidence expires when platform, filesystem/manager, kernel interface, terminal, executable,
configuration, hook policy, or operation changes.
## Evidence
Every record contains `requirement` + revision, `suite`, `case`, `result`, and `limitation`.
Failure evidence includes invariant, initial state, event trace, transitions, effect ledger, expected/
actual grids, terminal bytes, fixture difference, and replay seed where applicable.
Suite-specific fields:
- **U:** inputs, expected invariant, actual value, forbidden effects;
- **SM:** initial/final state, ordered trace, transitions, effect ledger, forbidden effects;
- **R:** dimensions, mode, expected/actual grids, structural checks, terminal bytes when applicable;
- **A:** fixture, capability probe, isolated paths, executable/argv, bounded environment,
before/after manifests, process/network trace, forbidden effects;
- **PTY:** terminal identity/dimensions, input bytes, decoded events, output bytes, restoration,
signal/resize/disconnect events, platform limitation;
- **SIM:** seed, replay schedule, initial state, trace, invariant/effect assertions, capacities,
final state.
Non-applicable fields are explicit `not_applicable`. Evidence is bounded; only diagnostics may
truncate, with `truncated: true`. Cell grids are the screen oracle, but never replace dimension,
width, clipping, and initialization checks. Screenshots/recordings are supplementary.
The build graph additionally writes one bounded, transient suite-execution record per suite after a
fresh successful run (`spec-tool evidence` joins it to the current graph). It records suite
execution only, per `spec/ENGINE.md` suite evidence records; it never replaces the per-case evidence
fields above and never constitutes requirement acceptance.
### Deterministic formats
A replay trace is framed canonical JSON, one object per line, fixed key order, no insignificant
whitespace:
```text
<decimal payload length> <eight lowercase CRC-32/ISO-HDLC hex digits> <JSON payload>\n
```
Header: `schema`, `case`, `requirement`, `revision`, `suite`, `seed`. Events: increasing `sequence`,
`actor`, `event`, bounded inputs, effects, result. Raw bytes use lowercase hex plus byte length;
optional absence is `null`; authority/state/effect fields never truncate. Exclude timestamps, addresses,
pointers, PIDs, discovery order, and host-specific temporary paths. Failed simulations retain the
complete bounded trace and seed.
A fixture difference is sorted by raw relative path bytes, then operation. Each record has `path_hex`,
`path_length`, `operation` (`added`, `removed`, `changed`, `unchanged`), and bounded before/after
metadata: type, identity, size, modification timestamp/resolution, link state, and content digest
when observable. Unknown is explicit. Header: fixture identity/revision, root label, record count.
Duplicate paths, unsorted records, invalid lengths, missing operation tags, and unbounded fields fail.
Compare canonical artifacts as bytes; human reports are projections only.
## Requirement manifest
Generated [`REQUIREMENTS.md`](REQUIREMENTS.md) projects canonical `spec/model/requirements.zon`:
required suites, invariant status, registered verification obligations, platform-evidence status/
references, and limitation status/references. `unassessed` is a gap, never a pass. `mapped` means a
claimed verification path exists; it does not mean implementation or suite success. Evidence statuses
`not_required`, `required_missing`, and `recorded` do not establish coverage. References resolve to
authoritative paths/anchors; descriptions stay with their owners. Atomic obligations belong to
`spec/model/verification.zon`.
Consistency classes:
- **missing:** `mapped` requirement has no claimed verification path;
- **duplicated:** requirement, obligation, claim, or reference repeats;
- **obsolete:** owner/evidence/limitation/requirement/obligation reference fails to resolve at its
revision;
- **conflicting:** claim polarity disagrees with obligation, or status conflicts with references.
Checks prove structure and relationships only, not invariant sufficiency, evidence strength, or
product completeness. Semantic mapping remains human-owned until assessed.
## Source and test manifests
`spec/model/implementation.zon` owns production `src/**/*.zig` paths, revisions, SHA-256 fingerprints,
and realized obligations. `spec/model/tests.zon` owns test specs; `tests/implementations.zon` binds
fixtures to executable `tests/**/*.zig` sources, fixture revisions, modules, and fingerprints.
The lint/spec gate walks `src/` and `tests/` recursively. Every Zig source has exactly one applicable
owner. It rejects unregistered sources, duplicate ownership, stale fingerprints/revisions, skipped or
unfinished bound tests, handwritten product tests outside the fixture graph, and unknown bindings.
Generated fixture tests are derived from bindings, not exceptions. Move/delete = manifest change.
### Lint policy
Lint hard-fails with file, span, policy, and remediation. Use Zig AST where syntax matters; bounded
source scans only for literal policy tokens.
- **Skipped tests:** reject `error.SkipZigTest`; suite status must be executable.
- **Recursion:** AST call graph detects direct self-recursion and bounded strongly connected components;
no recursion exception exists. Function-pointer/indirect gaps remain explicit limitations.
- **Shell:** inspect process-call args/literals for interpreters, shell evaluation, command-string
construction, and package/path interpolation. Only registered process boundaries are allowed.
- **Telemetry/cache:** reject telemetry endpoints, analytics/event clients, unregistered network sinks,
scan-index persistence, metadata caches, and resume stores. Run logs and configured user config are
owner-approved.
- **Dependencies:** compare imports/build manifests with the first-party allowlist; undeclared or
vendored third-party code fails.
- **Bounds:** every capacity, timeout, queue, output, path, depth, and retry bound resolves to
`spec/model/limits.zon` or a documented language/ABI constant; new product bounds need registry and
boundary tests.
- **Processes:** every spawn/execute/signal/reap/manager-process call resolves to one `ADAPTERS.md`
registry entry with location, role, argv/output bounds, timeout, cancellation, network scope,
capability evidence, and owning tests.
Generated code is checked from canonical registries. Detector blind spots are evidence limitations,
not compliance.
## Negative-space coverage
### Cancellation and stale generations
Inject cancellation at every legal checkpoint: traversal root/enumeration/metadata/mount/capability/
depth-capacity; planning discovery/adapter/network/dependency/serialization/manifest; logging frame,
write/retry/flush; revalidation root/ancestor/leaf/child-set/final check; mutation/manager admission
and reconciliation. No checkpoint exists between final revalidation and adjacent mutation request.
Assert stop of new admission, reconciliation of admitted effects, durability, remaining-plan
invalidation, no rollback/continuation, and generation release. Indivisible syscall/transaction
completion is observed, never classified by event order.
Deliver every completion class before and after an effect: traversal, metadata, process, network,
logging, filesystem, manager, revalidation, reconciliation. Before effect: discard stale presentation
with no state/authority/accounting change. After effect: reconcile normally, retain result/audit,
update accounting, invalidate remaining plan. Reuse no old storage, handle, buffer, plan, or ID.
### Queues and accounting
Fill ordinary capacity while reserved completion, cancellation, resize, failure, shutdown, audit, and
control paths remain. Assert reserved capacity, deterministic mandatory processing, progress coalescing/
drop accounting, no silent required loss, admission stop, optional redraw suppression, live input/status/
quit, and pre-admission unavailability when authority/effect reserve cannot fit.
Inject overflow/unknown at block conversion, file, directory, hard-link, package, filesystem, unified,
selected, filtered, per-filesystem, and reclaim levels. Unknown/incomplete affected aggregate + one
warning + bounded evidence; independent values survive. No wrap, clamp, storage saturation, apparent-byte
substitution. Diagnostic counters may saturate only as `at least N`.
### Bytes and processes
Use invalid UTF-8, C0/DEL/C1/bidi controls, noncharacters, tabs/newlines/CR, separators, quotes,
option-like prefixes, shell metacharacters, leading hyphens, empty components, and post-sanitization
collisions in paths, targets, package names, and argv. Assert strict escaping, bounded width,
collision-safe deterministic labels, explicit unknowns, unchanged authority/argv bytes, and no shell
interpretation. Distinct raw identities never share an actionable display key.
Fake processes cover startup failure, timeout, ignored interrupt, escalation, stalled pipes, closure,
oversized stdout/stderr/required output, nonzero/signal exit, malformed output, detached descendants,
and outliving groups. Assert concurrent drain, bounded explicit truncation, cancellation/reaping,
uncertain classification, no deadlock/shell/unbounded allocation, and no mutation with incomplete
authority. Detached/unobservable = `uncertain`, never success.
### Logging
Fail open/create/parent flush, frame allocation, intent/result writes and partial writes, bounded
`EINTR`, flushes, audit/payload capacity, disk-full, quota, read-only remount, disconnect, and
descriptor operations independently. Intent failure blocks admission and future mutation. Result
failure after mutation pauses, marks observed/audit state uncertain, disables mutation, and offers
review/quit only. Never repair/truncate partial frames; authority/effect fields never truncate. Exactly
one intent precedes each admitted action; exactly one result follows it, including cancellation,
partial, uncertain, and signal outcomes.
### Plans, effects, and directories
Change each material plan field → review; each presentation field → same identity. Cover every action/
field tag, unknown/zero/max lengths, raw bytes, endianness, padding, version, dry-run byte identity,
mutable-storage aliasing, action keys/ties/dependencies/duplicates, discovery-order permutations,
group headers/collapse/cross-group edges, and common/filesystem/symlink/directory/package applicability.
Cover dependency edges/cycles, exact/missing/additional/ambiguous effects, failed/cancelled/skipped/
partial/uncertain outcomes, manager-level expectations, direct authority non-expansion, and independent
continuation only after revalidation.
For manifests cover every field, parent chains, empty/manual-only descendants, bulk prohibition,
deepest-first/raw-byte order, symlinks, capacity ±1, enumeration/metadata/cancellation failures,
and new/missing/moved/duplicate/changed/cross-mount entries. Revalidation changes every root/ancestor/
leaf field; traces assert root reconstruction, validation before descent, child-set comparison, final
check, immediate `unlinkat`/`AT_REMOVEDIR`, and no-follow behavior. Unsupported checks and special
types follow TJ-EXEC-03 and TJ-EXEC-05. Revalidation drift covers ancestor replacement, leaf
replacement, mount change on any reviewed path, link-count change against reviewed metadata, new or
removed children, and exactly recorded prior-dependency effects, each asserted with the owner-defined
fail-before-mutation and expected-effect behavior (TJ-EXEC-01, TJ-EXEC-02, TJ-EXEC-04, TJ-EXEC-05).
### UI, package, and classification
Confirmation covers every prefix, case, overflow, Backspace, mismatch, Escape/Ctrl-C, buffered input,
paste/mouse/escape input, repeated keys, stale generation, and partial plan change. Render every action,
manifest count, estimate state, counter state, and destructive-effect value; unknown estimate confirmable,
unknown authority not. Ordering covers every tier/key/threshold and discovery permutation.
Package ranking covers 0–11 known sizes, tenth ties, fewer-than-ten known plus unknown, unknown counts,
capacity exhaustion, and show-all without scan/allocation effects. Identity covers aliases, roots, native
keys, versions/slots, domains, unknown/conflicting ownership, provenance, and no executable action.
Package drift covers direct, indirect, and dependency-level additions and removals, manager-level
operation reorderings, declared hook identity, invocation-phase, and policy changes, cache-scope
changes, and manager-version, runtime-version, and effective-configuration changes outside the
evidenced tuple. Every changed effect returns the action to review and no manager operation is
admitted against it; every changed tuple demotes the operation to discovery-only until evidence is
repeated; a prior confirmation never authorizes a changed plan. A reordering that canonicalizes to
identical plan bytes preserves plan identity.
Set shapes are named per surface: empty, maximum, all-hidden, all-unknown, equal-rank, and exact
threshold-boundary sets, each asserted with the owner-defined inclusive boundary, review-list,
empty-result, and bulk-scope semantics (TJ-CLASS-14, TJ-UI-03, TJ-UI-04).
Terminal lifecycle covers normal exit, startup error, runtime error, handled signals, suspension,
resize below the required minimum, and disconnect, each asserted with the owner-defined restoration,
diagnostic, suspend/resume, bounded disconnect, and clamp behavior (TJ-TERM-09, TJ-TERM-02).
Input decoding covers buffered and bracketed-paste confirmation, key auto-repeat, legacy
unmarked-input disclosure, fragmented multibyte input, malformed mouse input, and keyboard recovery,
each asserted with the owner-defined generation discard, non-contribution, disclosure, and
ground-state recovery behavior (TJ-PLAN-10, TJ-TERM-07).
Focus/refresh/browser/filter/key-map tests cover reorder/insert/remove/hide/clear, empty state, generation
slots/exhaustion, stale effects, browser states/navigation, AND/OR/unknown/search, summaries, every key,
help, unavailable reasons, ASCII/no-color, and forbidden effects.
Thresholds use fixed realtime references below/at/above all bounds plus future/missing/invalid/
unrepresentable/coarse timestamps and refresh/wall-clock changes. Accounting covers every conversion,
aggregate, identity generation, overlap, hard-link combination, partial execution, and eventual-release
uncertainty. Symlink resolution covers host/proot relative/absolute roots, namespace boundaries, 39/40/41
links, loops, missing/untrusted namespaces, disagreement, separate identities, unknown-not-broken, and
no target authority.
### Normative inventory
Every limit in [`LIMITS.md`](LIMITS.md) has a named boundary test, reserved-capacity invariant, and
`limit - 1`, `limit`, `limit + 1` coverage:
- **scan:** `raw_path_bytes`, `raw_component_bytes`, `symlink_target_bytes`, `traversal_depth`,
`configured_scan_roots`, `workspace_roots`, `document_roots`, `exclusions`, `manual_only_rules`,
`filesystem_identity_domains`, `retained_findings`, `retained_package_records`, `retained_warnings`,
`hard_link_identity_records`, `plan_actions`, `manifest_entries_per_action`,
`manifest_entries_per_plan`, `expected_effects_per_plan`;
- **process:** `child_process_groups`, `arguments_per_invocation`, `argument_vector_bytes`,
`captured_stdout_bytes`, `captured_stderr_bytes`, `normalized_diagnostics_bytes`,
`test_process_timeout`, `discovery_timeout`, `planning_timeout`, `mutation_timeout`,
`interrupt_grace_period`, `termination_grace_period`, `kill_and_reap_period`;
- **queue:** `fixed_workers`, `pending_worker_jobs`, `worker_completions`, `ui_events`,
`input_bytes_per_turn`, `events_per_turn`, `cells_per_turn`, `terminal_bytes_per_turn`,
`terminal_writes_per_turn`, `worker_cancellation_interval`, `ui_work_per_turn`,
`input_acknowledgement`;
- **terminal:** `terminal_input_buffer_bytes`, `escape_sequence_bytes`, `escape_ambiguity_timeout`,
`cell_grid_dimensions`, `pending_terminal_output_bytes`, `terminal_restoration_attempts`,
`terminal_restoration_interval`;
- **logging:** `log_payload_bytes`, `diagnostic_argument_bytes`, `escaped_log_value_bytes`,
`log_write_attempts`, `log_eintr_retries`, `audit_events_per_action`.
Scalar limits test below/at/above with checked conversion and no negative case. Dimensions test each
axis independently and together. Alternatives test each component and mixed boundary pairs. Counts/
bytes also test empty input, exact capacity, omission accounting, and reserved capacity where required.
A registered limit without a named test fails the manifest.
Cover every traversal attempt outcome, root normalization, shared-storage alias, mount boundary,
capability/confidence transition, and display collision from [`FILESYSTEM_CAPABILITIES.md`](FILESYSTEM_CAPABILITIES.md);
every classification rule from [`CLASSIFICATION.md`](CLASSIFICATION.md); every adapter row/state,
version/configuration tuple, effect field, binding/result status, Android ID, and process role from
[`ADAPTERS.md`](ADAPTERS.md); every configuration invalid class and CLI option/conflict/stream/terminal
case from [`CONFIGURATION.md`](CONFIGURATION.md) and `model/cli.zon`; and every required terminal
size, status field, Unicode class, input protocol, restoration, write/backpressure, and unchanged frame.
## Gates
### Suite matrix
The build graph is authoritative:
| Gate | Runs |
| --- | --- |
| `zig build test` | engine/synthetic/tool/generated-registry tests, generated format, spec validation, and locally enabled `U`, `SM`, `R`, `A`, `SIM`; |
| `zig build check` | `test` plus source format and lint/spec validation; |
| `zig build ci` | `check` plus registered non-local `PTY`/`M` suites and admitted capable-platform lanes. |
A suite requires a test spec and executable binding. Missing binding = validation failure, not skip.
`-Dsuite=NAME` narrows fixture execution only; base generation, formatting, manifest, and spec checks
remain. Unavailable platform = `not_admitted`, never pass or silent skip.
### Tracked-file immutability
`check` and `ci` compare pre/post manifests of every tracked path: raw path, kind, byte length, and
SHA-256, sorted by raw bytes. The pre-gate snapshot includes existing dirty work; a clean tree is not
required. Any add/remove/rename/change fails with both records. The gate never repairs, restores,
stages, or deletes. Temporary outputs are outside the manifest; tracked projections must remain equal.
CI also records commit identity from a clean checkout. No warning or environment bypass.
Tests are deterministic, bounded, offline by default, and never modify operator data or real package
state.
### Deferred verification directions
These directions are explicitly rejected for version 1 gates and revisited only through a
specification change.
- **Agent-driven acceptance QA:** deferred. Repository gates must stay deterministic and mechanical;
an agent report is advisory observation, never gate evidence or a semantic authority (TJ-GOV-12).
Human-readable agent reports may accompany a release only as unregistered side material.
- **Native Zig fuzzing:** the pinned toolchain provides fuzz instrumentation and a continuous search
mode. Deferred for version 1 gates because the deterministic seeded negative-space suites own v1
coverage; admission requires a capable platform lane with a bounded corpus and failure retention
under the evidence rules above.
- **Sanitizer runtimes:** thread-sanitizer and C undefined-behavior instrumentation exist in the
toolchain but are not gates on this host. They are admitted only through capable-platform evidence
with the same admission rules as any platform lane.