pub(crate) fn eval_memory_load<AB: SP1AirBuilder>(
        &self,
        builder: &mut AB,
        local: &MemoryInstructionsColumns<AB::Var>,
    ) {
        // Verify the unsigned_mem_value column.
        self.eval_unsigned_mem_value(builder, local);

        // Assert that correct value of `mem_value_is_neg_not_x0`.
        // SAFETY: If the opcode is not `lb` or `lh`, then `is_lb + is_lh = 0`, so
        // `mem_value_is_neg_not_x0 = 0`. In the other case, `is_lb + is_lh = 1` (at most
        // one selector is on), so `most_sig_byte` and `most_sig_bit` are correct.
        // Since `op_a_0` is known to be correct, we can conclude that `mem_value_is_neg_not_x0` is
        // correct for all cases, including padding rows.
        builder.assert_eq(
            local.mem_value_is_neg_not_x0,
            (local.is_lb + local.is_lh) * local.most_sig_bit * (AB::Expr::one() - local.op_a_0),
        );

        // SAFETY: `is_lb + is_lh` is already constrained to be boolean.
        // This is because at most one opcode selector can be turned on.
        builder.send_byte(
            ByteOpcode::MSB.as_field::<AB::F>(),
            local.most_sig_bit,
            local.most_sig_byte,
            AB::Expr::zero(),
            local.is_lb + local.is_lh,
        );
        builder.assert_eq(
            local.most_sig_byte,
            local.is_lb * local.unsigned_mem_val[0] + local.is_lh * local.unsigned_mem_val[1],
        );

        // When the memory value is negative and not writing to x0, use the SUB opcode to compute
        // the signed value of the memory value and verify that the op_a value is correct.
        let signed_value = Word([
            AB::Expr::zero(),
            AB::Expr::one() * local.is_lb,
            AB::Expr::one() * local.is_lh,
            AB::Expr::zero(),
        ]);

        // SAFETY: As we mentioned before, `mem_value_is_neg_not_x0` is correct in all cases and
        // boolean in all cases.
        builder.send_instruction(
            AB::Expr::zero(),
            AB::Expr::zero(),
            AB::Expr::from_canonical_u32(UNUSED_PC),
            AB::Expr::from_canonical_u32(UNUSED_PC + DEFAULT_PC_INC),
            AB::Expr::zero(),
            Opcode::SUB.as_field::<AB::F>(),
            local.op_a_value,
            local.unsigned_mem_val,
            signed_value,
            AB::Expr::zero(),
            AB::Expr::zero(),
            AB::Expr::zero(),
            AB::Expr::zero(),
            AB::Expr::zero(),
            local.mem_value_is_neg_not_x0,
        );

        // Assert that correct value of `mem_value_is_pos_not_x0`.
        // SAFETY: If it's a store instruction or a padding row, `mem_value_is_pos = 0`.
        // If it's an unsigned instruction (LBU, LHU, LW), then `mem_value_is_pos = 1`.
        // If it's signed instruction (LB, LH), then `most_sig_bit` will be constrained correctly,
        // and same for `mem_value_is_pos`.
        let mem_value_is_pos = (local.is_lb + local.is_lh) * (AB::Expr::one() - local.most_sig_bit) +
            local.is_lbu +
            local.is_lhu +
            local.is_lw;
        builder.assert_eq(
            local.mem_value_is_pos_not_x0,
            mem_value_is_pos * (AB::Expr::one() - local.op_a_0),
        );

        // When the memory value is not positive and not writing to x0, assert that op_a value is
        // equal to the unsigned memory value.
        builder
            .when(local.mem_value_is_pos_not_x0)
            .assert_word_eq(local.unsigned_mem_val, local.op_a_value);

        // These two cases combine for all cases where it's a load instruction and `op_a_0 == 0`.
        // Since the store instructions have `op_a_immutable = 1`, this completely constrains the
        // `op_a`'s value.
    }
Evaluates constraints related to loading from memory.
crates/core/machine/src/memory/instructions/air.rs