CatCrypt Tactics Module #
This module provides tactic automation for CatCrypt proofs.
Submodules #
CatCrypt.Tactics.Basic- Basic tactics (ssprove_valid, ssprove_code_simpl)CatCrypt.Tactics.Sync- Synchronization tactics (ssprove_sync, ssprove_sync_eq)CatCrypt.Tactics.Invariant- Invariant tactics (ssprove_invariant, ssprove_restore)CatCrypt.Tactics.ProofFrog- ProofFrog-inspired automation (copy propagation, dead code elimination)CatCrypt.Tactics.Restore- Invariant restoration after put operations (ssprove_restore_pre, ssprove_restore_mem)CatCrypt.Tactics.LazySampling- Lazy/eager sampling infrastructure for PRF proofsCatCrypt.Tactics.Proc- Procedure unfolding (ssprove_proc)CatCrypt.Tactics.WP- Weakest precondition (ssprove_wp)CatCrypt.Tactics.Sim- Automated bisimulation (ssprove_sim)CatCrypt.Tactics.Auto- EasyCrypt-style auto (ssprove_auto_ec)CatCrypt.Tactics.SP- Strongest postcondition (ssprove_sp)CatCrypt.Tactics.SumCases- Sum-type case explosion (sum_cases, pkg_coherence_lite)CatCrypt.Tactics.SPNormalize- SPComp bind-chain normalizationCatCrypt.Tactics.Remember- Remembered-value reasoning (ssprove_remember, ssprove_forget)CatCrypt.Tactics.Triangle- Advantage triangle-inequality chainingCatCrypt.Tactics.CryptoAuto- Crypto-goal automation on top of AutoCatCrypt.Tactics.BindMatch- Bind-match normalization and IsPure bind-commutation swaps
Overview #
The CatCrypt tactic library provides automation for:
Code Validity #
ssprove_valid- Prove ValidCode goals for well-formed codessprove_code_simpl- Simplify and normalize code expressions
Relational Proofs #
ssprove_sync- Apply synchronous rules for matching operationsssprove_sync_eq- Synchronous rules with equality postconditions
Invariant Reasoning #
ssprove_invariant- Prove invariant preservationssprove_restore- Restore invariants after writesssprove_restore_pre- Restore precondition after put operations (from set_lhs/set_rhs)ssprove_restore_mem- Restore precondition including remembered values
EasyCrypt-Style Tactics #
ssprove_proc [d₁, d₂, ...]- Unfold game/oracle definitions (EasyCrypt'sproc)ssprove_wp- Weakest precondition for deterministic tails (EasyCrypt'swp)ssprove_sim- Automated bisimulation for structural matching (EasyCrypt'ssim)ssprove_auto_ec- Meta-tactic chaining wp + sync + skip (EasyCrypt'sauto)
Strongest Postcondition #
ssprove_sp- Process deterministic prefix forwards (EasyCrypt'ssp)ssprove_sp_step- Process one sp step from the head
One-Sided Sampling #
ssprove_rnd_lhs- Consume left-side sampling (EasyCrypt'srnd{1})ssprove_rnd_rhs- Consume right-side sampling (EasyCrypt'srnd{2})
ProofFrog-Inspired Automation #
ssprove_dead_code- Eliminate unused computations (samples, gets, pure values)ssprove_copy_propagate- Substitute known values (e.g., after set/get)ssprove_contract_all- Apply all contraction rules (duplicate get/put elimination)ssprove_canonicalize- Normalize code structure (bind association, pure inlining)ssprove_auto_pf- Apply all ProofFrog-style simplificationsssprove_auto_pf!- Aggressive automation including sync rules
Usage #
Import this module to get access to all CatCrypt tactics:
import CatCryptCore.Tactics
example : rHoare eqPre (sample α) (sample α) (fun a h₁ b h₂ => eqPre h₁ h₂ ∧ a = b) := by
ssprove_sync
See Also #
CatCrypt.Tactic.Basic- Lower-level pRHL tactics (rsame, rbind, etc.)