# IHVRK verification instructions

## 1. Evidence-only check (no source needed)
`python3 verify_ihvrk_evidence.py` in the evidence folder. See EXPECTED_RESULTS.md.

Manual spot checks:
* `sha256sum <file>` against `MANIFEST.json → files`.
* `z3_proofs.json`: every row `observed: UNSAT`, `sensitivity_observed: SAT`, with a non-empty counterexample.
* `tlc/design.txt`: ends with "Model checking completed. No error has been found." and the state count.
* `tlc/no_auth_check.txt` etc.: contain "is violated" plus a counterexample trace. A checker that never finds
  anything would not produce these.

## 2. Re-running from source (needs the repository at MANIFEST.source_commit)
```bash
git checkout <source_commit>
python3 -m venv v && . v/bin/activate && pip install -r ihvrk/requirements.lock
python3 -m pytest -q -p no:cacheprovider ihvrk/tests        # expect 0 failed; runtime tests skip without root
python3 -m ihvrk.solver.ihvrk_solver                        # exit 0
ihvrk/formal/run_tlc.sh                                     # Java + tla2tools.jar; ~25 min for the design run
python3 ihvrk/scripts/mutation_test.py                      # expect 30/30
python3 ihvrk/scripts/generate_evidence.py                  # regenerates evidence/; compare with the published copy
```
Runtime tests (`ihvrk/tests/runtime`) need root, cgroup v2 and systemd-run. They create and remove their own
`ihvrk-test-*.scope` units and freeze nothing else. Run them on a disposable VM, not on a production host.

## 3. Shared dependencies (independence is limited)
The implementation, the tests, the formal models and the stand-alone verifier were written by the same author in
the same session. The verifier shares no code with the implementation, but it shares the specification.
Fixture keys are generated per run (SOFTWARE_TEST). There is no shared infrastructure with the live CAIN services.