chore: Add sorry'ed definitions for rotate_{left/right} (#422)

* chore: Add sorry'ed definitions for rotate_{left/right} * Update backends/lean/Aeneas/Std/Scalar.lean * Update backends/lean/Aeneas/Std/Scalar.lean * Update backends/lean/Aeneas/Std/Scalar.lean * Update backends/lean/Aeneas/Std/Scalar.lean * Update backends/lean/Aeneas/Std/Scalar.lean * Update backends/lean/Aeneas/Std/Scalar.lean --------- Co-authored-by: Son HO <[email protected]>
AeneasVerif · Jan 20, 2025 · 4ba1278 · 4ba1278
1 parent 5e2dcdc
commit 4ba1278
Show file tree

Hide file tree

Showing 3 changed files with 118 additions and 0 deletions.
diff --git a/backends/lean/Aeneas/Std/Scalar.lean b/backends/lean/Aeneas/Std/Scalar.lean
@@ -1437,6 +1437,88 @@ 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  : Scalar ty) (shift : U32) : Scalar ty := sorry
+
+/- [core::num::{u8}::rotate_left] -/
+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 : Scalar ty) (shift : U32) : Scalar ty := sorry
+
+/- [core::num::{u8}::rotate_right] -/
+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
@@ -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
@@ -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)
+}