Constraints for memory ops:

[vivekvpandya]

The proposed constraints try to capture following semantics of RISC-V load store instructions

The LW instruction loads a 32-bit value from memory into rd. LH loads a 16-bit value from memory,
then sign-extends to 32-bits before storing in rd. LHU loads a 16-bit value from memory but then
zero extends to 32-bits before storing in rd. LB and LBU are defined analogously for 8-bit values.
The SW, SH, and SB instructions store 32-bit, 16-bit, and 8-bit values from the low bits of register
rs2 to memory.

New columns for memory stark:

register_value // rename current value column)
memory_value
reg_val_limbs // array of 32 Field
mem_val_limbs // array of 32 Field
sign_extended_mem_val // just to keep overall degree to 3

Constraints:

let reg_value_8_bits = reduce_with_powers(reg_val_limbs[0..7], 2);
let reg_value_16_bits = reduce_with_powers(reg_val_limbs[0..15], 2);
let mem_value_8_bits = reduce_with_powers(mem_val_limbs[0..7], 2);
let mem_value_16_bits = reduce_with_powers(mem_val_limbs[0..15], 2);
let signed_mem_value_8_bits = reduce_with_powers([1,1,1,1, 1,1,1,1, 1,1,1,1, 1,1,1,1, 1,1,1,1, 1,1,1,1].concat(mem_val_limbs[0..7]), 2);
let signed_mem_value_16_bits = reduce_with_powers([1,1,1,1, 1,1,1,1, 1,1,1,1, 1,1,1,1].concat(mem_val_limbs[0..15]), 2);

// Make sure reg_val_limbs and register value are related to each other
(register_value - reduce_with_powers(reg_val_limbs[0..31], 2)

// Make sure mem_val_limbs and memory_value are related to each other
(memory_value - reduce_with_powers(mem_val_limbs[0..31], 2)

// Make sure memory cell gets only lower 8 bits of register value
is_SB * (reg_value_8_bits - memory_value)

// Make sure memory cell gets only lower 16 bits of register value
is_SH * (reg_value_16_bits - memory_value)

// Make sure register and memory value are same
(is_SW + is_LW) * (register_value - memory_value)

// Make sure only lower 8 bits are loaded into register.
is_LBU * (register_value - mem_value_8_bits)

// Make sure only lower 16 bits are loaded into register.
is_LHU * (register_value - mem_value_16_bits)

// Make sure sign_extended_mem_val column is generated correctly when op is LB.
is_LB * (sign_extended_mem_val - (mem_val_limbs[7] * signed_mem_value_8_bits + (1 - mem_val_limbs[7]) * mem_value_8_bits))

// Make sure sign_extended_mem_val column is generated correctly when op is LH.
is_LH * (sign_extended_mem_val - (mem_val_limbs[15] * signed_mem_value_16_bits + (1 - mem_val_limbs[15]) * mem_value_16_bits))

// Make sure register gets correct value
(is_LB + is_LH) * (register_value - sign_extended_mem_val)

[matthiasgoergens]

It seems like you want the individual limbs to do something like a bitwise AND? We already have a 'gadget' for that. See how the shift instructions re-use it.

[vivekvpandya]

For SB/SH AND gadget work but , can we get sign extension with it for LB/LH?

AND gadget is based on XOR , which uses similar idea of dividing into 32 limbs.
So it feels my proposed constraints should not perform any worst than AND based solution