// SPDX-License-Identifier: CC-BY-SA-4.0
= K9 Receipt Schema (a2ml/k9-receipt)
:toc:
:icons: font

The evidence/receipt schema for a K9 SVC run. A *receipt* is the attested record
of what a `.k9` component did and was permitted to do. It is *canonical in A2ML*
(the `a2ml/k9-receipt` profile) with a *lossless JSON projection* for transport.

== Files

[cols="2,3",options="header"]
|===
| File | Role
| `PROFILE.a2ml` | The canonical schema — an `a2ml/k9-receipt` A2ML profile.
| `receipt.schema.json` | Lossless JSON projection (JSON Schema 2020-12).
| `example-receipt.a2ml` | A worked receipt in canonical A2ML form.
| `example-receipt.json` | The same receipt projected to JSON.
|===

== Why A2ML is canonical, JSON is a projection

The receipt is defined in A2ML so it inherits the *base record vocabulary*
(A2ML SPEC §7): the `component` record is hash-pinned and carries `provenance`
in exactly the same neutral shape as every other estate record, so a receipt
*cannot desync* from the artefact it describes. The JSON projection exists for
tooling that speaks JSON; it round-trips without loss — every field in one form
has a one-to-one counterpart in the other.

K9 is a *consumer* of A2ML here (dependency direction K9 → A2ML). A2ML core
ships only the neutral mechanism and base vocabulary and names no consumer.

== What a receipt records

[cols="2,4",options="header"]
|===
| Section (A2ML) / key (JSON) | Meaning
| `component` / `component` | Base record: identity, hash, provenance, timestamp, artefact_ref.
| `contract-result` / `contract_result` | Did the validation contracts pass, and which files.
| `leash` / `leash` | Requested vs enforced leash level, downgrade flag, and any unmet Hunt preconditions.
| `capabilities` / `capabilities` | Granted / requested / denied capability names (default-deny).
| `signatures` / `signatures` | Which signatures were checked and whether all were valid.
| `dry-run` / `dry_run` | Whether a dry-run plan was produced and reviewed, and the plan.
| `deploy-result` / `deploy_result` | Whether deploy was attempted and succeeded.
| `rollback-result` / `rollback_result` | Whether rollback was attempted and succeeded.
| `policy-decision` / `policy_decision` | The allow/deny policy decision and its reason.
| `failure` / `failure` (optional) | Present only for a refused or failed run: reason + stage.
|===

== Leash + capability semantics in a receipt

The `leash` block reflects `authorize_hunt` (`../leash.ncl`): a receipt shows
`enforced_level = "Hunt"` only when *all five* Hunt preconditions held
(signature, policy, sandbox, dry_run, capability_grant — owner directive,
all five always). Otherwise the receipt records `downgraded: true`, the
`enforced_level` it fell back to, and the exact `unmet_preconditions`.

The `capabilities` block reflects the default-deny model (`../capabilities.ncl`):
`granted` is the explicit pedigree grant, `requested` is what the run asked for,
and `denied` is `requested \ granted` (empty on success).

== Validating

[source,sh]
----
# JSON projection:
jq empty receipt.schema.json example-receipt.json
# (and validate example-receipt.json against receipt.schema.json with any
#  JSON-Schema 2020-12 validator)

# A2ML canonical form: validate under its declared profile
a2ml validate --profile a2ml/k9-receipt example-receipt.a2ml
----

== Naming hazard

K9's execution triad is *must / just / nickel*. Do not confuse it with the
contractiles family *must / trust / dust / intend* — a different estate concept.
`must` appears in both and means different things.
