Generalize Peterson invariant to N threads and add DSL local arrays

src/main/java/dev/samhb/interleave/core/PetersonState.java

@@ -59,6 +59,15 @@ public boolean flag(int threadId) {
         return flag[threadId];
     }
 
+    /**
+     * Returns the number of threads modeled by this state.
+     *
+     * @return thread count
+     */
+    public int threadCount() {
+        return flag.length;
+    }
+
     /**
      * Updates flag in this mutable modeled state.
      * @param threadId zero-based modeled thread ID

src/main/java/dev/samhb/interleave/format/ProgramLoader.java

@@ -274,11 +274,28 @@ private BenchmarkProgram load(ProgramDefinition def) {
             String invariantType = def.invariant().get("type").getAsString();
             invariantRegistry.validateCompatibility(invariantType, def.state().get("type").getAsString());
 
-            // mutual_exclusion_peterson requires exactly two threads
-            if ("mutual_exclusion_peterson".equals(invariantType) && threadDefs.size() != 2) {
-                throw new RegistryException(
-                    "Invariant 'mutual_exclusion_peterson' requires exactly two threads"
-                );
+            // mutual_exclusion_peterson requires at least two threads
+            if ("mutual_exclusion_peterson".equals(invariantType)) {
+                if (threadDefs.size() < 2) {
+                    throw new RegistryException(
+                        "Invariant 'mutual_exclusion_peterson' requires at least two threads"
+                    );
+                }
+                JsonObject invJson = def.invariant();
+                if (invJson.has("cs_pcs")) {
+                    if (invJson.get("cs_pcs").isJsonArray()) {
+                        int csPcsLen = invJson.getAsJsonArray("cs_pcs").size();
+                        if (csPcsLen != threadDefs.size()) {
+                            throw new RegistryException(
+                                "Invariant 'cs_pcs' length (" + csPcsLen + ") must match thread count (" + threadDefs.size() + ")"
+                            );
+                        }
+                    }
+                } else if (threadDefs.size() != 2) {
+                    throw new RegistryException(
+                        "Invariant 'mutual_exclusion_peterson' requires two threads when using thread0_cs_pc/thread1_cs_pc; use 'cs_pcs' for N threads"
+                    );
+                }
             }
 
             invariant = invariantRegistry.create(def.invariant());

src/main/java/dev/samhb/interleave/format/dsl/DslLoader.java

@@ -134,6 +134,7 @@ public static BenchmarkProgram load(ProgramDefinition def) {
                     } else if (lhs instanceof Lhs.LocalLhs ll) {
                         LocalDecl ld = decl.findLocal(ll.name());
                         if (ld == null) throw new RegistryException("Unknown local '" + ll.name() + "' at " + path + ".effects[" + eIdx + "]");
+                        if (ld.type() == FieldType.INT_ARRAY) throw new RegistryException("Local array '" + ll.name() + "' requires index: use local." + ll.name() + "[expr] at " + path + ".effects[" + eIdx + "]");
                         if (ld.type() != rhsType) throw new RegistryException("Type mismatch at " + path + ".effects[" + eIdx + "]: local '" + ll.name() + "' is " + ld.type() + ", rhs is " + rhsType);
                     } else if (lhs instanceof Lhs.ArrayLhs al) {
                         FieldDecl fd = decl.findField(al.arrayName());
@@ -152,6 +153,21 @@ public static BenchmarkProgram load(ProgramDefinition def) {
                         totalNodes += n;
                         if (totalNodes > 5000) throw new RegistryException("Total AST node count exceeds 5000");
                         // also check depth for index
+                    } else if (lhs instanceof Lhs.LocalArrayLhs lal) {
+                        LocalDecl ld = decl.findLocal(lal.localName());
+                        if (ld == null || ld.type() != FieldType.INT_ARRAY) throw new RegistryException("Unknown local array '" + lal.localName() + "' at " + path + ".effects[" + eIdx + "]");
+                        if (rhsType != FieldType.INT) throw new RegistryException("Array element assignment requires int at " + path + ".effects[" + eIdx + "]");
+                        try {
+                            TypeChecker.requireInt(lal.index(), decl);
+                        } catch (RegistryException ex) {
+                            throw new RegistryException("Array index must be int at " + path + ".effects[" + eIdx + "]: " + ex.getMessage(), ex);
+                        }
+                        int d = Expr.depth(lal.index());
+                        int n = Expr.nodeCount(lal.index());
+                        if (d > 16) throw new RegistryException("Expression depth exceeds 16 at " + path + ".effects[" + eIdx + "] lhs index");
+                        if (n > 5000) throw new RegistryException("Expression nodes exceed bound at " + path + ".effects[" + eIdx + "]");
+                        totalNodes += n;
+                        if (totalNodes > 5000) throw new RegistryException("Total AST node count exceeds 5000");
                     }
                     int d = Expr.depth(rhs);
                     int n = Expr.nodeCount(rhs);
@@ -434,8 +450,18 @@ private static StateDecl parseStateDecl(JsonObject stateJson) {
                         if (!initEl.isJsonPrimitive() || !initEl.getAsJsonPrimitive().isBoolean()) throw new RegistryException("'init' must be bool at " + path);
                         ld = LocalDecl.ofBool(name, initEl.getAsBoolean());
                     }
-                    case "int[]" -> throw new RegistryException("Local type 'int[]' not allowed at " + path + ".type");
-                    default -> throw new RegistryException("Unknown local type '" + typeStr + "' at " + path + ".type (valid: int, bool)");
+                    case "int[]" -> {
+                        if (!initEl.isJsonArray()) throw new RegistryException("'init' must be array at " + path);
+                        JsonArray arr = initEl.getAsJsonArray();
+                        if (arr.size() > 64) throw new RegistryException("Array length must be <=64 at " + path);
+                        int[] vals = new int[arr.size()];
+                        for (int k = 0; k < arr.size(); k++) {
+                            if (!arr.get(k).isJsonPrimitive() || !arr.get(k).getAsJsonPrimitive().isNumber()) throw new RegistryException("Array element must be int at " + path + ".init[" + k + "]");
+                            vals[k] = parseStrictInt(arr.get(k), path + ".init[" + k + "]");
+                        }
+                        ld = LocalDecl.ofArray(name, vals);
+                    }
+                    default -> throw new RegistryException("Unknown local type '" + typeStr + "' at " + path + ".type (valid: int, bool, int[])");
                 }
                 for (String k : o.keySet()) if (!k.equals("name") && !k.equals("type") && !k.equals("init")) throw new RegistryException("Unknown field '" + k + "' at " + path);
                 locals.add(ld);

src/main/java/dev/samhb/interleave/format/dsl/DynamicState.java

@@ -69,7 +69,13 @@ public DynamicState(StateDecl decl, int threadCount) {
         for (int tid = 0; tid < threadCount; tid++) {
             for (int j = 0; j < decl.locals().size(); j++) {
                 LocalDecl l = decl.locals().get(j);
-                localValues[tid][j] = l.type() == FieldType.INT ? l.intInit() : l.boolInit();
+                if (l.type() == FieldType.INT) {
+                    localValues[tid][j] = l.intInit();
+                } else if (l.type() == FieldType.BOOL) {
+                    localValues[tid][j] = l.boolInit();
+                } else {
+                    localValues[tid][j] = Arrays.copyOf(l.arrayInit(), l.arrayInit().length);
+                }
             }
         }
     }
@@ -235,6 +241,44 @@ public void setLocalBool(int tid, String name, boolean value) {
         localValues[tid][idx] = value;
     }
 
+    /**
+     * Returns a copy of a thread's declared {@code INT_ARRAY} local.
+     *
+     * @param tid the thread id
+     * @param name the declared local name
+     * @return copy of the array
+     */
+    public int[] getLocalArray(int tid, String name) {
+        int idx = indexOfLocal(name);
+        int[] arr = (int[]) localValues[tid][idx];
+        return Arrays.copyOf(arr, arr.length);
+    }
+
+    /**
+     * Returns direct array reference for internal use (no copy).
+     *
+     * @param tid the thread id
+     * @param name the declared local name
+     * @return array reference
+     */
+    int[] getLocalArrayRef(int tid, String name) {
+        int idx = indexOfLocal(name);
+        return (int[]) localValues[tid][idx];
+    }
+
+    /**
+     * Sets a thread's local array element.
+     *
+     * @param tid the thread id
+     * @param name the declared local name
+     * @param index element index
+     * @param value value to set
+     */
+    public void setLocalArrayElement(int tid, String name, int index, int value) {
+        int[] arr = getLocalArrayRef(tid, name);
+        arr[index] = value;
+    }
+
     /**
      * Resolves a declared field name to its storage index.
      *
@@ -280,7 +324,11 @@ public SharedState deepCopy() {
         }
         Object[][] localCopy = new Object[threadCount][decl.locals().size()];
         for (int tid = 0; tid < threadCount; tid++) {
-            localCopy[tid] = Arrays.copyOf(localValues[tid], localValues[tid].length);
+            for (int j = 0; j < decl.locals().size(); j++) {
+                Object lv = localValues[tid][j];
+                if (lv instanceof int[] arr) localCopy[tid][j] = Arrays.copyOf(arr, arr.length);
+                else localCopy[tid][j] = lv;
+            }
         }
         return new DynamicState(decl, threadCount, fieldCopy, localCopy);
     }
@@ -340,6 +388,13 @@ public void encodeTo(DataOutput out) throws IOException {
             out.writeInt(l.type().ordinal());
             out.writeInt(l.intInit());
             out.writeBoolean(l.boolInit());
+            int[] init = l.arrayInit();
+            if (init == null) {
+                out.writeInt(-1);
+            } else {
+                out.writeInt(init.length);
+                for (int v : init) out.writeInt(v);
+            }
         }
 
         // fields in declaration order: type ordinal, then value
@@ -360,8 +415,15 @@ public void encodeTo(DataOutput out) throws IOException {
         for (int tid = 0; tid < threadCount; tid++) {
             for (int j = 0; j < decl.locals().size(); j++) {
                 LocalDecl l = decl.locals().get(j);
-                if (l.type() == FieldType.INT) out.writeInt((Integer) localValues[tid][j]);
-                else out.writeBoolean((Boolean) localValues[tid][j]);
+                if (l.type() == FieldType.INT) {
+                    out.writeInt((Integer) localValues[tid][j]);
+                } else if (l.type() == FieldType.BOOL) {
+                    out.writeBoolean((Boolean) localValues[tid][j]);
+                } else {
+                    int[] arr = (int[]) localValues[tid][j];
+                    out.writeInt(arr.length);
+                    for (int v : arr) out.writeInt(v);
+                }
             }
         }
     }
@@ -393,11 +455,14 @@ public boolean equals(Object o) {
             } else if (!a.equals(b)) return false;
         }
         for (int tid = 0; tid < threadCount; tid++) {
-            if (!Arrays.equals(localValues[tid], that.localValues[tid])) {
-                // need deep equals for possibly int[]? locals are scalar only, so direct equals
-                boolean eq = true;
-                for (int j = 0; j < localValues[tid].length; j++) if (!localValues[tid][j].equals(that.localValues[tid][j])) eq = false;
-                if (!eq) return false;
+            for (int j = 0; j < localValues[tid].length; j++) {
+                Object a = localValues[tid][j];
+                Object b = that.localValues[tid][j];
+                if (a instanceof int[] arrA && b instanceof int[] arrB) {
+                    if (!Arrays.equals(arrA, arrB)) return false;
+                } else if (!a.equals(b)) {
+                    return false;
+                }
             }
         }
         return true;
@@ -418,7 +483,12 @@ public int hashCode() {
             if (v instanceof int[] arr) h = h * 31 + Arrays.hashCode(arr);
             else h = h * 31 + v.hashCode();
         }
-        for (Object[] row : localValues) h = h * 31 + Arrays.hashCode(row);
+        for (Object[] row : localValues) {
+            for (Object v : row) {
+                if (v instanceof int[] arr) h = h * 31 + Arrays.hashCode(arr);
+                else h = h * 31 + v.hashCode();
+            }
+        }
         return h;
     }
 
@@ -448,7 +518,10 @@ public String toString() {
             for (int tid = 0; tid < threadCount; tid++) {
                 for (int j = 0; j < decl.locals().size(); j++) {
                     LocalDecl l = decl.locals().get(j);
-                    sb.append("t").append(tid).append(".").append(l.name()).append("=").append(localValues[tid][j]);
+                    sb.append("t").append(tid).append(".").append(l.name()).append("=");
+                    Object lv = localValues[tid][j];
+                    if (lv instanceof int[] arr) sb.append(Arrays.toString(arr));
+                    else sb.append(lv);
                     if (tid != threadCount - 1 || j != decl.locals().size() - 1) sb.append(", ");
                 }
             }

src/main/java/dev/samhb/interleave/format/dsl/DynamicStep.java

@@ -55,6 +55,7 @@ public DynamicStep(int owner, Expr guard, List<Effect> effects, StateDecl decl,
             ExpressionReads.collect(e.rhs(), owner, r);
             // lhs index reads for array
             if (e.lhs() instanceof Lhs.ArrayLhs al) ExpressionReads.collect(al.index(), owner, r);
+            if (e.lhs() instanceof Lhs.LocalArrayLhs lal) ExpressionReads.collect(lal.index(), owner, r);
         }
         // Property observations are separate; step footprints describe execution and enabledness.
         this.reads = Set.copyOf(r);
@@ -76,6 +77,9 @@ private void addWrite(Lhs lhs, Set<MemoryLocation> w) {
         else if (lhs instanceof Lhs.ArrayLhs al) {
             if (al.index() instanceof Expr.IntLit lit) w.add(MemoryLocation.of(al.arrayName() + "[" + lit.value() + "]"));
             else w.add(MemoryLocation.of(al.arrayName()));
+        } else if (lhs instanceof Lhs.LocalArrayLhs lal) {
+            if (lal.index() instanceof Expr.IntLit lit) w.add(MemoryLocation.of("t" + owner + "." + lal.localName() + "[" + lit.value() + "]"));
+            else w.add(MemoryLocation.of("t" + owner + "." + lal.localName()));
         }
     }
 
@@ -172,10 +176,10 @@ public StepOutcome execute(SharedState state) {
                     if (ld.type() == FieldType.INT) {
                         if (rhsVal.type() != FieldType.INT) return StepOutcome.ASSERTION_FAILED;
                         ds.setLocalInt(owner, ll.name(), rhsVal.asInt());
-                    } else {
+                    } else if (ld.type() == FieldType.BOOL) {
                         if (rhsVal.type() != FieldType.BOOL) return StepOutcome.ASSERTION_FAILED;
                         ds.setLocalBool(owner, ll.name(), rhsVal.asBool());
-                    }
+                    } else return StepOutcome.ASSERTION_FAILED;
                 } else if (lhs instanceof Lhs.ArrayLhs al) {
                     FieldDecl fd = decl.findField(al.arrayName());
                     if (fd == null || fd.type() != FieldType.INT_ARRAY) return StepOutcome.ASSERTION_FAILED;
@@ -186,6 +190,16 @@ public StepOutcome execute(SharedState state) {
                     int[] arr = ds.getArrayRef(al.arrayName());
                     if (idx < 0 || idx >= arr.length) return StepOutcome.ASSERTION_FAILED;
                     arr[idx] = rhsVal.asInt();
+                } else if (lhs instanceof Lhs.LocalArrayLhs lal) {
+                    LocalDecl ld = decl.findLocal(lal.localName());
+                    if (ld == null || ld.type() != FieldType.INT_ARRAY) return StepOutcome.ASSERTION_FAILED;
+                    if (rhsVal.type() != FieldType.INT) return StepOutcome.ASSERTION_FAILED;
+                    Evaluator.Value idxVal = Evaluator.eval(lal.index(), ds, owner);
+                    if (idxVal.type() != FieldType.INT) return StepOutcome.ASSERTION_FAILED;
+                    int idx = idxVal.asInt();
+                    int[] arr = ds.getLocalArrayRef(owner, lal.localName());
+                    if (idx < 0 || idx >= arr.length) return StepOutcome.ASSERTION_FAILED;
+                    arr[idx] = rhsVal.asInt();
                 }
             }
             return StepOutcome.ADVANCED;

src/main/java/dev/samhb/interleave/format/dsl/Evaluator.java

@@ -113,13 +113,20 @@ public static Value eval(Expr expr, DynamicState state, int tid) {
             LocalDecl ld = state.decl().findLocal(l.name());
             if (ld == null) throw new RegistryException("Unknown local '" + l.name() + "'");
             if (ld.type() == FieldType.INT) return new IntVal(state.getLocalInt(tid, l.name()));
-            return new BoolVal(state.getLocalBool(tid, l.name()));
+            if (ld.type() == FieldType.BOOL) return new BoolVal(state.getLocalBool(tid, l.name()));
+            throw new RegistryException("Local '" + l.name() + "' is array; use local." + l.name() + "[index]");
         }
         if (expr instanceof Expr.ArrayAccess a) {
-            // local array access is not allowed (locals scalar only) — will have been rejected at type-check,
-            // but handle "local.name" case for robustness
             if (a.arrayName().startsWith("local.")) {
-                throw new EvalException("Local array access not supported: " + a.arrayName());
+                String localName = a.arrayName().substring("local.".length());
+                LocalDecl ld = state.decl().findLocal(localName);
+                if (ld == null || ld.type() != FieldType.INT_ARRAY) throw new RegistryException("Unknown local array '" + localName + "'");
+                Value idxVal = eval(a.index(), state, tid);
+                if (idxVal.type() != FieldType.INT) throw new RegistryException("Array index must be int");
+                int idx = idxVal.asInt();
+                int[] arr = state.getLocalArrayRef(tid, localName);
+                if (idx < 0 || idx >= arr.length) throw new EvalException("Array index out of bounds: " + a.arrayName() + "[" + idx + "] length " + arr.length);
+                return new IntVal(arr[idx]);
             }
             FieldDecl f = state.decl().findField(a.arrayName());
             if (f == null || f.type() != FieldType.INT_ARRAY) throw new RegistryException("Unknown array field '" + a.arrayName() + "'");

src/main/java/dev/samhb/interleave/format/dsl/ExpressionReads.java

@@ -20,7 +20,13 @@ static void collect(Expr expr, int owner, Set<MemoryLocation> out) {
         else if (expr instanceof Expr.LocalRef l) out.add(MemoryLocation.of("t" + owner + "." + l.name()));
         else if (expr instanceof Expr.ArrayAccess a) {
             if (a.arrayName().startsWith("local.")) {
-                out.add(MemoryLocation.of("t" + owner + "." + a.arrayName().substring(6)));
+                String localName = a.arrayName().substring("local.".length());
+                if (a.index() instanceof Expr.IntLit literal) {
+                    out.add(MemoryLocation.of("t" + owner + "." + localName + "[" + literal.value() + "]"));
+                } else {
+                    out.add(MemoryLocation.of("t" + owner + "." + localName));
+                    collect(a.index(), owner, out);
+                }
             } else if (a.index() instanceof Expr.IntLit literal) {
                 out.add(MemoryLocation.of(a.arrayName() + "[" + literal.value() + "]"));
             } else {

src/main/java/dev/samhb/interleave/format/dsl/Lhs.java

@@ -4,7 +4,7 @@
 /**
  * Left-hand side of an effect assignment.
  */
-public sealed interface Lhs permits Lhs.FieldLhs, Lhs.LocalLhs, Lhs.ArrayLhs {
+public sealed interface Lhs permits Lhs.FieldLhs, Lhs.LocalLhs, Lhs.ArrayLhs, Lhs.LocalArrayLhs {
     /**
      * Shared field scalar assignment.
      * @param name declared field or local name
@@ -21,4 +21,10 @@ record LocalLhs(String name) implements Lhs {}
      * @param index expression selecting an array element
      */
     record ArrayLhs(String arrayName, Expr index) implements Lhs {}
+    /**
+     * Per-thread local array element assignment.
+     * @param localName declared per-thread local array name
+     * @param index expression selecting an array element
+     */
+    record LocalArrayLhs(String localName, Expr index) implements Lhs {}
 }