Lean 4 backend: further function implementation (2) (#4827)

This PR implements the following functions in the Lean 4 backend
prelude:

- `modInt`
- `>=Int`
- `Bytes2Int`
- `Bytes.substr`

Due to implementing `Bytes2Int` the PR also adds `SortSignedness` to the
prelude, excluding it from the automatic generation.

Author: JuanCoRo

pyk/src/pyk/klean/k2lean4.py

@@ -59,25 +59,30 @@
     'SortString',
     'SortStringBuffer',
     'SortEndianness',
+    'SortSignedness',
 }
 _PRELUDE_FUNCS: Final = {
     "Lbl'UndsPlus'Int'Unds'",  # +Int
     "Lbl'Unds'-Int'Unds'",  # -Int
     "Lbl'UndsStar'Int'Unds'",  # *Int
     "Lbl'UndsSlsh'Int'Unds'",  # /Int
+    "Lbl'Unds'modInt'Unds'",  # modInt
     "LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int",  # maxInt
     "Lbl'Tild'Int'Unds'",  # ~Int
     "Lbl'Unds-LT-Eqls'Int'Unds'",  # <=Int
+    "Lbl'Unds-GT-Eqls'Int'Unds'",  # >=Int
     "Lbl'Unds-LT-'Int'Unds'",  # <Int
     "Lbl'Unds-GT-'Int'Unds'",  # >Int
     "Lbl'UndsEqlsEqls'Int'Unds'",  # ==Int
     "Lbl'Stop'Bytes'Unds'BYTES-HOOKED'Unds'Bytes",  # Bytes.empty
     "Lbllog2Int'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int",  # Int.log2
     "LblInt2Bytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Int'Unds'Int'Unds'Endianness",  # Int2Bytes
+    "LblBytes2Int'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Int'Unds'Bytes'Unds'Endianness'Unds'Signedness",  # Bytes2Int
     "LblpadRightBytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Bytes'Unds'Int'Unds'Int",  # padRight
     "LblpadLeftBytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Bytes'Unds'Int'Unds'Int",  # padLeft
     "LbllengthBytes'LParUndsRParUnds'BYTES-HOOKED'Unds'Int'Unds'Bytes",  # Bytes.length
     "LblreplaceAtBytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Bytes'Unds'Int'Unds'Bytes",  # Bytes.replaceAt
+    "LblsubstrBytes'LParUndsCommUndsCommUndsRParUnds'BYTES-HOOKED'Unds'Bytes'Unds'Bytes'Unds'Int'Unds'Int",  # Bytes.substr
 }
 
 _SYMBOL_OVERRIDES: Final = {

pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}/Prelude.lean

@@ -240,15 +240,18 @@ def «_+Int_» (x0 x1 : SortInt) : Option SortInt := some (x0 + x1)
 def «_-Int_» (x0 x1 : SortInt) : Option SortInt := some (x0 - x1)
 def «_*Int_» (x0 x1 : SortInt) : Option SortInt := some (x0 * x1)
 def «_/Int_» (x0 x1 : SortInt) : Option SortInt :=
-  if x1 == 0 then none else some (Int.tdiv x0 x1)
+  ite (x1 == 0) none (Int.tdiv x0 x1)
+def _modInt_ (x0 : SortInt) (x1 : SortInt) : Option SortInt :=
+  ite (x1 == 0) none (Int.emod x0 x1)
 def «maxInt(_,_)_INT-COMMON_Int_Int_Int» (x0 x1 : SortInt) :=
   some (ite (x0 < x1) x1 x0)
 def «log2Int(_)_INT-COMMON_Int_Int» (x0 : SortInt) : Option SortInt :=
-  ite (0 < x0) (some (Nat.log2 x0.toNat)) none
+  ite (0 < x0) ((Nat.log2 x0.toNat) : Int) none
 def «~Int_» (x0 : SortInt) : Option SortInt := some (.not x0)
 
 -- Comparisons
 def «_<=Int_» (x0 x1 : SortInt) : Option SortBool := some (x0 <= x1)
+def «_>=Int_» (x0 x1 : SortInt) : Option SortBool := some (x0 >= x1)
 def «_<Int_» (x0 x1 : SortInt) : Option SortBool := some (x0 < x1)
 def «_>Int_» (x0 x1 : SortInt) : Option SortBool := some (x0 > x1)
 def «_==Int_» (x0 x1 : SortInt) : Option SortBool := some (x0 == x1)
@@ -260,6 +263,11 @@ inductive SortEndianness : Type where
   | littleEndianBytes : SortEndianness
   deriving BEq, DecidableEq
 
+inductive SortSignedness : Type where
+  | signedBytes : SortSignedness
+  | unsignedBytes : SortSignedness
+  deriving BEq, DecidableEq
+
 def «.Bytes_BYTES-HOOKED_Bytes» : Option SortBytes := some .empty
 
 -- Adapted from https://github.com/runtimeverification/haskell-backend/blob/362dab30d6435ec117862fea722be67373572034/kore/src/Kore/Builtin/InternalBytes.hs#L496-L511
@@ -277,6 +285,31 @@ def «Int2Bytes(_,_,_)_BYTES-HOOKED_Bytes_Int_Int_Endianness» (x0 x1 : SortInt)
       | .succ l, n => ⟨(n % 256).toNat⟩ :: bytes l (n / 256)
     bytes x0.toNat x1
 
+-- Adapted from
+-- https://github.com/runtimeverification/haskell-backend/blob/362dab30d6435ec117862fea722be67373572034/kore/src/Kore/Builtin/InternalBytes.hs#L527-L543
+-- Note that we use `List.foldl` and not `ByteArray.foldl` for ease of reasoning
+def «Bytes2Int(_,_,_)_BYTES-HOOKED_Int_Bytes_Endianness_Signedness» (bytes : SortBytes) (endian : SortEndianness) (sign : SortSignedness) : Option SortInt :=
+  match sign with
+  | .unsignedBytes => Int.ofNat unsigned
+  | .signedBytes => if 2 * unsigned >= modulus then (Int.ofNat unsigned) - (Int.ofNat modulus)
+                    else Int.ofNat unsigned
+  where
+  modulus : Nat := res.1
+  unsigned : Nat := res.2
+  res : Nat×Nat :=
+    let littleEndian := match endian with
+                        | .littleEndianBytes => bytes.toList
+                            --match bytes with |⟨⟨l⟩⟩ => l
+                        | .bigEndianBytes => bytes.toList.reverse
+                            --match bytes with |⟨⟨l⟩⟩ => l.reverse
+    let go (res : Nat×Nat) (b : UInt8) : Nat×Nat :=
+      -- `place` is `res.1`
+      -- `acc` is `res.2`
+      let place := res.1 * 0x100
+      let acc := res.2 + res.1 * b.toNat
+      ⟨place, acc⟩
+    List.foldl go (1, 0) littleEndian
+
 /--
 Pads to the right `len - b.length` bytes with specified `val` value
 -/
@@ -304,3 +337,12 @@ def «replaceAtBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Bytes» (dest : SortByt
   let init := dest.data.extract 0 index.toNat
   let rem := dest.data.extract (index.toNat + src.size) dest.size
   some { data := init ++ src.data ++ rem }
+
+/--
+Get a new `Bytes` object containing a range of bytes from the input `Bytes`
+-/
+def «substrBytes(_,_,_)_BYTES-HOOKED_Bytes_Bytes_Int_Int» (b : SortBytes) (startIndex : SortInt) (endIndex : SortInt) : Option SortBytes :=
+  if startIndex < 0 then none else
+  if endIndex < startIndex then none else
+  if b.size < endIndex then none else
+  b.extract startIndex.toNat endIndex.toNat