Improve ProgramLogic tactics and support general Pr goals

[quangvdao]

Summary

• improve qvcgen / rvcgen planning, diagnostics, and theorem-driven automation so tactic replay and ambiguity reporting are more actionable
• support lower-bound and general Pr[...] goals in qvcgen, keeping lower bounds in Triple form and continuing other shapes in raw wp mode
• make probability-equality automation less brittle on nested mapped goals, expand tactic regressions, and update the live program-logic guide

Test plan

• lake build VCVio.ProgramLogic.Tactics.Examples Examples.ElGamal Examples.Schnorr Examples.OneTimePad

[github-actions]

🤖 Gemini PR Summary

Logic and Formalization

• Established a formal equivalence between lower-bound probability constraints and unary Hoare triples using indicator-function postconditions.
• Introduced relational transport theorems for simulateQ to facilitate the propagation of invariants and equality relations during simulation-based proofs.
• Proved theorems justifying the transformation of high-level probability goals into structured program logic obligations.

VCGen Tactic Infrastructure

• Planning Mechanism: Implemented a planning system for qvcgen and rvcgen that evaluates candidate steps—including structural rules, local hypotheses, and registered theorems—to select paths that minimize open goals.
• Theorem Registry: Added the @[rvcgen] attribute and an environment-based indexing system, enabling the relational tactic to perform efficient head-symbol lookups for automatic theorem application.
• Diagnostics and Feedback: Tactics now provide actionable "notes" explaining chosen steps and suggestions for local lemmas when automated stepping fails.
• Syntax Extensions: Added support for a with clause in relational steps for explicit theorem application and as ⟨...⟩ syntax for naming introduced variables.

Program Logic Support

• Goal Generalization: Expanded qvcgen to support lower-bound probability inequalities and general Pr[...] goals.
• Raw WP Mode: Enabled a fallback "raw wp mode" for goals not fitting the standard Triple shape (e.g., non-lower-bound Pr goals), allowing structural decomposition to continue using weakest precondition logic.
• Congruence Automation: Refactored probability congruence rewriting to improve handling of nested mapped goals and bind-swaps through a generalized chaining approach.

Documentation and Testing

• Proof Refactoring: Simplified security proofs for ElGamal and One-Time Pad by leveraging the new tactic planning and automation.
• Regression Suite: Added tests for if-then-else constructs, nested binds, and custom tactic hints.
• User Documentation: Updated the program-logic.md guide to cover the @[rvcgen] attribute, new syntax, and improved probability-equality automation.

---

Statistics

Metric	Count
📝 Files Changed	13
✅ Lines Added	866
❌ Lines Removed	208

---

Lean Declarations

✏️ **Added:** 16 declaration(s)

• def tryRawWpStructuralStep : TacticM Bool in VCVio/ProgramLogic/Tactics/Unary/Internals.lean
• lemma triple_propInd_iff_le_probEvent {ι : Type u} {spec : OracleSpec ι} in VCVio/ProgramLogic/Notation.lean
• theorem le_probOutput_iff_triple_indicator (oa : OracleComp spec α) [DecidableEq α] in VCVio/ProgramLogic/Unary/HoareTriple.lean
• def runProbEqCongrChainWithNames in VCVio/ProgramLogic/Tactics/Unary/Internals.lean
• def findRegisteredRVCGenTheoremCandidates : TacticM (Array Name) in VCVio/ProgramLogic/Tactics/Relational/Internals.lean
• def findRelHintCandidates : TacticM (Array Name) in VCVio/ProgramLogic/Tactics/Relational/Internals.lean
• theorem relTriple_simulateQ_run_eqRel_of_impl_eq_preservesInv in VCVio/ProgramLogic/Relational/SimulateQ.lean
• def findLoopInvHintCandidates : TacticM (Array Name) in VCVio/ProgramLogic/Tactics/Unary/Internals.lean
• def runRVCGenStepWithTheorem (thm : TSyntax term) (requireClosed : BoolinVCVio/ProgramLogic/Tactics/Relational/Internals.lean`
• def findRegisteredVCGenTheoremCandidates : TacticM (Array Name) in VCVio/ProgramLogic/Tactics/Unary/Internals.lean
• theorem relTriple_simulateQ_run'_of_query_map_eq in VCVio/ProgramLogic/Relational/SimulateQ.lean
• def formatCandidateNames (names : Array Name) : String in VCVio/ProgramLogic/Tactics/Common/Core.lean
• def findHoareCutHintCandidates : TacticM (Array Name) in VCVio/ProgramLogic/Tactics/Unary/Internals.lean
• def getRegisteredRVCGenTheorems (oa ob : Expr) : MetaM (Array Name) in VCVio/ProgramLogic/Tactics/Common/Registry.lean
• def withStepNotes (step : PlannedStep) (notes : List String) : PlannedStep in VCVio/ProgramLogic/Tactics/Common/Core.lean
• theorem le_probEvent_iff_triple_indicator (oa : OracleComp spec α) (p : α → Prop) in VCVio/ProgramLogic/Unary/HoareTriple.lean

✏️ **Affected:** 6 declaration(s) (line number changed)

• def throwQVCGenStepError : TacticM Unit in VCVio/ProgramLogic/Tactics/Unary/Internals.lean moved from L43 to L311
• def findUniqueHoareCutHint? : TacticM (Option Name) in VCVio/ProgramLogic/Tactics/Unary/Internals.lean moved from L251 to L260
• def findUniqueLoopInvHint? : TacticM (Option Name) in VCVio/ProgramLogic/Tactics/Unary/Internals.lean moved from L274 to L288
• def logPlannedStep (step : PlannedStep) (beforeGoals afterGoals : Nat) : TacticM Unit in VCVio/ProgramLogic/Tactics/Common/Core.lean moved from L54 to L61
• def findRegisteredVCGenTheorem? : TacticM (Option Name) in VCVio/ProgramLogic/Tactics/Unary/Internals.lean moved from L297 to L308
• def findUniqueRelHint? : TacticM (Option Name) in VCVio/ProgramLogic/Tactics/Relational/Internals.lean moved from L263 to L302

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• Examples/ElGamal.lean: This PR refines and simplifies existing proof scripts for ElGamal security theorems by consolidating multiple qvcgen_step tactic calls and streamlining simp arguments. No new theorems or definitions are introduced, and the changes do not add any sorry or admit placeholders.
• Examples/OneTimePad.lean: This change refactors the proof of cipherGivenMsg_equiv by extracting the bijectivity property of BitVec XOR into a local lemma. This modification improves proof structure and simplifies the application of the rvcgen_step tactic without introducing new theorems or sorry placeholders.
• VCVio/ProgramLogic/Notation.lean: This change introduces a new lemma, triple_propInd_iff_le_probEvent, which establishes that quantitative triples with indicator postconditions are equivalent to lower-bound constraints on event probabilities. No sorry or admit placeholders are added.
• VCVio/ProgramLogic/Relational/SimulateQ.lean: This file introduces two new theorems, relTriple_simulateQ_run_eqRel_of_impl_eq_preservesInv and relTriple_simulateQ_run'_of_query_map_eq, which establish relational transport properties for simulateQ. These results specialize existing invariant-preserving simulation lemmas into the RelTriple framework using equality relations to facilitate integration with probability-transport proofs and automated verification steps.
• VCVio/ProgramLogic/Tactics/Common/Core.lean: This PR enhances the tactic logging system by adding support for metadata notes and goal-count tracking to the PlannedStep structure. It introduces helper definitions to manage these notes and updates the logging logic to report the change in the number of open goals after a step is executed.
• VCVio/ProgramLogic/Tactics/Common/Registry.lean: This file introduces the @[rvcgen] attribute and a corresponding environment registry to support head-symbol-based theorem lookup for relational verification condition generation. It adds infrastructure for indexing and retrieving RelTriple theorems based on the head constants of their left and right computation sides, and no sorry placeholders are used.
• VCVio/ProgramLogic/Tactics/Examples.lean: This file adds several new examples and regression tests for the qvcgen and rvcgen tactics, demonstrating their use in handling nested binds, if-then-else constructs, and probability inequalities. It introduces two auxiliary irreducible definitions and a local theorem to verify custom tactic hints and uses #guard_msgs to validate tactic suggestions and error reporting. No sorry or admit placeholders are added.
• VCVio/ProgramLogic/Tactics/Relational.lean: This PR extends the rvcgen and rvcgen_step tactics by adding a with clause, allowing users to explicitly specify a relational theorem or assumption to apply during a verification step. It also introduces support for naming variables introduced by these explicit steps using the as ⟨...⟩ syntax. No sorry or admit placeholders were added.
• VCVio/ProgramLogic/Tactics/Relational/Internals.lean: The changes enhance the relational verification condition generator by implementing a selection mechanism that compares structural steps, local hints, and registered [rvcgen] theorems to choose the tactic step that minimizes remaining goals. This update introduces several new internal definitions for identifying candidate rules and provides improved error diagnostics that list viable suggestions when a step fails. No sorry or admit placeholders were added.
• VCVio/ProgramLogic/Tactics/Unary.lean: This change extends the qvcgen and qvcgen_step tactics to support raw weakest precondition (wp) goals and probability lower bounds, allowing the structural VCGen pipeline to handle a broader range of quantitative goals. It introduces a logging mechanism to notify users when the tactic transitions into "raw wp mode" and refactors probability congruence rewriting to use a more general chaining approach. The diff contains no sorry or admit placeholders.
• docs/agents/program-logic.md: The updates expand the rvcgen and qvcgen tactic suites to support explicit theorem application via with clauses and introduce a new @[rvcgen] attribute for automated relational lookup. Key enhancements include support for lower-bound probability inequalities and improved automation for bind-congruence and swaps, featuring syntax normalization and multi-binder support.
• VCVio/ProgramLogic/Unary/HoareTriple.lean: This PR introduces two new theorems, le_probEvent_iff_triple_indicator and le_probOutput_iff_triple_indicator, which establish the equivalence between lower bounds on probabilities and unary Hoare triples with indicator-function postconditions. These results facilitate reasoning about event and output probabilities within the program logic framework.
• VCVio/ProgramLogic/Tactics/Unary/Internals.lean: This update enhances the qvcgen tactic by implementing a planning heuristic that evaluates multiple candidate steps—including bind cuts, loop invariants, and registered theorems—and selects the one that most effectively reduces the goal count. The changes improve contextual error reporting with specific suggestions for local hypotheses, extend structural stepping to "raw wp" goals, and introduce several internal helper functions for probability-goal normalization and lowering. No sorry or admit placeholders were added.

---

Last updated: 2026-03-12 21:23 UTC.

[github-actions]

🤖 Initial AI review without external context

🤖 AI Review

Reviewed Revision

• Commit: e8d62777d5ae2c1eb4c833570d6c2b87fb157d41
• Commit message:

refactor(ProgramLogic): align probability indicator theorem names

Rename the lower-bound `probOutput` bridge to match the existing indicator-based theorem naming and keep the unary lowering path consistent with that API.

Made-with: Cursor

Overall Summary:
TL;DR: The PR is mathematically sound, and the vast majority of the formalized examples, program logic, and tactics are in excellent shape. However, there is a technical Lean 4 syntax issue involving missing string interpolation macros in the tactic error messages that needs to be addressed before merging.

Checklist Coverage:
No explicit specification checklist was provided for this PR.

Key Lean 4 / Mathlib Issues:

• Missing string interpolation macros (m!) in error messages (Affects 1 file: VCVio/ProgramLogic/Tactics/Unary/Internals.lean):
  In throwQVCGenStepError, standard string literals "..." are being used where string interpolation is intended. In Lean 4, standard string literals do not perform string interpolation; the string must be prefixed with m! (which generates MessageData) to properly evaluate and format variables like {indentExpr comp}, {cutMsg}, {invMsg}, and {theoremMsg}. Without the m! prefix, the tactic state will literally display the text {cutMsg} to the user rather than the intended variables. Please prefix all updated throwError strings within throwQVCGenStepError with m!.

Nitpicks:

• Array Idioms (VCVio/ProgramLogic/Tactics/Unary/Internals.lean): In findUniqueHoareCutHint? and findUniqueLoopInvHint?, the pattern found.toList.head? >>= fun first => if found.size = 1 then some first else none works fine, but using if found.size == 1 then some found[0]! else none is more idiomatic for arrays and avoids allocating an intermediate list.
• Implicit Arguments in iff Lemmas (VCVio/ProgramLogic/Unary/HoareTriple.lean): For rewrite lemmas like le_probEvent_iff_triple_indicator and le_probOutput_iff_triple_indicator, it is standard Mathlib practice to make arguments that appear on both sides of the iff implicit (e.g., {oa : OracleComp spec α} {p : α → Prop}), as they can be inferred from the goal. This significantly improves ergonomics when using apply or exact.

Overall Verdict: Changes Requested

---

📄 **Review for `Examples/ElGamal.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `Examples/OneTimePad.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Notation.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Relational/SimulateQ.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Common/Core.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Common/Registry.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Examples.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Relational.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Relational/Internals.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Unary.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:
None

📄 **Review for `VCVio/ProgramLogic/Tactics/Unary/Internals.lean`**

Verdict: Needs Minor Revisions

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:

• Missing string interpolation macros (m!) in error messages: In Lean 4, standard string literals "..." do not perform string interpolation. In order for {indentExpr comp}, {cutMsg}, {invMsg}, and {theoremMsg} to be evaluated and formatted, the string literal must be prefixed with m! (for MessageData generation, which allows indentExpr to properly format the expression). Without m!, the user will literally see the text {cutMsg} in their tactic state when an error is thrown.

  In throwQVCGenStepError, you have several occurrences of this issue introduced by the PR:

  throwError
    "qvcgen_step: found a `Triple` goal, but no matching rule applied to:{indentExpr comp}\n\
    Try `wp_step`, or manually unfolding the remaining arithmetic side conditions.\
    {cutMsg}{invMsg}{theoremMsg}"

  This should be:

  throwError m!
    "qvcgen_step: found a `Triple` goal, but no matching rule applied to:{indentExpr comp}\n\
    Try `wp_step`, or manually unfolding the remaining arithmetic side conditions.\
    {cutMsg}{invMsg}{theoremMsg}"

  Please ensure all updated throwError strings within throwQVCGenStepError (including the ones for Pr[...] = Pr[...] goals and raw wp mode) are prefixed with m!.

Nitpicks:

• Reusing expressions: In findUniqueHoareCutHint? and findUniqueLoopInvHint?, the pattern found.toList.head? >>= fun first => if found.size = 1 then some first else none is perfectly correct and functional, though if found.size == 1 then some found[0]! else none avoids allocating the intermediate list and might be slightly more idiomatic for arrays.

📄 **Review for `VCVio/ProgramLogic/Unary/HoareTriple.lean`**

Verdict: Approved

Critical Misformalizations:
None

Lean 4 / Mathlib Issues:
None

Nitpicks:

• For iff lemmas that are typically used as rewrite rules (like le_probEvent_iff_triple_indicator and le_probOutput_iff_triple_indicator), it is customary in Mathlib to make arguments that appear on both sides and can be inferred from the goal implicit (e.g., {oa : OracleComp spec α} {p : α → Prop}). While rw in Lean 4 is smart enough to instantiate explicit arguments via unification, making them implicit makes the lemmas more ergonomic to use with apply or exact.