Specification · Section 2 of 13

The language, by worked example

Walks the pseudo-language through a full IT-consulting ramavtal, then covers what a receipt looks like, the envelope/body grammar, and the three binding tiers of contract language.

Illustrative strawman (syntax will be forged against the corpus - this extends that example with ports, receipts, idempotency). An IT-consultant ramavtal:

mechanical-contract v0
id:      mk-se-2027-000042
title:   Ramavtal IT-konsulttjänster
prose:   ramavtal-2027-0042.pdf  sha256:9f2c44...        # Ricardian binding:
annex:   [ "§14 Force majeure", "§16 Sekretess" ]        # prose-only clauses, hashed,
                                                         # visible but not executable

parties:
  buyer:
    org:  212000-1355  "Lunds kommun"
    sign: eIDAS-qualified-seal | freja-orgid
  supplier:
    org:  556677-8899  "Konsultbolaget AB"
    sign: eIDAS-qualified-seal

validity:
  from 2027-01-01 to 2029-12-31
  extend: 2 x 12mo, notice 6mo, mode: active-renewal     # negative option: impossible

money:
  currency SEK
  vat 25% on services
  rounding per-line half-up 0.01

# ── DECLARED STATE ─────────────────────────────────────────────
state:
  pool hours.senior   capacity 3000 h
  pool hours.junior   capacity 2000 h
  pool budget.total   capacity 8_000_000 SEK             # takvolym: hard ceiling
  register deliveries                                    # accepted, not yet invoiced
  register invoices                                      # accepted, not yet paid

# ── EXTERNAL FACTS (signed fixings, never lookups) ─────────────
fixings:
  index aki   series SCB.AKI.J62  base 2026-09  signed-by scb-ingest  revise yearly 01-01

# ── ARTIFACTS: tables & variables by reference ─────────────────
artifacts:
  rate-table    art:kb-it-rates-2027      pin v2  sha256:d4e1...
                update: proposed-by supplier, approved-by buyer,
                        at-most 1 per year, window January,
                        bounds within index-clause cap          # an illegal update
                                                                # cannot become v3
  calendar      art:se-working-days        track latest          sha256:88a0...
  attest-table  art:lund-attestordning     track latest-approved # buyer-maintained

rates: from rate-table                     # variables resolve against the pinned
  senior  895 SEK/h  indexed-by aki  cap 4%/yr    # version at each event's
  junior  645 SEK/h  indexed-by aki  cap 4%/yr    # effective date

# ── PORTS: the capability manifest ─────────────────────────────
ports:
  in  allocation.request   from buyer     payload peppol.order              # avrop
  in  timesheet.submit     from supplier  payload sfti.timesheet            # people
  in  invoice.submit       from supplier  payload peppol.bis-billing-3     # invoicing IN: allowed
  in  payment.confirm      from buyer     payload iso20022.pain.002
  in  approval.grant       from buyer.attestant  payload signed-decision
  in  notice.send          from both      payload signed-text
  out receipt.emit         to submitter   always                            # proof of execution
  out notice.emit          to both        on rule-alerts
  out payment.instruct     CLOSED         # referee mode: machine never moves money
  out invoice.issue        CLOSED         # invoicing OUT: not part of this contract
  # material.delivery, rental.claim: NO PORT DECLARED -> materially and
  # legally not allowed under this contract. Absence is prohibition.

# ── CADENCE: rate limits, in contract terms ────────────────────
cadence:
  invoice.submit      at-most 1 per month per supplier     # faktureringsintervall
  invoice.submit      not-before matching delivery         # no advance billing
  payment.confirm     due within 30 days of invoice accept # betalningsvillkor;
                                                           # late -> obligation breach, dröjsmålsränta claimable
  allocation.request  at-most 20 per day per unit          # anti-splitting guard

# ── APPROVAL: straight-through vs someone-in-the-loop ──────────
approval:
  invoice.submit:
    if total <= 50_000 SEK   -> straight-through               # STP leg: no approval, immediate
    if total <= 1_000_000    -> require 1 of buyer.attestant
    otherwise                -> require 2 of buyer.attestant   # four-eyes / tvåhandsprincipen
  approver buyer.attestant means:
    human  eIDAS-signature (attestordning ref: reglemente 2026-11)
    | agent signing-key k-ai-01 bound-to policy sha256:ab12...  # AI approval = a keypair
                                                                # + a HASHED, versioned policy
  timeout: approval pending > 10 working-days -> escalate level 1

# ── ESCALATION: throw / catch / finally, for contracts ─────────
escalation:
  on pool-exhausted | rejected(3 times, 30d) | obligation-breached | approval-timeout:
    level 1  notify avtalsansvariga both parties        resolve-within 10 working-days
    level 2  suspend port invoice.submit                steering-group, 20 working-days
    level 3  formal dispute: mediation per prose §15    draws frozen, receipts keep flowing
    level 4  termination path opens per prose §17
  finally:                                # the survival clauses - run on ANY exit
    sekretess per §16                     lives 5y past termination
    garantiåtagande                       24mo per delivery
    return-of-materials                   within 30d

# ── RULES: if / which, nothing else ────────────────────────────
rule on allocation.request:
  if payload.role not in rates            -> reject "role not on rate card"
  which payload.role is
    senior: if pool hours.senior remaining < payload.hours -> reject "senior pool exhausted"
    junior: if pool hours.junior remaining < payload.hours -> reject "junior pool exhausted"
  reserve pool hours.[payload.role] amount payload.hours for payload.unit
  accept

rule on timesheet.submit:
  if no reservation matches payload.allocation-ref        -> reject "no call-off behind hours"
  if payload.hours > reservation.remaining                -> reject "exceeds call-off"
  record deliveries { role: payload.role, hours: payload.hours, period: payload.period }
  accept

rule on invoice.submit:                    # payload = EN 16931 invoice
  if payload.BT-13 not references this.id  -> reject "no contract reference"     # BT-13: order ref
  each line in payload.lines:              # bounded map over payload - only iteration allowed
    which line.item is
      hours.senior: expected := rates.senior at line.period      # index math runs here
      hours.junior: expected := rates.junior at line.period
      otherwise:    reject "line item not in contract"
    if line.BT-146 != expected             -> reject diff {      # BT-146: item net price
         billed: line.BT-146, contractual: expected,
         clause: rates + index aki, excess: (line.BT-146 - expected) * line.qty }
    if line.qty > deliveries unbilled for line.item -> reject "no delivery behind quantity"
  if invoice.total + pool budget.total consumed > pool budget.total capacity
                                           -> reject "takvolym breach"
  draw pools; record invoices; accept      # -> then the approval gate decides the leg:
                                           #    straight-through, or waits for approval.grant

rule on payment.confirm:
  if payload.ref not in invoices           -> reject "unknown invoice"
  mark invoices[payload.ref] paid
  accept

# ── ALERTS: assertions, not dashboard config ───────────────────
alerts:
  when pool hours.senior consumed > 80%          notify both "senior pool at {level}%"
  when today in notice-window(validity.extend)   notify buyer "extension decision due"
  when fixing aki stale > 13mo                   notify operator "index feed silent"

# ── EXECUTION CONTRACT (the machine's promises) ────────────────
execution:
  idempotency:  every submission carries submission-id (uuid v7);
                duplicate id -> return original receipt, state unchanged
  ordering:     events sequenced per contract; receipt N embeds hash(receipt N-1)
  receipts:     signed by platform seal; delivered over Peppol MLR-style response
  replay:       state is a pure fold over the receipt chain; any party can verify
  determinism:  no clock, no I/O, no floats, no unbounded loops -> lint-provable

What a receipt looks like (proof of execution)

An earlier draft drew the receipt flat, transport machinery and judgment mixed in one bag. Structured properly, every receipt is a universal envelope around a typed body:

{
  "envelope": {                                  // mk-envelope v1: the SAME fields for
    "artifact":      "mk/receipt",               // every receipt, every port, every profile
    "body-type":     "invoice.submit/verdict v1",
    "receipt":       "r-000217",
    "contract":      "mk-se-2027-000042 @ v3 (hash 9f2c44...)",
    "port":          "invoice.submit",
    "submission-id": "0197f2aa-...-7cde",
    "payload-hash":  "sha256:77ab01...",
    "prev-receipt":  "sha256:c41d90...",
    "state-before":  "sha256:5e12fa...",
    "state-after":   "sha256:5e12fa...",         // unchanged: rejected
    "verdict":       "REJECTED",                 // closed enum - lives HERE; the
    "body-hash":     "sha256:e0a1b2...",         // reasoning lives in the body (below)
    "at":            "2028-04-03T09:14:22Z"
  },
  "body": {                                      // schema: invoice.submit/verdict v1
    "rule-trace": [
      "invoice.submit: BT-13 ok",
      "line 3: which item -> hours.senior",
      "line 3: expected = 895 × aki(2028-03)/aki(2026-09) = 931.70",
      "line 3: BT-146 = 950.00 ≠ 931.70 -> REJECT",
      "diff: excess 18.30/h × 140h = 2,562.00 SEK, clause: rates.senior + index aki"
    ]
  },
  "seal": "JAdES platform seal over the envelope (RFC 3161 timestamp); the body is
           bound through body-hash - detachable without breaking chain or signature"
}

The rejection cites the clause, shows the arithmetic, and is signed. A dispute about this invoice is now a conversation about an 8-line receipt, not about a 40-page PDF. And because the supplier can run the same contract file BEFORE sending (pre-validation - the two-sided pull), the honest supplier never sends that invoice at all.

Envelope and body: one grammar for every message

The split is not an aesthetic choice - the stack this design rides has been enveloped at every layer for forty years, and we mirror the pattern one level up (the same move as MLR -> judgment receipt):

Layer	Envelope	Body
EDIFACT (1987)	UNB/UNH interchange + message headers	the INVOIC segments
Peppol transport	AS4/ebMS3 messaging envelope	payload
Peppol business	Business Message Envelope (SBDH) v2.0.1: sender, receiver, document type, instance id	the UBL invoice itself
ISO 20022	Business Application Header (head.001)	the pain/camt Document
Modern web	JOSE protected header · CloudEvents attributes	payload / data
W3C VC 2.0	literally called “enveloping proofs” (VC-JOSE-COSE)	the credential claims

A Peppol access point routes on the SBDH without ever parsing the invoice inside it. The mk grammar wants exactly that property, so:

The envelope is mk-core’s, frozen and universal. Identity (contract @ version hash, port), correlation (submission-id, payload-hash), sequence (prev-receipt, state hashes), the verdict enum, the body hash, the timestamp, the seal. Chain verifiers, archives, auditors, and dashboards process envelopes without understanding a single body schema - integrity is checkable by software that knows nothing about invoicing.
The body is typed per port, versioned, profile-constrained. invoice.submit/verdict v1 is a different schema from allocation.request/verdict v1; the envelope’s body-type declares which schema the body must be held against - “the body must also adhere to some schema”, literally. Bodies evolve by versioning; profiles constrain them, CIUS-style (§6); the envelope never changes.
The verdict sits in the envelope; the judgment sits in the body. The verdict is a closed enum - ACCEPTED / REJECTED / PENDING / ESCALATED / FAULTED (PENDING generalized per §7.5; FAULTED = never judged on the merits, §4.3) - universal machine semantics, the same five words for an invoice as for a timesheet. The rule trace (the arithmetic, the clause citations, the rate card) is port-specific judgment - and is exactly where the OSL 31:16-sealed material lives (§12: hourly and unit prices).
Which makes redaction fall out of the grammar. Detach the body, keep the envelope: the receipt still chains (prev-receipt and state hashes intact), still verifies (the seal covers the envelope; the body binds via body-hash), and still answers “invoice r-000217: REJECTED”. §12’s scoped receipts stop being custom machinery - a disclosure scope is just who gets bodies: parties get both, a steering group gets envelopes + digests, the public allmän-handling view gets envelopes. Salted per-field hashing inside the body (SD-JWT style) is the v2 refinement, on the same boundary.
Everything on the wire wears the same envelope. Submissions arrive enveloped (their SBDH maps onto mk-envelope fields), receipts leave enveloped, artifact versions publish enveloped (§5.6’s who-signs table IS an envelope spec), and the contract itself is one - §2’s header block (id, parties, validity, prose hash, seals) is the envelope; state, ports, and rules are the body. One grammar, four artifact classes, zero special cases.

Three tiers of language: executable, soft, comment

Soft contract language is something else - the worked example’s annex: line was this idea in embryo; promoted properly, every piece of language in a mechanical contract sits in exactly one of three tiers:

Tier	What it is	Binding status
Executable term	rules, ports, pools, cadences, imports	signed AND machine-enforced; carries `implements: ["§7.2"]` backlinks to the prose clauses it operationalizes
Soft term (prose-term)	force majeure, sekretess, lojalitetsplikt, “skäligt”/“väsentligt” clauses - legally operative language no machine should pretend to run	first-class and hashed: clause id + verbatim text inside the signed Ricardian bundle, visible in every rendering, prose governs on conflict (§10). NOT a comment - it binds the parties, just not the machine
Comment	annotations, rationale, examples	non-operative, hashed with the document but explicitly binding nobody

The tier split makes coverage a computable, honest number: every clause of the source prose is implemented (linked executable terms), soft-carried (prose-term, deliberately non-executable), or unhandled (a translation gap that must be resolved before signing - the linter refuses genesis with unhandled clauses, same spirit as §7.6’s strict linking). Translation in both directions is then well-defined: prose → mk is tier-assignment + rule authoring + clause linking (with the coverage report as the deliverable that keeps the translator honest), and mk → prose is a deterministic projection - Catala’s literate lesson pointed backwards: render each executable term as readable contract language beside its formal block, soft terms verbatim, the port manifest as a capability table. Both directions are running experiments in the reference implementation’s translation and rendering legs.

Findings from the prose-to-mk translation experiment - a 19-clause Swedish ramavtal translated end-to-end: 63% implemented / 32% soft / 1 comment / 0 unhandled, and 18 of 19 clauses tiered cleanly. Two creaks, both spec-relevant for v-next: (1) clauses are not tier-pure - real legal clauses mix an executable spine with soft connective tissue (a tvistlösning clause carries both the eskaleringstrappa AND lagval/“skälig tid” prose), so the tier must eventually attach at sub-clause granularity, not whole clauses; (2) “implemented” is binary but fidelity is not - an index formula translates airtight while “får inte delas upp i syfte att kringgå attest” is enforced only by a structural proxy (the anti-splitting cadence guard); coverage needs a fidelity dimension (faithful / proxy / partial) alongside the tier, or proxies masquerade as full captures.

Findings from the rendering experiment - the reverse projection works and found its own structural truth: the clause↔term relationship is many-to-many (one rates block implements §6 AND §7; one §10 spawns a port, two cadences, and a rule), so Catala-style physical adjacency is impossible without duplicating terms. The renderer’s answer, adopted into the design: two cross-linked spines - the Avtalstext (every clause once, in order, tier-tagged, citing the machine terms that enforce it) and the machine terms (every node once, as tables, citing back to their clauses) - “beside” achieved by bidirectional reference, not layout, which keeps the completeness invariant (every clause and every node rendered exactly once, machine-checked) provable. The projection opens by declaring itself: maskinell projektion; vid motstridighet gäller prosan.