Documentation

CatCryptCore.Deep.Tactics

Tactics for Deep Embedding Reasoning #

This file provides tactics for working with the deep embedding of CatCrypt computations, particularly for separation reasoning.

Main definitions #

Usage #

-- Proving separation of packages
example (p₁ p₂ : DeepPackage) (h : Disjoint p₁.locs p₂.locs) : DeepPackage.sep p₁ p₂ := by sep_solve

References #

Separation tactic #

source
def CatCrypt.tacticSep_solve :
Lean.ParserDescr

Tactic for solving separation goals.

The sep_solve tactic attempts to prove goals of the form DeepPackage.sep p₁ p₂ (i.e., Disjoint p₁.locs p₂.locs) by:

  1. Unfolding sep to Disjoint on location sets
  2. Simplifying location set definitions
  3. Using Finset.disjoint_* lemmas

Example:

example (p : DeepPackage) : DeepPackage.sep DeepPackage.empty p := by sep_solve
Equations
Instances For

    Disjointness tactic #

    source
    def CatCrypt.tacticDisj_solve :
    Lean.ParserDescr

    Tactic for solving disjointness goals on location sets.

    The disj_solve tactic attempts to prove goals of the form Disjoint s₁ s₂ for finite sets of Nats by:

    1. Converting to membership conditions
    2. Numeric reasoning with omega

    Example:

    example (s : Finset Nat) : Disjoint ∅ s := by disj_solve
    Equations
    Instances For

      Combined automation #

      source
      def CatCrypt.tacticSep_auto :
      Lean.ParserDescr

      Combined tactic for separation and disjointness reasoning.

      The sep_auto tactic combines separation and disjointness automation to handle common goals in CatCrypt proofs.

      It tries, in order:

      1. sep_solve for separation goals
      2. disj_solve for disjointness goals
      3. General simplification and automation

      Example:

      example (p : DeepPackage) : DeepPackage.sep DeepPackage.empty p := by sep_auto
      Equations
      Instances For

        Nominal Tactics #

        source
        def CatCrypt.tacticAtom_sep_solve :
        Lean.ParserDescr

        Tactic for solving atom separation goals.

        The atom_sep_solve tactic attempts to prove goals of the form NomPackage.atomSep p₁ p₂ (i.e., Disjoint p₁.atoms p₂.atoms) by:

        1. Unfolding atomSep to Disjoint on atom sets
        2. Using Finset.disjoint_* lemmas
        3. Applying freshness reasoning

        Example:

        example (p : NomPackage) : NomPackage.atomSep NomPackage.empty p := by atom_sep_solve
        Equations
        Instances For
          source
          def CatCrypt.tacticFresh_solve :
          Lean.ParserDescr

          Tactic for solving freshness goals.

          The fresh_solve tactic attempts to prove goals involving freshness of atoms for elements in nominal sets. It uses the Fresh predicate from the nominal sets library.

          Example:

          example (a : Atom) (s : Finset Atom) (h : a ∉ s) : Fresh a s := by fresh_solve
          Equations
          Instances For
            source
            def CatCrypt.tacticNom_auto :
            Lean.ParserDescr

            Tactic for nominal separation automation.

            The nom_auto tactic combines nominal tactics to handle common goals in nominal CatCrypt proofs:

            1. Package separation (both location-based and atom-based)
            2. Disjointness of atom sets
            3. Freshness goals

            Example:

            example (p : NomPackage) : NomPackage.atomSep NomPackage.empty p := by nom_auto
            Equations
            Instances For

              Documentation #

              Tactic Summary #

              TacticPurposeTypical Goal
              sep_solveProve package separationDeepPackage.sep p₁ p₂
              disj_solveProve set disjointnessDisjoint s₁ s₂
              sep_autoCombined automationAny of the above
              atom_sep_solveProve atom separationNomPackage.atomSep p₁ p₂
              fresh_solveProve freshnessFresh a x
              nom_autoFull nominal automationAny nominal goal

              Key Lemmas Used #

              The tactics use these key lemmas:

              Integration with Hybrid Arguments #

              These tactics are designed to support hybrid argument proofs in cryptography. The key workflow is:

              1. Define a sequence of games as DeepPackage or NomPackage values
              2. Use sep_solve or atom_sep_solve to show games have disjoint state
              3. Use nom_auto for automatic nominal reasoning
              4. Use structural induction on RawCode to relate game behaviors