lean-mlir icon indicating copy to clipboard operation
lean-mlir copied to clipboard

chore: mark div/rem instructions as .impure, with Id monad

Open tobiasgrosser opened this issue 8 months ago • 0 comments

This lets us say the following:

We accurately model all semantics in LLVM. For operations that are side-effectful (divisions and remainders), we mark them as such in our framework, which ensures that the peephole rewrite never rewrites such operations. We choose the side effecting monad to be $Id$, thereby effectively freezing undefined behaviour into poison, which is a safe semantic refinement to do.

tobiasgrosser avatar Jun 06 '24 17:06 tobiasgrosser