simple_lt_word.rs内容和用法

一、内容

作用

用于比较U256位的lhs是否小于rhs。

结构体

包含了两个gadget结构体，在simple_lt的基础上进行应用

pub struct SimpleComparisonGadget<F, const N_BYTES: usize> {
    lt: SimpleLtGadget<F, N_BYTES>, // lt = 1时，有lhs<rhs，即simple_lt的概念
    eq: SimpleIsZero<F>, // eq = 1 代表 lhs == rhs, 即 simple_is_zero的概念
}

pub struct SimpleLtWordGadget<F> {
    comparison_hi: SimpleComparisonGadget<F, Lt_Word_N_BYTES>, // 即SimpleComparisonGadget，可用与判断两数是否相等
    lt_lo: SimpleLtGadget<F, Lt_Word_N_BYTES>, // lt = 1时，有lhs<rhs，即simple_lt的概念
}

核心公式

hi_lt + hi_eq * lt_lo

hi_lt: 高位比较
hi_eq: 高位是否相等
lt_lo: 低位比较

也即，可以分为以下情况：

• 当hi_lt = 1时，代表已得出高位比较结果，此时能够确定lhs < rhs，此时hi_eq为0。总结：hi_lt = 1时，公式结果为1，有lhs < rhs；
• 当hi_lt = 0时，hi_eq = 1时，通过lt_lo比较两数大小，此时lt_lo = 1，代表lhs<rhs，否则 lhs >= rhs。总结：hi_lt = 0 且 hi_eq = 1时，lt = 1，公式结果为1，代表lhs < rhs；
• 当hi_lt = 0时，hi_eq = 0时，可得出lhs > rhs。总结：hi_lt = 0 且 hi_eq = 0，公式结果为0，得出lhs > rhs；

通过上述三种结果分析可得：当公式结果输出为1时，有 lhr < rhs，当公式结果输出为0时，有lhs >= rhs的结论。由于我们的目的是为了比较lhs < rhs的情况，我们只需要关注公式输出为1时的结果，能够满足我们的需求。

构造约束

SimpleComparisonGadget的约束：

pub fn get_constraints(&self) -> Vec<(String, Expression<F>)> {
    let mut res: Vec<(String, Expression<F>)> = Vec::new();

    res.extend(self.lt.get_constraints());
    res.extend(self.eq.get_constraints());

    res
}

SimpleLtWordGadget的约束：

pub fn get_constraints(&self) -> Vec<(String, Expression<F>)> {
    let mut res: Vec<(String, Expression<F>)> = Vec::new();

    res.extend(self.comparison_hi.get_constraints());
    res.extend(self.lt_lo.get_constraints());

    res
}

二、用法

在div_mod中有具体使用方法，如下：

let is_lt_lo = SimpleLtGadget::new(&c[1], &b[1], &lt[1], &diff[1]);
let comparison = SimpleComparisonGadget::new(&c[0], &b[0], &lt[0], is_zero, &diff[0]);

let is_lt = SimpleLtWordGadget::new(comparison, is_lt_lo);

其中c[1],b[1],lt[1],diff[1]代表c_lo,b_lo,lt_lo,diff_lo。