Clean up legacy comments and restore CountingOracle support lemmas

[quangvdao]

Summary

• Remove dead commented-out code from AsymmEncAlg.lean, LWE.lean, and OracleComp.lean that used obsolete API patterns (guard-based experiments, [= x | ...] notation, ++ₒ, sorry-based DecidableEq).
• Replace broken proof stubs with working proofs in CountingOracle.lean: ~250 lines of commented-out attempts are replaced with ~289 lines of complete proofs for counting oracle support characterization lemmas, including:
  • mem_support_simulate_iff: characterizes membership in support of simulate oa qc in terms of support at initial count 0
  • le_of_mem_support_simulate: query counts are monotonically non-decreasing through simulation
  • mem_support_snd_map_simulate_iff and variants: support characterization for the query-count projection
  • add_right_mem_support_simulate_iff / add_left_mem_support_simulate_iff: shift-invariance of support
  • mem_support_simulate_queryBind_iff: full characterization of support for query >>= oa patterns
  • exists_mem_support_of_mem_support: lifts plain support membership into counting simulation support

Test plan

• lake build passes (single commit, already on CI)

Made with Cursor

[github-actions]

🤖 AI-Generated PR Summary

Files Changed:

• VCVio/CryptoFoundations/AsymmEncAlg.lean
• VCVio/CryptoFoundations/HardnessAssumptions/LWE.lean
• VCVio/OracleComp/OracleComp.lean
• VCVio/OracleComp/QueryTracking/CountingOracle.lean

Overview of Changes:
This diff represents a significant code cleanup and modernization effort across the codebase.

Here is a summary of the key changes:

• Refactor Query Counting Logic: The most substantial change is in CountingOracle.lean. A large block of old, commented-out, and incomplete lemmas for reasoning about the support of query-counted computations has been deleted and replaced with a new, fully-proven implementation built on the modern simulateQ framework.

• Modernize Cryptographic Experiments: In AsymmEncAlg.lean, outdated definitions for cryptographic correctness and IND-CPA experiments have been removed. These old versions used a guard-based failure model, which has been superseded by a cleaner, Bool-based success/failure model.

• General Code Cleanup: The diff removes dead and commented-out code across several files to improve code hygiene. This includes:

  • Deleting an old, commented-out implementation of the LWE assumption in LWE.lean.
  • Removing unused helper lemmas and an incomplete DecidableEq instance from OracleComp.lean.

New 'sorry's: 0