diff --git a/ceno_emul/src/disassemble/mod.rs b/ceno_emul/src/disassemble/mod.rs
index ca6161000..94709e74b 100644
--- a/ceno_emul/src/disassemble/mod.rs
+++ b/ceno_emul/src/disassemble/mod.rs
@@ -250,6 +250,13 @@ impl InstructionProcessor for InstructionTranspiler {
     }
 
     /// Convert LUI to ADDI.
+    ///
+    /// RiscV's load-upper-immediate instruction is necessary to build arbitrary constants,
+    /// because its ADDI can only have a relatively small immediate value: there's just not
+    /// enough space in the 32 bits for more.
+    ///
+    /// Our internal ADDI does not have this limitation, so we can convert LUI to ADDI.
+    /// See [`InstructionTranspiler::process_auipc`] for more background on the conversion.
     fn process_lui(&mut self, dec_insn: UType) -> Self::InstructionResult {
         // Verify assumption that the immediate is already shifted left by 12 bits.
         assert_eq!(dec_insn.imm & 0xfff, 0);
@@ -264,6 +271,26 @@ impl InstructionProcessor for InstructionTranspiler {
     }
 
     /// Convert AUIPC to ADDI.
+    ///
+    /// RiscV's instructions are designed to be (mosty) position-independent.  AUIPC is used
+    /// to get access to the current program counter, even if the code has been moved around
+    /// by the linker.
+    ///
+    /// Our conversion here happens after the linker has done its job, so we can safely hardcode
+    /// the current program counter into the immediate value of our internal ADDI.
+    ///
+    /// Note that our internal ADDI can have arbitrary intermediate values, not just 12 bits.
+    ///
+    /// ADDI is slightly more general than LUI or AUIPC, because you can also specify an
+    /// input register rs1.  That generality might cost us sligthtly in the non-recursive proof,
+    /// but we suspect decreasing the total number of different instruction kinds will speed up
+    /// the recursive proof.
+    ///
+    /// In any case, AUIPC and LUI together make up ~0.1% of instructions executed in typical
+    /// real world scenarios like a `reth` run.
+    ///
+    /// TODO(Matthias): run benchmarks to verify the impact on recursion, once we have a working
+    /// recursion.
     fn process_auipc(&mut self, dec_insn: UType) -> Self::InstructionResult {
         let pc = self.pc;
         // Verify our assumption that the immediate is already shifted left by 12 bits.