diff --git a/.claude/commands/bugfix.md b/.claude/commands/bugfix.md
index 3e6758d37..70ba1cd28 100644
--- a/.claude/commands/bugfix.md
+++ b/.claude/commands/bugfix.md
@@ -145,6 +145,94 @@ Two tidier-looking rewrites of that line are both wrong:
   is named `$scrutineeN`, which the plugin skips; a hand-written `val` becomes a **named DFHDL
   value** and appears in the generated code. `DFBoolOrBitSpec`'s "selection operation" caught it.
 
+### Every member-creating front-end op needs a trydf'd, cleanly-named runtime def
+
+A raw `dfhdl.core.DFError$Derived` stack trace (instead of a formatted, positioned elaboration
+error) means some inline op creates IR members with **no `trydf` on its runtime path**: an inner
+TC conversion traps its own error and returns an errored value, and the first thing to touch it
+(`DFVal.Func`'s arg walk) throws the `Derived`, which nothing catches. The fix is never to wrap
+the inline body itself; move the `DFVal.Func` call (and, via by-name parameters, the TC-conversion
+arguments) into a **runtime def** wrapped in `trydf { ... }(using dfc, CTName("<opname>"))`
+(`DFBoolOrBit.Val.Ops.selRuntime` is the model; `CTName` is passed explicitly so the reported
+operation name stays the user-facing one).
+
+Two properties of that runtime def are load-bearing and easy to break:
+
+- **It must be public** (or at least reachable without a synthetic accessor). A `private` def
+  referenced from an inline body is compiled into an `inline$foo` accessor, and the plugin's
+  meta-context fallback deliberately skips `$`-named applies. The stamp it would have applied is
+  what *anonymizes* the propagated context, so without it a statement-positioned member silently
+  inherits the **design instance's own name** from the constructor DFC (`PrintCodeStringSpec`'s
+  "Boolean selection operation" caught three members all named after the outer `val id` binding).
+  The `treeOwnerApplyMap` + anonymous-fallback pair in `MetaContextGenPhase.transformApply` IS the
+  naming mechanism: spine applies of a `val` get the val's name, everything else gets an anonymous
+  stamp, and both assume they can stamp the op's context apply.
+- **Its error position comes from the plugin, not the DFC it happens to receive.** Applies inside
+  a *library* inline expansion carry the library's own tree positions, and for TASTy-unpickled
+  sources those are mangled (the tell: `DFBoolOrBit.scala:120:5642`, a line near the source's
+  line count with an offset-sized column). A **macro-synthesized** apply (e.g. the
+  `ExactOp3.apply` call that `exactOp3Macro` builds) is just as bad: its trees carry the
+  position of the quote inside the macro's own source (`Exact.scala:505`), even though
+  `Position.ofMacroExpansion` read *inside* that macro is the user span. `MetaContextGenPhase`
+  keeps an `inlinedUserPosStack` of enclosing user-source `Inlined` nodes and substitutes the
+  innermost user position wherever a stamp would otherwise carry an out-of-unit position; if
+  positions regress to library files, start there. To see who stamps what, add temporary **file
+  logging** (plugin `println` never reaches the sbtn client) around `addToTreeOwnerMap` and the
+  two stamp sites in `transformApply`, filtered to the Playground unit.
+
+Note the position such stamps produce is the innermost user-code inline call, which for a nested
+op is the failing *sub-expression*, not the whole statement; `DFDecimalSpec`'s "Runtime error
+positions" pins the exact spans.
+
+The **compile-time** twin of this disease is separate: a raw `compiletime.summonInline` failure
+inside an inline op's body reports at the summon site in the library
+(`DFBoolOrBit.scala:120:6431`-style once TASTy-mangled), with no outer position chain for the
+reporter to recover. Prove plugin-independence first with
+`-P:dfhdl.plugin:disableCustomPrinter`: the raw compiler output is identical, so neither the
+`CustomReporter` outer-drop nor any transform phase is the cause. The ops that report at the
+user's code get their positions from **Exact-boundary macros** that bind the user's expression at
+the call site, before inlining. Three cheaper spellings do NOT work from inside the inline body,
+because the inliner rewrites substituted argument trees to body-local positions (verified by
+macro file-logging: the user's literal argument arrives carrying a `DFBoolOrBit.scala` span): a
+TrapError-style given splicing `compiletime.error`, extra transparent-inline nesting around the
+summon, and a boundary macro taking the inline arg.
+
+The fix that works is restructuring the op through an `exactOp*` boundary: `sel` became a thin
+`transparent inline` forwarder to `exactOp3`, with its type-level dispatch re-encoded as
+mutually-exclusive `ExactOp3` given instances (disjointness via `NotGiven` guards, so no given
+prioritization). Two properties of that conversion carry the diagnostics:
+
+- **Search the op instance under the `ControlledMacroError` trap** (`activate()` before
+  `Implicits.search`, read `getLastMacroAbortError` on failure, `deactivate()` after — the
+  `DualSummonTrapError` protocol). Without the trap, a candidate whose nested TC resolution fails
+  through a reporting fallback macro RESOLVES with a stray `compiletime.error` spliced into the
+  instance, and that leftover is later reported at a library-internal span; with it, the
+  candidate aborts and the specific message (e.g. ``Unsupported value of type `"1"` for DFHDL
+  receiver type `Bit`.``) is captured.
+- **Report the trapped message at `Position.ofMacroExpansion`**, which inside an Exact-op macro
+  IS the user's expression span (the flattenInlined instrumentation confirmed it), not at any
+  tree position reachable from the operands.
+
+`exactOp1`/`exactOp2` still use the untrapped generic-message report and would benefit from the
+same upgrade. When converting an inline-dispatch op this way, the behavior matrix (which operand
+drives the result type, and every exception to it) must be transcribed case by case into disjoint
+givens; the op's existing print/selection spec tests are the safety net, and `UnstablePathSpec`
+guards the skolem concern that the old `asInstanceOf[OT]` retype was carrying (exactInfo's
+widening covers it at the macro boundary).
+
+`Exact.flattenInlined` is a related but distinct position-stripper, and worth ruling out
+explicitly when chasing a position bug: instrumenting it shows it discards `Inlined` wrappers
+whose `call` carries the user span (e.g. `method + @ Playground:<225..233>`) and hoists their
+proxy bindings into a flat macro-built Block, which is exactly why `MetaContextGenPhase`'s
+args-descent workaround exists ("macros (e.g., flattenInlined in Exact) strip Inlined wrappers
+that prepareForInlined relied on"). With that workaround the Exact-op stamps land correctly (the
+plugin debug log shows `ExactOp2.apply` stamped at user positions). It was NOT in the chain of
+either `sel` issue: the runtime junk stamps came from raw (non-Exact) inline bodies, and the
+compile-time `sel` failure happens before any Exact macro runs, because `sel`'s generic `OT`/`OF`
+params take the argument as-is; the INLINER itself repositions the substituted argument (macro
+logging showed the user's `"1"` literal arriving with the span of the `onTrue` reference inside
+the `sel` body).
+
 Both cost a full suite cycle to find, and neither is visible in the file being edited.
 
 ### Changing a type-level algebra: pick the mechanism by when it costs
@@ -202,6 +290,36 @@ failures to expect are therefore specs that assert an error and find none: `asse
 compile error for its snippet and then an elaboration error for its block, so "which half failed"
 is a real question and the failure position does not tell you.
 
+### Sibling op givens drift like twin helpers do
+
+The "twin helpers drift" rule from §2 applies to `ExactOp*` given families too. Issue #445: the
+commutative and non-commutative arith givens both carried wildcard-`Int` adaptation
+(`checkWildcardFit` + adapt to the bit-accurate operand), while the carry givens
+(`evOpCarryAddSubDFXInt`, `evOpCarryMulDFXInt`) had none, so an `Int <> CONST` parameter fell
+through to its runtime representation (signed 32-bit) and silently produced `SInt[33]` where
+`UInt[11]` was expected. When one given of a family handles a species of operand specially, diff
+the siblings for that branch before concluding the behavior difference is intentional.
+
+Two mechanism notes from that fix:
+
+- **Two operand species can be type-level identical and runtime distinct.** A Scala `Int`
+  (literal or runtime) and a DFHDL `Int` parameter both reach an op given as
+  `OutS = Boolean, OutW = Int, OutN = Int32`, but at runtime the Scala `Int` candidate has
+  already built a bit-accurate const at the value's minimal width, while the parameter is still
+  `DFInt32`. When the two need different semantics (carry ops: literals keep minimal width,
+  pinned by `100 *^ u8 == UInt[15]`; parameters adapt), dispatch on
+  `dfType.asIR.isDFInt32` at runtime and leave the static `Out` degraded, rather than inventing
+  an `IsConst`-style type-level discriminator (the §"stuck, not false" traps).
+- **For a new operand-legality rule on type-level `Boolean`/`Int` values, prefer a
+  `Check1`/`Check2` object (`Checked.scala`) over `AssertGiven`.** One object holds the condition
+  and message for every use site (alias it in `Constraints`, e.g. `CarryCheck`), it fails at
+  compile time when the types reduce, and the same instance is runtime-invocable with runtime
+  witnesses for the widened case. Empirically its failure inside an **untrapped** `exactOp2`
+  candidate resolution still surfaced the *specific* message at the *user's expression* span
+  (the spliced `compiletime.error` reports at the inlined call), so the generic-message caveat
+  above does not always cost you the diagnostic; verify per case with `assertCompileError` plus
+  one manual compile for the position.
+
 ### Probing type-level behaviour
 
 Two traps, each of which cost several cycles here:
@@ -290,6 +408,74 @@ mirrored rule (cache the resolved answer when it is `KnownConst`) is *unsound*,
 parametric. Prove which way the asymmetry runs before exploiting it, and pin **both** consumption
 orders in the regression test.
 
+### When the bug only appears across a serialization or cache boundary
+
+An internal `NoSuchElementException: key not found: "TW_..."` that fires only when the sub-design
+cache serves a hit, while a live elaboration of the identical source passes every check, is a
+**ghost binding**: a refTable VALUE whose member object was removed from the member list after the
+binding was made (issue #449). Live runs tolerate ghosts because the tokens a ghost emits still
+resolve in their own run; adoption re-mints tokens for members only, so a ghost's tokens dangle in
+the loading run. Lessons that generalize:
+
+- **The report's trigger may be cache-bypass, not cause.** A coarser cache above the buggy one
+  (the DFApp step cache replays the whole design on identical re-runs) can mean the failing run is
+  the FIRST to ever exercise the buggy path. "Edit + rebuild crashes, identical rebuild is fine"
+  read as invalidation; the truth was "adoption of this entry always crashes, and only the edit
+  makes elaboration actually run". Reproduce with two elaborations in one JVM through the
+  `MapSubDesignCache` seam before believing any staleness theory.
+- **Token forensics.** A ref token prints as `TW_<grpId1Hex>_<grpId2Hex>_<id>` with
+  `grpId = (position.hashCode, per-position JVM counter)`. In-JVM double elaboration gives the
+  storing run counter 0 and the loading run counter 1, so the failing token's counter says
+  immediately whether an unfreshened STORED token leaked through re-minting.
+- **Validate an artifact over its refTable VALUES, not only its keys.** "Every ref a member emits
+  is bound" (key closure) does not imply "every binding target is a member" (value re-uniting),
+  and only the second catches ghosts. `SanityCheck.refCheck` reports the same defect stage-side as
+  "Ref exists for a removed member"; `SubDesignEntry.isSelfContained` is the entry-level contract,
+  kept at SANITY level (asserted in the cache specs, never computed on the production store/lookup
+  path: always-on validation was rejected as redundant, since only a DFHDL bug or a dirty dev loop
+  can violate it). The stored entry is JSON, so all of this is checkable offline in a Playground
+  `@main` with no compiler edits.
+- **A removal decided on "unreferenced NOW" is unsound when a front-end handle can bind refs
+  LATER.** `MergeAssocFunc` absorbed an intermediate `+` Func and removed it before `lsbitsAt`
+  bound the offset refs to it (a method parameter is a handle; anonymity is about naming, not
+  about reachability from Scala code). A first fix made the removal resurrectable (un-ignore on
+  bind), and it worked, but was retired as compensation for a decision made at the wrong time.
+  The adopted principle instead, scoped to OPERATION SIMPLIFICATIONS
+  (arithmetic/logic/casting/conversion): a simplification never `setMember`s/`replaceMember`s/
+  removes an anonymous member; it builds a NEW member with fresh refs and leaves the superseded
+  one as debris for a snapshot-boundary sweep (`endDesign`, where "is it read?" has its final
+  answer). A blanket non-anonymous-target guard was rejected as too broad: construction
+  protocols (`initForced`, conditional-header retyping, `setName`/`tag`) legitimately keep
+  revision semantics; a ghost from one of those would surface loudly via `DB.check` /
+  `SanityCheck.refCheck` and the sanity-level `isSelfContained` contract in the cache specs.
+  Converted sites: `SimplifyFunc` (all extractors, with `rebindMeta` naming by `Ident` wrap and
+  the `=~` comparisons made ident-transparent via `stripTypePreservingAliases`) and the
+  DFDecimal carry peel/retype; the DFVal `AsIs` in-place conversions were audited and KEPT (a
+  revision, unlike a removal, cannot ghost: same-context bindings are re-pointed, cross-context
+  bindings to anons never exist).
+- **`clearDFHDL` before trusting a full-suite run that follows core elaboration edits.** Stale
+  `dfhdl-cache` entries stored by the pre-edit build stay digest-valid under uncommitted edits
+  (the `dfhdl@<version>` fold only changes on a commit), and adopting mixed-era entries can shift
+  the dclName enumeration: the AES `FullCompileSpec` file-NAME comparison failed with
+  `mulByte_0/1/2` renamed to `_1/2/3`, which reads like an enumeration bug and is cache debris.
+
+### A missed diagnostic can have several independent gates
+
+When the bug is "a warning/error SHOULD have fired and did not", the predicate that suppressed
+it is usually a conjunction, and more than one conjunct can be false for the same input. Fixing
+the gate the reporter (correctly) suspected and observing no change does not refute that fix; it
+means there is a SECOND gate. Issue #452: the parametric-width warning miss required both a
+width test that returned "not narrow" for unresolvable widths AND a tag check blind to the alias
+that parametric adaptation wraps around the tagged const (literal widths fold the const, so the
+alias only exists in the parametric regime). Re-run the reproducer after EACH gate fix, and
+diagnose the remaining gates by diffing the IR shape (`getCodeString`) of the warning and
+non-warning twins, not by re-reading the predicate.
+
+Probing designs outside the app runner has its own traps: a lib design class with all-defaulted
+parameters is auto-`@top`ed, and a bare `Design()` of a topped class returns a STAGED handle
+that never elaborates (no warnings, empty DB) — mark probe designs `@top(false)`. Read warnings
+via `dsn.dfc.getWarnings`; prefer `getCodeString` over `getDB` for IR inspection in a lib @main.
+
 ### Two habits that pay off
 
 - **Check the other backend.** Re-run with `compile --backend vhdl.v2008` (or `verilog`). If both
@@ -485,6 +671,49 @@ rule**, not a message worth improving. Add the verdict as a `newError` inside `g
 wins over the generic one automatically, and it arrives in the standard connectivity-error block
 (position, hierarchy, LHS, RHS) at no cost.
 
+### A conservative check over parametric bounds: prove, resolve, and only then reject
+
+A check that compares parameter-dependent index/width expressions (the slice-overlap check of
+issues #442/#447 is the archetype) must not collapse "parametric" to "unknown": that rejects
+`o(W-1, 0)` next to `o(2W-1, W)`, which are disjoint for every W. The machinery that fixed it
+generalizes:
+
+- **Decide on linear forms.** `IntExprCalc` decomposes an integer `DFVal` expression into
+  `Σ ci·basei + offset`; `Slice.Symbolic` carries `(lo, width)` as such forms, and
+  `IntExprCalc.DataCalc.proveNonNeg` proves `e >= 0` using validity facts (every slice width is
+  `>= 1` on the valid parameter domain). The single-fact proportional rule is enough for the
+  equal-bin family (`k*W` slices of width `W`) at any pair distance. When neither disjointness
+  nor overlap is provable, keep the conservative error but say *why* (a distinct message for
+  "cannot be proven disjoint"), the generic message misled the #442 reporter into a wrong theory.
+- **Resolve applied parameters through the instantiation site, never by gating on `isTop`.**
+  Under the hierarchical model *and* in DBs flattened from it (the backend printer's flat DB),
+  every design block's `ownerRef` is empty, so `isTop` reads true where it must not — that gate
+  silently kept a sub-design's `W` symbolic. `GoThroughDesignParams` is wrong in the other
+  direction: it folds even the elaboration root's parameters (that is `toScalaInt`'s job), and a
+  root parameter must stay symbolic because it is overridable in the generated HDL.
+  `DesignParam.instAppliedConstDataOpt` is the correct primitive: cached instance during
+  elaboration, `designBlockInstMap` on flat DBs, `parentSubDBOpt` walk-up on hierarchical
+  sub-DBs, and `None` exactly for the elaboration root.
+- **The check re-runs where you don't expect.** `connectionTable` is forced again by the backend
+  printer on the *flat* DB, so a connectivity-analysis fix must resolve under every DB model; a
+  test that only elaborates is blind to the print-time re-run. Pin it with
+  `getCompiledCodeString` (`ElaborationChecksSpec`'s sub-design slice test is the model).
+- **`clearDFHDL` between probe re-runs after compiler edits.** The sub-design elaboration cache
+  serves API-driven probes (`getCompiledCodeString`) too, not just DFApp runs; a cached child
+  elaboration skips the very code you just changed and the probe "reproduces" stale behavior.
+- One departial-coordinate trap fixed alongside: a vector `ApplyRange`'s indices are in **cell**
+  units and must be scaled by the cell width into bit coordinates; the old `shift(idxLow)` mixed
+  units and falsely errored even fully-literal `o(0, 1)` / `o(2, 3)` vector range connections.
+- **Symbolic elimination is a per-site semantic choice, not a smarter equivalence.** The width-fit
+  checks accept `LHS >= RHS` after a mixed `max`/`min` drops its symbolic operands
+  (`16 >= WIDTH max 16` decides as `16 >= 16`; `IntParamRef.compare(..., elimSymbolicMaxMin =
+  true)`), which deliberately tolerates the symbolic case's truncation. Two rules keep it safe:
+  it must NEVER back `=~`/`isSimilarTo` (calling `max(W,16)` similar to `16` would skip the
+  resize insertion in `toDFXIntOf` and miscompile), and every sibling decision site of the same
+  construct must adopt it together — carry promotion (`carryPromoteWidthCheck`) had to switch
+  with the TC width-fit check, or `sum := x + y` (anonymous, carry-promoted to `max+1`) would be
+  definitively rejected while `val xy = x + y; sum := xy` passes.
+
 ### Then measure the blast radius
 
 Run the full suite with the check in and **no stage fixes yet**. The failures are the deliverable
@@ -590,6 +819,43 @@ HDL method). A "simplification" that quietly moves an edge case is a second bug
   one backend's context split, audit the OTHER backend's rendering of the same IR feature: the
   distinction always exists somewhere, either in the literal or in the construct.
 
+- **A diagnostic that names IR members through the code printer inherits the code printer's
+  scoping, which is wrong for errors.** `refCodeString` renders a reference relative to the
+  reference's OWN design (and prints a `DesignParam` bare unconditionally), which is correct for
+  printing code and degenerate in an error message: two same-named constants from different
+  designs print identically ("width (OUTPUT_WIDTH) differs from width (OUTPUT_WIDTH)", issue
+  #448). Error messages must render relative to the ERROR SITE (`getRelativeName(dfc.ownerOption
+  ...)` → `c.OUTPUT_WIDTH` vs `OUTPUT_WIDTH`); that lives in a dedicated sibling
+  (`refErrorString` / `widthErrorString`), never in a change to the code-printing path. Related:
+  such runtime elaboration messages are untouched by the plugin's `disableCustomPrinter`, which
+  only affects scalac diagnostics; if a bad message survives that flag, stop suspecting the
+  custom printer.
+
+- **The Verilog printer prints arithmetic funcs bare and relies on the CONSUMER to size them —
+  self-determined contexts break that contract, and the fix belongs in a STAGE, not the
+  printer.** A carry-widened func (IR width exceeds its operands') is correct under an
+  assignment or a size cast (context-determined), and silently truncates as a concatenation
+  operand, because Verilog concat operands are self-determined. The `$signed({1'b0, ...})`
+  sign-conversion emission is such a context (issue #452 follow-up: `$signed({1'b0, a * 2'd3})`
+  pinned a promoted 4-bit mul at 2 bits). A printer-side width pin
+  (`$signed({1'b0, 4'(a * 2'd3)})`) works but was REJECTED by review: the established remedy
+  for "Verilog cannot render this anonymous construct inline" is the `NamedAliases` family —
+  a `NamedVerilogSelection` criterion names the carry func, its assignment provides the
+  widening context, and the concat sees a declared identifier. When auditing, check every
+  emission that embeds an expression in `{...}`. VHDL is immune (its helpers are
+  width-explicit) and DFacsimile follows IR semantics, so this class of bug is SV-only and
+  invisible to DFHDL-printout tests — pin the naming in `NamedSelectionSpec` and the emission
+  in `PrintVerilogCodeSpec` (append new tests at the END; mid-file inserts shift embedded
+  source positions).
+- **A transformation that wraps its operand BEFORE pattern-matching it hides the shape from
+  itself and every check inside the match.** `toDFXIntOf` applied the `.signed` sign fix first
+  and then matched for the carry-promotion candidate, so an unsigned chain meeting a signed
+  context was never promoted AND never warned (the warning lived inside the promotion branch).
+  Order shape-sensitive rewrites before wrapping, and when an upstream site pre-wraps (the
+  commutative sign alignment), unwrap the known wrapper — guarded by its exact signature
+  (signed alias over unsigned func, width == w+1, widths resolved through params) so
+  reinterpret casts stay untouched.
+
 The blast-radius step still applies, and here it reads inverted: a fully green suite with no
 reference output changed is not evidence the fix is inert, it confirms the whole branch was
 untested. The `ref/` grep from §2 predicts this: only the shared-variable form of `:=` appeared
@@ -641,9 +907,12 @@ Revert only the changed guard in place instead, and watch for a silent run.
 then passes, and the honest reading ("my reproducer is wrong, go find a different shape") sends you
 chasing a distinction that does not exist. The tell is a `scala.MatchError: <n> (of class
 java.lang.Integer)` from `compileIncremental` on some *other* subproject during the same session —
-the same corrupted-incremental-state symptom as after any front-end edit. Run `clean` before
-trusting a stashed run, and re-confirm on a clean build before concluding the test does not
-reproduce.
+the same corrupted-incremental-state symptom as after any front-end edit. A
+`dotty.tools.dotc.core.Denotations$StaleSymbolException` ("stale symbol ... referred to in run")
+while compiling a *downstream* subproject is the same disease, and so is a phantom
+`[E046] Cyclic Error ... Cyclic reference involving val <import>` in an untouched `core` file
+right after a `compiler_ir` edit — even a body-only one. Run `clean` before trusting a stashed
+run, and re-confirm on a clean build before concluding the test does not reproduce.
 
 This is not paranoia. A `<Stage>Spec` asserts on the DFHDL *printout*, and two different IRs can
 print identically — the printout is the stage contract precisely because it hides representation.
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/analysis/DFValAnalysis.scala b/compiler/ir/src/main/scala/dfhdl/compiler/analysis/DFValAnalysis.scala
index ce9b1b31a..18ae57ed1 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/analysis/DFValAnalysis.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/analysis/DFValAnalysis.scala
@@ -32,6 +32,43 @@ object Ident:
     if (alias.hasTagOf[IdentTag]) Some(alias.relValRef.get)
     else None
 
+extension (member: DFMember)
+  // The kind-level half of the unreferenced-anonymous sweeps: whether this member MAY be
+  // dropped when nothing reads it. SHARED by the `DropUnreferencedAnons` compiler stage and
+  // elaboration's end-of-design sweep (`DesignContext.sweepUnreadAnons`), so the two can never
+  // drift. The "is it read" half is deliberately NOT shared: the stage asks
+  // `originMembers.isEmpty` on the immutable DB, while the elaboration sweep computes
+  // reachability over `getRefs` on the mutable snapshot (where origin tracking is not final).
+  def isDroppableIfUnread(using MemberGetSet): Boolean = member match
+    // conditional headers can be values (referenced by nothing, driven per branch)
+    case _: DFConditional.Header => false
+    // idents are always kept
+    case Ident(_) => false
+    // a procedural (Unit-return) method call is a statement: referenced by nothing,
+    // dropped by nothing
+    case DFVal.Func.Call(call, _) if call.dfType =~ DFUnit => false
+    // a declaration is a PLACE, not an expression: an anonymous dcl must survive the
+    // elaboration sweep so the elaboration check can REJECT it ("anonymous port/var
+    // declarations are forbidden"), and unreferenced named dcls belong to
+    // `DropUnreferencedVars`. No change for the stage: post-check DBs hold no anonymous dcls.
+    case _: DFVal.Dcl => false
+    case dfVal: DFVal => dfVal.isAnonymous
+    case _: DFRange   => true
+    case _            => false
+end extension
+
+extension (dfVal: DFVal)
+  // Dereferences type-preserving `AsIs` wrappers (idents and other identity casts) down to the
+  // first value of a different shape. SHARED by `IntExprCalc.Calc.strip` and `SimplifyFunc`'s
+  // structural comparisons, so simplifications see through `Ident(a)` to `a` (a named ident is
+  // value-identical to what it wraps).
+  @tailrec def stripTypePreservingAliases(using MemberGetSet): DFVal = dfVal match
+    case alias: DFVal.Alias.AsIs =>
+      val relVal = alias.relValRef.get
+      if (alias.dfType == relVal.dfType) relVal.stripTypePreservingAliases
+      else alias
+    case _ => dfVal
+
 //A design parameter is an as-is alias that:
 //1. has `DesignParamTag` tag
 //TODO: This is not yet working. more complicated than initially thought.
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/ir/ConnectToMap.scala b/compiler/ir/src/main/scala/dfhdl/compiler/ir/ConnectToMap.scala
index e18a9da75..4161459b6 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/ir/ConnectToMap.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/ir/ConnectToMap.scala
@@ -16,19 +16,27 @@ object ConnectToMap:
   extension (ctm: ConnectToMap)(using MemberGetSet)
     def connectToVals: Set[ConnectToVal] = ctm.keySet
 
-    /** All nets whose slice overlaps `slice` on `dcl`, including ones whose overlap status is
-      * merely `Unknown` (conservative).
+    /** All nets whose slice overlaps `slice` on `connectToVal`, each with its overlap verdict:
+      * `Tri.Yes` for a proven overlap, `Tri.Unknown` when the relation could not be proven either
+      * way (conservatively included). Provably disjoint nets are excluded.
       */
-    def getNets(connectToVal: ConnectToVal, slice: Slice): Set[DFNet] =
+    def getNetsVerdicts(connectToVal: ConnectToVal, slice: Slice): Vector[(DFNet, Tri)] =
       ctm.get(connectToVal) match
         case Some(entry) =>
           val widthOpt = connectToVal.widthIntOpt
-          entry.nets.collect {
-            case (storedSlice, net)
-                if ConnectToMap.overlapsSlices(storedSlice, slice, widthOpt) != Tri.No =>
-              net
-          }.toSet
-        case None => Set.empty
+          entry.nets.view
+            .map { (storedSlice, net) =>
+              (net, ConnectToMap.overlapsSlices(storedSlice, slice, widthOpt))
+            }
+            .filter(_._2 != Tri.No)
+            .toVector
+        case None => Vector.empty
+
+    /** All nets whose slice overlaps `slice` on `dcl`, including ones whose overlap status is
+      * merely `Unknown` (conservative).
+      */
+    def getNets(connectToVal: ConnectToVal, slice: Slice): Set[DFNet] =
+      getNetsVerdicts(connectToVal, slice).view.map(_._1).toSet
     def getNets(dfVal: DFVal): Set[DFNet] =
       dfVal.departialPBNS match
         case Some(connectToVal, slice) => getNets(connectToVal, slice)
@@ -62,7 +70,7 @@ object ConnectToMap:
   /** Pairwise slice-overlap predicate used by `getNets`. Returns `Tri.Yes` only when provably
     * overlapping, `Tri.No` only when provably disjoint, `Tri.Unknown` otherwise.
     */
-  private def overlapsSlices(a: Slice, b: Slice, widthOpt: Option[Int]): Tri =
+  private def overlapsSlices(a: Slice, b: Slice, widthOpt: Option[Int])(using MemberGetSet): Tri =
     (a, b) match
       case (Slice.Concrete(ra), Slice.Concrete(rb)) =>
         if (ra.intersect(rb).nonEmpty) Tri.Yes else Tri.No
@@ -71,5 +79,40 @@ object ConnectToMap:
       case (Slice.Full, Slice.Concrete(r)) =>
         if (r.isEmpty) Tri.No else Tri.Yes
       case (Slice.Full, Slice.Full) => Tri.Yes
-      case _                        => Tri.Unknown
+      // a symbolic slice is a valid (nonempty) selection, so it always overlaps the full value
+      case (_: Slice.Symbolic, Slice.Full) | (Slice.Full, _: Slice.Symbolic) => Tri.Yes
+      case (Slice.Symbolic(loA, wA), Slice.Symbolic(loB, wB))                =>
+        symbolicOverlap(loA, wA, loB, wB)
+      case (Slice.Symbolic(loA, wA), Slice.Concrete(rb)) =>
+        import IntExprCalc.DataCalc.const
+        symbolicOverlap(loA, wA, const(rb.start), const(rb.length))
+      case (Slice.Concrete(ra), Slice.Symbolic(loB, wB)) =>
+        import IntExprCalc.DataCalc.const
+        symbolicOverlap(const(ra.start), const(ra.length), loB, wB)
+      case _ => Tri.Unknown
+
+  /** Overlap of `[loA, loA + wA)` and `[loB, loB + wB)` decided on the linear forms, for every
+    * valid parameter assignment. The slice widths serve as the `>= 1` facts for the inequality
+    * proofs (see [[IntExprCalc.DataCalc.proveNonNeg]]).
+    */
+  private def symbolicOverlap(
+      loA: IntExprCalc.Linear,
+      wA: IntExprCalc.Linear,
+      loB: IntExprCalc.Linear,
+      wB: IntExprCalc.Linear
+  )(using MemberGetSet): Tri =
+    import IntExprCalc.DataCalc.*
+    val facts = List(wA, wB)
+    def nonNeg(e: IntExprCalc.Linear): Boolean = proveNonNeg(e, facts)
+    // disjoint when one slice provably ends before the other begins:
+    // hiA < loB  <=>  loB - loA - wA >= 0 (and symmetrically)
+    if (nonNeg(sub(sub(loB, loA), wA)) || nonNeg(sub(sub(loA, loB), wB))) Tri.No
+    // overlapping when each slice provably begins no later than the other ends:
+    // loB <= hiA  <=>  loA + wA - 1 - loB >= 0 (and symmetrically)
+    else if (
+      nonNeg(addConst(sub(add(loA, wA), loB), -1)) &&
+      nonNeg(addConst(sub(add(loB, wB), loA), -1))
+    ) Tri.Yes
+    else Tri.Unknown
+  end symbolicOverlap
 end ConnectToMap
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/ir/Coverage.scala b/compiler/ir/src/main/scala/dfhdl/compiler/ir/Coverage.scala
index 0e50e2fe4..91b6b44bb 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/ir/Coverage.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/ir/Coverage.scala
@@ -6,19 +6,26 @@ import scala.collection.immutable
   * [[DFMember.departial]] to describe which bits of the underlying declaration an alias chain
   * touches.
   *
-  * The representation is deliberately conservative: when a slice's endpoints depend on a design
-  * parameter, we fall back to [[Slice.Unknown]] rather than attempting symbolic interval
-  * arithmetic.
+  * Parameter-dependent endpoints are kept as [[Slice.Symbolic]] linear forms (see
+  * [[IntExprCalc.DataCalc]]), so provably-disjoint parametric slices are recognized as such;
+  * [[Slice.Unknown]] remains the conservative fallback when the bounds cannot be linearized.
   */
 enum Slice derives CanEqual:
   /** A concrete bit range in the root value's coordinates. */
   case Concrete(range: Range)
 
+  /** A bit range `[lo, lo + width)` whose endpoints are linear forms over unresolved (top-design)
+    * parameters, in the root value's coordinates. Constructed only via [[Slice.symbolic]], so at
+    * least one of the two forms is non-constant.
+    */
+  case Symbolic(lo: IntExprCalc.Linear, width: IntExprCalc.Linear)
+
   /** The entire value. Used when the value's width itself is symbolic. */
   case Full
 
   /** A slice whose endpoints are symbolic and could not be resolved. */
   case Unknown
+end Slice
 
 object Slice:
   def fromRange(range: Range): Slice = Concrete(range)
@@ -28,16 +35,38 @@ object Slice:
     case Some(w) => Concrete(0 until w)
     case None    => Full
 
+  /** Build a symbolic slice, collapsing to [[Concrete]] when both forms are constant. */
+  def symbolic(lo: IntExprCalc.Linear, width: IntExprCalc.Linear): Slice =
+    if (lo.terms.isEmpty && width.terms.isEmpty)
+      Concrete(lo.offset until lo.offset + width.offset)
+    else Symbolic(lo, width)
+
+  /** Map an outer selection `outer` (relative to an alias whose selected region starts at bit
+    * `loBits` of the relative value and spans `selWidthBits` bits) into the relative value's
+    * coordinates.
+    */
+  def compose(outer: Slice, loBits: IntExprCalc.Linear, selWidthBits: IntExprCalc.Linear)(using
+      MemberGetSet
+  ): Slice =
+    import IntExprCalc.DataCalc.{add, const}
+    outer match
+      case Concrete(r)     => symbolic(add(loBits, const(r.start)), const(r.length))
+      case Symbolic(lo, w) => symbolic(add(lo, loBits), w)
+      case Full            => symbolic(loBits, selWidthBits)
+      case Unknown         => Unknown
+
   extension (slice: Slice)
     /** Shift the slice by a (concrete) delta in bit positions. Unknown/Full stay themselves —
       * shifting an unknown slice is still unknown.
       */
     def shift(delta: Int): Slice = slice match
-      case Concrete(r) => Concrete(Range(r.start + delta, r.end + delta))
-      case other       => other
+      case Concrete(r)     => Concrete(Range(r.start + delta, r.end + delta))
+      case Symbolic(lo, w) => Symbolic(lo.copy(offset = lo.offset + delta), w)
+      case other           => other
     def isEmpty: Boolean = slice match
-      case Concrete(r) => r.isEmpty
-      case _           => false
+      case Concrete(r)    => r.isEmpty
+      case Symbolic(_, w) => w.terms.isEmpty && w.offset <= 0
+      case _              => false
 
     /** Does this slice cover the full width of the underlying value? `Tri.Unknown` when either the
       * slice or the width is symbolic.
@@ -45,6 +74,7 @@ object Slice:
     def isFullOf(widthOpt: Option[Int]): Tri = slice match
       case Full        => Tri.Yes
       case Unknown     => Tri.Unknown
+      case _: Symbolic => Tri.Unknown
       case Concrete(r) =>
         widthOpt match
           case Some(w) => if (r.start == 0 && r.end == w) Tri.Yes else Tri.No
@@ -64,9 +94,9 @@ object Tri:
 /** Accumulated write coverage over one DFVal.
   *
   *   - `bits` holds the concretely-tracked bit positions that are proven assigned/connected.
-  *   - `unknownTouched` is set when a write with a [[Slice.Unknown]] or a [[Slice.Full]] over an
-  *     unknown width has been observed, meaning we know the value was touched but not precisely
-  *     where.
+  *   - `unknownTouched` is set when a write with a [[Slice.Unknown]], a [[Slice.Symbolic]], or a
+  *     [[Slice.Full]] over an unknown width has been observed, meaning we know the value was
+  *     touched but not precisely where.
   *   - `fullyCovered` is a latch flag set when we observe a write that covers the entire value,
   *     even if the value's width is symbolic (so we cannot represent it as a concrete BitSet). Once
   *     set, any coverage query returns `Yes` regardless of `bits`.
@@ -97,7 +127,8 @@ final case class Coverage(
         widthOpt match
           case Some(w) => copy(bits = bits ++ immutable.BitSet.fromSpecific(0 until w))
           case None    => copy(fullyCovered = true)
-      case Slice.Unknown => copy(unknownTouched = true)
+      // a symbolic slice has no concrete bit positions to track, so it degrades to "touched"
+      case _: Slice.Symbolic | Slice.Unknown => copy(unknownTouched = true)
 
   /** Does this coverage touch any bit of `slice`? */
   def overlaps(slice: Slice, widthOpt: Option[Int]): Tri =
@@ -116,7 +147,7 @@ final case class Coverage(
           if (bits.nonEmpty) Tri.Yes
           else if (unknownTouched) Tri.Unknown
           else Tri.No
-        case Slice.Unknown =>
+        case _: Slice.Symbolic | Slice.Unknown =>
           if (bits.nonEmpty || unknownTouched) Tri.Unknown
           else Tri.No
 
@@ -139,7 +170,7 @@ final case class Coverage(
               else Tri.No
             case None =>
               if (unknownTouched) Tri.Unknown else Tri.No
-        case Slice.Unknown => Tri.Unknown
+        case _: Slice.Symbolic | Slice.Unknown => Tri.Unknown
 
   /** Is this coverage full for the given (possibly unknown) width? */
   def isFull(widthOpt: Option[Int]): Tri = contains(Slice.Full, widthOpt)
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/ir/DB.scala b/compiler/ir/src/main/scala/dfhdl/compiler/ir/DB.scala
index f16fea8d4..ba154e8a8 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/ir/DB.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/ir/DB.scala
@@ -611,7 +611,8 @@ final case class DB private (
         toValAndSliceOption match
           // found target variable or port declaration for the given connection/assignment
           case Some(connectToVal, slice) =>
-            val prevNets = connToMap.getNets(connectToVal, slice)
+            val prevNetsVerdicts = connToMap.getNetsVerdicts(connectToVal, slice)
+            val prevNets = prevNetsVerdicts.view.map(_._1).toSet
             // checking multiple assignments from different domains, except for a condition
             // where the declaration is a shared variable.
             // this is used to define a shared variable which is against the RT model,
@@ -620,7 +621,7 @@ final case class DB private (
               case dcl: DFVal.Dcl if dcl.modifier.isShared => true
               case _                                       => false
             if (!isSharedVar)
-              prevNets.headOption.foreach: prevNet =>
+              prevNetsVerdicts.headOption.foreach: (prevNet, _) =>
                 if (prevNet.getOwnerDomain != net.getOwnerDomain)
                   newError(
                     s"""|Found multiple domain assignments to the same variable/port `${connectToVal.getFullName}`.
@@ -628,14 +629,26 @@ final case class DB private (
                         |The previous write occurred at ${prevNet.meta.position}""".stripMargin
                   )
             // go through all previous nets and check for collisions
-            prevNets.foreach: prevNet =>
+            prevNetsVerdicts.foreach: (prevNet, verdict) =>
               // multiple assignments are allowed in the same range, but not multiple
               // connections or a combination of an assignment and a connection
               if (prevNet.isConnection || prevNet.isAssignment && !net.isAssignment)
-                newError(
-                  s"""Found multiple connections write to the same variable/port `${connectToVal.getFullName}`.
-                     |The previous write occurred at ${prevNet.meta.position}""".stripMargin
-                )
+                if (verdict == Tri.Yes)
+                  newError(
+                    s"""Found multiple connections write to the same variable/port `${connectToVal.getFullName}`.
+                       |The previous write occurred at ${prevNet.meta.position}""".stripMargin
+                  )
+                // the slices could not be proven overlapping NOR disjoint (parameter-dependent
+                // indices the slice calculus cannot relate), so the write is conservatively
+                // rejected with an error that names the actual problem
+                else
+                  newError(
+                    s"""|Found a write to the same variable/port `${connectToVal.getFullName}` that cannot be proven to be
+                        |disjoint from a previous write, because their parameter-dependent bit ranges could not be
+                        |resolved. If the ranges never overlap, restructure their indexing so the compiler can relate
+                        |them, or use assignments within a process instead of connections.
+                        |The previous write occurred at ${prevNet.meta.position}""".stripMargin
+                  )
             // if no previous connection in this range, we add it to the range map
             if (prevNets.isEmpty)
               getConnToMap(
@@ -1670,6 +1683,55 @@ final case class DB private (
   //   * Rule 4: a loop containing an RT-domain shared-variable write moves whole into the
   //     clocked process, so all its content must be sequential-sink writes with settled
   //     reads; otherwise the loop must be split.
+  // The process block a member statement resides in, if any (walks out of nested
+  // conditional/step blocks; a domain owner boundary means the member is not in a process).
+  @tailrec private def ownerProcessOpt(member: DFMember): Option[ProcessBlock] =
+    member.ownerRef.get match
+      case pb: ProcessBlock => Some(pb)
+      case _: DFDomainOwner => None
+      case owner: DFBlock   => ownerProcessOpt(owner)
+      case _                => None
+
+  // A variable (or any part of it) written with both a blocking (`:=`) and a non-blocking
+  // (`:==`) assignment inside the same process commits at two different times, which is a
+  // semantic contradiction; the generated HDL then mixes `=`/`<=` on one variable inside a
+  // single process, which downstream tools reject (issue #446). The rule is per declaration
+  // and per process: which parts are assigned is irrelevant, and a consistently-assigned
+  // variable is fine with either kind (a blocking-assigned temporary in a clocked process
+  // is legitimate; see DropBAssignFromSeqProc). Shared variables are excluded, since their
+  // writes are already restricted to `:==` at compile time.
+  def mixedAssignKindCheck(): Unit =
+    val errors = collection.mutable.ArrayBuffer[String]()
+    val firstNets = collection.mutable.Map.empty[(ProcessBlock, DFVal.Dcl), DFNet]
+    val reported = collection.mutable.Set.empty[(ProcessBlock, DFVal.Dcl)]
+    members.foreach {
+      case net @ DFNet.Assignment(toVal, _) =>
+        toVal.departialDcl match
+          case Some((dcl, _)) if !dcl.modifier.isShared =>
+            ownerProcessOpt(net).foreach { pb =>
+              val key = (pb, dcl)
+              firstNets.get(key) match
+                case Some(prevNet) =>
+                  if (prevNet.op != net.op && !reported.contains(key))
+                    reported += key
+                    errors +=
+                      s"""|DFiant HDL connectivity error!
+                          |Position:  ${net.meta.position}
+                          |Hierarchy: ${net.getOwnerDesign.getFullName}
+                          |LHS:       ${printer.csDFValRef(net.lhsRef.get, net.getOwnerDesign)}
+                          |RHS:       ${printer.csDFValRef(net.rhsRef.get, net.getOwnerDesign)}
+                          |Message:   Found both blocking (`:=`) and non-blocking (`:==`) assignments to the same variable/port `${dcl.getFullName}` within the same process.
+                          |Use one assignment kind consistently for this variable inside the process.
+                          |The previous write occurred at ${prevNet.meta.position}""".stripMargin
+                case None => firstNets(key) = net
+            }
+          case _ =>
+      case _ =>
+    }
+    if (errors.nonEmpty)
+      throw new IllegalArgumentException(errors.mkString("\n\n"))
+  end mixedAssignKindCheck
+
   def sharedVarCheck(): Unit =
     val errors = collection.mutable.ArrayBuffer[String]()
     def memberError(member: DFMember, msg: String): Unit =
@@ -1677,12 +1739,6 @@ final case class DB private (
                     |Position:  ${member.meta.position}
                     |Hierarchy: ${member.getOwnerDesign.getFullName}
                     |Message:   $msg""".stripMargin
-    @tailrec def ownerProcessOpt(member: DFMember): Option[ProcessBlock] =
-      member.ownerRef.get match
-        case pb: ProcessBlock => Some(pb)
-        case _: DFDomainOwner => None
-        case owner: DFBlock   => ownerProcessOpt(owner)
-        case _                => None
     members.foreach { m =>
       // Rule 1: a write to a shared variable inside a `process(all)`
       m match
@@ -2031,6 +2087,7 @@ final case class DB private (
     condExprNamedValCheck()
     blockScopeCheck()
     sharedVarCheck()
+    mixedAssignKindCheck()
 
   // Whole-tree checks, run once on the root: the cross-design connectivity /
   // RT-domain / device-top checks, via the `*` clones that navigate the
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFMember.scala b/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFMember.scala
index d77dc104e..4500239b6 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFMember.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFMember.scala
@@ -386,20 +386,35 @@ object DFVal:
       case alias: DFVal.Alias                 => alias.relValRef.get.dealias
       case _                                  => None
     @tailrec private def departial(slice: Slice)(using MemberGetSet): (DFVal, Slice) =
+      import IntExprCalc.DataCalc.*
       dfVal match
         case partial: DFVal.Alias.Partial =>
           val relVal = partial.relValRef.get
           partial match
             case partial: DFVal.Alias.ApplyRange =>
-              partial.idxLowRef.getIntOpt match
-                case Some(idxLow) => relVal.departial(slice.shift(idxLow))
-                case None         => relVal.departial(Slice.Unknown)
+              // the selection indices are in cell units for a vector range selection,
+              // in bit units otherwise
+              val unitWidthOpt = relVal.dfType match
+                case DFVector(cellType = cellType) => linearOfTypeWidth(cellType)
+                case _                             => Some(const(1))
+              val newSlice = unitWidthOpt match
+                case Some(unitWidth) =>
+                  val loUnits = linearOfParamRef(partial.idxLowRef)
+                  val hiUnits = linearOfParamRef(partial.idxHighRef)
+                  val selWidthUnits = addConst(sub(hiUnits, loUnits), 1)
+                  (mulOpt(loUnits, unitWidth), mulOpt(selWidthUnits, unitWidth)) match
+                    case (Some(loBits), Some(selWidthBits)) =>
+                      Slice.compose(slice, loBits, selWidthBits)
+                    case _ => Slice.Unknown
+                case None => Slice.Unknown
+              relVal.departial(newSlice)
             case partial: DFVal.Alias.ApplyIdx =>
               partial.relIdx.get match
                 case DFVal.Alias.ApplyIdx.ConstIdx(idx) =>
-                  partial.dfType.widthIntOpt match
-                    case Some(w) => relVal.departial(slice.shift(idx * w))
-                    case None    => relVal.departial(Slice.Unknown)
+                  linearOfTypeWidth(partial.dfType) match
+                    case Some(cellWidth) =>
+                      relVal.departial(Slice.compose(slice, scale(cellWidth, idx), cellWidth))
+                    case None => relVal.departial(Slice.Unknown)
                 // if not a constant index selection, then the entire value range is affected
                 case _ =>
                   relVal.dealias match
@@ -530,6 +545,42 @@ object DFVal:
       appliedValRefOpt.getOrElse(defaultValRef.asInstanceOf[DFVal.Ref])
     def appliedOrDefaultVal(using MemberGetSet): DFVal =
       appliedValOpt.getOrElse(defaultValRef.get.asInstanceOf[DFVal])
+
+    // The applied constant data resolved ONLY through an instantiation site: the elaboration-time
+    // cached instance, the DB's instance map, or the hierarchical parent sub-DB walk-up. The
+    // instance map is queried directly and NOT via `appliedValRefOpt`, whose `isTop` gate reads
+    // the owner's `ownerRef` — empty for every design block under the hierarchical model (and in
+    // DBs flattened from it), so the gate misfires there; the map itself is correct in every DB
+    // model, and the elaboration root safely resolves to no instance (its entry is `top -> Nil`).
+    // The walk-up via `parentSubDBOpt` evaluates the `paramMap` entry in the parent sub-DB's
+    // getSet, whose refTable owns the ref. `None` exactly when no instantiation site exists: the
+    // design is the elaboration root (its parameters are the free variables of the compilation),
+    // or meta-programming with no cached instance. Never falls back to the construction-time
+    // snapshot or the default value, so callers can rely on `None` to keep root parameters
+    // symbolic.
+    protected[compiler] def instAppliedConstDataOpt(using
+        getSet: MemberGetSet,
+        policy: ConstData.CachePolicy
+    ): Option[ConstData[Any]] =
+      val ownerDesign = getOwnerDesign
+      val instOpt =
+        if (getSet.isMutable) ownerDesign.getCachedDesignInstOpt
+        else getSet.designDB.designBlockInstMap.get(ownerDesign).flatMap(_.headOption)
+      instOpt.flatMap(_.paramMap.get(getName)) match
+        case Some(paramRef)            => Some(paramRef.get.getConstData[Any](using getSet, policy))
+        case None if !getSet.isMutable =>
+          val paramName = getName
+          getSet.designDB.parentSubDBOpt.flatMap { parentSubDB =>
+            parentSubDB.atGetSet {
+              parentSubDB.members.collectFirst {
+                case inst: DFDesignInst if inst.getDesignBlock eq ownerDesign => inst
+              }.flatMap(_.paramMap.get(paramName)).map { paramRef =>
+                paramRef.get.getConstData[Any](using parentSubDB.getSet, policy)
+              }
+            }
+          }
+        case None => None
+    end instAppliedConstDataOpt
     protected def protIsFullyAnonymous(using MemberGetSet): Boolean = false
     protected def protGetConstData(using
         getSet: MemberGetSet,
@@ -558,33 +609,13 @@ object DFVal:
                       dv.getConstData(using getSet, updatedPolicy)
                     case _ => ConstData.UnknownConst(this)
         else
-          appliedValOpt match
-            case Some(av) => av.getConstData(using getSet, updatedPolicy)
-            case None     =>
-              // Under the hierarchical model the owner design's `ownerRef` is
-              // empty, so `appliedValRefOpt` (which gates on `isTop`) never finds
-              // the parent's binding for a non-top design. Walk up via
-              // `parentSubDBOpt` and evaluate the `paramMap` entry in the parent
-              // sub-DB's getSet — its refTable owns the ref. Fall back to the
-              // (possibly synthetic) default value if no parent binding exists.
-              val ownerDesign = getOwnerDesign
-              val paramName = getName
-              val viaParent: Option[ConstData[Any]] =
-                getSet.designDB.parentSubDBOpt.flatMap { parentSubDB =>
-                  parentSubDB.atGetSet {
-                    parentSubDB.members.collectFirst {
-                      case inst: DFDesignInst if inst.getDesignBlock eq ownerDesign => inst
-                    }.flatMap(_.paramMap.get(paramName)).map { paramRef =>
-                      paramRef.get.getConstData[Any](using parentSubDB.getSet, updatedPolicy)
-                    }
-                  }
-                }
-              viaParent.getOrElse {
-                defaultValRef.get match
-                  case dv: DFVal => dv.getConstData(using getSet, updatedPolicy)
-                  case _         => ConstData.NotConst
-              }
-          end match
+          // Resolve through the instantiation site; fall back to the (possibly
+          // synthetic) default value if no binding exists.
+          instAppliedConstDataOpt(using getSet, updatedPolicy).getOrElse {
+            defaultValRef.get match
+              case dv: DFVal => dv.getConstData(using getSet, updatedPolicy)
+              case _         => ConstData.NotConst
+          }
         end if
       else ConstData.UnknownConst(this)
     protected def `prot_=~`(that: DFMember)(using MemberGetSet): Boolean = that match
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFRef.scala b/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFRef.scala
index 7e91791fe..28623ac71 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFRef.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/ir/DFRef.scala
@@ -168,7 +168,14 @@ object IntParamRef:
     // Returns `None` when the unknown parts don't cancel.
     // Symbolic equivalence is decided by `IntExprCalc`, so e.g. `2 * W`
     // matches `W + W` and `max(W, W + 1)` matches `W + 1`.
-    def compare(that: IntParamRef)(func: (Int, Int) => Boolean)(using
+    // With `elimSymbolicMaxMin`, a mixed max/min additionally reduces to its
+    // constant operands (`max(W, 16)` reads as `16`), so a width-fit decision
+    // such as `16 >= max(W, 16)` answers definitively; this deliberately
+    // discards the symbolic case, so it is only for check sites that accept
+    // by that rule, never for equality/similarity (see `IntExprCalc.constDiff`).
+    def compare(that: IntParamRef, elimSymbolicMaxMin: Boolean = false)(
+        func: (Int, Int) => Boolean
+    )(using
         MemberGetSet
     ): Option[Boolean] =
       (intParamRef, that) match
@@ -184,7 +191,12 @@ object IntParamRef:
           for
             lVal <- asDFVal(intParamRef)
             rVal <- asDFVal(that)
-            diff <- IntExprCalc.constDiff(lVal, rVal, resolveDesignParams = true)
+            diff <- IntExprCalc.constDiff(
+              lVal,
+              rVal,
+              resolveDesignParams = true,
+              elimSymbolicMaxMin
+            )
           yield func(diff, 0)
     end compare
   end extension
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/ir/IntExprCalc.scala b/compiler/ir/src/main/scala/dfhdl/compiler/ir/IntExprCalc.scala
index d18900a65..2ae24ae2a 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/ir/IntExprCalc.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/ir/IntExprCalc.scala
@@ -1,4 +1,5 @@
 package dfhdl.compiler.ir
+import dfhdl.compiler.analysis.stripTypePreservingAliases
 import scala.collection.mutable
 import DFVal.Func.Op as FuncOp
 
@@ -21,13 +22,127 @@ object IntExprCalc:
 
   /** Decomposes `v` into its linear form. */
   def linearOf(v: DFVal, resolveDesignParams: Boolean)(using MemberGetSet): Linear =
-    Calc(resolveDesignParams).linear(v)
+    Calc(if (resolveDesignParams) ParamResolve.AppliedExpr else ParamResolve.Opaque).linear(v)
 
-  /** If `a - b` reduces to a constant (all symbolic terms cancel), returns it. */
-  def constDiff(a: DFVal, b: DFVal, resolveDesignParams: Boolean)(using
+  /** If `a - b` reduces to a constant (all symbolic terms cancel), returns it.
+    *
+    * With `elimSymbolicMaxMin` enabled, a `max`/`min` whose operands are partly symbolic and partly
+    * constant additionally reduces to its constant operands, ELIMINATING the symbolic dependency:
+    * `max(W, 16)` reads as `16`. This is a deliberate semantic choice for width-fit decisions (a
+    * comparison such as `16 >= max(W, 16)` then decides as `16 >= 16`), not an equivalence: never
+    * enable it for equality/similarity queries (`=~`, `isSimilarTo`), where `max(W, 16)` and `16`
+    * must stay distinct.
+    */
+  def constDiff(
+      a: DFVal,
+      b: DFVal,
+      resolveDesignParams: Boolean,
+      elimSymbolicMaxMin: Boolean = false
+  )(using
       MemberGetSet
   ): Option[Int] =
-    Calc(resolveDesignParams).constDiff(a, b)
+    Calc(
+      if (resolveDesignParams) ParamResolve.AppliedExpr else ParamResolve.Opaque,
+      elimSymbolicMaxMin
+    ).constDiff(a, b)
+
+  /** How the calculus treats a [[DFVal.DesignParam]] it reaches. */
+  private enum ParamResolve derives CanEqual:
+    /** Stays an opaque base, so a decision holds for any parameter assignment (elaboration-time
+      * folding, `SimplifyFunc`).
+      */
+    case Opaque
+
+    /** Substituted by the applied/default value EXPRESSION for non-top designs
+      * (`appliedOrDefaultVal`). Correct only under a getSet where the instantiation site is
+      * resolvable (the flat DB); used by post-elaboration width equivalence
+      * (`IntParamRef.compare`).
+      */
+    case AppliedExpr
+
+    /** Folded to the applied constant DATA, resolved only through an instantiation site
+      * (`DesignParam.instAppliedConstDataOpt`), which works under any getSet (elaboration-time
+      * cached instance, hierarchical sub-DB walk-up, or flat DB). A parameter with no instantiation
+      * site (the elaboration root's own parameters, overridable in the generated HDL) or one that
+      * does not fold to a constant stays an opaque base, so any decision made with this mode holds
+      * for every assignment of the root parameters. Used by the slice calculus ([[DataCalc]]).
+      */
+    case AppliedData
+  end ParamResolve
+
+  /** Linear calculus over slice bounds (parameter-dependent bit-range endpoints), used by
+    * [[DFMember.departial]] and the connectivity slice-overlap analysis. See
+    * [[ParamResolve.AppliedData]] for the design-parameter resolution semantics.
+    */
+  object DataCalc:
+    private def calc(using MemberGetSet): Calc = Calc(ParamResolve.AppliedData)
+    def const(i: Int): Linear = Linear(Nil, i)
+    def isConst(l: Linear): Boolean = l.terms.isEmpty
+    def linearOfVal(v: DFVal)(using MemberGetSet): Linear = calc.linear(v)
+    def linearOfParamRef(ref: IntParamRef)(using MemberGetSet): Linear =
+      ref.getRef match
+        case Some(typeRef) => linearOfVal(typeRef.get)
+        case None          => const(ref.getIntUNSAFE)
+    def add(a: Linear, b: Linear)(using MemberGetSet): Linear = calc.add(a, b)
+    def sub(a: Linear, b: Linear)(using MemberGetSet): Linear = calc.add(a, negate(b))
+    def negate(l: Linear): Linear = Linear(l.terms.map((c, b) => (-c, b)), -l.offset)
+    def addConst(l: Linear, k: Int): Linear = l.copy(offset = l.offset + k)
+    def scale(l: Linear, k: Int): Linear =
+      if (k == 0) Linear(Nil, 0)
+      else Linear(l.terms.map((c, b) => (c * k, b)), l.offset * k)
+
+    /** Product of two linear forms; defined only when at least one side is a constant. */
+    def mulOpt(a: Linear, b: Linear): Option[Linear] =
+      if (a.terms.isEmpty) Some(scale(b, a.offset))
+      else if (b.terms.isEmpty) Some(scale(a, b.offset))
+      else None
+
+    /** Total bit width of a type as a linear form, when expressible. */
+    def linearOfTypeWidth(t: DFType)(using MemberGetSet): Option[Linear] =
+      t.widthIntOpt match
+        case Some(w) => Some(const(w))
+        case None    =>
+          t match
+            case DFBits(widthParamRef) => Some(linearOfParamRef(widthParamRef))
+            case dec: DFDecimal        =>
+              Some(addConst(linearOfParamRef(dec.magnitudeWidthParamRef), dec.fractionWidth))
+            case vec: DFVector =>
+              vec.cellDimParamRefs.foldLeft(linearOfTypeWidth(vec.cellType)) { (accOpt, dim) =>
+                accOpt.flatMap(mulOpt(_, linearOfParamRef(dim)))
+              }
+            case opaque: DFOpaque => linearOfTypeWidth(opaque.actualType)
+            case _                => None
+
+    /** Proves `e >= 0` for every valid parameter assignment. Each fact in `facts` is a linear form
+      * known to be `>= 1` on the valid domain (slice widths: a slice of zero or negative width is
+      * never a valid elaboration). Two proof rules: a constant `e` decides directly, and a
+      * single-fact proportional bound: if `e == λ*f + c` with rational `λ >= 0`, then
+      * `e >= λ*1 + c`, so `λ + c >= 0` proves it. This covers the equal-bin pattern (`k*W`-based
+      * slices of width `W`) at any distance.
+      */
+    def proveNonNeg(e: Linear, facts: List[Linear])(using MemberGetSet): Boolean =
+      if (e.terms.isEmpty) e.offset >= 0
+      else
+        val c = calc
+        facts.exists { f =>
+          f.terms.nonEmpty && f.terms.length == e.terms.length && {
+            // pair each e-term with its baseEq f-term and derive λ = p/q from the first pair
+            val paired = e.terms.map { (ce, be) =>
+              f.terms.collectFirst { case (cf, bf) if c.baseEq(be, bf) => (ce, cf) }
+            }
+            paired.forall(_.nonEmpty) && {
+              val pairs = paired.flatten
+              val (p0, q0) = pairs.head
+              // normalize the denominator positive; λ >= 0 then requires p >= 0
+              val (p, q) = if (q0 < 0) (-p0, -q0) else (p0, q0)
+              p >= 0 &&
+              pairs.forall((ce, cf) => ce * q == cf * p) &&
+              // λ + c >= 0 with c = e.offset - λ*f.offset, scaled by q > 0
+              p + q * e.offset - p * f.offset >= 0
+            }
+          }
+        }
+  end DataCalc
 
   private object ConstInt:
     def unapply(v: DFVal): Option[Int] = v match
@@ -37,21 +152,23 @@ object IntExprCalc:
           case _               => None
       case _ => None
 
-  private final class Calc(resolveDesignParams: Boolean)(using MemberGetSet):
-    // Strip type-preserving AsIs wrappers and, when `resolveDesignParams` is
-    // enabled, DesignParams whose owner design has a parent (i.e., is not the
-    // top design). For non-top designs, the parameter was provided by the
-    // instantiating parent, so resolve it via `appliedOrDefaultVal`. Params on
-    // a top design have no parent and stay opaque: they are the symbolic free
-    // variables exposed to the user at elaboration time. Elaboration-time
-    // folding (SimplifyFunc) disables the resolution so its decisions hold for
-    // any parameter assignment and designs stay parametric.
-    private def strip(v: DFVal): DFVal = v match
-      case DFVal.Alias.AsIs(dfType = dt, relValRef = DFRef(relVal)) if dt == relVal.dfType =>
-        strip(relVal)
-      case dp: DFVal.DesignParam if resolveDesignParams && !dp.getOwnerDesign.isTop =>
+  private final class Calc(mode: ParamResolve, elimSymbolicMaxMin: Boolean = false)(using
+      getSet: MemberGetSet
+  ):
+    // Strip type-preserving AsIs wrappers and, under `AppliedExpr`, DesignParams
+    // whose owner design has a parent (i.e., is not the top design). For non-top
+    // designs, the parameter was provided by the instantiating parent, so
+    // resolve it via `appliedOrDefaultVal`. Params on a top design have no
+    // parent and stay opaque: they are the symbolic free variables exposed to
+    // the user at elaboration time. Elaboration-time folding (SimplifyFunc)
+    // disables the resolution (`Opaque`) so its decisions hold for any parameter
+    // assignment and designs stay parametric. `AppliedData` resolves in `linear`
+    // at the data level instead (see ParamResolve).
+    private def strip(v: DFVal): DFVal = v.stripTypePreservingAliases match
+      case dp: DFVal.DesignParam
+          if mode == ParamResolve.AppliedExpr && !dp.getOwnerDesign.isTop =>
         strip(dp.appliedOrDefaultVal)
-      case _ => v
+      case stripped => stripped
 
     // Ops whose operand order is irrelevant when comparing opaque bases.
     // Additive ops never reach the generic Func comparison (they are always
@@ -62,7 +179,7 @@ object IntExprCalc:
     // (each arg compared through its full linear form, so `clog2(2 * W)`
     // matches `clog2(W + W)`), or `=~` leaves after stripping. Commutative
     // ops compare their args as multisets, so `v1 * v2` matches `v2 * v1`.
-    private def baseEq(a: DFVal, b: DFVal): Boolean =
+    def baseEq(a: DFVal, b: DFVal): Boolean =
       (strip(a), strip(b)) match
         case (af: DFVal.Func, bf: DFVal.Func) if af.op == bf.op && af.dfType =~ bf.dfType =>
           if (af.op == FuncOp.`*`)
@@ -116,7 +233,7 @@ object IntExprCalc:
       }
       merged.filter(_._1 != 0).toList
 
-    private def add(l: Linear, r: Linear): Linear =
+    def add(l: Linear, r: Linear): Linear =
       Linear(canonical(l.terms ++ r.terms), l.offset + r.offset)
     private def negate(l: Linear): Linear =
       Linear(l.terms.map((c, b) => (-c, b)), -l.offset)
@@ -155,6 +272,13 @@ object IntExprCalc:
           case f :: Nil    => scale(linear(f), c)
           case _ if c == 0 => Linear(Nil, 0)
           case _           => Linear(List((c, sv)), 0)
+      // AppliedData: fold a design parameter to its applied constant data, resolved only
+      // through an instantiation site, so an elaboration root's parameters (which have none)
+      // and anything else unresolvable stay opaque bases
+      case dp: DFVal.DesignParam if mode == ParamResolve.AppliedData =>
+        dp.instAppliedConstDataOpt(using getSet, ConstData.CachePolicy.NoCache) match
+          case Some(ConstData.KnownConst(Some(i: BigInt))) if i.isValidInt => Linear(Nil, i.toInt)
+          case _ => Linear(List((1, dp)), 0)
       case sv @ DFVal.Func(op = op @ (FuncOp.max | FuncOp.min), args = args) =>
         // max/min reduce to a single linear form when all operands share the
         // same symbolic terms and differ only by their constant offsets:
@@ -166,6 +290,11 @@ object IntExprCalc:
         if (linears.tail.forall(sameTerms(_, head)))
           val offsets = linears.map(_.offset)
           Linear(head.terms, if (op == FuncOp.max) offsets.max else offsets.min)
+        // symbolic elimination (see `constDiff`): a mixed max/min reduces to its constant
+        // operands, dropping the symbolic ones, so e.g. `max(W, 16)` reads as `16`
+        else if (elimSymbolicMaxMin && linears.exists(_.terms.isEmpty))
+          val offsets = linears.collect { case Linear(Nil, k) => k }
+          Linear(Nil, if (op == FuncOp.max) offsets.max else offsets.min)
         else Linear(List((1, sv)), 0)
       case sv => Linear(List((1, sv)), 0)
     end linear
diff --git a/compiler/ir/src/main/scala/dfhdl/compiler/ir/SubDesignEntry.scala b/compiler/ir/src/main/scala/dfhdl/compiler/ir/SubDesignEntry.scala
index 17c7fb9b2..122bc3d1f 100644
--- a/compiler/ir/src/main/scala/dfhdl/compiler/ir/SubDesignEntry.scala
+++ b/compiler/ir/src/main/scala/dfhdl/compiler/ir/SubDesignEntry.scala
@@ -22,6 +22,44 @@ final case class SubDesignEntry(
     children: List[(StaticRef, SubDesignRef)]
 ) derives ReadWriter:
 
+  /** SANITY-LEVEL contract check, for tests and debugging only: deliberately NOT evaluated on
+    * the production store/lookup path (an O(members + refs) walk per entry would tax every cache
+    * interaction to defend against states only a DFHDL bug or a dirty dev loop can produce; a
+    * ghost-free elaboration is guaranteed by construction, and stale entries from other DFHDL
+    * builds retire through the code digest's version fold, with `clearDFHDL` covering
+    * uncommitted-edit dev loops).
+    *
+    * Whether this entry's DB is self-contained: every reference a member emits resolves in the
+    * entry's refTable, and every refTable binding's target is (a value-equal copy of) one of the
+    * entry's members.
+    *
+    * The value half is not implied by the key half: elaboration can leave a binding whose target
+    * object was removed from (or revised in) the member list after the binding was made (issue
+    * #449's ghost: `MergeAssocFunc` absorbed an intermediate Func and removed it, and the front end
+    * then bound new refs to it through its still-live handle). Such a ghost is harmless in its own
+    * run, whose refTable still resolves the tokens the ghost emits, but it cannot survive adoption:
+    * token re-minting covers members only, so the ghost keeps emitting the STORING run's tokens,
+    * which resolve against nothing in the loading run. `SanityCheck.refCheck` reports the same
+    * defect ("Ref exists for a removed member") in debug/spec runs.
+    *
+    * Only `getRefs` (the TwoWay refs) and `ownerRef` are required to be bound: the structural
+    * OneWay keys (`DFDesignInst.designRef`, a method call's design key) are deliberately absent
+    * from the refTable and resolve through the design registry instead.
+    *
+    * Consumed by the `ClassDesignCacheSpec` "issue #449" test.
+    */
+  def isSelfContained: Boolean =
+    val memberSet = db.members.toSet
+    val keysClosed = db.members.forall { m =>
+      (m.ownerRef.isInstanceOf[DFRef.Empty] || db.refTable.contains(m.ownerRef)) &&
+      m.getRefs.forall(db.refTable.contains)
+    }
+    keysClosed && db.refTable.valuesIterator.forall {
+      case _: DFMember.Empty => true
+      case t                 => memberSet.contains(t)
+    }
+  end isSelfContained
+
   /** This entry's design as a design of the LOADING run.
     *
     * A stored ref token means nothing to this run. The storing run minted it from its own
diff --git a/compiler/stages/src/main/scala/dfhdl/compiler/stages/DropUnreferenced.scala b/compiler/stages/src/main/scala/dfhdl/compiler/stages/DropUnreferenced.scala
index 3f908f7db..896e19b90 100644
--- a/compiler/stages/src/main/scala/dfhdl/compiler/stages/DropUnreferenced.scala
+++ b/compiler/stages/src/main/scala/dfhdl/compiler/stages/DropUnreferenced.scala
@@ -24,18 +24,13 @@ case object DropUnreferencedAnons extends HierarchyStage, NoCheckStage:
   def dependencies: List[Stage] = List()
   def nullifies: Set[Stage] = Set()
   @tailrec private def loop(rootDB: DB)(using MemberGetSet, RefGen): DB =
+    // the kind-level criteria (which members may be dropped and which are always kept) are the
+    // shared `isDroppableIfUnread` predicate, so this stage and elaboration's end-of-design
+    // sweep (`DesignContext.sweepUnreadAnons`) can never drift; only the "is it read" question
+    // differs (here: origin tracking on the immutable DB)
     val patchList = subDB.members.flatMap {
-      // skipping over conditional headers that can be considered values as well.
-      case _: DFConditional.Header => None
-      // idents are always kept
-      case Ident(_) => None
-      // a procedural (Unit-return) method call is a statement: referenced by nothing,
-      // dropped by nothing
-      case DFVal.Func.Call(call, _) if call.dfType =~ DFUnit    => None
-      case m: DFVal if m.isAnonymous && m.originMembers.isEmpty =>
-        Some(m -> Patch.Remove())
-      case m: DFRange if m.originMembers.isEmpty => Some(m -> Patch.Remove())
-      case _                                     => None
+      case m if m.isDroppableIfUnread && m.originMembers.isEmpty => Some(m -> Patch.Remove())
+      case _                                                     => None
     }
     if (patchList.isEmpty) subDB
     else
diff --git a/compiler/stages/src/main/scala/dfhdl/compiler/stages/NamedAliases.scala b/compiler/stages/src/main/scala/dfhdl/compiler/stages/NamedAliases.scala
index 0e4f323fe..0d3e89034 100644
--- a/compiler/stages/src/main/scala/dfhdl/compiler/stages/NamedAliases.scala
+++ b/compiler/stages/src/main/scala/dfhdl/compiler/stages/NamedAliases.scala
@@ -142,6 +142,13 @@ end NamedAliases
 case object NamedVerilogSelection extends NamedAliases:
   override def runCondition(using co: CompilerOptions): Boolean = co.backend.isVerilog
   private val carryOps = Set(FuncOp.`*`, FuncOp.+, FuncOp.-)
+  // A carry-widened unsigned func: its width exceeds its first operand's, so its printed
+  // Verilog form relies on consumer context to evaluate at the full width.
+  private def isCarryWidenedUInt(func: DFVal.Func)(using MemberGetSet): Boolean =
+    carryOps.contains(func.op) &&
+      (func.dfType match
+        case DFUInt(_) => !func.dfType.isSimilarTo(func.args.head.get.dfType)
+        case _         => false)
   extension (dfVal: DFVal)(using MemberGetSet)
     def hasVerilogName: Boolean =
       dfVal match
@@ -170,6 +177,15 @@ case object NamedVerilogSelection extends NamedAliases:
       case alias: DFVal.Alias.ApplyRange
           if alias.compareWidths(alias.relValRef.get)(_ != _).getOrElse(true) =>
         List(alias.relValRef.get)
+      // A carry-widened func (its width exceeds its operands') consumed by an
+      // unsigned-to-signed conversion must be named: the conversion prints as a
+      // `{1'b0, ...}` concatenation, whose operands are self-determined in Verilog, so
+      // an inline func would evaluate at its narrow operand width and truncate ahead of
+      // the sign extension. A named value's self-determined width is its declared width,
+      // which carries the widening through the concat.
+      case DFVal.Alias.AsIs(dfType = DFSInt(_), relValRef = DFRef(relVal: DFVal.Func))
+          if isCarryWidenedUInt(relVal) =>
+        List(relVal)
       case alias @ DFVal.Alias.AsIs(
             dfType = _: (DFDecimal | DFBits),
             relValRef = DFRef(relVal @ (DFBits.Val(_) | DFDecimal.Val(_)))
diff --git a/compiler/stages/src/test/scala/StagesSpec/ClassDesignCacheSpec.scala b/compiler/stages/src/test/scala/StagesSpec/ClassDesignCacheSpec.scala
index f0ea2b3f1..52525e4a8 100644
--- a/compiler/stages/src/test/scala/StagesSpec/ClassDesignCacheSpec.scala
+++ b/compiler/stages/src/test/scala/StagesSpec/ClassDesignCacheSpec.scala
@@ -2,6 +2,8 @@ package StagesSpec
 
 import dfhdl.*
 import dfhdl.compiler.ir
+import dfhdl.compiler.analysis.isDroppableIfUnread
+import dfhdl.compiler.printing.DefaultPrinter
 import dfhdl.core.{DFC, SubDesignCache}
 // scalafmt: { align.tokens = [{code = "<>"}, {code = "="}, {code = "=>"}, {code = ":="}]}
 
@@ -202,4 +204,65 @@ class ClassDesignCacheSpec extends StageSpec:
     assertCodeString(genParamHost(using cachedDFC(cache)), expectedParamCodeString)
     assertEquals(ClassBodyElaborations.count, 0)
   }
+
+  // ~~~ issue #449: a parametric slice whose offset expression is absorbed by index arithmetic ~~~
+  // Building the slice's high index absorbs the offset `+` Func (`SimplifyFunc.MergeAssocFunc`)
+  // BEFORE `lsbitsAt` binds its own refs to it. The absorbed Func must come back as a member
+  // (resurrectable removal) rather than stay a removed-member ghost among the refTable values:
+  // a ghost is harmless in its own run, whose refTable still resolves the tokens it emits, but
+  // cache adoption re-mints tokens for members only, so a ghost's tokens dangle in the loading
+  // run and the first ref resolution through it crashes.
+  def genSliceHost(using DFC): dfhdl.core.Design =
+    class SliceChild(
+        val W: Int <> CONST    = 11,
+        val BINS: Int <> CONST = 9
+    ) extends EDDesign:
+      val v = Bits(W * BINS) <> VAR
+      val o = Bits(W)        <> VAR
+      v <> all(0)
+      process(all):
+        for (i <- 0 until BINS)
+          o := v.lsbitsAt(i * W + 1, W)
+    end SliceChild
+    class SliceHost extends EDDesign:
+      val WIDTH: Int <> CONST = 4
+      val child               = SliceChild(W = WIDTH, BINS = 3)
+    new SliceHost
+  end genSliceHost
+
+  // Issue #449 regression: the `isSelfContained` assert is the entry contract's only
+  // enforcement point (a test-level sanity check, deliberately kept off the production
+  // store/lookup path), and the debris assert pins the end-of-design sweep: superseded
+  // simplification intermediates never reach a stored entry.
+  test("issue #449: a cached child with an absorbed slice-offset Func round-trips") {
+    val cache    = new MapSubDesignCache
+    val liveFlat = genSliceHost(using liveDFC).getDB.newToOld
+    val liveCS   =
+      import liveFlat.getSet
+      DefaultPrinter.csDB
+    // the first elaboration runs live; the stored entry must be self-contained (the absorbed
+    // offset Func stays a member since the slice reads it, no ghost refTable value) and
+    // debris-free (unread simplification leftovers swept at the end of the design)
+    genSliceHost(using cachedDFC(cache))
+    assertEquals(cache.entries.size, 1)
+    assert(cache.entries.values.forall { json =>
+      val entry             = ir.SubDesignEntry.fromJsonString(json)
+      given ir.MemberGetSet = entry.db.getSet
+      val readTargets       =
+        entry.db.members.view.flatMap(_.getRefs).flatMap(entry.db.refTable.get).toSet
+      entry.isSelfContained && entry.db.members.forall(m =>
+        !m.isDroppableIfUnread || readTargets.contains(m)
+      )
+    })
+    // the second elaboration adopts the entry; every ref in the flat view must resolve,
+    // and the design must print exactly as the live one
+    val cachedFlat = genSliceHost(using cachedDFC(cache)).getDB.newToOld
+    cachedFlat.check
+    assertEquals(cache.hits, 1)
+    val cachedCS =
+      import cachedFlat.getSet
+      DefaultPrinter.csDB
+    assertNoDiff(cachedCS, liveCS)
+  }
+
 end ClassDesignCacheSpec
diff --git a/compiler/stages/src/test/scala/StagesSpec/NamedSelectionSpec.scala b/compiler/stages/src/test/scala/StagesSpec/NamedSelectionSpec.scala
index 22d1f5578..5c18249a5 100644
--- a/compiler/stages/src/test/scala/StagesSpec/NamedSelectionSpec.scala
+++ b/compiler/stages/src/test/scala/StagesSpec/NamedSelectionSpec.scala
@@ -262,4 +262,28 @@ class NamedSelectionSpec extends StageSpec(stageCreatesUnrefAnons = true):
          |""".stripMargin
     )
   }
+  // a carry-widened func consumed by an unsigned-to-signed conversion is named, so the
+  // Verilog `{1'b0, ...}` sign-extension concat (whose operands are self-determined)
+  // sees a declared identifier instead of an inline func pinned at its narrow operand
+  // width (issue #452)
+  test("Sign-converted carry func is named") {
+    class SignedCarry extends EDDesign:
+      val a = UInt(8)  <> IN
+      val b = UInt(8)  <> IN
+      val o = SInt(10) <> OUT
+      o <> (a +^ b).signed
+
+    val id = (new SignedCarry).verilogNamedSelection
+    assertCodeString(
+      id,
+      """|class SignedCarry extends EDDesign:
+         |  val a = UInt(8) <> IN
+         |  val b = UInt(8) <> IN
+         |  val o = SInt(10) <> OUT
+         |  val o_part = a +^ b
+         |  o <> o_part.signed
+         |end SignedCarry
+         |""".stripMargin
+    )
+  }
 end NamedSelectionSpec
diff --git a/compiler/stages/src/test/scala/StagesSpec/PrintCodeStringSpec.scala b/compiler/stages/src/test/scala/StagesSpec/PrintCodeStringSpec.scala
index d26ffe558..e0a2edf34 100644
--- a/compiler/stages/src/test/scala/StagesSpec/PrintCodeStringSpec.scala
+++ b/compiler/stages/src/test/scala/StagesSpec/PrintCodeStringSpec.scala
@@ -2222,7 +2222,8 @@ class PrintCodeStringSpec extends StageSpec(stageCreatesUnrefAnons = true):
          |
          |class Foo extends RTDesign:
          |  val i = SInt(w) <> IN
-         |  val p2: Int <> CONST = p0 + 1
+         |  val p1: Int <> CONST = p0
+         |  val p2: Int <> CONST = p1 + 1
          |  val p3: Int <> CONST = p2 + (-1)
          |  val p4: Int <> CONST = p3 + 3
          |  val p5: Int <> CONST = p4 - 3
diff --git a/compiler/stages/src/test/scala/StagesSpec/PrintVerilogCodeSpec.scala b/compiler/stages/src/test/scala/StagesSpec/PrintVerilogCodeSpec.scala
index 718dbf93c..15059c17e 100644
--- a/compiler/stages/src/test/scala/StagesSpec/PrintVerilogCodeSpec.scala
+++ b/compiler/stages/src/test/scala/StagesSpec/PrintVerilogCodeSpec.scala
@@ -3262,4 +3262,46 @@ class PrintVerilogCodeSpec extends StageSpec:
          |""".stripMargin
     )
   }
+  // a carry-widened func under a sign conversion is hoisted to a named variable by
+  // `NamedVerilogSelection`: a concat operand is self-determined in Verilog, so an
+  // inline func inside the `$signed({1'b0, ...})` sign extension would be evaluated at
+  // its narrow operand width and truncate; the named variable's assignment provides the
+  // widening context and the concat sees a declared identifier (issue #452)
+  test("sign-converted carry func is named ahead of the concat") {
+    class SignedCarry extends EDDesign:
+      val a = UInt(2)  <> IN
+      val b = UInt(8)  <> IN
+      val c = UInt(8)  <> IN
+      val o = SInt(8)  <> OUT
+      val q = SInt(10) <> OUT
+      process(all):
+        o := sd"8'0" - 3 * a
+        q := (b +^ c).signed
+    val top = (new SignedCarry).getCompiledCodeString
+    assertNoDiff(
+      top,
+      """|`default_nettype none
+         |`timescale 1ns/1ps
+         |
+         |module SignedCarry(
+         |  input  wire logic [1:0] a,
+         |  input  wire logic [7:0] b,
+         |  input  wire logic [7:0] c,
+         |  output logic signed [7:0] o,
+         |  output logic signed [9:0] q
+         |);
+         |  `include "dfhdl_defs.svh"
+         |  logic [3:0] o_part;
+         |  logic [8:0] q_part;
+         |  always_comb
+         |  begin
+         |    o_part = 2'd3 * a;
+         |    o = 8'sd0 - 8'($signed({1'b0, o_part}));
+         |    q_part = b + c;
+         |    q = $signed({1'b0, q_part});
+         |  end
+         |endmodule
+         |""".stripMargin
+    )
+  }
 end PrintVerilogCodeSpec
diff --git a/core/src/main/scala/dfhdl/core/DFBits.scala b/core/src/main/scala/dfhdl/core/DFBits.scala
index a3e4b5dbe..16fa534c7 100644
--- a/core/src/main/scala/dfhdl/core/DFBits.scala
+++ b/core/src/main/scala/dfhdl/core/DFBits.scala
@@ -487,7 +487,7 @@ object DFBits:
               case _                    =>
                 if (dfType.compareWidths(dfVal.dfType)(_ != _).getOrElse(true))
                   throw new IllegalArgumentException(
-                    s"""|The argument width (${dfVal.dfType.widthCodeString}) is different than the receiver width (${dfType.widthCodeString}).
+                    s"""|The argument width (${dfVal.dfType.widthErrorString}) is different than the receiver width (${dfType.widthErrorString}).
                         |Consider applying `.resize` to resolve this issue.""".stripMargin
                   )
             dfVal.nameInDFCPosition.asValTP[DFBits[LW], RP]
@@ -536,9 +536,9 @@ object DFBits:
             case _                    =>
               if (dfType.compareWidths(dfValArg.dfType)(_ != _).getOrElse(true))
                 val lhsStr =
-                  if (castling) dfValArg.dfType.widthCodeString else dfType.widthCodeString
+                  if (castling) dfValArg.dfType.widthErrorString else dfType.widthErrorString
                 val rhsStr =
-                  if (castling) dfType.widthCodeString else dfValArg.dfType.widthCodeString
+                  if (castling) dfType.widthErrorString else dfValArg.dfType.widthErrorString
                 throw new IllegalArgumentException(
                   s"""|Cannot apply this operation between a value of $lhsStr bits width (LHS) and a value of $rhsStr bits width (RHS).
                       |An explicit conversion must be applied.""".stripMargin
@@ -763,8 +763,8 @@ object DFBits:
         def repeat[N <: IntP](num: IntParam[N])(using
             dfc: DFCG,
             check: Arg.Positive.CheckNUB[N]
-          // `LW`, not the equivalent `icL.OutW`: a path-dependent type reads as non-constant to
-          // the `IsConst` guard and would collapse the width (see `IntP.IsConstInt2`)
+            // `LW`, not the equivalent `icL.OutW`: a path-dependent type reads as non-constant to
+            // the `IsConst` guard and would collapse the width (see `IntP.IsConstInt2`)
         ): DFValTP[DFBits[IntP.*[LW, N]], icL.OutP | CONST] = trydf {
           val lhsVal = icL(lhs)
           num.toScalaIntOpt.foreach(check(_))
diff --git a/core/src/main/scala/dfhdl/core/DFBoolOrBit.scala b/core/src/main/scala/dfhdl/core/DFBoolOrBit.scala
index 9ce021734..32083c4c9 100644
--- a/core/src/main/scala/dfhdl/core/DFBoolOrBit.scala
+++ b/core/src/main/scala/dfhdl/core/DFBoolOrBit.scala
@@ -4,6 +4,7 @@ import ir.DFVal.Func.Op as FuncOp
 import dfhdl.internals.*
 
 import annotation.{implicitNotFound, targetName}
+import scala.util.NotGiven
 
 type BitNum = 0 | 1
 type BitOrBool = BitNum | Boolean
@@ -199,55 +200,137 @@ object DFBoolOrBit:
         @targetName("not2OfDFBool")
         inline def unary_~(using DFCG) = lhs.unary_!
 
+      // Runtime construction for the `sel` operation givens below. The
+      // candidates are by-name so their evaluation (including the TC
+      // conversion of the non-DFHDL candidate and the dfType access, which
+      // throws a derived error for an errored value) happens under `trydf`,
+      // surfacing as a positioned elaboration error instead of an escaping
+      // exception.
+      def selRuntime[OT <: DFTypeAny](
+          cond: DFValOf[DFBoolOrBit],
+          onTrue: => DFValOf[OT],
+          onFalse: => DFValOf[OT]
+      )(using dfc: DFC): DFValOf[OT] =
+        trydf {
+          val onTrueVal = onTrue
+          val onFalseVal = onFalse
+          DFVal.Func(onTrueVal.dfType, FuncOp.sel, List(cond, onTrueVal, onFalseVal))
+        }(using dfc, CTName("sel"))
+
+      // ~~~ `sel` candidate resolution ~~~
+      // The onTrue candidate type leads, except when onTrue is a DFHDL Int
+      // parameter (DFConstInt32) while onFalse is not, and when neither
+      // candidate is a DFHDL value the selection is deferred through
+      // BoolSelWrapper for an outer context to type. The cases are kept
+      // mutually exclusive via the NotGiven guards, so no given
+      // prioritization is involved.
+      given evSelOnTrueDFVal[
+          CP,
+          L <: DFValTP[DFBoolOrBit, CP],
+          TT <: DFTypeAny,
+          TP,
+          OT <: DFValTP[TT, TP],
+          OF,
+          RP
+      ](using
+          NotGiven[OT <:< DFConstInt32]
+      )(using
+          tc: DFVal.TC[TT, OF] { type OutP = RP }
+      ): ExactOp3Aux[FuncOp.sel.type, DFC, Any, L, OT, OF, DFValTP[TT, CP | TP | RP]] =
+        new ExactOp3[FuncOp.sel.type, DFC, Any, L, OT, OF]:
+          type Out = DFValTP[TT, CP | TP | RP]
+          def apply(lhs: L, mhs: OT, rhs: OF)(using DFC): Out =
+            selRuntime[TT](lhs, mhs, tc(mhs.dfType, rhs)).asValTP[TT, CP | TP | RP]
+      end evSelOnTrueDFVal
+      given evSelBothConstInt32[
+          CP,
+          L <: DFValTP[DFBoolOrBit, CP],
+          OT <: DFConstInt32,
+          OF <: DFConstInt32
+      ]: ExactOp3Aux[FuncOp.sel.type, DFC, Any, L, OT, OF, DFValTP[DFInt32, CP | CONST]] =
+        new ExactOp3[FuncOp.sel.type, DFC, Any, L, OT, OF]:
+          type Out = DFValTP[DFInt32, CP | CONST]
+          def apply(lhs: L, mhs: OT, rhs: OF)(using DFC): Out =
+            selRuntime[DFInt32](lhs, mhs, rhs).asValTP[DFInt32, CP | CONST]
+      end evSelBothConstInt32
+      given evSelOnFalseDFValFlip[
+          CP,
+          L <: DFValTP[DFBoolOrBit, CP],
+          OT <: DFConstInt32,
+          FT <: DFTypeAny,
+          FP,
+          OF <: DFValTP[FT, FP],
+          RP
+      ](using
+          NotGiven[OF <:< DFConstInt32]
+      )(using
+          tc: DFVal.TC[FT, OT] { type OutP = RP }
+      ): ExactOp3Aux[FuncOp.sel.type, DFC, Any, L, OT, OF, DFValTP[FT, CP | FP | RP]] =
+        new ExactOp3[FuncOp.sel.type, DFC, Any, L, OT, OF]:
+          type Out = DFValTP[FT, CP | FP | RP]
+          def apply(lhs: L, mhs: OT, rhs: OF)(using DFC): Out =
+            selRuntime[FT](lhs, tc(rhs.dfType, mhs), rhs).asValTP[FT, CP | FP | RP]
+      end evSelOnFalseDFValFlip
+      given evSelOnFalseDFVal[
+          CP,
+          L <: DFValTP[DFBoolOrBit, CP],
+          OT,
+          FT <: DFTypeAny,
+          FP,
+          OF <: DFValTP[FT, FP],
+          RP
+      ](using
+          NotGiven[OT <:< DFValAny]
+      )(using
+          tc: DFVal.TC[FT, OT] { type OutP = RP }
+      ): ExactOp3Aux[FuncOp.sel.type, DFC, Any, L, OT, OF, DFValTP[FT, CP | FP | RP]] =
+        new ExactOp3[FuncOp.sel.type, DFC, Any, L, OT, OF]:
+          type Out = DFValTP[FT, CP | FP | RP]
+          def apply(lhs: L, mhs: OT, rhs: OF)(using DFC): Out =
+            selRuntime[FT](lhs, tc(rhs.dfType, mhs), rhs).asValTP[FT, CP | FP | RP]
+      end evSelOnFalseDFVal
+      given evSelWrapperInt32[
+          CP,
+          L <: DFValTP[DFBoolOrBit, CP],
+          OT <: DFConstInt32,
+          OF
+      ](using
+          NotGiven[OF <:< DFValAny]
+      ): ExactOp3Aux[FuncOp.sel.type, DFC, Any, L, OT, OF, BoolSelWrapper[CP, OT, OF]] =
+        new ExactOp3[FuncOp.sel.type, DFC, Any, L, OT, OF]:
+          type Out = BoolSelWrapper[CP, OT, OF]
+          def apply(lhs: L, mhs: OT, rhs: OF)(using DFC): Out =
+            BoolSelWrapper[CP, OT, OF](lhs, mhs, rhs)
+      end evSelWrapperInt32
+      given evSelWrapper[
+          CP,
+          L <: DFValTP[DFBoolOrBit, CP],
+          OT,
+          OF
+      ](using
+          NotGiven[OT <:< DFValAny],
+          NotGiven[OF <:< DFValAny]
+      ): ExactOp3Aux[FuncOp.sel.type, DFC, Any, L, OT, OF, BoolSelWrapper[CP, OT, OF]] =
+        new ExactOp3[FuncOp.sel.type, DFC, Any, L, OT, OF]:
+          type Out = BoolSelWrapper[CP, OT, OF]
+          def apply(lhs: L, mhs: OT, rhs: OF)(using DFC): Out =
+            BoolSelWrapper[CP, OT, OF](lhs, mhs, rhs)
+      end evSelWrapper
+
       extension [T <: DFBoolOrBit, P](lhs: DFValTP[T, P])
         @targetName("notOfDFBoolOrBit")
         private[core] def not(using DFC): DFValTP[T, P] = trydf {
           DFVal.Func(lhs.dfType, FuncOp.unary_!, List(lhs))
         }
+        // The exactOp3 macro boundary binds all three operands at the user's
+        // call site, so candidate failures are reported at the user's code
+        // (an in-body summon would report inside this file), and the operand
+        // typing goes through exactInfo widening, which also covers the
+        // `unstableSkolemPrefix` concern noted in `DFVal.Ops.<>`.
         transparent inline def sel[OT, OF](inline onTrue: OT, inline onFalse: OF)(using
             dfc: DFCG
         ): Any =
-          inline val onTrueIsDFVal = inline compiletime.erasedValue[OT] match
-            case _: DFValAny => true
-            case _           => false
-          inline val onTrueIsDFConstInt32 = inline compiletime.erasedValue[OT] match
-            case _: DFConstInt32 => true
-            case _               => false
-          inline val onFalseIsDFVal = inline compiletime.erasedValue[OF] match
-            case _: DFValAny => true
-            case _           => false
-          inline val onFalseIsDFConstInt32 = inline compiletime.erasedValue[OF] match
-            case _: DFConstInt32 => true
-            case _               => false
-          // onTrue type has priority, except when onTrue is a DFHDL Int parameter while onFalse is not
-          inline if (onTrueIsDFVal && !(onTrueIsDFConstInt32 && !onFalseIsDFConstInt32))
-            // the branch is taken apart under `OT`, the type the caller inferred for it, and not
-            // under the type it is written with; see the `unstableSkolemPrefix` note in
-            // `DFVal.Ops.<>`
-            inline onTrue.asInstanceOf[OT] match
-              case ___onTrueDFVal: DFValTP[tt, tp] =>
-                val tc = compiletime.summonInline[DFVal.TC[tt, OF]]
-                val dfType = ___onTrueDFVal.dfType
-                inline if (isConstCheck[OF])
-                  DFVal.Func(dfType, FuncOp.sel, List(lhs, ___onTrueDFVal, tc(dfType, onFalse)))
-                    .asValTP[tt, P | tp]
-                else
-                  DFVal.Func(dfType, FuncOp.sel, List(lhs, ___onTrueDFVal, tc(dfType, onFalse)))
-                    .asValOf[tt]
-          else if (onFalseIsDFVal)
-            inline onFalse.asInstanceOf[OF] match
-              case ___onFalseDFVal: DFValTP[ft, fp] =>
-                val tc = compiletime.summonInline[DFVal.TC[ft, OT]]
-                val dfType = ___onFalseDFVal.dfType
-                inline if (isConstCheck[OT])
-                  DFVal.Func(dfType, FuncOp.sel, List(lhs, tc(dfType, onTrue), ___onFalseDFVal))
-                    .asValTP[ft, P | fp]
-                else
-                  DFVal.Func(dfType, FuncOp.sel, List(lhs, tc(dfType, onTrue), ___onFalseDFVal))
-                    .asValOf[ft]
-          else
-            BoolSelWrapper[P, OT, OF](lhs, onTrue, onFalse)
-        end sel
+          exactOp3[FuncOp.sel.type, DFC, Any](lhs, onTrue, onFalse)
       end extension
     end Ops
   end Val
diff --git a/core/src/main/scala/dfhdl/core/DFDecimal.scala b/core/src/main/scala/dfhdl/core/DFDecimal.scala
index 28eb93ec8..1e9740b74 100644
--- a/core/src/main/scala/dfhdl/core/DFDecimal.scala
+++ b/core/src/main/scala/dfhdl/core/DFDecimal.scala
@@ -142,6 +142,17 @@ object DFDecimal:
           [BaW <: Int, WcW <: Int] =>> "The wildcard `Int` value width (" + WcW +
             ") is larger than the bit-accurate value width (" + BaW + ")."
         ]
+    object `!(LN && RN)`
+        extends Check2[
+          Boolean,
+          Boolean,
+          [LN <: Boolean, RN <: Boolean] =>> ![LN && RN],
+          [LN <: Boolean,
+          RN <: Boolean] =>> "Carry operations require at least one bit-accurate operand (`UInt`/`SInt`), but both operands are `Int` values."
+        ]
+    // A carry operation widens relative to a bit-accurate operand, so at least one operand
+    // must be bit-accurate (native `Int` operands are wildcards with no width of their own).
+    type CarryCheck[LN <: NativeType, RN <: NativeType] = `!(LN && RN)`.Check[LN, RN]
     type SignStr[S <: Boolean] = ITE[S, "a signed", "an unsigned"]
     object `LS == RS`
         extends Check2[
@@ -1098,18 +1109,22 @@ object DFXInt:
                 (dfType.widthIntOpt, rhsWidthOpt) match
                   case (Some(dfTypeW), Some(rhsW)) => check(dfType.signed, dfTypeW, rhsSigned, rhsW)
                   case _                           =>
+                    import dfc.getSet
                     if (
                       !dfType.asIR.isDFInt32 && !rhs.dfType.asIR.isDFInt32 &&
                       !DFXInt.Val.Ops.hasImplicitlyFromIntTag(rhs.asIR)
                     )
-                      import dfc.getSet
                       // integer operands (fraction 0): the magnitude ref is the total-width
                       // ref and may be parametric
                       val dfTypeWidthRef = dfType.asIR.magnitudeWidthParamRef
                       val rhsWidthRef = rhs.dfType.asIR.magnitudeWidthParamRef
-                      def dfTypeWidthStr = dfTypeWidthRef.refCodeString
-                      def rhsWidthStr = rhsWidthRef.refCodeString
-                      dfTypeWidthRef.compare(rhsWidthRef)(_ >= _) match
+                      def dfTypeWidthStr = dfTypeWidthRef.refErrorString
+                      def rhsWidthStr = rhsWidthRef.refErrorString
+                      // width-fit acceptance rule: LHS >= RHS after symbolic elimination, so a
+                      // mixed max/min drops its symbolic operands (`16 >= WIDTH max 16` decides
+                      // as `16 >= 16`); a residual plain-symbol comparison stays undecidable
+                      // and is conservatively rejected below
+                      dfTypeWidthRef.compare(rhsWidthRef, elimSymbolicMaxMin = true)(_ >= _) match
                         case Some(false) =>
                           throw new IllegalArgumentException(
                             s"""The applied RHS value width ($rhsWidthStr) is larger than the LHS variable width ($dfTypeWidthStr)."""
@@ -1318,66 +1333,95 @@ object DFXInt:
           val dfValIR =
             if (dfType.asIR.isDFInt32 && lhs.dfType.asIR.isDFInt32) lhs.asIR
             else
-              val lhsSignFix: DFValOf[DFSInt[Int]] =
-                if (!lhs.dfType.asIR.isDFInt32 && dfType.signed && !lhs.dfType.signed)
-                  lhs.asValOf[DFUInt[Int]].signed.asValOf[DFSInt[Int]]
-                else lhs.asValOf[DFSInt[Int]]
-              // Auto-promote anonymous +/-/* to carry when target is wide enough
+              // Auto-promote anonymous +/-/* to carry when the target is wide enough. The
+              // promotion candidate is taken BEFORE any sign conversion: converting first
+              // wraps the func in a `.signed` alias that hides it from the promotion and
+              // pins the chain at its narrow width, which the Verilog backend then emits
+              // as a self-determined concat operand that truncates. An upstream anonymous
+              // sign-conversion alias (the commutative-arith sign alignment creates one)
+              // is unwrapped for the same reason.
               import IntParam.+
-              val funcWidth = lhsSignFix.widthIntParam
+              val signFixNeeded =
+                !lhs.dfType.asIR.isDFInt32 && dfType.signed && !lhs.dfType.signed
+              val (candidateIR, signWrapped) = signConversionRelVal(lhs.asIR) match
+                case Some(relVal) => (relVal, true)
+                case None         => (lhs.asIR, false)
 
-              // if not a constant, optimistically assume it's large enough to allow carry promotion
-              def carryPromoteWidthCheck: Boolean =
-                dfType.asFE[DFSInt[Int]].compareWidths(lhsSignFix.dfType)(_ > _).getOrElse(true)
+              // symbolic elimination keeps this consistent with the width-fit acceptance rule
+              // of the TC conversion: `16 > WIDTH max 16` decides as `16 > 16` (no promotion),
+              // so the anonymous form resolves exactly like a named intermediate value; if
+              // still undecidable, optimistically assume the target is large enough. The
+              // effective width includes the sign bit a later sign conversion adds.
+              def carryPromoteWidthCheck(effWidth: IntParam[Int]): Boolean =
+                dfType.asFE[DFSInt[Int]]
+                  .compareWidths(DFXInt(true, effWidth, BitAccurate), elimSymbolicMaxMin = true)(
+                    _ > _
+                  )
+                  .getOrElse(true)
 
-              val lhsCarryPromo: DFValOf[DFSInt[Int]] = lhsSignFix.asIR match
+              val lhsCarryPromo: DFValOf[DFSInt[Int]] = candidateIR match
                 case func @ ir.DFVal.Func(
                       dfType = dt @ (ir.DFUInt(_) | ir.DFSInt(_)),
                       op = op @ (FuncOp.+ | FuncOp.- | FuncOp.*)
                     )
-                    if func.isAnonymous && carryPromoteWidthCheck =>
-                  // For multi-arg merged Funcs (3+ args), peel the last arg:
-                  // Func(+, [a, b, c]) → Func(+, [Func(+, [a, b]), c])
-                  // Shrink the original func in-place to become the inner (non-carry)
-                  // Func, then add a new binary carry Func at the tail. This keeps
-                  // the inner before the carry Func in member order.
-                  // Skipped during meta-programming where MutableDB ref tracking is limited.
-                  val carryFunc =
+                    if func.isAnonymous && {
+                      val funcWidth: IntParam[Int] = func.asValOf[DFSInt[Int]].widthIntParam
+                      val effWidth =
+                        if (signFixNeeded || signWrapped) funcWidth + 1 else funcWidth
+                      carryPromoteWidthCheck(effWidth)
+                    } =>
+                  val funcWidth: IntParam[Int] = func.asValOf[DFSInt[Int]].widthIntParam
+                  // The carry-promoted Func is BUILT FRESH rather than revised in place (an
+                  // anonymous member is never revised; issue #449); the original Func becomes
+                  // debris for the end-of-design sweep. For multi-arg merged Funcs (3+ args),
+                  // the last arg is peeled: Func(+, [a, b, c]) becomes
+                  // Func(+, [Func(+, [a, b]), c]), with the inner (non-carry) Func added
+                  // before the carry Func so member order holds. The peel is skipped during
+                  // meta-programming, where no member is registered at all (see below).
+                  val carryArgVals: List[ir.DFVal] =
                     if (func.args.length > 2 && !dfc.inMetaProgramming)
-                      val lastArgRef = func.args.last
-                      // Shrink `func` in-place to the inner Func (N-1 args, non-carry)
-                      val innerFunc =
-                        dfc.mutableDB.setMember(func, _.copy(args = func.args.dropRight(1)))
-                      // Add a new binary carry Func at the tail referencing innerFunc
-                      func.copy(args =
-                        List(innerFunc.refTW[ir.DFVal](knownReachable = true), lastArgRef)
+                      val innerFunc = ir.DFVal.Func(
+                        dt,
+                        op,
+                        func.args.dropRight(1).map(_.get.refTW[ir.DFVal](knownReachable = true)),
+                        dfc.ownerOrEmptyRef,
+                        func.meta,
+                        func.tags
                       ).addMember
-                    else func
-                  // Check B: warn if sub-expressions contain implicit Int with
-                  // narrow non-carry arith. Check args (not func itself, since
-                  // the func is about to be carry-promoted).
-                  val argHasImplicitFromIntTag =
-                    carryFunc.args.exists(ref => hasImplicitlyFromIntTag(ref.get))
-                  val argsContainNarrowNonCarryArith =
-                    carryFunc.args.exists(ref => containsNarrowNonCarryArith(ref.get))
-                  val argsContainNarrowNonCarryArithWithTaggedOperand = carryFunc.args.exists(ref =>
-                    containsNarrowNonCarryArithWithTaggedOperand(ref.get)
-                  )
-                  if argHasImplicitFromIntTag && argsContainNarrowNonCarryArith ||
-                    argsContainNarrowNonCarryArithWithTaggedOperand
-                  then
-                    dfc.logEvent(DFWarning(op.toString, verilogSemanticsWarnMsg))
-                  end if
-                  val cw: IntParam[Int] = carryFunc.op.runtimeChecked match
+                      List(innerFunc, func.args.last.get)
+                    else func.args.map(_.get)
+                  // No Verilog-semantics warning for this shape: the promoted chain is
+                  // emitted under the target's width context (a size cast or the
+                  // assignment itself), and truncation to N bits commutes with +/-/*,
+                  // so Verilog's 32-bit evaluation agrees for every input (issue #453).
+                  val cw: IntParam[Int] = op.runtimeChecked match
                     case FuncOp.+ | FuncOp.- => funcWidth + 1
                     case FuncOp.*            => funcWidth + funcWidth
                   // integer carry arithmetic (fraction width 0), so the magnitude width is
                   // the total width
                   val newDT = dt.copy(magnitudeWidthParamRef = cw.ref)
-                  dfc.mutableDB
-                    .setMember(carryFunc, _.updateDFType(newDT))
-                    .asValOf[DFSInt[Int]]
-                case _ => lhsSignFix
+                  val promoted =
+                    if (dfc.inMetaProgramming)
+                      // no MutableDB revision under meta-programming (matching `setMember`'s
+                      // behavior there): the retyped value is returned unregistered
+                      func.updateDFType(newDT).asValOf[DFUInt[Int]]
+                    else
+                      ir.DFVal.Func(
+                        newDT,
+                        op,
+                        carryArgVals.map(_.refTW[ir.DFVal](knownReachable = true)),
+                        dfc.ownerOrEmptyRef,
+                        func.meta,
+                        func.tags
+                      ).addMember.asValOf[DFUInt[Int]]
+                  // the sign conversion is applied to the PROMOTED value, so the widening
+                  // happens before the concat the conversion prints as
+                  if (signFixNeeded || signWrapped) promoted.signed.asValOf[DFSInt[Int]]
+                  else promoted.asValOf[DFSInt[Int]]
+                case _ =>
+                  // no promotion: apply the plain sign fix when the target requires it
+                  if (signFixNeeded) lhs.asValOf[DFUInt[Int]].signed.asValOf[DFSInt[Int]]
+                  else lhs.asValOf[DFSInt[Int]]
               end lhsCarryPromo
               val nativeTypeChanged = dfType.nativeType != lhsCarryPromo.dfType.nativeType
               if (nativeTypeChanged) dfType.asIR.nativeType match
@@ -1433,9 +1477,62 @@ object DFXInt:
            |In DFHDL, Int literals are converted to minimum bit-accurate width.
            |Use carry operations (+^, -^, *^) or explicit bit-accurate literals (d"W'V").""".stripMargin
 
-      // Check if a value is tagged with ImplicitlyFromIntTag
-      private[core] def hasImplicitlyFromIntTag(dfVal: ir.DFVal): Boolean =
-        dfVal.tags.hasTagOf[ir.ImplicitlyFromIntTag]
+      // Check if a value is tagged with ImplicitlyFromIntTag. An implicit `Int` operand
+      // adapted to a parametric width keeps its tagged const under a resize alias (the
+      // fold into a single const happens only for literal widths), so the check follows
+      // alias chains down to the underlying value.
+      private[core] def hasImplicitlyFromIntTag(dfVal: ir.DFVal)(using ir.MemberGetSet): Boolean =
+        dfVal.tags.hasTagOf[ir.ImplicitlyFromIntTag] ||
+          (dfVal match
+            case alias: ir.DFVal.Alias => hasImplicitlyFromIntTag(alias.relValRef.get)
+            case _                     => false)
+
+      // A width reference resolved through design parameters: this runs during
+      // elaboration, where a parameter's applied (or default) value is known, so a
+      // parametric width like `CORDW + 1` resolves to its actual value.
+      private def resolvedWidthOf(ref: ir.IntParamRef)(using
+          getSet: ir.MemberGetSet
+      ): Option[Int] =
+        ref.getIntConstData(using
+          getSet,
+          ir.ConstData.CachePolicy.GoThroughDesignParams
+        ) match
+          case ir.ConstData.KnownConst(w) => Some(w)
+          case _                          => None
+
+      // A value's width classified as narrow (< 32 bits). A width that cannot be
+      // resolved counts as narrow: a false-positive warning costs one carry op, while a
+      // false negative is silently wrong hardware.
+      private def resolvedWidthIsNarrow(dfVal: ir.DFVal)(using ir.MemberGetSet): Boolean =
+        dfVal.dfType match
+          case dec: ir.DFDecimal =>
+            resolvedWidthOf(dec.magnitudeWidthParamRef) match
+              case Some(m) => m + dec.fractionWidth < 32
+              case None    => true
+          case _ =>
+            dfVal.dfType.widthIntOpt.map(_ < 32).getOrElse(true)
+
+      // An anonymous sign-conversion alias: an unsigned value reinterpreted as signed
+      // with exactly one extra bit (`.signed`). The Verilog backend emits it as
+      // `$signed({1'b0, ...})`, whose concatenation operand is self-determined, so a
+      // narrow chain stays narrow through it and the promotion/warning machinery must
+      // look through it. An equal-width alias is a reinterpret cast and never matches.
+      private def signConversionRelVal(dfVal: ir.DFVal)(using
+          ir.MemberGetSet
+      ): Option[ir.DFVal] =
+        dfVal match
+          case alias: ir.DFVal.Alias.AsIs if alias.isAnonymous =>
+            alias.dfType match
+              case ir.DFSInt(aliasWidthRef) =>
+                val relVal = alias.relValRef.get
+                relVal.dfType match
+                  case ir.DFUInt(relWidthRef) =>
+                    (resolvedWidthOf(aliasWidthRef), resolvedWidthOf(relWidthRef)) match
+                      case (Some(aw), Some(rw)) if aw == rw + 1 => Some(relVal)
+                      case _                                    => None
+                  case _ => None
+              case _ => None
+          case _ => None
 
       // Check if an anonymous sub-tree contains non-carry +/-/* with width < 32.
       private[core] def containsNarrowNonCarryArith(
@@ -1446,16 +1543,19 @@ object DFXInt:
             func.op match
               case FuncOp.+ | FuncOp.- | FuncOp.* =>
                 val isNonCarry = func.dfType =~ func.args.head.get.dfType
-                val isNarrowNonCarry = isNonCarry && func.widthIntOpt.map(_ < 32).getOrElse(false)
+                val isNarrowNonCarry = isNonCarry && resolvedWidthIsNarrow(func)
                 isNarrowNonCarry ||
                 func.args.exists(ref => containsNarrowNonCarryArith(ref.get))
               case _ =>
                 func.args.exists(ref => containsNarrowNonCarryArith(ref.get))
-          case _ => false
+          case _ =>
+            signConversionRelVal(dfVal) match
+              case Some(relVal) => containsNarrowNonCarryArith(relVal)
+              case None         => false
 
       // Check if an anonymous sub-tree contains narrow non-carry arith that
       // also has an ImplicitlyFromIntTag operand (Verilog "Forcing Larger
-      // Evaluation" pattern, or implicit Int in a chain assigned to wider target).
+      // Evaluation" pattern).
       private[core] def containsNarrowNonCarryArithWithTaggedOperand(
           dfVal: ir.DFVal
       )(using ir.MemberGetSet): Boolean =
@@ -1464,7 +1564,7 @@ object DFXInt:
             func.op match
               case FuncOp.+ | FuncOp.- | FuncOp.* =>
                 val isNonCarry = func.dfType =~ func.args.head.get.dfType
-                val isNarrowNonCarry = isNonCarry && func.widthIntOpt.map(_ < 32).getOrElse(false)
+                val isNarrowNonCarry = isNonCarry && resolvedWidthIsNarrow(func)
                 (isNarrowNonCarry && func.args.exists(ref => hasImplicitlyFromIntTag(ref.get))) ||
                 func.args.exists(ref =>
                   containsNarrowNonCarryArithWithTaggedOperand(ref.get)
@@ -1473,7 +1573,10 @@ object DFXInt:
                 func.args.exists(ref =>
                   containsNarrowNonCarryArithWithTaggedOperand(ref.get)
                 )
-          case _ => false
+          case _ =>
+            signConversionRelVal(dfVal) match
+              case Some(relVal) => containsNarrowNonCarryArithWithTaggedOperand(relVal)
+              case None         => false
 
       // Unified Verilog-semantics warning trigger shared by `/`, `%` (arithOp)
       // and comparison operations (DFXIntCompare). Warns when a narrow non-carry
@@ -1636,9 +1739,10 @@ object DFXInt:
             val rhsIsWildcard = isWildcardR.value
             val retVal =
               if (lhsIsWildcard && !rhsIsWildcard)
-                // LHS is wildcard: adapt to RHS type
+                // LHS is wildcard: adapt to RHS type, keeping the written operand order
                 checkWildcardFit(lhsVal.asValOf[DFInt32], rhsVal.dfType)
-                arithOp(rhsVal.dfType, op.value, rhsVal, lhsVal)
+                val lhsFix = lhsVal.toDFXIntOf(rhsVal.dfType)(using dfcAnon)
+                DFVal.Func(rhsVal.dfType, op.value, List(lhsFix, rhsVal))
               else if (rhsIsWildcard) // LHS may be wildcard or concrete
                 // RHS is wildcard: adapt to LHS type
                 checkWildcardFit(rhsVal.asValOf[DFInt32], lhsVal.dfType)
@@ -1655,8 +1759,12 @@ object DFXInt:
                   else rhsVal.asValOf[DFSInt[Int]]
                 lhsSFix.compareWidths(rhsSFix)(_ >= _) match
                   case Some(true)  => arithOp(lhsSFix.dfType, op.value, lhsSFix, rhsSFix)
-                  case Some(false) => arithOp(rhsSFix.dfType, op.value, rhsSFix, lhsSFix)
-                  case None        =>
+                  case Some(false) =>
+                    // RHS is wider: the result takes its type, but the written operand
+                    // order is kept, so the narrower LHS converts in place
+                    val lhsFix = lhsSFix.toDFXIntOf(rhsSFix.dfType)(using dfcAnon)
+                    DFVal.Func(rhsSFix.dfType, op.value, List(lhsFix, rhsSFix))
+                  case None =>
                     val lhsEffWidth: IntParam[Int] = lhsSFix.widthIntParam
                     val rhsEffWidth: IntParam[Int] = rhsSFix.widthIntParam
                     val maxWidth = lhsEffWidth.max(rhsEffWidth)
@@ -1755,6 +1863,8 @@ object DFXInt:
           icL: Candidate.Aux[L, LS, LW, LN, LP],
           icR: Candidate.Aux[R, RS, RW, RN, RP],
           op: ValueOf[Op]
+      )(using
+          carryCheck: CarryCheck[LN, RN]
       ): ExactOp2Aux[CarryOp[Op], DFC, DFValAny, L, R, DFValTP[
         DFXInt[LS || RS, IntP.ArithCarryWidth[LW, RW], BitAccurate],
         LP | RP
@@ -1764,9 +1874,26 @@ object DFXInt:
           val dfcAnon = dfc.anonymize
           val lhsVal = icL(lhs)(using dfcAnon)
           val rhsVal = icR(rhs)(using dfcAnon)
-          val resultSigned = lhsVal.dfType.signed || rhsVal.dfType.signed
           import IntParam.{+, max}
-          val commonWidth = lhsVal.widthIntParam.max(rhsVal.widthIntParam)
+          // A wildcard `Int` operand (a DFHDL `Int` parameter or an expression over one)
+          // adapts to the bit-accurate operand's sign and width before the carry widening,
+          // instead of contributing its 32-bit signed representation. `carryCheck` rules
+          // out two wildcard operands. Scala `Int` operands are already bit-accurate here
+          // (the candidate converts them at their value's minimal width), so they keep
+          // contributing that width to the common-width calculation.
+          val lhsIsWildcard = lhsVal.dfType.asIR.isDFInt32
+          val rhsIsWildcard = rhsVal.dfType.asIR.isDFInt32
+          carryCheck(lhsIsWildcard, rhsIsWildcard)
+          if (rhsIsWildcard) checkWildcardFit(rhsVal.asValOf[DFInt32], lhsVal.dfType)
+          else if (lhsIsWildcard) checkWildcardFit(lhsVal.asValOf[DFInt32], rhsVal.dfType)
+          val resultSigned: Boolean =
+            if (rhsIsWildcard) lhsVal.dfType.signed
+            else if (lhsIsWildcard) rhsVal.dfType.signed
+            else lhsVal.dfType.signed || rhsVal.dfType.signed
+          val commonWidth: IntParam[Int] =
+            if (rhsIsWildcard) lhsVal.widthIntParam
+            else if (lhsIsWildcard) rhsVal.widthIntParam
+            else lhsVal.widthIntParam.max(rhsVal.widthIntParam)
           val width = commonWidth + 1
           val dfType = DFXInt(resultSigned, width, BitAccurate)
           // Resize both operands to common width, converting to signed if needed
@@ -1793,6 +1920,8 @@ object DFXInt:
       ](using
           icL: Candidate.Aux[L, LS, LW, LN, LP],
           icR: Candidate.Aux[R, RS, RW, RN, RP]
+      )(using
+          carryCheck: CarryCheck[LN, RN]
       ): ExactOp2Aux[CarryOp[Op], DFC, DFValAny, L, R, DFValTP[
         DFXInt[LS || RS, IntP.+[LW, RW], BitAccurate],
         LP | RP
@@ -1802,21 +1931,46 @@ object DFXInt:
           val dfcAnon = dfc.anonymize
           val lhsVal = icL(lhs)(using dfcAnon)
           val rhsVal = icR(rhs)(using dfcAnon)
-          val resultSigned = lhsVal.dfType.signed || rhsVal.dfType.signed
           import IntParam.+
-          val width = lhsVal.widthIntParam + rhsVal.widthIntParam
-          val dfType = DFXInt(resultSigned, width, BitAccurate)
-          // Convert unsigned operand to signed if needed
-          val lhsFix =
-            if (resultSigned && !lhsVal.dfType.signed)
-              lhsVal.toDFXIntOf(DFXInt(true, lhsVal.widthIntParam + 1, BitAccurate))(using dfcAnon)
-            else lhsVal
-          val rhsFix =
-            if (resultSigned && !rhsVal.dfType.signed)
-              rhsVal.toDFXIntOf(DFXInt(true, rhsVal.widthIntParam + 1, BitAccurate))(using dfcAnon)
-            else rhsVal
-          DFVal.Func(dfType, FuncOp.`*`, List(lhsFix, rhsFix))
-            .asInstanceOf[Out]
+          // Same wildcard adaptation as carry add/sub: the wildcard `Int` operand takes
+          // the bit-accurate operand's sign and width, so the product doubles that width
+          // and keeps that sign.
+          val lhsIsWildcard = lhsVal.dfType.asIR.isDFInt32
+          val rhsIsWildcard = rhsVal.dfType.asIR.isDFInt32
+          carryCheck(lhsIsWildcard, rhsIsWildcard)
+          if (rhsIsWildcard) checkWildcardFit(rhsVal.asValOf[DFInt32], lhsVal.dfType)
+          else if (lhsIsWildcard) checkWildcardFit(lhsVal.asValOf[DFInt32], rhsVal.dfType)
+          if (lhsIsWildcard || rhsIsWildcard)
+            val baSigned: Boolean =
+              if (rhsIsWildcard) lhsVal.dfType.signed else rhsVal.dfType.signed
+            val baWidth: IntParam[Int] =
+              if (rhsIsWildcard) lhsVal.widthIntParam else rhsVal.widthIntParam
+            val commonType = DFXInt(baSigned, baWidth, BitAccurate)
+            val dfType = DFXInt(baSigned, baWidth + baWidth, BitAccurate)
+            val lhsFix = lhsVal.toDFXIntOf(commonType)(using dfcAnon)
+            val rhsFix = rhsVal.toDFXIntOf(commonType)(using dfcAnon)
+            DFVal.Func(dfType, FuncOp.`*`, List(lhsFix, rhsFix))
+              .asInstanceOf[Out]
+          else
+            val resultSigned = lhsVal.dfType.signed || rhsVal.dfType.signed
+            val width = lhsVal.widthIntParam + rhsVal.widthIntParam
+            val dfType = DFXInt(resultSigned, width, BitAccurate)
+            // Convert unsigned operand to signed if needed
+            val lhsFix =
+              if (resultSigned && !lhsVal.dfType.signed)
+                lhsVal.toDFXIntOf(DFXInt(true, lhsVal.widthIntParam + 1, BitAccurate))(using
+                  dfcAnon
+                )
+              else lhsVal
+            val rhsFix =
+              if (resultSigned && !rhsVal.dfType.signed)
+                rhsVal.toDFXIntOf(DFXInt(true, rhsVal.widthIntParam + 1, BitAccurate))(using
+                  dfcAnon
+                )
+              else rhsVal
+            DFVal.Func(dfType, FuncOp.`*`, List(lhsFix, rhsFix))
+              .asInstanceOf[Out]
+          end if
         }(using dfc, CTName("*^"))
       end evOpCarryMulDFXInt
 
diff --git a/core/src/main/scala/dfhdl/core/DFEnum.scala b/core/src/main/scala/dfhdl/core/DFEnum.scala
index 65102d386..66c2acad5 100644
--- a/core/src/main/scala/dfhdl/core/DFEnum.scala
+++ b/core/src/main/scala/dfhdl/core/DFEnum.scala
@@ -156,6 +156,20 @@ object DFEnum:
           DFVal.Func(lhs.dfType, FuncOp.unary_!, List(lhs))
         }
       end extension
+      extension [P, E <: DFEncoding](lhs: DFValTP[DFEnum[E], P])
+        // The entry encoding reinterpreted as an unsigned integer of the enum's width,
+        // composed as `.bits.uint`: every backend already renders that chain as a direct
+        // cast, so no dedicated enum-to-uint alias exists in the IR or the printers.
+        // The width is bound to a type parameter rather than read off the instance; see
+        // the note on `bits` in `DFVal.Ops`.
+        @targetName("uintOfDFEnum")
+        def uint[W <: IntP](using DFCG)(using Width.Aux[DFEnum[E], W]): DFValTP[DFUInt[W], P] =
+          trydf {
+            import DFVal.Ops.bits
+            import DFBits.Val.Ops.uint as bitsUint
+            lhs.bits.bitsUint
+          }
+      end extension
     end Ops
   end Val
 end DFEnum
diff --git a/core/src/main/scala/dfhdl/core/DFType.scala b/core/src/main/scala/dfhdl/core/DFType.scala
index a36172962..d53b86f90 100644
--- a/core/src/main/scala/dfhdl/core/DFType.scala
+++ b/core/src/main/scala/dfhdl/core/DFType.scala
@@ -267,14 +267,22 @@ object DFType:
       case dt: ir.DFBits    => dt.widthParamRef
       case dt: ir.DFDecimal => dt.magnitudeWidthParamRef
   extension [LW <: IntP](lhs: DFTypeW[LW])
-    protected[core] def compareWidths[RW <: IntP](rhs: DFTypeW[RW])(
+    protected[core] def compareWidths[RW <: IntP](
+        rhs: DFTypeW[RW],
+        elimSymbolicMaxMin: Boolean = false
+    )(
         func: (Int, Int) => Boolean
     )(using dfc: DFC): Option[Boolean] =
       import dfc.getSet
-      widthRef(lhs).compare(widthRef(rhs))(func)
+      widthRef(lhs).compare(widthRef(rhs), elimSymbolicMaxMin)(func)
     protected[core] def widthCodeString(using dfc: DFC): String =
       import dfc.getSet
       widthRef(lhs).refCodeString
+    // for diagnostics: qualifies a named width relative to the error site's owner
+    protected[core] def widthErrorString(using dfc: DFC): String =
+      import dfc.getSet
+      widthRef(lhs).refErrorString
+  end extension
 
 end DFType
 
diff --git a/core/src/main/scala/dfhdl/core/DFVal.scala b/core/src/main/scala/dfhdl/core/DFVal.scala
index cec9ab161..6f6bba4f1 100644
--- a/core/src/main/scala/dfhdl/core/DFVal.scala
+++ b/core/src/main/scala/dfhdl/core/DFVal.scala
@@ -409,10 +409,11 @@ object DFVal extends DFValLP:
 
   extension [LW <: IntP, LT <: DFTypeW[LW]](lhs: DFValOf[LT])
     protected[core] def compareWidths[RW <: IntP, RT <: DFTypeW[RW]](
-        rhs: DFValOf[RT]
+        rhs: DFValOf[RT],
+        elimSymbolicMaxMin: Boolean = false
     )(func: (Int, Int) => Boolean)(using dfc: DFC): Option[Boolean] =
       import dfc.getSet
-      lhs.dfType.compareWidths(rhs.dfType)(func)
+      lhs.dfType.compareWidths(rhs.dfType, elimSymbolicMaxMin)(func)
 
   trait InitCheck[I]
   given [I](using
@@ -907,12 +908,15 @@ object DFVal extends DFValLP:
               const.data.asInstanceOf[const.dfType.Data]
             )
             val newDFType = aliasTypeIR.dropUnreachableRefs
-            // the constant is replaced in place only when it is a throwaway literal freshly
-            // created at the current position. otherwise (an anonymous constant created
+            // The constant is replaced in place only when it is a throwaway literal freshly
+            // created at the current position. Otherwise (an anonymous constant created
             // elsewhere) it may be aliased by a live Scala reference and reused (e.g. a value
             // bound via tuple destructuring), so mutating it in place would corrupt those
             // uses; instead we materialize a new converted constant and leave the original
-            // untouched.
+            // untouched. NOTE (issue #449 audit): unlike a REMOVAL, an in-place revision
+            // cannot leave a ghost refTable value: same-context bindings are re-pointed by
+            // `setMember`, and cross-context bindings to anonymous members never exist
+            // (`cloneUnreachable` clones instead).
             if (relVal.inDFCPosition)
               dfc.mutableDB.setMember(
                 const,
@@ -948,6 +952,8 @@ object DFVal extends DFValLP:
                 dfType = ir.DFBits(_) | ir.DFUInt(_) | ir.DFSInt(_),
                 relValRef = ir.DFRef(ir.DFBoolOrBit.Val(deepRelVal))
               ) if asIs.isAnonymous && !forceNewAlias =>
+            // in-place retype of the intermediate cast (see the issue #449 audit note above:
+            // a revision, unlike a removal, cannot leave a ghost refTable value)
             dfc.mutableDB.setMember(
               asIs,
               _.copy(
diff --git a/core/src/main/scala/dfhdl/core/DFVector.scala b/core/src/main/scala/dfhdl/core/DFVector.scala
index 41775bb20..b31f50340 100644
--- a/core/src/main/scala/dfhdl/core/DFVector.scala
+++ b/core/src/main/scala/dfhdl/core/DFVector.scala
@@ -110,8 +110,8 @@ object DFVector:
               val dfTypeLengthRef = dfType.asIR.cellDimParamRefs.head
               val argLengthRef = arg.dfType.asIR.cellDimParamRefs.head
               if (dfTypeLengthRef.compare(argLengthRef)(_ != _).getOrElse(true))
-                val dfTypeLengthStr = dfTypeLengthRef.refCodeString
-                val argLengthStr = argLengthRef.refCodeString
+                val dfTypeLengthStr = dfTypeLengthRef.refErrorString
+                val argLengthStr = argLengthRef.refErrorString
                 throw new IllegalArgumentException(
                   s"""The argument vector length ($argLengthStr) is different than the receiver vector length ($dfTypeLengthStr)."""
                 )
@@ -141,7 +141,7 @@ object DFVector:
           dfType.lengthIntOpt match
             case Some(ll) => check(ll, dfVals.length)
             case None     =>
-              val dfTypeLengthStr = dfType.asIR.cellDimParamRefs.head.refCodeString
+              val dfTypeLengthStr = dfType.asIR.cellDimParamRefs.head.refErrorString
               throw new IllegalArgumentException(
                 s"""The argument vector length (${dfVals.length}) is different than the receiver vector length ($dfTypeLengthStr)."""
               )
@@ -211,8 +211,8 @@ object DFVector:
               val dfTypeLengthRef = dfType.asIR.cellDimParamRefs.head
               val argLengthRef = arg.dfType.asIR.cellDimParamRefs.head
               if (dfTypeLengthRef.compare(argLengthRef)(_ != _).getOrElse(true))
-                val dfTypeLengthStr = dfTypeLengthRef.refCodeString
-                val argLengthStr = argLengthRef.refCodeString
+                val dfTypeLengthStr = dfTypeLengthRef.refErrorString
+                val argLengthStr = argLengthRef.refErrorString
                 throw new IllegalArgumentException(
                   s"""The argument vector length ($argLengthStr) is different than the receiver vector length ($dfTypeLengthStr)."""
                 )
@@ -248,7 +248,7 @@ object DFVector:
               val check = summon[`LL == RL`.Check[Int, Int]]
               check(ll, dfVals.length)
             case None =>
-              val dfTypeLengthStr = dfType.asIR.cellDimParamRefs.head.refCodeString
+              val dfTypeLengthStr = dfType.asIR.cellDimParamRefs.head.refErrorString
               throw new IllegalArgumentException(
                 s"""The argument vector length (${dfVals.length}) is different than the receiver vector length ($dfTypeLengthStr)."""
               )
diff --git a/core/src/main/scala/dfhdl/core/IntParam.scala b/core/src/main/scala/dfhdl/core/IntParam.scala
index d1750c21e..fc1ae1d77 100644
--- a/core/src/main/scala/dfhdl/core/IntParam.scala
+++ b/core/src/main/scala/dfhdl/core/IntParam.scala
@@ -268,3 +268,21 @@ extension (intParamRef: ir.IntParamRef)
     import dfhdl.compiler.printing.refCodeString as refCodeStringIR
     given printer: Printer = DefaultPrinter
     intParamRef.refCodeStringIR
+  // Diagnostic rendering of a width/length parameter reference: a named parameter is
+  // qualified relative to the error site's owner (`c.OUTPUT_WIDTH` vs `OUTPUT_WIDTH`), so
+  // two same-named constants from different designs stay distinguishable in the message.
+  // Code printing (`refCodeString`) stays relative to the reference's own design, where
+  // such qualification would be wrong.
+  protected[core] def refErrorString(using dfc: DFC): String =
+    intParamRef match
+      case ref: ir.DFRef.TypeRef =>
+        import dfc.getSet
+        val dfVal = ref.get
+        if (dfVal.isAnonymous) refCodeString
+        else
+          val callOwner: ir.DFOwner | ir.DFMember.Empty = dfc.ownerOption match
+            case Some(owner) => owner.asIR
+            case None        => ir.DFMember.Empty
+          dfVal.getRelativeName(callOwner)
+      case int: Int => int.toString
+end extension
diff --git a/core/src/main/scala/dfhdl/core/MutableDB.scala b/core/src/main/scala/dfhdl/core/MutableDB.scala
index a067a0930..5854930cb 100644
--- a/core/src/main/scala/dfhdl/core/MutableDB.scala
+++ b/core/src/main/scala/dfhdl/core/MutableDB.scala
@@ -28,6 +28,7 @@ import dfhdl.compiler.ir.{
   SubDesignRef
 }
 
+import dfhdl.compiler.analysis.isDroppableIfUnread
 import scala.reflect.{ClassTag, classTag}
 import scala.util.control.NonFatal
 import collection.mutable
@@ -207,6 +208,43 @@ class DesignContext:
     globalDefSubDBs ++= sourceCtx.globalDefSubDBs
   end inject
 
+  // ~~~ the end-of-design sweep of unread droppable members ~~~
+  // Operation simplifications never revise or remove members (an anonymous member is an
+  // immutable expression-graph node; revising or removing one that a still-live front-end
+  // handle can later reference plants refTable values that are no longer members, which is
+  // fatal across the sub-design cache adoption boundary, issue #449). Superseded intermediates
+  // therefore accumulate as debris and are dropped HERE, at the snapshot boundary, where
+  // "is it read?" has its final answer. The kind-level criteria (`isDroppableIfUnread`) are
+  // shared with the `DropUnreferencedAnons` stage; a droppable member survives only when it is
+  // transitively reachable from a non-droppable member through `getRefs`. Reachability is
+  // computed over the refs and never over `refSet`, which misses binds that landed in a nested
+  // context's table (`newRefFor`'s fallback branch).
+  def sweepUnreadAnons()(using MemberGetSet): Unit =
+    val keep = new Array[Boolean](members.length)
+    val queue = mutable.ArrayDeque.empty[Int]
+    members.zipWithIndex.foreach { case (e, i) =>
+      if (!e.ignore && !e.irValue.isDroppableIfUnread)
+        keep(i) = true
+        queue += i
+    }
+    while (queue.nonEmpty)
+      val i = queue.removeHead()
+      members(i).irValue.getRefs.foreach { r =>
+        refTable.get(r).foreach { target =>
+          memberTable.get(target).foreach { ti =>
+            if (!keep(ti) && !members(ti).ignore)
+              keep(ti) = true
+              queue += ti
+          }
+        }
+      }
+    var i = 0
+    while (i < members.length)
+      val e = members(i)
+      if (!e.ignore && !keep(i)) members.update(i, e.copy(ignore = true))
+      i += 1
+  end sweepUnreadAnons
+
   def getImmutableMemberList: List[DFMember] =
     members.view.filterNot(e => e.ignore).map(e => e.irValue).toList
 
@@ -287,6 +325,12 @@ final class MutableDB():
       stack = current :: stack
       current = new DesignContext
     def endDesign(design: DFDesignBlock): Unit =
+      // Sweep unread droppable members before the snapshot (see `sweepUnreadAnons`). Skipped
+      // for a duplicate design (its snapshot is never read) and under meta-programming, where
+      // a stage's members gain their readers only after the patch lands in the target DB, so
+      // sweeping would delete live stage work.
+      if (!inMetaProgramming && current.duplicateOf.isEmpty)
+        current.sweepUnreadAnons()(using self.getSet)
       val currentMembers = current.getImmutableMemberList.drop(1)
       val currentRefTable = current.getImmutableRefTable
       val designType = design.dclName
diff --git a/core/src/main/scala/dfhdl/core/SimplifyFunc.scala b/core/src/main/scala/dfhdl/core/SimplifyFunc.scala
index 826583423..6df6a02a0 100644
--- a/core/src/main/scala/dfhdl/core/SimplifyFunc.scala
+++ b/core/src/main/scala/dfhdl/core/SimplifyFunc.scala
@@ -1,5 +1,6 @@
 package dfhdl.core
 import dfhdl.compiler.ir
+import dfhdl.compiler.analysis.stripTypePreservingAliases
 import DFVal.Func.Op as FuncOp
 import dfhdl.internals.Position
 
@@ -10,9 +11,12 @@ private object SimplifyFunc:
     if (dfc.inMetaProgramming) None
     else
       opArgs match
-        // These two run even in global context (no owner).
+        // These three run even in global context (no owner).
         case ConstFoldAddSubChain(v) => Some(v)
-        case MergeAssocFunc(v)       => Some(v)
+        // Must precede MergeAssocFunc, which otherwise consumes the same
+        // shape by appending the duplicate operand to the chain.
+        case MaxMinChainAbsorb(v) => Some(v)
+        case MergeAssocFunc(v)    => Some(v)
         // TODO: maybe drop this limitation, if we can make DropStructsVecs work in
         // global context.
         case _ if dfc.ownerOption.isEmpty => None
@@ -49,12 +53,13 @@ private object SimplifyFunc:
       dfc.ownerOrEmptyRef, dfc.getMeta, dfc.tags
     ).addMember
 
-  // Re-stamps an anonymous returning DFVal with the current meta so the outer
-  // val binding picks up its name, matching the existing pattern in
-  // ConstFoldAddSubChain. Named values are returned as-is.
+  // Naming without mutation: a simplification returns an EXISTING value, so a `val` binding's
+  // name is applied by wrapping the value in a named Ident rather than by restamping its meta
+  // (an anonymous member is never revised; issue #449). With an anonymous context the value is
+  // returned untouched and keeps its own meta.
   private def rebindMeta(v: ir.DFVal)(using dfc: DFC): ir.DFVal =
-    import dfc.getSet
-    if (v.isAnonymous) v.setMeta(_ => dfc.getMeta) else v
+    if (dfc.isAnonymous) v
+    else DFVal.Alias.AsIs.ident(v.asValAny).asIR
 
   // Extractor for an anonymous DFInt32 Const with a known Int payload.
   private object ConstInt:
@@ -101,13 +106,27 @@ private object SimplifyFunc:
                 case (FuncOp.-, FuncOp.+) => prevRHSData - currentRHSData
               if (newRHSData == BigInt(0)) Some(rebindMeta(prevLHSArg))
               else
-                // Clone prevFunc to avoid destructively modifying shared IR nodes
-                val clonedFunc = prevFunc.cloneAnonValueAndDepsHere
-                  .asInstanceOf[ir.DFVal.Func]
-                val clonedRHSArg = clonedFunc.args.last.get
-                  .asInstanceOf[ir.DFVal.Const]
-                dfc.mutableDB.setMember(clonedRHSArg, _.copy(data = Some(newRHSData)))
-                Some(dfc.mutableDB.setMember(clonedFunc, _.copy(meta = dfc.getMeta)))
+                // Fold by construction: a fresh Const carrying the folded payload plus a fresh
+                // Func referencing the original LHS. The superseded chain is left as debris for
+                // the end-of-design sweep (an anonymous member is never revised; issue #449).
+                val foldedConst = ir.DFVal.Const(
+                  ir.DFInt32, Some(newRHSData),
+                  dfc.ownerOrEmptyRef, prevRHSArg.meta, dfc.tags
+                ).addMember
+                Some(
+                  ir.DFVal.Func(
+                    ir.DFInt32,
+                    prevOp,
+                    List(
+                      prevLHSArg.refTW[ir.DFVal](knownReachable = true),
+                      foldedConst.refTW[ir.DFVal](knownReachable = true)
+                    ),
+                    dfc.ownerOrEmptyRef,
+                    dfc.getMeta,
+                    dfc.tags
+                  ).addMember
+                )
+              end if
             case _ => None
           end match
         // Const +/- Const fold. Runs when the LHS has been collapsed to a
@@ -125,17 +144,42 @@ private object SimplifyFunc:
           val result = currentOp.runtimeChecked match
             case FuncOp.+ => lhsData + rhsData
             case FuncOp.- => lhsData - rhsData
-          Some(
-            dfc.mutableDB.setMember(
-              lhs,
-              _.copy(data = Some(result), meta = dfc.getMeta)
-            )
-          )
+          // a fresh folded Const; the operand literals become debris for the sweep
+          Some(mkInt32Const(result))
         case _ => None
       end match
     end unapply
   end ConstFoldAddSubChain
 
+  // max/min chain absorption: when one operand is itself a same-op max/min
+  // Func that already carries the other operand as one of its arguments, the
+  // chain subsumes it (max(max(a, b), b) == max(a, b), likewise for min), so
+  // the existing chain value is returned as-is. This keeps unrolled width
+  // computations like max(max(max(16, W), W), W) minimized to max(16, W).
+  // Runs even in global context (no owner): it only reads the chain and never
+  // creates or removes members.
+  private object MaxMinChainAbsorb:
+    private def chainAbsorbs(chain: ir.DFVal, other: ir.DFVal, op: FuncOp)(using
+        dfc: DFC
+    ): Boolean =
+      import dfc.getSet
+      // ident-transparent: the chain and the compared operands may be (named) idents of the
+      // actual expressions, e.g. `max(M, b)` with `val M = max(a, b)`
+      chain.stripTypePreservingAliases match
+        case chainFunc: ir.DFVal.Func if chainFunc.dfType == ir.DFInt32 && chainFunc.op == op =>
+          val otherStripped = other.stripTypePreservingAliases
+          chainFunc.args.exists(_.get.stripTypePreservingAliases =~ otherStripped)
+        case _ => false
+    def unapply(opArgs: (ir.DFType, FuncOp, List[ir.DFVal]))(using dfc: DFC): Option[ir.DFVal] =
+      opArgs match
+        case (ir.DFInt32, op @ (FuncOp.max | FuncOp.min), List(a, b)) =>
+          if (chainAbsorbs(a, b, op)) Some(rebindMeta(a))
+          else if (chainAbsorbs(b, a, op)) Some(rebindMeta(b))
+          else None
+        case _ => None
+    end unapply
+  end MaxMinChainAbsorb
+
   // Merge consecutive same-op anonymous Funcs for associative operations.
   // E.g., `a + b + c` becomes Func(+, [a, b, c]) instead of nested binary Funcs.
   // For left-associative chains, only the first arg can be an absorbed Func.
@@ -159,26 +203,21 @@ private object SimplifyFunc:
             currentPos.lineEnd, currentPos.columnEnd
           )
           val meta = currentMeta.copy(position = mergedPos)
-          // If prevFunc is referenced elsewhere, absorbing it would orphan those
-          // refs. Clone it so we consume a private copy and leave the original
-          // (and its referrers) intact.
-          val absorbable =
-            if (dfc.mutableDB.DesignContext.current.getMemberRefs(prevFunc).isEmpty) prevFunc
-            else prevFunc.cloneAnonValueAndDepsHere.asInstanceOf[ir.DFVal.Func]
-          // Reuse absorbed Func's existing arg refs (so they aren't orphaned)
-          // and create new refs only for the tail args being appended.
-          val newArgRefs: List[ir.DFVal.Ref] =
-            absorbable.args ++ rest.map(_.refTW[ir.DFVal](knownReachable = true))
-          val func: ir.DFVal = ir.DFVal.Func(
-            dfType, op, newArgRefs,
-            dfc.ownerOrEmptyRef, meta, dfc.tags
+          // Purely additive: fresh refs for both the absorbed args and the appended tail args.
+          // The absorbed Func's own arg refs are never reused (reuse entangles the two members'
+          // tokens and breaks origin tracking), and the absorbed Func itself is never removed:
+          // the front end may still hold a handle to it and reference it later (e.g. `lsbitsAt`
+          // referencing its offset expression after the width computation absorbed it; issue
+          // #449). When nothing ends up reading it, the end-of-design sweep drops it.
+          val newArgRefs: List[ir.DFVal.Ref] = (prevFunc.args.map(_.get) ++ rest).map(
+            _.refTW[ir.DFVal](knownReachable = true)
+          )
+          Some(
+            ir.DFVal.Func(
+              dfType, op, newArgRefs,
+              dfc.ownerOrEmptyRef, meta, dfc.tags
+            ).addMember
           )
-          // Add positions newFunc at the tail (after any later-created arg deps).
-          // Reusing absorbable.args causes setOriginRefs to update their origin to
-          // newFunc, so the absorbed Func can simply be marked ignored.
-          func.addMember
-          getSet.remove(absorbable)
-          Some(func)
         case _ => None
       end match
     end unapply
@@ -194,14 +233,18 @@ private object SimplifyFunc:
               FuncOp.unary_-,
               List(const @ ir.DFVal.Const(dfType = _: ir.DFDecimal, data = Some(data: BigInt)))
             ) if (const.isAnonymous || const.asValAny.inDFCPosition) =>
+          // a fresh negated Const takes over the binding name; the original literal,
+          // anonymized, becomes debris for the sweep (an anonymous member is never revised
+          // in place; issue #449)
+          const.asValAny.anonymizeInDFCPosition
           Some(
-            dfc.mutableDB.setMember(
-              const,
-              _.copy(
-                data = Some(-data),
-                meta = dfc.getMeta
-              )
-            )
+            ir.DFVal.Const(
+              const.dfType,
+              Some(-data),
+              dfc.ownerOrEmptyRef,
+              dfc.getMeta,
+              dfc.tags
+            ).addMember
           )
         case _ => None
       end match
@@ -220,17 +263,13 @@ private object SimplifyFunc:
         // x * 1 / 1 * x  ->  x
         case (ir.DFInt32, FuncOp.`*`, List(x, ConstInt(1))) => Some(rebindMeta(x))
         case (ir.DFInt32, FuncOp.`*`, List(ConstInt(1), x)) => Some(rebindMeta(x))
-        // x * 0 / 0 * x  ->  0
+        // x * 0 / 0 * x  ->  0 (a fresh Const; the operands become debris for the sweep)
         case (ir.DFInt32, FuncOp.`*`, List(_, c @ ir.DFVal.Const(data = Some(d: BigInt))))
             if d == BigInt(0) && c.isAnonymous =>
-          Some(
-            dfc.mutableDB.setMember(c, _.copy(meta = dfc.getMeta))
-          )
+          Some(mkInt32Const(0))
         case (ir.DFInt32, FuncOp.`*`, List(c @ ir.DFVal.Const(data = Some(d: BigInt)), _))
             if d == BigInt(0) && c.isAnonymous =>
-          Some(
-            dfc.mutableDB.setMember(c, _.copy(meta = dfc.getMeta))
-          )
+          Some(mkInt32Const(0))
         case _ => None
       end match
     end unapply
@@ -241,11 +280,13 @@ private object SimplifyFunc:
     def unapply(opArgs: (ir.DFType, FuncOp, List[ir.DFVal]))(using dfc: DFC): Option[ir.DFVal] =
       import dfc.getSet
       opArgs match
-        // a - a  ->  0
-        case (ir.DFInt32, FuncOp.-, List(a, b)) if a =~ b =>
+        // a - a  ->  0 (ident-transparent: `W - a` cancels when `val W = <collapses to a>`)
+        case (ir.DFInt32, FuncOp.-, List(a, b))
+            if a.stripTypePreservingAliases =~ b.stripTypePreservingAliases =>
           Some(mkInt32Const(0))
         // max(a, a) / min(a, a)  ->  a
-        case (ir.DFInt32, FuncOp.max | FuncOp.min, List(a, b)) if a =~ b =>
+        case (ir.DFInt32, FuncOp.max | FuncOp.min, List(a, b))
+            if a.stripTypePreservingAliases =~ b.stripTypePreservingAliases =>
           Some(rebindMeta(a))
         case _ => None
     end unapply
@@ -298,12 +339,14 @@ private object SimplifyFunc:
           val chain = collectChain(prev) :+ ((if (currentOp == FuncOp.+) 1 else -1, curr))
           if (chain.size < 2) None
           else
-            // Find two terms with opposite signs whose DFVals are =~.
+            // Find two terms with opposite signs whose DFVals are =~ (ident-transparent).
             val indexed = chain.zipWithIndex
             val pairOpt: Option[(Int, Int)] = indexed.iterator.collectFirst {
               case ((s1, t1), i) =>
                 indexed.iterator.collectFirst {
-                  case ((s2, t2), j) if j != i && s1 == -s2 && t1 =~ t2 =>
+                  case ((s2, t2), j)
+                      if j != i && s1 == -s2 &&
+                        t1.stripTypePreservingAliases =~ t2.stripTypePreservingAliases =>
                     (i, j)
                 }
             }.flatten
diff --git a/core/src/test/scala/CoreSpec/DFBoolOrBitSpec.scala b/core/src/test/scala/CoreSpec/DFBoolOrBitSpec.scala
index 6be6e613d..9446c191c 100644
--- a/core/src/test/scala/CoreSpec/DFBoolOrBitSpec.scala
+++ b/core/src/test/scala/CoreSpec/DFBoolOrBitSpec.scala
@@ -126,6 +126,17 @@ class DFBoolOrBitSpec extends DFSpec:
     }
   }
 
+  // `sel` goes through the exactOp3 macro boundary, so a candidate failure is
+  // reported at the user's expression with the failing candidate's specific
+  // message (an in-body summon reported inside DFBoolOrBit.scala instead)
+  test("selection operation candidate error message and position") {
+    val bl = Boolean <> VAR
+    val bt = Bit <> VAR
+    val err = compiletime.testing.typeCheckErrors("""val x = bl.sel("1", bt)""").last
+    assertEquals(err.message, "Unsupported value of type `\"1\"` for DFHDL receiver type `Bit`.")
+    assertEquals(err.column, 8)
+  }
+
   test("Scala Boolean at the LHS of a logical op with a DFHDL value"):
     assertPluginError(
       "Unsupported Scala Boolean primitive at the LHS of `&&` with a DFHDL value.\nConsider switching positions of the arguments."
diff --git a/core/src/test/scala/CoreSpec/DFDecimalSpec.scala b/core/src/test/scala/CoreSpec/DFDecimalSpec.scala
index bdc19d34c..3f03f93be 100644
--- a/core/src/test/scala/CoreSpec/DFDecimalSpec.scala
+++ b/core/src/test/scala/CoreSpec/DFDecimalSpec.scala
@@ -808,6 +808,62 @@ class DFDecimalSpec extends DFSpec:
       s8 + bigUnsigned
     }
   }
+  test("Carry ops with wildcard Int operands") {
+    val u8 = UInt(8) <> VAR
+    val s8 = SInt(8) <> VAR
+    val param: Int <> CONST = 10
+
+    // A wildcard `Int` parameter adapts to the bit-accurate operand's sign and width,
+    // so `+^`/`-^` widen that operand's width by one bit (instead of promoting the
+    // parameter to a 32-bit signed value)
+    val c1: UInt[9] <> CONST = d"8'22" +^ param
+    assertEquals(c1, d"9'32")
+    val c2: UInt[9] <> CONST = param +^ d"8'22"
+    assertEquals(c2, d"9'32")
+    val c3: UInt[9] <> CONST = d"8'22" -^ param
+    assertEquals(c3, d"9'12")
+    val c4: UInt[9] <> CONST = param -^ d"8'3"
+    assertEquals(c4, d"9'7")
+    val c5: SInt[9] <> CONST = sd"8'22" +^ param
+    assertEquals(c5, sd"9'32")
+    // Carry mul with a wildcard parameter doubles the bit-accurate operand's width
+    val c6: UInt[16] <> CONST = d"8'22" *^ param
+    assertEquals(c6, d"16'220")
+    val c7: UInt[16] <> CONST = param *^ d"8'22"
+    assertEquals(c7, d"16'220")
+    val c8: SInt[16] <> CONST = sd"8'22" *^ param
+    assertEquals(c8, sd"16'220")
+    // Unsized `d"$param"` binding and parameter expressions adapt the same way
+    val c9: UInt[9] <> CONST = d"8'22" +^ d"$param"
+    assertEquals(c9, d"9'32")
+    val c10: UInt[9] <> CONST = d"8'22" +^ (param + 2)
+    assertEquals(c10, d"9'34")
+
+    // Both-Int carry ops are rejected: there is no bit-accurate operand to widen against
+    val param2: Int <> CONST = 3
+    val bothIntErr =
+      "Carry operations require at least one bit-accurate operand (`UInt`/`SInt`), but both operands are `Int` values."
+    assertCompileError(bothIntErr)("""param +^ param2""")
+    assertCompileError(bothIntErr)("""param -^ param2""")
+    assertCompileError(bothIntErr)("""param *^ param2""")
+    assertCompileError(bothIntErr)("""3 +^ param""")
+    assertCompileError(bothIntErr)("""param *^ 3""")
+    assertCompileError(bothIntErr)("""3 +^ 5""")
+
+    // The wildcard parameter must fit the bit-accurate operand
+    assertRuntimeErrorLog(
+      "Wildcard `Int` value width (10) is larger than the bit-accurate value width (8)."
+    ) {
+      val bigVal: Int <> CONST = 1000
+      u8 +^ bigVal
+    }
+    assertRuntimeErrorLog(
+      "Wildcard `Int` value is negative and cannot adapt to an unsigned bit-accurate value."
+    ) {
+      val negVal: Int <> CONST = -1
+      u8 +^ negVal
+    }
+  }
   test("d\"\" unsigned-only interpolation") {
     // d"" produces unsigned UInt constants
     assertEquals(d"0", d"1'0")
@@ -876,6 +932,9 @@ class DFDecimalSpec extends DFSpec:
          |u12 := (u8 *^ u8).resize(12)
          |u9 := (u8 + u8) +^ u8
          |u9 := (u8 + u8 + u8) +^ u8
+         |u10 := ((u8 + u8) +^ d"8'1").resize(10)
+         |u10 := ((u8 + u8b + u8) +^ d"8'1").resize(10)
+         |s9 := (s8 + s8) +^ sd"8'1"
          |""".stripMargin
     } {
       // Basic carry promotion for +
@@ -905,6 +964,33 @@ class DFDecimalSpec extends DFSpec:
       u9 := u8 + u8 + u8
       // carry promotion with 4 arguments
       u9 := u8 + u8 + u8 + u8
+      // Implicit-Int chain to a wider target: the outer op is promoted to carry
+      // under the target-width context, so no Verilog-semantics divergence remains
+      // (issue #453) and the promotion is visible in the printed code
+      u10 := u8 + u8 + 1
+      u10 := u8 + u8b + u8 + 1
+      s9 := s8 + s8 + 1
+    }
+  }
+  test("Arithmetic auto-carry promotion through sign conversion") {
+    val u2 = UInt(2) <> VAR
+    val s8 = SInt(8) <> VAR
+    val s9 = SInt(9) <> VAR
+    assertCodeString {
+      """|s8 := sd"8'0" - (d"2'3" *^ u2).signed.resize(8)
+         |s8 := s8 - (d"2'3" *^ u2).signed.resize(8)
+         |s9 := (d"2'3" *^ u2).signed.resize(8) +^ s8
+         |""".stripMargin
+    } {
+      // The unsigned narrow chain is promoted BEFORE the sign conversion the signed
+      // sibling forces, so the widening happens ahead of the conversion instead of the
+      // conversion pinning the chain at its narrow width
+      s8 := sd"8'0" - 3 * u2
+      s8 := s8 - 3 * u2
+      // The commutative sign alignment wraps the chain in a `.signed` alias before the
+      // conversion; the promotion unwraps it and re-applies the conversion on top,
+      // keeping the written operand order
+      s9 := 3 * u2 + s8
     }
   }
   test("Int32 arithmetic") {
@@ -972,11 +1058,11 @@ class DFDecimalSpec extends DFSpec:
     // Should NOT warn: (a + b) >> 2 — no implicit Int in the + chain
     val t2d = (a + b) >> 2
 
-    // Should warn: wider target with implicit Int in chain
+    // Should NOT warn: wider target with implicit Int in chain - the chain is
+    // emitted under the target-width context (size cast), so it is bit-exact
+    // with Verilog's 32-bit evaluation and truncation (issue #453)
     val sum = UInt(10) <> VAR
-    assertRuntimeWarningLog(warnMsg) {
-      sum := a + b + c + d + 1
-    }
+    sum := a + b + c + d + 1
 
     // Should NOT warn: wider target but explicit literal
     sum := a + b + c + d + d"1"
@@ -984,10 +1070,8 @@ class DFDecimalSpec extends DFSpec:
     // Should NOT warn: wider target but single op, carry promotion handles it
     sum := u8 + 1
 
-    // Should warn: wider target with chain, intermediate overflow
-    assertRuntimeWarningLog(warnMsg) {
-      sum := u8 + u8 + 1
-    }
+    // Should NOT warn: wider target with chain - same target-width context
+    sum := u8 + u8 + 1
 
     // Should NOT warn: target width == expression width
     u8 := u8 + 1
@@ -1128,9 +1212,9 @@ class DFDecimalSpec extends DFSpec:
     val arg = 10000
     val errMsg =
       "Wildcard `Int` value width (14) is larger than the bit-accurate value width (8)."
-    assertRuntimeErrorLog(errMsg, 43, 59)(cnt := cnt + arg)
-    assertRuntimeErrorLog(errMsg, 43, 67)(cnt := cnt + (cnt + arg))
-    assertRuntimeErrorLog(errMsg, 43, 65)(cnt := cnt + arg + cnt)
+    assertRuntimeErrorLog(errMsg, 50, 59)(cnt := cnt + arg)
+    assertRuntimeErrorLog(errMsg, 50, 66)(cnt := cnt + (cnt + arg))
+    assertRuntimeErrorLog(errMsg, 50, 65)(cnt := cnt + arg + cnt)
     assertRuntimeErrorLog(errMsg, 69, 78) { val x: Bits[8] <> VAL = cnt + arg }
   }
 
diff --git a/core/src/test/scala/CoreSpec/DFEnumSpec.scala b/core/src/test/scala/CoreSpec/DFEnumSpec.scala
index 0859e030d..6a312cb25 100644
--- a/core/src/test/scala/CoreSpec/DFEnumSpec.scala
+++ b/core/src/test/scala/CoreSpec/DFEnumSpec.scala
@@ -110,4 +110,30 @@ class DFEnumSpec extends DFSpec:
     assert((e0 != BinEnum.One).toScalaBoolean)
     assert((e1 != BinEnum.Zero).toScalaBoolean)
   }
+
+  test("Enum to UInt conversion") {
+    // the encoding value at the enum's width, for every encoding kind
+    val e1: MyEnum1 <> CONST = MyEnum1.Baz
+    assertEquals(e1.uint, d"2'2")
+    val e2: MyEnum2 <> CONST = MyEnum2.Bar
+    assertEquals(e2.uint, d"5'21")
+    val e3: MyEnum3 <> CONST = MyEnum3.Baz
+    assertEquals(e3.uint, d"3'4")
+    val e4: MyEnum4 <> CONST = MyEnum4.Baz
+    assertEquals(e4.uint, d"2'3")
+    val e5: MyEnum5 <> CONST = MyEnum5.Foo
+    assertEquals(e5.uint, d"8'200")
+    val eb: BinEnum <> CONST = BinEnum.One
+    assertEquals(eb.uint, d"1'1")
+    // the conversion is composed as `.bits.uint`, which is also how it prints
+    assertCodeString {
+      """|val x = MyEnum1 <> VAR
+         |val u = x.bits.uint
+         |""".stripMargin
+    } {
+      val x = MyEnum1 <> VAR
+      val u = x.uint
+      u.verifyValOf[UInt[2]]
+    }
+  }
 end DFEnumSpec
diff --git a/core/src/test/scala/CoreSpec/SameWidthArithSpec.scala b/core/src/test/scala/CoreSpec/SameWidthArithSpec.scala
index 6bfc7b88c..fa5787106 100644
--- a/core/src/test/scala/CoreSpec/SameWidthArithSpec.scala
+++ b/core/src/test/scala/CoreSpec/SameWidthArithSpec.scala
@@ -31,6 +31,51 @@ class SameWidthArithSpec extends NoDFCSpec:
     )
   }
 
+  // An unrolled accumulation over a parametric width grows its result width as a
+  // left-nested `max` chain (`((16 max W) max W) max W`). `SimplifyFunc.MaxMinChainAbsorb`
+  // collapses the repeated operand, so the chain stays minimal (`16 max W`). Design
+  // parameters are used since they stay symbolically opaque (a local `Int <> CONST`
+  // has known data and folds through `MaxMinWithOffset` instead).
+  // A named `val` over a collapsed simplification result wraps it in a named Ident (never a
+  // meta restamp of the underlying anonymous member; issue #449), and the simplifications see
+  // THROUGH such idents: the chain absorb and the self-cancellation below only fire when
+  // `M`/`E` dereference to the expressions they name.
+  test("simplifications see through named intermediates (idents)") {
+    class Top(val W: Int <> CONST = 11) extends DFDesign:
+      val M: Int <> CONST = 16 max W max W // absorbed, so `M` idents `16 max W`
+      val E: Int <> CONST = W max W // collapsed, so `E` idents `W`
+      val v = Int <> VAR
+      v := M max W // absorbs through the `M` ident
+      v := E - W // cancels through the `E` ident
+    assertNoDiff(
+      codeString(Top()),
+      """|class Top(val W: Int <> CONST = 11) extends DFDesign:
+         |  val M: Int <> CONST = 16 max W
+         |  val E: Int <> CONST = W
+         |  val v = Int <> VAR
+         |  v := M
+         |  v := 0
+         |end Top""".stripMargin
+    )
+  }
+
+  test("a repeated max/min chain over a design parameter is absorbed") {
+    class Top(val W: Int <> CONST = 11) extends DFDesign:
+      val v = Int <> VAR
+      v := 16 max W max W max W
+      v := 1 min W min W
+      v := W max 5 max W
+    assertNoDiff(
+      codeString(Top()),
+      """|class Top(val W: Int <> CONST = 11) extends DFDesign:
+         |  val v = Int <> VAR
+         |  v := 16 max W
+         |  v := 1 min W
+         |  v := W max 5
+         |end Top""".stripMargin
+    )
+  }
+
   test("a same-width sum has its operands' own type, without reduce") {
     class Top(val BIN_WIDTH: Int <> CONST = 11) extends EDDesign:
       val din = Bits(BIN_WIDTH * 2) <> IN
diff --git a/devdocs/elaboration-caching.md b/devdocs/elaboration-caching.md
index f5e3395f8..e5a9aa64f 100644
--- a/devdocs/elaboration-caching.md
+++ b/devdocs/elaboration-caching.md
@@ -149,6 +149,21 @@ like a live instantiation, so a design used by several parents is loaded once an
 elaboration of the same key. Embedding child bodies would duplicate every shared descendant, once per
 adopting parent.
 
+An entry must be SELF-CONTAINED (`SubDesignEntry.isSelfContained`): every ref its members emit
+resolves in its refTable, and every refTable binding target re-unites, by value, with one of its
+members. The value half is not implied by the key half: elaboration can leave a binding whose
+target object was removed from the member list after the binding was made (issue #449: a
+merge-absorbed intermediate Func rebound through a still-live front-end handle). Such a "ghost" is
+harmless in its own run, whose refTable still resolves the tokens the ghost emits, but adoption
+re-mints tokens for members only, so a ghost's tokens dangle in the loading run. The contract is a
+SANITY-LEVEL check (asserted in the cache specs; `SanityCheck.refCheck` reports the underlying
+defect as "Ref exists for a removed member" in debug/spec runs), deliberately NOT evaluated on the
+production store/lookup path: a ghost-free elaboration is guaranteed by construction (operation
+simplifications never revise or remove anonymous members; unread debris is swept once at the end
+of each design, `DesignContext.sweepUnreadAnons`), and only a DFHDL bug or a dirty dev loop
+(uncommitted DFHDL edits under an unchanged version; `clearDFHDL` territory) can produce a
+violating entry.
+
 Storing requires every child to be a stored entry itself: a keyless child (an impure design, or a
 class the plugin could not guard) cannot be referenced, so its parent is not storable either. Children
 end before their parents, so this simply propagates up the tree.
@@ -195,7 +210,8 @@ per-run mutable caches, so two elaborations must never adopt the same member obj
 
 Writes go through a temp file and an atomic move, so parallel test forks writing the same key stay
 consistent. A store that fails is not an error (the run simply stays live), and a corrupt entry is
-just a miss.
+just a miss ("corrupt" meaning a failed parse; structural validation is deliberately not on this
+path, see the self-containment note above).
 
 The full content key is `<code digest of the declaring class>|<localKey>`.
 
diff --git a/docs/transitioning/from-verilog/index.md b/docs/transitioning/from-verilog/index.md
index 9d57a659a..8aa89e11e 100644
--- a/docs/transitioning/from-verilog/index.md
+++ b/docs/transitioning/from-verilog/index.md
@@ -952,7 +952,7 @@ See [Arithmetic Operations][arithmetic-ops] and [Carry Arithmetic][carry-ops] fo
     type: verilog
 In Verilog, unsized integer literals are 32-bit. When combined with narrower signals, the wider literal causes the entire expression to evaluate at 32-bit width via context-dependent propagation. This prevents intermediate overflow in expressions like `(a + b + c + d) / 4`.
 
-In DFHDL, Scala `Int` literals are implicitly converted to minimum-width bit-accurate types (e.g., `4` becomes `UInt[3]`). Each arithmetic operation independently uses the LHS width, so intermediate results can overflow before reaching a division, shift, comparison, or wider-target assignment.
+In DFHDL, Scala `Int` literals are implicitly converted to minimum-width bit-accurate types (e.g., `4` becomes `UInt[3]`). Each arithmetic operation independently uses the LHS width, so intermediate results can overflow before reaching a division, shift, or comparison. (An assignment to a wider target is unaffected: the chain is automatically promoted to evaluate at the target width, matching Verilog.)
 
 DFHDL detects this pattern at elaboration and issues a warning. See [Implicit Scala `Int` and Verilog-semantics mismatch][arithmetic-ops] for the full list of warning triggers.
 
diff --git a/docs/user-guide/type-system/index.md b/docs/user-guide/type-system/index.md
index f4b882e9e..739feacf4 100755
--- a/docs/user-guide/type-system/index.md
+++ b/docs/user-guide/type-system/index.md
@@ -1262,7 +1262,7 @@ d"width'dec"
 - If specified, the output is padded with zeros
 - Returns `UInt[W]`, where `W` is the width in bits
 - An error occurs if the specified width is less than required to represent the value
-- When used with a DFHDL `Int` parameter, the interpolation binds it as unsigned
+- When used with a DFHDL `Int` parameter and an explicit or parametric width, the interpolation binds the parameter as an unsigned value of that width. Without a width, the parameter passes through unchanged and remains a [wildcard `Int` value][wildcard-ops].
 
 ```scala
 d"0"           // UInt[1], value = 0
@@ -1270,7 +1270,7 @@ d"255"         // UInt[8], value = 255
 d"8'42"        // UInt[8], value = 42
 d"1,023"       // UInt[10], value = 1023
 d"1_000"       // UInt[10], value = 1000
-d"$param"      // UInt[Int], unsigned binding of Int parameter
+d"$param"      // Int, parameter passes through as a wildcard value
 d"8'$param"    // UInt[8], unsigned binding with explicit width
 d"${w}'$param" // UInt[w.type], unsigned binding with parametric width
 ```
@@ -2260,7 +2260,7 @@ s8 := -u8
 
 ### Wildcard `Int` Values {#wildcard-ops}
 
-Both Scala `Int` values and DFHDL `Int` parameters (`Int <> CONST`) act as **wildcards** when used in operations with bit-accurate `UInt` or `SInt` values. The wildcard `Int` value adapts to the bit-accurate value's sign and width. If the wildcard `Int` value does not fit in the bit-accurate value's range or has incompatible sign, an error is generated.
+Both Scala `Int` values and DFHDL `Int` parameters (`Int <> CONST`) act as **wildcards** when used in operations with bit-accurate `UInt` or `SInt` values. The wildcard `Int` value adapts to the bit-accurate value's sign and width. If the wildcard `Int` value does not fit in the bit-accurate value's range or has incompatible sign, an error is generated. One exception: in [carry operations][carry-ops] a Scala `Int` operand contributes its value's minimal width instead of adapting, while a DFHDL `Int` parameter adapts as usual.
 
 ```scala
 val u8 = UInt(8) <> VAR
@@ -2355,6 +2355,10 @@ u9  := u8 + u8   // promoted to carry addition (width 9), exact fit
 u16 := u8 * u8   // promoted to carry multiplication (width 16), exact fit
 u12 := u8 * u8   // promoted to carry multiplication (width 16), resized to 12
 
+// Implicit Int operands participate in the promotion:
+u9  := u8 + u8 + 1   // elaborates to u9 := (u8 + u8) +^ d"8'1"
+u12 := u8 + u8 + 1   // elaborates to u12 := ((u8 + u8) +^ d"8'1").resize(12)
+
 // Named expressions are NOT promoted:
 val sum = u8 + u8  // UInt[8], named value
 u9 := sum          // resized from 8 to 9, no carry promotion
@@ -2421,25 +2425,19 @@ val t10a = (a + b + d"1'0") >> 1        // OK: 0 is explicit
 val t10c = (a +^ b +^ 0) >> 1           // OK: carry chain cannot overflow
 ```
 
-**4. Assignment to wider target with implicit `Int` in the chain:**
-An anonymous expression assigned to a wider target contains both an implicit `Int` and sub-32-bit `+`/`-`/`*` operations.
-```scala
-val sum = UInt(10) <> VAR
-sum := a + b + 1                        // WARNING: + 1 widens to 32-bit in Verilog, not in DFHDL
-val cnt = UInt(8) <> VAR
-cnt := cnt + 1                          // OK: same-width target, modular truncation matches
-// Accept overflow: replace the implicit Int with a bit-accurate literal
-sum := a + b + d"1"                     // OK: 1 is explicit
-// Prevent overflow: widen the chain with carry to match the wider target
-sum := a +^ b +^ 1                      // OK: carry chain widens result before assignment
-```
-
 **No warning** is issued when:
 
 - The expression uses carry operations (`+^`, `-^`, `*^`), which widen the result.
 - The integer constant is an explicit bit-accurate literal (e.g., `d"3'4"`).
 - The bit-accurate expression width is already 32 bits or wider.
-- The implicit `Int` is only used in modular operations (`+`, `-`, `*`) assigned to a same-width target.
+- The implicit `Int` is only used in modular operations (`+`, `-`, `*`) that feed an assignment. A same-width target wraps identically in both languages, and a wider target promotes the chain to evaluate at the target width (see the automatic carry promotion above), matching the context Verilog's assignment provides; truncation to the target width commutes with `+`/`-`/`*`, so the two evaluations agree for every input.
+```scala
+val sum = UInt(10) <> VAR
+// OK: promoted to carry, elaborates to sum := ((a + b) +^ d"8'1").resize(10)
+sum := a + b + 1
+val cnt = UInt(8) <> VAR
+cnt := cnt + 1                          // OK: same-width target, modular truncation matches
+```
 ///
 
 ### Carry Arithmetic (`+^`, `-^`, `*^`) {#carry-ops}
@@ -2470,6 +2468,8 @@ Carry operations widen the result to prevent overflow. Mixed signedness is allow
 | `UInt[LW]` | `SInt[RW]` | `SInt[LW + 1 + RW]` |
 ///
 
+**Wildcard `Int` operands:** at least one operand must be bit-accurate; a carry operation between two `Int` values is a compile-time error. A Scala `Int` operand contributes its value's minimal width to the tables above. A DFHDL `Int` parameter (`Int <> CONST`) instead [adapts][wildcard-ops] to the bit-accurate operand's sign and width, so `+^`/`-^` widen that operand by one bit and `*^` doubles its width.
+
 ```scala
 val u8 = UInt(8) <> VAR
 
@@ -2490,6 +2490,16 @@ val r4 = 100 *^ u8          // UInt[15]
 val s8 = SInt(8) <> VAR
 val r5 = s8 +^ s8           // SInt[9]
 val r6 = s8 *^ s8           // SInt[16]
+
+// DFHDL Int parameter adapts to the bit-accurate operand
+val param: Int <> CONST = 3
+val r7 = u8 +^ param        // UInt[9]  (param adapts to UInt[8], carry widens to 9)
+val r8 = u8 *^ param        // UInt[16] (param adapts to UInt[8], product doubles to 16)
+val r9 = s8 +^ param        // SInt[9]  (param adapts to SInt[8])
+
+// error: Carry operations require at least one bit-accurate
+// operand (`UInt`/`SInt`), but both operands are `Int` values.
+val e1 = param +^ 1
 ```
 
 
diff --git a/internals/src/main/scala/dfhdl/internals/Exact.scala b/internals/src/main/scala/dfhdl/internals/Exact.scala
index 9164c65de..be6a997fd 100644
--- a/internals/src/main/scala/dfhdl/internals/Exact.scala
+++ b/internals/src/main/scala/dfhdl/internals/Exact.scala
@@ -475,15 +475,26 @@ private def exactOp3Macro[Op, Ctx, OutUB](
         val (mhsBindings, mhsInner) = flattenInlined(mhsExactInfo.exactExpr.asTerm)
         val (rhsBindings, rhsInner) = flattenInlined(rhsExactInfo.exactExpr.asTerm)
         val allBindings = lhsBindings ++ mhsBindings ++ rhsBindings
-        Expr.summon[ExactOp3[
+        // The op instance is searched under the ControlledMacroError trap
+        // (the DualSummonTrapError protocol): a candidate whose nested TC
+        // resolution fails through a reporting fallback macro then ABORTS,
+        // its specific message captured, instead of resolving with a stray
+        // `compiletime.error` spliced into the instance, which would later
+        // be reported at the splice's library-internal position.
+        ControlledMacroError.activate()
+        val summoned = Expr.summonOrError[ExactOp3[
           Op,
           Ctx,
           OutUB,
           lhsExactInfo.Underlying,
           mhsExactInfo.Underlying,
           rhsExactInfo.Underlying
-        ]] match
-          case Some(expr) =>
+        ]]
+        // read before deactivate clears the trapped message
+        val lastError = ControlledMacroError.getLastMacroAbortError
+        ControlledMacroError.deactivate()
+        summoned match
+          case Right(expr) =>
             val appTerm = ascribeWidenedType('{
               $expr(
                 ${ lhsInner.asExpr },
@@ -497,8 +508,13 @@ private def exactOp3Macro[Op, Ctx, OutUB](
                 case Inlined(_, Nil, inner) => inner
                 case t                      => t
               Block(allBindings, innerTerm).asExprOf[OutUB]
-          case None =>
-            ControlledMacroError.report("Unsupported argument types for this operation.")
+          case Left(_) =>
+            // reported at the macro expansion position: the user's expression
+            report.errorAndAbort(
+              if (lastError.nonEmpty) lastError
+              else "Unsupported argument types for this operation.",
+              Position.ofMacroExpansion
+            )
         end match
       }
     }
diff --git a/lib/src/test/scala/ElaborationChecksSpec.scala b/lib/src/test/scala/ElaborationChecksSpec.scala
index ebae8fe93..f05980cb9 100644
--- a/lib/src/test/scala/ElaborationChecksSpec.scala
+++ b/lib/src/test/scala/ElaborationChecksSpec.scala
@@ -1092,4 +1092,464 @@ class ElaborationChecksSpec extends DesignSpec:
           |To Fix: split the loop so that the shared-variable write is in a purely-sequential loop.
           |""".stripMargin
     )
+
+  // `sel` constructs its selection Func through a trydf-wrapped runtime helper, so a
+  // candidate width mismatch must surface as a positioned elaboration error (and not as
+  // an escaping derived-error exception that aborts elaboration).
+  test("DFBoolOrBit sel candidate width checks"):
+    object Test:
+      @top(false) class SelFixed extends EDDesign:
+        val c = Bit <> IN
+        val a = UInt(8) <> IN
+        val y = UInt(8) <> OUT
+        // a runtime Scala Int, so the candidate width check runs at elaboration
+        // (a literal would already be rejected at compile time)
+        val arg = 512
+        y <> c.sel(a, arg)
+      end SelFixed
+      @top(false) class SelParam(val W: Int <> CONST = 14) extends EDDesign:
+        val c = Bit <> IN
+        val b = UInt(W) <> IN
+        val y = UInt(16) <> OUT
+        private var acc: UInt[Int] <> VAL = d"16'0"
+        for (_ <- 0 until 3) acc = acc + b
+        y <> c.sel(acc, d"16'0")
+      end SelParam
+    end Test
+    import Test.*
+    assertElaborationErrors(SelFixed())(
+      s"""|Elaboration errors found!
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1108:9 - 1108:27
+          |Hierarchy: SelFixed
+          |Operation: `apply`
+          |Message:   The applied RHS value width (10) is larger than the LHS variable width (8).""".stripMargin
+    )
+    // the accumulated width is a `max` chain the repeated-operand absorption keeps
+    // minimal (`16 max W`), and the width-fit check eliminates the symbolic max operand,
+    // so `16 max W >= 16` decides as `16 >= 16` and the parametric variant is accepted
+    SelParam()
+
+  test("disjoint parameter-dependent slice connections are accepted"):
+    object Test:
+      @top(false) class SliceParam(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W * 2) <> IN
+        val o = Bits(W * 2) <> OUT
+        o.lsbitsAt(0, W) <> i.lsbitsAt(0, W)
+        o.lsbitsAt(W, W) <> i.lsbitsAt(W, W)
+      end SliceParam
+      @top(false) class SliceLoop(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W * 3) <> IN
+        val o = Bits(W * 3) <> OUT
+        for (k <- 0 until 3)
+          o.lsbitsAt(k * W, W) <> i.lsbitsAt(k * W, W)
+      end SliceLoop
+      @top(false) class SliceHiLo(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W * 2) <> IN
+        val o = Bits(W * 2) <> OUT
+        o(W - 1, 0) <> i(W - 1, 0)
+        o(2 * W - 1, W) <> i(2 * W - 1, W)
+      end SliceHiLo
+      @top(false) class SliceParamHigh(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W) <> IN
+        val o = Bits(W) <> OUT
+        o(W - 1, 1) <> i(W - 1, 1)
+        o(0, 0) <> i(0, 0)
+      end SliceParamHigh
+      @top(false) class VecCellRanges(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W) X 4 <> IN
+        val o = Bits(W) X 4 <> OUT
+        o(0, 1) <> i(0, 1)
+        o(2, 3) <> i(2, 3)
+      end VecCellRanges
+      class VecSrc(val W: Int <> CONST = 4) extends EDDesign:
+        val q = Bits(W) <> OUT
+        q <> all(0)
+      @top(false) class VecElems(val W: Int <> CONST = 4) extends EDDesign:
+        val v = Bits(W) X 3 <> VAR
+        val o = Bits(W) <> OUT
+        for (k <- 0 until 3)
+          val s = VecSrc(W = W)
+          v(k) <> s.q
+        o <> v(0)
+      end VecElems
+      @top(false) class ProcConnMix(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W * 2) <> IN
+        val o = Bits(W * 2) <> OUT
+        process(all):
+          o.lsbitsAt(0, W) := i.lsbitsAt(0, W)
+        o.lsbitsAt(W, W) <> i.lsbitsAt(W, W)
+      end ProcConnMix
+    end Test
+    import Test.*
+    SliceParam()
+    SliceLoop()
+    SliceHiLo()
+    SliceParamHigh()
+    VecCellRanges()
+    VecElems()
+    ProcConnMix()
+
+  test("sub-design parameter-dependent slices resolve through applied parameters"):
+    object Test:
+      class MixChild(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W * 2) <> IN
+        val o = Bits(W * 2) <> OUT
+        o(3, 0) <> i(3, 0)
+        o(2 * W - 1, W) <> i(2 * W - 1, W)
+      end MixChild
+      @top(false) class MixParent extends EDDesign:
+        val i = Bits(8) <> IN
+        val o = Bits(8) <> OUT
+        val c = MixChild(4)
+        c.i <> i
+        o <> c.o
+      end MixParent
+    import Test.*
+    import dfhdl.compiler.stages.getCompiledCodeString
+    // the backend printing itself re-derives the connectivity on the flat DB, so the
+    // compiled code string (not just elaboration) is part of this regression
+    assertNoDiff(
+      MixParent().getCompiledCodeString,
+      """|`default_nettype none
+         |`timescale 1ns/1ps
+         |
+         |module MixChild#(parameter int W = 4)(
+         |  input  wire logic [(W * 2) - 1:0] i,
+         |  output      logic [(W * 2) - 1:0] o
+         |);
+         |  `include "dfhdl_defs.svh"
+         |  assign o[3:0] = i[3:0];
+         |  assign o[(2 * W) - 1:W] = i[(2 * W) - 1:W];
+         |endmodule
+         |
+         |`default_nettype none
+         |`timescale 1ns/1ps
+         |
+         |module MixParent(
+         |  input  wire logic [7:0] i,
+         |  output      logic [7:0] o
+         |);
+         |  `include "dfhdl_defs.svh"
+         |  logic [(4 * 2) - 1:0] c_i;
+         |  logic [(4 * 2) - 1:0] c_o;
+         |  MixChild #(
+         |    .W (4)
+         |  ) c(
+         |    .i /*<--*/ (c_i),
+         |    .o /*-->*/ (c_o)
+         |  );
+         |  assign c_i = i;
+         |  assign o   = c_o;
+         |endmodule
+         |""".stripMargin
+    )
+
+  test("overlapping parameter-dependent slice connections error"):
+    object Test:
+      @top(false) class SliceOverlap(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W * 2) <> IN
+        val o = Bits(W * 2) <> OUT
+        o.lsbitsAt(0, W) <> i.lsbitsAt(0, W)
+        o.lsbitsAt(0, W) <> i.lsbitsAt(W, W)
+      end SliceOverlap
+    import Test.*
+    assertElaborationErrors(SliceOverlap())(
+      s"""|Elaboration errors found!
+          |DFiant HDL connectivity error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1254:9 - 1254:45
+          |Hierarchy: SliceOverlap
+          |LHS:       o(W - 1, 0)
+          |RHS:       i((W + W) - 1, W)
+          |Message:   Found multiple connections write to the same variable/port `SliceOverlap.o`.
+          |The previous write occurred at ${currentFilePos}ElaborationChecksSpec.scala:1253:9 - 1253:45""".stripMargin
+    )
+
+  test("unprovable parameter-dependent slice connections error"):
+    object Test:
+      @top(false) class SliceUnprovable(val W: Int <> CONST = 4) extends EDDesign:
+        val i = Bits(W * 2) <> IN
+        val o = Bits(W * 2) <> OUT
+        o(3, 0) <> i(3, 0)
+        o(2 * W - 1, W) <> i(2 * W - 1, W)
+      end SliceUnprovable
+    import Test.*
+    assertElaborationErrors(SliceUnprovable())(
+      s"""|Elaboration errors found!
+          |DFiant HDL connectivity error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1274:9 - 1274:43
+          |Hierarchy: SliceUnprovable
+          |LHS:       o((2 * W) - 1, W)
+          |RHS:       i((2 * W) - 1, W)
+          |Message:   Found a write to the same variable/port `SliceUnprovable.o` that cannot be proven to be
+          |disjoint from a previous write, because their parameter-dependent bit ranges could not be
+          |resolved. If the ranges never overlap, restructure their indexing so the compiler can relate
+          |them, or use assignments within a process instead of connections.
+          |The previous write occurred at ${currentFilePos}ElaborationChecksSpec.scala:1273:9 - 1273:27""".stripMargin
+    )
+  test("consistent assignment kinds per process are accepted"):
+    object Test:
+      @top(false) class ConsistentNB extends EDDesign:
+        val clk, rst = Bit <> IN
+        val d = Bit <> IN
+        val q = Bit <> OUT
+        process(clk.rising, rst.rising):
+          if (rst) q :== 0
+          else q :== d
+      end ConsistentNB
+      @top(false) class BlockingTemp extends EDDesign:
+        val clk = Bit <> IN
+        val a, b = Bits(8) <> IN
+        val q = Bits(8) <> OUT
+        val tmp = Bits(8) <> VAR
+        process(clk.rising):
+          tmp := a | b
+          q :== tmp
+      end BlockingTemp
+      @top(false) class SplitProcesses extends EDDesign:
+        val clk = Bit <> IN
+        val d = Bits(8) <> IN
+        val q = Bits(8) <> OUT
+        process(clk.rising):
+          q(3, 0) := d(3, 0)
+        process(clk.rising):
+          q(7, 4) :== d(7, 4)
+      end SplitProcesses
+    end Test
+    import Test.*
+    ConsistentNB()
+    BlockingTemp()
+    SplitProcesses()
+
+  test("mixed assignment kinds to one variable in one process error"):
+    object Test:
+      @top(false) class MixedWhole extends EDDesign:
+        val clk, rst = Bit <> IN
+        val d = Bit <> IN
+        val q = Bit <> OUT
+        process(clk.rising, rst.rising):
+          if (rst) q := 0
+          else q :== d
+      end MixedWhole
+      @top(false) class MixedParts extends EDDesign:
+        val clk = Bit <> IN
+        val d = Bits(8) <> IN
+        val q = Bits(8) <> OUT
+        process(clk.rising):
+          q(3, 0) := d(3, 0)
+          q(7, 4) :== d(7, 4)
+      end MixedParts
+    end Test
+    import Test.*
+    assertElaborationErrors(MixedWhole())(
+      s"""|Elaboration errors found!
+          |DFiant HDL connectivity error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1332:16 - 1332:23
+          |Hierarchy: MixedWhole
+          |LHS:       q
+          |RHS:       d
+          |Message:   Found both blocking (`:=`) and non-blocking (`:==`) assignments to the same variable/port `MixedWhole.q` within the same process.
+          |Use one assignment kind consistently for this variable inside the process.
+          |The previous write occurred at ${currentFilePos}ElaborationChecksSpec.scala:1331:20 - 1331:26""".stripMargin
+    )
+    assertElaborationErrors(MixedParts())(
+      s"""|Elaboration errors found!
+          |DFiant HDL connectivity error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1340:11 - 1340:30
+          |Hierarchy: MixedParts
+          |LHS:       q(7, 4)
+          |RHS:       d(7, 4)
+          |Message:   Found both blocking (`:=`) and non-blocking (`:==`) assignments to the same variable/port `MixedParts.q` within the same process.
+          |Use one assignment kind consistently for this variable inside the process.
+          |The previous write occurred at ${currentFilePos}ElaborationChecksSpec.scala:1339:11 - 1339:29""".stripMargin
+    )
+  test("parametric max width-fit accepted via symbolic elimination"):
+    object Test:
+      @top(false) class MaxFitNamed(val WIDTH: Int <> CONST = 14) extends RTDesign:
+        val x = UInt(WIDTH) <> IN
+        val y = UInt(16) <> IN
+        val sum = UInt(16) <> OUT
+        val xy = x + y
+        sum := xy
+      end MaxFitNamed
+      @top(false) class MaxFitAnon(val WIDTH: Int <> CONST = 14) extends RTDesign:
+        val x = UInt(WIDTH) <> IN
+        val y = UInt(16) <> IN
+        val sum = UInt(16) <> OUT
+        sum := x + y
+      end MaxFitAnon
+      @top(false) class MaxFitCarry(val WIDTH: Int <> CONST = 14) extends RTDesign:
+        val x = UInt(WIDTH) <> IN
+        val y = UInt(16) <> IN
+        val sum20 = UInt(20) <> OUT
+        sum20 := x + y
+      end MaxFitCarry
+      @top(false) class WidthIdentities(val W: Int <> CONST = 8) extends RTDesign:
+        val a = Bits(W) <> IN
+        val b = Bits(1 * W) <> OUT
+        val c = Bits(W + 0) <> OUT
+        val d = Bits(W - 0) <> OUT
+        val z = Bits(0 * W + 4) <> OUT
+        b := a
+        c := a
+        d := a
+        z := h"4'0"
+      end WidthIdentities
+    end Test
+    import Test.*
+    MaxFitNamed()
+    MaxFitAnon()
+    MaxFitCarry()
+    WidthIdentities()
+
+  test("parametric max width-fit rejections"):
+    object Test:
+      @top(false) class MaxTooNarrow(val WIDTH: Int <> CONST = 14) extends RTDesign:
+        val x = UInt(WIDTH) <> IN
+        val y = UInt(16) <> IN
+        val sum15 = UInt(15) <> OUT
+        val xy = x + y
+        sum15 := xy
+      end MaxTooNarrow
+      @top(false) class PlainSymWidth(val WIDTH: Int <> CONST = 14) extends RTDesign:
+        val x = UInt(WIDTH) <> IN
+        val sum = UInt(16) <> OUT
+        sum := x
+      end PlainSymWidth
+    import Test.*
+    assertElaborationErrors(MaxTooNarrow())(
+      s"""|Elaboration errors found!
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1412:9 - 1412:20
+          |Hierarchy: MaxTooNarrow
+          |Operation: `:=`
+          |Message:   The applied RHS value width (WIDTH max 16) is larger than the LHS variable width (15).""".stripMargin
+    )
+    assertElaborationErrors(PlainSymWidth())(
+      s"""|Elaboration errors found!
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1417:9 - 1417:17
+          |Hierarchy: PlainSymWidth
+          |Operation: `:=`
+          |Message:   The applied RHS value width (WIDTH) is undefined compared to the LHS variable width (16).""".stripMargin
+    )
+
+  test("same-named width constants are qualified in DFBits width errors"):
+    object Test:
+      @top(false) class Child(val W: Int <> CONST = 4) extends EDDesign:
+        val OUTPUT_WIDTH = W * 2
+        val o = Bits(OUTPUT_WIDTH) <> OUT
+        o <> all(0)
+      end Child
+      @top(false) class Parent(val W: Int <> CONST = 8) extends EDDesign:
+        val OUTPUT_WIDTH = W
+        val o = Bits(OUTPUT_WIDTH) <> OUT
+        val c = Child(W = 4)
+        o <> c.o
+      end Parent
+    import Test.*
+    assertElaborationErrors(Parent())(
+      s"""|Elaboration errors found!
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1448:9 - 1448:17
+          |Hierarchy: Parent
+          |Operation: `apply`
+          |Message:   The argument width (c.OUTPUT_WIDTH) is different than the receiver width (OUTPUT_WIDTH).
+          |Consider applying `.resize` to resolve this issue.
+          |
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1448:9 - 1448:17
+          |Hierarchy: Parent
+          |Operation: `apply`
+          |Message:   The argument width (OUTPUT_WIDTH) is different than the receiver width (c.OUTPUT_WIDTH).
+          |Consider applying `.resize` to resolve this issue.""".stripMargin
+    )
+
+  test("same-named width constants are qualified in DFDecimal width errors"):
+    object Test:
+      @top(false) class Child(val W: Int <> CONST = 4) extends EDDesign:
+        val OUTPUT_WIDTH = W * 2
+        val o = UInt(OUTPUT_WIDTH) <> OUT
+        o <> 0
+      end Child
+      @top(false) class Parent(val W: Int <> CONST = 8) extends EDDesign:
+        val OUTPUT_WIDTH = W
+        val o = UInt(OUTPUT_WIDTH) <> OUT
+        val c = Child(W = 4)
+        o <> c.o
+      end Parent
+    import Test.*
+    assertElaborationErrors(Parent())(
+      s"""|Elaboration errors found!
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1479:9 - 1479:17
+          |Hierarchy: Parent
+          |Operation: `apply`
+          |Message:   The applied RHS value width (c.OUTPUT_WIDTH) is undefined compared to the LHS variable width (OUTPUT_WIDTH).
+          |
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1479:9 - 1479:17
+          |Hierarchy: Parent
+          |Operation: `apply`
+          |Message:   The applied RHS value width (OUTPUT_WIDTH) is undefined compared to the LHS variable width (c.OUTPUT_WIDTH).""".stripMargin
+    )
+
+  test("same-named design parameters are qualified in width errors"):
+    object Test:
+      @top(false) class Child(val W: Int <> CONST = 8) extends EDDesign:
+        val o = Bits(W) <> OUT
+        o <> all(0)
+      end Child
+      @top(false) class Parent(val W: Int <> CONST = 8) extends EDDesign:
+        val o = Bits(W) <> OUT
+        val c = Child(W = 4)
+        o <> c.o
+      end Parent
+    import Test.*
+    assertElaborationErrors(Parent())(
+      s"""|Elaboration errors found!
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1506:9 - 1506:17
+          |Hierarchy: Parent
+          |Operation: `apply`
+          |Message:   The argument width (c.W) is different than the receiver width (W).
+          |Consider applying `.resize` to resolve this issue.
+          |
+          |DFiant HDL elaboration error!
+          |Position:  ${currentFilePos}ElaborationChecksSpec.scala:1506:9 - 1506:17
+          |Hierarchy: Parent
+          |Operation: `apply`
+          |Message:   The argument width (W) is different than the receiver width (c.W).
+          |Consider applying `.resize` to resolve this issue.""".stripMargin
+    )
+
+  test("Verilog-semantics warning with parametric widths"):
+    object Test:
+      @top(false) class ParW(val CORDW: Int <> CONST = 16) extends EDDesign:
+        val err = SInt(CORDW + 1) <> IN
+        val dy = SInt(CORDW + 1) <> IN
+        val t = 2 * err >= dy
+      end ParW
+      @top(false) class ParWDiv(val CORDW: Int <> CONST = 16) extends EDDesign:
+        val a = UInt(CORDW) <> IN
+        val b = UInt(CORDW) <> IN
+        val t = (a + b) / 4
+      end ParWDiv
+    import Test.*
+    val warnMsg =
+      """|Implicit Scala/DFHDL Int conversion may produce different results than Verilog.
+         |In Verilog, integer literals are 32-bit, which can widen intermediate arithmetic.
+         |In DFHDL, Int literals are converted to minimum bit-accurate width.
+         |Use carry operations (+^, -^, *^) or explicit bit-accurate literals (d"W'V").""".stripMargin
+    def assertWarns(dsn: dfhdl.core.Design, expected: String*): Unit =
+      val warns = dsn.dfc.getWarnings.map(_.dfMsg)
+      assertEquals(warns.length, expected.length)
+      warns.lazyZip(expected).foreach(assertNoDiff(_, _))
+    // the parametric width resolves through the design parameter's applied (or default)
+    // value at elaboration, so the warning fires exactly as with a literal width
+    assertWarns(ParW(), warnMsg)
+    assertWarns(ParWDiv(), warnMsg)
+    // a parametric width that resolves to 32 bits or wider stays suppressed
+    assertWarns(ParW(31))
+
 end ElaborationChecksSpec
diff --git a/lib/src/test/scala/issues/IssueSpec.scala b/lib/src/test/scala/issues/IssueSpec.scala
index 34952cd75..2a2c48e7a 100644
--- a/lib/src/test/scala/issues/IssueSpec.scala
+++ b/lib/src/test/scala/issues/IssueSpec.scala
@@ -86,4 +86,6 @@ class IssuesSpec extends FunSuite:
     i147.ClockRstConnection().compile.lint
   test("i375 compiles with no exception"):
     i375.draw_line().compile
+  test("i450 compiles with no exception"):
+    i450.TopC().compile
 end IssuesSpec
diff --git a/lib/src/test/scala/issues/i450.scala b/lib/src/test/scala/issues/i450.scala
new file mode 100644
index 000000000..4fa1372ec
--- /dev/null
+++ b/lib/src/test/scala/issues/i450.scala
@@ -0,0 +1,24 @@
+package issues.i450
+
+import dfhdl.*
+
+// A `Bits` port whose width comes from a design parameter that is USED THROUGH ITS DEFAULT
+// (`new Consumer()`), tied to `all(0)` by the parent. A class parameter default is evaluated
+// inside the child's own context, so the default's literal is a child-context member; the
+// `all(0)` width resolution reaches it through the applied/default path after the child has
+// ended, and a simplification returns it in the parent's context. Applying the context meta
+// to that result by MUTATION used to crash with an internal `NoSuchElementException` (a
+// `memberTable` miss: the member belongs to the ended child context). Passing the same value
+// explicitly (`new Consumer(W = 36)`) never crashed, since the applied literal is created at
+// the call site, in the parent's context.
+class Consumer(val W: Int <> CONST = 36) extends EDDesign:
+  val i = Bits(W) <> IN
+  val o = Bits(W) <> OUT
+  o <> i
+
+@top(false) class TopC extends EDDesign:
+  val q = Bit <> OUT
+  q <> 0
+  val c = new Consumer()
+  c.i <> all(0)
+  c.o <> OPEN
diff --git a/plugin/src/main/scala/plugin/MetaContextGenPhase.scala b/plugin/src/main/scala/plugin/MetaContextGenPhase.scala
index d39bc1552..da7e78e84 100755
--- a/plugin/src/main/scala/plugin/MetaContextGenPhase.scala
+++ b/plugin/src/main/scala/plugin/MetaContextGenPhase.scala
@@ -36,6 +36,17 @@ class MetaContextGenPhase(setting: Setting) extends CommonPhase:
   val contextDefs = mutable.Map.empty[String, Tree]
   var clsStack = List.empty[TypeDef]
   var applyStack = List.empty[Apply]
+  // Enclosing `Inlined` nodes whose call is written in the compilation unit
+  // being compiled (innermost first). Trees inside a library inline expansion
+  // carry the library's own positions (often mangled for TASTy-unpickled
+  // sources), and macro-synthesized applies carry the position of the quote
+  // inside the macro's own source, so when such a tree needs a position
+  // stamp, the innermost user-code inline call is the position the user can
+  // act on.
+  var inlinedUserPosStack = List.empty[util.SrcPos]
+
+  private def isUserSourced(tree: Tree)(using Context): Boolean =
+    tree.span.exists && tree.srcPos.startPos.source == ctx.compilationUnit.source
 
   extension (tree: ValOrDefDef)(using Context)
     def needsNewContext: Boolean =
@@ -186,7 +197,9 @@ class MetaContextGenPhase(setting: Setting) extends CommonPhase:
                       metaInfo.nameOpt.isEmpty && argTree.isProxyContext &&
                       metaInfo.srcPos.startPos.source != ctx.compilationUnit.source
                     )
-                      enclosingUserSrcPos.getOrElse(metaInfo.srcPos)
+                      inlinedUserPosStack.headOption
+                        .orElse(enclosingUserSrcPos)
+                        .getOrElse(metaInfo.srcPos)
                     else metaInfo.srcPos
                   fixedApply.replaceArg(
                     argTree,
@@ -210,7 +223,17 @@ class MetaContextGenPhase(setting: Setting) extends CommonPhase:
               if (fixedApply.fun.symbol.name.toString.contains("$")) fixedApply
               // generating a new anonymous context
               else
-                fixedApply.replaceArg(argTree, argTree.setMeta(None, origApply.srcPos, None, Nil))
+                // An apply inside a library inline expansion (or synthesized
+                // by a macro, carrying the quote's own source position)
+                // points into library code; stamp it with the innermost
+                // user-code inline call position instead.
+                val srcPos =
+                  if (isUserSourced(origApply)) origApply.srcPos
+                  else
+                    inlinedUserPosStack.headOption
+                      .orElse(enclosingUserSrcPos)
+                      .getOrElse(origApply.srcPos)
+                fixedApply.replaceArg(argTree, argTree.setMeta(None, srcPos, None, Nil))
           end match
         case _ => fixedApply
     else fixedApply
@@ -488,11 +511,21 @@ class MetaContextGenPhase(setting: Setting) extends CommonPhase:
   end prepareForDefDef
 
   override def prepareForInlined(tree: Inlined)(using Context): Context =
+    if (isUserSourced(tree)) inlinedUserPosStack = tree.srcPos :: inlinedUserPosStack
     // skipping over redundant inlines that should not be used for positioning
     if (!tree.call.symbol.is(Permanent))
-      nameValOrDef(tree.expansion, EmptyValDef, tree.expansion.tpe, Some(tree.srcPos))
+      // A nested inline call within a library's own expansion carries the
+      // library position; walk its expansion with the innermost user-code
+      // inline position instead, so the context applies it reaches are
+      // stamped with a position the user can act on.
+      val walkPos = inlinedUserPosStack.headOption.getOrElse(tree.srcPos)
+      nameValOrDef(tree.expansion, EmptyValDef, tree.expansion.tpe, Some(walkPos))
     ctx
 
+  override def transformInlined(tree: Inlined)(using Context): Tree =
+    if (isUserSourced(tree)) inlinedUserPosStack = inlinedUserPosStack.drop(1)
+    tree
+
   // This is requires for situations like:
   // val (a, b) = (foo(using DFC), foo(using DFC))
   // It is desugared into: