feat(lean): add support for shift-left

CHANGELOG.md

@@ -30,6 +30,7 @@ Changes to the Lean backend:
  - Use the explicit monadic phase to insert `pure` and `←` only on demand, and
    not introduce extra `do` block (#1746)
  - Rename `Result` monad to `RustM` to avoid confusion with Rust `Result` type (#1768)
+ - Add support for shift-left (#1785)
  - Add support for default methods of traits (#1777)
 
 Miscellaneous:

hax-lib/proof-libs/lean/Hax/Integers/Ops.lean

@@ -61,6 +61,14 @@ class HaxShiftRight α β where
   -/
   shiftRight : α → β → RustM α
 
+/--The notation typeclass for left shift that returns a RustM. It enables the
+ notation `a <<<? b : RustM α` where `a : α` and `b : β`. -/
+class HaxShiftLeft α β where
+  /-- `a <<<? b` computes the panicking left-shift of `a` by `b`.  The meaning
+  of this notation is type-dependent. It panics if `b` exceeds the size of `a`.
+  -/
+  shiftLeft : α → β → RustM α
+
 /-- The notation typeclass for remainder.  This enables the notation `a %? b :
 RustM α` where `a b : α`.  -/
 class HaxRem α where
@@ -72,6 +80,7 @@ class HaxRem α where
 @[inherit_doc] infixl:65 " -? "   => HaxSub.sub
 @[inherit_doc] infixl:70 " *? "   => HaxMul.mul
 @[inherit_doc] infixl:75 " >>>? " => HaxShiftRight.shiftRight
+@[inherit_doc] infixl:75 " <<<? " => HaxShiftLeft.shiftLeft
 @[inherit_doc] infixl:70 " %? "   => HaxRem.rem
 @[inherit_doc] infixl:70 " /? "   => HaxDiv.div
 
@@ -85,7 +94,8 @@ class UnSigned (α: Type)
           (Mul α),
           (Div α),
           (Mod α),
-          (ShiftRight α)
+          (ShiftRight α),
+          (ShiftLeft α)
   where
   [deq : DecidableEq α]
   width    : Nat
@@ -174,6 +184,12 @@ instance {α : Type} [UnSigned α]: HaxShiftRight α α where
     if (UnSigned.width α) ≤ (UnSigned.toNat y) then .fail .integerOverflow
     else pure (x >>> y)
 
+/- Left shift on unsigned rust integers. Panics when shifting by more than the size -/
+instance {α : Type} [UnSigned α]: HaxShiftLeft α α where
+  shiftLeft x y :=
+    if (UnSigned.width α) ≤ (UnSigned.toNat y) then .fail .integerOverflow
+    else pure (x <<< y)
+
 /- Signed operations -/
 class Signed (α: Type)
   extends (LE α),
@@ -183,7 +199,8 @@ class Signed (α: Type)
           (Mul α),
           (Div α),
           (Mod α),
-          (ShiftRight α) where
+          (ShiftRight α),
+          (ShiftLeft α) where
   [dec: DecidableEq α]
   width    : Nat
   toBitVec : α → BitVec width
@@ -274,6 +291,15 @@ instance {α : Type} [Signed α] : HaxShiftRight α α where
     else
       .fail .integerOverflow
 
+/- Left shifting on signed integers. Panics when shifting by a negative number,
+   or when shifting by more than the size. -/
+instance {α : Type} [Signed α] : HaxShiftLeft α α where
+  shiftLeft x y :=
+    if 0 ≤ (Signed.toInt y) && (Signed.toInt y) < Int.ofNat (Signed.width α) then
+      pure (x <<< y)
+    else
+      .fail .integerOverflow
+
 /- Check that all operations are implemented -/
 
 class Operations α where
@@ -283,6 +309,7 @@ class Operations α where
   [instHaxDiv: HaxDiv α]
   [instHaxRem: HaxRem α]
   [instHaxShiftRight: HaxShiftRight α α]
+  [instHaxShiftLeft: HaxShiftLeft α α]
 
 instance : Operations u8 where
 instance : Operations u16 where

hax-lib/proof-libs/lean/lake-manifest.json

@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "Hax",
+ "lakeDir": ".lake"}

rust-engine/src/backends/lean.rs

@@ -115,6 +115,7 @@ impl Printer for LeanPrinter {
                 binops::rem,
                 binops::div,
                 binops::shr,
+                binops::shl,
                 binops::bitand,
                 binops::bitxor,
                 binops::logical_op_and,
@@ -582,6 +583,7 @@ set_option linter.unusedVariables false
                         binops::div => "/?",
                         binops::rem => "%?",
                         binops::shr => ">>>?",
+                        binops::shl => "<<<?",
                         binops::bitand => "&&&?",
                         binops::bitxor => "^^^?",
                         binops::logical_op_and => "&&?",

test-harness/src/snapshots/toolchain__lean-tests into-lean.snap

@@ -783,6 +783,7 @@ def Lean_tests.binop_resugarings (x : u32) : RustM u32 := do
   let rem : u32 ← (mul %? (4 : u32));
   let div : u32 ← (rem /? (5 : u32));
   let rshift : u32 ← (div >>>? x);
+  let lshift : u32 ← (div <<<? x);
   (pure x)
 
 def Lean_tests.Reject_do_dsl.rejected

tests/lean-tests/src/lib.rs

@@ -61,5 +61,6 @@ fn binop_resugarings(x: u32) -> u32 {
     let rem = mul % 4;
     let div = rem / 5;
     let rshift = div >> x;
+    let lshift = div << x;
     x
 }