code-notes/simple_lt.markdown

-# simple_lt.rs内容和用法
-
-## 一、内容
-
-### 核心公式
-
-`lhs - rhs == diff - (lt * range)`
-
-### 作用
-
-- 用于比较lhs是否小于rhs（最大支持一个格子，也即U128，区别simple_lt_word的用法）；
-- 延伸用途：可用于确定一个数是否为负数；
-
-注：diff应该是在range的范围内，在外部使用gadget时，要注意diff的范围。
-
-### 延伸用途讲解
-
-结论：假设操作数lhs为16bit的操作数，当lt=1，得到lhs为正数，当lt=0得到lhs应为负数。
-
-过程推导与讲解（假设lhs为16bit操作数）：
-
-- 该公式由减法公式推导而来，减法公式中有`a-b=c-carry<<16`，假设a,b为16bit操作数，在sub公式中，我们已有结论carry = 1时，a<b，carry = 0时，a>=b。
-- 将rhs设为2^15，range设为2^16，根据减法公式，则有lt=1时，lhs<rhs，那么代表lhs最高位不为1，该数应为正数，反之则有负数。
-
-### 与lt电路区别
-
-考虑与lt_gt电路的比较，本质上使用的是sub减法来进行两个数之间的比较，对于U256的比较有以下公式：
-
-```
-a_lo - b_lo = c_lo - carry_lo << 128
-a_hi - b_hi - carry_lo = c_hi - carry_hi << 128
-```
-
-当使用gadget时，用途更加简单明了，在我们只想比较类似于`a_hi`和`b_hi`的大小时，使用此公式不需要考虑`carry_lo`的情况。
-
-总结，与sub减法最终能实现的效果基本类似，但是不需要按照sub固定的格式来填充格子，使用上更加简单灵活。
-
-### 结构体
-
-```rust
-pub struct SimpleLtGadget<F, const N_BYTES: usize> {
-    lhs: Expression<F>,
-    rhs: Expression<F>,
-    lt: Expression<F>,
-    diff: Expression<F>,                         
-    range: F, 
-}
-
-```
-
-### 构造约束
-
-```rust
-pub fn get_constraints(&self) -> Vec<(String, Expression<F>)> {
-        let mut res: Vec<(String, Expression<F>)> = Vec::new();
-
-        // The equation we require to hold: `lhs - rhs == diff - (lt * range)`.
-        res.push((
-            "lhs - rhs == diff - (lt ⋅ range)".to_string(),
-            (self.lhs.clone() - self.rhs.clone())
-                - (self.diff.clone() - self.lt.clone() * self.range.clone()),
-        ));
-
-        res
-    }
-```
-
-该约束为核心公式中的算法。
-
-## 二、用法
-
-### slt_sgt中的应用
-
-```rust
-let rhs = Expression::Constant(F::from(SLTSGTRHS));
-let a_is_lt: SimpleLtGadget<F, 2> = SimpleLtGadget::new(&a_hi_u16, &rhs, &lt[0], &diff[0]);
-```
-
-这里的用法即为a为16bit的操作数，其中SLTSGTRHS为2^15。
-
-当构建完成后，可以直接使用`a_is_lt构建约束`:
-
-```rust
-constraints.extend(a_is_lt.get_constraints());
-```
-
-### div_mod中的应用
-
-在上述基础上，还需要添加对diff的范围约束，如下：
-
-```
- constraints.push((
-    format!("diff_{} = u16 sum", hi_or_lo),
-    diff[i].clone() - u16_sum_for_diff[i].clone(),
-));
-```
-
-上面两处应用中，slt_sgt中没有对diff进行范围约束的原因是diff的格子是在u16s的表中，已经约束了该值为u16，所以不需要再额外的对diff进行约束，如果diff在U256的格子里，例如分配在了oprand_0_hi、oprand_0_lo中，则需要对diff进行一次范围约束。
+# simple_lt.rs内容和用法
+
+## 一、内容
+
+### 核心公式
+
+`lhs - rhs == diff - (lt * range)`
+
+### 作用
+
+- 用于比较lhs是否小于rhs（最大支持一个格子，也即U128，区别simple_lt_word的用法）；
+- 延伸用途：可用于确定一个数是否为负数；
+
+注：diff应该是在range的范围内，在外部使用gadget时，要注意diff的范围。
+
+### 延伸用途讲解
+
+结论：假设操作数lhs为16bit的操作数，当lt=1，得到lhs为正数，当lt=0得到lhs应为负数。
+
+过程推导与讲解（假设lhs为16bit操作数）：
+
+- 该公式由减法公式推导而来，减法公式中有`a-b=c-carry<<16`，假设a,b为16bit操作数，在sub公式中，我们已有结论carry = 1时，a<b，carry = 0时，a>=b。
+- 将rhs设为`2^15`，range设为`2^16`，根据减法公式，则有lt=1时，lhs<rhs，那么代表lhs最高位不为1，该数应为正数，反之则有负数。
+
+### 与lt电路区别
+
+考虑与lt_gt电路的比较，本质上使用的是sub减法来进行两个数之间的比较，对于U256的比较有以下公式：
+
+```
+a_lo - b_lo = c_lo - carry_lo << 128
+a_hi - b_hi - carry_lo = c_hi - carry_hi << 128
+```
+
+当使用gadget时，用途更加简单明了，在我们只想比较类似于`a_hi`和`b_hi`的大小时，使用此公式不需要考虑`carry_lo`的情况。
+
+总结，与sub减法最终能实现的效果基本类似，但是不需要按照sub固定的格式来填充格子，使用上更加简单灵活。
+
+### 结构体
+
+```rust
+pub struct SimpleLtGadget<F, const N_BYTES: usize> {
+    lhs: Expression<F>,
+    rhs: Expression<F>,
+    lt: Expression<F>,
+    diff: Expression<F>,                         
+    range: F, 
+}
+
+```
+
+### 构造约束
+
+```rust
+pub fn get_constraints(&self) -> Vec<(String, Expression<F>)> {
+        let mut res: Vec<(String, Expression<F>)> = Vec::new();
+
+        // The equation we require to hold: `lhs - rhs == diff - (lt * range)`.
+        res.push((
+            "lhs - rhs == diff - (lt ⋅ range)".to_string(),
+            (self.lhs.clone() - self.rhs.clone())
+                - (self.diff.clone() - self.lt.clone() * self.range.clone()),
+        ));
+
+        res
+    }
+```
+
+该约束为核心公式中的算法。
+
+## 二、用法
+
+### slt_sgt中的应用
+
+```rust
+let rhs = Expression::Constant(F::from(SLTSGTRHS));
+let a_is_lt: SimpleLtGadget<F, 2> = SimpleLtGadget::new(&a_hi_u16, &rhs, &lt[0], &diff[0]);
+```
+
+这里的用法即为a为16bit的操作数，其中SLTSGTRHS为2^15。
+
+当构建完成后，可以直接使用`a_is_lt构建约束`:
+
+```rust
+constraints.extend(a_is_lt.get_constraints());
+```
+
+### div_mod中的应用
+
+在上述基础上，还需要添加对diff的范围约束，如下：
+
+```
+ constraints.push((
+    format!("diff_{} = u16 sum", hi_or_lo),
+    diff[i].clone() - u16_sum_for_diff[i].clone(),
+));
+```
+
+上面两处应用中，slt_sgt中没有对diff进行范围约束的原因是diff的格子是在u16s的表中，已经约束了该值为u16，所以不需要再额外的对diff进行约束，如果diff在U256的格子里，例如分配在了oprand_0_hi、oprand_0_lo中，则需要对diff进行一次范围约束。