From d15afa5cfc602f134879fe142ddc943a977f1b10 Mon Sep 17 00:00:00 2001 From: Winston Zhang Date: Mon, 20 Jan 2025 00:07:44 -0800 Subject: [PATCH 1/7] chore: Add sorry'ed definitions for rotate_{left/right} --- backends/lean/Aeneas/Std/Scalar.lean | 80 ++++++++++++++++++++++++++++ tests/lean/Scalars.lean | 20 +++++++ tests/src/scalars.rs | 16 ++++++ 3 files changed, 116 insertions(+) diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean index 5d3ee206..6fdceb6a 100644 --- a/backends/lean/Aeneas/Std/Scalar.lean +++ b/backends/lean/Aeneas/Std/Scalar.lean @@ -1437,6 +1437,86 @@ def core.num.Isize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Isize -- TODO: reasoning lemmas for wrapping sub +-- Rotate left +def Scalar.rotate_left {ty} (x y : Scalar ty) : Scalar ty := sorry +/- [core::num::{u8}::wrapping_sub] -/ +def core.num.U8.rotate_left := @Scalar.rotate_left ScalarTy.U8 + +/- [core::num::{u16}::rotate_left] -/ +def core.num.U16.rotate_left := @Scalar.rotate_left ScalarTy.U16 + +/- [core::num::{u32}::rotate_left] -/ +def core.num.U32.rotate_left := @Scalar.rotate_left ScalarTy.U32 + +/- [core::num::{u64}::rotate_left] -/ +def core.num.U64.rotate_left := @Scalar.rotate_left ScalarTy.U64 + +/- [core::num::{u128}::rotate_left] -/ +def core.num.U128.rotate_left := @Scalar.rotate_left ScalarTy.U128 + +/- [core::num::{usize}::rotate_left] -/ +def core.num.Usize.rotate_left := @Scalar.rotate_left ScalarTy.Usize + +/- [core::num::{i8}::rotate_left] -/ +def core.num.I8.rotate_left := @Scalar.rotate_left ScalarTy.I8 + +/- [core::num::{i16}::rotate_left] -/ +def core.num.I16.rotate_left := @Scalar.rotate_left ScalarTy.I16 + +/- [core::num::{i32}::rotate_left] -/ +def core.num.I32.rotate_left := @Scalar.rotate_left ScalarTy.I32 + +/- [core::num::{i64}::rotate_left] -/ +def core.num.I64.rotate_left := @Scalar.rotate_left ScalarTy.I64 + +/- [core::num::{i128}::rotate_left] -/ +def core.num.I128.rotate_left := @Scalar.rotate_left ScalarTy.I128 + +/- [core::num::{isize}::rotate_left] -/ +def core.num.Isize.rotate_left := @Scalar.rotate_left ScalarTy.Isize + +-- TODO: reasoning lemmas for rotate left + +-- Rotate right +def Scalar.rotate_right {ty} (x y : Scalar ty) : Scalar ty := sorry +/- [core::num::{u8}::wrapping_sub] -/ +def core.num.U8.rotate_right := @Scalar.rotate_right ScalarTy.U8 + +/- [core::num::{u16}::rotate_right] -/ +def core.num.U16.rotate_right := @Scalar.rotate_right ScalarTy.U16 + +/- [core::num::{u32}::rotate_right] -/ +def core.num.U32.rotate_right := @Scalar.rotate_right ScalarTy.U32 + +/- [core::num::{u64}::rotate_right] -/ +def core.num.U64.rotate_right := @Scalar.rotate_right ScalarTy.U64 + +/- [core::num::{u128}::rotate_right] -/ +def core.num.U128.rotate_right := @Scalar.rotate_right ScalarTy.U128 + +/- [core::num::{usize}::rotate_right] -/ +def core.num.Usize.rotate_right := @Scalar.rotate_right ScalarTy.Usize + +/- [core::num::{i8}::rotate_right] -/ +def core.num.I8.rotate_right := @Scalar.rotate_right ScalarTy.I8 + +/- [core::num::{i16}::rotate_right] -/ +def core.num.I16.rotate_right := @Scalar.rotate_right ScalarTy.I16 + +/- [core::num::{i32}::rotate_right] -/ +def core.num.I32.rotate_right := @Scalar.rotate_right ScalarTy.I32 + +/- [core::num::{i64}::rotate_right] -/ +def core.num.I64.rotate_right := @Scalar.rotate_right ScalarTy.I64 + +/- [core::num::{i128}::rotate_right] -/ +def core.num.I128.rotate_right := @Scalar.rotate_right ScalarTy.I128 + +/- [core::num::{isize}::rotate_right] -/ +def core.num.Isize.rotate_right := @Scalar.rotate_right ScalarTy.Isize + +-- TODO: reasoning lemmas for rotate right + end Std end Aeneas diff --git a/tests/lean/Scalars.lean b/tests/lean/Scalars.lean index 555f2c0d..03601f9c 100644 --- a/tests/lean/Scalars.lean +++ b/tests/lean/Scalars.lean @@ -48,4 +48,24 @@ def u32_use_shift_left (x : U32) : Result U32 := def i32_use_shift_left (x : I32) : Result I32 := x <<< 2#i32 +/- [scalars::u32_use_rotate_right]: + Source: 'tests/src/scalars.rs', lines 35:0-37:1 -/ +def u32_use_rotate_right (x : U32) : Result U32 := + Result.ok (core.num.U32.rotate_right x 2#u32) + +/- [scalars::i32_use_rotate_right]: + Source: 'tests/src/scalars.rs', lines 39:0-41:1 -/ +def i32_use_rotate_right (x : I32) : Result I32 := + Result.ok (core.num.I32.rotate_right x 2#u32) + +/- [scalars::u32_use_rotate_left]: + Source: 'tests/src/scalars.rs', lines 43:0-45:1 -/ +def u32_use_rotate_left (x : U32) : Result U32 := + Result.ok (core.num.U32.rotate_left x 2#u32) + +/- [scalars::i32_use_rotate_left]: + Source: 'tests/src/scalars.rs', lines 47:0-49:1 -/ +def i32_use_rotate_left (x : I32) : Result I32 := + Result.ok (core.num.I32.rotate_left x 2#u32) + end scalars diff --git a/tests/src/scalars.rs b/tests/src/scalars.rs index 80d264c3..892994f5 100644 --- a/tests/src/scalars.rs +++ b/tests/src/scalars.rs @@ -31,3 +31,19 @@ fn u32_use_shift_left(x: u32) -> u32 { fn i32_use_shift_left(x: i32) -> i32 { x << 2 } + +fn u32_use_rotate_right(x: u32) -> u32 { + x.rotate_right(2) +} + +fn i32_use_rotate_right(x: i32) -> i32 { + x.rotate_right(2) +} + +fn u32_use_rotate_left(x: u32) -> u32 { + x.rotate_left(2) +} + +fn i32_use_rotate_left(x: i32) -> i32 { + x.rotate_left(2) +} From 91df1765f6cc60f36b7dec4c24a2aa1d5938a3dc Mon Sep 17 00:00:00 2001 From: Son HO Date: Mon, 20 Jan 2025 10:29:50 +0000 Subject: [PATCH 2/7] Update backends/lean/Aeneas/Std/Scalar.lean --- backends/lean/Aeneas/Std/Scalar.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean index 6fdceb6a..af8f39f7 100644 --- a/backends/lean/Aeneas/Std/Scalar.lean +++ b/backends/lean/Aeneas/Std/Scalar.lean @@ -1479,7 +1479,7 @@ def core.num.Isize.rotate_left := @Scalar.rotate_left ScalarTy.Isize -- Rotate right def Scalar.rotate_right {ty} (x y : Scalar ty) : Scalar ty := sorry -/- [core::num::{u8}::wrapping_sub] -/ +/- [core::num::{u8}::rotate_right] -/ def core.num.U8.rotate_right := @Scalar.rotate_right ScalarTy.U8 /- [core::num::{u16}::rotate_right] -/ From 83d707c5b1a68d33d66c310249eddc582fba7749 Mon Sep 17 00:00:00 2001 From: Son HO Date: Mon, 20 Jan 2025 10:30:10 +0000 Subject: [PATCH 3/7] Update backends/lean/Aeneas/Std/Scalar.lean --- backends/lean/Aeneas/Std/Scalar.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean index af8f39f7..1a020b9c 100644 --- a/backends/lean/Aeneas/Std/Scalar.lean +++ b/backends/lean/Aeneas/Std/Scalar.lean @@ -1439,7 +1439,7 @@ def core.num.Isize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Isize -- Rotate left def Scalar.rotate_left {ty} (x y : Scalar ty) : Scalar ty := sorry -/- [core::num::{u8}::wrapping_sub] -/ +/- [core::num::{u8}::rotate_left] -/ def core.num.U8.rotate_left := @Scalar.rotate_left ScalarTy.U8 /- [core::num::{u16}::rotate_left] -/ From b3af5ccdd888f38ff511d766eca022bf74061f1a Mon Sep 17 00:00:00 2001 From: Son HO Date: Mon, 20 Jan 2025 10:31:48 +0000 Subject: [PATCH 4/7] Update backends/lean/Aeneas/Std/Scalar.lean --- backends/lean/Aeneas/Std/Scalar.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean index 1a020b9c..10034bf0 100644 --- a/backends/lean/Aeneas/Std/Scalar.lean +++ b/backends/lean/Aeneas/Std/Scalar.lean @@ -1439,6 +1439,7 @@ def core.num.Isize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Isize -- Rotate left def Scalar.rotate_left {ty} (x y : Scalar ty) : Scalar ty := sorry + /- [core::num::{u8}::rotate_left] -/ def core.num.U8.rotate_left := @Scalar.rotate_left ScalarTy.U8 From 6200ef7654de38230858528543dbd35edf58ff4f Mon Sep 17 00:00:00 2001 From: Son HO Date: Mon, 20 Jan 2025 10:32:09 +0000 Subject: [PATCH 5/7] Update backends/lean/Aeneas/Std/Scalar.lean --- backends/lean/Aeneas/Std/Scalar.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean index 10034bf0..3eeab0b5 100644 --- a/backends/lean/Aeneas/Std/Scalar.lean +++ b/backends/lean/Aeneas/Std/Scalar.lean @@ -1480,6 +1480,7 @@ def core.num.Isize.rotate_left := @Scalar.rotate_left ScalarTy.Isize -- Rotate right def Scalar.rotate_right {ty} (x y : Scalar ty) : Scalar ty := sorry + /- [core::num::{u8}::rotate_right] -/ def core.num.U8.rotate_right := @Scalar.rotate_right ScalarTy.U8 From 12e867a1f4fcf0f8c8359c733bfaaee5f08a654d Mon Sep 17 00:00:00 2001 From: Son HO Date: Mon, 20 Jan 2025 10:33:51 +0000 Subject: [PATCH 6/7] Update backends/lean/Aeneas/Std/Scalar.lean --- backends/lean/Aeneas/Std/Scalar.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean index 3eeab0b5..602e19b8 100644 --- a/backends/lean/Aeneas/Std/Scalar.lean +++ b/backends/lean/Aeneas/Std/Scalar.lean @@ -1438,7 +1438,7 @@ def core.num.Isize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Isize -- TODO: reasoning lemmas for wrapping sub -- Rotate left -def Scalar.rotate_left {ty} (x y : Scalar ty) : Scalar ty := sorry +def Scalar.rotate_left {ty} (x : Scalar ty) (shift : U32) : Scalar ty := sorry /- [core::num::{u8}::rotate_left] -/ def core.num.U8.rotate_left := @Scalar.rotate_left ScalarTy.U8 From c15943d27999de1e3ee677fb165fc38c0352e8f7 Mon Sep 17 00:00:00 2001 From: Son HO Date: Mon, 20 Jan 2025 10:34:36 +0000 Subject: [PATCH 7/7] Update backends/lean/Aeneas/Std/Scalar.lean --- backends/lean/Aeneas/Std/Scalar.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean index 602e19b8..7bbb584a 100644 --- a/backends/lean/Aeneas/Std/Scalar.lean +++ b/backends/lean/Aeneas/Std/Scalar.lean @@ -1479,7 +1479,7 @@ def core.num.Isize.rotate_left := @Scalar.rotate_left ScalarTy.Isize -- TODO: reasoning lemmas for rotate left -- Rotate right -def Scalar.rotate_right {ty} (x y : Scalar ty) : Scalar ty := sorry +def Scalar.rotate_right {ty} (x : Scalar ty) (shift : U32) : Scalar ty := sorry /- [core::num::{u8}::rotate_right] -/ def core.num.U8.rotate_right := @Scalar.rotate_right ScalarTy.U8