feat(arithmetization): sha2 precompile

.github/workflows/arithmetization-guest-programs-run.yml

@@ -65,6 +65,15 @@ jobs:
         working-directory: arithmetization/src/test
         timeout-minutes: 30
 
+      # Builds sha2_provider.zig with SHA2_ACCEL=true (the Zig SHA-256 wrapper) and runs it through
+      # the full interpreter, exercising the R_EVM_SHA2 custom-op dispatch. The target forces tracing
+      # mode (ZKC_EXEC_FLAGS=) because the interpreter's fast backend currently fails on an unrelated
+      # pre-existing instruction; the guest is self-checking and exits non-zero on any mismatch.
+      - name: Run SHA-256 accelerator guest with zkc interpreter
+        run: make sha2-zig-exec
+        working-directory: arithmetization/src/test
+        timeout-minutes: 30
+
       - name: Run l2-execution guest program with zkc interpreter
         run: make -C riscv-guests/l2-execution exec
         timeout-minutes: 30

arithmetization/src/main/lib/README.md

@@ -4,7 +4,7 @@ This folder contains the zkvm library: zkc implementations of EVM precompiles an
 | EVM precompiles     | status |    opc   | funct3 |   funct7  |
 |---------------------|:------:|:--------:|:------:|:---------:|
 | ECRECOVER           |   🔴   | custom-0 | 0b000  | 0b0000001 |
-| SHA2-256            |   🔴   | custom-0 |  0b... | 0b.....10 |
+| SHA2-256            |   🟢   | custom-0 | 0b000  | 0b0000010 |
 | RIPEMD              |   🔴   | custom-0 |  0b... | 0b.....11 |
 | IDENTITY            |   🔴   | custom-0 |  0b... | 0b....100 |
 | MODEXP_small        |   🔴   | custom-0 |  0b..0 | 0b....101 |

arithmetization/src/main/lib/sha2/constants.zkc

@@ -0,0 +1,91 @@
+// SHA-256 round constants: the first 32 bits of the fractional parts of the
+// cube roots of the first 64 prime numbers (FIPS 180-4 section 4.2.2).
+static SHA2_K(address:u6) -> (constant:u32) {
+    0x428a2f98,
+    0x71374491,
+    0xb5c0fbcf,
+    0xe9b5dba5,
+    0x3956c25b,
+    0x59f111f1,
+    0x923f82a4,
+    0xab1c5ed5,
+    0xd807aa98,
+    0x12835b01,
+    0x243185be,
+    0x550c7dc3,
+    0x72be5d74,
+    0x80deb1fe,
+    0x9bdc06a7,
+    0xc19bf174,
+    0xe49b69c1,
+    0xefbe4786,
+    0x0fc19dc6,
+    0x240ca1cc,
+    0x2de92c6f,
+    0x4a7484aa,
+    0x5cb0a9dc,
+    0x76f988da,
+    0x983e5152,
+    0xa831c66d,
+    0xb00327c8,
+    0xbf597fc7,
+    0xc6e00bf3,
+    0xd5a79147,
+    0x06ca6351,
+    0x14292967,
+    0x27b70a85,
+    0x2e1b2138,
+    0x4d2c6dfc,
+    0x53380d13,
+    0x650a7354,
+    0x766a0abb,
+    0x81c2c92e,
+    0x92722c85,
+    0xa2bfe8a1,
+    0xa81a664b,
+    0xc24b8b70,
+    0xc76c51a3,
+    0xd192e819,
+    0xd6990624,
+    0xf40e3585,
+    0x106aa070,
+    0x19a4c116,
+    0x1e376c08,
+    0x2748774c,
+    0x34b0bcb5,
+    0x391c0cb3,
+    0x4ed8aa4a,
+    0x5b9cca4f,
+    0x682e6ff3,
+    0x748f82ee,
+    0x78a5636f,
+    0x84c87814,
+    0x8cc70208,
+    0x90befffa,
+    0xa4506ceb,
+    0xbef9a3f7,
+    0xc67178f2
+}
+
+// SHA-256 initial hash values (FIPS 180-4 section 5.3.3).
+const SHA2_INITIAL_H0:u32 = 0x6a09e667
+const SHA2_INITIAL_H1:u32 = 0xbb67ae85
+const SHA2_INITIAL_H2:u32 = 0x3c6ef372
+const SHA2_INITIAL_H3:u32 = 0xa54ff53a
+const SHA2_INITIAL_H4:u32 = 0x510e527f
+const SHA2_INITIAL_H5:u32 = 0x9b05688c
+const SHA2_INITIAL_H6:u32 = 0x1f83d9ab
+const SHA2_INITIAL_H7:u32 = 0x5be0cd19
+
+const SHA2_BLOCK_BYTE_LENGTH:u32 = 64
+const SHA2_PADDING_START:u8 = 0x80
+
+// sha2_state layout: W[0..64) followed by H[0..8).
+const SHA2_H0:u7 = 64
+const SHA2_H1:u7 = 65
+const SHA2_H2:u7 = 66
+const SHA2_H3:u7 = 67
+const SHA2_H4:u7 = 68
+const SHA2_H5:u7 = 69
+const SHA2_H6:u7 = 70
+const SHA2_H7:u7 = 71

arithmetization/src/main/lib/sha2/impl.zkc

@@ -0,0 +1,162 @@
+include "constants.zkc"
+include "utils.zkc"
+include "../../riscv/memory.zkc"
+include "../../riscv/ram/read.zkc"
+include "../../riscv/ram/write.zkc"
+include "../../riscv/utils/type.zkc"
+
+// Compute SHA-256 over msg_length bytes in guest RAM. The custom instruction
+// ABI supplies the input address through rs1, the byte length through rs2, and
+// the output address through the current value of rd. Like the Keccak
+// accelerator, the instruction does not modify the architectural value of rd.
+//
+// The accelerated ABI currently accepts lengths through the interpreter's u32
+// path, matching Keccak. SHA-256's encoded bit length is nevertheless formed in
+// u64 before shifting, so all supported byte lengths are encoded correctly.
+fn sha2<ram, sha2_state>(msg_address:Address, msg_length:u32, output_address:Address) {
+    sha2_initialize()
+
+    // todo(arijit): use divmod (/%) once zkc version is bumped in prover-ray
+    var full_blocks:u32 = msg_length / SHA2_BLOCK_BYTE_LENGTH
+    var remainder:u6 = (msg_length % SHA2_BLOCK_BYTE_LENGTH) as u6
+    var current_address:Address = msg_address
+
+    // Absorb every complete message block before writing any output. This is
+    // important when the caller's input and output ranges overlap.
+    for block:u32 = 0; block<full_blocks; block = block + 1 {
+        sha2_load_message_block(current_address)
+        sha2_compress()
+        current_address = current_address + (SHA2_BLOCK_BYTE_LENGTH as Address)
+    }
+
+    var bit_length:u64 = (msg_length as u64) << 3
+    var bit_length_high:u32
+    var bit_length_low:u32
+    bit_length_high::bit_length_low = bit_length
+
+    // The final message bytes and 0x80 always fit in one block. The 64-bit
+    // length fits there as well only when the remainder is at most 55 bytes.
+    sha2_load_padding_block(current_address, remainder)
+    if remainder<56 {
+        sha2_state[14] = bit_length_high
+        sha2_state[15] = bit_length_low
+        sha2_compress()
+    } else {
+        sha2_compress()
+        sha2_load_length_block(bit_length_high, bit_length_low)
+        sha2_compress()
+    }
+
+    sha2_write_digest(output_address)
+}
+
+fn sha2_initialize<sha2_state>() {
+    sha2_state[SHA2_H0] = SHA2_INITIAL_H0
+    sha2_state[SHA2_H1] = SHA2_INITIAL_H1
+    sha2_state[SHA2_H2] = SHA2_INITIAL_H2
+    sha2_state[SHA2_H3] = SHA2_INITIAL_H3
+    sha2_state[SHA2_H4] = SHA2_INITIAL_H4
+    sha2_state[SHA2_H5] = SHA2_INITIAL_H5
+    sha2_state[SHA2_H6] = SHA2_INITIAL_H6
+    sha2_state[SHA2_H7] = SHA2_INITIAL_H7
+}
+
+// Load one complete message block. Guest RAM stores bytes little-endian within
+// each RAM word, while SHA-256 interprets every schedule word as big-endian.
+fn sha2_load_message_block<ram, sha2_state>(address:Address) {
+    for i:u5 = 0; i<16; i = i + 1 {
+        var word_address:Address = address + (4 * (i as Address))
+        var b0:u8 = read_8(word_address)
+        var b1:u8 = read_8(word_address + 1)
+        var b2:u8 = read_8(word_address + 2)
+        var b3:u8 = read_8(word_address + 3)
+        sha2_state[i as u7] = b0::b1::b2::b3
+    }
+}
+
+// Load the first padding block: remaining message bytes, one 0x80 byte, then
+// zeroes. The caller replaces W[14..16] with the length when it fits.
+fn sha2_load_padding_block<ram, sha2_state>(address:Address, remainder:u6) {
+    for word_index:u5 = 0; word_index<16; word_index = word_index + 1 {
+        var byte_index:u6 = (word_index as u6) << 2
+        var b0:u8 = sha2_padding_byte(address, remainder, byte_index)
+        var b1:u8 = sha2_padding_byte(address, remainder, byte_index + 1)
+        var b2:u8 = sha2_padding_byte(address, remainder, byte_index + 2)
+        var b3:u8 = sha2_padding_byte(address, remainder, byte_index + 3)
+        sha2_state[word_index as u7] = b0::b1::b2::b3
+    }
+}
+
+fn sha2_padding_byte<ram>(address:Address, remainder:u6, index:u6) -> (value:u8) {
+    if index<remainder {
+        value = read_8(address + (index as Address))
+    } else if index == remainder {
+        value = SHA2_PADDING_START
+    } else {
+        value = 0
+    }
+}
+
+fn sha2_load_length_block<sha2_state>(bit_length_high:u32, bit_length_low:u32) {
+    for i:u5 = 0; i<14; i = i + 1 {
+        sha2_state[i as u7] = 0
+    }
+    sha2_state[14] = bit_length_high
+    sha2_state[15] = bit_length_low
+}
+
+fn sha2_extend_schedule<sha2_state>() {
+    for i:u7 = 16; i<64; i = i + 1 {
+        var sigma0:u32 = sha2_small_sigma0(sha2_state[i - 15])
+        var sigma1:u32 = sha2_small_sigma1(sha2_state[i - 2])
+        sha2_state[i] = sha2_add4(sha2_state[i - 16], sigma0, sha2_state[i - 7], sigma1)
+    }
+}
+
+fn sha2_compress<sha2_state>() {
+    sha2_extend_schedule()
+
+    var a:u32 = sha2_state[SHA2_H0]
+    var b:u32 = sha2_state[SHA2_H1]
+    var c:u32 = sha2_state[SHA2_H2]
+    var d:u32 = sha2_state[SHA2_H3]
+    var e:u32 = sha2_state[SHA2_H4]
+    var f:u32 = sha2_state[SHA2_H5]
+    var g:u32 = sha2_state[SHA2_H6]
+    var h:u32 = sha2_state[SHA2_H7]
+
+    for i:u7 = 0; i<64; i = i + 1 {
+        var t1:u32 = sha2_add5(h, sha2_big_sigma1(e), sha2_choose(e, f, g), SHA2_K[i as u6], sha2_state[i])
+        var t2:u32 = sha2_add2(sha2_big_sigma0(a), sha2_majority(a, b, c))
+
+        h = g
+        g = f
+        f = e
+        e = sha2_add2(d, t1)
+        d = c
+        c = b
+        b = a
+        a = sha2_add2(t1, t2)
+    }
+
+    sha2_state[SHA2_H0] = sha2_add2(sha2_state[SHA2_H0], a)
+    sha2_state[SHA2_H1] = sha2_add2(sha2_state[SHA2_H1], b)
+    sha2_state[SHA2_H2] = sha2_add2(sha2_state[SHA2_H2], c)
+    sha2_state[SHA2_H3] = sha2_add2(sha2_state[SHA2_H3], d)
+    sha2_state[SHA2_H4] = sha2_add2(sha2_state[SHA2_H4], e)
+    sha2_state[SHA2_H5] = sha2_add2(sha2_state[SHA2_H5], f)
+    sha2_state[SHA2_H6] = sha2_add2(sha2_state[SHA2_H6], g)
+    sha2_state[SHA2_H7] = sha2_add2(sha2_state[SHA2_H7], h)
+}
+
+fn sha2_write_digest<ram, sha2_state>(output_address:Address) {
+    for i:u4 = 0; i<8; i = i + 1 {
+        var b0:u8, b1:u8, b2:u8, b3:u8
+        b0::b1::b2::b3 = sha2_state[SHA2_H0 + (i as u7)]
+        var word_address:Address = output_address + (4 * (i as Address))
+        write_8(word_address, b0)
+        write_8(word_address + 1, b1)
+        write_8(word_address + 2, b2)
+        write_8(word_address + 3, b3)
+    }
+}

arithmetization/src/main/lib/sha2/utils.zkc

@@ -0,0 +1,46 @@
+// SHA-256 uses addition modulo 2^32. Each helper performs the addition in a
+// wide unsigned type and then decomposes the result into a range-constrained
+// carry and low word. The carry is intentionally discarded.
+fn sha2_add2(a:u32, b:u32) -> (result:u32) {
+    var carry:u1
+    carry::result = (a as u33) + (b as u33)
+}
+
+fn sha2_add4(a:u32, b:u32, c:u32, d:u32) -> (result:u32) {
+    var carry:u2
+    carry::result = (a as u34) + (b as u34) + (c as u34) + (d as u34)
+}
+
+fn sha2_add5(a:u32, b:u32, c:u32, d:u32, e:u32) -> (result:u32) {
+    var carry:u3
+    carry::result = (a as u35) + (b as u35) + (c as u35) + (d as u35) + (e as u35)
+}
+
+fn sha2_rotr32(value:u32, amount:u5) -> (result:u32) {
+    var inverse_amount:u6 = 32 - (amount as u6)
+    result = (value >> amount) | (value << inverse_amount)
+}
+
+fn sha2_small_sigma0(value:u32) -> (result:u32) {
+    result = sha2_rotr32(value, 7) ^ sha2_rotr32(value, 18) ^ (value >> 3)
+}
+
+fn sha2_small_sigma1(value:u32) -> (result:u32) {
+    result = sha2_rotr32(value, 17) ^ sha2_rotr32(value, 19) ^ (value >> 10)
+}
+
+fn sha2_big_sigma0(value:u32) -> (result:u32) {
+    result = sha2_rotr32(value, 2) ^ sha2_rotr32(value, 13) ^ sha2_rotr32(value, 22)
+}
+
+fn sha2_big_sigma1(value:u32) -> (result:u32) {
+    result = sha2_rotr32(value, 6) ^ sha2_rotr32(value, 11) ^ sha2_rotr32(value, 25)
+}
+
+fn sha2_choose(e:u32, f:u32, g:u32) -> (result:u32) {
+    result = (e & f) ^ ((~e) & g)
+}
+
+fn sha2_majority(a:u32, b:u32, c:u32) -> (result:u32) {
+    result = (a & b) ^ (a & c) ^ (b & c)
+}

arithmetization/src/main/riscv/instruction_processing/r_type.zkc

@@ -8,6 +8,7 @@ include "../utils/signed_comparisons.zkc"
 include "../utils/multiplication.zkc"
 include "../../lib/ecrecover/impl.zkc"
 include "../../lib/keccak/impl.zkc"
+include "../../lib/sha2/impl.zkc"
 include "../../lib/io/write_output.zkc"
 include "../../lib/poseidon2/ram.zkc"
 
@@ -41,7 +42,7 @@ include "../../lib/poseidon2/ram.zkc"
 // treat register values as two's-complement integers.  Division and remainder
 // follow RISC-V semantics: division by zero returns −1 (or the dividend for REM),
 // and signed overflow (INT_MIN / −1) returns INT_MIN (or 0 for REM).
-fn process_R_type_instruction<registers, ram, keccak_state, poseidon2_state>(opcode:Opcode, instruction_parameters:u25,
+fn process_R_type_instruction<registers, ram, keccak_state, sha2_state, poseidon2_state>(opcode:Opcode, instruction_parameters:u25,
 output_write_address:OutputAddress) ->
 (new_output_write_address:OutputAddress) {
 
@@ -315,7 +316,7 @@ output_write_address:OutputAddress) ->
         }
 
         //
-        // case CUSTOM_1
+        // custom precompiles
         //
         case R_EVM_ECRECOVER: {
             printf "EVM ECRECOVER precompile "
@@ -329,6 +330,12 @@ output_write_address:OutputAddress) ->
             new_output_write_address = output_write_address
             return
         }
+        case R_EVM_SHA2: {
+            printf "EVM SHA2-256 precompile "
+            sha2(v1 as Address, v2 as u32, registers[rd] as Address)
+            new_output_write_address = output_write_address
+            return
+        }
         case R_KECCAK: {
             printf "KECCAK precompile "
             keccak(v1 as Address, v2 as u32, registers[rd] as Address)

arithmetization/src/main/riscv/interpreter.zkc

@@ -8,7 +8,7 @@ include "instruction_processing/s_type.zkc"
 include "instruction_processing/j_type.zkc"
 include "instruction_processing/u_type.zkc"
 
-fn interpreter<registers, ram, keccak_state, poseidon2_state>(instruction:u32, pc:Address, output_write_address:OutputAddress) -> (new_pc:Address, new_output_write_address:OutputAddress) {
+fn interpreter<registers, ram, keccak_state, sha2_state, poseidon2_state>(instruction:u32, pc:Address, output_write_address:OutputAddress) -> (new_pc:Address, new_output_write_address:OutputAddress) {
 
     var instruction_parameters:u25
     var instruction_type:Type

arithmetization/src/main/riscv/main.zkc

@@ -13,7 +13,7 @@ include "utils/register_utils.zkc"
 include "memory.zkc"
 
 // TODO @Ghost
-fn main<registers, ram, keccak_state, poseidon2_state>() {
+fn main<registers, ram, keccak_state, sha2_state, poseidon2_state>() {
     var instruction:Instruction
     var clock_cycle:u32 = 0
     var entry_point:Address
@@ -48,4 +48,3 @@ fn main<registers, ram, keccak_state, poseidon2_state>() {
         pc, output_write_address = interpreter(instruction, pc, output_write_address)
     }
 }
-

arithmetization/src/main/riscv/memory.zkc

@@ -38,5 +38,10 @@ const C:u7 = 80
 const D:u7 = 88
 const PIB:u7 = 96
 
+// SHA-256 scratch memory: W[0..64) is the message schedule and H[64..72)
+// stores the chaining state. Every schedule word is overwritten per block and
+// every chaining word is reinitialized per invocation.
+memory sha2_state(address:u7) -> (word:u32)
+
 // guest program output
 pub output guest_output(address:OutputAddress) -> (byte:u8)