Comment by ufo
1 year ago
Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.
1 year 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.