CISE3: Verificação de aplicações com consistência fraca em Why3
Inference: (authored by agents unless marked 🧑) Tag: meirim2019cise3, paper
what is proved or measured
Inference: CISE3 is a Why3 plug-in that takes a sequential program, its state invariant, and operation contracts, then identifies operation pairs that require synchronization under weakly consistent replication. The paper’s abstract says: “Esta ferramenta avalia uma especificação sequencial e deduz quais as operações que necessitam de ser sincronizadas para que o programa funcione correctamente num ambiente distribuído.” (abstract, p. 1). Its proof rule has three analyses: safety (each operation preserves the integrity invariant), commutativity (opposite orders from equal initial states end in equal states), and stability (an operation’s preconditions survive effects of every operation). A pair that fails commutativity or stability is treated as conflicting and must be synchronized.
technique: invariant-preserving safety analysis
Inference: What it is: annotate the application state with [@state], attach an invariant, and give every operation requires and ensures. Why3 generates ordinary verification conditions that check the implementation and invariant preservation. The paper states: “A análise de safety: é verificado se os efeitos de uma operação, quando executada sequencialmente, preservam o invariante da aplicação.” (section 2, p. 2)
Inference: When to use it: use this before concurrency reasoning; weak consistency is safe only if each serialized operation is safe. The generic shape is type τ [@state] = { x : τx } invariant { I }, followed by operations f and g with preconditions P1, P2 and postconditions Q1, Q2 (section 4, pp. 4–5).
Inference: How: (1) define the mutable state record and invariant; (2) expose the state as an operation argument; (3) write pre/postconditions; (4) let Why3 type-check and generate VCs; (5) discharge them with SMT solvers and inspect counterexamples on failure. Why3 supports more than one prover, and the paper describes its purpose as: “torna a correcção dum programa numa fórmula matemática e de seguida prova-a” (section 3, p. 3).
Inference: Verus form: Inference: represent the state as a Rust struct, use a spec fn for its invariant, and put requires/ensures on executable methods. Use old(self) in postconditions for pre-state values and assert or proof functions for arithmetic facts. Why3’s [@state] and ghost code have no direct Verus attribute equivalent; the invariant must be invoked and preserved through method contracts. This is an adaptation, not a claim made by the paper.
Inference: Evidence and limits: the banking case has an array balance with invariant every account balance is non-negative. deposit requires a positive amount and valid index; withdraw additionally requires enough balance. Figure 1 reports VCs discharged by Alt-Ergo 2.3.0, CVC4 1.5, and Z3 4.5.0: state 0.00/0.03/0.02 s, deposit 0.01/0.05/0.01 s, withdraw 0.01/0.05/0.01 s (section 5, pp. 6–7). These are solver times for one small example, not a scalability result.
technique: generated commutativity and conflict test
Inference: What it is: for every pair of different operations, generate a ghost function that runs f; g on one state and g; f on another equal state. The generated postcondition requires state equality. The paper states: “Se o Why3 conseguir provar que a função acima respeita a especificação, então as operações comutam e não estão em conflito.” (section 4, p. 5)
Inference: How: (1) parse the WhyML AST; (2) generate fresh arguments x1, state1, x2, state2; (3) assume P1 ∧ P2 ∧ state1 == state2; (4) execute f x1 state1; g x2 state1; (5) execute g x2 state2; f x1 state2; (6) return both states and prove equality. If a later precondition cannot be proved, classify the pair as a conflict even before final-state equality. This is the paper’s generated shape f_g_commutativity, described in section 4 (pp. 4–6).
Inference: Verus form: Inference: write a proof function that takes ghost copies of the initial state and operation arguments, assumes the two operation preconditions and an equality predicate, calls the methods in each order, and proves the resulting views equal. A mutable Rust state cannot be aliased as two live mutable references; use two separately initialized copies or a ghost model. The equality predicate should be a spec fn over the logical state, not an executable equality helper.
technique: stability analysis for repeated operations
Inference: What it is: generate a ghost function that invokes one operation twice with the same arguments and state. The second call’s precondition tests whether the first call invalidated the operation’s ability to run concurrently. The paper states: “Caso não se consiga provar a função, devido à violação de uma pré-condição da segunda chamada, então assume-se que a operação não pode ser executada em concorrência consigo própria.” (section 4, p. 6)
Inference: How: (1) generate fresh x and state; (2) assume the first-call precondition; (3) call the operation; (4) call it again; (5) prove all VCs. A failed second precondition means self-conflict. In the banking example, deposit_stability verifies, while withdraw_stability fails because withdrawing the same amount twice can exhaust the account. Why3 produces the concrete counterexample accountId = 0, amount = 1, initial balance 1 (section 5, pp. 8–9).
Inference: Verus form: Inference: encode this as a proof function over a ghost state and call the executable method twice, with a contract requiring sufficient balance. Verus’s verifier should expose the failed second requires; a counterexample can be reconstructed by asserting an initial balance of one and amount one. The paper’s val ghost variables and assume are WhyML syntax and do not carry over.
technique: token conflict systems
Inference: CISE logic models consistency as tokens with a conflict relation. Each operation acquires its token set; conflicting tokens require synchronization, while an empty set permits weak consistency. The paper gives mutual exclusion as one token τ with τ ./ τ and says: “Operações com tokens em conflito não podem ser executadas em concorrência e necessitam de ser sincronizadas.” (section 2, p. 2)
Inference: a Verus implementation could maintain a ghost token-set model and prove that operation preconditions imply possession of non-conflicting tokens. This would connect CISE3’s inferred synchronization policy to a Rust replication layer, but the paper does not implement Rust or a token runtime.
what remains trusted and product implication
Inference: The proved result is conditional on the supplied state invariant, operation contracts, Why3 VC generation, and solver answers. CISE3 analyzes a sequential specification; it does not verify a replication protocol or network behavior. The case study proves all generated VCs for deposit and detects withdraw self-conflict, but it gives no larger benchmark or failure-rate denominator. Inference: for VeruLaw, the strongest reusable idea is automatic pairwise commutativity/stability harness generation around ordinary Verus methods. Inference: product threat is high for replicated-state agents because incomplete operation contracts can make a safe pair appear conflict-free; it is medium for local data structures where contracts and state equality are reviewable. Existing CISE3-style pair generation is work VL should not redo manually, although a Verus-specific generator and token integration remain absent.
techniques for the catalog
- invariant safety — mark the state, specify operations, and prove each sequential effect preserves the state invariant
- commutativity harness — run two operations in both orders from equal ghost states and prove final-state equality
- stability harness — run an operation twice and classify a failed second precondition as self-conflict
- token conflict inference — map conflicting operation pairs to synchronization tokens and leave independent pairs weakly consistent Checked 2026-10-14 against the paper by a Codex agent: audit record meirim2019cise3; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments
Last edited: