Formally Verifying Peephole Optimisations in Lean

Posted11 days agoActive4d ago

l-mdev

19 points

7 comments

l-m.devResearchstory

informativepositive

Debate

20/100

Formal VerificationCompiler OptimizationsLean Programming Language

Key topics

Formal Verification

Compiler Optimizations

Lean Programming Language

Discussion Activity

Moderate engagement

First comment

Peak period

156-168h

Avg / period

4.5

Key moments

01Story posted
Dec 22, 2025 at 7:10 PM EST
11 days ago
Step 01
02First comment
Dec 29, 2025 at 5:43 AM EST
6d after posting
Step 02
03Peak activity
6 comments in 156-168h
Hottest window of the conversation
Step 03
04Latest activity
Dec 29, 2025 at 1:07 PM EST
4d ago
Step 04

Generating AI Summary...

Analyzing up to 500 comments to identify key contributors and discussion patterns

Discussion (7 comments)

Showing 9 comments

amluto

4d ago

3 replies

Is this concept of UB as poison actually sound? It seems to me (and I apologize for not using real notation, as I can read a little bit of Lean but I’ve never tried writing it, and my experience writing optimizers is nonexistent):

Suppose we start when an SSA-style function with inputs x and y:

And we rewrite it as:

    let z = x +nsw y --or anything else that is UB for some input
    0

The original code is a function that takes x and y and returns an instance of iN {n}, namely bitvec 0.

The new code also takes any input to bitvec 0, although it may discard a poison value along the way. But this is UB in the C model!

I wonder whether this situation can be avoided by declaring that there is no control flow and that the program representation disallows discarding values. (And select would need to return poison if any argument is poison even if the selector says that the poison is not used.)

yablak

4d ago

1 reply

iiic the model assumes no flow control, only select.

amluto

4d ago

It does. But maybe someone should prove (in Lean?) that the lack of flow control is sufficient.

Without a constraint that values aren’t ignored, the lack of flow control is certainly not sufficient, so trying to do this right would require defining (in Lean!) what an expression is.

jcranmer

4d ago

1 reply

The concept of poison here is not the same as C's definition of UB. LLVM has at least 3 different concepts that all vaguely count as UB (and probably closer to a half dozen when it gets fully formalized).

In C, UB is instant-UB--the moment you execute an operation that is UB, your program is undefined. LLVM also has instant-UB (I mean, any language that lets you dereference an arbitrary integer cast to a pointer has to have instant-UB). But poison isn't instant-UB--your program is perfectly safe to execute an operation that produces poison. It's only if a poison value reaches certain operations--essentially any control-flow decision point, or as an input to any operation that may cause instant-UB--that it causes UB in the C sense.

(This also means that operations that could trap--like x / 0--aren't modeled as poison in LLVM, but as instant-UB. It's safe to speculate an operation that causes poison, like x +nsw y, but it's not safe to speculate an operation that causes instant-UB, like x / y).

afiori

4d ago

1 reply

Is dereferencing an arbitrary integer cast to pointer UB on any platform? I would expect that it is system dependent but mostly not C-style UB

jcranmer

4d ago

Dereferencing an arbitrary integer cast to a pointer means you are dereferencing an arbitrary memory location, which includes memory that is outside the purview of the C abstract machine model, say the return address of the function. That means the effect of that operation can't be meaningfully constrained, and the only option for that is UB.

(Integer-to-pointer conversions beg the question of pointer provenance, which is a long, complicated topic that is still not fully solved, but does go to show that UB is actually a lot more complicated than most people expect.)

SkiFire13

4d ago

This kinda depends on how you model assignments. AFAIK in denotational semantics you usually express them a state update function, taking the previous state of the program and returning a new state with the value for that variable updated to the new one, or an error state if the expression evaluated to `poison`.

joek1301

4d ago

1 reply

> Let’s say for moral reasons you choose to link none of LLVM’s libraries (thanks for caring about your users!)

For what moral reasons would I avoid linking LLVM? I’m not familiar.

nuudlman

4d ago

I'm not sure about moral per se, but LLVM is practically a painful dependency—it doesn't have API compatibility between versions, release builds are rapidly approaching a gigabyte, you are given some franken-version by the system, and you won't have a good time if you end up linking/loading more than one version for whatever reason.

IIRC there was also some case where an LLVM bump caused tcmalloc to explode inside wine.

View full discussion on Hacker News

ID: 46360844Type: storyLast synced: 12/29/2025, 3:40:28 PM

Want the full context?

Jump to the original sources

Read the primary article or dive into the live Hacker News thread when you're ready.

Open link View on HN