Lean Abstractification

RESEARCH DRAFT · LEAN 4

Explore the fill.
Keep the proof.

A program sketch can change in carefully chosen places. Its specification stays fixed. This Lean interpretation of abstractification makes a correctness certificate the final condition for installation.

Try the bit sketchRead the research draft

Based on Alperen Keleş’s Abstractification · Direction by Alok

FIXED SKETCHBitVec w
~(x + left)
& (x + right)
typed fill(0, 1)
Every width. Every input.

Inductive certificate in Lean, including wrapping overflow and width zero.

Inspect the theorem
Snapshot 728a54eLean 4.34.1No third-party Lean packagesLean checks passed · Sep 30, 2026

01 / A CONCRETE SKETCH

Find the rightmost zero bit

Read from the least significant bit. Return a mask for the first zero, or zero if every bit is one.

An integer from 0 to 255

Explore an edge case
INPUT xMSB LSB
Positional scan00001000decimal 8
Filled expression00001000decimal 8
Outputs match on this input

Browser illustration, not a live Lean kernel. JavaScript evaluates 8-bit wrapping arithmetic and enumerates the 256 inputs. This visualization creates no certificate. The universal proof lives in the Lean source.

02 / THE MECHANISM

Search inside a fixed boundary

The optimizer proposes fills. It does not rewrite the reference, surrounding sketch, observer, or correctness checks.

1

Propose

Choose typed values from a closed, deterministic candidate list.

2

Check

Replay known counterexamples, then run the fixed verifier. Failed candidates receive no score.

3

Rank

Compare passing candidates with a declared cost model for a declared workload.

4

Certify & install

Require a separate proof covering every input allowed by the boundary.

A tested winner is still a proposal

The demo starts with replay input 255. The wrong fill (0, 0) passes that example, but full verification discovers input 0. The next wrong proposal is rejected using the accumulated counterexample.

A deliberately replay-only search can select a bad fill. The independent all-input certificate gate still rejects it.

Inspect the search and negative control

THE INSTALLATION OBLIGATION

Boundary.Valid fill :=
  ∀ input, pre input →
    observe (sketch fill input) =
    observe (reference input)

Installed boundary
  fill    : Fill
  correct : boundary.Valid fill

The guarantee concerns the chosen observations, under the chosen precondition.

Read Boundary and Installed

03 / WHAT THE PROOF SAYS

From eight bits to any width

The original finite 8-bit certificate is extended by induction, rather than by checking more inputs.

goodFill_equivalent

∀ {w : Nat} (x : BitVec w),
  sketch (goodFill w) x = reference x

The reference scans positions from low to high. The proof relates it to a recursive low-bit scan, then proves the filled expression agrees by induction through the two carry cases.

  • Full output equality, with precondition True
  • Wrapping carry and all-ones overflow included
  • Width zero included; no extra input assumption
  • No input enumeration, SAT solver, or native decision
Proof structure and assumptions

A direct 32-bit specialization

exact32 covers every BitVec 32. The audited installed32 packages the same proof for execution.

An explicit trust policy

install% audits transitive dependencies. The universal certificate uses Lean’s standard propext, Classical.choice, and Quot.sound axioms. Admissions, custom axioms, and native-decision trust axioms are rejected.

Repeatable checks

The repository check suite builds, audits, replays modules with leanchecker, requires 14 negative fixtures to fail, and runs the demo.

View the successful CI run

04 / CORRECTNESS BEFORE COST

The workload changes the winner

The demo counts one operation per bit inspection and four per bit expression. Both candidates are correct; only their scores change.

Toy operation counts only. These are not elapsed times, allocation results, or measured speedups.

Read the cost model and winner theorems
Reference scan16
Bit sketch (0, 1)8

Toy-cost winner: bit sketch

05 / SCOPE & OPEN WORK

A research draft with clear edges

Proofs make a specific promise. The boundary and the tools around it still matter.

IMPLEMENTED

Typed draft holes

draft_hole% name reports its expected type and local context, then fails elaboration. It cannot silently become an admitted or default executable value.

Agda-style refinement, case splitting, editor code actions, and a full interactive-hole rewrite remain future work.

LOGICAL SCOPE

The specification is a choice

The proof preserves declared observations on inputs satisfying the precondition. It does not establish that the specification captures every intended behavior.

The Installed type alone is not an axiom policy. Use the audited DSL or #audit_install and run the checks.

RUNTIME SCOPE

More evidence is needed

Lean elaboration is not an OS sandbox. These proofs do not verify foreign code, compiler substitutions, allocation failures, or compiler correctness.

The candidate proposer is finite and deterministic. There is no live LLM optimizer, and no benchmark reproducing the paper’s Rust allocation experiment.

More detail: Design and research scope · Verification and AI review

RUN THE ARTIFACT

Inspect it. Replay it.

Install elan and Python 3, then run the repository’s check suite. The pinned toolchain is Lean 4.34.1.

Open the repository
Inside the repository
sh scripts/check.sh

# Build and run the demonstration
lake build
lake exe abstractificationDemo