[
[
['111','add','hl'],
['108','add','hl'],
['122','add','hl'],
['29','remove','slide-up'],
['10','add','slide-down']
],
[
['16','add','hl'],
['16','remove','hidden'],
['17','remove','indent-1'],
['17','add','hl'],
['17','remove','hidden'],
['18','add','hl'],
['18','remove','hidden'],
['6','remove','indent-1'],
['112','add','hl'],
['112','remove','slide-left'],
['20','add','hl'],
['20','remove','hidden'],
['21','add','hl'],
['21','remove','hidden'],
['7','remove','indent-1'],
['8','remove','indent-1'],
['24','add','hl'],
['24','remove','hidden'],
['9','remove','indent-1'],
['109','add','hl'],
['109','remove','slide-left'],
['26','add','hl'],
['26','remove','hidden'],
['27','add','hl'],
['27','remove','hidden'],
['28','add','hl'],
['28','remove','hidden'],
['3','add','hidden'],
['17','add','indent-2'],
['6','add','indent-2'],
['111','remove','hl'],
['111','add','slide-right'],
['7','add','indent-2'],
['8','add','indent-2'],
['9','add','indent-2'],
['108','remove','hl'],
['108','add','slide-right'],
['122','remove','hl'],
['122','add','slide-right']
],
[
['16','remove','hl'],
['17','remove','hl'],
['18','remove','hl'],
['112','remove','hl'],
['20','remove','hl'],
['21','remove','hl'],
['24','remove','hl'],
['109','remove','hl'],
['26','remove','hl'],
['27','remove','hl'],
['28','remove','hl'],
['18','add','hl'],
['6','add','hl'],
['114','add','hl'],
['24','add','hl'],
['27','add','hl'],
['44','remove','slide-up'],
['29','add','slide-down']
],
[
['111','add','hl'],
['111','remove','slide-right'],
['18','remove','hl'],
['18','add','hidden'],
['6','remove','hl'],
['6','add','hidden'],
['114','remove','hl'],
['114','add','slide-right'],
['24','remove','hl'],
['24','add','hidden'],
['27','remove','hl'],
['27','add','hidden']
],
[
['111','remove','hl'],
['7','add','hl'],
['117','add','hl'],
['47','remove','slide-up'],
['44','add','slide-down']
],
[
['118','add','hl'],
['118','remove','slide-left'],
['119-slide','remove','slide-left'],
['7','remove','hl'],
['7','add','hidden'],
['117','remove','hl'],
['117','add','slide-right']
],
[
['118','remove','hl']
],
[
['119-flip','add','flipped'],
['47','add','slide-down']
],
[
['120','add','hl'],
['122','add','hl']
],
[
['121','add','hl'],
['121','remove','slide-right'],
['122','add','hl'],
['122','remove','slide-right'],
['120','remove','hl'],
['120','add','slide-left'],
['122','remove','hl'],
['122','add','slide-left'],
['119-slide','add','slide-left']
],
[
['121','remove','hl'],
['122','remove','hl'],
['16','add','hl'],
['20','add','hl'],
['21','add','hl'],
['109','add','hl'],
['26','add','hl'],
['28','add','hl'],
['98','remove','slide-up']
],
[
['100','remove','hidden'],
['17','remove','indent-2'],
['114','add','hl'],
['114','remove','slide-right'],
['8','remove','indent-2'],
['9','remove','indent-2'],
['108','add','hl'],
['108','remove','slide-right'],
['122','add','hl'],
['122','remove','slide-left'],
['16','remove','hl'],
['16','add','hidden'],
['17','add','indent-1'],
['20','remove','hl'],
['20','add','hidden'],
['21','remove','hl'],
['21','add','hidden'],
['8','add','indent-1'],
['9','add','indent-1'],
['109','remove','hl'],
['109','add','slide-right'],
['26','remove','hl'],
['26','add','hidden'],
['28','remove','hl'],
['28','add','hidden']
],
[
['114','remove','hl'],
['108','remove','hl'],
['122','remove','hl']
]
]
The starting point is $\lib{ss-real}$.
First, separate the cases for $\U$ into different branches of an if-statement. Within each branch, we can inline the behavior of $\Filter(\U,\cdot)$. These changes have no effect on the library's behavior.
$S_2$ is not used at all in the if-branch, so it can be removed without affecting the library's behavior.
The ``else if" branch generates and returns a OTP encryption of $\ptxt$, using $S_1$ as the key. We can use the security of OTP to show that the resulting output is uniform. In this three-hop maneuver, $S_1$ becomes $\key$ from the $\lib{otp-real}$ library and $S_2$ becomes $\ctxt$.
The branches of the if-statement can now be unified by writing them in terms of $\Filter$. The result is $\lib{ss-rand}$, which completes the proof.
$\lib{ss-real}$
$\lib{ss-rand}$
if $|\U| \ge 2$: return $\myerr$
if $\U = \{ 1 \}$:
$S_1 \gets \bits^\ell$
$S_2 := S_1 \oplus \ptxt$
else if $\U = \{ 2\}$:
$S_1 \gets \bits^\ell$
$S_2 $
${}:= {}$
$S_1 \oplus \ptxt$
$\otpenc(\ptxt)$
${}\gets \bits^\ell$
return
$\Filter(\U, S_1, S_2)$
$(\mynull, S_2)$
$\Filter(\U, S_1, S_2)$
else:
return $(\mynull, \mynull)$
$\link$
$\lib{otp-real}$
$\key \gets \bits^\ell$
$\ctxt := \key \oplus \ptxt$
return $\ctxt$
$\lib{otp-rand}$
$\ctxt \gets \bits^\ell$
return $\ctxt$