From bdce72bd8c38da5ffb837392c03265d0dc4ad7e5 Mon Sep 17 00:00:00 2001
From: Gustavo Delerue <gxdelerue@proton.me>
Date: Tue, 25 Nov 2025 11:55:35 +0000
Subject: [PATCH] Fix sym memory

---
 src/phl/ecPhlSym.ml | 10 +++++-----
 tests/phl_sym.ec    | 27 +++++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 5 deletions(-)
 create mode 100644 tests/phl_sym.ec

diff --git a/src/phl/ecPhlSym.ml b/src/phl/ecPhlSym.ml
index 4868fa478..4f0b20cea 100644
--- a/src/phl/ecPhlSym.ml
+++ b/src/phl/ecPhlSym.ml
@@ -9,8 +9,8 @@ open EcSubst
 let t_equivF_sym tc =
   let ef     = tc1_as_equivF tc in
   let ml, mr = ef.ef_ml, ef.ef_mr in
-  let pr     = {ml;mr;inv=(ts_inv_rebind (ef_pr ef) mr ml).inv} in
-  let po     = {ml;mr;inv=(ts_inv_rebind (ef_po ef) mr ml).inv} in
+  let pr     = {ml=mr;mr=ml;inv=(ts_inv_rebind (ef_pr ef) mr ml).inv} in
+  let po     = {ml=mr;mr=ml;inv=(ts_inv_rebind (ef_po ef) mr ml).inv} in
   let cond   = f_equivF pr ef.ef_fr ef.ef_fl po in
   FApi.xmutate1 tc `EquivSym [cond]
 
@@ -18,9 +18,9 @@ let t_equivF_sym tc =
 let t_equivS_sym tc =
   let es    = tc1_as_equivS tc in
   let (ml, mtl), (mr, mtr) = es.es_ml, es.es_mr in
-  let pr    = {ml;mr;inv=(ts_inv_rebind (es_pr es) mr ml).inv} in
-  let po    = {ml;mr;inv=(ts_inv_rebind (es_po es) mr ml).inv} in
-  let cond  = f_equivS mtl mtr pr es.es_sr es.es_sl po in
+  let pr    = {mr=ml;ml=mr;inv=(ts_inv_rebind (es_pr es) mr ml).inv} in
+  let po    = {mr=ml;ml=mr;inv=(ts_inv_rebind (es_po es) mr ml).inv} in
+  let cond  = f_equivS mtr mtl pr es.es_sr es.es_sl po in
   FApi.xmutate1 tc `EquivSym [cond]
 
 (*-------------------------------------------------------------------- *)
diff --git a/tests/phl_sym.ec b/tests/phl_sym.ec
new file mode 100644
index 000000000..aa9eb5b21
--- /dev/null
+++ b/tests/phl_sym.ec
@@ -0,0 +1,27 @@
+require import AllCore Int.
+
+
+module M = {
+  proc f1(a: int) = {
+    var c : int;
+    c <- a;
+    return c;
+  }
+
+  proc f2(a: int) = {
+    var d;
+    d <@ f1 (a);
+    
+    return d;
+  }
+}.
+
+lemma aux (a_: int) : hoare[M.f1 : a_ = a ==> res = a_].
+proof. proc; auto. qed.
+
+lemma test : equiv[M.f2 ~ M.f2 : ={arg} ==> ={res}].
+proc.
+inline {1}.
+symmetry.
+proc change {2} [1-2] : { a0 <- a; }. 
+abort.