gdp-ts: формальные доказательства в типах TypeScript без накладных расходов в рантайме

Каждый разработчик веб-сервисов хотя бы раз ловил неприятный баг: критическая мутация в базе данных выполнилась, потому что кто-то забыл вызвать функцию проверки прав строчкой выше. В динамических языках и даже в типизированном TypeScript мы привыкли полагаться на дисциплину команды или тесты. Но когда кодовую базу начинают активно дополнять автономные ИИ-агенты, человеческий фактор уступает место вероятностным ошибкам: модель генерирует правдоподобный вызов API, просто «забыв» неявный шаг предварительной валидации.

Библиотека gdp-ts от Гильермо Рауха предлагает математически строгое решение этой проблемы. Она переносит в экосистему TypeScript паттерн Ghosts of Departed Proofs (GDP), зародившийся в функциональном программировании на Haskell. Идея проста и элегантна: сделать так, чтобы опасную функцию физически невозможно было вызвать без предъявления специального цифрового «жетона» — доказательства того, что проверка действительно пройдена.

Анатомия фантомных доказательств в системе типов

В основе паттерна лежит разделение данных и утверждений об их свойствах. В стандартном коде проверка прав — это императивное действие: мы вызываем валидатор и надеемся, что последующий код защищен. В концепции GDP утверждение (например, «пользователь $U$ является администратором проекта $P$») материализуется как фантомный тип Proof<Predicate>.

Такой токен невозможно создать случайным литералом или пустой строкой: единственным легитимным эмитентом доказательства выступает доверенная функция ядра (trusted kernel). Чувствительная бизнес-логика объявляет токен обязательным аргументом. Если валидация не вызывалась, компилятор TypeScript выдает ошибку на этапе сборки еще до деплоя в тестовый контур.

import { Named, Proof, defineLemma } from '@gdp-ts/core';

// Определяем предикат авторизации с уникальным номинальным символом
type ProjectId = string;
type IsAdmin<User, Project> = { readonly __predicate: unique symbol };

// Доверенная функция: проверяет БД и только при успехе выпускает доказательство
export async function verifyAdminAccess<U, P>(
  userId: Named<U, string>,
  projectId: Named<P, ProjectId>
): Promise<Proof<IsAdmin<U, P>>> {
  const isAllowed = await db.permissions.check(userId, projectId);
  if (!isAllowed) {
    throw new Error('Доступ отклонен политикой безопасности');
  }
  // defineLemma создает номинальный токен доказательства без рантайм-веса
  return defineLemma<IsAdmin<U, P>>();
}

Защита мутаций и цепочки проверок без раздувания рантайма

Главная практическая ценность gdp-ts раскрывается при защите опасных операций. Функция удаления проекта, списания баланса или изменения пароля в своей сигнатуре требует токен с точным соответствием типов пользователя и проекта. Передать чужой токен от другого проекта компилятор не позволит благодаря номинальному связыванию Named<P, ...>.

При этом библиотека работает по принципу Zero Runtime Overhead: в результирующем JavaScript-коде все типы Proof и символьные обертки полностью исчезают. В процессе выполнения нет никаких тяжелых прокси-объектов или оберток, а оверхед на этапе тайпчека компилятора составляет всего около 0.3 мс на вызов.

// Защищенная операция: без валидного токена компилятор блокирует вызов
export async function updateProjectSecurity<U, P>(
  project: Named<P, ProjectId>,
  newSecret: string,
  proof: Proof<IsAdmin<U, P>>
): Promise<void> {
  // На уровне типов доказано: project проверен для пользователя U
  await db.projects.update({
    where: { id: project },
    data: { secretHash: hash(newSecret) }
  });
}

// Пример использования в обработчике запроса:
async function handleRequest(userId: string, projectId: string) {
  // 1. Привязываем уникальные номинальные типы к идентификаторам
  const u = Named(userId);
  const p = Named(projectId);

  // 2. Получаем доказательство через валидатор
  const adminProof = await verifyAdminAccess(u, p);

  // 3. Вызываем защищенную мутацию — сборка проходит успешно
  await updateProjectSecurity(p, 'super-secret-key', adminProof);
}

Границы применимости и дисциплина типизации

Поскольку TypeScript опирается на структурную типизацию, программист технически может попытаться обойти контракт грубым приведением as unknown as Proof<...>. Чтобы пресечь подобные лазейки, gdp-ts поставляется в комплекте с правилами для линтера и набором навыков для ИИ-агентов (npx skills add rauchg/gdp-ts), которые запрещают искусственный кастинг токенов доказательств.

Паттерн требует определенной зрелости архитектуры: вам придется аккуратно спроектировать доверенное ядро функций-валидаторов и привыкнуть к сигнатурам с обобщениями (generics). Однако для критических узлов — финансовых транзакций, multi-tenant изоляции и предотвращения уязвимостей IDOR — gdp-ts дает надежный щит на уровне компиляции, делая кодовую базу устойчивой к ошибкам как людей, так и нейросетей.