\procedure{$\O{Eval}(\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e})$}{
\pcassert (\n{LTK}[\n{h}] \neq \O{none}\left(\bin^{256}\right)) \\
\pcif \left(\begin{array}{c}\phantom{ \vee }\n{H}[\n{h}] = \O{some}\left(\lit{false}\right)\pclb \vee \neg \n{b}\end{array}\right) \pcthen\\
\pcind \n{k} \gets \O{unwrap}\left(\n{LTK}[\n{h}]\right)\\
\pcind \pcreturn \O{\n{prf}}(\n{k}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e})\\
\pcif \n{PRF}[\left(\begin{array}{c}\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e}\end{array}\right)] = \O{none}\left(\bin^{256}\right) \pcthen\\
\pcind\n{temp} \stackrel{id5}{\sample} \bin^{256}\\
\pcind \n{PRF}[\left(\begin{array}{c}\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e}\end{array}\right)] \gets \O{some}\left(\n{temp}\right)\\
\pcind \pcreturn \n{temp}\\
 \n{y} \gets \n{PRF}[\left(\begin{array}{c}\n{h}, \n{a}, \n{aa}, \n{c}, \n{d}, \n{e}\end{array}\right)]\\
 \pcreturn \O{unwrap}\left(\n{y}\right)\\
}
