Доказательства: теоремы, сертификаты и научные границы

Код в этой главе записан в прежней поверхности языка — со словами категория, объект, утилита. Сегодняшний компилятор её слова читает, но программой такой файл не считает: файл, где есть только утилиты, flang check отклоняет. Разбор задачи в главе верен; синтаксис переносится по таблице из главы «Старые модели».

Это самый тонкий модуль курса. Слово «доказательство» здесь означает не то, что обычно слышит бизнес-заказчик: FTS не устанавливает истинность бизнес-закона, а проверяет две вещи — что заявленный факт действительно найден в данных по однозначному пути и что цепочка морфизмов типизируется. Всё остальное — предпосылки, и они выписываются явным списком. Формулировка «FTS доказал, что заказ можно отгружать» неверна. Верная формулировка: «FTS проверил свидетельство и типизируемость вывода при условии объявленных законов».

Минимальный пример (теорема)

категория «Исполнение заказа»

  объект Заказ
    номер является строкой
    клиент является строкой
    оплачен является признаком
    «склад подтвердил» является признаком
    «готов к отгрузке» является состоянием «Готов к отгрузке»

  морфизм «Готовый заказ можно отгрузить»
    если «Готов к отгрузке»
    то «Отгрузить заказ разрешено»

  теорема «Заказ ЗК-7781 можно отгрузить»
    дано Заказ имеет «готов к отгрузке» равное да
    в данных заказы найти где номер равен «ЗК-7781»
    по морфизму «Готовый заказ можно отгрузить»
    следовательно «Отгрузить заказ разрешено»

Контекст — обычный JSON-снимок данных, не часть модели:

{
  "заказы": [
    {
      "номер": "ЗК-7781",
      "клиент": "ООО Маяк",
      "оплачен": true,
      "склад подтвердил": true,
      "готов к отгрузке": true
    }
  ]
}

Что делает компилятор

compile превращает поверхность в канонический документ и уже на этом шаге отклоняет часть ошибок. Теорема разворачивается в пропозицию:

{
  "kind": "apply",
  "functor": "Готовый заказ можно отгрузить",
  "arg": {
    "kind": "witness",
    "structure": "Заказ",
    "field": "готов к отгрузке",
    "selector": { "номер": "ЗК-7781" },
    "value": true,
    "path": ["заказы", { "номер": "ЗК-7781" }, "готов к отгрузке"]
  }
}

Парсер русской поверхности проверяет: существует ли поле, существует ли морфизм, совпадает ли домен морфизма с типом текущего шага и совпадает ли объявленное следовательно с вычисленным кодоменом. Все четыре проверки — синтаксические и ссылочные; данных на этом этапе ещё нет. validate дополнительно контролирует имена, дубликаты и ссылочную целостность, но не пересчитывает цепочку типов: для русской поверхности это уже сделано парсером, а для канонического JSON, полученного другим способом, — построителем сертификата.

Пропозиция, witness и тип

Соответствие Карри — Ховарда читается так: тип — это утверждение, терм этого типа — доказательство утверждения. prove печатает обе стороны. Реальный вывод на модели выше:

{
  "curry_howard": {
    "proposition": "Готовый заказ можно отгрузить(Π (x:Заказ). готов к отгрузке(x))",
    "witness": "Готовый заказ можно отгрузить (λx. π_готов к отгрузке(x))"
  },
  "categorical": {
    "category": "Исполнение заказа",
    "morphism": "Готовый заказ можно отгрузить ∘ π_готов к отгрузке",
    "domain": "Заказ",
    "codomain": "Type"
  },
  "path": ["заказы", { "номер": "ЗК-7781" }, "готов к отгрузке"]
}

Разбор записи Готовый заказ можно отгрузить(Π (x:Заказ). готов к отгрузке(x)):

• Π (x:Заказ). готов к отгрузке(x) — утверждение «для заказа x определено поле готов к отгрузке объявленного типа». Это утверждение о наличии свидетельства, а не о том, что все заказы готовы к отгрузке;
• λx. π_готов к отгрузке(x) — witness этого утверждения, проекция поля. Свидетельство здесь буквально: конкретное значение по конкретному пути;
• внешнее применение — это применение морфизма к witness, то есть обычная аппликация функции к аргументу. Тип результата — кодомен морфизма.

Две оговорки, без которых запись переоценивается. Первая: строка с Π и λ — читаемая нотация вывода, а не терм проверенного ядра с зависимыми типами; FTS не реализует нормализацию и не проверяет λ-термы. Равенство типов — номинальное, по имени: «Готов к отгрузке» совпадает с «Готов к отгрузке» и не совпадает ни с чем другим. Вторая: поле codomain в выводе prove равно строке Type, а не типу заключения. Настоящий тип заключения появляется только в сертификате, в поле conclusion.type — там это «Отгрузить заказ разрешено».

Морфизмы и композиция

Категорная часть минимальна и от этого честна. Объекты — типы (Заказ, «Готов к отгрузке», «Отгрузить заказ разрешено»). Морфизм — стрелка A → B с именем и объявленным законом. Композиция — последовательное применение стрелок при совпадении кодомена предыдущей с доменом следующей.

Это именно морфизмы, а не функторы: функтор отображал бы категорию целиком, вместе с её объектами и стрелками, и сохранял бы композицию. Отдельный переход A → B внутри одной категории функтором не является. В каноническом JSON поле исторически называется functors, а шаг сертификата — apply с полем functor; это наследие первой версии wire format, зафиксированное в документации языка. Поверхность (морфизм) и терминология исследования исправлены, публичное API отдаёт представление morphisms() над тем же полем, а миграция формата будет версионированной.

Композиция двух морфизмов на модели credit-limit.fts даёт такой вывод prove:

{
  "curry_howard": {
    "proposition": "(Пройденный скоринг открывает риск-проверку ∘ Успешная риск-проверка разрешает лимит) Π (x:Заявка на лимит). скоринг пройден(x)"
  },
  "categorical": {
    "morphism": "Пройденный скоринг открывает риск-проверку ∘ Успешная риск-проверка разрешает лимит",
    "domain": "Заявка на лимит",
    "codomain": "Type"
  }
}

Здесь есть ловушка чтения: в форме compose цепочка печатается в порядке объявления, слева направо, тогда как математическое ∘ читается справа налево. В форме apply (одиночный морфизм) порядок как раз стандартный: Готовый заказ можно отгрузить ∘ π_готов к отгрузке. Порядок фактического применения задаётся списком functors в документе, а не отрисованной строкой.

Symbolic derivation

Важная деталь, которую легко принять за баг. prove возвращает одинаковый результат с контекстом и без него: путь, пропозиция и witness выводятся из документа, а не из данных. Контекст влияет только на одно — при несовпадении значения prove бросает FTS_WITNESS_MISMATCH. То есть отсутствие ошибки от prove без контекста ничего не говорит о данных.

Точный контракт prove: он проверяет, что документ валиден и что путь свидетельства разрешается однозначно в ожидаемое значение. Типизируемость цепочки он заново не пересчитывает — она проверена компилятором при разборе теоремы и будет проверена ещё раз при построении сертификата.

Символическая деривация — это схема вывода: «если существует заявленный witness и верны объявленные законы, то заключение типизируется». Она полезна на этапе проектирования модели и бесполезна как основание для действия. В сертификате такому объекту присваивается статус symbolic, и в assumptions добавляется строка вида symbolic witness Заказ.готов к отгрузке : Готов к отгрузке.

Verified certificate

certify строит сертификат, verify независимо его перепроверяет:

fts check order-shipment.fts
fts certify order-shipment.fts --context order-shipment.context.json --pretty > proof.json
fts verify order-shipment.fts --context order-shipment.context.json --certificate proof.json

Сертификат на модели и снимке из первого раздела:

{
  "version": "fts-proof/1",
  "category": "Исполнение заказа",
  "status": "verified",
  "document_digest": "sha256:955d7f5d91674d9048a61dd2feedd28a76ae1aec70b3a3f4f8049383761a9829",
  "assumptions": [
    "Готовый заказ можно отгрузить : Готов к отгрузке → Отгрузить заказ разрешено [morphism.declared]"
  ],
  "steps": [
    {
      "rule": "witness",
      "structure": "Заказ",
      "field": "готов к отгрузке",
      "type": "Готов к отгрузке",
      "path": ["заказы", { "номер": "ЗК-7781" }, "готов к отгрузке"],
      "verified": true,
      "expected": true,
      "actual": true,
      "evidence_digest": "sha256:2b3351538d544658fcb6b9e59d8fc42e7de7593446c3303d8687f7d8ede15fae"
    },
    {
      "rule": "apply",
      "functor": "Готовый заказ можно отгрузить",
      "domain": "Готов к отгрузке",
      "codomain": "Отгрузить заказ разрешено",
      "law": "morphism.declared"
    }
  ],
  "conclusion": {
    "type": "Отгрузить заказ разрешено",
    "term": "Готовый заказ можно отгрузить(witness(Заказ.готов к отгрузке))"
  },
  "context_digest": "sha256:d0dc722124c5464cd0ccd5106f90fb9ed5da94be218e384488b13a287ff3096d",
  "certificate_digest": "sha256:58334701b7ba867d545524c5b6e0a6f4659bc288751f4c7a90a0fa3d0e73de68"
}

Статус verified присваивается, только если каждый witness разрешён в контексте и фактическое значение совпало с ожидаемым. Закон морфизма при этом остаётся в assumptions — сертификат не утверждает его, а перечисляет.

Digest считается не по тексту JSON, а по канонической форме: ключи объектов сортируются по кодовым единицам UTF-16, порядок массивов сохраняется, нечисловые значения, бесконечности и отрицательный ноль отвергаются. Поэтому перестановка ключей в исходном снимке даёт тот же context_digest и тот же certificate_digest — это проверяется экспериментально и является требованием воспроизводимости, а не деталью реализации.

Что происходит при подмене. verify не сравнивает строки, а заново строит вывод из документа и контекста, заново считает все дайджесты и сверяет их с присланными. Изменение любого байта данных, попадающего в канонический снимок, меняет context_digest, а через него — certificate_digest, и проверка даёт valid: false с расхождением expected_digest и actual_digest. Обратите внимание: поле status в результате проверки описывает заново построенный вывод, а не присланный сертификат. Строгий режим (assertVerified, команда fts verify) дополнительно требует status = verified и отклоняет символический сертификат с кодом FTS_CERTIFICATE_SYMBOLIC.

certify и verify используют node:crypto и в браузерную сборку не входят. Песочница на сайте умеет только prove: получить сертификат в браузере нельзя по устройству пакета. Это осознанное архитектурное ограничение — выпуск сертификата и авторизация действия относятся к доверенной серверной границе.

Что это НЕ доказывает

• Истинность бизнес-закона. если «Готов к отгрузке» то «Отгрузить заказ разрешено» — предпосылка, а не теорема. FTS доказывает утверждение относительно списка assumptions, и убрать этот список нельзя.
• Полноту модели. Морфизм не знает про санкционные списки, блокировку клиента и просрочку. Верный вывод по неполной модели остаётся верным выводом по неполной модели.
• Актуальность снимка. Сертификат связан с состоянием данных на момент выпуска. Между verify и фактической отгрузкой мир может измениться.
• Авторство. SHA-256 связывает артефакты, но не удостоверяет, кто их выпустил; для этого нужна цифровая подпись сертификата, которой в текущей версии нет.
• Отсутствие дефекта в реализации. Доверенная база — нормализатор, правила ядра, канонизатор и verifier. Ошибка в них не обнаруживается сертификатом.
• Богатую систему типов. Равенство типов номинальное; параметрических и зависимых типов нет.

Отдельно про научный и патентный статус. В исследовательских материалах проекта метасвойства (детерминированность разрешения пути, единственность типа вывода, сохранение типов, завершаемость проверки, относительная корректность, обнаружение модификации сертификата) сформулированы и доказаны индукцией — но для публикационного уровня этого недостаточно. Нужен отдельный формальный слой: операционная семантика, typing judgments, выбранные safety-свойства с доказательствами, reference implementation, репликационный пакет и benchmark.

Для патента ситуация строже. Нельзя заявлять как новое ни соответствие Карри — Ховарда, ни категорную композицию, ни статическую типизацию, ни JSON Schema, ни криптографический хеш, ни proof-carrying code, ни вызов инструментов агентами. Потенциально охраноспособной может быть конкретная совокупность признаков и достигаемый технический результат, а вывод о новизне допустим только после патентного и библиографического поиска. Публичное раскрытие до подачи заявки в ряде юрисдикций разрушает новизну, поэтому корректный порядок — поиск уровня техники, консультация патентного поверенного, подача, публикация. Сертификат FTS — хороший объект исследования и machine-checkable evidence, но не патентная экспертиза.

Практика в песочнице

Одиночный морфизм и разбор вывода prove:

Композиция двух морфизмов — сравните morphism и порядок применения:

Диаграмма той же категории — объекты и стрелки без доказательной части:

Напомним: в песочнице доступен только prove. Полей status, assumptions и дайджестов там нет — они появляются в выводе fts certify в Node.js.

Типичные ошибки

• FTS_WITNESS_MISMATCH — «witness does not match context at заказы[номер="ЗК-7781"].готов к отгрузке: expected true, got false». Свидетельство найдено, но значение другое. Это не ошибка модели: она означает, что по данным заказ отгружать нельзя.
• FTS_WITNESS_MISMATCH с got <missing> — путь не разрешился. Три разных причины дают одно сообщение: элемента нет, корневой ключ назван иначе, либо селектор совпал более чем с одним элементом. Реализация требует ровно одного совпадения, поэтому дубликат номера в снимке выглядит как отсутствие данных.
• FTS_PROOF_TYPE_MISMATCH — «морфизм «Оплаченный заказ можно отгрузить» ожидает «Оплата подтверждена», получено «Готов к отгрузке»». Возникает уже при компиляции, до всяких данных.
• FTS_UNKNOWN_FUNCTOR — «не найден морфизм «…»»: теорема ссылается на стрелку, которой нет в категории.
• FTS_THEOREM_CONCLUSION — «теорема объявляет «Счёт можно выставить», но вывод имеет тип «Отгрузить заказ разрешено»». Объявленное заключение не совпало с кодоменом последнего морфизма.
• FTS_CERTIFICATE_SYMBOLIC — строгая проверка получила сертификат без подтверждённого свидетельства.
• FTS_CERTIFICATE_MISMATCH — сертификат не соответствует документу и контексту: изменились данные, модель или сам сертификат.

Чек-лист

1. Заключение теоремы совпадает с кодоменом последнего морфизма — иначе модель не скомпилируется.
2. Селектор свидетельства выбирает ровно один элемент; в снимке есть устойчивый идентификатор.
3. Для решения о действии используется fts verify со статусом verified; symbolic действие не разрешает.
4. Список assumptions прочитан вслух и принят ответственным за бизнес-правило, а не разработчиком.
5. Вместе с решением сохранены исходник, контекст и сертификат — иначе проверку нельзя повторить.
6. В формулировках для заказчика вместо «доказано, что заказ можно отгрузить» говорится «проверено свидетельство и типизируемость вывода при условии объявленных законов».

Кейсы каталога по этой теме

Дальше: интеграция с любым языком