An in-toto predicate type

receipt/v1

A signed record of one run of a Velaris program: the budget it was given, every refusal and every declassification, the parameters it ran under, how it ended and how long it took - bound, by sha256, to the same source files a capability/v1 attestation names. The attestation is what the program may do; the receipt is what one run of it did.

Predicate type: https://gowrishankar-infra.github.io/velaris-lang/receipt/v1 - this page.
Schema: schema.json, JSON Schema draft 2020-12, for the predicate.
Definition: velaris-spec SPEC.md section 8.7, dedicated to the public domain under CC0.

{
  "_type": "https://in-toto.io/Statement/v1",
  "subject": [
    {"name": "examples/effects.vel",
     "digest": {"sha256": "37a7df8f595907f9e00f3e9be71ce1f00b584dbe70074dc37e8fad85e3cba5f7"}}
  ],
  "predicateType": "https://gowrishankar-infra.github.io/velaris-lang/receipt/v1",
  "predicate": {
    "schema": "velaris.receipt/1",
    "producer": {"name": "velaris-lang", "version": "8.1.0",
                 "uri": "https://github.com/gowrishankar-infra/velaris-lang"},
    "specification": "velaris-spec 0.10.0",
    "startedAt": "2026-09-14T00:00:00.000Z",
    "wall_time_ms": 41.7,
    "budget": "clock,fs:read:/work/report.txt,fs:write:/work/report.txt,io,rand",
    "run_parameters": {"seed": null, "freeze_time": null, "timeout": null,
                       "max_memory_mb": null, "max_read_bytes": 67108864,
                       "confinement": "none"},
    "effects_used": {"clock": 1, "rand": 1, "fs": 2, "io": 4},
    "refusals": [],
    "declassifications": [],
    "exit": {"status": 0, "outcome": "ok", "code": null},
    "complete": true
  }
}

Fields

Field	Meaning
`subject`	the program that ran, by the sha256 of its text, then each file it imported, by the sha256 of its bytes - the subjects `velaris attest` writes for the same files
`budget`	the budget the run was given, in the budget grammar
`run_parameters`	`seed`, `freeze_time`, `timeout`, `max_memory_mb`, `max_read_bytes`, and `confinement`: `none` when the budget was the only boundary
`effects_used`	each effect and how many operations of it the budget let through; null when the run was stopped from outside before it could say
`refusals`	each refusal as its code, its effect and its line, whether it stopped the run, and how many times - never the path, host or module the program named
`declassifications`	each declassification as the reason written in the program and its line, and how many times - never the value
`exit`	`status`, `outcome` (ok, refused, failed, did_not_compile, timeout, out_of_memory) and the `code` that ended it
`wall_time_ms`, `startedAt`	by the producer's clock
`complete`	false when the run was stopped from outside: what is listed happened, and a count is at least that

What it does not say

It holds no value the program handled, and nothing of its output, input or arguments. It does not hide what a program controls that is not a value: its exit status, which lines it reached and how long it ran are in it, and a program that has declassified a value can choose those. A declassification's reason is text its author wrote, and nothing checks it. A signed receipt says that its signer ran this producer on these bytes and saw this run; it is no stronger than the machine it was made on, and it says nothing about any other run.

A producer

velaris-lang writes receipts from 8.1:

velaris program.vel --allow io --receipt program.receipt.json
velaris.run(source, allow={"io"}).receipt
POST /run  {"source": "...", "allow": ["io"], "receipt": true}

It signs none; they are signed as an attestation is - cosign attest-blob --statement, or sigstore-python's sign_dsse - and cosign verify-blob-attestation --type https://gowrishankar-infra.github.io/velaris-lang/receipt/v1 checks one against the program's own bytes. Every release of velaris-lang carries one for an example program, signed by its release workflow and verified there.