Function check_invariants 

pub fn check_invariants(
    invariants: &[Invariant],
    store_cells: &HashMap<String, Ty>,
    agent_name: &str,
    input: &ResolvedCommons,
    expr_types: &mut HashMap<Span, Ty>,
    errors: &mut Vec<CompileError>,
    refs: &mut RefSink,
    hints: &mut HintSink,
    locals: &mut LocalsSink,
    requirements: &mut RequirementSink,
)

Check an agent’s invariant declarations (v0.80 §14). Each predicate is a pure Bool-typed expression over the agent’s state fields (referenced by bare name), plus implies/is. The pass enforces:

• bynk.invariant.duplicate_name — two invariants share a name.
• bynk.invariant.cross_agent_reference — a predicate names another agent (§14 closes that door; sagas/scenarios are the cross-agent tools).
• bynk.invariant.impure_predicate — a predicate uses an effectful or test-only construct (Effect, ? propagation, expect, Val).
• bynk.invariant.not_bool — the predicate does not type to Bool.

Store Cell fields are placed in scope as the predicate’s locals; invariants read fields directly by bare name, mirroring the design-notes worked examples.