meta.contracts.observation_coverage

Incomplete observation cannot establish conformance. Unmapped requests, unsupported receiver checks, and uninstrumented effects remain explicit gaps. Strict acceptance requires complete checking of the declared scope, as well as absence of violations. Diagnostics identify the checking scenario, relevant model rule when one exists, and observed call path; an unknown mapping is not silently attributed to the caller.

Verification injects each gap into an otherwise passing scenario and requires an incomplete or failing result, including cached requests and unsupported async boundaries. A call-only report does not claim that input reads, context construction, ordinary uninstrumented helpers, or task propagation were checked.

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

Implementation

Implemented crates/sage-meta/src/contracts.rs:399–404

sage_meta::contracts · lib:sage_meta

#![allow(unused)]
fn main() {
    // {anchor}`meta.contracts.observation_coverage`
    pub fn finish(mut self) -> ContractReport {
        if !self.active.is_empty() {
            self.record_gap(format!(
                "unclosed architectural invocations: {}",
                self.active

}

See more source ↗

TODO crates/sage-meta/tests/contracts_plan.rs:28–35

sage_meta::todo · test:contracts_plan

TODO: Exercise effect hooks and async/task propagation; reject absent observation within the declared scope and identify its test context.

#![allow(unused)]
fn main() {
    // {anchor}`meta.contracts.observation_coverage`<<
    #[test]
    #[sage::test(meta.contracts.observation_coverage)]
    fn declared_effects_and_async_boundaries_have_complete_scope_accounting() {
        // TODO: Exercise effect hooks and async/task propagation; reject absent
        // observation within the declared scope and identify its test context.
    }
    // >>

}

See more source ↗

Tests and review

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

Implemented sage_meta::real_salsa_contract_fixture

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

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.language.calls.declared)]
#[sage::test(meta.language.calls.forbidden)]
#[sage::test(meta.contracts.validated_session)]
#[sage::test(meta.contracts.cache_invocations)]
#[sage::test(meta.contracts.observation_coverage)]
fn real_salsa_contract_fixture() {
    let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR"));
    let fixture = root.join("tests/fixtures/contracts");
    let output = std::process::Command::new(env!("CARGO"))
        .args(["test", "--locked", "--manifest-path"])
        .arg(fixture.join("Cargo.toml"))
        .args(["--", "--nocapture", "--test-threads=1"])
        .env(
            "CARGO_TARGET_DIR",
            root.join("../../target/sage-contract-fixture"),
        )
        .output()
        .expect("run the isolated contracts fixture");
    assert!(
        output.status.success(),
        "contract fixture failed:\n{}\n{}",
        String::from_utf8_lossy(&output.stdout),
        String::from_utf8_lossy(&output.stderr)
    );
    let stdout = String::from_utf8(output.stdout).unwrap();
    let evidence: Vec<serde_json::Value> = stdout
        .lines()
        .filter_map(|line| line.split_once("SAGE_CONTRACT_EVIDENCE:"))
        .map(|(_, json)| serde_json::from_str(json).unwrap())
        .collect();
    assert_eq!(evidence.len(), 2, "expected cold and prewarmed reports");
    let root = "sage_contract_fixture::nodes::Root::run";
    let helper = "sage_contract_fixture::nodes::Helper::work";
    let leaf = "sage_contract_fixture::nodes::Leaf::read";
    for prewarmed in [false, true] {
        let sample = evidence
            .iter()
            .find(|sample| sample["prewarmed"] == prewarmed)
            .expect("each cache scenario must report evidence");
        let operations = &sample["model"]["operations"];
        assert!(operations[helper]["invokes"].as_array().unwrap().is_empty());
        assert_eq!(
            operations[root]["prohibits"][0]["targets"],
            serde_json::json!([leaf])
        );
        let report = &sample["contracts"];
        assert_eq!(report["calls_conform"], false);
        assert_eq!(report["coverage"]["checked_requests"], 3);
        assert!(report["coverage"]["gaps"].as_array().unwrap().is_empty());
        let violations = report["violations"].as_array().unwrap();
        assert_eq!(violations.len(), 2);
        assert_eq!(violations[0]["kind"], "UndeclaredCall");
        assert_eq!(violations[1]["kind"], "ForbiddenTransitive");
        assert_eq!(violations[1]["rule"]["operation"], root);
        assert_eq!(
            violations[1]["path"]
                .as_array()
                .unwrap()
                .iter()
                .map(|frame| frame["operation"].as_str().unwrap())
                .collect::<Vec<_>>(),
            [root, helper, leaf],
        );
        if prewarmed {
            let events = sample["query_events"].as_array().unwrap();
            assert!(events.iter().any(|event| {
                let event = event.as_str().unwrap();
                event.starts_with("return Leaf::read") && event.contains("[Reused]")
            }));
            assert!(
                !events
                    .iter()
                    .any(|event| event.as_str().unwrap().starts_with("execute Leaf::read"))
            );
        }
    }
}
}

See more source ↗

TODO sage_meta::todo::declared_effects_and_async_boundaries_have_complete_scope_accounting

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(meta.contracts.observation_coverage)]
    fn declared_effects_and_async_boundaries_have_complete_scope_accounting() {
        // TODO: Exercise effect hooks and async/task propagation; reject absent
        // observation within the declared scope and identify its test context.
    }
}

See more source ↗

Implemented sage_meta::observation_gaps_and_effect_coverage_are_explicit

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

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.observation_coverage)]
fn observation_gaps_and_effect_coverage_are_explicit() {
    let model = model(
        r#"
        context Context { """Context.""" }
        class Root { """Root.""" input value: u32;
            fn run() -> u32 { """Run.""" envelope {
                reads self.value; creates context: crate::Context;
            } }
        }
    "#,
    );
    let mut checked = session(model.clone(), &["Root::run"]);
    let run = checked.enter("demo::Root::run", None);
    checked.exit(run);
    let report = checked.finish();
    report.assert_calls_conform();
    assert_eq!(
        report
            .coverage
            .unchecked_effects
            .into_iter()
            .collect::<Vec<_>>(),
        [UncheckedEffect::Reads, UncheckedEffect::Creates]
    );

    let mut incomplete = session(model, &["Root::run"]);
    incomplete.record_gap("unmapped Salsa query at input.rs:42");
    assert!(!incomplete.finish().calls_conform);
}
}

See more source ↗

Implemented sage_meta::self_permission_rejects_different_and_unknown_receivers

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

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.observation_coverage)]
#[sage::test(meta.language.envelopes.receiver_calls)]
fn self_permission_rejects_different_and_unknown_receivers() {
    let model = model(
        r#"
        class Item { """Item."""
            fn run() -> u32 { """Run.""" envelope { invokes self.read(); } }
            query read() -> u32 { """Read.""" envelope {} }
        }
    "#,
    );
    for receiver in [Some("item:other"), None] {
        let mut checked = session(model.clone(), &["Item::run"]);
        let run = checked.enter("demo::Item::run", Some("item:1"));
        let read = checked.enter("demo::Item::read", receiver);
        checked.exit(read);
        checked.exit(run);
        let report = checked.finish();
        assert!(!report.calls_conform);
        if receiver.is_some() {
            assert_eq!(report.violations[0].kind, ViolationKind::ReceiverMismatch);
        } else {
            assert!(report.coverage.gaps[0].contains("receiver identity required"));
        }
    }
}
}

See more source ↗

Implemented sage_meta::unknown_boundaries_roots_and_unbalanced_exits_cannot_pass

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

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.observation_coverage)]
fn unknown_boundaries_roots_and_unbalanced_exits_cannot_pass() {
    let mut session = session(model(FORBIDDEN), &["Root::run", "Missing::run"]);
    let root = session.enter("demo::Helper::work", None);
    let unknown = session.enter("demo::Missing::run", None);
    session.exit(root);
    session.exit(unknown);
    let report = session.finish();
    assert!(!report.calls_conform);
    assert!(
        report
            .violations
            .iter()
            .any(|v| v.kind == ViolationKind::UnknownOperation)
    );
    assert!(
        report
            .violations
            .iter()
            .any(|v| v.kind == ViolationKind::UnexpectedRoot)
    );
    assert!(
        report
            .violations
            .iter()
            .any(|v| v.kind == ViolationKind::UnbalancedExit)
    );
    assert!(
        report
            .coverage
            .gaps
            .iter()
            .any(|gap| gap.contains("unclosed"))
    );
    assert!(
        report
            .coverage
            .gaps
            .iter()
            .any(|gap| gap.contains("configured root"))
    );
}
}

See more source ↗

Review: Accepted · Codex /root/anchor_185 independent source review.

Baseline: independently verified exact byte equality of both historical implementation sources and all three historical test-source files against the current workspace. Reassessed the complete current claim, both implementation entries and all five test entries; prior approval is context, not execution evidence.
Source assessment: ContractSession preserves unknown operations, unexpected roots and malformed exits as violations, missing receiver identity and incomplete scope as gaps, and finish permits calls_conform only when both collections are empty. Violations retain the observed invocation path and applicable ContractRule; unchecked Reads and Creates remain explicitly separate from call conformance. observation_gaps_and_effect_coverage_are_explicit directly checks both unchecked effects in an otherwise successful call report and rejects an injected unmapped gap. self_permission_rejects_different_and_unknown_receivers checks mismatch failure versus unavailable-identity gaps. unknown_boundaries_roots_and_unbalanced_exits_cannot_pass asserts unknown/root/exit violations and configured-root/unclosed gaps. These assertions would detect false acceptance or disappearance of the named diagnostics.
real_salsa_contract_fixture asserts cold and prewarmed failure, three checked requests, no spurious gaps, exact violation kinds, rule operation and complete root/helper/leaf path, and actual cache reuse without leaf execution. Captured fixture source additionally exercises unmapped generated/missing mappings, absent compiled snapshots with all operation mappings absent, cross-thread cached execution gaps, and malformed lifecycle replays against a conforming baseline. Captured SalsaObserver source records missing provenance, unsupported thread propagation and lifecycle inconsistencies as gaps; unsuccessful mapping remains None instead of borrowing caller identity. Captured query/model/expected fixture data and runtime setup helpers establish the scenarios underlying these assertions.
Deferral: the ordinary call-only evidence does not establish strict whole-scope conformance for input reads, context construction, uninstrumented ordinary helpers or async tasks. Both the explicit TODO implementation and test declared_effects_and_async_boundaries_have_complete_scope_accounting account for this remaining requirement: effect hooks, task-context propagation and instrumentation that detects absent declared-scope observation must exist before complete scope and scenario-context diagnostics can be tested. The stub has no behavioral assertions and is not counted as implementation or execution evidence. Existing path/rule and cold/warm scenario diagnostics cover the implemented subset; full declared-scope/scenario accounting remains visibly TODO. No N/A entries occur. No edits needed for this accurately deferred state.
Execution: ran review start/read and baseline comparisons, then review record; no behavioral tests or workspace build run by this reviewer. Coordinator-reported 321 passing functional tests and successful root build are separate reported evidence.

Browse meta anchors

116 anchors

Anchor Implementation Tests

meta (116) 102 Implemented24 TODO 103 Implemented36 TODO

meta.anchors (22) 22 Implemented 21 Implemented12 TODO

anchor_pages Implemented ImplementedTODO

Every specification anchor has a stable page identifying the rule and showing its definition, context, implementation entries, and tests/evidence. The page includes Rust excerpts and access to surrounding source, and exposes each entry’s placeholder status and explanation. Multiple sites remain individually inspectable rather than being reduced to a single coverage badge.

Symposiun AGentic Environment (SAGE)

meta.contracts.observation_coverage

Implementation

Tests and review