\(\Fstore \) is \(\Frand \)’s companion: where one produces values and lets them be forgotten, the other takes values and holds them until they are. A party puts a value at an index, gets it back, and erases it; the leak reports what is still held. Together they are what Chapter 1 means by a protocol keeping no state on a machine tape — all randomness through \(\Frand \), all persistence through \(\Fstore \), each exposing what it holds through its own \(\op {Leak}\).
The fields. \(\Frand \)’s exactly, save the parameter: \(\PID \), \(\Ps \) and \(\admits \) parameters, \(\uses := \emptyset \), and \(\pars := \none \), a store reading none. Like \(\Frand \)’s, its state is shared across the parties it serves — one party may get what another put, which is what makes it a store rather than a per-party tape, and what Chapter 1 means by sharing being the point.
Three states, not two. An index is in one of three conditions, and the code keeps them apart on purpose. It is \(\unset \) if nothing was ever put there; it holds a value if something was put and not erased; and it is \(\none \) if it was put and then erased. The operation \(\opl {Put}\) accepts an index in either empty condition, so an erased index is reusable; \(\opl {Get}\) refuses only \(\unset \), so a get on an erased index is answered \(\none \) rather than refused. The distinction earns its place in the difference between those two answers: a caller can tell nothing was ever here from something was here and is gone, which is what makes erasure observable to the protocol that performed it rather than a silent hole. A store that hid the difference would refuse both alike and could not be asked whether an erasure had happened.
Functionality \(\Fstore \)
\(\PID \), \(\Ps \), \(\admits \), \(\uses := \emptyset \), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\op {Put}(i,x)\) from \(\id '\)
\(\id .\op {Erase}(i)\) from \(\id '\)
auto
\(\id .\op {Get}(i)\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
Two remarks on the code. The refusals are written as requires rather than as returns of \(\rej \), which is the same thing said in the framework’s own words: Section 3.6 answers a refused require with \(\rej \), so lines 3 and 8 give exactly the two refusals a store owes, and no core of this paper returns \(\rej \) by writing it. And \(\op {Erase}\) refuses nothing: erasing an index that holds nothing is a no-op that answers \(\ok \), because a protocol erasing defensively should not have to know whether there was anything there.