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.

Компоненты

Путь	Назначение
src/gate.ts	ftsGate(spec_source, context, options) -> GateResult
src/fallacies.ts	детектор структурных логических ошибок: detectFallacies(document, options) -> FallacyFinding[]
src/manifest.ts	загрузка и валидация библиотеки морфизмов, проверка композиции derived
src/cli.ts	fts-gate check / fts-gate morphisms
src/mcp.ts	MCP-сервер: fts_gate_check, fts_morphisms_list
morphisms/	.fts-модули доменных аксиом + manifest.json
grammars/fts.gbnf	GBNF-грамматика для constrained decoding
examples/	успешные пути, контрпример, фикстуры каждого отказа
examples/fallacies/	по фикстуре на каждый код детектора, с разбором ошибки в шапке файла
scripts/scan-fallacies.mjs	npm run fallacies:scan — прогон детектора по всему корпусу .fts

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

---

Коды отказа

Код	Что не удалось	Дополнительные поля
PARSE_ERROR	разобрать поверхностный синтаксис	diagnostics
TYPE_ERROR	проверить сигнатуру: имена, типы полей, операнды, типизация apply/compose	diagnostics
UNVERIFIED_MORPHISM	снять предпосылку: морфизма нет в манифесте, он proposed, либо его сигнатура подменена	missing_morphisms
PROPERTY_VIOLATION	исполнить примеры без нарушений: расхождение с ожидается или нарушение блока свойство	failures
CERTIFICATE_ERROR	построить сертификат: witness не разрешился по пути или не совпал со значением (а также нехватка свидетельства при requireEvidence)	diagnostics
VERIFICATION_ERROR	подтвердить сертификат независимой перепроверкой	—
MANIFEST_ERROR	загрузить библиотеку морфизмов: нет source у verified, derived не композируется, дубли, опора на proposed	—
INTERNAL_ERROR	что-либо непредвиденное; гарантирует отсутствие исключений наружу	—

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

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

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

Код	Что не удалось	Каталог	Глава
CIRCULAR_PREMISE	получить независимое основание: петля dom(m) = cod(m), цепочка вывода, вернувшаяся к своему начальному типу, или цикл в derived_from	№10	08, «Проверка графом оснований»
NON_EXHAUSTIVE	покрыть разбираемое поле: непокрытая полярность признака или ограниченный промежуток между порогами	№8	08, §6
EQUIVOCATION	удержать один смысл за идентификатором: поле с двумя типами, закон с двумя сигнатурами	№23, №31	08, §15
REVERSED_MORPHISM	применить морфизм в объявленную сторону: P → Q, Q ⊢ P или обращение закона библиотеки	№15, №33	06, §1 и §3
EXAMPLE_AS_PROOF	опереть свойство на примеры, задевающие все ветки правил	№2	09
VACUOUS_MORPHISM	найти населённый домен: witness такого типа построить нечем	№66	06, §13
UNDECLARED_BOUNDARY	определить поведение ровно на пороге: два правила срабатывают в одной точке	№30	08, §7
REIFICATION	различить вещь и высказывание о вещи: объект несёт сам себя как состояние	№49	08, §20

Отказ детектора означает отказ в сертификации, а не ложность содержания (каталог №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.

Уровень доверия	Смысл	Допустим как предпосылка
verified	проверено человеком, обязательна ссылка source на документ ревью или внешний источник	да
derived	выведено из verified типизированной композицией; цепочка проверяется механически	да
proposed	предложено моделью, не проверено (или проверено и отклонено)	нет

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

Записи 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 теста. На каждый код отказа минимум один, плюс успешные пути, детерминированность, независимость проверяющего и контрпример.

Тест	Проверяет
PARSE_ERROR	незакрытая кавычка-ёлочка
TYPE_ERROR	синтаксически безупречное правило со ссылкой на необъявленное поле
UNVERIFIED_MORPHISM / not_in_manifest	корректно типизированный морфизм, которого нет в библиотеке
UNVERIFIED_MORPHISM / signature_mismatch	подмена домена под проверенным именем
UNVERIFIED_MORPHISM / proposed	контрпример: пароль засчитан как второй фактор
PROPERTY_VIOLATION / property_violated	правила на 15 % + 10 % против свойства «не больше 20 %»
PROPERTY_VIOLATION / example_mismatch	пример ожидает 3000, правила дают 2000
CERTIFICATE_ERROR	requireEvidence против trivial и symbolic сертификатов
MANIFEST_ERROR	verified-запись без source
успешный путь	apply с одним морфизмом; compose с двумя; дайджесты; assumptions
независимость проверяющего	подделанный и переподписанный сертификат отвергается
устойчивость	ftsGate не бросает исключение ни на одном мусорном входе
CIRCULAR_PREMISE	петля dom = cod; цепочка A → B → C → A; цикл в derived_from
REVERSED_MORPHISM	witness со стороны кодомена; обратное направление закона библиотеки
VACUOUS_MORPHISM	морфизм с ненаселённым доменом при объявленной теореме
EQUIVOCATION	поле «сумма» как деньги и как строка; один закон с двумя сигнатурами
REIFICATION	объект, несущий сам себя как состояние
NON_EXHAUSTIVE	промежуток (50000, 100000) между порогами; непокрытая полярность признака
UNDECLARED_BOUNDARY	два правила, срабатывающие ровно при сумме 1000
EXAMPLE_AS_PROOF	свойство при правиле, не задетом ни одним примером
негативы детектора	по одному «промаху мимо дефекта» на каждый код: смежные пороги, одиночное правило поверх умолчания, широкое перекрытие, одинаковые типы поля, носитель с отдельным именем
весь корпус чист	ни одна проверенная спека репозитория не даёт находки
№67 «Ошибка ошибки»	ни один отказ не содержит слов «ложно», «неверно» и синонимов; verdict на месте
канарейка	вендорный парсер по-прежнему выдаёт диагностику, из которой читается обратное применение

---

Лицензия

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