`eager proc` only accepts equalities as invariant

[JoaoDiogoDuarte]

Situation

eager proc I rejects any invariant that is not a conjunction of same-name variable equalities:

eager: the invariant must be a conjunction of same-name variable equalities

Minimal example (eager_equiv_inv.ec, EasyCrypt r2026.05-23-g7f13cec):

require import AllCore.

module type OT = { proc get(x : int) : int }.
module type AT (O : OT) = { proc run() : bool }.

section.
declare module O <: OT.
declare module A <: AT {-O}.

declare op R : (glob O) -> (glob O) -> bool.
declare axiom R_eqv : forall a b c, R a a /\ (R a b => R b a) /\ (R a b => R b c => R a c).

local module OW = { proc get(x : int) = { var r; r <@ O.get(x); return r; } }.

local module S = {
  var y : int
  proc s() = { y <@ O.get(0); }
}.

local lemma challenge_commutes :
  eager [S.s();, A(OW).run ~ A(OW).run, S.s(); :
         ={glob A, S.y} /\ R (glob O){1} (glob O){2}
     ==> ={res, glob A, S.y} /\ R (glob O){1} (glob O){2}].
proof.
  eager proc (={S.y} /\ R (glob O){1} (glob O){2}).   (* rejected here *)
  admit.
qed.
end section.

The tactic simply refuses the invariant. Equality is the special case R := (=), so the generalization would not change existing proofs.

Workarounds do not help. Restricting to oracles whose R is equality excludes exactly the oracles whose state is not observable.

Why this is useful (at least for me):

Lazy and eager sampling abstract oracles. - A random oracle sampled on demand and one whose table is drawn in advance give the same answers, but their memories differ. Relating them query by query needs an invariant such as "the two tables agree wherever both are defined", or "the same answers are committed". That is an equivalence on glob O, but not exactly ={glob O}.

Solution Claude proposed because I am bad at ocaml and do not understand EasyCrypt's underlying code

Feature: invariants that are equivalence relations

• It is purely the syntactic gate ensure_eq_shape (ecPhlEager.ml:140–145), called at line 327. The rest of the rule already treats I as an arbitrary two-sided formula: equivF_abs_spec takes any ts_inv, and sg_d is S ~ S : I ==> I.
• The one place equality is used. Goal (f), "o′ ~ o′ : Eq ==> I ∧ ={res}", builds its precondition from eq_on_fun, i.e. equality on everything o′ uses (lines 343–347). This is the step that relates a run to itself, and it is where equality stands in for reflexivity.
• Suggested change.
  a. Replace ensure_eq_shape with generated side goals stating that I is an equivalence on the two memories:
  • reflexive: forall &m, I{m,m};
  • symmetric: forall &1 &2, I{1,2} => I{2,1};
  • transitive: forall &1 &2 &3, I{1,2} => I{2,3} => I{1,3}.
    A conjunction of same-name equalities meets all three trivially, so the current shape check could stay as a fast path that skips these goals.
    b. In goal (f), replace the Eq precondition by I (with ={o′.params}), or keep Eq ∧ I, whichever the meta-proof needs.
    c. Keep the existing checks: the invariant must not depend on A, and the oracles must not use A. Point 1's check also stays, since point 2 relies on S not touching A.

For direct equality, no need to even expose this to the user, keep as is (prevents breaking existing proofs)

• Caveat. This changes a rule's side conditions, so the rule's soundness proof has to be redone. As far as I can tell, equality is used only through reflexivity, the chaining of steps (transitivity), and running a program against itself in (f). But that should be confirmed against the original justification of the eager rules before relaxing the gate.

[fdupress]

@loutr and @bgregoir changed eager recently to strengthen the constraint back to "conjunction of equalities".

Guys, is there scope for loosening it back, or does it immediately yield an unsound rule?

[bgregoir]

This is funny, we encounter exactly the same problem yesterday with @loutr. We solved the proof by first introducing an intermediate games enforcing the invariant (by adding "if" in the code), and then using eager tactic. We agree that the eager proc rule should allows stronger invariant like the if, seq and while rule already do. But this require to be able to write properly the proof first. So it will not be immediate.

[fdupress]

I think @JoaoDiogoDuarte is after a rule where the relational part of the invariant is a general relation. Your solution here would not work there, and this is the bit I'm not sure is sound.

For updating the rule, perhaps a conseq pRHL HL HL => pRHL-style rule would work here? (And could even be out of the TCB if you find a way of defining a module inside a proof...)