Report.proved

Every postcondition holds and no runtime error is possible. With

Report.proved: bool

an observation (sv.equivalent), no postcondition depends on what it ignores, and some engine’s doubles meet it (floats_unmet). Under semantics="substrait", the reference’s proof also carries over (transfer is empty).