# Verification of Control System Runtime Using an Executable Semantic Model +
## 4 Denotations of Instructions
### Memory and Stack Operations  
Listing 2 illustrates the implementation of Get1 BMem and Get8 BMem functions, which read 1 and 8 bytes of data from memory, respectively. Similar functions for reading 2 and 4 bytes are also implemented. They take an address and memory as parameters to specify the data retrieval. Get1 BMem returns a byte value obtained from the specified memory address, while Get8 BMem retrieves 8 bytes, converts them to a uint64 value, and returns it. The lower part of Listing 2 showcases Upd1 BMem and Upd4 BMem functions, responsible for writing 1 and 4 bytes of data to memory, respectively. Upd1 BMem writes the byte value to the memory at the specified address and returns the updated memory. Upd4 BMem converts the uint32 value to an array of bytes, then inserts each byte value into the memory starting from the specified address. Copying data from the source memory to the destination memory is achieved through the MemMove function as depicted in Listing 3. The first two parameters determine the starting index for copying data to the destination memory, while the subsequent two parameters denote the index and source memory, respectively. The final parameter specifies the number of bytes to be copied. Initially, a new memory is instantiated, serving as a duplicate of the destination memory. Subsequently, the function retrieves the specified number of bytes from the source memory. Then, it inserts the copied bytes from the source memory into the newly created memory, commencing from the designated destination address, _address\(1\)_. Ultimately, the updated memory is returned. ```
letGet1 BMem(address:Address,mem:Storage):byte= mem. [int<|address] letGet8 BMem(address:Address,mem:Storage):uint64= letbyteArray=[| letmutableiterator=address while(iterator<address+8 us)do yieldmem. [int<|iterator] iterator<-iterator+1 us| |] BitConverter.ToUlnt64(byteArray,0) letUpd1 BMem(address:Address,mem:Storage,value:byte):Storage= letnew_mem=Array.copymem new_mem. [int<|address]<-value new_mem letUpd8 BMem(address:Address,mem:Storage,value:uint64):Storage= letnew_mem=Array.copymem letbyteArray=BitConverter.GetBytes(value) letmutableiterator=address forbinbyteArraydo new_mem. [int<|iterator]<-b iterator<-iterator+1 us new_mem
```  
Listing 3: Memory read and update functions. ```
letMemMove(address1:Address,mem1:Storage,address2:Address,mem2:Storage,count:uint16):Storage= letnew_mem=Array.copymem1 letcopiedByteArray=[| letmutableiterator=address2 while(iterator<address2+count)do yieldmem2. [int<|iterator] iterator<-iterator+1 us| |] letmutableiterator2=address1 forbincopiedByteArraydo new_mem. [int<|iterator2]<-b iterator2<-iterator2+1 us new_mem
```  
On Listing 4, the implementations of stack-related functions are presented. The Push function takes as parameters the stack on which a value of type Address is to be pushed. If the stack is empty, the value is pushed onto the stack, and a new stack with the pushed value is returned. If the stack represented by the list already contains values, the list elements are reversed, the value to be pushed is added to the beginning of the list, and then the list elements are reversed again. The Pop function takes the stack as a parameter, and its task is to return the last pushed value on the stack along with the new stack after removing the value. If the stack is empty, the function returns None along with an empty stack and an appropriate message for the user. Otherwise, the last value from the list, which is the last pushed address on the stack, is retrieved, and this value is returned along with the stack after removing this value.