Yann Leray

**Name of the Vulnerable Software and Affected Versions** Rocq Prover (affected versions not specified) **Description** The guard checker fails to recheck the recursive tree representation of an inductive type parameter after it has been modified by transport. This allows a fixpoint to apply a rewrite along an equality between types to its recursive argument; while the guard checker accepts this because the inductive type is preserved, the recorded recursive tree for the parameter is altered. A subsequent fixpoint calling the first inherits this altered tree without verification, allowing non-structurally decreasing calls to be accepted as terminating. This can lead to non-terminating definitions that prove false propositions, such as a natural number equaling its own successor. **Recommendations** At the moment, there is no information about a newer version that contains a fix for this vulnerability.