Documentation

CatCryptCore.Tactics.Basic

Basic CatCrypt Tactics #

This file provides basic tactic automation for CatCrypt proofs, including tactics for ValidCode goals and code simplification.

Main tactics #

Simp sets #

References #

Simp Set Population #

The simp sets are declared in CatCrypt.Tactics.SimpAttr (separate file required because register_simp_attr creates attributes that cannot be used in the same file they are declared in).

ValidCode Tactics #

source
def CatCrypt.Tactics.tacticSsprove_valid :
Lean.ParserDescr

ssprove_valid is a tactic for proving ValidCode goals.

This tactic attempts to discharge ValidCode obligations by:

  1. Unfolding definitions
  2. Applying structural rules for bind, return, sample, etc.
  3. Checking that operations access only permitted locations

Example:

theorem mycode_valid : ValidCode L I (do
    let x ← get loc
    return x) := by
  ssprove_valid
Equations
Instances For
    source
    def CatCrypt.Tactics.tacticSsprove_code_simpl :
    Lean.ParserDescr

    ssprove_code_simpl is a tactic for simplifying CatCrypt code.

    This tactic normalizes code by:

    1. Associating binds to the right: (x >>= f) >>= g → x >>= (fun a => f a >>= g)
    2. Simplifying pure/return: pure a >>= f → f a
    3. Eliminating dead code (unused sample, get, pure)
    4. Contracting redundant operations (duplicate get/put, put-get)
    5. Copy propagation (set-get same location)

    Example:

    example : ((c >>= f) >>= g) = (c >>= fun x => f x >>= g) := by
  ssprove_code_simpl
    Equations
    Instances For
      source
      structure CatCrypt.Tactics.ValidConfig :
      Type

      Configuration for ssprove_valid tactic

      • maxDepth : ℕ

        Maximum recursion depth

      • unfold : Bool

        Whether to unfold definitions

      • auto : Bool

        Whether to use automation

      Instances For
        source
        def CatCrypt.Tactics.tacticSsprove_valid! :
        Lean.ParserDescr

        ssprove_valid! is a more aggressive version of ssprove_valid that uses additional automation.

        Equations
        Instances For

          Distribution-Level Simplification #

          The ssprove_distr_simp tactic normalizes terms at the SDistr level, after SPComp definitions have been unfolded. This handles the common pattern:

          simp only [SPComp.bind_def, SPComp.sample, SPComp.pure_def,
           SDistr.bind_assoc, SDistr.pure_bind]

          which appears 100+ times across shallow embedding proofs.

          source
          def CatCrypt.Tactics.tacticSsprove_distr_simp :
          Lean.ParserDescr

          ssprove_distr_simp normalizes sub-distribution terms.

          After unfolding SPComp to SDistr, this tactic reassociates binds, eliminates pure-bind pairs, and normalizes sampling definitions.

          Example:

          -- Goal involves (SDistr.uniform α).bind (fun a => (SDistr.pure (a, h)).bind ...)
ssprove_distr_simp
-- Goal is now normalized with bind_assoc and pure_bind applied
          Equations
          Instances For

            Enhanced Monadic Normalization #

            The ssprove_proc tactic normalizes SPComp programs at the monadic level, analogous to EasyCrypt's proc; inline *; auto. It chains bind_assoc, pure_bind, bind_pure, monad_bind_eq, and monad_pure_eq, then tries congr/funext to push through binders, and rfl to close.

            This replaces the common 5-10 line pattern:

            simp only [SPComp.monad_bind_eq, SPComp.bind_assoc, SPComp.pure_bind, ...]
congr 1; funext _
simp only [...]
rfl

            with a single ssprove_proc call.

            source
            def CatCrypt.Tactics.tacticSsprove_proc :
            Lean.ParserDescr

            ssprove_proc normalizes SPComp monadic programs.

            Analogous to EasyCrypt's proc; inline *; auto:

            1. Simplify with monad_bind_eq, bind_assoc, pure_bind, bind_pure
            2. Try rfl
            3. If stuck, try congr 1; funext to descend through binders
            Equations
            Instances For
              source
              def CatCrypt.Tactics.tacticSsprove_proc_unfold_ :
              Lean.ParserDescr

              ssprove_proc_unfold defs unfolds definitions then normalizes.

              Usage: ssprove_proc_unfold my_real my_ideal

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

                Bijection Coupling Tactic #

                The ssprove_rnd tactic automates change-of-variables on sampling steps, analogous to EasyCrypt's rnd f g; auto. Given a goal about SPComp.sample, it applies a bijection to transform the distribution.

                This replaces:

                apply sdist_of_eq
congr 1; funext a
exact SPComp.sample_bind_equiv (Equiv.addRight k) (fun a => ...)

                with ssprove_rnd (Equiv.addRight k).

                source
                def CatCrypt.Tactics.tacticSsprove_rnd_ :
                Lean.ParserDescr

                ssprove_rnd e applies bijection e : α ≃ β to a sampling step.

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

                  Exponentiation Normalization Tactic #

                  The exp_simp tactic normalizes group exponentiation terms, analogous to EasyCrypt's algebra tactic. It:

                  1. Rewrites groupExp (exp w) e to exp (w * e) via groupExp_mul'
                  2. Combines exp a * exp b to exp (a + b) via exp_add'
                  3. Normalizes raw field accessors (smul, sadd) to notation (*, +)
                  4. Tries ring on remaining scalar goals inside exp
                  5. Tries group on remaining group goals

                  This closes goals like exp(a*b+c) * exp(d) = exp(b*a+c+d) in one step.

                  source
                  def CatCrypt.Tactics.tacticExp_simp :
                  Lean.ParserDescr
                  Equations
                  Instances For