# ML-VIC-001 — Vickrey Auction

English technical report, edition 1.0. Publication: 2026-10-20. Recorded run: 2026-10-10 Europe/Moscow. This is a project verification record, not an accredited certificate or an independent audit. No new Lean or Anvil run was performed for this website adaptation.

## Overview

Two participants, one item, no reserve price, second price. The higher bid wins; equal bids go to participant 0. The winner pays min(b0, b1); the loser pays zero. This is an outcome-computation core: it does not hold assets, transfer ETH, or transfer title to the item. The economic model assumes those abstract obligations are enforced elsewhere.

Model bids and nonnegative private values are Nat. Runtime bids are Fin (2^128). Quasilinear utility is Int, so overbidding can produce negative utility. DSIC concerns unilateral deviation for a fixed rival bid; collusion, budget limits and a complete commit/reveal protocol are outside the economic guarantee. Truthfulness is weak dominance, not a claim that every deviation is strictly worse.

## Verified Properties — recorded claims

Every group below has source status PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED. This means the supplied pinned record reports a successful check. It does not mean the website reran Lean or independently audited the result.

### C01 / One winner, including ties

Exactly one participant wins; participant 0 wins when bids are equal.

Plain-language reading: There is always one winner. A tie goes to participant 0.

Declarations: `Vickrey.allocation_unique`, `Vickrey.allocation_rules`, `Vickrey.tie_to_zero`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Economics.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C02 / The correct second price

The winner pays min(b0, b1); the loser pays 0.

Plain-language reading: The higher bidder wins and pays the lower bid, not its own bid.

Declarations: `Vickrey.payment_correct`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Economics.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C03 / Truthful bidding (DSIC)

A truthful bid weakly dominates any unilateral deviation for every rival bid.

Plain-language reading: Under the stated economic assumptions, changing your own bid away from your value cannot improve your utility over truthful bidding.

Declarations: `Vickrey.dsic`, `Vickrey.dsic_bounded`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Economics.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C04 / Nonnegative utility when truthful

A participant bidding truthfully has nonnegative utility.

Plain-language reading: With truthful bidding and the stated assumptions, the modeled value received is at least the modeled payment.

Declarations: `Vickrey.individual_rationality`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Economics.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C05 / Allocation to the higher value

Under truthful bidding, welfare equals max(v0, v1).

Plain-language reading: When bids reflect values, the item goes to a participant who values it most.

Declarations: `Vickrey.welfare_maximization`, `Vickrey.welfare_dominates_allocation`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Economics.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C06 / Balanced model accounting

Participant transfers plus seller revenue sum to zero; this is not a proof of ETH transfers.

Plain-language reading: The abstract payment accounting balances. The core does not actually move funds.

Declarations: `Vickrey.accounting`, `Vickrey.utility_accounting`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Economics.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C07 / Encoding and bounded values

Two 32-byte words; bids and price stay in the bounded domain.

Plain-language reading: The input and output use fixed-size encodings, and accepted bids are unsigned values below 2^128.

Declarations: `Vickrey.word_exact`, `Vickrey.word_order`, `Vickrey.input_size`, `Vickrey.output_size`, `Vickrey.abi_word_roundtrip`, `Vickrey.price_in_range`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Abi.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C08 / Structured AST and Yul execution

The selected structured AST is related to the model for every valid bid; source fuel = 128, not gas.

Plain-language reading: The selected structured program is linked to the auction model. The number 128 counts source-interpreter steps; it is not a gas budget.

Declarations: `Vickrey.structured_ast_decodes_exactly`, `Vickrey.settlement_refinement`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/SettlementExecution.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C09 / Compilation to the exact bytes

The real compiler endpoint premises, stack checks and runtime-byte equality are discharged.

Plain-language reading: The recorded proof connects the selected compiler pipeline to these exact runtime bytes, rather than assuming compilation is correct.

Declarations: `Vickrey.compiler_certificate`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/SettlementProof.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C10 / Execution of the exact runtime

With sufficient logical interpreter fuel: the exact encoded auction outcome or actual OutOfGas.

Plain-language reading: From the specified fresh ABI frame, the exact code returns the right encoded result or runs out of gas. No gas limit guaranteeing success is proven.

Declarations: `Vickrey.settlement_runtime`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/SettlementProof.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

### C11 / Invalid-input rejection in Yul

An empty revert at the Yul layer when calldata.size < 2^256; not a universal rejection theorem for the EVM runtime.

Plain-language reading: Bad inputs are rejected in the specified Yul model. This is not an all-cases guarantee for the gas-charged EVM runtime.

Declarations: `Vickrey.admissible_invalid_input_refinement`

Source: https://github.com/VileBody/vickrey-lean-solidus/blob/d02ea87ce713d589c72328b89902a92d11275480/Vickrey/Admissibility.lean (private repository; access required). Local source index: evidence/source-index.json. C08's declaration source is not included in the 15 excerpts; its status comes from the supplied record and pinned repository.

## Verification Scope

The proof starts from Generated.astJson as an existing structured Lean.Json value and uses the actual structured Solidus decoder. It continues through Yul execution and the pinned Solidus compiler pipeline to the exact 157-byte runtime and EVMYulLean EVM.X from freshGasfulEntry. Runtime-byte equality is part of the recorded proof, not only a checksum comparison. Concrete compilation prerequisites are discharged by Vickrey.compiler_certificate.

For every valid pair of bids and arbitrary EVM gas, with sufficient logical interpreter fuel, the final theorem permits either the exact encoded auction result or actual OutOfGas. No sufficient EVM gas bound for successful execution is proven. Source fuel = 128 belongs to the Yul interpreter; it is not transaction gas. The selected compiler target is Cancun.

Selectorless wire ABI: exactly 64 input bytes, uint256(bid0) || uint256(bid1), big-endian, each value < 2^128, msg.value = 0. Output: 64 bytes, winner index and payment. This is a specified fresh execution frame, not a deployment or transaction-reachability theorem.

Invalid-input rejection is a separate Yul-layer result with premise calldata.size < 2^256. The natural lengths 64 and 2^256 + 64 alias as a 256-bit CALLDATASIZE, so an unrestricted ByteArray-length claim is not inferred. Three unchanged legacy parser/unbounded-calldata obligations remain UNPROVEN diagnostic targets; they are not the selected required verification endpoint.

Not established: Yul text to solc transformation, serialized JSON parsing, contract deployment, transaction-level reachability, the entire Ethereum lifecycle, a sufficient gas bound, ETH transfers, escrow, commit/reveal incentives, collusion or budget constraints. The experimental wrapper is separately reported as UNPROVEN formally; its executable tests do not extend the core proof.

Trust includes the Lean kernel/toolchain, the meaning and adequacy of selected upstream EVM/Yul semantics, the model assumptions and execution frame. Reported allowlisted axioms: propext, Classical.choice, Quot.sound. No independent verification of all Ethereum semantics is asserted.

Exact endpoint (unchanged):

```lean
def ExactRuntimeGasfulSettlement : Prop :=
  ∀ (a b : Bid) (base : SourceState) (gas : EvmYul.UInt256),
    ∃ openFuel : Nat,
      let run := EvmYul.EVM.X (max openFuel (gas.toNat + 6))
        (EvmYul.EVM.D_J (Bytecode.ofList Generated.runtimeBytes)
          (EvmYul.UInt256.ofNat 0))
        (freshGasfulEntry Generated.runtimeBytes base a b gas)
      (∃ final, run = .ok (.success final (encodeOutcome (auction a.val b.val)))) ∨
        GasfulBridge.OutOfGasFrameSemantics run
```

## Evidence

Repository: VileBody/vickrey-lean-solidus, private at retrieval. Branch: codex/verify-refinement, not the older main prototype.

Commit: d02ea87ce713d589c72328b89902a92d11275480
Tree: da1a82df7e4612091f2996fea7ffc1d8b33cb01b
Commit timestamp UTC: 2026-10-09T23:39:57Z

The repository-recorded local make verify is VERIFIED: 22 stages, each exit code 0. The source README reports 293.1 seconds, an audit of 264 public theorems (including helper lemmas, not 264 distinct security guarantees), 1113 valid and 14 invalid Anvil cases. These are historical recorded counts, not tests newly executed by this website. At input (10, 5), the executable negative test expects price 5 and detects a mutant returning 10. The README separately reports a formal mutation regression; the executable negative-test file is not itself that proof report.

The publication packaging record reports 15 matching original Git blob IDs, 12 matching included inputs against a historical list of 115 SHA-256 values, identical runtime and 8 successful package-tool unit tests. During this website adaptation PACKAGE_INTEGRITY_OK was reproduced: 29 files, 15 originals, 12/115 historical hashes, 157 runtime bytes. The tool-test attempt here passed 6 of 8; one was blocked by Windows symlink privilege and one failed on Git CRLF/LF conversion. These utility checks are neither proof replay nor auction verification. No Lean, Anvil or remote full-source export was rerun here.

The manifest and hashes are unsigned. Integrity relative to them does not authenticate authorship, verify the commit signature or replace Lean. No hosted CI run or independent audit is established. If a raw verifier record uses end_to_end_verified, it refers only to the explicitly declared structured-AST-to-runtime scope, not a complete deployed protocol.

Runtime binary SHA-256 (157 decoded bytes): 5ad69bf3ad48717a7beb1a083d2229241934fd01370062bbcdf89e15ff29349e
Hex text file SHA-256: 2607c4326db51db03c769e25e905db191b582a9a17ae731411dfe0b2b28fdef5

These are different hashes of different byte sequences. They are not keccak256 or a deployed contract address.

## Reproducibility

Recorded verification: a saved check result for the pinned commit. Reproducible proof: a new successful check of the full source tree and pinned dependencies, with new logs. Independent audit: a separate review by an independent party. Only the first is supported by this publication; instructions for the second are provided, but a new successful run and the third are not claimed.

This is not a complete offline proof bundle. Some Lean imports, compiler certificates and all third-party dependencies/tools are absent. Do not run make verify inside source-excerpts. Full source requires authorized access to the private repository. Public source redistribution and reuse terms are not inferred; current site access remains private.

See REPRODUCE.en.md for the full commands and environment limitations. Lean 4.28.0, solc 0.8.26+commit.8a97fa7a and Foundry 1.5.1 are pinned. Recorded environment: macOS-15.3.1-arm64, Python 3.12.3. Solidus: 32c7cdbc0b466bdb13ce6eeabe5add8c49f356e2; EVMYulLean: b08573c65e33feb5331abe2b7c1d76be89bb8eff; mathlib: 8f9d9cff6bd728b17a24e163c9402775d9e6a365. Complete revisions remain in versions.json and lake-manifest.json.

## Downloads and provenance

The English record and report are editorial translations. Original evidence, source code, theorem names, hashes and statuses remain byte-identical in the evidence archive and excerpts. The original manifest applies only to the original package layout, not to this adapted website's extra English files. Package identity is not an auditor signature. A new source commit requires a new record with its own evidence.