Use specialized format for FENCE

jolt-core/src/zkvm/instruction/fence.rs

@@ -1,4 +1,4 @@
-use crate::zkvm::instruction::{InstructionFlags, NUM_INSTRUCTION_FLAGS};
+use crate::zkvm::instruction::NUM_INSTRUCTION_FLAGS;
 use tracer::instruction::{fence::FENCE, RISCVCycle};
 
 use crate::zkvm::lookup_table::LookupTables;
@@ -20,9 +20,7 @@ impl Flags for FENCE {
     }
 
     fn instruction_flags(&self) -> [bool; NUM_INSTRUCTION_FLAGS] {
-        let mut flags = [false; NUM_INSTRUCTION_FLAGS];
-        flags[InstructionFlags::IsRdNotZero] = self.operands.rd != 0;
-        flags
+        [false; NUM_INSTRUCTION_FLAGS]
     }
 }
 

tracer/src/instruction/fence.rs

@@ -1,14 +1,16 @@
 use serde::{Deserialize, Serialize};
 
-use crate::{declare_riscv_instr, emulator::cpu::Cpu};
+use crate::{
+    declare_riscv_instr, emulator::cpu::Cpu, instruction::format::format_fence::FormatFence,
+};
 
-use super::{format::format_i::FormatI, RISCVInstruction, RISCVTrace};
+use super::{RISCVInstruction, RISCVTrace};
 
 declare_riscv_instr!(
     name   = FENCE,
     mask   = 0x0000707f,
     match  = 0x0000000f,
-    format = FormatI,
+    format = FormatFence,
     ram    = ()
 );
 

tracer/src/instruction/format/format_fence.rs

@@ -0,0 +1,51 @@
+use crate::emulator::cpu::Cpu;
+use serde::{Deserialize, Serialize};
+use std::fmt::Debug;
+
+use super::{InstructionFormat, InstructionRegisterState, NormalizedOperands};
+
+#[derive(Default, Debug, Clone, Copy, PartialEq, Serialize, Deserialize)]
+pub struct FormatFence {}
+
+#[derive(Default, Debug, Copy, Clone, Serialize, Deserialize, PartialEq)]
+pub struct RegisterStateFormatFence {}
+
+impl InstructionRegisterState for RegisterStateFormatFence {
+    #[cfg(any(feature = "test-utils", test))]
+    fn random(_: &mut rand::rngs::StdRng, _: &NormalizedOperands) -> Self {
+        Self {}
+    }
+}
+
+impl InstructionFormat for FormatFence {
+    type RegisterState = RegisterStateFormatFence;
+
+    fn parse(_word: u32) -> Self {
+        FormatFence {}
+    }
+
+    fn capture_pre_execution_state(&self, _state: &mut Self::RegisterState, _cpu: &mut Cpu) {
+        // No-op
+    }
+
+    fn capture_post_execution_state(&self, _state: &mut Self::RegisterState, _cpu: &mut Cpu) {
+        // No-op
+    }
+
+    #[cfg(any(feature = "test-utils", test))]
+    fn random(_: &mut rand::rngs::StdRng) -> Self {
+        Self {}
+    }
+}
+
+impl From<NormalizedOperands> for FormatFence {
+    fn from(_: NormalizedOperands) -> Self {
+        Self {}
+    }
+}
+
+impl From<FormatFence> for NormalizedOperands {
+    fn from(_: FormatFence) -> Self {
+        NormalizedOperands::default()
+    }
+}

tracer/src/instruction/format/mod.rs

@@ -5,6 +5,7 @@ use std::fmt::Debug;
 pub mod format_amo;
 pub mod format_assert_align;
 pub mod format_b;
+pub mod format_fence;
 pub mod format_i;
 pub mod format_inline;
 pub mod format_j;

z3-verifier/src/cpu_constraints.rs

@@ -29,9 +29,10 @@ use tracer::instruction::{
     ecall::ECALL,
     fence::FENCE,
     format::{
-        format_assert_align::AssertAlignFormat, format_b::FormatB, format_i::FormatI,
-        format_j::FormatJ, format_load::FormatLoad, format_r::FormatR, format_s::FormatS,
-        format_u::FormatU, format_virtual_right_shift_i::FormatVirtualRightShiftI,
+        format_assert_align::AssertAlignFormat, format_b::FormatB, format_fence::FormatFence,
+        format_i::FormatI, format_j::FormatJ, format_load::FormatLoad, format_r::FormatR,
+        format_s::FormatS, format_u::FormatU,
+        format_virtual_right_shift_i::FormatVirtualRightShiftI,
         format_virtual_right_shift_r::FormatVirtualRightShiftR,
     },
     jal::JAL,
@@ -494,7 +495,7 @@ test_instruction_constraints!(BLT, FormatB);
 test_instruction_constraints!(BLTU, FormatB);
 test_instruction_constraints!(BNE, FormatB);
 test_instruction_constraints!(ECALL, FormatI);
-test_instruction_constraints!(FENCE, FormatI);
+test_instruction_constraints!(FENCE, FormatFence);
 test_instruction_constraints!(JAL, FormatJ);
 test_instruction_constraints!(JALR, FormatI);
 test_instruction_constraints!(LD, FormatLoad);

z3-verifier/src/lib.rs

@@ -61,4 +61,7 @@ macro_rules! template_format {
             rs2: 3,
         }
     };
+    (FormatFence) => {
+        FormatFence {}
+    };
 }