# fts-gate

Верификационный гейт поверх [FTS](https://github.com/digitable-lol/fts) — языка исполняемых
спецификаций. Ключевое свойство: **отказ является следствием типовой ошибки, а не
решением языковой модели.**

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

Границы гарантии описаны предельно честно в **[docs/guarantees.md](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`](https://github.com/digitable-lol/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](docs/guarantees.md).

Отключается опцией `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`](docs/morphism-review.md): по разделу на закон, с тем,
что именно проверено и чего закон не утверждает.

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

> **Рабочий набор доменных морфизмов Digitable в этот репозиторий не входит.**
> `.fts`-модули с реальными правилами живут в закрытом репозитории и подключаются
> к гейту через `manifestPath` / `manifest` или через собственный каталог
> `morphisms/`.
>
> Здесь опубликованы только **схема** библиотеки — формат `manifest.json`, его
> валидация в `src/manifest.ts` и проверка композиции `derived` — и **один
> нейтральный пример модуля**, [`morphisms/access-control.fts`](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`](https://github.com/digitable-lol/fts).

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

### Сборка

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

### Библиотека

```ts
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

```bash
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

```json
{
  "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](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), и ниже описан
интерфейс, а не реализация обучения.

```ts
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`](NOTICE).