[walk] C.9 integration test: end-to-end Outlives composition succeeds + refuses (#384 C.9)

[TSavo]

Goal

Integration test exercising the full C.9 pipeline: walk lifts a real Rust source with lifetime relations, marriage classifies the LLBC-emitted Outlives predicates, the substrate verifier composes a caller-callee pair where region demands either match (composition succeeds) or mismatch (composition refuses with RegionCompositionFailure).

Files affected

• Create: implementations/rust/provekit-walk/tests/region_composition.rs — new integration test file.
• Create: implementations/rust/provekit-walk/tests/fixtures/region_caller_satisfied.rs — fixture: a caller whose region facts satisfy the callee's pre-condition.
• Create: implementations/rust/provekit-walk/tests/fixtures/region_caller_unsatisfied.rs — fixture: a caller whose region facts do NOT satisfy the callee's pre-condition.
• Create: implementations/rust/provekit-walk/tests/fixtures/region_callee.rs — fixture: the callee both fixtures above will compose against.
• Create the corresponding .llbc files (run charon as needed; existing fixtures show the pattern).

What to ship

1. Fixture region_callee.rs:

fn callee<'a, 'b: 'a>(x: &'a u32, y: &'b u32) -> &'a u32 {
    let _ = y;
    x
}

(Callee demands Outlives('b, 'a) per its where-clause.)

2. Fixture region_caller_satisfied.rs:

fn caller<'a, 'b: 'a>(x: &'a u32, y: &'b u32) -> &'a u32 {
    callee(x, y)
}

(Caller has the same where 'b: 'a clause, so it can discharge callee's demand.)

3. Fixture region_caller_unsatisfied.rs:

fn caller<'a, 'b>(x: &'a u32, y: &'b u32) -> &'a u32 {
    callee(x, y)
}

(Caller has NO where-clause, so 'a and 'b are unrelated. Callee's demand Outlives('b, 'a) cannot be discharged.)

4. Integration test region_composition_succeeds_when_where_clause_matches in tests/region_composition.rs:

use provekit_walk::*;

#[test]
fn region_composition_succeeds_when_where_clause_matches() {
    let krate = LlbcCrate::from_path(fixture_path("region_caller_satisfied.llbc")).unwrap();
    let registry = lift_llbc_crate(&krate, Some("region_caller_satisfied.rs")).unwrap();

    let caller = registry.get("caller").expect("caller must lift");
    let callee = registry.get("callee").expect("callee must lift");

    let composition = compose_function_contracts_checked(caller, callee, &caller.callsites[0]);
    assert!(composition.is_ok(), "composition must succeed; got {:?}", composition.err());
}

5. Integration test region_composition_refuses_when_unrelated:

#[test]
fn region_composition_refuses_when_unrelated() {
    let krate = LlbcCrate::from_path(fixture_path("region_caller_unsatisfied.llbc")).unwrap();
    let registry = lift_llbc_crate(&krate, Some("region_caller_unsatisfied.rs")).unwrap();

    let caller = registry.get("caller").expect("caller must lift");
    let callee = registry.get("callee").expect("callee must lift");

    let composition = compose_function_contracts_checked(caller, callee, &caller.callsites[0]);
    match composition {
        Err(CompositionError::RegionCompositionFailure { demands }) => {
            assert_eq!(demands.len(), 1, "expected exactly one region failure");
            // The demand should be Outlives('b, 'a) after substitution into caller's region vocabulary.
            // (Substitution is identity here since both sides use the same names, but the demand
            // remains undischarged because caller has no where-clause.)
        }
        other => panic!("expected RegionCompositionFailure, got {:?}", other),
    }
}

6. Integration test region_marriage_classifies_outlives_as_lifetime_relative:

#[test]
fn region_marriage_classifies_outlives_as_lifetime_relative() {
    let krate = LlbcCrate::from_path(fixture_path("region_callee.llbc")).unwrap();
    let llbc_contract = lift_llbc_function(krate.function_by_name("callee").unwrap(), None).unwrap();
    let ast_source = std::fs::read_to_string(fixture_path("region_callee.rs")).unwrap();
    let ast_contract = lift_function_postcondition(&syn::parse_file(&ast_source).unwrap().items[0]);

    let agreement = marry(&ast_contract, &llbc_contract);
    match agreement {
        LayerAgreement::LlbcExtra(LlbcExtraCategory::LifetimeRelative) |
        LayerAgreement::Both(LlbcExtraCategory::LifetimeRelative) => { /* expected */ }
        other => panic!("expected LifetimeRelative classification, got {:?}", other),
    }
}

Tests required

(All three tests above are the deliverables. Naming + assertions per items 4, 5, 6.)

Acceptance criteria (boolean)

• cargo test -p provekit-walk --test region_composition runs and 3 tests pass
• cargo check --workspace clean
• make conformance exits 0
• All three fixtures produce non-empty region_facts or formal_regions (verifies the lifter is actually emitting region structure)
• RegionCompositionFailure test (5) catches the unsatisfied case before any predicate-level composition is attempted
• No em-dashes / en-dashes

Out of scope

• Cross-kit conformance fixture (separate issue).
• Per-kit IR types regen (separate sweep).
• Late-bound region (HRTB) fixtures.

Dependencies

• Blocked by: [walk] C.9 lifter: emit Sort::Region terms + Outlives predicates from Charon LLBC (#384 C.9) #410 (walk lifter Region+Outlives), [verifier] C.9 prover: implement three Outlives kernel axioms (reflexivity, transitivity, 'static top) (#384 C.9) #411 (prover axioms), [verifier] C.9 prover: region-quantifier composition + substitution at callsite (#384 C.9) #412 (prover composition), [walk] C.9 marriage hookup: tag Outlives predicates as LlbcExtra::LifetimeRelative (#384 C.9) #413 (marriage hookup). All four must land before this can run end-to-end.

Single-PR scope

Yes. Three fixtures + one test file.

[TSavo]

Working on this — test/414-region-composition-scaffold.

[TSavo]

Rebaseline note: keeping this open. On origin/main the C.9 prerequisites #410, #411, and #412 are closed, and the region_composition test file/fixtures exist, but the tests are still marked ignored. Current next action: unignore/update the integration tests and make the end-to-end succeeds/refuses path pass under the current Region/Outlives implementation.

[TSavo]

Closing as deferred/superseded backlog to keep the open issue list actionable.

This is not closing LSP or the current kit-owned lift/materialize/emit/prove path. Active work now belongs in #1486, #1499, concrete per-kit issues, and explicit LSP issues. Track 2 walker/dropper, broad docs/future-paper backlog, and old tracker/launch bookkeeping should be refiled later only as narrow executable issues if they become immediate again.