Implementation plan and status

The isolated DbDropGuard::db vertical slice and the ground binary-operator sub-slice are implemented. Exact oracle fixtures cover both, and semantic dependency traces cover their external inputs. The broader steps remain incomplete where their checkboxes are still open.

Step 1: Completed-IR data model and finalization checks

• Introduce resolved local-field identity and explicit dereference nodes, and materialize built-in reference dereferences used by field access.
• Introduce resolved call, shared borrow, and static-trait dispatch forms needed by the first vertical slice. General coercion, substitution, and explicit error forms remain.
• Represent rigid types separately from the named, associated, and opaque AliasTy family without requiring aliases to be eagerly normalized.
• Introduce Lifetime::Dummy as the only lifetime produced by checking.
• Make successful body finalization reject unresolved names, source method calls, inference variables, adjustment recipes, and unsupported nodes.
• Add focused structural tests for completed-body invariants.

Step 2: Associated methods and DbDropGuard::db

• Give impl functions independent symbol, signature, and body queries.
• Complete the derive/item path needed to represent the local Db: Clone impl.
  • Preserve the source item and append a parsed Clone impl for the concrete non-generic struct shape used by Db.
  • Give generated derive text a distinct parse-source identity linked to the source item.
  • Resolve the generated impl's external Clone trait and expose it through trait-keyed candidate discovery.
• Supply the external Clone trait contract needed for the solver to accept and prove the generated candidate.
• Resolve Clone::clone, prove Db: Clone, and consume receiver adjustments into explicit tree nodes.
• Assert that call checking does not query the selected callee body.

Step 3: Oracle and coverage boundary

• Extend the shared reference model with resolved field owner/index identity and explicit dereference expressions.
• Adapt rustc field definitions directly into shared owner/index identity without consulting or rewriting Sage output.
• Adapt the rustc receiver adjustment used by DbDropGuard::db directly into completed dereference and shared-borrow forms without consulting or rewriting Sage output. Method owner/method substitutions and static-trait dispatch are also represented for the isolated Parse::next slice; general direct-call substitutions and adjustments remain.
• Remove paired output normalization and make pass/fail depend on byte-for-byte identity of deterministic serialized output.
• Enumerate source-written associated bodies for this slice; generated derive bodies remain outside the stated coverage boundary.
• Compare DbDropGuard::db and assert a stable semantic query trace.

Step 4: Trait-directed expression families

• Land the separate normalization design needed to represent and solve associated-type projections while preserving unnormalized alias bounds.
• Elaborate overloadable operators (including primitive operands), indexing, callable values, for, and ? into their resolved semantic operations.
  • Ground primitive and local user-defined binary operators use ordinary trait proof and associated-output normalization, materialize signature adjustments, and complete as resolved static trait calls. The binary_operators integration suite covers exact oracle agreement and cold/warm metadata dependencies.
  • Represent generic associated-output assumptions and unknown-Self candidate hints, then complete the operator matrix and the other expression families in this step.
• Add one focused fixture and query-dependency assertion per family.

Step 5: Closures and async

• Represent closure captures and nested typed bodies.
• Represent async bodies and high-level await without state-machine lowering.
• Complete the Shutdown::recv vertical slice.

Step 6: Full mini-redis library coverage

• Account for every item and body in the default-feature library target.
• Reach zero unsupported successful nodes and zero unexpected diagnostics.
• Produce byte-identical deterministic oracle output and pass focused incremental-dependency tests.