This is a small correctness gate for prebuilt binaries with a default 28-second outer wall budget. Build time is separate. It is designed to catch material native CP and numerical optimization regressions during development; it is not a substitute for full conformance, solver-quality or scaling benchmarks, and does not establish CPLEX/Gurobi parity.
From the source root, run one command:
These executable paths are verified for the combined build/native-compat build. Its optimization library is build/native-compat/gecode/optimize/libgecodeoptimize.dylib on the local macOS build; paths and suffixes vary on other platforms. Build the gecode-test and optimize-fast-benchmark targets (the latter also builds the C shared library) before running the gate. Build time remains separate from its deadline.
The complete gate now requires the optimization binary to include both HiGHS and the native integer bridge (GECODE_OPTIMIZE_WITH_HIGHS=ON and GECODE_OPTIMIZE_WITH_NATIVE=ON). The reference configuration is the combined build with GECODE_ENABLE_OPTIMIZE=ON. The hybrid case additionally requires the checked 128-bit certificate implementation available on supported GCC/Clang compilers. A numerical-only standalone binary cannot pass the required native Exact case, even when a separate CP test binary is provided. The existing gecode-test executable supplies the original native CP cases; there is no need to run its entire suite. A missing binary, unavailable backend, omitted case or unmatched native test pattern fails the command. No feature case is optionally skipped.
The command emits a JSON report on stdout and exits zero only if all 35 required cases pass before the outer deadline. --output /new/path/report.json additionally saves a new report and refuses to overwrite any existing file. No existing benchmark output is modified. Optional repeated --library /path/to/library arguments record hashes of dynamically linked solver libraries. Hash those libraries when comparing shared builds: an executable hash alone does not identify its runtime dependencies.
Required cases and independent answers
| Case | Coverage and oracle |
|---|---|
| native_neighborhoods | Eight-assignment oracle proves optimum -29 after an actual radius-one incumbent improvement; original witness, global proof and shared status accounting are checked. |
| lp_sensitivity | Selected-basis coefficient and equality RHS intervals for both senses, tagged finite/infinite endpoints, objective slopes, quota rejection and historical source ownership. |
| lp_evidence | Both objective senses recover a feasible original base point and improving ray with fixed-variable and row recession checks; a contradictory bounded LP gives signed Farkas multipliers y=1,z=-1, summing to 0 >= 1. Private solve identities, checked witnesses, historical ownership and exact auxiliary-call counts are required. Status is evidence_checked; margins/slopes are not source objective values. |
| cp_distinct | Existing Int::Distinct::Dom::Dense: domain-consistent all-different tested against the original assignment predicate. |
| cp_element | Existing Int::Element::Matrix::Int::IntVar::XY: two-dimensional indexed selection with the original direct lookup oracle. |
| cp_cumulative | Existing four-task, capacity-two cumulative case with both propagation flags; original resource-usage predicate checks 500 seeded assignments. |
| cp_search | Existing single-thread DFS with binary branching and recomputation distance two; original known solution count and resumption after a failure stop are checked. |
| lp_min_offset | Two-variable LP, minimum 4. Primal (1,4) and the sum of the two lower-bound rows give matching cost 11, before offset -7. |
| lp_max_offset | Two-variable LP, maximum 15, primal (2,2) including offset 5; nonnegative row multipliers 4/3 and 1/3 give the matching upper bound. |
| bounded_integer | Atomic bulk variables and CSR row construction with a reversed column mapping; Negative and positive bounded integer domains; all 66 integer pairs are enumerated outside the solver. Minimum 13. |
| mixed_recourse | Six fixed-charge MILPs with binary opening, bounded integer production and continuous recourse. For each integer choice, optimal recourse is max(0,demand-3*n); exhaustive enumeration gives [-1,5,8,21,24,30]. Both C++ and Python compute that oracle. |
| indicators_boolean | Both indicator activation values plus AND/OR helpers; expected activation 1, quantity 7 and objective -13. Original logical metadata is independently validated. |
| semis | Semi-continuous lower 3 and semi-integer lower 2.5; active-domain optimum is 8, then row edits permit zero in both domains and objective -1. |
| multiobjective | Two ordered objectives with offsets and opposite senses, plus a sparse start. First minimize total to 14, then maximize the second objective to 1; expected (x,y)=(0,4). |
| infeasible | Integer x in [0,0.5] and x>=0.25 has no integer witness. Requires Infeasible. |
| unbounded | A free variable minimizing itself has the explicit improving ray x=-t. Requires Unbounded, rather than accepting an ambiguous status. |
| edits_io | Historical result survives bounds edits; objectives 5→7; LP and MPS reimports each retain 7; cancellation fixture yields -1. Separate precision witnesses reject x=1 and accept x=2 before and after both file round trips. |
| limit_contracts | Zero deadline, cancelled token and unsupported certified request must produce their distinct documented terminations. |
| session_reoptimization | Compatible LP row/bound/objective edits give 5,13,18,-6 while preserving the historical result and reusing one loaded model. MIP objectives 2,3,5,5 check reuse of a revalidated feasible incumbent, rejection after an invalidating bound edit, and explicit-start precedence. |
| diagnostics_groups | x in [0,10] with x>=11 must report the upper-bound/row conflict. Integer [0.25,0.75] must report lower bound, upper bound and integrality. Every retained deletion witness is checked against an independently reconstructed free-system subset; original models remain unchanged. |
| native_exact_reified | Explicit Backend::Native with Guarantee::Exact, both indicator activation values, exposed gate and a semi-integer zero alternative. C++ and Python independently enumerate 56 original assignments and obtain minimum -11, maximum 12; native proof completion must report the matching bound. |
| native_regular | Sparse signed-symbol DFA with two reachable states in a billion-state namespace. Missing zero edges reject; independent parity enumeration gives exact min/max -3/1. |
| scenario_batches | Four continuous scenarios override a variable bound, objective coefficient/offset and row sides. Both reused and cold solves must reach analytic objectives [5,9,-11,7], retain private per-scenario identities and pass original-model checks. |
| native_globals | A three-task schedule combines all-different, table, element with negative base, cumulative resource capacity, and a three-node circuit with negative labels. Independent schedule/cycle enumeration gives minimum 7 and maximum 30. Auto must select native search and preserve Exact completion. |
| c_api_ownership | The C ABI solves a MILP with continuous recourse at 5.75, then changes the integer bound and obtains 6.25. Both historical results retain copied values after destroying their model and session. |
| feasibility_repair | An impossible demand requires minimum weighted violation 1 and original objective -1; its repair must fail the original feasibility check and pass the private model check. A demand edit permits zero violation, then ordered refinement reaches objective -2. |
| native_checked_lp | Signed bounded-integer ranged-row model, both objective senses and offset, repeated checked LP deductions. Both languages enumerate the feasible box and obtain minimum 13 and maximum 26; the native result must include actual LP calls and accepted bounds. |
| solution_pool | Three integer projections with continuous recourse, ranked objectives [1,2,3], independent original witnesses and an infeasible remainder proving exhaustion. A second solve stops at two entries and must report RequestedLimit, without claiming exhaustion or original scalar optimality for later entries. |
| integer_presolve | Exact fixed substitution and signed ranged-row propagation followed by native min/max solves. Reconstructed original-slot witnesses give objectives 3 and 7, keep tombstones and original identity, and clear the reduced solve's scalar status/bounds. |
| native_frontier_bounds | Best-bound search proves min/max -17/17; depth-first search interrupted at four admitted nodes retains incumbents -15/15, valid unresolved-frontier bounds -17/17 and gap 2. Both original witnesses are checked. |
| convex_quadratic | Bounded continuous convex minimization and concave maximization using weighted affine squares; optima 3.5 and 2.5. Independent x+y=1 identity, original primal/KKT checks and outward tangent-bound gap check; explicit HiGHS QP provenance. |
| native_root_covers | Binary 3*x+3*y<=5 implies x+y<=1; min/max 15/19, original witnesses, one independently verified root cover and separate LP/cut accounting. |
| native_binary_branching | Exact binary min/max -17/17, actual complete reliability probe pairs, manual choices and the ordinary-node plus probe-attempt accounting identity; no LP calls. |
| native_complete_start | Exactly feasible but poor original starts omit their live indicator gate; native min/max must accept them, derive the gate and improve to independently enumerated objectives -4/7, with exact completed bounds. |
| lp_observations | Analytic continuous min/max LPs reach objectives 15/19; original row duals 2/3, reduced costs (0,1)/(-1,0), finite-side slacks, basis availability and independent KKT checks must agree. The exported owning basis is submitted to a second solve, which must retain the independently checked optimum. |
Native selections are exact manifest entries passed through the existing prefix selector. The runner requires exactly one output line containing that full name and one positive test marker. Empty output, multiple matches, duplicated cases or a negative marker cannot pass. Native iterations and threads are fixed at one and the seed is 1701.
HiGHS solves use one thread, seed 1701, zero requested MIP gap, a shared remaining deadline within each case, and the original-model validator. The native integer bridge uses its required deterministic seed 0, exact integer checking, and explicit native selection or automatic global-model dispatch; its reported guarantee is exact. The session and diagnostics cases report HiGHS and numerical. Native bridge provenance comes from its solve results: plain native cases use Gecode native, and the explicit hybrid uses Gecode native + checked LP with both versions. The frontier and reliability cases report Gecode native frontier. Pools retain HiGHS numerical provenance. The quadratic case uses its required seed 0, reports HiGHS QP and retains a numerical guarantee.
Assertions are not used for the panel's correctness checks, so release builds still execute every check. The runner independently checks the expected status, objective array, finite timing values, positive check count, correct backend identity, version and guarantee. Native Exact objectives require exact equality with the independent integer oracle. Other optimization results are numerical, tolerance-qualified checks. Neither route emits proof certificates.
The precision fixture intentionally uses witness validation and file round trips, rather than demanding that the numerical backend solve an ill-scaled model. Its coefficients 100000000000000.125 and 100000000000000.25 must remain distinct. Broader numerical robustness remains part of the full conformance and stress suites.
Time bound, cleanup and evidence
The outer monotonic clock begins at runner entry and covers argument processing, source and binary hashing, child startup, all cases, checking, cleanup and report writing. A default 0.75-second reserve is removed from the work budget. Each subprocess additionally has a four-second wall limit, reduced to the remaining outer work budget; --budget-seconds may reduce the outer limit but cannot exceed 28 seconds. --case-seconds may adjust the per-case limit within the outer limit. Required cases remaining at exhaustion are explicitly recorded as not_run and the run fails.
A watchdog enforces the outer deadline even during a blocked child or report write. Its last-resort exit code is 124; that failure can leave no complete JSON report. Ordinary timeout paths kill the child's process group and reap it within the cleanup reserve. Process groups are also killed after successful parent exit so that descendants cannot linger. Output uses bounded temporary files, avoiding inherited stdout/stderr pipe hangs; more than 64 KiB on either stream fails. Any stderr is retained and fails the case. Temp directories are unique and removed after the run.
The process-group runner currently supports POSIX/macOS/Linux. A Windows Job Object implementation is present for platform testing, but Windows FAST support remains unfinished and disabled. The main command returns Unsupported, records all required cases as not_run, and launches no benchmark binary. WINDOWS_RUNTIME_VERIFIED is a checked-in false constant; there is no environment or command-line bypass. This guard records missing platform evidence, not a request for permission. Deliberate session escape by a child and an unresponsive operating system are outside the containment/timing promise; this is a regression harness for trusted solver binaries.
Reports include per-case wall time, command, return code, stdout/stderr, observed status/objectives, backend/version/guarantee, correctness and failures; SHA-256 hashes of both executables and optional shared libraries; content hashes for the optimization sources, panel, fixtures, runner, containment module, the four sparse LP/certificate headers and relevant original CP test sources; platform, Python version, seeds and threads. The report's elapsed_seconds is sampled immediately before report serialization; the watchdog and successful-exit deadline check also cover serialization and output. An external wall measurement is used to verify the complete command stays below 30 seconds.
Timings collected while builds or other workloads run are correctness diagnostics only. The report defaults to timing_comparable: false; compare performance only in a separate uncontended run with matching compiler/configuration, hardware, dependencies and artifacts. This small panel provides a fast failure signal, not reliable aggregate solver speed rankings.
Harness tests
The runner tests cover absent/multiple native matches, wrong optimization statuses/objectives, incorrect native/backend guarantee attribution, missing checks, NaN/infinity, malformed JSON, stderr, nonzero exits, missing executables, excessive output, per-process and whole-run deadlines, descendant cleanup, explicit incomplete-case reporting, and preservation of an existing report. Run the numerical panel for correctness separately from the uncontended whole-command wall measurement.
Pending Windows containment and verification gates
process_containment.py uses ctypes.WinDLL with explicit argument and result types. Windows DWORD/BOOL stay 32 bits, while handles, SIZE_T and attribute identifiers follow pointer width. Tests check structure sizes and offsets against the Windows SDK declarations for STARTUPINFOEXW, process information and Job Object accounting/limits. Windows x86 and x64 CI runs are required; passing layout mocks on macOS does not verify the calling convention or runtime behavior. Microsoft STARTUPINFOEXW, extended job limits, Windows SDK attribute definitions.
Before launch, the runner publishes the process owner to its existing outer watchdog. It creates an unnamed, non-inheritable job with JOB_OBJECT_LIMIT_KILL_ON_JOB_CLOSE; neither breakaway flag is enabled. PROC_THREAD_ATTRIBUTE_JOB_LIST assigns the child to that job during CreateProcessW, and CREATE_SUSPENDED prevents execution until a successful membership check and ResumeThread returning exactly one. Creation-time assignment avoids the orphaned suspended-process interval in a create-then-assign sequence. Failure to install the attribute or verify membership aborts launch; there is no uncontained fallback. This requires Windows 10 / Server 2016 or newer. Microsoft process attributes, CreateProcessW, ResumeThread.
Only separately duplicated stdin, stdout and stderr handles appear in PROC_THREAD_ATTRIBUTE_HANDLE_LIST. Caller-owned handles retain their inheritance flags; the job, process and thread handles are never inherited. Attribute buffers and their referenced handle arrays live through process creation and attribute-list deletion. The executable and working directory must be fully qualified paths, and the command line uses CRT argument quoting with the documented UTF-16 size limit. Microsoft process attributes, DuplicateHandle, CreateProcessW.
Cleanup terminates the entire job even after a successful root exit, waits for the root within the existing reserve, and checks ActiveProcesses until descendants exit or that reserve expires. Every owned handle is closed, with the job closed last as an additional termination path. Termination, query, wait and close failures fail the case. An unsuccessfully closed job stays attached to the watchdog, and another case cannot start. The watchdog terminates the job and exits without waiting; process exit closes the final owner handle. The same outer 28-second clock, output checks and report rules apply to the implementation under test. Microsoft job accounting, TerminateJobObject, Job Objects.
Job containment covers ordinary CreateProcess descendants, including nested jobs. It is not a security sandbox: for example, Microsoft documents that processes launched through WMI Win32_Process.Create are outside this inheritance. Restricted containing jobs may reject creation; that remains an explicit failure. No PowerShell or taskkill cleanup fallback is used. Microsoft Job Objects.
The new .github/workflows/fast-windows-containment.yml workflow exercises Python x64 and x86 on Windows Server 2022. Its mandatory real-API command is:
The first command rejects non-Windows hosts, missing real fixtures, or any skipped test. Required runtime evidence includes suspended launch and membership, Unicode/quoted arguments, stdout/stderr and exit codes, termination after root success, nested jobs, denied breakaway, stdio-only inheritance, post-creation verification/resume failures, abrupt owner exit, and watchdog termination. Runner tests additionally exercise deadline, flood, missing-binary and fail-closed command behavior. Mock tests inject failures at job creation/configuration, each stdio duplicate, attribute setup, process creation, membership, resume, termination, wait, exit-code retrieval, accounting query and handle close; they verify kill/close attempts and bounded waits.
Evidence at implementation time: local macOS protocol, POSIX process-group and Windows API-mock tests pass. Windows runtime tests are unavailable locally and are explicitly skipped. The workflow is configured but has not been executed here. Windows FAST completion requires recorded successful runs of both architectures, review of that evidence, and a separate change enabling the main command. It then still requires the full required native/numerical panel on Windows with prebuilt matching binaries and an independently measured whole-command wall time below 30 seconds. Containment-only CI cannot satisfy that solver/timing gate.
Generated by
1.18.0