Link file for air

CoqOfRust/blacklist.txt

@@ -22,4 +22,10 @@ move_sui/links/
 move_sui/simulations/move_bytecode_verifier_meter/lib.v
 # Because it does not change much right now and takes a long time to compile
 move_sui/proofs
-move_sui/simulations
+move_sui/simulations
+# Plonky3 related files that does not pass
+plonky3/commit/src/adapters/extension_mmcs.v
+plonky3/merkle-tree/src/hiding_mmcs.v
+plonky3/merkle-tree/src/mmcs.v
+plonky3/monty-31/src/monty_31.v
+plonky3/poseidon2/src/external.v

CoqOfRust/plonky3/air/links/air.v

@@ -0,0 +1,95 @@
+Require Import CoqOfRust.CoqOfRust.
+Require Import CoqOfRust.links.M.
+Require Import plonky3.air.air.
+
+(* pub trait AirBuilder: Sized { *)
+Module AirBuilder.
+(* 
+    type F: Field;
+
+    type Expr: Algebra<Self::F> + Algebra<Self::Var>;
+
+    type Var: Into<Self::Expr>
+        + Copy
+        + Send
+        + Sync
+        + Add<Self::F, Output = Self::Expr>
+        + Add<Self::Var, Output = Self::Expr>
+        + Add<Self::Expr, Output = Self::Expr>
+        + Sub<Self::F, Output = Self::Expr>
+        + Sub<Self::Var, Output = Self::Expr>
+        + Sub<Self::Expr, Output = Self::Expr>
+        + Mul<Self::F, Output = Self::Expr>
+        + Mul<Self::Var, Output = Self::Expr>
+        + Mul<Self::Expr, Output = Self::Expr>;
+
+    type M: Matrix<Self::Var>;
+
+    fn main(&self) -> Self::M;
+
+    fn is_first_row(&self) -> Self::Expr;
+    fn is_last_row(&self) -> Self::Expr;
+    fn is_transition(&self) -> Self::Expr {
+        self.is_transition_window(2)
+    }
+    fn is_transition_window(&self, size: usize) -> Self::Expr;
+
+    fn when<I: Into<Self::Expr>>(&mut self, condition: I) -> FilteredAirBuilder<'_, Self> {
+        FilteredAirBuilder {
+            inner: self,
+            condition: condition.into(),
+        }
+    }
+
+    fn when_ne<I1: Into<Self::Expr>, I2: Into<Self::Expr>>(
+        &mut self,
+        x: I1,
+        y: I2,
+    ) -> FilteredAirBuilder<'_, Self> {
+        self.when(x.into() - y.into())
+    }
+
+    fn when_first_row(&mut self) -> FilteredAirBuilder<'_, Self> {
+        self.when(self.is_first_row())
+    }
+
+    fn when_last_row(&mut self) -> FilteredAirBuilder<'_, Self> {
+        self.when(self.is_last_row())
+    }
+
+    fn when_transition(&mut self) -> FilteredAirBuilder<'_, Self> {
+        self.when(self.is_transition())
+    }
+
+    fn when_transition_window(&mut self, size: usize) -> FilteredAirBuilder<'_, Self> {
+        self.when(self.is_transition_window(size))
+    }
+
+    fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I);
+
+    fn assert_zeros<const N: usize, I: Into<Self::Expr>>(&mut self, array: [I; N]) {
+        for elem in array {
+            self.assert_zero(elem);
+        }
+    }
+
+    fn assert_bools<const N: usize, I: Into<Self::Expr>>(&mut self, array: [I; N]) {
+        let zero_array = array.map(|x| x.into().bool_check());
+        self.assert_zeros(zero_array);
+    }
+
+    fn assert_one<I: Into<Self::Expr>>(&mut self, x: I) {
+        self.assert_zero(x.into() - Self::Expr::ONE);
+    }
+
+    fn assert_eq<I1: Into<Self::Expr>, I2: Into<Self::Expr>>(&mut self, x: I1, y: I2) {
+        self.assert_zero(x.into() - y.into());
+    }
+
+    fn assert_bool<I: Into<Self::Expr>>(&mut self, x: I) {
+        self.assert_zero(x.into().bool_check());
+    }
+*)
+  Class Run (Self : Set) `{Link Self} : Set := {
+  }.
+End AirBuilder.

CoqOfRust/plonky3/baby-bear/src/aarch64_neon/mod.rs

@@ -0,0 +1,4 @@
+mod packing;
+mod poseidon2;
+
+pub use packing::*;

CoqOfRust/plonky3/baby-bear/src/aarch64_neon/packing.rs

@@ -0,0 +1,36 @@
+use core::arch::aarch64::{int32x4_t, uint32x4_t};
+use core::mem::transmute;
+
+use p3_monty_31::{MontyParametersNeon, PackedMontyField31Neon};
+
+use crate::BabyBearParameters;
+
+const WIDTH: usize = 4;
+
+impl MontyParametersNeon for BabyBearParameters {
+    // SAFETY: This is a valid packed representation of P.
+    const PACKED_P: uint32x4_t = unsafe { transmute::<[u32; WIDTH], _>([0x78000001; WIDTH]) };
+    // This MU is the same 0x88000001 as elsewhere, just interpreted as an `i32`.
+    // SAFETY: This is a valid packed representation of MU.
+    const PACKED_MU: int32x4_t = unsafe { transmute::<[i32; WIDTH], _>([-0x77ffffff; WIDTH]) };
+}
+
+pub type PackedBabyBearNeon = PackedMontyField31Neon<BabyBearParameters>;
+
+#[cfg(test)]
+mod tests {
+    use p3_field_testing::test_packed_field;
+
+    use super::WIDTH;
+    use crate::BabyBear;
+
+    const SPECIAL_VALS: [BabyBear; WIDTH] =
+        BabyBear::new_array([0x00000000, 0x00000001, 0x00000002, 0x78000000]);
+
+    test_packed_field!(
+        crate::PackedBabyBearNeon,
+        &[crate::PackedBabyBearNeon::ZERO],
+        &[crate::PackedBabyBearNeon::ONE],
+        p3_monty_31::PackedMontyField31Neon::<crate::BabyBearParameters>(super::SPECIAL_VALS)
+    );
+}

CoqOfRust/plonky3/baby-bear/src/aarch64_neon/poseidon2.rs

@@ -0,0 +1,59 @@
+//! Eventually this will hold a vectorized Neon implementation of Poseidon2 for PackedBabyBearNeon
+//! Currently this is essentially a placeholder to allow compilation and testing on Neon devices.
+//!
+//! Converting the AVX2/AVX512 code across to Neon is on the TODO list.
+
+#[cfg(test)]
+mod tests {
+    use p3_symmetric::Permutation;
+    use rand::rngs::SmallRng;
+    use rand::{Rng, SeedableRng};
+
+    use crate::{BabyBear, PackedBabyBearNeon, Poseidon2BabyBear};
+
+    type F = BabyBear;
+    type Perm16 = Poseidon2BabyBear<16>;
+    type Perm24 = Poseidon2BabyBear<24>;
+
+    /// Test that the output is the same as the scalar version on a random input.
+    #[test]
+    fn test_neon_poseidon2_width_16() {
+        let mut rng = SmallRng::seed_from_u64(1);
+
+        // Our Poseidon2 implementation.
+        let poseidon2 = Perm16::new_from_rng_128(&mut rng);
+
+        let input: [F; 16] = rng.random();
+
+        let mut expected = input;
+        poseidon2.permute_mut(&mut expected);
+
+        let mut neon_input = input.map(Into::<PackedBabyBearNeon>::into);
+        poseidon2.permute_mut(&mut neon_input);
+
+        let neon_output = neon_input.map(|x| x.0[0]);
+
+        assert_eq!(neon_output, expected);
+    }
+
+    /// Test that the output is the same as the scalar version on a random input.
+    #[test]
+    fn test_neon_poseidon2_width_24() {
+        let mut rng = SmallRng::seed_from_u64(1);
+
+        // Our Poseidon2 implementation.
+        let poseidon2 = Perm24::new_from_rng_128(&mut rng);
+
+        let input: [F; 24] = rng.random();
+
+        let mut expected = input;
+        poseidon2.permute_mut(&mut expected);
+
+        let mut neon_input = input.map(Into::<PackedBabyBearNeon>::into);
+        poseidon2.permute_mut(&mut neon_input);
+
+        let neon_output = neon_input.map(|x| x.0[0]);
+
+        assert_eq!(neon_output, expected);
+    }
+}