Skip to content

Instantly share code, notes, and snippets.

@halcwb

halcwb/Session.fsx

Last active August 23, 2026 18:19
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save halcwb/0080593eec0d3af6a836df6a56f0044c to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save halcwb/0080593eec0d3af6a836df6a56f0044c to your computer and use it in GitHub Desktop.
Download ZIP
Modelling main EHR - GenPRES - User session management
Raw
Session.fsx
// ═══════════════════════════════════════════════════════════════════════════════
// GenPRES – MainEHR Integration: the system model, executable
// ═══════════════════════════════════════════════════════════════════════════════
//
// A runnable model of the design document *GenPRES – MainEHR Integration*. The
// document is leading: every type, message and branch below exists to carry one of
// its Actors, Concepts, Constraints or Rules, and cites it by number. Nothing the
// document does not sanction lives here.
//
// The file is standalone — no #load, no #r. Run it with:
//
// dotnet fsi Session.fsx
//
// It prints a trace per scenario and ends with a count of self-checks.
//
// ═══════════════════════════════════════════════════════════════════════════════
// SECTION 0 — THE SYSTEM MODEL, AS THE DOCUMENT STATES IT
// ═══════════════════════════════════════════════════════════════════════════════
//
// ── Actors ─────────────────────────────────────────────────────────────────────
// [ours] = under construction. [given] = existing infrastructure, not ours to
// change. The User is neither — they are who the system is for.
//
// 1. MainEHR Workstation [given] the running EHR Client
// 2. MainEHR LaunchScript [ours] a VB.NET script behind a button in the
// Workstation. Runs on trigger, then exits.
// The only part of MainEHR we control.
// 3. GenPRES Client [ours] GenPRES UI running in a Browser
// 4. GenPRES Server [ours] GenPRES backend
// 5. GenPRES Database [ours] holds the SessionRecords, PatientRecords and
// UserCredentials. The Server is its only writer.
// 6. PatientDataPlatform [given] a shared, read-only copy of the databases of
// MainEHR, GenPRES and other applications
// 7. User person who uses MainEHR and GenPRES
// 8. Broker [ours] hands a launch from the LaunchScript to the Server
// 9. UserRegistry [ours] says who a login belongs to, what that person
// may do, and how to reach them by mail
// 10. MailService [given] sends mail, outside GenPRES and outside MainEHR
//
// ── Roles ──────────────────────────────────────────────────────────────────────
// The UserRegistry decides the Role. MainEHR and GenPRES enforce it independently.
//
// 1. Prescriber may read and write — writing meaning creating TreatmentPlans
// 2. Reader may never create a TreatmentPlan. Like any User they may prescribe
// within their Session (Concept 15), but nothing of it can be saved.
//
// ── Concepts ───────────────────────────────────────────────────────────────────
//
// 1. UserContext User identification and User Role.
// 2. PatientContext PatientId and Patient Data relevant for GenPRES. The User
// can supply the data by hand; only a launch can supply the
// identification. Launched, the data is read from the
// PatientDataPlatform once, at the launch, and not refreshed
// while the Session lives: in-Session staleness is accepted.
// 3. LaunchAssertion asserts a MainEHR login, and the Patient if one is active
// — no verified identity, no Role.
// 4. LaunchCredential opaque single-use reference to a LaunchAssertion, short
// lifetime.
// 5. MainEHR Session the period a User is logged in at a Workstation. Many
// Patients can be handled in it, one active at a time.
// 6. MainEHR PatientRecord all patient data maintained by MainEHR.
// 7. GenPRES UserCredential held by GenPRES for one User — the login by which the
// UserRegistry knows that person, a PIN if one is set, and
// the count of consecutive wrong PIN entries (Rule 27). The
// PIN is optional: a UserCredential may hold none, either
// because the User has never set one or because it was
// removed, and one without a PIN cannot sign. It carries no
// Role and no identity of its own.
// 8. GenPRES Session the interaction of a User with GenPRES — for a Patient if
// the launch supplied one, otherwise for no Patient; opened
// without a launch, it is anonymous (Rule 13). Only a Session
// with a Patient allows opening or creating TreatmentPlans
// (Rule 12). A Session has no state in GenPRES Server between
// requests: its identity and standing live in its
// SessionRecord, its work in GenPRES Client (Rule 31).
// 9. GenPRES SessionRecord binds a SessionId to exactly one User — the UserContext
// as the launch established it, and the mail address — or to
// no User, when anonymous — and to a Patient if it has one.
// Records whether the Session is open or ended, when it last
// heard from the Client (Rule 8), and whether the User has
// been told about its ending. Kept after the Session ends.
// 10. OrderContext a PatientContext together with the OrderScenarios currently
// under consideration. It has an identity that persists across
// TreatmentPlans, and carries the UserContext of the User whose
// Session last changed it — stamped at each save (Rule 14), so
// an OrderContext that is never saved carries none.
// 11. OrderScenario one proposed Order together with the prescribing information
// that gives it meaning but is not part of the Order itself.
// 12. GenPRES PatientRecord the append-only history of a Patient in GenPRES — a
// sequence of TreatmentPlans, every one carrying that Patient's
// PatientId: the one thing no TreatmentPlan may change.
// 13. TreatmentPlan the Patient's treatment plan as it stood when saved — a set of
// their OrderContexts, carrying the UserContext of the User who
// created it and a reference to the TreatmentPlan it was created
// from — its base — if any. Either Signed or Unsigned.
// 14. Saving and Signing one act — creating a TreatmentPlan. Signing is saving while
// supplying the PIN of the Session's User: the TreatmentPlan is
// then Signed, otherwise Unsigned. There is no other way a
// TreatmentPlan comes into being.
// 15. Prescribing changing, within a Session, the Patient Data of the
// PatientContext and adding, removing or changing
// OrderContexts. Prescribing touches only the Session, and the
// work lives in GenPRES Client (Rule 31): nothing reaches the
// PatientRecord until a TreatmentPlan is created, and the Server
// computes on what the Client sends without keeping any of it.
//
// ── Constraints ────────────────────────────────────────────────────────────────
// Notation:
// X -> Y X initiates a connection to Y and receives Y's response on it. Grants
// initiation in that direction only; the reverse is never implied.
// X => Y X launches Y with initial parameters. One-way: no response, no error
// path back.
// X <-> Y interaction, not request–response: a User can read what Y shows and
// act on it.
// Any pair without an edge cannot exchange data at all. Edges do not compose — no
// component relays on another's behalf unless stated.
//
// User Interaction
// U1. Any User <-> MainEHR Workstation
// U2. Any User <-> MainEHR LaunchScript — the User starts it; while it runs it can
// report its own acts back (the Broker
// exchange, the launching of the browser),
// and it exits at once, so nothing later
// ever comes from it.
// U3. Any User <-> GenPRES Client
//
// Communication
// C1. MainEHR Workstation -> UserRegistry
// C2. MainEHR Workstation -> PatientDataPlatform
// C3. MainEHR LaunchScript -> Broker
// C4. MainEHR LaunchScript => GenPRES Client
// C5. GenPRES Client -> GenPRES Server
// C6. GenPRES Server -> Broker
// C7. GenPRES Server -> UserRegistry
// C8. GenPRES Server -> PatientDataPlatform
// C9. GenPRES Server -> GenPRES Database
// C10. GenPRES Server -> MailService
//
// ── Consequences ───────────────────────────────────────────────────────────────
// Derived from the edges above — not new assertions.
//
// 1. The LaunchScript learns nothing after the launch. What it can report to the
// User (User Interaction 2) ends with its own acts: the Broker exchange (UC-1
// ext 3a) and the launching of the browser. Expired credential, Server down,
// wrong patient — none of it reaches it. Error handling falls to the Client,
// except when the Server is unreachable: the Client is served by the Server, so
// then no Client is served either and the User is left with the browser's error
// page.
// 2. The Broker is the only party both the LaunchScript and the Server can reach,
// so it is the sole channel between the EHR side and GenPRES.
// 3. Only the Broker knows whether a credential was redeemed, and it cannot tell
// the LaunchScript, which has exited.
// 4. The credential travels in a URL, so it lands in browser history, the address
// bar, and possibly referrer and proxy logs — hence single use, short lifetime.
// 5. Both the Workstation and the LaunchScript run on the User's PC, so their calls
// originate there. Every workstation needs network access to the UserRegistry,
// the PatientDataPlatform and the Broker, plus whatever secret authenticates it.
// 6. The Server cannot reach a Client (edge C5 goes one way only), so a Client only
// learns its Session ended at its next request. Until then it shows a
// live-looking screen.
//
// ── Invariants ─────────────────────────────────────────────────────────────────
// 1. A User has at most one active Patient at any moment in a MainEHR Session.
//
// ── Possibilities ──────────────────────────────────────────────────────────────
// 1. Users can leave a logged in MainEHR Session open and another User can act in it.
// 2. Multiple Users can have the same Patient active each in their own MainEHR Session.
//
// ── Rules ──────────────────────────────────────────────────────────────────────
// What the [ours] components must enforce. One assertion each; grouped for reading,
// numbered straight through for citing.
//
// Launch
// 1. The LaunchScript decides which MainEHR User may run it.
// 2. A LaunchCredential is accepted once; a second presentation is refused.
// 3. A LaunchCredential is accepted only within its lifetime.
// 4. Only the Server may redeem a LaunchCredential at the Broker.
// 5. The Server takes the Role from the UserRegistry at each launch, never from
// the launch itself.
// 6. If a launch cannot be honoured — no credential, no Role, or a required PIN
// not set (Rule 24) — no Session is opened by it. There is no silent fallback:
// at most, the Client offers the User a fresh anonymous open (Rule 13; UC-8),
// which carries nothing over from the launch — no User, no Patient.
//
// Session
// 7. A User has at most one open Session; opening another closes the rest. The
// limit is per User, not per Patient: two Users may each hold their own
// Sessions for the same Patient at once.
// 8. Every request from the Client refreshes its Session's idle clock.
// 9. A Session ends when the User closes it, when it has been idle too long, when
// the wrong-PIN limit is reached (Rule 27), or when that same User opens another
// Session (Rule 7). Closing is an explicit act in the Client: a browser that
// vanishes is indistinguishable from one gone quiet, so the Session is left to
// idle out. A Server restart ends nothing: the Server holds no Session state to
// lose (Rule 31).
// 10. When a Session ends other than by the User closing it, the User is told at the
// next opportunity: through any Client still holding that SessionId, at its next
// request, or at the User's next launch. Told once, never twice.
// 11. The SessionId is a bearer credential: it never travels in a URL.
// 12. A Session without a PatientId lets the User prescribe (Concept 15), Patient
// Data included, but a TreatmentPlan cannot be opened or created.
// 13. A Session opened without a launch is anonymous: it binds to no User and
// carries no UserContext, no Role, and no PatientId. Rules that speak of the
// Session's User (7, 10) do not apply to it, and it need not idle out (Rule 9):
// it may remain open indefinitely, as keeping it has no consequence.
//
// Record
// 14. Every TreatmentPlan is created under the credentials of exactly one User — the
// Session's — and carries that User's identity. Within it, every OrderContext
// changed in the Session is stamped with that same UserContext; an unchanged
// OrderContext keeps the stamp it had.
// 15. A TreatmentPlan is either Signed or Unsigned.
// 16. Only the most recent Signed TreatmentPlan counts clinically.
// 17. The most recent Signed TreatmentPlan is the only one another User can open —
// older TreatmentPlans are record, not views.
// 18. Only the User who created an Unsigned TreatmentPlan can open that TreatmentPlan.
// 19. A User can only start with the most recent TreatmentPlan that is either Signed or
// Unsigned and their own. Where neither exists, the User works from nothing.
// 20. A User may create a new TreatmentPlan, unless a Signed one exists that is newer
// than the TreatmentPlan the User opened with — the one most recently opened in
// the Session, so opening the newest Signed one lifts the block (UC-6).
//
// Notification
// 21. If a User is about to create a TreatmentPlan and an Unsigned one of another User
// exists that is newer than the TreatmentPlan the User opened with — any
// TreatmentPlan at all, where the User opened with nothing — the User is notified —
// told whose work it is, not its contents — and may choose not to create.
//
// Signing
// 22. The Server is the only party that verifies a UserCredential; the PIN never
// leaves GenPRES.
// 23. Every launch checks whether a PIN is set for the login.
// 24. A Prescriber with no PIN must set one before the launch continues, and only
// after the UserRegistry has recognised their login.
// 25. A Reader is never asked for a PIN: a Reader never creates a TreatmentPlan, so they
// have nothing to prove.
// 26. The Server mails the User and records the change on every setting of a PIN
// and every removal of one, the first setting included. The address comes from
// the UserRegistry.
// 27. Wrong PIN entries count per UserCredential, across Sessions: a wrong entry at
// the configurable limit ends the Session (Rule 9). A correct entry resets the
// count, and a newly set PIN (Rule 26) starts with a count of zero.
//
// Configuration
// 28. A LaunchCredential lives long enough to carry one launch — a page load and a
// retry or two — and no longer.
// 29. A Session lives long enough to span the gaps between a clinician's actions.
// 30. The wrong-PIN limit is small enough to make guessing hopeless, large enough
// to forgive mistyping.
//
// State — where Session state lives; chosen so that the Server keeps none of it.
// 31. The Server holds no Session state between requests: what a User is prescribing
// lives in the Client, and a Session's identity and standing live in its
// SessionRecord in the Database. Two Users' work cannot meet in the Server,
// because the Server holds neither.
// 32. The Server takes the User and the Patient of a request from the SessionRecord,
// never from the request's payload.
// 33. The TreatmentPlan a Session opened with travels as a token the Server issued at the
// opening — bound to the Session, the Patient and the TreatmentPlan — returned by the
// Client with every create and verified then (Rules 19, 20). The Client cannot
// make one.
// 34. A choice to create anyway (Rule 21) travels the same way: a token issued with
// the notice, naming the Unsigned TreatmentPlans it disclosed, honoured for those and
// for nothing newer.
// 35. The stamps of Rule 14 are computed by the Server against the base TreatmentPlan; a
// stamp arriving from the Client is never accepted.
// 36. The Rule 20 check and the append are one act at the Database: a TreatmentPlan lands
// only if the head the check saw is still the head. More than one Server may
// run; the Database arbitrates.
//
// ── Guarantees ─────────────────────────────────────────────────────────────────
// What the Rules add up to. Derived, not asserted. Checked at the end of the run.
//
// 1. One constant. A PatientRecord is a sequence of TreatmentPlans in which the
// PatientId is the only constant.
// 2. One version. At any moment exactly one TreatmentPlan is the visible version and the
// only starting point for updating it.
// 3. Carts and one checkout. The cart is private — it lives in the User's own Client
// and the Server keeps none of it (Rule 31) — signing is the only checkout, and
// the first User to sign wins the version (Rule 36).
// 4. Audit. A Signed TreatmentPlan carries the User who signed it, every OrderContext
// carries the User whose Session last changed it, and the record is append-only.
//
// ── Open Questions ─────────────────────────────────────────────────────────────
// 1. Mail deliverability. Rule 26's guarantee holds only if the UserRegistry
// address is current and the MailService delivers. Neither can be checked here.
// 2. Unsigned TreatmentPlans in the PatientDataPlatform. Rules 17 and 18 bind GenPRES,
// but the PatientDataPlatform holds a copy of the Database readable by the
// Workstation and other applications. Unsigned work, closed to other Users
// inside GenPRES, may thus be readable outside it.
// 3. Payload. Under Rule 31 the whole of the work travels with every computing
// request and every create. Whether that is acceptable is a measurement, not a
// judgement. A bad number would force a server-side cache of the work, which must
// then be built as an optimisation the Rules never depend on, losable without
// breaking anything. This model shows the pure design: `ServerState` holds
// counters, the in-flight table and nothing else, and that is asserted after
// every scenario step.
//
// ── Where this model differs from the repository ───────────────────────────────
// The repository's GenPRES Server is already stateless between requests. That is no
// longer a divergence from the document: it is the specified design (Rule 31),
// extended here with the Session identity and standing that the SessionRecord holds
// and the tokens of Rules 33 and 34 that make a client-held cart safe to trust.
//
//
// The rest of the file is in three parts:
// 1. types — the vocabulary: identities, concepts, messages, actor state
// 2. modules — the edge table, the Record rules, the tokens, and the reducer
// 3. scenarios — the harness, UC-1 .. UC-13, and the derived assertions
// ═══════════════════════════════════════════════════════════════════════════════
// 1. TYPES
// ═══════════════════════════════════════════════════════════════════════════════
// ───────────────────────────── identities ─────────────────────────────
type UserId = UserId of string // stable key: what audit keys on
type LoginName = LoginName of string // unique today, but renameable
type MailAddress = MailAddress of string // from the UserRegistry (Rule 26)
type PatientId = PatientId of string
type BrowserId = BrowserId of int
type LaunchCredential = LaunchCredential of string // Concept 4: opaque to GenPRES
type LaunchNo = LaunchNo of int // readable handle, safe to log
type SessionId = SessionId of string // Rule 11: bearer, never in a URL
type SessionNo = SessionNo of int // traces and ui only, never a key
type TreatmentPlanId = TreatmentPlanId of string
type TreatmentPlanNo = TreatmentPlanNo of int // ordering within one PatientRecord
type OrderContextId = OrderContextId of string // Concept 10: persists across plans
type AttemptId = AttemptId of int // correlates one launch across ports
/// Rule 31. Correlates the several Database legs of ONE request. Created when the
/// request arrives, dropped with its reply — never carried from one request to the
/// next, which is the whole of what makes the Server stateless.
type RequestId = RequestId of int
type Pin = Pin of string // Concept 7. Never leaves GenPRES.
/// Roles. The UserRegistry decides which.
type Role =
| Prescriber
| Reader
/// The ten Actors of the document, plus Environment — which is not a use case actor
/// but the world they run in: the clock, and starting and stopping infrastructure.
type ActorId =
| User // Actor 7
| MainEhrWorkstation // Actor 1 [given]
| MainEhrLaunchScript // Actor 2 [ours]
| GenPresClient of BrowserId // Actor 3 [ours]
| GenPresServer // Actor 4 [ours]
| GenPresDatabase // Actor 5 [ours]
| PatientDataPlatform // Actor 6 [given]
| Broker // Actor 8 [ours]
| UserRegistry // Actor 9 [ours]
| MailService // Actor 10 [given]
| Environment
// ───────────────────────────── the concepts ─────────────────────────────
/// Concept 1. Identification and Role — nothing else. The Role is the registry's
/// answer (Rule 5), never the launch's.
type UserContext =
{
UserId : UserId
Login : LoginName
Role : Role
}
/// Patient Data relevant for GenPRES. Opaque here: this is a model of the protocol,
/// not of the clinical content.
type PatientData = PatientData of string
/// Concept 2. Only a launch can supply the identification; the User can supply the
/// data by hand. Read from the PatientDataPlatform once, at the launch, and not
/// refreshed while the Session lives.
type PatientContext =
{
Patient : PatientId option
Data : PatientData option
}
/// Concept 3. The whole of what crosses the Broker port, and only as trustworthy as
/// whatever wrote it: a login to look up, and a Patient if one was active. No
/// verified identity, no Role.
type LaunchAssertion =
{
Login : LoginName
Patient : PatientId option
}
/// Concept 7. Carries no Role and no identity of its own. A UserCredential without a
/// PIN cannot sign.
type UserCredential =
{
Login : LoginName
Pin : Pin option
AttemptCount : int // Rule 27: counts across Sessions
}
/// Concept 10. It has an identity that persists across TreatmentPlans, a PatientId it
/// belongs to, whatever the User is putting into it, and the stamp: the UserContext
/// of the User whose Session last changed it (Rule 14).
///
/// Abstracted here: the document's OrderContext is a PatientContext together with the
/// OrderScenarios under consideration (Concepts 10, 11). None of the clinical content
/// is modelled — `Content` stands in for the whole of it, opaque like PatientData.
/// What the Rules turn on is only that it has an identity, names a Patient
/// (Guarantee 1, Rule 32), can be compared with the base to tell changed from
/// unchanged (Rule 35), and carries a stamp.
///
/// The cart is client-held (Rule 31), so all four fields arrive from the Client with
/// every request — and the Server trusts exactly two of them: `Id` and `Content`.
/// `Patient` is checked against the SessionRecord and `Stamp` is recomputed.
type OrderContext =
{
Id : OrderContextId
Patient : PatientId option
Content : string
Stamp : UserContext option
}
/// Concept 13. Signed or Unsigned (Rule 15), by exactly one User (Rule 14), over the
/// TreatmentPlan it was created from — its base — if any.
type TreatmentPlan =
{
Id : TreatmentPlanId
No : TreatmentPlanNo
Patient : PatientId
By : UserContext
Base : TreatmentPlanId option
Orders : OrderContext list
Signed : bool
At : int
}
/// What the Server hands the Database to append (Rule 36). It has no Id and no No:
/// those are the Database's to mint, because the Database is what serialises the
/// appends now that more than one Server may run.
type TreatmentPlanDraft =
{
Patient : PatientId
By : UserContext
Base : TreatmentPlanId option
Orders : OrderContext list
Signed : bool
}
/// Concept 12. Append-only. Newest first, so the Record rules are `List.tryFind`.
/// The PatientId is the one thing no TreatmentPlan may change (Guarantee 1).
type PatientRecord =
{
Patient : PatientId
Plans : TreatmentPlan list
}
// ───────────────────────────── the tokens ─────────────────────────────
/// Rule 33. The TreatmentPlan a Session opened with, as something the Client can hold
/// and hand back but cannot make. Minted at the opening of the Session and re-minted
/// whenever the baseline moves — an open (Rule 17) or a create — because Rules 20 and
/// 21 are both measured from it.
///
/// `Mac` stands in for an HMAC over the other three fields and a secret only the
/// Server knows. Verification is recomputing it and comparing.
type OpenedToken =
{
Sid : SessionId
Patient : PatientId option
Plan : TreatmentPlanId option
Mac : string
}
/// Rule 34. The User's choice to create anyway, as something that names exactly what
/// they were shown: honoured for those Unsigned TreatmentPlans and for nothing newer.
type NoticeToken =
{
Sid : SessionId
Disclosed : TreatmentPlanId list
Mac : string
}
// ───────────────────────────── session state ─────────────────────────────
/// Rule 9, exactly: the four ways a Session ends, and no others. A Server restart is
/// not among them — the Server holds no Session state to lose (Rule 31).
type EndMark =
| ClosedByUser
| Idle
| Superseded
| WrongPinLimit
/// Two states. `OpenOrGone` also covers "the Client has gone quiet and the Server
/// cannot yet tell" — Rule 9 says a vanished browser is indistinguishable from a
/// silent one, so there is nothing finer to record.
type SessionState =
| OpenOrGone
| Ended of mark: EndMark * at: int
/// Rule 10, as a state rather than a timestamp. `int option` could not tell "no
/// notice is owed" apart from "one is owed and not yet given": a Session the User
/// closed themselves is owed nothing at all (Rule 10 speaks only of endings other
/// than by the User), while one that idled out is. Orthogonal to *how* a Session
/// ended — being told is not a way for a Session to end.
///
/// "Notice" is the document's own noun for this — "the notice comes with the new
/// launch", "the notice is not repeated", "no notice at the next launch", "a harmless
/// notice". Not `Notification`: in the document that word is the heading of the Rules
/// group holding Rule 21 — the notice that another User's Unsigned work exists, which
/// is a different thing entirely and is carried here by `UnsignedWorkNotice`.
type SessionNotice =
/// The Session is open, or the User closed it themselves. Nothing is owed.
| NotOwed
/// It ended in a way the User has not been told about, and will be at the next
/// opportunity: a Client still holding that SessionId, or the User's next launch.
| Owed
/// Told, and once only.
| Told of at: int
/// Concept 9 — the record of a Session, and now the whole of what GenPRES remembers
/// of one between requests (Rule 31). Lives in the Database, is kept after the
/// Session ends, and the Server is its only writer.
///
/// It carries the UserContext, not merely the UserId: the Role a Session runs under
/// is the one its launch established (UC-13 ext 1a), and Rule 32 takes the User of a
/// request from here rather than from the payload. The mail address rides along for
/// the same reason — Rule 26 has to reach the User with no Session in memory to ask.
type SessionRecord =
{
Id : SessionId
No : SessionNo
/// None: the Session was anonymous (Rule 13).
User : UserContext option
Mail : MailAddress option
Patient : PatientId option
Launch : LaunchNo option // None: no launch — an anonymous open
OpenedAt : int
/// Rule 8: every request from the Client refreshes this. The idle clock lives
/// here because there is nowhere else for it to live.
LastSeen : int
State : SessionState
/// Rule 10. Set by `endWith`, so the obligation is created by the same act
/// that creates the ending and cannot drift from it.
Notice : SessionNotice
}
// ───────────────────────────── failures ─────────────────────────────
type LaunchFailure =
| NotFound
| CredentialExpired // Rule 3
| AlreadyRedeemed // Rule 2
| BrokerUnreachable // UC-1 ext 8b
type RegistryFailure =
| NoRole // the registry knows the login, and says no
| RegistryUnreachable // the registry cannot say
/// Which exchange a Database answer belongs to: a launch in flight, one request in
/// flight, or the idle sweep. Nothing outlives its exchange.
type DbTag =
| ForLaunch of AttemptId
| ForRequest of RequestId
| ForSweep
// ───────────────────────────── messages ─────────────────────────────
/// What travels from the Client to the Server inside a Session. Every one of these
/// arrives as a `SessionRequest`, so Rule 8's idle-clock refresh has exactly one home
/// — and every one of them is answered out of its own payload plus the SessionRecord,
/// with nothing kept afterwards (Rule 31).
type SessionCmd =
/// Concept 15. The Client has already changed its own cart; this sends the whole
/// of it for computing. The answer comes back from the payload, and the Server
/// keeps none of it.
| Compute of OrderContext list
/// Concept 14. Saving and Signing are one act. `None` saves — the TreatmentPlan is
/// Unsigned. `Some pin` signs — Signed, if the PIN verifies (Rule 22). The whole
/// cart travels, with the opened-with token (Rule 33) and, where the User is
/// answering a Rule 21 notice, the token that came with it (Rule 34).
| CreateTreatmentPlan of
Pin option * OrderContext list * PatientData option * OpenedToken * NoticeToken option
| OpenTreatmentPlan of TreatmentPlanId // Rules 17, 18
| ResetPin // UC-7
| CloseSession // Rule 9
/// What the User does at the Client. Distinct from `SessionCmd`: some of these are
/// purely local (the cart is the Client's), and every one that does reach the Server
/// carries the cart with it.
///
/// There is no `Proceed` and no `HoldOff`. Under Rule 34 proceeding is re-sending the
/// create with the token the notice came with, and holding off is not sending it.
type UserAct =
| Prescribes of OrderContextId // Concept 15: add or change, in the Client
| EntersPatientData of PatientData // Concept 2: the User supplies it by hand
| Saves // Concept 14, Unsigned
| Signs of Pin // Concept 14, Signed if it verifies
| OpensTreatmentPlan of TreatmentPlanId // Rules 17, 18
| AsksPinReset // UC-7
| ClosesSession // Rule 9
/// UC-9 step 5. The cart survived the Session because it was never in the Server
/// (Rule 31); the User carries it into the next one as fresh prescribing. It
/// survives exactly as far as the browser does.
| CarriesOverFrom of BrowserId
type Msg =
// ── Environment: the clock and the infrastructure ──
| Tick
| Start of ActorId
| Stop of ActorId
// ── U1. User <-> MainEHR Workstation ──
| LogIn of LoginName
| SelectPatient of PatientId
| ClearPatient
// ── U2. User <-> MainEHR LaunchScript ──
| TriggerLaunch
/// UC-1 ext 3a. The one launch failure the EHR side can report: the Broker edge is
/// request-response, and the LaunchScript has not yet exited. Its reporting ends
/// with its own acts — after the launch it learns nothing (Consequence 1).
| LaunchError of string
// ── C3. MainEHR LaunchScript <-> Broker. No Role: the launch carries no rights. ──
| PrepareLaunch of LoginName * PatientId option
| LaunchPrepared of LaunchCredential
| LaunchNotPrepared
// ── C4. MainEHR LaunchScript => GenPRES Client. One-way: Consequence 1. ──
| OpenUrl of LaunchCredential
// ── U3. User <-> GenPRES Client ──
| Refresh // re-present whatever is in the address bar
| OpenDirectly // UC-8: no launch, no credential
| AcceptAnonymousOffer // Rule 6, UC-1 ext 9a
| ChoosePin of Pin // UC-2 step 3, mid-launch
| Act of UserAct
| CloseBrowser // UC-12 ext 2a: nothing reaches the Server
// ── C5. GenPRES Client -> GenPRES Server ──
| RedeemLaunch of LaunchCredential
| OpenAnonymous // Rule 13
| SupplyPin of AttemptId * Pin // UC-2: the launch is suspended on a human
| SessionRequest of SessionId * SessionCmd
// ── C6. GenPRES Server <-> Broker ──
| ResolveLaunch of AttemptId * LaunchCredential
| LaunchResolved of AttemptId * LaunchNo * LaunchAssertion
| LaunchRejected of AttemptId * LaunchNo option * LaunchFailure
// ── C7. GenPRES Server <-> UserRegistry. The credential never reaches here. ──
| ResolveUser of AttemptId * LoginName
| UserResolved of AttemptId * UserContext * MailAddress
| UserUnresolved of AttemptId * RegistryFailure
// ── C8. GenPRES Server <-> PatientDataPlatform ──
| ReadPatientData of AttemptId * PatientId
| PatientDataRead of AttemptId * PatientData
| PatientDataUnavailable of AttemptId
// ── C9. GenPRES Server <-> GenPRES Database. The Server is its only writer. ──
| ReadCredential of DbTag * LoginName
| CredentialRead of DbTag * UserCredential option
| WriteCredential of DbTag * UserCredential
| CredentialWritten of DbTag * UserCredential
| RemovePin of DbTag * LoginName
| PinRemoved of DbTag * UserCredential
| ReadRecord of DbTag * PatientId
| RecordRead of DbTag * PatientRecord
/// Rule 36. The Rule 20 check and the append are one act at the Database: the
/// Server sends the head its check saw, and the TreatmentPlan lands only if that is
/// still the head. The draft has no Id: the Database mints it, because the
/// Database is what orders the record now.
| AppendIf of DbTag * TreatmentPlanId option * TreatmentPlanDraft
| TreatmentPlanAppended of DbTag * TreatmentPlan
| AppendRefused of DbTag * TreatmentPlanId
| WriteSessionRecord of SessionRecord
| ReadSessionRecord of DbTag * SessionId
| SessionRecordRead of DbTag * SessionRecord option
| ReadSessionRecords of DbTag
| SessionRecordsRead of DbTag * SessionRecord list
// ── C10. GenPRES Server -> MailService ──
| SendMail of MailAddress * string
// ── GenPRES Server -> GenPRES Client (replies only: Consequence 6) ──
| SessionOpened of
SessionId * SessionNo * UserContext option * PatientContext * OrderContext list * OpenedToken
| PinRequired of AttemptId // UC-2: choose one, and nothing else is offered
| LaunchRefused // carries no reason, deliberately
| NotAuthorised // the registry says no; no reason either
| AuthorityUnavailable // the registry cannot say
| ServerUnreachable
/// Rule 10's one telling. The mark is what ended it.
| SessionEnded of EndMark option // None: the Server has no such record
/// The request is refused because the Session is not open — but the User has
/// already been told why, and Rule 10 says never twice.
| SessionRefused
| PriorSessionNotice of (SessionNo * SessionState) list // Rule 10
/// Rule 31. The answer to `Compute`, computed from the payload and kept nowhere.
| Computed of OrderContext list
| CreateBlocked of TreatmentPlanId // Rules 20, 36
/// Rule 21: whose work, not its contents. Rule 34: and the token that names what
/// was disclosed, which is what a choice to create anyway must return.
| UnsignedWorkNotice of UserContext * NoticeToken
/// Rules 32, 33. The payload contradicted the SessionRecord, or the token did not
/// verify. Carries a reason for the trace; the Client shows nothing but a refusal.
| CreateRefused of string
| TreatmentPlanCreated of TreatmentPlanId * bool * OpenedToken
| TreatmentPlanOpened of TreatmentPlanId * OrderContext list * OpenedToken
| PinRejected of int // Rule 27: attempts left
| NoTreatmentPlanHere // Rule 12
| NotPermitted // Roles: a Reader never creates a TreatmentPlan
| PinReset // UC-7 step 2
// ── any actor -> Environment (standing in for the audit log) ──
/// An envelope no edge permits. Not merely dropped: a forged or misrouted
/// envelope is exactly the event worth alerting on.
| Refused of Envelope
/// Rule 26's other half — "records the change". The mail is the User-facing
/// notice; this is the record.
| Noted of string
and Envelope =
{
From : ActorId
To : ActorId
Msg : Msg
}
// ───────────────────────────── actor state ─────────────────────────────
/// The Broker's own record. It has a lifecycle — issued when, spent or not — that no
/// message carries. GenPRES never sees it, only the LaunchAssertion projected from
/// it, which deliberately drops the credential and the spent flag.
type LaunchRecord =
{
Credential : LaunchCredential
No : LaunchNo
Login : LoginName
Patient : PatientId option
IssuedAt : int
Redeemed : bool
}
/// Actor 1 [given]. Invariant 1: at most one active Patient at a time.
type WorkstationState =
{
ActiveUser : LoginName option
ActivePatient : PatientId option
NextTab : int
}
/// Actor 8. Under SMART on FHIR this would be the EHR's authorisation server.
type BrokerState =
{
Launches : Map<LaunchCredential, LaunchRecord>
NextNo : int
Up : bool
}
/// Actor 9. Says who a login belongs to, what that person may do, and how to reach
/// them by mail. The only source of a Role (Rule 5).
type RegistryState =
{
Users : Map<LoginName, UserContext * MailAddress>
Up : bool
}
/// Actor 6 [given]. Read-only, and read once per launch (Concept 2).
type PlatformState =
{
Data : Map<PatientId, PatientData>
Up : bool
}
/// Actor 5. The Server is its only writer. Open Question 2 concerns a copy of this
/// held by the PatientDataPlatform.
///
/// `NextPlan` lives here, not in the Server: Rule 36 makes the Database the party
/// that decides whether an append lands, so it is also the party that can hand out an
/// ordering. More than one Server may run; only one Database does.
type DatabaseState =
{
Sessions : SessionRecord list // Concept 9
Records : Map<PatientId, PatientRecord> // Concept 12
Credentials : Map<LoginName, UserCredential> // Concept 7
NextPlan : int
}
/// One launch attempt, mid-flight. The stages follow UC-1's trace, and the order is
/// the document's, not a convenience:
/// Rule 24 the PIN is offered only after the registry has recognised the login
/// Rule 25 a Reader skips the credential stage entirely
/// ext 1a no Patient: the platform and record stages are skipped
/// ext 11a the platform being unreachable is not a failure
/// The credential is handed to the Broker and not kept: after ResolveLaunch, GenPRES
/// holds only the launch number, which is safe to log and safe to store.
type LaunchCtx =
{
Client : ActorId
Launch : LaunchNo
Assertion : LaunchAssertion
}
/// A launch in flight, with the tick it reached this stage. The tick is what makes an
/// abandoned launch collectable: everything here is waiting on a round trip that
/// should return promptly, except AwaitingPinChoice, which waits on a human (UC-2).
///
/// This table has always had the shape Rule 31 asks for: per-attempt, and nothing
/// retained once the reply goes out. It is not Session state.
type PendingLaunch =
| AwaitingAssertion of client: ActorId
| AwaitingUser of LaunchCtx
| AwaitingCredential of LaunchCtx * UserContext * MailAddress
/// UC-2. The launch is suspended on a human and may stay here indefinitely.
| AwaitingPinChoice of LaunchCtx * UserContext * MailAddress
| AwaitingPinWritten of LaunchCtx * UserContext * MailAddress
| AwaitingPatientData of LaunchCtx * UserContext * MailAddress
| AwaitingRecord of LaunchCtx * UserContext * MailAddress * PatientContext
/// Rule 7 needs the User's other SessionRecords, and the Server no longer mirrors
/// them — so closing the rest is a Database leg like any other.
| AwaitingPriors of LaunchCtx * UserContext * MailAddress * PatientContext * TreatmentPlan option
/// One entry in the Server's launch table.
type PendingEntry =
{
Stage : PendingLaunch
Since : int
}
/// How far one in-Session request has got through its Database legs. Every stage
/// carries what the earlier legs returned, because there is nowhere else to keep it:
/// the Server holds nothing between requests (Rule 31), and this table is emptied by
/// the reply.
type RequestStage =
/// Rule 32: before anything else, who and which Patient this Session is.
| AwaitingSessionRecord
/// Rules 17 to 21 are decided against the PatientRecord.
| AwaitingPatientRecord of SessionRecord
/// Rule 22, carrying the record, the head the Rule 20 check saw, and the base.
| AwaitingUserCredential of SessionRecord * PatientRecord * TreatmentPlan option
/// Rule 36: the Database is deciding whether the append lands.
| AwaitingAppend of SessionRecord
/// UC-7 step 2. Rule 26 mails the address on the record, so the record is held.
| AwaitingPinRemoved of SessionRecord
/// Rule 31 made visible: one entry per request in flight, created when the request
/// arrives and removed with its reply. Nothing here survives the answer.
type RequestCtx =
{
Sid : SessionId
Client : ActorId
Cmd : SessionCmd
Stage : RequestStage
}
/// Actor 4. Counters, what is in flight, and whether it is up — and nothing else.
/// That is Rule 31 as a type: there is no field a Session could live in.
type ServerState =
{
/// One entry per in-Session request, gone with the reply.
InFlight : Map<RequestId, RequestCtx>
/// One entry per launch attempt, gone with the launch.
Pending : Map<AttemptId, PendingEntry>
/// Separate id spaces, so separate counters. All monotonic — an id is never
/// reissued. The TreatmentPlan counter is not here: Rule 36 moved it to the
/// Database, which is the party that orders a PatientRecord.
NextAttempt : int
NextRequest : int
NextSessionId : int
Up : bool
}
/// Actor 3. Carries no identity of its own: a User is only known through a launch.
/// It does carry the work, though — the cart is here and nowhere else (Rule 31), so
/// this is where a Session's contents survive a Server restart, and where they die
/// when the browser does.
type BrowserState =
{
/// Consequence 4: the credential is in the address bar, and stays there.
UrlCredential : LaunchCredential option
/// Rule 11: a bearer credential, held here and sent in the request.
Sid : SessionId option
/// What the Server said this Session's User and Patient are (Concepts 1, 2).
/// Shown to the User; never sent back as an assertion — Rule 32 takes both
/// from the SessionRecord.
User : UserContext option
Patient : PatientId option
/// The cart (Concept 15). Travels with every request and lives nowhere else.
Working : OrderContext list
Data : PatientData option
/// Rule 33. Issued by the Server, returned with every create.
Opened : OpenedToken option
/// Rule 34. Kept from the last UnsignedWorkNotice, returned to create anyway.
Notice : NoticeToken option
/// The attempt this Client was asked to choose a PIN for (UC-2).
AwaitingPin : AttemptId option
/// Rule 6: whether a fresh anonymous open is on offer.
AnonymousOffer : bool
/// Whatever the Client is currently putting in front of the User. Not only
/// notices: a question (Rule 21), a prompt (UC-2), an unavailability. The
/// Session-ended notice of Rule 10 is one of the things that can land here.
Showing : string option
Closed : bool
}
/// The world the participants run in, not a participant's own state. It disappears
/// in production: real time arrives as Tick.
type EnvState =
{
Now : int
}
/// Every field is state owned by exactly one participant — Clients per key — except
/// Env, which is the world they all run in. Nothing is shared, so nothing in the
/// model can depend on a memory read across what will be a process boundary. The
/// rule is a convention over the reducer, not something the type enforces: only the
/// branch bodies decide who reads what.
type Hospital =
{
Workstation : WorkstationState
Broker : BrokerState
Registry : RegistryState
Platform : PlatformState
Database : DatabaseState
GenPres : ServerState
Clients : Map<BrowserId, BrowserState>
Mail : (MailAddress * string) list // what the MailService sent
Audit : string list // Rule 26's "records the change"
Env : EnvState
}
// ═══════════════════════════════════════════════════════════════════════════════
// 2. MODULES
// ═══════════════════════════════════════════════════════════════════════════════
// ───────────────────────────── configuration ─────────────────────────────
// Rules 28, 29, 30. Owned by the actor named in the comment, not by the model.
// The unit is one handled message: `update` advances the clock on every move, so a
// lifetime has to be read against the length of a cascade, not a count of Ticks — a
// launch from trigger to open Session is some twenty-odd of them.
/// Rule 28. Long enough to carry one launch — a page load and a retry or two.
/// The Broker owns this; GenPRES never sees it.
let credentialTtl = 20
/// Rule 29. Long enough to span the gaps between a clinician's actions.
let sessionTtl = 25
/// Rule 30. Small enough to make guessing hopeless, large enough to forgive
/// mistyping. Owned by GenPRES.
let wrongPinLimit = 3
// ───────────────────────────── the edge table ─────────────────────────────
/// The document's notation, as data.
type EdgeKind =
| Request // X -> Y initiate, and receive Y's reply
| Launch // X => Y one-way: no response, no error path
| Interact // X <-> Y read what Y shows, and act on it
module Edges =
/// The document's Constraints section, verbatim. Anything not here cannot
/// exchange data at all, and edges do not compose.
let table : (ActorId * EdgeKind * ActorId) list =
[
// User Interaction
User, Interact, MainEhrWorkstation // U1
User, Interact, MainEhrLaunchScript // U2
User, Interact, GenPresClient(BrowserId 0) // U3
// Communication
MainEhrWorkstation, Request, UserRegistry // C1
MainEhrWorkstation, Request, PatientDataPlatform // C2
MainEhrLaunchScript, Request, Broker // C3
MainEhrLaunchScript, Launch, GenPresClient(BrowserId 0) // C4
GenPresClient(BrowserId 0), Request, GenPresServer // C5
GenPresServer, Request, Broker // C6
GenPresServer, Request, UserRegistry // C7
GenPresServer, Request, PatientDataPlatform // C8
GenPresServer, Request, GenPresDatabase // C9
GenPresServer, Request, MailService // C10
// U2 is `<->` and not `=>`: the LaunchScript reports the one failure it
// can see — the Broker exchange — before it exits (UC-1 ext 3a). What
// bounds it is not the edge but its own lifetime: it exits at the launch,
// so nothing later ever comes from it (Consequence 1). The edge that
// carries Consequence 1 is C4, which stays `=>`.
]
/// Clients differ by BrowserId; edges do not.
let private tag =
function
| GenPresClient _ -> GenPresClient(BrowserId 0)
| a -> a
let private has kind a b =
table |> List.exists (fun (x, k, y) -> k = kind && x = tag a && y = tag b)
/// May `from` put this envelope on the wire to `to_`?
///
/// A Request edge permits both the initiation and the reply that comes back on
/// the same connection. A Launch edge permits the one direction only — which is
/// what makes Consequence 1 true by construction: nothing can ever be sent back
/// to the LaunchScript, because no edge carries it.
let permits from to_ =
// Environment is not a use case actor: it is the clock and the power switch,
// and every actor may write to the audit log.
if from = Environment || to_ = Environment then true
elif has Interact from to_ || has Interact to_ from then true
elif has Launch from to_ then true
elif has Request from to_ then true
elif has Request to_ from then true // the reply leg
else false
// ───────────────────────────── the record rules ─────────────────────────────
/// Rules 16 to 21. Small total functions over a TreatmentPlan list held newest first, so
/// "most recent" is `List.tryFind` and "newer than" is a comparison of TreatmentPlanNo.
module PatientRecord =
let empty patient = { Patient = patient; Plans = [] }
let private no (s: TreatmentPlan) = let (TreatmentPlanNo n) = s.No in n
/// Rule 36's half of the check: what the Server saw as the head when it decided.
let head (r: PatientRecord) = r.Plans |> List.tryHead |> Option.map _.Id
/// "newer than the TreatmentPlan the User opened with" — and where the User opened
/// with nothing, any TreatmentPlan at all counts as newer (Rule 21's parenthesis).
let private newerThan (openedWith: TreatmentPlanId option) (s: TreatmentPlan) (r: PatientRecord) =
match openedWith with
| None -> true
| Some id ->
match r.Plans |> List.tryFind (fun x -> x.Id = id) with
| Some baseline -> no s > no baseline
| None -> true // the baseline is not in this record at all
/// Rule 16. The only TreatmentPlan that counts clinically.
let latestSigned (r: PatientRecord) =
r.Plans |> List.tryFind _.Signed
/// Rule 19. Where neither exists, the User works from nothing. A Reader never
/// creates a TreatmentPlan, so this can only ever hand them the latest Signed one.
let startsFrom (u: UserId) (r: PatientRecord) =
r.Plans
|> List.tryFind (fun s -> s.Signed || s.By.UserId = u)
/// Rules 17 and 18. The most recent Signed TreatmentPlan is the only one another User
/// can open — older TreatmentPlans are record, not views — and an Unsigned TreatmentPlan
/// opens only for the User who created it.
let mayOpen (u: UserId) (id: TreatmentPlanId) (r: PatientRecord) =
match r.Plans |> List.tryFind (fun s -> s.Id = id) with
| None -> None
| Some s when s.Signed ->
if latestSigned r |> Option.map _.Id = Some id then Some s else None
| Some s -> if s.By.UserId = u then Some s else None
/// Rule 20. A Signed TreatmentPlan newer than the one the User opened with blocks the
/// create — and opening that Signed TreatmentPlan lifts the block, because it becomes
/// the one the Session opened with.
let blocking (openedWith: TreatmentPlanId option) (r: PatientRecord) =
latestSigned r |> Option.filter (fun s -> newerThan openedWith s r)
/// Rule 21, and Rule 34's half of it: *every* Unsigned TreatmentPlan of another User
/// newer than the one opened with, because the notice token names what was
/// disclosed and is honoured for nothing newer. Newest first.
let unsignedElsewhere (u: UserId) (openedWith: TreatmentPlanId option) (r: PatientRecord) =
r.Plans
|> List.filter (fun s ->
not s.Signed && s.By.UserId <> u && newerThan openedWith s r)
/// Concept 12: append-only. The newest TreatmentPlan goes on the front, and no
/// existing one is ever touched.
let append (s: TreatmentPlan) (r: PatientRecord) =
{ r with Plans = s :: r.Plans }
// ───────────────────────────── the credential ─────────────────────────────
/// Concept 7 and Rule 27.
module UserCredential =
let fresh login = { Login = login; Pin = None; AttemptCount = 0 }
/// Rule 26: a newly set PIN starts with a count of zero.
let setPin pin c = { c with Pin = Some pin; AttemptCount = 0 }
/// UC-7 step 2: the UserCredential stays, now without a PIN. Concept 7: one
/// without a PIN cannot sign.
let removePin c = { c with Pin = None; AttemptCount = 0 }
/// Rule 22: verification happens here and nowhere else. Rule 27: a correct entry
/// resets the count, a wrong one advances it.
let verify (pin: Pin) (c: UserCredential) =
match c.Pin with
| Some p when p = pin -> true, { c with AttemptCount = 0 }
| _ -> false, { c with AttemptCount = c.AttemptCount + 1 }
/// Rule 27: a wrong entry at the limit ends the Session (Rule 9).
let atLimit c = c.AttemptCount >= wrongPinLimit
let attemptsLeft c = max 0 (wrongPinLimit - c.AttemptCount)
// ───────────────────────────── the session record ─────────────────────────────
module SessionRecord =
/// Rule 10, on the one axis that decides it: a User who closed was offered the
/// save, so there is nothing to tell them. Every other ending owes a notice.
/// Three branches, not four: a Server restart is no longer an ending (Rule 9).
let owesNotice =
function
| ClosedByUser -> false
| Idle | Superseded | WrongPinLimit -> true
/// Ending is idempotent: an already settled record is left alone, so the first
/// mark is the one that stands — and so is the obligation it created.
let endWith mark now (s: SessionRecord) =
match s.State with
| Ended _ -> s
| OpenOrGone ->
{ s with
State = Ended(mark, now)
Notice = if owesNotice mark then Owed else NotOwed }
/// Rule 10. Told once, never twice — now a single field, not a pair that could
/// disagree with `State`.
let tellsAtNextOpportunity (s: SessionRecord) = s.Notice = Owed
/// Whether ending this record now would leave the User owed a notice: either it
/// is still open, and this launch is about to close it (Rule 7), or it ended
/// earlier in a way nobody has yet mentioned.
let wouldOweNotice (s: SessionRecord) =
match s.State with
| OpenOrGone -> true
| Ended _ -> tellsAtNextOpportunity s
/// Spends the one telling the User gets. Idempotent, and silent where nothing was
/// owed — there is no way to be told twice.
let told now (s: SessionRecord) =
match s.Notice with
| Owed -> { s with Notice = Told now }
| NotOwed
| Told _ -> s
/// Rule 8. The idle clock lives on the record, because it is the only thing that
/// outlives a request.
let seen now (s: SessionRecord) = { s with LastSeen = now }
let isOpen (s: SessionRecord) = s.State = OpenOrGone
let userId (s: SessionRecord) = s.User |> Option.map _.UserId
// ───────────────────────────── the tokens ─────────────────────────────
/// Rules 33 and 34. The Client holds the cart, so anything the Server must be able to
/// trust about a create has to be something the Client cannot forge. Both tokens are
/// the same trick: the Server states a fact, signs it, and refuses to believe the
/// fact unless the signature comes back with it.
///
/// `secret` stands in for the key. It is `private`, so nothing outside this module —
/// no scenario, no forgery test — can compute a mac. That is the point: the tests
/// below can build a token with the right fields and a wrong mac, and watch it fail.
module Token =
let private secret = "hmac-key-known-only-to-the-server"
let private sid (SessionId s) = s
let private pat = function Some(PatientId p) -> p | None -> "-"
let private snap = function Some(TreatmentPlanId s) -> s | None -> "-"
let private macOpened s p n =
$"mac|%s{secret}|opened|%s{sid s}|%s{pat p}|%s{snap n}"
let private macNotice s (ids: TreatmentPlanId list) =
let named = ids |> List.map (fun (TreatmentPlanId i) -> i) |> List.sort |> String.concat ","
$"mac|%s{secret}|notice|%s{sid s}|%s{named}"
/// Rule 33. Minted at the opening of a Session, and re-minted whenever the
/// baseline moves: an open (Rule 17) or a create both make a new TreatmentPlan the one
/// Rules 20 and 21 are measured from.
let mintOpened s p n : OpenedToken =
{ Sid = s; Patient = p; Plan = n; Mac = macOpened s p n }
/// Rule 34. Minted with the notice, naming exactly the Unsigned TreatmentPlans it
/// disclosed.
let mintNotice s (ids: TreatmentPlanId list) : NoticeToken =
{ Sid = s; Disclosed = ids; Mac = macNotice s ids }
/// Recompute and compare. A token whose fields were edited no longer matches its
/// mac, and a token whose mac was guessed does not match its fields.
let verifyOpened (t: OpenedToken) =
t.Mac = macOpened t.Sid t.Patient t.Plan
let verifyNotice (t: NoticeToken) =
t.Mac = macNotice t.Sid t.Disclosed
// ───────────────────────────── the reducer ─────────────────────────────
module Hospital =
let empty =
{
Workstation = { ActiveUser = None; ActivePatient = None; NextTab = 1 }
Broker = { Launches = Map.empty; NextNo = 1; Up = true }
Registry = { Users = Map.empty; Up = true }
Platform = { Data = Map.empty; Up = true }
Database =
{
Sessions = []
Records = Map.empty
Credentials = Map.empty
NextPlan = 1
}
GenPres =
{
InFlight = Map.empty
Pending = Map.empty
NextAttempt = 1
NextRequest = 1
NextSessionId = 1
Up = true
}
Clients = Map.empty
Mail = []
Audit = []
Env = { Now = 0 }
}
let blankClient =
{
UrlCredential = None
Sid = None
User = None
Patient = None
Working = []
Data = None
Opened = None
Notice = None
AwaitingPin = None
AnonymousOffer = false
Showing = None
Closed = false
}
let private onClient id f h =
let current = h.Clients |> Map.tryFind id |> Option.defaultValue blankClient
{ h with Clients = h.Clients |> Map.add id (f current) }
let private clientState id h =
h.Clients |> Map.tryFind id |> Option.defaultValue blankClient
let private send from to_ msg = { From = from; To = to_; Msg = msg }
let private pend now stage = { Stage = stage; Since = now }
// ── the in-flight table (Rule 31) ──
let private putFlight rid ctx (h: Hospital) =
{ h with GenPres.InFlight = h.GenPres.InFlight |> Map.add rid ctx }
let private dropFlight rid (h: Hospital) =
{ h with GenPres.InFlight = h.GenPres.InFlight |> Map.remove rid }
/// Rule 26, both halves: the User is mailed, and the change is recorded.
let private pinChanged (mail: MailAddress option) (what: string) =
[
match mail with
| Some m -> send GenPresServer MailService (SendMail(m, what))
| None -> ()
send GenPresServer Environment (Noted what)
]
// ── Rule 35: the stamps are the Server's to compute ──
/// Rule 14 says an OrderContext changed in the Session is stamped with the
/// Session's User and an unchanged one keeps the stamp it had. With the cart in
/// the Client (Rule 31) there is no Session to ask what changed, and no reason to
/// believe a Client that says so — so the Server diffs the payload against the
/// base TreatmentPlan by OrderContextId. Same id and same content: the base's stamp
/// stands. New id, or changed content: this User's stamp. Whatever stamp arrived
/// is discarded unread (Rule 35).
let private stampAgainst (uc: UserContext) (basePlan: TreatmentPlan option) (orders: OrderContext list) =
let baseline = basePlan |> Option.map _.Orders |> Option.defaultValue []
orders
|> List.map (fun o ->
match baseline |> List.tryFind (fun b -> b.Id = o.Id) with
| Some b when b.Content = o.Content -> { o with Stamp = b.Stamp }
| _ -> { o with Stamp = Some uc })
// ── the launch, and what ends it ──
/// UC-1 steps 13 and 14, and the last step of the anonymous open. Rule 19 has
/// already picked the TreatmentPlan the Session starts from, if there is one, and Rule
/// 7's other Sessions of this User have already been read back from the Database
/// — the Server keeps no copy of them (Rule 31).
let private openSession
(client: ActorId)
(launch: LaunchNo option)
(user: UserContext option)
(mail: MailAddress option)
(pctx: PatientContext)
(start: TreatmentPlan option)
(others: SessionRecord list)
(h: Hospital) =
let sid = SessionId $"sid-%04i{h.GenPres.NextSessionId}"
let no = SessionNo h.GenPres.NextSessionId
// Rules 7 and 10 both speak of the Session's User, so neither applies to an
// anonymous open (Rule 13). Rule 7 is per User, not per Patient: this closes
// every other Session of *this* User, whichever Patient it was opened for,
// and closes nobody else's.
let priors =
match user with
| None -> []
| Some uc ->
others
|> List.filter (fun r ->
SessionRecord.userId r = Some uc.UserId && SessionRecord.wouldOweNotice r)
// endWith leaves an already settled record alone, so a Session that
// idled out keeps Idle — and keeps the obligation that ending created,
// which this launch is the opportunity to discharge.
|> List.map (
SessionRecord.endWith Superseded h.Env.Now
>> SessionRecord.told h.Env.Now)
let orders = start |> Option.map _.Orders |> Option.defaultValue []
let record =
{
Id = sid
No = no
User = user
Mail = mail
Patient = pctx.Patient
Launch = launch
OpenedAt = h.Env.Now
LastSeen = h.Env.Now
State = OpenOrGone
Notice = NotOwed
}
// Rule 33. The Client gets the TreatmentPlan the Session opened with as something
// it can hand back but not make.
let token = Token.mintOpened sid pctx.Patient (start |> Option.map _.Id)
{ h with GenPres.NextSessionId = h.GenPres.NextSessionId + 1 },
[
send GenPresServer GenPresDatabase (WriteSessionRecord record)
for r in priors do
send GenPresServer GenPresDatabase (WriteSessionRecord r)
send GenPresServer client (SessionOpened(sid, no, user, pctx, orders, token))
if not priors.IsEmpty then
send GenPresServer client
(PriorSessionNotice(priors |> List.map (fun r -> r.No, r.State)))
]
/// UC-1 steps 11 and 12, and where they are skipped. A Reader arrives here
/// straight from the registry (Rule 25); a Prescriber only once the PIN question
/// is settled (Rules 23, 24).
let private afterCredential att (ctx: LaunchCtx) uc mail (h: Hospital) =
match ctx.Assertion.Patient with
| None ->
// ext 1a: no Patient, so no data to fetch and no record to read. Rule 7
// still applies — this User's other Sessions close — so the SessionRecords
// are still read.
let pctx = { Patient = None; Data = None }
{ h with
GenPres.Pending =
h.GenPres.Pending
|> Map.add att (pend h.Env.Now (AwaitingPriors(ctx, uc, mail, pctx, None))) },
[ send GenPresServer GenPresDatabase (ReadSessionRecords(ForLaunch att)) ]
| Some p ->
{ h with
GenPres.Pending =
h.GenPres.Pending |> Map.add att (pend h.Env.Now (AwaitingPatientData(ctx, uc, mail))) },
[ send GenPresServer PatientDataPlatform (ReadPatientData(att, p)) ]
/// Rule 6. A launch that cannot be honoured opens no Session. There is no silent
/// fallback; where relaunching would not cure it, the Client is left to offer a
/// fresh anonymous open, which carries nothing over.
let private refuseLaunch att client reply (h: Hospital) =
{ h with GenPres.Pending = h.GenPres.Pending |> Map.remove att },
[ send GenPresServer client reply ]
// ── creating a TreatmentPlan: one request, several Database legs, no Session state ──
/// Rule 36. The Server hands over the head its Rule 20 check saw; the Database
/// appends only if that is still the head. The draft has no Id — that is the
/// Database's to mint, because the Database is what orders the record.
let private appendDraft
rid (ctx: RequestCtx) (r: SessionRecord) (pr: PatientRecord)
(basePlan: TreatmentPlan option) (uc: UserContext) (pin: Pin option)
(orders: OrderContext list) (h: Hospital) =
match r.Patient with
| None -> dropFlight rid h, [ send GenPresServer ctx.Client NoTreatmentPlanHere ] // Rule 12
| Some p ->
let draft =
{
Patient = p // Guarantee 1, Rule 32
By = uc // Rule 14
Base = basePlan |> Option.map _.Id // Concept 13
Orders = orders |> stampAgainst uc basePlan // Rule 35
Signed = pin.IsSome // Rules 15, 16
}
h |> putFlight rid { ctx with Stage = AwaitingAppend r },
[ send GenPresServer GenPresDatabase (AppendIf(ForRequest rid, PatientRecord.head pr, draft)) ]
/// Rules 20 and 21, in that order, then the PIN (Rule 22). UC-3 ext 3c fixes the
/// order: signing without saving first is one act, and the block and the
/// notification are settled before the User is ever asked for a PIN.
let private decideCreate rid (ctx: RequestCtx) (r: SessionRecord) (pr: PatientRecord) (h: Hospital) =
match ctx.Cmd, r.User with
| CreateTreatmentPlan(pin, orders, _, opened, notice), Some uc ->
let openedWith = opened.Plan
let basePlan = pr.Plans |> List.tryFind (fun s -> Some s.Id = openedWith)
match PatientRecord.blocking openedWith pr with
| Some blocker ->
// Rule 20. The remedy is to open that Signed TreatmentPlan (Rule 17), which
// makes it the one the Session opened with and lifts the block.
dropFlight rid h, [ send GenPresServer ctx.Client (CreateBlocked blocker.Id) ]
| None ->
let outstanding = pr |> PatientRecord.unsignedElsewhere uc.UserId openedWith
// Rule 34. The token is honoured for exactly the Unsigned TreatmentPlans
// the notice disclosed, and for nothing newer. A token the Client made
// itself does not verify, so it counts as none at all.
let honoured =
match notice with
| Some t when Token.verifyNotice t && t.Sid = ctx.Sid -> Set.ofList t.Disclosed
| _ -> Set.empty
match outstanding |> List.filter (fun s -> not (honoured.Contains s.Id)) with
| undisclosed :: _ ->
// Rule 21. Whose work it is, not its contents. The User may still
// say no, and saying yes means coming back with this token.
let token = Token.mintNotice ctx.Sid (outstanding |> List.map _.Id)
dropFlight rid h,
[ send GenPresServer ctx.Client (UnsignedWorkNotice(undisclosed.By, token)) ]
| [] ->
match pin with
| None -> appendDraft rid ctx r pr basePlan uc None orders h // a save: Unsigned
| Some _ ->
// Rule 22: the Server is the only party that verifies, so the
// credential has to be fetched before anything is signed.
h |> putFlight rid { ctx with Stage = AwaitingUserCredential(r, pr, basePlan) },
[ send GenPresServer GenPresDatabase (ReadCredential(ForRequest rid, uc.Login)) ]
| _ -> dropFlight rid h, []
/// The SessionRecord has come back, the Session is open, and Rule 8's clock has
/// been refreshed. This is where Rule 32 bites: the User and the Patient of the
/// request are read off the record, and the payload is believed about nothing
/// else. Concept 15 — what a User may do inside a Session, and what they may not.
let private dispatch rid (ctx: RequestCtx) (r: SessionRecord) (h: Hospital) =
let refuse msg = dropFlight rid h, [ send GenPresServer ctx.Client msg ]
/// Rule 12: a Session without a PatientId lets the User prescribe, Patient
/// Data included, but a TreatmentPlan cannot be opened or created.
let withPatient f =
match r.Patient with
| None -> refuse NoTreatmentPlanHere
| Some p -> f p
/// Roles: a Reader may never create a TreatmentPlan. Rule 13: an anonymous Session
/// has no User at all, so there is nobody to create as and nobody to sign as.
let withPrescriber f =
match r.User with
| Some uc when uc.Role = Prescriber -> f uc
| _ -> refuse NotPermitted
match ctx.Cmd with
| Compute orders ->
// Rule 31. The answer is computed from the payload and nothing is kept —
// the cart went home with the reply, as it arrived with the request.
dropFlight rid h, [ send GenPresServer ctx.Client (Computed orders) ]
| CloseSession ->
// Rule 9: closing is an explicit act in the Client. Rule 10 adds nothing
// — it speaks only of endings other than by the User.
let ended = r |> SessionRecord.endWith ClosedByUser h.Env.Now
dropFlight rid h, [ send GenPresServer GenPresDatabase (WriteSessionRecord ended) ]
| ResetPin ->
// UC-7 step 2. The UserCredential stays, now without a PIN; Concept 7 says
// one without a PIN cannot sign.
match r.User with
| None -> refuse NotPermitted
| Some uc ->
h |> putFlight rid { ctx with Stage = AwaitingPinRemoved r },
[ send GenPresServer GenPresDatabase (RemovePin(ForRequest rid, uc.Login)) ]
| OpenTreatmentPlan _ ->
withPatient (fun p ->
match r.User with
| None -> refuse NotPermitted // Rule 13
| Some _ ->
h |> putFlight rid { ctx with Stage = AwaitingPatientRecord r },
[ send GenPresServer GenPresDatabase (ReadRecord(ForRequest rid, p)) ])
| CreateTreatmentPlan(_, orders, _, opened, _) ->
withPatient (fun p ->
withPrescriber (fun _ ->
// Rule 33. The Client cannot make an opened-with token, and this
// is where that is worth something: the baseline Rules 20 and 21
// are measured from is the Server's own word, handed back.
if not (Token.verifyOpened opened) then
refuse (CreateRefused "the opened-with token does not verify (Rule 33)")
elif opened.Sid <> ctx.Sid || opened.Patient <> r.Patient then
refuse (CreateRefused "the opened-with token is for another Session (Rule 33)")
// Rule 32 and Guarantee 1. The PatientId is the one thing no
// TreatmentPlan may change, and the payload does not get a vote on it.
elif orders |> List.exists (fun o -> o.Patient <> None && o.Patient <> Some p) then
refuse (CreateRefused "an OrderContext names another Patient (Rule 32)")
else
h |> putFlight rid { ctx with Stage = AwaitingPatientRecord r },
[ send GenPresServer GenPresDatabase (ReadRecord(ForRequest rid, p)) ]))
// ══════════════════════════════════════════════════════════════════════════
// The reducer proper. Dispatch names the sender as well as the recipient, so
// every branch states who may send it. Whether the two may exchange anything
// at all was already settled by the edge table, in `run`, before we get here.
// ══════════════════════════════════════════════════════════════════════════
let rec update (h: Hospital) (env: Envelope) : Hospital * Envelope list =
// every move takes a tick of time
let h = { h with Env.Now = h.Env.Now + 1 }
match env.From, env.To, env.Msg with
// ── the audit log, and the person ──
// Recorded, not acted on. Handled first, and never refused itself: refusing a
// refusal would not terminate.
| _, Environment, Refused e ->
let line = $"REFUSED %A{e.From} -> %A{e.To}"
{ h with Audit = line :: h.Audit }, []
| _, Environment, Noted what -> { h with Audit = what :: h.Audit }, []
// A person reads what is sent to them; there is no state to change.
| _, User, _ -> h, []
// ── the clock ──
// The clock is advanced by the prefix above, on this envelope like any other,
// so a Tick adds nothing of its own: it exists to reach the Server, whose
// sweep runs on nothing else.
| Environment, Environment, Tick ->
h, [ send Environment GenPresServer Tick ]
// ── infrastructure ──
| Environment, Broker, Stop _ -> { h with Broker.Up = false }, []
| Environment, Broker, Start _ -> { h with Broker.Up = true }, []
| Environment, UserRegistry, Stop _ -> { h with Registry.Up = false }, []
| Environment, UserRegistry, Start _ -> { h with Registry.Up = true }, []
| Environment, PatientDataPlatform, Stop _ -> { h with Platform.Up = false }, []
| Environment, PatientDataPlatform, Start _ -> { h with Platform.Up = true }, []
// Rule 9: a Server restart ends nothing. There is no Session state to lose —
// identity and standing are in the SessionRecords, the work is in the Clients
// (Rule 31). What does go is what was in flight at that instant: requests
// half-way through their Database legs, and launches half-way through theirs.
// Their Clients see the same silence as any other unreachable Server.
| Environment, GenPresServer, Stop _ when h.GenPres.Up ->
{ h with
GenPres =
{ h.GenPres with
InFlight = Map.empty
Pending = Map.empty
Up = false } }, []
// And coming back settles nothing either: no records to read, nothing to mark.
| Environment, GenPresServer, Start _ when not h.GenPres.Up ->
{ h with GenPres.Up = true }, []
| Environment, GenPresServer, (Start _ | Stop _) -> h, []
// A Server that is down answers its clients and does nothing else. Ordering
// matters twice over: this pair must sit above every other Server branch, and
// the client-facing case must be the narrow one. A reply from the Broker, the
// registry, the platform or the Database is an in-flight answer to a Server
// that is gone — dropped, not answered. Ticks are dropped too: a down Server
// runs no sweeps.
| _, GenPresServer,
(RedeemLaunch _ | OpenAnonymous | SupplyPin _ | SessionRequest _) when not h.GenPres.Up ->
h, [ send GenPresServer env.From ServerUnreachable ]
| _, GenPresServer, _ when not h.GenPres.Up -> h, []
// ── Rule 9: the idle sweep ──
// The clock a Session is swept against is on its SessionRecord (Rule 8), and
// the records are in the Database (Rule 31), so the sweep is a read like any
// other rather than a walk over something the Server holds.
| Environment, GenPresServer, Tick ->
let now = h.Env.Now
// A launch nobody is coming back for. Every stage is waiting on a round
// trip that should return promptly — except AwaitingPinChoice, which the
// document suspends on a human and which may therefore sit for as long as
// it likes (UC-2 step 3). Bounded by Rule 29's constant: Rule 28's belongs
// to the Broker, and GenPRES never sees it.
let abandoned (p: PendingEntry) =
match p.Stage with
| AwaitingPinChoice _ -> false
| _ -> now - p.Since > sessionTtl
{ h with
GenPres.Pending =
h.GenPres.Pending |> Map.filter (fun _ p -> not (abandoned p)) },
[ send GenPresServer GenPresDatabase (ReadSessionRecords ForSweep) ]
| GenPresDatabase, GenPresServer, SessionRecordsRead(ForSweep, rs) ->
// Rule 13: an anonymous Session need not idle out — keeping it has no
// consequence — so only a Session bound to a User is swept.
let now = h.Env.Now
let stale =
rs
|> List.filter (fun r ->
SessionRecord.isOpen r && r.User.IsSome && now - r.LastSeen > sessionTtl)
h,
[ for r in stale ->
send GenPresServer GenPresDatabase
(WriteSessionRecord(r |> SessionRecord.endWith Idle now)) ]
// ── Actor 1: the MainEHR Workstation ──
| User, MainEhrWorkstation, LogIn u -> { h with Workstation.ActiveUser = Some u }, []
| User, MainEhrWorkstation, SelectPatient p -> { h with Workstation.ActivePatient = Some p }, []
| User, MainEhrWorkstation, ClearPatient -> { h with Workstation.ActivePatient = None }, []
// ── Actor 2: the MainEHR LaunchScript ──
// Rule 1: the LaunchScript decides which MainEHR User may run it. It is a
// script behind a button *in* the Workstation, so the login and the active
// Patient are its own context, not something fetched over an edge — there is
// no edge between Actors 1 and 2, and none is needed.
//
// Note what it does NOT do: it never asks about, decides on, or transmits a
// Role. The launch carries a login and a Patient (Concept 3), and the Role
// comes from the UserRegistry at the far end (Rule 5).
| User, MainEhrLaunchScript, TriggerLaunch ->
match h.Workstation.ActiveUser with
| Some u ->
// ext 1a: no active Patient is not an error. The launch goes without
// one, and GenPRES opens with no Patient (Rule 12).
h, [ send MainEhrLaunchScript Broker (PrepareLaunch(u, h.Workstation.ActivePatient)) ]
| None ->
h, [ send MainEhrLaunchScript User (LaunchError "no MainEHR login: nobody to launch as") ]
| Broker, MainEhrLaunchScript, LaunchPrepared cred ->
let tab = BrowserId h.Workstation.NextTab
// The launch, and then the LaunchScript exits. Consequence 1 is not a
// promise made here: edge C4 is `=>`, so nothing can be sent back at all.
{ h with Workstation.NextTab = h.Workstation.NextTab + 1 },
[ send MainEhrLaunchScript (GenPresClient tab) (OpenUrl cred) ]
// UC-1 ext 3a. The one launch failure the EHR side can report: the Broker
// edge is request-response and the LaunchScript has not yet exited.
| Broker, MainEhrLaunchScript, LaunchNotPrepared ->
h, [ send MainEhrLaunchScript User (LaunchError "the Broker is unreachable — stay in MainEHR") ]
// ── Actor 8: the Broker ──
| MainEhrLaunchScript, Broker, PrepareLaunch _ when not h.Broker.Up ->
h, [ send Broker env.From LaunchNotPrepared ]
| GenPresServer, Broker, ResolveLaunch(att, _) when not h.Broker.Up ->
h, [ send Broker env.From (LaunchRejected(att, None, BrokerUnreachable)) ]
| MainEhrLaunchScript, Broker, PrepareLaunch(login, patient) ->
let cred = LaunchCredential $"cred-%04i{h.Broker.NextNo}"
let record =
{
Credential = cred
No = LaunchNo h.Broker.NextNo
Login = login
Patient = patient
IssuedAt = h.Env.Now
Redeemed = false
}
{ h with
Broker.Launches = h.Broker.Launches |> Map.add cred record
Broker.NextNo = h.Broker.NextNo + 1 },
[ send Broker env.From (LaunchPrepared cred) ]
// Rules 2, 3 and 4. Rule 4 is this branch's shape: only the Server appears in
// the From position, so no other party can redeem.
| GenPresServer, Broker, ResolveLaunch(att, cred) ->
let reject no f = [ send Broker env.From (LaunchRejected(att, no, f)) ]
match h.Broker.Launches |> Map.tryFind cred with
| None -> h, reject None NotFound
| Some l when l.Redeemed -> h, reject (Some l.No) AlreadyRedeemed // Rule 2
| Some l when h.Env.Now - l.IssuedAt > credentialTtl ->
h, reject (Some l.No) CredentialExpired // Rule 3
| Some l ->
{ h with
Broker.Launches = h.Broker.Launches |> Map.add cred { l with Redeemed = true } },
[ send Broker env.From
(LaunchResolved(att, l.No, { Login = l.Login; Patient = l.Patient })) ]
// ── Actor 9: the UserRegistry ──
| GenPresServer, UserRegistry, ResolveUser(att, _) when not h.Registry.Up ->
h, [ send UserRegistry env.From (UserUnresolved(att, RegistryUnreachable)) ]
| GenPresServer, UserRegistry, ResolveUser(att, login) ->
match h.Registry.Users |> Map.tryFind login with
| Some(uc, mail) -> h, [ send UserRegistry env.From (UserResolved(att, uc, mail)) ]
| None -> h, [ send UserRegistry env.From (UserUnresolved(att, NoRole)) ]
// ── Actor 6: the PatientDataPlatform ──
// Concept 2: read once, at the launch. Whether it is down or simply holds
// nothing for this Patient makes no difference to the caller (ext 11a).
| GenPresServer, PatientDataPlatform, ReadPatientData(att, p) ->
match (if h.Platform.Up then h.Platform.Data |> Map.tryFind p else None) with
| Some d -> h, [ send PatientDataPlatform env.From (PatientDataRead(att, d)) ]
| None -> h, [ send PatientDataPlatform env.From (PatientDataUnavailable att) ]
// ── Actor 10: the MailService ──
| GenPresServer, MailService, SendMail(addr, what) ->
{ h with Mail = (addr, what) :: h.Mail }, []
// ── Actor 5: the GenPRES Database. The Server is its only writer. ──
| GenPresServer, GenPresDatabase, ReadCredential(tag, login) ->
h, [ send GenPresDatabase env.From (CredentialRead(tag, h.Database.Credentials |> Map.tryFind login)) ]
| GenPresServer, GenPresDatabase, WriteCredential(tag, c) ->
{ h with Database.Credentials = h.Database.Credentials |> Map.add c.Login c },
[ send GenPresDatabase env.From (CredentialWritten(tag, c)) ]
| GenPresServer, GenPresDatabase, ReadRecord(tag, p) ->
let r =
h.Database.Records
|> Map.tryFind p
|> Option.defaultValue (PatientRecord.empty p)
h, [ send GenPresDatabase env.From (RecordRead(tag, r)) ]
// Rule 36. The Rule 20 check and the append are one act, and this is where it
// is made one: the Server states the head its check saw, and the TreatmentPlan
// lands only if that is still the head. More than one Server may run — the
// arbitration is here, not in an assumption that only one of them writes.
//
// Concept 12: append-only. Nothing already in the record is touched. The Id
// and the ordering are minted here, because ordering a record is the same
// authority as deciding what may join it.
| GenPresServer, GenPresDatabase, AppendIf(tag, expected, draft) ->
let r =
h.Database.Records
|> Map.tryFind draft.Patient
|> Option.defaultValue (PatientRecord.empty draft.Patient)
match PatientRecord.head r with
| actual when actual = expected ->
let plan =
{
Id = TreatmentPlanId $"plan-%04i{h.Database.NextPlan}"
No = TreatmentPlanNo h.Database.NextPlan
Patient = draft.Patient
By = draft.By
Base = draft.Base
Orders = draft.Orders
Signed = draft.Signed
At = h.Env.Now
}
{ h with
Database.Records =
h.Database.Records |> Map.add draft.Patient (r |> PatientRecord.append plan)
Database.NextPlan = h.Database.NextPlan + 1 },
[ send GenPresDatabase env.From (TreatmentPlanAppended(tag, plan)) ]
| Some actual ->
h, [ send GenPresDatabase env.From (AppendRefused(tag, actual)) ]
| None ->
// The head the Server saw is gone from an append-only record: cannot
// happen. Refusing is the safe answer, and names what it saw instead.
h, [ send GenPresDatabase env.From (AppendRefused(tag, TreatmentPlanId "none")) ]
| GenPresServer, GenPresDatabase, WriteSessionRecord r ->
let existing = h.Database.Sessions |> List.exists (fun x -> x.Id = r.Id)
{ h with
Database.Sessions =
if existing then h.Database.Sessions |> List.map (fun x -> if x.Id = r.Id then r else x)
else r :: h.Database.Sessions }, []
| GenPresServer, GenPresDatabase, ReadSessionRecord(tag, sid) ->
h,
[ send GenPresDatabase env.From
(SessionRecordRead(tag, h.Database.Sessions |> List.tryFind (fun x -> x.Id = sid))) ]
| GenPresServer, GenPresDatabase, ReadSessionRecords tag ->
h, [ send GenPresDatabase env.From (SessionRecordsRead(tag, h.Database.Sessions)) ]
// UC-7 step 2. Distinct from a WriteCredential so that removing a PIN is
// never confused with the write-back of a wrong-entry count (Rule 27) — the
// two would otherwise look identical once the PIN is gone.
| GenPresServer, GenPresDatabase, RemovePin(tag, login) ->
let c =
h.Database.Credentials
|> Map.tryFind login
|> Option.defaultValue (UserCredential.fresh login)
|> UserCredential.removePin
{ h with Database.Credentials = h.Database.Credentials |> Map.add login c },
[ send GenPresDatabase env.From (PinRemoved(tag, c)) ]
// ══════════════════════════════════════════════════════════════════════
// Actor 4: the GenPRES Server. A launch, leg by leg — UC-1 steps 7 to 14.
// ══════════════════════════════════════════════════════════════════════
// Step 7 into 8. The credential is handed to the Broker and not kept: from
// here on GenPRES holds only the launch number, which is safe to log.
| GenPresClient _, GenPresServer, RedeemLaunch cred ->
let att = AttemptId h.GenPres.NextAttempt
{ h with
GenPres.NextAttempt = h.GenPres.NextAttempt + 1
GenPres.Pending = h.GenPres.Pending |> Map.add att (pend h.Env.Now (AwaitingAssertion env.From)) },
[ send GenPresServer Broker (ResolveLaunch(att, cred)) ]
// Rule 6. A refusal opens nothing. LaunchRefused carries no reason
// deliberately: expired, spent and never-existed are one answer to a Client.
| Broker, GenPresServer, LaunchRejected(att, _, _) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingAssertion client) -> refuseLaunch att client LaunchRefused h
| _ -> h, [] // a late or duplicate answer
// Step 8 into 9. What the launch asserted — a login and maybe a Patient. Now
// ask who that login is; the credential does not travel to the registry.
| Broker, GenPresServer, LaunchResolved(att, no, assertion) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingAssertion client) ->
let ctx = { Client = client; Launch = no; Assertion = assertion }
{ h with GenPres.Pending = h.GenPres.Pending |> Map.add att (pend h.Env.Now (AwaitingUser ctx)) },
[ send GenPresServer UserRegistry (ResolveUser(att, assertion.Login)) ]
| _ -> h, []
// Step 9. Rule 6: no Role, no Session — and no guessing either.
| UserRegistry, GenPresServer, UserUnresolved(att, failure) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingUser ctx) ->
let reply =
match failure with
| NoRole -> NotAuthorised
| RegistryUnreachable -> AuthorityUnavailable
refuseLaunch att ctx.Client reply h
| _ -> h, []
// Step 9 into 10. Rule 5: the Role is the registry's answer, never the
// launch's — the launch never carried one (Concept 3).
| UserRegistry, GenPresServer, UserResolved(att, uc, mail) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingUser ctx) ->
match uc.Role with
// Rule 25: a Reader is never asked for a PIN. Not asked and ignored —
// not asked at all: the credential stage is skipped whole.
| Reader -> afterCredential att ctx uc mail h
// Rule 23: every launch checks whether a PIN is set for the login.
| Prescriber ->
{ h with
GenPres.Pending =
h.GenPres.Pending |> Map.add att (pend h.Env.Now (AwaitingCredential(ctx, uc, mail))) },
[ send GenPresServer GenPresDatabase (ReadCredential(ForLaunch att, uc.Login)) ]
| _ -> h, []
// Step 10, and UC-2 step 1. Rule 24: a Prescriber with no PIN must set one
// before the launch continues — and only now, once the registry has said who
// the login belongs to. A login the registry does not recognise never reaches
// this branch, so it can never enrol.
| GenPresDatabase, GenPresServer, CredentialRead(ForLaunch att, credential) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingCredential(ctx, uc, mail)) ->
match credential |> Option.bind _.Pin with
| Some _ -> afterCredential att ctx uc mail h
| None ->
{ h with
GenPres.Pending =
h.GenPres.Pending |> Map.add att (pend h.Env.Now (AwaitingPinChoice(ctx, uc, mail))) },
[ send GenPresServer ctx.Client (PinRequired att) ]
| _ -> h, []
// UC-2 steps 3 and 4. The launch has been suspended on a human, possibly for
// a long while, and nothing else was offered meanwhile.
| GenPresClient _, GenPresServer, SupplyPin(att, pin) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingPinChoice(ctx, uc, mail)) ->
// Creating the UserCredential if GenPRES holds none for that login
// yet. Rule 26: a newly set PIN starts with a count of zero, so there
// is nothing on an existing credential worth carrying over.
let c = UserCredential.fresh uc.Login |> UserCredential.setPin pin
{ h with
GenPres.Pending =
h.GenPres.Pending |> Map.add att (pend h.Env.Now (AwaitingPinWritten(ctx, uc, mail))) },
[ send GenPresServer GenPresDatabase (WriteCredential(ForLaunch att, c)) ]
| _ -> h, []
| GenPresDatabase, GenPresServer, CredentialWritten(ForLaunch att, _) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingPinWritten(ctx, uc, mail)) ->
let (LoginName l) = uc.Login
// Rule 26: mailed and recorded, the first setting included. Then the
// launch continues from UC-1 step 11.
let h, out = afterCredential att ctx uc mail h
h, (pinChanged (Some mail) $"PIN set for %s{l}") @ out
| _ -> h, []
// Step 11. Concept 2: read once, at the launch, and not refreshed while the
// Session lives. ext 11a: unavailable is not a failure — the PatientContext
// carries the PatientId and no data, and the User fills it in by hand.
| PatientDataPlatform, GenPresServer, (PatientDataRead(att, _) | PatientDataUnavailable att) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingPatientData(ctx, uc, mail)) ->
match ctx.Assertion.Patient with
| None -> h, [] // cannot happen: ext 1a skipped this stage
| Some p ->
let data =
match env.Msg with
| PatientDataRead(_, d) -> Some d
| _ -> None
let pctx = { Patient = Some p; Data = data }
{ h with
GenPres.Pending =
h.GenPres.Pending |> Map.add att (pend h.Env.Now (AwaitingRecord(ctx, uc, mail, pctx))) },
[ send GenPresServer GenPresDatabase (ReadRecord(ForLaunch att, p)) ]
| _ -> h, []
// Step 12. Rule 19 picks the TreatmentPlan the Session starts from: the most recent
// that is either Signed, by whoever, or Unsigned and this User's own. Where
// neither exists, the Session starts from nothing. Then Rule 7's other
// Sessions, which the Server no longer mirrors and so must read (Rule 31).
| GenPresDatabase, GenPresServer, RecordRead(ForLaunch att, record) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingRecord(ctx, uc, mail, pctx)) ->
let start = record |> PatientRecord.startsFrom uc.UserId
{ h with
GenPres.Pending =
h.GenPres.Pending
|> Map.add att (pend h.Env.Now (AwaitingPriors(ctx, uc, mail, pctx, start))) },
[ send GenPresServer GenPresDatabase (ReadSessionRecords(ForLaunch att)) ]
| _ -> h, []
// Steps 13 and 14. Rule 7 closes this User's other Sessions, Rule 10 says so
// once, and Rule 33 hands the Client the token it will return with every
// create. From here the Server keeps nothing of the Session but its record.
| GenPresDatabase, GenPresServer, SessionRecordsRead(ForLaunch att, others) ->
match h.GenPres.Pending |> Map.tryFind att |> Option.map _.Stage with
| Some(AwaitingPriors(ctx, uc, mail, pctx, start)) ->
let h, out = openSession ctx.Client (Some ctx.Launch) (Some uc) (Some mail) pctx start others h
{ h with GenPres.Pending = h.GenPres.Pending |> Map.remove att }, out
| _ -> h, []
// Rule 13 / UC-8. No launch, so no LaunchCredential, and GenPRES cannot know
// who is at the keyboard. Neither the PatientRecord nor the
// PatientDataPlatform is ever touched: with no PatientId there is nothing to
// read. Rule 7 counts a User's Sessions and this one binds to none, so there
// is nothing to close and no SessionRecords to read either.
| GenPresClient _, GenPresServer, OpenAnonymous ->
openSession env.From None None None { Patient = None; Data = None } None [] h
// ══════════════════════════════════════════════════════════════════════
// Actor 4: the GenPRES Server, in Session — one request, several legs
// ══════════════════════════════════════════════════════════════════════
// Rule 31 in one branch: a request arrives with everything it needs except who
// sent it, and the answer to that is in the Database. Nothing about this
// Session was in memory a moment ago, and nothing will be a moment after the
// reply. Rule 8's refresh has one home, here, because every in-Session act
// travels as this one message shape.
| GenPresClient _, GenPresServer, SessionRequest(sid, cmd) ->
let rid = RequestId h.GenPres.NextRequest
let ctx = { Sid = sid; Client = env.From; Cmd = cmd; Stage = AwaitingSessionRecord }
{ h with GenPres.NextRequest = h.GenPres.NextRequest + 1 } |> putFlight rid ctx,
[ send GenPresServer GenPresDatabase (ReadSessionRecord(ForRequest rid, sid)) ]
// Rule 32: the User and the Patient of the request come from here. Rule 10:
// where the Session is gone, this is the next opportunity to say so.
| GenPresDatabase, GenPresServer, SessionRecordRead(ForRequest rid, record) ->
match h.GenPres.InFlight |> Map.tryFind rid with
| None -> h, []
| Some ctx ->
match record with
| None ->
dropFlight rid h, [ send GenPresServer ctx.Client (SessionEnded None) ]
| Some r when not (SessionRecord.isOpen r) ->
if SessionRecord.tellsAtNextOpportunity r then
let mark = match r.State with Ended(m, _) -> Some m | OpenOrGone -> None
let told = r |> SessionRecord.told h.Env.Now
dropFlight rid h,
[
send GenPresServer GenPresDatabase (WriteSessionRecord told)
send GenPresServer ctx.Client (SessionEnded mark)
]
else
// Told once, never twice: the request is still refused, but the
// notice is not repeated.
dropFlight rid h, [ send GenPresServer ctx.Client SessionRefused ]
| Some r ->
// Rule 8. Every request refreshes the idle clock, and the clock is
// a field of the record now, so refreshing it is a write.
let r = r |> SessionRecord.seen h.Env.Now
let refreshed = send GenPresServer GenPresDatabase (WriteSessionRecord r)
let h, out = dispatch rid ctx r h
// CloseSession writes the ended record itself; anything else gets
// the refresh. Writing both would be harmless but noisy.
match ctx.Cmd with
| CloseSession -> h, out
| _ -> h, refreshed :: out
// The PatientRecord came back for a request part-way through.
| GenPresDatabase, GenPresServer, RecordRead(ForRequest rid, record) ->
match h.GenPres.InFlight |> Map.tryFind rid with
| Some({ Stage = AwaitingPatientRecord r } as ctx) ->
match ctx.Cmd, r.User with
// Rules 17 and 18. Opening the most recent Signed TreatmentPlan is also how
// a blocked User gets unblocked: Rule 33's token is re-minted over it,
// so it becomes the TreatmentPlan the Session opened with and Rule 20 no
// longer bites.
| OpenTreatmentPlan id, Some uc ->
match record |> PatientRecord.mayOpen uc.UserId id with
| Some s ->
dropFlight rid h,
[ send GenPresServer ctx.Client
(TreatmentPlanOpened(s.Id, s.Orders, Token.mintOpened ctx.Sid r.Patient (Some s.Id))) ]
| None ->
dropFlight rid h, [ send GenPresServer ctx.Client NotPermitted ]
| CreateTreatmentPlan _, Some _ -> decideCreate rid ctx r record h
| _ -> dropFlight rid h, []
| _ -> h, []
// Rule 22: the Server is the only party that verifies a UserCredential, and
// the PIN never leaves GenPRES. Rule 27: the count is per credential and
// survives the Session, so guessing is capped outright rather than per visit.
| GenPresDatabase, GenPresServer, CredentialRead(ForRequest rid, credential) ->
match h.GenPres.InFlight |> Map.tryFind rid with
| Some({ Stage = AwaitingUserCredential(r, pr, basePlan) } as ctx) ->
match ctx.Cmd, r.User with
| CreateTreatmentPlan(Some pin, orders, _, _, _), Some uc ->
let before = credential |> Option.defaultValue (UserCredential.fresh uc.Login)
let ok, after = UserCredential.verify pin before
let writeBack =
send GenPresServer GenPresDatabase (WriteCredential(ForRequest rid, after))
if ok then
let h, out = appendDraft rid ctx r pr basePlan uc (Some pin) orders h
h, writeBack :: out
elif UserCredential.atLimit after then
// Rule 9: a wrong entry at the limit ends the Session. Rule 10:
// and this request is the opportunity to say so.
let ended =
r
|> SessionRecord.endWith WrongPinLimit h.Env.Now
|> SessionRecord.told h.Env.Now
dropFlight rid h,
[
writeBack
send GenPresServer GenPresDatabase (WriteSessionRecord ended)
send GenPresServer ctx.Client (SessionEnded(Some WrongPinLimit))
]
else
dropFlight rid h,
[
writeBack
send GenPresServer ctx.Client (PinRejected(UserCredential.attemptsLeft after))
]
| _ -> dropFlight rid h, []
| _ -> h, []
// Rule 36 said yes. Rule 33: the Session now stands on what it just created,
// so a fresh token goes back with the answer — Rules 20 and 21 are measured
// from here on out against this TreatmentPlan.
| GenPresDatabase, GenPresServer, TreatmentPlanAppended(ForRequest rid, plan) ->
match h.GenPres.InFlight |> Map.tryFind rid with
| Some({ Stage = AwaitingAppend r } as ctx) ->
dropFlight rid h,
[ send GenPresServer ctx.Client
(TreatmentPlanCreated(
plan.Id,
plan.Signed,
Token.mintOpened ctx.Sid r.Patient (Some plan.Id))) ]
| _ -> h, []
// Rule 36 said no: somebody else's TreatmentPlan landed between this Server's
// Rule 20 read and its append. The answer is the one the Client already
// understands — take up their version (Rule 17).
| GenPresDatabase, GenPresServer, AppendRefused(ForRequest rid, actual) ->
match h.GenPres.InFlight |> Map.tryFind rid with
| Some ctx -> dropFlight rid h, [ send GenPresServer ctx.Client (CreateBlocked actual) ]
| None -> h, []
// UC-7 step 2. The PIN is gone; the UserCredential stays. Rule 26: mailed and
// recorded, every removal as well as every setting — to the address on the
// SessionRecord, since there is no Session in memory to hold one.
| GenPresDatabase, GenPresServer, PinRemoved(ForRequest rid, c) ->
match h.GenPres.InFlight |> Map.tryFind rid with
| Some({ Stage = AwaitingPinRemoved r } as ctx) ->
let (LoginName l) = c.Login
dropFlight rid h,
(pinChanged r.Mail $"PIN removed for %s{l}")
@ [ send GenPresServer ctx.Client PinReset ]
| _ -> h, []
// Written, and nothing more to say.
| GenPresDatabase, GenPresServer, CredentialWritten _
| GenPresDatabase, GenPresServer, TreatmentPlanAppended _
| GenPresDatabase, GenPresServer, AppendRefused _
| GenPresDatabase, GenPresServer, PinRemoved _
| GenPresDatabase, GenPresServer, SessionRecordsRead _
| GenPresDatabase, GenPresServer, SessionRecordRead _
| GenPresDatabase, GenPresServer, RecordRead _
| GenPresDatabase, GenPresServer, CredentialRead _ -> h, []
// ══════════════════════════════════════════════════════════════════════
// Actor 3: the GenPRES Client — and the cart, which lives here (Rule 31)
// ══════════════════════════════════════════════════════════════════════
// A closed browser is not there any more. Nothing it might have sent reaches
// the Server (UC-12 ext 2a), which is exactly why no close can be inferred —
// and the cart went with it, because the cart was only ever here.
| _, GenPresClient b, _ when
h.Clients |> Map.tryFind b |> Option.map _.Closed |> Option.defaultValue false ->
h, []
// Consequence 4: the credential travels in a URL, so it lands in the address
// bar — and stays there, which is what makes a refresh a retry.
| MainEhrLaunchScript, GenPresClient b, OpenUrl cred ->
h |> onClient b (fun s -> { s with UrlCredential = Some cred }),
[ send (GenPresClient b) GenPresServer (RedeemLaunch cred) ]
// F5. The address bar is the Client's only memory of the launch, so this is
// the one branch that reads UrlCredential rather than merely clearing it.
| User, GenPresClient b, Refresh ->
match h.Clients |> Map.tryFind b |> Option.bind _.UrlCredential with
| Some cred -> h, [ send (GenPresClient b) GenPresServer (RedeemLaunch cred) ]
| None -> h, []
// UC-8. The Client has no LaunchCredential to present, and asks for a Session
// without one.
| User, GenPresClient b, OpenDirectly ->
h |> onClient b (fun s -> { s with UrlCredential = None }),
[ send (GenPresClient b) GenPresServer OpenAnonymous ]
// Rule 6 / UC-1 ext 9a. The offer carries nothing over from the launch: no
// User, no Patient. It is only made where relaunching would not cure the
// failure — an unrecognised login, or an unreachable registry.
| User, GenPresClient b, AcceptAnonymousOffer ->
match h.Clients |> Map.tryFind b with
| Some s when s.AnonymousOffer ->
h |> onClient b (fun s -> { s with AnonymousOffer = false; Showing = None }),
[ send (GenPresClient b) GenPresServer OpenAnonymous ]
| _ -> h, []
// UC-2 step 3. Nothing else was on offer until this was answered.
| User, GenPresClient b, ChoosePin pin ->
match h.Clients |> Map.tryFind b |> Option.bind _.AwaitingPin with
| Some att ->
h |> onClient b (fun s -> { s with AwaitingPin = None; Showing = None }),
[ send (GenPresClient b) GenPresServer (SupplyPin(att, pin)) ]
| None -> h, []
// Concept 15 and Rule 31: prescribing changes the Client's own cart, and the
// whole of it then travels — to be computed on, or to be saved. Rule 11: the
// SessionId rides in the request, never in a URL, and it is also what
// refreshes the idle clock.
| User, GenPresClient b, Act a ->
let st = clientState b h
let toServer cmd = [ send (GenPresClient b) GenPresServer (SessionRequest(st.Sid.Value, cmd)) ]
match st.Sid with
| None -> h, []
| Some _ ->
match a with
| Prescribes id ->
// Whatever the User just did to it. Content is opaque here; what
// matters is that it differs from the base, which is how the
// Server can tell changed from unchanged (Rule 35).
let content = $"v%i{h.Env.Now}"
let working =
if st.Working |> List.exists (fun o -> o.Id = id) then
st.Working
|> List.map (fun o -> if o.Id = id then { o with Content = content } else o)
else
st.Working
@ [ { Id = id; Patient = st.Patient; Content = content; Stamp = None } ]
h |> onClient b (fun s -> { s with Working = working }), toServer (Compute working)
| EntersPatientData d ->
// Concept 2: the User can always supply the data by hand — with a
// Patient or without one (Rule 12).
h |> onClient b (fun s -> { s with Data = Some d }), toServer (Compute st.Working)
| Saves ->
match st.Opened with
| Some tok -> h, toServer (CreateTreatmentPlan(None, st.Working, st.Data, tok, st.Notice))
| None -> h, [] // Rule 33: the Client cannot make one
| Signs pin ->
match st.Opened with
| Some tok -> h, toServer (CreateTreatmentPlan(Some pin, st.Working, st.Data, tok, st.Notice))
| None -> h, []
| OpensTreatmentPlan id -> h, toServer (OpenTreatmentPlan id)
| AsksPinReset -> h, toServer ResetPin
| ClosesSession ->
// UC-12 ext 1a: the Client can warn that unsaved changes are about
// to be discarded, but closed is closed. They existed only here
// (Rule 31), so closing is what discards them.
h |> onClient b (fun s ->
{ s with Working = []; Data = None; Opened = None; Notice = None }),
toServer CloseSession
| CarriesOverFrom src ->
// UC-9 step 5. The unsaved work outlived its Session because it
// was never in the Server (Rule 31). It comes into this one as
// fresh prescribing (Concept 15) — not as a resumed Session, and
// with no claim on the old one's stamps: Rule 35 will decide those.
let source = clientState src h
let carried =
source.Working
|> List.filter (fun o -> st.Working |> List.forall (fun x -> x.Id <> o.Id))
|> List.map (fun o -> { o with Patient = st.Patient; Stamp = None })
let working = st.Working @ carried
h |> onClient b (fun s -> { s with Working = working }), toServer (Compute working)
| User, GenPresClient b, CloseBrowser ->
// UC-12 ext 2a: nothing reaches the Server. A vanished browser is
// indistinguishable from a silent one, so the Session is left to idle out
// — and the cart is gone, because it was only ever here (Rule 31).
h |> onClient b (fun s ->
{ s with
Closed = true
Working = []
Data = None
Opened = None
Notice = None }), []
| GenPresServer, GenPresClient b, SessionOpened(sid, _, user, pctx, orders, token) ->
h |> onClient b (fun s ->
{ s with
UrlCredential = None
AwaitingPin = None
AnonymousOffer = false
Sid = Some sid
User = user
Patient = pctx.Patient
Data = pctx.Data
Working = orders
Opened = Some token
Notice = None }), []
| GenPresServer, GenPresClient b, PinRequired att ->
h |> onClient b (fun s ->
{ s with
AwaitingPin = Some att
Showing = Some "choose a PIN — nothing else is offered until you do" }), []
| GenPresServer, GenPresClient b, LaunchRefused ->
// ext 8a: relaunching cures this, so relaunching is what is offered.
h |> onClient b (fun s ->
{ s with
UrlCredential = None
Showing = Some "the launch failed — relaunch from MainEHR" }), []
| GenPresServer, GenPresClient b, NotAuthorised ->
// ext 9a: relaunching would not help, so the anonymous open is the only
// offer worth making (Rule 6).
h |> onClient b (fun s ->
{ s with
UrlCredential = None
AnonymousOffer = true
Showing = Some "not authorised — continue anonymously?" }), []
// The registry being down is transient, so a relaunch — which mints a fresh
// credential, the one thing F5 cannot do once this one is spent — plausibly
// cures it. Both offers stand. Contrast NotAuthorised above, where the answer
// will be the same however often it is asked.
| GenPresServer, GenPresClient b, AuthorityUnavailable ->
h |> onClient b (fun s ->
{ s with
UrlCredential = None
AnonymousOffer = true
Showing =
Some "authorisation could not be checked — relaunch from MainEHR, or continue anonymously?" }), []
// Consequence 1: no Client at all is served when the Server is down, so in
// practice the User sees the browser's own error page. Where a Client was
// already served, the credential stays in the address bar and a refresh
// retries — for as long as Rule 3 allows. The cart stays too (Rule 31): a
// Server that is down has not ended anything (Rule 9).
| GenPresServer, GenPresClient b, ServerUnreachable ->
h |> onClient b (fun s -> { s with Showing = Some "GenPRES is unavailable" }), []
// The Session is gone; the work is not. It was never in the Server, so the
// Client still holds it and may offer to carry it into the next Session as
// fresh prescribing (Concept 15; UC-9 step 5).
| GenPresServer, GenPresClient b, SessionEnded mark ->
let text =
match mark with
| Some m -> $"the session ended: %A{m} — relaunch from MainEHR"
| None -> "no such session — relaunch from MainEHR"
h |> onClient b (fun s -> { s with Sid = None; Opened = None; Showing = Some text }), []
| GenPresServer, GenPresClient b, SessionRefused ->
h |> onClient b (fun s -> { s with Sid = None; Opened = None }), []
| GenPresServer, GenPresClient b, PriorSessionNotice _ ->
h |> onClient b (fun s ->
{ s with Showing = Some "work in an earlier session may have been lost" }), []
// Rule 31: the answer comes back from the payload, and the Client keeps it —
// because the Client is the only party that keeps anything.
| GenPresServer, GenPresClient b, Computed orders ->
h |> onClient b (fun s -> { s with Working = orders }), []
| GenPresServer, GenPresClient b, CreateBlocked _ ->
h |> onClient b (fun s ->
{ s with Showing = Some "someone signed since you opened — take up their version" }), []
// Rule 34. The token is what a choice to create anyway must return, so the
// Client keeps it: proceeding is re-sending the create, holding off is not.
| GenPresServer, GenPresClient b, UnsignedWorkNotice(uc, token) ->
let (LoginName l) = uc.Login
h |> onClient b (fun s ->
{ s with
Notice = Some token
Showing = Some $"unsigned work of %s{l} is newer than yours — create anyway?" }), []
| GenPresServer, GenPresClient b, CreateRefused why ->
h |> onClient b (fun s -> { s with Showing = Some $"the save was refused: %s{why}" }), []
// Rules 33 and 34. The baseline moved, so the old token is spent and a new one
// arrives with the answer; the notice, having been acted on, is spent too.
| GenPresServer, GenPresClient b, TreatmentPlanCreated(_, _, token) ->
h |> onClient b (fun s -> { s with Opened = Some token; Notice = None }), []
| GenPresServer, GenPresClient b, TreatmentPlanOpened(_, orders, token) ->
h |> onClient b (fun s ->
{ s with Working = orders; Opened = Some token; Notice = None }), []
| GenPresServer, GenPresClient b, PinRejected left ->
h |> onClient b (fun s -> { s with Showing = Some $"wrong PIN — %i{left} left" }), []
| GenPresServer, GenPresClient b, NoTreatmentPlanHere ->
h |> onClient b (fun s -> { s with Showing = Some "no patient: nothing can be saved" }), []
| GenPresServer, GenPresClient b, NotPermitted ->
h |> onClient b (fun s -> { s with Showing = Some "not permitted" }), []
| GenPresServer, GenPresClient b, PinReset ->
h |> onClient b (fun s ->
{ s with Showing = Some "PIN removed — relaunch to set a new one" }), []
// ── anything else ──
// An envelope an edge permits but the recipient does not accept. Recorded
// rather than swallowed, so a misrouted or forged message shows in the trace.
| _ -> h, [ send env.To Environment (Refused env) ]
/// The edge table is enforced here, before anything is delivered: an envelope no
/// edge permits never reaches its recipient at all. That is what separates the
/// Constraints section from a convention — no component can relay on another's
/// behalf, even by accident, because the wire does not exist.
///
/// `depthFirst` is the scheduler. Depth first — a cascade runs to the end before
/// the next thing in the inbox starts — is the readable default and what every
/// scenario but one uses. Breadth first interleaves the cascades leg by leg, which
/// is the only way to put two creates in flight at once and so the only way to
/// exercise Rule 36. It is the same messages either way; only the order differs,
/// which is precisely what Rule 36 exists to be safe against.
let runWith depthFirst fuel hospital inbox =
let rec loop fuel h trace queue =
match queue with
| [] -> h, List.rev trace, "completed"
| _ when fuel <= 0 -> h, List.rev trace, "exhausted"
| env :: rest ->
if Edges.permits env.From env.To then
let h, out = update h env
let next = if depthFirst then out @ rest else rest @ out
loop (fuel - 1) h (env :: trace) next
else
let refusal = { From = env.To; To = Environment; Msg = Refused env }
let h, _ = update h refusal
loop (fuel - 1) h (refusal :: env :: trace) rest
loop fuel hospital [] inbox
let run fuel hospital inbox = runWith true fuel hospital inbox
// ───────────────────────────── printing ─────────────────────────────
/// Rendering an envelope for the trace. Formatting only: no branch here decides
/// anything, so a message may be added without touching the model.
module Envelope =
let actorName =
function
| User -> "User"
| MainEhrWorkstation -> "Workstation"
| MainEhrLaunchScript -> "LaunchScript"
| GenPresClient(BrowserId i) -> $"Client%i{i}"
| GenPresServer -> "Server"
| GenPresDatabase -> "Database"
| PatientDataPlatform -> "Platform"
| Broker -> "Broker"
| UserRegistry -> "Registry"
| MailService -> "Mail"
| Environment -> "Env"
let private tagName =
function
| ForLaunch(AttemptId a) -> $"#%i{a}"
| ForRequest(RequestId r) -> $"req-%i{r}"
| ForSweep -> "sweep"
let private planName = function Some(TreatmentPlanId s) -> s | None -> "(nothing)"
let private cmdName =
function
| Compute os -> $"Compute (%i{os.Length} order contexts)"
| CreateTreatmentPlan(pin, os, _, tok, notice) ->
let what = match pin with Some(Pin p) -> $"Sign (pin %s{p})" | None -> "Save"
let n = match notice with Some _ -> " +notice" | None -> ""
$"%s{what} (%i{os.Length} order contexts, opened-with %s{planName tok.Plan}%s{n})"
| OpenTreatmentPlan(TreatmentPlanId s) -> $"OpenTreatmentPlan %s{s}"
| ResetPin -> "ResetPin"
| CloseSession -> "CloseSession"
let private actName =
function
| Prescribes(OrderContextId o) -> $"Prescribes %s{o}"
| EntersPatientData(PatientData d) -> $"EntersPatientData \"%s{d}\""
| Saves -> "Saves"
| Signs(Pin p) -> $"Signs (pin %s{p})"
| OpensTreatmentPlan(TreatmentPlanId s) -> $"OpensTreatmentPlan %s{s}"
| AsksPinReset -> "AsksPinReset"
| ClosesSession -> "ClosesSession"
| CarriesOverFrom(BrowserId b) -> $"CarriesOverFrom Client%i{b}"
let rec describe (m: Msg) =
match m with
| Tick -> "Tick"
| Start a -> $"Start %s{actorName a}"
| Stop a -> $"Stop %s{actorName a}"
| LogIn(LoginName u) -> $"LogIn %s{u}"
| SelectPatient(PatientId p) -> $"SelectPatient %s{p}"
| ClearPatient -> "ClearPatient"
| TriggerLaunch -> "TriggerLaunch"
| LaunchError e -> $"LaunchError \"%s{e}\""
| PrepareLaunch(LoginName u, p) ->
let pat = match p with Some(PatientId x) -> x | None -> "(no patient)"
$"PrepareLaunch %s{u} %s{pat}"
| LaunchPrepared(LaunchCredential c) -> $"LaunchPrepared %s{c}"
| LaunchNotPrepared -> "LaunchNotPrepared"
| OpenUrl(LaunchCredential c) -> $"GET /genpres?launch=%s{c}"
| Refresh -> "F5"
| OpenDirectly -> "OpenDirectly"
| AcceptAnonymousOffer -> "AcceptAnonymousOffer"
| ChoosePin(Pin p) -> $"ChoosePin %s{p}"
| Act a -> actName a
| CloseBrowser -> "CloseBrowser"
| RedeemLaunch(LaunchCredential c) -> $"RedeemLaunch %s{c}"
| OpenAnonymous -> "OpenAnonymous"
| SupplyPin(AttemptId a, Pin p) -> $"SupplyPin #%i{a} %s{p}"
| SessionRequest(SessionId s, c) -> $"%s{s}: %s{cmdName c}"
| ResolveLaunch(AttemptId a, LaunchCredential c) -> $"ResolveLaunch #%i{a} %s{c}"
| LaunchResolved(AttemptId a, LaunchNo n, x) ->
let (LoginName u) = x.Login
let pat = match x.Patient with Some(PatientId p) -> p | None -> "(no patient)"
$"LaunchResolved #%i{a} launch-%03i{n} -> %s{u} / %s{pat} (a login and a patient: no identity, no role)"
| LaunchRejected(AttemptId a, no, f) ->
let tag = match no with Some(LaunchNo n) -> $"launch-%03i{n}" | None -> "launch-???"
$"LaunchRejected #%i{a} %s{tag} %A{f}"
| ResolveUser(AttemptId a, LoginName u) -> $"ResolveUser #%i{a} %s{u}"
| UserResolved(AttemptId a, uc, _) ->
let (UserId u) = uc.UserId
$"UserResolved #%i{a} %s{u} %A{uc.Role}"
| UserUnresolved(AttemptId a, f) -> $"UserUnresolved #%i{a} %A{f}"
| ReadPatientData(AttemptId a, PatientId p) -> $"ReadPatientData #%i{a} %s{p}"
| PatientDataRead(AttemptId a, _) -> $"PatientDataRead #%i{a}"
| PatientDataUnavailable(AttemptId a) -> $"PatientDataUnavailable #%i{a}"
| ReadCredential(t, LoginName u) -> $"ReadCredential %s{tagName t} %s{u}"
| CredentialRead(t, c) ->
let pin = match c |> Option.bind _.Pin with Some _ -> "pin set" | None -> "no pin"
$"CredentialRead %s{tagName t} (%s{pin})"
| WriteCredential(t, _) -> $"WriteCredential %s{tagName t}"
| CredentialWritten(t, _) -> $"CredentialWritten %s{tagName t}"
| RemovePin(t, LoginName u) -> $"RemovePin %s{tagName t} %s{u}"
| PinRemoved(t, _) -> $"PinRemoved %s{tagName t}"
| ReadRecord(t, PatientId p) -> $"ReadRecord %s{tagName t} %s{p}"
| RecordRead(t, r) -> $"RecordRead %s{tagName t} (%i{r.Plans.Length} plans)"
| AppendIf(t, expected, d) ->
$"""AppendIf %s{tagName t} head=%s{planName expected} %s{if d.Signed then "Signed" else "Unsigned"}"""
| TreatmentPlanAppended(_, s) -> let (TreatmentPlanId i) = s.Id in $"TreatmentPlanAppended %s{i}"
| AppendRefused(t, TreatmentPlanId a) -> $"AppendRefused %s{tagName t} head is now %s{a}"
| WriteSessionRecord r ->
let (SessionNo n) = r.No
$"WriteSessionRecord ses-%03i{n} %A{r.State}"
| ReadSessionRecord(t, SessionId s) -> $"ReadSessionRecord %s{tagName t} %s{s}"
| SessionRecordRead(t, r) ->
let what = match r with Some x -> $"%A{x.State}" | None -> "(no such session)"
$"SessionRecordRead %s{tagName t} %s{what}"
| ReadSessionRecords t -> $"ReadSessionRecords %s{tagName t}"
| SessionRecordsRead(t, rs) -> $"SessionRecordsRead %s{tagName t} (%i{rs.Length})"
| SendMail(MailAddress a, what) -> $"SendMail {a}: \"%s{what}\""
| SessionOpened(SessionId s, SessionNo n, u, p, os, tok) ->
let who =
match u with
| Some uc -> let (LoginName l) = uc.Login in $"%s{l}/%A{uc.Role}"
| None -> "anonymous"
let pat = match p.Patient with Some(PatientId x) -> x | None -> "(no patient)"
$"SessionOpened %s{s} ses-%03i{n} %s{who} %s{pat} (%i{os.Length} order contexts, opened-with %s{planName tok.Plan})"
| PinRequired(AttemptId a) -> $"PinRequired #%i{a}"
| LaunchRefused -> "LaunchRefused"
| NotAuthorised -> "NotAuthorised"
| AuthorityUnavailable -> "AuthorityUnavailable"
| ServerUnreachable -> "ServerUnreachable"
| SessionEnded m -> $"SessionEnded %A{m}"
| SessionRefused -> "SessionRefused"
| PriorSessionNotice ss ->
let names =
ss |> List.map (fun (SessionNo i, m) -> $"ses-%03i{i}=%A{m}") |> String.concat ", "
$"PriorSessionNotice [%s{names}]"
| Computed os -> $"Computed (%i{os.Length} order contexts)"
| CreateBlocked(TreatmentPlanId s) -> $"CreateBlocked by %s{s}"
| UnsignedWorkNotice(uc, t) ->
let (LoginName l) = uc.Login
$"UnsignedWorkNotice (%s{l}, disclosing %i{t.Disclosed.Length})"
| CreateRefused why -> $"CreateRefused \"%s{why}\""
| TreatmentPlanCreated(TreatmentPlanId s, signed, _) ->
$"""TreatmentPlanCreated %s{s} %s{if signed then "Signed" else "Unsigned"}"""
| TreatmentPlanOpened(TreatmentPlanId s, os, _) -> $"TreatmentPlanOpened %s{s} (%i{os.Length} order contexts)"
| PinRejected n -> $"PinRejected (%i{n} left)"
| NoTreatmentPlanHere -> "NoTreatmentPlanHere"
| NotPermitted -> "NotPermitted"
| PinReset -> "PinReset"
| Noted what -> $"Noted \"%s{what}\""
| Refused e ->
$"REFUSED << %s{actorName e.From} -> %s{actorName e.To} %s{describe e.Msg} >>"
let show (env: Envelope) =
$" %-12s{actorName env.From} -> %-12s{actorName env.To} %s{describe env.Msg}"
/// The idle sweep runs on every Tick and says nothing most of the time. Keeping it
/// out of the printed trace is formatting, not filtering: the envelopes are all
/// still in `lastTrace`, and the assertions see them.
let noise (env: Envelope) =
match env.Msg with
| Tick -> true
| ReadSessionRecords ForSweep
| SessionRecordsRead(ForSweep, _) -> true
| _ -> false
// ═══════════════════════════════════════════════════════════════════════════════
// 3. SCENARIOS AND ASSERTIONS
// ═══════════════════════════════════════════════════════════════════════════════
// ───────────────────────────── what the world does ─────────────────────────────
let atWorkstation msg = { From = User; To = MainEhrWorkstation; Msg = msg }
let triggerLaunch = { From = User; To = MainEhrLaunchScript; Msg = TriggerLaunch }
let envt to_ msg = { From = Environment; To = to_; Msg = msg }
let tick = envt Environment Tick
let ticks n = List.replicate n tick
let atClient b msg = { From = User; To = GenPresClient(BrowserId b); Msg = msg }
let act b a = atClient b (Act a)
/// UC-1 steps 1 and 2. `None` is ext 1a: no Patient is active in the MainEHR Session.
let launchAs (LoginName login) (patient: PatientId option) =
[
atWorkstation (LogIn(LoginName login))
match patient with
| Some p -> atWorkstation (SelectPatient p)
| None -> atWorkstation ClearPatient
triggerLaunch
]
// ───────────────────────────── the Cast ─────────────────────────────
// The document's Cast. Their state is the state before the first use case runs;
// later use cases inherit whatever earlier ones left behind.
//
// One Workstation stands in for many. Nothing in the Rules distinguishes them:
// Rule 7 counts a User's Sessions, not a workstation's, and Invariant 1 is about one
// MainEHR Session. So "User B at their own workstation" is modelled by User B
// logging in — User A's GenPRES Session is untouched either way.
let ucA = { UserId = UserId "u-a"; Login = LoginName "dr.a"; Role = Prescriber }
let ucB = { UserId = UserId "u-b"; Login = LoginName "dr.b"; Role = Prescriber }
let ucC = { UserId = UserId "u-c"; Login = LoginName "nurse.c"; Role = Reader }
let mailA = MailAddress "a@hospital"
let mailB = MailAddress "b@hospital"
let mailC = MailAddress "c@hospital"
let pinA = Pin "1111"
let pinB = Pin "2222"
let pat1 = PatientId "pat-1" // no GenPRES PatientRecord yet
let pat2 = PatientId "pat-2" // head is a Signed TreatmentPlan
let pat3 = PatientId "pat-3" // head is an Unsigned TreatmentPlan of A's, over a Signed one
let oc id pat by =
{ Id = OrderContextId id; Patient = Some pat; Content = $"%s{id}/as-saved"; Stamp = Some by }
let mkPlan n patient by signed baseOn orders =
{
Id = TreatmentPlanId $"plan-%04i{n}"
No = TreatmentPlanNo n
Patient = patient
By = by
Base = baseOn
Orders = orders
Signed = signed
At = 0
}
let p2Signed = mkPlan 1 pat2 ucA true None [ oc "oc-1" pat2 ucA ]
let p3Signed = mkPlan 2 pat3 ucB true None [ oc "oc-2" pat3 ucB ]
let p3Unsigned = mkPlan 3 pat3 ucA false (Some p3Signed.Id) [ oc "oc-2" pat3 ucB; oc "oc-3" pat3 ucA ]
/// The world the Cast starts in.
let world =
let h = Hospital.empty
let h =
{ h with
Registry.Users =
Map.ofList [
ucA.Login, (ucA, mailA)
ucB.Login, (ucB, mailB)
ucC.Login, (ucC, mailC)
] }
let h =
{ h with
Platform.Data =
Map.ofList [
pat1, PatientData "pat-1: 4y, 17kg"
pat2, PatientData "pat-2: 7y, 24kg"
pat3, PatientData "pat-3: 1y, 9kg"
] }
let h =
{ h with
Database.Credentials =
Map.ofList [
ucA.Login, { Login = ucA.Login; Pin = Some pinA; AttemptCount = 0 }
ucB.Login, { Login = ucB.Login; Pin = Some pinB; AttemptCount = 0 }
] }
let h =
{ h with
Database.Records =
Map.ofList [
pat2, { Patient = pat2; Plans = [ p2Signed ] }
pat3, { Patient = pat3; Plans = [ p3Unsigned; p3Signed ] }
] }
// The Cast's TreatmentPlans occupy plan-0001 to plan-0003, so the Database mints from
// above them. Ids are never reissued.
{ h with Database.NextPlan = 10 }
// ───────────────────────────── assertions ─────────────────────────────
let mutable lastTrace : Envelope list = []
/// Every envelope of every scenario, so the Consequences and Guarantees can be
/// checked over the whole run rather than one step of it.
let mutable allTrace : Envelope list = []
let mutable checks = 0
let mutable failures = 0
/// Rule 31, structurally: after every scenario step, is the Server empty of requests?
let mutable everCarriedARequest = false
let expect label cond =
checks <- checks + 1
if cond then printfn $" [ok] {label}"
else
failures <- failures + 1
printfn $" [FAIL] {label}"
let saw (p: Msg -> bool) = lastTrace |> List.exists (fun e -> p e.Msg)
let never (p: Msg -> bool) = not (saw p)
let sawTo actor (p: Msg -> bool) =
lastTrace |> List.exists (fun e -> e.To = actor && p e.Msg)
let countOf (p: Msg -> bool) = lastTrace |> List.filter (fun e -> p e.Msg) |> List.length
/// Did `first` happen before `second` in the trace? Used where the document fixes an
/// order — Rule 24, and UC-3 ext 3c.
let before (first: Msg -> bool) (second: Msg -> bool) =
let idx p = lastTrace |> List.tryFindIndex (fun e -> p e.Msg)
match idx first, idx second with
| Some a, Some b -> a < b
| _ -> false
// ───────────────────────────── reading the world ─────────────────────────────
// Everything a Session is, is in the Database now (Rule 31), and everything it is
// working on is in a Client. There is no third place to look.
let recNo n (h: Hospital) = h.Database.Sessions |> List.tryFind (fun r -> r.No = SessionNo n)
let stateOf n h = recNo n h |> Option.map _.State
let noticeOf n (h: Hospital) = recNo n h |> Option.map _.Notice
let wasTold n h = match noticeOf n h with Some(Told _) -> true | _ -> false
let lastSeenOf n (h: Hospital) = recNo n h |> Option.map _.LastSeen
/// Newest first: `WriteSessionRecord` puts a new record on the front.
let newestRecord (h: Hospital) = h.Database.Sessions |> List.tryHead
let openRecords (h: Hospital) = h.Database.Sessions |> List.filter SessionRecord.isOpen
let openCount h = (openRecords h).Length
let recordCount (h: Hospital) = h.Database.Sessions.Length
let openOfUser (uc: UserContext) h =
openRecords h |> List.filter (fun r -> SessionRecord.userId r = Some uc.UserId)
let recordFor p (h: Hospital) =
h.Database.Records |> Map.tryFind p |> Option.defaultValue (PatientRecord.empty p)
let headOf p h = (recordFor p h).Plans |> List.tryHead
let planCount p h = (recordFor p h).Plans.Length
let lastTab (h: Hospital) = h.Workstation.NextTab - 1
let clientOf b (h: Hospital) = h.Clients |> Map.tryFind (BrowserId b)
let showingOf b h = clientOf b h |> Option.bind _.Showing
let sidAt b h = clientOf b h |> Option.bind _.Sid
let userAt b h = clientOf b h |> Option.bind _.User
let patientAt b h = clientOf b h |> Option.bind _.Patient
let dataAt b h = clientOf b h |> Option.bind _.Data
let workingAt b h = clientOf b h |> Option.map _.Working |> Option.defaultValue []
/// Rule 33: the TreatmentPlan the Session opened with, as the Client holds it.
let openedAt b h = clientOf b h |> Option.bind _.Opened |> Option.bind _.Plan
let noticeAt b h = clientOf b h |> Option.bind _.Notice
let mailsTo (addr: MailAddress) (h: Hospital) = h.Mail |> List.filter (fst >> (=) addr)
let credentialOf (uc: UserContext) (h: Hospital) = h.Database.Credentials |> Map.tryFind uc.Login
// ───────────────────────────── running a scenario ─────────────────────────────
/// One PatientRecord as a chain, oldest first, each link `id/who/Signed-or-Unsigned`.
/// The arrow is "and then", not "became": a PatientRecord is append-only (Concept 12),
/// so every link is still there and each stands on the one to its left.
let private planChain (r: PatientRecord) =
r.Plans
|> List.rev
|> List.map (fun s ->
let (TreatmentPlanId i) = s.Id
let (LoginName l) = s.By.Login
$"""%s{i}/%s{l}/%s{if s.Signed then "S" else "U"}""")
|> String.concat " -> "
let private planChains (h: Hospital) =
h.Database.Records
|> Map.toList
|> List.map (fun (PatientId p, r) -> p, planChain r)
|> List.filter (snd >> (<>) "")
/// What the Patients' treatment plans looked like going in. Printed above the trace so
/// that the state printed below it can be read as a difference rather than as a fact:
/// a scenario touches one Patient, and without the baseline the others read as though
/// they had moved too.
let plansBefore (h: Hospital) =
printfn " treatment plans before (oldest first, -> = and then):"
for p, chain in planChains h do
printfn $" %s{p}: %s{chain}"
let dump (before: Hospital) (h: Hospital) =
printfn $" now=%i{h.Env.Now} open=%i{openCount h} in-flight=%i{h.GenPres.InFlight.Count} launches=%i{h.GenPres.Pending.Count}"
h.Database.Sessions
|> List.rev
|> List.iter (fun r ->
let (SessionNo n) = r.No
let who =
match r.User with
| Some uc -> let (LoginName l) = uc.Login in l
| None -> "anonymous"
let pat = match r.Patient with Some(PatientId p) -> p | None -> "(no patient)"
let told =
match r.Notice with
| Told at -> $" told={at}"
| Owed -> " owed a notice"
| NotOwed -> ""
printfn $" ses-%03i{n} %-10s{who} %-11s{pat} %A{r.State}%s{told}")
let was = planChains before |> Map.ofList
printfn " treatment plans after:"
for p, chain in planChains h do
let mark = if was.TryFind p = Some chain then " (unchanged)" else " (appended)"
printfn $" %s{p}: %s{chain}%s{mark}"
h.Clients
|> Map.iter (fun (BrowserId b) x ->
let cart = if x.Working.IsEmpty then "" else $" cart=%i{x.Working.Length}"
match x.Showing with
| Some n -> printfn $" Client%i{b}: %s{n}%s{cart}"
| None -> if cart <> "" then printfn $" Client%i{b}:%s{cart}")
/// Rule 31, checked after every step: whatever the Server was doing, it is not doing
/// it any more, and it kept nothing.
let private noteFlight (h: Hospital) =
if not h.GenPres.InFlight.IsEmpty then everCarriedARequest <- true
let step label h inbox =
printfn ""
printfn $"== {label} =="
plansBefore h
let after, trace, outcome = Hospital.run 4000 h inbox
lastTrace <- trace
allTrace <- allTrace @ trace
trace |> List.filter (Envelope.noise >> not) |> List.iter (Envelope.show >> printfn "%s")
if outcome <> "completed" then printfn $" !! {outcome}"
noteFlight after
dump h after
after
/// A scenario that runs but whose trace is not worth printing in full.
let quiet label h inbox =
let h, trace, _ = Hospital.run 4000 h inbox
lastTrace <- trace
allTrace <- allTrace @ trace
noteFlight h
ignore label
h
/// The one scenario that needs the cascades interleaved rather than run one after the
/// other: Rule 36's race (see `Hospital.runWith`).
let racing label h inbox =
printfn ""
printfn $"== {label} =="
plansBefore h
let after, trace, outcome = Hospital.runWith false 4000 h inbox
lastTrace <- trace
allTrace <- allTrace @ trace
trace |> List.filter (Envelope.noise >> not) |> List.iter (Envelope.show >> printfn "%s")
if outcome <> "completed" then printfn $" !! {outcome}"
noteFlight after
dump h after
after
// ═══════════════════════════════════════════════════════════════════════════════
// UC-1 User launches GenPRES
// ═══════════════════════════════════════════════════════════════════════════════
let uc1 () =
printfn ""
printfn "############### UC-1 User launches GenPRES ###############"
// Goal: User A gets GenPRES open on the Patient they have selected, able to
// prescribe, save and sign. Patient 1 has no PatientRecord, so the Session starts
// from nothing.
let launched = step "UC-1 main — A launches for Patient 1" world (launchAs ucA.Login (Some pat1))
expect "UC-1 one Session, open, and the Role is the registry's"
(openCount launched = 1
&& stateOf 1 launched = Some OpenOrGone
&& (newestRecord launched |> Option.bind _.User |> Option.map _.Role) = Some Prescriber)
expect "UC-1 the SessionRecord carries the UserContext and the mail address (Concept 9)"
((newestRecord launched |> Option.bind _.User) = Some ucA
&& (newestRecord launched |> Option.bind _.Mail) = Some mailA)
expect "UC-1 step 8: the launch asserted a login and a Patient, and no Role"
(saw (function
| LaunchResolved(_, _, a) -> a.Login = ucA.Login && a.Patient = Some pat1
| _ -> false))
expect "UC-1 step 9: the Role came from the UserRegistry (Rule 5)"
(saw (function UserResolved(_, uc, _) -> uc.Role = Prescriber | _ -> false))
expect "UC-1 step 10: a PIN is set, so the launch continues and none is asked for (Rule 23)"
(saw (function CredentialRead(_, Some c) -> c.Pin.IsSome | _ -> false)
&& never (function PinRequired _ -> true | _ -> false))
expect "UC-1 step 11: the PatientContext was read once, at the launch (Concept 2)"
(saw (function PatientDataRead _ -> true | _ -> false)
&& countOf (function ReadPatientData _ -> true | _ -> false) = 1)
expect "UC-1 step 12: Patient 1 has no record, so the Session starts from nothing (Rule 19)"
(openedAt 1 launched = None && workingAt 1 launched = [])
expect "UC-1 step 13: the SessionRecord was written to the Database (Concept 9)"
(launched.Database.Sessions.Length = 1)
// Rule 33. The Client is handed the token it will return with every create, and
// it could not have made one: the mac is over a secret it never sees.
expect "UC-1 step 14: the Client holds an opened-with token that verifies (Rule 33)"
((clientOf 1 launched |> Option.bind _.Opened |> Option.map Token.verifyOpened) = Some true)
expect "UC-1 and from here the Server keeps nothing of the Session (Rule 31)"
(launched.GenPres.InFlight.IsEmpty && launched.GenPres.Pending.IsEmpty)
expect "UC-1 the credential is spent, and is not kept by GenPRES (Rule 2)"
(launched.Broker.Launches |> Map.forall (fun _ l -> l.Redeemed))
// ── UC-1 ext 1a — no Patient is active in the MainEHR Session ──
// GenPRES opens and A can prescribe, but a TreatmentPlan cannot be opened or created.
let noPatient = step "UC-1 ext 1a — no Patient active" world (launchAs ucA.Login None)
expect "1a a Session opens without a Patient"
(openCount noPatient = 1 && (newestRecord noPatient |> Option.bind _.Patient) = None)
expect "1a steps 11 and 12 are skipped: no data to fetch, no PatientRecord to read"
(never (function ReadPatientData _ -> true | _ -> false)
&& never (function ReadRecord _ -> true | _ -> false))
let _ =
step "UC-1 ext 1a — and a TreatmentPlan cannot be created (Rule 12)" noPatient
[ act 1 (Prescribes(OrderContextId "oc-9")); act 1 Saves ]
expect "1a prescribing works; creating does not"
(saw (function Computed _ -> true | _ -> false)
&& saw (function NoTreatmentPlanHere -> true | _ -> false)
&& never (function TreatmentPlanCreated _ -> true | _ -> false))
// ── UC-1 ext 3a — the Broker is unreachable ──
// The one launch failure the EHR side can report: its Broker edge is
// request-response and it has not yet exited.
let brokerDown =
step "UC-1 ext 3a — the Broker is unreachable" world
(envt Broker (Stop Broker) :: launchAs ucA.Login (Some pat1))
expect "3a no credential exists, nothing was opened, and the LaunchScript says so"
(saw (function LaunchError _ -> true | _ -> false)
&& never (function LaunchPrepared _ -> true | _ -> false)
&& brokerDown.Clients.IsEmpty
&& openCount brokerDown = 0)
// ── UC-1 ext 5a / 7a — the Server is unreachable ──
// In production the Client is served by the Server, so ext 5a shows the browser's
// own error page and nothing of ours. The model has no notion of the page being
// served, so both extensions arrive here as the same answer: unavailable, and the
// credential stays in the address bar (Consequence 4) so a refresh retries for as
// long as Rule 3 allows.
let serverDown =
step "UC-1 ext 5a — the Server is down at the launch" world
(envt GenPresServer (Stop GenPresServer) :: launchAs ucA.Login (Some pat1))
expect "5a nothing opens, and the Client is told GenPRES is unavailable"
(openCount serverDown = 0
&& sawTo (GenPresClient(BrowserId 1)) (function ServerUnreachable -> true | _ -> false))
let retried =
step "UC-1 ext 7a — the Server comes back, and F5 retries within Rule 3's window" serverDown
(ticks 2 @ [ envt GenPresServer (Start GenPresServer); atClient 1 Refresh ])
expect "7a the parked credential is still good, and the Session opens"
(openCount retried = 1 && saw (function SessionOpened _ -> true | _ -> false))
let expired =
step "UC-1 ext 7a — but not past credentialTtl (Rule 3, Rule 28)" serverDown
(ticks 10 @ [ envt GenPresServer (Start GenPresServer); atClient 1 Refresh ])
expect "7a an aged credential opens nothing"
(openCount expired = 0
&& saw (function LaunchRejected(_, _, CredentialExpired) -> true | _ -> false)
&& saw (function LaunchRefused -> true | _ -> false))
// ── UC-1 ext 7b — the LaunchCredential is stolen before the Client presents it ──
// The credential is in a URL (Consequence 4): whoever presents it first wins
// (Rule 2), so within its lifetime a thief gains A's Session. Park it unredeemed —
// a Server that was down when the browser opened — so the thief can actually get
// there first. Left to itself the legitimate Client redeems inside the launch
// cascade and no thief could ever win, which is the race below, not this one.
let parked =
step "UC-1 ext 7b — the credential sits unredeemed in the address bar" world
(envt GenPresServer (Stop GenPresServer) :: launchAs ucA.Login (Some pat1))
let thief =
step "UC-1 ext 7b — a thief presents it first, and gains A's Session" parked
[
envt GenPresServer (Start GenPresServer)
{
From = GenPresClient(BrowserId 99)
To = GenPresServer
Msg = RedeemLaunch(LaunchCredential "cred-0001")
}
]
expect "7b the thief holds a live Session — and it is bound to A (Rules 2, 5)"
(openCount thief = 1
&& (newestRecord thief |> Option.bind _.User |> Option.map _.UserId) = Some ucA.UserId
&& sidAt 99 thief = (newestRecord thief |> Option.map _.Id))
let aLocked = step "UC-1 ext 7b — and A's own retry is refused" thief [ atClient 1 Refresh ]
expect "7b whoever presents it first wins; the loser gets nothing (Rule 2)"
(openCount aLocked = 1
&& saw (function LaunchRejected(_, _, AlreadyRedeemed) -> true | _ -> false)
&& saw (function LaunchRefused -> true | _ -> false))
// The damage is bounded: the thief saves at most Unsigned work in A's name.
let thiefSaved =
step "UC-1 ext 7b — the thief can save, and it is attributed to A" aLocked
[
act 99 (Prescribes(OrderContextId "oc-stolen"))
act 99 Saves
]
expect "7b Unsigned work in A's name — attribution is per credential, not per person (Rules 14, 32)"
(planCount pat1 thiefSaved = 1
&& (headOf pat1 thiefSaved |> Option.map _.By) = Some ucA
&& (headOf pat1 thiefSaved |> Option.map _.Signed) = Some false)
let thiefBlocked =
step "UC-1 ext 7b — but cannot sign: signing needs A's PIN" thiefSaved
[ act 99 (Signs(Pin "guess")) ]
expect "7b nothing is Signed, and the guess costs A an attempt (Concept 14; Rules 22, 27)"
(saw (function PinRejected _ -> true | _ -> false)
&& (recordFor pat1 thiefBlocked |> PatientRecord.latestSigned).IsNone
&& (credentialOf ucA thiefBlocked |> Option.map _.AttemptCount) = Some 1)
let evicted =
step "UC-1 ext 7b — A's own next launch evicts them" thiefBlocked (launchAs ucA.Login (Some pat1))
expect "7b one open Session, the thief's superseded, and A is told something held it (Rules 7, 10)"
(openCount evicted = 1
&& (match stateOf 1 evicted with Some(Ended(Superseded, _)) -> true | _ -> false)
&& saw (function PriorSessionNotice _ -> true | _ -> false))
// Single use and short lifetime are the containment, not prevention (Rules 2, 3, 28).
// The other ordering is legal too, and is what happens when nothing delays the
// legitimate Client: it redeems inside the launch cascade, and the thief arrives
// to a credential already spent.
let lostRace =
step "UC-1 ext 7b — a thief arriving second gets nothing" world
(launchAs ucA.Login (Some pat1)
@ [
{
From = GenPresClient(BrowserId 99)
To = GenPresServer
Msg = RedeemLaunch(LaunchCredential "cred-0001")
}
])
expect "7b arriving second, the thief is refused and opens nothing (Rule 2)"
(openCount lostRace = 1
&& saw (function LaunchRejected(_, _, AlreadyRedeemed) -> true | _ -> false)
&& sidAt 99 lostRace = None)
// ── UC-1 ext 8a — the credential is expired or already redeemed ──
// Covered by 7a and 7b above: both end in LaunchRefused, which carries no reason.
// ext 8b — the Server cannot reach the Broker.
// Starting from ext 5a: the credential is still parked and unredeemed, so there is
// something for the Server to fail to redeem.
let _ =
step "UC-1 ext 8b — the Broker is unreachable at redemption" serverDown
[
envt GenPresServer (Start GenPresServer)
envt Broker (Stop Broker)
atClient 1 Refresh
]
expect "8b redemption fails and the launch is refused"
(saw (function LaunchRejected(_, _, BrokerUnreachable) -> true | _ -> false)
&& saw (function LaunchRefused -> true | _ -> false))
// ── UC-1 ext 9a — the UserRegistry cannot say what the login may do ──
let registryDown =
step "UC-1 ext 9a — the registry is unreachable" world
(envt UserRegistry (Stop UserRegistry) :: launchAs ucA.Login (Some pat1))
expect "9a no launched Session, and rights fail closed (Rules 5, 6)"
(openCount registryDown = 0
&& saw (function AuthorityUnavailable -> true | _ -> false))
expect "9a the anonymous open is offered — relaunching would not cure this"
((clientOf 1 registryDown |> Option.map _.AnonymousOffer) = Some true)
let wentAnonymous =
step "UC-1 ext 9a — A accepts, and gets a fresh anonymous open (Rule 6)" registryDown
[ atClient 1 AcceptAnonymousOffer ]
expect "9a it carries nothing over from the launch: no User, no Patient"
(openCount wentAnonymous = 1
&& (newestRecord wentAnonymous |> Option.bind _.User) = None
&& (newestRecord wentAnonymous |> Option.bind _.Patient) = None)
// ── UC-1 ext 9b — the launching User is a Reader ──
let asReader = step "UC-1 ext 9b — C, a Reader, launches for Patient 3" world (launchAs ucC.Login (Some pat3))
expect "9b a Session opens, with the Reader Role"
((newestRecord asReader |> Option.bind _.User |> Option.map _.Role) = Some Reader)
expect "9b a Reader is never asked for a PIN — not asked and ignored, but not asked (Rule 25)"
(never (function ReadCredential _ -> true | _ -> false)
&& never (function PinRequired _ -> true | _ -> false))
expect "9b and starts from the most recent Signed TreatmentPlan, not A's Unsigned head (Rules 18, 19)"
(openedAt 1 asReader = Some p3Signed.Id)
// ── UC-1 ext 10a — User A has no PIN yet ──
// First launch as a Prescriber. UC-2 is this case in full: a PIN must be set
// before the launch continues (Rule 24).
// ── UC-1 ext 11a — the PatientDataPlatform is unreachable ──
let noPlatform =
step "UC-1 ext 11a — the PatientDataPlatform is unreachable" world
(envt PatientDataPlatform (Stop PatientDataPlatform) :: launchAs ucA.Login (Some pat2))
expect "11a the launch continues: a PatientId and no data (Concept 2)"
(openCount noPlatform = 1
&& (newestRecord noPlatform |> Option.bind _.Patient) = Some pat2
&& dataAt 1 noPlatform = None)
expect "11a TreatmentPlans work as normal — the PatientId is there (Rule 12)"
(openedAt 1 noPlatform = Some p2Signed.Id)
// ── UC-1 ext 13a / 14a — A already has an open Session, or the wrong Patient ──
// Rule 7 is per User, not per Patient, so both are the same mechanism: the
// earlier Session is closed and A is told work in it may have been lost.
let wrongPatient = step "UC-1 ext 14a — A launched for the wrong Patient" world (launchAs ucA.Login (Some pat1))
let relaunched =
step "UC-1 ext 13a/14a — A activates Patient 2 and relaunches" wrongPatient
(launchAs ucA.Login (Some pat2))
expect "14a the wrong Session is closed, whichever Patient it was for (Rule 7)"
(openCount relaunched = 1
&& (newestRecord relaunched |> Option.bind _.Patient) = Some pat2
&& (match stateOf 1 relaunched with Some(Ended(Superseded, _)) -> true | _ -> false))
expect "13a and A is told, once (Rule 10)"
(saw (function PriorSessionNotice _ -> true | _ -> false)
&& wasTold 1 relaunched)
launched
// ═══════════════════════════════════════════════════════════════════════════════
// UC-2 First launch as a Prescriber: no PIN yet
// ═══════════════════════════════════════════════════════════════════════════════
let uc2 () =
printfn ""
printfn "############### UC-2 First launch as a Prescriber ###############"
// Precondition: UC-1 has reached step 10 — the UserContext carries the Prescriber
// Role, and no PIN is set for that login.
let noPin =
{ world with Database.Credentials = world.Database.Credentials |> Map.remove ucA.Login }
let asked =
step "UC-2 main — A launches as a Prescriber for the first time" noPin
(launchAs ucA.Login (Some pat1))
expect "UC-2 the launch stops and asks for a PIN, and offers nothing else (Rules 23, 24)"
(saw (function PinRequired _ -> true | _ -> false)
&& openCount asked = 0
&& never (function SessionOpened _ -> true | _ -> false))
// The order matters: a login the registry does not recognise never gets to enrol.
expect "UC-2 the PIN is offered only after the registry recognised the login (Rule 24)"
(before (function UserResolved _ -> true | _ -> false)
(function PinRequired _ -> true | _ -> false))
let unknown =
step "UC-2 — a login the registry does not know never reaches the PIN question" noPin
(launchAs (LoginName "dr.x") (Some pat1))
expect "UC-2 an unrecognised login is refused before any PIN is offered (UC-1 ext 9a)"
(openCount unknown = 0
&& saw (function NotAuthorised -> true | _ -> false)
&& never (function PinRequired _ -> true | _ -> false))
let enrolled =
step "UC-2 steps 3 to 5 — A chooses a PIN and the launch continues" asked
[ atClient 1 (ChoosePin(Pin "9999")) ]
expect "UC-2 step 4: the PIN is set on A's UserCredential, created since GenPRES held none"
((credentialOf ucA enrolled |> Option.bind _.Pin) = Some(Pin "9999"))
expect "UC-2 step 4: the change is recorded and A is mailed, the first setting included (Rule 26)"
((mailsTo mailA enrolled).Length = 1
&& enrolled.Audit |> List.exists (fun a -> a.Contains "PIN set"))
expect "UC-2 a newly set PIN starts with a count of zero (Rule 27)"
((credentialOf ucA enrolled |> Option.map _.AttemptCount) = Some 0)
expect "UC-2 step 5: the launch continues from UC-1 step 11"
(openCount enrolled = 1
&& saw (function SessionOpened _ -> true | _ -> false)
&& saw (function PatientDataRead _ -> true | _ -> false))
// ── UC-2 ext 3a — A does not set a PIN ──
let askedAgain =
step "UC-2 ext 3a — A does not set a PIN; the next launch asks again" asked
(launchAs ucA.Login (Some pat1))
expect "3a a required PIN is not set, so no Session is opened (Rule 6) — and it asks again"
(openCount askedAgain = 0
&& saw (function PinRequired _ -> true | _ -> false))
// A Reader in the same position is never asked at all.
let readerNoPin =
step "UC-2 — a Reader with no PIN is never asked (Rule 25)" noPin
(launchAs ucC.Login (Some pat2))
expect "UC-2 the Reader's launch is never held up by a PIN"
(openCount readerNoPin = 1
&& never (function PinRequired _ -> true | _ -> false))
// Not a document scenario — model hygiene. A launch that stalls mid-flight would
// otherwise sit in the launch table forever, which is harmless here and a leak in
// production. Everything but AwaitingPinChoice is waiting on a round trip and is
// collectable; that one waits on a human and is not.
let stalled =
let ctx =
{
Client = GenPresClient(BrowserId 1)
Launch = LaunchNo 1
Assertion = { Login = ucA.Login; Patient = Some pat1 }
}
{ world with
GenPres.Pending =
Map.empty
|> Map.add (AttemptId 90) { Stage = AwaitingUser ctx; Since = 0 }
|> Map.add (AttemptId 91) { Stage = AwaitingPinChoice(ctx, ucA, mailA); Since = 0 } }
let swept = step "UC-2 — an abandoned launch is collected; one waiting on a human is not" stalled (ticks 12)
expect "UC-2 a launch stalled mid-flight is dropped; one suspended on a human is kept (UC-2 step 3)"
(not (swept.GenPres.Pending.ContainsKey(AttemptId 90))
&& swept.GenPres.Pending.ContainsKey(AttemptId 91))
// ═══════════════════════════════════════════════════════════════════════════════
// UC-3 Prescribe, save and sign
// ═══════════════════════════════════════════════════════════════════════════════
let uc3 () =
printfn ""
printfn "############### UC-3 Prescribe, save and sign ###############"
// Precondition: UC-1 completed — A has an open Session for Patient 2, started from
// its Signed head, and holds the Prescriber Role.
let opened = quiet "UC-3 precondition" world (launchAs ucA.Login (Some pat2))
expect "UC-3 precondition: the Session started from Patient 2's Signed head (Rule 19)"
(openedAt 1 opened = Some p2Signed.Id)
let saved =
step "UC-3 steps 1 and 2 — A prescribes and saves" opened
[
act 1 (Prescribes(OrderContextId "oc-4"))
act 1 Saves
]
expect "UC-3 step 1: each change goes to the Server, which answers from the payload (Rules 8, 31)"
(saw (function Computed _ -> true | _ -> false))
expect "UC-3 step 2: nothing blocks and nothing warns (Rules 20, 21)"
(never (function CreateBlocked _ -> true | _ -> false)
&& never (function UnsignedWorkNotice _ -> true | _ -> false))
expect "UC-3 step 2: an Unsigned TreatmentPlan is appended, carrying A's UserContext (Rule 14)"
(planCount pat2 saved = 2
&& (headOf pat2 saved |> Option.map _.Signed) = Some false
&& (headOf pat2 saved |> Option.map _.By) = Some ucA)
expect "UC-3 step 2: and its base (Concept 13)"
((headOf pat2 saved |> Option.bind _.Base) = Some p2Signed.Id)
expect "UC-3 Rule 14: the OrderContext changed in the Session is stamped"
(headOf pat2 saved
|> Option.map _.Orders
|> Option.defaultValue []
|> List.forall (fun o -> o.Stamp = Some ucA))
expect "UC-3 Rule 33: the create carried the opened-with token, and a new one came back"
(saw (function SessionRequest(_, CreateTreatmentPlan(_, _, _, t, _)) -> t.Plan = Some p2Signed.Id | _ -> false)
&& openedAt 1 saved = (headOf pat2 saved |> Option.map _.Id))
let signed = step "UC-3 step 3 — A signs" saved [ act 1 (Signs pinA) ]
expect "UC-3 step 3: a Signed TreatmentPlan in A's name (Concept 14, Rules 14, 15)"
(planCount pat2 signed = 3
&& (headOf pat2 signed |> Option.map _.Signed) = Some true
&& (headOf pat2 signed |> Option.map _.By) = Some ucA)
expect "UC-3 step 3: it is now the most recent Signed TreatmentPlan and counts clinically (Rule 16)"
((recordFor pat2 signed |> PatientRecord.latestSigned |> Option.map _.Id)
= (headOf pat2 signed |> Option.map _.Id))
expect "UC-3 the correct entry reset the wrong-entry count (Rule 27)"
((credentialOf ucA signed |> Option.map _.AttemptCount) = Some 0)
// ── UC-3 ext 2a — the record has moved on since A opened ──
// If what appeared is Unsigned, A is notified and may create anyway or hold off
// (Rule 21). If a Signed TreatmentPlan appeared, creating is blocked (Rule 20). UC-6 is
// this case in full.
// ── UC-3 ext 3a — A does not sign ──
// The Unsigned TreatmentPlan stays at the head, inert. Only A can open it (Rule 18),
// and it counts for nothing until signed (Rule 16).
expect "3a an Unsigned head does not count clinically (Rule 16)"
((recordFor pat2 saved |> PatientRecord.latestSigned |> Option.map _.Id) = Some p2Signed.Id)
expect "3a only its creator can open it (Rule 18)"
((recordFor pat2 saved |> PatientRecord.mayOpen ucA.UserId (headOf pat2 saved).Value.Id).IsSome
&& (recordFor pat2 saved |> PatientRecord.mayOpen ucB.UserId (headOf pat2 saved).Value.Id).IsNone)
// ── UC-3 ext 3b — A gives the wrong PIN ──
let wrongOnce = step "UC-3 ext 3b — A gives the wrong PIN" saved [ act 1 (Signs(Pin "0000")) ]
expect "3b verification fails and no TreatmentPlan is created"
(planCount pat2 wrongOnce = 2
&& saw (function PinRejected _ -> true | _ -> false))
expect "3b the count is on the UserCredential, not the Session (Rule 27)"
((credentialOf ucA wrongOnce |> Option.map _.AttemptCount) = Some 1)
let atLimit =
step "UC-3 ext 3b — and at the limit the Session ends (Rules 9, 27)" wrongOnce
[
act 1 (Signs(Pin "0000"))
act 1 (Signs(Pin "0000"))
]
expect "3b the Session ends at the wrong-PIN limit"
(openCount atLimit = 0
&& (match stateOf 1 atLimit with Some(Ended(WrongPinLimit, _)) -> true | _ -> false)
&& saw (function SessionEnded(Some WrongPinLimit) -> true | _ -> false))
expect "3b the count survives the Session: it is not a fresh start"
((credentialOf ucA atLimit |> Option.map _.AttemptCount) = Some wrongPinLimit)
// ── UC-3 ext 3c — A signs without saving first ──
// Steps 2 and 3 become one act, and the block and notification checks run before
// the PIN is asked for. Set up a block, and watch nothing ask for a credential.
let bSigned =
quiet "UC-3 ext 3c setup — B signs while A is open" opened
(launchAs ucB.Login (Some pat2)
@ [ act 2 (Prescribes(OrderContextId "oc-5")); act 2 (Signs pinB) ])
let blocked =
step "UC-3 ext 3c — A signs without saving, and is blocked before the PIN" bSigned
[ act 1 (Prescribes(OrderContextId "oc-6")); act 1 (Signs pinA) ]
expect "3c the block is decided first: no credential is ever read (Rules 20, 22)"
(saw (function CreateBlocked _ -> true | _ -> false)
&& never (function ReadCredential(ForRequest _, _) -> true | _ -> false))
expect "3c and nothing was appended"
(planCount pat2 blocked = planCount pat2 bSigned)
signed
// ═══════════════════════════════════════════════════════════════════════════════
// UC-4 Work left unsigned by someone else
// ═══════════════════════════════════════════════════════════════════════════════
let uc4 () =
printfn ""
printfn "############### UC-4 Work left unsigned by someone else ###############"
// Precondition: Patient 3's head is an Unsigned TreatmentPlan of A's over an older
// Signed one. B launches, holding the Prescriber Role.
let bOpen = step "UC-4 step 1 — B launches for Patient 3" world (launchAs ucB.Login (Some pat3))
expect "UC-4 step 1: B starts from the older Signed TreatmentPlan, not A's Unsigned head (Rules 18, 19)"
(openedAt 1 bOpen = Some p3Signed.Id)
expect "UC-4 step 1: A's Unsigned work is closed to B (Rule 18)"
(recordFor pat3 bOpen |> PatientRecord.mayOpen ucB.UserId p3Unsigned.Id).IsNone
let warned =
step "UC-4 step 2 — B enters orders and saves" bOpen
[
act 1 (Prescribes(OrderContextId "oc-7"))
act 1 Saves
]
expect "UC-4 step 2: B is told an Unsigned TreatmentPlan of another User is newer (Rule 21)"
(saw (function UnsignedWorkNotice(uc, _) -> uc = ucA | _ -> false))
expect "UC-4 step 2: and the create waits — the User may still choose not to"
(planCount pat3 warned = 2)
expect "UC-4 step 2: the notice came with a token naming what it disclosed (Rule 34)"
((noticeAt 1 warned |> Option.map _.Disclosed) = Some [ p3Unsigned.Id ])
// Rule 34: proceeding is re-sending the create with that token. There is no
// `Proceed` message; holding off is simply not sending this.
let bSaved = step "UC-4 step 2 — B chooses to create anyway, returning the token" warned [ act 1 Saves ]
expect "UC-4 step 2: an Unsigned TreatmentPlan of B's own is appended (Rules 14, 34)"
(planCount pat3 bSaved = 3
&& (headOf pat3 bSaved |> Option.map _.By) = Some ucB
&& (headOf pat3 bSaved |> Option.map _.Signed) = Some false)
expect "UC-4 step 2: and the notice is spent — the token does not linger (Rule 34)"
(noticeAt 1 bSaved = None)
let bSigned = step "UC-4 step 3 — B signs" bSaved [ act 1 (Signs pinB) ]
expect "UC-4 step 3: a Signed TreatmentPlan in B's name; it now counts clinically (Rules 15, 16)"
((headOf pat3 bSigned |> Option.map _.Signed) = Some true
&& (recordFor pat3 bSigned |> PatientRecord.latestSigned |> Option.map _.By) = Some ucB)
// ── step 4 — A's Unsigned work is superseded ──
let aReturns = step "UC-4 step 4 — A launches for Patient 3 after B signed" bSigned (launchAs ucA.Login (Some pat3))
expect "UC-4 step 4: A's Session starts from B's Signed TreatmentPlan (Rule 19)"
(openedAt 2 aReturns
= (recordFor pat3 aReturns |> PatientRecord.latestSigned |> Option.map _.Id))
// "Nobody but User A could ever open it, and now not even User A can act on it."
// Rule 18 does still let A open their own Unsigned TreatmentPlan — it is unqualified.
// What has gone is the acting: Rule 20 blocks creating anything from it, because
// B's Signed TreatmentPlan is newer than the one A would then have opened with.
let aOnDeadEnd =
step "UC-4 step 4 — A opens the old work, and can do nothing with it" aReturns
[
act 2 (OpensTreatmentPlan p3Unsigned.Id)
act 2 (Signs pinA)
]
expect "UC-4 step 4: A may still open their own Unsigned TreatmentPlan (Rule 18)"
(saw (function TreatmentPlanOpened(id, _, _) -> id = p3Unsigned.Id | _ -> false))
expect "UC-4 step 4: but creating anything from it is blocked, for good (Rule 20)"
(saw (function CreateBlocked _ -> true | _ -> false)
&& (headOf pat3 aOnDeadEnd |> Option.map _.By) = Some ucB)
// ── UC-4 ext 2a — B holds off at the notification ──
// There is nothing to send: under Rule 34 the create is only made by returning the
// token, so holding off is the absence of a message. `warned` is that state.
expect "2a nothing is created; both TreatmentPlans stand, each usable only by its own User"
(planCount pat3 warned = 2
&& (headOf pat3 warned |> Option.map _.Id) = Some p3Unsigned.Id)
// ── UC-4 ext 4a — A launches before B signs ──
let aBeforeBSigns =
step "UC-4 ext 4a — A launches for Patient 3 before B signs" bSaved (launchAs ucA.Login (Some pat3))
expect "4a A starts from A's own Unsigned head: B's is Unsigned too, so it does not supersede (Rule 19)"
(openedAt 2 aBeforeBSigns = Some p3Unsigned.Id)
let aSignsFirst =
step "UC-4 ext 4a — A may sign: no newer Signed TreatmentPlan exists (Rule 20)" aBeforeBSigns
[ act 2 (Signs pinA) ]
expect "4a A is notified of B's newer Unsigned work (Rule 21), and nothing is created yet"
(saw (function UnsignedWorkNotice(uc, _) -> uc = ucB | _ -> false))
let aWon = step "UC-4 ext 4a — A re-sends with the token, and signing first blocks B" aSignsFirst [ act 2 (Signs pinA) ]
expect "4a whichever of the two signs first blocks the other (Rule 20)"
((recordFor pat3 aWon |> PatientRecord.latestSigned |> Option.map _.By) = Some ucA)
let bNowBlocked = step "UC-4 ext 4a — B tries to sign after A did" aWon [ act 1 (Signs pinB) ]
expect "4a B is blocked by A's Signed TreatmentPlan (Rule 20)"
(saw (function CreateBlocked _ -> true | _ -> false))
ignore bNowBlocked
bSigned
// ═══════════════════════════════════════════════════════════════════════════════
// UC-5 Someone else takes over the workstation
// ═══════════════════════════════════════════════════════════════════════════════
let uc5 () =
printfn ""
printfn "############### UC-5 Someone else takes over the workstation ###############"
// Precondition: A has an open Session for Patient 1 and walks away. Possibility 1:
// this is not ours to prevent, only to handle.
let aWalksAway = quiet "UC-5 precondition" world (launchAs ucA.Login (Some pat1))
let bSaves =
step "UC-5 steps 1 to 4 — B works and saves in A's Session" aWalksAway
[
act 1 (Prescribes(OrderContextId "oc-8"))
act 1 Saves
]
expect "UC-5 step 4: the TreatmentPlan is created under the Session's credentials — A's (Rules 14, 32)"
(planCount pat1 bSaves = 1
&& (headOf pat1 bSaves |> Option.map _.By) = Some ucA)
expect "UC-5 step 4: and so are the stamps on every OrderContext B changed (Rules 14, 35)"
(headOf pat1 bSaves
|> Option.map _.Orders
|> Option.defaultValue []
|> List.forall (fun o -> o.Stamp = Some ucA))
// Step 5: signing always names the Session's User, so the Client asks for A's PIN.
// Step 6: B does not have it. Supplying their own proves nothing — the Server
// verifies against the Session's User's credential (Rules 14, 22, 32).
let bTriesToSign = step "UC-5 steps 5 and 6 — B signs, with the only PIN they have" bSaves [ act 1 (Signs pinB) ]
expect "UC-5 step 6: the work stays Unsigned and does not count clinically (Rules 15, 16)"
(saw (function PinRejected _ -> true | _ -> false)
&& (headOf pat1 bTriesToSign |> Option.map _.Signed) = Some false
&& (recordFor pat1 bTriesToSign |> PatientRecord.latestSigned).IsNone)
// Signing always names the Session's User, so verification runs against A's
// credential whoever is at the keyboard — which is exactly what caps B's guessing
// in ext 6a, and why it costs A their allowance rather than B's.
expect "UC-5 the wrong entry counted against the Session's User's credential — A's, not B's (Rules 22, 27, 32)"
((credentialOf ucB bTriesToSign |> Option.map _.AttemptCount) = Some 0
&& (credentialOf ucA bTriesToSign |> Option.map _.AttemptCount) = Some 1)
// ── UC-5 ext 5a — B relaunches as themselves ──
let bOwnSession =
step "UC-5 ext 5a — B relaunches from MainEHR as themselves, Patient 1 active" bSaves
(launchAs ucB.Login (Some pat1))
expect "5a Rule 7 is per User: a Session of B's own opens, and A's is untouched"
(openCount bOwnSession = 2
&& (openOfUser ucA bOwnSession).Length = 1
&& (openOfUser ucB bOwnSession).Length = 1)
expect "5a it starts from nothing: no Signed TreatmentPlan, and the Unsigned one is A's (Rules 18, 19)"
(openedAt 2 bOwnSession = None)
let bReEnters =
step "UC-5 ext 5a — B re-enters the work and signs; the notice comes first" bOwnSession
[
act 2 (Prescribes(OrderContextId "oc-8"))
act 2 (Signs pinB)
]
expect "5a B is notified of the newer Unsigned TreatmentPlan (Rule 21)"
(saw (function UnsignedWorkNotice(uc, _) -> uc = ucA | _ -> false))
let bSignedOwn = step "UC-5 ext 5a — B re-sends with the token (Rule 34)" bReEnters [ act 2 (Signs pinB) ]
expect "5a and signs as themselves (Rules 14, 15)"
((headOf pat1 bSignedOwn |> Option.map _.By) = Some ucB
&& (headOf pat1 bSignedOwn |> Option.map _.Signed) = Some true)
// ── UC-5 ext 5b — B cannot log in to MainEHR at that workstation ──
// No path to a Session of B's own. The work stays Unsigned until A opens it in a
// Session of their own and signs; nobody else can.
expect "5b the work stays Unsigned, and only A can ever act on it (Rules 18, 19)"
((recordFor pat1 bSaves |> PatientRecord.mayOpen ucB.UserId (headOf pat1 bSaves).Value.Id).IsNone
&& (recordFor pat1 bSaves |> PatientRecord.mayOpen ucA.UserId (headOf pat1 bSaves).Value.Id).IsSome)
// ── UC-5 ext 6a — B guesses instead ──
let guessed =
step "UC-5 ext 6a — B guesses at A's PIN" bTriesToSign
[
act 1 (Signs(Pin "0001"))
act 1 (Signs(Pin "0002"))
]
expect "6a at the configured number of consecutive wrong entries the Session ends (Rules 9, 27)"
(openCount guessed = 0
&& (match stateOf 1 guessed with Some(Ended(WrongPinLimit, _)) -> true | _ -> false))
expect "6a the Unsigned TreatmentPlan stays, and A is told of the ending (Rule 10)"
(planCount pat1 guessed = 1
&& saw (function SessionEnded(Some WrongPinLimit) -> true | _ -> false))
let relaunchNoHelp =
step "UC-5 ext 6a — relaunching as A does not reset the count (Rule 27)" guessed
(launchAs ucA.Login (Some pat1) @ [ act 2 (Signs(Pin "0003")) ])
expect "6a the count belongs to the UserCredential, so guessing is capped outright"
((credentialOf ucA relaunchNoHelp |> Option.map _.AttemptCount |> Option.map (fun c -> c >= wrongPinLimit))
= Some true)
bSignedOwn
// ═══════════════════════════════════════════════════════════════════════════════
// UC-6 Two Users, one Patient
// ═══════════════════════════════════════════════════════════════════════════════
let uc6 () =
printfn ""
printfn "############### UC-6 Two Users, one Patient ###############"
// Precondition: A and B each hold an open Session for Patient 2. Rule 7 permits
// this: it limits Sessions per User, not per Patient.
let both =
step "UC-6 precondition — A and B each open a Session for Patient 2" world
(launchAs ucA.Login (Some pat2) @ launchAs ucB.Login (Some pat2))
expect "UC-6 Rule 7 limits Sessions per User, not per Patient: both are open"
(openCount both = 2
&& (openOfUser ucA both).Length = 1
&& (openOfUser ucB both).Length = 1)
// Guarantee 3, and the reason it now holds by construction: the two carts are in
// two Browsers, and the Server holds neither (Rule 31).
expect "UC-6 the two carts are in the two Clients, and nowhere else (Rule 31, Guarantee 3)"
(both.GenPres.InFlight.IsEmpty && sidAt 1 both <> sidAt 2 both)
let aSigned =
step "UC-6 step 2 — A saves and signs" both
[
act 1 (Prescribes(OrderContextId "oc-a"))
act 1 Saves
act 1 (Signs pinA)
]
expect "UC-6 step 2: an Unsigned then a Signed TreatmentPlan in A's name"
(planCount pat2 aSigned = 3
&& (headOf pat2 aSigned |> Option.map _.Signed) = Some true
&& (headOf pat2 aSigned |> Option.map _.By) = Some ucA)
// Consequence 6: neither User saw the other's work — a Client only learns anything
// at its own next request.
let bBlocked =
step "UC-6 step 3 — B saves, and is blocked" aSigned
[
act 2 (Prescribes(OrderContextId "oc-b"))
act 2 Saves
]
expect "UC-6 step 3: a Signed TreatmentPlan newer than the one B opened with blocks the create (Rule 20)"
(saw (function CreateBlocked _ -> true | _ -> false)
&& planCount pat2 bBlocked = 3)
let bTookOver =
step "UC-6 step 4 — B opens A's Signed TreatmentPlan, which lifts the block (Rule 17)" bBlocked
[ act 2 (OpensTreatmentPlan (headOf pat2 bBlocked).Value.Id) ]
expect "UC-6 step 4: opening it re-mints the token, so it is what the Session opened with (Rule 33)"
(saw (function TreatmentPlanOpened _ -> true | _ -> false)
&& openedAt 2 bTookOver = (headOf pat2 bBlocked |> Option.map _.Id))
let bReapplied =
step "UC-6 step 4 — B reapplies their own work, saves and signs" bTookOver
[
act 2 (Prescribes(OrderContextId "oc-b"))
act 2 (Signs pinB)
]
expect "UC-6 step 4: the signature attests the whole set in B's name (Rules 14, 15)"
((headOf pat2 bReapplied |> Option.map _.By) = Some ucB
&& (headOf pat2 bReapplied |> Option.map _.Signed) = Some true)
// Rule 14, the half that only shows here — and Rule 35, which is how the Server
// knows: it diffed the payload against the base TreatmentPlan, rather than believing
// any stamp the Client sent.
let orders = headOf pat2 bReapplied |> Option.map _.Orders |> Option.defaultValue []
expect "UC-6 step 4: the OrderContext B changed carries B's stamp"
(orders |> List.exists (fun o -> o.Id = OrderContextId "oc-b" && o.Stamp = Some ucB))
expect "UC-6 step 4: the ones B left untouched keep A's stamp (Rules 14, 35)"
(orders |> List.exists (fun o -> o.Id = OrderContextId "oc-a" && o.Stamp = Some ucA)
&& orders |> List.exists (fun o -> o.Id = OrderContextId "oc-1" && o.Stamp = Some ucA))
// ── UC-6 ext 2a — B saves, Unsigned, before A signs ──
let bSavedFirst =
step "UC-6 ext 2a — B saves Unsigned before A signs" both
[
act 2 (Prescribes(OrderContextId "oc-b"))
act 2 Saves
]
expect "2a B is not blocked: nothing Signed is newer (Rule 20)"
(never (function CreateBlocked _ -> true | _ -> false)
&& planCount pat2 bSavedFirst = 2)
let _ =
step "UC-6 ext 2a — but A is notified when creating (Rule 21)" bSavedFirst
[ act 1 Saves ]
expect "2a A is told whose work it is, and may proceed or hold off"
(saw (function UnsignedWorkNotice(uc, _) -> uc = ucB | _ -> false))
// Nothing attested is ever lost: the PatientRecord is append-only (Concept 12), so
// a Signed TreatmentPlan survives whatever follows. What is not protected is Unsigned
// work: superseded, it can never be signed (Rules 19, 20).
expect "UC-6 nothing attested is lost: A's Signed TreatmentPlan survives B's (Concept 12)"
(recordFor pat2 bReapplied
|> _.Plans
|> List.exists (fun s -> s.Signed && s.By = ucA))
bReapplied
// ═══════════════════════════════════════════════════════════════════════════════
// UC-7 A User forgets their PIN
// ═══════════════════════════════════════════════════════════════════════════════
let uc7 () =
printfn ""
printfn "############### UC-7 A User forgets their PIN ###############"
// Precondition: A has an open Session and a UserCredential with a PIN set but
// forgotten.
let opened = quiet "UC-7 precondition" world (launchAs ucA.Login (Some pat2))
let reset = step "UC-7 steps 1 and 2 — A asks GenPRES to reset the PIN" opened [ act 1 AsksPinReset ]
expect "UC-7 step 2: the PIN is removed and the UserCredential stays (Concept 7)"
((credentialOf ucA reset).IsSome
&& (credentialOf ucA reset |> Option.bind _.Pin) = None)
// Rule 26 has to reach A with no Session in memory to ask, so the address comes
// off the SessionRecord (Concept 9).
expect "UC-7 step 2: the change is recorded and A is mailed (Rule 26, Concept 9)"
((mailsTo mailA reset).Length = 1
&& reset.Audit |> List.exists (fun a -> a.Contains "PIN removed"))
let stillSaves =
step "UC-7 step 3 — A can still save" reset
[ act 1 (Prescribes(OrderContextId "oc-r")); act 1 Saves ]
expect "UC-7 step 3: saving still works"
(planCount pat2 stillSaves = 2 && (headOf pat2 stillSaves |> Option.map _.Signed) = Some false)
let cannotSign =
step "UC-7 step 3 — but a UserCredential without a PIN cannot sign" stillSaves [ act 1 (Signs pinA) ]
expect "UC-7 step 3: nothing verifies, so nothing is signed (Concept 7, Rule 22)"
(saw (function PinRejected _ -> true | _ -> false)
&& (recordFor pat2 cannotSign |> PatientRecord.latestSigned |> Option.map _.Id) = Some p2Signed.Id)
let relaunched = step "UC-7 step 4 — A relaunches; UC-2 follows (Rules 23, 24)" reset (launchAs ucA.Login (Some pat2))
expect "UC-7 step 4: no PIN is set and A holds the Prescriber Role, so one is asked for"
(saw (function PinRequired _ -> true | _ -> false))
let newPin = step "UC-7 step 5 — A sets a new PIN, and is mailed again (Rule 26)" relaunched [ atClient 2 (ChoosePin(Pin "5555")) ]
expect "UC-7 step 5: a mail goes to A each time — once at removal, once at the new setting"
((mailsTo mailA newPin).Length = 2)
expect "UC-7 step 5: and the new PIN starts with a count of zero (Rule 27)"
((credentialOf ucA newPin |> Option.map _.AttemptCount) = Some 0)
// ── UC-7 ext 1a — B, at A's open workstation, triggers the reset ──
// Every step runs the same way, and B ends up able to sign as A. This cannot be
// prevented: a launch proves control of a MainEHR Session, not a person
// (Possibility 1). What the mails buy is that A learns of it through a channel B
// does not control.
let bResets = step "UC-7 ext 1a — B triggers the reset at A's open workstation" opened [ act 1 AsksPinReset ]
expect "1a it cannot be prevented — but the mail goes to A, not to whoever did it"
((credentialOf ucA bResets |> Option.bind _.Pin) = None
&& (mailsTo mailA bResets).Length = 1
&& (mailsTo mailB bResets).Length = 0)
expect "1a and the recorded change shows which TreatmentPlans were signed afterwards"
(bResets.Audit |> List.exists (fun a -> a.Contains "dr.a"))
newPin
// ═══════════════════════════════════════════════════════════════════════════════
// UC-8 User opens GenPRES directly
// ═══════════════════════════════════════════════════════════════════════════════
let uc8 () =
printfn ""
printfn "############### UC-8 User opens GenPRES directly ###############"
// GenPRES as Clinical Decision Support, not as order management. No launch, so no
// LaunchCredential — and GenPRES cannot know who is at the keyboard.
let anon = step "UC-8 steps 1 to 3 — A opens the GenPRES address in a browser" world [ atClient 1 OpenDirectly ]
expect "UC-8 step 3: an anonymous Session — no User, no Role, no PatientId (Rule 13)"
(openCount anon = 1
&& (newestRecord anon |> Option.bind _.User) = None
&& (newestRecord anon |> Option.bind _.Patient) = None)
expect "UC-8 step 3: its SessionRecord binds to no User (Concept 9)"
((recNo 1 anon |> Option.bind _.User) = None
&& (recNo 1 anon |> Option.bind _.Launch) = None)
expect "UC-8 anonymous use needs no Role and no UserRegistry check"
(never (function ResolveUser _ -> true | _ -> false))
let prescribing =
step "UC-8 step 4 — A prescribes: Patient Data and OrderContexts by hand" anon
[
act 1 (EntersPatientData(PatientData "3y, 14kg, by hand"))
act 1 (Prescribes(OrderContextId "oc-x"))
]
expect "UC-8 step 4: prescribing works, Patient Data included (Concepts 2, 15)"
((dataAt 1 prescribing).IsSome && (workingAt 1 prescribing).Length = 1)
expect "UC-8 step 4: each request refreshes the Session's idle clock (Rules 8, 12)"
(countOf (function SessionRequest _ -> true | _ -> false) = 2
&& lastSeenOf 1 prescribing > (recNo 1 anon |> Option.map _.LastSeen))
let noSaving = step "UC-8 step 5 — nothing can be saved" prescribing [ act 1 Saves; act 1 (Signs pinA) ]
expect "UC-8 step 5: no TreatmentPlan can be opened or created (Rule 12)"
(saw (function NoTreatmentPlanHere -> true | _ -> false)
&& never (function TreatmentPlanCreated _ -> true | _ -> false))
expect "UC-8 neither the PatientRecord nor the PatientDataPlatform is ever touched"
(never (function ReadRecord _ -> true | _ -> false)
&& never (function ReadPatientData _ -> true | _ -> false))
expect "UC-8 step 5: the work exists only in the Client (Rule 31)"
((workingAt 1 noSaving).Length = 1 && noSaving.GenPres.InFlight.IsEmpty)
let idled = step "UC-8 — and it need not idle out: keeping it has no consequence (Rule 13)" noSaving (ticks 30)
expect "UC-8 an anonymous Session may remain open indefinitely (Rule 13)"
(openCount idled = 1 && stateOf 1 idled = Some OpenOrGone)
// ── UC-8 ext 2a — the browser does present a LaunchCredential ──
// That is a launch: UC-1 from step 7. Covered by UC-1 throughout.
// ── UC-8 ext 2b — the same Browser later launches properly ──
// The launched Session is another Session; Rule 7 counts only a User's Sessions,
// and an anonymous Session binds to none. (The model opens the launch in a fresh
// tab, since a launch always does; nothing in the Rules turns on that.)
let alsoLaunched = step "UC-8 ext 2b — the same person later launches properly" idled (launchAs ucA.Login (Some pat1))
expect "2b the anonymous Session is untouched and may simply live on (Rules 7, 13)"
(openCount alsoLaunched = 2
&& stateOf 1 alsoLaunched = Some OpenOrGone
&& never (function PriorSessionNotice _ -> true | _ -> false))
// And the work in the browser is gone when the browser goes — it was only ever
// there (Rule 31).
let browserClosed = step "UC-8 step 5 — and it is gone when the browser goes" idled [ atClient 1 CloseBrowser ]
expect "UC-8 step 5: the cart dies with the browser (Rule 31)"
(workingAt 1 browserClosed).IsEmpty
idled
// ═══════════════════════════════════════════════════════════════════════════════
// UC-9 A Session ends out from under the User
// ═══════════════════════════════════════════════════════════════════════════════
let uc9 () =
printfn ""
printfn "############### UC-9 A Session ends out from under the User ###############"
// Precondition: UC-3 ran through step 2 and stopped. A's Session for Patient 2 is
// open, an Unsigned TreatmentPlan of A's stands at the head, and further unsaved
// changes sit on the screen.
let saved =
quiet "UC-9 precondition" world
(launchAs ucA.Login (Some pat2)
@ [
act 1 (Prescribes(OrderContextId "oc-4"))
act 1 Saves
act 1 (Prescribes(OrderContextId "oc-unsaved"))
])
expect "UC-9 precondition: an Unsigned TreatmentPlan stands, and one change is unsaved"
(planCount pat2 saved = 2 && (workingAt 1 saved).Length = 3)
let idled = step "UC-9 step 1 — A is called away, and the idle clock runs out (Rules 8, 9)" saved (ticks 12)
expect "UC-9 step 1: the Session ends and its record is marked ended"
(openCount idled = 0
&& (match stateOf 1 idled with Some(Ended(Idle, _)) -> true | _ -> false))
expect "UC-9 step 1: the ending creates the obligation — a notice is now owed (Rule 10)"
(noticeOf 1 idled = Some Owed)
// Step 2: the Server cannot reach the Client, which keeps showing a live-looking
// screen (Consequence 6). Nothing was sent, and nothing could have been.
expect "UC-9 step 2: nothing was sent to the Client when the Session ended (Consequence 6)"
(never (function SessionEnded _ -> true | _ -> false))
let told = step "UC-9 steps 3 and 4 — A returns and acts" idled [ act 1 (Prescribes(OrderContextId "oc-later")) ]
expect "UC-9 step 4: the request is refused, A is told, and the obligation is spent"
(saw (function SessionEnded(Some Idle) -> true | _ -> false)
&& wasTold 1 told)
// Step 5, the change the stateless design makes. The unsaved work was never
// anywhere but the Client (Rule 31): the ended Session accepts nothing, but the
// Client still holds it.
expect "UC-9 step 5: the unsaved changes are still in the Client (Rule 31)"
((workingAt 1 told) |> List.exists (fun o -> o.Id = OrderContextId "oc-unsaved"))
expect "UC-9 step 5: and they never reached the record (Concept 15)"
(planCount pat2 told = 2
&& (headOf pat2 told
|> Option.map _.Orders
|> Option.defaultValue []
|> List.exists (fun o -> o.Id = OrderContextId "oc-unsaved")
|> not))
expect "UC-9 step 5: the Unsigned TreatmentPlan stands, A's own to resume (Rules 18, 19)"
((recordFor pat2 told |> PatientRecord.startsFrom ucA.UserId |> Option.map _.Id)
= (headOf pat2 told |> Option.map _.Id))
let relaunched = step "UC-9 step 6 — A relaunches. Told once already, A is not told again (Rule 10)" told (launchAs ucA.Login (Some pat2))
expect "UC-9 step 6: no notice at the relaunch"
(never (function PriorSessionNotice _ -> true | _ -> false))
// Step 5 continued: the Client may offer to carry the surviving cart into the next
// Session as fresh prescribing (Concept 15) — not as a resumed Session.
let carried =
step "UC-9 step 5 — A carries the surviving work into the new Session" relaunched
[
act 2 (CarriesOverFrom(BrowserId 1))
act 2 Saves
]
expect "UC-9 step 5: the unsaved OrderContext from before the idle-out lands in the next TreatmentPlan"
(headOf pat2 carried
|> Option.map _.Orders
|> Option.defaultValue []
|> List.exists (fun o -> o.Id = OrderContextId "oc-unsaved"))
expect "UC-9 step 5: and it is fresh prescribing — stamped by A in this Session (Rules 14, 35)"
(headOf pat2 carried
|> Option.map _.Orders
|> Option.defaultValue []
|> List.exists (fun o -> o.Id = OrderContextId "oc-unsaved" && o.Stamp = Some ucA))
// "They survive exactly as far as the browser does — closed, they are gone."
let browserGoneFirst =
step "UC-9 step 5 — but close the browser first, and there is nothing to carry" told
([ atClient 1 CloseBrowser ] @ launchAs ucA.Login (Some pat2))
let nothingCarried =
step "UC-9 step 5 — the new Session gets only what the record held" browserGoneFirst
[
act 2 (CarriesOverFrom(BrowserId 1))
act 2 Saves
]
expect "UC-9 step 5: closed is gone — the unsaved work is nowhere"
(headOf pat2 nothingCarried
|> Option.map _.Orders
|> Option.defaultValue []
|> List.exists (fun o -> o.Id = OrderContextId "oc-unsaved")
|> not)
// ── UC-9 ext 1a — the Server restarts instead ──
// Nothing ends. This is the headline change of the stateless design: the Session's
// identity and standing are in its SessionRecord, its work is in the Client, and
// the Server held neither (Rules 9, 31).
let restarted =
step "UC-9 ext 1a — the Server restarts instead" saved
[ envt GenPresServer (Stop GenPresServer); tick; envt GenPresServer (Start GenPresServer) ]
expect "1a nothing ends: the Session is still open (Rules 9, 31)"
(openCount restarted = 1 && stateOf 1 restarted = Some OpenOrGone)
expect "1a the Server settled nothing at the start — there was nothing to settle"
(never (function ReadSessionRecords ForSweep -> true | _ -> false)
&& never (function WriteSessionRecord _ -> true | _ -> false))
expect "1a the Client still holds its cart (Rule 31)"
((workingAt 1 restarted).Length = 3)
let seenBefore = lastSeenOf 1 restarted
let afterRestart =
step "1a — and the next request continues the Session (Rules 8, 9)" restarted
[ act 1 (Prescribes(OrderContextId "oc-after-restart")) ]
expect "1a the next request is served, and refreshes the idle clock"
(saw (function Computed _ -> true | _ -> false)
&& never (function SessionEnded _ -> true | _ -> false)
&& lastSeenOf 1 afterRestart > seenBefore)
// While it is down, requests fail as in UC-1 ext 7a.
let whileDown =
step "1a — while it is down, requests fail as in UC-1 ext 7a" saved
[ envt GenPresServer (Stop GenPresServer); act 1 (Prescribes(OrderContextId "oc-nope")) ]
expect "1a a down Server is unreachable, not an ending"
(saw (function ServerUnreachable -> true | _ -> false)
&& stateOf 1 whileDown = Some OpenOrGone)
// ── UC-9 ext 1b — A opens another Session at another workstation ──
let elsewhere = step "UC-9 ext 1b — A opens another Session instead" saved (launchAs ucA.Login (Some pat2))
expect "1b the launch itself ends the old Session, and the notice comes with it (Rules 7, 9, 10)"
(openCount elsewhere = 1
&& (match stateOf 1 elsewhere with Some(Ended(Superseded, _)) -> true | _ -> false)
&& saw (function PriorSessionNotice _ -> true | _ -> false))
let oldTab = step "UC-9 ext 1b — the old Client's next request is refused, but not told twice (Rule 10)" elsewhere [ act 1 (Prescribes(OrderContextId "oc-z")) ]
expect "1b refused, and the notice is not repeated"
(saw (function SessionRefused -> true | _ -> false)
&& never (function SessionEnded _ -> true | _ -> false))
ignore oldTab
told
// ═══════════════════════════════════════════════════════════════════════════════
// UC-10 A Reader consults a Patient
// ═══════════════════════════════════════════════════════════════════════════════
let uc10 () =
printfn ""
printfn "############### UC-10 A Reader consults a Patient ###############"
// Precondition: as UC-9. Patient 2's head is an Unsigned TreatmentPlan of A's over its
// Signed one. C, a Reader, launches for Patient 2.
let withUnsignedHead =
quiet "UC-10 precondition" world
(launchAs ucA.Login (Some pat2)
@ [ act 1 (Prescribes(OrderContextId "oc-4")); act 1 Saves ])
let reading = step "UC-10 steps 1 and 2 — C launches for Patient 2" withUnsignedHead (launchAs ucC.Login (Some pat2))
expect "UC-10 step 1: C never creates a TreatmentPlan, so no Unsigned one of their own can exist (Rules 17, 19)"
(openedAt 2 reading = Some p2Signed.Id)
expect "UC-10 step 2: C reads the plan that counts clinically (Rule 16)"
(workingAt 2 reading = p2Signed.Orders)
expect "UC-10 step 3: A's newer Unsigned TreatmentPlan is not shown — only its creator can open it (Rule 18)"
(recordFor pat2 reading |> PatientRecord.mayOpen ucC.UserId (headOf pat2 reading).Value.Id).IsNone
// Its existence is not announced either: the only notification of another's
// Unsigned work fires at TreatmentPlan creation (Rule 21), and a Reader never creates.
let exploring =
step "UC-10 step 4 — C prescribes within the Session to explore alternatives" reading
[
act 2 (Prescribes(OrderContextId "oc-what-if"))
act 2 Saves
act 2 (Signs(Pin "0000"))
]
expect "UC-10 step 4: prescribing works (Concept 15), but saving and signing are not offered"
(saw (function Computed _ -> true | _ -> false)
&& saw (function NotPermitted -> true | _ -> false)
&& planCount pat2 exploring = planCount pat2 reading)
expect "UC-10 step 4: no PIN is ever asked for, and none is ever read (Rule 25)"
(never (function PinRequired _ -> true | _ -> false)
&& never (function ReadCredential _ -> true | _ -> false))
expect "UC-10 step 3: the existence of A's Unsigned work goes unannounced (Rule 21)"
(never (function UnsignedWorkNotice _ -> true | _ -> false))
// A Reader can thus be reading a plan that a Prescriber already knows is being
// superseded. The model accepts this deliberately: Unsigned work counts for
// nothing until it is signed (Rule 16), so there is nothing yet to tell a Reader.
exploring
// ═══════════════════════════════════════════════════════════════════════════════
// UC-11 A User resumes their own Unsigned work
// ═══════════════════════════════════════════════════════════════════════════════
let uc11 () =
printfn ""
printfn "############### UC-11 A User resumes their own Unsigned work ###############"
// Precondition: UC-9 completed. Patient 2's head is A's own Unsigned TreatmentPlan over
// the older Signed one, and A launches again for Patient 2.
let parked =
quiet "UC-11 precondition" world
(launchAs ucA.Login (Some pat2)
@ [ act 1 (Prescribes(OrderContextId "oc-4")); act 1 Saves ]
@ ticks 12)
let resumed = step "UC-11 step 1 — A launches again for Patient 2" parked (launchAs ucA.Login (Some pat2))
expect "UC-11 step 1: the Session starts from A's own Unsigned head, not the older Signed one (Rule 19)"
(openedAt 2 resumed = (headOf pat2 resumed |> Option.map _.Id))
expect "UC-11 step 1: and it carries the work that was saved into it"
((workingAt 2 resumed).Length = 2)
let signed =
step "UC-11 steps 2 and 3 — A reviews, adjusts and signs" resumed
[
act 2 (Prescribes(OrderContextId "oc-4"))
act 2 (Signs pinA)
]
expect "UC-11 step 3: nothing blocks and nothing warns (Rules 20, 21)"
(never (function CreateBlocked _ -> true | _ -> false)
&& never (function UnsignedWorkNotice _ -> true | _ -> false))
expect "UC-11 step 3: a Signed TreatmentPlan in A's name; it now counts clinically (Rules 14, 15, 16)"
((headOf pat2 signed |> Option.map _.Signed) = Some true
&& (headOf pat2 signed |> Option.map _.By) = Some ucA
&& (recordFor pat2 signed |> PatientRecord.latestSigned |> Option.map _.Id)
= (headOf pat2 signed |> Option.map _.Id))
expect "UC-11 step 3: the TreatmentPlan's base is the Unsigned one it was resumed from (Concept 13)"
((headOf pat2 signed |> Option.bind _.Base) = (headOf pat2 resumed |> Option.map _.Id))
// ── UC-11 ext 3a — a Signed TreatmentPlan appeared since the launch ──
let bSignedMeanwhile =
quiet "UC-11 ext 3a setup" resumed
(launchAs ucB.Login (Some pat2)
@ [
act 3 (Prescribes(OrderContextId "oc-c"))
// B opened from the older Signed TreatmentPlan, so A's Unsigned head is
// newer and Rule 21 fires on B as well. B re-sends with the token.
act 3 (Signs pinB)
act 3 (Signs pinB)
])
let aBlocked =
step "UC-11 ext 3a — A signs after a Signed TreatmentPlan appeared" bSignedMeanwhile
[ act 2 (Signs pinA) ]
expect "3a creating is blocked (Rule 20)"
(saw (function CreateBlocked _ -> true | _ -> false))
let aRecovered =
step "UC-11 ext 3a — A opens it, reapplies, and continues (Rule 17; UC-6 step 4)" aBlocked
[
act 2 (OpensTreatmentPlan (headOf pat2 aBlocked).Value.Id)
act 2 (Prescribes(OrderContextId "oc-4"))
act 2 (Signs pinA)
]
expect "3a opening the newest Signed TreatmentPlan lifts the block"
((headOf pat2 aRecovered |> Option.map _.By) = Some ucA
&& (headOf pat2 aRecovered |> Option.map _.Signed) = Some true)
// ── UC-11 ext 3b — another User's Unsigned TreatmentPlan appeared since the launch ──
let bSavedMeanwhile =
quiet "UC-11 ext 3b setup" resumed
(launchAs ucB.Login (Some pat2)
@ [
act 3 (Prescribes(OrderContextId "oc-d"))
act 3 Saves
act 3 Saves
])
let aWarned =
step "UC-11 ext 3b — A signs after another's Unsigned TreatmentPlan appeared" bSavedMeanwhile
[ act 2 (Signs pinA) ]
expect "3b A is notified and decides (Rule 21) — not blocked (Rule 20)"
(saw (function UnsignedWorkNotice(uc, _) -> uc = ucB | _ -> false)
&& never (function CreateBlocked _ -> true | _ -> false))
ignore aWarned
signed
// ═══════════════════════════════════════════════════════════════════════════════
// UC-12 User closes GenPRES
// ═══════════════════════════════════════════════════════════════════════════════
let uc12 () =
printfn ""
printfn "############### UC-12 User closes GenPRES ###############"
// Precondition: UC-11 completed. A has an open Session for Patient 2, its work
// signed, and nothing unsaved remains.
let signedUp =
quiet "UC-12 precondition" world
(launchAs ucA.Login (Some pat2)
@ [ act 1 (Prescribes(OrderContextId "oc-4")); act 1 (Signs pinA) ])
let closed = step "UC-12 steps 2 and 3 — A closes the Session in the Client" signedUp [ act 1 ClosesSession ]
expect "UC-12 step 3: the Session ends, marked closed by the User (Rule 9, Concept 9)"
(openCount closed = 0
&& (match stateOf 1 closed with Some(Ended(ClosedByUser, _)) -> true | _ -> false))
expect "UC-12 step 3: and no notice is ever owed — not owed and then skipped (Rule 10)"
(noticeOf 1 closed = Some NotOwed)
let nextLaunch = step "UC-12 step 4 — the next launch starts clean" closed (launchAs ucA.Login (Some pat2))
expect "UC-12 step 4: no notice follows — Rule 10 speaks only of endings other than by the User"
(never (function PriorSessionNotice _ -> true | _ -> false)
&& noticeOf 1 nextLaunch = Some NotOwed)
// ── UC-12 ext 1a — unsaved changes remain at the close ──
let withUnsaved =
quiet "UC-12 ext 1a setup" signedUp [ act 1 (Prescribes(OrderContextId "oc-dangling")) ]
let closedAnyway = step "UC-12 ext 1a — A closes with unsaved changes: closed is closed" withUnsaved [ act 1 ClosesSession ]
expect "1a they existed only in the Client and are gone (Rule 31); anything saved stands (Concept 12)"
(openCount closedAnyway = 0
&& (workingAt 1 closedAnyway).IsEmpty
&& planCount pat2 closedAnyway = 2
&& (headOf pat2 closedAnyway
|> Option.map _.Orders
|> Option.defaultValue []
|> List.exists (fun o -> o.Id = OrderContextId "oc-dangling")
|> not))
// ── UC-12 ext 2a — A closes the browser instead ──
let browserGone = step "UC-12 ext 2a — A closes the browser instead" signedUp [ atClient 1 CloseBrowser ]
expect "2a nothing reaches the Server, so no close can be inferred (Rule 9)"
(openCount browserGone = 1
&& stateOf 1 browserGone = Some OpenOrGone
&& never (function SessionRequest _ -> true | _ -> false))
let idledOut = step "UC-12 ext 2a — the Session idles out instead" browserGone (ticks 12)
expect "2a it idles out, and A is told at the next opportunity (Rule 10; UC-9)"
(match stateOf 1 idledOut with Some(Ended(Idle, _)) -> true | _ -> false)
let harmlessNotice = step "UC-12 ext 2a — a harmless notice, the price of the indistinguishability" idledOut (launchAs ucA.Login (Some pat2))
expect "2a the notice arrives at the next launch"
(saw (function PriorSessionNotice _ -> true | _ -> false))
ignore harmlessNotice
closed
// ═══════════════════════════════════════════════════════════════════════════════
// UC-13 A User's authority is withdrawn
// ═══════════════════════════════════════════════════════════════════════════════
let uc13 () =
printfn ""
printfn "############### UC-13 A User's authority is withdrawn ###############"
// Precondition: UC-3 ran once more through step 2 and stopped. Patient 2's head is
// an Unsigned TreatmentPlan of A's over the Signed one. Then the UserRegistry stops
// returning a Role for A's login.
let aSaved =
quiet "UC-13 precondition" world
(launchAs ucA.Login (Some pat2)
@ [ act 1 (Prescribes(OrderContextId "oc-4")); act 1 Saves ])
let withdrawn = { aSaved with Registry.Users = aSaved.Registry.Users |> Map.remove ucA.Login }
let refused = step "UC-13 steps 1 and 2 — A launches; the registry returns no Role" withdrawn (launchAs ucA.Login (Some pat2))
// A's Session from the precondition is still open, and stays open — that is ext 1a
// below. What the failed launch must not do is open another one.
expect "UC-13 step 2: no Role, so the launch opens no Session (Rules 5, 6)"
(saw (function UserUnresolved(_, NoRole) -> true | _ -> false)
&& saw (function NotAuthorised -> true | _ -> false)
&& never (function SessionOpened _ -> true | _ -> false))
let cds = step "UC-13 step 3 — A accepts the anonymous open: CDS is all that remains" refused [ atClient 2 AcceptAnonymousOffer ]
expect "UC-13 step 3: hand-entered patients, no records, nothing saved (UC-8; Rule 13)"
((newestRecord cds |> Option.bind _.User) = None
&& (newestRecord cds |> Option.bind _.Patient) = None)
let againRefused = step "UC-13 step 3 — every later launch ends the same way (Rule 5)" cds (launchAs ucA.Login (Some pat2))
expect "UC-13 step 3: the Role is taken from the registry at each launch, so the withdrawal stands"
(saw (function NotAuthorised -> true | _ -> false))
expect "UC-13 step 4: A's UserCredential remains, but is inert (Concepts 7, 14)"
((credentialOf ucA againRefused).IsSome
&& (credentialOf ucA againRefused |> Option.bind _.Pin).IsSome)
// ── step 5 — the Unsigned TreatmentPlan is stranded ──
let bWorksPast =
step "UC-13 step 5 — B's next Session starts from the Signed TreatmentPlan below (Rule 19)" againRefused
(launchAs ucB.Login (Some pat2))
expect "UC-13 step 5: only A could open the stranded work, and A can no longer reach it"
(openedAt 4 bWorksPast = Some p2Signed.Id)
let bNotified =
step "UC-13 step 5 — B is notified of the stranded work at the save (Rule 21)" bWorksPast
[ act 4 (Prescribes(OrderContextId "oc-e")); act 4 (Signs pinB) ]
expect "UC-13 step 5: B is told whose work it is"
(saw (function UnsignedWorkNotice(uc, _) -> uc = ucA | _ -> false))
let superseded = step "UC-13 step 5 — B re-sends with the token, and their signature supersedes it for good" bNotified [ act 4 (Signs pinB) ]
expect "UC-13 step 5: B's Signed TreatmentPlan now counts, and A's work can never be signed (Rules 16, 20)"
((headOf pat2 superseded |> Option.map _.By) = Some ucB
&& (headOf pat2 superseded |> Option.map _.Signed) = Some true)
// ── UC-13 ext 1a — the withdrawal happens while A's Session is open ──
// Rule 5 checks at the launch, just as Concept 2 reads data at the launch:
// in-Session currency of the Role is accepted the same way. With no Session in
// memory, this is Concept 9 doing the work — the Role comes off the SessionRecord
// the launch wrote, and the registry is not asked again (Rule 32).
let stillWorking =
step "UC-13 ext 1a — the withdrawal lands while A's Session is open" withdrawn
[ act 1 (Prescribes(OrderContextId "oc-f")); act 1 (Signs pinA) ]
expect "1a the open Session keeps the Role its launch established (Concept 9, Rule 32)"
((headOf pat2 stillWorking |> Option.map _.By) = Some ucA
&& (headOf pat2 stillWorking |> Option.map _.Signed) = Some true
&& never (function ResolveUser _ -> true | _ -> false))
superseded
// ═══════════════════════════════════════════════════════════════════════════════
// Rules 32 to 36 — the stateless design under attack
// ═══════════════════════════════════════════════════════════════════════════════
//
// The cart is in the Client now (Rule 31), so everything the Server used to know by
// remembering it must instead arrive with the request — and be worth nothing unless
// the Server itself vouched for it. These are the tests that say so: a Client that
// edits a token, invents one, lies about the Patient, or forges a stamp, and a
// Database that arbitrates two Servers racing for the same head.
/// A Client putting an envelope on the wire by hand — which is what an attacker has,
/// and what the honest Client's own branches deliberately never do.
let fromClient b msg = { From = GenPresClient(BrowserId b); To = GenPresServer; Msg = msg }
let tokensAndArbitration () =
printfn ""
printfn "############### Rules 32-36 The stateless design under attack ###############"
// ── Rule 33: an opened-with token the Client edited ──
let both =
quiet "tokens precondition" world
(launchAs ucA.Login (Some pat2) @ launchAs ucB.Login (Some pat2))
let bWon =
step "Rule 33 setup — B signs, so A's opened-with token is now stale" both
[ act 2 (Prescribes(OrderContextId "oc-b")); act 2 (Signs pinB) ]
let newestSigned = (recordFor pat2 bWon |> PatientRecord.latestSigned |> Option.map _.Id).Value
let honestStale = step "Rule 33 — A's honest but stale token: blocked, as before (Rule 20)" bWon [ act 1 Saves ]
expect "Rule 33 an honest stale token is believed, and Rule 20 does the refusing"
(saw (function CreateBlocked _ -> true | _ -> false)
&& never (function CreateRefused _ -> true | _ -> false)
&& planCount pat2 honestStale = planCount pat2 bWon)
// Now A edits the token to name the newest Signed TreatmentPlan — which would lift the
// Rule 20 block — and guesses at the mac.
let forged =
let sid = (sidAt 1 bWon).Value
let tok = { Sid = sid; Patient = Some pat2; Plan = Some newestSigned; Mac = "mac|guessed" }
step "Rule 33 — A edits the token to name the newest Signed TreatmentPlan" bWon
[ fromClient 1 (SessionRequest(sid, CreateTreatmentPlan(None, workingAt 1 bWon, None, tok, None))) ]
expect "Rule 33 the token does not verify, so the create is refused — not merely blocked"
(saw (function CreateRefused _ -> true | _ -> false)
&& never (function TreatmentPlanCreated _ -> true | _ -> false)
&& planCount pat2 forged = planCount pat2 bWon)
// ── Rule 34: a notice token that is out of date, and one the Client made ──
let bOpen = quiet "Rule 34 precondition" world (launchAs ucB.Login (Some pat3))
let bWarned = step "Rule 34 — B saves and is notified of A's Unsigned work (Rule 21)" bOpen [ act 1 Saves ]
expect "Rule 34 the notice disclosed exactly the one Unsigned TreatmentPlan that exists"
((noticeAt 1 bWarned |> Option.map _.Disclosed) = Some [ p3Unsigned.Id ])
// While B deliberates, A saves again: a *newer* Unsigned TreatmentPlan of another User,
// which B's token does not name.
let aSavedMeanwhile =
quiet "Rule 34 — A saves again while B deliberates" bWarned
(launchAs ucA.Login (Some pat3)
@ [ act 2 (Prescribes(OrderContextId "oc-a2")); act 2 Saves ])
let notifiedAgain =
step "Rule 34 — B returns the token it was given, but the record has moved on" aSavedMeanwhile
[ act 1 Saves ]
expect "Rule 34 the token is honoured for what it disclosed and for nothing newer"
(saw (function UnsignedWorkNotice _ -> true | _ -> false)
&& never (function TreatmentPlanCreated _ -> true | _ -> false)
&& planCount pat3 notifiedAgain = planCount pat3 aSavedMeanwhile)
let thenAccepted = step "Rule 34 — B returns the fresh token, and the create lands" notifiedAgain [ act 1 Saves ]
expect "Rule 34 a token naming everything outstanding is honoured"
(planCount pat3 thenAccepted = planCount pat3 notifiedAgain + 1
&& (headOf pat3 thenAccepted |> Option.map _.By) = Some ucB)
let _ =
let sid = (sidAt 1 bOpen).Value
let tok = { Sid = sid; Disclosed = [ p3Unsigned.Id ]; Mac = "i-made-this-up" }
let opened = (clientOf 1 bOpen).Value.Opened.Value
step "Rule 34 — B skips the notice by inventing a token" bOpen
[
fromClient 1
(SessionRequest(sid, CreateTreatmentPlan(None, workingAt 1 bOpen, None, opened, Some tok)))
]
expect "Rule 34 a self-made token is treated as none at all: B is notified, not honoured"
(saw (function UnsignedWorkNotice _ -> true | _ -> false)
&& never (function TreatmentPlanCreated _ -> true | _ -> false))
// ── Rule 32 / Guarantee 1: the payload names another Patient ──
let aOnPat2 = quiet "Rule 32 precondition" world (launchAs ucA.Login (Some pat2))
let wrongPatient =
let sid = (sidAt 1 aOnPat2).Value
let smuggled =
[ { Id = OrderContextId "oc-smuggled"; Patient = Some pat3; Content = "elsewhere"; Stamp = None } ]
let opened = (clientOf 1 aOnPat2).Value.Opened.Value
step "Rule 32 — the payload names a Patient the SessionRecord does not" aOnPat2
[ fromClient 1 (SessionRequest(sid, CreateTreatmentPlan(None, smuggled, None, opened, None))) ]
expect "Rule 32 the Patient comes from the SessionRecord, and a payload that disagrees is refused"
(saw (function CreateRefused _ -> true | _ -> false)
&& planCount pat2 wrongPatient = planCount pat2 aOnPat2
&& planCount pat3 wrongPatient = planCount pat3 aOnPat2)
// ── Rule 35: the payload arrives pre-stamped with another User ──
let preStamped =
let sid = (sidAt 1 aOnPat2).Value
let claimed =
[
{ Id = OrderContextId "oc-1"; Patient = Some pat2; Content = "oc-1/as-saved"; Stamp = Some ucB }
{ Id = OrderContextId "oc-new"; Patient = Some pat2; Content = "fresh"; Stamp = Some ucB }
]
let opened = (clientOf 1 aOnPat2).Value.Opened.Value
step "Rule 35 — the cart arrives stamped with B, in A's Session" aOnPat2
[ fromClient 1 (SessionRequest(sid, CreateTreatmentPlan(None, claimed, None, opened, None))) ]
let stamps = headOf pat2 preStamped |> Option.map _.Orders |> Option.defaultValue []
expect "Rule 35 the forged stamps are nowhere: the Server recomputed them against the base"
(stamps |> List.forall (fun o -> o.Stamp <> Some ucB))
expect "Rule 35 unchanged content keeps the base's stamp; the new one gets the Session's User"
(stamps |> List.exists (fun o -> o.Id = OrderContextId "oc-1" && o.Stamp = Some ucA)
&& stamps |> List.exists (fun o -> o.Id = OrderContextId "oc-new" && o.Stamp = Some ucA))
// ── Rule 36: two creates, both past their Rule 20 read ──
// The single-writer assumption is gone: more than one Server may run, and this is
// what makes that safe. Interleaving the cascades leg by leg is the only way to
// put two creates in flight at once — same messages, different order, which is
// exactly what Rule 36 exists to be safe against.
let raced =
racing "Rule 36 — two Sessions on one Patient, two creates in flight at once" both
[ act 1 Saves; act 2 Saves ]
expect "Rule 36 both got past their Rule 20 read: two AppendIf on the same head"
(countOf (function AppendIf _ -> true | _ -> false) = 2
&& (lastTrace
|> List.choose (function
| { Msg = AppendIf(_, expected, _) } -> Some expected
| _ -> None)
|> List.distinct
|> List.length) = 1)
expect "Rule 36 exactly one landed; the other was refused by the Database"
(countOf (function TreatmentPlanAppended _ -> true | _ -> false) = 1
&& countOf (function AppendRefused _ -> true | _ -> false) = 1
&& planCount pat2 raced = planCount pat2 both + 1)
expect "Rule 36 the loser gets the answer it already understands: take up their version"
(countOf (function CreateBlocked _ -> true | _ -> false) = 1)
// ═══════════════════════════════════════════════════════════════════════════════
// Consequences — derived from the edges, checked over every scenario
// ═══════════════════════════════════════════════════════════════════════════════
let consequences () =
printfn ""
printfn "############### Consequences ###############"
// Consequence 1. The LaunchScript learns nothing after the launch. This is not a
// discipline the branches keep — it is the shape of edge C4, which is `=>`. The
// only thing that ever reaches the LaunchScript is the Broker's answer to its own
// request, and the User's trigger.
let toLaunchScript =
allTrace |> List.filter (fun e -> e.To = MainEhrLaunchScript)
expect "C1 nothing reaches the LaunchScript but its own Broker answer and the User's trigger"
(toLaunchScript |> List.forall (fun e -> e.From = Broker || e.From = User))
expect "C1 in particular, neither the Server nor a Client can ever reach it"
(toLaunchScript
|> List.forall (fun e ->
e.From <> GenPresServer && (match e.From with GenPresClient _ -> false | _ -> true)))
// And the edge table is what says so, not the branches. Edge C4 is `=>`, which
// grants the one direction only, so there is no wire back at all.
expect "C1 the edge table refuses a reply to the LaunchScript outright"
(not (Edges.permits GenPresServer MainEhrLaunchScript)
&& not (Edges.permits (GenPresClient(BrowserId 1)) MainEhrLaunchScript))
// "Any pair without an edge cannot exchange data at all. Edges do not compose — no
// component relays on another's behalf unless stated."
expect "Constraints: a pair without an edge cannot exchange data at all"
(not (Edges.permits MainEhrWorkstation GenPresServer)
&& not (Edges.permits GenPresDatabase PatientDataPlatform)
&& not (Edges.permits (GenPresClient(BrowserId 1)) Broker)
&& not (Edges.permits (GenPresClient(BrowserId 1)) UserRegistry))
// Consequence 2. The Broker is the only party both the LaunchScript and the Server
// can reach, so it is the sole channel between the EHR side and GenPRES.
let reachableFrom a =
Edges.table
|> List.filter (fun (x, _, _) -> x = a)
|> List.map (fun (_, _, y) -> y)
|> Set.ofList
let shared = Set.intersect (reachableFrom MainEhrLaunchScript) (reachableFrom GenPresServer)
expect "C2 the Broker is the only party both the LaunchScript and the Server can reach"
(shared = Set.ofList [ Broker ])
// Consequence 3. Only the Broker knows whether a credential was redeemed, and it
// cannot tell the LaunchScript, which has exited.
expect "C3 the Broker's answers go only to the Server, the one party that asked"
(allTrace
|> List.forall (fun e ->
match e.Msg with
| LaunchResolved _
| LaunchRejected _ -> e.To = GenPresServer
| _ -> true))
// Consequence 6. The Server cannot reach a Client: edge C5 goes one way only, so
// every Server-to-Client envelope is a reply riding that request's connection.
expect "C6 there is no edge from the Server to a Client, so nothing can be pushed"
(Edges.table
|> List.exists (fun (x, _, y) ->
x = GenPresServer && (match y with GenPresClient _ -> true | _ -> false))
|> not)
// Rule 11. The SessionId is a bearer credential and never travels in a URL. The
// only message that is a URL is OpenUrl, and it carries a LaunchCredential.
expect "Rule 11 the only thing that ever travels as a URL is a LaunchCredential"
(allTrace
|> List.forall (fun e ->
match e.Msg with
| OpenUrl _ -> e.To |> function GenPresClient _ -> true | _ -> false
| _ -> true))
// Rule 22. The PIN never leaves GenPRES. GenPRES is the Client, the Server and the
// Database; everything else is outside it.
let outsideGenPres =
Set.ofList
[
Broker
UserRegistry
PatientDataPlatform
MailService
MainEhrWorkstation
MainEhrLaunchScript
]
let carriesPin (m: Msg) =
match m with
| ChoosePin _ | SupplyPin _ -> true
| Act(Signs _) -> true
| SessionRequest(_, CreateTreatmentPlan(Some _, _, _, _, _)) -> true
| WriteCredential(_, c) | CredentialWritten(_, c) | PinRemoved(_, c) -> c.Pin.IsSome
| CredentialRead(_, Some c) -> c.Pin.IsSome
| _ -> false
expect "Rule 22 no envelope carrying a PIN ever goes outside GenPRES"
(allTrace
|> List.filter (fun e -> carriesPin e.Msg)
|> List.forall (fun e -> not (outsideGenPres.Contains e.To)))
expect "Rule 22 and the mail that says a PIN changed never carries the PIN itself"
(allTrace
|> List.forall (fun e ->
match e.Msg with
| SendMail(_, what) -> not (what.Contains "9999" || what.Contains "1111")
| _ -> true))
// Rule 10, over every SessionRecord ever written to the Database in every
// scenario. These two are what the typed state buys: with a bare timestamp,
// "no notice is owed" and "one is owed and not yet given" were the same value,
// and neither could be asserted.
let everyRecordWritten =
allTrace
|> List.choose (fun e ->
match e.Msg with
| WriteSessionRecord r -> Some r
| _ -> None)
expect "Rule 10 a Session the User closed is never owed a notice"
(everyRecordWritten
|> List.forall (fun r ->
match r.State with
| Ended(ClosedByUser, _) -> r.Notice = NotOwed
| _ -> true))
expect "Rule 10 an open Session owes nothing either: the ending is what creates it"
(everyRecordWritten
|> List.forall (fun r -> r.State <> OpenOrGone || r.Notice = NotOwed))
expect "Rule 10 nothing is ever Told without an ending that owed it"
(everyRecordWritten
|> List.forall (fun r ->
match r.State, r.Notice with
| Ended(mark, _), Told _ -> SessionRecord.owesNotice mark
| _, Told _ -> false
| _ -> true))
// Rule 4. Only the Server may redeem a LaunchCredential at the Broker.
expect "Rule 4 every redemption at the Broker came from the Server"
(allTrace
|> List.forall (fun e ->
match e.Msg with
| ResolveLaunch _ -> e.From = GenPresServer && e.To = Broker
| _ -> true))
// Rule 5. The Role a Session carries is byte-for-byte the registry's answer, never
// synthesised: every launched Session is preceded by a UserResolved carrying the
// very same UserContext. Anonymous opens are excluded — they carry no User at all
// (Rule 13). The type-level half is that LaunchAssertion has no Role field to
// carry one (Concept 3), so the launch could not have supplied it.
let indexed = allTrace |> List.indexed
let resolvedBefore (i: int) (uc: UserContext) =
indexed
|> List.exists (fun (j, e) ->
j < i && (match e.Msg with UserResolved(_, uc', _) -> uc' = uc | _ -> false))
expect "Rule 5 every Session's Role came from the registry, and came first"
(indexed
|> List.forall (fun (i, e) ->
match e.Msg with
| SessionOpened(_, _, Some uc, _, _, _) -> resolvedBefore i uc
| _ -> true))
// ── Rule 31, structurally ──
// The Server carries nothing across requests. This is checked after every step of
// every scenario, not sampled: `noteFlight` trips a flag the moment a step ends
// with anything in the in-flight table.
expect "Rule 31 the in-flight table is empty at the end of every scenario step"
(not everCarriedARequest)
// And the type says the same thing: `ServerState` has counters, the two in-flight
// tables and `Up`. There is no field a Session could live in — no cart, no
// opened-with, no last-seen — so "the Server holds no Session state" is not a
// discipline the branches keep but something the state cannot express.
expect "Rule 31 the whole of the work travels with every request (Open Question 3)"
(allTrace
|> List.exists (fun e ->
match e.Msg with
| SessionRequest(_, CreateTreatmentPlan(_, orders, _, _, _)) -> not orders.IsEmpty
| _ -> false))
// ── Rule 32 ──
// The payload has no User in it to be believed — `SessionCmd` carries orders, data
// and tokens, and a token names a SessionId, not an identity — so the only place a
// TreatmentPlan's `By` can have come from is a SessionRecord the Server had just read.
// That is what this checks: every conditional append is preceded by the read that
// supplied its User.
let readARecordFor (i: int) (uc: UserContext) =
indexed
|> List.exists (fun (j, e) ->
j < i && (match e.Msg with SessionRecordRead(_, Some r) -> r.User = Some uc | _ -> false))
expect "Rule 32 every TreatmentPlan's User came off a SessionRecord, never off the payload"
(indexed
|> List.forall (fun (i, e) ->
match e.Msg with
| AppendIf(_, _, d) -> readARecordFor i d.By
| _ -> true))
// ── Rules 33 and 34 ──
expect "Rule 33 every token the Server ever issued verifies, and every stale one was refused honestly"
(allTrace
|> List.forall (fun e ->
match e.Msg with
| SessionOpened(_, _, _, _, _, t) -> Token.verifyOpened t
| TreatmentPlanCreated(_, _, t) -> Token.verifyOpened t
| TreatmentPlanOpened(_, _, t) -> Token.verifyOpened t
| _ -> true))
expect "Rule 34 every notice the Server ever sent carried a token that verifies"
(allTrace
|> List.forall (fun e ->
match e.Msg with
| UnsignedWorkNotice(_, t) -> Token.verifyNotice t
| _ -> true))
// ── Rule 36 ──
// There is no message that appends a TreatmentPlan unconditionally: `AppendIf` is the
// only way in, and every one of them states the head its Rule 20 check saw.
let appendIfs = allTrace |> List.filter (fun e -> match e.Msg with AppendIf _ -> true | _ -> false)
let appended = allTrace |> List.filter (fun e -> match e.Msg with TreatmentPlanAppended _ -> true | _ -> false)
expect "Rule 36 every TreatmentPlan that landed came through a conditional append"
(appended.Length <= appendIfs.Length && appended.Length > 0)
expect "Rule 36 and every conditional append went to the Database, the one arbiter"
(appendIfs |> List.forall (fun e -> e.To = GenPresDatabase))
// ── Rule 9 ──
// Four endings, and a Server restart is not one of them. The type says so — there
// is no `EndMark` for it — and UC-9 ext 1a shows what happens instead.
let marksSeen =
everyRecordWritten
|> List.choose (fun r -> match r.State with Ended(m, _) -> Some m | OpenOrGone -> None)
|> List.distinct
expect "Rule 9 all four endings occur across the run, and nothing else ever ends a Session"
(marksSeen |> List.sort = List.sort [ ClosedByUser; Idle; Superseded; WrongPinLimit ])
// ═══════════════════════════════════════════════════════════════════════════════
// Guarantees — what the Rules add up to
// ═══════════════════════════════════════════════════════════════════════════════
let guarantees () =
printfn ""
printfn "############### Guarantees ###############"
// A record built up over several creates, by two Users, with a block and a
// takeover in the middle of it.
let g0 = quiet "G" world (launchAs ucA.Login (Some pat2))
let g1 = quiet "G" g0 [ act 1 (Prescribes(OrderContextId "g-1")); act 1 Saves ]
let g2 = quiet "G" g1 [ act 1 (Prescribes(OrderContextId "g-2")); act 1 (Signs pinA) ]
let g3 = quiet "G" g2 (launchAs ucB.Login (Some pat2))
let g4 = quiet "G" g3 [ act 2 (Prescribes(OrderContextId "g-3")); act 2 (Signs pinB) ]
let record = recordFor pat2 g4
// ── Guarantee 1: one constant ──
expect "G1 the PatientId is the one thing no TreatmentPlan may change"
(record.Plans |> List.forall (fun s -> s.Patient = pat2))
expect "G1 and only a launch supplies one, so no hand ever set it (Rules 12, 13, 32)"
(g4.Database.Records
|> Map.forall (fun p r -> r.Plans |> List.forall (fun s -> s.Patient = p)))
// ── Guarantee 2: one version ──
let signedOnes = record.Plans |> List.filter _.Signed
expect "G2 exactly one TreatmentPlan is the visible version: the most recent Signed one (Rules 16, 17)"
((PatientRecord.latestSigned record |> Option.map _.Id) = (signedOnes |> List.tryHead |> Option.map _.Id))
expect "G2 nothing else can be opened by another User (Rule 17)"
(record.Plans
|> List.filter (fun s -> Some s.Id <> (PatientRecord.latestSigned record |> Option.map _.Id))
|> List.forall (fun s ->
// openable by its creator if Unsigned (Rule 18), by nobody else
(record |> PatientRecord.mayOpen ucC.UserId s.Id).IsNone))
expect "G2 and each User has exactly one starting point (Rule 19)"
([ ucA; ucB; ucC ]
|> List.forall (fun uc -> (record |> PatientRecord.startsFrom uc.UserId) |> Option.isSome))
// ── Guarantee 3: carts and one checkout ──
// The cart is private by construction now: it lives in the User's own Client and
// the Server keeps none of it (Rule 31). The checkout is single by construction
// too: the Database arbitrates the append (Rule 36).
expect "G3 signing is the only checkout: every Signed TreatmentPlan came from a create with a PIN"
(signedOnes |> List.forall (fun s -> s.By.Role = Prescriber))
expect "G3 a Reader never appears as the creator of anything (Roles)"
(g4.Database.Records
|> Map.forall (fun _ r -> r.Plans |> List.forall (fun s -> s.By.Role <> Reader)))
expect "G3 every TreatmentPlan after the first stands on a base (Concept 13)"
(record.Plans
|> List.filter (fun s -> s.No <> TreatmentPlanNo 1)
|> List.forall (fun s -> s.Base.IsSome))
expect "G3 the two carts never met in the Server: it held neither (Rule 31)"
(g4.GenPres.InFlight.IsEmpty
&& (g4.Clients |> Map.exists (fun _ c -> not c.Working.IsEmpty)))
// ── Guarantee 4: audit ──
expect "G4 a Signed TreatmentPlan carries the User who signed it (Concepts 13, 14; Rule 14)"
(signedOnes |> List.forall (fun s -> s.By.UserId = ucA.UserId || s.By.UserId = ucB.UserId))
expect "G4 every OrderContext in every TreatmentPlan carries the User whose Session last changed it"
(g4.Database.Records
|> Map.forall (fun _ r ->
r.Plans |> List.forall (fun s -> s.Orders |> List.forall (_.Stamp.IsSome))))
expect "G4 and the stamps are not all the signer's: B's signature kept A's work attributed to A"
(record.Plans
|> List.tryHead
|> Option.map (fun s ->
s.By = ucB
&& s.Orders |> List.exists (fun o -> o.Stamp = Some ucA)
&& s.Orders |> List.exists (fun o -> o.Stamp = Some ucB))
|> Option.defaultValue false)
// Append-only: each record is the previous one with something on the front, and
// nothing that was already there is ever touched.
let history = [ recordFor pat2 g0; recordFor pat2 g1; recordFor pat2 g2; recordFor pat2 g4 ]
expect "G4 the record is append-only: every earlier version is a suffix of the later one (Concept 12)"
(history
|> List.pairwise
|> List.forall (fun (earlier, later) ->
later.Plans.Length >= earlier.Plans.Length
&& later.Plans |> List.skip (later.Plans.Length - earlier.Plans.Length)
= earlier.Plans))
// Stated as the claim rather than as a count: every Signed TreatmentPlan that existed
// at any point in the history is still in the record at the end of it.
let everSigned =
history |> List.collect (fun r -> r.Plans |> List.filter _.Signed) |> List.distinct
expect "G4 nothing attested is ever lost: every Signed TreatmentPlan ever made is still there"
(everSigned <> []
&& everSigned |> List.forall (fun s -> record.Plans |> List.contains s))
// What is not protected: Unsigned work. Superseded, it can never be signed.
expect "G4 what is not protected is Unsigned work — superseded, it can never be signed (Rules 19, 20)"
(record |> PatientRecord.blocking (Some(TreatmentPlanId "plan-0010"))).IsSome
// ═══════════════════════════════════════════════════════════════════════════════
// THE RUN
// ═══════════════════════════════════════════════════════════════════════════════
let runAll () =
uc1 () |> ignore
uc2 ()
uc3 () |> ignore
uc4 () |> ignore
uc5 () |> ignore
uc6 () |> ignore
uc7 () |> ignore
uc8 () |> ignore
uc9 () |> ignore
uc10 () |> ignore
uc11 () |> ignore
uc12 () |> ignore
uc13 () |> ignore
tokensAndArbitration ()
consequences ()
guarantees ()
printfn ""
printfn "######################################################################"
printfn $" {checks - failures}/{checks} checks passed"
if failures > 0 then printfn $" {failures} FAILED"
runAll ()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment