From 7370a45083e92e1c532fd4491a7175d6509b2fb4 Mon Sep 17 00:00:00 2001
From: Thomas Lively <tlively@google.com>
Date: Thu, 9 Oct 2025 10:31:24 -0700
Subject: [PATCH] Do not store continuation arities

Real implementations will determine continuation arities by inspecting
the type immediates on the instructions that manipulate those
continuations, not by reading the arities off the continuations at
runtime. Update the semantics given in the explainer to compute arities
from type immediates as well.
---
 proposals/stack-switching/Explainer.md | 37 +++++++++++---------------
 1 file changed, 16 insertions(+), 21 deletions(-)

diff --git a/proposals/stack-switching/Explainer.md b/proposals/stack-switching/Explainer.md
index d0fb016b..4c70383d 100644
--- a/proposals/stack-switching/Explainer.md
+++ b/proposals/stack-switching/Explainer.md
@@ -1050,15 +1050,15 @@ of event, even if they use the correct tag.
 * New store component `conts` for allocated continuations
   - `S ::= {..., conts <continst>?*}`
 
-* A continuation is a context annotated with its hole's arity
-  - `continst ::= (E : n)`
+* A continuation is a context
+  - `continst ::= E`
 
 
 #### Administrative instructions
 
 * `(ref.cont a)` represents a continuation value, where `a` is a *continuation address* indexing into the store's `conts` component
   - `ref.cont a : [] -> [(ref $ct)]`
-    - iff `S.conts[a] = epsilon \/ S.conts[a] = (E : n)`
+    - iff `S.conts[a] = epsilon \/ S.conts[a] = E`
       + iff `E[val^n] : t2*`
       + and `(val : t1)^n`
     - and `$ct ~~ cont $ft`
@@ -1087,10 +1087,8 @@ H^ea ::=
 * `S; F; (ref.null t) (cont.new $ct)  -->  S; F; trap`
 
 * `S; F; (ref.func fa) (cont.new $ct)  -->  S'; F; (ref.cont |S.conts|)`
-  - iff `S' = S with conts += (E : n)`
+  - iff `S' = S with conts += E`
   - and `E = _ (invoke fa)`
-  - and `$ct ~~ cont $ft`
-  - and `$ft ~~ [t1^n] -> [t2*]`
 
 * `S; F; (ref.null t) (cont.bind $ct $ct')  -->  S; F; trap`
 
@@ -1098,11 +1096,11 @@ H^ea ::=
   - iff `S.conts[ca] = epsilon`
 
 * `S; F; v^n (ref.cont ca) (cont.bind $ct $ct')  -->  S'; F; (ref.cont |S.conts|)`
-  - iff `S.conts[ca] = (E' : n')`
-  - and `$ct' ~~ cont $ft'`
-  - and `$ft' ~~ [t1'*] -> [t2'*]`
-  - and `n = n' - |t1'*|`
-  - and `S' = S with conts[ca] = epsilon with conts += (E : |t1'*|)`
+  - iff `S.conts[ca] = E'`
+  - and `$ct ~~ cont [t1*] -> [t2*]`
+  - and `$ct' ~~ cont [t1'*] -> [t2'*]`
+  - and `n = |t1*| - |t1'*|`
+  - and `S' = S with conts[ca] = epsilon with conts += E`
   - and `E = E'[v^n _]`
 
 * `S; F; (ref.null t) (resume $ct hdl*)  -->  S; F; trap`
@@ -1111,8 +1109,9 @@ H^ea ::=
   - iff `S.conts[ca] = epsilon`
 
 * `S; F; v^n (ref.cont ca) (resume $ct hdl*)  -->  S'; F; prompt{hdl'*} E[v^n] end`
-  - iff `S.conts[ca] = (E : n)`
+  - iff `S.conts[ca] = E`
   - and `S' = S with conts[ca] = epsilon`
+  - and `$ct ~~ cont [t1^n] -> [t2*]`
   - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]`
 
 * `S; F; (ref.null t) (resume_throw $ct $e hdl*)  -->  S; F; trap`
@@ -1128,10 +1127,10 @@ H^ea ::=
   - iff `S.conts[ca] = epsilon`
 
 * `S; F; (ref.null t) (ref.cont ca) (resume_throw_ref $ct hdl*)  -->  S; F; trap`
-  - iff `S.conts[ca] = (E : n)`
+  - iff `S.conts[ca] = E`
 
 * `S; F; (ref.exn ea) (ref.cont ca) (resume_throw_ref $ct hdl*)  -->  S'; F; prompt{hdl'*} E[(ref.exn ea) throw_ref] end`
-  - iff `S.conts[ca] = (E : n)`
+  - iff `S.conts[ca] = E`
   - and `S' = S with conts[ca] = epsilon`
   - and `hdl'* = hdl*[F.module.tags / 0..|F.module.tags|-1]`
 
@@ -1154,15 +1153,11 @@ H^ea ::=
   - iff `S.conts[ca] = epsilon`
 
 * `S; F; (prompt{hdl1* (on ea switch) hdl2*} H^ea[v^n (ref.cont ca) (switch $ct ea)] end) --> S''; F; prompt{hdl1* (on ea switch) hdl2*} E[v^n (ref.cont |S.conts|)] end`
-  - iff  `S.conts[ca] = (E : n')`
-  - and `n' = 1 + n`
+  - iff  `S.conts[ca] = E`
   - and `(on switch ea) notin hdl1*`
-  - and `$ct ~~ cont $ft`
-  - and `$ft ~~ [t1* (ref $ct2)] -> [t2*]`
-  - and `$ct2 ~~ cont $ft2`
-  - and `$ft2 ~~ [t1'^m] -> [t2'*]`
+  - and `$ct ~~ cont [t1^n (ref $ct2)] -> [t2*]`
   - and `S' = S with conts[ca] = epsilon`
-  - and `S'' = S' with conts += (H^ea : m)`
+  - and `S'' = S' with conts += H^ea`
 
 ### Binary format