zkevm-docs/8-arithmetic.markdown

@@ -164,26 +164,55 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 - Length 
   arithmetic中的布局: 
 
-| tag | cnt | operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo |
-|-----|-----|-----|-----|-----|-----|
-| Length| 1| length| offset| data_size| 0|
-| Length| 0|normal_length |zero_length |0 | 0|
 
-  输入：length,offset,data_size  
-  输出：normal_length, zero_length  
-  计算方式：  
-      以codecopy为例，length:为要copy的长度，offset为bytecode偏移量(即复制起始位置)，data_size为bytecode的总长度
-  ```rust
-  fn length(length: u64, offset: u64, data_size: u64) -> (normal_length: u64, zero_length: u64) {
-      if offset > data_size {
-          return 0, length
-      } else if offset + length < data_size {
-          return length,0
+| tag | cnt | operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo | u16_0 | u16_1 | u16_2 | u16_3 | u16_4 | u16_5 | u16_6 | u16_7 |
+|-----|-----|-----|-----|-----|-----|-----|-----|-----|-----|-----|-----|-----|-----| 
+| Length| 3|  0 |   0  | 0 |  0 |  length_minus_datasize-minus-offset_0 | length_minus_datasize-minus-offset_1 | length_minus_datasize-minus-offset_2 |length_minus_datasize-minus-offset_3 |   datasize_minus_offset_0 | datasize_minus_offset_1 | datasize_minus_offset_2 | datasize_minus_offset_3 |
+| Length| 2| length_gt_datasize-minus-offset | datasize_gt_offset | offset_24_inv | offset_overflow | offset_lo_0 | offset_lo_1 | offset_lo_2 | offset_lo_3 | offset_lo_4 | offset_lo_5 | offset_lo_6 | offset_lo_7 | address_8 | address_9 |
+| Length| 1| offset_hi| offset_lo | real_length | zero_length  | datasize_lo_0 | datasize_lo_1 | datasize_lo_2 | datasize_lo_3 | datasize_lo_4 | datasize_lo_5 | datasize_lo_6 | datasize_lo_7 |  
+| Length| 0|length_hi | length_lo | datasize_hi | datasize_lo  |  length_lo_0 | length_lo_1 | length_lo_2 | length_lo_3 | length_lo_4 | length_lo_5 | length_lo_6 | length_lo_7 | 
+   
+  限制: 
+```rust
+    // datasize_lo_16 constraints 
+    let expr_datasize = expr_from_u16s([datasize_lo_0,datasize_lo_1,datasize_lo_2,datasize_lo_3]);
+    datasize_lo = expr_from_u16s([datasize_lo_0,datasize_lo_1,datasize_lo_2,datasize_lo_3,datasize_lo_4,datasize_lo_5,datasize_lo_6,datasize_lo_7]);
+    // length_lo_16 constraints 
+    let expr_length = expr_from_u16s([length_lo_0,length_lo_1,length_lo_2,length_lo_3]);
+    length_lo = expr_from_u16s([length_lo_0,length_lo_1,length_lo_2,length_lo_3,length_lo_4,length_lo_5,length_lo_6,length_lo_7]);
+    // offset_lo_16 constraints 
+    let offset_24 = offset_hi *2^64 + expr_from_u16s([offset_lo_4,offset_lo_5,offset_lo_6,offset_7]);
+    let is_offset_24_zero = SimpleIsZero(offset_24,offset_24_inv,"");
+    offset_overflow = (1-is_offset_24_zero)
+    let expr_offset = expr_from_u16s([offset_lo_0,offset_lo_1,offset_lo_2,offset_lo_3]);
+    if offset_overflow {
+        expr_offset = 0xffffffffffffffff;
     }else{
-          return data_size-offset, offset+length-data_size
+        offset_lo = expr_offset;
     } 
+    // 
+    let datasize_gt_offset, datasize_minus_offset = expr_datasize - expr_offset;
+    // datasize_minus_offset = datasize_gt_offset * 2^64 + expr_datasize - expr_offset;
+    if !datasize_gt_offset {
+        real_length = 0;
+        zero_length = expr_length;
+    }else{
+    let length_gt_datasize-minus-offset , length_minus_datasize-minus-offset  = expr_length - datasize_minus_offset;
+    // length_minus_datasize-minus-offset = length_gt_datasize-minus-offset * 2^64 + expr_length - datasize_minus_offset ;
+    if !length_gt_datasize-minus-offset {
+        real_length = expr_length;
+        zero_length = 0;
+    }else {
+        real_length = datasize_minus_offset;
+        zero_length = length_minus_datasize-minus-offset
     }
-  ```
+}
+      
+```
+  输入：length,offset,data_size  
+  输出：real_length, zero_length  
+ 
+
   
 # 实现 arithmetic 子电路中 Add 例子