ProofFrog-Inspired Tactics

This file provides tactics inspired by ProofFrog's automatic game transformations. ProofFrog is a Python-based cryptographic proof verifier that uses AST canonicalization and SMT solving for automatic equivalence proofs.

Main Tactics

• ssprove_copy_propagate - Substitute known values for variables
• ssprove_dead_code - Eliminate unused computations
• ssprove_unreachable - Prove unreachable code paths
• ssprove_canonicalize - Put code into canonical form
• ssprove_auto_pf - Apply all ProofFrog-style simplifications

Comparison with ProofFrog

Feature	ProofFrog	CatCrypt (these tactics)
Inlining	Automatic	ssprove_code_simpl
Copy propagation	Automatic	ssprove_copy_propagate
Dead code elimination	Automatic	ssprove_dead_code
Unreachable code	Z3	ssprove_unreachable (decide/omega)
Canonicalization	AST-based	ssprove_canonicalize

Implementation Notes

Unlike ProofFrog which operates on ASTs externally, these tactics work within Lean's type system. This provides full soundness guarantees but requires explicit lemmas for each transformation.

References

• ProofFrog: https://prooffrog.github.io/ (source: https://github.com/ProofFrog/ProofFrog)
• [Barbosa et al., "Mechanizing Proofs about Adversaries"]

Dead Code Elimination

These tactics eliminate computations whose results are not used.

def CatCrypt.Tactics.tacticSsprove_dead_sample_lhs : Lean.ParserDescr

ssprove_dead_sample_lhs eliminates an unused sample on the left side.

Rewrites let _ ← sample α; k to k when the sample result is not used.

Example:

theorem example : rHoare Φ (do let _ ← SPComp.sample Bool; k) c₂ Ψ := by
  ssprove_dead_sample_lhs
  -- Goal is now: rHoare Φ k c₂ Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_dead_sample_lhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_dead_sample_lhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_dead_sample_lhs" false)

def CatCrypt.Tactics.tacticSsprove_dead_sample_rhs : Lean.ParserDescr

ssprove_dead_sample_rhs eliminates an unused sample on the right side.

Equations

• CatCrypt.Tactics.tacticSsprove_dead_sample_rhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_dead_sample_rhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_dead_sample_rhs" false)

def CatCrypt.Tactics.tacticSsprove_dead_get_lhs : Lean.ParserDescr

ssprove_dead_get_lhs eliminates an unused get on the left side.

Rewrites let _ ← get l; k to k when the get result is not used.

Equations

• CatCrypt.Tactics.tacticSsprove_dead_get_lhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_dead_get_lhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_dead_get_lhs" false)

def CatCrypt.Tactics.tacticSsprove_dead_get_rhs : Lean.ParserDescr

ssprove_dead_get_rhs eliminates an unused get on the right side.

Equations

• CatCrypt.Tactics.tacticSsprove_dead_get_rhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_dead_get_rhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_dead_get_rhs" false)

def CatCrypt.Tactics.tacticSsprove_dead_pure_lhs : Lean.ParserDescr

ssprove_dead_pure_lhs eliminates an unused pure on the left side.

Rewrites let _ ← pure v; k to k.

Equations

• CatCrypt.Tactics.tacticSsprove_dead_pure_lhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_dead_pure_lhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_dead_pure_lhs" false)

def CatCrypt.Tactics.tacticSsprove_dead_pure_rhs : Lean.ParserDescr

ssprove_dead_pure_rhs eliminates an unused pure on the right side.

Equations

• CatCrypt.Tactics.tacticSsprove_dead_pure_rhs = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_dead_pure_rhs 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_dead_pure_rhs" false)

def CatCrypt.Tactics.tacticSsprove_dead_code : Lean.ParserDescr

ssprove_dead_code attempts to eliminate all dead code on both sides.

This tactic repeatedly applies dead code elimination rules until no more simplifications are possible. It handles:

• Unused samples
• Unused gets
• Unused pure values

Example:

theorem example : rHoare Φ
    (do let _ ← SPComp.sample Bool; let _ ← SPComp.get l; k)
    (do let _ ← SPComp.sample Nat; k')
    Ψ := by
  ssprove_dead_code
  -- Goal is now: rHoare Φ k k' Ψ

Equations

• CatCrypt.Tactics.tacticSsprove_dead_code = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_dead_code 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_dead_code" false)

Copy Propagation

These tactics substitute known values for variables, propagating information from earlier computations to later uses.

def CatCrypt.Tactics.tacticSsprove_copy_propagate_get_lhs : Lean.ParserDescr

ssprove_copy_propagate_get_lhs propagates a known value from get.

After x ← get l, if we know the heap value at l, we can substitute that value for x in subsequent code.

Currently implemented as a rewrite using get_value_eq.

Equations

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

def CatCrypt.Tactics.tacticSsprove_copy_propagate_get_rhs : Lean.ParserDescr

ssprove_copy_propagate_get_rhs propagates a known value on the right side.

Equations

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

def CatCrypt.Tactics.tacticSsprove_copy_propagate_set_get_lhs : Lean.ParserDescr

ssprove_copy_propagate_set_get_lhs propagates the set value to subsequent get.

After set l v, a get l returns v. This tactic combines set and get into the known value.

Equations

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

def CatCrypt.Tactics.tacticSsprove_copy_propagate_set_get_rhs : Lean.ParserDescr

ssprove_copy_propagate_set_get_rhs propagates on the right side.

Equations

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

def CatCrypt.Tactics.tacticSsprove_copy_propagate : Lean.ParserDescr

ssprove_copy_propagate attempts to propagate all known values.

This tactic combines:

1. Propagating set values to subsequent gets
2. Inlining pure values via pure_bind
3. Simplifying with known equalities

Example:

theorem example : rHoare Φ
    (do SPComp.set l 42; let x ← SPComp.get l; f x)
    c₂ Ψ := by
  ssprove_copy_propagate
  -- Goal uses f 42 instead of f x

Equations

• CatCrypt.Tactics.tacticSsprove_copy_propagate = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_copy_propagate 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_copy_propagate" false)

Unreachable Code Detection

These tactics identify and eliminate unreachable code paths using Lean's decision procedures.

def CatCrypt.Tactics.tacticSsprove_unreachable : Lean.ParserDescr

ssprove_unreachable proves a goal when the precondition is false.

This handles cases where the precondition is contradictory, meaning the code path is unreachable.

Example:

theorem example : rHoare (fun _ _ => False) c₁ c₂ Ψ := by
  ssprove_unreachable

Equations

• CatCrypt.Tactics.tacticSsprove_unreachable = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_unreachable 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_unreachable" false)

def CatCrypt.Tactics.tacticSsprove_unreachable_branch_lhs : Lean.ParserDescr

ssprove_unreachable_branch eliminates an unreachable if-branch.

When an if-condition is provably false, the else branch is taken.

Equations

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

def CatCrypt.Tactics.tacticSsprove_unreachable_branch_rhs : Lean.ParserDescr

Equations

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

Canonicalization

These tactics put code into a canonical form for easier comparison and automated reasoning.

def CatCrypt.Tactics.tacticSsprove_canonicalize_lhs : Lean.ParserDescr

ssprove_canonicalize_lhs puts the left-side code into canonical form.

Canonical form has:

1. Binds associated to the right: ((a >>= f) >>= g) → (a >>= (f >=> g))
2. Pure values inlined: pure x >>= f → f x
3. Trivial binds removed: a >>= pure → a

Equations

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

def CatCrypt.Tactics.tacticSsprove_canonicalize_rhs : Lean.ParserDescr

ssprove_canonicalize_rhs puts the right-side code into canonical form.

Equations

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

def CatCrypt.Tactics.tacticSsprove_canonicalize : Lean.ParserDescr

ssprove_canonicalize puts both sides into canonical form.

Equations

• CatCrypt.Tactics.tacticSsprove_canonicalize = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_canonicalize 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_canonicalize" false)

Contract Rules (Enhanced)

Enhanced versions of contract rules that combine multiple optimizations.

def CatCrypt.Tactics.tacticSsprove_contract_all_lhs : Lean.ParserDescr

ssprove_contract_all_lhs applies all contraction rules on the left side.

This combines:

• Duplicate get elimination
• Duplicate put elimination
• Put-get contraction

Equations

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

def CatCrypt.Tactics.tacticSsprove_contract_all_rhs : Lean.ParserDescr

ssprove_contract_all_rhs applies all contraction rules on the right side.

Equations

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

def CatCrypt.Tactics.tacticSsprove_contract_all : Lean.ParserDescr

ssprove_contract_all applies all contraction rules on both sides.

Equations

• CatCrypt.Tactics.tacticSsprove_contract_all = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_contract_all 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_contract_all" false)

Comprehensive Automation

The main tactic that combines all ProofFrog-style optimizations.

def CatCrypt.Tactics.tacticSsprove_auto_pf : Lean.ParserDescr

ssprove_auto_pf applies all ProofFrog-style simplifications automatically.

The _pf suffix marks ProofFrog provenance, parallel to the _ec suffix on the EasyCrypt automation verb ssprove_auto_ec; the two are distinct tactics.

This tactic performs the following optimizations in order:

1. Canonicalization (normalize bind structure)
2. Dead code elimination (remove unused computations)
3. Copy propagation (substitute known values)
4. Contraction (eliminate redundant operations)

After these optimizations, the goal should be in a normalized form that makes equivalence proofs easier.

Example:

theorem game_equiv : rHoare eqPre
    (do let _ ← SPComp.sample Bool;  -- dead
        SPComp.set l 42;
        let x ← SPComp.get l;        -- copy propagate to 42
        let y ← SPComp.get l;        -- contract with previous get
        f x y)
    (do SPComp.set l 42;
        f 42 42)
    eqPost := by
  ssprove_auto_pf
  ssprove_sync_eq

Equations

• CatCrypt.Tactics.tacticSsprove_auto_pf = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_auto_pf 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_auto_pf" false)

def CatCrypt.Tactics.tacticSsprove_auto_pf! : Lean.ParserDescr

ssprove_auto_pf! is a more aggressive version that also tries sync rules.

This adds:

• Attempting reflexivity for identical code
• Attempting sync rules for matching operations
• Using simp for remaining simplifications

Equations

• CatCrypt.Tactics.tacticSsprove_auto_pf! = Lean.ParserDescr.node `CatCrypt.Tactics.tacticSsprove_auto_pf! 1024 (Lean.ParserDescr.nonReservedSymbol "ssprove_auto_pf!" false)

Game Transformation Helpers

These tactics help with common game transformation patterns.

def CatCrypt.Tactics.tacticSsprove_inline_lhs_ : Lean.ParserDescr

ssprove_inline_lhs inlines a definition on the left side.

Use this when you want to expand a named computation for further simplification.

Equations

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

def CatCrypt.Tactics.tacticSsprove_inline_rhs_ : Lean.ParserDescr

ssprove_inline_rhs inlines a definition on the right side.

Equations

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

def CatCrypt.Tactics.tacticSsprove_rewrite_lhs_ : Lean.ParserDescr

ssprove_rewrite_lhs rewrites using an equality lemma on the left side.

Equations

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

def CatCrypt.Tactics.tacticSsprove_rewrite_rhs_ : Lean.ParserDescr

ssprove_rewrite_rhs rewrites using an equality lemma on the right side.

Equations

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