Panel: Compilation Frameworks
summary
Discussion shows a concrete path for quantify over bitwidth proofs: Lean supports quantifying bitwidth but only offers high‑performance automation for fixed widths, so general proofs require case analysis that delegates many cases to decision procedures. Sparse-format reasoning uses a greedy worklist to propagate storage formats, relies on inlining for interprocedural knowledge, and handles missing dimensions via precondition checks and rewrite injections for common scalars like alpha/beta. Implementation lessons: translating LLVM to e-graph terms is costly — prefer a dialect in ML; egglog is faster and more actively maintained than egg.
AI-written summary · about
chapters (7)
- 0:00Panel introduction
- 0:23Proving bit vector properties
- 2:26Control flow handling
- 6:00Verified backend challenges
- 8:31Egglog versus pure egg
- 9:56Prototypes vs frameworks tradeoffs
- 16:51ML rebuilding lessons
related talks
13mInteractive Bit Vector Reasoning using Verified Bitblasting
01h 05mAll the Languages Together
15mScaling Optimization Over Uncertainty via Compilation
53mSemantics-based program manipulation in the age of LLMs
32mBit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebr...
16mCertified Decision Procedures for Width-Independent Bitvector Predicates
25mSource-level debugging of compiler-optimised code: ill-posed, but not impossible
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends