procedure {:checksum "2"} P(); implementation {:id "P"} {:checksum "1"} P() { assert 1 != 1; }