# Ampoule run predicate, v1

Predicate type: `https://ampoule.dev/attestation/run/v1`

The URI is permanent: every signed receipt carries it. A breaking change to
the fields gets a new version (`/v2`), never an edit to this one.

An in-toto [Statement v1] with this predicate records one execution of
untrusted code inside a sealed Ampoule micro-VM: which kernel ran it, what
went in, what came out, and how much work it took. It is carried in a
[DSSE] envelope signed with Ed25519.

[Statement v1]: https://github.com/in-toto/attestation/blob/main/spec/v1/statement.md
[DSSE]: https://github.com/secure-systems-lab/dsse/blob/master/protocol.md

## Statement

```json
{
  "_type": "https://in-toto.io/Statement/v1",
  "subject": [{ "name": "output", "digest": { "sha256": "<output_sha256>" } }],
  "predicateType": "https://ampoule.dev/attestation/run/v1",
  "predicate": {
    "version": 1,
    "kernel_sha256": "e028af09…",
    "vmm": "firecracker",
    "runtime": "js",
    "flags": 260,
    "deterministic": true,
    "seed": 7,
    "payload_sha256": "bf75c921…",
    "output_sha256": "12cece5a…",
    "fuel": 14354058,
    "status": 0
  }
}
```

The subject is the output, the artifact the run produced. Its digest must
equal `predicate.output_sha256`; verifiers reject a statement where they differ.

## Predicate fields

| field | meaning |
|---|---|
| `version` | Receipt format version, `1`. |
| `kernel_sha256` | SHA-256 of the kernel ELF the VM booted. The language runtimes (QuickJS, CPython) are embedded in the kernel, so this pins them too. |
| `vmm` | `qemu` or `firecracker`. Informational: deterministic runs give the same output and fuel on both. |
| `runtime` | `rhai`, `wasm`, `js` or `python`. |
| `flags` | Request flags as sent in the mailbox (runtime bit, `0x100` = deterministic). |
| `deterministic` | Clock and randomness derived from `seed`, limits fuel-only. Only these runs can be re-executed to the same result. |
| `seed` | The seed used for clock and randomness. |
| `payload_sha256` | SHA-256 of the exact request bytes: the source for rhai/js/python; for wasm, `u32le module_len ‖ module ‖ input`. Computed by the guest and checked by the host. |
| `output_sha256` | SHA-256 of the exact output bytes, computed by the guest and checked by the host. |
| `fuel` | Work done: wasmi fuel consumed for wasm/js/python, Rhai operations counted by the engine for rhai. For deterministic runs, part of what replay must reproduce. |
| `status` | `0` success, `1` error raised by the code, `2` runtime unavailable, other values are limits or faults. A signed receipt with a nonzero status attests a failed run, not a successful one. |

## Envelope and signing

- `payloadType` is `application/vnd.in-toto+json`; the signature is Ed25519
  over the DSSE pre-authentication encoding
  `DSSEv1 <len(type)> <type> <len(body)> <body>`.
- `keyid` is the lowercase hex SHA-256 of the raw 32-byte public key.
- Ed25519 is deterministic: the same statement and key give byte-identical
  envelopes, so two deterministic runs can be compared as envelopes.
- The host only signs when it has re-hashed the payload and output and they
  match what the guest reported.

## What a signature does and does not prove

It proves that the holder of the key vouched for this run, and that nothing
in the statement changed afterwards. It does not prove that the key holder
was honest, or what hardware ran the VM. That is tamper evidence, not remote
attestation. For deterministic runs the signer does not need to be trusted at
all: anyone with the kernel image, the payload and the seed can re-execute and
compare output digest and fuel (`verify --replay`). Replay needs the exact
kernel named by `kernel_sha256`: receipts produced before Rhai fuel was
recorded (older kernel hash) only replay against their own kernel. Binding the signing key to
a measured kernel through a TEE is future work.

## Verifying

```
ampoule-verify envelope.json --key <pubkey-hex|file> [--output F] [--payload F] [--kernel F]
cargo run -p verify --release -- --replay envelope.json --key <pubkey> --js code.js
```

The public key is the trust anchor and must reach the verifier by some other
channel than the envelope. `ampoule-verify pubkey` prints the key a host signs with.