Fix MBA simplification cases reported at REcon 2026; optimize core math

include/cobra/core/DecompositionEngine.h

@@ -40,6 +40,9 @@ namespace cobra {
         std::unique_ptr< Expr > expr;
         ExtractorKind kind;
         uint8_t degree_used = 0;
+        // kProductAST only: true when the whole input is a single product term
+        // (SplitAddTree found no additive split), i.e. the core equals the input.
+        bool single_product = false;
     };
 
     struct DecompositionResult

include/cobra/core/ExprCost.h

@@ -22,4 +22,16 @@ namespace cobra {
 
     bool IsBetter(const ExprCost &candidate, const ExprCost &baseline);
 
+    // Returns true when `candidate` is a pathological size blow-up relative to
+    // `baseline`. A blow-up must clear two bars at once: it more than doubles
+    // the baseline's weighted size AND is large in absolute terms. The ratio
+    // catches change-of-basis expansions proportional to a large input (e.g.
+    // sum(xi) - xor(xi) recovers an exponential AND-basis form); the absolute
+    // floor spares the small ~2x expansions of legitimate canonicalization
+    // (NOT-over-arith lowering ~(b*b) -> -(b*b)-1 roughly doubles a tiny
+    // expression). This is deliberately keyed on weighted_size alone: it is a
+    // size-explosion guard, distinct from IsBetter's full lexicographic
+    // "is this an improvement" comparison.
+    bool IsCostBlowup(const ExprCost &candidate, const ExprCost &baseline);
+
 } // namespace cobra

include/cobra/core/ExprUtils.h

@@ -18,6 +18,10 @@ namespace cobra {
     /// Rewrite every kVariable node's var_index through index_map.
     void RemapVarIndices(Expr &expr, const std::vector< uint32_t > &index_map);
 
+    /// Deep structural equality: same kind, constant, var_index, and children
+    /// (in order). Unlike std::hash<Expr> this never reports false positives.
+    bool ExprStructurallyEqual(const Expr &lhs, const Expr &rhs);
+
     /// Map a subset of variable names to their indices in the full variable list.
     std::vector< uint32_t > BuildVarSupport(
         const std::vector< std::string > &all_vars,
@@ -27,8 +31,8 @@ namespace cobra {
     /// Check if an Expr subtree contains only constants (no variables).
     bool IsConstantSubtree(const Expr &expr);
 
-    /// Returns true if any node in the AST is kShr.
-    bool ContainsShr(const Expr &expr);
+    /// Returns true if any node in the AST has the given kind.
+    bool ContainsType(const Expr &expr, Expr::Kind kind);
 
     /// Append the var_index of every kVariable node (pre-order). Duplicates
     /// are preserved; callers that want a deduplicated support set must
@@ -46,13 +50,9 @@ namespace cobra {
     /// Chains: constant folding → negation refolding → ExtractCommonFactor
     /// → constant folding.
     ///
-    /// Semantics-preserving under the assumption that std::hash<Expr>
-    /// does not collide on the input AST. ExtractCommonFactor uses
-    /// hash-based factor equality, so a hash collision could in
-    /// principle produce a non-equivalent rewrite. The hash-collision
-    /// tradeoff is accepted at the project level (see audit
-    /// 2026-05-04 lifting-passes-29 / -65). Callers requiring strict
-    /// semantics-preservation must re-verify the result.
+    /// Semantics-preserving: ExtractCommonFactor matches common factors by
+    /// exact structural equality (ExprStructurallyEqual), so the distributive
+    /// rewrite never fires on a non-equal factor.
     std::unique_ptr< Expr > CleanupFinalExpr(std::unique_ptr< Expr > expr, uint32_t bitwidth);
 
     /// Check if an Expr subtree depends on any variable.

include/cobra/core/MathUtils.h

@@ -37,15 +37,17 @@ namespace cobra {
     }
 
     // Modular inverse of an odd number x modulo 2^bits.
-    // Hensel lifting: x*x = 1 mod 8 for all odd x, so 3 bits are
-    // correct initially. Each iteration doubles the number of
-    // correct bits.
+    // Newton/Hensel lifting: the seed ((3 * x) ^ 2) -- i.e. (3*x) XOR 2, not a
+    // square -- satisfies x * seed = 1 mod 32 for all odd x, so 5 bits are
+    // correct initially. Each iteration doubles the correct bits
+    // (5 -> 10 -> 20 -> 40 -> 80), so 64-bit inverses need 4 iterations. (The
+    // bare seed x is correct to only 3 bits and would need a 5th iteration.)
     inline uint64_t ModInverseOdd(uint64_t x, uint32_t bits) {
         assert(bits >= 1);
         assert(x & 1);
         const uint64_t kModMask = Bitmask(bits);
-        uint64_t inv            = x & kModMask;
-        for (uint32_t b = 3; b < bits; b *= 2) { inv = (inv * (2 - (x * inv))) & kModMask; }
+        uint64_t inv            = ((3 * x) ^ 2) & kModMask;
+        for (uint32_t b = 5; b < bits; b *= 2) { inv = (inv * (2 - (x * inv))) & kModMask; }
         return inv & kModMask;
     }
 

include/cobra/core/PatternMatcher.h

@@ -20,4 +20,10 @@ namespace cobra {
     std::unique_ptr< Expr >
     SimplifyPatternSubtrees(std::unique_ptr< Expr > expr, uint32_t bitwidth);
 
+    // Recursively cancel XOR operands that appear an even number of times
+    // (T ^ T == 0), flattening nested XOR chains. This is an exact algebraic
+    // identity (no full-width approximation), so the result is provably
+    // equivalent to the input at every bit width.
+    std::unique_ptr< Expr > SimplifyXorChains(std::unique_ptr< Expr > expr, uint32_t bitwidth);
+
 } // namespace cobra

lib/core/CoeffInterpolator.cpp

@@ -28,12 +28,16 @@ namespace cobra {
         // "without this variable" entry from the "with" entry to isolate its
         // contribution. Equivalent to evaluating directly in the (1, x, y, x&y)
         // basis rather than computing a change-of-basis matrix.
+        //
+        // Canonical block butterfly: each var pairs index i (bit clear) with
+        // i + half (bit set), so we touch exactly len/2 elements per var with
+        // no per-element bit test and contiguous access within each half-block.
         for (uint32_t var = 0; var < num_vars; ++var) {
-            const uint32_t stride = 1U << var;
-            for (size_t i = 0; i < len; ++i) {
-                if ((i & stride) != 0u) {
-                    const size_t i0 = i & ~static_cast< size_t >(stride);
-                    sig[i]          = (sig[i] - sig[i0]) & mask;
+            const size_t half  = size_t{ 1 } << var;
+            const size_t block = half << 1;
+            for (size_t base = 0; base < len; base += block) {
+                for (size_t i = base; i < base + half; ++i) {
+                    sig[i + half] = (sig[i + half] - sig[i]) & mask;
                 }
             }
         }

lib/core/CoefficientSplitter.cpp

@@ -1,5 +1,6 @@
 #include "cobra/core/CoefficientSplitter.h"
 #include "cobra/core/BitWidth.h"
+#include "cobra/core/MathUtils.h"
 #include "cobra/core/Trace.h"
 #include <bit>
 #include <cassert>
@@ -12,20 +13,8 @@ namespace cobra {
 
     uint64_t ModInverseOddHalf(uint64_t x, uint32_t w) {
         assert(w >= 2);
-        assert(x & 1);
-
-        // Target: x^{-1} mod 2^{w-1}.
-        // Hensel lifting: inv = x is correct mod 2^3 (since x^2 = 1 mod 8
-        // for all odd x). Each iteration doubles correct bits.
-        const uint32_t kTargetBits = w - 1;
-        const uint64_t kModMask = (kTargetBits >= 64) ? UINT64_MAX : (1ULL << kTargetBits) - 1;
-
-        uint64_t inv = x & kModMask;
-        // ceil(log2(kTargetBits)) iterations, starting from 3 correct bits
-        for (uint32_t bits = 3; bits < kTargetBits; bits *= 2) {
-            inv = (inv * (2 - (x * inv))) & kModMask;
-        }
-        return inv & kModMask;
+        // x^{-1} mod 2^{w-1} is exactly the general odd inverse at width w-1.
+        return ModInverseOdd(x, w - 1);
     }
 
     namespace {

lib/core/DecompositionEngine.cpp

@@ -157,8 +157,9 @@ namespace cobra {
         }
 
         CoreCandidate core;
-        core.expr = std::move(core_expr);
-        core.kind = ExtractorKind::kProductAST;
+        core.expr           = std::move(core_expr);
+        core.kind           = ExtractorKind::kProductAST;
+        core.single_product = (products.size() == 1);
         return SolverResult< CoreCandidate >::Success(std::move(core));
     }
 

lib/core/DecompositionPasses.cpp

@@ -166,6 +166,30 @@ namespace cobra {
                 FullWidthCheckEval(*active_eval, num_vars, *core_payload.expr, ctx.bitwidth);
 
             if (direct_check.passed) {
+                // A degenerate product core -- the whole input as a single
+                // product term (single_product) -- "passes" the direct check
+                // only because it IS the input. Emitting it short-circuits the
+                // worklist as a no-op winner before the decomposition/signature
+                // passes can recover a simpler form. When such a core also has a
+                // (full-width-confirmed) spurious variable, a real reduction is
+                // reachable, so decline the short-circuit and let later passes
+                // run. Genuine sum-of-product cores (single_product == false)
+                // and cores with no spurious variable are unaffected. The
+                // cheap boolean elimination gates the 128-probe full-width
+                // confirmation: full-width spurious vars are always a subset
+                // of the boolean ones, so an empty boolean result is final.
+                if (expected_kind == ExtractorKind::kProductAST && core_payload.single_product
+                    && !EliminateAuxVars(decomp_sig, active_vars).spurious_vars.empty()
+                    && !EliminateAuxVars(decomp_sig, active_vars, *active_eval, ctx.bitwidth)
+                            .spurious_vars.empty())
+                {
+                    return Ok(
+                        PassResult{
+                            .decision    = PassDecision::kNotApplicable,
+                            .disposition = ItemDisposition::kRetainCurrent,
+                        }
+                    );
+                }
                 auto cost_info = ComputeCost(*core_payload.expr);
                 WorkItem cand_item;
                 cand_item.payload = CandidatePayload{

lib/core/ExprCost.cpp

@@ -92,4 +92,14 @@ namespace cobra {
             );
     }
 
+    bool IsCostBlowup(const ExprCost &candidate, const ExprCost &baseline) {
+        // Output must exceed this multiple of the input to count as a blow-up.
+        constexpr uint32_t kBlowupRatio    = 2;
+        // ...and exceed this absolute weighted size, sparing the small ~2x
+        // expansions of legitimate canonicalization on tiny inputs.
+        constexpr uint32_t kBlowupAbsFloor = 32;
+        return candidate.weighted_size > kBlowupRatio * baseline.weighted_size
+            && candidate.weighted_size > kBlowupAbsFloor;
+    }
+
 } // namespace cobra

lib/core/ExprUtils.cpp

@@ -32,6 +32,18 @@ namespace cobra {
         for (auto &child : expr.children) { RemapVarIndices(*child, index_map); }
     }
 
+    bool ExprStructurallyEqual(const Expr &lhs, const Expr &rhs) {
+        if (lhs.kind != rhs.kind || lhs.constant_val != rhs.constant_val
+            || lhs.var_index != rhs.var_index || lhs.children.size() != rhs.children.size())
+        {
+            return false;
+        }
+        for (size_t i = 0; i < lhs.children.size(); ++i) {
+            if (!ExprStructurallyEqual(*lhs.children[i], *rhs.children[i])) { return false; }
+        }
+        return true;
+    }
+
     std::unique_ptr< Expr > BuildAndProduct(uint64_t mask) {
         std::unique_ptr< Expr > result;
         while (mask != 0) {
@@ -60,10 +72,10 @@ namespace cobra {
         });
     }
 
-    bool ContainsShr(const Expr &expr) {
-        if (expr.kind == Expr::Kind::kShr) { return true; }
-        return std::ranges::any_of(expr.children, [](const auto &child) {
-            return ContainsShr(*child);
+    bool ContainsType(const Expr &expr, Expr::Kind kind) {
+        if (expr.kind == kind) { return true; }
+        return std::ranges::any_of(expr.children, [kind](const auto &child) {
+            return ContainsType(*child, kind);
         });
     }
 
@@ -133,15 +145,17 @@ namespace cobra {
 
     namespace {
 
-        // Flatten a left-folded Add chain into a list of terms.
-        void FlattenAdd(
-            std::unique_ptr< Expr > node, std::vector< std::unique_ptr< Expr > > &terms
+        // Flatten a left-folded binary associative chain of `kind` (kAdd or
+        // kMul) into its operand list, moving each leaf out of the tree.
+        void FlattenAssoc(
+            std::unique_ptr< Expr > node, Expr::Kind kind,
+            std::vector< std::unique_ptr< Expr > > &out
         ) {
-            if (node->kind == Expr::Kind::kAdd) {
-                FlattenAdd(std::move(node->children[0]), terms);
-                FlattenAdd(std::move(node->children[1]), terms);
+            if (node->kind == kind) {
+                FlattenAssoc(std::move(node->children[0]), kind, out);
+                FlattenAssoc(std::move(node->children[1]), kind, out);
             } else {
-                terms.push_back(std::move(node));
+                out.push_back(std::move(node));
             }
         }
 
@@ -161,7 +175,7 @@ namespace cobra {
             if (expr->kind != Expr::Kind::kAdd) { return expr; }
 
             std::vector< std::unique_ptr< Expr > > terms;
-            FlattenAdd(std::move(expr), terms);
+            FlattenAssoc(std::move(expr), Expr::Kind::kAdd, terms);
 
             uint64_t const_sum = 0;
             std::vector< std::unique_ptr< Expr > > non_const;
@@ -214,18 +228,6 @@ namespace cobra {
             return expr;
         }
 
-        // Flatten binary Mul chain into factor list.
-        void FlattenMul(
-            std::unique_ptr< Expr > node, std::vector< std::unique_ptr< Expr > > &factors
-        ) {
-            if (node->kind == Expr::Kind::kMul) {
-                FlattenMul(std::move(node->children[0]), factors);
-                FlattenMul(std::move(node->children[1]), factors);
-            } else {
-                factors.push_back(std::move(node));
-            }
-        }
-
         // Rebuild a left-folded Mul chain from a factor list.
         std::unique_ptr< Expr > RebuildMul(std::vector< std::unique_ptr< Expr > > &factors) {
             auto result = std::move(factors[0]);
@@ -248,7 +250,7 @@ namespace cobra {
 
             // Flatten the Add chain.
             std::vector< std::unique_ptr< Expr > > terms;
-            FlattenAdd(std::move(expr), terms);
+            FlattenAssoc(std::move(expr), Expr::Kind::kAdd, terms);
 
             if (terms.size() < 2) {
                 if (terms.size() == 1) { return std::move(terms[0]); }
@@ -266,7 +268,7 @@ namespace cobra {
             for (auto &t : terms) {
                 TermFactors tf;
                 if (t->kind == Expr::Kind::kMul) {
-                    FlattenMul(std::move(t), tf.factors);
+                    FlattenAssoc(std::move(t), Expr::Kind::kMul, tf.factors);
                 } else {
                     tf.factors.push_back(std::move(t));
                 }
@@ -280,9 +282,8 @@ namespace cobra {
                 if (candidate->kind == Expr::Kind::kConstant) { continue; }
                 if (candidate->kind == Expr::Kind::kVariable) { continue; }
 
-                auto candidate_hash = std::hash< Expr >{}(*candidate);
-
-                // Check all other terms for this factor.
+                // Check all other terms for this factor, matching on exact
+                // structural equality (never a false positive, unlike a hash).
                 bool universal = true;
                 std::vector< size_t > match_indices;
                 match_indices.push_back(fi);
@@ -291,11 +292,7 @@ namespace cobra {
                     for (size_t fj = 0; fj < all_factors[ti].factors.size(); ++fj) {
                         auto &f = all_factors[ti].factors[fj];
                         if (f->kind == Expr::Kind::kConstant) { continue; }
-                        if (std::hash< Expr >{}(*f) == candidate_hash
-                            && f->kind == candidate->kind)
-                        {
-                            // Deep equality check via CloneExpr comparison.
-                            // Use the hash as strong filter — collisions are rare.
+                        if (ExprStructurallyEqual(*f, *candidate)) {
                             found = true;
                             match_indices.push_back(fj);
                             break;