# Design of Distributed Reconfigurable Robotics Systems with ReconROS

Christian Lienen<EMAIL_ADDRESS>1234-5678-9012 and  Marco Platzner
<EMAIL_ADDRESS>Paderborn University, Computer Science DepartmentWarburger
Str. 100PaderbornGermany33098<EMAIL_ADDRESS>
(2021)

###### Abstract.

Robotics applications process large amounts of data in real-time and require
compute platforms that provide high performance and energy-efficiency. FPGAs
are well-suited for many of these applications, but there is a reluctance in
the robotics community to use hardware acceleration due to increased design
complexity and a lack of consistent programming models across the
software/hardware boundary. In this paper we present ReconROS, a framework
that integrates the widely-used robot operating system (ROS) with ReconOS,
which features multithreaded programming of hardware and software threads for
reconfigurable computers. This unique combination gives ROS2 developers the
flexibility to transparently accelerate parts of their robotics applications
in hardware. We elaborate on the architecture and the design flow for ReconROS
and report on a set of experiments that underline the feasibility and
flexibility of our approach.

robot operating system (ROS), FPGA acceleration, robotics

††copyright: acmcopyright††journalyear: 2021††doi:
00.0000/0000000.0000000††journal: JACM††journalvolume: 00††journalnumber:
0††article: 000††publicationmonth: 1††ccs: Computer systems organization
Embedded and cyber-physical systems††ccs: Computer systems organization
Architectures††ccs: Computer systems organization Robotics

##  1\. Introduction

Robotics systems are often distributed and can involve challenging
computational tasks. Resource-efficiency is a fundamental challenge of such
systems since large amounts of data must be processed with soft or even hard
real-time constraints (Yanmaz et al., 2018). Compared to implementations on
CPUs and GPUs, FPGAs have been shown to offer higher performance and higher
energy-efficiency for many of the involved tasks, e.g., for vision kernels
(Qasaimeh et al., 2019), for morphological image processing functions (Brugger
et al., 2015), for feature detection and description algorithms (Ulusel et
al., 2016), and for convolutional neural network inference (Venieris and
Bouganis, 2019). However, despite the demonstrated advantages of FPGAs, their
proliferation into the robotics domain is still limited for several reasons.
On one hand, FPGA design and, all the more, software/hardware co-design are
arguably more challenging than embedded software development. On the other
hand, robotics engineers and application developers are typically not trained
in FPGA circuit or hardware/software co-design.

High level synthesis (HLS) tools are available today that accept standard
C/C++ for describing behavior and (semi-)automatically take such descriptions
to FPGA hardware. Although HLS tools increase productivity and are thus highly
useful, a consistent programming model for implementing software and hardware
functions is still lacking. Porting a robotics application from software to
hardware or accelerating parts of the application in hardware requires the
creation of suitable interfaces between software and FPGA hardware and very
often leads to a re-development of substantial parts of the application.

The distributedness of typical robotics systems that is caused by the spatial
placement of sensors and actors and the demand for increased computational
capacity or robustness, also poses challenges for hardware acceleration. There
have been approaches for including reconfigurable hardware into distributed
embedded systems, for example ReCoNets (Haubelt et al., 2003), but these
approaches are not compatible with existing and widely-used software
abstractions for creating distributed robotics systems.

In our work, we take up a very popular programming environment in the robotics
domain, the robot operating system (ROS). ROS is a middleware layer that
models applications as set of communicating nodes and provides several
communication mechanisms for information exchange.

In this paper, which is an extension of our previous conference publication
(Lienen et al., 2020), we present the open source project ReconROS as a novel
integration of ROS with ReconOS (Agne et al., 2014).

ReconOS provides an architecture and programming model to enable shared memory
multi-threading for software and hardware threads. As a result, ReconROS
allows robotics developers to utilize hardware acceleration for ROS
applications either as hardware-accelerated ROS nodes or as ROS nodes mapped
completely to hardware. The latter option provides a consistent programming
model for ROS applications, independently of the mapping of ROS nodes to
software or hardware.

The remainder of the paper is organized as follows: Section 2 provides an
overview over ROS and related approaches for integrating hardware accelerators
into ROS. Section 3 elaborates on different approaches for accelerating ROS
applications, before Section 4 details ReconROS with its architecture and
design flow. In Section 5, we present experiments to quantify overheads
involved when mapping ROS nodes to hardware and to demonstrate the feasibility
and flexibility of ReconROS. Finally, Section 6 concludes the paper and gives
an outlook to future work.

##  2\. Background and Related Work

In this section, we first briefly introduce the robot operating system (ROS)
and then analyze and compare related approaches for integrating FPGA hardware
acceleration into ROS.

###  2.1. The Robot Operating System (ROS)

The Robot Operating System (ROS)111https://www.ros.org is an open source
middleware on top of Linux for robotics applications that was originally
developed by William Garage and is now coordinated by the Open Robotic
Foundation. ROS comprises a multitude of libraries and an infrastructure for
building and reusing robot-related software modules. The ROS programming
paradigm splits larger software architectures into nodes, which use certain
communication mechanisms for information exchange.

The decomposition into nodes promises code reusability and modularity for
robot architectures. Available communication mechanisms comprise (i) a many-
to-many publish/subscribe model, which allows to broadcast messages to
multiple subscribers but is one-way, (ii) services that follow a client-server
model where the server provides data only if requested by the client,
basically mimicking a remote procedure call, and (iii) actions.

Actions is the most elaborated communication mechanism where a client inquires
about a functionality at a server, starts the functionality if it is
available, and then receives regular feedback about the server’s progress.
Technically, actions are implemented in two phases. The first phase
corresponds to a ROS service and the second phase comprises a second ROS
service and a feedback channel using the ROS publish/subscribe mechanism.

ROS2 is the latest release of ROS. In earlier versions only one ROS node per
Linux process was supported. This prevented the use of shared memory
communication when both ROS nodes are mapped to the same compute node. While
this limitation was mitigated through the support of so-called nodelets, with
ROS2 multiple ROS nodes can natively run within one Linux process and there is
support for shared memory communication. ROS2 is built on top of an
exchangeable communication layer, the data distribution service (DDS). DDS is
an industry standard for decentralized communication and available from
different vendors. Compared to older ROS versions, the use of DDS provides
better configurability and improves properties such as scalability,
reliability and durability (Maruyama et al., 2016).

Another important element of ROS are ROS messages, which are multi-layered
combinations of built-in data types such as integers, floats and strings.
Besides predefined message types, e.g., for images or 3D point clouds, custom
messages can be created. Since the length of a message might vary during
runtime, the ROS2 middleware supports dynamic memory allocation for messages.

###  2.2. Related Approaches for ROS-FPGA Integration

In the last years, a few approaches have been presented that integrate
reconfigurable hardware accelerators into a ROS software architecture.
Yamashina et al. (Yamashina et al., 2015) proposed so-called ROS-compliant
FPGA components. A ROS node is implemented in software and accesses the
hardware component, i.e., the accelerator, via a software wrapper.
Communication within the ROS network is completely handled in software and,
whenever acceleration is needed, only the payload of the ROS message is
transmitted to the hardware component. Semantically, the communication between
the ROS software wrapper and the hardware accelerator is a remote procedure
call, realized in Xilinux. In (Yamashina et al., 2016), the automated design
tool cReComp (creator for reconfigurable component) is presented to help
generate ROS-compliant FPGA components and thus reduce development costs. For
the implementation of a ROS-compliant FPGA component with cReComp, the
developer has to modify a configuration file and create user logic for the
hardware accelerator. The configuration file contains information about the
interface between the processing system and the programmable logic. cReComp
generates the software and hardware parts for this interface. An evaluation by
a group of test developers confirmed higher design productivity compared to
manually designed interfaces.

In follow-up work, Sugata et al. (Sugata et al., 2017) identify the
communication times between ROS nodes as bottlenecks and aim to reduce these
times through implementing the ROS publish/subscribe messaging in hardware. In
their system, communication is divided into two phases: the connection
establish phase, which is supported by software, and the data communication
phase that is realized by two network stacks implemented in FPGA hardware.
This reduces the communication time between nodes by 50 percent.

Ohkawa et al. (Ohkawa et al., 2019) extend this work by using high level
synthesis (HLS) for accelerator implementation and ROS protocol interpretation
to increase productivity. Their approach takes the ROS message definition, the
ROS node configuration, and behavioral code written in C/C++ for the
accelerator and generates the FPGA design. The infrastructure of the generated
design includes several components: the hardwired TCP/IP stacks for the data
communication phase, a data conversion between ROS messages and the
application, an interface between the data conversion and the application,
and, finally, the application itself.

Leal et al. (Leal et al., 2020) present Forest, an approach for combining the
more recent release ROS2 with hardware acceleration. Forest uses configuration
files to specify so-called ROS2-FPGA nodes, which are a composition of a ROS2
software node, an HLS-coded FPGA hardware module, and a PYNQ driver for the
interaction between the ROS2 software node and the hardware module.

While (Sugata et al., 2017; Ohkawa et al., 2019) migrate almost a complete ROS
node to hardware, Podlubne and Göhringer (Podlubne and Göhringer, 2019) go one
step further and propose a methodology for full-hardware implementation of a
number of ROS nodes. Their hardware designs comprise four parts: the ROS
application nodes that use publish/subscribe communication, a so-called
application-to-ROS converter, a communication interface, and a manager.
Basically, the application-to-ROS converter serializes the ROS-based IP
traffic on an AXI bus, the communication interface handles the AXI messages
and sends them to a TCP/IP stack to connect to external ROS nodes, and the
manager coordinates the communication between the ROS nodes and the TCP/IP
stack. Conceptually, the application-to-ROS converter must reside in hardware,
but the communication interface and the manger could also be mapped to the
processing system of the platform FPGA. However, the main feature of this
methodology is the option to implement one or more ROS nodes fully in hardware
and map them to reconfigurable logic without the need of using a processor.
Likewise, any application implemented in reconfigurable hardware can be made
ROS-compatible. Furthermore, the presented implementation can use dynamic
custom ROS messages.

Strohmer et al. (Strohmer et al., 2019) presented a ROS-enabled hardware
framework for experimental robotics. They use the programmable logic on a
Xilinx Zynq-7000 for signal conditioning and partition the available CPU cores
into a non real-time part running Linux with ROS and a real-time part running
control algorithms. A distributed network of FPGAs can extend the signal
conditioning part using TosNet, which provides memory access across multiple
nodes by memory mirroring.

Eisoldt et al. (Eisoldt et al., 2021) contributed ReconfROS, a framework for
ROS hardware acceleration based on shared-memory communication. The
architecture on the system-on-chip comprises a software part including a ROS
node, a shared memory area, and one or more processing blocks in the
programmable logic. The software-mapped ROS node subscribes to topics and
writes received messages into the shared memory area, from where the data can
be accessed by the hardware processing blocks. Finally, the software-mapped
ROS node publishes the resulting data. The control of the processing blocks is
done via control registers which are mapped into the virtual address space of
the software application.

##  3\. Design Considerations

The goal of this work is to provide developers of ROS2-based robotics
applications with a flexible means to utilize programmable logic for hardware
acceleration. On the level of ROS2 applications, there are several schemes for
such an integration, which are sketched in Figure 1. Figure 1(a) shows a
scheme where some parts of a ROS2 node, typically runtime-consuming functions,
are mapped to one or several accelerators in programmable logic. The semantics
of the communication between the ROS2 node and the accelerators is that of a
remote procedure call (RPC). In Figure 1(b), a hardware accelerator is shared
between several ROS2 nodes. Communication semantics is still RPC, but the
implementation is more involved since proper arbitration between the accesses
of the ROS2 nodes is required. The third scheme shown in Figure 1(c) is the
most advanced and allows to map complete ROS2 nodes to hardware. Essentially,
the hardware accelerator is turned into a ROS2 node. In this scheme, all ROS2
nodes can communicate via the ROS2 communication mechanisms, independently of
their mapping to software or hardware. Semantically, this is the most
intriguing scheme since it provides a consistent programming model across
hardware and software where all ROS2 nodes use exactly the same ROS2
functions.

Figure 1. Different schemes for integrating ROS2 node with hardware
accelerators

Often, developers decide to attach interfaces to sensors and actuators
directly to the reconfigurable hardware and provide peripheral cores in
hardware to access them rather than putting them under operating system
control on the host CPU. Figure 1(d) and Figure 1(e) sketch such schemes with
dashed lines. While these schemes are popular for maximizing performance in
concrete robotics applications, there are also two possible pitfalls:

First, flexibility is reduced since directly connected peripherals can not be
accessed by other ROS2 nodes, and much less so when the ROS2 nodes are mapped
to different compute nodes in a distributed system. Second, many sensors and
actors come with standardized interfaces and corresponding drivers, e.g., USB,
for which the use of an existing, software-accessible peripheral of the
compute platform is much more productive than to implement suitable interfaces
and protocol stacks in hardware.

Along the same line, the scheme shown in Figure 1(f) directly connects several
ROS2 nodes mapped to hardware without relying on ROS2 communication
mechanisms. This can increase performance in particular cases, but again lacks
flexibility since the mapping of the ROS2 nodes is severely constrained.

ReconROS222https://github.com/Lien182/ReconROS integrates the ROS2 middleware
with the ReconOS/Linux architecture and programming model for
hardware/software multithreading on platform FPGAs and can realize all schemes
shown in Figure 1(a)-(f) and their combinations. On one hand, ReconOS enables
us to develop applications as a set of software and hardware threads under the
shared memory model. On the other hand, ROS2 allows for declaring several ROS2
nodes within one Linux process. Therefore, in the schemes shown in Figure
1(a)(b)(d) each hardware accelerator is encapsulated by a ReconOS hardware
thread. In contrast to most of related work, ReconROS hardware accelerators
can communicate with the ROS2 software nodes not only by passing data in an
RPC manner, but can also use shared memory communication in the Linux virtual
address space, which is more efficient when larger data structures have to be
passed. In such a case, pointers to arbitrarily large ROS2 messages are passed
and the accelerators themselves retrieve the relevant message payload from
shared memory. Furthermore, since ReconOS hardware threads can execute
standard operating system synchronization primitives, the required arbitration
for the scheme in Figure 1(b) is straight-forward to realize.

In the more advanced schemes shown in Figure 1(c)(e)(f), ReconOS hardware
threads implement complete ROS2 nodes and allow them to access operating
system functions and also ROS2 communication primitives, using the whole set
of standard and even custom-defined ROS messages.

Table 1 compares ReconROS with related approaches. In contrast to all other
approaches except for (Leal et al., 2020), ReconROS leverages the more future-
oriented ROS2 version which promises improved scalability and real-time
properties. Hardware acceleration of a ROS node mostly implies to partition
the node and implement it as hardware/software co-design. This is followed by
all approaches except (Podlubne and Göhringer, 2019). Mapping several ROS
nodes to hardware is possible in (Eisoldt et al., 2021) and ReconROS. Full
memory access for hardware accelerators and arbitrarily long ROS messages are
featured by (Eisoldt et al., 2021) and ReconROS. A consistent
hardware/software programming model and the support of all available ROS2
communication paradigms are unique features of ReconROS.

Characteristic |  (Yamashina et al., 2015),(Yamashina et al., 2016), (Sugata et al., 2017),(Ohkawa et al., 2019) | (Podlubne and Göhringer, 2019) | (Strohmer et al., 2019) | (Eisoldt et al., 2021) | (Leal et al., 2020) |  ReconROS
---|---|---|---|---|---|---
ROS version | 1 | 1 | 1 | 1 | 2 | 2
Support of hardware/software co-designed ROS nodes | ✓ | ✗ | ✓ | ✓ | ✓ | ✓
Multiple ROS nodes per FPGA | ✗ | ✓ | ✗ | ✗ | ✗ | ✓
Consistent hardware/software programming model | ✗ | ✗ | ✗ | ✗ | ✗ | ✓
Memory access for hardware accelerators | ✗ | ✗ | ✗ | ✓ | ✗ | ✓
Support of arbitrarily long ROS messages | ✗ | ✗ | ✗ | ✓ | ✗ | ✓
Support of ROS services and actions | ✗ | ✗ | ✗ | ✗ | ✗ | ✓
Table 1. Comparison of approaches for integrating hardware accelerators with
ROS

##  4\. ReconROS

In this section, we present the architecture of ReconROS, followed by the
design flow and an example that shows the programming interface.

Figure 2. ReconROS architecture with two hardware ROS2 nodes (threads) and
several software ROS2 nodes (threads)

###  4.1. Hardware/Software Architecture

ReconROS inherits most of its hardware architecture from the underlying
ReconOS (Agne et al., 2014; Lübbers and Platzner, 2009). Figure 2 shows an
example architecture with two hardware ROS2 nodes (threads) and several
software ROS2 nodes (threads). The hardware threads are mapped to
reconfigurable slots and are connected to the Linux operating system kernel
running on the CPU via the operating system interface (OSIF) and to shared
memory via the memory interface (MEMIF). A so-called operating system finite
state machine (OSFSM) is attached to each hardware thread to serialize the
thread’s operating system interactions. On the CPU, the communication with the
OSIF is handled by a ReconROS driver and by light-weight delegate threads that
serve the operating system calls for the hardware threads. The memory
subsystem enables the hardware threads to access the whole address space of
the ReconROS application, including shared memory and memory-mapped
peripherals. ReconOS supports virtual memory and therefore includes an MMU in
its memory subsystem.

ReconROS object | ROS2 equivalent | Description
---|---|---
rosnode | node |  | Represents a ROS2 node (software or hardware)
---
in the ReonROS Stack
rosmsg | message |  | Message type for communication mechanisms
---
publish/subscribe, service, or action
rossub | subscriber |  | Enables a rosnode to subscribe to a topic
---
using a specific rosmsg
rospub | publisher |  | Enables a rosnode to publish to a topic
---
using a specific rosmsg
rossrvs / rossrvc | service server / client |  | Extends a rosnode by the capability to act as
---
server or client for ROS2 services
rosacts / rosactc | action server / client |  | Extends a rosnode by the capability to act as
---
server or client for ROS2 actions
Table 2. Objects of the ReconROS stack

To realize ReconROS, we have developed two additional components, (i) the
ReconROS stack and (ii) the ReconROS API for software and hardware threads.
The ReconROS stack extends the existing set of ReconOS objects such as
semaphores or mailboxes with ROS2-related objects. Table 2 lists the objects
of the ReconROS stack. ROS2 nodes mapped to either software or hardware can
create these objects and call corresponding methods in exactly the same way.

The ReconROS API abstracts the standard ROS2 API and allows ReconOS threads to
access the objects of the ReconROS stack. As indicated in Figure 2, the
ReconROS API is available for both software and hardware threads. While due to
the flexibility of the underlying ReconOS system any ROS2 function can be made
available for hardware threads, the current set of provided functions dealing
with the objects listed in Table 2 is sufficient to implement ROS2 hardware
nodes that receive data, process it, and send it back. In particular, ROS2
hardware nodes can publish and subscribe to topics and assume both server and
client roles in ROS2 services and actions. Software threads can not only
access the ReconROS API but also the standard ROS2 API to utilize a richer set
of functions.

In contrast to most of related work, our ROS2 hardware nodes can access shared
memory and thus implement a more efficient ROS message handling. When hardware
threads access functions of the ReconROS API, e.g., for subscribing or
publishing to topics, the OSIF and the delegate thread mechanism are used to
pass pointers between the ReconROS stack in software and the hardware threads
to allow them to access the ROS message data structures in memory through
their MEMIFs. Compared to message communication via the OSIF, which
corresponds roughly to the mechanism used in most of related work, this design
decision brings about two advantages: First, the MEMIF interface provides
higher data rates due to the used AXI high performance interface of the
processing system. Second, the transmission of the data can be done without
using the processing system, which leads to more potential for parallel
execution of software and hardware threads.

Figure 3 exemplifies the sequence of events when a hardware ROS2 node
initiates the function ROS_SUBSCRIBER_TAKE from the ReconROS API 1. The
function call of the hardware thread includes the command for this API
function and a reference to the subscriber. The command is transmitted by the
OSFSM and unblocks the corresponding delegate thread on the CPU. The delegate
then executes the ROS2 subscriber take function rcl_take on behalf of the
hardware thread 2. When a message for the subscribed topic becomes available,
the ReconROS stack stores it in main memory 3 and unblocks the delegate thread
4, which in turn sends the message pointer via the OSIF back to the hardware
thread 5. Subsequently, the hardware thread can read the message via its MEMIF
6.

Publishing a message from a hardware thread works analogously: First, the
hardware threads stores the message in the main memory. Then, it sends a
ROS_publish command and the message pointer via the OSIF interface to its
delegate thread, which executes the command.

Figure 3. Sequence of events when a ROS2 hardware node calls the
ROS_SUBSCRIBER_TAKE function from the ReconROS API

The ReconROS mechanism described in Figure 3 also supports the implementation
of ROS2 services and actions. ROS2 services comprise the receiving and sending
of a single message, while the more involved ROS2 actions combine two ROS2
services with a publish/subscribe feedback channel.

###  4.2. Design Flow

The design flow for a ReconROS application adapts the original ReconOS design
flow (Agne et al., 2014) and is sketched in Figure 4. The flow starts with the
specification of a ReconROS project comprising a project configuration file,
the sources for software and hardware threads that represent the ROS2 nodes,
and the definition of message types used for the application.

The configuration file specifies the used ROS2 objects with their
dependencies, the ReconOS architecture including, in particular, the number of
reconfigurable slots and the mapping of hardware threads to reconfigurable
slots, and the settings for the build tool flow.

The basic element of each ReconROS application is the rosnode object, which
represents a ROS2 node in the network. A rosnode object can be extended by one
or more communication objects, which can be subscriber (rossub) or publisher
(rospub) objects for specific topics in case of publish/subscribe
communication, service (rossrvs / rossrvc) objects for client-server
communications, and action (rosacts / rosactc) objects for ROS2 actions. In
addition, each of these extensions, i.e., publisher, subscriber, service, and
action, requires a reference to an instance of a ROS message rosmsg of a
specific type. Declarations of rosmsg objects include the communication type,
a group, and the message type. For example, a specific message declaration
could specific ’Image’ as message type, ’sensor_msgs’ as group, and
publish/subscribe as communication type.

Threads for ROS2 software nodes can be developed in C and threads for ROS2
hardware nodes in C/C++ for use with high-level synthesis or, alternatively in
VHDL. Importantly, we provide the same ReconROS API for software and hardware
threads which greatly simplifies the creation of hardware-accelerated versions
of software threads.

Based on the configuration file and the sources, the ReconOS development kit
(rdk) creates the ReconROS binaries for the specific project.

The rdk command export_msg extracts information from the message package
definition and creates a Colcon project, which is then compiled to the message
package by the command build_msg. Colcon is a ROS2 build tool, and the message
package comprises message-related data and scripts that are used by the ROS2
runtime. The rdk command export_sw creates the software project based on the
sources for software threads and configuration data. The software project also
includes the ReconOS delegate threads, all necessary initialization functions
for the ReconOS primitives, and the ROS2 middleware dependencies. Moreover,
the software project includes header definitions for the messages, which are
part of the compiled message package. The binaries for the ARM architecture
are then created by the rdk command build_sw.

Both commands, build_sw and build_msg employ an ARM-32 docker container
emulated with Qemu to build the binaries. Compared to a standard cross-
compilation tool chain for the embedded ARM cores, our setup greatly
simplifies the ROS2 build step with all its dependencies since the package
manager within the container can be used.

Finally, the rdk command export_hw creates the hardware project based on the
sources for hardware threads and configuration data. The hardware project
contains the complete ReconROS architecture with its OSIFs, MEMIFs, and
supporting modules. The command calls Xilinx Vivado HLS for high-level
synthesis and thus also requires the message header definitions. The FPGA
bitstream is then created by the rdk command build_hw.

Figure 4. ReconROS design flow

###  4.3. Example ROS2 Application

As an example we elaborate on a ROS2 application comprising four nodes, which
is shown in Figure 5. Node 1 captures images from a camera and publishes them
to the topic /image_raw. Node 2, the digital image processing node (DIP),
subscribes to this topic, offloads the processing of a Sobel image filter to
node 3, and publishes the filtered images to the topic /image_filtered. Node 4
reads and displays the filtered images. The data exchange between the DSP node
and the image processing node is done with a ROS2 service called
sobel_service. The ReconROS application comprises nodes 2 and 3, where both
are to be mapped to reconfigurable hardware and run either on a single or on
two FPGA platforms. Nodes 1 and 4 are assumed to be existing or being compiled
with appropriate ROS2 design flows to other target architectures, e.g.,
desktop PCs.

Figure 5. Example ROS2 application

Listing 1 shows the ROS2-related part of the configuration file for the nodes
2 and 3.

The information for the ROS2 nodes is organized into so-called resource
groups. Lines 1–4 specify node 3, beginning with the definition of a rosnode
object named ”Sobel” in line 2. In line 3, a message object of type ROS2
service message is defined with further references to a ROS2 message package
and the communication as well as service types. Line 4 declares a ROS2 server
object for a ROS2 service, connects it to the ROS2 node node_3 and the message
object filter_service_msg, assigns the name ”sobelservice” to it, and sets the
polling time for checking for new service requests to $10000\>\mu s$.

Lines 6–12 specify node 2, including the rosnode object named ”DIP”, the same
message object as used by node 2, and a client object for a ROS2 service.
Additionally, node 2 is extended with the message object image_msg of a ROS2
built-in message type and corresponding subscriber and publisher objects for
the topics /image_raw and /image_filtered.

Listing 1: Configuration file (ROS2-related part) for the ReconROS application
shown in Figure 5

⬇

1 [ResourceGroup(at)ResourceGroupSobel]

2 node_3 = rosnode, "Sobel"

3 filter_service_msg = rossrvmsg, application_msgs, srv, SobelSrv

4 filter_server = rossrvs, node_3, filter_service_msg, "sobelservice", 10000

5

6 [ResourceGroup(at)ResourceGroupDIP]

7 node_2 = rosnode, "DIP"

8 filter_service_msg = rossrvmsg, application_msgs, srv, SobelSrv

9 filter_client = rossrvc, node_2, filter_service_msg, "sobelservice", 10000

10 image_msg = rosmsg, sensor_msgs, msg, Image

11 sub = rossub, node_2, image_msg, "/image_raw", 10000

12 pub = rospub, node_2, image_msg, "/image_filtered"

Listing 2 presents C/C++ code for the HLS-implementation of the ”Sobel” ROS2
node. Using the ReconROS API, the processing loop starts in line 3 with a
blocking read for a new service request. When a request becomes available, the
function ROS_SERVICESERVER_TAKE returns a pointer to the service request data
structure. With the help of the OFFSETOF macro, line 4 determines another
pointer to the address of the request’s payload. The macro MEM_READ is
employed to first read the address of the image in line 7 and then to read the
image into a ram structure within the FPGA in line 8. After a Sobel filter
function is executed on the image in line 10, the result is written back to
main memory via the MEM_WRITE macro. Finally, the node sends the filtered data
back to the node requesting the filter service.
(ROS_SERVICESERVER_SEND_RESPONSE).

Listing 2: C/C++ code (partial) for the HLS implementation of the ”Sobel” ROS2
node

⬇

1 while(1) {

2 // Wait for service request and get pointer to payload

3 pMsg = ROS_SERVICESERVER_TAKE(resourcedip_srv, resourcedip_filter_srv_req);

4 pMsg += OFFSETOF(application_msgs__srv__SobelSrv_Request, img.data.data);

5

6 // Get pointer to image in memory and copy it to FPGA-internal memory

7 MEM_READ(pMsg, pPayloadService, 4);

8 MEM_READ(pPayloadService[0], ram, IMAGE_SIZE * 4);

9

10 SobelFilter(ram);

11

12 // Write filtered image back to memory and send service response

13 MEM_WRITE(ram, pPayloadService[0], IMAGE_SIZE * 4);

14 ROS_SERVICESERVER_SEND_RESPONSE(resourcedip_srv,
resourcedip_filter_srv_res);

15 }

Listing 3 displays a similar procedure for the ”DIP” node, which is expanded
with three communication objects, a subscriber object for the topic
/image_raw, a client object for the service /sobel_service, and a publisher
object for the topic /image_filtered.

Listing 3: C/C++ code (partial) for the HLS implementation of the ”DIP” ROS2
node

⬇

1 while(1) {

2 // Wait for published image and get pointer to payload

3 pMsg = ROS_SUBSCRIBER_TAKE(resourcesobel_subdata, resourcesobel_image_msg);

4 pMsg += OFFSETOF(sensor_msgs__msg__Image, data.data);

5

6 // Get pointer to image in memory and copy it to FPGA-internal memory

7 MEM_READ(pMsg, pPayloadPubSub, 4);

8 MEM_READ(pPayloadPubSub[0], ram, IMAGE_SIZE * 4);

9

10 // Request filter service, pServiceRequest is set up during initialization

11 MEM_WRITE(ram, pServiceRequest[0], IMAGE_SIZE * 4);

12
ROS_SERVICECLIENT_SEND_REQUEST(resourcesobel_srv,resourcesobel_filter_srv_req);

13

14 // Wait for service response and get pointer to payload

15 pMsg = ROS_SERVICECLIENT_TAKE(resourcesobel_srv,
resourcesobel_filter_srv_res);

16 pMsg += OFFSETOF(application_msgs__srv__SobelSrv_Response, img.data.data);

17

18 // Get pointer to payload and copy it to FPGA-internal memory

19 MEM_READ(pMsg, pPayloadService, 4);

20 MEM_READ(pPayloadService[0], ram, IMAGE_SIZE * 4);

21

22 // Write filtered image back to memory and publish it

23 MEM_WRITE(ram, pPayloadPubSub[0], IMAGE_SIZE * 4);

24 ROS_PUBLISHER_PUBLISH(resourcesobel_pubdata, resourcesobel_image_msg);

25 }

##  5\. Evaluation

In this section, we first describe experiments to quantify the overheads
involved for mapping ROS2 nodes to hardware, followed by a distributed
mechatronics application example that demonstrates the feasibility and
flexibility of ReconROS.

Figure 6. ReconROS ping-pong application

###  5.1. ROS2 Hardware Node Overheads and Communication Times

To characterize runtime overheads when mapping ROS2 nodes to hardware instead
of software, and contrasting them to communication times within a ROS2
network, we have first

implemented a ping-pong ReconROS application with two ROS2 nodes distributed
onto a desktop PC and a Mini-ITX 7Z100 board containing a Xilinx Zynq-7100
platform FPGA, connected via Gigabit Ethernet as shown in Figure 6. The
platform FPGA runs Ubuntu 18.04 and ReconROS based on ROS2 dashing. All ROS2
nodes use the same C/C++ source for software and hardware implementations.
Software implementations have been compiled with optimizations level O3, and
hardware implementations have been created with HLS without any optimizations.
The ROS2 node on the PC publishes messages to the topic T:/send. The ROS2 node
on the Zynq subscribes to this topic, creates copies of received messages in
local memory, and publishes them to the topic T:/recv.

Table 3 presents the runtimes for these copy tasks in software and hardware,
$t_{copy-SW}$ and $t_{copy-HW}$, and the resulting speedup $S_{copy}$, as well
as the runtimes for the overall ping-pong application measured as roundtrip
time $t_{round}=t_{end}-t_{start}$ at the PC and the resulting speedup
$S_{round}$ for different message sizes. Since the underlying ReconOS
implementation has a lower memory bandwidth compared to the Zynq’s ARM
processor subsystem and there is additional hardware-software signaling
required, we observe a slowdown for the hardware ROS2 copy node, which is
distinct for larger message sizes. For example, copying a message of 6 MiB is
about $4\times$ slower in hardware than in software. While improving ReconOS’
memory subsystem would obviously reduce the slowdown, Table 3 also shows that
for the overall ping-pong application where we have to take communication into
account the slowdown is less pronounced with $1.15\times$ for a 6 MiB message.

Message size |  $t_{copy-SW}$ [ms] |  $t_{copy-HW}$ [ms] |  $S_{copy}$ |  $t_{round-SW}$ [ms] |  $t_{round-HW}$ [ms] |  $S_{round}$
---|---|---|---|---|---|---
4 Byte | 0.01 | 0.01 | 1.00 | 1.68 | 1.70 | 0.99
8 KiB | 0.03 | 0.12 | 0.15 | 11.39 | 11.47 | 0.99
1 MiB | 3.59 | 12.81 | 0.28 | 58.71 | 66.24 | 0.89
6 MiB | 18.91 | 76.35 | 0.25 | 381.44 | 438.02 | 0.87
Table 3. Runtimes of software and hardware ROS2 nodes and for the overall
ping-pong application, and corresponding speedups

The ReconROS communication times in Table 3 are in the same order as that of
related work (Sugata et al., 2017), where communication times were measured
between a ROS node on a PC and a ROS node on an ARM within a Zynq for messages
of size 1 MiB and 6 MiB, albeit on a different ROS version. Importantly, the
two versions of the ReconROS ping-pong application in Figure 6(a) and (b) are
semantically identical. Switching from one to the other simply requires a
change in the ReconROS configuration file and to start the software or
hardware ROS node, respectively, in the application’s main routine.

Generally, the overall ROS2 application speedup or slowdown, respectively,
achieved by moving individual ROS2 nodes from software to hardware depends on
i) the raw speedup of the ROS2 node, ii) the message size, iii) the overall
application’s topology and involved communication patterns and times, and iv)
the ratio between node computation times and communication times. The ROS2
nodes in the ping-pong application do not represent any computational load.
Hence, we have implemented the following four smaller applications on the
platform shown in Figure 6:

#### Inverse kinematics:

This application computes control signals for driving a servo motor that sets
a joint angle based on a desired position and orientation of a robotic
manipulation platform. The application is part of a larger mechatronic system
(Lienen, 2019) for controlling the movements of a Stewart platform (Stewart,
1965a) with six degrees of freedom. The computation involves coordinate
transformations and an iterative implementation of the $\arctan()$ function.
The ROS2 input message is an unsigned 32 Bit integer packed with two fixed-
point numbers in Q8.6 format that represent the desired rotation angles of the
platform around the x-axis and the y-axis. The ROS2 output messages is also a
32 Bit unsigned integer containing a 10 Bit unsigned integer which is the
pulse width coded control signal for the motor.

#### Number sorting:

This application sorts an array of 32 Bit unsigned integers based on the odd-
even transposition sort algorithm (Knuth, 1998). The algorithm is based on a
comparator network that employs $n$ stages with $n$ comparisons each to sort
$n$ numbers. The ROS2 node on the PC generates random numbers and publishes
messages comprising 2048 numbers as an array. The Zynq-based ROS2 node sorts
the data and sends it back.

#### Sobel filter:

This application implements a Sobel image filter (Gonzalez and Woods, 2018)
operating on three channels (RGB) of dimension $640\times 480$. The filter
applies two filter kernels on each channel of the image and calculates the
absolute value of the dot product as an approximation for the geometric mean.
The ROS2 input and output messages are of the type Image from the ROS2 sensor
message package.

#### MNIST classifier:

This application classifies handwritten digits from the MNIST dataset. The
classifier is implemented as a ROS2 service, which accepts input request
images of size $28\times 28$ as custom ROS2 messages and response the
estimated digit. The classifier consists of three convolution layers, three
pooling layers and two fully connected layers. The achieved accuracy is about
97%.

ReconROS application |  Slice LUTs |  DSP |  BRAM
---|---|---|---
Inverse kinematics | 4802 (1.73%) | 17 (0.84%) | 3 (0.40%)
Number sorting | 10396 (3.75%) | 0 (0.00%) | 2 (0.26%)
Sobel filter | 13625 (4.91%) | 0 (0.00%) | 10 (1.32%)
MNIST classifier | 26071 (9.40%) | 18 (0.89%) | 57.5 (7.62%)
Table 4. Resource usage and utilization (in % of the Xilinx Zynq 7100) for the
implemented ReconROS applications

Table 4 displays resource usage and FPGA utilization for the four
applications, and Table 5 the runtimes for the Zynq-bound ROS2 nodes, which
are either mapped to the ARM core ($t_{node-SW}$) or to reconfigurable logic
($t_{node-HW}$), the resulting raw speedup $S_{node}$, as well as the runtimes
for the overall application measured as roundtrip time
$t_{round}=t_{end}-t_{start}$ at the PC and the resulting speedup $S_{round}$.
The inverse kinematics application achieves a raw ROS2 node speedup of
$6.32\times$, the sobel filter and MNIST classifier also achieve raw speedups,
but the number sorting application does not benefit from hardware mapping. It
has to be noted that the goal of these experiments has been to evaluate the
overheads involved for ReconROS applications rather than achieving high
speedups through hardware acceleration. There is obviously a certain potential
to improve the raw speedups for the hardware-mapped ROS2 nodes, in particular
for the number sorting application where more parallelism can be exploited.
Depending on the relation between communication and computation times, the
speedups for the overall ROS2 applications are sometimes considerably lower
than the raw speedups, i.e., for inverse kinematics, sometimes slightly lower,
i.e., for the sobel filter and the MNIST classifier, and in the case of number
sorting even slightly higher.

ReconROS application |  $t_{node-SW}$ [ms] |  $t_{node-HW}$ [ms] |  $S_{node}$ |  $t_{round-SW}$ [ms] |  $t_{round-HW}$ [ms] |  $S_{round}$
---|---|---|---|---|---|---
Inverse kinematics | 1.20 | 0.19 | 6.32 | 7.70 | 6.64 | 1.16
Number sorting | 17.44 | 35.11 | 0.50 | 24.42 | 42.08 | 0.58
Sobel filter | 37.53 | 22.28 | 1.68 | 83.39 | 68.54 | 1.22
MNIST classifier | 88.03 | 30.74 | 2.86 | 98.58 | 41.25 | 2.39
Table 5. Runtimes of software and hardware ROS2 nodes and for the overall
applications, and corresponding speedups

###  5.2. Mechatronics Model

To showcase the suitability of ReconROS for distributed hardware-accelerated
ROS2 applications we present the mechatronics model (Lienen, 2019) shown in
Figure 7. The model comprises three ball-on-plate stations that are able to
balance a mechanical platform such that a ball thrown onto the platform does
not fall off. To this end we employ a Stewart platform (Stewart, 1965b) that
allows the system to move an object in six degrees of freedom, including
linear translations in $x$, $y$ and $z$ direction but also three rotations
(pitch, roll, and yaw). Stewart platforms are perfectly suitable for high
dynamic mechatronics applications such as flight simulators or telescopes. In
our setup, we drive six servo motors by pulse-width modulated signals to
adjust corresponding angles between the motor axes and the legs connecting to
the platform, which then results in the wanted movement. To capture the
position $(x,y)$ of the ball on the platform we use a resistive touchscreen
mounted on the surface of the platform.

Additionally, each ball-on-plate station is equipped with a monitor, and a
camera is capturing all stations.

The computing infrastructure includes three ZedBoards, as outlined in Figure
7. Each ZedBoard is equipped with a Xilinx Zynq-7020 platform FPGA and runs
Ubuntu 18.04 and ReconROS based on ROS2 dashing. The servo actors and
touchscreen sensors are connected to ZedBoard-Main, the camera is connected to
ZedBoard-1 and the monitor inputs on the three ball-on-plate stations are
driven by a ZedBoard each. All compute platforms are connected in an Ethernet
network.

The overall ROS2 application splits into two parts, the control of ball-on-
plate stations and a video processing chain. Figure 8 shows all involved ROS2
nodes with their communication objects. The control loop for a ball-on-plate
station comprises the four ROS2 nodes Touch, Control, Inverse and Servo. The
Touch node starts a new control cycle by reading the actual position of the
ball on the platform. This information is scaled and sent to the Control node
that implements a PID controller and a Kalman filter to determine the desired
rotations for the platform with respect to the $x$ and $y$ axes. The
subsequent Inverse node applies inverse kinematics transformations to
determine the required angle for each of the six servo motors. Finally, the
Servo node converts the angles into pulse width modulated signals to drive the
motors.

The video processing chain includes ROS2 nodes for video input, HDMI in,
processing, Filter, and video output, HDMI out. The HDMI interface
implementation includes mechanisms for the transport of image data from and to
the main memory without processor interaction by using AXI VDMAs (Video Direct
Memory Access).

All ROS2 nodes use publish/subscribe mechanisms to communicate with topics
shown in Figure 8.

Figure 7. Mechatronics model based on three ball-on-plate stations with
Stewart platforms Figure 8. ROS2 application with node and communication
objects for the mechatronics model shown in Figure 7

We have realized all ROS2 nodes in software and hardware. Table 6 lists the
raw node runtimes. The hardware implementations of the inverse kinematics and
the filter nodes can exploit low-level parallelism and achieve speedups. All
other nodes are either more control-flow intensive, exhibit little
computation, or are bound by the memory bandwidth and are thus better mapped
to software.

Given that both software and hardware implementations for the ROS2 nodes are
available, developers can easily distribute the nodes across the boards in the
network, change the mapping of nodes in the project configuration files, and
re-build the system. One specific example for such a mapping of nodes is
indicated in Figure 8. With this mapping, the sampling time of the Touch node
and, thus, the control loop could be set to 20 ms which results in rather
smooth movements of the Stewart platforms. It must be noted that the
implemented system is not a hard real-time system with a guaranteed sampling
period of 20 ms. Creating a hard real-time system would require to modify
ReconROS and the underlying ROS2 and Linux layers, as well as substitute
Ethernet communication with a real-time version and is clearly out of scope
for this work. Table 7 lists the resources required for this specific mapping,
including the actual hardware-mapped nodes, the necessary ReconROS
infrastructure, and the components needed for the HDMI input and output
interfaces.

ROS2 node |  $t_{node-SW}$ [ms] |  $t_{node-HW}$ [ms] |  $S_{node}$
---|---|---|---
Servo | 0.001 |  $<$ 0.001 |  $\approx$1
Control | 0.017 | 0.030 | 0.57
Inverse | 1.430 | 0.196 | 7.30
Touch | 0.001 |  $<$ 0.001 |  $\approx$1
HDMI In | 5.160 | 18.460 | 0.28
HDMI Out | 4.590 | 18.400 | 0.25
Filter | 37.530 | 22.280 | 1.68
Table 6. Runtimes for the ROS2 nodes of the mechatronics example in software and hardware Board |  FPGA |  Slice LUTs |  DSP |  BRAM
---|---|---|---|---
Zedboard Main | Zynq-7020 | 13467 (25.31%) | 0 (0.00%) | 3 (2.14%)
Zedboard 1 | Zynq-7020 | 13235 (24.88%) | 77 (35.00%) | 3 (2.14%)
Zedboard 2 | Zynq-7020 | 13031 (24.49%) | 77 (35.00%) | 3 (2.14%)
Table 7. Resource utilization of the three involved FPGA-boards

##  6\. Conclusion and Future Work

In this paper we have presented ReconROS, a novel approach that enables
developers of ROS2 robotics applications to leverage the performance and
energy-efficiency of FPGA implementations. ReconROS bases on ReconOS and
allows for flexible hardware acceleration of ROS2 nodes through an API that
supports a consistent programming model for ROS2 nodes across the
hardware/software boundary, while preserving the main advantages of ReconOS
such as full memory access for hardware threads or operating system like
synchronization mechanisms for hardware/software co-designed applications.

Future work is planned along the following lines: First, we want to leverage
partial reconfiguration available with ReconOS (Agne et al., 2014) to manage
the reprogrammable hardware resources more efficiently, for example by
configuring ROS2 hardware nodes on demand. Second, since in distributed ROS
networks not all compute nodes might be equipped with platform FPGAs, we plan
to investigate the feasibility of a ROS2 node offering acceleration-as-a-
service. Third, while programming distributed robotics applications with FPGA
acceleration is greatly supported by ReconROS, there is a demand for
simulating such systems before deployment and for adding runtime monitoring
functionality that can be used for debugging. Finally, we plan to showcase
ReconROS for multi-drones (Scherer and Rinner, 2020) which are one of the most
demanding classes of distributed robotics systems.

## References

  * (1)
  * Agne et al. (2014) A. Agne, M. Happe, A. Keller, E. Lübbers, B. Plattner, M. Platzner, and C. Plessl. 2014.  ReconOS: An Operating System Approach for Reconfigurable Computing.  _IEEE Micro_ 34, 1 (2014), 60–71.
  * Brugger et al. (2015) Christian Brugger, Lorenzo Dal’Aqua, Javier Alejandro Varela, Christian De Schryver, Mohammadsadegh Sadri, Norbert Wehn, Martin Klein, and Michael Siegrist. 2015.  A quantitative cross-architecture study of morphological image processing on CPUs, GPUs, and FPGAs. In _Proc. 2015 IEEE Symposium on Computer Applications Industrial Electronics (ISCAIE)_. 201–206.
  * Eisoldt et al. (2021) Marc Eisoldt, Steffen Hinderink, Marco Tassemeier, Marcel Flottmann, Juri Vana, Thomas Wiemann, Julian Gaal, Marc Rothmann, and Mario Porrmann. 2021.  ReconfROS: Running ROS on Reconfigurable SoCs.  In _Proc. of the 2021 Drone Systems Engineering and Rapid Simulation and Performance Evaluation: Methods and Tools Proceedings_. 16–21.
  * Gonzalez and Woods (2018) R.C. Gonzalez and R.E. Woods. 2018.  _Digital Image Processing_.  Pearson.
  * Haubelt et al. (2003) C. Haubelt, D. Koch, and J. Teich. 2003.  ReCoNet: modeling and implementation of fault tolerant distributed reconfigurable hardware. In _Proc. 16th Symposium on Integrated Circuits and Systems Design, 2003. SBCCI 2003_. 343–348.
  * Knuth (1998) D.E. Knuth. 1998\.  _The Art of Computer Programming: Volume 3: Sorting and Searching_.  Pearson Education.
  * Leal et al. (2020) Daniel Pinheiro Leal, Midori Sugaya, Hideharu Amano, and Takeshi Ohkawa. 2020.  Automated Integration of High-Level Synthesis FPGA Modules with ROS2 Systems. In _2020 International Conference on Field-Programmable Technology (ICFPT)_. IEEE, 292–293.
  * Lienen (2019) Christian Lienen. 2019\.  _Implementing a Real-time System on a Platform FPGA operated with ReconOS_.  Master’s thesis.  https://ris.uni-paderborn.de/publication/15874
  * Lienen et al. (2020) Christian Lienen, Marco Platzner, and Bernhard Rinner. 2020\.  ReconROS: Flexible Hardware Acceleration for ROS2 Applications. In _2020 International Conference on Field-Programmable Technology (ICFPT)_.
  * Lübbers and Platzner (2009) Enno Lübbers and Marco Platzner. 2009.  ReconOS: Multithreaded Programming for Reconfigurable Computers.  _ACM Transactions on Embedded Computing Systems_ 9, 1 (2009), 8:1–8:33.
  * Maruyama et al. (2016) Yuya Maruyama, Shinpei Kato, and Takuya Azumi. 2016\.  Exploring the Performance of ROS2. In _Proc. 13th International Conference on Embedded Software_. ACM, Article 5, 10 pages.
  * Ohkawa et al. (2019) T. Ohkawa, Y. Sugata, H. Watanabe, N. Ogura, K. Ootsu, and T. Yokota. 2019\.  High Level Synthesis of ROS Protocol Interpretation and Communication Circuit for FPGA. In _Proc. 2019 IEEE/ACM 2nd International Workshop on Robotics Software Engineering (RoSE)_. 33–36.
  * Podlubne and Göhringer (2019) A. Podlubne and D. Göhringer. 2019.  FPGA-ROS: Methodology to Augment the Robot Operating System with FPGA Designs. In _Proc. 2019 International Conference on ReConFigurable Computing and FPGAs (ReConFig)_.
  * Qasaimeh et al. (2019) Murad Qasaimeh, Kristof Denolf, Jack Lo, Kees Vissers, Joseph Zambreno, and Phillip H. Jones. 2019\.  Comparing Energy Efficiency of CPU, GPU and FPGA Implementations for Vision Kernels. In _Proc. 2019 IEEE International Conference on Embedded Software and Systems (ICESS)_. 1–8.
  * Scherer and Rinner (2020) Jürgen Scherer and Bernhard Rinner. 2020.  Multi-Robot Persistent Surveillance With Connectivity Constraints.  _IEEE Access_ 8 (2020), 15093–15109.
  * Stewart (1965a) D. Stewart. 1965a.  A Platform with Six Degrees of Freedom. In _Proc. of the Institution of Mechanical Engineers_ , Vol. 180. 371–386.
  * Stewart (1965b) D. Stewart. 1965b.  A Platform with Six Degrees of Freedom.  _Proc. of the Institution of Mechanical Engineers_ 180, 1 (1965), 371–386.
  * Strohmer et al. (2019) B. Strohmer, A. BØgild, A. S. SØrensen, and L. B. Larsen. 2019.  ROS-Enabled Hardware Framework for Experimental Robotics. In _Proc. 2019 International Conference on ReConFigurable Computing and FPGAs (ReConFig)_.
  * Sugata et al. (2017) Yuhei Sugata, Takeshi Ohkawa, Kanemitsu Ootsu, and Takashi Yokota. 2017.  Acceleration of Publish/Subscribe Messaging in ROS-Compliant FPGA Component. In _Proc. of the 8th International Symposium on Highly Efficient Accelerators and Reconfigurable Technologies (HEART2017)_ (Bochum, Germany). ACM, Article 13, 6 pages.
  * Ulusel et al. (2016) Onur Ulusel, Christopher Picardo, Christopher B. Harris, Sherief Reda, and R. Iris Bahar. 2016\.  Hardware acceleration of feature detection and description algorithms on low-power embedded platforms. In _Proc. 2016 26th International Conference on Field Programmable Logic and Applications (FPL)_. 1–9.
  * Venieris and Bouganis (2019) Stylianos I. Venieris and Christos-Savvas Bouganis. 2019.  fpgaConvNet: Mapping Regular and Irregular Convolutional Neural Networks on FPGAs.  _IEEE Transactions on Neural Networks and Learning Systems_ 30, 2 (2019), 326–342.
  * Yamashina et al. (2016) Kazushi Yamashina, Hitomi Kimura, Takeshi Ohkawa, Kanemitsu Ootsu, and Takashi Yokota. 2016.  CReComp: Automated Design Tool for ROS-Compliant FPGA Component. In _Proc. IEEE 10th International Symposium on Embedded Multicore/Many-Core Systems-on-Chip, MCSoC 2016_. IEEE, 138–145.
  * Yamashina et al. (2015) Kazushi Yamashina, Takeshi Ohkawa, Kanemitsu Ootsu, and Takashi Yokota. 2015.  Proposal of ROS-compliant FPGA component for low-power robotic systems (retraction notice). In _Proc. International Conference on Intelligent Earth Observing and Applications 2015_ , Vol. 9808. 98082N.
  * Yanmaz et al. (2018) Evşen Yanmaz, Saeed Yahyanejad, Bernhard Rinner, Hermann Hellwagner, and Christian Bettstetter. 2018\.  Drone networks: Communications, coordination, and sensing.  _Ad Hoc Networks_ 68 (2018), 1–15.


###  5.5 Adding assertions to other models and tools

It is also useful to add communicable assertions to the widely-used applied pi
calculus [1]. It would be especially interesting to see how this impacts the
notion of static equivalence, and then study expressibility and decidability.
As mentioned earlier, one can express certain “equivalence” properties in a
more natural manner with assertions as compared to the terms-only model.
Another promising extension is to study which equivalence properties can be
expressed as reachability properties in this manner, like in [25]. These would
also help us to extend existing tools [21, 33, 11, 13] with assertions.

## References

  * [1] Martín Abadi, Bruno Blanchet, and Cédric Fournet.  The applied pi calculus: mobile values, new names, and secure communication.  Journal of the ACM, 65(1):1:1–1:41, 2017.
  * [2] Martín Abadi and Véronique Cortier.  Deciding knowledge in security protocols under equational theories.  Theoretical Computer Science, 367(1–2):2–32, 2006.
  * [3] Ben Adida.  Helios: web-based open-audit voting.  In 17th Conference on Security Symposium, pages 335–348, 2008.
  * [4] Roberto M. Amadio, Denis Lugiez, and Vincent Vanackére.  On the symbolic reduction of processes with cryptographic functions.  Theoretical Computer Science, 290(1):695–740, 2003.
  * [5] Myrto Arapinis, Jia Liu, Eike Ritter, and Mark Ryan.  Stateful applied pi calculus: observational equivalence and labelled bisimilarity.  Journal of Logical and Algebraic Methods in Programming, 89:95–149, 2017.
  * [6] Michael Backes, Cătălin Hritçu, and Matteo Maffei.  Automated verification of remote electronic voting protocols in the applied pi-calculus.  In 21st IEEE Computer Security Foundations Symposium, pages 195–209, 2008.
  * [7] Michael Backes, Matteo Maffei, and Dominique Unruh.  Zero-knowledge in the applied pi-calculus and automated verification of the Direct Anonymous Attestation protocol.  In 29th IEEE Symposium on Security and Privacy, pages 202–215, 2008.
  * [8] A. Baskar, R. Ramanujam, and S. P. Suresh.  A dexptime-complete Dolev-Yao theory with distributive encryption.  In 35th International Symposium on Mathematical Foundations of Computer Science, volume 6281 of Lecture Notes in Computer Science, pages 102–113, 2010.
  * [9] Mathieu Baudet.  Deciding security of protocols against off-line guessing attacks.  In 12th ACM Conference on Computer and Communications Security, pages 16–25, 2005.
  * [10] Bruno Blanchet.  An efficient cryptographic protocol verifier based on Prolog rules.  In 14th IEEE Computer Security Foundations Workshop, pages 82–96, 2001.
  * [11] Bruno Blanchet.  Modeling and verifying security protocols with the applied pi calculus and ProVerif.  Foundations and Trends in Privacy and Security, 1(1):1–135, 2016.
  * [12] Bruno Blanchet and Andreas Podelski.  Verification of cryptographic protocols: tagging enforces termination.  Theoretical Computer Science, 333(1–2):67–90, 2005.
  * [13] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina.  The DEEPSEC prover.  In Computer Aided Verification, volume 10982 of Lecture Notes in Computer Science, pages 28–36, 2018.
  * [14] Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina.  The hitchhiker’s guide to decidability and complexity of equivalence properties in security protocols.  In Logic, Language, and Security: Essays Dedicated to Andre Scedrov on the Occasion of his 65th Birthday, volume 12300 of Lecture Notes in Computer Science, pages 127–145, 2020.
  * [15] Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, and Mathieu Turuani.  An NP decision procedure for protocol insecurity with XOR.  Theoretical Computer Science, 338(1–3):247–274, 2005.
  * [16] Hubert Comon-Lundh and Vitaly Shmatikov.  Intruder deductions, constraint solving and insecurity decisions in presence of exclusive or.  In 18th IEEE Symposium on Logic in Computer Science, pages 271–280, 2003.
  * [17] Véronique Cortier, Stéphanie Delaune, and Pascal Lafourcade.  A survey of algebraic properties used in cryptographic protocols.  Journal of Computer Security, 14(1):1–43, 2006.
  * [18] Véronique Cortier, Stéphanie Delaune, and Vaishnavi Sundararajan.  A decidable class of security protocols for both reachability and equivalence properties.  Journal of Automated Reasoning, 65(4):479–520, 2021.
  * [19] Véronique Cortier and Steve Kremer.  Formal models and techniques for analyzing security protocols: a tutorial.  Foundations and Trends in Programming Languages, 1(3):151–267, 2014.
  * [20] Véronique Cortier, Michaël Rusinowitch, and Eugen Zălinescu.  A resolution strategy for verifying cryptographic protocols with CBC encryption and blind signatures.  In 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 12–22, 2005.
  * [21] Cas J. F. Cremers.  The Scyther tool: verification, falsification, and analysis of security protocols.  In 20th International Conference on Computer Aided Verification, volume 5123 of Lecture Notes in Computer Science, pages 414–418, 2008.
  * [22] Danny Dolev and Andrew Yao.  On the security of public-key protocols.  IEEE Transactions on Information Theory, 29(2):198–208, 1983.
  * [23] Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov.  Multiset rewriting and the complexity of bounded security protocols.  Journal of Computer Security, 12(2):247–311, 2004.
  * [24] Atsushi Fujioka, Tatsuaki Okamoto, and Kazuo Ohta.  A practical secret voting scheme for large scale elections.  In Advances in Cryptology – AUSCRYPT, volume 718 of Lecture Notes in Computer Science, pages 244–251, 1992.
  * [25] Sébastien Gondron, Sebastian Mödersheim, and Luca Viganò.  Privacy as reachability.  In 35th IEEE Computer Security Foundations Symposium, pages 130–146, 2022.
  * [26] Jens Groth and Amit Sahai.  Efficient non-interactive proof systems for bilinear groups.  In Advances in Cryptology – EUROCRYPT, volume 4965 of Lecture Notes in Computer Science, pages 415–432, 2008.
  * [27] Nevin Heintze and Doug Tygar.  A model for secure protocols and their compositions.  IEEE Transactions on Software Engineering, 22(1):16–30, 1996.
  * [28] Steve Kremer and Robert Künnemann.  Automated analysis of security protocols with global state.  Journal of Computer Security, 24(5):583–616, 2016.
  * [29] Steve Kremer and Mark Ryan.  Analysis of an electronic voting protocol in the applied pi calculus.  In Programming Languages and Systems – ESOP 2005, volume 3444 of Lecture Notes in Computer Science, pages 186–200, 2005.
  * [30] Pascal Lafourcade, Denis Lugiez, and Ralf Treinen.  Intruder deduction for the equational theory of abelian groups with distributive encryption.  Information and Computation, 205(4):581–623, 2007.
  * [31] Matteo Maffei, Kim Pecina, and Mathieu Reinert.  Security and privacy by declarative design.  In 26th IEEE Computer Security Foundations Symposium, pages 81–96, 2003.
  * [32] David A. McAllester.  Automatic recognition of tractability in inference relations.  Journal of the ACM, 40(2):284–303, 1993.
  * [33] Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin.  The TAMARIN prover for the symbolic analysis of security protocols.  In 25th International Conference on Computer Aided Verification, volume 8044 of Lecture Notes in Computer Science, pages 696–701, 2013.
  * [34] Jonathan K. Millen and Vitaly Shmatikov.  Constraint solving for bounded-process cryptographic protocol analysis.  In 8th ACM Conference on Computer and Communications Security, pages 166–175, 2001.
  * [35] R. Ramanujam, Vaishnavi Sundararajan, and S. P. Suresh.  Existential assertions for voting protocols.  In Financial Cryptography and Data Security, volume 10323 of Lecture Notes in Computer Science, pages 337–352, 2017.
  * [36] R. Ramanujam and S. P. Suresh.  Decidability of context-explicit security protocols.  Journal of Computer Security, 13(1):135–165, 2005.
  * [37] R. Ramanujam and S. P. Suresh.  A (restricted) quantifier elimination for security protocols.  Theoretical Computer Science, 367(1–2):228–256, 2006.
  * [38] Michaël Rusinowitch and Mathieu Turuani.  Protocol insecurity with finite number of sessions and composed keys is NP-complete.  Theoretical Computer Science, 299(1–3):451–475, 2003.

##  Appendix A Proof of Theorem 40

We want to check if $(S;A)\vdash_{\mathit{a}}\alpha$, where ${\sf
bv}(\alpha)\cap{\sf vars}(S;A)=\emptyset$. Let $(T;E)=\mathit{ker}(S;A)$. By
Theorem 16, this reduces to checking if there is a substitution $\mu$ with
${\sf dom}(\mu)={\sf bv}(\alpha)$ s.t. and $X\subseteq{\sf hat}(\alpha)$ s.t.
$\forall{}x\in{\sf bv}(\alpha):T\vdash_{\mathit{dy}}\mu(x)$ and for all
$\beta\in X$, $(T;E)\vdash_{\mathit{a}}\mu(\beta)$. For formulas in $X$ that
are not of the form ${{t}\bowtie{u}}$, all terms occurring in them are
variables or names, so $\mu$ is atomic on variables occurring in them. It
therefore suffices to only consider assertions of the form ${{t}\bowtie{u}}$.

So the problem is as follows. There is a set of terms $\mathscr{C}$ and
$(T;E)$ with ${\sf st}(T)\cup{\sf st}(E)\subseteq\mathscr{C}$, and a
substitution $\mu$ with ${\sf dom}(\mu)\cap{\sf vars}(T;E)=\emptyset$, which
satisfies some derivabilities of the form $T\vdash_{\mathit{dy}}t$ and
$T;E\vdash_{\mathit{eq}}{{t}\bowtie{u}}$, where $t,u\in\mathscr{C}$. We seek a
small $\nu$ that preserves the above derivabilities. To reduce clutter, we use
$Z$ to refer to ${\sf dom}(\mu)$. Let $\mathscr{D}=\mathscr{C}\setminus Z$.
Since $T\vdash_{\mathit{dy}}\mu(x)$, all variables occurring in $\mu(x)$ must
also be in ${\sf vars}(T)$. But ${\sf vars}(T;E)\cap Z=\emptyset$, so ${\sf
vars}(\mu(x))\cap Z=\emptyset$.

Define $t\approx u$ iff $T;E\vdash_{\mathit{eq}}\mu({{t}\bowtie{u}})$. It is
easy to see that $\approx$ is a partial equivalence relation (on the subset of
terms $t$ such that $T\vdash_{\mathit{dy}}\mu(t)$).

We say that $x\in Z$ is _minimal_ if there is no $t\in\mathscr{D}$ with
$x\approx t$. Let $\mathscr{V}_{m}$ denote the set of all minimal variables.
Our strategy for finding a small $\nu$ is to “zap” minimal variables, and
propagate the change to (interpretations of) non-minimal variables. To this
end, it is convenient to translate every term to an “equivalent” one with only
minimal variables. The notion of equivalence is based on unifiability under
$\mu$. The set of all such terms that are equivalent to terms in $\mathscr{C}$
is defined as follows.

######  Definition 41.

$\widehat{\mathscr{C}}\coloneqq\\{t\mid{\sf vars}(t)\cap
Z\subseteq\mathscr{V}_{m},\text{ either }t\in\mathscr{V}_{m}\text{ or
}\exists{u}\in\mathscr{D}:t\approx u\\}$.

######  Lemma 42.

For every $t\in\mathscr{C}$ with $T\vdash_{\mathit{dy}}\mu(t)$, there is
${t}^{*}\in\widehat{\mathscr{C}}$ such that:
$T\vdash_{\mathit{dy}}\mu({t}^{*})$; $t\approx{t}^{*}$; and for all
$x\in\mathscr{V}_{m}$, $\mathbb{P}_{x}({{t}^{*}})\subseteq\mathbb{A}(T\cup
Z,{t}^{*})$.

###### Proof.

For $x,y\in Z$, $x\prec y$ iff $\exists{r}\in\mathscr{D}[x\in{\sf st}(r)\text{
and }r\approx y]$.

We now show that $\prec$ is acyclic. Towards this, we claim that if $x\prec y$
and $y\prec z$, then there is some term $a$ (not necessarily in $\mathscr{C}$)
s.t. $\mu(x)$ is a proper subterm of $\mu(a)$ and $a\approx z$. Extending this
reasoning, we see that if $x\prec^{+}x$, we have some term $a$ such that
$\mu(x)$ is a proper subterm of $\mu(a)$ and
$(T;E)\vdash_{\mathit{eq}}{{\mu(a)}\bowtie{\mu(x)}}$. But $E$ is consistent,
which means that there is some $\lambda$ s.t.
$\lambda(\mu(a))=\lambda(\mu(x))$. But this is incompatible with $\mu(x)$
being a proper subterm of $\mu(a)$. Thus $\prec$ is acyclic.

We now prove the claim. Suppose $x\prec y$ and $y\prec z$. Then there exists
$r,s\in\mathscr{D}$ such that $x\in{\sf st}(r)$,
$(T;E)\vdash_{\mathit{eq}}{{\mu(r)}\bowtie{\mu(y)}}$, $y\in{\sf st}(s)$, and
$(T;E)\vdash_{\mathit{eq}}{{\mu(s)}\bowtie{\mu(z)}}$. Let
$a={s}[{r}]_{\mathbb{P}_{y}({s})}$. We see that $\mu(x)$ is a proper subterm
of $\mu(a)$. From the abstractability conditions satisfied by $\mu$ and the
derivability of $\mu(x)$ for all $x\in Z$, we can justify the applications of
${\sf subst}$ necessary to obtain
$(T;E)\vdash_{\mathit{eq}}{{\mu(a)}\bowtie{\mu(z)}}$ and thus $a\approx z$.

Since $\prec$ is acyclic, we can define a notion of _rank_ of variables:
$\mathit{rank}(x)=\max\\{\mathit{rank}(y)\mid y\prec^{+}x\\}+1$. For a term
$u\in\mathscr{D}$, we define $\mathit{rank}(u)=\max\\{\mathit{rank}(x)\mid
x\in{\sf vars}(u)\cap Z\\}$. It is easy to verify that if $u\in\mathscr{D}$
and $x\approx u$, then $\mathit{rank}(x)>\mathit{rank}(u)$. It is also easy to
see that if $x\in\mathscr{V}_{m}$, then $x\in Z$ has rank $0$.

Having set up this machinery, we prove the lemma by induction on
$\delta(t)=(\mathit{rank}(t),|t|)$. First fix an ordering on
$\widehat{\mathscr{C}}$. For $\delta(t)=(0,0)$, we have that $t$ is a variable
$x$ and $\mathit{rank}(x)=0$. We have two cases to consider.

  * •

$x\in\mathscr{V}_{m}$: Choose ${x}^{*}=x$.

  * •

$x\notin\mathscr{V}_{m}$: This means that there is some $u\in\mathscr{D}$ s.t.
$x\approx u$. But since $\mathit{rank}(x)=0$, ${\sf vars}(u)\cap Z=\emptyset$
for each such $u$. Choose ${x}^{*}$ to be the earliest such $u$ (according to
the ordering on $\widehat{\mathscr{C}}$). Clearly
$(T;E)\vdash{{\mu(x)}\bowtie{\mu({x}^{*})}}$, and by Lemma 15,
$T\vdash_{\mathit{dy}}\mu({x}^{*})$. Finally ${\sf vars}({x}^{*})\cap
Z=\emptyset$, so it is vacuously true that
$\mathbb{P}_{y}({{x}^{*}})\subseteq\mathbb{A}(T\cup Z,{x}^{*})$ for all
$y\in\mathscr{V}_{m}$.

So suppose $\delta(t)>(0,0)$ and that the theorem is true for all $u$ such
that $\delta(u)<\delta(t)$. There are two cases to consider:

  * •

$t$ is a variable, say $x$: Then $\mathit{rank}(x)>0$, and there is
$u\in\mathscr{D}$ s.t. $x\approx u$, whence
$\mathit{rank}(u)<\mathit{rank}(x)$. Pick the earliest such
$u\in\widehat{\mathscr{C}}$. By IH there is ${u}^{*}$, and we define
${x}^{*}={u}^{*}$. Since $x\approx u$ and $u\approx{u}^{*}$, we have
$x\approx{x}^{*}$, by transitivity.

  * •

$t$ is not a variable: For each $y\in{\sf vars}(t)\cap Z$, there is ${y}^{*}$.
We obtain ${t}^{*}$ by replacing each $y$ by ${y}^{*}$. Clearly ${\sf
vars}({t}^{*})\cap Z\subseteq\mathscr{V}_{m}$. Also since all variables appear
in abstractable positions of $t$, we can justify the relevant applications of
${\sf subst}$ to justify $t\approx{t}^{*}$. Finally, if $z$ appears in an
abstractable position in $r$ and $y$ appears in an abstractable position in
$s$, then $z$ appears in an abstractable position in
${s}[{r}]_{\mathbb{P}_{y}({s})}$. Thus the abstractability part of the
statement is also fulfilled. ∎

We now define the substitution $\nu$ as follows. Assume that there is some
${\sf m}\in T\cap\mathscr{N}$ such that ${\sf m}\notin{\sf
st}(E\cup\\{\alpha\\})\cup{\sf st}({\sf rng}(\mu))$.777Thus ${\sf m}$ is a
“spare name” that does not occur in any of the derivations under
consideration. Let $\nu_{m}$ be the substitution that maps each
$x\in\mathscr{V}_{m}$ to ${\sf m}$. For all $x\in Z:\nu(x)=\nu_{m}({x}^{*})$.
Notice that for all $x\in{\sf dom}(\nu)$, either $\nu(x)={\sf m}$ or there is
$u\in\mathscr{D}$ s.t. $\nu(x)=\nu(u)$. Thus we can show that $\nu$ is
$|\mathscr{C}|$-bounded following the proof of Theorem 39. To complete the
proof of Theorem 40, we just need to show that $\nu$ preserves derivability.
This is proved in Theorem 44, the main result of this section. But first we
state a useful observation.

######  Observation 43.

a

  1. 1.

For $x\in Z$, if $\mu(x)\in\mathscr{C}$ then $x\notin\mathscr{V}_{m}$.

  2. 2.

If $t\in\widehat{\mathscr{C}}$ and $\mu(t)\in\mathscr{C}$, then ${\sf
vars}(t)\cap Z=\emptyset$ and $\mu(t)=t$.

###### Proof.

a

  1. 1.

Let $\mu(x)=t\in\mathscr{C}$. Since ${\sf vars}(t)\cap Z=\emptyset$, we have
that $t\notin Z$ and $\mu(t)=t$. Thus $t\in\mathscr{D}$, and
${{\mu(x)}\bowtie{\mu(t)}}$ is derivable using the ${\sf eq}$ rule, i.e.,
$x\approx t$. Therefore $x\notin\mathscr{V}_{m}$.

  2. 2.

For every $x\in{\sf vars}(t)\cap Z$, $\mu(x)\in\mathscr{C}$. Thus we have
$x\notin\mathscr{V}_{m}$, by the previous part. But since
$t\in\widehat{\mathscr{C}}$, we have that ${\sf vars}(t)\cap
Z\subseteq\mathscr{V}_{m}$. The only conclusion is that ${\sf vars}(t)\cap
Z=\emptyset$, and thus $\mu(t)=t$. ∎

######  Theorem 44.

a

  1. 1.

For any $t\in\mathscr{C}$, if $T\vdash_{\mathit{dy}}\mu(t)$ then
$T\vdash_{\mathit{dy}}\nu(t)$.

  2. 2.

For any $t,u\in\mathscr{C}$, if
$T;E\vdash_{\mathit{eq}}{{\mu(t)}\bowtie{\mu(u)}}$ then
$T;E\vdash_{\mathit{eq}}{{\nu(t)}\bowtie{\nu(u)}}$.

###### Proof.

By Lemma 42, it suffices to prove the following. Let
$r,s\in\widehat{\mathscr{C}}$ such that $\forall{x}\in\mathscr{V}_{m}$,
$\mathbb{P}_{x}({(r,s)})\subseteq\mathbb{A}(T\cup Z,(r,s))$. If
$T\vdash_{\mathit{dy}}\mu(r)$ then $T\vdash_{\mathit{dy}}\nu_{m}(r)$; and if
$T;E\vdash_{\mathit{eq}}{{\mu(r)}\bowtie{\mu(s)}}$ then
$T;E\vdash{{\nu_{m}(r)}\bowtie{\nu_{m}(s)}}$.

  1. 1.

Suppose $T\vdash_{\mathit{dy}}r$ for $r$ as above. Since all positions of
variables from $Z$ occurring in $r$ are abstractable w.r.t. $T\cup Z$, and
since $T\cup\\{{\sf m}\\}\vdash_{\mathit{dy}}{\sf m}$, we can easily prove by
induction on the size of terms that $T\cup{\sf
m}\vdash_{\mathit{dy}}\nu_{m}(r)$.

  2. 2.

Suppose $T;E\vdash_{\mathit{eq}}{{\mu(r)}\bowtie{\mu(s)}}$ for $r,s$ as above.
Let $\pi$ be a normal proof of $T;E\vdash{{\mu(r)}\bowtie{\mu(s)}}$ with last
rule ${\sf r}$. We prove the desired statement by induction on the structure
of $\pi$. There are the following cases to consider.

     * •

${\sf r}\in\\{{\sf ax},{\sf eq},{\sf proj}\\}$: Three cases arise:
${{\mu(r)}\bowtie{\mu(s)}}\in E$, and thus $\mu(r),\mu(s)\in\mathscr{C}$. Or
$\mu(r)=\mu(s)$ and $T\vdash_{\mathit{dy}}\mu(r)$ via a proof ending in ${\sf
ax}$ or a destructor rule, and thus $\mu(r),\mu(s)\in{\sf
st}(T)\subseteq\mathscr{C}$. Or by subterm property for normal
$\vdash_{\mathit{eq}}$-proofs $\mu(r),\mu(s)\in{\sf
st}(T;E)\subseteq\mathscr{C}$. Thus $\mu(r),\mu(s)\in\mathscr{C}$ in all three
cases. By Observation 43, ${\sf vars}(r,s)\cap Z=\emptyset$. Thus
$\nu_{m}(r)=r=\mu(r)$ and $\nu_{m}(s)=s=\mu(s)$. Therefore $\pi$ itself is a
proof of ${{\nu_{m}(r)}\bowtie{\nu_{m}(s)}}$.

     * •

${\sf r}={\sf trans}$: Suppose the immediate subproofs are
$\pi_{1},\ldots,\pi_{n}$, with each $\pi_{i}$ deriving
${{v_{i-1}}\bowtie{v_{i}}}$. Let $\mu(r)=v_{0}$ and $\mu(s)=v_{n}$. Since no
$\pi_{i}$ ends in ${\sf trans}$ and no two adjacent $\pi_{i}$’s end in ${\sf
cons}$, each $v_{i}$ (for $0<i<n$) appears in at least one proof ending in
${\sf ax}$, ${\sf eq}$ or ${\sf proj}$. Thus, by the subterm property,
$v_{i}\in{\sf st}(T;E)\subseteq\mathscr{C}$ for $0<i<n$. Since ${\sf
vars}(T;E)\cap Z=\emptyset$, it follows that $v_{i}\in\widehat{\mathscr{C}}$
and $\mu(v_{i})=v_{i}$. Thus we can view each $\pi_{i}$ as deriving
${{\mu(r_{i-1})}\bowtie{\mu(r_{i})}}$, where
$r_{i-1},r_{i}\in\widehat{\mathscr{C}}$ (taking $r_{0}$ and $r_{n}$ to be $r$
and $s$). By IH, there are proofs $\varpi_{1},\ldots,\varpi_{n}$, with each
$\varpi_{i}$ deriving ${{\nu_{m}(r_{i-1})}\bowtie{\nu_{m}(r_{i})}}$. By
composing them using ${\sf trans}$, we get a proof of
$T;E\vdash{{\nu_{m}(r)}\bowtie{\nu_{m}(s)}}$, as desired.

     * •

${\sf r}={\sf cons}$: Suppose $r={\sf f}(r_{1},\ldots,r_{n})$ and $s={\sf
f}(s_{1},\ldots,s_{n})$. Each $r_{i},s_{i}\in\widehat{\mathscr{C}}$, and the
immediate subproofs are $\pi_{1},\ldots,\pi_{n}$, with each $\pi_{i}$ deriving
${{\mu(r_{i})}\bowtie{\mu(s_{i})}}$. By IH we have proofs
$\varpi_{1},\ldots,\varpi_{n}$, with each $\varpi_{i}$ proving
${{\nu_{m}(r_{1})}\bowtie{\nu_{m}(s_{1})}}$. We can compose them with the
${\sf cons}$ rule to get the desired proof of
${{\nu_{m}(r)}\bowtie{\nu_{m}(s)}}$.

Suppose, on the other hand, that $r$ is a variable. Since
$r\in\widehat{\mathscr{C}}$, $r\in\mathscr{V}_{m}$. Now
$s\in\widehat{\mathscr{C}}$, so either $s\in\mathscr{V}_{m}$ or there is
$a\in\mathscr{D}$ with $s\approx a$. But in the second case, $r\approx a$ (by
symmetry and transitivity), which cannot happen for a minimal variable $r$.
Therefore $s\in\mathscr{V}_{m}$. And we have $\nu_{m}(r)=\nu_{m}(s)={\sf m}\in
T$, so there is a proof of
$T,E\vdash_{\mathit{eq}}{{\nu_{m}(r)}\bowtie{\nu_{m}(s)}}$ ending in ${\sf
eq}$.

We have a similar argument in case $s$ is a variable, thereby proving the
theorem. ∎

##  Appendix B Normalization and subterm property for $\vdash_{\mathit{eq}}$

Suppose $E\cup\\{\alpha\\}$ consist only of atomic formulas and $\pi$ is a
proof of $T;E\vdash_{\mathit{eq}}\alpha$. We say that $\pi$ is _normal_ if the
following hold.

  1. 1.

All $\vdash_{\mathit{dy}}$ subproofs are normal.

  2. 2.

The premise of ${\sf sym}$ can only be the conclusion of ${\sf ax}$ or ${\sf
prom}$.

  3. 3.

The premise of ${\sf eq}$ can only be the conclusion of a destructor rule.

  4. 4.

No premise of a ${\sf trans}$ is of the form ${{a}\bowtie{a}}$, or the
conclusion of a ${\sf trans}$.

  5. 5.

Adjacent premises of a ${\sf trans}$ are not conclusions of ${\sf cons}$.

  6. 6.

No premise of ${\sf int}$ is the conclusion of ${\sf int}$ or ${\sf wk}$.

  7. 7.

No subproof ending in ${\sf proj}$ contains ${\sf cons}$.

A set $E$ of atomic formulas is said to be _consistent_ if there is a
$\lambda$ s.t. $\lambda(t)=\lambda(u)$ for each ${{t}\bowtie{u}}\in E$, and
$\lambda(t)\in\\{t_{1},\ldots,t_{n}\\}$ for each
$t\twoheadleftarrow{[t_{1},\ldots,t_{n}]}\in E$.

R1 | ${\sf eq}({\sf f}(\pi_{1},\pi_{2}))$
---|---
${\sf cons}_{{\sf f}}({\sf eq}(\pi_{1}),{\sf eq}(\pi_{2}))$
R2 | ${\sf sym}({\sf eq}(\pi))$
${\sf eq}(\pi)$
R3 | ${\sf sym}({\sf sym}(\pi))$
$\pi$
R4 | ${\sf sym}({\sf r}(\pi_{1},\ldots,\pi_{k}))$
${\sf r}({\sf sym}(\pi_{1}),\ldots,{\sf sym}(\pi_{k}))$
R5 | ${\sf trans}(\pi_{1},\ldots,\pi_{i-1},\varpi,\pi_{i},\ldots,\pi_{r-1})$
${\sf trans}(\pi_{1},\ldots,\pi_{i-1},\pi_{i},\ldots,\pi_{r-1})$
R6 | ${\sf trans}(\pi_{1},\ldots,{\sf trans}(\pi^{1}_{i},\ldots,\pi^{k}_{i}),\ldots,\pi_{r-1})$
${\sf trans}(\pi_{1},\ldots,\pi^{1}_{i},\ldots,\pi^{k}_{i},\ldots,\pi_{r-1})$
R7 | ${\sf trans}(\pi_{1},\ldots,{\sf cons}(\pi^{1}_{i-1},\pi^{2}_{i-1}),{\sf cons}(\pi^{1}_{i},\pi^{2}_{i}),\ldots,\pi_{r-1})$
${\sf trans}(\pi_{1},\ldots,{\sf cons}({\sf
trans}(\pi^{1}_{i-1},\pi^{1}_{i}),{\sf
trans}(\pi^{2}_{i-1},\pi^{2}_{i})),\ldots,\pi_{r-1})$
R8 | ${\sf proj}_{j}({\sf cons}(\pi_{1},\pi_{2}))$
$\pi_{j}$
R9 | ${\sf proj}_{j}({\sf trans}(\pi_{1},\ldots,\pi_{i-1},{\sf cons}_{{\sf f}}(\pi^{1}_{i},\pi^{2}_{i}),\pi_{i+1},\ldots,\pi_{r-1}))$
${\sf trans}({\sf proj}_{j}({\sf
trans}(\pi_{1},\ldots,\pi_{i-1})),\pi^{j}_{i},{\sf proj}_{j}({\sf
trans}(\pi_{i+1},\ldots,\pi_{r-1})))$
R10 | ${\sf int}(\pi_{1},\ldots,\pi_{k-1},{\sf int}(\pi_{k},\ldots,\pi_{m}),\pi_{m+1},\ldots,\pi_{n})$
${\sf
int}(\pi_{1},\ldots,\pi_{k-1},\pi_{k},\ldots,\pi_{m},\pi_{m+1},\ldots,\pi_{n})$
R11 | ${\sf int}(\pi_{1},\ldots,{\sf wk}(\pi_{i}),\ldots,\pi_{n})$
${\sf wk}(\pi_{i})$
Table 3: Proof transformation rules. The proof represented by the first line
in each row is transformed to the proof represented by the second line. In R4,
${\sf r}\in\\{{\sf trans},{\sf proj},{\sf cons}\\}$. In R5, ${\sf
conc}(\varpi)$ is assumed to be of the form ${{a}\bowtie{a}}$.

We next prove normalization for $\vdash_{\mathit{eq}}$ proofs (with a
consistent LHS). We present proof transformation rules in Table 3. To save
space, we use _proof terms_ – ${\sf r}(\pi_{1},\ldots,\pi_{n})$ denotes a
proof $\pi$ with last rule ${\sf r}$ and immediate subproofs
$\pi_{1},\ldots,\pi_{n}$. It is assumed that the derivations are from a
consistent $(T;E)$. R1 is applicable when ${\sf f}$ is a constructor rule, and
ensures that $\vdash_{\mathit{dy}}$ subproofs do not end in a constructor
rule. R2 and R3 eliminate some occurrences of ${\sf sym}$, while R4 pushes
${\sf sym}$ up towards the axioms. R5 and R6 ensure that no premise of ${\sf
trans}$ is the conclusion of ${\sf eq}$ or ${\sf trans}$. R7 ensures that
adjacent premises of ${\sf trans}$ are not the result of ${\sf cons}$. R8
simplifies proofs where ${\sf proj}$ follows ${\sf cons}$. We will discuss R9
later. R10 ensures that the conclusion of ${\sf int}$ is not a premise of
${\sf int}$. In R11, $\pi_{i}$ proves an equality ${{v}\bowtie{n}}$, and it is
weakened to a list membership of the form $v\twoheadleftarrow\ell^{\prime}$,
but by consistency, even after intersection, the conclusion must be of the
form $v\twoheadleftarrow{\ell}$ where $\lambda(v)$ is an element of $\ell$ for
some $\lambda$. Thus we can directly apply weakening to $\pi_{i}$ to get the
same conclusion.

R9 requires some explanation. Let $\pi_{i}$ be the proof ${\sf cons}_{{\sf
f}}(\pi^{1}_{i},\pi^{2}_{i})$, and let ${\sf conc}(\pi_{j})$ be
${{t_{j}}\bowtie{t_{j+1}}}$, for $1\leq j<r$. We see that ${\sf conc}({\sf
trans}(\pi_{1},\ldots,\pi_{r-1}))$ is ${{t_{1}}\bowtie{t_{r}}}$. Since ${\sf
proj}$ is applied on this, there is some constructor ${\sf g}$ such that
$t_{e}={\sf g}(t^{1}_{e},t^{2}_{e})$ for $e\in\\{1,r\\}$. Since $\pi_{i}$ ends
in ${\sf cons}_{{\sf f}}$, we see that $t_{e}={\sf f}(t^{1}_{e},t^{2}_{e})$
for $e\in\\{i,i+1\\}$. But ${{t_{1}}\bowtie{t_{i}}}$ is provable from $(T;E)$,
which is consistent. Therefore it has to be the case that ${\sf f}={\sf g}$.
Thus we see that for all $e\in\\{1,i,i+1,r\\}$, $t_{e}={\sf
f}(t^{1}_{e},t^{2}_{e})$. So we can rewrite the LHS of R9 to the RHS to get a
valid proof. Note that we can apply ${\sf proj}$ on ${{t_{1}}\bowtie{t_{i}}}$
in the transformed proof since all components of $t_{1}$ and $t_{i}$ are
abstractable – for $t_{1}$ this is true because the ${\sf proj}$ rule was
applied to ${{t_{1}}\bowtie{t_{r}}}$ in the proof on the LHS; and for $t_{i}$
this follows from the fact that $\pi^{1}_{i}$ (resp. $\pi^{2}_{i}$) derives
${{t^{1}_{i}}\bowtie{t^{1}_{i+1}}}$ (resp.
${{t^{2}_{i}}\bowtie{t^{2}_{i+1}}}$), and so by Lemma 15,
$T\vdash_{\mathit{dy}}\\{t^{1}_{i},t^{2}_{i}\\}$. For a similar reason, we can
apply ${\sf proj}$ on ${{t_{i+1}}\bowtie{t_{r}}}$.

######  Theorem 45.

If $(T;E)\vdash_{\mathit{eq}}\alpha$ then there is a normal proof of
$(T;E)\vdash\alpha$ in the $\vdash_{\mathit{eq}}$ system.

###### Proof.

Let $\pi$ be any proof of $(T;E)\vdash\alpha$ such that all DY subproofs of
$\pi$ are normal. Suppose we repeatedly apply the transformations of Table 3
starting with $\pi$ and reach a proof $\varpi$ on which we can no longer apply
any of the rules. Then $\varpi$ satisfies clauses 1 to 6 in the definition of
normal proofs (since none of the rewrite rules, in particular R1–R7 and
R10–R11, apply to $\varpi$).

Clause 7 is also satisfied by $\varpi$, for the following reason. Suppose a
subproof $\varpi_{1}$ ends in ${\sf proj}$ and $\varpi_{2}$ is a maximal
subproof of $\varpi_{1}$ ending in ${\sf cons}$. $\varpi_{2}$ is a proper
subproof of $\varpi_{1}$, so there has to be a subproof of $\varpi_{1}$ of the
form $\rho={\sf r}(\cdots\varpi_{2}\cdots)$. Since ${\sf cons}$ appears as the
rule above ${\sf r}$, a priori, ${\sf r}$ can only be one of $\\{{\sf
sym},{\sf trans},{\sf proj},{\sf cons}\\}$. But since $\varpi_{2}$ is a
_maximal subproof_ of $\varpi_{1}$ ending in ${\sf cons}$, ${\sf r}\neq{\sf
cons}$. Since R4 and R8 cannot be applied on $\varpi$, ${\sf r}\notin\\{{\sf
sym},{\sf proj}\\}$. But if ${\sf r}={\sf trans}$, then $\rho$ is a proper
subproof of $\varpi_{1}$. In particular, it is the immediate subproof of some
$\rho^{\prime}={\sf r}^{\prime}(\cdots\rho\cdots)$. Now ${\sf r}^{\prime}$
cannot be ${\sf subst}$, since then ${\sf conc}(\rho^{\prime})$ is a list
membership assertion, which cannot occur in a proof ending in ${\sf proj}$.
${\sf r}^{\prime}\neq{\sf cons}$, as that would violate the maximality of
$\varpi_{2}$. ${\sf r}^{\prime}\notin\\{{\sf sym},{\sf trans},{\sf proj}\\}$,
since then one of the rewrite rules R4, R6, R8 would apply to $\varpi$. We
have ruled out all possible cases for ${\sf r}^{\prime}$, and thus we are
forced to conclude that $\varpi_{2}$ cannot be a subproof of $\varpi_{1}$.
Thus, ${\sf cons}$ does not occur in any subproof of $\varpi$ ending in ${\sf
proj}$, and $\varpi$ satisfies all the clauses in the definition of normal
proofs.

We next show that we can always reach a stage where no transformation is
enabled. To begin with, apply the rules R2–R4 until the premise of each
occurrence of ${\sf sym}$ is the conclusion of an ${\sf ax}$ or a ${\sf
prom}$. None of the other rules converts a proof ending in ${\sf ax}$ or ${\sf
prom}$ to one which does not, so the above property is preserved even if we
apply the other rules in any order.

Associate three sizes to an $\vdash_{\mathit{eq}}$-proof $\pi$:

  * •

$\delta_{1}(\pi)$ is the sum of the sizes of the $\vdash_{\mathit{dy}}$
subproofs of $\pi$,

  * •

$\delta_{2}(\pi)$ is the number of ${\sf cons}$ rules that occur in $\pi$, and

  * •

$\delta_{3}(\pi)$ is the size of the proof $\pi$ (number of nodes in the proof
tree).

We also define
$\delta(\pi)\coloneqq(\delta_{1}(\pi),\delta_{2}(\pi),\delta_{3}(\pi))$.

We now show that if $\pi^{\prime}$ is obtained from $\pi$ by one application
of any of the transformation rules other than R2–R4,
$\delta(\pi^{\prime})<\delta(\pi)$.

  * •

If R1 is applied, $\delta_{1}(\pi^{\prime})<\delta_{1}(\pi)$ and so
$\delta(\pi^{\prime})<\delta(\pi)$.

  * •

If R7 or R9 is applied, we have $\delta_{1}(\pi^{\prime})\leq\delta_{1}(\pi)$
and $\delta_{2}(\pi^{\prime})<\delta_{2}(\pi)$. Therefore,
$\delta(\pi^{\prime})<\delta(\pi)$.

  * •

If R5, R6, R8, R10 or R11 is applied, we have that
$\delta_{i}(\pi^{\prime})\leq\delta_{i}(\pi)$ for $i\in\\{1,2\\}$ and
$\delta_{3}(\pi^{\prime})<\delta_{3}(\pi)$. So
$\delta(\pi^{\prime})<\delta(\pi)$.

Thus, once we apply R2–R4 till they can no longer be applied, we cannot have
an infinite sequence of transformations starting from any $\pi$. Hence, every
proof $\pi$ can be transformed into a normal proof $\varpi$ with the same
conclusion. ∎

We state and prove the subterm property next.

######  Theorem 46.

For any normal proof $\pi$ of $T;E\vdash_{\mathit{eq}}\alpha$,
${\sf terms}(\pi)\subseteq{\sf st}(T)\cup{\sf st}(E\cup\\{\alpha\\})$, and
${\sf lists}(\pi)\subseteq{\sf lists}(E\cup\\{\alpha\\})\cup\\{[n]\mid
n\in{\sf st}(T)\cup{\sf st}(E\cup\\{\alpha\\})\\}$. If $\pi$ does not contain
${\sf cons}$, then ${\sf terms}(\pi)\subseteq{\sf st}(T)\cup{\sf st}(E)$ .
Also, if $\pi$ does not end in ${\sf wk}$ and does not end in ${\sf int}$,
then ${\sf lists}(\pi)\subseteq{\sf lists}(E)\cup\\{[n]\mid n\in{\sf
st}(T)\cup{\sf st}(E)\\}$.

We implicitly use the following easily provable facts.

  1. (F1)

If a normal proof $\pi$ ends in ${\sf trans}$ and an immediate subproof
$\varpi$ does not end in ${\sf cons}$, then ${\sf cons}$ does not occur in
$\varpi$.

  2. (F2)

If a normal proof $\pi$ derives a list membership assertion, ${\sf cons}$ does
not occur in $\pi$.

###### Proof.

Let ${\sf r}$ be the last rule of $\pi$. We have the following cases. We
mention ${\sf lists}(\pi)$ only in cases where the rules involve lists.

  * •

${\sf r}={\sf ax}$: $\alpha\in E$, so ${\sf terms}(\pi)\subseteq{\sf st}(E)$
and ${\sf lists}(\pi)\subseteq{\sf lists}(E)$.

  * •

${\sf r}={\sf eq}$: $\alpha$ is ${{t}\bowtie{t}}$ and
$T\vdash_{\mathit{dy}}t$. Since $\pi$ is a normal proof whose
$\vdash_{\mathit{dy}}$ subproofs are also normal, $T\vdash_{\mathit{dy}}t$ via
a proof ending in a destructor rule, and by subterm property for
$\vdash_{\mathit{dy}}$, it follows that $t\in{\sf st}(T)$. Thus ${\sf
terms}(\pi)=\\{t\\}\subseteq{\sf st}(T)$.

  * •

${\sf r}={\sf sym}$: ${\sf terms}(\pi)={\sf terms}(\pi^{\prime})$, where
$\pi^{\prime}$ is the immediate subproof, and the statement follows by IH.

  * •

${\sf r}={\sf cons}$: $\alpha$ is ${{{\sf f}(t_{1},t_{2})}\bowtie{{\sf
f}(u_{1},u_{2})}}$, and for $i\in\\{1,2\\}$, there is a subproof $\pi_{i}$
with conclusion ${{t_{i}}\bowtie{u_{i}}}$. By IH, ${\sf
terms}(\pi_{i})\subseteq{\sf st}(T\cup\\{t_{i},u_{i}\\})\cup{\sf
st}(E)\subseteq{\sf st}(T)\cup{\sf st}(E\cup\\{\alpha\\})$ for
$i\in\\{1,2\\}$. Thus ${\sf terms}(\pi)\subseteq{\sf st}(T)\cup{\sf
st}(E\cup\\{\alpha\\})$.

  * •

${\sf r}={\sf trans}$: Suppose the subproofs of $\pi$ are $\pi_{1}$ through
$\pi_{k-1}$ with conclusions ${{t_{1}}\bowtie{t_{2}}}$ through
${{t_{k-1}}\bowtie{t_{k}}}$ respectively, and
$\alpha={{t_{1}}\bowtie{t_{k}}}$. Since $\pi$ is a normal proof, no two
adjacent premises of ${\sf r}$ are obtained by ${\sf cons}$, and no premise of
${\sf r}$ is obtained by ${\sf trans}$. The following cases arise.

    * –

$r\in\\{t_{1},t_{k}\\}$. In this case, $r\in{\sf st}(\alpha)$.

    * –

$r\in{\sf terms}(\pi_{i})$, where $\pi_{i}$ does not end in ${\sf cons}$. By
(F1), ${\sf cons}$ does not occur in $\pi_{i}$. By IH, $r\in{\sf
st}(T)\cup{\sf st}(E)$.

    * –

$r\in{\sf terms}(\pi_{i})$, where $\pi_{i}$ ends in ${\sf cons}$, and
$1<i<k-1$. Both $\pi_{i-1}$ and $\pi_{i+1}$ end in a rule other than ${\sf
cons}$, by normality of $\pi$. So, by (F1), ${\sf cons}$ does not occur in
$\pi_{i-1}$ and $\pi_{i+1}$, and $t_{i},t_{i+1}\in{\sf
terms}(\pi_{i-1})\cup{\sf terms}(\pi_{i+1})\subseteq{\sf st}(T)\cup{\sf
st}(E)$ (by IH on $\pi_{i-1}$ and $\pi_{i+1}$). So, by applying IH on
$\pi_{i}$, we get $r\in{\sf st}(T)\cup{\sf
st}(E\cup\\{{{t_{i}}\bowtie{t_{i+1}}}\\})\subseteq{\sf st}(T)\cup{\sf st}(E)$.

    * –

$r\in{\sf terms}(\pi_{1})$, where $\pi_{1}$ ends in ${\sf cons}$. By normality
of $\pi$, we see that $\pi_{2}$ ends in a rule other than ${\sf cons}$. So
${\sf cons}$ does not occur in $\pi_{2}$. By IH on $\pi_{2}$, $t_{2}\in{\sf
terms}(\pi_{2})\subseteq{\sf st}(T)\cup{\sf st}(E)$. By IH on $\pi_{1}$,
$r\in{\sf st}(T\cup\\{t_{1},t_{2}\\})\cup{\sf st}(E)\subseteq{\sf
st}(T)\cup{\sf st}(E\cup\\{\alpha\\})$.

    * –

$r\in{\sf terms}(\pi_{k-1})$, where $\pi_{k-1}$ ends in ${\sf cons}$. The
proof is similar to the above.

  * •

${\sf r}={\sf proj}$: Let $\alpha={{t}\bowtie{u}}$, got from a proof
$\pi^{\prime}$ with conclusion ${{a}\bowtie{b}}$. Since $\pi$ is normal, ${\sf
cons}$ does not occur in $\pi$ (or in $\pi^{\prime}$). By IH, $a,b\in{\sf
terms}(\pi^{\prime})\subseteq{\sf st}(T)\cup{\sf st}(E)$. Since $t,u\in{\sf
st}(\\{a,b\\})$, we have ${\sf terms}(\pi)\subseteq{\sf st}(T)\cup{\sf
st}(E)$.

  * •

${\sf r}={\sf prom}$: $\alpha$ is ${{t}\bowtie{u}}$, and the immediate
subproof $\pi^{\prime}$ proves $t\twoheadleftarrow{[u]}$. $\pi^{\prime}$ does
not contain ${\sf cons}$, and so by IH, ${\sf terms}(\pi)={\sf
terms}(\pi^{\prime})\subseteq{\sf st}(T)\cup{\sf st}(E)$. Note that ${\sf
lists}(\pi)\subseteq{\sf lists}(\pi^{\prime})\cup\\{[u]\\}$, so the statement
about lists is also true.

  * •

${\sf r}={\sf wk}$: Let $\pi^{\prime}$ be the immediate subproof. The result
follows from IH and the fact that ${\sf lists}(\pi)={\sf
lists}(\pi^{\prime})\cup{\sf lists}(\alpha)$.

  * •

${\sf r}={\sf int}$: All terms in the conclusion appear in some proper
subproof, so the statement on terms follows by IH. None of the subproofs ends
in ${\sf int}$ or ${\sf wk}$ (and does not contain ${\sf cons}$). Thus ${\sf
lists}(\pi^{\prime})\subseteq{\sf lists}(E)\cup\\{[n]\mid n\in{\sf
st}(T)\cup{\sf st}(E)]$, for every subproof $\pi^{\prime}$. It follows that
${\sf lists}(\pi)\subseteq{\sf lists}(E\cup\\{\alpha\\})\cup\\{[n]\mid
n\in{\sf st}(T)\cup{\sf st}(E\cup\\{\alpha\\})\\}$.

  * •

${\sf r}={\sf subst}$: Let the major premise be $t\twoheadleftarrow{\ell}$ and
the minor premise be ${{t}\bowtie{u}}$. Both $t,u$ are from
$\mathscr{V}\cup\mathscr{N}$, and thus are in ${\sf st}(T)\cup{\sf st}(E)$.
The result follows from IH.

  * •

${\sf r}={\sf say}$: Let the major premise be $\beta$ and the minor premise be
$\mathit{sk}_{a}$. Since $T\vdash_{\mathit{dy}}\mathit{sk}_{a}$,
$\mathit{sk}_{a}\in{\sf st}(T)$. And ${\sf terms}(\pi)\subseteq{\sf
st}(T)\cup{\sf st}(E)\cup{\sf st}(\beta)\cup\\{\mathit{pk}_{a}\\}\subseteq{\sf
st}(T)\cup{\sf st}(E\cup\\{\alpha\\})$. ∎