TheReefink

любительская исследовательская группа, занимающаяся детерминированными, доказанными машиной расширениями для локальных ИИ-помощников · ghillie, сам коготь →

Мы собираемся безопасно мутировать наши когти — детерминированно — и строить инструменты, расширяющие их досягаемость, с доказанным кодом. Любительская исследовательская группа, в радиолюбительском смысле: наши собственные машины, наши собственные доказательства, ничего, что просило бы доверия. Why organisation beats brain size →

Люди говорят, чего хотят.

Когти служат.

Когти решают, как меняться, и сотрудничают, чтобы это сделать.

Эксперимент открывает результаты.

Все выигрывают, и все предоставляют вычислительную мощность.

Три правила

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

Станьте частью этого — заново выведите своё первое доказательство сегодня

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

1. Получите доказчик. Бесплатная цепочка инструментов GNAT FSF — она несёт доказчик SPARK и инструменты сборки в одном пакете:

https://github.com/alire-project/GNAT-FSF-builds/releases
  (gnatprove-x86_64-linux, -darwin, or -windows64 — unpack anywhere)

Одного этого пакета достаточно для шага 3, повторного вывода доказательства. Его недостаточно для шага 4, сборки фронта: в нём есть gcc и ld, но нет среды выполнения C и стартовых объектов, поэтому на машине, где их нет, сборка проваливается после того, как доказательство уже снялось, — худший из возможных моментов для обнаружения недостающей части. Вам также понадобятся binutils и libc6-dev. Это обычные инструменты сборки любой Linux-системы, уже присутствующие почти на любой машине, используемой для разработки; без них остаётся разве что голый контейнер или свежая минимальная установка. На Debian и Ubuntu:

sudo apt-get install binutils libc6-dev
# Fedora/RHEL: the equivalents are binutils and glibc-devel

2. Получите стартовое расширение. Настоящее решающее ядро — brief-fill policy, решающее, когда помощник может отвечать от имени своего владельца, — поставляется в виде исходного кода с его доказательством и полной таблицей истинности:

brief-fill-policy.tar.gz (6 918 байт)
sha256: 14bb06671459784d2d571e7b5e2afc3037894c241517612b026dbe053fb6b180

Это тот же файл, по тому же адресу, который называет индекс каталога и который проверяет ваш ghillie — один артефакт, поэтому эта страница и машина не могут разойтись во мнениях. Вся полка — на странице каталога.

3. Заново выведите доказательство. Из распакованного пакета:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2
# success: "0 unproved" — four named theorems, discharged on YOUR machine:
#   NEVER-FILLED-WITHOUT-A-LICENSING-RULE
#   AN-ABSENT-STORE-NEVER-LETS-A-FILL-THROUGH
#   NOTHING-INVENTED-EVER
#   NOTHING-ASKED-THAT-A-RULE-ALREADY-ANSWERS

4. Попробуйте это сломать. Отредактируйте исходный код так, чтобы отсутствующее хранилище правил пропускало ответ, и запустите доказчик снова. Он откажет — назвав именно ту теорему, которую вы предали. Этот отказ и есть вся модель безопасности, и вы только что увидели, как она работает, никому не доверяя. Затем соберите фронт и проверьте каждую строку его выданной таблицы истинности (core/REPROVE.md в пакете проведёт вас через это).

Цель

Достичь положения, в котором наша изобретательность и сотрудничество делают наши токены и наше рассуждение наилучшими из доступных — и каждого участника фактически сверхбогатым. Богатым в той валюте, что здесь имеет значение: доказанное рассуждение накапливается как библиотека, а не как пирог — каждое добавленное ядро делает каждого участника богаче за ничей счёт, пока коготь обычного участника не станет командовать большей проверяемой способностью, чем можно арендовать за деньги.

Почему работа названа в честь Ву

Единица работы фабрики — одно доказанное правило, выкованное из простого предложения — называется Ву, в честь Chien-Shiung Wu.

В 1956 году Chen-Ning Yang и Tsung-Dao Lee задали великолепный вопрос — отличает ли природа левое от правого? — который почти никто не считал достойным задавания. Именно эксперимент Ву — её конструкция, её установка, её измерение — на него ответил. Нобелевская премия в следующем году досталась только теоретикам. Вопрос заслуживал своей премии; ответ — тоже, и ответ был оставлен за бортом.

Обе половины этой истории живут здесь. Смелый вопрос, прямо заданный, — это то, с чего начинается каждая часть нашей работы — мы чтим Яна и подражаем ему. Но мы называем единицу работы в честь Ву, потому что работа — это доказательство: не идея, не объявление — продемонстрированный, проверяемый результат. И мы называем её в честь неё публично, потому что знаем, как легко стирается тот, кто проводит демонстрацию, и здесь этого не случится.

Что впереди

Терминал — коготь, которому служат эти расширения: локальный помощник без слушателя и без входящего пути (он опрашивает наружу; ничто не достигает внутрь), а важные решения — каждое за доказанным ядром. Открытый исходный код (AGPL-3.0) — выпущен: исходный код и бинарники на github.com/the-dark-factory/Ghillie_AGPL. Проверьте бинарники перед запуском: релиз несёт SHA256SUMS-assets.txt, который охватывает тарболы точно в том виде, в каком они скачаны, поэтому sha256sum -c SHA256SUMS-assets.txt проверяет их как есть. (Старый SHA256SUMS всё ещё там для тех, кто на него ссылался; он перечисляет дайджесты распакованных бинарников в формате с префиксом платформы, который sha256sum -c прочитать не может.)
The catalogue is live — работающий ghillie устанавливает расширения, которые заново доказываются на его собственной машине: ghillie -catalogue https://thereef.ink/catalogue -abilities-available, затем -get-ability <name> -reprove. Ничто не устанавливается, пока его доказательство сначала не снимется на вашем железе.
The catalogue — больше расширений, заново выводимых в той же форме: тихие часы, потолки расходов, гранты на контакты, правило рта (отказы никогда не перефразируются), у каждого — свои названные теоремы.
Кооператив — общие журналы пробелов, благодаря которым записанное слепое пятно одного когтя становится прозорливостью каждого когтя, и объединённая работа над доказательствами: доказывание — единственная нагрузка, которую можно безопасно принять от незнакомцев, потому что снятие либо заново выводится, либо нет.

Отчёты

Запустили доказательство? Что-то вежливо сломали? Нашли скучный результат? Пишите на tonythegair@gmail.com. Находки публикуются; больше о вас ничего не спрашивают — у этой страницы нет скриптов, куки и аналитики, что можно проверить, прочитав её. Машина, которая отдаёт вам страницу, всё же хранит одну короткую, усечённую строку на каждый запрос, и прямо об этом говорит: что записывает сервер.

Патронаж

TheReefink патронирует The Dark Factory Ltd, которая выделила значительные ресурсы на её успех — доказывающую машинерию, первые расширения и грядущий терминал. Патронаж не покупает никаких исключений: всё, что патрон выпускает здесь, проверяемо по тому же правилу, что и всё остальное, а участник, который вежливо это нарушит, окажет группе услугу.