Spaces:
Running
Running
File size: 5,055 Bytes
518343a | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 | /**
* Tests for Multi-Agent Cooperative Termination Gate
* Lean theorem: Lutar.Thesis.MultiAgent.all_agents_terminate (GREEN)
*
* Property: 7 organs each with finite fuel budget terminate within budget steps.
*/
import { describe, it, expect } from "vitest";
import {
runMultiAgentTermination,
ouroborosAgents,
type AgentSpec,
} from "../src/multi_agent_terminator";
// ---------------------------------------------------------------------------
// Deterministic cases
// ---------------------------------------------------------------------------
describe("runMultiAgentTermination — GREEN theorem all_agents_terminate", () => {
it("single agent with fuel=1: terminates in 1 step", () => {
const agents: AgentSpec[] = [
{ id: "test", fuel: 1, step: () => 1 },
];
const r = runMultiAgentTermination(agents);
expect(r.allTerminated).toBe(true);
expect(r.traces[0]!.terminatedWithin).toBe(true);
expect(r.traces[0]!.stepsRun).toBe(1);
});
it("single agent with fuel=10, consuming 2/step: terminates in 5 steps", () => {
const agents: AgentSpec[] = [
{ id: "fast", fuel: 10, step: () => 2 },
];
const r = runMultiAgentTermination(agents);
expect(r.allTerminated).toBe(true);
expect(r.traces[0]!.fuelConsumed).toBe(10);
});
it("7 Ouroboros organs with fuel 100 each: all terminate", () => {
const agents = ouroborosAgents();
const r = runMultiAgentTermination(agents);
expect(r.allTerminated).toBe(true);
expect(r.violations).toHaveLength(0);
expect(r.traces).toHaveLength(7);
for (const trace of r.traces) {
expect(trace.terminatedWithin).toBe(true);
}
});
it("3 agents, mixed budgets: all terminate", () => {
const agents: AgentSpec[] = [
{ id: "a", fuel: 5, step: () => 1 },
{ id: "b", fuel: 10, step: () => 3 },
{ id: "c", fuel: 7, step: () => 2 },
];
const r = runMultiAgentTermination(agents);
expect(r.allTerminated).toBe(true);
expect(r.receipt.lean_theorem).toBe(
"Lutar.Thesis.MultiAgent.all_agents_terminate"
);
});
it("receipt fields are correct", () => {
const agents = ouroborosAgents({ amaru: 5, sentra: 5 });
const r = runMultiAgentTermination([agents[0]!, agents[1]!]);
expect(r.receipt.formula).toBe("all_agents_terminate");
expect(r.receipt.lean_file).toBe(
"Lutar/Thesis/TH_V18_15_MultiAgentFairness.lean"
);
expect(r.receipt.inputs_hash).toHaveLength(64);
expect(typeof r.receipt.ts).toBe("string");
});
it("throws on non-integer fuel", () => {
expect(() =>
runMultiAgentTermination([{ id: "x", fuel: 1.5, step: () => 1 }])
).toThrow(/integer/);
});
it("throws on zero fuel", () => {
expect(() =>
runMultiAgentTermination([{ id: "x", fuel: 0, step: () => 1 }])
).toThrow(/finite positive integer/);
});
it("step returning 0 throws (violates termination precondition)", () => {
expect(() =>
runMultiAgentTermination([
{ id: "bad", fuel: 10, step: () => 0 },
])
).toThrow(/must return integer ≥ 1/);
});
it("ouroborosAgents produces 7 named organs", () => {
const agents = ouroborosAgents();
const ids = agents.map((a) => a.id).sort();
expect(ids).toEqual(
["a11oy", "amaru", "rosie", "sentra", "uds-mesh", "vessels", "vsp-otel"]
);
});
it("ouroborosAgents respects custom budgets", () => {
const agents = ouroborosAgents({ amaru: 42, sentra: 17 });
const amaru = agents.find((a) => a.id === "amaru")!;
const sentra = agents.find((a) => a.id === "sentra")!;
expect(amaru.fuel).toBe(42);
expect(sentra.fuel).toBe(17);
});
});
// ---------------------------------------------------------------------------
// Fuzz: 1000 random agent configs
// ---------------------------------------------------------------------------
describe("runMultiAgentTermination — 1000 random configs (theorem fuzz)", () => {
it("7 organs each with random budget [1,100]: all terminate", () => {
let failures = 0;
for (let i = 0; i < 1000; i++) {
const budgets: Record<string, number> = {};
for (const organ of ["amaru", "sentra", "vessels", "rosie", "vsp-otel", "uds-mesh", "a11oy"]) {
budgets[organ] = Math.floor(Math.random() * 100) + 1;
}
const agents = ouroborosAgents(budgets);
const r = runMultiAgentTermination(agents);
if (!r.allTerminated) failures++;
}
expect(failures).toBe(0);
});
it("random agents 1–10 with random budgets 1–50: all terminate", () => {
let failures = 0;
for (let i = 0; i < 200; i++) {
const n = Math.floor(Math.random() * 10) + 1;
const agents: AgentSpec[] = Array.from({ length: n }, (_, k) => ({
id: `agent-${k}`,
fuel: Math.floor(Math.random() * 50) + 1,
step: () => Math.floor(Math.random() * 3) + 1, // consume 1–3 per step
}));
const r = runMultiAgentTermination(agents);
if (!r.allTerminated) failures++;
}
expect(failures).toBe(0);
});
});
|