Patient journal

The scenarios doc #1 argued that patientdatalagen already describes our machine. This example calls that bluff: here is the journal written AS a mechanical contract. Small vocabulary, hard semantics - the pools are nearly absent (nothing is allocated), the registers dominate, and the entire contract is about WHO MAY WRITE, WHO MAY READ, and the receipts both leave behind. Legal grounding lives in the patientdatalagen research note; this file is the mechanics.

Profile: mk-se-health (hypothetical). Unlike every other example, the template author is effectively the legislature: PDL mandates the terms, the vårdgivare operates the instrument, the patient holds rights in it without ever signing it. That asymmetry is the first thing the example forces.

The contract

mechanical-contract v0
id:       mk-se-health-journal-19XXXXXX-XXXX     # one instrument per patient
profile:  mk-se-health                           # binds PDL (2008:355) + HSLF-FS 2016:40
template: tpl-pdl-journal @ v2                   # statutory template: terms mandated
                                                 # by law, not negotiated
parties:
  vardgivare:  org 232100-0255 "Region Skåne"  sign eIDAS-seal    # signs + operates
  patient:     party<person>  BENEFICIARY       # rights-holder, never signed

artifacts:
  hosp-register        art:socialstyrelsen-hosp   track latest   # legitimation lookup
  care-relations       art:region-care-relations  track latest-approved
                       class party-maintained-register           # §5.6: vårdgivaren
                                                                 # maintains, every
                                                                 # change receipted
state:
  register entries     shape { author: id<hosp>, unit: id<careunit>,
                               content: opaque, at: date }       # the journal itself:
                                                                 # content is OPAQUE -
                                                                 # the machine governs
                                                                 # access, never medicine
  register corrections shape { entry: id<entry>, note: opaque }  # rattelse: marked,
                                                                 # original stays readable
  register sparrar     shape { scope: id<careunit>, by: patient }
  register consents    shape { scope: sammanhallen, granted: bool }

ports:
  in   entry.write       from vardgivare.staff   payload journal-entry
  in   entry.sign        from author             payload signed-decision
  in   correction.mark   from vardgivare.staff   payload correction      # NEVER delete
  read journal.read      from vardgivare.staff | patient                 # the new
                                                 # port kind - access itself receipted
  in   sparr.set         from patient            payload signed-declaration
  in   sparr.lift        from patient            payload signed-declaration
  in   consent.grant     from patient            payload signed-decision # sammanhållen
  in   consent.revoke    from patient            payload signed-decision # journalföring
  in   emergency.open    from vardgivare.staff   payload signed-reason   # nödöppning
  in   destruction.order from ivo                payload signed-decision # the ONLY
                                                 # deletion path: IVO decision
  out  receipt.emit      to submitter            always
  # note what is ABSENT: no invoice port, no payment port, no export port.
  # a journal that cannot leak through an undeclared opening - by grammar.

cadence:
  due entry.sign  within 14 days of entry.write     # osignerade anteckningar: today a
                                                    # recurring audit finding, here a
                                                    # breached obligation with a receipt
rule on entry.write:
  if payload.author not in hosp-register            -> reject "not legitimerad"
  if payload.author not in care-relations[patient]  -> reject "inre sekretess"
  record entries { ... }                            # append-only; no update verb exists
  accept

rule on journal.read:                               # read semantics
  if reader is patient                              -> allow scope full
  if reader not in care-relations[patient]          -> reject "inre sekretess"    # PROXY:
                                                    # the register row stands in for
                                                    # "deltar i vården" - leg-D fidelity
                                                    # lesson: proxy, not faithful capture
  if reader.unit in sparrar and no emergency open   -> reject "sparrad"
  allow scope entries where unit not in sparrar
  # every verdict here - allowed AND refused - emits a receipt: the access log
  # that PDL mandates and the loggutdrag folds over

rule on emergency.open:                             # nödöppning: bryta spärren
  escalate level nod                                # declared disclosure WIDENING
  accept

escalation:
  level nod:                                        # §12: per-level disclosure scopes,
    widen journal.read scope all-units for 24h      # on max difficulty
    due review by vardgivare.chefsansvarig within 5 working-days   # mandatory
    notify patient                                  # after-the-fact review, receipted

disclosure:                                         # §12.3 posture, instantiated
  patient:        everything, always, including ALL read receipts (loggutdrag)
  staff:          entries per care-relation + spärr state
  ivo/tillsyn:    envelopes + digests; bodies per court/tillsyn order
  # loggutdrag = fold(read receipts where subject = patient) - a query, not a feature

What the fold answers

• “Who read my journal in March?” - fold the journal.read receipts: reader, unit, scope, timestamp, and the rule branch that admitted them. The loggutdrag stops being a report someone generates and becomes a replay anyone can verify.
• “Was anything altered?” - nothing CAN be altered: no update verb exists, corrections are marked additions, and the hash chain proves it without disclosing one word of content (envelope/body detachment, §2).
• “Was the spärr respected?” - every rejected read is ALSO a receipt. Today’s audit asks “show me your access controls”; this asks “show me the refusals” - evidence of the control working, not a description of it.

What this example stresses

Edge	Spec section
Receipted reads - access as a first-class event	§12.4 (v-next flag, now with worked syntax)
Disclosure scopes + per-level widening (nödöppning)	§12.3
opaque carrying content the machine must never judge	§8.4
Party-maintained registers as authorization ground truth	§5.6
Append-only forever: corrections, IVO-only destruction	§1 replay covenant

Questions this example forced

• The beneficiary party. The patient holds ports (sparr.set, journal.read), receives receipts, and can trigger escalation - but never signed anything, and the terms were never negotiated: law mandates them. The spec’s party model assumes signatories. Proposed: a declared party role class - signatory | beneficiary | executor - where beneficiaries derive standing from the profile (statute) or from a genesis declaration (tredjemansavtal; third-party beneficiary is ancient contract law). Executor-as-party (§3.6) was already the first crack in “party = signer”; this names the pattern.
• The read port kind. Reads move no state, yet must be receipted, and both grants AND refusals are evidence. Three sub-questions. (a) Verdict vocabulary: ACCEPTED fits, state-after == state-before always - fine. (b) Log volume is the real creak: a hospital reads thousands of times a day; folding a decade of reads to answer a pool query is absurd. Proposed: reads chain in a SEPARATE access chain per contract, periodically anchored (its head hash recorded as an event) into the main chain - IHE ATNA made the same split (audit repository beside the clinical record) for the same reason. State replay never touches the access chain; loggutdrag folds only it. (c) Reading the read-log is itself a receipted read - recursion is fine (one level, boring), but must be said.
• Spärr is runtime capability change, and ports are static. The manifest is signed and fixed; the patient closes doors at runtime. Resolution adopted in the example: the manifest never changes - journal.read stays declared; the spärr is a GUARD over patient-controlled state (the sparrar register). Capability = port ∧ guards, and “absent port = prohibition” survives untouched. This pattern generalizes: any revocable permission is a guard over a register, never a manifest edit.
• Decades-long artifacts vs signature lifetimes. A journal outlives RSA key sizes, seal certificates, and probably the vårdgivare. Prior art exists and suffices: eIDAS LTA archival profiles (XAdES-LTA) re-timestamp evidence before algorithms age out; the host’s archival duty becomes a HOSTING.md obligation. Named, shelved - not a v1 problem, but a v1 format decision (receipts must be re-timestampable without re-signing).

Honesty block, unchanged from the scenarios note: this is not the wedge and must not become it. The example exists because it is the hardest access-control domain Swedish law has - if the primitives hold here, §12’s machinery has its worked example. They held, at the cost of four forced questions - which is the point of forcing.