Понедельник, 19:30-22:00, Кочерга.
Дмитрий Волков, wldhx@wldhx.me (FB527CDAC1176535A4CF9B4C0E8CB6EC231EDDFE).
Изучаем математические законы за написанием надёжного софта с целью: делать лучше.
Баги. Баги баги баги баѓ̰̪̜̝͍̮ͅг̮̝͓̺̪г̫̗̣̯̟и̣̪̩ ̭̙͓̹̰ͅба̜͕̹͝г̯̬̗̝̹и̮͜ ̨̘̙͉б͘а̛̣͇̪͓аг̨̲̬͚̻̙̲и̬̝̫ ̺̗̰͟б͎̦͘а͈̼̲͓̀ͅг̺̜̼и̡. Делают жизнь программистов хуже, заставляют пользователей страдать, а когда в ракетах “Патриот” — убивают людей. Устранить! много методов: экстремальное программирование, паттерны, лучшие практики… Инженерия! не наука. Сложное, взаимосвязанное, собираемое из кусочков… математика! План: украсть всё у математиков!
Не написать тест — проверить три точки из всего пространства — а доказать теорему. Не “ну у меня вроде работает…”, а “Работает”. Сложнее; окупается для библиотек.
Конструктивная верификация — через инструменты доказательства — логических теорем. Из логики и элементов алгебры к программированию и обратно. Темы.
Формат: обычно мы будем проводить семинары по Logical Foundations. Когда какую-то тему захочется раскрыть дополнительно, я предложу другие материалы и/или расскажу лекцию. ДЗ будет объявляться после каждой встречи.
Слайды: http://nikolai.kosmatov.free.fr/publications/tutorial_2018_09_30_secdev2018.pdf (доп. источники здесь в References).
Сам Why3: http://proval.lri.fr/submissions/boogie11.pdf.
Верифицированный микрогипервизор и общий подход: https://uberspark.org/.
Дополнительные материалы:
Обсудили Jitk и мою работу с верифицированным интерпретатором в ядре: посмотрели, как пользоваться CertiCoq.
Рассмотренные программные коды находятся в https://github.com/PrincetonUniversity/VST, progs/{sumarray_verif.v,sumarray.{c,v}}.
Теория: Verifiable C, http://www.cs.princeton.edu/~appel/papers/vst.pdf.
К следующему разу: GamePad, DeepWeb, первые 10 глав Verifiable C.
Обсудили области труда: low-level (VST, Fiat/Crypto, CertiKOS, Kami), general-purpose prog (hs-to-coq), distributed sys (CRDT, Verdi), криптография (Easycrypt), ML (Reluplex, Gamepad), Why3; Coq без слёзок (ssreflect, cpdt, mathcomp).
akamaus рассказал о экспериментах в формализации матанализа.
grwlf рассказал о кокерах и спаниелях в Huawei, всем рекомендую.
К следующему разу: GamePad, полистать CPDT.
https://coq.inria.fr/distrib/current/refman/user-extensions/syntax-extensions.html
ДЗ - Imp до L1461.
Обсудили [Wadler 2015] “Propositions as types”.
ДЗ - IndProp, посмотреть Wadler, и ProofObjects.
ДЗ - задачи до строки 1100 (51%).
Обсудили IDE для Coq, @mrkun рассказал свои решения последней (*****) задачи в Logic, посмотрели часть CIC: The terms и Conversion rules, и закончили Logic разделом Coq vs. Set Theory.
let, если есть λ?Как определить кольцо? Или какую-нибудь алгебраическую структуру?
#goodfirsttheoremex_intro.natов, что universe inconsistency?Что такое Ε и Γ?
https://coq.inria.fr/distrib/current/refman/language/cic.html#typing-rules
Есть ли глубинное сходство ζ и линейных типов?
https://stackoverflow.com/questions/41837820/agda-like-programming-in-coq-proof-general
destruct и discriminate?:info
C-c C-a в PG.
Search, в т.ч. Search "_ + _".. Найти все определения с таким термом, такой подстрокой, или такой формы по паттерну.Locate, например Locate "+".. Найти соответствие нотации определениям.Print, например Print Nat.add.. Напечатать правую сторону определения. (C-w в company-mode).Хоткей ввести лемму
Категорически рекомендую company-coq. Он отвечает во всяком случае на первый и последний из этих вопросов (M-x company-coq-tutorial).
Фан: Machine Learning in Proof General: Interfacing Interfaces.
Обсуждался model checking интерфейсов по мотивам https://hillelwayne.com/post/formally-specifying-uis/.
Lists.baz -> False?Почему eqn в тактиках иногда делает хуже?
eqn в induction ломает индуктивную гипотезу.
https://stackoverflow.com/questions/31049657/in-coq-how-to-do-induction-n-eqn-hn-in-a-way-that-doesnt-mess-up-the-induct
Fixpoint, которая запрещает легальные функции?Можно ли синтезировать не только типы, но и Prop?
К этому семинару задание - дочитать Basics, прочитать Induction, и сделать все упражнения.
Если что-то не получится или будет непонятно - сформулировать это и спросить на встрече; задание сделано, если оно зелёненькое; проверить всё до курсора - Ctrl-→ в CoqIDE. Так можно прокликивать через каждую тактику.
С собой понадобится ноутбук с CoqIDE или Proof General.
Обсудили средства индустриальной верификации на спектре между мейнстримом (типами / “простым” статическим анализом) и конструктивной. С одной стороны, это генеративное / property-based тестирование (QuickCheck) → фаззинг (afl (+rr?)) → контракты и статический анализ (Frama-C), с другой - средства моделирования (Alloy, TLA+).
Посмотрели слайды: HACMS, Classical analysis with Coq.
Интересная экосистема - Why3.
http://spinroot.com/spin/whatispin.html
Вводный семинар. Можно не готовиться; понадобится ноутбук с CoqIDE или Proof General.
Что такое = в теоремах? (@philipb)
Ответ на этот вопрос — в цепочке Logic - IndProp - ProofObjects - IndPrinciples: перед тем, как его обсуждать, я бы хотел наработать прикладной скилл в Coq. Интересантам рекомендую PLFA (по нему тоже можно задавать вопросы); ещё есть мысль сделать reading group для более академических тем и рассказывать прочитанное на семинарах (много тем можно найти в Coq: credits).
Как проверять алгоритмическую сложность?
Можно ли верифицировать нечёткие вещи, типа нейронных сетей?
Что нужно закодировать (какого рода буквы написать), чтобы, например, доказать теорему о собственном значении матрицы?
Всю аксимотатику и все зависимости этой теоремы, точно как в учебнике по линалу. Также см. Coq wiki: as a teaching tool in mathematics.
Coq vs Agda
Agda проще / элегантнее / интуитивно консистентнее (например, в ней только один язык, а не четыре), но в Coq больше автоматизации: например, для похожих доказательств можно написать свои тактики. Поэтому для более индустриальных / прикладных доказательств удобен скорее он. To the best of my knowledge, это отражается и проектами в Coq / Agda: в Coq делают больше прикладных проектов, а в Agda более абстрактную математику / теорию типов. Интересантам рекомендуется PLFA.
Хочу практический пример на C++!
На семинаре 21 я больше расскажу про область верификации вообще и другие методы (кроме конструктивной), и покажу пару примеров.
Какие есть прикладные проекты? Это что, вот это всё прямо в продакшне?
Кроме ↑, имеет смысл посмотреть в вводные слайды CIS500: там примеры именно конструктивной верификации.
Coq очень классный! Как написать ещё такой?
А как работают числа? А отрицательные числа бывают? А с плавающей точкой? А hard float?
Когда я делаю destruct + rewrite, в некоторых теоремах получается гипотеза false = true. Этнорм?
Каковы границы применимости? Можно ли было, например, верификацией найти Meltdown - или он был бы корректным поведением в наших теоремах, и следствием несмоделированного эффекта?
Ааа я плаваю~
Рекомендую TAPL (Литература), и не забывать про интерактивность и пошаговое прокликивание. Если понятно математически, но непонятно, как донести до Coq, напишите доказательство по шагам на бумаге (и посмотрите примеры этого в книге).
Если что-то забыто — напишите на форум.
Форум: https://forum.kocherga.club/c/iacsv-19.
Чтобы получить доступ, напишите свой SSH-ключ и желаемый username мне на электронную почту (сверху).
Использование:
Через nix или cargo установить pijul.
ssh pijul@iacsv.kocherga.club работает. (Если нет — писать на почту или жаловаться на семинаре.)Зайти в свою директорию с Logical Foundations и закоммитить:
Запушить: pijul push pijul@iacsv.kocherga.club:$MY_USERNAME/lf (список, куда вообще можно пушить, можно посмотреть через (2))
Если (4) не работает — возможно, проблема в парсинге sshconfig. Достоверно известно, что если ключ лежит в ~/.ssh/id_rsa, всё работает. Можно пожаловаться на семинаре.
…ммм, а как смотреть скор? — Мы работаем над этим.
Я использую Emacs + Proof General, потому что без vim-кейбиндингов (CoqIDE) неудобно, и потому что он просто работает. Если вы умеете в emacs, (use-package proof-general), а если нет - см., например, этот tutorial (важны пункты <=5). Ключевое сочетание клавиш - C-C C-RET (выполнить до курсора).