feat: Add sha512 precompiles

core/src/air/mod.rs

@@ -6,6 +6,7 @@ mod polynomial;
 mod public_values;
 mod sub_builder;
 mod word;
+mod word_64;
 
 pub use builder::*;
 pub use extension::*;
@@ -15,3 +16,4 @@ pub use polynomial::*;
 pub use public_values::*;
 pub use sub_builder::*;
 pub use word::*;
+pub use word_64::*;

core/src/air/word_64.rs

@@ -0,0 +1,132 @@
+use core::fmt::Debug;
+use std::{
+    array::IntoIter,
+    ops::{Index, IndexMut},
+};
+
+use p3_field::{AbstractField, Field};
+use serde::{Deserialize, Serialize};
+use sphinx_derive::AlignedBorrow;
+
+use super::BaseAirBuilder;
+use crate::air::Word;
+
+/// The size of a word64 in bytes.
+pub const WORD64_SIZE: usize = 8;
+
+/// A double word is a 64-bit value represented in an AIR.
+#[derive(
+    AlignedBorrow, Clone, Copy, Debug, Default, PartialEq, Eq, Hash, Serialize, Deserialize,
+)]
+#[repr(C)]
+pub struct Word64<T>(pub [T; WORD64_SIZE]);
+
+impl<T> Word64<T> {
+    /// Applies `f` to each element of the word64.
+    pub fn map<F, S>(self, f: F) -> Word64<S>
+    where
+        F: FnMut(T) -> S,
+    {
+        Word64(self.0.map(f))
+    }
+
+    /// Extends a variable to a word64.
+    pub fn extend_var<AB: BaseAirBuilder<Var = T>>(var: T) -> Word64<AB::Expr> {
+        Word64([
+            AB::Expr::zero() + var,
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+        ])
+    }
+}
+
+impl<T: Clone> Word64<T> {
+    /// Splits into two words.
+    pub fn to_le_words(self) -> [Word<T>; 2] {
+        let limbs: Vec<T> = self.into_iter().collect();
+        [
+            limbs[..4].iter().cloned().collect(),
+            limbs[4..].iter().cloned().collect(),
+        ]
+    }
+}
+
+impl<T: AbstractField> Word64<T> {
+    /// Extends a variable to a word64.
+    pub fn extend_expr<AB: BaseAirBuilder<Expr = T>>(expr: T) -> Word64<AB::Expr> {
+        Word64([
+            AB::Expr::zero() + expr,
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+        ])
+    }
+
+    /// Returns a word64 with all zero expressions.
+    pub fn zero<AB: BaseAirBuilder<Expr = T>>() -> Word64<T> {
+        Word64([
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+            AB::Expr::zero(),
+        ])
+    }
+}
+
+impl<F: Field> Word64<F> {
+    /// Converts a word64 to a u64.
+    pub fn to_u64(&self) -> u64 {
+        // TODO: avoid string conversion
+        u64::from_le_bytes(self.0.map(|x| x.to_string().parse::<u8>().unwrap()))
+    }
+}
+
+impl<T> Index<usize> for Word64<T> {
+    type Output = T;
+
+    fn index(&self, index: usize) -> &Self::Output {
+        &self.0[index]
+    }
+}
+
+impl<T> IndexMut<usize> for Word64<T> {
+    fn index_mut(&mut self, index: usize) -> &mut Self::Output {
+        &mut self.0[index]
+    }
+}
+
+impl<F: AbstractField> From<u64> for Word64<F> {
+    fn from(value: u64) -> Self {
+        Word64(value.to_le_bytes().map(F::from_canonical_u8))
+    }
+}
+
+impl<T> IntoIterator for Word64<T> {
+    type Item = T;
+    type IntoIter = IntoIter<T, WORD64_SIZE>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.0.into_iter()
+    }
+}
+
+impl<T: Clone> FromIterator<T> for Word64<T> {
+    fn from_iter<I: IntoIterator<Item = T>>(iter: I) -> Self {
+        let mut iter = iter.into_iter();
+        let elements = std::array::from_fn(|_| iter.next().unwrap());
+        Word64(elements)
+    }
+}

core/src/lib.rs

@@ -30,4 +30,4 @@ use stark::StarkGenericConfig;
 /// This string should be updated whenever any step in verifying an SP1 proof changes, including
 /// core, recursion, and plonk-bn254. This string is used to download SP1 artifacts and the gnark
 /// docker image.
-pub const SPHINX_CIRCUIT_VERSION: &str = "v1.0.8.1-testnet";
+pub const SPHINX_CIRCUIT_VERSION: &str = "v1.0.8.2-testnet";

core/src/operations/add_64.rs

@@ -0,0 +1,129 @@
+use crate::air::{Word64, WordAirBuilder, WORD64_SIZE};
+use crate::bytes::event::ByteRecord;
+
+use p3_air::AirBuilder;
+use p3_field::{AbstractField, Field};
+use sphinx_derive::AlignedBorrow;
+
+/// A set of columns needed to compute the add of two double words.
+#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
+#[repr(C)]
+pub struct Add64Operation<T> {
+    /// The result of `a + b`.
+    pub value: Word64<T>,
+
+    /// Trace.
+    pub carry: [T; WORD64_SIZE - 1],
+}
+
+impl<F: Field> Add64Operation<F> {
+    pub fn populate(
+        &mut self,
+        record: &mut impl ByteRecord,
+        shard: u32,
+        channel: u32,
+        a_u64: u64,
+        b_u64: u64,
+    ) -> u64 {
+        let expected = a_u64.wrapping_add(b_u64);
+        self.value = Word64::from(expected);
+        let a = a_u64.to_le_bytes();
+        let b = b_u64.to_le_bytes();
+
+        let mut carry = [0u8; WORD64_SIZE - 1];
+        if u64::from(a[0]) + u64::from(b[0]) > 255 {
+            carry[0] = 1;
+            self.carry[0] = F::one();
+        }
+        for i in 1..WORD64_SIZE - 1 {
+            if u64::from(a[i]) + u64::from(b[i]) + u64::from(carry[i - 1]) > 255 {
+                carry[i] = 1;
+                self.carry[i] = F::one();
+            }
+        }
+
+        let base = 256u64;
+        let overflow = u64::from(
+            a[0].wrapping_add(b[0])
+                .wrapping_sub(expected.to_le_bytes()[0]),
+        );
+        debug_assert_eq!(overflow.wrapping_mul(overflow.wrapping_sub(base)), 0);
+
+        // Range check
+        {
+            record.add_u8_range_checks(shard, channel, &a);
+            record.add_u8_range_checks(shard, channel, &b);
+            record.add_u8_range_checks(shard, channel, &expected.to_le_bytes());
+        }
+        expected
+    }
+
+    pub fn eval<AB: WordAirBuilder<F = F>>(
+        builder: &mut AB,
+        a: Word64<AB::Var>,
+        b: Word64<AB::Var>,
+        cols: Add64Operation<AB::Var>,
+        shard: AB::Var,
+        channel: impl Into<AB::Expr> + Clone,
+        is_real: AB::Expr,
+    ) {
+        let one = AB::Expr::one();
+        let base = AB::F::from_canonical_u32(256);
+
+        let mut builder_is_real = builder.when(is_real.clone());
+
+        // For each limb, assert that difference between the carried result and the non-carried
+        // result is either zero or the base.
+        let overflow_0 = a[0] + b[0] - cols.value[0];
+        let overflow_1 = a[1] + b[1] - cols.value[1] + cols.carry[0];
+        let overflow_2 = a[2] + b[2] - cols.value[2] + cols.carry[1];
+        let overflow_3 = a[3] + b[3] - cols.value[3] + cols.carry[2];
+        let overflow_4 = a[4] + b[4] - cols.value[4] + cols.carry[3];
+        let overflow_5 = a[5] + b[5] - cols.value[5] + cols.carry[4];
+        let overflow_6 = a[6] + b[6] - cols.value[6] + cols.carry[5];
+        let overflow_7 = a[7] + b[7] - cols.value[7] + cols.carry[6];
+        builder_is_real.assert_zero(overflow_0.clone() * (overflow_0.clone() - base));
+        builder_is_real.assert_zero(overflow_1.clone() * (overflow_1.clone() - base));
+        builder_is_real.assert_zero(overflow_2.clone() * (overflow_2.clone() - base));
+        builder_is_real.assert_zero(overflow_3.clone() * (overflow_3.clone() - base));
+        builder_is_real.assert_zero(overflow_4.clone() * (overflow_4.clone() - base));
+        builder_is_real.assert_zero(overflow_5.clone() * (overflow_5.clone() - base));
+        builder_is_real.assert_zero(overflow_6.clone() * (overflow_6.clone() - base));
+        builder_is_real.assert_zero(overflow_7.clone() * (overflow_7.clone() - base));
+
+        // If the carry is one, then the overflow must be the base.
+        builder_is_real.assert_zero(cols.carry[0] * (overflow_0.clone() - base));
+        builder_is_real.assert_zero(cols.carry[1] * (overflow_1.clone() - base));
+        builder_is_real.assert_zero(cols.carry[2] * (overflow_2.clone() - base));
+        builder_is_real.assert_zero(cols.carry[3] * (overflow_3.clone() - base));
+        builder_is_real.assert_zero(cols.carry[4] * (overflow_4.clone() - base));
+        builder_is_real.assert_zero(cols.carry[5] * (overflow_5.clone() - base));
+        builder_is_real.assert_zero(cols.carry[6] * (overflow_6.clone() - base));
+
+        // If the carry is not one, then the overflow must be zero.
+        builder_is_real.assert_zero((cols.carry[0] - one.clone()) * overflow_0.clone());
+        builder_is_real.assert_zero((cols.carry[1] - one.clone()) * overflow_1.clone());
+        builder_is_real.assert_zero((cols.carry[2] - one.clone()) * overflow_2.clone());
+        builder_is_real.assert_zero((cols.carry[3] - one.clone()) * overflow_3.clone());
+        builder_is_real.assert_zero((cols.carry[4] - one.clone()) * overflow_4.clone());
+        builder_is_real.assert_zero((cols.carry[5] - one.clone()) * overflow_5.clone());
+        builder_is_real.assert_zero((cols.carry[6] - one.clone()) * overflow_6.clone());
+
+        // Assert that the carry is either zero or one.
+        builder_is_real.assert_bool(cols.carry[0]);
+        builder_is_real.assert_bool(cols.carry[1]);
+        builder_is_real.assert_bool(cols.carry[2]);
+        builder_is_real.assert_bool(cols.carry[3]);
+        builder_is_real.assert_bool(cols.carry[4]);
+        builder_is_real.assert_bool(cols.carry[5]);
+        builder_is_real.assert_bool(cols.carry[6]);
+        builder_is_real.assert_bool(is_real.clone());
+
+        // Range check each byte.
+        {
+            builder.slice_range_check_u8(&a.0, shard, channel.clone(), is_real.clone());
+            builder.slice_range_check_u8(&b.0, shard, channel.clone(), is_real.clone());
+            builder.slice_range_check_u8(&cols.value.0, shard, channel, is_real);
+        }
+    }
+}

core/src/operations/and.rs

@@ -3,6 +3,8 @@ use sphinx_derive::AlignedBorrow;
 
 use crate::air::ByteAirBuilder;
 use crate::air::Word;
+use crate::air::Word64;
+use crate::air::WORD64_SIZE;
 use crate::bytes::event::ByteRecord;
 use crate::bytes::ByteLookupEvent;
 use crate::bytes::ByteOpcode;
@@ -69,3 +71,64 @@ impl<F: Field> AndOperation<F> {
         }
     }
 }
+
+/// A set of columns needed to compute the and of two word64s.
+#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
+#[repr(C)]
+pub struct And64Operation<T> {
+    /// The result of `x & y`.
+    pub value: Word64<T>,
+}
+
+impl<F: Field> And64Operation<F> {
+    pub fn populate(
+        &mut self,
+        record: &mut ExecutionRecord,
+        shard: u32,
+        channel: u32,
+        x: u64,
+        y: u64,
+    ) -> u64 {
+        let expected = x & y;
+        let x_bytes = x.to_le_bytes();
+        let y_bytes = y.to_le_bytes();
+        for i in 0..WORD64_SIZE {
+            let and = x_bytes[i] & y_bytes[i];
+            self.value[i] = F::from_canonical_u8(and);
+
+            let byte_event = ByteLookupEvent {
+                shard,
+                channel,
+                opcode: ByteOpcode::AND,
+                a1: u32::from(and),
+                a2: 0,
+                b: u32::from(x_bytes[i]),
+                c: u32::from(y_bytes[i]),
+            };
+            record.add_byte_lookup_event(byte_event);
+        }
+        expected
+    }
+
+    pub fn eval<AB: ByteAirBuilder<F = F>>(
+        builder: &mut AB,
+        a: Word64<AB::Var>,
+        b: Word64<AB::Var>,
+        cols: And64Operation<AB::Var>,
+        shard: AB::Var,
+        channel: impl Into<AB::Expr> + Copy,
+        is_real: AB::Var,
+    ) {
+        for i in 0..WORD64_SIZE {
+            builder.send_byte(
+                AB::F::from_canonical_u32(ByteOpcode::AND as u32),
+                cols.value[i],
+                a[i],
+                b[i],
+                shard,
+                channel,
+                is_real,
+            );
+        }
+    }
+}