主要观点：作者过去一年一直在思考和研究 JIT 编译器中的整数优化，介绍了最新的用于指定 JIT 中整数操作窥孔优化的小领域特定语言（DSL），包括其动机、规则、实现细节等，并提及后续的改进计划和感谢他人的反馈。
关键信息：

• 之前整数优化代码冗长且易出错，决定创建 DSL 以更声明式表达规则。
• DSL 规则包括名称、模式和目标，支持多种操作和条件，如常量计算、检查等。
• 规则有优先级和活跃度，会打印统计信息，目前缺少终止和汇合检查等。
• 所有规则在编译为实际 JIT 代码前用 Z3 证明正确性，也检查规则是否可应用。
• DSL 实现方式及与其他工具的结合，目前已合并到 PyPy 主分支，部分优化仍为旧样式。
  重要细节：
• 规则示例如add_zero匹配int_add(x, 0)并将其优化为x，sub_x_x匹配int_sub(x, x)并优化为0等。
• 中间结果计算可通过额外赋值实现，如sub_add_consts中计算C = C1 + C2。
• 检查用于限制规则应用条件，如eq_one中检查x为布尔值。
• 规则顺序影响应用，sub_x_x和sub_add优先于sub_add_consts。
• 证明规则正确性时若失败会输出反例，部分IntBound方法在 Z3 证明中受限。
• 实现 DSL 用rply解析，通过 Z3 API 证明，模式匹配代码生成受 Luc Maranget 论文启发。
• 后续计划包括支持溢出检查变体、处理除法等操作、移植排序比较以及实现简化的 e-graph 等。