Function lower_invariant_ir 

pub fn lower_invariant_ir(
    inv: &Invariant,
    store_cells: &HashMap<String, TyId>,
    program: &CheckedProgram,
) -> IrPredicate

P6.8 ([DECISION A]/[DECISION E], #1165): lower an agent invariant into a real IrPredicate — seeds the predicate’s own scope from store_cells exactly as checker::check_invariants does (bynk-check/src/checker.rs: each store Cell field in scope by bare name, reading as its element type), then lowers predicate through the ordinary lower_expr_ir machinery unchanged. Takes store_cells as a parameter rather than re-deriving it from program ([DECISION E]) — a certified CheckedProgram carries no persisted “this agent’s store cells” table; that scope is check_agent_decls’s own transient scratch, never persisted to TypedCommons. Called once per agent’s own invariant list, by whichever future slice builds IrItem::Agent for real — not once per handler, mirroring check_invariants’s own once-per-agent posture.