-
Notifications
You must be signed in to change notification settings - Fork 59
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'feat/init-stdlib' into feat/uints
- Loading branch information
Showing
11 changed files
with
239 additions
and
175 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,30 +1,24 @@ | ||
@ noname.0.7.0 | ||
@ public inputs: 1 | ||
|
||
v_3 == (v_2) * (v_2 + -1) | ||
0 == (v_3) * (1) | ||
1 == (v_4) * (1) | ||
v_6 == (v_5) * (-1 * v_2 + v_4) | ||
-1 * v_7 + 1 == (v_6) * (1) | ||
v_8 == (v_7) * (-1 * v_2 + v_4) | ||
0 == (v_8) * (1) | ||
v_10 == (v_9) * (v_9 + -1) | ||
0 == (v_10) * (1) | ||
1 == (v_11) * (1) | ||
v_13 == (v_12) * (-1 * v_9 + v_11) | ||
-1 * v_14 + 1 == (v_13) * (1) | ||
v_15 == (v_14) * (-1 * v_9 + v_11) | ||
0 == (v_15) * (1) | ||
v_17 == (v_16) * (v_16 + -1) | ||
0 == (v_17) * (1) | ||
1 == (v_18) * (1) | ||
v_20 == (v_19) * (-1 * v_16 + v_18) | ||
-1 * v_21 + 1 == (v_20) * (1) | ||
v_22 == (v_21) * (-1 * v_16 + v_18) | ||
0 == (v_22) * (1) | ||
v_1 == (v_7 + 2 * v_14 + 4 * v_21) * (1) | ||
1 == (-1 * v_7 + 1) * (1) | ||
1 == (v_14) * (1) | ||
1 == (-1 * v_21 + 1) * (1) | ||
v_1 == (v_7 + 2 * v_14 + 4 * v_21) * (1) | ||
1 == (v_3) * (1) | ||
v_5 == (v_4) * (-1 * v_2 + v_3) | ||
-1 * v_6 + 1 == (v_5) * (1) | ||
v_7 == (v_6) * (-1 * v_2 + v_3) | ||
0 == (v_7) * (1) | ||
1 == (v_9) * (1) | ||
v_11 == (v_10) * (-1 * v_8 + v_9) | ||
-1 * v_12 + 1 == (v_11) * (1) | ||
v_13 == (v_12) * (-1 * v_8 + v_9) | ||
0 == (v_13) * (1) | ||
1 == (v_15) * (1) | ||
v_17 == (v_16) * (-1 * v_14 + v_15) | ||
-1 * v_18 + 1 == (v_17) * (1) | ||
v_19 == (v_18) * (-1 * v_14 + v_15) | ||
0 == (v_19) * (1) | ||
v_1 == (v_6 + 2 * v_12 + 4 * v_18) * (1) | ||
1 == (-1 * v_6 + 1) * (1) | ||
1 == (v_12) * (1) | ||
1 == (-1 * v_18 + 1) * (1) | ||
v_1 == (v_6 + 2 * v_12 + 4 * v_18) * (1) | ||
2 == (v_1) * (1) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
37 changes: 14 additions & 23 deletions
37
src/stdlib/native/bits.no → src/stdlib/native/bits/lib.no
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,41 +1,32 @@ | ||
hint fn nth_bit(value: Field, const nth: Field) -> Field; | ||
|
||
fn from_bits(bits: [Bool; LEN]) -> Field { | ||
let mut lc1 = 0; | ||
let mut e2 = 1; | ||
let zero = 0; | ||
|
||
for index in 0..LEN { | ||
lc1 = lc1 + if bits[index] {e2} else {zero}; | ||
e2 = e2 + e2; | ||
} | ||
return lc1; | ||
} | ||
|
||
fn to_bits(const LEN: Field, value: Field) -> [Bool; LEN] { | ||
let mut bits = [false; LEN]; | ||
let mut lc1 = 0; | ||
let mut e2 = 1; | ||
|
||
let one = 1; | ||
let zero = 0; | ||
|
||
// todo: ITE should allow literals | ||
let true_val = true; | ||
let false_val = false; | ||
|
||
for index in 0..LEN { | ||
let bit_num = unsafe nth_bit(value, index); | ||
|
||
// constrain the bit_num to be 0 or 1 | ||
assert_eq(bit_num * (bit_num - 1), 0); | ||
|
||
// convert the bit_num to boolean | ||
bits[index] = if bit_num == 1 {true_val} else {false_val}; | ||
|
||
lc1 = lc1 + if bits[index] {e2} else {zero}; | ||
e2 = e2 + e2; | ||
} | ||
assert_eq(lc1, value); | ||
|
||
assert_eq(from_bits(bits), value); | ||
return bits; | ||
} | ||
|
||
fn from_bits(bits: [Bool; LEN]) -> Field { | ||
let mut lc1 = 0; | ||
let mut e2 = 1; | ||
let zero = 0; | ||
|
||
for index in 0..LEN { | ||
lc1 = lc1 + if bits[index] {e2} else {zero}; | ||
e2 = e2 + e2; | ||
} | ||
return lc1; | ||
} |
File renamed without changes.
Oops, something went wrong.