procedure {:checksum "P0$proc#0"} P0(); // Action: skip implementation {:id "P0"} {:checksum "P0$impl#0"} P0() { call P0(); } function F0() : bool { true }