fix(graph): fvc_search self-protects its FVC_MAX_VERTICES stack buffers (RG-2 #2)

docs/spec/changelog/2026-08-31.md

@@ -1,5 +1,19 @@
 # Changelog: week of 2026-08-31 (Mon) – 2026-09-06 (Sun)
 
+## FindVertexColoring — exported search self-protects its stack buffers (RG-2 #2)
+
+`fvc_search` (exported in `src/graph/graph.h`) drives a branch-and-bound whose
+inner `fvc_bb` uses stack arrays `seen[]`/`forbid[]` sized to `FVC_MAX_VERTICES`
+(128). The 128-vertex cap was enforced only in the head
+`builtin_find_vertex_coloring`, not in `fvc_search` — and because the symbol is
+exported while `FVC_MAX_VERTICES` is not, a cross-TU caller passing a larger
+graph could not discover the precondition and would overflow those buffers.
+`fvc_search` now refuses (`return 0`) when `n > FVC_MAX_VERTICES`, putting the
+invariant with the buffers it protects. No behaviour change on the head path,
+which already filters `n > 128`. Closes the RG-2 adversarial finding #2.
+Regression: a direct `fvc_search` on `CompleteGraph[129]` must return 0 with
+zero steps (`test_vertex_coloring_internals`, `tests/test_graph.c`).
+
 ## Build — `USE_MPFR=0` / `USE_LAPACK=0` config compiles cleanly again
 
 The `build-no-mpfr` CI job (`make USE_MPFR=0 USE_FLINT=0 USE_ECM=0 USE_LAPACK=0

src/graph/vertexcoloring.c

@@ -317,7 +317,11 @@ static void fvc_bb(FvcBB* s, int ncoloured, int used) {
 int fvc_search(const GraphAdj* a, int* colour, long* steps_out) {
     int n = a->n;
     if (steps_out) *steps_out = 0;
-    if (n <= 0) return 0;
+    /* Self-protect: fvc_bb's seen[]/forbid[] are stack arrays sized to the cap
+     * (FVC_MAX_VERTICES + 2). The head enforces the cap before calling in, but
+     * this symbol is exported (graph.h) and FVC_MAX_VERTICES is not, so a
+     * cross-TU caller cannot see the precondition -- enforce it here too. */
+    if (n <= 0 || n > FVC_MAX_VERTICES) return 0;
 
     int ub = fvc_dsatur_bound(a, colour);
     if (ub <= 0) return 0;                  /* allocation failure inside DSATUR */

tests/test_graph.c

@@ -418,6 +418,23 @@ static void test_vertex_coloring_internals(void) {
         ASSERT_MSG(ub >= 3, "DSATUR on C5 cannot beat chi = 3");
         free(c); graph_adj_free(a); expr_free(g);
     }
+
+    /* Exported-symbol precondition (RG-2 adversarial finding #2). fvc_bb's
+     * seen[]/forbid[] are stack arrays sized to FVC_MAX_VERTICES, and the cap is
+     * enforced in the head -- not in fvc_search, which graph.h exports. A direct
+     * caller passing n > cap must be refused (0), never overflow the buffers.
+     * CompleteGraph[129] is one vertex over the cap and drives exactly that. */
+    {
+        Expr* g = evaluate(parse_expression("CompleteGraph[129]"));
+        GraphAdj* a = graph_build_adj(g);
+        ASSERT(a != NULL && a->n == 129);
+        int* c = calloc((size_t)a->n, sizeof(int));
+        steps = 999;
+        ASSERT_MSG(fvc_search(a, c, &steps) == 0,
+                    "fvc_search must refuse n > FVC_MAX_VERTICES, not overflow");
+        ASSERT_MSG(steps == 0, "a cap-refused search reports zero steps");
+        free(c); graph_adj_free(a); expr_free(g);
+    }
 }
 
 /* ---- FindVertexColoring: the registered head (AC-1 .. AC-18) --------------