Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unify all NVIC circuits for a single web-proof circuit #23

Closed
wants to merge 11 commits into from
Closed

Unify all NVIC circuits for a single web-proof circuit #23

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
10c9c07
added test/http/locker.test.ts
0xJepsen Nov 1, 2024
cf2b7f2
use updated circuits local paths. All compile
0xJepsen Nov 1, 2024
69c6129
compose web_proof.circom
0xJepsen Nov 1, 2024
784db46
compose web_proof.circom
0xJepsen Nov 1, 2024
118d4cb
change aes input to data bytes
0xJepsen Nov 1, 2024
a67abae
save
0xJepsen Nov 1, 2024
1723184
save
0xJepsen Nov 1, 2024
493eef5
Update web_proof.circom
0xJepsen Nov 1, 2024
021b3d7
Revert "compose web_proof.circom"
0xJepsen Nov 1, 2024
6d12a42
starting on test
0xJepsen Nov 1, 2024
757ed4f
fix aes fold
0xJepsen Nov 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 20 additions & 18 deletions circuits/aes-gcm/nivc/aes-gctr-nivc.circom
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,25 +5,27 @@ include "../../utils/array.circom";


// Compute AES-GCTR
template AESGCTRFOLD(INPUT_LEN) {
assert(INPUT_LEN % 16 == 0);
var DATA_BYTES = (INPUT_LEN * 2) + 4;
template AESGCTRFOLD(DATA_BYTES) {

assert(DATA_BYTES % 16 == 0);
var TOTAL_BYTES_ACROSS_NIVC = (DATA_BYTES * 2) + 4;

signal input key[16];
signal input iv[12];
signal input aad[16];
signal input plainText[16];

// step_in[0..INPUT_LEN] => accumulate plaintext blocks
// step_in[INPUT_LEN..INPUT_LEN*2] => accumulate ciphertext blocks
// step_in[INPUT_LEN*2..INPUT_LEN*2+4] => accumulate counter
signal input step_in[DATA_BYTES];
signal output step_out[DATA_BYTES];
// step_in[0..DATA_BYTES] => accumulate plaintext blocks
// step_in[DATA_BYTES..DATA_BYTES*2] => accumulate ciphertext blocks
// step_in[DATA_BYTES_LEN*2..DATA_BYTES*2+4] => accumulate counter
signal input step_in[TOTAL_BYTES_ACROSS_NIVC];
signal output step_out[TOTAL_BYTES_ACROSS_NIVC];
signal counter;

// We extract the number from the 4 byte word counter
component last_counter_bits = BytesToBits(4);
for(var i = 0; i < 4; i ++) {
last_counter_bits.in[i] <== step_in[INPUT_LEN*2 + i];
last_counter_bits.in[i] <== step_in[DATA_BYTES*2 + i];
}
component last_counter_num = Bits2Num(32);
// pass in reverse order
Expand All @@ -34,8 +36,8 @@ template AESGCTRFOLD(INPUT_LEN) {
counter <== last_counter_num.out - 1;

// write new plain text block.
signal plainTextAccumulator[DATA_BYTES];
component writeToIndex = WriteToIndex(DATA_BYTES, 16);
signal plainTextAccumulator[TOTAL_BYTES_ACROSS_NIVC];
component writeToIndex = WriteToIndex(TOTAL_BYTES_ACROSS_NIVC, 16);
writeToIndex.array_to_write_to <== step_in;
writeToIndex.array_to_write_at_index <== plainText;
writeToIndex.index <== counter * 16;
Expand All @@ -49,22 +51,22 @@ template AESGCTRFOLD(INPUT_LEN) {
aes.plainText <== plainText;

for(var i = 0; i < 4; i++) {
aes.lastCounter[i] <== step_in[INPUT_LEN*2 + i];
aes.lastCounter[i] <== step_in[DATA_BYTES*2 + i];
}

// accumulate cipher text
signal cipherTextAccumulator[DATA_BYTES];
component writeCipherText = WriteToIndex(DATA_BYTES, 16);
signal cipherTextAccumulator[TOTAL_BYTES_ACROSS_NIVC];
component writeCipherText = WriteToIndex(TOTAL_BYTES_ACROSS_NIVC, 16);
writeCipherText.array_to_write_to <== plainTextAccumulator;
writeCipherText.array_to_write_at_index <== aes.cipherText;
writeCipherText.index <== INPUT_LEN + counter * 16;
writeCipherText.index <== DATA_BYTES + counter * 16;
writeCipherText.out ==> cipherTextAccumulator;

// get counter
signal counterAccumulator[DATA_BYTES];
component writeCounter = WriteToIndex(DATA_BYTES, 4);
signal counterAccumulator[TOTAL_BYTES_ACROSS_NIVC];
component writeCounter = WriteToIndex(TOTAL_BYTES_ACROSS_NIVC, 4);
writeCounter.array_to_write_to <== cipherTextAccumulator;
writeCounter.array_to_write_at_index <== aes.counter;
writeCounter.index <== INPUT_LEN*2;
writeCounter.index <== DATA_BYTES*2;
writeCounter.out ==> step_out;
}
1 change: 0 additions & 1 deletion circuits/aes-gctr-nivc.circom
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,5 @@ pragma circom 2.1.9;

include "aes-gcm/nivc/aes-gctr-nivc.circom";

// Note(WJ 2024-10-31): I put this here like this because i have tests i wanted to include for this component
// the circomkit tests become unhappy when there is a main.
component main { public [step_in] } = AESGCTRFOLD(48);
34 changes: 2 additions & 32 deletions circuits/extract_value.circom
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,35 +1,5 @@
pragma circom 2.1.9;

include "circomlib/circuits/gates.circom";
include "@zk-email/circuits/utils/array.circom";
include "json/nivc/extractor.circom";

template MaskExtractFinal(TOTAL_BYTES, maxValueLen) {
signal input step_in[TOTAL_BYTES];
signal output step_out[TOTAL_BYTES];

signal is_zero_mask[TOTAL_BYTES];
signal is_prev_starting_index[TOTAL_BYTES];
signal value_starting_index[TOTAL_BYTES];

value_starting_index[0] <== 0;
is_prev_starting_index[0] <== 0;
is_zero_mask[0] <== IsZero()(step_in[0]);
for (var i=1 ; i<TOTAL_BYTES ; i++) {
is_zero_mask[i] <== IsZero()(step_in[i]);
is_prev_starting_index[i] <== IsZero()(value_starting_index[i-1]);
value_starting_index[i] <== value_starting_index[i-1] + i * (1-is_zero_mask[i]) * is_prev_starting_index[i];
}

// log("value starting index", value_starting_index[TOTAL_BYTES-1]);

signal value[maxValueLen] <== SelectSubArray(TOTAL_BYTES, maxValueLen)(step_in, value_starting_index[TOTAL_BYTES-1], maxValueLen);
for (var i = 0 ; i < maxValueLen ; i++) {
// log(i, value[i]);
step_out[i] <== value[i];
}
for (var i = maxValueLen ; i < TOTAL_BYTES ; i++) {
step_out[i] <== 0;
}
}

component main { public [step_in] } = MaskExtractFinal(4160, 200);
component main { public [step_in] } = MaskExtractFinal(49, 32, 32);
36 changes: 2 additions & 34 deletions circuits/http_body_mask.circom
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,38 +1,6 @@
pragma circom 2.1.9;

include "parser-attestor/circuits/http/interpreter.circom";
include "http/nivc/body_mask.circom";

template HTTPMaskBodyNIVC(TOTAL_BYTES, DATA_BYTES) {
// ------------------------------------------------------------------------------------------------------------------ //
// ~~ Set sizes at compile time ~~
// Total number of variables in the parser for each byte of data
var PER_ITERATION_DATA_LENGTH = 5;
// -> var TOTAL_BYTES = DATA_BYTES * (PER_ITERATION_DATA_LENGTH + 1); // data + parser vars
// ------------------------------------------------------------------------------------------------------------------ //

// ------------------------------------------------------------------------------------------------------------------ //
// ~ Unravel from previous NIVC step ~
// Read in from previous NIVC step (HttpParseAndLockStartLine or HTTPLockHeader)
signal input step_in[TOTAL_BYTES];

signal data[DATA_BYTES];
signal parsing_body[DATA_BYTES];
for (var i = 0 ; i < DATA_BYTES ; i++) {
data[i] <== step_in[i];
parsing_body[i] <== step_in[DATA_BYTES + i * 5 + 4];
}

// ------------------------------------------------------------------------------------------------------------------ //
// ~ Write out to next NIVC step
signal output step_out[TOTAL_BYTES];
for (var i = 0 ; i < DATA_BYTES ; i++) {
step_out[i] <== data[i] * parsing_body[i];
}
// Write out padded with zeros
for (var i = DATA_BYTES ; i < TOTAL_BYTES ; i++) {
step_out[i] <== 0;
}
}

component main { public [step_in] } = HTTPMaskBodyNIVC(4160, 320);
component main { public [step_in] } = HTTPMaskBodyNIVC(48, 16);

86 changes: 2 additions & 84 deletions circuits/http_lock_header.circom
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,87 +1,5 @@
pragma circom 2.1.9;

include "parser-attestor/circuits/http/interpreter.circom";
include "parser-attestor/circuits/utils/array.circom";

template LockHeader(TOTAL_BYTES, DATA_BYTES, headerNameLen, headerValueLen) {
// ------------------------------------------------------------------------------------------------------------------ //
// ~~ Set sizes at compile time ~~
// Total number of variables in the parser for each byte of data
var PER_ITERATION_DATA_LENGTH = 5;
var TOTAL_BYTES_USED = DATA_BYTES * (PER_ITERATION_DATA_LENGTH + 1); // data + parser vars
// ------------------------------------------------------------------------------------------------------------------ //

// ------------------------------------------------------------------------------------------------------------------ //
// ~ Unravel from previous NIVC step ~
// Read in from previous NIVC step (HttpParseAndLockStartLine or HTTPLockHeader)
signal input step_in[TOTAL_BYTES];

signal data[DATA_BYTES];
for (var i = 0 ; i < DATA_BYTES ; i++) {
data[i] <== step_in[i];
}

signal input header[headerNameLen];
signal input value[headerValueLen];

component headerNameLocation = FirstStringMatch(DATA_BYTES, headerNameLen);
headerNameLocation.data <== data;
headerNameLocation.key <== header;

component headerFieldNameValueMatch;
headerFieldNameValueMatch = HeaderFieldNameValueMatch(DATA_BYTES, headerNameLen, headerValueLen);
headerFieldNameValueMatch.data <== data;
headerFieldNameValueMatch.headerName <== header;
headerFieldNameValueMatch.headerValue <== value;
headerFieldNameValueMatch.index <== headerNameLocation.position;

// TODO: Make this assert we are parsing header!!!
// This is the assertion that we have locked down the correct header
headerFieldNameValueMatch.out === 1;

// ------------------------------------------------------------------------------------------------------------------ //
// ~ Write out to next NIVC step
signal output step_out[TOTAL_BYTES];
for (var i = 0 ; i < DATA_BYTES ; i++) {
// add plaintext http input to step_out
step_out[i] <== step_in[i];

// add parser state
step_out[DATA_BYTES + i * 5] <== step_in[DATA_BYTES + i * 5];
step_out[DATA_BYTES + i * 5 + 1] <== step_in[DATA_BYTES + i * 5 + 1];
step_out[DATA_BYTES + i * 5 + 2] <== step_in[DATA_BYTES + i * 5 + 2];
step_out[DATA_BYTES + i * 5 + 3] <== step_in[DATA_BYTES + i * 5 + 3];
step_out[DATA_BYTES + i * 5 + 4] <== step_in[DATA_BYTES + i * 5 + 4];
}
// Pad remaining with zeros
for (var i = TOTAL_BYTES_USED ; i < TOTAL_BYTES ; i++ ) {
step_out[i] <== 0;
}
}

// TODO: Handrolled template that I haven't tested YOLO.
template FirstStringMatch(dataLen, keyLen) {
signal input data[dataLen];
signal input key[keyLen];
signal output position;

var matched = 0;
var counter = 0;
component stringMatch[dataLen - keyLen];
component hasMatched[dataLen - keyLen];
for (var idx = 0 ; idx < dataLen - keyLen ; idx++) {
stringMatch[idx] = IsEqualArray(keyLen);
stringMatch[idx].in[0] <== key;
for (var key_idx = 0 ; key_idx < keyLen ; key_idx++) {
stringMatch[idx].in[1][key_idx] <== data[idx + key_idx] * (1 - matched);
}
hasMatched[idx] = IsEqual();
hasMatched[idx].in <== [stringMatch[idx].out, 1];
matched += hasMatched[idx].out;
counter += (1 - matched); // TODO: Off by one? Move before?
}
position <== counter;
}

component main { public [step_in] } = LockHeader(4160, 320, 12, 31);
include "http/nivc/lock_header.circom";

component main { public [step_in] } = LockHeader(48, 16, 12, 16);
125 changes: 2 additions & 123 deletions circuits/http_parse_and_lock_start_line.circom
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,126 +1,5 @@
pragma circom 2.1.9;

include "parser-attestor/circuits/http/parser/machine.circom";
include "parser-attestor/circuits/http/interpreter.circom";
include "parser-attestor/circuits/utils/bytes.circom";
include "http/nivc/parse_and_lock_start_line.circom";

// TODO: Note that TOTAL_BYTES will match what we have for AESGCMFOLD step_out
// I have not gone through to double check the sizes of everything yet.
template LockStartLine(TOTAL_BYTES, DATA_BYTES, beginningLen, middleLen, finalLen) {
// ------------------------------------------------------------------------------------------------------------------ //
// ~~ Set sizes at compile time ~~
// Total number of variables in the parser for each byte of data
var AES_BYTES = DATA_BYTES + 50; // TODO: Might be wrong, but good enough for now
var PER_ITERATION_DATA_LENGTH = 5;
var TOTAL_BYTES_USED = DATA_BYTES * (PER_ITERATION_DATA_LENGTH + 1); // data + parser vars
// ------------------------------------------------------------------------------------------------------------------ //

// ------------------------------------------------------------------------------------------------------------------ //
// ~ Unravel from previous NIVC step ~
// Read in from previous NIVC step (JsonParseNIVC)
signal input step_in[TOTAL_BYTES];

signal data[DATA_BYTES];
for (var i = 0 ; i < DATA_BYTES ; i++) {
data[i] <== step_in[50 + i];
}

// // TODO: check if these needs to here or not
// component dataASCII = ASCII(DATA_BYTES);
// dataASCII.in <== data;

signal input beginning[beginningLen];
signal input middle[middleLen];
signal input final[finalLen];

// Initialze the parser
component State[DATA_BYTES];
State[0] = HttpStateUpdate();
State[0].byte <== data[0];
State[0].parsing_start <== 1;
State[0].parsing_header <== 0;
State[0].parsing_field_name <== 0;
State[0].parsing_field_value <== 0;
State[0].parsing_body <== 0;
State[0].line_status <== 0;

/*
Note, because we know a beginning is the very first thing in a request
we can make this more efficient by just comparing the first `beginningLen` bytes
of the data ASCII against the beginning ASCII itself.
*/
// Check first beginning byte
signal beginningIsEqual[beginningLen];
beginningIsEqual[0] <== IsEqual()([data[0],beginning[0]]);
beginningIsEqual[0] === 1;

// Setup to check middle bytes
signal startLineMask[DATA_BYTES];
signal middleMask[DATA_BYTES];
signal finalMask[DATA_BYTES];

var middle_start_counter = 1;
var middle_end_counter = 1;
var final_end_counter = 1;
for(var data_idx = 1; data_idx < DATA_BYTES; data_idx++) {
State[data_idx] = HttpStateUpdate();
State[data_idx].byte <== data[data_idx];
State[data_idx].parsing_start <== State[data_idx - 1].next_parsing_start;
State[data_idx].parsing_header <== State[data_idx - 1].next_parsing_header;
State[data_idx].parsing_field_name <== State[data_idx - 1].next_parsing_field_name;
State[data_idx].parsing_field_value <== State[data_idx - 1].next_parsing_field_value;
State[data_idx].parsing_body <== State[data_idx - 1].next_parsing_body;
State[data_idx].line_status <== State[data_idx - 1].next_line_status;

// Check remaining beginning bytes
if(data_idx < beginningLen) {
beginningIsEqual[data_idx] <== IsEqual()([data[data_idx], beginning[data_idx]]);
beginningIsEqual[data_idx] === 1;
}

// Set the masks based on parser state
startLineMask[data_idx] <== inStartLine()(State[data_idx].parsing_start);
middleMask[data_idx] <== inStartMiddle()(State[data_idx].parsing_start);
finalMask[data_idx] <== inStartEnd()(State[data_idx].parsing_start);

// Increment counters based on mask information
middle_start_counter += startLineMask[data_idx] - middleMask[data_idx] - finalMask[data_idx];
middle_end_counter += startLineMask[data_idx] - finalMask[data_idx];
final_end_counter += startLineMask[data_idx];
}

// Additionally verify beginning had correct length
beginningLen === middle_start_counter - 1;

// Check middle is correct by substring match and length check
signal middleMatch <== SubstringMatchWithIndex(DATA_BYTES, middleLen)(data, middle, middle_start_counter);
middleMatch === 1;
middleLen === middle_end_counter - middle_start_counter - 1;

// Check final is correct by substring match and length check
signal finalMatch <== SubstringMatchWithIndex(DATA_BYTES, finalLen)(data, final, middle_end_counter);
finalMatch === 1;
// -2 here for the CRLF
finalLen === final_end_counter - middle_end_counter - 2;

// ------------------------------------------------------------------------------------------------------------------ //
// ~ Write out to next NIVC step (Lock Header)
signal output step_out[TOTAL_BYTES];
for (var i = 0 ; i < DATA_BYTES ; i++) {
// add plaintext http input to step_out
step_out[i] <== step_in[50 + i];

// add parser state
step_out[DATA_BYTES + i * 5] <== State[i].next_parsing_start;
step_out[DATA_BYTES + i * 5 + 1] <== State[i].next_parsing_header;
step_out[DATA_BYTES + i * 5 + 2] <== State[i].next_parsing_field_name;
step_out[DATA_BYTES + i * 5 + 3] <== State[i].next_parsing_field_value;
step_out[DATA_BYTES + i * 5 + 4] <== State[i].next_parsing_body;
}
// Pad remaining with zeros
for (var i = TOTAL_BYTES_USED ; i < TOTAL_BYTES ; i++ ) {
step_out[i] <== 0;
}
}

component main { public [step_in] } = LockStartLine(4160, 320, 8, 3, 2);
component main { public [step_in] } = ParseAndLockStartLine(48, 16, 8, 3, 2);
4 changes: 1 addition & 3 deletions circuits/json/nivc/extractor.circom
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,4 @@ template MaskExtractFinal(DATA_BYTES, MAX_STACK_HEIGHT, MAX_VALUE_LENGTH) {
}
// TODO: Do anything with last depth?
// step_out[TOTAL_BYTES_ACROSS_NIVC - 1] <== 0;
}

// component main { public [step_in] } = MaskExtractFinal(4160, 320, 200);
}
Loading
Loading