From 0fd5faa1fb8721ece3924d81d5b8d14b5b54cdf9 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Mon, 25 Apr 2022 00:13:27 -0400
Subject: [PATCH] adapt to JALR decode bugfix

---
 src/riscv/Proofs/EncodeDecode.v | 5 -----
 src/riscv/Utility/Encode.v      | 2 --
 2 files changed, 7 deletions(-)

diff --git a/src/riscv/Proofs/EncodeDecode.v b/src/riscv/Proofs/EncodeDecode.v
index d1b85fe..61d9a7f 100644
--- a/src/riscv/Proofs/EncodeDecode.v
+++ b/src/riscv/Proofs/EncodeDecode.v
@@ -187,10 +187,6 @@ Ltac prove_encode_decode :=
        ];
   try apply_encode_decode_lemma_by_format.
 
-Axiom TODO_spec_bug_in_JALR: forall inst,
-  encode_I opcode_JALR (bitSlice inst 7 12) (bitSlice inst 15 20) funct3_JALR
-    (signExtend 12 (bitSlice inst 20 32)) = inst.
-
 Lemma encode_decodeCSR: forall bw inst,
     0 <= inst < 2 ^ 32 ->
     isValidCSR (decodeCSR bw inst) = true ->
@@ -233,7 +229,6 @@ Lemma encode_decodeI: forall bw inst,
     encode (IInstruction (decodeI bw inst)) = inst.
 Proof.
   prove_encode_decode.
-  apply TODO_spec_bug_in_JALR.
 Qed.
 
 Ltac apply_encode_decode_lemma_by_ext :=
diff --git a/src/riscv/Utility/Encode.v b/src/riscv/Utility/Encode.v
index 46ae629..64c114e 100644
--- a/src/riscv/Utility/Encode.v
+++ b/src/riscv/Utility/Encode.v
@@ -5,8 +5,6 @@ Require Import riscv.Utility.Utility.
 
 Local Open Scope Z_scope.
 
-Definition funct3_JALR: MachineInt := 0. (* TODO why does Decode not define & check this? *)
-
 Record InstructionMapper{T: Type} := mkInstructionMapper {
   map_Invalid: Z -> T;
   map_R(opcode: MachineInt)(rd rs1 rs2: Register)(funct3: MachineInt)(funct7: MachineInt): T;