fts-gate

Верификационный гейт поверх FTS — языка исполняемых спецификаций. Ключевое свойство: отказ является следствием типовой ошибки, а не решением языковой модели.

Когда обычный ассистент «не отвечает», это его выбор, который можно переформулировать, уговорить или обойти джейлбрейком. Когда отказывает fts-gate, система не смогла построить доказательство: для морфизма, которого нет в библиотеке проверенных законов, частичная функция M(m) не определена, правило типизации APPLY неприменимо, и вывода просто не существует. Уговорить нечего.

Границы гарантии описаны предельно честно в docs/guarantees.md — включая рабочий контрпример, который проходит все проверки FTS полностью зелёным и всё-таки выдаёт привилегированный доступ по одному паролю.

Архитектура

                    spec_source (.fts)         context (JSON)
                          │                          │
                          ▼                          │
   ┌──────────────────────────────────────────┐      │
   │ 1. compile()          → PARSE_ERROR      │      │
   ├──────────────────────────────────────────┤      │
   │ 2. validate()         → TYPE_ERROR       │      │
   │    Σ = (C, Δ, M): имена, типы, apply     │      │
   ├──────────────────────────────────────────┤      │
   │ 2.5 детектор: структура вывода           │      │
   │    → CIRCULAR_PREMISE, REVERSED_MORPHISM,│      │
   │      VACUOUS_MORPHISM, EQUIVOCATION,     │      │
   │      REIFICATION                         │      │
   ├──────────────────────────────────────────┤      │
   │ 3. discharge premises                    │◀── morphisms/manifest.json
   │    → UNVERIFIED_MORPHISM                 │    verified / derived / proposed
   ├──────────────────────────────────────────┤      │
   │ 4. testUtilities()    → PROPERTY_VIOLATION│     │
   │    примеры и свойства                    │      │
   ├──────────────────────────────────────────┤      │
   │ 4.5 детектор: слой утилит                │      │
   │    → NON_EXHAUSTIVE, UNDECLARED_BOUNDARY,│      │
   │      EXAMPLE_AS_PROOF                    │      │
   ├──────────────────────────────────────────┤      │
   │ 5. certify()  (производитель)            │◀─────┤
   │    → CERTIFICATE_ERROR                   │      │
   ├──────────────────────────────────────────┤      │
   │ 6. verify()   (независимый проверяющий)  │◀─────┘
   │    → VERIFICATION_ERROR                  │
   └──────────────────────────────────────────┘
                          │
             ┌────────────┴────────────┐
             ▼                         ▼
      status: "certified"       status: "refused"
      result, certificate,      code, detail,
      morphisms_used, digests   missing_morphisms?, failures?,
                                fallacies?, explains?, verdict?

Детектор разбит на два прохода не для красоты: дефекты самого вывода (круг, обратное направление, пустой домен) не зависят от того, допустимы ли посылки, и сообщаются до обращения к манифесту; дефекты слоя утилит сообщаются после исполнения примеров, чтобы сломанный пример оставался сломанным примером, а не превращался в претензию к обобщению.

Шаги 5 и 6 разделены намеренно: производитель доказательства и проверяющий не делят состояние, как того требует proof-carrying подход. Проверяющий заново строит вывод из документа и контекста и сравнивает дайджесты.

ftsGate никогда не бросает исключение наружу — любое непредвиденное условие становится отказом INTERNAL_ERROR, поэтому вызывающий всегда может ветвиться по полю status.

Компоненты

Сам язык FTS — отдельный пакет @digitable/fts; гейт подключает его как обычную зависимость и ничего из него не копирует.

Related MCP server: Chiasmus

Коды отказа

Причины UNVERIFIED_MORPHISM различаются полем reason: not_in_manifest, proposed, signature_mismatch.

Коды детектора логических ошибок

src/fallacies.ts превращает каталог логических ошибок (67 позиций) в механические проверки над Σ = (C, Δ, M). Каждый отказ несёт fallacies (список находок), explains (глава курса, объясняющая ошибку) и verdict.

Отказ детектора означает отказ в сертификации, а не ложность содержания (каталог №67, «Ошибка ошибки»). Это не риторика, а инвариант: поле verdict проговаривает границу дословно, а тест механически запрещает словам «ложно» и «неверно» появляться в тексте отказа.

Границы детектора — сколько позиций каталога он покрывает, почему «ошибок не найдено» не значит «ошибок нет» и почему устранение структурных дефектов делает ложный вывод убедительнее, — в docs/guarantees.md §2.4.

Отключается опцией detectFallacies: false: гейт ведёт себя ровно как до появления детектора. Полезно для ablation и для замера «сколько добавил детектор».

Библиотека морфизмов

morphisms/manifest.json — единственный источник истины о том, какие доменные законы допустимы как предпосылки. В этом репозитории: 10 записей — 4 морфизма модуля access-control.fts (3 verified, 1 derived), 1 отклонённый закон контрпримера (proposed) и 5 примитивов стандартной библиотеки FTS.

Морфизм сопоставляется с записью по имени, после чего сверяется вся сигнатура: домен, кодомен и идентификатор закона. Поэтому нельзя одолжить доверие у чужого имени, подставив под него другой домен.

Записи derived не принимаются на слово: при загрузке манифеста проверяется, что цепочка действительно композируется (dom(m₁) = dom(m), cod(mᵢ) = dom(mᵢ₊₁), cod(mₙ) = cod(m)) и не опирается на proposed.

Каждый verified-морфизм несёт поле source со ссылкой на конкретный документ, по которому закон был проверен человеком. Для опубликованного набора это docs/morphism-review.md: по разделу на закон, с тем, что именно проверено и чего закон не утверждает.

Что лежит в этом репозитории, а что нет

Рабочий набор доменных морфизмов Digitable в этот репозиторий не входит. .fts-модули с реальными правилами живут в закрытом репозитории и подключаются к гейту через manifestPath / manifest или через собственный каталог morphisms/.

Здесь опубликованы только схема библиотеки — формат manifest.json, его валидация в src/manifest.ts и проверка композиции derived — и один нейтральный пример модуля, morphisms/access-control.fts (MFA и привилегированный доступ), чтобы формат было на чём показать.

Добавление морфизма

1. Объявить его в .fts-модуле в morphisms/ вместе с по закону «id».

2. Добавить запись в manifest.json с той же сигнатурой и полем source.

3. npm test — тест each .fts module declares exactly the morphisms the manifest attributes to it не даст манифесту и модулю разойтись для тех модулей, которые лежат рядом.

Подключение

Требования

Node.js ≥ 20 (проверено на v24.18). Единственная рантайм-зависимость — сам язык FTS, пакет @digitable/fts.

Пакет пока не опубликован в npm, поэтому зависимость объявлена git-адресом. То, что npm упаковывает из того репозитория, не содержит dist/ (это артефакт сборки, а prepare-скрипта там нет), поэтому установленную зависимость нужно один раз собрать. Это делает scripts/bootstrap-fts.mjs, подключённый как prepare: он скачивает src/**/*.ts ровно того коммита, который поставил npm, и компилирует его локальным TypeScript. Отдельно скрипт вызывается как npm run bootstrap:fts; он идемпотентен и станет лишним, как только @digitable/fts появится в npm.

Сборка

npm ci                  # ставит зависимости и собирает dist FTS (prepare)
npm test                # 62/62
npm run grammar:check   # 26 / 10 / 200

Библиотека

import { ftsGate } from "@digitable-lol/fts-gate"

const result = ftsGate(source, context)
if (result.status === "refused") {
  console.error(result.code, result.detail, result.missing_morphisms)
} else {
  console.log(result.certificate.certificate_digest, result.morphisms_used)
}

Опции: requireEvidence (отклонять symbolic и trivial сертификаты), manifestPath / manifest (альтернативная библиотека морфизмов).

CLI

node dist/src/cli.js check examples/access-revocation.fts \
  --context examples/access-revocation.context.json --pretty   # exit 0

node dist/src/cli.js check examples/password-mfa.fts \
  --context examples/password-mfa.context.json --pretty        # exit 1

node dist/src/cli.js morphisms --trust proposed --pretty

Коды возврата: 0 — сертифицировано, 1 — отказ (код в поле .code), 2 — ошибка вызова или ввода-вывода. В stdout всегда ровно один JSON-объект.

MCP

{
  "mcpServers": {
    "fts-gate": {
      "command": "node",
      "args": ["/абсолютный/путь/до/fts-gate/dist/src/mcp.js"]
    }
  }
}

Два read-only инструмента:

• fts_gate_check — { source, context?, require_evidence? } → полный GateResult. Отказ возвращается как нормальный результат (isError: false): гейт отработал штатно. isError: true означает сломанный вызов или сломанную библиотеку, а не отказ.

• fts_morphisms_list — { trust?, domain? } → библиотека морфизмов с уровнями доверия, источниками и дайджестом манифеста.

Грамматика для constrained decoding

grammars/fts.gbnf — GBNF для llama.cpp, покрывающая русскую отступную поверхность целиком: категория, объект/структура, морфизм, утилита (правило, свойство, пример), теорема, кавычки-ёлочки, все фразы сравнения, процентные операнды, комментарии //.

Это строгое подмножество языка парсера. Сознательные ограничения: отступ ровно два пробела, только русская поверхность, фиксированный порядок строк утилиты, одна теорема в конце документа, без одиночных кавычек и блочных комментариев. Полный список — grammars/README.md.

Проверяется с двух сторон командой npm run grammar:check (собственный парсер GBNF и распознаватель, llama.cpp не нужен):

positive corpus — 26 accepted   (все .fts русской поверхности репозитория и примеры пакета @digitable/fts)
negative corpus — 10 rejected
generated corpus — 200 строк сэмплированы из грамматики и поданы в compile(): 0 синтаксических отказов

Грамматика гарантирует синтаксис и ничего больше: сгенерированный документ всё ещё может не пройти validate и тем более может быть содержательно ложным.

Детектор как функция награды (задел на обучение генератора)

Детектор даёт бесплатный автоматический negative reward: спецификация с кругом в основаниях, обратным морфизмом или непокрытой веткой отвергается кодом, детерминированно, без разметки и без модели-судьи. Это готовый источник сигнала для обучения генератора спек (например, через GRPO), и ниже описан интерфейс, а не реализация обучения.

import { compile } from "@digitable/fts"
import { detectFallacies, ftsGate, loadManifest } from "@digitable-lol/fts-gate"

const manifest = loadManifest()          // грузится один раз, кэшируется

// Уровень 1. Только структура: не нужен ни контекст, ни библиотека морфизмов.
export function structuralPenalty(sample: string): number {
  let document
  try {
    document = compile(sample)
  } catch {
    return -1                             // синтаксис: сигнал есть и без детектора
  }
  return -detectFallacies(document, { manifest }).length
}

// Уровень 2. Весь гейт: одно число и код, по которому видно, что именно сломано.
export function gateReward(sample: string, context?: unknown): { reward: number; code?: string } {
  const result = ftsGate(sample, context)
  if (result.status === "certified") return { reward: 1 }
  return { reward: -1, code: result.code }
}

Свойства, из-за которых это работает как награда:

• разметка не нужна. Метка вычисляется из самого сэмпла;

• детерминированность. Один и тот же вход даёт один и тот же список находок в одном и том же порядке — награда воспроизводима между эпохами;

• дёшево. Проверки — проходы по разобранному документу; тяжёлых шагов нет;

• градуированность. detectFallacies возвращает список, а не булево: можно штрафовать по числу находок и по коду отдельно, а finding.explains даёт текстовое объяснение для reward-модели или для датасета исправлений;

• разделение уровней. detectDerivationFallacies и detectUtilityFallacies вызываются по отдельности, если нужно наградить только один слой.

И два предупреждения, без которых интерфейс легко применить не туда:

1. Награда обучает форме, а не истине. Генератор, максимизирующий этот сигнал, научится писать структурно безупречные спецификации — в том числе безупречно ложные. examples/password-mfa.fts набирает максимум по детектору. Единственный источник предметной истинности — ревью морфизмов в манифесте, и в награде он присутствует только как UNVERIFIED_MORPHISM, то есть как «взял закон из проверенного списка», а не «сказал правду».

2. Отсутствие находок — не подтверждение. Нулевой штраф означает «известные проверки промолчали», а не «ошибок нет» (docs/guarantees.md §2.4).

Тесты

npm test — 62 теста. На каждый код отказа минимум один, плюс успешные пути, детерминированность, независимость проверяющего и контрпример.

Лицензия

BSD 2-Clause — как и сам язык FTS, от которого проект наследует. Происхождение кода и материалов описано в NOTICE.