LiveHD TODO

Single hub for all pending work. One bullet per open task below, grouped by topic (Pyrope, Verilog, LiveHD — no open Verilog tasks right now) then by Group N. Each badge links to that task's own page under todo/<topic>/<id>.html.

Dependencies. Items in the same Group can be done in parallel; all letters in Group N must complete before Group N+1 starts. Group letters are shared across the three topics, so cross-topic dependencies stay visible.

Lifecycle. A task page is deleted the moment its work lands — this hub is strictly current work. Conceptual "why/what" lives in the LiveHD & Pyrope docs; agent build/process rules live in AGENTS.md.

Recommended next — 19 subtasks

Goals (set 2026-07-26). G1 — fast synthesis iteration: ABC attribute annotations leveraging incremental synthesis + LEC, where LEC is always Verilog-vs-Verilog or Pyrope-vs-Pyrope, never source-vs-netlist. G2 — bring Pyrope up clean: translate large Verilog designs to Pyrope, then iterate module-by-module with LEC and cleanup. G3 — incremental assert/assume moving toward SVA (temporal) semantics, where the novelty is very fast assert/assume via incremental reuse and cvc5 feedback. G2 and G3 outrank G1.

What this list is. Every item below is an already-diagnosed gap — it lives on a task page, in a fixme-tagged target, or in a landed-work record. Nothing here is new design; each item names the page that owns it so the work lands there and this list stays a pointer. Ordering is dependency-first inside each tier.

Tier A — blockers shared by G2 and G3 (do these first)

• R1 — assert/assume under an if silently dropped the guard. LANDED 2026-07-26 lower_cassert connected only the cond pin to the __fproperty Sub, so a property inside an if became unconditional — strictly stronger than what the user wrote, and wrong in both directions: if a<4 { assert(a<10) } refuted with a=10 (a value the guard excludes), and a guarded assume over-constrained the environment into a false PROVEN. Both measured against the pre-fix binary. implies was the only correct spelling, which is why no checked-in fixture (and nothing in ../lhdsuite) carried a guarded design-body property — the bug had no corpus.
  
  Shipped: the obligation is now guard implies cond (SystemVerilog's procedural-assertion semantics). lower_if's existing path_cond_ stack — built for 1a-mem write enables — is armed whenever the body holds a property (a one-time pre-scan, not the dynamic mem_map_ test, so a guard cannot depend on statement order), and lower_cassert folds or2(not1(guard), cond) into the single cond pin. Folded, not carried as a second port: every consumer (pass.formal, the verify monitor encode, cgen_verilog, cgen_sim) then honors it by construction, where a separate guard port would reproduce this bug once per consumer that forgot to read it. match rides the same stack (it lowers to a unique_if whose arms are branch-lowered before the Hotmux merge). cassert is deliberately excluded — it is an elaboration check that must fold to a comptime constant, and !guard || cond under a runtime guard never folds. Test-block asserts are untouched: prp_sim emits them as real C++ control flow.
  
  Regression: case 9 of lhd/tests/lhd_formal_verify_test.sh — if/nested/elif/else and three match arms all prove (each named, so a regression says which gate was dropped); a property false under its own guard still refutes; and the over-constrained-assume case must NOT prove. 9a and 9c flip verdict if the fold is removed; 9b is the no-over-correction check and does not discriminate on its own.
  
  Phase 2 — antecedent vacuity — ALSO LANDED 2026-07-26. R1 traded a wrong-property bug for a possible vacuous-pass bug: a guard that can never hold makes guard implies cond trivially PROVEN while checking nothing. tolg now also leaves the RAW guard on a second guard sink that is diagnostic-only — a consumer that ignores it loses a warning, never correctness, which is the whole reason the obligation itself stayed folded into one pin. Each obligation carries guarded + vacuous_guard in formal_report.json, prints a VACUOUS continuation row under its verdict, warns (formal-vacuous-guard) at BOTH tiers — lhd formal verify and plain lhd compile via pass.formal, which is the flow a user actually runs — and fails under formal.strict. Severity ruling: warning by default, not the hard error a contradictory assume set gets, because a dead antecedent leaves the obligation genuinely TRUE (only an unsatisfiable assume set makes a proof unsound to rely on) and a guard unreachable at this top can be reachable under another parent.
  
  The measure is a FREE FRAME, not the unrolled window — the one design decision worth remembering. "Was the guard ever true in the cycles we checked?" is the intuitive question and it is wrong: an inductive proof settles at one checked step, so a live count == 5 guard reads as dead, and the same design flips answer depending on which strategy wins the ind/bmc race. Measured — bound=10 on a counter reported the same 1 checked step as bound=3. So the question asked is "is this guard satisfiable at all, over free inputs and free state?" (prover.is_false at the compile tier; one extra fresh-symbol encode at the verify tier), which over-approximates reachability and therefore has no false positives, no bound dependence, and no engine dependence. Deliberate non-goal: a guard satisfiable in the abstract but unreachable from reset is also vacuous and is not reported — detecting that is a reachability problem whose only cheap proxy is the unstable window.
  
  Phase 2 traps paid for: the free frame is wrapped in push/pop because it is the only place that ADDS assertions after verdicts settle, and getTimeoutCoreAssuming below it returns a subset of the solver's assertions — an unpopped frame would put vg_ equalities in a core meant to name toxic obligations. And the guard driver must be resolved by walking inp_edges: an unguarded fproperty has no guard sink pin at all, and get_driver_of_sink_name aborts in a dbg build on a pin that was never created — which is the COMMON path, so it took down every existing test until fixed. Regressions: case 10 of lhd_formal_verify_test.sh (10d pins the bound-independence — a window-based implementation fails it) and case 10 of lhd_formal_fail_test.sh (compile tier, with a live-guard control). Suite 1444/0. Home: 2f-verify.
• R1b — upass_dependency_test.sh was already red. LANDED 2026-07-26 Found while validating R1, unrelated to it (the pre-fix binary fails identically): --set upass.order=assert truncates the pass list, so simple.prp's cassert(c == 10) reaches the tolg seam undischarged and hard-errors cassert-not-comptime under the 2026-07-25 cassert ruling. Fixed by adding --set upass.tolg=false — the test is about uPass order resolution, and the seam explicitly exempts the LNAST-only tiers.
• R2 — make "assume anywhere in the code" mean something (root / child policy). G3 · medium Today a root-module input assume is a hard compile error (assume-refuted), while a child-module assume defers to a runtime check and is never re-proven at the parent that binds it — and pass/formal/pass_formal.cpp:351-367 promotes only PROVEN assumes to hypotheses, so an undischarged assume constrains nothing. Net: an assume either fails the build or is a no-op. Needs a ruling first (is a root input assume an environment constraint or an obligation? who discharges a child's — the parent binding, per the fcore contract?), then the wiring. Done when: lhd/tests:hier_property_test sheds its fixme tag — its case 3 (a parent that violates a submodule's assume must FAIL) is what keeps the fix honest. Home: 2f-verify (hierarchy half).
• R3 — multi-module Pyrope recompile: resolve sibling-file callees. G2 · medium pass.prp_writer emits one .prp per module, so recompiling the top of a freshly translated design dies with upass.tolg: call to 'mul' has no hardware lowering, and a monomorphized varargs callee is emitted as a qualified file.name(...) call that re-parses as an undefined read. This blocks the entire G2 loop — you cannot recompile what the translator just produced — and it is simultaneously 2w-prp_writer's A-LEC blocker and 2i-import's importer-dir-relative resolution slice. Done when: mod_mul_add, mod_twopaths and the three *_varargs_* cases join the prp-p2p-* allow-list, and the writer emits the bare callee name.

Tier B — G2: Verilog → Pyrope at scale

• R4 — re-baseline the 250-module XiangShan sweep. G2 · small (machine time) verification.html is a 2026-07-04 snapshot: LEC(lhd) pass 142 / inconclusive 64 / timeout 43 / fail 1; LEC(lgyosys) pass 160 / timeout 85; SIM pass 160 / error 45 / timeout 19 / skipped 20. It predates split_selfref at cprop, pass.single_edge, struct-typed ports, param provenance, the slang wire-classification split, and the clock-blindness encoder guards — some of which move those columns forward and some (the guards) deliberately backward. Re-run gen_verification.py and triage the residue by failure class, not by module. Done when: the regenerated table ships with a per-class residual count, each class pointing at the page that owns it. Everything else in this tier should be re-ordered by what it says.
• R5 — per-port memory clock binding. G2 · medium 2m-multiport_mem A: upass/tolg/upass_tolg.cpp:1273-1274 wires the Memory cell's clock_pin from one module-wide clock, so XiangShan's data_mem_8x4 (three distinct port clocks) silently collapses both read ports onto W0_clk — wrong Verilog, no diagnostic. The cell already models a per-port clock (clock_pin is pid 2, "×1 or n_ports") and cgen already derives single- vs multi-clock from the per-port drivers, so this is reader + tolg wiring. Memories are also where the R4 inconclusive/timeout residue concentrates.
• R6 — lhd compile links several lg: inputs; retire --lib. G2+G1 · medium 2i-import S3+S4: export a process-independent semdiff::canonical_hash plus the bottom-up Merkle driver, lift the pure-lg:-only cap (lhd/lhd_kernel.cpp:2632, "multiple lg: inputs are not supported yet"), and replace today's hhds name-hash dedup with digest → bucket → structural_match confirm → dedup + a report. This is also the user-requested replacement for --lib lg:sky130_vendor_flat_lg on the post-ABC LEC command, which is why it carries a G1 tag. Trap (non-negotiable): never dedup on the digest alone — a hash collision must be confirmed by structural_match or it becomes wrong hardware.
• R7 — prp→prp logical-fidelity bucket, memories first. G2 · medium 2w-prp_writer B: ~34 equiv pairs re-emit clean Pyrope that recompiles but is not equivalent to the golden .v — the safety net cannot see it, only lhd lec can. Work the buckets in this order: every mem_* (shares root causes with R5), then condout_*/cond_modified_read, then reg_async_flag/reg_attr_override/reg_delay_init, and finally the surprising small ones (trivial_if). The per-case triage recipe is already written on the page; promote each into prp-p2p-* as it is fixed.
• R8 — the two remaining 2i-issues lowering defects. G2 · small each A registered-output interface -> (reg count:u8@[0]) — the canonical counter straight out of docs/pyrope/04-variables.md, hard-erroring with homes at stage 0 … requires home -1 because the state-reg branch applies the feedforward home.min + 1 == rec.min invariant to a register that pins σ(q)=σ(din) with no flop crossing. B hierarchical (nested-tuple) enums — read of undefined variable 'eagle', because nested-enum detection accepts only an explicit enum(...) value, not the bare tuple the spec prescribes. Both are root-caused to a line with a proposed fix on the page. This is the "translated design still needs hand edits" class.
• R9 — the six silent simulation bugs (latch / negedge / memory). G2 · medium prp-sim-{latch_sim_clockgate_high, latch_sim_l1_buffer, flop_sim_secondary_negedge, mem_sim_negedge_write, hier_sim_negedge_sub, flop_sim_peek_secondary} — 4-tick trackers whose expected values come from Icarus on the netlist LiveHD itself emits. Each fails today with no diagnostic (lhd sim reports 0 errors and hands back wrong numbers) and each carries control asserts that pass, so a failure is attributable. Sim is the cheap oracle in the G2 iterate loop, so a silently-wrong sim poisons every iteration that trusts it. Home: 2f-latch (M6 residue). Fixture traps recorded there: implies lowers to || and short-circuits (hiding peek bugs), and a memory read carries same-address write forwarding (masking dropped writes).
• R10 — the translated-code cleanup batch. G2 · small each, independent (a) emitted Verilog ports are all signed even when the GraphIO says unsigned (2i-import item 6d, cgen_verilog.cpp); (b) prp-tbd-vector_io_ports — a positional/array port has no lowering in either direction (the named-tuple twin passes); (c) prp-tbd-wire_field_const_store — a const store to a wire-bundle field is folded and dropped, then tolg errors wire 'io.a' is never driven on valid code; (d) LSP hover on a translated module reports src: int where it should read src: u128 / pc: u64 (AluDataModule.prp:508) — readability is the ergonomics of the whole iterate loop (2n).
• R20 — Clock_cell: one recognized clock operator (gate / invert / divide). G2+G3 · medium A clock gate is INSTANTIATED in real RTL, so its output is an opaque Sub and every flop or memory it clocks refuses to encode. Measured on //bench:minion_lec 2026-07-26: 30 defs refuse — 22 flop + 8 memory, while 110/140 prove and nothing times out. Blackboxing the gate is what breaks the parent — an ICG’s output is a CLOCK and the encoder has no clock-identity model, so “prove the leaf, then box it” does not compose, and trusting prim_clk_gate is self-defeating. Replace the pattern with a first-class Clock_cell(clk_ref, en, div=1, invert=false) recognized at three entry points (inline RTL, an instantiated cell at the Sub boundary with NO inlining so lec_trust is respected, and a DECLARED foundry blackbox), then let each consumer lower its own view: LEC and formal verify (one shared encoder) and sim to a commit condition, synthesis to a real ICG cell so the shared gate survives — which also makes the cell the anchor for future POWER work (gating-coverage metrics, automatic clock-gate insertion, power-gating domains): a representation to keep, not a normalization to fold away. v1 is div=1 only — div>1 is an honest “not implemented” error (no test cases, pass_single_edge.cpp:521 refuses slots>2, and a divider’s initial phase would have to become part of its identity or two out-of-phase dividers compare equal; 2^N only even then — an odd divider takes the blackbox path). Step 0 is a soundness fix and lands first: memory_clock_shape_ok accepts ANY Sub on a memory clock pin — measured 21 of 21 minion memory clock edges are Sub-driven and encode as “commits every step”, so fixing the flop side first would mint false PROVENs. Done when: minion_lec’s 30 refusals go to 0, prim_clk_gate leaves lec_trust, and minion’s sim_cpu_top_ok flips to 1 (lhdsuite fixme issue 12), with lec_clock_blindness_test still refuting gated-vs-ungated. Home: 2f-latch M9; cross-ref R5 (2m-multiport_mem A) for the memory clock pin.

Tier C — G3: fast incremental assert/assume

• R11 — cone-scoped obligation cache keys (this is the "incremental" in incremental assert/assume). G3 · medium-large · highest leverage verify_obligation_key (pass/lec/query.cpp:5056) mixes every assertion of the whole encoding plus the scope, so any edit anywhere in the design invalidates every obligation's cached verdict — today's cache is a re-run cache, not an incremental one. Re-key each obligation on the digest of its own fan-in cone (semdiff::canonical_digest — already the formal verdict cache's identity primitive and the same digest 2opt-incr uses per ABC region) plus the in-force assume set and scope, so an edit re-proves only the obligations whose cone actually moved. Traps: the cone must cover state reachable within the checked bound (a bounded verdict is only valid at its bound — rule B); the assume set and scope must stay in the key or a constrained proof aliases an unconditional one (the P1 rule); a rename must be a miss, never a wrong bind. Done when: editing one module of a multi-property design re-proves only that module's obligations — pinned by a test that counts obligations with solve_ms > 0 in formal_report.json. Home: 2f-verify.
• R12 — cvc5 feedback: getDifficulty, getUnsatCore, and stop mining redundant bounds. G3 · medium Three named remainders on 2f-verify: produce-difficulty is still unused repo-wide (it is the hardness-mass ranking signal, and it is callable right after any checkSat including a timeout); getUnsatCore earns-its-keep pruning is unimplemented, so every inductive survivor is emitted rather than only those that demonstrably help a stuck obligation; and the range templates emit tight plus next-pow2 with no subsumption filter (count ≤ 5 AND count ≤ 7) — the one accidental overlapping-assume site in the repo. All three make the mined formal_mined.prp something an agent can paste without curating.
• R13 — temporal minimal core: rose / fell / stable. G3 · small-medium past[n] now lowers (a depth-n stage shift register; prp-tbd-temporal_past is already untagged), so what remains of the ruled-minimal core is the three pure functions of x and past(x), restricted to verification contexts. This is the SVA on-ramp: it is the smallest step that lets a property talk about time without any engine work (they produce ordinary flop cones the landed BMC/induction ladder already handles). Done when: delay2 LECs against its golden Verilog, a two-cycle property built from rose proves through lhd formal verify, and the docs drop the TBD marks for the core while deleting the out-of-scope operators. Home: 3f-temporal.
• R14 — re-admit design assumes into lhd lec. G3+G1 · small After the per-block assume-scoping change, lhd lec honors no user assume of any kind: graph_has_assume lives in prove_properties (verify) only, and compile_lec_formal_helpers was deleted. The engine hook (Lec_options::assumptions + the monitor encode in query.cpp) was deliberately retained and left unused, so re-admitting is flag wiring plus the P1 input-vs-internal classification and the "PROVEN under N input assume(s)" disclosure. Wanted by G1 too — the RTL-vs-RTL iteration gate should be allowed to run under the design's own environment constraints rather than over all inputs. Home: 2f-lec.
• R15 — emit assert/assume/coverpoint into slop. G3 · medium Properties exist for the formal tier only. Emitting them into the simulator gives the agent loop a cheap tier that runs before cvc5 (a failing sim assert is a refutation found in milliseconds) and makes coverpoint report something. Home: 4b.

Tier D — G1: fast synthesis iteration

• R16 — ABC memory admission. G1 · medium 2opt-incr subtask 0, still the stated prerequisite. The shipped 30M-GE coloring cap bounds the region's size estimate, not what ABC actually allocates — the measured mapping peak factor is 2.5–29.6×. Sample RSS growth after ~5% of estimated work (not 5% of nodes), project both completed-translation and mapping peak, and refuse cleanly — delete the partial network, emit no partial result, exit nonzero with a smaller-coloring recommendation — with pass.abc.allow_oversize=true as the acknowledged bypass and pass.abc.memory_budget_mb=N for CI determinism. This is what makes an unattended iteration loop safe to leave running on a notebook.
• R17 — post-ABC netlist fidelity, so the loop's LEC and STA actually run. G1 · medium Measured on dino today: memories expand to sky130 flops instead of staying an lgraph Memory / ware/rtl/cgen_memory_* instance (ABC has no memory support enabled by default, so they should never have been handed to it); the emitted Verilog carries always @(posedge 'hx /*cgen-miss*/) blocks; pass opentimer reports zero timing through the black-boxed memories; and lhd pass --help / lhd pass opentimer --help do not work the way pass abc --help does. Pair this with 3a-synth A — flops must keep instance-prefixed hierarchical names across the flatten, or post-synthesis LEC loses tier-1 correspondence for no reason. Done when: lg:dino_lg_abc LECs against dino_prp/PipelinedDualIssueCPU.prp and pass opentimer returns a real critical path on it.
• R18 — FIB timing probe + partition refinement policy. G1 · large 2opt-incr D+E. The probe answers "is X faster?" in seconds by resynthesizing only the touched cone with boundary delays pinned from the original run — ephemeral, never stitched, so its area redundancy structurally cannot reach P&R. Settle the page's open question first: does the probe need a one-sided guarantee (never claims faster when it is not) or only a good estimate? The pruning role argues for one-sided. E then grows a partition when its critical path spans input→output and splits above the band — which needs the GE→gate calibration 2c-color-size left open (421 GE/node measured on XSCore, so pass.color's 1k–5k GE bucket is not LiveSynth's 1k–5k gate band).
• R19 — parallel per-partition mapping + the area / no-op validation. G1 · large 2opt-incr B's parallel half is the lec fork pattern with a graph result rather than a verdict blob: per-child GraphLibrary saves, load_merge in the parent, srcid/QoR/refusal merging — and it interacts directly with R16, since splitting the memory budget N ways can refuse regions that map fine sequentially. F is the headline claim worth publishing: 24 of Anubis' 144 changes are NoChange by construction and both commercial flows burn ~106s re-synthesizing them, while a digest-keyed cache answers in O(#regions) lookups against a published baseline — and area, the one metric this flow is known to bleed, was never measured by the lineage.

Deliberately not on this list (nothing here moves G1–G3 in the near term): 2n LSP phases D–E (only the hover-width bug made it, as R10d), 2p-piper, 3l, 3c, 4c/4e, the Group-5 test/bench reorgs, cleanup, and the research tracks 4f-fluid-lec / 4f-bitwuzla / 3f-fluid. 3p and its prp-tbd-stdlib_import tracker are held back too: a standard library is worth building after R3–R8 settle what translated Pyrope actually looks like. 3f-semdiff's alg=functional n:m matcher is the one judgement call — it would shrink every miter, but R11's cone-scoped cache buys more per unit of work on the same designs, so it waits.

Pre TODO

Ideas to either turn into full todo pages or drop, ordered by date added (dd/mm/yyyy). Nothing pending right now (LEC-FLUID was promoted to 4f-fluid-lec in the 2026-07-10 formal reorg).

Pyrope

• Group 2:
  • 2i-issues Non-LEC compiler defects surfaced by the unexpected_* corpus (re-verified 2026-06-20, three oracles: lgyosys + cvc5 + exhaustive iverilog): registered-output interface -> (reg x@[0]) (A) and hierarchical enums (B) remain open, with no checked-in regression yet — their repros live inline in the 2i-issues page. The separate documented-but-unimplemented TBD features (temporal, testbench, stdlib, verif-extras) ship fixme-tagged prp-tbd-* fail-by-design tests under inou/prp/tests/fixme/ (see the TBD-pending section below).
• Group 3 — needs still-unspecified codegen/verification tasks first:
  • 3f-temporal Temporal library, trimmed to a minimal core (ruling 2026-07-10): past[n], rose, fell, stable — pure flop-lowering functions. next[n], windowed eventually/always, changed, and the .[rising]/.[falling]/.[changed] sugar are dropped from scope. Proving the resulting assertions is the landed 2f-verify engine's job.
  • 3f-fluid fluid lambdas: valid/retry/fire elastic lowering (parses only today).
  • 3f-macro macro= memory-compiler binding (reg ram:[1024]u32:[macro="sram_32kx32"]).
  • 3p Pyrope standard hardware library (prplib.ware) for common pipelined and non-pipelined designs: adders, multipliers, shifters, GCD, and debug/experimental blocks; includes deciding where prplib resides and how imports resolve. Also owns the comptime/software stdlib import("prp"): plus/len/map/filter/reduce, strings, math.
• Group 4:
  • 4b Emit assert/assume/coverpoint into slop.

TBD features still pending (2026-06-20 audit). Distinct from the A/B lowering defects in 2i-issues, these are Pyrope features that are documented (see docs/pyrope/15-tbd.md and the per-feature pyrope/3f-* pages) but not yet implemented. Each documented TBD was re-tested against a fresh bazel build -c dbg //lhd:lhd; the table is the verdict. The not-done ones (except the two the audit was told to skip — fluid and hierarchical enums) now ship a fail-by-design regression under inou/prp/tests/fixme/, wired as a fixme-tagged prp-tbd-* target (.bazelrc filters -fixme so bazel test //… stays green; clear the filter to see the failure, e.g. bazel test //inou/prp:prp-tbd-temporal_past --test_tag_filters=). Each flips green and sheds its fixme tag once the feature lands.

LiveHD

• Group 2:
  • 2n Pyrope LSP server — Phase B's documentSymbol remainder, findReferences, plus Phases D–E (workspace/packaging) remain (hover + goToDefinition/declaration incl. cross-file import() landed).
  • 2i-import Import & library-link redesign — a library is a directory (flat short pub names), a module's identity is its forward-canonical structure digest (the 3f-semdiff canonical digest, not name/path), and name collisions need no rename: structurally-identical modules dedup by digest at merge, distinct same-name modules coexist under unique internal file.entity names, and Verilog emission flattens to the bare entity name when unique (qualified on collision — landed). The same .prp compiles in the interactive single-file flow (imports → sibling source, importer-dir-relative; fixes the LSP false "unresolved import") and a hermetic parallel-bazel flow (imports → artifacts via lhd scan). Closes porting-log friction A1/A7/2f/6a/6c/C1.
  • 2m-multiport_mem Multiport / multi-clock memory codegen: per-port clock binding — multi-clock memories are silently collapsed to the write-port clock (driving case XiangShan data_mem_8x4, three distinct port clocks; R0_clk/R1_clk dropped from the emitted memory instance), a wrong-Verilog miscompile rather than a compile error.
  • 2w-prp_writer pass.prp_writer codegen completeness: prp→prp re-emission now hard-errors on unimplemented constructs (safety net; --set prp_writer.debug=true overrides) and the pipeline (stage[N]/@[N]), type_spec and tuple_concat round-trip + LEC (new prp-p2p-* family). Remaining: the unimplemented timecheck/for/func_def nodes and ~34 equiv pairs that emit clean-but-not-equivalent Pyrope (multi-clock memory is 2m-multiport_mem's).
  • 2f-lec LEC remainder on the shared core — LANDED 2026-07-10: the XSCore second splitter attack, F1 parallel hierarchical driver, checked/disclosed impl-side formal helpers, and persistent winning-engine/split-selector replay; LANDED 2026-07-11: two-tier state correspondence (semdiff full-match speculative pairing injected as uncertain, drop-all+retry-once on REFUTE, bounded-Proven suppression, entity-keyed pair hints — lec.state_pairing). Remaining: the memory items (same-shape permutation pairing retry, diverged-use collapse regression).
  • 2f-latch Full latch support (lgraph / Verilog / Pyrope / LEC latch-only and mixed / simulation), unified with flops and multiple clocks. Scope ruling 2026-07-20: SIMPLE latches, NO time borrowing (that is a backend technique; LiveHD stops at the ABC call and ABC's netlist has no borrowing either) — so a latch is exactly a flop-with-enable committing at the CLOSING edge of its window, an abstraction whose precondition M3 CHECKS rather than assumes. M0–M8 LANDED 2026-07-24: latches and negedge state now work in BOTH formal and simulation. The vehicle is M8 — edge normalization (pass.single_edge): a conditional LGraph→LGraph pass that REMOVES latches and negedge state before the solver sees them — verification and simulation only, never on the synthesis path (lhd compile still emits a real always_latch and negedge, asserted). It is SKIPPED entirely on a design with no latch, no negedge state and one clock net, which is the whole blast-radius argument. All three false-PROVEN clock-blindness holes are closed, including the same-clock EDGE hole M4 could not reach (it is dissolved by slotting, not encoded); the three verify fixtures are green and each MUTATES to a verbatim REFUTED; all 8 prp-v2prp2v latch/negedge reverse targets carry REAL verdicts instead of equivalence UNCHECKED. The transformation itself is validated against iverilog (source netlist vs normalized, 39 periods, two negative controls), which is what the binding cross-model gating rule demands. Fixed along the way: the verify fork-race codec dropped the refusal flag (a live vacuous exit-0 pass); cgen_verilog emitted an undeclared single-fanout flop enable; the slang reader lost an INFERRED latch (always @(*) if (en) q = d; read as comb with an X default). Deliberately not done: known-ratio multi-clock slotting (a second clock domain is skipped, so the detected-edge encoder and M6's sim model keep it), P>2, hierarchy (a stateful Sub fails closed), and witness-index decimation (an honest SKIP ships instead).
  • 2p-piper pass.piper — extract the landed pipeline-timing resolution (σ interval propagation, pipe_min/pipe_max narrowing on plain Flop cells — no Stage cell — and pending_time discharge) out of the inline tolg Time_checker into a standalone re-runnable lgraph pass, making its in-memory handoff maps durable attrs, adding true range intersection + the leftover-obligation guard, and deciding where the global σ timing lives (upass.timecheck stays as early diagnostics).
  • 2f-verify The agent-driven assert/assume loop — P1 + P2 + P3 LANDED 2026-07-12: assume-form discipline (input assumes = free disclosed env constraints; state-touching assumes = prove-then-use obligations — a false one REFUTES instead of faking a PROVEN; assume_nocheck_formal accepted + warned + disclosed), formal_report.json on every run (per-obligation verdicts/solve_ms/unknown_why, structured timeout core, artifact paths), and the mining core loop (learned literals + max-probe-seeded register templates → base proof → joint Houdini → paste-ready formal_mined.prp + mined[]; round-trip re-proves, stale facts refute). Remaining: ranking signals (getDifficulty/getUnsatCore), more template families, literal-recurrence filter, signed rendering. Memory-invariant templates and requires/ensures contracts are 3f-verify.
  • 2f-sim Agent-oriented lhd sim query API — one stateless, versioned JSON batch with five operation families (signals, value, changes, find, snapshot/diff), lossless full-width values, structured errors and automatic single-replay checkpoint planning. Existing --list-signals/--probe/--break-when become compatibility sugar; 4e's indexed trace store is a possible later backend, not a prerequisite. WaveformQA supplies the external correctness/speed benchmark for agent-generated queries across eight temporal-reasoning categories.
  • 2opt-freq Agent-in-the-loop frequency optimization — a coding agent iterates on Pyrope/Verilog with a compile → LEC gate (cycle-accurate, edited-vs-previous source) → pass.abc → QoR loop; only LEC-passing edits survive. Delivers the kernel primitives the loop lacks: ABC post-map delay/QoR read-back with srcid attribution (phase-1 oracle), block-scoped {::[abc="…", color="…"] …} attributes lowering to seeded colors (source-coded pass.color), per-region Map_options overrides, and the pass.opentimer driver as the phase-2 accurate scorer (absorbed from 3y-agent G).
  • 2opt-incr Incremental synthesis (LiveSynth DAC'17 / thesis ch.4, re-ported onto the cone engine) — fast better/worse? answers for small RTL edits: a DECISION ORACLE, not a fabrication path. 0/A/C landed 2026-07-16 (pass.abc caches regions under --workdir by default — digest-keyed reuse, NoChange = all hits/zero ABC, LEC-gated; abc.cache=false disables); B half (QoR aggregation), D/E/F pending. Two speeds: an ephemeral FIB timing probe that prunes (never stitched, so its area redundancy cannot reach P&R) and a durable DISJOINT-partition resynthesis before P&R — disjoint because the 2017 area bleed was inherent to overlapping single-output cones. Reuses 2f-lec's cone_digest to replace the paper's hand-rolled diff (83–95% of its live runtime) and the ABC cone prover to replace its per-net SAT setup (3.8–15.6× a full synthesis). v1 = area + timing; power deferred (needs VCD activity). NB the lineage never measured area or power.
  • 2f-formal Generic formal / compile-time tier — the engine rebase and the stateful verdict ladder LANDED 2026-07-11 (mode=fast unchanged, prove.cpp retained); reset-exclusion RESOLVED 2026-07-12 (the sound coarse guard + primary-reset-input pinning ship; the per-flop reset_pin guard was rejected as UNSOUND — recorded on the page). PENDING: only the ABC EXDC don't-care network, whose constraint pool includes assume_nocheck_synth facts (the compile tier is that form's only consumer; the form is a silent no-op until then).
• Group 3:
  • 3a-synth Synthesis flow follow-ons — flattening-aware state matching: the flop name-preservation contract through pass.abc/inline, semdiff virtual-flatten descent on call-tree mismatch (resolver-based, no hhds change for tier-2), and a small flattened-vs-hier LEC acceptance (ruling 2026-07-11: attack flattening here, once synthesis runs, not in the per-def matcher).
  • 3f-verify Forward-looking lhd formal verify work split off the agent-loop critical path (2026-07-12): automated memory-invariant templates (old V8 Attack A — near-term the agent hand-writes per-entry invariants where timeout cores point), requires/ensures lambda-contract lowering, and the dropped-by-ruling record (CEGAR lazy reads, learned-literal replay).
  • 3f-semdiff Functional (n:m) gap matching between two LGraphs (alg=functional) — per-gap boundary equivalence via a bounded miter gives unmatched regions shared IDs (+↔RCA), letting 2f-lec solve only the still-unmatched gaps. The v1 structural engine landed; the full-match (SRP/ERP signature) state pairing feeding 2f-lec's tier-2 correspondence landed 2026-07-11 (state_pairing); the canonical digest (semdiff::canonical_digest, consumed by the formal verdict cache and 2i-import) lives here.
  • 3l Demand-driven (lazy) emit + dead-code elimination for upass — remaining sea-of-nodes subtask.
  • 3y-agent lhd agent @tag workspace (setup/run/status/list/describe, TOML, JSONL) + deferred kernel follow-ups (multi-lg: linking residuals, graphviz emit; the pass.opentimer driver moved to 2opt-freq).
  • 3c Partition descriptor as a tree-level HHDS attribute.
• Group 4:
  • 4c Checkpoint format + reload validator (partition-keyed via state_shape_hash) — absorbs 4g; the hot-probe half landed as runtime --probe.
  • 4e Queryable indexed trace store (slice/transition/distribution queries).
  • 4f-fluid-lec Transaction-level (accepted-stream) equivalence for elastic valid/retry interfaces — think-more research track on the 2f-lec engine (promoted from Pre-TODO).
  • 4f-bitwuzla Optional bitwuzla solver backend — revisit only if cvc5 BV/array performance proves insufficient; would join the shared formal engine's portfolio, not replace cvc5.
• Group 5:
  • 5d Test reorg (tests/ layout, contract-test coverage, compile-driver script moves).
  • 5e IDAP perf-sweep pass (toggle passes, measure marginal cost, anti-pattern cleanup).
  • 5f Benchmark contracts (codegen throughput, simulation speed, agent-loop latency).
• Backlog: cleanup — replace the unmaintained C++ mustache library with inja.

Test status

The live suite (bazel test //inou/prp/... //upass/... //lnast/... //pass/...) was fully green at the last reorg snapshot. Doc-described errors that have no negative test yet are tracked in the prp_error_test_coverage note.