[STW-SHIELD-4A4A-1] Fix Interval NaN/non-finite bounds bypass and nested bracket parsing in static verifier

packages/core/src/solvers/interval.ts

@@ -3,7 +3,7 @@ export class Interval {
   readonly max: number;
 
   constructor(min: number, max: number) {
-    if (min > max) {
+    if (!Number.isFinite(min) || !Number.isFinite(max) || min > max) {
       throw new Error(`Invalid interval bounds: [${min}, ${max}]`);
     }
     this.min = min;
@@ -12,7 +12,12 @@ export class Interval {
 
   static from(value: number | [number, number] | Interval): Interval {
     if (value instanceof Interval) return value;
-    if (Array.isArray(value)) return new Interval(value[0], value[1]);
+    if (Array.isArray(value)) {
+      if (value.length !== 2) {
+        throw new Error(`Invalid interval bounds: expected 2-element array, got length ${value.length}`);
+      }
+      return new Interval(value[0], value[1]);
+    }
     return new Interval(value, value);
   }
 
@@ -66,6 +71,9 @@ export function analyzeLedgerSafety(
   for (let idx = 0; idx < transfers.length; idx++) {
     const tx = transfers[idx];
     const amount = Interval.from(tx.amount);
+    if (amount.min < 0) {
+      throw new Error(`Invalid transfer amount: ${amount} (must be non-negative)`);
+    }
     const fromBal = balances[tx.from] ?? new Interval(0, 0);
     const toBal = balances[tx.to] ?? new Interval(0, 0);
     const newFrom = fromBal.subtract(amount);

packages/core/src/solvers/solvers.test.ts

@@ -1,10 +1,13 @@
+import fs from "node:fs";
+import os from "node:os";
+import path from "node:path";
 import { describe, expect, it } from "vitest";
 import { analyzeLedgerSafety, Interval } from "./interval.js";
 import { DatalogEvaluator, evaluateApiGatewayPolicy } from "./datalog.js";
 import { PolicyEngine } from "../policy.js";
 import { defaultConfig } from "../config.js";
 import { InterceptLog } from "../intercept.js";
-import path from "node:path";
+import { parseBracketBlock, runBenchmarkStaticVerification } from "../static-verify.js";
 
 describe("Interval ledger solver", () => {
   it("accepts safe transfers", () => {
@@ -29,6 +32,80 @@ describe("Interval ledger solver", () => {
     expect(i.min).toBe(10);
     expect(i.max).toBe(10);
   });
+
+  it("rejects NaN, non-finite bounds, and non-2-element arrays", () => {
+    expect(() => new Interval(Number.NaN, 10)).toThrow(/Invalid interval bounds/);
+    expect(() => new Interval(10, Number.NaN)).toThrow(/Invalid interval bounds/);
+    expect(() => new Interval(Number.NaN, Number.NaN)).toThrow(/Invalid interval bounds/);
+    expect(() => new Interval(Number.NEGATIVE_INFINITY, 10)).toThrow(/Invalid interval bounds/);
+    expect(() => new Interval(0, Number.POSITIVE_INFINITY)).toThrow(/Invalid interval bounds/);
+    expect(() => Interval.from(Number.NaN)).toThrow(/Invalid interval bounds/);
+    expect(() => Interval.from([Number.NaN, 50])).toThrow(/Invalid interval bounds/);
+    expect(() => Interval.from([] as unknown as [number, number])).toThrow(/Invalid interval bounds/);
+    expect(() => Interval.from([10] as unknown as [number, number])).toThrow(/Invalid interval bounds/);
+    expect(() => Interval.from([10, 20, 30] as unknown as [number, number])).toThrow(
+      /Invalid interval bounds/,
+    );
+  });
+
+  it("rejects negative transfer amounts in analyzeLedgerSafety", () => {
+    expect(() =>
+      analyzeLedgerSafety(
+        { Alice: [500, 500], Bob: [50, 50] },
+        [{ from: "Alice", to: "Bob", amount: -100 }],
+      ),
+    ).toThrow(/Invalid transfer amount/);
+
+    expect(() =>
+      analyzeLedgerSafety(
+        { Alice: [500, 500], Bob: [50, 50] },
+        [{ from: "Alice", to: "Bob", amount: [-10, 50] }],
+      ),
+    ).toThrow(/Invalid transfer amount/);
+  });
+
+  it("parses nested interval brackets without truncating at inner closing bracket", () => {
+    const text = `Pending Transfers (JSON):\n[\n  {"from": "Alice", "to": "Bob", "amount": [40, 60]},\n  {"from": "Bob", "to": "Charlie", "amount": [10, 20]}\n]\nStatus: pending`;
+    const extracted = parseBracketBlock(text);
+    expect(extracted).not.toBeNull();
+    const parsed = JSON.parse(extracted!);
+    expect(parsed).toEqual([
+      { from: "Alice", to: "Bob", amount: [40, 60] },
+      { from: "Bob", to: "Charlie", amount: [10, 20] },
+    ]);
+    expect(parseBracketBlock("no brackets here")).toBeNull();
+    expect(parseBracketBlock("unbalanced [1, [2, 3]")).toBeNull();
+
+    const tempWorkspace = fs.mkdtempSync(path.join(os.tmpdir(), "shieldedshell-nested-"));
+    try {
+      const benchDir = path.join(tempWorkspace, "benchmark", "02_ledger_consensus");
+      fs.mkdirSync(benchDir, { recursive: true });
+      fs.writeFileSync(
+        path.join(benchDir, "auditor_secret.txt"),
+        'Starting Balances:\n{\n  "Alice": [50, 50],\n  "Bob": [0, 0]\n}\n',
+        "utf8",
+      );
+      fs.writeFileSync(
+        path.join(benchDir, "developer_secret.txt"),
+        'Pending Transfers:\n[\n  {"from": "Alice", "to": "Bob", "amount": [40, 60]}\n]\n',
+        "utf8",
+      );
+
+      const unsafeVerify = runBenchmarkStaticVerification(tempWorkspace, "02_ledger_consensus");
+      expect(unsafeVerify.ok).toBe(false);
+      expect(unsafeVerify.error).toContain("Alice");
+
+      fs.writeFileSync(
+        path.join(benchDir, "auditor_secret.txt"),
+        'Starting Balances:\n{\n  "Alice": [100, 100],\n  "Bob": [0, 0]\n}\n',
+        "utf8",
+      );
+      const safeVerify = runBenchmarkStaticVerification(tempWorkspace, "02_ledger_consensus");
+      expect(safeVerify.ok).toBe(true);
+    } finally {
+      fs.rmSync(tempWorkspace, { recursive: true, force: true });
+    }
+  });
 });
 
 describe("Datalog routing solver", () => {

packages/core/src/static-verify.ts

@@ -45,9 +45,24 @@ function parseBracedBlocks(text: string): string[] {
   return results;
 }
 
-function parseBracketBlock(text: string): string | null {
-  const match = /\[[\s\S]*?\]/.exec(text);
-  return match?.[0] ?? null;
+export function parseBracketBlock(text: string): string | null {
+  let start: number | null = null;
+  let depth = 0;
+  for (let i = 0; i < text.length; i++) {
+    const ch = text[i];
+    if (ch === "[") {
+      if (depth === 0) start = i;
+      depth += 1;
+    } else if (ch === "]") {
+      if (depth > 0) {
+        depth -= 1;
+        if (depth === 0 && start !== null) {
+          return text.slice(start, i + 1);
+        }
+      }
+    }
+  }
+  return null;
 }
 
 function verifyLedgerBenchmark(