fix lt
This commit is contained in:
parent
3674c7b2b7
commit
e2a6d4e999
7 changed files with 51 additions and 85 deletions
|
@ -1,8 +0,0 @@
|
|||
// we can compare numbers up to 2^(pbits - 2) - 1, ie any number which fits in (pbits - 2) bits
|
||||
// lt should not work for the maxvalue = 2^(pbits - 2) - 1 augmented by one
|
||||
|
||||
def main(a):
|
||||
pbits = 254
|
||||
// maxvalue = 2**252 - 1
|
||||
maxvalue = 7237005577332262213973186563042994240829374041602535252466099000494570602496 - 1
|
||||
return if 0 < (maxvalue + 1) then 1 else 0 fi
|
|
@ -1,5 +0,0 @@
|
|||
// as p - 1 is greater than p/2, comparing to it should fail
|
||||
|
||||
def main(a):
|
||||
p = 21888242871839275222246405745257275088548364400416034343698204186575808495617
|
||||
return if 0 < p - 1 then 1 else 0 fi
|
|
@ -1,8 +0,0 @@
|
|||
// we can compare numbers up to 2^(pbits - 2) - 1, ie any number which fits in (pbits - 2) bits
|
||||
// lt should work for the maxvalue = 2^(pbits - 2) - 1
|
||||
|
||||
def main(a):
|
||||
pbits = 254
|
||||
// maxvalue = 2**252 - 1
|
||||
maxvalue = 7237005577332262213973186563042994240829374041602535252466099000494570602496 - 1
|
||||
return if 0 < maxvalue then 1 else 0 fi
|
|
@ -1,10 +1,3 @@
|
|||
def bar(a):
|
||||
return a + 42
|
||||
|
||||
def foo():
|
||||
a = 3
|
||||
return bar(a)
|
||||
|
||||
def main():
|
||||
a = foo()
|
||||
return a
|
||||
return if 333 < 77 then 1 else 2 fi
|
||||
|
||||
|
|
|
@ -169,24 +169,13 @@ impl Flattener {
|
|||
statements_flattened
|
||||
.push(FlatStatement::Definition(lhs_id, lhs_flattened));
|
||||
|
||||
let mut lhs_bits = vec![];
|
||||
|
||||
// rhs
|
||||
let rhs_id = self.use_sym();
|
||||
statements_flattened
|
||||
.push(FlatStatement::Definition(rhs_id, rhs_flattened));
|
||||
|
||||
let mut rhs_bits = vec![];
|
||||
|
||||
// check that lhs and rhs are within the right range, ie, their last two bits are zero
|
||||
|
||||
// lhs
|
||||
{
|
||||
// define variables for the bits
|
||||
for i in 0..self.bits {
|
||||
lhs_bits.push(self.use_sym());
|
||||
}
|
||||
|
||||
let lhs_bits: Vec<FlatVariable> = (0..self.bits).map(|_| self.use_sym()).collect();
|
||||
|
||||
// add a directive to get the bits
|
||||
statements_flattened.push(FlatStatement::Directive(DirectiveStatement::new(
|
||||
lhs_bits.clone(),
|
||||
|
@ -197,10 +186,10 @@ impl Flattener {
|
|||
// bitness checks
|
||||
for i in 0..self.bits - 2 {
|
||||
statements_flattened.push(FlatStatement::Definition(
|
||||
lhs_bits[i],
|
||||
lhs_bits[i + 2],
|
||||
FlatExpression::Mult(
|
||||
box FlatExpression::Identifier(lhs_bits[i]),
|
||||
box FlatExpression::Identifier(lhs_bits[i]),
|
||||
box FlatExpression::Identifier(lhs_bits[i + 2]),
|
||||
box FlatExpression::Identifier(lhs_bits[i + 2]),
|
||||
),
|
||||
));
|
||||
}
|
||||
|
@ -212,8 +201,8 @@ impl Flattener {
|
|||
lhs_sum = FlatExpression::Add(
|
||||
box lhs_sum,
|
||||
box FlatExpression::Mult(
|
||||
box FlatExpression::Identifier(lhs_bits[i]),
|
||||
box FlatExpression::Number(T::from(2).pow(i)),
|
||||
box FlatExpression::Identifier(lhs_bits[i + 2]),
|
||||
box FlatExpression::Number(T::from(2).pow(self.bits - 2 - i - 1)),
|
||||
),
|
||||
);
|
||||
}
|
||||
|
@ -227,12 +216,14 @@ impl Flattener {
|
|||
}
|
||||
|
||||
// rhs
|
||||
{
|
||||
let rhs_id = self.use_sym();
|
||||
statements_flattened
|
||||
.push(FlatStatement::Definition(rhs_id, rhs_flattened));
|
||||
|
||||
// rhs
|
||||
{
|
||||
// define variables for the bits
|
||||
for i in 0..self.bits {
|
||||
rhs_bits.push(self.use_sym());
|
||||
}
|
||||
let rhs_bits: Vec<FlatVariable> = (0..self.bits).map(|_| self.use_sym()).collect();
|
||||
|
||||
// add a directive to get the bits
|
||||
statements_flattened.push(FlatStatement::Directive(DirectiveStatement::new(
|
||||
|
@ -244,10 +235,10 @@ impl Flattener {
|
|||
// bitness checks
|
||||
for i in 0..self.bits - 2 {
|
||||
statements_flattened.push(FlatStatement::Definition(
|
||||
rhs_bits[i],
|
||||
rhs_bits[i + 2],
|
||||
FlatExpression::Mult(
|
||||
box FlatExpression::Identifier(rhs_bits[i]),
|
||||
box FlatExpression::Identifier(rhs_bits[i]),
|
||||
box FlatExpression::Identifier(rhs_bits[i + 2]),
|
||||
box FlatExpression::Identifier(rhs_bits[i + 2]),
|
||||
),
|
||||
));
|
||||
}
|
||||
|
@ -259,8 +250,8 @@ impl Flattener {
|
|||
rhs_sum = FlatExpression::Add(
|
||||
box rhs_sum,
|
||||
box FlatExpression::Mult(
|
||||
box FlatExpression::Identifier(rhs_bits[i]),
|
||||
box FlatExpression::Number(T::from(2).pow(i)),
|
||||
box FlatExpression::Identifier(rhs_bits[i + 2]),
|
||||
box FlatExpression::Number(T::from(2).pow(self.bits - 2 - i - 1)),
|
||||
),
|
||||
);
|
||||
}
|
||||
|
@ -275,7 +266,6 @@ impl Flattener {
|
|||
|
||||
// sym = (lhs * 2) - (rhs * 2)
|
||||
let subtraction_result_id = self.use_sym();
|
||||
let mut sub_bits = vec![];
|
||||
|
||||
statements_flattened.push(FlatStatement::Definition(
|
||||
subtraction_result_id,
|
||||
|
@ -286,9 +276,7 @@ impl Flattener {
|
|||
));
|
||||
|
||||
// define variables for the bits
|
||||
for i in 0..self.bits {
|
||||
sub_bits.push(self.use_sym());
|
||||
}
|
||||
let sub_bits: Vec<FlatVariable> = (0..self.bits).map(|_| self.use_sym()).collect();
|
||||
|
||||
// add a directive to get the bits
|
||||
statements_flattened.push(FlatStatement::Directive(DirectiveStatement::new(
|
||||
|
@ -316,7 +304,7 @@ impl Flattener {
|
|||
box expr,
|
||||
box FlatExpression::Mult(
|
||||
box FlatExpression::Identifier(sub_bits[i]),
|
||||
box FlatExpression::Number(T::from(2).pow(i)),
|
||||
box FlatExpression::Number(T::from(2).pow(self.bits - i - 1)),
|
||||
),
|
||||
);
|
||||
}
|
||||
|
|
|
@ -57,4 +57,33 @@ impl<T: Field> Executable<T> for RustHelper {
|
|||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use field::FieldPrime;
|
||||
use super::*;
|
||||
|
||||
#[test]
|
||||
fn bits_of_one() {
|
||||
let inputs = vec![FieldPrime::from(1)];
|
||||
let res = RustHelper::Bits.execute(&inputs).unwrap();
|
||||
assert_eq!(res[253], FieldPrime::from(1));
|
||||
for i in 0..252 {
|
||||
assert_eq!(res[i], FieldPrime::from(0));
|
||||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn bits_of_42() {
|
||||
let inputs = vec![FieldPrime::from(42)];
|
||||
let res = RustHelper::Bits.execute(&inputs).unwrap();
|
||||
assert_eq!(res[253], FieldPrime::from(0));
|
||||
assert_eq!(res[252], FieldPrime::from(1));
|
||||
assert_eq!(res[251], FieldPrime::from(0));
|
||||
assert_eq!(res[250], FieldPrime::from(1));
|
||||
assert_eq!(res[249], FieldPrime::from(0));
|
||||
assert_eq!(res[248], FieldPrime::from(1));
|
||||
assert_eq!(res[247], FieldPrime::from(0));
|
||||
}
|
||||
}
|
|
@ -43,27 +43,4 @@ mod tests {
|
|||
s.insert(key, value);
|
||||
assert_eq!(s.get(&key).unwrap(), value);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn insert_binary_variable() {
|
||||
let mut s = DirectSubstitution::new();
|
||||
let key = FlatVariable::new(1).with_binary(23);
|
||||
let value = FlatVariable::new(123);
|
||||
s.insert(key, value);
|
||||
assert_eq!(s.get(&key).unwrap(), value);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn insert_twice_with_same_prefix() {
|
||||
let mut s = DirectSubstitution::new();
|
||||
let key1 = FlatVariable::new(1).with_binary(23);
|
||||
let value1 = FlatVariable::new(123);
|
||||
let key2 = FlatVariable::new(1).with_binary(24);
|
||||
let value2 = FlatVariable::new(456);
|
||||
s.insert(key1, value1);
|
||||
s.insert(key2, value2);
|
||||
|
||||
assert_eq!(s.get(&key1).unwrap(), value1);
|
||||
assert_eq!(s.get(&key2).unwrap(), value2);
|
||||
}
|
||||
}
|
Loading…
Reference in a new issue