[libre-riscv-dev] [Bug 306] Formal Correctness Proof for ALU pipeline