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 и привилегированный доступ), чтобы формат было на чём показать.

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

Объявить его в .fts-модуле в morphisms/ вместе с по закону «id».
Добавить запись в manifest.json с той же сигнатурой и полем source.
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 вызываются по отдельности, если нужно наградить только один слой.

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

Награда обучает форме, а не истине. Генератор, максимизирующий этот сигнал, научится писать структурно безупречные спецификации — в том числе безупречно ложные. examples/password-mfa.fts набирает максимум по детектору. Единственный источник предметной истинности — ревью морфизмов в манифесте, и в награде он присутствует только как UNVERIFIED_MORPHISM, то есть как «взял закон из проверенного списка», а не «сказал правду».
Отсутствие находок — не подтверждение. Нулевой штраф означает «известные проверки промолчали», а не «ошибок нет» (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.

Navigation Menu

Uh oh!

Repository files navigation

fts-gate

Архитектура

Компоненты

Коды отказа

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

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

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

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

Подключение

Требования

Сборка

Библиотека

CLI

MCP

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

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

Тесты

Лицензия

About

Releases

Packages

Contributors

Languages

Name		Name	Last commit message	Last commit date
docs		docs
examples		examples
grammars		grammars
morphisms		morphisms
scripts		scripts
src		src
test		test
.gitignore		.gitignore
LICENSE		LICENSE
LICENSE-RU.md		LICENSE-RU.md
NOTICE		NOTICE
README.md		README.md
package-lock.json		package-lock.json
package.json		package.json
tsconfig.json		tsconfig.json

Uh oh!

Latest commit

History

Folders and files

Repository files navigation

fts-gate

Архитектура

Компоненты

Коды отказа

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

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

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

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

Подключение

Требования

Сборка

Библиотека

CLI

MCP

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

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

Тесты

Лицензия

About

Resources

Stars

Watchers

Forks

Releases

Packages

Contributors

Languages