Making program logic formulas memory-agnostic

[oskgo]

Rather than program logic formulas hardcoding mhr as the bound memory in single sided formulas and mleft and mright as the bound memories in two sided formulas we make the formulas carry along the bound memor(y/ies).

The end goal is to allow things like nested hoare statements.

Re-do of #762

The number of touched files in the PR is causing significant slowdown in the GitHub web-interface on my end, so if this happens to anyone else just waiting half a minute seems to work.

[Copilot]

Pull Request Overview

This PR makes program logic formulas memory-agnostic by allowing formulas to carry along their bound memory(ies) instead of hardcoding specific memories like mhr, mleft, and mright. This enables more flexible composition of logic statements and supports nested Hoare statements.

Key changes include:

• Introduction of ss_inv and ts_inv types for single-sided and two-sided invariants that carry memory information
• Refactoring of formula construction and manipulation functions to work with memory-parameterized types
• Updates to proof tactics and reasoning rules to handle the new memory-aware formula structures

Reviewed Changes

Copilot reviewed 90 out of 90 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
theories/modules/EventPartitioning.ec	Updates probabilistic reasoning with memory-aware formula transformations
theories/crypto/KeyEncapsulationMechanisms.eca	Adds memory context preservation in cryptographic proofs
theories/algebra/Ring.ec	Adds simplification hint for ring subtraction
theories/algebra/Ideal.ec	Removes redundant proof step now handled by simplification
src/phl/ecPhlWp.ml	Core weakest precondition changes for memory-parameterized formulas
src/phl/ecPhlWhile.mli	Updates function signatures for memory-aware while loop tactics
src/phl/ecPhlWhile.ml	Comprehensive refactoring of while loop reasoning with new memory types
src/phl/ecPhlUpto.ml	Updates up-to reasoning for memory-parameterized formulas
src/phl/ecPhlTrans.mli	Updates transitivity rule signatures for new memory types
src/phl/ecPhlTrans.ml	Refactors transitivity reasoning with memory-aware formulas
src/phl/ecPhlTAuto.ml	Updates automatic tactics for memory-parameterized judgments
src/phl/ecPhlSym.ml	Simplifies symmetry rules using new memory rebinding functions
src/phl/ecPhlSwap.ml	Updates statement swapping for new memory handling
src/phl/ecPhlSp.ml	Refactors symbolic execution with memory-parameterized formulas
src/phl/ecPhlSkip.ml	Updates skip rule for memory-aware formulas
src/phl/ecPhlRwEquiv.ml	Updates equivalence rewriting for new memory types
src/phl/ecPhlRnd.mli	Updates random sampling rule signatures
src/phl/ecPhlRnd.ml	Comprehensive refactoring of randomness reasoning
src/phl/ecPhlRewrite.ml	Updates expression rewriting for memory-parameterized formulas
src/phl/ecPhlRCond.ml	Updates conditional reasoning with new memory types
src/phl/ecPhlPrRw.mli	Updates probability rewriting signatures
src/phl/ecPhlPrRw.ml	Refactors probability rewriting for memory-aware formulas
src/phl/ecPhlPr.mli	Updates probability reasoning signatures
src/phl/ecPhlPr.ml	Updates probability tactics for memory-parameterized formulas
src/phl/ecPhlOutline.ml	Simplifies outlining with improved memory handling
src/phl/ecPhlLoopTx.ml	Updates loop transformations for new memory types
src/phl/ecPhlInline.ml	Updates inlining tactics for memory-aware formulas
src/phl/ecPhlHiBdHoare.ml	Updates bounded Hoare logic for new memory types

---

_{Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.}

[fdupress]

External CI is green, @oskgo.