Good catch on the trust model, if timestamps or provenance are mutable, the checker cant save you there. But thats not a knock on the decidable fragment, its just a different assumption boundary, like any static check over an untrusted log.