Typestates 0.7 uplift

.github/workflows/build.yml

@@ -16,6 +16,25 @@ env:
   GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
 jobs:
+  lint:
+    name: Lint (typestates verify)
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v4
+
+      - name: Setup Nim
+        uses: jiro4989/setup-nim-action@v2
+        with:
+          nim-version: 'stable'
+
+      - name: Install typestates
+        run: nimble install -y "typestates@0.7.2"
+
+      - name: Typestates verify
+        run: typestates verify -W --format=github src/
+
   test:
     name: Test nim-${{ matrix.nim-version }} / ${{ matrix.runs-on }}
     runs-on: ${{ matrix.runs-on }}

CHANGELOG.md

@@ -7,6 +7,24 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### BREAKING
+
+- `CASAttempt` typestate restructured into a proper typestate union. `CASPending` now transitions to `CASSucceeded | CASFailed` (aliased as `CASResult`) via `executeCAS`, replacing the previous single-state design with `assumeSuccess` / `assumeFailure` escape hatches. The `assumeSuccess` and `assumeFailure` procs have been removed. Callers that drove `CASAttempt` outside the bundled MPMC machinery must migrate to the union return form. These helpers were only consumed by `tests/t_cas.nim`; the bundled MPMC machinery calls `compareExchangeWeak` directly and was unaffected. No public lock-free queue API is affected.
+
+### Changed
+
+- Bump minimum `typestates` to 0.7.2. Pulls in the upstream `match` macro fixes for generic and cross-module contexts shipped in nim-typestates v0.7.1 / v0.7.2.
+- `opaqueStates = true` and `initial:` / `terminal:` DSL blocks added to 5 SET typestates: `CASAttempt`, `SPSCPopOp`, `SPSCPushOp`, `VirtualValueN`, and `VirtualValueN1`.
+- 8 hand-written `case .kind` dispatches across 4 facade modules (`sipsic.nim`, `mupmuc.nim`, `mupsic.nim`, `sipmuc.nim`) replaced with the generated `match` macro for compile-time exhaustiveness.
+
+### Added
+
+- CI: `typestates verify -W --format=github src/` step in `build.yml` to gate the typestate model against drift.
+
+### Fixed
+
+- 22 read-only typestate accessors across `src/lockfreequeues/typestates/` now carry `{.notATransition.}`. typestates' verifier flagged these once `typestates verify -W` was wired into CI; the procs are pure data extraction and were never transitions.
+
 ## [4.1.0] - 2026-05-01
 
 ### Added

lockfreequeues.nimble

@@ -11,8 +11,8 @@ entryPoints    = @["tests/test.nim"]
 # Dependencies
 requires "nim >= 2.2.0"
 requires "unittest2"
-requires "typestates >= 0.6.0"
-requires "debra >= 0.5.0"
+requires "typestates >= 0.7.2"
+requires "debra >= 0.7.0"
 
 # Tasks
 task test, "Runs the test suite":

src/lockfreequeues.nim

@@ -1,13 +1,13 @@
 when compileOption("threads"):
   import
     ./lockfreequeues/[
-      atomic_dsl, exceptions, mupmuc, mupsic, sipmuc, sipsic,
-      unbounded_mupmuc, unbounded_mupsic, unbounded_sipmuc, unbounded_sipsic,
+      atomic_dsl, exceptions, mupmuc, mupsic, sipmuc, sipsic, unbounded_mupmuc,
+      unbounded_mupsic, unbounded_sipmuc, unbounded_sipsic,
     ]
 
   export
-    atomic_dsl, exceptions, mupmuc, mupsic, sipmuc, sipsic,
-    unbounded_mupmuc, unbounded_mupsic, unbounded_sipmuc, unbounded_sipsic
+    atomic_dsl, exceptions, mupmuc, mupsic, sipmuc, sipsic, unbounded_mupmuc,
+    unbounded_mupsic, unbounded_sipmuc, unbounded_sipsic
 else:
   # threading off, only provide sipsic
   import ./lockfreequeues/[atomic_dsl, sipsic]

src/lockfreequeues/mupmuc.nim

@@ -176,16 +176,16 @@ proc push*[N, P, C: static int, T](self: MupmucProducer[N, P, C, T], item: T): b
   var op = mpmc_push.start[N]()
   var spins = InitialSpin
   while true:
-    let claim = op.tryClaim(queueBase[])
-    case claim.kind
-    of mMPMCPushFull:
-      return claim.mpmcpushfull.extractFalse()
-    of mMPMCPushSlotClaimed:
-      return claim.mpmcpushslotclaimed.complete(queueBase[], item)
-    of mMPMCPushStart:
-      op = claim.mpmcpushstart # CAS race or producer raced ahead: retry
-      backoffOnRetry(spins)
-      continue
+    var claim = op.tryClaim(queueBase[])
+    match claim:
+      MPMCPushFull(full):
+        return full.extractFalse()
+      MPMCPushSlotClaimed(slotClaimed):
+        return slotClaimed.complete(queueBase[], item)
+      MPMCPushStart(restart):
+        op = restart # CAS race or producer raced ahead: retry
+        backoffOnRetry(spins)
+        continue
 
 proc push*[N, P, C: static int, T](
     self: MupmucProducer[N, P, C, T], items: openArray[T]
@@ -225,16 +225,16 @@ proc pop*[N, P, C: static int, T](self: Consumer[N, P, C, T]): Option[T] =
   var op = mpmc_pop.start[N]()
   var spins = InitialSpin
   while true:
-    let claim = op.tryClaim(queueBase[])
-    case claim.kind
-    of mMPMCPopEmpty:
-      return none(T)
-    of mMPMCPopSlotClaimed:
-      return some(claim.mpmcpopslotclaimed.complete(queueBase[]))
-    of mMPMCPopStart:
-      op = claim.mpmcpopstart # CAS race or consumer raced ahead: retry
-      backoffOnRetry(spins)
-      continue
+    var claim = op.tryClaim(queueBase[])
+    match claim:
+      MPMCPopEmpty(_):
+        return none(T)
+      MPMCPopSlotClaimed(slotClaimed):
+        return some(slotClaimed.complete(queueBase[]))
+      MPMCPopStart(restart):
+        op = restart # CAS race or consumer raced ahead: retry
+        backoffOnRetry(spins)
+        continue
 
 proc pop*[N, P, C: static int, T](
     self: Consumer[N, P, C, T], count: int

src/lockfreequeues/mupsic.nim

@@ -59,18 +59,17 @@ type
 # object-field offsets are computed structurally, so a match for one
 # instantiation implies a match for all.
 static:
-  doAssert offsetOf(Mupsic[8, 4, int], head) ==
-    offsetOf(MupsicPushBase[8, 4, int], head)
-  doAssert offsetOf(Mupsic[8, 4, int], tail) ==
-    offsetOf(MupsicPushBase[8, 4, int], tail)
+  doAssert offsetOf(Mupsic[8, 4, int], head) == offsetOf(
+    MupsicPushBase[8, 4, int], head
+  )
+  doAssert offsetOf(Mupsic[8, 4, int], tail) == offsetOf(
+    MupsicPushBase[8, 4, int], tail
+  )
   doAssert offsetOf(Mupsic[8, 4, int], cells) ==
     offsetOf(MupsicPushBase[8, 4, int], cells)
-  doAssert offsetOf(Mupsic[8, 4, int], head) ==
-    offsetOf(MupsicBase[8, 4, int], head)
-  doAssert offsetOf(Mupsic[8, 4, int], tail) ==
-    offsetOf(MupsicBase[8, 4, int], tail)
-  doAssert offsetOf(Mupsic[8, 4, int], cells) ==
-    offsetOf(MupsicBase[8, 4, int], cells)
+  doAssert offsetOf(Mupsic[8, 4, int], head) == offsetOf(MupsicBase[8, 4, int], head)
+  doAssert offsetOf(Mupsic[8, 4, int], tail) == offsetOf(MupsicBase[8, 4, int], tail)
+  doAssert offsetOf(Mupsic[8, 4, int], cells) == offsetOf(MupsicBase[8, 4, int], cells)
 
 proc clear[N, P: static int, T](self: var Mupsic[N, P, T]) =
   self.head.store(0'u64, moRelaxed)
@@ -133,16 +132,16 @@ proc push*[N, P: static int, T](self: Producer[N, P, T], item: T): bool =
   var op = mpsc_push.start[N]()
   var spins = InitialSpin
   while true:
-    let claim = op.tryClaim(queueBase[])
-    case claim.kind
-    of mMPSCPushFull:
-      return claim.mpscpushfull.extractFalse()
-    of mMPSCPushSlotClaimed:
-      return claim.mpscpushslotclaimed.complete(queueBase[], item)
-    of mMPSCPushStart:
-      op = claim.mpscpushstart # CAS race or producer raced ahead: retry
-      backoffOnRetry(spins)
-      continue
+    var claim = op.tryClaim(queueBase[])
+    match claim:
+      MPSCPushFull(full):
+        return full.extractFalse()
+      MPSCPushSlotClaimed(slotClaimed):
+        return slotClaimed.complete(queueBase[], item)
+      MPSCPushStart(restart):
+        op = restart # CAS race or producer raced ahead: retry
+        backoffOnRetry(spins)
+        continue
 
 proc push*[N, P: static int, T](
     self: Producer[N, P, T], items: openArray[T]
@@ -193,16 +192,16 @@ proc pop*[N, P: static int, T](self: var Mupsic[N, P, T]): Option[T] =
   var op = mpsc_pop.start[N]()
   var spins = InitialSpin
   while true:
-    let claim = op.tryClaim(queueBase[])
-    case claim.kind
-    of mMPSCPopEmpty:
-      return none(T)
-    of mMPSCPopSlotClaimed:
-      return some(claim.mpscpopslotclaimed.complete(queueBase[]))
-    of mMPSCPopStart:
-      op = claim.mpscpopstart # CAS race or consumer raced ahead: retry
-      backoffOnRetry(spins)
-      continue
+    var claim = op.tryClaim(queueBase[])
+    match claim:
+      MPSCPopEmpty(_):
+        return none(T)
+      MPSCPopSlotClaimed(slotClaimed):
+        return some(slotClaimed.complete(queueBase[]))
+      MPSCPopStart(restart):
+        op = restart # CAS race or consumer raced ahead: retry
+        backoffOnRetry(spins)
+        continue
 
 proc pop*[N, P: static int, T](self: var Mupsic[N, P, T], count: int): Option[seq[T]] =
   ## Pop up to `count` items from the queue (best-effort drain).

src/lockfreequeues/sipmuc.nim

@@ -58,18 +58,17 @@ type
 # object-field offsets are computed structurally, so a match for one
 # instantiation implies a match for all.
 static:
-  doAssert offsetOf(Sipmuc[8, 4, int], head) ==
-    offsetOf(SipmucPushBase[8, 4, int], head)
-  doAssert offsetOf(Sipmuc[8, 4, int], tail) ==
-    offsetOf(SipmucPushBase[8, 4, int], tail)
+  doAssert offsetOf(Sipmuc[8, 4, int], head) == offsetOf(
+    SipmucPushBase[8, 4, int], head
+  )
+  doAssert offsetOf(Sipmuc[8, 4, int], tail) == offsetOf(
+    SipmucPushBase[8, 4, int], tail
+  )
   doAssert offsetOf(Sipmuc[8, 4, int], cells) ==
     offsetOf(SipmucPushBase[8, 4, int], cells)
-  doAssert offsetOf(Sipmuc[8, 4, int], head) ==
-    offsetOf(SipmucBase[8, 4, int], head)
-  doAssert offsetOf(Sipmuc[8, 4, int], tail) ==
-    offsetOf(SipmucBase[8, 4, int], tail)
-  doAssert offsetOf(Sipmuc[8, 4, int], cells) ==
-    offsetOf(SipmucBase[8, 4, int], cells)
+  doAssert offsetOf(Sipmuc[8, 4, int], head) == offsetOf(SipmucBase[8, 4, int], head)
+  doAssert offsetOf(Sipmuc[8, 4, int], tail) == offsetOf(SipmucBase[8, 4, int], tail)
+  doAssert offsetOf(Sipmuc[8, 4, int], cells) == offsetOf(SipmucBase[8, 4, int], cells)
 
 proc clear[N, C: static int, T](self: var Sipmuc[N, C, T]) =
   self.head.store(0'u64, moRelaxed)
@@ -106,16 +105,16 @@ proc push*[N, C: static int, T](self: var Sipmuc[N, C, T], item: T): bool =
   var op = spmc_push.start[N]()
   var spins = InitialSpin
   while true:
-    let claim = op.tryClaim(queueBase[])
-    case claim.kind
-    of sSPMCPushFull:
-      return claim.spmcpushfull.extractFalse()
-    of sSPMCPushSlotClaimed:
-      return claim.spmcpushslotclaimed.complete(queueBase[], item)
-    of sSPMCPushStart:
-      op = claim.spmcpushstart # CAS race or producer raced ahead: retry
-      backoffOnRetry(spins)
-      continue
+    var claim = op.tryClaim(queueBase[])
+    match claim:
+      SPMCPushFull(full):
+        return full.extractFalse()
+      SPMCPushSlotClaimed(slotClaimed):
+        return slotClaimed.complete(queueBase[], item)
+      SPMCPushStart(restart):
+        op = restart # CAS race or producer raced ahead: retry
+        backoffOnRetry(spins)
+        continue
 
 proc push*[N, C: static int, T](
     self: var Sipmuc[N, C, T], items: openArray[T]
@@ -184,16 +183,16 @@ proc pop*[N, C: static int, T](self: Consumer[N, C, T]): Option[T] =
   var op = spmc_pop.start[N]()
   var spins = InitialSpin
   while true:
-    let claim = op.tryClaim(queueBase[])
-    case claim.kind
-    of sSPMCPopEmpty:
-      return none(T)
-    of sSPMCPopSlotClaimed:
-      return some(claim.spmcpopslotclaimed.complete(queueBase[]))
-    of sSPMCPopStart:
-      op = claim.spmcpopstart # CAS race or consumer raced ahead: retry
-      backoffOnRetry(spins)
-      continue
+    var claim = op.tryClaim(queueBase[])
+    match claim:
+      SPMCPopEmpty(_):
+        return none(T)
+      SPMCPopSlotClaimed(slotClaimed):
+        return some(slotClaimed.complete(queueBase[]))
+      SPMCPopStart(restart):
+        op = restart # CAS race or consumer raced ahead: retry
+        backoffOnRetry(spins)
+        continue
 
 proc pop*[N, C: static int, T](self: Consumer[N, C, T], count: int): Option[seq[T]] =
   ## Pop up to `count` items from the queue (best-effort drain).

src/lockfreequeues/sipsic.nim

@@ -43,12 +43,11 @@ proc push*[N: static int, T](self: var Sipsic[N, T], item: T): bool =
   let loaded = op.loadPointers(queueBase[])
   var fullCheck = loaded.checkFull()
 
-  case fullCheck.kind
-  of sSPSCPushFull:
-    return move(fullCheck).spscpushfull.extractFalse()
-  of sSPSCPushNotFull:
-    return
-      move(fullCheck).spscpushnotfull.writeData(queueBase[], item).complete(queueBase[])
+  match fullCheck:
+    SPSCPushFull(full):
+      return full.extractFalse()
+    SPSCPushNotFull(notFull):
+      return notFull.writeData(queueBase[], item).complete(queueBase[])
 
 proc push*[N: static int, T](
     self: var Sipsic[N, T], items: openArray[T]
@@ -96,11 +95,11 @@ proc pop*[N: static int, T](self: var Sipsic[N, T]): Option[T] =
   let loaded = op.loadPointers(queueBase[])
   var emptyCheck = loaded.checkEmpty()
 
-  case emptyCheck.kind
-  of sSPSCPopEmpty:
-    return none(T)
-  of sSPSCPopNotEmpty:
-    return some(move(emptyCheck).spscpopnotempty.complete(queueBase[]))
+  match emptyCheck:
+    SPSCPopEmpty(_):
+      return none(T)
+    SPSCPopNotEmpty(notEmpty):
+      return some(notEmpty.complete(queueBase[]))
 
 proc pop*[N: static int, T](self: var Sipsic[N, T], count: int): Option[seq[T]] =
   ## Pop `count` items from the queue.