CopyCircuit hi-lo changes

[lightsing]

Layout Changes

CopyCircuitConfig

Dream's design: https://hackmd.io/geYBzdKjRdmO948KCGnh-Q?view

Changes

• is_front_mask: Advice => [LtChip; 16], LtGadget compares address < addr_copy_start.
  is_front_mask implies a byte cell has address < addr_copy_start, which means it's a masked byte and won't be accumlated in the rlc value.

Adds

• value_limbs: [Advice; 16], holds the half word bytes value.
• is_not_back_mask: [LtChip; 16], LtGadget compare address < addr_copy_end.
  This strange naming is for disambiguation, since result needs to be opposite.
  !is_not_back_mask implies a byte cell has address >= address_copy_end, which means it's a masked byte and won't be accumlated in the rlc value.
• is_inbound_read: [LtChip; 16], compare src_addr_end > address.
  The addr_copy_end might be larger than src_addr_end.
  !is_inbound_read implies a byte cell has address >= src_addr_end, which means it's a out-of-bound read, it's value should be 0.

Removes

• value: replaced by value_limbs
• value_prev: no longer used
• word_index: no longer used
• mask: replaced by is_front_mask || !is_not_back_mask
• is_pad: replaced by !is_inbound_read
• is_src_end: replaced by is_inbound_read
• is_word_end: no longer used

CopyTable

Adds

• addr_copy_start: The start of the src/dest address for the copy event. Might not aligned by 32 bytes, indicating masked bytes.
• addr_copy_end: The end of the src/dest address for the copy event. Might not aligned by 32 bytes, indicating masked bytes.

Changes

• address: holds current half-word address, always aligned and increase by 16

Constraint Changes

CopyCircuitConfig

• value_acc == value_acc' + sum(value_i * !(is_front_mask || !is_not_back_mask))
• !is_inbound_read implies value == 0