Two properties, and they are the two halves of what a store is for. \(\opl {FinKeep}\), persistence: a value put and not erased is the value got back. \(\opl {FinGone}\), erasure: a value erased is not got back. Both take the search reading, and both are two finalizations of one game — they read the same trace of the same three relays and differ in the verdict alone, which is the test Section 17.2 gives for sharing a shell.
They are played over \(\gamma := \{\Gm \} \cup \{\Fstore \}\) with \(\Fstore .\admits := \{\Gm .\PID \}\) pinned and \(\Fstore .\Ps \subseteq \Gm .\Ps \), tightness as before and for the same reason: a put the game does not see is a value the verdict cannot account for. The relays refuse the root, for Section 13.2’s reason: both verdicts compare a got value against a put one, so a \(\rej \) of the game’s own making in the trace would be read as a value and could win either.
Game shell over \(\Fstore \); the finalizations follow
\(\PID := (\Gm .F,0,0)\), \(\Ps := \Fstore .\Ps \cup \{Z\}\), \(\admits := \Zpid \), \(\uses := \{(\Fstore ,\serves _{\Gm })\}\), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\opdef {Put}(i,x)\) from \(\id '\)
\(\id .\op {Erase}(i)\) from \(\id '\)
auto
\(\id .\opdef {Get}(i)\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
The finalizations of \(\Gm \); the shell over \(\Fstore \) is shared
\(\id .\opdef {FinKeep}()\) from \(\id '\) (persistence)
\(\id .\opdef {FinGone}()\) from \(\id '\) (erasure)
The verdicts, in words. The finalization \(\op {FinKeep}\) returns \(1\) if some get answered other than the value the last successful put at that index left there, no erasure intervening. The finalization \(\op {FinGone}\) returns \(1\) if some get answered exactly the value an erasure was supposed to have removed, no put having restored it in between. Both read the trace’s order, as Section 17.2’s steadiness does and for the same reason: a store is a claim about what happens between one call and the next, and between is an ordering.
Proposition 14.1 (\(\Fstore \) has both properties). For \(\op {Fin}\) either of \(\op {FinKeep}\) and \(\op {FinGone}\), for every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {Fin}}] = 0\). So \(\{\Fstore \}\) has each property within \(0\) against \(\bigl (\ZenvSet _{\gamma ,\gamma },\Xset \bigr )\) in the sense of Definition 5.8, for \(\Xset \) the class of all occupants.
Proof. One invariant carries both properties: \(\V {L}[i]\) changes only inside a call the trace records, and to the value that call names. It comes from tightness (no caller but the game passes the guard), from the game’s own wrapper intercepting at a corrupt party before any core runs, and from \(\Fstore \)’s cores placing no call, so nothing runs between a relay’s call and its return and entries append in execution order. Both properties are then read off it by the same move: assume the verdict’s conjuncts, and track which lines could have written \(\V {L}[i]\) between the entries named. Persistence turns on the put refusing an occupied index, so no later put can intervene unrecorded; erasure turns on \(\bits \) containing neither \(\none \) nor \(\unset \), so the value a get returns after an erase cannot be the value put before it. Everything rests on one invariant: \(\V {L}[i]\) changes only inside a call the trace records, and to the value that call names. By tightness no caller but \(\Gm \) passes \(\opl {Guard}\)’s line 2 at \(\Fstore \), and \(\Gm \) reaches it only through the shell’s three relays (lines 5, 11 and 15); at a corrupt party the game’s own wrapper intercepts a step earlier and no core of \(\gamma \) runs at all (Remark 5.4). \(\Fstore \)’s cores place no call, so no other machine of \(\gamma \) runs between a relay’s call and its return, and entries append in execution order. Line numbers below name \(\Fstore \)’s own cores unless said otherwise.
For persistence: suppose \(e_j = (\atom {put},\cdot ,i,x,\ok )\) and \(e_k = (\atom {get},\cdot ,i,y)\) with \(j < k\) and no \(\atom {erase}\) at \(i\) between. The put answered \(\ok \), so \(\op {Put}\)’s line 3 passed and its line 4 set \(\V {L}[i] \gets x\). Only that line and \(\op {Erase}\)’s line 6 write \(\V {L}[i]\), and by the invariant each is recorded: no \(\atom {erase}\) entry at \(i\) lies between, and a further \(\atom {put}\) at \(i\) answering \(\ok \) cannot lie between either, line 3 refusing an occupied index and \(\V {L}[i]\) being occupied from \(j\) on. So \(\V {L}[i] = x \neq \unset \) still at \(k\), \(\op {Get}\)’s line 8 passes, and its line 9 returns \(x\); hence \(y = x\) and the verdict at line 22 gives \(0\).
For erasure: suppose \(e_j = (\atom {put},\cdot ,i,x,\ok )\), \(e_k = (\atom {erase},\cdot ,i)\) and \(e_l = (\atom {get},\cdot ,i,x)\) with \(j < k < l\) and no successful \(\atom {put}\) at \(i\) between \(k\) and \(l\). \(\op {Erase}\)’s line 6 set \(\V {L}[i] \gets \none \) at \(k\), and by the invariant the only line that could restore a value is \(\op {Put}\)’s line 4 inside a recorded \(\atom {put}\) at \(i\) answering \(\ok \), which the hypothesis excludes. So \(\V {L}[i] = \none \) at \(l\), and \(\op {Get}\)’s line 9 returns \(\none \). Now \(x \neq \none \): \(x\) was written by line 4 from a \(\op {Put}\)’s argument, and \(\bits \) contains neither \(\none \) nor \(\unset \). Hence the get did not answer \(x\), contrary to \(e_l\), and the verdict at line 29 gives \(0\). □
Both transfer by Corollary 5.11 with nothing to discharge beyond its four standing conditions: \(\Fstore \)’s cores place no call at all, so the responsive-call hypothesis is met the cheap way and dummy completeness is untouched, exactly as for \(\Frand \) and \(\Gpki \). The three functionalities that ask the adversary nothing are the three that pay nothing, and the pattern is not a coincidence — what Section 17.2 charges the clock is the notification, and a functionality with no notification has no bill.