init

.gitignore

@@ -0,0 +1,3 @@
+*.r1cs
+*.bin
+node_modules/*

README.md

@@ -1,2 +1,5 @@
 # web-prover-circuits
- Circuits for Pluto's `web-prover`
+Circuits for Pluto's `web-prover`
+
+## Releases
+Will zip up all artifacts for the circuits with versions for ease of use!

aes_gcm.circom

@@ -0,0 +1,91 @@
+pragma circom 2.1.9;
+
+include "aes-proof/circuits/aes-gcm/aes-gcm-foldable.circom";
+include "aes-proof/circuits/aes-gcm/utils.circom";
+include "@zk-email/circuits/utils/array.circom";
+
+
+template AESGCMFOLD(bytesPerFold, totalBytes, inputBytes) {
+    // cannot fold outside chunk boundaries.
+    assert(bytesPerFold % 16 == 0);
+    assert(totalBytes % 16 == 0);
+
+    signal input key[16];
+    signal input iv[12];
+    signal input aad[16];
+    signal input plainText[bytesPerFold];
+    // signal input cipherText[totalBytes];
+
+    // Output from the last encryption step
+    // Always use last bytes for inputs which are not same size.
+    // step_in[0..4] => lastCounter
+    // step_in[4..20] => lastTag
+    // step_in[20..21] => foldedBlocks
+    // step_in[22] => plainText matching // TODO: ccan just check, don't need to carry over
+    // step_in[23] => cipherText matching // TODO: ccan just check, don't need to carry over
+    signal input step_in[inputBytes];
+
+    // For now, attempt to support variable fold size. Potential fix at 16 in the future.
+    component aes = AESGCMFOLDABLE(bytesPerFold, totalBytes\16);
+    aes.key       <== key;
+    aes.iv        <== iv;
+    aes.aad       <== aad;
+    aes.plainText <== plainText;
+
+    // Fold inputs
+    var inputIndex = bytesPerFold - 4;
+    for(var i = 0; i < 4; i++) {
+        aes.lastCounter[i] <== step_in[inputIndex];
+        inputIndex+=1;
+    }
+
+    for(var i = 0; i < 16; i++) {
+        aes.lastTag[i] <== step_in[inputIndex];
+        inputIndex+=1;
+    }
+    // TODO: range check, assertions, stuff.
+    inputIndex+=15;
+    aes.foldedBlocks <== step_in[inputIndex];
+
+    // Fold Outputs
+    signal output step_out[inputBytes];
+    var outputIndex = 0;
+    for (var i = 0 ; i < bytesPerFold - 4 ; i++) {
+        step_out[outputIndex] <== 0;
+        outputIndex += 1;
+    }
+    for(var i = 0; i < 4; i++) {
+        step_out[outputIndex] <== aes.counter[i];
+        outputIndex += 1;
+    }
+    for(var i = 0; i < 16; i++) {
+        step_out[outputIndex] <== aes.authTag[i];
+        outputIndex += 1;
+    }
+    for (var i = 0 ; i < 15 ; i++) {
+        // TODO: check correctness
+        step_out[outputIndex] <== 0;
+        outputIndex += 1;
+    }
+    step_out[outputIndex] <== step_in[47] + bytesPerFold \ 16;
+
+    // // Constrain
+    // signal plainTextCheckIndex           <== 48 + ((step_in[15] - 1) * bytesPerFold);
+    // signal plainTextBlock[bytesPerFold]  <== SelectSubArray(inputBytes, bytesPerFold)(step_in, plainTextCheckIndex, bytesPerFold);
+    // signal isPlainTextMatch              <== IsEqualArray(bytesPerFold)([plainText, plainTextBlock]);
+    step_out[48] <== step_in[48];
+    // step_out[48]                         <== step_in[48] * isPlainTextMatch;
+
+    // // Constrain ciphertext matches
+    // signal cipherTextCheckIndex          <== (step_in[15] - 1) * bytesPerFold;
+    // signal cipherTextBlock[bytesPerFold] <== SelectSubArray(totalBytes, bytesPerFold)(cipherText, cipherTextCheckIndex, bytesPerFold);
+    // signal isCipherTextMatch             <== IsEqualArray(bytesPerFold)([aes.cipherText, cipherTextBlock]);
+    step_out[49] <== step_in[49];
+    // step_out[49]                         <== step_in[49] * isCipherTextMatch;
+
+    for(var i = 50 ; i < inputBytes ; i++) {
+        step_out[i] <== step_in[i];
+    }
+}
+
+component main { public [step_in] } = AESGCMFOLD(16, 320, 4160);

extract_value.circom

@@ -0,0 +1,35 @@
+pragma circom 2.1.9;
+
+include "circomlib/circuits/gates.circom";
+include "@zk-email/circuits/utils/array.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);

http_body_mask.circom

@@ -0,0 +1,38 @@
+pragma circom 2.1.9;
+
+include "parser-attestor/circuits/http/interpreter.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);
+

http_lock_header.circom

@@ -0,0 +1,87 @@
+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);
+

http_parse_and_lock_start_line.circom

@@ -0,0 +1,126 @@
+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";
+
+// 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);