Timings for DecodeEncodeI.v

1. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev/./rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.timing
2. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-fiat-crypto-with-bedrock.dev/./rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.timing

Require Import riscv.Proofs.DecodeEncodeProver.

Lemma decodeI_encode: forall (inst: InstructionI) (iset: InstructionSet),
    verify (IInstruction inst) iset ->
    decode iset (encode (IInstruction inst)) = IInstruction inst.
Proof.
 prove_decode_encode.
 Qed.