Function check_migrations 

pub fn check_migrations(
    agent: &AgentDecl,
    store_cells: &HashMap<String, TyId>,
    types: &HashMap<String, Arc<TypeDecl>>,
    input: &ResolvedCommons,
    tys: &Types,
    expr_types: &mut HashMap<ExprId, TypedExpr>,
    errors: &mut Vec<CompileError>,
    refs: &mut RefSink,
    hints: &mut HintSink,
    locals: &mut LocalsSink,
    requirements: &mut RequirementSink,
    callees: &mut HashMap<ExprId, Callee>,
)

State-migrations S2 (#2224, track §3.3): check each migrate step’s body on its own terms, with no lock: the old parameter names a record type, the body is pure and key-free, each := targets a Cell or Map field with a value of that field’s type, and no field is assigned twice (record-literal semantics). What the lock alone can check (the old shape against the recorded version, and which changes the step covers) is schema_registry::reconcile_agents’s.

A bare current field reads its carried value, so the scope is the agent’s Cell fields (as for invariants) plus old and each let in order.