## 5 Hierarchical Blockchain Model
### Block Structure and Data Abstraction
#### 5.1.2. Blockchain in String Abstract Domain  
In this section, we present abstract domains for string data. Although various abstract domains exist, let us recall from [42] two among them: \"Prefix and Suffix\" and \"Bricks\". Given an alphabet \(\Sigma\) consisting of characters, a string is a sequence (possibly infinite) of elements in \(\Sigma\). Let us consider S=\(\Sigma^{*}\), which is the set of all possible strings of any length (possibly infinite) generated from \(\Sigma\). Formally, the concrete string domain is represented in the form of the lattice: \(\mathsf{L}_{\mathsf{c}}\)= \(\langle\wp(S),\Xi,\emptyset,S,\cup,\cap\rangle\). Prefix and Suffix Abstract Domain  
A prefix \(x\) is an abstraction of a set of strings (including the string \(x\) itself) which begin with \(x\) followed by other characters. Formally, the prefix abstract domain is represented by the abstract lattice \(\mathsf{L}_{\bar{A}}\)=\(\langle\bar{A},\Xi,\bot,\top,\sqcup,\sqcap\rangle\) where \(\bar{A}=\Sigma^{*}\cup\{\bot\}\). Given two prefixes \(\overline{x},\overline{y}\in\bar{A}\), the partial order \(\sqsubseteq\) is defined as:  
\[\overline{x}\sqsubseteq\overline{y}\quad\text{iff }\quad len(\overline{x}) \geq len(\overline{y})\wedge\forall i\in[0,len(\overline{y})-1]:\overline{x}[ i]=\overline{y}[i]\]  
Figure 8: Abstract Block in Interval Domain. Figure 7: Galois connection between \(\mathsf{L}_{\mathsf{c}}\) and \(\mathsf{L}_{\bar{I}}\). where \(len(a)\) returns the number of characters in '\(a\)'. In other words, \(\overline{y}\) is greater than \(\overline{x}\) iff \(\overline{y}\) is the prefix of \(\overline{x}\). Observe that the top element \(\top\) in \(\mathbb{A}\) is the empty prefix \(\epsilon\). The meet operation \(\sqcap\) and join operation \(\sqcup\) in is defined as:  
\[\sqcap(\overline{x_{1}},\overline{x_{2}}) =\left\{ \begin{array}{ll}\overline{x_{1}}&\text{if }\overline{x_{1}}\sqsubseteq \overline{x_{2}}\\ \overline{x_{2}}&\text{if }\overline{x_{2}}\sqsubseteq\overline{x_{1}}\\ \bot&\text{Otherwise}\end{array} \right.\] \[\sqcup(\overline{x_{1}},\overline{x_{2}}) =\left\{ \begin{array}{ll}\overline{x_{1}}&\text{if }\overline{x_{2}}\sqsubseteq \overline{x_{1}}\\ \overline{x_{2}}&\text{if }\overline{x_{1}}\sqsubseteq\overline{x_{2}}\\ \top&\text{Otherwise}\end{array} \right.\]  
Therefore, the Galois connection between \(\mathsf{L}_{c}\) and \(\mathsf{L}_{\mathbb{A}}\) is established as \(\langle\mathsf{L}_{c},\alpha_{\mathbb{A}},\gamma_{\mathbb{A}},\mathsf{L}_{ \mathbb{A}}\rangle\), where  
and  
\[\forall\overline{v}\in\mathbb{A}:\ \ \gamma_{\mathbb{A}}(\overline{v})=\{s\in S \ |\ prefix(s)=\overline{v}\}\]  
The suffix domain is constructed in the similar way. Given a concrete block, its corresponding abstract version in the prefix domain is depicted in Figure 9.  
Bricks abstract domain [42] is defined with an aim to capture both inclusion and order amongst characters, using regular expressions [43]. A brick is defined as an element of the form \(\overline{B}=[X]^{min,max}\) where \(X\in\wp(S)\). Both \(min\) and \(max\) are positive integer values which represent that all strings are built by combining (in order) the strings in \(X\) taking each of them between \(min\) and \(max\) times altogether. For example, [_(\"so\", \"\(le\)\")_]_1,2 = \(\{so\), \(le\), \(so\), \(lele\), \(so\), \(leso\)}. In bricks abstract domain, a set of strings is approximated by a combination of bricks. For example, [[\"manage\"]]_0,1 [[\"ment\"]]_1,1 = [ment, management], where [[\"manage\"]]_0,1 concretizes to [\(e\), \"manage\"] and [[\"ment\"]]_1,1 concretizes to [\"ment\"]. Formally, the abstract domain of bricks is defined as: \(\overline{BR}=\overline{B}\); that is, the set of all finite sequences of bricks. The abstract partial order in bricks domain is \(\langle\overline{BR},\sqsubseteq,\bot,\top,\sqcap,\sqcup\rangle\).