-
Alban Gruin authored
This fix an issue in state_leb, in which an instruction in a later stage would be less advanced than an instruction in an earlier stage with a lower latency. This also adds two lemmas related to comparison to simplify more complex theorems. Signed-off-by:
Alban Gruin <alban.gruin@irit.fr>
Alban Gruin authoredThis fix an issue in state_leb, in which an instruction in a later stage would be less advanced than an instruction in an earlier stage with a lower latency. This also adds two lemmas related to comparison to simplify more complex theorems. Signed-off-by:
Alban Gruin <alban.gruin@irit.fr>
definitions.v 8.64 KiB