Redesign symbolic size expressions for exact maps and certified bounds

[isPANN]

Background

Reduction metadata currently uses one lossy Expr representation for exact structural size calculation, symbolic composition, and asymptotic growth. Constants become f64, missing variables evaluate as zero, and concrete results are rounded and cast to usize. It also lacks one exact canonical representation shared by contract-specific consumers. The audit in #1125 demonstrates that these semantics cannot support trustworthy Pareto ranking.

Complexity theory also separates exact construction facts from certified resource bounds:

• parameterized reductions require k' <= g(k), not equality (Marx, Parameterized Reduction);
• kernelization bounds output size by a function of the parameter, and Turing kernelization may produce several instances (Witteveen–Bottesch–Torenvliet);
• fine-grained Turing reductions control the sum of costs over multiple query sizes rather than one terminal size (Carmosino et al., Definition 1);
• treewidth-dependent constructions may assume a supplied tree decomposition rather than computing exact treewidth (Kolman–Koutecký).

This issue is a complete replacement, not a compatibility migration. The existing formula text syntax may remain because it is adequate, but the old AST, old evaluator, ambiguous overhead contract, and all superseded call paths must be removed.

Objective

Build one exact canonical symbolic-expression core and three explicit consumers:

1. SizeMap: checked equalities for exact concrete target sizes.
2. SizeBound: certified monotone inequalities for conservative target bounds.
3. Growth: asymptotic simplification and display.

Migrate every registered reduction to the new contracts. Every registered target size field must be explicitly accounted for as exact, bound-only, or unavailable with a reason. No existing declaration is automatically reinterpreted as exact or certified merely to preserve behavior.

Canonical expression representation

Keep one formula parser and one public canonical semantic DAG shared by runtime and proc macros:

enum ExprNode {
    Const(BigRational),
    Var(Symbol),
    Add(Box<[Expr]>),
    Mul(Box<[Expr]>),
    Pow(Expr, Expr),
    Exp(Expr),
    Log(Expr),
    Factorial(Expr),
}

struct Expr(Arc<ExprNode>);

The expression domain is eventually-positive problem-size functions. The public representation is a mathematical IR, not a source-syntax tree. Parsing lowers equivalent syntax immediately:

a - b   -> a + (-1) * b
a / b   -> a * b^-1
-a      -> (-1) * a
sqrt(a) -> a^(1/2)

Requirements:

• Decimal literals are parsed exactly into arbitrary-precision rationals; 2.372 becomes 593/250 without passing through binary floating point.
• Integer intermediates use arbitrary precision. Fixed-width overflow is checked only when converting an exact constructed size to the repository's concrete ProblemSize representation.
• Add and Mul are flattened, constants are folded exactly, equal terms and powers are combined, and operands have deterministic structural order.
• Canonicalization must preserve the value of eventually-positive size functions. Consumers validate the canonical semantic expression rather than the author's surface spelling.
• Variable names are owned. Runtime parsing must not leak strings for 'static lifetimes.
• The proc macro and runtime parser share the same grammar and AST semantics. Delete the current ParsedExpr/Expr semantic duplication.
• Substitution, composition, equality, hashing where required, serialization, display, variable collection, and growth conversion are implemented once against the canonical DAG.
• Immutable Arc sharing and traversal-local memoization keep repeated path composition proportional to the unique DAG rather than an expanded expression tree.

SizeMap

SizeMap is a validated mapping from target field names to canonical Expr values.

source ProblemSize + SizeMap -> exact target ProblemSize | SizeMapError

Construction accepts only integral constants, fields, addition, subtraction, multiplication, exact division, and non-negative integral powers. Validation compiles expressions into a private checked-integer form; invalid operators are rejected before evaluation. Runtime evaluation has no approximate branch.

Errors name the edge and target field and distinguish:

• missing input field;
• negative output;
• non-integral division/result;
• division by zero;
• concrete target size outside the supported ProblemSize range.

Maximum Independent Set → Clique:

num_vertices = num_vertices
num_edges = num_vertices * (num_vertices - 1) / 2 - num_edges

For (num_vertices=5, num_edges=4), the exact result is (5, 6).

SizeBound

SizeBound is a separately validated mapping from target fields to conservative monotone expressions.

source bound vector + SizeBound -> target bound vector | SizeBoundError

• Bound values use arbitrary-precision non-negative integers so a mathematically valid bound is not truncated to usize.
• Registration rejects expressions that are not proven monotone in every referenced input field.
• After canonicalization, negative coefficients, negative variable powers, and functions without a structural monotonicity rule cannot enter SizeBound. If canonicalization eliminates such syntax completely, validation uses the resulting semantic expression.
• Certified-bound Big-O is derived from SizeBound. When requested, an exact terminal SizeMap expression may also be projected to Growth; neither projection may re-enter path composition or construct a concrete ProblemSize.

Maximum Independent Set → Clique may use:

num_vertices = num_vertices
num_edges = num_vertices ^ 2

No choose2 or other special formula syntax is introduced.

Explicit field accounting

For every registered reduction and every registered target size field, metadata must say one of:

• an exact formula is present in SizeMap;
• a certified upper formula is present in SizeBound but exact propagation is unavailable;
• propagation is unavailable, with a concise reason naming the missing statistic or hard parameter.

An exact field may also have a separate monotone bound. Absence is never interpreted as zero, identity, a same-named field, or permission to use the other contract.

Exact treewidth is not added as a required field. A width bound is admissible only when already present as cheap input metadata or when a decomposition/certificate is part of the model input.

Numeric targets such as ILP, QUBO, Knapsack, and Factoring must account for encoding/coefficient bit length where needed for a valid complexity bound; variable and constraint counts alone are not treated as total encoding size.

Search semantics

Expose two separate APIs and result types:

• Exact search: every required field on every edge must have a SizeMap; compare exact terminal vectors only.
• Certified-bound search: compose SizeBound; compare terminal guaranteed-bound vectors only.

Rules:

• no fallback between modes;
• no shared Pareto frontier between exact and bound results;
• no default mode that silently selects one based on availability;
• retain distinct intermediate paths;
• apply dominance only at the requested terminal problem;
• exclude Turing/multi-query edges from single-target size ranking until they receive a separate query-cost model.

Implementation requirements

1. Replace the existing expression AST and both parsing/code-generation paths with the exact canonical immutable DAG described above.
2. Delete the floating concrete evaluator, missing-variable default, rounding, saturation, leaked variable names, and superseded parser/evaluator code.
3. Reimplement Growth on the canonical AST and confine floating approximation to an explicitly named complexity-estimation boundary.
4. Implement SizeMap, its validation, checked evaluation, errors, and constructed-target oracle.
5. Implement SizeBound, monotonicity validation, arbitrary-precision bound evaluation/composition, and errors.
6. Replace reduction registry metadata and macro syntax directly; do not accept legacy overhead as an alias.
7. Migrate all registered reductions. Do not automatically classify existing formulas; inspect their construction or proof and declare exact, bound, or unavailable deliberately.
8. Replace all library, CLI, MCP, export, documentation, and test callers; delete unused forwarding and compatibility code.
9. Preserve complete-path terminal-only Pareto semantics from Redesign reduction-path selection around final composed overhead #1093/PR Symbolic growth, exact Pareto path search, and deterministic solver backends #1083.

The implementation may be large. Architectural completeness takes priority over minimizing changed files or lines. If delivery is split for review, each change must follow an explicit dependency sequence on one integration branch; no intermediate compatibility layer may land on main, and the final merge removes every superseded path.

Verification

Provide one repository-wide behavioural suite:

cargo test symbolic_size_contracts --features example-db -- --nocapture

It must print counts and a final PASS, and prove:

1. Canonical DAG: n * (n - 1) / 2 - m deterministically normalizes to -1 * m + n * (-1 + n) * 2^-1, and that canonical form survives serialize/deserialize/display.
2. Exact literals: 2.372 is exactly 593/250.
3. Owned variables: repeated runtime parsing of dynamic variable names does not leak allocations.
4. Known exact map: the canonical five-vertex, four-edge Maximum Independent Set → Clique case predicts and constructs (5, 6).
5. Known bound: the same constructed target satisfies its certified bound.
6. Repository accounting: every registered target size field is classified; the test prints total exact, bound-only, and unavailable field counts, and reports zero unclassified fields.
7. Exact oracle: every executable canonical example with declared exact fields matches the independently measured constructed target field-by-field; checked count equals eligible count and mismatch count is zero.
8. Bound oracle: every executable canonical example with declared bounds satisfies them field-by-field; checked count equals eligible measurable bound count and violation count is zero.
9. Exact negative controls: missing field, negative result, non-integral result, division by zero, and out-of-range concrete output are rejected.
10. Bound controls: canonical expressions with an irreducible negative coefficient (n - m) or negative variable power (n / m) are rejected during SizeBound construction; an expression such as n - n may normalize to the admissible constant zero.
11. Contract isolation: exact search on a path lacking a required map returns unavailable and never consults its bound; bound search never reports an exact result.
12. Growth isolation: exp(n) remains valid for complexity/growth handling but cannot enter SizeMap or produce ProblemSize.
13. No local pruning: the synthetic complement case retains both prefixes and compares only terminal results.
14. No legacy path: the old floating concrete evaluator and ambiguous legacy registry fields have been deleted while the behavioural suite and full repository checks pass.

Then run:

make check
cargo test --manifest-path problemreductions-cli/Cargo.toml

Both commands must exit successfully.

Dependencies

• Builds on the audit and known-answer fixture in Make reduction size overhead exact and verifiable before Pareto comparison #1125.
• Supersedes Make reduction size overhead exact and verifiable before Pareto comparison #1125's assumption that Big-O must universally derive from exact formulas.
• Preserves Redesign reduction-path selection around final composed overhead #1093 and PR Symbolic growth, exact Pareto path search, and deterministic solver backends #1083 terminal-only comparison semantics.

Out of scope

• Compatibility aliases or dual old/new execution paths.
• Automatic reinterpretation of existing overhead declarations.
• choose2 or other special syntax added only for this feature.
• Exact or approximate treewidth computation.
• Generic tree-decomposition/certificate infrastructure.
• Learned or empirical solver-cost prediction.
• Turing query-cost modeling.
• Mixing exact and certified-bound results in one frontier.

[isPANN]

Open-source design review: decisions adopted for this application

This design was checked against mature symbolic systems and solver infrastructure, then narrowed to the needs of reduction-size propagation.

Adopt

1. One authoritative, lossless source expression

   • Follow Symbolica's general-expression to restricted-representation pattern: parse once into Expr, then validate/compile it for SizeMap, SizeBound, or Growth.
   • The restricted forms are private semantic plans, not additional public ASTs and not additional parsers.
   • Because the runtime library and proc-macro crate cannot depend on each other, the AST and parser must live in a small macro-independent internal crate shared by both.

2. Exact and approximate numeric domains are separate

   • Follow SymPy, Symbolica, and Z3: integer/rational literals are exact; approximation is an explicit operation at the growth-estimation boundary.
   • Use num_bigint::BigInt, num_bigint::BigUint, and num_rational::BigRational; do not implement repository-local arbitrary-precision numbers.
   • Parse decimals from text directly. Never construct an exact constant by first passing it through f64.

3. Validation is consumer-specific

   • SizeMap::try_from(Expr) admits the exact-integer fragment and compiles it to checked integer evaluation.
   • SizeBound::try_from(Expr) admits only expressions whose non-negativity and monotonicity follow structurally from the size-domain rules.
   • Growth::from(Expr) may normalize and approximate after the exact/bound contracts have been separated.

4. Bound proof uses a deliberately small structural calculus

   • All source size fields have domain N.
   • Non-negative constants and variables are non-negative and monotone.
   • Addition and multiplication of non-negative monotone expressions preserve those properties.
   • A non-negative integral power preserves those properties.
   • Canonical expressions with negative coefficients, negative variable powers, or functions without a built-in monotonicity rule are rejected; validation does not reject surface syntax that canonicalization has eliminated.
   • If a construction has a valid but non-monotone exact formula, authors provide a separate looser monotone bound, such as n^2 for complement edges.
   • Cross-field facts such as m <= n(n-1)/2 are not silently assumed.

5. Use one canonical semantic DAG before consumer validation

   • The public expression is a mathematical IR for eventually-positive size functions, not a source-syntax tree.
   • Parsing lowers subtraction, division, negation, and square root into Add, Mul, and Pow, then performs deterministic exact canonicalization.
   • Consumer validation is semantic: n - n may normalize to the valid constant zero, while irreducible negative coefficients or negative variable powers remain visible and are rejected by SizeBound.
   • Growth may perform additional consumer-specific analysis, but it does not own another parser or public AST.

Deliberately reject

• No SymPy-style general assumptions engine. It is substantially more complex than our domain and still does not make arbitrary relations between size fields easy to prove.
• No SMT dependency for registration. Z3's exact arithmetic sorts are a useful model for domain separation, but solver-backed monotonicity would make validity depend on theorem-proving behavior and cost.
• No e-graph/equality saturation. egg is appropriate when many rewrite alternatives must be explored; our expressions are small and our transformations are fixed.
• No full CAS dependency. Symbolica is a strong architectural reference, but the project only needs a small expression language plus three tightly defined consumers.

Terminology correction

In this issue, canonical expression DAG means the single authoritative, algebraically normalized semantic representation shared by macro and runtime code. Surface operators such as subtraction, division, negation, and square root are syntax sugar and are not preserved as public node variants. Contract-specific validators consume this DAG directly; private compiled plans remain separate for SizeMap, SizeBound, and Growth.

References

• Symbolica expressions and exact domains: https://symbolica.io/docs/expressions.html
• Symbolica general versus restricted polynomial representations: https://symbolica.io/docs/guide/polynomials.html
• Symbolica algebraic domain traits: https://docs.rs/symbolica/latest/symbolica/domains/index.html
• SymPy exact numbers and expression construction: https://docs.sympy.org/latest/modules/core.html
• SymPy explicit numerical evaluation: https://docs.sympy.org/latest/modules/evalf.html
• SymPy assumptions limitations: https://docs.sympy.org/latest/guides/assumptions.html
• Z3 integer and real arithmetic sorts: https://microsoft.github.io/z3guide/docs/theories/Arithmetic/
• egg and equality saturation: https://docs.rs/egg/latest/egg/
• num-rational arbitrary-precision support: https://docs.rs/crate/num-rational/latest/features