Conversation
The formal/ directory does not exist on master. Not part of it -- absent entirely: 50 files, zero of them present. Both workflows that drive it, formal-yosys.yml and formal-mutation.yml, trigger only on pull_request/push to master and are themselves absent from it, so the Actions API has no record of either ever running. Not a failed run. No run. Of the 26 workflows in the tree these are the only two missing from master. This carries formal/ and those two workflows and nothing else. Every path is new to master, so no existing file is modified. The branch they came from is 1213 commits ahead and is not what should be merged. Four independent defects had to be fixed before either could produce a result, each invisible behind the one before it: * no Zig installed in the job that runs zig (0b4e93d) * `str | None` raising TypeError at import under Python 3.9, which is /usr/bin/python3 on the machine this was written on, against a CI step that pins no version (07cc025) * `import yaml` in two scan scripts with nothing installing PyYAML * the harness self-check leaking a Zig cache directory per run The load-bearing step is the vacuity check: a formal job that only runs a prover cannot tell "all properties hold" from "there are no properties", and this repository has already shipped three CI jobs that were a bare `echo`.
Contributor
PR DashboardGenerated at: 2026-08-27 13:51:48 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
The first run of this workflow -- the first ever -- died on it:
ERROR: Command syntax error: Unknown option or option in arguments.
> chformal -lower
Yosys comes from `apt-get install -y yosys`, unpinned, so the version is
whatever the runner image ships. `-lower` converts $check cells into
$assert/$assume, and a Yosys old enough to lack the option is old enough not
to emit $check at all -- the same failing log proves it, listing `$assert 1`
and `$assume 1` in the very design it then refused to lower.
So the flag is a no-op on the old Yosys and load-bearing on the new one.
Detected once and substituted into all 29 call sites, rather than choosing a
side.
Deliberately NOT removed outright. On a newer Yosys the properties would
arrive as $check cells, `sat` would find no asserts, and every proof in this
job would pass VACUOUSLY -- which is the exact failure the $check counter in
this workflow exists to catch, and not one to hand it on purpose.
This is what the gate is for. It ran once and immediately found a real
incompatibility that had been invisible for as long as the workflow had never
run.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-27 14:05:00 UTC
Summary
Seal Status
|
…hind
The corpus size scan failed on the second run of this workflow -- and correctly.
The baseline travelled with formal/ from the branch the harness was calibrated
on, and this puts formal/ on master, which is a different tree:
population branch master
coq-sources 30 30
coq-sources-lines 3328 3283 -45
gate-invocations 47 48
gate-scripts 38 47
gate-scripts-lines 6225 7051
generated-rtl 13 12 -1
generated-rtl-lines 1247 821 -426
specs 497 650
specs-lines 76092 134602
workflows 38 47
workflows-lines 3848 4169
Master is NOT behind. It carries 153 more specs and 9 more workflows than the
branch this harness was written against. The three shrinks are differences
between two trees, not deletions by this change: nothing here removes a file.
The scan's own rule is that a baseline may only assume the files of the commit
it ships in, and this one now does.
This is the gate working. Run 1 died at step 7 on `chformal -lower`; run 2 got
as far as this and found a real calibration mismatch that would otherwise have
been discovered by whoever merged it.
Note that the file's `specs-lines 76092` remark is SUPERSEDED, not answered. It
argued that value was right for the corpus and the corpus was behind, citing 55
edited-but-uncommitted .t27 files in one working tree. That is an argument about
that tree; it does not transfer to master.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-27 14:15:38 UTC
Summary
Seal Status
|
…assert
Run 3 reached the load-bearing step and failed there:
Assert the property set is non-empty -> exit 1
with `CHFORMAL_LOWER:` empty in the environment, meaning the probe added in the
previous commit had correctly found a Yosys without `-lower`.
Six sites counted cells with
| grep -oE '[0-9]+ +\$check' | awk '{print $1}' | tail -1
`$check` is the NEWER Yosys cell, and `chformal -lower` is what turns it into
`$assert`/`$assume`. The Yosys `apt-get install -y yosys` provides has neither:
no `-lower` option and no `$check` cell. It emits `$assert` directly -- which
the very first run of this workflow printed in its own failure log, listing
`$assert 1` and `$assume 1`.
So on the Yosys this job actually installs, the anti-vacuity step returns zero
every time. The step whose entire purpose is to distinguish "all properties
hold" from "there are no properties" could NEVER PASS, and was wrong in the
direction that makes the gate impossible rather than the direction that makes
it decorative. Both are fatal; only one is loud, and it stayed quiet because
the workflow had never run.
Counting both names and summing is correct on either version: a new Yosys
reports `$check` before lowering, an old one reports `$assert`, and after
lowering both report `$assert`.
This is the third defect found by running this workflow, all with one root
cause -- written against a Yosys it was never executed on.
Contributor
PR DashboardGenerated at: 2026-08-27 14:24:58 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Four runs failed at "Assert the property set is non-empty" and not one printed
how many cells it found, or whether yosys elaborated the design at all.
n=$(yosys -p "... stat" | grep -oE ... | awk ...)
yosys's output goes into the command substitution, so nothing it printed reaches
the log; and under `set -euo pipefail` a grep that matches nothing exits 1, the
assignment fails, and `set -e` kills the step BEFORE the echo on the next line --
so the one diagnostic it had was unreachable in exactly the case it was written
for.
Now captures to a file, prints the property cells found (or says none were), and
counts with awk alone. All six sites.
This does not fix the underlying emptiness. It makes the next run say what is
actually there, which four runs could not.
Contributor
PR DashboardGenerated at: 2026-08-27 14:33:52 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
… the name
The step now prints its evidence, and the first run with that change said:
$assert 6
$assert 6
check cells: 0
The properties were there all along. Six of them.
`stat` prints the cell NAME first and its count second. The pattern this
replaces -- `grep -oE '[0-9]+ +\$check'` -- wanted `6 $check`, the count BEFORE
the name, and so could never have matched on any Yosys, whatever cell that
Yosys emitted.
So the counter was wrong in TWO independent ways, wrong cell name and wrong
field order, either of which alone forced it to report zero. Fixing the cell
name one commit ago changed nothing -- and would have read as a refuted
diagnosis if the step had not also been made to show its work in the same
round.
MAX, not sum. `stat` prints the tally once per module and once for the design,
so six properties appear as two lines of 6. Summing gives 12, and inflating a
VACUITY counter is the dangerous direction: it lets a shortfall pass unseen.
`-flatten` guarantees a single module, so the maximum is the true count.
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-27 14:44:15 UTC
Summary
Seal Status
|
…ection
Run 6 got two property sets PROVED -- interrupt_controller and axi_lite_slave,
both `SAT proof finished - no model found: SUCCESS!` -- and failed on the third
with the arithmetic visible for the first time:
$assert 8
$assume 4
dma check cells: 8
::error::Expected >=12 $check cells for dma_props, found 8.
8 + 4 = 12, which is the threshold exactly.
These thresholds were written against `$check`, and on a Yosys that emits
`$check` ONE cell kind covers assertions and assumptions together. This Yosys
splits them, so counting only `$assert` undercuts every threshold in the file
by precisely the number of assumptions the design carries. The dma design is
the case where that difference crosses the line; irq and axi passed only
because they happen to have no assumptions.
Summed WITHIN a `=== module ===` section and maximised ACROSS sections. `stat`
prints the same tally once per module and once for the design, so a flat sum
would double it -- and inflating a vacuity counter is the direction that lets a
shortfall pass unseen.
This is the fourth defect in one counter: wrong cell name, wrong field side,
missing cell kind, and a shape that could not report any of them. Each was
invisible while the workflow had never run, and each was hidden behind the
one before it.
Contributor
PR DashboardGenerated at: 2026-08-27 14:51:31 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This was referenced Aug 27, 2026
This was referenced Sep 10, 2026
specs(automation): leela-agent-link -- linking a connected seller to her Leela editorial agent
#3601
Merged
Merged
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The
formal/directory does not exist on masterNot incomplete on master — absent. 50 files, none present. Both workflows
that drive it trigger only on
pull_request/pushtomasterand arethemselves absent from it, so the Actions API has no record of either ever
running:
Not a failed run. No run. Of the 26 workflows in the tree these are the
only two missing from master; the other 24 are there.
What this PR is
formal/and those two workflows, and nothing else. Every path is new tomaster, so no existing file is modified — 77 files, all additions.
The branch these come from is 1213 commits ahead of master and is not what
should be merged. This is the subsystem, not the branch.
Four defects had to be fixed first, each hidden behind the last
A gate that cannot run has as many reasons as it has reasons, and fixing the
visible one only makes the next one visible:
No Zig in the job that runs
zig. The self-check sat at step 10 of 70with nothing installing it. Fixed in
0b4e93d60, pinned to 0.16.0 —deliberately, because that is the version every published figure was
measured on, while the only other Zig in this repo's CI is 0.13.0 and the
two are not interchangeable (
usingnamespacewas removed in 0.16).str | NoneraisingTypeErrorat import under Python 3.9. The CI stepis a bare
python3 formal/…with no version pinned, and/usr/bin/python3on the machine this was written on is 3.9.6. Fixed with
from __future__ import annotations.py_compilepassed all 47 scripts while this was broken, becausestr | Noneis valid syntax in 3.9 and only fails when thedefexecutes. Importing all 47 under 3.9 found it in seconds, and found two
more.
import yamlwith nothing installing PyYAML.orphan_scan.pyandabsence_sweep.pyboth need it; neither workflow installed it, so bothsteps could only ever have raised
ModuleNotFoundError. Pinned to 6.0.2 — agate whose dependency moves under it grades a moving target.
The self-check leaked a Zig cache directory per run, ~45 MB each. Now
one root per invocation, removed in
finallyand swept at startup —because
finallydoes not run when a job is killed, and a job that compilesthe whole corpus is exactly the one a supervisor kills when disk is tight.
Why the vacuity check is the load-bearing step
A formal job that only runs a prover cannot distinguish "all properties hold"
from "there are no properties". This repository has already shipped three CI
jobs that were a bare
echo. Counting$checkcells makes the differenceobservable.
harness_selfcheck.pydoes the same for the measurement harness: it mutatesone digit inside a passing assertion and requires the harness to notice, with a
negative control that runs the same mutation through the known cache defect
and must miss it. If both notice, it reports a weak pass rather than a pass —
a gate that cannot fail is decoration.
What merging this does not do
It does not make the gates green. It makes them run, which is the
prerequisite nobody has had. Expect the first run to find things; that is the
point of it.