packages/policy/src/gates/pareto_stabilization.ts

/**
 * Pareto Finite Stabilization Gate
 *
 * @lean_theorem Lutar.Thesis.ParetoStabilization.th_v18_11_pareto_stabilization
 * @lean_file    Lutar/Thesis/TH_V18_11_ParetoFiniteStabilization.lean
 * @lean_status  GREEN — 0 sorries
 * @lean_commit  see LEAN_COMMIT_SHA env var; pin at CI time from lutar-lean/lean-toolchain
 *
 * Theorem (Lynch 1996 Distributed Algorithms Ch.8; Sipser 2012 Intro to Theory of Computation):
 *   For finite discrete multi-objective optimization over objectives O ⊂ ℝⁿ (finite set),
 *   the Pareto frontier F* stabilizes in at most |O| steps.
 *   Proof: Each update either adds a new non-dominated point (bounded by |O|) or removes
 *   dominated points. Since |O| is finite, the frontier cannot oscillate indefinitely.
 *   The governance optimizer reaches a fixed point in finite rounds.
 *
 * Applications:
 *   - Multi-organ Ouroboros governance convergence guarantee
 *   - Budget allocation convergence across 7 organs under discrete utility spaces
 *
 * References:
 *   Lynch (1996) Distributed Algorithms Ch.8 — stabilization in finite systems
 *   Sipser (2012) Introduction to the Theory of Computation §7
 *   Lutar/Thesis/TH_V18_11_ParetoFiniteStabilization.lean
 *
 * SPDX-License-Identifier: Apache-2.0
 */

import * as crypto from "crypto";

// ---------------------------------------------------------------------------
// Types
// ---------------------------------------------------------------------------

/** A multi-dimensional objective vector (maximize each dimension) */
export type ObjectiveVector = readonly number[];

export interface ParetoStabilizationResult {
  /** True iff the Pareto frontier stabilized before maxRounds */
  stabilized: boolean;
  /** Round at which stabilization was detected (1-indexed) */
  stabilizationRound: number;
  /** Final Pareto frontier */
  paretoFrontier: ObjectiveVector[];
  /** Total rounds processed */
  roundsProcessed: number;
  /** DSSE receipt */
  receipt: ParetoDsseReceipt;
}

export interface ParetoDsseReceipt {
  formula: string;
  lean_theorem: string;
  lean_file: string;
  lean_commit_sha: string;
  inputs_hash: string;
  output: {
    stabilized: boolean;
    stabilizationRound: number;
    frontierSize: number;
    roundsProcessed: number;
  };
  ts: string;
}

// ---------------------------------------------------------------------------
// Pareto dominance
// ---------------------------------------------------------------------------

/**
 * Returns true if `a` dominates `b` (a ≥ b in all dimensions, a > b in at least one).
 */
function dominates(a: ObjectiveVector, b: ObjectiveVector): boolean {
  if (a.length !== b.length) {
    throw new Error(`dominates: dimension mismatch ${a.length} vs ${b.length}`);
  }
  let strictlyBetter = false;
  for (let i = 0; i < a.length; i++) {
    if (a[i]! < b[i]!) return false;
    if (a[i]! > b[i]!) strictlyBetter = true;
  }
  return strictlyBetter;
}

/**
 * Compute Pareto frontier: non-dominated subset of `objectives`.
 */
function computeParetoFrontier(
  objectives: ObjectiveVector[]
): ObjectiveVector[] {
  const frontier: ObjectiveVector[] = [];
  for (const cand of objectives) {
    // Check if any existing frontier member dominates cand
    if (frontier.some((f) => dominates(f, cand))) continue;
    // Remove any frontier members dominated by cand
    const newFrontier = frontier.filter((f) => !dominates(cand, f));
    newFrontier.push(cand);
    frontier.length = 0;
    frontier.push(...newFrontier);
  }
  return frontier;
}

/**
 * Frontier equality check (order-independent).
 */
function frontierEqual(
  a: ObjectiveVector[],
  b: ObjectiveVector[]
): boolean {
  if (a.length !== b.length) return false;
  const toStr = (v: ObjectiveVector) => v.join(",");
  const setA = new Set(a.map(toStr));
  return b.every((v) => setA.has(toStr(v)));
}

// ---------------------------------------------------------------------------
// Internal helpers
// ---------------------------------------------------------------------------

function sha256Hex(obj: unknown): string {
  return crypto.createHash("sha256").update(JSON.stringify(obj)).digest("hex");
}

// ---------------------------------------------------------------------------
// Public API
// ---------------------------------------------------------------------------

/**
 * Assert the Pareto finite stabilization theorem.
 *
 * Given a sequence of round-by-round candidate objective vectors, check that
 * the Pareto frontier stabilizes (does not change) within `maxRounds` rounds.
 *
 * @param candidateStream  Array of rounds; each round is an array of new objective vectors.
 *                         Objectives accumulate across rounds.
 * @param maxRounds        Maximum rounds before declaring non-stabilization (default 50)
 *
 * @returns ParetoStabilizationResult with stabilization round and DSSE receipt.
 *
 * By the Lean theorem, stabilization is guaranteed if the total objective space is finite.
 */
export function paretoStabilizationGate(
  candidateStream: ObjectiveVector[][],
  maxRounds = 50
): ParetoStabilizationResult {
  let allObjectives: ObjectiveVector[] = [];
  let prevFrontier: ObjectiveVector[] = [];
  let stabilizationRound = -1;
  let roundsProcessed = 0;

  for (let r = 0; r < Math.min(candidateStream.length, maxRounds); r++) {
    allObjectives = allObjectives.concat(candidateStream[r]!);
    const newFrontier = computeParetoFrontier(allObjectives);
    roundsProcessed = r + 1;

    if (r > 0 && frontierEqual(prevFrontier, newFrontier)) {
      stabilizationRound = r + 1;
      prevFrontier = newFrontier;
      break;
    }
    prevFrontier = newFrontier;
  }

  const stabilized = stabilizationRound !== -1;
  const inputs_hash = sha256Hex({ candidateStream, maxRounds });
  const lean_commit_sha = process.env["LEAN_COMMIT_SHA"] ?? "unknown";

  const receipt: ParetoDsseReceipt = {
    formula: "th_v18_11_pareto_stabilization",
    lean_theorem:
      "Lutar.Thesis.ParetoStabilization.th_v18_11_pareto_stabilization",
    lean_file: "Lutar/Thesis/TH_V18_11_ParetoFiniteStabilization.lean",
    lean_commit_sha,
    inputs_hash,
    output: {
      stabilized,
      stabilizationRound,
      frontierSize: prevFrontier.length,
      roundsProcessed,
    },
    ts: new Date().toISOString(),
  };

  return {
    stabilized,
    stabilizationRound,
    paretoFrontier: prevFrontier,
    roundsProcessed,
    receipt,
  };
}

/**
 * Build a candidate stream from a static pool of objectives.
 * Splits the pool across `rounds` batches evenly.
 * Convenience for testing stabilization under finite objective spaces.
 */
export function buildCandidateStream(
  objectives: ObjectiveVector[],
  rounds: number
): ObjectiveVector[][] {
  const batchSize = Math.ceil(objectives.length / rounds);
  const stream: ObjectiveVector[][] = [];
  for (let i = 0; i < objectives.length; i += batchSize) {
    stream.push(objectives.slice(i, i + batchSize));
  }
  return stream;
}