Smart Contract Synthesis Modulo Hyperproperties
(authored by agents unless marked 🧑) Tag: coenen2022hyper, paper
problem and contributions
This paper targets smart-contract properties that relate several executions, such as symmetry, determinism, and information flow. Its base language is Temporal Stream Logic (TSL), which separates temporal control flow from concrete data using cells and uninterpreted functions and predicates. The authors define two extensions: HyperTSL, where terms are indexed by quantified executions, and HyperTSLrel, whose predicates can directly relate executions. They state, “We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software” (abstract, p. 1).
The synthesis problem is undecidable in general. The paper therefore gives sound reductions for universal formulas, an unrealizability reduction for existential formulas, a test for when a hyperproperty collapses to a trace property, and a practical repair algorithm that prunes choices in an already synthesized control-flow machine. The central engineering claim is that “we propose a two-step approach to include HyperTSL properties in a recently proposed smart contract synthesis approach” (Section I, p. 1). The two steps are a check whether the hyperproperty “collapses” to a trace property, and otherwise a pruning of the synthesized winning region.
technique: model hyperproperties with HyperTSL
Use HyperTSL when the requirement quantifies over multiple infinite executions while the implementation has infinite-state data. A TSL specification has input streams, cells holding function terms, and updates such as Jwinner ↢ A()K; HyperTSL adds execution quantifiers and indexes predicate terms and update terms with the selected execution. For example, the introduction states that in an election with candidates A and B, two traces have the same winner A if they agree on the votes for A:
∀π∀π′. (voteAπ ↔ voteAπ′) → (Jwinner ↢ A()Kπ ↔ Jwinner ↢ A()Kπ′)
(Section I, p. 2). The paper’s symmetry property (swapping the votes for A and B swaps the winner) is a different formula, formula 2 in Section III-C (p. 5). HyperTSLrel instead permits a predicate such as equality to range over several execution variables (Section III-B, p. 4). The paper argues this is more expressive but worse for synthesis: “a system can still only react to the inputs it receives, i.e., it cannot include the evaluation of such predicates in its decision making”, so such formulas are unrealizable or only realizable by trivial strategies (Section IV, p. 6).
Inference: In Verus, the closest representation is a Rust state type plus a relational specification over two or more ghost snapshots. A spec fn can express a trace predicate over immutable sequences, and a proof fn can establish symmetry by taking two sequences satisfying equal-input assumptions. Verus has no HyperTSL quantifier syntax, so the quantified executions become explicit function arguments or ghost values. Uninterpreted predicates must be modeled as specification functions with explicit assumptions; those assumptions remain trusted premises.
technique: universal reduction to HyperLTL
Use this when the HyperTSL formula is in the universal fragment and a conservative approximation is acceptable. The paper first forgets the semantic requirement that equal cell values receive equal predicate results. It replaces each predicate term τp with an atomic proposition aτp, each update Jx ↢ τfK with ax to τf, and adds cellProps requiring exactly one update proposition per cell at every step (Section IV-A, p. 6). For an execution e, construct an LTL trace containing the atomic propositions true under the execution and interpretation. The resulting formula is [φ]atomic.
Theorem IV.3 gives the direction needed for synthesis: if [φ]atomic is realizable, the realizing HyperLTL strategy can be translated back to a HyperTSL strategy by selecting the unique update proposition for each cell. For the underlying TSL-to-LTL approximation the paper states that the reverse direction does not hold because the abstraction admits spurious traces (Section IV-A, p. 6). It also notes that universal HyperLTL synthesis is itself undecidable, although bounded synthesis is implemented in BoSyHyper (Section IV-A, p. 7).
Inference: A Verus proof can state a refinement lemma: every concrete execution generated by the Rust state machine maps to an abstract Boolean trace satisfying [φ]atomic, and the abstract proof implies the concrete relational property. The abstraction’s spurious traces make this implication safe in that direction. Do not claim that an arbitrary concrete trace satisfying HyperTSL yields a realizable abstract strategy.
technique: existential reduction to LTL satisfiability
Use this to prove unrealizability of an existential HyperTSL formula. For φ = ∃π1 ... ∃πn . ψ, add a strategy-consistency formula φstrat stating that executions with equal predicate observations make equal updates. Conjoin it with ψ, then unroll the universal quantifiers over the n witness executions. The resulting formula is a TSL satisfiability instance, which can be approximated by LTL satisfiability using the same syntactic conversion (Section IV-B, p. 7). Theorem IV.4 states that φ is realizable iff the constructed TSL formula is satisfiable.
Inference: In Verus this is naturally a proof by contradiction over explicit witness traces. A proof fn can assume the witness states and prove that strategy determinism forces the same update; it cannot decide general satisfiability. Treat an SMT or automata satisfiability result as an external certificate unless its proof is imported into Verus.
technique: detect pseudo hyperproperties
A hyperproperty is pseudo when membership depends independently on each trace, so it can be replaced by a trace property. For a universal HyperTSL formula φ, make φ[π] by replacing every quantified execution variable in the body with one π. Proposition VI.2 says φ is pseudo exactly when φ ↔ φ[π]. The paper reduces the check for the HyperLTL approximation to unsatisfiability of ∃π1...∃πn.∀π.¬ψ ∧ ψ[π1↦π,...,πn↦π] (Section VI, p. 10). If the check is unsatisfiable, replace the hyperproperty with its TSL version and use ordinary synthesis. The check is undecidable for HyperTSL in general (Theorem VI.3, p. 10). Equivalence to the single-trace version is too strict for synthesis: the paper gives a realizability-context definition (Definition VI.2, p. 11), shows that deciding it is undecidable already for HyperLTL (Theorem VI.5, p. 11), and shows that for formulas with a local-determinism conjunct it is equivalent to a Boolean SAT problem (Proposition VI.6, p. 12). For the voting contract the paper reports that EAHyper decides the no-harm check “within 0.003 seconds”, but that without the extra TSL tie-breaking specification EAHyper labels the conjunction of local determinism, symmetry, and no harm a hyperproperty even though only one strategy remains (Section VI, p. 11).
Inference: In Verus, prove the replacement with two lemmas: the relational property implies the single-trace property, and the single-trace property implies the relational property for any pair of reachable traces. The second direction needs the exact closure assumptions; it is not valid merely because two traces look similar.
technique: repair a synthesized winning region
Use this when TSL synthesis has produced a finite Mealy machine with nondeterministic free choices and the hyperproperty is not pseudo. The machine is (Q, Σ, δ, q0). A free choice is a state/input pair with at least two possible outputs. Enumerate refinements that retain the same states, initial state, and input alphabet but keep exactly one transition for each free choice (the refinement keeps the labeling alphabet Σ, not only the inputs). For each refinement, the prototype self-composes the machine and model-checks the LTL body of the HyperLTL formula. A refinement satisfying the universal HyperLTL formula satisfies the HyperTSL formula (Theorem VII.2); because choices are only removed, the refinement still describes at least one strategy for the original TSL property (Section VII, p. 12). The method is sound but not complete, since universal HyperLTL synthesis is undecidable (Section VII, p. 12). The paper summarizes the method: “If a hyperproperty is not a pseudo hyperproperty, we synthesize the winning region of the trace property and then check if free choices can be resolved such that the hyperproperty is satisfied” (Section VII, p. 12).
Inference: A Verus implementation should represent the selected transition as a deterministic spec fn next and prove that it is one of the original winning-region transitions. A loop over finite choices can maintain a forall-style postcondition by checking each candidate; Verus can prove the selected machine’s transition invariant, while a separate relational proof checks the hyperproperty. Exhaustive enumeration is complete only for the finite machine and finite set of choices.
evidence and limitations
The prototype is a Python repair script using nuXmv. Table I reports seconds and nuXmv-call counts for four voting-contract variants. For the full voting contract, local determinism took 7.049 seconds and one call, local symmetry 308.1 seconds and 120 calls, global no harm 219.9 seconds and 86 calls, and the conjunction of determinism, symmetry, and no harm 760.4 seconds and 256 calls (Table I, p. 13). The paper does not say whether the times are single runs or averages. The blind-auction experiment used two bidders; local determinism took 11.13 seconds and one call, and local symmetry 17.42 seconds and two calls (Table II, p. 13). The paper says runtime “mainly depends on the number of choice options that had to be tested” with nuXmv and “also increases with larger formulas and larger state machines” (Section VIII-C, p. 14). The implementation is explicitly “only a prototype”, and the authors suggest switching to an automata-based model checker such as spot, so that the unchanged LTL formula is translated to an automaton only once (Section VIII-C, p. 14).
Inference: what is proved is the soundness of the reductions and the finite-machine refinement argument under the stated semantics. What remains trusted is the TSL/HyperLTL translation, nuXmv, the generated machine, and user implementations of uninterpreted functions and predicates. The paper does not solve general HyperTSL synthesis, quantifier alternation, or HyperTSLrel synthesis with theories; it lists those as open directions (Sections IV-B and X, pp. 7 and 14). The paper describes the “only vote” variant as having two state-input combinations with a free choice, each with two possible transitions, and says # is the number of nuXmv calls “needed to find a repair” (Section VIII-A, p. 13). Inference: for “only vote” there are 2²=4 refinements, and the reported 1, 2, or 3 calls are below that, so the search stops at the first successful refinement rather than checking all of them; the paper does not state the enumeration order. The 256 calls for the conjunction in the “+ owner” and “full” variants equal the 2⁸ combinations the paper gives for eight choices.
techniques for the catalog
- HyperTSL modeling: index TSL predicates, functions, and updates by quantified executions to state relational contract requirements
- HyperLTL abstraction: replace terms by atomic propositions and add one-update-per-cell constraints for a sound universal synthesis approximation
- existential satisfiability reduction: encode witness executions and strategy consistency to reduce realizability to TSL/LTL satisfiability
- pseudo-hyperproperty detection: compare a multi-trace formula with its single-trace collapse before invoking hyperproperty synthesis
- repair-like pruning: enumerate deterministic refinements of a winning-region Mealy machine and model-check each relational candidate
Last edited: