Gearbox BytecodeRepository Version Index

A fresh version is recorded, every relevant latest-version shortcut advances exactly when needed, and no unrelated modeled state changes.

View Lean

Gearbox is a DeFi credit protocol. Its BytecodeRepository records which contract bytecode is allowed for each contract type and version.

The repository keeps three shortcuts for finding the latest version: latest overall, latest in the same hundred-series such as 3xx, and latest in the same ten-series such as 31x. This proof checks what happens to those shortcuts when the internal _allowContract function fills a previously empty type-version slot.

Why It Matters

Suppose version 310 is added. The registry currently says 305 is the latest version overall and in the 3xx family, and it has no latest entry yet for the 31x release line. After the insertion, all three shortcuts should read 310. If one stayed stale or jumped to an unrelated value, Gearbox could look up the wrong version or one that does not exist.

Gearbox's deployer helpers use the latest patch index to deploy a contract and compute its address. The theorem rules out stale or over-advanced indexes created by the modeled fresh insertion. It does not establish the safety of the stored bytecode or the wider protocol.

How This Was Modeled and Proven

We reduced the relevant source branch to one registry entry, a version list, and three stored latest-version bookmarks. Then we checked the transition in three steps:

  1. Model: recreate the relevant storage and branch logic in Lean, including the same version helpers as the pinned source.
  2. Rule: write down exactly what every modeled field must contain before and after a fresh version is allowed.
  3. Proof: let Lean expand the modeled branch and its storage updates, then check that the result always matches that rule when the slot starts empty and the supplied hash is not zero.

The full-state check also makes sure unrelated modeled entries do not change. The final Proofs.lean covers the fresh insertion, the same-hash no-op, and the different-hash rejection without case-specific axioms, sorry, or admit.

Scope

Included: the fresh, nonzero-hash branch of internal _allowContract, including the hash write, version-set membership, and exact overall, major, and minor maximum updates. The same-hash early return is covered by its separate no-op theorem.

Removal excluded: removePublicContractType conditionally clears the owner, iterates the version set, and resets hashes and indexes. Its deletion loop needs a separate model and proof.

Caller guards excluded: the external system and public allowance paths add upload, audit, domain, ownership, and author checks, plus domain or owner writes. Those caller-level branches need separate models. They are not assumed to be proved here.

Model boundary: we manually mapped the relevant Solidity into Lean and compared the two line by line. Lean proves the rule for that model; it does not prove that the translation itself is equivalent to the Solidity or deployed bytecode.

Also not proved: deployment state, bytecode hashing or signatures, deployment behavior, EnumerableSet enumeration order, full BytecodeRepository or protocol security, or source-branch reachability. The model observes set membership only.

Proof artifacts
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout b0f3ca43d503130fb661abac91cc51701b56b966
lake build Benchmark.Cases.Gearbox.BytecodeVersionIndex.Compile

Hypotheses

The proof covers the fresh-insertion branch only when these two conditions are true.

  • The slot starts emptyoldAllowed[cType][ver] = 0

    Specs.lean

    This proof is about adding a new type-version entry, not replacing one that already has a hash.

  • The supplied hash is not zerobytecodeHash != 0

    Specs.lean

    Zero marks an empty slot. If the new hash were also zero, the function would treat it as the same-hash no-op instead of a new insertion. The proof therefore excludes zero.

Learn More