Conventional commits are overrated.

\begin{exmp}

    Consider signature $\texttt{BV[t]}$. Let $\texttt{BV.Sym} = \{or\}$ and $\texttt{BV.T} = \{t\}$.

    Mapping $\varphi$ for $or$ results in: \[ or~::~(t \rightarrow \vartextvisiblespace)~

                                                      (t \rightarrow \vartextvisiblespace)~

                                                      (\vartextvisiblespace \rightarrow t)\]

    Mapping $\varphi$ for $or$ results in: \[or~::~(t \rightarrow \vartextvisiblespace)

                                                  ~(t \rightarrow \vartextvisiblespace)

                                                  ~(\vartextvisiblespace \rightarrow t)\]

\end{exmp}

\subsection{Structure}

                \State $set~ith~bit~in~res~on~0$

            \EndIf

        \EndFor

    \State~\Return~$res$

    \State\Return~$res$

    \caption{Pseudocode for \texttt{or} function symbol from structure $bv_{32}$}

    \end{algorithmic}

\label{alg:or}

Once it is empty, the computation ends. In this thesis, stacks are formally defined as follows:

\begin{theorem}

    Assume a finite set of values $\Gamma$. A stack \texttt{St} is a finite sequence of values,

    Assume a finite set of values~$\Gamma$. A stack \texttt{St} is a finite sequence of values,

    thus $St = \Gamma^k,~where~k \in \mathbb{N}$. Analogically, the definition of the set of

    all stacks is:

    \[S = \{\Gamma^k~|~\forall~k \in \mathbb{N}\}\]

The machine reaches an \textit{undefined state} whenever the value on the first stack is not an instruction

or the executed instruction is ill-formed. This state is denoted as $\bot$.

\paragraph{Program}

\begin{theorem}

    A program from the Cthulhu point of view is defined as a quadruple \texttt{(H, M, T, s)}, where:

    \begin{itemize}

    \end{itemize}

\end{theorem}

Each instruction encodet into 32 bits.~\textit{Structure id} represents first

Each instruction encoded into 32 bits.~\textit{Structure id} represents first

12 bits, whereas \textit{operation} and its \textit{arguments} are encoded into the remaining 20 bits.

\begin{exmp}

    As an example consider the following instruction:

\subsection{Quote instruction}

\textit{Quote instruction} is a signature that defines operations serving as constructors for 

instructions in a particular program. Formally, it is defined as follows:

instructions in the particular program. Formally, it is defined as follows:

\begin{theorem}

    Let $\mathcal{P}$ be an arbitrary program. Q is signature \texttt{(T, Sym, $\varphi$)}, where

    \begin{itemize}

        \item $T~=~\{instr\}$

        \item $Sym~=~\{quote(x)\}$, where $x$ is an instruction. However, instructions may only

              consist of operations from set $\mathcal{P}.M~\setminus~\{q\}$, where $\mathcal{P}.M$

              is the set of all structures in the program $\mathcal{P}$ and $q$ is the structure

              implementing signature \texttt{Q}. In other words, operation $quote(x)$ is undefined

              for other quote instructions.

        \item $Sym~=~\{quote(x)\}$, where $x$ is an instruction that consist of an operation from set

              $\mathcal{P}.M~\setminus~\{q\}$, where $\mathcal{P}.M$ is the set of all structures in the

              program $\mathcal{P}$ and $q$ is the structure implementing signature \texttt{Q}. In other words,

              operation $quote(x)$ is undefined for other quote instructions.

        \item $quote(x)~::~(\vartextvisiblespace \rightarrow instr)$

    \end{itemize}

\end{theorem}

The structure implementing quote instruction signature is defined for each program separately,

since its definition is tied up to instructions used in the particular program.

\begin{exmp}

As an example consider the instruction from example 4. The quote instruction for it has the

following form:

\[quote(bv_{32}~add~1~2~3)~A\] where A is the number of stack where newly created instruction

should be pushed.

\end{exmp}

\section{Predefined structures}

Cthulhu offers several pre-defined structures that implement three distinct

signatures, which are detailed in the following section. These provided structures serve as

        \item $Sym~=~\{const,~store,~fetch\}$

        \item $const~::~(\vartextvisiblespace \rightarrow d)$

        \item $store~::~(d \rightarrow \vartextvisiblespace)

                       ~(key \rightarrow \vartextvisiblespace)

                       ~(value \rightarrow \vartextvisiblespace)

                       ~(k \rightarrow \vartextvisiblespace)

                       ~(v \rightarrow \vartextvisiblespace)

                       ~(\vartextvisiblespace \rightarrow d)$

        \item $fetch~::~(X \rightarrow s[X])

                       ~(d \rightarrow \vartextvisiblespace)

                       ~(key \rightarrow \vartextvisiblespace)

                       ~(\vartextvisiblespace \rightarrow value)

                       ~(k \rightarrow \vartextvisiblespace)

                       ~(\vartextvisiblespace \rightarrow v)

                       ~(\vartextvisiblespace \rightarrow d)$

    \end{itemize}

    Where $X \in G^*,~G \subseteq T$ and $d,~key,~value \in T$. $s[X]$ represents

    Where $X \in G^*,~G \subseteq T$ and $d,~k,~v \in T$. $s[X]$ represents

    a sequence of types from $X$ and holds that $s[X] \in T$.

\end{description}

Cthulhu provides the corresponding structure named $dict$. In the following are

\begin{itemize}

    \item \texttt{Const} creates a new dictionary on a given stack.

    \item \texttt{Store} creates a new dictionary with inserted pair key-value.

    \item \texttt{Fetch} 

    \item \texttt{Fetch} obtains a value from the given dictionary and removes the key-value pair.

\end{itemize}

Corresponding structure \texttt{q} implementing signature \texttt{Q} is provided.

It has only one operation named $quot$ that has a bit different syntax as usual.

Consider the instruction from example 4. The quote instruction for it has the following form:

\[quote(bv_{32}~add~1~2~3)~A\] where A is the number of stack where newly created instruction

should be pushed.

\section{Linearity}

The linearity principle restricts a program to use each value exactly once during

the computation. All values stored on the stacks are created during the computation,

operations mirror modifications that the modeled operation performs when executed on the

Cthulhu machine:

\begin{itemize}

    \item \texttt{Pop A as X} removes a value from the top of the stack \texttt{A} and stores

    \item \texttt{POP A as X} removes a value from the top of the stack \texttt{A} and stores

          it into the variable \texttt{X}.

    \item \texttt{Push X to A} stores the value \texttt{X} on the top of the stack \texttt{A}.

    \item \texttt{Pack A as X} pops all values from the stack \texttt{A} and stores them into the sequence \texttt{X}.

    \item \texttt{Unpack X to A} pushes all values from the sequence \texttt{X} on the stack \texttt{B}.

    \item \texttt{PUSH X to A} stores the value \texttt{X} on the top of the stack \texttt{A}.

    \item \texttt{PASK A as X} pops all values from the stack \texttt{A} and stores them into the sequence \texttt{X}.

    \item \texttt{UNPACK X to A} pushes all values from the sequence \texttt{X} on the stack \texttt{B}.

    \item \texttt{X $\leftarrow$ op $Y_1,\ldots,~Y_n$} assigns variable \texttt{X} the result of

          an operation \texttt{op} applied to arguments $Y_1,~\ldots,~Y_n$, $n \in \mathbb{N}$.

    \item \texttt{INSERT [ K~: V ] to D} stores a key-value pair into the dictionary \texttt{D}.

    \item \texttt{[ V, E ] $\leftarrow$ OBTAIN K from D} obtains the value \texttt{V} under the

          key \texttt{K} from the dictionary \texttt{D}. OBTAIN creates a new dictionary \texttt{E}

          without the key-value pair, too.

\end{itemize}

Programs modeled via this operations are not restricted by the linearity principle.

However, the operations that they model are still linear. That is the result of the

atomic behavior of each auxiliary operation; thus, its non-linear implementation is not

reflected at the higher level.

atomic behavior of each operation; thus, its non-linear implementation is not reflected

at the higher level.

\subsection{Evaluation step}

In this subsection, the transformations between the Cthulhu machine states are described.

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~~~~A~as~X

        \State~POP~A~as~X

        \State~UNPACK~X~to~B

    \caption{seq unpack A B}

    \end{algorithmic}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~~A~as~X

        \State~POP~A~as~X

        \State~reverse~values~in~sequence~X

        \State~PUSH~X~to~B

    \caption{seq reverse A B}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~~A~as~X

        \State~POP~A~as~X

        \State~PUSH~X~to~B

        \State~PUSH~X~to~C

    \caption{seq dup A B}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~PACK~~~A~as~X

        \State~POP~~~~B~as~Y

        \State~PACK~A~as~X

        \State~POP~B~as~Y

        \State~UNPACK~Y~to~A

        \State~PUSH~~~X~to~C

        \State~PUSH~X~to~C

    \caption{seq pivot A B C}

    \end{algorithmic}

\label{alg:seq_pivot}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~X~$\leftarrow$~const

        \State~X~$\gets$~const

        \State~PUSH~X~to~A

    \caption{bv const}

    \end{algorithmic}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~A~as~X

        \State~Y~$\leftarrow$~unop~X

        \State~Y~$\gets$~unop~X

        \State~PUSH~Y~to~B

    \caption{bv unop A B}

    \end{algorithmic}

    \begin{algorithmic}

        \State~POP~A~as~X

        \State~POP~B~as~Y

        \State~Z~$\leftarrow$~binop~X~Y

        \State~Z~$\gets$~binop~X~Y

        \State~PUSH~Z~to~C

    \caption{bv binop A B C}

    \end{algorithmic}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~~A~as~X

        \State~POP~A~as~X

        \State~PUSH~X~to~B

    \caption{bv move A B}

    \end{algorithmic}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~~A~as~X

        \State~POP~A~as~X

        \State~PUSH~X~to~B

        \State~PUSH~X~to~C

    \caption{bv dup A B}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~A~as~X

        \State~evaluate~the~condition~X

        \State~if~true~~-~continue~in~computation

        \State~if~false~-~abort~the~program

        \State~decide~according~to~value~in~X

        \State~if~X~==~1~-~continue~in~computation

        \State~if~X~==~0~-~abort~the~program

    \caption{bv assume A}

    \end{algorithmic}

\label{alg:bv_assume}

\subsubsection{Dictionary operations}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~X~$\leftarrow$~const

        \State~X~$\gets$~const

        \State~PUSH~X~to~A

    \caption{dict const A}

    \end{algorithmic}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~POP~~A~as~X

        \State~POP~~B~as~K

        \State~POP~A~as~X

        \State~POP~B~as~K

        \State~PACK~C~as~V

        \State~requires~K~not~to~be~present~in~X

        \State~INSERT~\{~K~:~V~\}~to~D

        \State~INSERT~[~K~:~V~]~to~D

        \State~PUSH~X~to~D

    \caption{dict store A B C D}

    \end{algorithmic}

\begin{algorithm}[H]

    \begin{algorithmic}

        \State~PACK~~A~as~X

        \State~POP~~B~as~Y

        \State~POP~~C~as~Z

        \State~obtain~value~stored~under~the~key~Z

        \State~UNPACK~Y[~~Z~]~to~A

        \State~store~the~dictionary~Y~without~the~key~Z

        \State~PUSH~~Y[~~-Z~]~to~D

        \State~PUSH~X~~to~E

        \State~PACK~A~as~X

        \State~POP~B~as~Y

        \State~POP~C~as~K

        \State~[~V,~F~]~$\gets$~OBTAIN~K~from~Y

        \State~UNPACK~V~to~A

        \State~PUSH~F~to~D

        \State~PUSH~X~to~E

    \caption{dict fetch A B C D E}

    \end{algorithmic}

\label{alg:dict_fetch}

Finally, formal definitions of an evaluation step and an evaluation of a Cthulhu program are as follows:

\begin{theorem}

    Assume a set of all states $\Psi$ from definition 5. An evaluation step of a Cthulhu program

    is a binary relation $\vdash$ on the set $\Psi \times \Psi$.

    Assume a set of all states $\Psi$ from definition five and a program $\mathcal{P}$.

    Let $\mathcal{I}$ be a set of all instructions used in $\mathcal{P}$.

    An evaluation step of a Cthulhu program is a binary relation $\vdash$ on the set $\Psi \times \Psi$.

    Two states $\mu$ and $\pi$ are in relation $\Psi$, if there is an instruction in set $\mathcal{I}$

    such that execution of the instruction in state $\mu$ transforms the state of the Cthulhu machine

    to state $\pi$.

\end{theorem}

\begin{theorem}

\end{theorem}

\section{Substitution}

\subsection{Implementation}

The idea behind the substitution algorithm is to iterate the instruction sequence until

As stated before, programmers can define their own structures based on predefined

structures. These user-defined structures are referred to as \textit{logical structures}.

Besides the definition of the structure and its operations, users need to provide the

substitution from the logical structure to its implementation. This section provides

the description of substitution algorithm used in the Cthulhu and shows how to define

substitutions for logical structures.

\subsection{Substitution algorithm}

The idea behind the substitution algorithm is to iterate the input instruction sequence until

all logical structures are substituted for their implementations. It is important to note

that even logical structures may use other logical structures. As a result, the

that logical structure definition may use other logical structures. As a result, the

replacement process continues until a complete iteration occurs without further substitutions.

The pseudocode for substitution algorithm is shown in the following figure:

The pseudocode for substitution algorithm is as follows:

\begin{algorithm}[H]

\textbf{Input: }{Sequence of instructions loaded from the source file.} \\

\begin{algorithmic}

\State$\mathcal{L} \gets set~of~all~logical~structures$

\State$\mathcal{S} \gets \{seq,~bv_8,~bv_{16},~bv_{32},~dict\}$

\State~Iterate~the~instruction~sequence~until~the~first~iteration

\State~occurs~in~which~no~substitution~is~performed.

\State Iterate~the~instruction~sequence~until~the~first~iteration

\State occurs~in~which~no~substitution~is~performed.

\caption{Substitution procedure}

\end{algorithmic}

\label{alg:subst}

\end{algorithm}

\paragraph{Termination}

Let's analyze the termination of the algorithm. Firstly, it is important to recognize

that the input sequence of instructions is finite, containing a definite number of

logical structures. In each iteration of the inner while loop, the entire program is traversed.

Despite the potential for expansion due to substitution, currently substituted instructions

are skipped, ensuring that termination is guaranteed for the inner while loop.

Regarding the outer while loop, termination occurs when an iteration is reached where no

instruction undergoes substitution. This outcome is assured due to the prohibition of

recursively defined logical structures. Therefore, every substituted program exclusively

employs logical structures that do not use the presently substituted structure within

their definitions.

The substitution procedure accepts a finite instruction sequence containing a defined number

of logical structures as input. In each iteration, the procedure substitutes every logical structure

for its implementation. Since the set of logical structures is finite, and recursive definitions

are undefined after a certain number of iterations, all of the logical structures will be

substituted, and the instruction sequence will only contain predefined structures, as described

in section 2.3.

\paragraph{Corectness}