\procedure{$\O{Reveal}(\n{ctr})$}{
\pcparse \O{unwrap}\left(\n{State}[\n{ctr}]\right) \pcas \left(\begin{array}{c}\n{U}, \n{u}, \n{V}, \n{ltk}, \n{acc}, \n{k}, \n{ni}, \pclb\n{nr}, \n{kmac}, \n{sid}, \n{mess}\end{array}\right)\\
\pcassert \n{acc} = \O{some}\left(\lit{true}\right) \\
\pcassert \n{RevTested}[\O{unwrap}\left(\n{sid}\right)] = \O{none}\left(\O{Boolean}\right) \\
 \n{RevTested}[\O{unwrap}\left(\n{sid}\right)] \gets \O{some}\left(\lit{false}\right)\\
 \pcreturn \O{unwrap}\left(\n{k}\right)\\
}
