From dbe3d72c038533268aba2a5596310d687b054523 Mon Sep 17 00:00:00 2001 From: Xingyu Xie Date: Mon, 24 Aug 2026 10:54:23 +0200 Subject: [PATCH] fix(equiv): equivF_abs must check glob-A footprint on both oracles `FunAbsLow.equivF_abs_spec` (and `equivF_abs_upto`) ran `check_oracle_use` on the right oracle only when it was syntactically equal to the left one. With two distinct oracle modules where the right oracle writes a global that belongs to `glob A`, the `={glob A}` obligation was silently dropped while still asserted in the conclusion, so EC accepted a false equiv[ A(O1).main ~ A(O2).main : ={glob A} ==> ={res} ] which `byequiv` turns into `1 = 0`. Check both oracles unconditionally, each against its own abstract top (`topl`/`topr`). When either oracle touches `glob A` the `eqglob` obligation is now correctly required. This exposes a pre-existing unsoundness in the standard library: `theories/query_counting/Counter.eca` declares the distinguisher `D` with `{ -S }` but not `{ -Counter }`, so `Counter.c` is in `glob D` and the counter-incrementing right oracle writes it. `ind_counting` is therefore false (a distinguisher that branches on `Counter.c` queries a different number of times against `S` vs `Counter(S)`). Restrict `D` to `{ -S, -Counter }` (the file's second section already uses `{ -Counter }`); the stdlib then builds clean (128/128). Regression: tests/equivf-abs-oracle-glob.ec (asserts the buggy proof no longer closes, via the `fail` idiom). Co-Authored-By: Claude Opus 4.8 --- src/phl/ecPhlFun.ml | 6 ++---- tests/equivf-abs-oracle-glob.ec | 31 +++++++++++++++++++++++++++++ theories/query_counting/Counter.eca | 2 +- 3 files changed, 34 insertions(+), 5 deletions(-) create mode 100644 tests/equivf-abs-oracle-glob.ec diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml index 6b1449c3c4..67d367f1b4 100644 --- a/src/phl/ecPhlFun.ml +++ b/src/phl/ecPhlFun.ml @@ -205,8 +205,7 @@ module FunAbsLow = struct let use = try check_oracle_use pf env topl o_l; - if EcPath.x_equal o_l o_r - then check_oracle_use pf env topl o_r; + check_oracle_use pf env topr o_r; false with _ -> true in @@ -330,8 +329,7 @@ module UpToLow = struct let ospec o_l o_r = check_oracle_use pf env topl o_l; - if EcPath.x_equal o_l o_r - then check_oracle_use pf env topl o_r; + check_oracle_use pf env topr o_r; let fo_l = EcEnv.Fun.by_xpath o_l env in let fo_r = EcEnv.Fun.by_xpath o_r env in diff --git a/tests/equivf-abs-oracle-glob.ec b/tests/equivf-abs-oracle-glob.ec new file mode 100644 index 0000000000..83e7b3fa14 --- /dev/null +++ b/tests/equivf-abs-oracle-glob.ec @@ -0,0 +1,31 @@ +(* Regression for the equivF_abs oracle-footprint asymmetry. + + `equiv ... proc` for an abstract adversary must require that BOTH oracles + leave `glob A` unchanged, not only the left one. Here the right oracle O2 + writes the concrete global Shared.g (which an unrestricted `A` may touch, so + Shared.g in glob A) while the left oracle O1 does not, so the `={glob A}` + invariant is not preserved by the oracle pair and this equiv is not provable. + + Before the fix `check_oracle_use` was run on the right oracle only when + o_l = o_r, so the distinct-oracle case silently dropped the obligation and + the proof below closed (and could be turned into a proof of `false`). With + the fix the O2 `={glob A}` obligation remains, so the closing `by` must + fail. *) +require import AllCore. + +module Shared = { var g : int }. + +module type O = { proc f() : unit }. +module type Adv (M : O) = { proc main() : int }. + +module O1 : O = { proc f() : unit = { } }. +module O2 : O = { proc f() : unit = { Shared.g <- Shared.g + 1; } }. + +section. +declare module A <: Adv. + +lemma bad : equiv[ A(O1).main ~ A(O2).main : ={glob A} ==> ={res} ]. +proof. +fail (by proc (true) => //; proc; auto). +abort. +end section. diff --git a/theories/query_counting/Counter.eca b/theories/query_counting/Counter.eca index 432dbb04b7..d119448214 100644 --- a/theories/query_counting/Counter.eca +++ b/theories/query_counting/Counter.eca @@ -35,7 +35,7 @@ module Counter(S : System) = { section. declare module S <: System { -Counter }. - declare module D <: Distinguisher { -S }. + declare module D <: Distinguisher { -S, -Counter }. lemma ind_counting (E : (glob S) -> bool) &m: