ML-VIC-001 / RESEARCH CASE / EDITION 1.0
Two bids. One winner.
A precise, checkable boundary.
How do you connect an auction’s rules to the code that computes its result? This case documents a saved check of one small auction core — and makes clear what that check does and does not cover.
Recorded verificationNot an independent audit. No fresh Lean or Anvil run for this publication.
Illustrative outcome calculation in integer units, not ETH deposits. Ties go to participant 0, including 0 / 0. Winner pays min(b0, b1); loser pays zero. No funds move. Not a new proof run.
INTERACTIVE EXPLANATION, NOT PROOF EXECUTION
OVERVIEW
The higher bidder wins one item and pays the lower bid. If both bids are equal, participant 0 wins. There is no reserve price.
Source: Model.lean / auction ↗Status: Recorded evidence; not independently rerun
The core returns the winner and payment amount. It does not hold funds, transfer ETH or transfer ownership of the item. Those responsibilities belong to a separate system.
The economic results assume two participants with nonnegative private values, utility equal to value received minus payment, and actual enforcement of the modeled payment and item transfer. They consider one participant changing their own bid — not collusion or a complete commit/reveal protocol.
Source: Record / mechanism + formal_scope ↗Status: Recorded evidence; not independently rerun
Participant 0 wins; price = b1.
b0 < b1Participant 1 wins; price = b0.
VERIFIED PROPERTIES
11 groups explain the result from auction rules to exact runtime. Each has its own scope. Open a group for the exact statement, theorem names and source.
“Verified Properties” describes the supplied recorded check, not a new verification performed by this website. C01–C06 concern the economic model; later groups concern encoding and execution. The 11 groups are not a percentage of protocol security.
There is always one winner. A tie goes to participant 0.
EXACT SCOPE / mathematical_model
Exactly one participant wins; participant 0 wins when bids are equal.
Vickrey.allocation_uniqueVickrey.allocation_rulesVickrey.tie_to_zeroSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Economics.lean ↗Status: Proof reported in pinned repository; saved check passed
The higher bidder wins and pays the lower bid, not its own bid.
EXACT SCOPE / mathematical_model
The winner pays min(b0, b1); the loser pays 0.
Vickrey.payment_correctSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Economics.lean ↗Status: Proof reported in pinned repository; saved check passed
Under the stated economic assumptions, changing your own bid away from your value cannot improve your utility over truthful bidding.
EXACT SCOPE / mathematical_model
A truthful bid weakly dominates any unilateral deviation for every rival bid.
Vickrey.dsicVickrey.dsic_boundedSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Economics.lean ↗Status: Proof reported in pinned repository; saved check passed
With truthful bidding and the stated assumptions, the modeled value received is at least the modeled payment.
EXACT SCOPE / mathematical_model
A participant bidding truthfully has nonnegative utility.
Vickrey.individual_rationalitySource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Economics.lean ↗Status: Proof reported in pinned repository; saved check passed
When bids reflect values, the item goes to a participant who values it most.
EXACT SCOPE / mathematical_model
Under truthful bidding, welfare equals max(v0, v1).
Vickrey.welfare_maximizationVickrey.welfare_dominates_allocationSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Economics.lean ↗Status: Proof reported in pinned repository; saved check passed
The abstract payment accounting balances. The core does not actually move funds.
EXACT SCOPE / mathematical_model
Participant transfers plus seller revenue sum to zero; this is not a proof of ETH transfers.
Vickrey.accountingVickrey.utility_accountingSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Economics.lean ↗Status: Proof reported in pinned repository; saved check passed
The input and output use fixed-size encodings, and accepted bids are unsigned values below 2^128.
EXACT SCOPE / abi
Two 32-byte words; bids and price stay in the bounded domain.
Vickrey.word_exactVickrey.word_orderVickrey.input_sizeVickrey.output_sizeVickrey.abi_word_roundtripVickrey.price_in_rangeSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Abi.lean ↗Status: Proof reported in pinned repository; saved check passed
The selected structured program is linked to the auction model. The number 128 counts source-interpreter steps; it is not a gas budget.
EXACT SCOPE / structured_ast_and_yul
The selected structured AST is related to the model for every valid bid; source fuel = 128, not gas.
Vickrey.structured_ast_decodes_exactlyVickrey.settlement_refinementSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The declaration source is not among the 15 supplied excerpts; its presence and successful check are reported by the pinned record.
Source: record.en.json / C08 ↗Status: Proof reported in pinned repository; saved check passed
The recorded proof connects the selected compiler pipeline to these exact runtime bytes, rather than assuming compilation is correct.
EXACT SCOPE / compiler
The real compiler endpoint premises, stack checks and runtime-byte equality are discharged.
Vickrey.compiler_certificateSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/SettlementProof.lean ↗Status: Proof reported in pinned repository; saved check passed
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.
EXACT SCOPE / evm_fresh_frame
With sufficient logical interpreter fuel: the exact encoded auction outcome or actual OutOfGas.
Vickrey.settlement_runtimeSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/SettlementProof.lean ↗Status: Proof reported in pinned repository; saved check passed
Bad inputs are rejected in the specified Yul model. This is not an all-cases guarantee for the gas-charged EVM runtime.
EXACT SCOPE / yul_only
An empty revert at the Yul layer when calldata.size < 2^256; not a universal rejection theorem for the EVM runtime.
Vickrey.admissible_invalid_input_refinementSource status: PROOF_PRESENT_IN_PINNED_REPOSITORY; RECORDED_CHECK_PASSED
This is the source’s recorded status, not a new Lean run. The local excerpt preserves the original declaration; imported dependencies are not all included.
Source: Vickrey/Admissibility.lean ↗Status: Proof reported in pinned repository; saved check passed
TRUTHFUL BIDDING IS WEAK DOMINANCE UNDER THE MODEL ASSUMPTIONS. IT DOES NOT GUARANTEE EVERY STRATEGY IS SAFE OR EVERY DEVIATION IS STRICTLY WORSE.
VERIFICATION SCOPE
The recorded proof connects the chosen structured program to its exact runtime and execution in a specified fresh frame.
Define who wins and what the winner pays. Under the stated assumptions, the record also covers truthful bidding and utility.
Explore the explanation; this animation does not execute the compiler, EVM or Lean proof checker.
Source: EvmRefinementGoal.lean + SettlementProof.lean ↗Status: Recorded evidence; not independently rerun
For valid bids, from the specified fresh ABI frame and with enough logical interpreter fuel, the runtime either returns the exact auction result or satisfies the actual OutOfGas semantics. This does not prove a gas limit that guarantees success. Logical interpreter fuel and EVM gas are separate quantities.
Source: Vickrey.settlement_runtime : ExactRuntimeGasfulSettlement ↗Status: Recorded evidence; not independently rerun
Fin (2^128); model bids: Nat; utility: Int.msg.value = 0.freshGasfulEntry, not an arbitrary transaction or deployed contract state.Source: Abi.lean + record / runtime ↗Status: Recorded evidence; not independently rerun
Source: Record / formal_scope.excluded ↗Status: Explicitly outside the recorded guarantee
The rejection result is at the Yul layer, with the assumption calldata.size < 2^256. It is not a universal invalid-input theorem for the gas-charged EVM runtime. The lengths 64 and 2^256 + 64 would otherwise alias as CALLDATASIZE.
Source: Vickrey.admissible_invalid_input_refinement ↗Status: Recorded evidence; not independently rerun
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 runThe concrete compiler premises are discharged by Vickrey.compiler_certificate, rather than left as assumptions about compilation. The proof starts from an existing structured Generated.astJson value; Yul text-to-solc transformation and serialized JSON parsing are outside this boundary.
Trust remains in the Lean kernel and toolchain, the adequacy of the selected upstream EVM/Yul semantics, the economic assumptions and the declared frame. Reported allowlisted axioms: propext, Classical.choice, Quot.sound.
Three unchanged legacy parser/unbounded-calldata diagnostic targets remain UNPROVEN; they do not replace the selected verification gate. A separate experimental commit/reveal/escrow wrapper is also formally UNPROVEN; its executable tests do not extend this core proof.
Source: Original README + EvmRefinementGoal.lean ↗Status: Recorded evidence; not independently rerun
EVIDENCE
A saved check is meaningful only with its inputs, date and scope. We keep the historical run separate from publication and packaging checks.
VERIFIED · 22 stages · all exit codes 0. The original README also reports 293.1 seconds, 264 public theorems including helper lemmas, 1113 valid and 14 invalid Anvil cases. These are historical counts, not fresh website tests or 264 independent security guarantees.
Source: verification.json; counts in original README ↗Status: Recorded evidence; not independently rerun
The supplied packaging record reports 15 matching original Git blob IDs and 12 included inputs matching a historical list of 115 SHA-256 values. The 157 binary runtime bytes match their recorded hash.
Source: packaging-checks.json ↗Status: Package integrity only; not proof replay
PACKAGE_INTEGRITY_OK was reproduced for 29 package files, 15 originals, 12/115 historical hashes and 157 runtime bytes. Of 8 utility tests attempted here, 6 passed; Windows symlink privilege and CRLF/LF conversion prevented two from passing. Lean, Anvil and remote full-source export were not rerun.
Source: English report / adaptation checks ↗Status: Local packaging checks; no new proof check
d02ea87ce713d589c72328b89902a92d11275480Branch: codex/verify-refinement. The original repository was private at retrieval; its main branch contains an older prototype.
TREEda1a82df7e4612091f2996fea7ffc1d8b33cb01b5ad69bf3ad48717a7beb1a083d2229241934fd01370062bbcdf89e15ff29349eTEXT .HEX FILE SHA-256 / A DIFFERENT BYTE SEQUENCE2607c4326db51db03c769e25e905db191b582a9a17ae731411dfe0b2b28fdef5Source: Source index + original record ↗Status: Unsigned identifiers; not authorship authentication
Hashes check consistency with an unsigned record. They are not an auditor’s signature, proof replay, keccak256 or a deployed contract address. A raw end_to_end_verified flag refers only to the record’s explicitly declared structured-AST-to-runtime scope. No hosted CI run or independent audit is established.
REPRODUCIBILITY
A saved successful check for the pinned commit, with its scope and source evidence.
Available in this publicationA new successful check using the full source, pinned dependencies and fresh logs. Instructions are provided; a new successful run is not claimed.
Full private source and dependencies required.A separate review by an independent party. This project record is not that review and has no external auditor signature.
No independent audit claimed.Source: Record / recorded_verification, packaging + trust ↗Status: Evidence levels kept separate
python3 tools/verify_package.py
Run this inside the original unpacked archive, not the adapted website directory. Expected: PACKAGE_INTEGRITY_OK. It checks the unsigned package inventory, not the Lean proofs.
python3 tools/build_source_bundle.py --repo-root /path/to/vickrey-lean-solidus
Requires authorized private-repository access. The tool exports the pinned commit, checks all 115 historical input hashes and 15 originals, excludes uncommitted changes and credentials, and does not run Lean. Remote export was not tested here.
cd vickrey-source-d02ea87 cp -R results ../recorded-results-d02ea87 cp versions.json ../recorded-versions-d02ea87.json cp lake-manifest.json ../recorded-lake-manifest-d02ea87.json make bootstrap make verify
Keep the historical evidence untouched; save new logs and versions separately. Bootstrap may update lock or metadata files. A new run does not expand the verification boundary, and OutOfGas remains an allowed outcome.
The package contains 15 excerpts, not every Lean import or compiler certificate. Third-party dependencies and executables are absent. Do not run make verify inside source-excerpts.
The source recommends macOS arm64, Python 3.12+, Git, Xcode CLI and elan. Cold builds need a network connection, several GB of disk and about 5 GB RAM for one certificate according to the README. Bootstrap supplies macOS arm64 tools; Linux requires solc/forge/cast/anvil in PATH and is not confirmed by this publication.
Source: English reproduction guide, translated from REPRODUCE.md ↗Status: Procedure supplied; fresh proof reproduction not performed
Source: versions.json; full dependency revisions in lake-manifest.json ↗Status: Recorded evidence; not independently rerun
DOWNLOADS
English explanations sit alongside unchanged original evidence. No source license or right to public redistribution is inferred.
All 11 claim groups, exact theorem, assumptions, evidence and limitations in English.
Commands, pinned tools, private-source access and the limits of a fresh run.
English translation. Numbers, IDs, theorem names, hashes and source statuses preserved.
15 unchanged source excerpts and package tools. Includes original Russian commentary. Not a full offline proof bundle.
The exact binary identified by the record. Not a deployable protocol or asset-custody system.
Original file paths, Git blob IDs, SHA-256 values and private-repository provenance.
SOURCE: ML-VIC-001 EDITION 1.0 / STATUS: EDITORIAL TRANSLATION + ORIGINAL EVIDENCE. ORIGINAL MANIFESTS APPLY TO THE ORIGINAL PACKAGE, NOT THE ADAPTED WEBSITE’S EXTRA ENGLISH FILES.
FROM A BOUNDED CORE TO YOUR MECHANISM
This case demonstrates a focused research boundary. Your mechanism needs its own requirements, assumptions and verification goals.
Discuss your mechanism