simple_lt

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固定的格式来填充格子，使用上更加简单灵活。

结构体

pub struct SimpleLtGadget<F, const N_BYTES: usize> {
    lhs: Expression<F>,
    rhs: Expression<F>,
    lt: Expression<F>,
    diff: Expression<F>,                         
    range: F, 
}

构造约束

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中的应用

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构建约束:

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进行一次范围约束。