TheReefink

аматорська дослідницька група, що займається детермінованими, доведеними машиною розширеннями для локальних ІІ-помічників · ghillie, сам кіготь →

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

Три правила

1. Ніщо не просить довіри. Кожне твердження, на яке покладається учасник, повинне бути таким, яке він міг би заново вивести сам: доведення, дайджест, таблиця істинності. «Так каже супровідник» — це не та категорія, якою ми користуємося.
2. Відмови — це знахідки. Доведення, яке не знімається, сховище, яке неможливо прочитати, чесно зафіксована прогалина — це система, що працює як слід, і це записується, а не згладжується. Нудний звіт — воно зробило рівно те, що казали його теореми, знову — теж знахідка.
3. Власник завжди старший за кіготь за званням. Розширення вирішують; вони ніколи не набувають повноважень. Жоден експеримент цього не змінює, хоч би що він довів.

Станьте частиною цього — заново виведіть своє перше доведення сьогодні

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

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, яке вирішує, коли помічник може відповідати від імені свого власника, — постачається у вигляді джерельного коду з його доведенням і повною таблицею істинності:

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, яка виділила значні ресурси на її успіх — доводчу машинерію, перші розширення і термінал, що прийде. Патронаж не купує жодних винятків: усе, що патрон випускає тут, перевірне за тим самим правилом, що й усе інше, а учасник, який ввічливо це порушить, зробить групі послугу.