The property harnesses run in 8.5 minutes and CI runs none of them

[Rafael-SOWNet]

#746's standing condition "correctness coverage grows with the surface" is marked Met, with one caveat attached: the in-CI corpus is small and a set of property harnesses exists that CI never runs. This issue is about that caveat, and it is filed because measuring it showed the obstacle is not what I assumed.

The measurement

Ten self-contained harnesses, run one at a time against 2dbeedf7 on one desktop, library already built:

harness	what it asks	wall
confluence	do the rule sets converge	2s
boundcheck	does Simplify keep the value at the boundary — across a branch cut, off the real line, beside a pole	3s
canoncheck	is there a canonical form — idempotence, order independence, agreement between writings	4s
casbench	does a corpus with known answers still solve — wrong / error / timeout, not just solved	5s
rootcheck	is the root set complete, on polynomials built from known factors	9s
propcheck	does each transformation satisfy a property it must satisfy, numerically	10s
egraph	equality saturation against memory cost	70s
simpsweep	does a simplification keep the value, at sampled real points	72s
rulecheck	does a rule set do what it declares — termination, value preservation	87s
crashcheck	does anything take the process down — one child process per case, 1890 cases	245s
	total	≈8.5 min

All ten exited 0. I had assumed this was a nightly-sized job and proposed it as one; it is a test-job-sized job. crashcheck alone is half of it, and it is half of it because it spawns 1890 child processes — that cost would grow on a shared runner and much more so on Windows.

Not included, and each for its own reason: docsamples needs the wiki and website checked out; intbench needs the Rubi suite, which is downloaded rather than vendored because it carries no licence statement; libcompare pulls MathNet.Symbolics and Symbolism from NuGet and was not timed. sympyparity is a special case — SymPyParity.yml already runs a scheduled in-repo watch, so that one is partly answered already.

Why this is not just "add a workflow"

The harnesses live in a separate private workspace, not in this repository, so nothing here can run them today. That makes this a question for maintainers rather than a patch: would you want them in-repo? The code is mine to contribute if so.

There is already a shape to copy. AotSmokeTest and DotnetBenchmark are console projects under Sources/Tests/ that are in the solution, are driven by a workflow, and are not picked up by dotnet test. A Sources/Tests/Harnesses/ folder would sit alongside them. (One practical note: dotnet sln add rewrites the whole solution file — a single project added came out as several hundred changed lines, line endings and extra platform configurations included. The three entries are better inserted by hand.)

The part that needs deciding, and it is not the runtime

These harnesses generate reports; they do not assert. Wiring them to CI means choosing what fails the build, and the naive choice is wrong: a count moving is usually not a regression. boundcheck went from 41 rewritten shapes to 35 over a fortnight with 0 disagreements throughout, which reads like Simplify losing capability and was nothing of the kind — a parser fix had stopped 1/3 arriving as a division, so the fold that used to happen no longer had anything to fold.

So the gate should be the list, not the number — and this repository already has that pattern twice:

• Corpus/corpus-baseline.tsv — a committed baseline, one line per problem, regenerated rather than hand-edited, diffed per commit.
• PerformanceGate — reads a committed baseline and fails on allocation moving more than 3%, while reporting time rather than failing on it, because a shared runner's wall clock belongs to whoever else is on the host.

The same for a harness: commit the list of shapes it flags, fail when the list changes, and let the counts move freely.

Two constraints that follow from the harnesses' own semantics:

• casbench and crashcheck report a timeout as a verdict, so they must not share a runner with competing load or CI turns into a finding. That is already why the workspace's own runner script runs them alone and first.
• Wall clock must never be the assertion, for the reason PerformanceGate already documents.

Suggested first step

One workflow, the six harnesses under 10s (confluence, boundcheck, canoncheck, casbench, rootcheck, propcheck — 33s together), each gated on a committed list. That is small enough to run on every push rather than nightly, and it answers the caveat for the properties a corpus structurally cannot check: completeness of a root set, behaviour at a branch cut, idempotence of a normal form. The four slower ones can follow on a schedule once the baseline mechanism has proven itself.

Part of #746 — the "correctness coverage grows with the surface" standing condition.

[Rafael-SOWNet]

A coverage gap in crashcheck that turned up while refreshing the reports against 2dbeedf7, added here because it bears on what "adopt the harness" would actually be adopting.

crashcheck builds one instance of every concrete Entity type by reflection, and reports the types it could not build. That list grew from 22 to 24 between 6a97c071 and 2dbeedf7, and the two additions are Argmaxf and Argminf — the binder forms added by #1222.

Why they fail

The harness takes the shortest constructor of at most three parameters that are all Entity, fills it from a cycling leaf list (x, 2, 1/2, …), and then requires the instance to survive Stringize() → ToEntity(), since text is how the case reaches the child process. For Argmaxf(Expression, Var, Over) that is Argmaxf(x, 2, 1/2), which prints as argmax(x, 2 in 1/2) — and the parser refuses it, because argmax requires its second argument to be a membership whose element is a variable:

parse(argmax(x, 2 in 1/2))  =>  InvalidArgumentParseException: argmax expects its second
                                argument to say which variable ranges over which set

So the type is honestly reported as unreachable. Fine, and fixable with a written shape — argmax(x ^ 2, x in [0; 1]) parses and round-trips.

The part worth flagging

Maximumf and Minimumf are declared identically — (Entity Expression, Entity Var, Entity Over), same Binding.Of(Var).In(Over) initialiser — and they are not on the uncovered list. Not because they are covered. Because the max( grammar rule has a binary fall-through that argmax( does not:

'max(' … $args.list.Count == 2 && $args.list[1] is Inf { Element: Variable }
           ? MathS.Maximum(…)                              // the binder
           : $args.list.Aggregate((a, b) => MathS.Max(a, b))  // the binary node

so max(x, 2 in 1/2) does not throw — it parses, as the binary Maxf. The round trip succeeds and the harness records Maximumf as built, while the expression that actually reaches the child process is a different node type carrying a nonsense 2 in 1/2 as an operand.

So the true count of unreached binder nodes is four, and only two of them say so. Argmaxf and Argminf are visible precisely because their parser rule is stricter; Maximumf and Minimumf are invisible because theirs is more forgiving. A harness that reports its own gaps is the right design, and this is a hole in the gap-reporting rather than in the coverage.

What it implies for this proposal

Two things, both small:

• Written shapes for the four binder forms, which is a one-line-each addition.
• "Built" has to assert the round trip returns the same node type, not merely that it parses. That check is what would have caught Maximumf, and it costs one comparison.

It is also a concrete instance of the argument above for gating on the list rather than the count. Nothing here is a regression and no number went the wrong way — crashcheck still reports 0 crashed and 0 did-not-finish across 1890 cases. What carried the information was two names appearing in a list, which is exactly the signal a count would have hidden: the total went up, 1834 → 1890, at the same time as coverage of these four went nowhere.

[Rafael-SOWNet]

Done. CI now runs ten of these harnesses on every change to the library, from Sources/Tests/Harnesses, through .github/workflows/Harnesses.yml:

PR	harnesses	fails on
#1650	BoundCheck, RootCheck, CasBench	a disagreement at a boundary, a missing or false root, a wrong answer
#1651	PropCheck	a property that does not hold
#1652	SimpSweep, RuleCheck, CrashCheck	a changed value, a set that does not settle or breaks its declaration, a crash
#1653	CanonCheck, Confluence	a change to the findings committed beside them (HARNESS_UPDATE_BASELINE=1 records one)
#1656	DocSamples	a wiki or website sample that does not compile, throws, or prints something its page doesn't say

None of them fails on a timeout. Every report names the commit it measured and is uploaded with the run. DocSamples' first run found three wiki outputs that #1635 and a union change had made stale, and the wiki is corrected.

Three stay outside CI, each for its own reason:

• intbench needs Rubi's suite, which carries no licence statement, so it can't be vendored;
• libcompare is a comparison with other libraries, and nothing in it is a defect;
• egraph measures memory cost, which is a number rather than a verdict.

The workspace copies of the ten are retired.