2f-formal Generic formal / compile-time tier — ABC EXDC remainder

The generic-formal page (the shared engine lives in pass/lec; the verify CLI's agent-loop objective is 2f-verify, LEC-specific work is 2f-lec). The compile-time tier is DONE except ABC EXDC: pass.formal mode=normal was re-based onto lec::prove_properties 2026-07-11 (compile profile: engine=bmc in-process, tiny bound, deterministic rlimit=budget_k×4096, timeout=0, ignore_assumes=true; mode=fast unchanged; prove.cpp RETAINED for fast/Hotmux/assumes/fallback), with the stateful verdict ladder: 1-induction proven ⇒ elide; BMC-from-reset refuted with refuted_at ≥ reset_hold ⇒ reachable CEX ⇒ deferred hard error; otherwise keep the runtime check + deferred warning. Tests lhd/tests/lhd_formal_rebase_test.sh.

Reset-exclusion is RESOLVED 2026-07-12 — record the trap. The sound part ships: the coarse BMC-window guard (pass_formal.cpp:504) + primary reset INPUT pinning in the induction rung (reset_negset gated on is_graph_input_pin). DO NOT resurrect the per-flop guard that pins a flop's own reset_pin/negreset inactive in the step — attempted and REVERTED as UNSOUND: reset_pin can carry a DESIGN-CONTROLLED derived signal (Pyrope reset_pin=ref <wire>, slang soft-reset nets, Yosys ARST/SRST/ALOAD/CLR), so pinning it drops REACHABLE mid-trace soft-reset states → false unbounded-Proven → set_proven silently ELIDES the runtime assert → miscompile; the step-vacuity base.isSat() guard does not catch it. Only a PRIMARY reset INPUT inherits the "no mid-trace reset" environment assumption. Same for reset-less power-on-initial flops. assert_always keeps Reset_policy::Include.

Pending — ABC EXDC don't-care network

• Hand the constraints already gathered per region (pass/abc/abc_map.cpp:386-417 — the assume_constraints gathering loop, currently a (void) no-op awaiting this item) to ABC's mfs/fraig as an EXDC network. Constraint sources: (a) proven asserts/assumes, (b) sidecar invariants proven unbounded by the verify engine, (c) assume_nocheck_synth facts — the compile tier is the only consumer of that form (assume-form contract; per-encounter diag warning; the user explicitly owns the risk). Status of the form today (survey 2026-07-12): assume_nocheck_synth parses in LEC formal blocks and is then skipped by every formal engine (lhd/lhd_kernel_formal.cpp:1673-1675) — until this item lands, the form is consumed by NOTHING, so writing one is a silent no-op.

Policy carried forward (unchanged)

• Asymmetric soundness: hard-error only on a definitive refutation that cannot be an artifact (stateless cone, or reachable-by-BMC witness, after assumes). Budget / Unknown / possibly-unreachable never error — a budget mistune can never turn a good build into a false error.
• Only proven assumes are hypotheses (no circular self-proof); the consistency check runs before any removal; contradictory assume set ⇒ warning + removals suppressed. assume_nocheck_synth facts are never proof hypotheses — they are synthesis-only don't-cares by explicit user fiat; assume_nocheck_formal is ignored by this tier entirely.

Future / deferred (other pages)

• The agent-driven verify loop (assume discipline, formal_report.json, mining) — 2f-verify, the current priority.
• Memory-invariant templates, requires/ensures contracts — 3f-verify.
• Temporal assertion proofs — 3f-temporal lowering on the shared engine.
• pass/memory port-sharing & banking — not yet paged (gets its own page when scheduled); calls the Prover primitives with its own conservative fallback.
• Runtime fallback execution — running runtime_check-marked asserts in sim/slop (4b).