Never do implementation work in the main worktree at /home/holmes/poc-7.
Before editing code, running task validation, or committing, create or switch to
a dedicated git worktree for the task.
When creating instructions for an assistant in this repo:
- Include explicit Success Criteria (SCs).
- Include explicit tests/checks that prove each SC is satisfied.
- Include end-to-end validation checks showing all delivered functionality works as expected, not only SC-specific checks.
Prefer CLI end-to-end tests for new user-visible or runtime behavior. When a test needs data that is not available through the CLI/RPC surface, add a first-class daemon/CLI observability or query surface instead of reaching into internal SQL tables from the test.
When changing repo command-entry files, projector registration/families, runtime/state decision seams, or Verus proof modules:
- Success Criteria:
- Every changed or new
src/**/commands.rsandsrc/**/commands_api.rsfile is indexed indocs/planning/COMMAND_FORMAL_COVERAGE.mdwith a Verus mirror and concrete targeted checks. - Every changed or new runtime/state decision seam remains indexed in
docs/planning/FORMAL_SEAM_COVERAGE.md. - Every new non-module file under
verus-proofs/src/is indexed indocs/planning/FORMAL_SEAM_COVERAGE.md. - Every changed covered runtime command/seam/projector path also changes at least one mapped Verus mirror in the same diff.
- Registered projector families remain assigned to Verus-covered projector proof modules, and their TLA/runtime mapping rows stay current.
- Every changed or new
- Required checks:
- Run
scripts/run_merge_readiness_checks.sh targeted. This is the primary agent/merge-readiness gate and must pass before merge. - Run
python3 scripts/check_formal_seam_coverage.pyafter seam/proof-map edits. - Run
python3 scripts/check_command_formal_coverage.pyafter command/projector coverage edits. - Run
python3 scripts/check_formal_mirror_updates.pyafter touching any covered runtime command/seam/projector path. - Run
python3 scripts/check_projector_tla_conformance.pyandpython3 scripts/check_projector_tla_bijection.pywhen projector mapping rows change.
- Run
- End-to-end validation:
- Each changed command or projector path must keep at least one executable pass case and one executable reject/conflict/break case.
When changing event schemas, signer-family rules, dependency checks, projector
guards, docs/tla/runtime_check_catalog.md, or
docs/tla/projector_conformance_matrix.md:
- Success Criteria:
- The runtime change has an executable pass case and an executable break case.
- The affected TLA/runtime check mapping is updated in the catalog or matrix in the same change.
- No TLA/runtime check may be claimed in repo instructions or docs without a concrete code path or executable test covering it.
- Required checks:
- Run targeted Rust tests that exercise the changed validation path.
- Run
python3 scripts/check_projector_tla_conformance.pyandpython3 scripts/check_projector_tla_bijection.pywhen you update the touched mapping rows and expect those rows to stay current.
- End-to-end validation:
- At least one projection-path test must prove the changed event is accepted on the valid path and rejected or blocked on the invalid path.