# IHVRK assurance case

## Claim

Within the **declared scope** below, a protected operation run through `ExecutionGate` starts at most once, and only
after an enrolled, active, independent human verifier has signed an approval of that exact action (or two distinct
break-glass operators have signed grants for it), the authorization policy and its Z3 encoding agree on AUTHORIZE,
and the decision is recorded in a hash-chained ledger.

**Declared scope:** a single service node; registry and ledger on local storage; software-held service keys; trusted
service clock with declared uncertainty; the protected operation reachable only through the gate. **Out of scope:**
the live CAIN gateway, MCPGate and the three public sites (IHVRK is not integrated there), multi-node deployment, and
kernel-level enforcement.

## Argument

1. **Identity.** Only keys in enrollment records signed by a pinned enrollment authority can approve. Agent ids and
   agent keys cannot be enrolled, and a verifier cannot approve a request made under its own id. A kid never changes
   key. Revocation is versioned and monotone, and a stale list blocks. *(I2, I3, I4, I14; A1–A12, E1, E7)*
2. **Cryptographic provenance.** Every signed structure is canonical JSON with a domain separator, and `alg`/`kid`
   are inside the signature. Only pure Ed25519 is accepted. Unknown fields, floats, duplicate keys and alternative
   encodings are rejected. *(signature and canonical unit suites; B3, H5–H7)*
3. **Action binding.** The approval names the action digest, resource, tenant, agent, scope, epoch, policy version
   and challenge id, and each is compared with the stored request. The gate recomputes the digest of the action it
   is about to run. *(I7, I8, I9; C2–C4, D2, D10, D11)*
4. **Policy evaluation.** Two independently written encodings must agree. Z3 shows that no state violating I2–I10 or
   I12–I14 is authorized, and that each proof depends on its guard. Timeouts, UNKNOWN, exceptions and disagreement
   block. *(z3_proofs.json; differential property test; H1–H9)*
5. **Permit consumption.** A single SQLite transaction moves the permit ISSUED→CONSUMED and the request
   →EXECUTING. Thread and process races yield exactly one start. *(I1, I11, I15; D1, D3, I9; TLA+ NoDoubleExecution)*
6. **Liveness without permission.** Every request reaches a terminal state under fairness of the service and the
   clock only, even if no human ever answers. *(TLA+ EventuallyResolved; expire/reconcile tests)*
7. **Runtime containment** (supporting, not load-bearing for the claim). The agent cgroup can be frozen while
   pending; an enforcer crash leaves it frozen. *(F1–F12)*
8. **Evidence integrity.** Modification, deletion, reordering, duplication, replayed approvals, unexplained
   permits, incomplete executions and clock regressions are detected by the chain. Rewrite and truncation are
   detected only against an off-host signed checkpoint. *(G1–G14)*

## Evidence

All under `ihvrk/evidence/`, listed with sha256 in `MANIFEST.json`, which also records the source commit:
`test_results.json`, `z3_proofs.json`, `tlc_summary.json` + `tlc/*.txt`, `mutation.json`, `benchmark.json`,
`ebpf_verifier_load.txt`, `sample_ledger/`. Stand-alone check: `verify_ihvrk_evidence.py` (standard library only).

## Assumptions

| ID | Assumption |
|---|---|
| A-TCB | The service host (OS, Python, SQLite, `cryptography`, Z3) is not compromised. |
| A-KEYS | Enrollment-authority and break-glass operator keys are held off the service host; verifier keys stay on verifier devices. |
| A-TIME | The service clock is correct within its declared uncertainty. |
| A-STORE | The registry file lives on one host's local filesystem with working locks and fsync. |
| A-PATH | The protected operation is reachable only through `ExecutionGate.execute`. |
| A-ENROLL | The enrollment authority proofs verifier identities before signing enrollments. |
| A-CKPT | Checkpoints are exported off-host regularly. |
| A-KERNEL | For runtime containment: cgroup v2, root-run gatekeeper, agent confined to its cgroup. |

## Limitations

See `LIMITATIONS.md` (L-INTEG, L-STORE, L-HSM, L-RT-LSM, L-HUMAN, L-LEDGER and others). The claim says nothing about
whether the person behind a verifier key understood the action.

## Release gates (`release_gate.json`)

| Gate | Condition that blocks | Result |
|---|---|---|
| G1 | a forbidden execution state is reachable in a required formal model | PASS (Z3 15/15; TLC design no error) |
| G2 | a required safety invariant fails | PASS |
| G3 | a critical authorization or replay test fails | PASS (296/296) |
| G4 | an invalid approval yields a permit | PASS (class A, B, E tests) |
| G5 | an unresolved solver result grants permission | PASS (I10, H1–H9) |
| G6 | a protected action runs without a valid action-bound permit | PASS within scope (A-PATH) |
| G7 | a critical ledger-integrity test fails | PASS (G1–G14) |
| G8 | a required runtime enforcement control is missing | **BLOCKED**: eBPF LSM cannot attach on this host (L-RT-LSM); the user-space daemon is not written |
| G9 | a known critical defect lacks a disposition | PASS (F-001..F-005 fixed) |
| G10 | release artifacts cannot be linked to the tested source revision | PASS (MANIFEST.source_commit) |
| G11 | required evidence missing or unverifiable | PASS (stand-alone verifier) |
| G12 | deployment violates a mandatory trust assumption | **BLOCKED for production**: L-INTEG (not wired into the live path), L-HSM (software keys) |

## Verdict

**RELEASE_GATE_BLOCKED** for the full IHVRK scope the prompt describes (kernel enforcement and production
integration are missing).

For the narrower **library + reference gate** scope declared above, all applicable gates pass, with open
findings (L-DOS) and no independent review: **RELEASE_CANDIDATE_WITH_OPEN_FINDINGS**. That is not a
production-readiness statement.