Comment by ufo
3 months ago
Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.
3 months ago
Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.
We know that they correctly implement their specification*
No, they are correct, because the deciders themselves are just a cog in the proof of the overall theorem. The specification of the deciders is not part of the TCB, so to speak.