[
[
['8','add','hl'],
['93','add','hl'],
['88','add','hl'],
['17','remove','slide-up'],
['2','add','slide-down']
],
[
['22','add','hl'],
['22','remove','hidden'],
['23','add','hl'],
['23','remove','hidden'],
['89','add','hl'],
['89','remove','slide-left'],
['4','add','hidden'],
['8','remove','hl'],
['8','add','hidden'],
['93','remove','hl'],
['93','add','slide-left'],
['88','remove','hl'],
['88','add','slide-right']
],
[
['22','remove','hl'],
['23','remove','hl'],
['89','remove','hl'],
['92','add','hl'],
['23','add','hl'],
['89','add','hl'],
['95','add','hl'],
['32','remove','slide-up'],
['17','add','slide-down']
],
[
['93','add','hl'],
['93','remove','slide-left'],
['38','add','hl'],
['38','remove','hidden'],
['90','add','hl'],
['90','remove','slide-left'],
['42','add','hl'],
['42','remove','hidden'],
['43','add','hl'],
['43','remove','hidden'],
['44','add','hl'],
['44','remove','hidden'],
['45','add','hl'],
['45','remove','hidden'],
['46','add','hl'],
['46','remove','hidden'],
['47','add','hl'],
['47','remove','hidden'],
['12','remove','indent-1'],
['13','remove','indent-2'],
['14','remove','indent-1'],
['92','remove','hl'],
['92','add','slide-right'],
['23','remove','hl'],
['23','add','hidden'],
['89','remove','hl'],
['89','add','slide-right'],
['95','remove','hl'],
['95','add','slide-left'],
['12','add','indent-2'],
['13','add','indent-3'],
['14','add','indent-2']
],
[
['93','remove','hl'],
['38','remove','hl'],
['90','remove','hl'],
['42','remove','hl'],
['43','remove','hl'],
['44','remove','hl'],
['45','remove','hl'],
['46','remove','hl'],
['47','remove','hl'],
['43','add','hl'],
['44','add','hl'],
['45','add','hl'],
['46','add','hl'],
['47','add','hl'],
['53','remove','slide-up'],
['32','add','slide-down']
],
[
['95','add','hl'],
['95','remove','slide-left'],
['12','remove','indent-2'],
['13','remove','indent-3'],
['14','remove','indent-2'],
['43','remove','hl'],
['43','add','hidden'],
['44','remove','hl'],
['44','add','hidden'],
['45','remove','hl'],
['45','add','hidden'],
['46','remove','hl'],
['46','add','hidden'],
['47','remove','hl'],
['47','add','hidden'],
['12','add','indent-1'],
['13','add','indent-2'],
['14','add','indent-1']
],
[
['95','remove','hl'],
['5','add','hl'],
['6','add','hl'],
['42','add','hl'],
['69','remove','slide-up'],
['53','add','slide-down']
],
[
['77','add','hl'],
['77','remove','hidden'],
['81','add','hl'],
['81','remove','hidden'],
['82','add','hl'],
['82','remove','hidden'],
['83','add','hl'],
['83','remove','hidden'],
['84','add','hl'],
['84','remove','hidden'],
['85','add','hl'],
['85','remove','hidden'],
['5','remove','hl'],
['5','add','hidden'],
['6','remove','hl'],
['6','add','hidden'],
['42','remove','hl'],
['42','add','hidden']
],
[
['77','remove','hl'],
['81','remove','hl'],
['82','remove','hl'],
['83','remove','hl'],
['84','remove','hl'],
['85','remove','hl']
]
]
The starting point is $\lib{prf-real+ro}$.
$\prfquery$ calls $\ro$, and we can inline the logic of $\ro$ into $\prfquery$.
$\ro$ is implemented by a lazy random dictionary $H$. We can partition $H$ into two separate dictionaries, based on whether the input starts with the prefix $\key$. Values of the form $\rotable[\key\|X]$ are now stored in $\prftable[X]$. Calls to $\ro$ made within $\prfquery$ \emph{always} include the $\key$ prefix, but the adversary's direct calls to $\ro$ may or may not.\FORMATTINGHACK{\pagebreak}
Modify $\ro$ to act as if its inputs never have a prefix $\key$. The library's behavior will change only in the bad event that the calling program calls $\ro$ on an input that begins with $\key$. We must later show that this bad event has negligible probability.
The value $\key$ is used \emph{only} to decide whether to trigger the bad event, so we can move the choice of $\key$ and all the bad event logic to the end of time without affecting its probability.\FORMATTINGHACK{\pagebreak}
$\lib{prf-real+ro}$
$\key \gets \bits^\secpar$
if
$\rotable[\key\|X]$ undefined:
$\prftable[X]$ undefined:
$\rotable[\key\|X] \gets \bits^n$
$\prftable[X] \gets \bits^n$
return
$\ro(\key \| X)$
$\rotable[\key\|X]$
$\prftable[X]$
if $A$ begins with $\key$:
write $\key \| X := A$
if $\prftable[X]$ undefined:
$\prftable[X] \gets \bits^n$
return $\prftable[X]$
else:
$\mathcal{A} := \mathcal{A} \cup \{ A \}$
if $\rotable[A]$ undefined:
$\rotable[A] \gets \bits^n$
return $\rotable[A]$
$\key \gets \bits^\secpar$
for each $A \in \mathcal{A}$:
if $A$ begins with $\key$: $\badvar := \mytrue$