An oracle-checked method body

The external-method chapter explains why Sage produces a resolved call. This chapter explains how the same DbDropGuard::db example checks that result against rustc without teaching either emitter to imitate the other.

The fixture is a standalone Rust program under test-fixtures/oracle/mini_redis/db_drop_guard.rs. The important body remains:

#![allow(unused)]
fn main() {
impl DbDropGuard {
    fn db(&self) -> Db {
        self.db.clone()
    }
}
}

1. Check Sage's semantic path

Exact equality is insufficient if both producers accidentally omit the same body. A unit test using the same source program checks Sage's completed IR directly:

example_assert_elaborated_clone_body

This assertion establishes that body checking succeeded and that method syntax was consumed. It then walks the semantic result: a statically dispatched Clone::clone call receives a shared reference to the resolved db field, whose base explicitly dereferences the local self binding.

This test establishes the checker and elaborator path, but it does not read the oracle fixture or Sage's normalized output. The fixture therefore separately checks both projections for the source-written body and the resolved call/borrow/field/dereference shape. Both emitters omitting the same method does not count as conformance.

2. Select the same source item independently

Source-written impl methods participate in the shared output. Sage discovers them from checked impl items and excludes compiler-generated derive methods by its own parse provenance:

example_sage_source_impl_functions

The rustc emitter walks HIR impl items and independently applies the same coverage boundary using rustc expansion provenance:

example_oracle_source_impl_functions

Neither side uses the other side's item list. The exclusion is specifically for derive-generated methods; source-written methods and methods generated by other represented macros remain within the intended comparison scope.

3. Project into one shared typed tree

The two emitters begin from different internal representations:

• Sage already has a ResolvedCall with explicit dereference, field, and shared-reference nodes.
• rustc has a type-checked HIR method call plus method resolution and receiver adjustments in TypeckResults.

Each emitter minimally projects its native facts into rust-ref. For this body, both must produce the same definition identities, static trait dispatch, types, and explicit operations. The projection is per-emitter adaptation; there is no comparison-side rewrite which can erase a disagreement.

Definition-path segment kinds are part of that identity. The fixture requires the Clone::clone target to contain the exact native hierarchy:

example_exact_external_def_path

The clone module and Clone trait both occupy Rust's type namespace, but that does not make them the same kind. Each adapter obtains the kind for each definition rather than applying the leaf function kind to its ancestors.

4. Let deterministic text decide

The harness serializes the two Crate<NormalizedDef> values independently and uses byte-for-byte equality as the conformance boundary:

example_exact_oracle_comparison

If the strings differ, the JSON-tree comparison only explains where. It cannot turn structurally equal but differently ordered output—or semantically unequal output—into a pass.

For this vertical slice, each serialized output must also equal the same checked-in, reviewable JSON snapshot byte for byte:

example_exact_db_drop_guard_snapshot

This catches a coordinated adapter mistake even when rustc and Sage happen to emit the same wrong shared value. It does not adapt either output.

The complete validation chain for this example is therefore:

Rust fixture
├─ Sage parse/check/elaborate ── structural coverage ── Sage projection ── exact snapshot
└─ rustc type checking ──────────────────────────────── rustc projection ─ exact snapshot
                                                                      │
                                    deterministic serialized identity ┘

The semantic unit test catches regressions in Sage's elaborated body, while the structural checks, exact snapshot, and exact cross-emitter comparison establish this fixture's current coverage and representation boundary. The broader destination contract is specified in Oracle Test Harness.

Review packet

This example has one inspectable artifact for each review question:

Reproduce the packet with:

cargo test -p sage-test-harness clone_method_call_is_elaborated_to_a_resolved_trait_call
cargo test -p sage-test-harness clone_method_body_has_a_narrow_reusable_semantic_query_trace
cargo test -p sage-test-harness unrelated_body_edit_exposes_current_body_invalidation
cargo test -p sage-oracle-harness --test oracle_compare -- mini_redis/db_drop_guard.rs