House sale, financed

The brutal everyday contract. A person buys a house with a mortgage. Six parties, money held by a neutral third party, two conditions that can unwind the whole thing, a completion day where three separate contracts must settle together or not at all, title that passes only on full payment, and a registration authority at the end. It is the best single illustration of how a mechanical contract integrates with the world - because it needs both integration mechanisms at once, and the contrast between them is the whole lesson.

The two ways a contract meets the world

A mechanical contract pulls in outside things two ways, and this deal uses both:

• Flatten a module (§7.7). The statutory ground (Jordabalken, the estate-agent law) and the deposit mechanic are modules - governed fragments you use and the machine flattens into the signed contract before signing. You author or vet them; they become your bytes. law/se/jordabalken, law/se/fastighetsmaklarlagen, std/se/handpenning-escrow.
• Reference a remote contract (§7.1/§7.2). The buyer’s bank, the seller’s bank and Lantmäteriet each run their own mechanical contract, on their own machines. You do not embed them and you never see their rules. You reference them by pinned hash, interact only through their visible ports and standard payloads, and trust their signed receipts - not a live call. Pinned, binding, never wired.

The rule that falls out: flatten what you own; reference what someone else runs. A statutory clause is yours to carry. A bank’s loan is the bank’s to run - you just need its promise to be binding and its receipt to be verifiable.

The cast

Party	How it appears	Role
Seller / Buyer	signatories to the köpekontrakt	sign, pay, transfer title
Estate agent (mäklare)	party + escrow holder	neutral intermediary; holds the deposit on a client account it can never own
Buyer’s bank	remote contract	issues the lånelöfte (a standing, conditional commitment), then disburses the loan at completion
Seller’s bank	remote contract	receives payoff of the old mortgage, releases the old pantbrev
Lantmäteriet	remote authority	grants lagfart (title registration) - a receipted external act
(inspector)	appointed slot	optional; a report a condition guards on

The lånelöfte, as a remote reference

Before the bidding, the buyer gets a lånelöfte - the bank’s standing promise to lend up to an amount, valid for a window, subject to the specific property. In mk, that promise is not copied into the purchase contract. It is the bank’s own contract, and the purchase references it:

ports:
  in  lanelofte.valid    from contract se-storbank/lanelofte-2027-4471   # bank's OWN
                        port commitment.confirm                          #   contract,
                        pinned sha256:7b1e9c...                          #   on its machine
                        payload: iso20022.loan-commitment                # visible payload
                        trust: publisher-seal                            # signed receipt,
                                                                         #   never an RPC

Three things make that binding without wiring: the pin is a signed term (the deal only accepts this exact bank contract, at this version); the bank co-declares the port in its own document; and trust is the signed receipt, verified offline. The financing condition then simply guards on it - lanelofte.valid.amount >= price - handpenning - buyer-equity - and if the bank’s commitment does not cover the gap, the deal never arms.

The deal, step by step

1. Köpekontrakt signed (genesis) - formkrav met (JB 4:1).
2. Handpenning (10%) paid into the agent’s client account - the std/se/handpenning-escrow module, held by a party that owns neither side of it.
3. Conditions run: the financing condition (does the lånelöfte cover?) and the inspection condition. Either can fail, and on failure the escrow refunds the buyer and the deal unwinds. No condition failing -> the escrow releases to the seller.
4. Tillträde (completion) is a saga across three contracts (§7.3): an all-of join waits for loan.disbursed (buyer’s bank), payoff.confirmed and pantbrev.released (seller’s bank). Only when all three land does title move (seller -> buyer, on the köpebrev, at full payment - retention of title, §8.3) and the köpebrev issue. If a downstream leg faults, the compensation reverses it.
5. Likvidavräkning - the price splits, conservation-checked: agent commission + payoff of the seller’s old loan + net to the seller. Every krona traces.
6. Lagfart - the buyer applies to Lantmäteriet (a remote authority contract); the registration is a receipted external decision. Ownership already passed on the köpebrev; lagfart records it.

What this example stresses

• Escrow held by a neutral third party - the deposit moves only to buyer or seller, never to the holder. Borrow-style ownership (§8.3): hold without own.
• A deal that can unwind - conditions precedent with a refund path, not a fixed-forward obligation.
• Atomic settlement across sovereign contracts - three contracts on three machines must settle together; a saga, not distributed ACID.
• Retention of title - moves title ... on kopebrev.issue is äganderättsförbehåll, executable.
• A registration authority whose act is constitutive of the record but not of ownership - a timing distinction the model has to state precisely.
• Both integrations side by side - the clearest demonstration of flatten-vs-reference in the whole corpus.

The contract, in mk

# § 1 Parties and property (köpekontrakt, JB 4:1 formkrav)
parties:
  seller   person: "Anders Ek"   sign: eIDAS-QES
  buyer    person: "Bea Lund"    sign: eIDAS-QES
  agent    org: "Nyckel Fastigheter AB"  role: appointed+executor  sign: eIDAS-seal

use module:law/se/jordabalken@v1              # FLATTENED law mirrors + the deposit
use module:law/se/fastighetsmaklarlagen@v1    #   mechanic - authored/vetted, so
use module:std/se/handpenning-escrow@v1       #   they become the signed bytes
  with: { amount: handpenning, stakeholder: party:agent,
          payer: party:buyer, payee: party:seller,
          release-on: conditions.cleared, refund-on: condition.failed }

# § 3/§ 5 Banks + registry as REMOTE contracts - pinned, binding, never wired
ports:
  in  lanelofte.valid   from contract se-storbank/lanelofte-2027-4471  port commitment.confirm  pinned sha256:7b1e9c...
  in  loan.disbursed    from contract se-storbank/lanelofte-2027-4471  port disbursement.pay    pinned sha256:7b1e9c...  payload: iso20022.pacs.008
  in  payoff.confirmed  from contract se-annanbank/inteckning-2019-8830 port payoff.settle       pinned sha256:c40a11...
  in  pantbrev.released from contract se-annanbank/inteckning-2019-8830 port pantbrev.release    pinned sha256:c40a11...
  out lagfart.ansokan   to contract se-lantmateriet/inskrivning        port lagfart.apply       pinned sha256:9f77e2...

# A condition is composed, not a keyword: a register written by `record`, read by `check`
rule on lanelofte.valid:
  check lanelofte.valid.amount >= price - handpenning - buyer-equity  else reject "..."
  record conditions.financing = cleared          # §8.1 register write; status = fold

# § 5 Tillträde: an all-of JOIN (§3.7) across three sovereign contracts + a §7.3 saga
rule on tilltrade   join all-of [ loan.disbursed, payoff.confirmed, pantbrev.released ]:
  check conditions.financing == cleared and conditions.inspection == cleared   # the gate:
                                           else reject "villkor ej uppfyllda"   #  read the latch
  check loan.disbursed.amount + handpenning + buyer-equity == price
                                           else reject "likviden stämmer inte"
  moves title fastighet  seller -> buyer   when kopebrev.issue    # §8.3 (retention of title)
  emit kopebrev.issue
  accept
  compensate:                                    # §7.3 saga = REAL reversing effects, not magic:
    move money.slutlikvid disbursed -> party:buyer
    emit kopebrev.rescind to: {seller, buyer}
    within 1 day

Every construct maps to a defined primitive: check, record, move, moves title ... when (§8.3), the all-of join (§3.7), split (§6, marketplace example), the compensate saga leg (§7.3). There is no condition, unwind, or return-everything verb - a condition is a register + record + check, and “return everything” is an explicit move back. That composition is itself named as a module (std/se/villkor), the same way a function names a composition of smaller operations - the compose-upward discipline, without a runtime.

This example is illustrative: the surface syntax shown here is a strawman: the parser and engine that would run it are the reference implementation’s later work, currently behind the specification on money movement, joins, and modules.