# Verified Vickrey: Lean 4 + Yul + Solidus

**Доказательная цепочка settlement-core замкнута: структурированный AST → точный runtime → реальное исполнение EVM.**

Два участника, один лот, ничья в пользу участника 0, вторая цена.
Независимая модель и DSIC/IR/welfare/payment/accounting доказаны в Lean 4.
Настоящий Yul AST исполняется по семантике EVMYulLean, компилируется закреплённым
Solidus и связан kernel-доказательством с сохранёнными **157 байтами** runtime.

Главная теорема [`settlement_runtime`](Vickrey/SettlementProof.lean) не имеет
предпосылок о компиляции или правильности исходного результата. Для всех
допустимых ставок и произвольного газа реальный `EVM.X` из fresh ABI frame
возвращает точный ответ аукциона либо OutOfGas, при достаточном логическом
топливе интерпретатора. Порог газа для гарантированного успеха не доказан.

Формальная граница начинается с явного `Lean.Json` AST. Текст Yul, работа solc,
парсинг JSON-строки, создание контракта и вся транзакционная обработка Ethereum
не объявляются формально проверенными. Точные границы — в
[отчёте](docs/report.md), [графе](docs/proof-graph.md) и
[описании сертификатов](docs/compiler-certificates.md).

Локальный `make verify` выполнен: **VERIFIED**, код выхода 0, 293,1 секунды.
Прошли 22 этапа, аудит 264 публичных теорем, 1113 допустимых и 14 неверных
входов в Anvil, а также негативная проверка изменённой второй цены.

Verifier сохраняет [результат и SHA входов](results/verification.json),
[аудит всех публичных теорем](results/full-axioms.json),
[логи и exit codes](logs/commands.jsonl).
Неполученное обязательное доказательство завершает команду ошибкой.

Приватный репозиторий: [VileBody/vickrey-lean-solidus](https://github.com/VileBody/vickrey-lean-solidus).
[CI](.github/workflows/verify.yml) запускается **только вручную** и в ходе этой
работы не запускался. Push и pull request его не запускают. Проверка на чистом
hosted runner пока не подтверждена; [подробности CI](docs/ci.md).

```sh
make bootstrap                  # закреплённые инструменты и зависимости
make artifacts                  # явная регенерация сохранённых артефактов
make verify                     # строгая проверка всей цепочки ядра
make -C wrapper verify          # отдельные исполняемые тесты обвязки
make verify-economics            # только экономика, ABI и примитив
make negative-proof             # исходное доказательство проходит, мутант отвергается
make verify-legacy-diagnostics   # прежние более широкие цели; ожидается ошибка
```

`make verify` проверяет pins и неизменность зависимостей, собирает доказательства,
аудирует аксиомы, требует закрытый compiler certificate и теорему реального
EVM-исполнения, повторяет компиляцию для сравнения артефактов, запускает Anvil
и формальную мутацию. Проверены обе ветки, ничьи, пределы и неверные входы.
Генерация свидетеля, native-компиляция и SHA-256 не заменяют доказательства Lean.
Допустимые аксиомы — только `propext`, `Classical.choice`, `Quot.sound`.

Три исходные цели про строковый parser и неограниченную длину calldata сохранены
неизменными в `obligations/`. Их отдельный
[диагностический запуск](results/legacy-diagnostics.json) остаётся `UNPROVEN`.
Новый обязательный endpoint проверяет настоящий структурированный compiler
pipeline и те же байты. Для отказов явно задана область `calldata.size < 2^256`;
иначе натуральные длины 64 и `2^256 + 64` дают одинаковый `CALLDATASIZE`.

Wire ABI ядра без селектора: ровно 64 байта `uint256(bid0) || uint256(bid1)`,
big-endian; каждое значение `< 2^128`, `msg.value = 0`. Ответ — два слова:
индекс победителя и платёж. Ядро вычисляет результат; оно не переводит ETH
и не хранит право на лот.

Отдельная экспериментальная обвязка commit-reveal/escrow находится в
[`wrapper/`](wrapper/README.md). Она реализована после закрытия доказательства
ядра: `make -C wrapper verify` прошёл, 34 теста и 256 fuzz-итераций. Это
проверка исполняемых сценариев, формальный статус обвязки — `UNPROVEN`.
Её стратегические свойства и переводы средств не входят в доказанную
DSIC; правила и ограничения описаны в [protocol.md](docs/protocol.md).

Основные материалы:

- [Модель](Vickrey/Model.lean), [экономика](Vickrey/Economics.lean), [ABI](Vickrey/Abi.lean).
- [Полное исполнение AST](Vickrey/SettlementExecution.lean), [допустимые входы](Vickrey/Admissibility.lean).
- [Точные конечные формулировки](Vickrey/EvmRefinementGoal.lean), [итоговые доказательства](Vickrey/SettlementProof.lean).
- [Yul](contracts/Settlement.yul), [solc AST](artifacts/Settlement.ast.json),
  [runtime](artifacts/Settlement.runtime.hex), [initcode](artifacts/Settlement.creation.hex).
- [Версии](versions.json), [Anvil](results/evm-tests.json), [формальная мутация](results/negative-proof.json).

Среда воспроизведения: macOS arm64, Python 3.12+, Git, Xcode CLI и elan.
Lean 4.28.0 выбирается через `lean-toolchain`; solc 0.8.26 и Foundry 1.5.1
закреплены bootstrap. Полная холодная сборка требует нескольких ГБ на диске;
проверка сертификата расписания стека может занимать около 5 ГБ RAM.
Исторические абсолютные пути в логах относятся к прежнему workspace.