From e2390ebe4c6b883779bda0209464e95e9980ee0b Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 14:26:57 +0100 Subject: [PATCH 01/10] `rust-engine/src/resugarings.rs`: Remove `BinOp` resugaring --- rust-engine/src/resugarings.rs | 55 ---------------------------------- 1 file changed, 55 deletions(-) diff --git a/rust-engine/src/resugarings.rs b/rust-engine/src/resugarings.rs index 2962b95cf..f9dcd6dbd 100644 --- a/rust-engine/src/resugarings.rs +++ b/rust-engine/src/resugarings.rs @@ -54,61 +54,6 @@ impl Resugaring for FunctionsToConstants { } } -/// Binop resugaring. Used to identify expressions of the form `(f e1 e2)` where -/// `f` is a known identifier. -pub struct BinOp { - /// Stores a set of identifiers that should be resugared as binary - /// operations. Usually, those identifiers come from the hax encoding. Each - /// backend can select its own set of identifiers Typically, if the backend - /// has a special support for addition, `known_ops` will contain - /// `hax::machine::int::add` - pub known_ops: HashSet, -} - -impl BinOp { - /// Adds a new binary operation from a list of (hax-introduced) names - pub fn new(known_ops: &[GlobalId]) -> Self { - Self { - known_ops: HashSet::from_iter(known_ops.iter().cloned()), - } - } -} - -impl AstVisitorMut for BinOp { - fn enter_expr_kind(&mut self, x: &mut ExprKind) { - let ExprKind::App { - head, - args, - generic_args, - bounds_impls, - trait_, - }: &mut ExprKind = x - else { - return; - }; - let ExprKind::GlobalId(id) = &*head.kind else { - return; - }; - let [lhs, rhs] = &args[..] else { return }; - if self.known_ops.iter().any(|defid| id == defid) { - *x = ExprKind::Resugared(ResugaredExprKind::BinOp { - op: *id, - lhs: lhs.clone(), - rhs: rhs.clone(), - generic_args: generic_args.clone(), - bounds_impls: bounds_impls.clone(), - trait_: trait_.clone(), - }); - } - } -} - -impl Resugaring for BinOp { - fn name(&self) -> String { - "binop".to_string() - } -} - /// Tuples resugaring. Resugars tuple constructors to the dedicated expression variant [`ResugaredExprKind::Tuple`], /// and tuple types to the dedicated type variant [`ResugaredTyKind::Tuple`]. pub struct Tuples; From ff0e744afc278e1ff361c3deadef1f236fd5e151 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 14:29:37 +0100 Subject: [PATCH 02/10] `ast/resugared.rs`: remove `BinOp` in `ResugaredExpressionKind` enum --- rust-engine/src/ast/resugared.rs | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/rust-engine/src/ast/resugared.rs b/rust-engine/src/ast/resugared.rs index b91c54bcc..4282559bb 100644 --- a/rust-engine/src/ast/resugared.rs +++ b/rust-engine/src/ast/resugared.rs @@ -36,22 +36,6 @@ pub enum ResugaredItemKind { // TODO: drop `clippy::large_enum_variant` when https://github.com/cryspen/hax/issues/1666 is addressed. #[allow(clippy::large_enum_variant)] pub enum ResugaredExprKind { - /// Binary operations (identified by resugaring) of the form `f(e1, e2)` - BinOp { - /// The identifier of the operation (`f`) - op: GlobalId, - /// The left-hand side of the operation (`e1`) - lhs: Expr, - /// The right-hand side of the operation (`e2`) - rhs: Expr, - /// The generic arguments applied to the function. - generic_args: Vec, - /// If the function requires generic bounds to be called, `bounds_impls` - /// is a vector of impl. expressions for those bounds. - bounds_impls: Vec, - /// If we apply an associated function, contains the impl. expr used. - trait_: Option<(ImplExpr, Vec)>, - }, /// A tuple constructor. /// /// # Example: From fbf82518edaa89a9362ed86d47fe6f7aab8bcfb9 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 14:31:21 +0100 Subject: [PATCH 03/10] `backends/rust.rs`: remove `ResugaredExprKind::BinOp` match case --- rust-engine/src/backends/rust.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/rust-engine/src/backends/rust.rs b/rust-engine/src/backends/rust.rs index 7de81543c..5ab1dd302 100644 --- a/rust-engine/src/backends/rust.rs +++ b/rust-engine/src/backends/rust.rs @@ -590,7 +590,6 @@ const _: () = { } fn resugared_expr_kind(&self, resugared_expr_kind: &ResugaredExprKind) -> DocBuilder { match resugared_expr_kind { - ResugaredExprKind::BinOp { .. } => unreachable!("BinOp resugaring not active"), ResugaredExprKind::Tuple(values) => print_tuple!(values), ResugaredExprKind::LetPure { .. } => unreachable!("LetPure resugaring not active"), } From 5ba1103ca252af072c013db5c103b385ee68bfc2 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 14:35:30 +0100 Subject: [PATCH 04/10] `backends/lean.rs`: Remove `BinOp` from `resugaring_phases` --- rust-engine/src/backends/lean.rs | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 57933a43e..dcf8bd854 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -142,24 +142,7 @@ impl RenderView for LeanPrinter { impl Printer for LeanPrinter { fn resugaring_phases() -> Vec> { - vec![ - Box::new(BinOp::new(&[ - binops::add, - binops::sub, - binops::mul, - binops::rem, - binops::div, - binops::shr, - binops::shl, - binops::bitand, - binops::bitxor, - binops::logical_op_and, - binops::logical_op_or, - binops::Index::index, - ])), - Box::new(FunctionsToConstants), - Box::new(LetPure), - ] + vec![Box::new(FunctionsToConstants), Box::new(LetPure)] } } From a3e69f1112148ea66f7d25296f49a5a67ba811e3 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 14:37:58 +0100 Subject: [PATCH 05/10] `backends/lean.rs`: remove resugared `BinOp` match case in `expr` fn --- rust-engine/src/backends/lean.rs | 27 --------------------------- 1 file changed, 27 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index dcf8bd854..1d9a3da47 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -997,33 +997,6 @@ const _: () = { .group() .nest(INDENT), - ExprKind::Resugared(ResugaredExprKind::BinOp { op, lhs, rhs, .. }) => { - // TODO : refactor this, moving this code directly in the `App` node (see - // https://github.com/cryspen/hax/issues/1705) - if *op == binops::Index::index { - return docs![lhs, "[", line_!(), rhs, line_!(), "]_?"] - .nest(INDENT) - .group(); - } - let symbol = match *op { - binops::add => "+?", - binops::sub => "-?", - binops::mul => "*?", - binops::div => "/?", - binops::rem => "%?", - binops::shr => ">>>?", - binops::shl => "<< "&&&?", - binops::bitxor => "^^^?", - binops::logical_op_and => "&&?", - binops::logical_op_or => "||?", - _ => unreachable!(), - }; - docs![lhs, line!(), docs![symbol, softline!(), rhs].group()] - .group() - .nest(INDENT) - .parens() - } ExprKind::Resugared(ResugaredExprKind::Tuple { .. }) => { unreachable!("This printer doesn't use the tuple resugaring") } From 39a4d4ebb616a0f6353ff9e0cc1cab0173fae30c Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 14:40:17 +0100 Subject: [PATCH 06/10] `backends/lean.rs`: add `App` `GlobalId` match case for known binops --- rust-engine/src/backends/lean.rs | 39 ++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 1d9a3da47..ee85ddee7 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -862,6 +862,20 @@ const _: () = { bounds_impls: _, trait_, } => { + let bin_ops = [ + binops::add, + binops::sub, + binops::mul, + binops::div, + binops::rem, + binops::shr, + binops::shl, + binops::bitand, + binops::bitxor, + binops::logical_op_and, + binops::logical_op_or, + binops::Index::index, + ]; match (&args[..], &generic_args[..], head.kind()) { ([arg], [], ExprKind::GlobalId(LIFT)) => docs![reflow!("← "), arg].parens(), ([arg], [], ExprKind::GlobalId(PURE)) => { @@ -883,6 +897,31 @@ const _: () = { ([arg], [], ExprKind::GlobalId(binops::neg)) => { docs!["-?", softline!(), arg].parens() } + ([lhs, rhs], [], ExprKind::GlobalId(op)) if bin_ops.contains(op) => { + if *op == binops::Index::index { + return docs![lhs, "[", line_!(), rhs, line_!(), "]_?"] + .nest(INDENT) + .group(); + } + let symbol = match *op { + binops::add => "+?", + binops::sub => "-?", + binops::mul => "*?", + binops::div => "/?", + binops::rem => "%?", + binops::shr => ">>>?", + binops::shl => "<< "&&&?", + binops::bitxor => "^^^?", + binops::logical_op_and => "&&?", + binops::logical_op_or => "||?", + _ => unreachable!(), + }; + docs![lhs, line!(), docs![symbol, softline!(), rhs].group()] + .group() + .nest(INDENT) + .parens() + } _ => { // Fallback for any application docs![ From 4e3b63ef577f73ad609ad9075b7e64af2b1c9fe4 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 15:08:31 +0100 Subject: [PATCH 07/10] `CHANGELOG.md`: Update --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 33aa8837e..74398dd14 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## [Unreleased] Changes to the Rust Engine: + - Remove `BinOp` resugaring (#1950) Changes to the frontend: From 84975e7c185b31fe3c939f3bc99040b310b9c218 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 16:13:17 +0100 Subject: [PATCH 08/10] `backends/lean.rs`: isolate match pattern for `binops::Index::index` --- rust-engine/src/backends/lean.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index ee85ddee7..7579342ea 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -897,12 +897,12 @@ const _: () = { ([arg], [], ExprKind::GlobalId(binops::neg)) => { docs!["-?", softline!(), arg].parens() } + ([lhs, rhs], [], ExprKind::GlobalId(binops::Index::index)) => { + docs![lhs, "[", line_!(), rhs, line_!(), "]_?"] + .nest(INDENT) + .group() + } ([lhs, rhs], [], ExprKind::GlobalId(op)) if bin_ops.contains(op) => { - if *op == binops::Index::index { - return docs![lhs, "[", line_!(), rhs, line_!(), "]_?"] - .nest(INDENT) - .group(); - } let symbol = match *op { binops::add => "+?", binops::sub => "-?", From 43b87349ffcb2e73648658ddbdd324570cab0069 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 16:28:19 +0100 Subject: [PATCH 09/10] `backends/lean.rs`: remove `bin_ops` list in favor of a pattern --- rust-engine/src/backends/lean.rs | 34 ++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 15 deletions(-) diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 7579342ea..e2446e4fb 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -862,20 +862,6 @@ const _: () = { bounds_impls: _, trait_, } => { - let bin_ops = [ - binops::add, - binops::sub, - binops::mul, - binops::div, - binops::rem, - binops::shr, - binops::shl, - binops::bitand, - binops::bitxor, - binops::logical_op_and, - binops::logical_op_or, - binops::Index::index, - ]; match (&args[..], &generic_args[..], head.kind()) { ([arg], [], ExprKind::GlobalId(LIFT)) => docs![reflow!("← "), arg].parens(), ([arg], [], ExprKind::GlobalId(PURE)) => { @@ -902,7 +888,25 @@ const _: () = { .nest(INDENT) .group() } - ([lhs, rhs], [], ExprKind::GlobalId(op)) if bin_ops.contains(op) => { + // TODO: Replace this match pattern with an `if let` guard when the feature stabilizes + // Tracking PR: https://github.com/rust-lang/rust/pull/141295 + ( + [lhs, rhs], + [], + ExprKind::GlobalId( + op @ (binops::add + | binops::sub + | binops::mul + | binops::div + | binops::rem + | binops::shr + | binops::shl + | binops::bitand + | binops::bitxor + | binops::logical_op_and + | binops::logical_op_or), + ), + ) => { let symbol = match *op { binops::add => "+?", binops::sub => "-?", From a033c488ebddd6a3dfba5b25b8698ed708862286 Mon Sep 17 00:00:00 2001 From: Juan C Date: Mon, 16 Feb 2026 16:59:25 +0100 Subject: [PATCH 10/10] `resugarings.rs`: remove unused import `HashSet` --- rust-engine/src/resugarings.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/rust-engine/src/resugarings.rs b/rust-engine/src/resugarings.rs index be74ebb21..aa68cbffe 100644 --- a/rust-engine/src/resugarings.rs +++ b/rust-engine/src/resugarings.rs @@ -9,7 +9,6 @@ use crate::ast::resugared::*; use crate::ast::visitors::*; use crate::ast::*; use crate::printer::*; -use std::collections::HashSet; /// Transforms [`ItemKind::Fn`] of arity zero into [`ResugaredItemKind::Constant`]. /// Rust `const` items are encoded by the `ImportThir` phase of the hax engine as function of arity zero.