meta.contracts.validated_session

A checking session uses one immutable, validated contract model and its source correspondence index. Every event refers to that same snapshot. Enabled enforcement fails if its model is missing or invalid, or if the indexed Rust source cannot be paired with the running binary. Loading is cached for the session; source edits take effect only in a subsequent session.

Verification exercises cached loads, parallel first use, explicit model roots, missing and invalid files, source/build mismatch rejection, and a subsequent session seeing model edits. Independently configured fixture sessions can use different models without modifying an active session.

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

Implementation

Implemented crates/sage-meta/src/contracts.rs:154–159

sage_meta::contracts · lib:sage_meta

#![allow(unused)]
fn main() {
    // {anchor}`meta.contracts.validated_session`
    pub fn new(model: Arc<ContractModel>, roots: impl IntoIterator<Item = String>) -> Self {
        let roots: BTreeSet<_> = roots.into_iter().collect();
        let gaps = roots
            .iter()
            .filter(|root| !model.operations.contains_key(*root))

}

See more source ↗

TODO crates/sage-meta/tests/contracts_plan.rs:10–17

sage_meta::todo · test:contracts_plan

TODO: Exercise missing files, explicit roots, parallel first use, and model edits becoming visible only when a new loading session starts.

#![allow(unused)]
fn main() {
    // {anchor}`meta.contracts.validated_session`<<
    #[test]
    #[sage::test(meta.contracts.validated_session)]
    fn automatic_runtime_loading_is_cached_and_rejects_unavailable_models() {
        // TODO: Exercise missing files, explicit roots, parallel first use, and
        // model edits becoming visible only when a new loading session starts.
    }
    // >>

}

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::automatic_runtime_loading_is_cached_and_rejects_unavailable_models

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

#![allow(unused)]
fn main() {
#[test]
    #[sage::test(meta.contracts.validated_session)]
    fn automatic_runtime_loading_is_cached_and_rejects_unavailable_models() {
        // TODO: Exercise missing files, explicit roots, parallel first use, and
        // model edits becoming visible only when a new loading session starts.
    }
}

See more source ↗

Implemented sage_meta::source_snapshot_mismatch_is_rejected

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

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.validated_session)]
fn source_snapshot_mismatch_is_rejected() {
    let index = index(VALID);
    assert!(index.verify_source("src/lib.rs", VALID).is_ok());
    assert!(matches!(
        index.verify_source("src/lib.rs", &VALID.replace("compute", "other")),
        Err(LookupError::SourceMismatch { .. })
    ));
    assert!(matches!(
        index.verify_source("unknown.rs", VALID),
        Err(LookupError::SourceMismatch { .. })
    ));
}
}

See more source ↗

Implemented sage_meta::invalid_static_model_never_becomes_a_runtime_contract

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

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.validated_session)]
fn invalid_static_model_never_becomes_a_runtime_contract() {
    let document = parse(
        "demo/crate.sage",
        r#"
        crate demo { """Demo.""" }
        class Root { """Root."""
            fn run() -> u32 { """Run.""" envelope {
                invokes self.run(); forbid transitive self.run;
            } }
        }
    "#,
    )
    .unwrap();
    let diagnostics = ContractModel::new(&[document]).unwrap_err();
    assert!(
        diagnostics
            .iter()
            .any(|error| error.message.contains("forbidden transitive call"))
    );
}
}

See more source ↗

Implemented sage_meta::repeated_roots_are_independent_and_models_are_shared_immutably

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

#![allow(unused)]
fn main() {
#[test]
#[sage::test(meta.contracts.validated_session)]
fn repeated_roots_are_independent_and_models_are_shared_immutably() {
    let model = model(FORBIDDEN);
    let mut first = session(model.clone(), &["Root::run", "Leaf::read"]);
    // Prewarming a leaf does not grant future callers permission to request it.
    let leaf = first.enter("demo::Leaf::read", None);
    first.exit(leaf);
    let root = first.enter("demo::Root::run", None);
    let helper = first.enter("demo::Helper::work", None);
    first.exit(helper);
    first.exit(root);
    first.finish().assert_calls_conform();
    let mut second = session(model, &["Root::run"]);
    let root = second.enter("demo::Root::run", None);
    let leaf = second.enter("demo::Leaf::read", None);
    second.exit(leaf);
    second.exit(root);
    assert_eq!(second.finish().violations.len(), 2);
}
}

See more source ↗

Review: Accepted · Codex /root/anchor_186 independent review.

Reassessed the complete validated_session claim and both implementation entries plus all five associated tests. Baseline: independently verified exact byte equality of both historical implementation files and all four historical test files; also verified unchanged SalsaObserver and fixture-test context. This supports comparison with the supplied prior review, not substitution for current assessment.
Source: ContractModel owns resolved operations behind a private map with immutable access; new rejects validation diagnostics before constructing it. ContractSession retains one Arc and every request/prohibition lookup uses that model. Separate session state and observer-local immutable index/verified-source mappings permit independently configured models without mutating an active session. repeated_roots_are_independent_and_models_are_shared_immutably meaningfully asserts a conforming first session and two violations in an independent second session using the shared model. invalid_static_model_never_becomes_a_runtime_contract asserts rejection of forbidden static contracts. source_snapshot_mismatch_is_rejected asserts exact source acceptance and modified/unknown-file rejection. Captured verify_source compares indexed text with compiled text; SalsaObserver checks supplied compiled snapshots at construction and fails conformance for observed unpaired sources, retaining the index and mapping for the session.
real_salsa_contract_fixture checks subprocess success and cold/prewarmed model, violations, path and coverage values in its annotated body. Captured fixture setup supplies include_str! compiled source and validated model documents; its stale-source and unpaired-source assertions supplement source/build mismatch coverage, and its reset creates independent sessions. This is manual fixture loading, not evidence of cached automatic loading or model-update discovery.
The ordinary implementation establishes the immutable runtime core. The second implementation entry and automatic_runtime_loading_is_cached_and_rejects_unavailable_models test are explicit TODO evidence, with no behavioral assertions: automatic loader implementation is the prerequisite for cached loads, parallel first use, explicit model roots, unavailable/missing-file rejection and new-session visibility of edits. These remain deferred, including full automatic invalid-file loading behavior; static-invalid-model rejection already has substantive coverage. Distinct fixture model configuration is supported by constructor ownership, while automatic reload/edit scenarios are covered by the declared deferral. No N/A entries exist and no deferred behavior is claimed implemented.
Execution: I ran review start/read and baseline comparisons, and am recording this report; I ran no behavioral tests or workspace build. The coordinator separately reports 321 functional tests and a passing root build. No requested edits; existing loader TODO remains visible.

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.validated_session

Implementation

Tests and review