Automated Bisimulation Tactic

This file provides tactics for automatic bisimulation proofs in pRHL, analogous to EasyCrypt's sim tactic.

Main tactics

• ssprove_sim - automatically prove equivalence by structural matching
• ssprove_sim? - like ssprove_sim, but also emits a Try this: suggestion with the explicit script of steps that fired
• ssprove_sim_bij f - sim with explicit bijection for sampling steps
• ssprove_sim_step - one step of sim (match heads, apply rule)

What EasyCrypt does

EasyCrypt's sim automatically proves pRHL equivalences by structurally matching both programs and maintaining a conjunction of equalities. It works backwards, applying coupling rules for each matching operation pair:

Both sides have	Rule applied
sample T	diagonal coupling
get l	synchronized get
set l v	synchronized set
pure v	same return
sample + bijection	bijection coupling
bind c k	decompose + recurse

How it maps to CatCrypt

We compose existing tactics in the same structural matching order:

1. Normalize both sides (code_simpl)
2. Try to match heads and apply appropriate relational rule
3. Recurse on continuations
4. Close remaining goals with automation

References

• EasyCrypt: sim tactic
• CatCrypt/Rocq: r_reflexivity_alt procedure

Additional Rules for Sim

These rules complement the existing sync rules for use in bisimulation.

theorem CatCrypt.Relational.rHoare_get_sync_eq {l : Core.Location} : rHoare eqPre (Core.SPComp.get l) (Core.SPComp.get l) eqPost

Synchronized get on two possibly different locations, with the precondition implying both heap equality and location agreement.

This rule is used by sim when both sides do get l for the same l and the precondition implies the heaps agree on l.

theorem CatCrypt.Relational.rHoare_set_sync_eq {l : Core.Location} {v : l.ty} : rHoare eqPre (Core.SPComp.set l v) (Core.SPComp.set l v) fun (x : Unit) (h₁ : Core.Heap) (x_1 : Unit) (h₂ : Core.Heap) => eqPre h₁ h₂

Synchronized set on the same location with the same value, preserving heap equality.

theorem CatCrypt.Relational.rHoare_sample_same_eq (α : Type) [Fintype α] [Nonempty α] : rHoare eqPre (Core.SPComp.sample α) (Core.SPComp.sample α) eqPost

Sampling the same type preserves heap equality and gives equal values.

theorem CatCrypt.Relational.rHoare_ret_same_eq {α : Type} {a : α} : rHoare eqPre (pure a) (pure a) eqPost

Return same value with heap equality.

theorem CatCrypt.Relational.rHoare_bind_eq {α β : Type} {c₁ c₂ : Core.SPComp α} {f₁ f₂ : α → Core.SPComp β} (hc : rHoare eqPre c₁ c₂ eqPost) (hf : ∀ (a : α), rHoare eqPre (f₁ a) (f₂ a) eqPost) : rHoare eqPre (c₁.bind f₁) (c₂.bind f₂) eqPost

Bind with eqPost intermediate and eqPost final gives eqPost.

Register core rules with @[rspec]

RSpec Lookup Tactic

def CatCrypt.Tactics.tacticSsprove_rspec : Lean.ParserDescr

ssprove_rspec queries the @[rspec] discrimination tree for a lemma matching the current goal and applies it.

Equations

• CatCrypt.Tactics.tacticSsprove_rspec = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_rspec 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_rspec" false)

Reorder Tactic

def CatCrypt.Tactics.tacticSsprove_reorder : Lean.ParserDescr

ssprove_reorder tries to commute mismatched head operations to align both sides of a pRHL judgment. It applies reorder rules from CatCrypt.Relational.Reorder as a fallback when heads don't match.

Tries (in order):

1. rHoare_sample_comm — both sides sample but in opposite type order
2. rHoare_reorder_pure_l — commute IsPure past anything on LHS
3. rHoare_reorder_pure_r — same for RHS
4. rHoare_sample_past_get_l — commute sample past get on LHS
5. rHoare_sample_past_set_l — commute sample past set on LHS

Equations

• CatCrypt.Tactics.tacticSsprove_reorder = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_reorder 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_reorder" false)

Sim Tactics

def CatCrypt.Tactics.tacticSsprove_sim_step : Lean.ParserDescr

ssprove_sim_step matches the head operation on both sides and applies the appropriate relational rule.

It tries (in order):

1. Same return value → rHoare_ret_same
2. Same sample → rHoare_sample_same
3. Synchronized get → rHoare_get_sync
4. Synchronized set → rHoare_set_sync
5. Bind decomposition → rHoare_bind

After applying a rule, it introduces continuation variables if needed.

Equations

• CatCrypt.Tactics.tacticSsprove_sim_step = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_sim_step 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_sim_step" false)

def CatCrypt.Tactics.tacticSsprove_sim : Lean.ParserDescr

ssprove_sim automatically proves pRHL equivalences by structurally matching both programs.

The tactic:

1. Normalizes both sides (code_simpl)
2. Repeatedly matches heads and applies coupling rules
3. Tries to close remaining goals with automation

This handles most cases where both programs have the same structure and perform the same operations in the same order.

Example:

-- Identical programs
theorem sim_ident : rHoare eqPre
    (do let k ← SPComp.sample Bool; SPComp.pure k)
    (do let k ← SPComp.sample Bool; SPComp.pure k)
    eqPost := by
  ssprove_sim

-- Same structure with rfl-closable side conditions
theorem sim_sample_get : rHoare eqPre
    (do let x ← SPComp.sample Bool; let v ← SPComp.get l; SPComp.pure (x, v))
    (do let x ← SPComp.sample Bool; let v ← SPComp.get l; SPComp.pure (x, v))
    eqPost := by
  ssprove_sim

Equations

• CatCrypt.Tactics.tacticSsprove_sim = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_sim 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_sim" false)

Script-Emitting Variant: ssprove_sim?

def CatCrypt.Tactics.tacticSsprove_sim? : Lean.ParserDescr

ssprove_sim? runs the same fixpoint as ssprove_sim, records which underlying steps fired (normalization, sync/sample/ret/bind rules, rspec lookups, reorders, per-goal closers) in order, and emits a Try this: suggestion with the equivalent explicit tactic script. Use it to freeze an automated ssprove_sim proof into an explicit script.

The proof state after ssprove_sim? is the same as after ssprove_sim (same alternatives tried in the same order), so it can be left in place or replaced by the suggestion.

Replay notes:

• Step lines are emitted with fully-qualified lemma names and replay sequentially (each step acts on the then-current main goal, exactly as repeat ssprove_sim_step does).
• ssprove_wp_step, ssprove_rspec, and ssprove_reorder are composite/ dynamic steps; they are recorded as themselves rather than expanded.
• If every remaining goal is fully closed by its closer, one closer line is emitted per goal; otherwise the original all_goals (first | ...) combo is emitted as a single faithful fallback line.

Equations

• CatCrypt.Tactics.tacticSsprove_sim? = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_sim? 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_sim?" false)

def CatCrypt.Tactics.tacticSsprove_sim_bij_ : Lean.ParserDescr

ssprove_sim_bij f applies sim with an explicit bijection for the first sampling step.

Use this when the two programs sample from the same type but relate the samples through a bijection f.

Example:

-- Programs related by negation bijection
theorem sim_bij : rHoare eqPre
    (SPComp.sample Bool)
    (SPComp.sample Bool)
    (fun a h₁ b h₂ => eqPre h₁ h₂ ∧ notBij a = b) := by
  ssprove_sim_bij notBij

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Tactics.tacticSsprove_sim_eq : Lean.ParserDescr

ssprove_sim_eq proves equivalence under eqPre/eqPost.

Specialized version of sim that maintains heap equality throughout. More aggressive at closing goals since it knows the invariant.

Equations

• CatCrypt.Tactics.tacticSsprove_sim_eq = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_sim_eq 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_sim_eq" false)

def CatCrypt.Tactics.tacticSsprove_sim_auto : Lean.ParserDescr

ssprove_sim_auto extends ssprove_sim with automatic postcondition inference.

When both sides sample from the same distribution but apply different pure functions, it automatically closes the proof by:

1. Using ssprove_sim_step rules (including rHoare_same_step)
2. Applying rHoare_ret to reduce return goals to value equations
3. Trying simp_all/grind to close the value equations

This automates the most common manual postcondition pattern: sample same distribution, apply different functions, prove results equal.

Example:

-- Both sides sample a Bool, but apply different functions.
-- ssprove_sim_auto closes this automatically.
theorem example : rHoare eqPre
    (do let k ← SPComp.sample Bool; SPComp.pure (k && true))
    (do let k ← SPComp.sample Bool; SPComp.pure k)
    eqPost := by
  ssprove_sim_auto

Equations

• CatCrypt.Tactics.tacticSsprove_sim_auto = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_sim_auto 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_sim_auto" false)

def CatCrypt.Tactics.tacticSsprove_try_bij_ : Lean.ParserDescr

ssprove_try_bij f applies a bijection coupling step with bijection f.

This is a convenience wrapper around rHoare_bij_step that also introduces the sampled value.

Example:

-- Couple via XOR bijection
ssprove_try_bij (boolXorBij m)
-- Goal becomes: ∀ k, rHoare Φ (k₁ k) (k₂ (xor k m)) Ψ

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Tactics.tacticSsprove_couple_bij_ : Lean.ParserDescr

ssprove_couple_bij f — the bijection-coupling combinator. Opens the coupling with ssprove_try_bij f (change of variables of the uniform sample along the Equiv f) and discharges the aligned continuation with ssprove_sim_auto. This fuses the verbatim two-step tail of every perfect-security coupling proof (one-time pad, PRF/PRG, commitments, secret sharing, …).

Equations

• One or more equations did not get rendered due to their size.

ssprove_sim? smoke test

The example below is closed by ssprove_sim and exercises the recording variant: it produces a Try this: info suggestion with the explicit script.