[Refactor] Separate model and reduction semantics from solver execution: repository audit and implementation plan

[isPANN]

Goal and responsibility boundaries

This package is about problem models, mathematical reductions, and solution mappings. Models and rules must not change their mathematical semantics to accommodate a particular solver's numerical range, tolerances, termination statuses, or search capabilities.

Implement this work under the following contract:

Layer	Responsible for	Not responsible for
Problem / model	Mathematical meaning of instances and solutions, feasibility, objective values, correct computation in the declared representation	HiGHS tolerances, solver statuses, search size, recovering from solver failure
ReduceTo / ReductionResult	Target construction, applicability domain, parameter relationships, mapping target witnesses that satisfy the preconditions into source witnesses	Calling a backend, repairing backend solutions, independently checking global optimality
HiGHS adapter	Encoding native ILP for the backend, execution, status interpretation, numerical decoding, and checking witnesses against the original ILP	Branching on source model names, changing constraints, independently proving global optimality
Solver orchestration	Deterministic selection of registered capabilities, executing reduction chains, using conclusions accepted by the adapter, extracting and validating source witnesses	Adding another backend precision policy, silently switching solvers after failure
CLI / MCP	Calling public APIs, transporting and presenting results	Implementing separate model validation, reductions, or solver conclusions

Optimal / Infeasible are conclusions under the selected backend's contract, not additional formal proofs. The adapter may return a successful optimal solution only when the backend reports optimality and its witness passes validation; timeouts, non-optimal termination, and invalid results must produce explicit errors. Floating-point backend arithmetic alone does not justify adding a certificate system or downgrading all normal results throughout the package.

Incorrect coefficients, overflow, discarded nonzero terms, and incorrect witness mappings remain this library's responsibility. Floating-point models use their declared ordinary floating-point arithmetic; this does not require converting every computation to exact arithmetic. Backend tolerances must not define model semantics.

Audit scope and evidence

Audit baseline: refactor/native-ilp-adapter, commit 59775947c40be6c0a3b842b3935f96fb879f0d95. PR #1147 already introduces the native ILP adapter on this branch. Check whether this work has reached the main branch before implementation; do not create another adapter.

The repository-wide static scan covered:

• src/models/: 208 Rust files across graph/formula/set/algebraic/misc and shared model code.
• src/rules/: 286 Rust files, including direct reductions, casts, shared extractors, parameter metadata, the reduction graph, and geometric mappings.
• 201 files under src/unit_tests/models/, 278 under src/unit_tests/rules/, plus solver and integration tests.
• 21 files under src/solvers/, 11 under src/topology/, the registry, generated macros, CLI/MCP, example-db, design and paper documentation, skills, and review scripts.
• The current workspace also contains untracked .agents/skills/, verifier/, and some skills. Their relevant policies were inspected, but these files are not part of the baseline commit. Do not include these directories wholesale in implementation commits.

Method: scan solver calls, floating-point tolerances/conversions, search dimensions, constructor domain restrictions, shared validation APIs, and their callers; then read the relevant production paths in full. Distinguish production methods from example-db builders and tests. This is a repository-wide responsibility-boundary audit, not a claim to have reproved every reduction theorem or run the entire test suite.

Checks actually performed:

1. A temporary Rust program outside the repository, depending directly on the current source, confirmed:
   • For ILP<bool,f64>, 5e-10*x <= 0 evaluates to Ok(true) at x=1.
   • For a one-set MaximumSetPacking<i64> -> ILP<bool> instance, target assignment [2] evaluates as infeasible, but extraction returns Ok([false]).
   • The same instance has universe_size=1, but the constructed target has 0 constraints.
   • For CVP with B=[[1]] and both the integer target and witness equal to 2^53, zero-distance evaluation fails with InexactFloatConversion.
   • The same CVP instance serializes integer JSON through the existing dynamic serde API, contrary to the documented universal JSON range restriction.
2. cargo test --lib generic_decision_ilp_respects_maximization_bounds -- --nocapture passed. This test explicitly requires UnresolvedDecision when a triangle has no independent set of size 2, confirming the current behavior.
3. Enumerating all 16 assignments in the existing QUBO scaling test gave objective values in [-3.3e-8, 6e-9]. Their spread, 3.9e-8, is smaller than the test's absolute tolerance of 1e-7; this branch cannot distinguish the best assignment from the worst.

A. Models contain numerical transport and backend acceptance policies

A1. Floating-point ILP tolerances expand the feasible set — high priority

Locations: ILP model, adapter decoding and validation.

The f64 implementation of ILPCoefficient::satisfies() relaxes comparisons by 1e-9 * max(|lhs|, |rhs|, 1). This affects Problem::evaluate(), brute force, direct extraction, and any future backend, not just the HiGHS interface. from_integer() also ties floating-point model evaluation to the global exact-float conversion gate.

Cause: Model evaluation, numerical encoding, and backend acceptance share the model's comparison/conversion methods.

Changes:

• Keep the existing ILPCoefficient, LinearConstraint::is_satisfied(), ILP::is_feasible(), and Problem::evaluate() path. Define one consistent model arithmetic/comparison contract there. Do not add evaluate_for_highs, lenient, strict, or caller-dependent switches.
• Remove backend-style tolerance relaxation from model comparisons. Evaluate and compare f64 expressions using ordinary finite floating-point arithmetic; retain integer semantics for integer expressions. Converting integer variable values into a floating-point domain follows that domain's declared ordinary rounding semantics, not the backend's input-range policy.
• Handle returned-value integrality and range at the adapter's decoding boundary, then call the same evaluation/witness API on the original ILP. Report InvalidSolution when that model rejects the witness; do not alter constraints or add a permissive model branch.
• Some floating-point equality instances may consequently report an invalid returned solution. Expose that limitation through an explicit error rather than expanding the model's feasible set to pass tests.

Acceptance: A small constraint-violating assignment is rejected by direct evaluation, public witness validation, and extraction. Adapter decoding policies are tested in the adapter module. All four native integer/floating-point ILP combinations continue to use one execution entry point.

A2. ExpectedRetrievalCost computes the same mathematical quantity through two conversion paths

Locations: model expected_cost, rule latency_distance and coefficient construction.

The model converts usize latency to i64, then through i64_to_exact_f64; the rule duplicates the latency formula and casts directly with as f64. The same quantity therefore has conflicting representation policies.

Changes: Make the existing latency calculation a pure mathematical method owned by the model and reused by both callers. Convert under the floating-point model's single arithmetic policy. Delete the duplicated formula and backend-style precision gate in the model. Retain finite-probability checks, the input representation convention for probability sums, and non-finite arithmetic checks; these are not HiGHS tolerances.

Acceptance: Explicit assignments on small instances produce corresponding objectives in the source model and constructed target. Do not create a numerical conversion helper for each rule.

B. CVP's integer semantics and existing exact algorithm are restricted by an f64 interface

Locations: CVP model, customized CVP solver, SubsetSum→CVP, CVP→QUBO. Coordinate with #1146.

Findings and causes:

• ClosestVectorTarget::to_f64() serves both model evaluation and the solver. Integer bases, targets, and witnesses pass through a floating-point gate first.
• The solver already uses BigRational, but integer basis entries must pass an f64 check before rational conversion, and integer targets detour through f64. Removing one check alone leaves equivalent restrictions elsewhere.
• Model evaluation uses floating-point accumulation and sqrt(). The SubsetSum rule stores and compares against sqrt(n). Rank checks and the rule's exact elimination also use different intermediate representations.

Plan:

1. Replace the f64-centric numerical method on the existing ClosestVectorTarget with the mathematical coordinate conversion the model needs. Integers enter integer/rational arithmetic directly; finite f64 coordinates enter the existing rational representation according to their stored values. Remove integer→float→rational round trips.
2. Use squared distance as the common CVP objective. Provide one model-owned squared_distance() implementation and use it from Problem::evaluate(). Represent squared distance with the existing BigRational dependency and update the Min value type; enable serialization support on that dependency as needed, without adding an arithmetic framework. Squared distance preserves minimizers, but the returned objective API and documentation must explicitly change.
3. Use the same coordinate semantics in existing sphere enumeration. Remove f64 gates on bases, targets, and candidate coefficients. After removing those gates, retain necessary checked arithmetic for the algorithm's actual i64 candidate updates; a floating-point range gate must not substitute for integer arithmetic checks.
4. Use the integer squared threshold n in SubsetSum→CVP. Remove sqrt(n) and threshold-protection explanations motivated by floating-point precision. Reuse the model's squared-distance API rather than privately recomputing another distance in the rule.
5. Retain CVP→QUBO's mathematical finite box and quadratic expansion. If constructed coefficients cannot fit the target's i64 representation, return a reduction error. Fix rank/independent-row selection in the model's existing shared computation path; do not reorder rows in one rule merely to bypass a model validator defect. Mathematically meaningful triangular structure may remain.
6. Update registration, DynProblem evaluation/serialization, examples, the paper, and typed/dynamic callers. Do not retain old distance evaluation as a hidden compatibility branch.

Acceptance: Ordinary integer and floating-point targets use the same mathematical interface. Zero/nonzero distances, SubsetSum YES/NO thresholds, and CVP→QUBO mappings are correct. Retain the existing large-integer zero-distance failure as one regression for this shared path, without spreading it across other models.

C. Shared witness validation evaluates configurations without checking feasibility — high priority

Locations: validate_target_solution, DynProblem, set-packing extractor, local SteinerTree check.

The scan found 267 textual matches for validate_target_solution. The shared function only returns Ok(target.evaluate(solution)?), so it does not reject Ok(Or(false)), Ok(Min(None)), Ok(Max(None)), or infeasible Extremum values. Some rules add .value.is_none() checks locally; others do not.

Cause: The shared API does not distinguish an evaluable configuration from a feasible witness, leaving callers to compensate locally.

Shared API plan:

// Add a default mathematical method to the existing Problem trait.
// Apply the witness-value bound at method level.
fn evaluate_witness(
    &self,
    solution: &Self::Solution,
) -> Result<Option<Self::Value>, EvaluationError>
where
    Self::Value: SolutionAggregate;

• Reuse existing SolutionAggregate::contributes_to_solution(&value, &value) semantics and call evaluate() once. Some(value) means a feasible witness, None means an evaluable but infeasible configuration, and Err means a structural/arithmetic error. This does not check global optimality.
• Delegate existing DynProblem::evaluate_witness_dyn() to this typed method, retaining its formatting responsibility.
• Make validate_target_solution() call the same method, translate None into ExtractionError, and continue returning the evaluated value for rules that need it. Keep this helper's reduction-error translation responsibility; do not add another validator.
• Update necessary trait bounds, macros, VariantReductionResult, and composed extraction callers. Delete local feasibility checks superseded by the shared check. Rule-specific one-hot, path, pairing, and similar decoding preconditions still need their existing helpers.
• Direct typed extraction, ReductionChain, dynamic extraction, and CLI/MCP must use the same check. A CLI-only patch is insufficient.

Acceptance: The set-packing [2] example fails extraction through every entry point. Feasible non-optimal witnesses remain extractable where the mapping permits them. Structural errors, infeasibility, and arithmetic errors remain distinguishable. Cover Or/Min/Max/Extremum in shared validation tests instead of duplicating tests across all rules.

D. Solver orchestration applies inconsistent policies to the same backend conclusion — high priority

Locations: CompiledIlpPipeline, resolver, typed ILPSolver, CLI bundle. Coordinate with the witness-validation portion of #1141.

Findings:

• After the adapter accepts a target optimum, the pipeline still returns UnresolvedDecision when the mathematical threshold is not satisfied.
• Successful ILP/customized paths in the resolver call evaluate_dyn(), potentially wrapping an infeasible evaluation as Optimal; the CLI bundle already calls evaluate_witness_dyn().
• Typed ILPSolver::solve() only downcasts the pipeline result into a source solution, without common final source-witness validation.
• The CLI bundle does not reuse the fixed pipeline's aggregate threshold interpretation when converting a successful target solve into a source conclusion.

Changes:

1. Keep HighsAdapter::solve(&ILP<V,C>) as the only backend execution entry for the four native ILP combinations. Preserve deterministic registration and native terminal paths. Encoding/returned-value range restrictions belong in the adapter.
2. Interpret Optimal / Infeasible / Unbounded / TimeLimit / GapLimit / backend failure explicitly in the adapter. Inspect the backend status behind its existing zero-objective re-solve for status disambiguation; retain this adaptation only where the backend actually leaves ambiguity. Models/rules must not trigger retries based on numerical magnitude, and general failures must not become infeasibility.
3. After the adapter accepts an optimum, interpret decision thresholds through existing DynAggregateReductionResult::extract_value_from_solution_dyn() or its typed aggregate equivalent. A missed threshold produces source NO/Infeasible. Delete UnresolvedDecision, its dedicated handling, and tests permitting that behavior.
4. Share one implementation of “completed target solve→aggregate interpretation→witness extraction→source-witness validation” in src/solvers/. Reuse existing executed reduction steps and aggregate callbacks for both fixed pipelines and explicit bundles. Do not duplicate threshold branches in the CLI or dispatch mathematical semantics by problem name.
5. Dynamic success paths use existing evaluate_witness_dyn(); typed success paths use C's Problem::evaluate_witness(). Invalid witnesses produce errors, not repaired solutions or source infeasibility.
6. Keep SolveOutcome's Optimal / Infeasible under the existing backend contract, with typed errors for operational failures. Update error enums, exhaustive matches, CLI/MCP documentation, and downstream integration tests. Do not add compatibility wrappers for old errors.

Acceptance: For a triangle, independent-set threshold 1 yields YES and threshold 2 yields NO. Typed/default/explicit ILP/bundle paths agree. Injected invalid returned witnesses fail through every entry point. Timeouts and backend failures never become NO. Test errors in shared orchestration/adapter code, without manufacturing HiGHS precision failures for every source model.

E. A global numerical gate conflates three different responsibilities

Main callers:

Path	Actual responsibility	Change belongs in
solvers/ilp/adapter.rs	HiGHS input encoding and returned-value decoding	Adapter transport contract
models/algebraic/ilp.rs, models/misc/expected_retrieval_cost.rs	Floating-point model evaluation	Model arithmetic policy in A
models/algebraic/closest_vector_problem.rs, solvers/customized/closest_vector_problem.rs, rules/subsetsum_closestvectorproblem.rs	CVP coordinates and distances	Common mathematical interface in B
rules/ilp_i64_ilp_f64.rs, qubo_casts.rs, spinglass_casts.rs, maximumsetpacking_casts.rs, closestvectorproblem_casts.rs	Explicit numerical variant conversion	Mathematical contract of the conversion
topology/kings_subgraph.rs, triangular_subgraph.rs, unit_disk_graph.rs; rules/maximumindependentset_casts.rs	Discrete-to-floating-point geometry	Representation contract preserving actual adjacency
rules/unitdiskmapping/weighted.rs	Mathematical gadget weight construction	Gadget and target numerical-domain contracts

Finding: types.rs incorrectly describes 2^53-1 as the largest integer exactly representable by f64. The gate also rejects some integers that are exactly representable. Conversely, a lossless scalar conversion does not establish that subsequent floating-point accumulation or backend solving is free of rounding.

Changes:

• Restrict existing i64_to_exact_f64() to callers that actually need lossless scalar conversion. Implement actual scalar representability and correct error messages/constant usage. Reuse this helper instead of scattering casts and reverse-conversion branches. Check the boundary once; do not turn this into a precision audit for every rule.
• Backend input acceptance is defined by the adapter's encoding contract. It must not restrict integer model construction, integer rules, or evaluation that does not use that backend.
• Remove solver-path dependencies on explicit integer→floating-point variant edges used only for backend execution; the native ILP pipeline already avoids that step. Retain conversions with independent mathematical uses as ordinary explicit rules, documenting their representation domain and formal coefficient/coordinate embedding without promising error-free machine evaluation or HiGHS optimality.
• Do not build whole-instance precision proofs, coefficient-sum safety thresholds, or optimizer revalidation to preserve cast edges. transform = exact describes parameter relationships, not exact numerical solving.
• A geometric mapping that changes adjacency is a reduction error. Preserve existing adjacency checks and mathematical gadget weight bounds. Do not remove these as solver-precision policy.
• Correct docs/src/design.md's claim that CLI/MCP universally reject large integer JSON. No corresponding public transport gate was found, and dynamic serde output was verified. Describe the actual public codecs; do not impose floating-point limits on every Rust model for a particular consumer.

Acceptance: Lossless conversion has one implementation and test location. Integer models/rules operate within their own declared domains independently of HiGHS support. Geometric edges preserve adjacency. The paper distinguishes formal embeddings from machine computation.

F. Search-space representation still constrains models

Locations: IntegerKnapsack, OpenShopScheduling, BruteForceProblem / CartesianIndices, registration macros. Coordinate with #1143.

Findings and causes:

• IntegerKnapsack's evaluate() calls BruteForceProblem::dimensions() to check multiplicity; its constructor also requires capacity/size+1 to fit usize. Mathematical evaluation depends on the searcher's domain-length representation.
• OpenShopScheduling's constructor requires the enumeration horizon plus one to be representable. Other models have unchecked products/casts in derived dimensions, such as capacity as usize + 1 in flow dimensions.
• Shared CartesianIndices first requires the product of all coordinate cardinalities to fit usize, although one assignment may be small.

Changes:

1. Evaluate IntegerKnapsack directly from mathematical multiplicity, capacity, and objective arithmetic, without calling a solver trait. If an upper bound is shared, let the model own the mathematical bound and the solver read it.
2. Distinguish bounds required by actual model storage/witness formats from cardinalities needed only for enumeration. Move only the latter out of constructors. Do not mechanically remove real representation constraints, such as PreemptiveScheduling's dense time witness format.
3. Replace the existing BruteForceProblem API directly with fallible coordinate-count / coordinate-cardinality methods. Update registration macros, brute_force_dimensions, CLI inspect, test support, and every implementation together. Use Separate lazy search cardinality from machine-sized storage requirements #1143's single migration, without safe_dimensions or model-specific exceptions.
4. Terminate CartesianIndices by mixed-radix exhaustion instead of requiring the total search count to fit usize. Actual coordinate-count, mask, or table representation failures still produce typed errors in their owning layer. Do not add computational-difficulty thresholds.
5. highlyconnecteddeletion_ilp.rs protects 1u64 << n only with a debug assertion. This is a mask representation limit in the construction. Return an explicit ReductionError at that construction boundary; do not narrow HighlyConnectedDeletion's mathematical domain or redirect to another rule.

Acceptance: Direct model construction/evaluation does not call enumeration dimensions. Small-instance solving remains consistent. A short prefix of a large Cartesian product can be iterated; unrepresentable coordinates/tables return errors instead of panicking. Test actual interface boundaries without exhausting huge search spaces.

Scope: This API migration touches many model files and clearly exceeds the 20-file PR threshold. Before implementation, provide the exact change list and confirm scope. Do not evade the migration by introducing hidden compatibility branches.

G. Mathematical definitions and parameter metadata need separate fixes

These are not adapter problems. Removing backend policy does not justify deleting their guards.

G1. Incorrect parameter declaration in MaximumSetPacking→ILP

rule:43 declares exact num_constraints = universe_size, but construction at line 68 keeps only constraints for elements appearing in multiple sets. A single set {0} gives 1 != 0.

Changes: Use the existing upper_bound relationship for the whole parameter block (num_vars = num_sets is also a valid upper bound). Preserve construction's omission of unnecessary constraints. Do not add redundant constraints to satisfy metadata or invent a source-model parameter solely for this rule. Update the corresponding paper relationship.

Acceptance: Compare actual Problem::parameters() with the declaration through existing ParameterTransform. One single-set instance and one instance with shared elements are sufficient.

G2. Mathematical domain restrictions must not be removed as backend restrictions

• maxcut_minimummatrixcover.rs requires nonnegative weights because its target is documented as a nonnegative matrix. However, MinimumMatrixCover::new() only checks matrix shape; construction/serde and documentation need alignment. Do not simply remove the rule's negative-weight check and claim support for the full MaxCut domain.
• decisionminimumvertexcover_hamiltoniancircuit.rs registers an i64-weight source but requires unit weights at runtime. Express this premise with the existing One mathematical variant, complete its Decision metadata, and update registration/callers for that exact endpoint. Do not choose edges by inspecting weights in the solver.
• SteinerTreeInGraphs documents a subtree, but its predicate only checks terminal connectivity, allowing cycles and unrelated selected edges; with 0/1 terminals, it accepts any edge selection. SteinerTree already has different acyclicity/whole-selection connectivity checks. The former's ILP rule accepts only positive weights and rejects empty terminals. The fact that a positive-weight optimum can be a tree does not define all model witnesses as trees.

Plan and order:

1. Establish the definition/behavior discrepancies using small cyclic/disconnected witnesses. Consult the existing paper definitions and settle both Steiner models' domains and 0/1-terminal conventions before changing code. The adapter must not decide mathematical definitions.
2. Reuse existing tree predicates where the mathematical semantics coincide, and align all public construction/serde/evaluation paths. If the two names describe the same problem, explicitly propose the API scope of merging them before implementation; do not retain duplicate implementations through hidden conversions or aliases.
3. Under the agreed semantics, reuse existing vertex-selection, connectivity-flow, and tree-edge-count construction in steinertree_ilp.rs to support signed weights. Do not rely on positive objectives to make an incorrect feasible set happen to yield a correct optimum. Do not force genuinely different problems into an unsuitable shared construction.
4. Enforce MinimumMatrixCover's nonnegative-matrix definition through its existing common construction path. Keep this MaxCut mapping's mathematical applicability domain explicit. Full signed MaxCut continues to use its existing suitable rules, without rerouting inside this edge.

Coordinate with the remaining mathematical-domain work in #1092. Its old i32/CVP representation is not evidence for the current implementation. G2's mathematical-definition and API-scope decisions are explicit prerequisites for that work, without blocking independent A–F fixes.

H. Tests and examples need clearer responsibilities

Findings:

• The small-scale branch in the QUBO scaling test cannot discriminate between solutions.
• The adapter precision comparison codifies the model discrepancy of integer rejection versus floating-point tolerance acceptance.
• assert_bf_vs_ilp() is a solver integration check, not sufficient evidence by itself for every mathematical rule.
• Direct solve calls located in rule files belong to example-db builders or test helpers. No direct HiGHS invocation was found inside reduce_to() or core extractors. 94 rule files already use shared rule_example_via_*ilp helpers.
• The untracked local verifier/ uses default pred solve for source and target validation. That provides end-to-end integration evidence; backend timeouts/failures do not automatically refute model/rule theorems.

Changes:

1. Model tests cover definitions, instance/configuration domains, and direct evaluation. Rule tests cover construction, witness mappings, and parameter relationships, using manual witnesses or small exhaustive enumeration. Enumeration is a legitimate test tool without making models depend on solvers.
2. Keep a small representative set of HiGHS round-trip integration tests. Attribute failures to construction, solving, extraction, or source validation. Do not change mathematical rules to accommodate the backend.
3. Delete the ineffective tiny-scale QUBO branch and retain the ordinary-scale reference comparison. Replace the adapter's 2^52 model-tolerance comparison with ordinary small-constraint checks. Test decoding/range boundaries centrally in the adapter/conversion helper once.
4. Retain necessary Knapsack/flow regressions preserving large integer coefficients: these check mathematical construction and do not call HiGHS. Do not turn them into templates for every rule.
5. Do not relocate all canonical example files. Keep example construction isolated under example-db. Where touched, replace duplicated solving boilerplate with existing example-db builder APIs; do not alter production reduction construction to make an example solvable.
6. If the local verifier is included, retain its existing recording/replay and explicit failure reporting without creating another verification framework. Document the different evidentiary scope of mathematical oracles and default-backend integration. Remove claims that passing the default solver proves model correctness.

I. Documentation and skills perpetuate the coupling

Locations:

• verify-reduction type gate: prohibits Max→Min and may STOP for different inner Rust types in Min.
• add-rule: similar type gates, mandatory exact helpers for every i64→f64 conversion, and blanket boundary-test requirements.
• review-quality: mechanical thresholds such as at least five vertices and assertion counts.
• review-structural: fixed test-function counts and a numerical checklist without responsibility boundaries.
• Related guidance in add-model, fix-rule-issue, and .claude/CLAUDE.md's numerical/testing policies.
• design.md: global conversion policy, JSON range claims, UnresolvedDecision, and special QUBO tolerance guidance.
• paper variant-conversion section: mixes mathematical embeddings, Rust helpers, and machine-evaluation guarantees.

Existing counterexamples and stale content: minimumvertexcover_maximumindependentset.rs already implements a Max→Min witness mapping, contradicting the skill's mechanical optimization-direction gate. ReductionResult does not require identical Value types. The skill also describes MinimumHittingSet as Min<usize>, whereas current src/models/set/minimum_hitting_set.rs:135 uses Min<i64>. Do not extend numerical type restrictions based on that stale example.

Changes:

1. Make .claude/CLAUDE.md and docs/src/design.md the canonical responsibility/arithmetic contract. Skills reference and apply it instead of duplicating a separate numerical policy.
2. Check actual associated types, mathematical objective relationships, and whether the extractor is implementable in Rust. Different optimization directions can be handled by objective relationships/complement mappings. Different Rust numeric types do not automatically invalidate a witness reduction. Check aggregate mappings against their actual value-conversion contracts.
3. Choose boundary tests from concrete implementation risks. Remove fixed vertex, assertion, and test-function counts as correctness gates. Retain construction, mathematical counterexample, mapping, and necessary integration checks. No corresponding precision/assertion-count gate was found in scripts/pipeline_checks.py; the findings are primarily in skills. Check the actual review entry points during implementation without adding a counting framework.
4. Remove guidance requiring each rule to handle solver precision. State failure attribution and adapter responsibilities explicitly. Ordinary input validation, representation errors, and finite floating-point values remain legitimate concerns.
5. Update affected API/CLI/getting-started documentation, ILP/CVP/conversion paper sections, and examples. The paper describes mathematical definitions and guarantees; implementation documentation explains Rust helpers. Do not present transform=exact as proof of backend accuracy.
6. .agents/skills is currently an untracked copy differing from .claude/skills. Maintain one canonical source, configure local entry points to reference it directly, and remove independent policies from superseded copies. Do not commit the whole untracked directory or create a synchronization framework.

Implementation order, shared APIs, and delivery boundaries

Phase	Work	Call chain to update together	Completion condition
1	Responsibility contract and skill gates (I)	CLAUDE, design, add/review/verify skills	Guidance matches existing witness/aggregate APIs
2	Shared witness validation (C)	Problem→DynProblem→extractor/chain→typed/dynamic solve→CLI/MCP	No entry point bypasses invalid-witness checks
3	ILP model, adapter, and solver conclusions (A, D, ILP portion of E)	ILPCoefficient→HighsAdapter→CompiledIlpPipeline→resolver/bundle	Consistent normal YES/NO; backend restrictions stay out of models/rules
4	CVP and remaining conversions (B, E)	CVP model→customized solver→SubsetSum/CVP rules→serialization/paper	One implementation of each mathematical quantity; no f64 detours
5	Separate enumeration capability from models (F, with #1143)	BruteForceProblem→all implementations→macros→registry→inspect/test support	One fallible API without compatibility bypasses
6	Mathematical domains and parameters (G)	Relevant models, rules, registration, paper	Correct parameter formulas; domains settled before implementation
Alongside every phase	Tests and documentation (H, I)	Existing tests/docs for changed behavior	No accumulated stale tests/interfaces; each phase independently reviewable

Implementation constraints:

• Consolidate responsibilities through existing APIs. Do not introduce a solver framework, generic adapter layer, runtime difficulty estimator, certificate system, or precision-audit platform.
• Typed and dynamic mathematical APIs share one implementation. Keep necessary type erasure at the existing registry boundary. No if model_name == ..., strict/lenient, fallback, or second extractor to bypass the contract.
• Replace old APIs, update every caller, and delete superseded error branches, wrappers, and duplicate checks. No version suffixes or compatibility paths.
• Retain correct mathematical bounds, including distance bounds and big-M derivations. Remove nonmathematical restrictions or misplaced rationales such as making HiGHS solve more easily. Retain actual arithmetic checks required for signed constructions.
• Do not delete geometric adjacency validation, ordinary probability-input tolerances, or explicit model representation constraints merely because their descriptions mention precision or range.
• Coordinate Separate witness feasibility and source solve conclusions at shared boundaries #1141's shared witness validation, Keep CVP solving and objective evaluation in exact rational arithmetic #1146's CVP work, and Separate lazy search cardinality from machine-sized storage requirements #1143's enumeration migration under this contract. Do not downgrade results throughout the library to independently prove backend optimality. Editing this issue does not automatically edit those other issues.
• Each implementation PR contains only its task's changes. Confirm the exact scope before exceeding 20 changed files or 1,000 added lines. This issue does not authorize committing the local stash, untracked verifier/skills, generated data, or temporary probes wholesale.

Overall acceptance

• Problem::evaluate() and reduce_to() do not consult backend tolerances, solver statuses, or solver search restrictions.
• Problem::evaluate_witness() is the shared typed/dynamic feasibility implementation, correctly used by all public extraction/solving entry points.
• HiGHS encoding, returned-value decoding, status interpretation, and original-ILP validation stay at the adapter/orchestration boundary.
• Every native ILP terminal uses the same adapter; integer pipelines do not depend on float-cast edges.
• Accepted backend optima produce normal YES/NO through mathematical aggregate mappings; timeouts, invalid returned witnesses, and general backend errors never become NO.
• CVP objectives, its solver, SubsetSum thresholds, and QUBO mappings follow one mathematical definition, with all public outputs updated.
• Pure model construction/evaluation does not require a representable enumeration space; search representation failures produce explicit errors in the search implementation.
• Set-packing parameter declarations match construction; mathematical-domain issues and backend limitations are tracked and fixed separately.
• Tests do not mask behavior by expanding tolerances or accepting UnresolvedDecision; shared numerical boundaries are not retested in every rule.
• Documentation matches actual APIs; skills permit valid witness reductions with different objective directions or numerical types.

Validation: run each phase's existing focused tests first, then the repository's actual make check and make mcp-test commands. Run make paper for phases affecting example-db/the paper. HiGHS is currently a regular dependency; do not use the obsolete --features ilp-highs command. Validate new executable behavior under repository coverage requirements; do not manufacture mirror tests for documentation/skill edits. Record actual build/test failures and never report unexecuted checks as passing. Generated paper data, temporary probes, and audit output are not commit artifacts.