feat(vm): add constrained SHA-256 compression precompile

bin/cli/src/main.rs

@@ -412,7 +412,7 @@ fn cmd_execute(
     // below (the flamegraph path drives execution inside the executor and does
     // not expose per-log data). `None` means "not counted", so the accel lines
     // are omitted rather than printed as misleading zeros.
-    let mut accel_counts: Option<(u64, u64)> = None;
+    let mut accel_counts: Option<(u64, u64, u64)> = None;
 
     let cycle_count = if let Some(ref output_path) = flamegraph.path {
         // Shared execute+flamegraph path (executor::flamegraph) instead of
@@ -480,6 +480,7 @@ fn cmd_execute(
         let mut cycle_count: u64 = 0;
         let mut keccak_calls: u64 = 0;
         let mut ecsm_calls: u64 = 0;
+        let mut sha256_calls: u64 = 0;
         // Reused per chunk: `(current_pc, a7)` for logs whose a7 matches an
         // accelerator syscall number. This is a cheap superset — a non-ECALL
         // instruction can hold the same value in src1 — that `accelerator_of`
@@ -512,6 +513,7 @@ fn cmd_execute(
                 match accelerator_of(executor.instructions.get(pc), a7) {
                     Some(Accelerator::Keccak) => keccak_calls += 1,
                     Some(Accelerator::Ecsm) => ecsm_calls += 1,
+                    Some(Accelerator::Sha256) => sha256_calls += 1,
                     None => {}
                 }
             }
@@ -526,16 +528,17 @@ fn cmd_execute(
         }
 
         if cycles {
-            accel_counts = Some((keccak_calls, ecsm_calls));
+            accel_counts = Some((keccak_calls, ecsm_calls, sha256_calls));
         }
         cycle_count
     };
 
     if cycles {
         println!("Cycles: {}", cycle_count);
-        if let Some((keccak_calls, ecsm_calls)) = accel_counts {
+        if let Some((keccak_calls, ecsm_calls, sha256_calls)) = accel_counts {
             println!("Keccak calls: {}", keccak_calls);
             println!("Ecsm calls: {}", ecsm_calls);
+            println!("Sha256 compression calls: {}", sha256_calls);
         }
     }
 
@@ -1104,13 +1107,16 @@ mod tests {
 
     // `accelerator_of` must match the prover's `CpuOperation::from_log`: count an
     // invocation only when the instruction is an ECALL AND a7 is the accelerator
-    // syscall number. Covers both accelerators, the non-accelerator syscalls, a
+    // syscall number. Covers all accelerators, the non-accelerator syscalls, a
     // non-ECALL whose src1 collides with an accelerator number, and a cache miss.
     #[test]
     fn accelerator_of_mirrors_prover_classification() {
         use executor::vm::instruction::execution::{ECSM_SYSCALL_NUMBER, KECCAK_SYSCALL_NUMBER};
 
         let ecall = Instruction::EcallEbreak;
+        let sha = executor::vm::instruction::execution::SHA256_SYSCALL_NUMBER;
+        assert_eq!(accelerator_of(Some(&ecall), sha), Some(Accelerator::Sha256));
+        assert_eq!(accelerator_of(Some(&Instruction::Fence), sha), None);
 
         assert_eq!(
             accelerator_of(Some(&ecall), KECCAK_SYSCALL_NUMBER),

crypto/ethrex-crypto/src/lib.rs

@@ -8,6 +8,8 @@
 //! Accelerated today:
 //! - `keccak256`: a sponge over the `keccak_permute` precompile (riscv64; on
 //!   host it falls back to software keccak for tests).
+//! - `sha256`: the padding wrapper over the SHA-256 compression precompile
+//!   (riscv64; on host it falls back to the trait's own sha2 default).
 //! - `secp256k1_ecrecover`: the ECDSA recovery's 2-term linear combination is
 //!   evaluated through the ECSM `ecsm_mul` precompile (riscv64), reconstructing
 //!   the full point from x-only queries; on host / degenerate inputs it falls
@@ -63,6 +65,18 @@ impl Crypto for LambdaVmEcsmCrypto {
         #[cfg(not(target_arch = "riscv64"))]
         return keccak_hash(input);
     }
+
+    fn sha256(&self, input: &[u8]) -> [u8; 32] {
+        // riscv64 guest: IV, padding and the length encoding in the wrapper,
+        // the 64 rounds per block in the compression accelerator.
+        #[cfg(target_arch = "riscv64")]
+        return lambda_vm_syscalls::sha256::sha256(input);
+        // host (tests / non-guest): the ecall isn't available off-target.
+        // `NativeCrypto` takes every trait default, so this is the same sha2
+        // call the default `sha256` would have made, with no extra dependency.
+        #[cfg(not(target_arch = "riscv64"))]
+        return ethrex_crypto::NativeCrypto.sha256(input);
+    }
 }
 
 // ── ECDSA secp256k1 recovery via the ECSM precompile ────────────────────────

crypto/stark/src/table.rs

@@ -457,6 +457,15 @@ impl<F: IsField> Table<F> {
         self.data[idx] = value;
     }
 
+    /// Whether the row-major data is backed by the spill mmap rather than the
+    /// heap. Exposed so callers can assert that a table they expected to spill
+    /// actually did: nothing else about a spilled table is observable from the
+    /// outside, since every accessor reads through the backing transparently.
+    #[cfg(feature = "disk-spill")]
+    pub fn is_spilled(&self) -> bool {
+        self.mmap_backing.is_some()
+    }
+
     /// Spill the table's row-major data to a temp file and mmap it back.
     /// Frees the heap `data` Vec while preserving access through
     /// [`Self::get`], [`Self::get_row`], and [`Self::columns`].

docs/precompiles/sha256.md

@@ -0,0 +1,59 @@
+# SHA-256 compression precompile
+
+The VM implements the compression syscall specified in `spec/sha256.typ`:
+
+| Register | Meaning |
+|---|---|
+| a7 | -1 (`u64::MAX`) |
+| a0 | Pointer to 32 bytes of SHA-256 state, eight big-endian words |
+| a1 | Pointer to one 64-byte message block, sixteen big-endian words |
+
+The syscall reads both complete inputs before replacing the state with the
+compression result. Arbitrary byte alignment and overlapping operands are
+supported. Overflowing address ranges are rejected before writing. The syscall
+performs compression only; `lambda_vm_syscalls::sha256::sha256` supplies the
+standard IV, length encoding, padding and multiblock processing.
+
+## Proof integration
+
+Five fixed tables constrain the compression core, 64 rounds, 48 expanded
+schedule words, rotations/XORs, and verifier-committed round constants. They
+connect to the existing ECALL, memory and range-check arguments. State writes
+use the existing combined read/write memory convention. Continuation collection
+and disk-spill estimates account for the new tables and memory accesses.
+
+This implementation uses bit constraints for Ch/Maj and rotations rather than
+the BYTE_ALU/HWSL layout proposed in the spec. The rotation table accepts the
+four tuples needed by SHA-256. Constraint degree remains at most three. This
+is a new proof implementation requiring review, not an audited equivalence
+claim about the spec's table layout.
+
+The fixed-table count increases from 11 to 16. This changes the proof format;
+proofs from older versions are not compatible with this verifier.
+
+## Validation
+
+The dedicated guest checks 104 hashes against a Python hashlib oracle: thirteen
+lengths (0, 1, 31, 32, 55, 56, 63, 64, 65, 127, 128, 129, 1024), each at eight
+byte alignments. Executor tests exercise compression, overlapping operands,
+32-bit address-limb boundaries and rejected overflowing ranges. Prover tests
+cover complete proofs, continuation boundaries and rejection of corrupted
+outputs, pointers, round constants, schedule dependencies and rotation results.
+
+```sh
+make compile-programs-asm
+make executor/program_artifacts/rust/sha256.elf
+cargo test --release -p executor sha256
+cargo test --release -p lambda-vm-prover sha256 --lib
+```
+
+## Earlier application experiment
+
+An isolated Amsterdam ethrex guest at revision
+`89e160231d80b5d9bdfa8a7074e470298641d24d`, with its SHA provider routed through
+this wrapper, used 26,654,728 instructions versus 37,145,872 before acceleration
+(28.24% fewer) on a mainnet-derived local replay. The smaller fixtures saved
+31–35%. Both sides used the same executor with verified arithmetic hints.
+These are earlier integration measurements, not a benchmark of this PR branch,
+and the replay is not a canonical mainnet block. Guest wiring and other guest
+optimizations are outside this VM-only change.

executor/programs/asm/test_sha256.s

@@ -0,0 +1,21 @@
+.globl main
+main:
+ la a0, state
+ la a1, message
+ li a7, -1
+ ecall
+ li a0, 1
+ la a1, state
+ li a2, 32
+ li a7, 64
+ ecall
+ li a0, 0
+ li a7, 93
+ ecall
+.data
+.byte 0
+state:
+.byte 106,9,230,103,187,103,174,133,60,110,243,114,165,79,245,58,81,14,82,127,155,5,104,140,31,131,217,171,91,224,205,25
+.byte 0,0
+message:
+.byte 97,98,99,128,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,24

executor/programs/asm/test_sha256_overlap.s

@@ -0,0 +1,32 @@
+.globl main
+main:
+ la a0, state
+ la a1, message
+ li a7, -1
+ ecall
+ la a0, state
+ la a1, state
+ li a7, -1
+ ecall
+ la a0, state
+ la a1, state
+ addi a1, a1, 3
+ li a7, -1
+ ecall
+ li a0, 1
+ la a1, state
+ li a2, 32
+ li a7, 64
+ ecall
+ li a0, 0
+ li a7, 93
+ ecall
+.data
+.byte 0
+state:
+.byte 106,9,230,103,187,103,174,133,60,110,243,114,165,79,245,58,81,14,82,127,155,5,104,140,31,131,217,171,91,224,205,25
+.byte 0,0
+message:
+.byte 97,98,99,128,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,24
+
+.zero 64

executor/programs/rust/sha256/.cargo/config.toml

@@ -0,0 +1,5 @@
+[target.riscv64im-lambda-vm-elf]
+rustflags = [
+  "--cfg", "getrandom_backend=\"custom\"",
+  "-C", "passes=lower-atomic"
+]