From ecc8a86d8af55f13099efc5f2834dc9214ca0135 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Fri, 30 Aug 2024 07:57:06 -0700 Subject: [PATCH] More tests to be fixed --- Makefile | 2 +- test/issue_49/Cargo.lock | 7 ++++ test/issue_49/Cargo.toml | 8 +++++ test/issue_49/src/main.rs | 9 +++++ test/symcrust/Cargo.lock | 7 ++++ test/symcrust/Cargo.toml | 8 +++++ test/symcrust/c.yaml | 6 ++++ test/symcrust/src/main.rs | 71 +++++++++++++++++++++++++++++++++++++++ 8 files changed, 117 insertions(+), 1 deletion(-) create mode 100644 test/issue_49/Cargo.lock create mode 100644 test/issue_49/Cargo.toml create mode 100644 test/issue_49/src/main.rs create mode 100644 test/symcrust/Cargo.lock create mode 100644 test/symcrust/Cargo.toml create mode 100644 test/symcrust/c.yaml create mode 100644 test/symcrust/src/main.rs diff --git a/Makefile b/Makefile index e68bf86..6c67e84 100644 --- a/Makefile +++ b/Makefile @@ -3,7 +3,7 @@ KRML_HOME ?= $(dir $(abspath $(lastword $(MAKEFILE_LIST))))/../karamel EURYDICE ?= ./eurydice $(EURYDICE_FLAGS) CHARON ?= $(CHARON_HOME)/bin/charon -BROKEN_TESTS = step_by where_clauses chunks mutable_slice_range closure +BROKEN_TESTS = step_by where_clauses chunks mutable_slice_range closure issue_49 symcrust TEST_DIRS = $(filter-out $(BROKEN_TESTS),$(subst test/,,$(shell find test -maxdepth 1 -mindepth 1 -type d))) .PHONY: all diff --git a/test/issue_49/Cargo.lock b/test/issue_49/Cargo.lock new file mode 100644 index 0000000..70c7650 --- /dev/null +++ b/test/issue_49/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "issue_49" +version = "0.1.0" diff --git a/test/issue_49/Cargo.toml b/test/issue_49/Cargo.toml new file mode 100644 index 0000000..f84f2f1 --- /dev/null +++ b/test/issue_49/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "issue_49" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/issue_49/src/main.rs b/test/issue_49/src/main.rs new file mode 100644 index 0000000..f460c04 --- /dev/null +++ b/test/issue_49/src/main.rs @@ -0,0 +1,9 @@ +pub fn f(a: usize, b: usize) -> usize { + a.min(b) +} + +fn main() { + let expected = 0; + let actual = f(0, 0); + assert_eq!(expected, actual); +} diff --git a/test/symcrust/Cargo.lock b/test/symcrust/Cargo.lock new file mode 100644 index 0000000..74fd6e7 --- /dev/null +++ b/test/symcrust/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "symcrust" +version = "0.1.0" diff --git a/test/symcrust/Cargo.toml b/test/symcrust/Cargo.toml new file mode 100644 index 0000000..9250c33 --- /dev/null +++ b/test/symcrust/Cargo.toml @@ -0,0 +1,8 @@ +[package] +name = "symcrust" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/test/symcrust/c.yaml b/test/symcrust/c.yaml new file mode 100644 index 0000000..48a0a35 --- /dev/null +++ b/test/symcrust/c.yaml @@ -0,0 +1,6 @@ +files: + - name: symcrust + api: + - [ symcrust, "*" ] + private: + - [ "*" ] diff --git a/test/symcrust/src/main.rs b/test/symcrust/src/main.rs new file mode 100644 index 0000000..23e5dcf --- /dev/null +++ b/test/symcrust/src/main.rs @@ -0,0 +1,71 @@ +#[allow(non_snake_case)] +#[no_mangle] +pub fn SymCrustMlKemPolyElementCompressAndEncode( + coeffs: &[u16; 256], + nBitsPerCoefficient: u32, + dst: &mut [u8] ) +{ + let SYMCRYPT_MLKEM_COMPRESS_MULCONSTANT : u64 = 0x9d7dbb; + let SYMCRYPT_MLKEM_COMPRESS_SHIFTCONSTANT : u32 = 35; + let mut multiplication: u64; + let mut coefficient: u32; + let mut nBitsInCoefficient: u32; + let mut bitsToEncode: u32; + let mut nBitsToEncode: u32; + let mut cbDstWritten: usize = 0; + let mut accumulator: u32 = 0; + let mut nBitsInAccumulator: u32 = 0; + + assert!(nBitsPerCoefficient > 0); + assert!(nBitsPerCoefficient <= 12); + assert!( dst.len() as u64 == (256*u64::from(nBitsPerCoefficient) / 8) ); + + for i in 0..256 + { + nBitsInCoefficient = nBitsPerCoefficient; + coefficient = u32::from(coeffs[i]); // in range [0, Q-1] + + // first compress the coefficient + // when nBitsPerCoefficient < 12 we compress per Compress_d in draft FIPS 203; + if nBitsPerCoefficient < 12 + { + // Multiply by 2^(nBitsPerCoefficient+1) / Q by multiplying by constant and shifting right + multiplication = u64::from(coefficient) * SYMCRYPT_MLKEM_COMPRESS_MULCONSTANT; + coefficient = (multiplication >> (SYMCRYPT_MLKEM_COMPRESS_SHIFTCONSTANT-(nBitsPerCoefficient+1))) as u32; + + // add "half" to round to nearest integer + coefficient += 1; + + // final divide by two to get multiplication by 2^nBitsPerCoefficient / Q + coefficient >>= 1; // in range [0, 2^nBitsPerCoefficient] + + // modular reduction by masking + coefficient &= (1u32< 0 + { + nBitsToEncode = nBitsInCoefficient.min(32-nBitsInAccumulator); + + bitsToEncode = coefficient & ((1u32<>= nBitsToEncode; + nBitsInCoefficient -= nBitsToEncode; + + accumulator |= bitsToEncode << nBitsInAccumulator; + nBitsInAccumulator += nBitsToEncode; + if nBitsInAccumulator == 32 + { + dst[cbDstWritten..cbDstWritten+4].copy_from_slice( &accumulator.to_le_bytes() ); + cbDstWritten += 4; + accumulator = 0; + nBitsInAccumulator = 0; + } + } + } +} + +fn main() { + println!("Hello, world!"); +}