Move the memory to the end in functions (#148)

Co-authored-by: devops <devops@runtimeverification.com>

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.111
+0.1.112

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.111"
+version = "0.1.112"
 description = "K tooling for the RISC-V architecture"
 readme = "README.md"
 requires-python = "~=3.10"

src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

@@ -15,18 +15,18 @@ module SPARSE-BYTES-SIMPLIFICATIONS
 For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` and `#bytes(B +Bytes BS) EF` to obtain as exact as possible values for `pickFront`.
 
 ```k
-  rule pickFront(#bytes(substrBytes(B, I, J) +Bytes _) _ , J0) => substrBytes(substrBytes(B, I, J), 0, J0)
+  rule pickFront(J0, #bytes(substrBytes(B, I, J) +Bytes _) _) => substrBytes(substrBytes(B, I, J), 0, J0)
     requires 0 <=Int I andBool I <=Int J andBool J <=Int lengthBytes(B)
      andBool J0 <=Int lengthBytes(substrBytes(B, I, J))
   [simplification(44), preserves-definedness]
-  rule pickFront(#bytes(B +Bytes _) _ , I) => substrBytes(B, 0, I)
+  rule pickFront(I, #bytes(B +Bytes _) _) => substrBytes(B, 0, I)
     requires I >Int 0 andBool I <=Int lengthBytes(B)    [simplification(45), preserves-definedness]
-  rule pickFront(#bytes(B +Bytes BS) EF, I) => B +Bytes pickFront(#bytes(BS) EF, I -Int lengthBytes(B))
+  rule pickFront(I, #bytes(B +Bytes BS) EF) => B +Bytes pickFront(I -Int lengthBytes(B), #bytes(BS) EF)
     requires I >Int lengthBytes(B)                      [simplification(45), preserves-definedness]
 
-  rule dropFront(#bytes(B +Bytes BS) EF , I) => dropFront(#bytes(substrBytes(B, I, lengthBytes(B)) +Bytes BS) EF, 0) 
+  rule dropFront(I, #bytes(B +Bytes BS) EF) => dropFront(0, #bytes(substrBytes(B, I, lengthBytes(B)) +Bytes BS) EF) 
     requires I >Int 0 andBool I <Int lengthBytes(B)     [simplification(45), preserves-definedness]
-  rule dropFront(#bytes(B +Bytes BS) EF, I) => dropFront(#bytes(BS) EF, I -Int lengthBytes(B)) 
+  rule dropFront(I, #bytes(B +Bytes BS) EF) => dropFront(I -Int lengthBytes(B), #bytes(BS) EF) 
     requires I >=Int lengthBytes(B)                     [simplification(45), preserves-definedness]
 ```
 
@@ -36,11 +36,11 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _`
 To write a byte to a symbolic sparse byte region, we need to:
 
 ```k
-  rule writeBytesBF(#bytes(B +Bytes BS) EF, I, V, NUM) => #bytes(replaceAtBytes(B, I, Int2Bytes(NUM, V, LE)) +Bytes BS) EF
+  rule writeBytesBF(I, V, NUM, #bytes(B +Bytes BS) EF) => #bytes(replaceAtBytes(B, I, Int2Bytes(NUM, V, LE)) +Bytes BS) EF
     requires I >=Int 0 andBool I +Int NUM <=Int lengthBytes(B)  [simplification(45)]
-  rule writeBytesBF(#bytes(B +Bytes BS) EF, I, V, NUM) => prepend(substrBytes(B, 0, I) +Bytes Int2Bytes(NUM, V, LE), dropFront(#bytes(BS) EF, I +Int NUM -Int lengthBytes(B)))
+  rule writeBytesBF(I, V, NUM, #bytes(B +Bytes BS) EF) => prepend(substrBytes(B, 0, I) +Bytes Int2Bytes(NUM, V, LE), dropFront(I +Int NUM -Int lengthBytes(B), #bytes(BS) EF))
     requires I <Int lengthBytes(B) andBool I +Int NUM >Int lengthBytes(B)    [simplification(45)]
-  rule writeBytesBF(#bytes(B +Bytes BS) EF, I, V, NUM) => prepend(B, writeBytesBF(#bytes(BS) EF, I -Int lengthBytes(B), V, NUM))
+  rule writeBytesBF(I, V, NUM, #bytes(B +Bytes BS) EF) => prepend(B, writeBytesBF(I -Int lengthBytes(B), V, NUM, #bytes(BS) EF))
     requires I >=Int lengthBytes(B)                             [simplification(45)]
 ```
 

src/kriscv/kdist/riscv-semantics/riscv.md

@@ -93,16 +93,16 @@ module RISCV-MEMORY
 ```
 We abstract the particular memory representation behind `loadBytes` and `storeBytes` functions. For multi-byte loads and stores, we presume a little-endian architecture.
 ```k
-  syntax Int ::= loadBytes(memory: Memory, address: Int, numBytes: Int) [function, total, symbol(Memory:loadBytes)]
-  rule loadBytes(MEM, ADDR, NUM) => readBytes(MEM, ADDR, NUM)
+  syntax Int ::= loadBytes(address: Int, numBytes: Int, memory: Memory) [function, total, symbol(Memory:loadBytes)]
+  rule loadBytes(ADDR, NUM, MEM) => readBytes(ADDR, NUM, MEM)
 
-  syntax Memory ::= storeBytes(memory: Memory, address: Int, bytes: Int, numBytes: Int) [function, total, symbol(Memory:storeBytes)]
-  rule storeBytes(MEM, ADDR, BS, NUM) => writeBytes(MEM, ADDR, BS, NUM)
+  syntax Memory ::= storeBytes(address: Int, bytes: Int, numBytes: Int, memory: Memory) [function, total, symbol(Memory:storeBytes)]
+  rule storeBytes(ADDR, BS, NUM, MEM) => writeBytes(ADDR, BS, NUM, MEM)
 ```
 Instructions are always 32-bits, and are stored in little-endian format regardless of the endianness of the overall architecture.
 ```k
   syntax Instruction ::= fetchInstr(memory: Memory, address: Int) [function, total]
-  rule fetchInstr(MEM, ADDR) => disassemble(loadBytes(MEM, ADDR, 4))
+  rule fetchInstr(MEM, ADDR) => disassemble(loadBytes(ADDR, 4, MEM))
 ```
 Registers should be manipulated with the `writeReg` and `readReg` functions, which account for `x0` always being hard-wired to contain all `0`s.
 ```k
@@ -314,40 +314,40 @@ The remaining branch instructions proceed analogously, but performing different
 `LB`, `LH`, and `LW` load `1`, `2`, and `4` bytes respectively from the memory address which is `OFFSET` greater than the value in register `RS1`, then sign extends the loaded bytes and places them in register `RD`.
 ```k
   rule <instrs> LB RD , OFFSET ( RS1 ) => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 1), 8)) </regs>
+       <regs> REGS => writeReg(REGS, RD, signExtend(loadBytes(readReg(REGS, RS1) +Word chop(OFFSET), 1, MEM), 8)) </regs>
        <mem> MEM </mem>
 
   rule <instrs> LH RD , OFFSET ( RS1 ) => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 2), 16)) </regs>
+       <regs> REGS => writeReg(REGS, RD, signExtend(loadBytes(readReg(REGS, RS1) +Word chop(OFFSET), 2, MEM), 16)) </regs>
        <mem> MEM </mem>
 
   rule <instrs> LW RD , OFFSET ( RS1 ) => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, signExtend(loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 4), 32)) </regs>
+       <regs> REGS => writeReg(REGS, RD, signExtend(loadBytes(readReg(REGS, RS1) +Word chop(OFFSET), 4, MEM), 32)) </regs>
        <mem> MEM </mem>
 ```
 `LBU` and `LHU` are analogous to `LB` and `LH`, but zero-extending rather than sign-extending.
 ```k
    rule <instrs> LBU RD , OFFSET ( RS1 ) => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 1)) </regs>
+       <regs> REGS => writeReg(REGS, RD, loadBytes(readReg(REGS, RS1) +Word chop(OFFSET), 1, MEM)) </regs>
        <mem> MEM </mem>
 
   rule <instrs> LHU RD , OFFSET ( RS1 ) => .K ...</instrs>
-       <regs> REGS => writeReg(REGS, RD, loadBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), 2)) </regs>
+       <regs> REGS => writeReg(REGS, RD, loadBytes(readReg(REGS, RS1) +Word chop(OFFSET), 2, MEM)) </regs>
        <mem> MEM </mem>
 ```
 Dually, `SB`, `SH`, and `SW` store the least-significant `1`, `2`, and `4` bytes respectively from `RS2` to the memory address which is `OFFSET` greater than the value in register `RS1`.
 ```k
   rule <instrs> SB RS2 , OFFSET ( RS1 ) => .K ...</instrs>
        <regs> REGS </regs>
-       <mem> MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), readReg(REGS, RS2) &Int 255, 1) </mem>
+       <mem> MEM => storeBytes(readReg(REGS, RS1) +Word chop(OFFSET), readReg(REGS, RS2) &Int 255, 1, MEM) </mem>
 
   rule <instrs> SH RS2 , OFFSET ( RS1 ) => .K ...</instrs>
        <regs> REGS </regs>
-       <mem> MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), readReg(REGS, RS2) &Int 65535, 2) </mem>
+       <mem> MEM => storeBytes(readReg(REGS, RS1) +Word chop(OFFSET), readReg(REGS, RS2) &Int 65535, 2, MEM) </mem>
 
   rule <instrs> SW RS2 , OFFSET ( RS1 ) => .K ...</instrs>
        <regs> REGS </regs>
-       <mem> MEM => storeBytes(MEM, readReg(REGS, RS1) +Word chop(OFFSET), readReg(REGS, RS2) &Int 4294967295, 4) </mem>
+       <mem> MEM => storeBytes(readReg(REGS, RS1) +Word chop(OFFSET), readReg(REGS, RS2) &Int 4294967295, 4, MEM) </mem>
 ```
 We presume a single hart with exclusive access to memory, so `FENCE` and `FENCE.TSO` are no-ops.
 ```k

src/kriscv/kdist/riscv-semantics/sparse-bytes.md

@@ -49,62 +49,62 @@ We provide helpers to prepend either data or an empty region to an existing `Spa
 ```
 `pickFront` is a helper function for picking the first `N` bytes from a `SparseBytes` value.
 ```k
-  syntax Bytes ::= pickFront(SparseBytes, Int) [function, total]
-  rule pickFront(_, I) => .Bytes requires I <=Int 0
-  rule pickFront(.SparseBytes, I) => .Bytes requires I >Int 0
-  rule pickFront(#empty(N) _, I) => padRightBytes(.Bytes, I, 0)
+  syntax Bytes ::= pickFront(Int, SparseBytes) [function, total]
+  rule pickFront(I, _) => .Bytes requires I <=Int 0
+  rule pickFront(I, .SparseBytes) => .Bytes requires I >Int 0
+  rule pickFront(I, #empty(N) _) => padRightBytes(.Bytes, I, 0)
     requires I >Int 0 andBool I <=Int N
-  rule pickFront(#empty(N) BF, I) => padRightBytes(.Bytes, I, 0) +Bytes pickFront(BF, I -Int N)
+  rule pickFront(I, #empty(N) BF) => padRightBytes(.Bytes, I, 0) +Bytes pickFront(I -Int N, BF)
     requires I >Int 0 andBool I >Int N
-  rule pickFront(#bytes(B) _, I) => substrBytes(B, 0, I)
+  rule pickFront(I, #bytes(B) _) => substrBytes(B, 0, I)
     requires I >Int 0 andBool I <=Int lengthBytes(B)
-  rule pickFront(#bytes(B) EF, I) => B +Bytes pickFront(EF, I -Int lengthBytes(B))
+  rule pickFront(I, #bytes(B) EF) => B +Bytes pickFront(I -Int lengthBytes(B), EF)
     requires I >Int lengthBytes(B)
 ```
 `dropFront` is a helper function for dropping the first `N` bytes from a `SparseBytes` value.
 ```k
-  syntax SparseBytes ::=  dropFront(SparseBytes, Int) [function, total]
-  rule dropFront(SBS, I) => SBS    requires I <=Int 0
-  rule dropFront(.SparseBytes, I) => .SparseBytes requires I >Int 0
-  rule dropFront(#empty(N) BF, I) => #empty(N -Int I) BF requires I >Int 0 andBool I <Int N
-  rule dropFront(#empty(N) BF, I) => dropFront(BF, I -Int N) requires I >Int 0 andBool I >=Int N
-  rule dropFront(#bytes(B) EF, I) => dropFront(#bytes(substrBytes(B, I, lengthBytes(B))) EF, 0) 
+  syntax SparseBytes ::=  dropFront(Int, SparseBytes) [function, total]
+  rule dropFront(I, SBS) => SBS    requires I <=Int 0
+  rule dropFront(I, .SparseBytes) => .SparseBytes requires I >Int 0
+  rule dropFront(I, #empty(N) BF) => #empty(N -Int I) BF requires I >Int 0 andBool I <Int N
+  rule dropFront(I, #empty(N) BF) => dropFront(I -Int N, BF) requires I >Int 0 andBool I >=Int N
+  rule dropFront(I, #bytes(B) EF) => dropFront(0, #bytes(substrBytes(B, I, lengthBytes(B))) EF) 
     requires I >Int 0 andBool I <Int lengthBytes(B)
-  rule dropFront(#bytes(B) EF, I) => dropFront(EF, I -Int lengthBytes(B)) requires I >=Int lengthBytes(B)
+  rule dropFront(I, #bytes(B) EF) => dropFront(I -Int lengthBytes(B), EF) requires I >=Int lengthBytes(B)
 ```
 `readBytes(SBS, I, NUM)` reads `NUM` bytes from a given index `I` in `O(E)` time, where `E` is the number of `#empty(_)` or `#bytes(_)` entries in the list up to the location of the index.
 ```k
-  syntax Int ::= readBytes(SparseBytes, Int, Int) [function, total]
+  syntax Int ::= readBytes(Int, Int, SparseBytes) [function, total]
 
-  rule readBytes(SBS, I, NUM) => Bytes2Int(pickFront(dropFront(SBS, I), NUM), LE, Unsigned)
+  rule readBytes(I, NUM, SBS) => Bytes2Int(pickFront(NUM, dropFront(I, SBS)), LE, Unsigned)
 ```
 `writeBytes(SBS, I, V, NUM)` writes value `V` with length `NUM` bytes to a given index `I`. With regards to time complexity,
 - If the index is in the middle of an existing `#empty(_)` or `#bytes(_)` region, time complexity is `O(E)` where `E` is the number of entries up to the index.
 - If the index happens to be the first or last index in an `#empty(_)` region directly boarding a `#bytes(_)` region, then the `#bytes(_)` region must be re-allocated to append the new value, giving worst-case `O(E + B)` time, where `E` is the number of entries up to the location of the index and `B` is the size of this existing `#bytes(_)`.
 ```k
   syntax SparseBytes ::=
-      writeBytes  (SparseBytes  , Int, Int, Int) [function, total]
-    | writeBytesEF(SparseBytesEF, Int, Int, Int) [function, total]
-    | writeBytesBF(SparseBytesBF, Int, Int, Int) [function, total]
+      writeBytes  (Int, Int, Int, SparseBytes  ) [function, total]
+    | writeBytesEF(Int, Int, Int, SparseBytesEF) [function, total]
+    | writeBytesBF(Int, Int, Int, SparseBytesBF) [function, total]
 
-  rule writeBytes(BF:SparseBytesBF, I, V, NUM) => writeBytesBF(BF, I, V, NUM)
-  rule writeBytes(EF:SparseBytesEF, I, V, NUM) => writeBytesEF(EF, I, V, NUM)
+  rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF)
+  rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF)
 
-  rule writeBytesEF(_           , I, _, _) => .SparseBytes    requires I <Int 0 // error case for totality
-  rule writeBytesEF(.SparseBytes, I, V, NUM) => prependEmpty(I, #bytes(Int2Bytes(NUM, V, LE)) .SparseBytes)    requires I >=Int 0
-  rule writeBytesEF(#empty(N) BF, I, V, NUM) => prependEmpty(I, prepend(Int2Bytes(NUM, V, LE), prependEmpty(N -Int I -Int NUM, BF)))
+  rule writeBytesEF(I, _, _  , _           ) => .SparseBytes    requires I <Int 0 // error case for totality
+  rule writeBytesEF(I, V, NUM, .SparseBytes) => prependEmpty(I, #bytes(Int2Bytes(NUM, V, LE)) .SparseBytes)    requires I >=Int 0
+  rule writeBytesEF(I, V, NUM, #empty(N) BF) => prependEmpty(I, prepend(Int2Bytes(NUM, V, LE), prependEmpty(N -Int I -Int NUM, BF)))
     requires I >=Int 0 andBool I +Int NUM <=Int N
-  rule writeBytesEF(#empty(N) BF, I, V, NUM) => prependEmpty(I, prepend(Int2Bytes(NUM, V, LE), dropFront(BF, I +Int NUM -Int N)))
+  rule writeBytesEF(I, V, NUM, #empty(N) BF) => prependEmpty(I, prepend(Int2Bytes(NUM, V, LE), dropFront(I +Int NUM -Int N, BF)))
     requires I <Int N andBool I +Int NUM >Int N
-  rule writeBytesEF(#empty(N) BF, I, V, NUM) => prependEmpty(N, writeBytesBF(BF, I -Int N, V, NUM))
+  rule writeBytesEF(I, V, NUM, #empty(N) BF) => prependEmpty(N, writeBytesBF(I -Int N, V, NUM, BF))
     requires I >=Int N
 
-  rule writeBytesBF(_           , I, _, _  ) => .SparseBytes    requires I <Int 0 // error case for totality
-  rule writeBytesBF(#bytes(B) EF, I, V, NUM) => #bytes(replaceAtBytes(B, I, Int2Bytes(NUM, V, LE))) EF
+  rule writeBytesBF(I, _, _  , _           ) => .SparseBytes    requires I <Int 0 // error case for totality
+  rule writeBytesBF(I, V, NUM, #bytes(B) EF) => #bytes(replaceAtBytes(B, I, Int2Bytes(NUM, V, LE))) EF
     requires I >=Int 0 andBool I +Int NUM <=Int lengthBytes(B)
-  rule writeBytesBF(#bytes(B) EF, I, V, NUM) => prepend(substrBytes(B, 0, I) +Bytes Int2Bytes(NUM, V, LE), dropFront(EF, I +Int NUM -Int lengthBytes(B)))
+  rule writeBytesBF(I, V, NUM, #bytes(B) EF) => prepend(substrBytes(B, 0, I) +Bytes Int2Bytes(NUM, V, LE), dropFront(I +Int NUM -Int lengthBytes(B), EF))
     requires I <Int lengthBytes(B) andBool I +Int NUM >Int lengthBytes(B)
-  rule writeBytesBF(#bytes(B) EF, I, V, NUM) => prepend(B, writeBytesEF(EF, I -Int lengthBytes(B), V, NUM))
+  rule writeBytesBF(I, V, NUM, #bytes(B) EF) => prepend(B, writeBytesEF(I -Int lengthBytes(B), V, NUM, EF))
     requires I >=Int lengthBytes(B)
 endmodule
 ```

src/kriscv/term_builder.py

@@ -278,11 +278,11 @@ def sort_memory() -> KSort:
 
 
 def load_bytes(mem: KInner, addr: KInner, num_bytes: KInner) -> KInner:
-    return KApply('Memory:loadBytes', mem, addr, num_bytes)
+    return KApply('Memory:loadBytes', addr, num_bytes, mem)
 
 
 def store_bytes(mem: KInner, addr: KInner, value: KInner, num_bytes: KInner) -> KInner:
-    return KApply('Memory:storeBytes', mem, addr, value, num_bytes)
+    return KApply('Memory:storeBytes', addr, value, num_bytes, mem)
 
 
 def regs(dct: dict[int, int]) -> KInner:

src/tests/integration/test-data/specs/pick-drop0.k

@@ -4,7 +4,7 @@ module PICK-DROP0
   claim [id]:
     <instrs> #CHECK_HALT => #HALT </instrs>
     <regs>
-        1 |-> (signExtend ( ... bits: Bytes2Int ( pickFront ( dropFront ( #bytes ( W1:Bytes +Bytes b"\x00\x00\x00\x00" ) #empty ( 4 ) #bytes ( Int2Bytes ( 4 , signExtend ( ... bits: Bytes2Int ( substrBytes ( W0:Bytes , 28 , 32 ) , LE , Unsigned ) , signBitIdx: 32 ) &Int 4294967295 , LE )  ) .SparseBytes , 20 ) , 4 ) , LE , Unsigned ) , signBitIdx: 32 ) => Bytes2Int ( substrBytes ( W1 , 20 , 24 ) , LE , Unsigned ))
+        1 |-> (signExtend ( ... bits: Bytes2Int ( pickFront ( 4 , dropFront ( 20 , #bytes ( W1:Bytes +Bytes b"\x00\x00\x00\x00" ) #empty ( 4 ) #bytes ( Int2Bytes ( 4 , signExtend ( ... bits: Bytes2Int ( substrBytes ( W0:Bytes , 28 , 32 ) , LE , Unsigned ) , signBitIdx: 32 ) &Int 4294967295 , LE )  ) .SparseBytes ) ) , LE , Unsigned ) , signBitIdx: 32 ) => Bytes2Int ( substrBytes ( W1 , 20 , 24 ) , LE , Unsigned ))
     </regs>
     <pc> 0 </pc>
     <haltCond> ADDRESS ( 0 ) </haltCond>

src/tests/integration/test-data/specs/pickfront0.k

@@ -8,7 +8,7 @@ module PICKFRONT0
     </regs>
     <pc> 0 </pc>
     <mem>
-    #bytes(pickFront ( #bytes ( substrBytes ( W0:Bytes , 16 , 32 ) +Bytes W1:Bytes +Bytes b"\x00\x00\x00\x00\x00" ) .SparseBytes , 4 )) .SparseBytes
+    #bytes(pickFront ( 4 , #bytes ( substrBytes ( W0:Bytes , 16 , 32 ) +Bytes W1:Bytes +Bytes b"\x00\x00\x00\x00\x00" ) .SparseBytes )) .SparseBytes
     => #bytes ( substrBytes ( W0:Bytes , 16 , 20 ) ) .SparseBytes
     </mem>
     <haltCond> ADDRESS ( 0 ) </haltCond>

…n/test-data/specs/store-symbolic-bytes.k …n/test-data/specs/store-symbolic-value.ksrc/tests/integration/test-data/specs/store-symbolic-bytes.k renamed to src/tests/integration/test-data/specs/store-symbolic-value.k src/tests/integration/test-data/specs/store-symbolic-bytes.k renamed to src/tests/integration/test-data/specs/store-symbolic-value.k

@@ -1,4 +1,4 @@
-module STORE-SYMBOLIC-BYTES
+module STORE-SYMBOLIC-VALUE
   imports RISCV
 
   claim [id]:
@@ -9,10 +9,10 @@ module STORE-SYMBOLIC-BYTES
     <pc> 0 </pc>
     <mem>
     storeBytes(
-        #bytes ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes, 
         0, 
         X:Int,
-        4
+        4,
+        #bytes ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes
     ) =>
     #bytes ( Int2Bytes ( 4 , X , LE ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes
     </mem>