Function logos_rt_push_i32 

pub unsafe extern "C" fn logos_rt_push_i32(
    frame: *mut i64,
    vec_slot: i64,
    ptr_slot: i64,
    len_slot: i64,
    value: i64,
)

Push helper for pinned half-width Int lists (ListRepr::IntsI32 = Vec<i32>): the value TRUNCATES to its low 4 bytes. The narrowing proof guarantees every pushed value fits i32, so the truncation is lossless; debug_assert catches a proof violation in test builds. The refreshed ptr_slot is the Vec<i32> element buffer (4-byte stride — the stencil and regalloc loads movsxd from it).

Safety

See logos_rt_push_i64; vec_slot must be a live *mut Vec<i32>.