Ваше первое доказательство

десять минут · три шага · ничего, что нужно принимать на веру

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

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

Что вы сейчас проверите

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

• оно никогда не заполняет ответ без правила, которое это разрешает;
• если хранилище правил отсутствует, ничего не проходит;
• оно никогда ничего не изобретает;
• оно никогда не спрашивает у вас то, на что уже отвечает правило.

Это не обещания из блог-поста. Это теоремы, и доказчик сейчас попытается их опровергнуть.

Шаг 1 — получите доказчик

Это бесплатно, и это не наше — это приходит из сообщества Ada, а не от нас. В этом и суть: то, что проверяет нашу работу, не должно быть тем, что вручили вам мы. Одна честная оговорка насчёт «десяти минут»: отсчёт начинается после того, как это скачается, а весит это несколько сотен мегабайт — быстро на хорошей линии, медленнее на плохой.

Шаг 2 — получите правило

При первом запуске вы можете проигнорировать контрольную сумму — доказательство в шаге 3 от неё не зависит. Она нужна, когда вы захотите подтвердить, что полученный вами файл — это тот файл, который опубликовали мы, и что это тот же файл, который называет каталог.

Шаг 3 — попросите свой компьютер проверить это

Откройте терминал в распакованной папке и выполните две строки:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

Подождите. Когда всё завершится, найдите эти два слова:

0 unproved

Вот и всё. Это всё упражнение целиком. Ничего больше устанавливать не нужно, и этот шаг работает на обычной машине, на которой больше ничего нет — доказчик, который вы скачали, несёт всё, что нужно доказательству.

Что только что произошло

Ваш компьютер взял четыре утверждения выше, попытался найти случай, при котором хоть одно из них не выполняется, и не смог — потому что такого случая нет. Не «мы это протестировали, и вроде всё в порядке». Не «так говорит сопровождающий». Машина, которую нельзя уговорить, искала контрпример и вернулась ни с чем.

Вы не поверили нам на слово, что это так. Вы увидели, как это происходит, на железе, которое принадлежит вам.

Дополнительно — сломайте это нарочно

Это стоит сделать, если у вас есть ещё пять минут, потому что проверка, которая всегда говорит «да», немногого стоит.

Откройте brief_fill_policy_pkg.ads в любом текстовом редакторе и измените правило так, чтобы отсутствующее хранилище всё равно пропускало ответ. Запустите ту же команду снова. Она откажет — и назовёт именно ту теорему, которую вы только что сломали.

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

Чего это не доказывает

Мы лучше скажем это сейчас, чем позволим вам обнаружить это позже. Доказательства охватывают правила принятия решений — кто может видеть что, что может уйти, что должна пройти каждая доставка. Они не делают волшебным остальное программное обеспечение, и мы не утверждаем обратного. Эта честность и есть сделка, и это вся сделка.

Куда двигаться дальше

• Полное руководство — соберите фронт и проверьте каждую строку его выданной таблицы истинности.
• Каталог — остальная часть полки, каждая деталь заново выводима тем же способом.
• Ghillie — помощник, которому служат эти правила.
• Машина Рифа — какое железо вам понадобится, если вы захотите пойти дальше этой страницы.

Если не сработало — это находка, и нам хотелось бы о ней услышать. Отказ, который вы не можете объяснить, интереснее нам, чем успех.