docs(ebs-spec): spec ListVolumes and ListSnapshots

spec/EBSProvider/Capabilities.tla

@@ -0,0 +1,27 @@
+------------------------------------------------- MODULE Capabilities -------------------------------------------------
+(*********************************************************************************************************************)
+(* The optional behaviour that an implementation advertises.                                                         *)
+(*********************************************************************************************************************)
+EXTENDS EBSProvider
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Interface methods
+
+GetCapabilitiesRequests == {<<>>}
+
+GetCapabilities(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* The implementation reports which optional behaviour it supports.                                                *)
+  (*******************************************************************************************************************)
+     \* The provider failed to answer.
+  \/ /\ val = None
+     /\ err \in ProviderErrors
+     /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \* Every answer is the same, so an earlier one may be cached.
+  \/ /\ val = Capabilities
+     /\ err = None
+     /\ UNCHANGED vars
+
+=======================================================================================================================

spec/EBSProvider/EBSProvider.tla

@@ -0,0 +1,164 @@
+------------------------------------------------- MODULE EBSProvider --------------------------------------------------
+(*********************************************************************************************************************)
+(* The state that an implementation exposes, and the types and constants that every other module shares.             *)
+(*********************************************************************************************************************)
+EXTENDS
+  Naturals,
+  Sequences,
+  FiniteSets,
+  Functions,
+  TLC
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Constants
+
+CONSTANTS
+  MaxBytes,
+  VolumeIDs, VolumeHandles,
+  NodeIDs, NBDURIs, DevicePaths,
+  SnapshotIDs, SnapshotHandles,
+  AvailabilityZones, Timestamps,
+  Parameters, ProviderData,
+  ListTokens, MaxListResults,
+  \* The optional behaviour that the implementation advertises, which never changes.
+  Capabilities,
+  \* Whether the provider may fail to answer at any point in a behaviour.
+  ProviderMayFail,
+  \* Stands in for an optional field that a request or response omitted.
+  None
+
+ASSUME MaxBytes \in Nat \ {0}
+ASSUME VolumeIDs /= {} /\ VolumeHandles /= {}
+ASSUME NodeIDs /= {} => NBDURIs /= {} \/ DevicePaths /= {}
+ASSUME SnapshotIDs /= {} => SnapshotHandles /= {} /\ Timestamps /= {}
+ASSUME ListTokens /= {}
+ASSUME MaxListResults \in Nat \ {0}
+ASSUME ListTokens /= {}
+ASSUME None \notin UNION {VolumeIDs, VolumeHandles, NodeIDs, SnapshotIDs, SnapshotHandles,
+                          AvailabilityZones, Timestamps, Parameters, ProviderData, ListTokens}
+ASSUME Capabilities \in [online_expansion          : BOOLEAN,
+                         sparse_extent_reporting   : BOOLEAN,
+                         crash_consistent_snapshot : BOOLEAN,
+                         volume_seeding            : BOOLEAN,
+                         read_only_publish         : BOOLEAN,
+                         volume_enumeration        : BOOLEAN,
+                         snapshot_enumeration      : BOOLEAN,
+                         owner_routing             : BOOLEAN,
+                         exclusion                 : [scope             : {"none", "node", "cluster"},
+                                                      claim_ttl_seconds : Nat,
+                                                      fences_lost_claim : BOOLEAN]]
+ASSUME ProviderMayFail \in BOOLEAN
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Variables
+
+VARIABLES
+  \* Every volume that the implementation exposes, keyed by volume ID.
+  volumes,
+  \* Every publication that the implementation exposes, keyed by the volume and the node it is published to.
+  publications,
+  \* Every snapshot that the implementation exposes, keyed by snapshot ID.
+  snapshots
+
+vars == <<volumes, publications, snapshots>>
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Miscellaneous
+
+IsPartialFn(f, D, R) == DOMAIN f \subseteq D /\ \A x \in DOMAIN f : f[x] \in R
+
+Optional(S) == S \union {None}
+
+InsertKey(f, x, y) == f @@ (x :> y)
+
+RemoveKey(f, x) == RestrictDomain(f, LAMBDA x_2 : x_2 /= x)
+
+KeyExists(f, x) == x \in DOMAIN f
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Types
+
+Bytes == 0..MaxBytes
+
+\* The errors that an implementation may return when its provider fails to answer.
+ProviderErrors == IF ProviderMayFail
+                  THEN {"internal", "unavailable"}
+                  \* Otherwise an implementation could conform by refusing to answer.
+                  ELSE {}
+
+CapacityRanges == [required_bytes : Bytes, limit_bytes : Bytes]
+
+VolumeStates == {"available", "in-use"}
+
+Volumes == [capacity_bytes     : 1..MaxBytes,
+            state              : VolumeStates,
+            handle             : VolumeHandles,
+            availability_zone  : Optional(AvailabilityZones),
+
+            \* Never returned, but kept to tell a retry from a conflicting request.
+            source_snapshot_id : Optional(SnapshotIDs),
+            parameters         : Optional(Parameters),
+            provider_data      : Optional(ProviderData)]
+
+\* How a published volume is reached on its node, either over NBD or as a host block device.
+Exports == [kind    : {"nbd"},
+            nbd_uri : NBDURIs]
+           \union
+           [kind        : {"block"},
+            device_path : DevicePaths,
+            size_bytes  : 1..MaxBytes]
+
+\* A volume published to a node, and whether it was published read-only.
+Publications == [export    : Exports,
+                 read_only : BOOLEAN]
+
+SnapshotStates == {"pending", "completed", "error"}
+
+Snapshots == [size_bytes       : 1..MaxBytes,
+              created_at       : Timestamps,
+              state            : SnapshotStates,
+              handle           : SnapshotHandles,
+              source_volume_id : VolumeIDs]
+
+-----------------------------------------------------------------------------------------------------------------------
+\* State helpers
+
+\* The part of a volume that the implementation returns.
+VolumeView(volID) ==
+  ("id" :> volID) @@ Restrict(volumes[volID], {"capacity_bytes",
+                                               "state",
+                                               "handle",
+                                               "availability_zone",
+                                               "provider_data"})
+
+\* The nodes that a volume is published to.
+PublishedNodes(volID) == {n \in NodeIDs : KeyExists(publications, <<volID, n>>)}
+
+\* The part of a publication that the implementation returns.
+PublicationView(volID, nodeID) == [volume_id |-> volID,
+                                   node_id   |-> nodeID,
+                                   export    |-> publications[volID, nodeID].export]
+
+\* The part of a snapshot that the implementation returns.
+SnapshotView(snapID) == ("id" :> snapID) @@ snapshots[snapID]
+
+\* The number of refs that a page may hold, with an omitted or oversized request clamped to the maximum.
+PageSize(m) == IF m <= 0 \/ m > MaxListResults THEN MaxListResults ELSE m
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Invariants
+
+TypeOK ==
+  /\ IsPartialFn(volumes, VolumeIDs, Volumes)
+  /\ IsPartialFn(publications, VolumeIDs \X NodeIDs, Publications)
+  /\ IsPartialFn(snapshots, SnapshotIDs, Snapshots)
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Initial state
+
+Init ==
+  /\ volumes      = <<>>
+  /\ publications = <<>>
+  /\ snapshots    = <<>>
+
+=======================================================================================================================

spec/EBSProvider/README.md

@@ -0,0 +1,140 @@
+# EBSProvider specification
+
+The contract that every implementation of the `EBSProvider` interface must meet.
+
+## Terminology
+
+- **Provider:** the service that backs an implementation's operations, such as Viperblock.
+  The memory implementation has none.
+- **Implementation:** a Go implementation of the `EBSProvider` interface, which adapts between the shapes of the contract and the shapes that its provider expects.
+- **Contract:** the behaviour that this specification requires of every implementation, as observed through the interface.
+
+## Open questions
+
+### EBSProvider
+
+- What may a failed call change?
+  A failed call leaves the state unchanged, but a timeout can arrive after the provider acted, and a crash can leave work half done.
+- Is the schema version part of the contract?
+  Every method refuses an unsupported version with `unsupported_version`, and the conformance suite tests it, but the specification does not model versions.
+- Are `internal` and `unavailable` the only errors that a failed provider may cause?
+- Must a present but malformed ID be refused with `invalid_argument`?
+  IDs are opaque here, so only an omitted one is refused.
+
+### Capabilities
+
+#### GetCapabilities
+
+- Is it a lasting promise that capabilities never change, even when an implementation or its provider is upgraded or reconfigured after an earlier answer was cached?
+
+### Volumes
+
+- Who decides whether a volume is `in-use`?
+  An implementation may track attachments itself, or derive the state from whether a publication claim is held.
+
+#### CreateVolume
+
+- May the capacity be anywhere in the requested range, as CSI allows?
+  An implementation that rounds up would then fail the comparison that tells a retry from a conflicting request.
+- May seed data be combined with a source snapshot?
+  The Viperblock implementation refuses, the memory implementation accepts.
+- Must the source snapshot be completed?
+  AWS refuses one that is not.
+- Must an implementation store the availability zone, parameters and source snapshot, so that it can detect a conflicting retry?
+  The Viperblock implementation does not.
+- Should a retry be compared against the original request rather than the current volume?
+  A retry after ExpandVolume conflicts on capacity.
+- Should a retry with a different source snapshot volume ID conflict?
+  It is not compared.
+- Is byte equality the meaning of equal parameters, or may an implementation compare them semantically?
+- Should `MaxSeedBytes` be modelled?
+  Seed data larger than it is refused with `invalid_argument`.
+
+#### GetVolume
+
+- Must an implementation compare the handle?
+  The Viperblock implementation ignores it.
+- Is `not_found` the right error for a volume that was deleted and recreated under the same ID?
+
+#### ListVolumes
+
+- Must following next tokens list every volume that exists throughout the walk exactly once?
+  The conformance suite tests it, but the specification describes each call alone, so it does not say how one page relates to the next.
+- What should a starting token that the implementation never issued do?
+  Every implementation treats any token as a position to resume after, while CSI refuses an invalid one with `ABORTED`.
+- May a page hold fewer refs than requested yet carry a next token?
+  AWS and CSI allow it, but here a next token comes only with a full page, so that a walk cannot stall on empty pages.
+
+#### ExpandVolume
+
+- Should a request below the current capacity succeed without change, as CSI recommends, rather than be refused with `invalid_argument`?
+  It is refused here, as AWS refuses `ModifyVolume` to a smaller size and the conformance suite tests, while CSI says the plugin should reply OK when the volume is already at least the requested size.
+- Must a block export's size follow an online expansion?
+  A published volume keeps its export's `size_bytes`, so after it grows the export reports the old size.
+
+#### PublishVolume
+
+- Should `volume_in_use` depend on the exclusion scope?
+  An implementation whose scope is `none` lets two writers in, and one whose scope is `node` cannot see another node, yet both are refused here.
+- Must a republish to the same node with a different `read_only` be refused?
+  The Viperblock implementation refuses it with `volume_in_use`, while the memory implementation ignores the flag.
+- May two volumes on one node share an NBD URI or a device path?
+- Must a block export's size equal the volume's capacity?
+
+#### UnpublishVolume
+
+- Must an implementation compare the handle?
+  Both the Viperblock and memory implementations ignore it.
+- Is a provider that fails to seal the volume a failed provider?
+  The Viperblock implementation answers `internal` and leaves the volume published, which the specification allows only when the provider may fail.
+- Should a claim that lapses through its TTL be modelled, as a step that happens without a call?
+- Should a volume that does not exist be refused with `not_found`?
+  It succeeds here, as CSI requires and the conformance suite tests, while AWS refuses `DetachVolume` on a missing volume with `InvalidVolume.NotFound`.
+
+#### DeleteVolume
+
+- Must an implementation compare the handle before refusing a published volume?
+  The memory implementation does, and succeeds without deleting it, while the Viperblock implementation ignores the handle and refuses with `volume_in_use`.
+- Should a volume that does not exist be refused with `not_found`?
+  It succeeds here, as CSI requires and the conformance suite tests, while AWS refuses `DeleteVolume` on a missing volume with `InvalidVolume.NotFound`.
+
+### Snapshots
+
+- Should a pending snapshot's move to `completed` or `error` be modelled, as a step that happens without a call?
+  Without it a pending snapshot never completes, and no snapshot is ever in `error`.
+
+#### CreateSnapshot
+
+- May success return a `pending` snapshot?
+  AWS starts a snapshot as `pending`, while the memory implementation returns `completed` and the NATS implementation waits for completion and refuses anything else.
+- Must a retry compare the volume handle?
+  It is ignored, as in the memory implementation, so a volume deleted and recreated under the same ID returns the old snapshot.
+- Should a copy's ID count as a retry?
+  A copy keeps its source's volume ID, so creating a snapshot of that volume under the copy's ID returns the copy.
+- Should `crash_consistent_snapshot` be modelled?
+  The specification does not model volume data, so it cannot say what a snapshot of a published volume holds.
+
+#### CopySnapshot
+
+- Should a retried copy return the existing copy, as a retried CreateVolume does, rather than `already_exists`?
+- May a source that is not completed be copied?
+  AWS refuses until it is.
+- What state does a copy start in?
+  The memory implementation always returns `completed`, while AWS starts a copy as `pending`.
+
+#### ListSnapshots
+
+- The questions for ListVolumes apply here too.
+- Must a ref carry the source volume ID?
+  The Viperblock implementation leaves it empty, since reading it costs a fetch per snapshot, yet reconciliation needs it to act on a snapshot whose metadata is lost.
+
+#### DeleteSnapshot
+
+- Is the handle check part of the contract?
+  The Viperblock implementation ignores the handle and deletes anyway.
+- May a pending snapshot be deleted?
+  AWS allows it.
+- What does success promise?
+  The Go docs say the snapshot is gone, but a snapshot whose handle did not match is left in place.
+- Should a snapshot that does not exist be refused with `not_found`?
+  It succeeds here, as CSI requires and the conformance suite tests, while AWS refuses `DeleteSnapshot` on a missing snapshot with `InvalidSnapshot.NotFound`.

spec/EBSProvider/Snapshots.tla

@@ -0,0 +1,159 @@
+-------------------------------------------------- MODULE Snapshots ---------------------------------------------------
+(*********************************************************************************************************************)
+(* The lifecycle of a snapshot, from its creation to its deletion.                                                   *)
+(*********************************************************************************************************************)
+EXTENDS EBSProvider
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Interface methods
+
+CreateSnapshotRequests == [snapshot_id   : Optional(SnapshotIDs),
+                           volume_id     : Optional(VolumeIDs),
+                           volume_handle : Optional(VolumeHandles)]
+
+CreateSnapshot(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* A volume's data is frozen as a snapshot, from which new volumes can be restored. A retry of a call that         *)
+  (* already succeeded returns the same snapshot.                                                                    *)
+  (*******************************************************************************************************************)
+  LET snapID == req.snapshot_id
+      volID  == req.volume_id
+
+      Errors ==
+        LET checks == [invalid_argument |-> None \in {snapID, volID},
+                       already_exists   |-> /\ KeyExists(snapshots, snapID)
+                                            /\ snapshots[snapID].source_volume_id /= volID,
+                       \* Only checked for a new snapshot, so a retry outlives the volume.
+                       not_found        |-> /\ ~KeyExists(snapshots, snapID)
+                                            /\ \/ ~KeyExists(volumes, volID)
+                                               \/ req.volume_handle \notin {None, volumes[volID].handle}]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+           \* A retry returns the existing snapshot.
+        /\ \/ /\ KeyExists(snapshots, snapID)
+              /\ UNCHANGED snapshots
+
+           \/ /\ ~KeyExists(snapshots, snapID)
+              \* The handle, creation time and state are the implementation's choice.
+              /\ \E h \in SnapshotHandles \ {snapshots[x].handle : x \in DOMAIN snapshots},
+                    t \in Timestamps,
+                    s \in {"pending", "completed"} :
+                   snapshots' = InsertKey(snapshots, snapID, [size_bytes       |-> volumes[volID].capacity_bytes,
+                                                              created_at       |-> t,
+                                                              state            |-> s,
+                                                              handle           |-> h,
+                                                              source_volume_id |-> volID])
+        /\ val = SnapshotView(snapID)'
+        /\ err = None
+        /\ UNCHANGED <<volumes, publications>>
+
+
+CopySnapshotRequests == [source_snapshot_id      : Optional(SnapshotIDs),
+                         destination_snapshot_id : Optional(SnapshotIDs),
+                         volume_id               : Optional(VolumeIDs)]
+
+CopySnapshot(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* A snapshot is copied under a new ID, sharing its frozen data, and the copy can be deleted independently         *)
+  (* of it.                                                                                                          *)
+  (*******************************************************************************************************************)
+  LET srcSnapID == req.source_snapshot_id
+      dstSnapID == req.destination_snapshot_id
+      volID     == req.volume_id
+
+      Errors ==
+        LET checks == [invalid_argument |-> \/ None \in {srcSnapID, dstSnapID, volID}
+                                            \/ srcSnapID = dstSnapID
+                                            \* Only compared, not looked up, since a snapshot outlives its volume.
+                                            \/ /\ KeyExists(snapshots, srcSnapID)
+                                               /\ snapshots[srcSnapID].source_volume_id /= volID,
+                       already_exists   |-> KeyExists(snapshots, dstSnapID),
+                       not_found        |-> srcSnapID \notin Optional(DOMAIN snapshots)]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        \* The handle and creation time are the implementation's choice.
+        /\ \E h \in SnapshotHandles \ {snapshots[x].handle : x \in DOMAIN snapshots},
+              t \in Timestamps :
+             snapshots' = InsertKey(snapshots, dstSnapID, [created_at |-> t,
+                                                           handle     |-> h]
+                                                           @@ snapshots[srcSnapID])
+        /\ val = SnapshotView(dstSnapID)'
+        /\ err = None
+        /\ UNCHANGED <<volumes, publications>>
+
+
+ListSnapshotsRequests == [max_results    : -1..(MaxListResults + 1),
+                          starting_token : Optional(ListTokens)]
+
+ListSnapshots(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* Some of the snapshots are listed, a page at a time, and nothing changes. A call with no starting token that     *)
+  (* returns no next token lists every snapshot.                                                                     *)
+  (*******************************************************************************************************************)
+  LET Errors ==
+    LET checks == [unsupported_capability |-> ~Capabilities.snapshot_enumeration]
+    IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        /\ LET refs == {[id               |-> id,
+                         source_volume_id |-> snapshots[id].source_volume_id,
+                         handle           |-> snapshots[id].handle] : id \in DOMAIN snapshots}
+           \* The page and the next token are the implementation's choice.
+           IN \E page \in SUBSET refs, next \in Optional(ListTokens) :
+                /\ Cardinality(page) <= PageSize(req.max_results)
+                /\ next /= None => Cardinality(page) = PageSize(req.max_results)
+                /\ req.starting_token = None /\ next = None => page = refs
+                /\ val = [snapshots |-> page, next_token |-> next]
+        /\ err = None
+        /\ UNCHANGED vars
+
+
+DeleteSnapshotRequests == [snapshot_id : Optional(SnapshotIDs),
+                           handle      : Optional(SnapshotHandles)]
+
+DeleteSnapshot(req, err) ==
+  (*******************************************************************************************************************)
+  (* A snapshot is deleted, so that no new volume can be restored from it. Volumes already restored from it,         *)
+  (* and copies of it, are unaffected.                                                                               *)
+  (*******************************************************************************************************************)
+  LET snapID == req.snapshot_id
+
+      Errors ==
+        LET checks == [invalid_argument |-> snapID = None]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        /\ snapshots' = IF /\ KeyExists(snapshots, snapID)
+                           /\ req.handle \notin {None, snapshots[snapID].handle}
+                        THEN snapshots
+                        \* Record removal is idempotent so that retries succeed.
+                        ELSE RemoveKey(snapshots, snapID)
+        /\ err = None
+        /\ UNCHANGED <<volumes, publications>>
+
+=======================================================================================================================

spec/EBSProvider/Volumes.tla

@@ -0,0 +1,286 @@
+--------------------------------------------------- MODULE Volumes ----------------------------------------------------
+(*********************************************************************************************************************)
+(* The lifecycle of a volume, from its creation to its deletion.                                                     *)
+(*********************************************************************************************************************)
+EXTENDS EBSProvider
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Control plane operations
+
+CreateVolumeRequests == [volume_id                 : Optional(VolumeIDs),
+                         capacity_range            : CapacityRanges,
+                         availability_zone         : Optional(AvailabilityZones),
+                         source_snapshot_id        : Optional(SnapshotIDs),
+                         source_snapshot_volume_id : Optional(VolumeIDs),
+                         parameters                : Optional(Parameters),
+                         seed_data                 : Bytes]
+
+CreateVolume(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* A volume of the requested capacity is created, either blank or holding a snapshot's data, optionally            *)
+  (* with seed data written at its start. A retry of a call that already succeeded returns the same volume.          *)
+  (*******************************************************************************************************************)
+  LET volID     == req.volume_id
+      snapID    == req.source_snapshot_id
+      snapVolID == req.source_snapshot_volume_id
+      capacity  == req.capacity_range
+
+      \* Any warranted error may be returned, since the order of checks is not part of the contract.
+      Errors ==
+        LET checks == [invalid_argument       |-> \/ volID = None
+                                                  \/ capacity.required_bytes <= 0
+                                                  \/ /\ capacity.limit_bytes > 0
+                                                     /\ capacity.required_bytes > capacity.limit_bytes
+                                                  \/ req.seed_data > capacity.required_bytes
+                                                  \/ snapID /= None /\ snapVolID = None
+                                                  \* Only checked for a new volume, so a retry outlives the snapshot.
+                                                  \/ /\ ~KeyExists(volumes, volID)
+                                                     /\ KeyExists(snapshots, snapID)
+                                                     /\ \/ capacity.required_bytes < snapshots[snapID].size_bytes
+                                                        \/ snapshots[snapID].source_volume_id /= snapVolID,
+                       \* Seed data is not compared, since it only applies on creation.
+                       already_exists         |-> /\ KeyExists(volumes, volID)
+                                                  /\ \/ volumes[volID].capacity_bytes     /= capacity.required_bytes
+                                                     \/ volumes[volID].availability_zone  /= req.availability_zone
+                                                     \/ volumes[volID].source_snapshot_id /= snapID
+                                                     \/ volumes[volID].parameters         /= req.parameters,
+                       not_found              |-> /\ ~KeyExists(volumes, volID)
+                                                  /\ snapID \notin Optional(DOMAIN snapshots),
+                       unsupported_capability |-> /\ req.seed_data > 0
+                                                  /\ ~Capabilities.volume_seeding]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+           \* A retry returns the existing volume.
+        /\ \/ /\ KeyExists(volumes, volID)
+              /\ UNCHANGED volumes
+
+           \/ /\ ~KeyExists(volumes, volID)
+              \* The handle and provider data are the implementation's choice.
+              /\ \E h \in VolumeHandles \ {volumes[x].handle : x \in DOMAIN volumes},
+                    pd \in Optional(ProviderData) :
+                   volumes' = InsertKey(volumes, volID, [capacity_bytes     |-> capacity.required_bytes,
+                                                         state              |-> "available",
+                                                         handle             |-> h,
+                                                         availability_zone  |-> req.availability_zone,
+                                                         source_snapshot_id |-> snapID,
+                                                         parameters         |-> req.parameters,
+                                                         provider_data      |-> pd])
+        /\ val = VolumeView(volID)'
+        /\ err = None
+        /\ UNCHANGED <<publications, snapshots>>
+
+
+GetVolumeRequests == [volume_id : Optional(VolumeIDs),
+                      handle    : Optional(VolumeHandles)]
+
+GetVolume(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* A volume's current capacity, state and handle are read, and nothing changes.                                    *)
+  (*******************************************************************************************************************)
+  LET volID == req.volume_id
+
+      Errors ==
+        LET checks == [invalid_argument |-> volID = None,
+                       not_found        |-> \/ ~KeyExists(volumes, volID)
+                                            \/ req.handle \notin {None, volumes[volID].handle}]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        /\ val = VolumeView(volID)
+        /\ err = None
+        /\ UNCHANGED vars
+
+
+ListVolumesRequests == [max_results    : -1..(MaxListResults + 1),
+                        starting_token : Optional(ListTokens)]
+
+ListVolumes(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* Some of the volumes are listed, a page at a time, and nothing changes. A call with no starting token that       *)
+  (* returns no next token lists every volume.                                                                       *)
+  (*******************************************************************************************************************)
+  LET Errors ==
+    LET checks == [unsupported_capability |-> ~Capabilities.volume_enumeration]
+    IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        /\ LET refs == {[id |-> id, handle |-> volumes[id].handle] : id \in DOMAIN volumes}
+           \* The page and the next token are the implementation's choice.
+           IN \E page \in SUBSET refs, next \in Optional(ListTokens) :
+                /\ Cardinality(page) <= PageSize(req.max_results)
+                /\ next /= None => Cardinality(page) = PageSize(req.max_results)
+                /\ req.starting_token = None /\ next = None => page = refs
+                /\ val = [volumes |-> page, next_token |-> next]
+        /\ err = None
+        /\ UNCHANGED vars
+
+
+ExpandVolumeRequests == [volume_id      : Optional(VolumeIDs),
+                         handle         : Optional(VolumeHandles),
+                         capacity_range : CapacityRanges]
+
+ExpandVolume(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* A volume grows to the requested capacity, keeping its data. A published volume grows only if the                *)
+  (* implementation supports online expansion, and a request for the current capacity succeeds without change.       *)
+  (*******************************************************************************************************************)
+  LET volID    == req.volume_id
+      capacity == req.capacity_range
+
+      Errors ==
+        LET checks == [invalid_argument |-> \/ volID = None
+                                            \/ capacity.required_bytes = 0
+                                            \/ /\ capacity.limit_bytes > 0
+                                               /\ capacity.required_bytes > capacity.limit_bytes
+                                            \/ /\ KeyExists(volumes, volID)
+                                               /\ capacity.required_bytes < volumes[volID].capacity_bytes,
+                       not_found        |-> \/ ~KeyExists(volumes, volID)
+                                            \/ req.handle \notin {None, volumes[volID].handle},
+                       volume_in_use    |-> /\ PublishedNodes(volID) /= {}
+                                            /\ ~Capabilities.online_expansion
+                                            /\ capacity.required_bytes > volumes[volID].capacity_bytes]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        /\ volumes' = [volumes EXCEPT ![volID].capacity_bytes = capacity.required_bytes]
+        /\ val = VolumeView(volID)'
+        /\ err = None
+        /\ UNCHANGED <<publications, snapshots>>
+
+
+PublishVolumeRequests == [volume_id : Optional(VolumeIDs),
+                          handle    : Optional(VolumeHandles),
+                          node_id   : Optional(NodeIDs),
+                          read_only : BOOLEAN]
+
+PublishVolume(req, val, err) ==
+  (*******************************************************************************************************************)
+  (* A volume's data becomes reachable on a node, through an export that a VM there can attach, either an NBD        *)
+  (* URI or a host block device. Reads and writes through the export reach the volume, and a read-only export        *)
+  (* refuses writes. Only one node at a time may reach a volume.                                                     *)
+  (*******************************************************************************************************************)
+  LET volID  == req.volume_id
+      nodeID == req.node_id
+
+      Errors ==
+        LET checks == [invalid_argument       |-> None \in {volID, nodeID},
+                       not_found              |-> \/ ~KeyExists(volumes, volID)
+                                                  \/ req.handle \notin {None, volumes[volID].handle},
+                       unsupported_capability |-> /\ req.read_only
+                                                  /\ ~Capabilities.read_only_publish,
+                       volume_in_use          |-> PublishedNodes(volID) \ {nodeID} /= {}]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ val = None
+        /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+           \* A retry returns the existing publication.
+        /\ \/ /\ KeyExists(publications, <<volID, nodeID>>)
+              /\ UNCHANGED publications
+
+           \/ /\ ~KeyExists(publications, <<volID, nodeID>>)
+              \* The type of export is the implementation's choice.
+              /\ \E x \in Exports :
+                   publications' = InsertKey(publications, <<volID, nodeID>>, [export    |-> x,
+                                                                               read_only |-> req.read_only])
+        /\ volumes' = [volumes EXCEPT ![volID].state = "in-use"]
+        /\ val = PublicationView(volID, nodeID)'
+        /\ err = None
+        /\ UNCHANGED snapshots
+
+
+UnpublishVolumeRequests == [volume_id : Optional(VolumeIDs),
+                            handle    : Optional(VolumeHandles),
+                            node_id   : Optional(NodeIDs)]
+
+UnpublishVolume(req, err) ==
+  (*******************************************************************************************************************)
+  (* A volume's export on a node is torn down, so that its data is no longer reachable there. Once no node           *)
+  (* can reach the volume, it is available again.                                                                    *)
+  (*******************************************************************************************************************)
+  LET volID  == req.volume_id
+      nodeID == req.node_id
+
+      Errors ==
+        LET checks == [invalid_argument |-> None \in {volID, nodeID}]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        \* Record removal is idempotent so that retries succeed.
+        /\ publications' = RemoveKey(publications, <<volID, nodeID>>)
+        \* The volume is available again once no node holds it.
+        /\ volumes' = IF \/ ~KeyExists(volumes, volID)
+                         \/ PublishedNodes(volID)' /= {}
+                      THEN volumes
+                      ELSE [volumes EXCEPT ![volID].state = "available"]
+        /\ err = None
+        /\ UNCHANGED snapshots
+
+
+DeleteVolumeRequests == [volume_id : Optional(VolumeIDs),
+                         handle    : Optional(VolumeHandles)]
+
+DeleteVolume(req, err) ==
+  (*******************************************************************************************************************)
+  (* A volume is deleted, so that its data is gone. Snapshots taken from it are unaffected.                          *)
+  (*******************************************************************************************************************)
+  LET volID == req.volume_id
+
+      Errors ==
+        LET checks == [invalid_argument |-> volID = None,
+                       volume_in_use    |-> /\ PublishedNodes(volID) /= {}
+                                            /\ req.handle \in {None, volumes[volID].handle}]
+        IN {e \in DOMAIN checks : checks[e]}
+
+     \* The request was rejected, or the provider failed to answer.
+  IN \/ /\ err \in Errors \union ProviderErrors
+        /\ UNCHANGED vars
+
+     \* The request was accepted.
+     \/ /\ Errors = {}
+        \* Record removal is idempotent so that retries succeed.
+        /\ volumes' = IF /\ KeyExists(volumes, volID)
+                         /\ req.handle \notin {None, volumes[volID].handle}
+                      THEN volumes
+                      ELSE RemoveKey(volumes, volID)
+        /\ err = None
+        /\ UNCHANGED <<publications, snapshots>>
+
+-----------------------------------------------------------------------------------------------------------------------
+\* Specification
+
+=======================================================================================================================