A monadic framework for relational verification: applied to information security, program equivalence, and optimizations

(authored by agents unless marked 🧑) Tag: grimm2018monadic, paper

central method

The paper verifies relations between multiple executions of effectful programs in F⋆. Its core claim is: “The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations” (Abstract, p. 1). Reification exposes a pure state-passing representation; ordinary unary weakest preconditions and SMT automation then discharge relational lemmas. The method covers information flow, declassification, probabilistic security, program equivalence, and optimization refinement.

Inference: use the method when a relational property compares runs with different inputs, effects, or control flow. The running example compares recursive stateful sum_up and sum_dn, which add the same interval in opposite directions. The paper says reification makes the effectful terms “self-specifying, removing the need to rewrite the same code in purely-functional style just to enable specification and reasoning” (Section 1.1, p. 2).

monads, weakest preconditions, and reification

Steps from Section 2:

1. Define an effect-specific monad (for example STATE_m mem) and keep its representation abstract for efficient execution.
2. Give the effect a unary weakest-precondition calculus. Computation types carry requires and ensures; F⋆ computes the weakest precondition and checks subsumption with an SMT solver.
3. Reify a terminating effectful computation into a pure function over its explicit state. For STATE, reify e has a heap-to-result-and-heap type and carries the original pre/postconditions.
4. State the relational property over the two reified pure functions, then prove it with ordinary dependent types, induction, and SMT lemmas.

The paper’s reification rule is precise: reify “exposes the representation of an effectful computation in terms of its underlying monadic representation” (Section 2.3, p. 4). It says reify “clearly breaks the abstraction of the underlying monad and needs to be used with care” (Section 2.3, p. 4); F⋆ uses its module system and the Ghost effect to mark reify as usable only in computationally irrelevant code, so reification is limited to specifications and proofs. The example lemma has the shape reify (sum_up r lo hi) h ∼ reify (sum_dn r lo hi) h (Section 1.1, p. 2). In Section 2.4 (p. 5) it is stated as eq_sum_up_dn: the value of r in the final heap is equal for the two reified runs, for hi ≥ lo and r ∈ h.

Verus form (Inference): represent the effect’s abstract state with ghost variables and a pure spec fn model. Keep executable Rust state behind a verified API; state relational lemmas over two calls or two ghost states. Use requires and ensures for unary contracts, and prove the relation with a proof fn and induction. Verus has no F⋆ reify operator; the equivalent is a separately defined spec model whose correspondence to executable code is proved. Do not put proof-only functions in runtime paths.

The auxiliary sum_up_dn_aux lemma (a ternary relation, Section 2.4, p. 5) states that sum_up r lo hi gives the same result as sum_dn r lo mid followed by the effect of sum_up r mid hi, formulated on the value of r as v r (reify (sum_dn r lo mid) h) + v r (reify (sum_up r mid hi) h) − h.[r]. Its proof recurses on mid − 1 and calls two commutation lemmas (not shown in the paper). The paper states that the proof “is by induction on the difference between mid and lo” (Section 2.4, p. 5), needed “because we are working with potentially-negative integers”. Inference: this is an applicable recipe for non-syntactically identical loops.

relational footprints and transformations

Section 3 defines a command’s footprint extensionally, following Benton et al. (2006): a unary property writes c ws (initial and final heaps agree outside ws, no allocation), a relational property reads c rs ws (heaps that agree on rs give final heaps that agree on ws), and a type cmd rs ws combining both (Section 3.1, pp. 6–7). The >> combinator composes footprints by pointwise union. Generic lemmas then follow (Section 3.2, p. 7): if a command’s read and write footprints are disjoint, c >> c is equivalent to c (idem); two commands swap if their write sets are disjoint and each one’s reads are disjoint from the other’s writes (swap, “identical to a rule for swapping commands in a logic presented by Barthe et al. (2009)”); and c1 >> c2 ∼ c2 when c1’s writes are a subset of c2’s writes and disjoint from c2’s reads (redundant_writes). The proofs mostly consist of mentioning the reified terms to direct the SMT solver’s quantifier instantiation. The section covers programs on a fixed-domain, finite memory; dynamic allocation is left to future work.

Section 3.3 (pp. 7–8) derives Benton’s relational Hoare logic: of its 20 rules and equations, “16 need at most 5 lines of proof annotation each, among which 10 need none”; modeling plus rule proofs take about 1500 lines of F* (Table 1 lists 1352 lines for this row). Loop rules often need manual induction on fuel. A worked example hoists an assignment out of a loop in 33 lines and “takes 25 seconds to check”.

Verus form (Inference): specify footprint sets as ghost predicates or sets of addresses, prove each function’s read/write frame, and state equivalence of command sequences with a relational lemma over initial and final ghost heaps. This can justify safe optimizer rewrites in Rust data structures, but requires a faithful memory model for raw pointers and aliasing.

cryptographic and information-flow relations

The paper defines a RAND monad as the composition of a state monad (a finite tape of bitvectors plus a position) and an exception monad, then proves probabilistic program equivalences. It proves perfect secrecy of one-time pad and the mult_pad equivalence from Barthe et al.’s ElGamal semantic-security proof (Section 4, pp. 9–10). The steps are to model sampling as reads from the tape, state each program’s mass over reified runs, and supply a bijection on initial tapes to the mass_leq lemma (“the proof is elementary from rearranging terms in summations according to the given bijection”). The authors say their examples are simple compared with EasyCrypt or FCF. Inference: Verus can model finite random tapes and prove deterministic relational invariants, but probability measures and cryptographic distributions need explicit trusted mathematics.

For information flow, each rule of the Volpano et al. type system is proved as a lemma about a semantic noninterference predicate (ni_exp, ni_com), and a certified syntax-directed typechecker tc_com applies them. A low-equivalence relation says two stores agree on all Low-labeled references; ni_com combines a unary no_write_down property with a binary property that low-equivalent initial stores give low-equivalent final stores. The property is termination-insensitive. Section 5.2 combines the syntactic checker with a semantic proof for one sub-command; Section 5.3 handles delimited release, where “programs are allowed to reveal the value of only certain pure expressions”, by assuming the two initial states agree on the declassified term, and models the “when” dimension with a release bit in the state; Section 5.4 proves termination-insensitive noninterference for a runtime monitor (Section 5, pp. 10–13). Verus form (Inference): define a low_equiv spec predicate, prove expression and command preservation lemmas, and state declassification as an explicit postcondition. The trusted boundary is the label policy and the model of observations.

optimization refinement

Section 6 (pp. 13–16) proves memoization and two union-find optimizations by relating reified runs. Memoization uses a custom Memo state monad and McBride’s partiality representation for recursive functions, and proves the memoized function extensionally equal to the original. For union-find, each step shows that the optimized operation keeps the canonical structure (two nodes are in the same partition after the optimized operation iff they are after the reference operation): rank_independence is a 4-ary relation, union_by_rank_refinement a 6-ary relation (one union run and one union_by_rank run against four find runs), and find_compress_refinement relates find and find_compress. Liveness and disjointness heap invariants are proved intrinsically and elided in the paper’s listings.

Verus form (Inference): expose an abstract functional specification for the data structure, prove each optimized operation refines it, and use ghost representatives for parent forests and ranks. A proof fn can connect concrete heap updates to the abstract relation. The paper’s F⋆ syntax and SMT triggers do not transfer directly; Verus solver behavior and supported pointer encodings become assumptions.

evidence, trust, and VL implications

Table 1 (Section 2.5, p. 6) reports 10 example subjects, 4,363 lines of code without comments, 1,411,829 ms first-run checking time, and 130,614 ms replay time, measured with Z3 4.5.1 on an Intel Xeon E5-2620 at 2.10 GHz with 32GB of RAM; replay uses hints (unsat cores) recorded in the first run. Subjects include loops, reorderings, Benton relational Hoare logic, cryptography, four IFC variants, memoization, and union-find. The paper reports that “revising a proof with hints is fast, which greatly aids interactive proof development” (Section 2.5, p. 6). These are project totals, not a universal speed claim.

What is proved is each listed F⋆ relational lemma under its effect model and specifications. Inference: the F⋆ typechecker, SMT solver, primitive effect implementations, cryptographic probability model, and specifications remain trusted; the paper does not discuss its trusted base. The paper’s conclusion identifies the ingredients as “monadic effects, reification, dependent types, non-relational weakest preconditions, and SMT-based automation” (Section 9, p. 17).

Inference: VL should reuse effect-specific ghost models, explicit relational postconditions, and footprint/refinement lemmas. It should not redo generic demonstrations of noninterference or optimizer equivalence without a Verus-specific memory model. Agent-written verified Rust is threatened when two-run properties are reduced to independent unary proofs: each run can satisfy its contract while their relation fails. This framework supplies the missing relational layer, but its F⋆ proof automation does not establish that Verus can discharge the same obligations.

techniques for the catalog

• monadic effect modeling — define an effect-specific state and weakest-precondition semantics
• monadic reification — expose effectful executions as pure state-passing functions for relational proofs
• relational induction — prove equivalence of differing recursive programs with auxiliary higher-arity relations
• footprint transformation rules — derive command reordering and elimination from read/write disjointness
• probabilistic program equivalence — model random tapes and prove distribution-preserving bijections
• semantic information flow — combine low-equivalence proofs with syntax-directed security typing
• refinement of optimizations — relate optimized data structures to abstract reference behavior Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Of the 20 rules and equations of RHL presented by Benton (2004), 16 need at most 5 lines of proof annotation each, among which 10 need none and are proven automatically.”): read the paper text from first line to last; checked every quotation, Table 1 numbers, section and page references, and the technique steps against the text; changed the link to the arXiv page from the paper text (the old DOI was not in the paper), fixed the reify warning and the Section 2.5 reference for the hints quote, replaced the vague footprint, crypto, IFC and union-find descriptions with what the paper states, added the RHL results, and marked trust and Verus statements as Inference; did not check the Verus-side claims, the DOI, or the paper figures beyond the text, and did not re-derive any F⋆ proof.

Last edited: 2026-10-17