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” (abstract, p. 1).
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 trace quantifiers and indexes predicates, functions, and updates with the selected execution. For example, the paper writes the election symmetry condition as
∀π∀π′. (voteAπ ↔ voteAπ′) → (Jwinner ↢ A()Kπ ↔ Jwinner ↢ A()Kπ′)
(Section I, p. 1). HyperTSLrel instead permits a predicate such as equality to range over two execution variables, which is more expressive but cannot generally be used by a strategy because the strategy sees only its current input stream (Section III, pp. 3–4).
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, pp. 5–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. The paper explicitly warns 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. 6).
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, pp. 6–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, pp. 9–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. A special local-determinism conjunct reduces the realizability-context check to Boolean SAT (Proposition VI.6, p. 10).
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. For each refinement, self-compose the machine and model-check the LTL body of the HyperLTL approximation. The first refinement satisfying the universal property is a valid implementation; because choices are only removed, at least one strategy for the original TSL property remains (Section VII, pp. 10–11). 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. 10).
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. 12). These are single reported runs, not 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. 12). The paper says runtime mainly depends on the number of choices tested, and also grows with formula and machine size (Section VIII-C, p. 12). The implementation is explicitly a prototype, and the authors suggest translating the unchanged LTL formula to an automaton once instead of on every nuXmv call (Section VIII-C, p. 12).
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 (Section X, p. 13). A numerical inconsistency is avoided here: Table I’s “only vote” machine is described as having two free-choice state/input combinations with two transitions each, hence 2²=4 refinements, while the text says the number of calls is the number of refinements tested and reports two calls for symmetry. That call count is therefore not the full Cartesian enumeration and should not be interpreted as 4 exhaustive checks.
Inference: For VL, the reusable idea is to synthesize or write a finite control skeleton, retain nondeterministic choices as explicit ghost data, and discharge relational requirements with a bounded self-composition proof. The product threat is high for agent-written verified Rust if the relational specification omits an execution, because Verus can prove the chosen formula while the contract violates an unmodeled trace relation. The threat is lower when every free choice and every quantified trace is represented in a finite certificate and the model checker or Verus proof checks that certificate.
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
Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.
Last edited: