From 2efa23040a7a92f0fc1ff8413586104ed1c3814d Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Mon, 2 Nov 2026 16:53:26 +0000
Subject: [PATCH] fix(solver): validate fence constraint indices

---
 check.ml  | 14 ++++++++++++++
 solver.ml |  3 +++
 2 files changed, 17 insertions(+)

diff --git a/check.ml b/check.ml
index 9571596022e1f1ce7bcfcb5dd9a6a7d6a68cc7f5..99f34f734d9ac3744323d6eb0407146b34482db1 100644
--- a/check.ml
+++ b/check.ml
@@ -148,6 +148,19 @@ let graph () =
   Printf.printf "unfenced graph closed: %d states, %d edges, %d violating states\n%!"
     (Array.length graph.states) graph.edges (List.length graph.violations)
 
+let constraints () =
+  List.iter (fun (count, clauses) ->
+    rejects (fun () -> ignore (Solver.candidate ~count ~budget:1 clauses))
+      "invalid fence constraint")
+    [-1, []; 1, [[-1]]; 1, [[1]]; 0, [[0]]];
+  let solve count budget clauses = Solver.solve (Solver.candidate ~count ~budget clauses) in
+  require (solve 0 0 [] = Solver.Sat []) "empty candidate set satisfies zero budget";
+  require (solve 0 (-1) [] = Solver.Unsat) "negative lower budget remains unsatisfiable";
+  require (solve 2 0 [[0; 1]] = Solver.Unsat) "zero budget cannot hit a nonempty clause";
+  require (solve 2 1 [[0]; [1]] = Solver.Unsat) "independent singleton clauses require two fences";
+  require (solve 2 2 [[0]; [1]] = Solver.Sat [Solver.Truth true; Solver.Truth true])
+    "candidate values follow clause indices"
+
 let validation () =
   let case = read "buffering" in
   let open Sexp in
@@ -207,6 +220,7 @@ let () =
   buffers ();
   outcomes ();
   graph ();
+  constraints ();
   validation ();
   repair folder;
   Printf.printf "%d checks passed; %d bounded reference states; %.1fs\n%!"
diff --git a/solver.ml b/solver.ml
index 4a43cc6fed21a3974800e17163faa2d84205308c..f4eba6c7159852e3976b905ac3574e2be7b78226 100644
--- a/solver.ml
+++ b/solver.ml
@@ -204,6 +204,9 @@ let compile ?(timeout=300000) ?fixed ?(require_goal=true) ?(blocks=[]) case mode
   {source = Buffer.contents buffer; probes}
 
 let candidate ~count ~budget clauses =
+  if count < 0 then invalid_arg "negative fence candidate count";
+  List.iter (List.iter (fun index ->
+    if index < 0 || index >= count then invalid_arg "fence constraint index outside candidates")) clauses;
   let lines = ref [Store.read (Filename.concat (Store.root ()) "smt/fences.smt2")] in
   let add line = lines := line :: !lines in
   for i = 0 to count - 1 do add (Printf.sprintf "(declare-const f%d Bool)" i) done;