meta.contracts.correspondence

Every Sage correspondence unit has one or more Rust locations declared through #[sage::item(...)]. Every such annotation resolves to a compatible Sage unit in its containing modeled crate. Crate and module headers, named declarations, and explicit methods are correspondence units. Multiple source locations are permitted; module markers provide source coverage but do not establish runtime execution coverage. Cargo package and target metadata determine Rust ownership.

Verification exercises missing locations, dangling annotations, wrong crates, incompatible operation kinds, multiple sites, abstract markers, Cargo library and binary roots, and declarations produced by supported generators. Arbitrary macro tokens do not establish a generated declaration’s existence.

Read in specification context · design/meta/contracts.md

Implementation

Implemented crates/sage-meta/src/correspondence.rs:361–366

sage_meta::correspondence · lib:sage_meta

#![allow(unused)]
fn main() {
    // {anchor}`meta.contracts.correspondence`
    // {anchor}`meta.book.crate_ownership`
    pub fn validate(&self, documents: &[Document]) -> Vec<Diagnostic> {
        #[derive(Clone, Copy)]
        enum Unit {
            Namespace,

}

See more source ↗

Implemented crates/sage-meta/src/workspace.rs:48–53

sage_meta::workspace · lib:sage_meta

#![allow(unused)]
fn main() {
// {anchor}`meta.contracts.correspondence`
pub fn document_namespace(documents: &[Document], document: &Document) -> Option<String> {
    match &document.header {
        crate::Header::Crate { name, .. } => Some(name.clone()),
        crate::Header::Module(path) => {
            let name = crate_source_owner(documents, Path::new(&document.file))?;

}

See more source ↗

Tests and review

Indexed tests and the implementation-completeness and test-adequacy review; no test run is implied.

Implemented sage_meta::annotations_on_unsupported_nodes_cannot_silently_disappear

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn annotations_on_unsupported_nodes_cannot_silently_disappear() {
    let index = index(
        r#"struct Container { #[sage::item(crate::Value)] field: u32 }
        #[sage::itm(crate::Root)] struct Misspelled;
    "#,
    );
    assert_eq!(index.diagnostics.len(), 2);
    assert!(index.diagnostics.iter().all(|diagnostic| {
        diagnostic
            .message
            .contains("unsupported Sage attribute or placement")
    }));
}
}

See more source ↗

Implemented sage_meta::cargo_owner_covers_both_library_and_binary_and_explicit_nested_module_paths

crates/sage-meta/tests/correspondence.rs · test:correspondence

#[test]
#[sage::test(meta.contracts.correspondence)]
fn cargo_owner_covers_both_library_and_binary_and_explicit_nested_module_paths() {
    let fixture = std::env::temp_dir().join(format!(
        "sage-correspondence-targets-{}",
        std::process::id()
    ));
    std::fs::create_dir_all(fixture.join("src/inline")).unwrap();
    std::fs::write(
        fixture.join("Cargo.toml"),
        r#"[package]
name = "fixture-package"
version = "0.0.0"
edition = "2024"
[workspace]
[lib]
name = "custom_lib_name"
[[bin]]
name = "custom-bin-name"
path = "src/main.rs"
"#,
    )
    .unwrap();
    std::fs::write(
        fixture.join("src/lib.rs"),
        r#"#[sage::item(crate)] mod r#abstract {}
        mod inline { #[path = "actual.rs"] mod nested; }
    "#,
    )
    .unwrap();
    std::fs::write(
        fixture.join("src/inline/actual.rs"),
        "#[sage::item(crate::Value)] pub struct Thing;",
    )
    .unwrap();
    std::fs::write(
        fixture.join("src/main.rs"),
        "#[sage::item(crate::Root::run)] fn main() {}",
    )
    .unwrap();
    let index = CorrespondenceIndex::load(&fixture).unwrap();
    assert_eq!(
        index.entries["fixture_package::Value"][0].file,
        "src/inline/actual.rs"
    );
    assert_eq!(
        index.entries["fixture_package::Value"][0].target,
        "lib:custom_lib_name"
    );
    assert_eq!(
        index.entries["fixture_package::Root::run"][0].target,
        "bin:custom-bin-name"
    );
    assert_eq!(
        index
            .lookup(&fixture.join("src/main.rs").to_string_lossy(), 1)
            .unwrap()
            .sage_item,
        "fixture_package::Root::run"
    );
    std::fs::remove_dir_all(fixture).unwrap();
}

See more source ↗

Implemented sage_meta::conditional_mappings_cannot_silently_pass_reverse_validation

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn conditional_mappings_cannot_silently_pass_reverse_validation() {
    for attribute in [
        "#[cfg_attr(test, sage::item(foreign::Missing))]",
        "#[cfg_attr(test, cfg_attr(feature = \"nested\", sage::item(crate::Missing)))]",
        "#[cfg_attr(test, path = \"other.rs\")]",
    ] {
        let source = format!("{VALID}\n{attribute}\nmod conditional {{}}");
        let diagnostics = index(&source).validate(&model());
        assert!(
            diagnostics
                .iter()
                .any(|diagnostic| diagnostic.message.contains("cfg_attr are unsupported")),
            "{diagnostics:?}"
        );
    }
    let source = format!("{VALID}\n#[cfg_attr(test, allow(dead_code))]\nmod unrelated {{}}");
    assert!(index(&source).validate(&model()).is_empty());
}
}

See more source ↗

Implemented sage_meta::deletion_dangling_targets_wrong_crates_and_wrong_kinds_fail

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn deletion_dangling_targets_wrong_crates_and_wrong_kinds_fail() {
    for (source, expected) in [
        (
            VALID.replace("#[sage::item(crate::Value)]", ""),
            "has no Rust",
        ),
        (
            VALID.replace("crate::Value", "crate::Missing"),
            "unknown Sage item demo::Missing",
        ),
        (
            VALID.replace("crate::Value", "foreign::Value"),
            "different crate",
        ),
        (
            VALID.replace("struct ActualValue;", "fn ActualValue() {}"),
            "incompatible Rust Function",
        ),
        (VALID.replace("crate::Value", "Value"), "start with crate"),
        (
            VALID.replace("crate::Value", "crate::Value, 42"),
            "expects one crate-qualified",
        ),
    ] {
        let diagnostics = index(&source).validate(&model());
        assert!(
            diagnostics
                .iter()
                .any(|diagnostic| diagnostic.message.contains(expected)),
            "{expected}: {diagnostics:?}"
        );
    }
}
}

See more source ↗

Implemented sage_meta::generated_declarations_reject_hidden_or_misspelled_correspondences

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn generated_declarations_reject_hidden_or_misspelled_correspondences() {
    for (attribute, expected) in [
        (
            "#[cfg_attr(feature = \"alternate\", sage::item(crate::Value))]",
            "conditional Sage annotations",
        ),
        (
            "#[cfg_attr(feature = \"outer\", cfg_attr(feature = \"inner\", sage::itm(crate::Value)))]",
            "conditional Sage annotations",
        ),
        (
            "#[sage::itm(crate::Value)]",
            "unsupported Sage attribute or placement",
        ),
        (
            "#[cfg_attr(feature = \"alternate\", path = \"other.rs\")]",
            "conditional Sage annotations",
        ),
    ] {
        for position in 0..4 {
            let mut attributes = ["", "", "", ""];
            attributes[position] = attribute;
            let source = format!(
                r#"define_kind_symbols! {{
                {} pub struct Symbol<'db> {{ data: SymbolDataPriv<'db> }}
                {} pub enum SymbolData<'db> {{ .. }}
                {{}}
                {} pub enum FnSymbol<'db> {{ Local(LocalFn<'db>), Ext(Kind::Fn) }}
                {{}}
                {} pub enum Intrinsic<'db> {{ Local(LocalIntrinsic<'db>) }}
            }}"#,
                attributes[0], attributes[1], attributes[2], attributes[3]
            );
            let index = index(&source);
            assert_eq!(
                index.diagnostics.len(),
                1,
                "{position}: {attribute}: {:?}",
                index.diagnostics
            );
            let diagnostic = &index.diagnostics[0];
            assert!(
                diagnostic.message.contains(expected),
                "{}",
                diagnostic.message
            );
            assert_eq!(
                &source[diagnostic.span.start..diagnostic.span.end],
                attribute
            );
        }
    }
}
}

See more source ↗

Implemented sage_meta::known_generator_accepts_unconditional_mapping_and_unrelated_cfg_attr

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn known_generator_accepts_unconditional_mapping_and_unrelated_cfg_attr() {
    let index = index(
        r#"define_kind_symbols! {
        #[cfg_attr(feature = "debug", derive(Debug))]
        #[sage::item(crate::Root)]
        pub struct Symbol<'db> { data: SymbolDataPriv<'db> }
        pub enum SymbolData<'db> { .. }
        {}
        #[cfg(feature = "functions")]
        #[sage::item(crate::Value)]
        pub enum FnSymbol<'db> { Local(LocalFn<'db>), Ext(Kind::Fn) }
        {}
    }"#,
    );
    assert!(index.diagnostics.is_empty(), "{:?}", index.diagnostics);
    assert!(index.entries["demo::Root"][0].macro_input);
    assert_eq!(
        index.entries["demo::Value"][0].cfg,
        ["#[cfg(feature = \"functions\")]"]
    );
}
}

See more source ↗

Implemented sage_meta::known_symbol_generator_is_parsed_but_arbitrary_macro_tokens_are_not_anchors

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn known_symbol_generator_is_parsed_but_arbitrary_macro_tokens_are_not_anchors() {
    let index = index(
        r#"define_kind_symbols! {
        #[sage::item(crate::Root)]
        pub struct Symbol<'db> { data: SymbolDataPriv<'db> }
        pub enum SymbolData<'db> { .. }
        {}
        #[sage::item(crate::Value)]
        pub enum FnSymbol<'db> { Local(LocalFn<'db>), Ext(Kind::Fn) }
        {}
        pub enum Intrinsic<'db> { Local(LocalIntrinsic<'db>) }
    }
    arbitrary! { #[sage::item(crate::Fake)] struct NotProven; }
    "#,
    );
    assert!(index.entries["demo::Root"][0].macro_input);
    assert!(index.entries["demo::Value"][0].macro_input);
    assert!(!index.entries.contains_key("demo::Fake"));
}
}

See more source ↗

Implemented sage_meta::maps_independently_named_rust_declarations_and_checks_both_directions

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn maps_independently_named_rust_declarations_and_checks_both_directions() {
    let index = index(VALID);
    assert!(
        index.validate(&model()).is_empty(),
        "{:?}",
        index.validate(&model())
    );
    let mapped = index.lookup("src/lib.rs", 9).unwrap();
    assert_eq!(mapped.sage_item, "demo::Root::run");
    assert_eq!(mapped.site.rust_path, "demo::Implementation::compute");
    assert_eq!(mapped.site.kind, RustItemKind::Method);
    assert_eq!(mapped.site.line, 8);
    assert!(matches!(
        index.lookup("another/src/lib.rs", 9),
        Err(LookupError::Missing { .. })
    ));
    assert_eq!(index.entries["demo"][0].rust_path, "demo::abstract");
}
}

See more source ↗

Implemented sage_meta::markers_are_source_coverage_not_executable_coverage

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn markers_are_source_coverage_not_executable_coverage() {
    let source = r#"
        #[sage::item(crate)]
        #[sage::item(crate::Root)]
        #[sage::item(crate::Value)]
        #[sage::item(crate::Root::run)]
        mod r#abstract {}
    "#;
    let index = index(source);
    assert!(index.validate(&model()).is_empty());
    assert!(
        index.entries["demo::Root::run"]
            .iter()
            .all(|site| !site.executable)
    );
    assert!(matches!(
        index.lookup("src/lib.rs", 6),
        Err(LookupError::Missing { .. })
    ));
}
}

See more source ↗

Implemented sage_meta::module_headers_require_correspondence_in_addition_to_the_crate_header

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn module_headers_require_correspondence_in_addition_to_the_crate_header() {
    let documents = [
        parse(
            "demo/crate.sage",
            r#"crate demo { """Fixture.""" module syntax; }"#,
        )
        .unwrap(),
        parse("demo/syntax.sage", "module crate::syntax;").unwrap(),
    ];
    let source = "#[sage::item(crate)] mod root {}\n#[sage::item(crate::syntax)] mod parser {}";
    let complete = index(source);
    assert!(complete.validate(&documents).is_empty());
    assert_eq!(
        complete.entries["demo::syntax"][0].rust_path,
        "demo::parser"
    );
    let missing = index(&source.replace("#[sage::item(crate::syntax)]", ""));
    let diagnostics = missing.validate(&documents);
    assert_eq!(diagnostics.len(), 1, "{diagnostics:?}");
    assert!(diagnostics[0].message.contains("demo::syntax"));
    assert!(diagnostics[0].message.contains("has no Rust"));
}
}

See more source ↗

Implemented sage_meta::multiple_cfg_sites_preserve_conditions_without_claiming_active_build_coverage

crates/sage-meta/tests/correspondence.rs · test:correspondence

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.correspondence)]
fn multiple_cfg_sites_preserve_conditions_without_claiming_active_build_coverage() {
    let index = index(
        r#"#[cfg(feature = "a")]
        mod first {
            #[sage::item(crate::Root::run)]
            fn chosen() {}
        }
        #[cfg(not(feature = "a"))]
        #[sage::item(crate::Root::run)]
        fn other() {}
    "#,
    );
    let sites = &index.entries["demo::Root::run"];
    assert_eq!(sites.len(), 2);
    assert!(sites[0].cfg[0].contains("feature = \"a\""));
    assert!(sites[1].cfg[0].contains("not"));
    assert_eq!(
        index.lookup("src/lib.rs", 4).unwrap().site.rust_path,
        "demo::first::chosen"
    );
}
}

See more source ↗

Review: Accepted · final_quality.

Reviewed the entire meta.contracts.correspondence claim, both associated implementation files (correspondence.rs and workspace.rs), and all eleven associated tests. This is source inspection; no tests were executed by this reviewer, and coordinator-run suite results are separate.

CorrespondenceIndex::validate builds required units for crate/module headers, named types/classes and each explicitly declared class method. document_namespace uses the modeled crate header and nearest enclosing modeled crate for module documents. Every required unit must have at least one indexed Rust site; every annotation is checked in reverse for its containing Cargo package owner, existing Sage target and compatible namespace/type/operation category. Module markers are allowed as source evidence while executable remains false; runtime lookup only accepts executable sites in the exact matching callable region. Site vectors allow multiple source locations and preserve textual cfg conditions without evaluating execution. Cargo metadata supplies package ownership and target roots/names, independent of filesystem spelling or customized Rust target names. Rust source extraction follows inline and explicit out-of-line module paths, records supported declarations and rejects misplaced/conditional correspondence attributes instead of silently dropping them.

The exact supported define_kind_symbols adapter parses structural declarations, the placeholder enum and both enum-family groups and marks their locations as macro input; arbitrary invocation token bodies are recorded as opaque rather than inspected as declarations. Captured generator syntax confirms the structural families the adapter is intended to recognize. Captured fixture index/model/VALID helpers construct actual RustSource and parsed Sage documents with independently named Rust declarations, so mapping assertions exercise the real extraction/validation paths.

All associated tests were assessed individually. maps_independently_named_rust_declarations_and_checks_both_directions validates the complete fixture and asserts operation identity, distinct Rust method path/kind/line, exact-file lookup and crate marker naming. deletion_dangling_targets_wrong_crates_and_wrong_kinds_fail checks removed evidence, unknown targets, foreign ownership, function-versus-type incompatibility, unqualified names and malformed argument syntax. module_headers_require_correspondence_in_addition_to_the_crate_header proves an explicit module is a separate required unit and asserts exactly one missing-module error after deletion. markers_are_source_coverage_not_executable_coverage accepts module markers for all units but asserts no executable site and failed runtime lookup. multiple_cfg_sites_preserve_conditions_without_claiming_active_build_coverage requires two sites with their respective conditions and the correct nested function lookup. cargo_owner_covers_both_library_and_binary_and_explicit_nested_module_paths creates a real Cargo fixture with differing package/library/binary names and an explicit nested module path, asserting file, target identities and absolute-path operation lookup.

annotations_on_unsupported_nodes_cannot_silently_disappear requires two placement/spelling diagnostics. conditional_mappings_cannot_silently_pass_reverse_validation checks direct/nested conditional Sage mappings and conditional module paths while accepting unrelated cfg_attr. known_symbol_generator_is_parsed_but_arbitrary_macro_tokens_are_not_anchors asserts the known generated sites are marked macro_input and an arbitrary macro's fake declaration is absent. known_generator_accepts_unconditional_mapping_and_unrelated_cfg_attr checks a positive known-generator case, no diagnostics and preserved cfg. generated_declarations_reject_hidden_or_misspelled_correspondences exercises four declaration positions against four problematic attribute forms, requiring exactly one appropriate diagnostic whose source span equals the offending attribute.

Together these cover the claim's explicit verification matrix: missing/dangling/wrong-crate/incompatible sites, multiple locations, abstract module markers, Cargo library/binary ownership, supported generated declarations and exclusion of arbitrary macro token evidence. The distinction between source coverage and runtime execution is preserved in both implementation and assertions. There are no associated TODO or N/A entries. No concrete defect or additional necessary source change was found; requested edits are empty.

Browse meta anchors

116 anchors

Specification anchors and declared coverage
AnchorImplementationTests
meta (116)102 Implemented24 TODO103 Implemented36 TODO
meta.anchors (22)22 Implemented21 Implemented12 TODO
anchor_pagesImplementedImplementedTODO
book_explorerImplementedImplementedTODO
canonical_sourcesImplementedImplementedTODO
meta.anchors.content (7)7 Implemented7 Implemented
blocksImplementedImplemented
explicit_endImplementedImplemented
headingImplementedImplemented
literal_syntaxImplementedImplemented
next_anchorImplementedImplemented
source_endImplementedImplemented
unmatched_endImplementedImplemented
context_navigationImplementedImplementedTODO
evidence_statusImplementedImplementedTODO
explorer_navigationImplementedTODO
implementation_coverageImplementedImplementedTODO
implementation_referencesImplementedImplementedTODO
placeholder_statusImplementedImplementedTODO
point_excerptsImplementedImplementedTODO
region_balanceImplementedImplemented
region_excerptsImplementedImplementedTODO
test_coverageImplementedImplemented
test_referencesImplementedImplemented
unique_namesImplementedImplementedTODO
meta.book (21)10 Implemented18 TODO12 Implemented18 TODO
anchor_movesImplementedTODOImplementedTODO
authorityImplementedTODOImplementedTODO
browser_deliveryTODOImplementedTODO
browser_dependenciesTODOTODO
browser_rust_sourceTODOTODO
browser_searchTODOTODO
browser_serveTODOTODO
browser_structureTODOTODO
chapter_namesImplementedTODOImplementedTODO
crate_ownershipImplementedImplemented
crates_landingImplementedImplemented
entity_linksTODOTODO
index_groupsImplementedTODOImplementedTODO
index_namespace_pagesImplementedImplemented
index_rowsImplementedTODOImplementedTODO
index_statusImplementedTODOImplementedTODO
rfd_changesTODOTODO
sage_chaptersTODOImplementedTODO
self_descriptionTODOTODO
shared_modelImplementedTODOImplementedTODO
source_rolesTODOTODO
meta.contracts (4)4 Implemented3 TODO4 Implemented3 TODO
cache_invocationsImplementedTODOImplementedTODO
correspondenceImplementedImplemented
observation_coverageImplementedTODOImplementedTODO
validated_sessionImplementedTODOImplementedTODO
meta.language (39)39 Implemented39 Implemented
meta.language.calls (2)2 Implemented2 Implemented
declaredImplementedImplemented
forbiddenImplementedImplemented
meta.language.classes (3)3 Implemented3 Implemented
abstract_completeImplementedImplemented
override_signatureImplementedImplemented
single_inheritanceImplementedImplemented
meta.language.contexts (1)1 Implemented1 Implemented
inheritanceImplementedImplemented
meta.language.envelopes (7)7 Implemented7 Implemented
class_callsImplementedImplemented
createsImplementedImplemented
direct_callsImplementedImplemented
leafImplementedImplemented
permissionsImplementedImplemented
readsImplementedImplemented
receiver_callsImplementedImplemented
meta.language.fields (2)2 Implemented2 Implemented
context_stateImplementedImplemented
kindsImplementedImplemented
meta.language.methods (2)2 Implemented2 Implemented
kindsImplementedImplemented
proseImplementedImplemented
meta.language.model (3)3 Implemented3 Implemented
forbidden_pathsImplementedImplemented
inherited_prohibitionsImplementedImplemented
virtual_dispatchImplementedImplemented
meta.language.types (19)19 Implemented19 Implemented
argument_arityImplementedImplemented
declaration_proseImplementedImplemented
enum_variantsImplementedImplemented
field_proseImplementedImplemented
generic_parametersImplementedImplemented
member_commasImplementedImplemented
name_resolutionImplementedImplemented
opaque_representationImplementedImplemented
preludeImplementedImplemented
qualified_namesImplementedImplemented
recursive_valuesImplementedImplemented
struct_fieldsImplementedImplemented
tuplesImplementedImplemented
type_expressionsImplementedImplemented
unique_fieldsImplementedImplemented
unique_parametersImplementedImplemented
unique_variantsImplementedImplemented
unknown_namesImplementedImplemented
variant_proseImplementedImplemented
meta.reviews (27)27 Implemented27 Implemented
claim_textImplementedImplemented
complete_test_setImplementedImplemented
decisionsImplementedImplemented
fragment_associationsImplementedImplemented
fragment_formatImplementedImplemented
fragment_freshnessImplementedImplemented
gateImplementedImplemented
input_formatImplementedImplemented
input_fragmentsImplementedImplemented
output_formatImplementedImplemented
preparationImplementedImplemented
record_requiredImplementedImplemented
recorded_readsImplementedImplemented
recordingImplementedImplemented
review_delegationImplementedImplemented
review_diagnosticsImplementedImplemented
review_instructionsImplementedImplemented
review_scopeImplementedImplemented
selector_claimImplementedImplemented
selector_line_rangeImplementedImplemented
selector_testImplementedImplemented
selector_whole_fileImplementedImplemented
source_representationImplementedImplemented
stalenessImplementedImplemented
summary_formatImplementedImplemented
test_sourceImplementedImplemented
validation_layoutImplementedImplemented
meta.validation (3)3 TODO3 TODO
claim_specific_evidenceTODOTODO
independent_inspectionTODOTODO
review_packetsTODOTODO