zkevm-docs/8-arithmetic.markdown

@@ -414,55 +414,138 @@ a * b + c = d
 
 ## Length 
 
-arithmetic中的布局: 
+### length  电路功能：
 
+输入 offset, length, size
 
-| 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 |
-| 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 | 
+返回 real\_len, zero\_len, overflow, _real\_len\_is\_zero, zero\_len\_is\_zero(？待定)_
 
-  限制: 
-```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{
-        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  
+*   offset，length，size，需要 u64\_overflow 约束
+    
+*   判断 offset + length > size
+    
+*   三种情况_(不用管length是否为0)_，需要返回    **return (real\_len, zero\_len)**：                   
+    
+
+1.  offset + length <= size，                    **return (length,  0)**
+    
+2.  offset + length > size，分为两种情况：
+    
+    1.  offset < size ，                            **return (size - offset, offset + length - size)**
+        
+    2.  offset >= size,                             **return (0, length).**
+
+### arithmetic中的布局: 
+
+
+| operand0     | operand1     | operand2         | operand3         | cnt | u16s(0-3) | u16s(4_7)        |
+|--------------|--------------|------------------|------------------|-----|-----------|------------------|
+| real_len_inv | zero_len_inv | lt_offset_size   |                  | 2   | diff      | diff_offset_size |
+| real_len     | zero_len     | real_len_is_zero | zero_len_is_zero | 1   | size      | offset_bound     |
+| offset       | length       | size             | overflow         | 0   | offset    | length           |
+
+### 约束
+
+1.  **operand 和 u16s 大小相等**
+    
+    1.  offset, size, length
+        
+    2.  offset\_bound = offset + length
+        
+
+2.  **约束 size 是否小于 offset\_bound**
+    
+    1.  使用 SimpleLtGadget::new(size, offset\_bound, overflow, diff)，range 设置为2^64
+        
+    2.  overflow is bool
+        
+
+3.  **约束 offset 是否小于 size**
+    
+    1.  使用 SimpleLtGadget::new(offset, size, lt\_offset\_size, diff\_offset\_size)，range 设置为2^64
+        
+    2.  lt\_offset\_size is bool
+        
+
+4.  **三种情况下 (real\_len, zero\_len) 的约束：**
+                
+
+**参考上文，使用overflow 和  lt\_offset\_size 作为 selector，那么公式为：**
+
+1.  real\_len = (1-overflow) \* length 
+    
+
++ overflow \*  lt\_offset\_size \* (size - offset)
+
+2.  zero\_len = overflow \* lt\_offset\_size \* (offset\_bound - size)
+    
+
++ overflow \* (1 - lt\_offset\_size) \* length
+
+5.  **约束 real\_len\_is\_zero, zero\_len\_is\_zero**
+    
+    1.  SimpleIsZero（real\_len，real\_len\_inv）
+        
+    2.  SimpleIsZero（zero\_len，zero\_len\_inv）
+
+## memory expansion
+
+memory expansion 电路的功能是给定offset\_bound，计算是否需要拓展内存。
+
+offset\_bound 的代表的是访问内存段的**右区间**：
+
+1.  访问长度length是固定的，比如 mload 指令, offset = 10，mload 一次访问 length=32，那么offset\_bound = 42.
+    
+2.  另外还存在另一种情况，访问内存时，给定了 offset， length 是任意值：当length 不为0，那么 offset\_bound = offset + length。当length = 0，offset\_bound = 0，所以这时候无论offset取什么值，内存都不会拓展。
+    
+
+### 电路设计
+
+|  operand0  |  operand1  |  operand2  |  operand3  |  cnt  |  u16s(0-3)  |  u16s(4\_7)  |
+| --- | --- | --- | --- | --- | --- | --- |
+|  r0  |   |   |   |  1  |  diff  |  r1\|r2\|r3\|r4  |
+|  offset\_bound  |  memory\_chunk\_prev  |  expansion\_tag  |  access\_memory\_size  |  0  |  offset\_bound  |  access\_memory\_size  |
+
+### 约束设计：
+
+:::
+**约束 operand 和 u16s** 
+:::
+
+*   offset\_bound  = offset\_bound
+    
+*   access\_memory\_size = access\_memory\_size
+    
+*    SimpleBinaryNumber::new（ ++r0|r1|r2|r3|r4++ ）.value  = remainder 
+    
+
+:::
+**约束** access_memory_size = \lfloor (offset + 31) / 32  \rfloor
+:::
+
+*   access\_memory\_size \* 32 + remainder = offset + 31
+    
+
+:::
+**约束** memory_chunk_cur = Max( memory_chunk_prev， access_memory_size)
+:::
+
+*   约束 expansion\_tag 是 0 或 1
+    
+*   使用 SimpleLtGadget::new(memory\_chunk\_prev, access\_memory\_size, expansion\_tag, diff)，range 设置为2^64
+    
+
+### 有length 的时候如何约束offset\_bound
+
+添加加一个 length\_inv _(大部分电路里面已经有了)_
+
+因为如果length= 0，offset\_bound = 0; 
+
+否则 offset\_bound = （offset + length）
+
+那么公式为：
+
+**offset\_bound = (offset + length) \* length \* length\_inv**
 
 ## U64Overflow