11 ms·
Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.
by ufo 1y ago
Last but not least, those deciders were implemented and verified in the Rocq proof assistant, so we know they are correct.
- lairv 1y agoWe know that they correctly implement their specification*
- meithecatte 1y agoNo, 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.