Kyber spec.

.github/workflows/rust.yml

@@ -2,13 +2,17 @@ name: Build & Test
 
 on:
   push:
-    branches: [ "main" ]
+    branches: [ "main", "dev" ]
   pull_request:
-    branches: [ "main" ]
+    branches: [ "main", "dev" ]
 
 env:
   CARGO_TERM_COLOR: always
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   build:
     strategy:

.github/workflows/specs.yml

@@ -0,0 +1,50 @@
+name: Specs
+
+on:
+  push:
+    branches: [ "main", "dev" ]
+  pull_request:
+    branches: [ "main", "dev" ]
+
+env:
+  CARGO_TERM_COLOR: always
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    strategy:
+      fail-fast: false
+      matrix:
+        os:
+          - macos-latest
+          - ubuntu-latest
+          - windows-latest
+
+    runs-on: ${{ matrix.os }}
+
+    steps:
+
+    - name: Setup Ubuntu
+      if: matrix.os == 'ubuntu-latest'
+      run: sudo apt-get install ninja-build
+    - name: Setup MacOS
+      if: matrix.os == 'macos-latest'
+      run: brew install ninja
+    - name: Setup Windows
+      if: matrix.os == 'windows-latest'
+      run: |
+        echo "VCPKG_ROOT=$env:VCPKG_INSTALLATION_ROOT" | Out-File -FilePath $env:GITHUB_ENV -Append
+        vcpkg install openssl:x64-windows-static-md
+
+    - uses: actions/checkout@v3
+
+    - name: Build
+      working-directory: specs
+      run: cargo build --verbose
+
+    - name: Run tests
+      working-directory: specs
+      run: cargo test --verbose

Cargo.toml

@@ -8,7 +8,7 @@ documentation = "https://docs.rs/libcrux/"
 description = "Formally Verified Cryptography"
 readme = "Readme.md"
 repository = "https://github.com/cryspen/libcrux"
-exclude = ["/tests"]
+exclude = ["/tests", "/specs"]
 
 [lib]
 crate-type = ["staticlib", "cdylib", "lib"]

specs/.gitignore

@@ -0,0 +1,2 @@
+Cargo.lock
+target/

specs/Cargo.toml

@@ -0,0 +1,2 @@
+[workspace]
+members = ["hacspec-lib", "kyber"]

specs/hacspec-lib/.gitignore

@@ -0,0 +1,2 @@
+Cargo.lock
+/target

specs/hacspec-lib/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "hacspec-lib"
+version = "0.0.1"
+edition = "2021"
+
+[dependencies]

specs/hacspec-lib/src/bit_vector.rs

@@ -0,0 +1,139 @@
+pub struct BitVector {
+    bits: Vec<u8>,
+}
+
+pub struct BitVectorChunks<'a> {
+    chunk_iterator: std::slice::Chunks<'a, u8>,
+}
+
+impl BitVectorChunks<'_> {
+    pub fn next(&mut self) -> Option<BitVector> {
+        self.chunk_iterator.next().map(|bits| BitVector {
+            bits: bits.to_vec(),
+        })
+    }
+}
+
+impl IntoIterator for BitVector {
+    type Item = u8;
+    type IntoIter = <Vec<u8> as IntoIterator>::IntoIter;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.bits.into_iter()
+    }
+}
+
+impl From<&[u8]> for BitVector {
+    fn from(bytes: &[u8]) -> Self {
+        let mut out = Vec::with_capacity(bytes.len() * 8);
+
+        for byte in bytes {
+            for j in 0..u8::BITS {
+                out.push((byte >> j) & 1);
+            }
+        }
+
+        Self { bits: out }
+    }
+}
+
+impl BitVector {
+    pub fn new(bits: Vec<u8>) -> Self {
+        for bit in &bits {
+            assert!(*bit == 0 || *bit == 1);
+        }
+
+        Self { bits }
+    }
+    pub fn chunks(&self, chunk_size: usize) -> BitVectorChunks {
+        BitVectorChunks {
+            chunk_iterator: self.bits.chunks(chunk_size),
+        }
+    }
+}
+
+pub trait Bits {
+    fn bit(&self, bit: usize) -> u8;
+    fn iter(&self) -> BitsIter<'_>;
+}
+
+pub struct BitsIter<'a> {
+    bytes: &'a [u8],
+    bit: usize,
+}
+
+impl Iterator for BitsIter<'_> {
+    type Item = u8;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        let byte_index = self.bit / 8;
+        if byte_index >= self.bytes.len() {
+            return None;
+        }
+
+        let out = self.bytes.bit(self.bit);
+        self.bit += 1;
+
+        Some(out)
+    }
+}
+
+impl Bits for &[u8] {
+    fn bit(&self, bit: usize) -> u8 {
+        let byte = bit / 8;
+        let byte_bit = 7 - bit % 8;
+        (self[byte] >> byte_bit) & 1
+    }
+
+    fn iter(&self) -> BitsIter<'_> {
+        BitsIter {
+            bytes: self,
+            bit: 0,
+        }
+    }
+}
+
+impl Bits for Vec<u8> {
+    fn bit(&self, bit: usize) -> u8 {
+        self.as_slice().bit(bit)
+    }
+
+    fn iter(&self) -> BitsIter<'_> {
+        BitsIter {
+            bytes: self,
+            bit: 0,
+        }
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bit_vector::Bits;
+
+    #[test]
+    fn bits() {
+        // 00000001 00000010 00000011 00000100 00000101 00000110 ...
+        //        1        2        3        4        5        6
+        let v = vec![1u8, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16];
+
+        let mut bit = 0;
+        for i in bit..7 {
+            assert_eq!(v.bit(i), 0);
+        }
+        bit += 7;
+        assert_eq!(v.bit(bit), 1);
+        bit = 8;
+        for i in bit..14 {
+            assert_eq!(v.bit(i), 0);
+        }
+        bit = 14;
+        assert_eq!(v.bit(bit), 1);
+        bit += 1;
+        assert_eq!(v.bit(bit), 0);
+
+        for bit in v.iter() {
+            eprint!("{bit}");
+        }
+        eprintln!();
+    }
+}

specs/hacspec-lib/src/field.rs

@@ -0,0 +1,95 @@
+use std::ops;
+
+pub trait FieldElement:
+    Copy
+    + Clone
+    + PartialEq
+    + From<u8>
+    + From<u16>
+    + From<u32>
+    + Into<u16>
+    + ops::Add<Output = Self>
+    + ops::Sub<Output = Self>
+    + ops::Mul<Output = Self>
+{
+    const ZERO: Self;
+
+    fn new(number: u16) -> Self;
+    fn bit(&self, bit: usize) -> u8;
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub struct PrimeFieldElement<const MODULUS: u16> {
+    pub value: u16,
+}
+
+impl<const MODULUS: u16> FieldElement for PrimeFieldElement<MODULUS> {
+    const ZERO: Self = Self { value: 0 };
+
+    fn new(number: u16) -> Self {
+        Self {
+            value: number % MODULUS,
+        }
+    }
+
+    fn bit(&self, bit: usize) -> u8 {
+        ((self.value >> bit) & 1) as u8
+    }
+}
+
+impl<const MODULUS: u16> PrimeFieldElement<MODULUS> {
+    pub const MODULUS: u16 = MODULUS;
+}
+
+impl<const MODULUS: u16> From<u8> for PrimeFieldElement<MODULUS> {
+    fn from(number: u8) -> Self {
+        Self::new(u16::from(number))
+    }
+}
+impl<const MODULUS: u16> From<u16> for PrimeFieldElement<MODULUS> {
+    fn from(number: u16) -> Self {
+        Self::new(number)
+    }
+}
+impl<const MODULUS: u16> From<PrimeFieldElement<MODULUS>> for u16 {
+    fn from(value: PrimeFieldElement<MODULUS>) -> Self {
+        value.value
+    }
+}
+impl<const MODULUS: u16> From<u32> for PrimeFieldElement<MODULUS> {
+    fn from(number: u32) -> Self {
+        let remainder_as_u32 = number % u32::from(MODULUS);
+
+        Self::new(remainder_as_u32.try_into().unwrap())
+    }
+}
+
+impl<const MODULUS: u16> ops::Add for PrimeFieldElement<MODULUS> {
+    type Output = Self;
+
+    fn add(self, other: Self) -> Self {
+        let sum: u32 = u32::from(self.value) + u32::from(other.value);
+
+        sum.into()
+    }
+}
+impl<const MODULUS: u16> ops::Sub for PrimeFieldElement<MODULUS> {
+    type Output = Self;
+
+    fn sub(self, other: Self) -> Self {
+        let difference: i32 =
+            i32::try_from(self.value).unwrap() - i32::try_from(other.value).unwrap();
+        let representative = difference.rem_euclid(MODULUS.into());
+
+        u16::try_from(representative).unwrap().into()
+    }
+}
+impl<const MODULUS: u16> ops::Mul for PrimeFieldElement<MODULUS> {
+    type Output = Self;
+
+    fn mul(self, other: Self) -> Self {
+        let product: u32 = u32::from(self.value) * u32::from(other.value);
+
+        product.into()
+    }
+}