add new transition rejecting stop_canister calls (#229)

spec/_attachments/interface-spec-changelog.md

@@ -12,6 +12,7 @@
 * Remove `senders` field from user delegations.
 * The maximum length of a nonce in an ingress message is 32 bytes.
 * Update specification of responses from the endpoint `/api/v2/status`.
+* Stop canister calls might be rejected upon timeout.
 
 ### 0.21.0 (2023-09-18) {#0_21_0}
 * Canister cycle balance cannot decrease below the freezing limit after executing `install_code` on the management canister.

spec/index.md

@@ -4387,13 +4387,13 @@ The controllers of a canister can stop a canister. Stopping a canister goes thro
 
 We encode this behavior via three (types of) transitions:
 
-1.  First, any `stop_canister` call sets the state of the canister to `Stopping`; we record in the status the origin (and cycles) of all `stop_canister` calls which arrive at the canister while it is stopping (or stopped).
+1.  First, any `stop_canister` call sets the state of the canister to `Stopping`; we record in the IC state the origin (and cycles) of all `stop_canister` calls which arrive at the canister while it is stopping (or stopped). Note that every such `stop_canister` call can be rejected by the system at any time (the canister stays stopping in this case), e.g., if the `stop_canister` call could not be responded to for a long time.
 
 2.  Next, when the canister has no open call contexts (so, in particular, all outstanding responses to the canister have been processed), the status of the canister is set to `Stopped`.
 
 3.  Finally, each pending `stop_canister` call (which are encoded in the status) is responded to, to indicate that the canister is stopped.
 
-    Conditions  
+Conditions
 
 ```html
 
@@ -4417,8 +4417,6 @@ S with
 
 ```
 
-The next two transitions record any additional 'stop\_canister' requests that arrive at a stopping (or stopped) canister in its status.
-
 Conditions  
 
 ```html
@@ -4471,12 +4469,8 @@ S with
 
 ```
 
-:::note
-
 Sending a `stop_canister` message to an already stopped canister is acknowledged (i.e. responded with success), but is otherwise a no-op:
 
-:::
-
 Conditions  
 
 ```html
@@ -4505,6 +4499,31 @@ S with
 
 ```
 
+Pending `stop_canister` calls may be rejected by the system at any time (the canister stays stopping in this case):
+
+Conditions
+
+```html
+
+S.canister_status[CanisterId] = Stopping (Older_origins · (O, C) · Younger_origins)
+
+```
+
+State after
+
+```html
+
+S with
+    canister_status[CanisterId] = Stopping (Older_origins · Younger_origins)
+    messages = S.Messages ·
+      ResponseMessage {
+        origin = O
+        response = Reject (SYS_TRANSIENT, 'Stop canister request timed out')
+        refunded_cycles = C
+      }
+
+```
+
 #### IC Management Canister: Starting a canister
 
 The controllers of a canister can start a `stopped` canister. If the canister is already running, the command has no effect on the canister.
@@ -4568,7 +4587,7 @@ S with
         } ·
         [ ResponseMessage {
             origin = O
-            response = Reject (CANISTER_REJECT, 'Canister has been restarted')
+            response = Reject (CANISTER_ERROR, 'Canister has been restarted')
             refunded_cycles = C
           }
         | (O, C) ∈ Origins