Worked examples · 03 of 07
Cabin rental
A one-person company rents out a cabin by the week, handling bookings, a returnable deposit, a damage-claim window, and cancellation refunds.
- SIZE
- small
- PROFILE
- mk-se-b2c / b2b
- STRESSES
- Time-sliced occupancy (the keyed-pool gap), deposit-as-escrow with a claim window, cancellation ladders as which-over-event-math, and disputed human judgment parking money in escrow.
The §6.2 two-person-AB test, played straight: a one-man AB rents out a sommarstuga by the week. No lawyer, no procurement department - a template, a booking, a deposit that must come back unless something broke. It looks trivial and it immediately breaks something: the pool model cannot say “booked for week 29”. That fracture is this example’s reason to exist.
Profile: mk-se-b2c (same gap as example 01) or mk-se-b2b for company retreats - the mechanics are identical.
The fracture, first
§8.5 models a specific cabin as a named pool: pool unit:cabin capacity 1. Draw it, it’s gone. But a rental is not consumed - it is occupied for a date range, and two bookings for different weeks must both succeed while two for the same week must not. Capacity-1 says nothing about time; the double-booking question is an interval overlap question, and the current pool flavors cannot ask it.
Proposed primitive: the keyed pool - a pool family indexed by a key from a closed domain, each cell an independent capacity pool:
pool cabin.nights keyed-by date within validity capacity 1 each
A booking draws the cells 2027-07-12 .. 2027-07-19; overlap = one of those cells already drawn = the §3.1 boundedness question, per cell. Nothing new mathematically - coloured Petri nets (Jensen, 1981) are exactly this: tokens carrying values, places indexed by data. §6.3’s coupon register (“each code a capacity-1 pool”) was secretly the same shape - a pool keyed by code. Hotel/GDS inventory has run per-date availability cells for fifty years. The primitive is corpus-demanded (rentals, venues, vehicles, staff scheduling, berth allocation), lint-friendly (finite key domain within validity), and it collapses the named-pool flavor into keyed-by identity.
The contract
mechanical-contract v0
id: mk-se-2027-cabin-0007
template: tpl-stugavtal @ v1
parties:
landlord: org 559234-5678 "Stugbolaget AB" sign eIDAS-seal
guest: party<consumer> ref booking-payment # example 01 identity questions apply
money: currency SEK rounding total half-up 1.00
state:
pool cabin.nights keyed-by date within validity capacity 1 each # keyed pool
pool money.rent capacity 8_400 SEK stages available|reserved|disbursed
pool money.deposit capacity 3_000 SEK stages available|reserved|disbursed
bind stay shape { from: date, to: date } at genesis
artifacts:
price-table art:stuga-prices-2027 pin v1 # SEK/night by season
house-rules class contract-bilaga sha256:... # soft: prose, hashed, binding
ports:
in payment.confirm from psp payload psp-attested-settlement
in cancel.request from guest payload signed-text
in checkin.confirm from landlord payload signed-decision
in checkout.confirm from landlord payload signed-decision
in damage.claim from landlord payload signed-claim + evidence(opaque)
in damage.accept from guest payload signed-decision
out refund.instruct to psp
out receipt.emit to submitter always
rule on genesis:
each night in stay.from .. stay.to: # bounded map over the range
if pool cabin.nights[night] drawn -> reject "double-booked"
reserve pool cabin.nights[stay.from .. stay.to]
reserve money.rent + money.deposit # deposit: escrow, §3.4
cadence:
cancellation ladder on cancel.request: # pure event math: compare
which (stay.from - event.at) is # payload dates to the
>= 30 days: refund 100% of rent # cancel event's timestamp
>= 7 days: refund 50%
otherwise: refund 0%
always: refund deposit 100%; release cabin.nights cells # cells return to the pool -
# resellable, structurally
due damage.claim within 5 days of checkout.confirm # claim window: silence
# releases the deposit
due refund deposit within 7 days of claim-window close
rule on damage.claim:
if amount > money.deposit capacity -> reject "exceeds deposit; excess is a civil claim"
which guest response is
damage.accept: draw money.deposit amount; refund remainder
otherwise (14 days): escalate level 1 # disputed damage: humans
# judge, the machine holds
escalation: # the money meanwhile
level 1 notify both, deposit frozen resolve-within 20 working-days
level 2 ARN / small-claims per prose deposit stays frozen, receipts flow
What this example stresses
| Edge | Spec section |
|---|---|
| Time-sliced occupancy - the keyed-pool gap | §8.5 (falsified as written) |
| Deposit = reserve-with-expiry escrow, claim window as due | §3.4 |
| Cancellation ladders as which-over-event-math | §3.2, §9 |
| Disputed human judgment (damage) parking money in escrow + escalation | §4.1-4.2 |
| Two-person-AB authoring bar | §6.2 |
Questions this example forced
- Keyed pools. As argued above: §8.5’s four flavors cannot express occupancy over time; the named flavor is the degenerate case of a pool keyed by identity. Proposed: adopt
keyed-by <domain>as a vetted primitive (coloured-Petri semantics, finite key domain, per-cell boundedness). This is precisely the §9 mechanism working as designed - the corpus demanded, the primitive gets vetted. Proposed; it touches the core data model. - Partial refunds are computed money flows.
refund 50%is the first place a RULE computes an amount that then moves through a linear pool - the linter must proverefund ≤ reservedfor every ladder branch (conservation, §6.4’s lesson applied to rules). Cheap to check, must be named as a lint promise. - “Silence releases the deposit.” The claim window closing with no event is what triggers the refund due - an obligation triggered by the absence of an event. §3.4’s expiry machinery covers it (event-math over the window), but note the honest dependency: nothing HAPPENS until someone pokes the contract (§3.4’s untrusted alarm clock / §3.6 heartbeat). For a consumer-facing deposit, the profile should mandate a heartbeat so the guest’s refund never waits for the landlord’s goodwill to evaluate.
The meta-finding: the smallest examples break the most. The ramavtal of §2 fit the primitives because the primitives were forged against it; the sommarstuga found a real gap in an afternoon. That is exactly why these examples exist.
The contract, in mk
The full fixture in the working v0.1 grammar - Swedish clauses governing, English mk blocks:
---
mk: v0
id: tpl-stugavtal
title: Hyresvillkor - sommarstuga per vecka
prose-lang: sv (governs)
profile: mk-se-b2c
template: true
---
# Hyresvillkor Stugbolaget AB
## § 1 Parterna och bokningen {#klausul-1 .implemented}
Uthyrare är Stugbolaget AB, org.nr 559234-5678. Hyresgäst är den konsument
som genomför bokningen. Bokningen avser stugan för de nätter som anges
vid bokningstillfället. Ångerrätt gäller inte vid upplåtelse av logi
[law:se/sfs/2005:59#kap2-p11]. <!-- statutory exemption: no angerratt
module here, deliberately - absence is readable -->
```mk
parameters:
stay shape: { from: date, to: date }
rent money SEK
parties:
landlord org: 559234-5678 "Stugbolaget AB" sign: eIDAS-seal
guest from: parameters sign: payment-authorization
state:
pool cabin.nights keyed-by: date within validity capacity: 1 each # keyed pool
pool money.rent capacity: {rent} stages: available|reserved|disbursed
rule on genesis:
each night in stay.from .. stay.to:
require cabin.nights[night] available
else reject "dubbelbokad"
reserve cabin.nights[stay.from .. stay.to]
reserve money.rent
accept
implements: [#klausul-1]
§ 2 Avbokning {#klausul-2 .implemented}
Vid avbokning senast 30 dagar före ankomst återbetalas hela hyran; senast 7 dagar före ankomst halva hyran; därefter sker ingen återbetalning. Depositionen återbetalas alltid vid avbokning.
ports:
in payment.confirm from: psp payload: psp-attested-settlement
in cancel.request from: guest payload: signed-text
in checkin.confirm from: landlord payload: signed-decision
in checkout.confirm from: landlord payload: signed-decision
out receipt.emit to: submitter always
cadence: cancellation on cancel.request kind: ladder # first-match, top-down:
| notice before stay.from | refund of rent | # rows overlap BY DESIGN,
|--------------------------|----------------| # order disambiguates
| >= 30 days | 100% |
| >= 7 days | 50% |
| otherwise | 0% |
implements: [#klausul-2]
caption: "Avbokning 30 dagar före: full återbetalning; 7 dagar: halva hyran."
rule on cancel.request:
refund := cancellation[stay.from - event.at] of {rent} # the ladder, applied
emit refund.instruct amount: refund
release cabin.nights[stay.from .. stay.to] # nights resellable,
accept # structurally
§ 3 Deposition {#klausul-3 .implemented}
Hyresgästen erlägger en deposition om 3 000 kronor som återbetalas efter avresa om skadeanspråk inte framställts inom fem dagar.
use module:market/deposit@v2 # THIRD-PARTY module (Marknadsjuristerna AB),
with: { amount: 3_000 SEK, # publisher-sealed, hash-pinned via the tag:
holder: party:landlord, # @v2 resolves ONCE at flatten, recorded
payer: party:guest, # as sha256 beside the tag
end-event: checkout.confirm,
claim-window: 5 days }
implements: [#klausul-3]
§ 4 Tvist {#klausul-4 .soft}
Tvist som inte kan lösas mellan parterna kan prövas av Allmänna reklamationsnämnden.
use module:std/se/dispute-arn@v1 # STANDARD module - same ladder the
with: { notify-window: 5 working-days } # webshop uses: ONE vetted artifact,
implements: [#klausul-4] # many consuming contracts (§5.3)