Documentation

CatCryptCore.Tactics.Auto

EasyCrypt-Style Auto Tactic #

This file provides an auto-style meta-tactic that chains together wp, sync, conditional resolution, and goal closure, analogous to EasyCrypt's auto tactic.

Main tactics #

What EasyCrypt does #

EasyCrypt's auto is a meta-tactic that chains:

  1. wp to consume deterministic suffixes
  2. rnd for random sampling
  3. skip for empty programs
  4. Repeats until no progress

How it maps to CatCrypt #

We chain our existing tactics in the same order:

  1. ssprove_wp for deterministic tails
  2. ssprove_sync for synchronized operations (EasyCrypt's rnd)
  3. rHoare_ret_same / rHoare_refl for empty programs (EasyCrypt's skip)
  4. ssprove_rcondt / ssprove_rcondf for conditionals

References #

source
def CatCrypt.Tactics.tacticSsprove_auto_step :
Lean.ParserDescr

ssprove_auto_step performs one round of EasyCrypt-style automation.

It tries (in order):

  1. WP step (consume deterministic tail)
  2. Sync rule (coupling for matching operations)
  3. Bind decomposition
  4. Conditional resolution
  5. Dead code elimination
  6. Goal closure (rfl, assumption, trivial)
Equations
Instances For
    source
    def CatCrypt.Tactics.tacticSsprove_auto_ec :
    Lean.ParserDescr

    ssprove_auto_ec is the EasyCrypt-style auto tactic.

    It normalizes code, then repeatedly applies auto steps until no more progress can be made. Finally, it tries to close all remaining goals.

    This tactic handles common patterns:

    • Programs with deterministic tails followed by sampling
    • Identical programs (reflexivity)
    • Programs differing only in dead code
    • Programs with matching conditionals

    Example:

    -- Prove two games equivalent when they sample and return the same thing
theorem game_equiv : rHoare eqPre
    (do let k ← SPComp.sample Bool; pure (xor k x))
    (do let k ← SPComp.sample Bool; pure (xor k x))
    eqPost := by
  ssprove_auto_ec
    Equations
    Instances For
      source
      def CatCrypt.Tactics.tacticSsprove_auto_ec! :
      Lean.ParserDescr

      ssprove_auto_ec! is a more aggressive version that also tries reflexivity and full simplification upfront.

      It first attempts to prove the goal by reflexivity (identical programs), then falls back to step-by-step automation.

      Equations
      Instances For