Fix MBA simplification cases reported at REcon 2026; optimize core math#48
Merged
Conversation
Deep Expr structural equality existed only as a file-local helper in OrchestratorPasses.cpp. Move it to ExprUtils (declaration + definition) so other passes can reuse it instead of re-implementing deep comparison. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
GAMBA recon cases obfuscate x | y as the inclusion-exclusion form A + B - (A&B) with arbitrary (including arithmetic, non-disjoint) operands, which CoBRA previously left as a messier equivalent. Add a structural recovery to SimplifyPatternSubtrees that flattens the additive form and collapses +c*A +c*B -c*(A&B) to +c*(A|B), reading A and B from the AND node's children (B may span several additive terms). Gated by a strict coefficient match (so XOR's -2*(A&B) cannot misfire), a cost-reduction check, and a FullWidthCheck soundness backstop. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
For a single-product input, ExtractProductCore returns a core equal to the whole input, whose direct full-width check trivially passes. Emitting it as a solved candidate halts the worklist before the decomposition/signature passes can recover a simpler form, so GAMBA recon cases like the parity sign-square (x1+x2)*(1-2*(x3&1))*(1-2*(x3&1)) (and its XOR-self-cancel full form) were left unchanged. Decline the short-circuit when the product core is the whole input (single_product) AND a full-width-confirmed spurious variable exists, so the worklist continues to the extractors that recover the reduced form. Genuine sum-of-product cores and cores with no spurious variable are unaffected, so product-inside-bitwise decomposition (QSynth, Multivariate) is preserved. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
The {0,1} signature of a high-bit masking result like x & 128 is all-zero (bit 7
is invisible on {0,1}), so the boolean candidate is 0 and fails the full-width
check. The case is solved by AuxVarEliminator + TemplateDecomposer, but its atom
pool seeded only {0, 1, 2, mask}, so it could not synthesize the literal mask
constant M for M >= 8 within the bounded layer depth. GAMBA recon cases like
((x & 128) + (y & 127)) & 128 (carry-free masked add: y&127 < 128 is disjoint
from bit 7) were left unsupported.
Seed data-derived constants into the pool after Populate: the OR-fold of the
observed probe outputs (recovers the mask) plus a few distinct output values
(cover split masks). Soundness is unchanged -- every candidate is
FullWidthCheckEval-gated, so extra constants only widen the search, and a genuine
carry (((x & 255) + (y & 255)) & 255) is not falsely collapsed to x & 255.
Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
(A ^ B) ^ B == A is exact at every bit width, but when the surviving operand A
has a degenerate {0,1} signature (e.g. ((x+y)&z)|3, which is constant 3 on
{0,1}), no signature or decomposition pass re-emits it, so the worklist
exhausts and CoBRA echoes the obfuscated input unchanged.
Add SimplifyXorChains (top-down: flatten each XOR chain and drop operands of
even multiplicity by exact structural equality) and apply it as an exhaustion
fallback in the orchestrator -- when the raw input collapses to a strictly
cheaper form, return that instead of reporting unsupported. The cancellation is
an exact algebraic identity (not a full-width approximation), so the result is
provably equivalent; the full-width check is defense in depth and the fallback
only fires on the otherwise-doomed exhaustion path.
QSynthEA gains 2 cases (verify-failed 7->6, search-exhausted 21->20) whose
inputs contained structurally-repeated XOR operands.
Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
A CoB-linear function such as sum(xi) - xor(xi) is recovered by change-of-basis as a linear combination of AND-basis monomials whose size grows exponentially with the variable count (an 8-variable input of ~30 weighted nodes expanded to ~1000). The core Simplify path had no input-vs-output size check, so it returned the blow-up even though the input was already minimal. Guard in ToSimplifyOutcome: when a successful result both more than doubles the input AND exceeds an absolute floor (32 weighted nodes), keep the input instead and report it unsupported with a kCostRejected reason. The ratio spares genuine simplifications of large obfuscated inputs (cheaper output); the absolute floor spares the small expansions of legitimate canonicalization (e.g. NOT-over-arith lowering ~(b*b) -> -(b*b)-1, which roughly doubles a tiny expression). Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
The product-core no-op short-circuit ran the 128-probe full-width EliminateAuxVars on every single-product core. Full-width spurious variables are always a subset of the boolean ones, so an empty boolean result is final: run the cheap 2-arg EliminateAuxVars first and only escalate to the full-width overload when it finds a candidate. The gate decision is unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
TryRecoverInclusionExclusion flattened every additive subtree during pattern-subtree peeling, even those with no AND term to recover. Add a no-allocation precondition (AdditiveHasBinaryAnd) that mirrors FlattenAdditive's descent and returns true only for the additive trees that contain a top-level 2-child AND term -- the only terms TryRecoverDisjunctionAt can act on. Additive nodes without an AND term now skip the flatten and per-term scan entirely. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
The data-derived constant seeding could Probe() and Push() the same constant value repeatedly (or_fold and several equal target values). Push already dedups the pool by probe-vals, so the repeats only wasted Probe() calls. Track seeded values in a set and skip duplicates; the resulting pool is identical. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
…r match - Merge the duplicated owning FlattenAdd and FlattenMul into one FlattenAssoc(node, kind, out); update the three call sites. - Add ContainsXor (mirrors ContainsShr) for the orchestrator XOR guard. - Match common factors in ExtractCommonFactor by ExprStructurallyEqual instead of a hash-plus-kind filter. Structural equality never matches a non-equal factor, removing the hash-collision unsoundness the docstring previously accepted; update the docstring to match. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
…ostics - Extract the output-size blow-up gate into IsCostBlowup(candidate, baseline) with named kBlowupRatio/kBlowupAbsFloor constants. Semantics are unchanged (output > 2x input and > 32 weighted size). - Compute the input expression cost once in Simplify() and thread it through ToSimplifyOutcome, reusing it in the XOR exhaustion fallback so the input cost is no longer computed twice on that path. - On the XOR-cancel success path, clear the exhaustion failure lineage (reason_code, cause_chain, candidate_failed_verification) so a kSimplified result no longer reports a stale search-exhausted reason. - Guard the XOR fallback with ContainsXor so the clone and walk are skipped when the input has no XOR. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
Both helpers were identical except for the node kind they matched. Replace them with one ContainsType(expr, kind) and update all call sites (Orchestrator shift/xor guards, SemilinearNormalizer, StructureRecovery, the mask-audit bench, and the dynamic-mask tests). Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
Seed the Hensel inverse with ((3*x) ^ 2), which is correct to 5 bits (vs 3 for the bare x), so the doubling loop runs one fewer iteration at every width (4 instead of 5 at 64-bit). Output is the unique inverse mod 2^bits, so it is bit-identical to the previous seed. Add exhaustive small-width and random 64-bit correctness tests. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
ModInverseOddHalf(x, w) is exactly the odd inverse at width w-1, so replace its duplicated Hensel loop with a call to ModInverseOdd(x, w-1). It keeps its name and tests and inherits the stronger seed. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
Replace the scan-all-indices-with-branch Mobius loop with the canonical block butterfly: each variable pairs index i with i+half over half-blocks, touching exactly len/2 elements per variable with no per-element bit test and contiguous access. Same subset-Mobius transform. Add a randomized property test against a naive Mobius reference. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
…Poly Extract the forward-difference + factorial-coefficient conversion into RecoverFromGrid. RecoverAndVerifyPoly now keeps an incrementally-grown evaluation grid across degrees min..cap: each higher degree extends the grid by its new shell instead of re-evaluating the whole grid from scratch, so every support point is evaluated at most once. Reuse is exact because the evaluator is pure; per-degree results, early-exit, and reason codes are unchanged. RecoverMultivarPoly evaluates its grid then delegates to RecoverFromGrid, so its behavior is identical. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
The bottom-up boolean-signature evaluator allocated a fresh 2^n result vector per tree node. Thread a free-list buffer pool through the recursion: binary nodes release their right child's buffer, which leaf nodes then reuse. This bounds live buffers (and allocations) to ~tree depth instead of one per leaf. Output is bit-identical. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
The matrix build recomputed FallingFactorial(coord, exp) once per (row, col, dim) for only (grid_base) x (per_var_cap+1) distinct pairs. Precompute the table once per solve and look it up. Bit-identical. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
OddPartFactorial(e, bw) equals the 64-bit odd-part product masked to bw, so build a per-degree table once (incrementally) and use it under the existing kPrecMask instead of recomputing the odd-part product per monomial. Bit-identical. Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
kyle-elliott-tob
changed the title
Co-Authored-By: Claude Opus 4.8 (1M context) <[email protected]>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This branch lands two related bodies of work on the simplifier.
MBA simplification fixes (reported by @arnaugamez at REcon 2026)
Fixes for MBA expressions CoBRA did not simplify before — left unsupported,
returned unchanged, or expanded into a larger form:
A | Bfrom the inclusion-exclusion formA + B - (A & B)during pattern-subtree peeling.((x & 2^k) + (y & (2^k - 1))) & 2^k -> x & 2^kby seeding mask constants in the template decomposer.(A ^ B) ^ B -> Aat the exhaustion fallback (exact rewrite, full-width-checked).sum(xi) - xor(xi)) keeps the smaller input instead of an exponential AND-basis form.Simplifier cleanup and core-math optimization
Follow-on refactors and performance work, all behavior-preserving (bit-identical
outputs; dataset counts unchanged):
ExprStructurallyEqualtoExprUtils; generalizeContainsShr/ContainsXorintoContainsType(expr, kind); mergeFlattenAdd/FlattenMulinto oneFlattenAssoc; match common factors inExtractCommonFactorby structural equality.IsCostBlowup; compute the input cost once and thread it; clear the stale exhaustion reason on the XOR-cancel success path; guard the XOR fallback withContainsType.ModInverseOdd(one fewer doubling iteration); delegateModInverseOddHalftoModInverseOdd; canonical block butterfly inInterpolateCoefficients; reuse the interpolation grid across degrees inRecoverAndVerifyPoly(each support point evaluated once); recycle per-node buffers inEvalSigRecursive; precompute the falling-factorial and odd-part-factorial tables inWeightedPolyFitandRecoverFromGrid.Testing
Credits
Bug reports by Arnau Gamez (@arnaugamez), raised during his REcon 2026 talk.
🤖 Generated with Claude Code