We will often need to sanitize simulator outputs, so attacks do not affect ideal functionalities too adversely. In honest-majority settings, for instance, we typically sanitize a \(\none \) output to a non-\(\none \) one to preserve liveness. We write such a procedure \(\San [\Clean ](v; c)\), where \(\Clean \) is a predicate on a value together with whatever context it consults, and replace a simulator output \(v\) by \(v' \gets \San [\Clean ](v; c)\), which operates as below unless stated otherwise. The context \(c\) after the semicolon lists the functionality state the predicate reads; it is read-only, and different predicates take different contexts.
Sanitizer \(\opdef {San}[\Clean ]\)
predicate \(\Clean \), value \(v\), context \(c\)
So sanitization acts only when \(\Clean (v; c)\) fails, and what it returns then satisfies \(\Clean \).1 Our sanitizers need no more than read-only access to the functionality state. How line 3 picks is part of the specification — the picked value reaches the caller, so different rules are observably different functionalities — and we fix the lexicographically first good value throughout. The choice matters less than it looks: the pick surfaces only when the slot’s own answer fails \(\Clean \), and an adversary preferring some particular good value may simply submit it.