Repository navigation
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 bycompose: 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) andsubstitution(a change of coordinates with its
denominator, inverse and inclusion checked). Oneconstruction
certificate, re-derived byverifyfrom its own file. Two examples:
construction_split.jsonandconstruction_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"]isoptimum,feasible,bound,
float_candidateorinfeasible. A zero objective now reports an EXACT
FEASIBLE point, not an optimum, inoptand inverify. same_obligationbindssoscertificates to theirSOSSpec;
same_programbinds afarkas_rayto 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): validnonnegcertificates failed
their own self-check. Names are now canonical, a condition named with*
is refused, and a certificate written by 0.34 still reads. nonnegignored--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
Fractioncarryinggmpy2.mpzparts crashed exact elimination
("cannot create fmpz/fmpq"); foreign exact rationals are now read exactly
(agmpy2.mpqwas 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_obligationansweredNoneforsoscertificates.- 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
numpythere. - With CBC through PuLP 4, an infeasible LP came back "Undefined" and
inconclusive; an exact Farkas ray is now sought and, checked, settles it.