-
Notifications
You must be signed in to change notification settings - Fork 80
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
c7fdc6c
commit 3846637
Showing
7 changed files
with
272 additions
and
14 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
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 |
---|---|---|
@@ -0,0 +1,65 @@ | ||
use std::convert::int; | ||
use std::utils::cross_product; | ||
use std::utils::unchanged_until; | ||
use std::machines::binary::ByteBinary; | ||
|
||
// Computes bitwise operations on two 32-bit numbers | ||
// decomposed into 4 bytes each. | ||
machine Binary8(byte_binary: ByteBinary) with | ||
latch: latch, | ||
operation_id: operation_id, | ||
// Allow this machine to be connected via a permutation | ||
call_selectors: sel, | ||
{ | ||
operation and<0> A1, A2, A3, A4, B1, B2, B3, B4 -> C1, C2, C3, C4; | ||
|
||
operation or<1> A1, A2, A3, A4, B1, B2, B3, B4 -> C1, C2, C3, C4; | ||
|
||
operation xor<2> A1, A2, A3, A4, B1, B2, B3, B4 -> C1, C2, C3, C4; | ||
|
||
col witness operation_id; | ||
|
||
col fixed latch(i) { 1 }; | ||
|
||
col witness A1, A2, A3, A4; | ||
col witness B1, B2, B3, B4; | ||
col witness C1, C2, C3, C4; | ||
|
||
link => C1 = byte_binary.run(operation_id, A1, B1); | ||
link => C2 = byte_binary.run(operation_id, A2, B2); | ||
link => C3 = byte_binary.run(operation_id, A3, B3); | ||
link => C4 = byte_binary.run(operation_id, A4, B4); | ||
} | ||
|
||
// Computes bitwise operations on two 32-bit numbers | ||
// decomposed into two 16-bit limbs each. | ||
machine Binary16(byte_binary: ByteBinary) with | ||
latch: latch, | ||
operation_id: operation_id, | ||
// Allow this machine to be connected via a permutation | ||
call_selectors: sel, | ||
{ | ||
operation and<0> I1, I2, I3, I4 -> O1, O2; | ||
operation or<1> I1, I2, I3, I4 -> O1, O2; | ||
operation xor<2> I1, I2, I3, I4 -> O1, O2; | ||
|
||
col witness operation_id; | ||
|
||
col fixed latch(i) { 1 }; | ||
|
||
let I1: inter = A1 + 256 * A2; | ||
let I2: inter = A3 + 256 * A4; | ||
let I3: inter = B1 + 256 * B2; | ||
let I4: inter = B3 + 256 * B4; | ||
let O1: inter = C1 + 256 * C2; | ||
let O2: inter = C3 + 256 * C4; | ||
|
||
col witness A1, A2, A3, A4; | ||
col witness B1, B2, B3, B4; | ||
col witness C1, C2, C3, C4; | ||
|
||
link => C1 = byte_binary.run(operation_id, A1, B1); | ||
link => C2 = byte_binary.run(operation_id, A2, B2); | ||
link => C3 = byte_binary.run(operation_id, A3, B3); | ||
link => C4 = byte_binary.run(operation_id, A4, B4); | ||
} |
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,9 +1,10 @@ | ||
mod arith; | ||
mod binary; | ||
mod binary_bb; | ||
mod range; | ||
mod hash; | ||
mod memory; | ||
mod memory_with_bootloader_write; | ||
mod shift; | ||
mod split; | ||
mod write_once_memory; | ||
mod write_once_memory; |
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 |
---|---|---|
@@ -0,0 +1,73 @@ | ||
use std::machines::binary::ByteBinary; | ||
use std::machines::binary_bb::Binary16; | ||
|
||
machine Main { | ||
reg pc[@pc]; | ||
reg X0_1[<=]; | ||
reg X0_2[<=]; | ||
reg X1_1[<=]; | ||
reg X1_2[<=]; | ||
reg X2_1[<=]; | ||
reg X2_2[<=]; | ||
reg A1; | ||
reg A2; | ||
|
||
ByteBinary byte_binary; | ||
Binary16 binary(byte_binary); | ||
|
||
instr and X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.and(X0_1, X0_2, X1_1, X1_2); | ||
instr or X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.or(X0_1, X0_2, X1_1, X1_2); | ||
instr xor X0_1, X0_2, X1_1, X1_2 -> X2_1, X2_2 link ~> (X2_1, X2_2) = binary.xor(X0_1, X0_2, X1_1, X1_2); | ||
|
||
instr assert_eq X0_1, X0_2, X1_1, X1_2 { | ||
X0_1 = X1_1, | ||
X0_2 = X1_2 | ||
} | ||
|
||
function main { | ||
|
||
// AND | ||
A1, A2 <== and(0, 0, 0, 0); | ||
assert_eq A1, A2, 0, 0; | ||
A1, A2 <== and(0xffff, 0xffff, 0xffff, 0xffff); | ||
assert_eq A1, A2, 0xffff, 0xffff; | ||
A1, A2 <== and(0xffff, 0xffff, 0xabcd, 0xef01); | ||
assert_eq A1, A2, 0xabcd, 0xef01; | ||
A1, A2 <== and(0xabcd, 0xef01, 0xffff, 0xffff); | ||
assert_eq A1, A2, 0xabcd, 0xef01; | ||
A1, A2 <== and(0, 0, 0xabcd, 0xef01); | ||
assert_eq A1, A2, 0, 0; | ||
A1, A2 <== and(0xabcd, 0xef01, 0, 0); | ||
assert_eq A1, A2, 0, 0; | ||
|
||
// OR | ||
A1, A2 <== or(0, 0, 0, 0); | ||
assert_eq A1, A2, 0, 0; | ||
A1, A2 <== or(0xffff, 0xffff, 0xffff, 0xffff); | ||
assert_eq A1, A2, 0xffff, 0xffff; | ||
A1, A2 <== or(0xffff, 0xffff, 0xabcd, 0xef01); | ||
assert_eq A1, A2, 0xffff, 0xffff; | ||
A1, A2 <== or(0xabcd, 0xef01, 0xffff, 0xffff); | ||
assert_eq A1, A2, 0xffff, 0xffff; | ||
A1, A2 <== or(0, 0, 0xabcd, 0xef01); | ||
assert_eq A1, A2, 0xabcd, 0xef01; | ||
A1, A2 <== or(0xabcd, 0xef01, 0, 0); | ||
assert_eq A1, A2, 0xabcd, 0xef01; | ||
|
||
// XOR | ||
A1, A2 <== xor(0, 0, 0, 0); | ||
assert_eq A1, A2, 0, 0; | ||
A1, A2 <== xor(0xffff, 0xffff, 0xffff, 0xffff); | ||
assert_eq A1, A2, 0, 0; | ||
A1, A2 <== xor(0xffff, 0xffff, 0xabcd, 0xef01); | ||
assert_eq A1, A2, 0x5432, 0x10fe; | ||
A1, A2 <== xor(0xabcd, 0xef01, 0xffff, 0xffff); | ||
assert_eq A1, A2, 0x5432, 0x10fe; | ||
A1, A2 <== xor(0, 0, 0xabcd, 0xef01); | ||
assert_eq A1, A2, 0xabcd, 0xef01; | ||
A1, A2 <== xor(0xabcd, 0xef01, 0, 0); | ||
assert_eq A1, A2, 0xabcd, 0xef01; | ||
|
||
return; | ||
} | ||
} |
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 |
---|---|---|
@@ -0,0 +1,83 @@ | ||
use std::machines::binary::ByteBinary; | ||
use std::machines::binary_bb::Binary8; | ||
|
||
machine Main { | ||
reg pc[@pc]; | ||
reg X0_1[<=]; | ||
reg X0_2[<=]; | ||
reg X0_3[<=]; | ||
reg X0_4[<=]; | ||
reg X1_1[<=]; | ||
reg X1_2[<=]; | ||
reg X1_3[<=]; | ||
reg X1_4[<=]; | ||
reg X2_1[<=]; | ||
reg X2_2[<=]; | ||
reg X2_3[<=]; | ||
reg X2_4[<=]; | ||
reg A1; | ||
reg A2; | ||
reg A3; | ||
reg A4; | ||
|
||
ByteBinary byte_binary; | ||
Binary8 binary(byte_binary); | ||
|
||
instr and X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.and(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4); | ||
instr or X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.or(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4); | ||
instr xor X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 -> X2_1, X2_2, X2_3, X2_4 link ~> (X2_1, X2_2, X2_3, X2_4) = binary.xor(X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4); | ||
|
||
instr assert_eq X0_1, X0_2, X0_3, X0_4, X1_1, X1_2, X1_3, X1_4 { | ||
X0_1 = X1_1, | ||
X0_2 = X1_2, | ||
X0_3 = X1_3, | ||
X0_4 = X1_4 | ||
} | ||
|
||
function main { | ||
|
||
// AND | ||
A1, A2, A3, A4 <== and(0, 0, 0, 0, 0, 0, 0, 0); | ||
assert_eq A1, A2, A3, A4, 0, 0, 0, 0; | ||
A1, A2, A3, A4 <== and(0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff); | ||
assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; | ||
A1, A2, A3, A4 <== and(0xff, 0xff, 0xff, 0xff, 0xab, 0xcd, 0xef, 0x01); | ||
assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; | ||
A1, A2, A3, A4 <== and(0xab, 0xcd, 0xef, 0x01, 0xff, 0xff, 0xff, 0xff); | ||
assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; | ||
A1, A2, A3, A4 <== and(0, 0, 0, 0, 0xab, 0xcd, 0xef, 0x01); | ||
assert_eq A1, A2, A3, A4, 0, 0, 0, 0; | ||
A1, A2, A3, A4 <== and(0xab, 0xcd, 0xef, 0x01, 0, 0, 0, 0); | ||
assert_eq A1, A2, A3, A4, 0, 0, 0, 0; | ||
|
||
// OR | ||
A1, A2, A3, A4 <== or(0, 0, 0, 0, 0, 0, 0, 0); | ||
assert_eq A1, A2, A3, A4, 0, 0, 0, 0; | ||
A1, A2, A3, A4 <== or(0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff); | ||
assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; | ||
A1, A2, A3, A4 <== or(0xff, 0xff, 0xff, 0xff, 0xab, 0xcd, 0xef, 0x01); | ||
assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; | ||
A1, A2, A3, A4 <== or(0xab, 0xcd, 0xef, 0x01, 0xff, 0xff, 0xff, 0xff); | ||
assert_eq A1, A2, A3, A4, 0xff, 0xff, 0xff, 0xff; | ||
A1, A2, A3, A4 <== or(0, 0, 0, 0, 0xab, 0xcd, 0xef, 0x01); | ||
assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; | ||
A1, A2, A3, A4 <== or(0xab, 0xcd, 0xef, 0x01, 0, 0, 0, 0); | ||
assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; | ||
|
||
// XOR | ||
A1, A2, A3, A4 <== xor(0, 0, 0, 0, 0, 0, 0, 0); | ||
assert_eq A1, A2, A3, A4, 0, 0, 0, 0; | ||
A1, A2, A3, A4 <== xor(0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff); | ||
assert_eq A1, A2, A3, A4, 0, 0, 0, 0; | ||
A1, A2, A3, A4 <== xor(0xff, 0xff, 0xff, 0xff, 0xab, 0xcd, 0xef, 0x01); | ||
assert_eq A1, A2, A3, A4, 0x54, 0x32, 0x10, 0xfe; | ||
A1, A2, A3, A4 <== xor(0xab, 0xcd, 0xef, 0x01, 0xff, 0xff, 0xff, 0xff); | ||
assert_eq A1, A2, A3, A4, 0x54, 0x32, 0x10, 0xfe; | ||
A1, A2, A3, A4 <== xor(0, 0, 0, 0, 0xab, 0xcd, 0xef, 0x01); | ||
assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; | ||
A1, A2, A3, A4 <== xor(0xab, 0xcd, 0xef, 0x01, 0, 0, 0, 0); | ||
assert_eq A1, A2, A3, A4, 0xab, 0xcd, 0xef, 0x01; | ||
|
||
return; | ||
} | ||
} |