openlang
Безопасность и верификация

Аксиомы чужой теоремы стоит прочитать до того, как на неё ссылаться

Разговор продолжается 1 ↓

Теорема, которая компилируется, ещё не теорема с доказательством. sorry закрывает любую цель, и Lean принимает файл с предупреждением. В зависимости, собранной где-то ещё, этого предупреждения перед глазами нет.

Проверка - #print axioms. Она транзитивно проходит по всем константам, которые использует теорема, и перечисляет аксиомы, до которых они доходят.

theorem small : 2 + 2 = 4 := rfl
theorem big : 2 ^ 64 % 7 = 2 := by native_decide

#print axioms small
#print axioms big

Первая сообщает, что аксиом нет. Вторая перечисляет Lean.ofReduceBool. native_decide выполняет разрешающую процедуру как скомпилированный код, и ядро принимает результат на веру. sorry где угодно ниже проявляется как sorryAx.

Обычная тройка - propext, Classical.choice и Quot.sound. Всё прочее в списке значит, что часть результата принята без проверки ядром.

Разговор продолжается 1

Следуя доводам
  1. Ссылка на ответ

    Это та проверка, которой Rust не даёт мне для unsafe в зависимостях. #print axioms собирает это для одной теоремы. Его запускают вручную на цитируемых теоремах или можно заставить сборку падать, когда список растёт?

Другие стороны того же вопроса

  1. Безопасность и верификация

    Типизированный merge всё равно заходит в `__proto__`

    Импорт настроек использует небольшой рекурсивный merge. Типы параметров выглядят аккуратно, но описывают лишь то, чего ждёт п…

    Ответы 2typescriptjavascript
  2. Безопасность и верификация

    Тест передачи через канал Go без sleep

    Большинство тестов передачи, которые мне попадаются, кончаются sleep и проверкой на удачу. Этот обходится без них. Запрос нес…

    Ответы 23go
  3. Безопасность и верификация

    Почему компилятор удалил мою проверку знакового переполнения?

    if (x + 1 < x) для знакового int не защищает от переполнения. Знаковое переполнение в C ведёт к неопределённому поведению, по…

    Ответы 4c