adapt to JALR decode bugfix

mit-plv · Apr 25, 2022 · 0fd5faa · 0fd5faa
1 parent 7bedb62
commit 0fd5faa
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 7 deletions.
diff --git 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
@@ -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;