Clean up, optimisations and refactors

.github/tickets/m4/m4-p2-2-superopt.md

@@ -18,6 +18,7 @@ Its responsibilities are:
 * A map keyed by neurons and latency, scored by `HardwareCost`, holding only verified networks
 * Output: the best network per cell, its cost, the step it was verified to, and its export as Verilog and NIR when it fits the profile
 
+The command should extend the `superopt` command and part superoptimiser built for library parts with `--spec`, because a contract is already a spec with cases, and a second superoptimiser would drift from the first.
 Every seed should pass the verifier before the search starts, because a wrong seed would make every descendant compete against a wrong reference.
 A network should enter the map only after passing the verifier's held-out step, and the bounded proof should run on each new elite once, because proofs on every candidate cost too much and an unproven elite must not be reported.
 Evaluations should be charged to the shared evaluation budget in the same units as the other searches, because the synthesis arm is compared on the same budget.

.github/tickets/m4/m4-p2-4-library-superopt.md

@@ -0,0 +1,40 @@
+---
+number: 143
+title: Superoptimise kept parts against their contracts
+milestone: M4
+labels:
+  - area: search
+  - area: cli
+parent: m4-p2-superoptimisation
+---
+
+The library already holds correct parts (evolved delays and sequencers, and hand-built count parts that evolution has not found), and each has a contract to check against, but the only time a part is made smaller is the short shrink when it is first found, and nothing ever makes one faster.
+We want a `superopt` command that takes kept or hand-built parts as seeds, searches for smaller and faster networks that still meet the part's contract, and saves an improvement to the library only when it is verified and proven at least as far as the seed.
+
+Its responsibilities are:
+* Seeds, picked by option: `--part FILE`, `--only NAMES` from the library folder, or `--hand-built` for the hand-built parts, each verified before the search starts
+* The search: the shrink search's edits and admission, with a MAP-Elites map keyed by neurons and latency, scored by `HardwareCost` and then latency
+* Proof: `BoundedCheck` on each new elite once, to at least the bound the seed was proven to
+* Write-back: replacing the library's part when the new one is no worse on cost and latency and better on one, with its origin saying which part it was superoptimised from
+* A report per seed: cost and latency before and after, the bound proven, and the evaluations spent
+
+A seed that fails its contract should be refused with the failing case, because every descendant would be compared against a wrong reference.
+A part should replace a kept one only when it is proven to at least the kept part's bound, because a smaller part that is less proven is not like for like.
+Under the hardware profile, seeds and edits should stay inside the profile, and a profile part should be saved to the profile library only, because conforming can change behaviour and the two libraries hold different rule forms.
+Latency should be an objective beside cost, because a part that is just as small but answers sooner makes every composition built from it faster.
+Evaluations should be charged to the shared evaluation budget, because spec superoptimisation and the synthesis arm will be compared in the same units.
+The command should be one `Command` with a registry line and a menu item on the library parts page, because every command is run the same way from the menu and the command line.
+This command should be the one that later takes `--spec`, because a contract is already a spec with cases and a superoptimiser for specs only adds seeds and verification steps to it.
+
+Where: new `Search/PartSuperoptimiser.cs`, new `Application/SuperoptService.cs`, new `Cli/Commands/SuperoptCommand.cs`; `Search/ShrinkSearch.cs`, `Search/PartSearch.cs`, `Search/Algorithms/MapElites.cs`, `Specs/Verification/Verifier.cs`, `Specs/Verification/BoundedCheck.cs`, `Specs/Parts/HardwareCost.cs`, `Specs/Parts/LibraryPart.cs`, `Specs/Parts/HandBuiltParts.cs`, `Specs/Parts/ReferenceParts.cs`, `Specs/Parts/ModuleLibrary.cs`, `Application/PartLibraries.cs`, `Storage/PartLibraryFiles.cs`, `Cli/Commands/CommandRegistry.cs`, `Cli/Menus/MainMenu.cs`.
+
+Done when:
+- [ ] `superopt --hand-built` returns, for at least three hand-built count parts, a part with fewer neurons or a lower latency than its seed, verified and proven to the seed's bound, on at least 8 of 10 seeds
+- [ ] `superopt --only "delay 2,sequencer 2"` on `parts/` and `parts-profile/` never saves a part that is worse than the one kept
+- [ ] A seed that fails its contract is refused with the failing case
+- [ ] A saved part's origin names the part it was superoptimised from, and the `parts` command shows it
+- [ ] RESEARCH.md has a table of every seed's cost, latency and bound before and after
+- [ ] The README command table and menu list `superopt`
+- [ ] `dotnet test` green
+
+Read first: RESEARCH.md "Spec to verified circuit", "Proving contracts", README "Compile, then shrink"

.github/tickets/m4/m4-p2-5-speed-and-size.md

@@ -0,0 +1,32 @@
+---
+number: 144
+title: Keep the smallest and the fastest part for each contract
+milestone: M4
+labels:
+  - area: modules
+  - area: search
+parent: m4-p2-superoptimisation
+---
+
+The library keeps one part per contract and replaces it only with a cheaper one of the same behaviour, so a part that is larger but answers in fewer steps is thrown away, even though some compositions are limited by time and not by size.
+We want the library to keep, for each contract, every part on the front of hardware cost against latency, with composition and superoptimisation able to ask for the smallest or the fastest.
+
+Its responsibilities are:
+* The front: a new part joins when no kept part is at least as cheap and at least as fast, and kept parts it beats on both leave
+* Files: one file per part on the front, named so the smallest keeps today's file name
+* Choosing: compositions take the smallest by default, and a `--prefer small|fast` setting picks otherwise
+* Showing the front in the `parts` command
+
+The smallest part should keep today's file name, because saved libraries, exports and tests name parts by it.
+Parts on the front should be compared by the same `HardwareCost` order the shrink search uses, because two orders would disagree on which part is smaller.
+The front should be small, because a part that is a step faster and a neuron larger is rarely worth a file; parts should join only when they are faster by at least one step or smaller by at least one neuron.
+
+Where: `Specs/Parts/ModuleLibrary.cs`, `Specs/Parts/LibraryPart.cs`, `Specs/Parts/HardwareCost.cs`, `Storage/PartLibraryFiles.cs`, `Application/PartLibraries.cs`, `Application/LibraryView.cs`, `Search/CompositionSpace.cs`, `Application/Settings.cs`.
+
+Done when:
+- [ ] A library given a smaller-but-slower and a larger-but-faster part for one contract keeps both, and drops a third part beaten by one of them on both
+- [ ] A library saved before this change loads unchanged, with each part as the smallest on its front
+- [ ] `parts --only NAME` lists the front, and composition with `--prefer fast` uses the fastest part
+- [ ] `dotnet test` green
+
+Read first: RESEARCH.md "Spec to verified circuit", "A verified spiking parts library, and search beyond evolution"

.github/tickets/m4/m4-p2-6-rebuild-composites.md

@@ -0,0 +1,30 @@
+---
+number: 145
+title: Rebuild composite parts when a part they use gets smaller
+milestone: M4
+labels:
+  - area: modules
+parent: m4-p2-superoptimisation
+---
+
+A promoted part (the add loop, or a promoted composition) is saved with its recipe, but its network is the flattened one from when it was promoted, so a smaller copy of one of its children later does not make it smaller.
+We want superoptimising or replacing a part to rebuild every composite part whose recipe uses it, verify the rebuilt part on its contract, prove it to its old bound, and keep it when it is cheaper.
+
+Its responsibilities are:
+* Finding the composites whose recipes name the replaced part, nested ones included, innermost first
+* Rebuilding each from its recipe with the new child, and its glue unchanged
+* Verifying and proving the rebuilt part, keeping it only when it passes and is cheaper or faster
+* Logging each rebuild: the part, the child that changed, the cost before and after, and the result
+
+A rebuilt part should be verified again even though its children are, because a child with a different latency can break timing the glue relies on.
+A rebuild that fails should keep the old composite and say which check failed, because the old one is still correct.
+Rebuilding should be offered after the superoptimiser saves a part and on its own as `superopt --rebuild`, because a library edited by hand needs it too.
+
+Where: `Specs/Parts/PartRecipe.cs`, `Specs/Parts/Composition.cs`, `Specs/Parts/PartWiring.cs`, `Search/Modules/Promotion.cs`, `Specs/Parts/ModuleLibrary.cs`, `Specs/Verification/Verifier.cs`, `Specs/Verification/BoundedCheck.cs`, `Application/PartLibraries.cs`.
+
+Done when:
+- [ ] Replacing the register with a smaller verified register rebuilds the add loop, which passes its contract to its old bound with fewer neurons
+- [ ] A child that breaks a composite's timing leaves the old composite kept and logs the failing check
+- [ ] `dotnet test` green
+
+Read first: RESEARCH.md "Composing modules into machines", "Proving contracts"

.github/tickets/m4/m4-p2-7-saved-networks.md

@@ -0,0 +1,32 @@
+---
+number: 146
+title: Superoptimise a saved network on its task, with held-out values
+milestone: M4
+labels:
+  - area: search
+  - area: cli
+parent: m4-p2-superoptimisation
+---
+
+Runs of `evolve`, `compose` and `compile` save correct networks for tasks with no contract (Fibonacci, the natural numbers), and shrinking them is scored only on the values the task checks, so a smaller network can be right on those and wrong just past them.
+We want `superopt --network FILE --task NAME` to superoptimise a saved network on its task, admitting a network only when it passes the task's values and a set of held-out values the search never scored.
+
+Its responsibilities are:
+* Loading the network and refusing it, with the first wrong value, when it does not solve the task
+* Held-out values: for sequence and generator tasks, the values after the last one scored; for other tasks, inputs the task does not check
+* The search: the same superoptimiser as for parts, with the task's check and the held-out values as admission
+* Output: the smallest and the fastest admitted networks, saved to a run folder as the compile run's files are
+
+Held-out values should never be scored during the search, because a search that sees them overfits to them as it does to the training values.
+A task with no held-out values should be refused with a message saying so, because an unchecked shrink is what this ticket exists to stop.
+The run should report how many candidates passed training but failed held-out values, because that is the overfitting rate the spec route is meant to remove.
+
+Where: `Search/ShrinkSearch.cs`, `Application/CompileService.cs`, `Application/NetworkRunService.cs`, `Application/RunFolders.cs`, `Storage/NetworkFiles.cs`, `Specs/Tasks/SequenceTask.cs`, `Specs/Tasks/GeneratorTask.cs`, `Search/Benchmarking/TaskSuite.cs`, the superoptimiser from this epic.
+
+Done when:
+- [ ] The compiled Fibonacci network from a `compile` run shrinks to at most 10 neurons and gives the next 4 values past the ones it was scored on
+- [ ] A network that fails its task is refused with the first wrong value
+- [ ] The run reports how many candidates failed only the held-out values
+- [ ] `dotnet test` green
+
+Read first: RESEARCH.md "Spec to verified circuit", README "Compile, then shrink"

.github/tickets/m4/m4-p2-superoptimisation.md

@@ -13,12 +13,14 @@ Its responsibilities are:
 * Verification steps for a spec: training cases, held-out cases, a bounded proof, and counterexamples fed back
 * The superoptimiser: seeds, edits, a cost map, and re-verification of every elite
 * Synthesis from the same spec on the same budget, as the comparison arm
+* Superoptimising what is already solved: kept and hand-built parts against their contracts, the composite parts built from them, and saved networks against their tasks with held-out values
+* Keeping the smallest and the fastest part for each contract
 
 Correctness should be a hard constraint, not a weighted term, because a smaller network that is wrong on one held-out case is not an improvement, and weighting would trade them.
 Cost should be `HardwareCost` under the hardware profile, because results that only hold for regex rules do not transfer to integrate-and-fire chips.
 The superoptimiser should take its search through the search interface from M2.5, with evolution as the first method, because exact synthesis, windowed improvement and rewrites in M5 are further methods for the same command.
 
-Order: after the counterexample loop in M3 Part 3 and the compiled parts in M3 Part 1; verification steps; superoptimiser; synthesis comparison.
+Order: parts first, since they need only what exists today: superoptimise kept parts; keep the smallest and the fastest; rebuild composites; saved networks on their tasks. Then, after the counterexample loop in M3 Part 3 and the compiled parts in M3 Part 1: verification steps; the superoptimiser for specs; synthesis comparison.
 
 Done when: `superopt` on the add and multiply specs, seeded from compiled networks, returns networks smaller than their seeds that pass held-out cases and a bounded proof, and the synthesis arm's results on the same budget are reported next to them.