diff --git a/Examples/README.md b/Examples/README.md
index c59df37..fffe8ad 100644
--- a/Examples/README.md
+++ b/Examples/README.md
@@ -26,6 +26,8 @@ dotnet run --project IronKernel -- run hello.ikc
 | `contracts.ikr` | Operative/applicative contracts and guarded folding | Prints validated results |
 | `coroutines.ikr` | Cooperative scheduling experiment | Historical example; not yet covered by the compatibility suite |
 | `zipper.ikr` | Delimited continuations | Functional zipper traversal |
+| `constant-width.ikr` | Mutable vectors, CPS backtracking, `args` | Enumerates constant-width chessboard figures; takes `n k w` |
+| `constant-width-amb.ikr` | `shift`/`reset` as an `amb` layer, `vau` search strategies, encapsulation types | Same problem, direct style; also solves n-queens and builds width 3/4/8 figures |
 | `sqrt.ikr` | Operative-based numeric procedure | Defines `sqrt`; intentionally produces no output |
 | `yingyang.ikr` | Classic yin-yang continuation loop | Intentionally non-terminating; do not use it to test packaging |
 
diff --git a/Examples/constant-width-amb.ikr b/Examples/constant-width-amb.ikr
new file mode 100644
index 0000000..7ac23cb
--- /dev/null
+++ b/Examples/constant-width-amb.ikr
@@ -0,0 +1,434 @@
+; Figures of constant width, second take: nondeterminism and algebra
+; ==================================================================
+;
+; `constant-width.ikr` transcribes the backtracking search from
+;
+;   https://ademar.name/blog/2009/04/finding-figures-of-constant-wi.html
+;
+; faithfully, continuation-passing style and all. This file attacks the same
+; problem -- see that file, or the Hernandez-Robert paper it cites, for what a
+; figure of constant width is -- from two directions that suit IronKernel
+; rather than F#.
+;
+; 1. Backtracking is not a program shape here, it is a library.
+;
+;    `shift`/`reset` in IronKernel are multi-shot and re-delimiting, which is
+;    exactly what a nondeterministic `amb` needs: a choice point invokes the
+;    captured continuation once per alternative. So the solver is written in
+;    *direct style* -- `(let ((c (pick-column x lo hi))) ...)` reads as "let c
+;    be a column", and the enumeration, the undo of the board state, and the
+;    pruning all happen inside `pick-column`. There is not one explicit
+;    continuation argument in the search.
+;
+;    The other half of that split is that the *strategy* becomes a value. The
+;    solver only ever calls `emit`; two operatives decide what that means:
+;    `collect` gathers every solution, `first-of` escapes with the first one
+;    through `call/cc`. Same solver, different searches, chosen at the call
+;    site. Adding a "first 10" or a randomized strategy is a handler, not a
+;    rewrite.
+;
+;    A consequence worth stating: this solver enumerates figures of *exactly*
+;    type (n,k,w), disconnected ones included. The original algorithm grows a
+;    figure outward from a seed square and so can only ever find connected
+;    figures -- it explicitly cannot solve the n-queens problem, which is the
+;    w=1 case. This one can, and `(figures 8 8 1)` returning 92 is the check.
+;
+; 2. For width 3 and up, do not search at all -- build.
+;
+;    The paper's Lemma 1 says that composing an *extended* constant width
+;    figure with any constant width figure multiplies the widths, and that a
+;    figure decomposable into transversals stays decomposable. That is a
+;    constructive recipe, and it is far cheaper than search: the original
+;    program needed about 31 days to exhaust width 3 on an 11x11 board, whereas
+;    composing the paper's Figure 3 with its Figure 2 and deleting a transversal
+;    produces a width 3 figure in milliseconds. Widths 4 and 8 come out of the
+;    same handful of lines, and peeling the width 8 one twice reaches width 6 --
+;    which the paper reports its authors never managed to find by search.
+;
+;    `transversal` is itself written against the `amb` layer from part 1, so
+;    the same three-line nondeterminism library drives both halves of the file.
+;
+; Run it:
+;
+;   dotnet run --project IronKernel -- Examples/constant-width-amb.ikr
+;
+; Takes about half a minute, nearly all of it in the 8-queens enumeration --
+; the constructive half of the file runs in milliseconds. Requires the default
+; `unrestricted` profile (it prints to the host console).
+;
+; Everything printed is checked by `fig-type`, which shares no code with the
+; searcher or the builders. The searcher's counts also agree with an
+; independent exhaustive row-by-row search: 92 and 4 for 8- and 6-queens, and
+; 1, 5, 2, 24, 30 figures of type (4,4,2), (5,4,2), (6,6,2), (7,6,2), (8,8,2).
+
+; ---------------------------------------------------------------------------
+; 1. Nondeterminism as a library
+; ---------------------------------------------------------------------------
+
+(defn (reverse xs)
+  (letrec ((loop (lambda (l acc)
+                   (if (null? l) acc (loop (cdr l) (cons (car l) acc))))))
+    (loop xs ())))
+
+; The solution sink. Nondeterministic code calls `emit`; what that does is
+; whatever the enclosing strategy installed.
+(define sink (make-vector 1 (lambda (s) #inert)))
+(defn (emit s) ((vector-ref sink 0) s))
+
+; Abandon this branch: capture the continuation up to the delimiter and drop
+; it, so control returns to the most recent choice point.
+(defn (fail) (shift (lambda (k) #inert)))
+
+; Yield each element of xs in turn. `k` is multi-shot and re-delimits, so the
+; whole remaining computation runs once per alternative.
+(defn (amb xs) (shift (lambda (k) (for-each xs k))))
+
+; Strategy 1: run body, return the list of everything it emitted.
+(define collect
+  (vau body env
+    (let ((acc (make-vector 1 ())) (saved (vector-ref sink 0)))
+      (vector-set! sink 0
+        (lambda (s) (vector-set! acc 0 (cons s (vector-ref acc 0)))))
+      (reset (eval env (cons sequence body)))
+      (vector-set! sink 0 saved)
+      (reverse (vector-ref acc 0)))))
+
+; Strategy 2: stop at the first emission and escape with it, or () if there is
+; none. The whole search tree below the first hit is never explored.
+(define first-of
+  (vau body env
+    (let ((saved (vector-ref sink 0)))
+      (let ((r (call/cc (lambda (return)
+                          (vector-set! sink 0 (lambda (s) (return s)))
+                          (reset (eval env (cons sequence body)))
+                          ()))))
+        (vector-set! sink 0 saved)
+        r))))
+
+; ---------------------------------------------------------------------------
+; 2. The solver: emit every figure of exactly type (n, k, w)
+;
+; Rows are decided in order. Each row is either skipped or given exactly w
+; columns, and a row's squares are chosen left to right. Every line carries a
+; count of squares placed on it so far; a line is legal at the end when that
+; count is 0 or w, and legal in the middle when the shortfall still fits in the
+; rows below.
+; ---------------------------------------------------------------------------
+
+(defn (figures n k w)
+  (define col (make-vector n 0))
+  (define pd  (make-vector (- (* 2 n) 1) 0))
+  (define nd  (make-vector (- (* 2 n) 1) 0))
+  (define fig (make-vector 1 ()))
+
+  (defn (pdx x y) (+ x y))
+  (defn (ndx x y) (- (+ n (- x y)) 1))
+
+  (defn (free? x y)
+    (if (< (vector-ref col y) w)
+      (if (< (vector-ref pd (pdx x y)) w)
+        (< (vector-ref nd (ndx x y)) w)
+        #f)
+      #f))
+
+  (defn (bump! x y d)
+    (vector-set! col y (+ (vector-ref col y) d))
+    (vector-set! pd (pdx x y) (+ (vector-ref pd (pdx x y)) d))
+    (vector-set! nd (ndx x y) (+ (vector-ref nd (ndx x y)) d)))
+
+  (defn (place! x y)
+    (bump! x y 1)
+    (vector-set! fig 0 (cons (cons x y) (vector-ref fig 0))))
+
+  (defn (unplace! x y)
+    (bump! x y -1)
+    (vector-set! fig 0 (cdr (vector-ref fig 0))))
+
+  ; The one choice point of the search. Each legal column in [lo,hi) is placed,
+  ; offered to the continuation, and taken back once that continuation has run
+  ; to exhaustion -- so the board is always consistent with the caller's view,
+  ; and the caller never sees a continuation at all.
+  (defn (pick-column x lo hi)
+    (shift (lambda (k)
+      (letrec ((loop (lambda (c)
+                       (if (< c hi)
+                         (begin
+                           (if (free? x c)
+                             (begin (place! x c) (k c) (unplace! x c))
+                             #inert)
+                           (loop (+ c 1)))
+                         #inert))))
+        (loop lo)))))
+
+  ; `need` more squares in row x, all in columns >= y. Reads as a loop; is a
+  ; tree.
+  (defn (fill-row x y need)
+    (if (zero? need)
+      #inert
+      (let ((c (pick-column x y (+ (- n need) 1))))
+        (fill-row x (+ c 1) (- need 1)))))
+
+  ; How many cells of diagonal `d` lie in rows x..n-1. Both diagonal families
+  ; are indexed so that this one formula serves for each.
+  (defn (cells-from d x)
+    (let ((lo (if (> x (- d (- n 1))) x (- d (- n 1))))
+          (hi (if (< (- n 1) d) (- n 1) d)))
+      (if (< hi lo) 0 (+ (- hi lo) 1))))
+
+  ; A line is still viable if it is untouched, already full, or short by no
+  ; more than the cells it has left. At x = n this is the 0-or-w test.
+  (defn (line-ok? used avail)
+    (if (zero? used) #t (if (eq? used w) #t (<= (- w used) avail))))
+
+  (define ndiags (- (* 2 n) 1))
+
+  (defn (feasible? x)
+    (let ((rowsleft (- n x)))
+      (letrec
+        ((cols (lambda (c)
+                 (if (eq? c n) #t
+                   (if (line-ok? (vector-ref col c) rowsleft)
+                     (cols (+ c 1)) #f))))
+         ; both diagonal families share an index, so one `cells-from` serves
+         ; the pair
+         (diags (lambda (d)
+                  (if (eq? d ndiags) #t
+                    (let ((a (cells-from d x)))
+                      (if (line-ok? (vector-ref pd d) a)
+                        (if (line-ok? (vector-ref nd d) a)
+                          (diags (+ d 1)) #f)
+                        #f))))))
+        (if (cols 0) (diags 0) #f))))
+
+  (defn (solve x placed)
+    (if (eq? x n)
+      ; every row decided: the figure must have k filled rows and no line may
+      ; be left part-way
+      (if (eq? placed k)
+        (if (feasible? n) (emit (vector-ref fig 0)) (fail))
+        (fail))
+      (begin
+        (if (< (- n x) (- k placed)) (fail) #inert)   ; too few rows left
+        (if (feasible? x) #inert (fail))
+        (if (amb (list #t #f))
+          (begin (if (< placed k) #inert (fail))
+                 (fill-row x 0 w)
+                 (solve (+ x 1) (+ placed 1)))
+          (solve (+ x 1) placed)))))
+
+  (solve 0 0))
+
+; ---------------------------------------------------------------------------
+; 3. Figures as an abstract type, and the constant width test
+; ---------------------------------------------------------------------------
+
+(provide! (figure figure? fig-n fig-squares)
+  (define (enc figure? dec) (make-encapsulation-type))
+  (define figure (lambda (n squares) (enc (list n squares))))
+  (define fig-n (lambda (f) (car (dec f))))
+  (define fig-squares (lambda (f) (cadr (dec f)))))
+
+(defn (tally! v i) (vector-set! v i (+ (vector-ref v i) 1)))
+
+; (n k w) when f has constant width, () otherwise. Everything this file builds
+; is checked with this, and it shares no code with the builders.
+(defn (fig-type f)
+  (let* ((n (fig-n f)) (s (fig-squares f)) (m (- (* 2 n) 1))
+         (rw (make-vector n 0)) (cl (make-vector n 0))
+         (pd (make-vector m 0)) (nd (make-vector m 0)))
+    (for-each s (lambda (p)
+      (tally! rw (car p))
+      (tally! cl (cdr p))
+      (tally! pd (+ (car p) (cdr p)))
+      (tally! nd (- (+ n (- (car p) (cdr p))) 1))))
+    ; fold the four families together: every non-zero count must agree
+    (letrec ((scan (lambda (v i len w)
+                     (if (eq? i len) w
+                       (let ((c (vector-ref v i)))
+                         (if (zero? c) (scan v (+ i 1) len w)
+                           (if (zero? w) (scan v (+ i 1) len c)
+                             (if (eq? c w) (scan v (+ i 1) len w) -1))))))))
+      (let* ((w1 (scan rw 0 n 0)) (w2 (scan cl 0 n w1))
+             (w3 (scan pd 0 m w2)) (w (scan nd 0 m w3)))
+        (if (< w 1) () (list n (/ (length s) w) w))))))
+
+; `/` truncates toward zero, so fold the negative case back by hand.
+(defn (modulo a m) (let ((r (- a (* m (/ a m))))) (if (< r 0) (+ r m) r)))
+
+; Extended constant width: the diagonals wrap around the board, so the lines
+; are i+j and i-j taken mod n. Lemma 1 needs this of its left operand.
+(defn (extended? f)
+  (let* ((n (fig-n f)) (s (fig-squares f))
+         (p (make-vector n 0)) (q (make-vector n 0)))
+    (for-each s (lambda (sq)
+      (tally! p (modulo (+ (car sq) (cdr sq)) n))
+      (tally! q (modulo (- (car sq) (cdr sq)) n))))
+    (let ((t (fig-type f)))
+      (if (null? t) #f
+        (let ((w (car (cddr t))))
+          (letrec ((ok (lambda (v i)
+                         (if (eq? i n) #t
+                           (let ((c (vector-ref v i)))
+                             (if (zero? c) (ok v (+ i 1))
+                               (if (eq? c w) (ok v (+ i 1)) #f)))))))
+            (if (ok p 0) (ok q 0) #f)))))))
+
+; ---------------------------------------------------------------------------
+; 4. The algebra
+; ---------------------------------------------------------------------------
+
+; Lemma 1: drop a copy of f1 into every square of f2. If f1 has extended
+; constant width w1 and f2 constant width w2, the result has constant width
+; w1*w2 on a board (n1*n2) wide.
+(defn (compose f1 f2)
+  (let ((m (fig-n f1)) (acc (make-vector 1 ())))
+    (for-each (fig-squares f2) (lambda (q)
+      (for-each (fig-squares f1) (lambda (p)
+        (vector-set! acc 0
+          (cons (cons (+ (car p) (* m (car q))) (+ (cdr p) (* m (cdr q))))
+                (vector-ref acc 0)))))))
+    (figure (* m (fig-n f2)) (vector-ref acc 0))))
+
+(defn (same-square? p q) (if (eq? (car p) (car q)) (eq? (cdr p) (cdr q)) #f))
+
+(defn (member-of? p s)
+  (if (null? s) #f (if (same-square? p (car s)) #t (member-of? p (cdr s)))))
+
+; A transversal is a subset meeting every line of f exactly once. Because f has
+; constant width w and kw squares, it touches exactly k lines of each of the
+; four families, so a transversal is one square per filled row whose columns
+; and diagonals are all distinct -- a perfect matching, found here by the same
+; `amb` machinery as the figure search. Nondeterministic: wrap in `first-of`.
+(defn (transversal f)
+  (let* ((n (fig-n f)) (s (fig-squares f)) (m (- (* 2 n) 1))
+         (byrow (make-vector n ()))
+         (uc (make-vector n 0)) (up (make-vector m 0)) (un (make-vector m 0)))
+    (for-each s (lambda (p)
+      (vector-set! byrow (car p) (cons p (vector-ref byrow (car p))))))
+    (letrec
+      ((pdx (lambda (p) (+ (car p) (cdr p))))
+       (ndx (lambda (p) (- (+ n (- (car p) (cdr p))) 1)))
+       (avail? (lambda (p)
+                 (if (zero? (vector-ref uc (cdr p)))
+                   (if (zero? (vector-ref up (pdx p)))
+                     (zero? (vector-ref un (ndx p)))
+                     #f)
+                   #f)))
+       (mark! (lambda (p d)
+                (vector-set! uc (cdr p) (+ (vector-ref uc (cdr p)) d))
+                (vector-set! up (pdx p) (+ (vector-ref up (pdx p)) d))
+                (vector-set! un (ndx p) (+ (vector-ref un (ndx p)) d))))
+       (pick (lambda (cands)
+               (shift (lambda (k)
+                 (for-each cands (lambda (p)
+                   (if (avail? p)
+                     (begin (mark! p 1) (k p) (mark! p -1))
+                     #inert)))))))
+       (go (lambda (r acc)
+             (if (eq? r n)
+               (emit (reverse acc))
+               (if (null? (vector-ref byrow r))
+                 (go (+ r 1) acc)
+                 (let ((p (pick (vector-ref byrow r))))
+                   (go (+ r 1) (cons p acc))))))))
+      (go 0 ()))))
+
+; Deleting a transversal from a figure of constant width w leaves one of
+; constant width w-1.
+(defn (fig-remove f t)
+  (let ((acc (make-vector 1 ())))
+    (for-each (fig-squares f) (lambda (p)
+      (if (member-of? p t)
+        #inert
+        (vector-set! acc 0 (cons p (vector-ref acc 0))))))
+    (figure (fig-n f) (vector-ref acc 0))))
+
+(defn (peel f)
+  (let ((t (first-of (transversal f))))
+    (if (null? t) () (fig-remove f t))))
+
+; ---------------------------------------------------------------------------
+; 5. Reporting
+; ---------------------------------------------------------------------------
+
+(defn (describe name f)
+  (let ((t (fig-type f)))
+    (if (null? t)
+      (printf "  {0}: NOT of constant width\n" name)
+      (printf "  {0}: {1} squares on {2}x{2}, type ({2},{3},{4}){5}\n"
+              name (length (fig-squares f)) (car t) (cadr t) (car (cddr t))
+              (if (extended? f) ", extended" "")))))
+
+(defn (draw f)
+  (let ((n (fig-n f)) (s (fig-squares f)))
+    (letrec ((loop (lambda (x y)
+                     (if (eq? x n) #inert
+                       (if (eq? y n)
+                         (begin (print "\n") (loop (+ x 1) 0))
+                         (begin
+                           (print (if (member-of? (cons x y) s) "Q" "."))
+                           (loop x (+ y 1))))))))
+      (loop 0 0))))
+
+(defn (draw-squares n s) (draw (figure n s)))
+
+; ---------------------------------------------------------------------------
+; 6. Demonstration
+; ---------------------------------------------------------------------------
+
+(print "searching -- one solver, two strategies\n\n")
+
+(printf "  (8,8,1) queens        : {0} solutions\n"
+        (length (collect (figures 8 8 1))))
+(printf "  (6,6,1) queens        : {0} solutions\n"
+        (length (collect (figures 6 6 1))))
+(printf "  (4,4,2)               : {0} figure(s)\n"
+        (length (collect (figures 4 4 2))))
+(printf "  (5,4,2)               : {0} figure(s)\n"
+        (length (collect (figures 5 4 2))))
+(printf "  (6,6,2), all          : {0} figure(s)\n"
+        (length (collect (figures 6 6 2))))
+(printf "  (6,6,2), first only   : {0} squares\n"
+        (length (first-of (figures 6 6 2))))
+(print "\n")
+(draw-squares 5 (car (collect (figures 5 4 2))))
+
+(print "\nbuilding -- Lemma 1 and transversal deletion\n\n")
+
+; The paper's Figure 2 and Figure 3, the two smallest width 2 figures. Both
+; come straight out of the search above; Figure 3 is the one with the wrapping
+; diagonals, which is what makes the composition below legal.
+(define fig2 (figure 4 '((0 & 1) (0 & 2) (1 & 0) (1 & 3)
+                         (2 & 0) (2 & 3) (3 & 1) (3 & 2))))
+(define fig3 (figure 5 '((0 & 1) (0 & 3) (1 & 0) (1 & 4)
+                         (3 & 0) (3 & 4) (4 & 1) (4 & 3))))
+
+(describe "Figure 2" fig2)
+(describe "Figure 3" fig3)
+
+(define w4 (compose fig3 fig2))
+(define w3 (peel w4))
+(define w2 (peel w3))
+(define w1 (peel w2))
+
+(describe "fig3 . fig2" w4)
+(describe "  peeled once" w3)
+(describe "  peeled twice" w2)
+(describe "  peeled thrice" w1)
+
+(print "\n  constant width 3 on a 20x20 board (the paper's Figure 6):\n\n")
+(draw w3)
+
+; One more composition doubles the width again, and peeling that reaches the
+; widths in between. The paper reports that its authors never found a figure of
+; width 6 with a computer search; this one is built and checked in under a
+; second.
+(define w8 (compose fig3 w4))
+(define w7 (peel w8))
+(define w6 (peel w7))
+
+(print "\n")
+(describe "fig3 . (fig3 . fig2)" w8)
+(describe "  peeled once" w7)
+(describe "  peeled twice" w6)
+(print "\n")
diff --git a/Examples/constant-width.ikr b/Examples/constant-width.ikr
new file mode 100644
index 0000000..814d45d
--- /dev/null
+++ b/Examples/constant-width.ikr
@@ -0,0 +1,304 @@
+; Figures of constant width on a chessboard
+; =========================================
+;
+; A *figure* is any set of squares on an n x n board. It has *constant width w*
+; when every row, every column and every diagonal (slope +1 and slope -1) meets
+; it in either 0 or exactly w squares. A figure of constant width w occupying
+; k*w squares is said to be of type (n, k, w); k is then also its number of
+; non-empty rows. Figures of type (n, n, 1) are exactly the solutions of the
+; n-queens problem.
+;
+;   Janko Hernandez, Leonel Robert, "Figures of Constant Width on a Chessboard",
+;   American Mathematical Monthly 112 (2005) 42-50.
+;   https://userweb.ucs.louisiana.edu/~C00254569/hernandez-robert.pdf
+;
+; This program is an IronKernel transcription of the exhaustive backtracking
+; search described in
+;
+;   https://ademar.name/blog/2009/04/finding-figures-of-constant-wi.html
+;
+; It enumerates the *connected* figures of type (n, _, w). Two squares are
+; adjacent when they share a row, a column, or a main diagonal; a figure is
+; connected when every pair of its squares is joined by a chain of such steps.
+; Constant width 1 figures (the n-queens solutions) are totally disconnected,
+; so they are never reported.
+;
+; How the search works
+; --------------------
+; For each of the 2n + 2(2n-1) lines of the board we keep the number of squares
+; that still have to be placed on it: w for an untouched line, 0 for a saturated
+; one. Committing to a square decrements the four counters running through it.
+;
+; The frontier ("buffer") holds squares that are already committed but whose
+; local constraints have not been discharged yet. Popping a square p off the
+; frontier means choosing, right there, *every* square that still has to share a
+; line with p: exactly (cap-r p) more in its row, (cap-c p) in its column, and
+; likewise on both diagonals. Those choices join the frontier, and every other
+; square on p's four lines is permanently out of play -- which is what makes the
+; search converge instead of wandering the board.
+;
+; When the frontier drains, every committed square has all four of its lines
+; saturated, so the accumulated set is a figure of constant width w. It is
+; connected, because the frontier only ever grew along lines of squares already
+; in it.
+;
+; Running it
+; ----------
+;   dotnet run --project IronKernel -- Examples/constant-width.ikr          ; 5 4 2
+;   dotnet run --project IronKernel -- Examples/constant-width.ikr 4 4 2
+;   dotnet run --project IronKernel -- Examples/constant-width.ikr 6 6 2
+;   dotnet run --project IronKernel -- Examples/constant-width.ikr 11 10 3
+;
+; The arguments are  n k w : the board size, the width, and k as a pruning
+; bound. Give all three or none. k*w is not a filter on the output but a cutoff
+; on the search: a branch is abandoned as soon as it can no longer reach k*w
+; squares, yet a branch that survives still reports whatever figure it lands on,
+; which may be a smaller one. So every figure of type (n, k', w) with k' >= k is
+; guaranteed to be found, some figures below k appear as a bonus, and raising k
+; only makes the search faster. Each figure is printed with the type it really
+; has.
+;
+; The default 5 4 2 run finds five figures in about three seconds: the paper's
+; Figure 3, of type (5,4,2), plus the four placements of its Figure 2 -- the
+; unique connected figure of type (4,4,2) -- inside the 5x5 board.
+;
+;   args      time     figures found
+;   ------    ------   -----------------------------------------------
+;   4 4 2     0.4 s    1 x (4,4,2)          the paper's Figure 2
+;   5 4 2     3 s      5 x (5,4,2)          the default run
+;   6 6 2     16 s     2 x (6,6,2)
+;   6 4 2     28 s     15 x (6,4,2), 2 x (6,6,2)
+;   7 6 2     5.6 min  24 x (7,6,2), 4 x (7,4,2)
+;
+; These counts agree with an independent exhaustive row-by-row search. Width 3
+; is a different world: the smallest figure of constant width 3 lives on an
+; 11x11 board, and the original F# program needed some 31 days to exhaust
+; (11, _, 3), so treat that last command line as a long-running job rather than
+; a demo.
+;
+; The default `unrestricted` profile is required: the program prints through the
+; host console and parses its arguments with System.Int32.Parse.
+;
+; Hot paths below use nested `if` rather than `cond`, `and?` and `or?`. Those
+; three are compound operatives from the bootstrap library and cost an `eval`
+; per clause; `if` is a primitive. Avoiding them in the innermost loops makes
+; the whole search about three times faster.
+
+; ---------------------------------------------------------------------------
+; Small list helpers (the bootstrap library deliberately stays minimal)
+; ---------------------------------------------------------------------------
+
+(defn (append xs ys)
+  (if (null? xs) ys (cons (car xs) (append (cdr xs) ys))))
+
+(defn (>=? a b) (not? (< a b)))
+
+; ---------------------------------------------------------------------------
+; The search
+;
+;   n       board size
+;   w       the constant width
+;   k       pruning bound: branches that can no longer reach k*w squares are cut
+;   report  applied to every figure found, as a list of (x . y) squares
+; ---------------------------------------------------------------------------
+
+(defn (find-figures n k w report)
+
+  ; Remaining capacity of every line. Rows and columns are indexed by
+  ; coordinate; the diagonal of slope -1 through (x, y) is indexed by x + y and
+  ; the one of slope +1 by n + (x - y) - 1, so both fit in 2n-1 slots.
+  (define rows    (make-vector n w))
+  (define columns (make-vector n w))
+  (define diag1   (make-vector (- (* 2 n) 1) w))
+  (define diag2   (make-vector (- (* 2 n) 1) w))
+
+  (defn (pdiag p) (+ (car p) (cdr p)))
+  (defn (ndiag p) (- (+ n (- (car p) (cdr p))) 1))
+
+  (defn (cap-r  p) (vector-ref rows    (car p)))
+  (defn (cap-c  p) (vector-ref columns (cdr p)))
+  (defn (cap-pd p) (vector-ref diag1   (pdiag p)))
+  (defn (cap-nd p) (vector-ref diag2   (ndiag p)))
+
+  ; Add d to each of the four counters running through p.
+  (defn (alter! p d)
+    (let ((r (car p)) (c (cdr p)) (i1 (pdiag p)) (i2 (ndiag p)))
+      (vector-set! rows    r  (+ (vector-ref rows    r)  d))
+      (vector-set! columns c  (+ (vector-ref columns c)  d))
+      (vector-set! diag1   i1 (+ (vector-ref diag1   i1) d))
+      (vector-set! diag2   i2 (+ (vector-ref diag2   i2) d))
+      #inert))
+
+  (defn (take!    p) (alter! p -1))
+  (defn (restore! p) (alter! p  1))
+
+  ; A square becomes unusable as soon as any one of its four lines is full.
+  (defn (open? p)
+    (if (zero? (cap-r  p)) #f
+      (if (zero? (cap-c  p)) #f
+        (if (zero? (cap-pd p)) #f
+          (if (zero? (cap-nd p)) #f #t)))))
+
+  ; The board minus the corner regions, whose diagonals are shorter than w and
+  ; so can never carry a full width.
+  (defn (playable-board)
+    (let ((lo (- w 1)) (hi (- (- (* 2 n) w) 1)))
+      (letrec
+        ((keep? (lambda (p)
+                  (and? (<= lo (pdiag p)) (<= (pdiag p) hi)
+                        (<= lo (ndiag p)) (<= (ndiag p) hi))))
+         ; built back to front, so the result comes out in row-major order
+         (loop (lambda (x y acc)
+                 (cond ((< x 0) acc)
+                       ((< y 0) (loop (- x 1) (- n 1) acc))
+                       (#t (let ((p (cons x y)))
+                             (loop x (- y 1)
+                                   (if (keep? p) (cons p acc) acc))))))))
+        (loop (- n 1) (- n 1) ()))))
+
+  ; Split the candidate squares by how they see q: same row, same column, same
+  ; diagonal of slope -1, same diagonal of slope +1, or unrelated. Two distinct
+  ; squares share at most one of the four lines, so the tests are disjoint.
+  ; Returns (r rws c cls d1 dg1 d2 dg2 rest), each count beside its list.
+  (defn (collect q avail)
+    (let ((qx (car q)) (qy (cdr q)) (qp (pdiag q)) (qn (- (car q) (cdr q))))
+      (letrec
+        ((loop
+           (lambda (av r rws c cls d1 dg1 d2 dg2 rest)
+             (if (null? av)
+               (list r rws c cls d1 dg1 d2 dg2 rest)
+               (let* ((p (car av)) (tail (cdr av))
+                      (x (car p)) (y (cdr p)))
+                 (if (eq? x qx)
+                   (loop tail (+ r 1) (cons p rws) c cls d1 dg1 d2 dg2 rest)
+                 (if (eq? y qy)
+                   (loop tail r rws (+ c 1) (cons p cls) d1 dg1 d2 dg2 rest)
+                 (if (eq? (+ x y) qp)
+                   (loop tail r rws c cls (+ d1 1) (cons p dg1) d2 dg2 rest)
+                 (if (eq? (- x y) qn)
+                   (loop tail r rws c cls d1 dg1 (+ d2 1) (cons p dg2) rest)
+                   (loop tail r rws c cls d1 dg1 d2 dg2 (cons p rest)))))))))))
+        (loop avail 0 () 0 () 0 () 0 () ()))))
+
+  ; Drop the squares that have gone dead, and count what is left.
+  (defn (count-open avail)
+    (letrec
+      ((loop (lambda (av len kept)
+               (if (null? av)
+                 (list len kept)
+                 (if (open? (car av))
+                   (loop (cdr av) (+ len 1) (cons (car av) kept))
+                   (loop (cdr av) len kept))))))
+      (loop avail 0 ())))
+
+  ; Commit to exactly m of the still-open squares of `avail`, in every possible
+  ; way, appending each choice to the frontier before invoking k*. Every square
+  ; is restored on the way out, so the counters are unchanged on return.
+  (defn (choose avail m bufflen buff k*)
+    (letrec
+      ((loop (lambda (av chosen j)
+               (if (zero? j)
+                 (k* (+ bufflen m) (append buff chosen))
+                 (if (null? av)
+                   #inert
+                   (let ((p (car av)) (tail (cdr av)))
+                     (if (open? p)
+                       (begin (take! p)
+                              (loop tail (cons p chosen) (- j 1))
+                              (restore! p))
+                       #inert)
+                     (loop tail chosen j)))))))
+      (loop avail () m)))
+
+  ;   sol     squares whose constraints are already discharged
+  ;   len     how many more squares this branch still has to reach
+  ;   avail   candidate squares, avlen of them
+  ;   buff    committed squares awaiting their turn, bufflen of them
+  (defn (search sol len avlen avail bufflen buff)
+    (if (< (+ avlen bufflen) len)
+      #inert                                      ; too few squares left
+      (if (null? buff)
+        (report sol)                              ; frontier drained: a figure
+        (let* ((p (car buff)) (tail (cdr buff)))
+          (let (((r rws c cls d1 dg1 d2 dg2 rest) (collect p avail))
+                ; The capacities are read before any of the four groups is
+                ; touched. No square lies on two of p's lines, so choosing
+                ; within one group cannot disturb the other three counters.
+                (need-r  (cap-r  p)) (need-c  (cap-c  p))
+                (need-pd (cap-pd p)) (need-nd (cap-nd p)))
+            ; not enough candidates left on one of p's lines to fill it
+            (if (if (< r need-r) #t
+                  (if (< c need-c) #t
+                    (if (< d1 need-pd) #t (< d2 need-nd))))
+              #inert
+              (choose rws need-r (- bufflen 1) tail
+                (lambda (b1 buf1)
+                  (choose cls need-c b1 buf1
+                    (lambda (b2 buf2)
+                      (choose dg1 need-pd b2 buf2
+                        (lambda (b3 buf3)
+                          (choose dg2 need-nd b3 buf3
+                            (lambda (b4 buf4)
+                              (let (((avlen* avail*) (count-open rest)))
+                                (search (cons p sol) (- len 1)
+                                        avlen* avail* b4 buf4))))))))))))))))
+
+  ; Seed the search at every square in turn. Each figure is found exactly once,
+  ; from its first square in row-major order: a seed only ever sees the squares
+  ; that follow it.
+  (letrec
+    ((loop (lambda (l avlen)
+             (if (null? l)
+               #inert
+               (let ((p (car l)) (tail (cdr l)))
+                 (take! p)
+                 (search () (* k w) (- avlen 1) tail 1 (list p))
+                 (restore! p)
+                 (loop tail (- avlen 1)))))))
+    (let (((len board) (count-open (playable-board))))
+      (loop board len))))
+
+; ---------------------------------------------------------------------------
+; Reporting
+; ---------------------------------------------------------------------------
+
+(defn (occupied? p sol)
+  (cond ((null? sol) #f)
+        ((and? (eq? (car p) (car (car sol)))
+               (eq? (cdr p) (cdr (car sol)))) #t)
+        (#t (occupied? p (cdr sol)))))
+
+(defn (draw n sol)
+  (letrec ((loop (lambda (x y)
+                   (cond ((>=? x n) #inert)
+                         ((>=? y n) (print "\n") (loop (+ x 1) 0))
+                         (#t (print (if (occupied? (cons x y) sol) "Q " ". "))
+                             (loop x (+ y 1)))))))
+    (loop 0 0)))
+
+(defn (report-figures n k w)
+  (let ((found (make-vector 1 0)))
+    (printf "connected figures of constant width {0} on a {1}x{1} board\n" w n)
+    (printf "(pruning branches that cannot reach {0} squares)\n\n" (* k w))
+    (find-figures n k w
+      (lambda (sol)
+        (vector-set! found 0 (+ (vector-ref found 0) 1))
+        (printf "#{0}: type ({1}, {2}, {3})\n"
+                (vector-ref found 0) n (/ (length sol) w) w)
+        (draw n sol)
+        (print "\n")))
+    (printf "{0} figure(s)\n" (vector-ref found 0))))
+
+; ---------------------------------------------------------------------------
+; Entry point
+; ---------------------------------------------------------------------------
+
+(defn (arg i default)
+  (letrec ((nth (lambda (xs j)
+                  (cond ((null? xs) default)
+                        ((zero? j) (. System.Int32 Parse (car xs)))
+                        (#t (nth (cdr xs) (- j 1)))))))
+    (nth args i)))
+
+(let ((n (arg 0 5)) (k (arg 1 4)) (w (arg 2 2)))
+  (time (report-figures n k w)))
diff --git a/README.md b/README.md
index a0cd69b..edc6100 100644
--- a/README.md
+++ b/README.md
@@ -107,6 +107,15 @@ Public packages use NuGet.org initially. See
 [`ADR 0001`](docs/adr/0001-source-project-and-package-conventions.md) for the
 extension and ecosystem decision.
 
+### Libraries in this repository
+
+[`lib/`](lib/) holds first-party IronKernel packages, each an ordinary
+`.ikproj` built with `ik test` / `ik pack`.
+
+| Package | Provides |
+|---|---|
+| [`IronKernel.Amb`](lib/IronKernel.Amb/) | Nondeterministic search: `amb`, `require`, bracketed choice, and pluggable search strategies over multi-shot delimited continuations |
+
 ## REPL
 
 ```bash
diff --git a/lib/IronKernel.Amb/.gitignore b/lib/IronKernel.Amb/.gitignore
new file mode 100644
index 0000000..b262931
--- /dev/null
+++ b/lib/IronKernel.Amb/.gitignore
@@ -0,0 +1,3 @@
+bin/
+obj/
+*.ikc
diff --git a/lib/IronKernel.Amb/IronKernel.Amb.ikproj b/lib/IronKernel.Amb/IronKernel.Amb.ikproj
new file mode 100644
index 0000000..de85efe
--- /dev/null
+++ b/lib/IronKernel.Amb/IronKernel.Amb.ikproj
@@ -0,0 +1,18 @@
+<Project Sdk="Microsoft.NET.Sdk">
+  <PropertyGroup>
+    <TargetFramework>net10.0</TargetFramework>
+    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
+    <RestorePackagesWithLockFile>true</RestorePackagesWithLockFile>
+    <PackageId>IronKernel.Amb</PackageId>
+    <Version>0.1.0</Version>
+    <Authors>IronKernel</Authors>
+    <Description>Nondeterministic search for IronKernel: amb, require, and pluggable search strategies built on multi-shot delimited continuations.</Description>
+    <PackageTags>ironkernel</PackageTags>
+    <IronKernelMain>src/amb.ikr</IronKernelMain>
+    <IronKernelProfile>unrestricted</IronKernelProfile>
+  </PropertyGroup>
+  <ItemGroup>
+    <IronKernelSource Include="src/**/*.ikr" />
+    <IronKernelTest Include="test/**/*.ikr" />
+  </ItemGroup>
+</Project>
diff --git a/lib/IronKernel.Amb/README.md b/lib/IronKernel.Amb/README.md
new file mode 100644
index 0000000..49aba5f
--- /dev/null
+++ b/lib/IronKernel.Amb/README.md
@@ -0,0 +1,96 @@
+# IronKernel.Amb
+
+Nondeterministic search for IronKernel. Choice points are ordinary
+expressions, the search strategy is a value, and the code doing the searching
+never mentions a continuation.
+
+```scheme
+(collect
+  (let ((a (amb (list 1 2))))
+    (let ((b (amb (list 10 20))))
+      (emit (cons a b)))))
+; => ((1 . 10) (1 . 20) (2 . 10) (2 . 20))
+```
+
+Built on IronKernel's `shift`/`reset`, which are multi-shot and re-delimit when
+resumed — so a choice point can invoke its captured continuation once per
+alternative.
+
+## Use
+
+```bash
+ik add IronKernel.Amb 0.1.0
+```
+
+Or, from a checkout of this repository:
+
+```bash
+cd lib/IronKernel.Amb
+ik test
+ik pack
+```
+
+## API
+
+### Choice points
+
+| Form | Meaning |
+|---|---|
+| `(amb xs)` | Yield each element of `xs`. An empty list fails. |
+| `(amb-range lo hi)` | Yield each integer in `[lo, hi)` without building a list. |
+| `(require test)` | Continue only if `test` holds, otherwise fail. |
+| `(fail)` | Abandon the current branch. |
+| `(amb-bracket xs ok? enter! leave!)` | Yield each `x` satisfying `ok?`, with `enter!` applied before the continuation runs and `leave!` after it finishes. |
+| `(amb-bracket-range lo hi ok? enter! leave!)` | The same over `[lo, hi)`. |
+
+### Reporting
+
+| Form | Meaning |
+|---|---|
+| `(emit s)` | Report a solution. A no-op outside any strategy. |
+
+### Strategies
+
+Operatives. Each installs a delimiter, runs the body, and restores the
+previous handler.
+
+| Form | Returns |
+|---|---|
+| `(collect body …)` | List of every solution, in the order found. |
+| `(first-of body …)` | The first solution, or `()`. Escapes through `call/cc`, so the rest of the tree is never explored. |
+| `(count-of body …)` | How many solutions, retaining none of them. |
+| `(search handler body …)` | `#inert`; applies `handler` to each solution. Use for strategies of your own. |
+
+## Mutable state and backtracking
+
+A search that mutates a board or a set of used lines has to undo that mutation
+when a branch is abandoned, and doing it at the call site does not work: by the
+time a choice expression returns, the rest of the search has already run inside
+the continuation. The undo belongs to the choice point, which is what
+`amb-bracket` is for.
+
+```scheme
+(let ((y (amb-bracket-range 0 n
+           (lambda (c) (free? x c))        ; guard
+           (lambda (c) (mark! x c 1))      ; before the continuation runs
+           (lambda (c) (mark! x c -1)))))  ; after it has been exhausted
+  (place-queen (+ x 1)))
+```
+
+State stays consistent with the caller's view of it, and the caller still never
+sees a continuation. `test/amb_test.ikr` builds n-queens this way in about
+twenty lines.
+
+## Notes
+
+- Strategies nest: an inner search runs to completion inside one branch of an
+  outer one.
+- The library performs no host I/O.
+- `amb` and friends must run inside a strategy — that is what installs the
+  `reset` their `shift` needs.
+
+## Origin
+
+Extracted from [`Examples/constant-width-amb.ikr`](../../Examples/constant-width-amb.ikr),
+which enumerates figures of constant width on a chessboard and, as the width-1
+case, solves the n-queens problem.
diff --git a/lib/IronKernel.Amb/src/amb.ikr b/lib/IronKernel.Amb/src/amb.ikr
new file mode 100644
index 0000000..9689d71
--- /dev/null
+++ b/lib/IronKernel.Amb/src/amb.ikr
@@ -0,0 +1,163 @@
+; IronKernel.Amb -- nondeterministic search as a library
+; ======================================================
+;
+; Backtracking, expressed so that the code doing the searching never mentions
+; a continuation. IronKernel's `shift`/`reset` are multi-shot and re-delimit
+; when resumed, so a choice point can simply invoke its captured continuation
+; once per alternative:
+;
+;   (collect
+;     (let ((a (amb (list 1 2))))
+;       (let ((b (amb (list 10 20))))
+;         (emit (cons a b)))))
+;   ; => ((1 . 10) (1 . 20) (2 . 10) (2 . 20))
+;
+; Two ideas carry the library.
+;
+; Choice points are ordinary expressions. `amb` returns each element of a
+; list, `amb-range` each integer of a half-open interval, and `require` prunes
+; the current branch. Search code reads as if it were straight-line code that
+; happens to be run once per candidate.
+;
+; The strategy is a value. Nondeterministic code only ever calls `emit`; what
+; that means is decided by the operative wrapping it. `collect` gathers every
+; solution, `first-of` escapes with the first, `count-of` tallies without
+; retaining anything, and `search` takes an arbitrary handler so you can add
+; your own. The searcher does not change when the strategy does.
+;
+; Mutable state and backtracking
+; ------------------------------
+; A search that mutates a board, a counter or a set of used lines has to undo
+; that mutation when a branch is abandoned. Doing it at the call site does not
+; work: by the time a choice expression returns, the rest of the search has
+; already run inside the continuation. The undo belongs to the choice point,
+; which is what `amb-bracket` provides -- it enters a candidate, hands it to
+; the continuation, and leaves it only once that continuation has run to
+; exhaustion:
+;
+;   (let ((c (amb-bracket-range 0 n free? place! unplace!)))
+;     (place-rest (+ c 1)))
+;
+; State is therefore always consistent with the caller's view of it, and the
+; caller still never sees a continuation.
+;
+; Notes
+; -----
+; * `emit` outside any strategy is a no-op, so a nondeterministic procedure is
+;   safe to call anywhere.
+; * Strategies nest. Each installs its own delimiter, so an inner search runs
+;   to completion inside one branch of an outer one, and restores the previous
+;   handler when it is done.
+; * Nothing here performs host I/O.
+
+(provide! (fail require amb amb-range amb-bracket amb-bracket-range
+           emit search collect first-of count-of)
+
+  ; --- private ------------------------------------------------------------
+
+  (define list-reverse
+    (lambda (xs)
+      (letrec ((loop (lambda (l acc)
+                       (if (null? l) acc (loop (cdr l) (cons (car l) acc))))))
+        (loop xs ()))))
+
+  ; The handler in force. Held in a vector so that the strategy operatives can
+  ; swap it dynamically and put it back afterwards.
+  (define sink (make-vector 1 (lambda (s) #inert)))
+
+  (define with-sink
+    (lambda (handler thunk)
+      (let ((saved (vector-ref sink 0)))
+        (vector-set! sink 0 handler)
+        (reset (thunk))
+        (vector-set! sink 0 saved))))
+
+  ; --- choice points ------------------------------------------------------
+
+  ; Abandon this branch: capture the continuation up to the delimiter and drop
+  ; it, returning control to the most recent choice point.
+  (define fail (lambda () (shift (lambda (k) #inert))))
+
+  ; Keep going only if the test holds.
+  (define require (lambda (test) (if test #inert (fail))))
+
+  ; Yield each element of xs. An empty list fails.
+  (define amb (lambda (xs) (shift (lambda (k) (for-each xs k)))))
+
+  ; Yield each integer in [lo, hi) without building the list.
+  (define amb-range
+    (lambda (lo hi)
+      (shift (lambda (k)
+        (letrec ((loop (lambda (i)
+                         (if (< i hi) (begin (k i) (loop (+ i 1))) #inert))))
+          (loop lo))))))
+
+  ; Yield each x of xs satisfying ok?, with enter! applied before the
+  ; continuation runs and leave! after it has finished exploring. Use this
+  ; whenever a candidate has to be recorded in mutable state.
+  (define amb-bracket
+    (lambda (xs ok? enter! leave!)
+      (shift (lambda (k)
+        (for-each xs (lambda (x)
+          (if (ok? x)
+            (begin (enter! x) (k x) (leave! x))
+            #inert)))))))
+
+  ; amb-bracket over the integers in [lo, hi).
+  (define amb-bracket-range
+    (lambda (lo hi ok? enter! leave!)
+      (shift (lambda (k)
+        (letrec ((loop (lambda (i)
+                         (if (< i hi)
+                           (begin
+                             (if (ok? i)
+                               (begin (enter! i) (k i) (leave! i))
+                               #inert)
+                             (loop (+ i 1)))
+                           #inert))))
+          (loop lo))))))
+
+  ; --- reporting a solution ------------------------------------------------
+
+  (define emit (lambda (s) ((vector-ref sink 0) s)))
+
+  ; --- strategies ----------------------------------------------------------
+
+  ; Run body with an arbitrary handler applied to every solution.
+  (define search
+    (vau (handler & body) env
+      (with-sink (eval env handler)
+                 (lambda () (eval env (cons sequence body))))
+      #inert))
+
+  ; Every solution, in the order found.
+  (define collect
+    (vau body env
+      (let ((acc (make-vector 1 ())))
+        (with-sink
+          (lambda (s) (vector-set! acc 0 (cons s (vector-ref acc 0))))
+          (lambda () (eval env (cons sequence body))))
+        (list-reverse (vector-ref acc 0)))))
+
+  ; How many solutions, retaining none of them.
+  (define count-of
+    (vau body env
+      (let ((n (make-vector 1 0)))
+        (with-sink
+          (lambda (s) (vector-set! n 0 (+ (vector-ref n 0) 1)))
+          (lambda () (eval env (cons sequence body))))
+        (vector-ref n 0))))
+
+  ; The first solution, or () if there is none. Escapes through call/cc, so
+  ; the rest of the search tree is never explored. The handler is restored on
+  ; both paths.
+  (define first-of
+    (vau body env
+      (let ((saved (vector-ref sink 0)))
+        (let ((found
+                (call/cc (lambda (return)
+                           (vector-set! sink 0 (lambda (s) (return s)))
+                           (reset (eval env (cons sequence body)))
+                           ()))))
+          (vector-set! sink 0 saved)
+          found)))))
diff --git a/lib/IronKernel.Amb/test/amb_test.ikr b/lib/IronKernel.Amb/test/amb_test.ikr
new file mode 100644
index 0000000..18d510a
--- /dev/null
+++ b/lib/IronKernel.Amb/test/amb_test.ikr
@@ -0,0 +1,153 @@
+; Tests for IronKernel.Amb.
+;
+; `ik test` loads src/ then this file, and counts the file as failing if
+; evaluating it raises. Failures are tallied so that every check runs, then the
+; last form references an unbound name to fail the run and point at the tally.
+
+(define failures (make-vector 1 0))
+
+(defn (check name ok)
+  (if ok
+    (printf "  ok    {0}\n" name)
+    (begin
+      (printf "  FAIL  {0}\n" name)
+      (vector-set! failures 0 (+ (vector-ref failures 0) 1)))))
+
+(defn (list-equal? xs ys)
+  (if (null? xs)
+    (null? ys)
+    (if (null? ys) #f
+      (if (eq? (car xs) (car ys)) (list-equal? (cdr xs) (cdr ys)) #f))))
+
+; --- choice points ----------------------------------------------------------
+
+(check "amb enumerates a list"
+  (list-equal? (collect (emit (amb (list 1 2 3)))) (list 1 2 3)))
+
+(check "amb over () fails"
+  (null? (collect (emit (amb ())))))
+
+(check "nested amb takes the cross product"
+  (eq? 4 (length (collect (let ((a (amb (list 1 2))))
+                            (let ((b (amb (list 10 20))))
+                              (emit (cons a b))))))))
+
+(check "amb-range enumerates a half-open interval"
+  (list-equal? (collect (emit (amb-range 2 5))) (list 2 3 4)))
+
+(check "require prunes a branch"
+  (list-equal? (collect (let ((a (amb-range 0 10)))
+                          (require (< a 3))
+                          (emit a)))
+               (list 0 1 2)))
+
+(check "fail abandons a branch"
+  (list-equal? (collect (let ((a (amb (list 1 2 3))))
+                          (if (eq? a 2) (fail) #inert)
+                          (emit a)))
+               (list 1 3)))
+
+; --- strategies -------------------------------------------------------------
+
+(check "count-of tallies solutions"
+  (eq? 4 (count-of (emit (amb-range 0 4)))))
+
+(check "first-of returns the first solution"
+  (eq? 6 (first-of (let ((a (amb (list 5 6 7))))
+                     (require (> a 5))
+                     (emit a)))))
+
+(check "first-of returns () when there is none"
+  (null? (first-of (let ((a (amb (list 1 2)))) (fail) (emit a)))))
+
+(check "search accepts a custom handler"
+  (let ((total (make-vector 1 0)))
+    (search (lambda (s) (vector-set! total 0 (+ (vector-ref total 0) s)))
+      (emit (amb-range 1 5)))
+    (eq? 10 (vector-ref total 0))))
+
+(check "emit outside a strategy is a no-op"
+  (begin (emit 'ignored) #t))
+
+(check "strategies nest"
+  (list-equal? (collect (let ((a (amb-range 0 3)))
+                          (emit (count-of (emit (amb-range 0 a))))))
+               (list 0 1 2)))
+
+; --- bracketed choice -------------------------------------------------------
+
+(define st (make-vector 1 0))
+
+(defn (bump v) (vector-set! st 0 (+ (vector-ref st 0) v)))
+(defn (drop v) (vector-set! st 0 (- (vector-ref st 0) v)))
+
+(check "amb-bracket exposes state to the continuation"
+  (list-equal? (collect (let ((x (amb-bracket (list 1 2 3)
+                                              (lambda (v) #t) bump drop)))
+                          (emit (vector-ref st 0))))
+               (list 1 2 3)))
+
+(check "amb-bracket restores state afterwards"
+  (zero? (vector-ref st 0)))
+
+(check "amb-bracket honours its guard"
+  (list-equal? (collect (let ((x (amb-bracket (list 1 2 3 4)
+                                              (lambda (v) (< v 3)) bump drop)))
+                          (emit x)))
+               (list 1 2)))
+
+(check "amb-bracket-range brackets nested choices"
+  (let ((seen (collect (let ((a (amb-bracket-range 1 4
+                                  (lambda (v) #t) bump drop)))
+                         (let ((b (amb-bracket-range 1 4
+                                    (lambda (v) (> v a)) bump drop)))
+                           (emit (vector-ref st 0)))))))
+    ; a+b over 1<=a<b<=3: 1+2, 1+3, 2+3
+    (if (list-equal? seen (list 3 4 5)) (zero? (vector-ref st 0)) #f)))
+
+; --- integration: n-queens --------------------------------------------------
+;
+; Constant width 1 in the sense of Examples/constant-width-amb.ikr: one queen
+; per row, no two sharing a column or a diagonal.
+
+(defn (queens n)
+  (let ((col (make-vector n 0))
+        (d1 (make-vector (- (* 2 n) 1) 0))
+        (d2 (make-vector (- (* 2 n) 1) 0))
+        (acc (make-vector 1 ())))
+    (letrec
+      ((i1 (lambda (x y) (+ x y)))
+       (i2 (lambda (x y) (- (+ n (- x y)) 1)))
+       (free? (lambda (x y)
+                (if (zero? (vector-ref col y))
+                  (if (zero? (vector-ref d1 (i1 x y)))
+                    (zero? (vector-ref d2 (i2 x y)))
+                    #f)
+                  #f)))
+       (mark! (lambda (x y d)
+                (vector-set! col y (+ (vector-ref col y) d))
+                (vector-set! d1 (i1 x y) (+ (vector-ref d1 (i1 x y)) d))
+                (vector-set! d2 (i2 x y) (+ (vector-ref d2 (i2 x y)) d))))
+       (enter! (lambda (x) (lambda (y)
+                 (mark! x y 1)
+                 (vector-set! acc 0 (cons y (vector-ref acc 0))))))
+       (leave! (lambda (x) (lambda (y)
+                 (mark! x y -1)
+                 (vector-set! acc 0 (cdr (vector-ref acc 0))))))
+       (go (lambda (x)
+             (if (eq? x n)
+               (emit (vector-ref acc 0))
+               (let ((y (amb-bracket-range 0 n
+                          (lambda (c) (free? x c))
+                          (enter! x)
+                          (leave! x))))
+                 (go (+ x 1)))))))
+      (go 0))))
+
+(check "6-queens has 4 solutions"  (eq? 4  (count-of (queens 6))))
+(check "5-queens has 10 solutions" (eq? 10 (count-of (queens 5))))
+(check "queens leaves no state behind"
+  (eq? 6 (length (first-of (queens 6)))))
+
+(printf "\n{0} failure(s)\n" (vector-ref failures 0))
+(if (zero? (vector-ref failures 0)) #inert (amb-tests-failed))