0.35.0

Contracts across a construction; seven defects of 0.34 fixed; the scope of
an LP typed; physical conflicts in assign. No new commands (62); one new
kind (66): construction. The schema stays 5; new optional fields:
resources and physical (assignment).

New

• ConstructionSpec, run by compose: graphs and resources under stable
  names, and steps that are contracts over them -- lift (resources carried
  from a child graph to its parent, the final packing and cover REBUILT and
  checked), catalogue (every one-vertex extension generated by the checker
  and mapped by an isomorphism or excluded by a forbidden induced subgraph;
  one omitted extension invalidates it), credit (owners partitioning the
  bases, every local state declared and covered, one cut distribution, the
  global sum in fractions), hosting (a matching per host, tied to the
  graph's edges), glue (ports consumed once, one owner per interior, no
  perforated cover taken for a closed one, a joint value only from a global
  witness), certificate (embedded, verified, tied to its obligation),
  cegis (a synthesised parameter backed by a certified resource), charts
  (an atlas: leaves recomputed, each chart's certificates tied to its
  selectors) and substitution (a change of coordinates with its
  denominator, inverse and inclusion checked). One construction
  certificate, re-derived by verify from its own file. Two examples:
  construction_split.json and construction_charts.json.
• AssignmentSpec(resources=...): no resource twice on a receiver. The
  relaxation's optimum that repeats one is named as such, not as a physical
  packing; a physical assignment is found and checked beside it.
• Typed LP scope: meta["scope"] is optimum, feasible, bound,
  float_candidate or infeasible. A zero objective now reports an EXACT
  FEASIBLE point, not an optimum, in opt and in verify.
• same_obligation binds sos certificates to their SOSSpec;
  same_program binds a farkas_ray to its program.
• Polynomials as text in data specs (certo.polynomials.parse_text): exact
  numbers, names, + - * /, ^, parentheses -- nothing else is read.

Fixed

• A region's products were named in the spec's order (g2*g10) and
  looked up in the verifier's (g10*g2): valid nonneg certificates failed
  their own self-check. Names are now canonical, a condition named with *
  is refused, and a certificate written by 0.34 still reads.
• nonneg ignored --timeout: the Bernstein tensor and the simplex of
  the multipliers now look at the clock, and a run stopped by it is TIMEOUT
  (and a verification stopped by it, inconclusive).
• A Fraction carrying gmpy2.mpz parts crashed exact elimination
  ("cannot create fmpz/fmpq"); foreign exact rationals are now read exactly
  (a gmpy2.mpq was rounded to a denominator of 10^12 before).
• A sum built with += over 1500 terms passed Python's recursion limit when
  read; the reader is now iterative.
• synth --prove-candidate --oneline (and --json) printed the search's
  line while writing the combined certificate; they now print the combined
  result, the one the file holds.
• A constant polynomial needed a box in nonneg; its sign is now read.
• same_obligation answered None for sos certificates.
• A clean install on Python 3.12+ could not import pulp: PuLP 4.1.0
  (like 4.0.1) imports numpy without declaring it. certo now declares
  numpy there.
• With CBC through PuLP 4, an infeasible LP came back "Undefined" and
  inconclusive; an exact Farkas ray is now sought and, checked, settles it.

0.34.0

CEGIS finds functions and says which counterexamples decide; branch and
bound takes your incumbent and runs twice as fast; options tested in
combination. No new commands (62) and no new kinds (65); the schema stays
5. New optional field: decisive (cegis_none).

New

• Templates in synth (certo.templates: polynomial, combination):
  the found object is a function, named in the result, optimised and proved
  unbounded with --prove-candidate.
• Decisive counterexamples: a minimal set that forces "none" (or "nothing
  better"), checked by verify -- alone sufficient, none removable.
• mixed --prove-optimal --incumbent FILE and --progress, and the same
  through certo.api.run("mixed", spec, prove_optimal=True, ...).
• DivisibilitySpec for solve: the incidence matrix built for you, Q and
  Z, and the obstruction when Q says yes and Z says no.
• CERTO_WORKSPACE_EXTRA: extra directories the MCP server may read.
• Every option in combination is now tested: synth, cover, nonneg,
  step, covering, compose.

Faster

• A branch-and-bound node on the 1048-column packing: 0.92 s to 0.45 s.

Changed

• certo report writes to the user's data directory by default.

Fixed (0.33.1, never published on its own)

• synth --prove-candidate after an optimised synthesis (minimize /
  maximize) ended with KeyError: 'implementation': the synth_optimum
  certificate keeps the candidate in the half that found it. The CLI, the
  MCP tool and the verifier of the combined synth_proved certificate now
  read the candidate from either shape (cegis.implementation_of).

0.33.0

HiGHS spoken to directly, a step between bounds checked, a packing by
table. One new command (62): step; one new kind (65): bound_step. The
schema stays 5; new optional fields: problem and maximum
(recurrence_table).

New

• HiGHS through highspy, not PuLP, for every continuous solve: the
  optimal basis feeds the exact route (one elimination on it, before any
  rounding), duals oriented by strong duality, Farkas rays sought on an IIS's
  rows, and branch and bound started from HiGHS's MIP incumbent (re-certified
  by mixed) with HiGHS's bound reported as solver_bound.
  CERTO_HIGHS_DIRECT=0 restores the PuLP route.
• certo step (StepSpec): from D <= f and substitutions x <= u,
  does D <= g follow on a box? Monotonicity, ranges and the comparison, each
  a certified sign (bound_step, solver-free); a wrong step with its point
  and the bound that does follow.
• cover --maximum by the packing recurrence up to 62 elements,
  solver-free; --sat keeps the SAT route.
• Coherent forgeries in verify --tamper: the claim changed with its
  metadata fixed to match, all caught.
• certo.existence.estimate_cliques: the size of a clique LP before it is
  built -- columns, non-zeros, dense and sparse memory.
• verify --obligation ties a standalone farkas_ray to your program.

Fixed

• A Farkas proof of a claim was labelled a refutation of the hypotheses; it is
  a proof.

0.32.0

Every engine within its budget, a search that says what is not there,
conditioned coverings, roles moved on one graph, and the best candidate.
Two new commands (61): covering and roles; three new kinds (64):
conditioned_cover, role_transport, synth_optimum. The schema stays 5;
new optional fields: profiles (affine_semigroup), cleared
(polynomial_nonneg), pending, needs, not_closed (proof).

Fixed

• Seventeen engines ignored the time budget (semigroup, number,
  shrink, parametric among them): each now runs under its timeout_ms
  and the run's deadline, stops inside its loops, and a test runs every one
  past its deadline. semigroup keeps what it decided.
• A semigroup's status read as one answer for many questions: each point
  now says member, not_member or undecided, and the scope says these are
  COUNTS, not physical objects.

New

• certo covering (CoveringSpec): a box, conditions and alternative
  obligations; the leaves, each with its reason, tile the box, boundaries
  included (conditioned_cover, solver-free). Unresolved leaves are listed; a
  point where everything fails is a counterexample.
• certo roles (RoleSpec): roles exchanged on one graph without
  changing it -- the automorphism, and each declared property before and after
  (role_transport, solver-free).
• The best candidate: SynthSpec(minimize=...) / maximize, certified by
  the candidate and the refuted search for a better one (synth_optimum).
  correctness as {name: formula} names which obligation each
  counterexample breaks.
• Prerequisite chains in compose: ProofSpec.pending(...) and
  lemma(..., needs=[...]); a theorem resting on a pending prerequisite is
  NOT CLOSED, said as the verdict.
• Semigroup profiles: the least value of a free coordinate with the point
  in S, every smaller value excluded.
• NonnegSpec(clear_denominators=True): the sign of the denominator
  proved on the box, and the numerator certified with that orientation.
• Why a question did not settle: a timeout or unknown from prove or
  check reads the theory, floors, products and the hypotheses that bring
  them, and says what to try (meta["hardness"]).
• find answers with a verdict -- found, not_available (why, and what
  instead) or not_in_certo -- each result with its confidence, what it does
  not establish, an example and the call for the CLI, MCP and the API;
  find --spec FILE says what can be done with a spec. Spec methods indexed.
• verify --obligation covers atlas and covering certificates, and a
  nonneg with cleared denominators.

0.31.0

Inputs kept as written, and a certificate tied to its obligation. No new
commands (59) and no new kinds (61); the schema stays 5. New optional fields:
cleared (ideal) and scope (cegis, cegis_none).

Fixed

• A binary variable kept its bounds only above. variable("x", 1, 1, kind="binary") came back as (0, 1), and opt certified the minimum of a
  program where x could be 0. The bounds are now intersected with {0, 1}; an
  empty range is refused.
• Hypergraph and cover labels that print alike were merged. [1, 2] and
  ["1", "2"] became one hyperedge (a matching of 2 reported as 1), and a
  JSON spec read "1" as a number. Labels stay as written, and two different
  elements with the same printed identity are refused before any verdict.
• A hypergraph with no hyperedges (a triangle-free graph) is nu = tau = 0
  with its certificate, not an error.
• The API ran a HypergraphSpec as its LP under every command, so
  api.run("cover", h, maximum=True) was refused; it is now read by the
  command, and cover takes minimum, maximum and sat in the API too.
• verify --spec with the right hash at another path no longer warns that
  the spec is gone; it says the file moved.
• synth's on_round is also called for the accepted round.

New

• ideal --clear-denominators: N / D certified as N, each D
  recorded in cleared and assumed non-zero (relative), checked by
  verify.
• verify --obligation SPEC and certo.obligation: is a certificate
  about THIS obligation -- ideal, nonneg, cover, CNF, LP, or a prove proof
  hypothesis by hypothesis -- with a canonical fingerprint. A valid
  certificate of 0 = 0 standing in for a claim is named.
• Evidence classes on every result, the card and status: proof,
  refutation, identity, sign, counterexample, witness, feasible, LP optimum,
  optimum, relaxation bound, finite check, synthesis, composition, ...
• SynthSpec.scope: the model searched, what is over-approximated, and
  whether counterexamples are realisable, said by the certificate.

0.30.0

Optima by SAT with a proof, faster exact arithmetic, and a program tied to
its certificate. No new commands (59); one new kind (61), sat_optimum;
the schema stays 5.

New

• cover --minimum --sat and cover --maximum: the optimum of a cover,
  partition or packing (a hypergraph matching) by SAT -- pysat proposes, when
  installed -- certified by the chosen parts, counted, and a DRUP proof
  refuting certo's own encoding of the bound beyond it (sat_optimum).
  --minimum takes this route by itself past 62 elements.
• exists takes a transversal HypergraphSpec: --max-parts k refuted
  is tau > k, by DRAT.
• LPSpec.to_data(): the program as a JSON spec, bounds and kinds kept;
  certificate.same_program(cert, spec) names what differs between a
  certificate's program and yours.
• VerifyReport.method; LPSpec points .var() and friends to their names;
  a DRAT refutation with no steps says unit propagation closes it.

Faster

• The exact simplex in GMP rationals (gmpy2, optional): the same
  answers, measured 3.9 times faster. FLINT solves the exact systems of
  the float-basis route and multiplies large integer matrices for matrix.
• Branch and bound keeps a node's Farkas ray only -- sparse, never
  serialising the dense matrix twice per infeasible node -- and reads its
  discrete variables without walking every column.

0.29.0

The least concentrated optimum, the best constant, both signs of an
objective, and hypergraphs. No new commands (59) or kinds (60); the schema
stays 5.

New

• opt --diffuse: among the optimal solutions, the least possible
  largest joint load of a pair of resources, certified by the dual of a
  second program that holds the optimum -- whether a concentrated support is
  this solution's or every optimal one's.
• The best constant on a refutation: a refuted bound on one variable,
  with linear hypotheses, comes back with the constant they do give and its
  variable_range certificate (best_constant).
• HypergraphSpec (matching, transversal; JSON too) under opt, mixed --prove-optimal and cover --minimum; triangle_packing and
  triangle_cover give nu(G) and tau(G).
• cover --minimum with the LP bound and the gap, in one output.

Fixed

• A minimisation's objective, both ways: opt and the card give the
  declared value and the canonical one the certificate stores, with the sense;
  a harness read -1/8 for a minimum of 1/8. The card says exact: false
  for a valid partial certificate.
• The card no longer counts an LP's row names as hypotheses used.

0.28.0

Negatives and Boolean refutations as certificates, an ideal you can steer,
and Lean reading the declaration a binding names. No new commands (59);
three new kinds (60): propositional_refutation, recurrence_table,
repair_refusal. The schema stays 5, with optional fields (eliminated,
nonzero on ideal; lean, mode on lean_binding).

New

• prove --drat: a Boolean core -- incidences and counts Sum(If(b, 1, 0)) <= k included -- encoded by certo and refuted by a DRUP proof that
  verify checks by unit propagation, with no solver in the trusted base.
• cover --minimum: the minimum number of candidates partitioning (or
  covering) a universe, proved by a recurrence over masks whose whole table
  is the certificate -- optimality and exhaustiveness, solver-free.
• A refused repair is a certificate (repair_refusal): the step and the
  reasons, re-derived by verify.
• ideal: SUPPLIED cofactors checked with no search; linear definitions
  eliminated first and the cofactors lifted back to the original equations,
  each substitution replayed by verify; nonzero denominators as declared
  obligations (relative degree, owed in status); --progress.
• bind with Lean: the elaborated type, its hash and its axioms are
  recorded; a binding without discharges asks Lean's kernel whether the
  declaration's type IS certo's export of the certificate -- PROVED and
  kernel_checked, or REFUTED. verify --elaborate asks again.

Fixed

• export --theorem NAME declared Certo.NAME: the exporters' namespace
  wrapped the named theorem. Named theorems are written outside it.
• The exact LP from the float basis reads the matrix sparsely: a 66 017 x
  218 program certified its exact optimum (218) where 0.27 stopped partial at
  its budget, never building the dense matrix.

0.27.0

What a result is, one clock for a run, and an exact LP that closes.
No new commands (59) or kinds (57); the schema stays 5, with one optional
field on every kind (card).

New

• The card. A spec declares its result's role (consumer, existence,
  refutation, finite_check), the link of the chain it belongs to, and
  what it is still PENDING on: s.role(...).link(...).pending("CP7"), on
  every spec type, or "card": {...} in a JSON spec. The certificate
  carries it (optional field card, in the digest); verify prints the
  card -- kind, degree, role and link, scope, hypotheses used and cited,
  what is NOT established here, and the provenance (producing and verifying
  versions, schema, id; interpreter and package in --json, the MCP and the
  API). All of it labelled DECLARED: nothing about it is checked.
• Aggregates that say how much is checked. status counts the degrees
  (with --verify), the declared roles, and how many certificates rest on
  something pending -- a PASS there is conditional -- and lists pending
  dependencies and cited hypotheses with what is still owed. --oneline
  adds a seventh field, pending=k, only when there is something pending.
• The regime that matters. s.regime("l_ge_6", l >= 6, integers=["l"])
  declares where the result is meant, which is not a hypothesis; prove
  reports for each regime whether the hypotheses are inhabited there or
  EMPTY (the theorem vacuous where it was meant). check --hypotheses-only --regime NAME, and --integers.
• One clock for a run. --deadline (and each MCP call) sets a run
  deadline that every solver call, the engines with clocks of their own
  (ideal, the exact LP, profile, CEGIS), sweeps and branch and bound
  read: a run stops with TIMEOUT and what it had -- a sweep with the items
  not reached named, branch and bound with its frontier certificate --
  instead of being killed. Children (geng, cbc, lake) end with certo.
  The hard stop stays as the backstop. --timeout-ms keeps its meaning.
• The MCP server under a watchdog. Each tool call has a run deadline
  (CERTO_MCP_CALL_S, 600 s); a call that does not come back is answered
  without it, and past two such calls still running the server refuses new
  work until they end (CircuitOpen).
• cliques_of: every clique of a graph as a candidate, for "no
  partition into k cliques" (examples/clique_partition.py).
• FLINT for large polynomial products (fmpq_mpoly), exact, with the
  Python loop as the fallback (CERTO_NO_FLINT=1): the parametric examples
  run in 8.2 s instead of 11.7.

Fixed

• The exact LP on a large degenerate quotient closes. A 4130-column
  program never certified in a two-minute budget; the float dual is basic,
  and its basis is now solved exactly (denominators past the ladder, 2598216
  here), the primal from the float support: 3.5 s, verified complete. The
  exact simplex solves a wide program as its primal, pivots sparsely, and its
  phase 2 keeps the deadline (it ran past budgets).
• A Farkas core with an equality failed its own self-check. An equality
  is two rows and one name; requiring a name per row made prove report
  INVALID for a correct proof.
• A check model was labelled with a CNF witness line whose {n} and
  {names} were never filled.
• Branch and bound stopped by the run's deadline before its first design
  says so, instead of blaming the residual LP.

0.26.3

Corrections from four reports on 0.26.2, two of them wrong answers.
No new commands (59); one new kind (57), cegis_none; the schema stays 5.

Correctness

• synth said "no object exists" for a spec that has one. The search
  learned behavior AND correctness at each counterexample; when the domain
  depends on the implementation (x >= k), that excluded every candidate
  the counterexample is not an input of -- k = 1 was refuted by x = 0,
  found against k = 0. It learns behavior IMPLIES correctness now. Never
  a false PROVED: the found object is always re-checked.
• prove_candidate refuted a correct candidate when universal_behavior
  mentions an implementation variable: the domain kept it free, so the
  obligation read "for every k". The candidate is substituted in the domain
  too (a user's report, with the workaround that confirmed it).
• A capacity_profile source's value and parameter_load are checked.
  Both are derived from the masses and shown to the reader; changing 108/5 to
  0 verified as complete.

Fixed

• capacity_profile finds a profile from a degenerate endpoint dual. A
  dual optimal at an end but not the profile's line crossed the other line AT
  the end, and the bisection ran to its depth limit ("nested deeper than any
  real profile"). A line equal to the profile at both ends covers the
  interval, by concavity, and prices it.
• capacity_profile keeps its time budget. limits was taken and never
  read; the search and each of its linear programs now stop at the clock --
  TIMEOUT, stopped_by: time, no certificate.
• prove_candidate takes the candidate in either shape, {name: value}
  from meta or {name: [sort, value]} from the certificate, and refuses
  an unknown or missing name by name instead of cannot unpack.
• Certificate.to_dict() returns a copy. It handed out the payload
  itself, so editing "its" dict edited the certificate.

New

• A synthesis negative carries a certificate, cegis_none: the
  constraints with the contract instantiated at each counterexample are
  unsatisfiable, and the counterexamples assign inputs only. synth results
  also print their scope -- the bounded input domain, or the implementations
  and inputs a negative is about.
• export --lean --theorem NAME: a named theorem instead of an
  anonymous example (NAME_k for several; the namespace for a semigroup),
  checked for correspondence as before and compiled in the Lean gate.