From a77eec782fb33e082d05c84eb51d9716e8fc6992 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 6 Oct 2026 23:28:53 +0200 Subject: [PATCH] refactor(pl): symmetry as recheckable per-logic rules PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `symmetry` tactic class: - rules/equiv/ecEquivSym.ml: the two trusted symmetry rules of the equiv logic, for statements (`equiv [c ~ c' : P ==> Q]` from `equiv [c' ~ c : P' ==> Q']`, the memory types exchanged as well) and for procedures, where P' and Q' are P and Q with their two memories swapped. Each is documented as an inference rule in the .mli and emits a (parameterless) node with a registered checker ("equivS-sym", "equivF-sym"). The subgoal builder needs no environment and the rules have no side condition. - EcPhlSym is reduced to the dispatcher (interface unchanged), still used by `symmetry` and `rewrite equiv`. Behaviour is unchanged. A new test, tests/sym-equiv.ec, exercises both rules (including different local variables on each side) and the error paths; it passes with the builds before and after this change. The stdlib and the unit tests pass under EC_RECHECK=1 with no RecheckFailure; each checker, when deliberately broken, is caught only under EC_RECHECK (on the new test, and on the stdlib: equivS-sym 4 files, equivF-sym 4). --- src/phl/ecPhlSym.ml | 35 +++++------------- src/phl/rules/equiv/ecEquivSym.ml | 51 ++++++++++++++++++++++++++ src/phl/rules/equiv/ecEquivSym.mli | 29 +++++++++++++++ tests/sym-equiv.ec | 59 ++++++++++++++++++++++++++++++ 4 files changed, 148 insertions(+), 26 deletions(-) create mode 100644 src/phl/rules/equiv/ecEquivSym.ml create mode 100644 src/phl/rules/equiv/ecEquivSym.mli create mode 100644 tests/sym-equiv.ec diff --git a/src/phl/ecPhlSym.ml b/src/phl/ecPhlSym.ml index 7d706dcc36..cb3e931130 100644 --- a/src/phl/ecPhlSym.ml +++ b/src/phl/ecPhlSym.ml @@ -1,31 +1,14 @@ -(*-------------------------------------------------------------------- *) -open EcFol -open EcCoreGoal -open EcLowPhlGoal +(* -------------------------------------------------------------------- *) open EcAst -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 cond = f_equivF pr ef.ef_fr ef.ef_fl po in - FApi.xmutate1 tc `EquivSym [cond] -(*-------------------------------------------------------------------- *) -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 mtr mtl pr es.es_sr es.es_sl po in - FApi.xmutate1 tc `EquivSym [cond] +open EcCoreGoal +open EcLowPhlGoal -(*-------------------------------------------------------------------- *) -let t_equiv_sym tc = +(* -------------------------------------------------------------------- *) +(* The [sym] rules (statement and procedure equiv) live in + [rules/equiv/ecEquivSym.ml]. This module only keeps the dispatcher. *) +let t_equiv_sym (tc : tcenv1) = match (FApi.tc1_goal tc).f_node with - | FequivF _ -> t_equivF_sym tc - | FequivS _ -> t_equivS_sym tc + | FequivF _ -> EcEquivSym.t_equivF_sym tc + | FequivS _ -> EcEquivSym.t_equivS_sym tc | _ -> tc_error_noXhl ~kinds:[`Equiv `Any] !!tc diff --git a/src/phl/rules/equiv/ecEquivSym.ml b/src/phl/rules/equiv/ecEquivSym.ml new file mode 100644 index 0000000000..aa2b8e4292 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSym.ml @@ -0,0 +1,51 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* The equiv [sym] rules have no parameters. *) +type EcCoreGoal.rule += + | REquivSSym + | REquivFSym + +(* -------------------------------------------------------------------- *) +(* Pure cores shared by the rules and their checkers: exchange the two + programs (and memory types), and swap the memories of the pre- and + postcondition. They need no environment and have no side condition. *) +let equivS_sym_subgoals (es : equivS) : form list = + 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 + [f_equivS mtr mtl pr es.es_sr es.es_sl po] + +let equivF_sym_subgoals (ef : equivF) : form list = + 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 + [f_equivF pr ef.ef_fr ef.ef_fl po] + +(* -------------------------------------------------------------------- *) +(* Rules (TCB). *) +let t_equivS_sym (tc : tcenv1) = + let es = tc1_as_equivS tc in + FApi.xrule1 tc REquivSSym (equivS_sym_subgoals es) + +let t_equivF_sym (tc : tcenv1) = + let ef = tc1_as_equivF tc in + FApi.xrule1 tc REquivFSym (equivF_sym_subgoals ef) + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivSSym -> + Some (EcPlRecheck.checker_of "equivS-sym" pf_as_equivS + (fun _hyps es -> equivS_sym_subgoals es)) + | REquivFSym -> + Some (EcPlRecheck.checker_of "equivF-sym" pf_as_equivF + (fun _hyps ef -> equivF_sym_subgoals ef)) + | _ -> None) diff --git a/src/phl/rules/equiv/ecEquivSym.mli b/src/phl/rules/equiv/ecEquivSym.mli new file mode 100644 index 0000000000..3b4dc0c091 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivSym.mli @@ -0,0 +1,29 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal.FApi + +(* ==================================================================== *) +(* Rules (trusted) *) + +(* [t_equivS_sym] — exchange of the two sides: + + equiv [c' ~ c : P[&2/&1, &1/&2] ==> Q[&2/&1, &1/&2]] + ---------------------------------------------------- + equiv [c ~ c' : P ==> Q] + + The two statements and the types of their memories are exchanged; the + relations [P] and [Q] are kept, with their two memories swapped (a + simultaneous substitution [&1 := &2, &2 := &1]). No side condition. + + Node: [REquivSSym]. Checker: "equivS-sym". *) +val t_equivS_sym : backward + +(* [t_equivF_sym] — same for procedures: + + equiv [f' ~ f : P[&2/&1, &1/&2] ==> Q[&2/&1, &1/&2]] + ---------------------------------------------------- + equiv [f ~ f' : P ==> Q] + + In [Q], [res{1}] and [res{2}] are exchanged along with the memories. + + Node: [REquivFSym]. Checker: "equivF-sym". *) +val t_equivF_sym : backward diff --git a/tests/sym-equiv.ec b/tests/sym-equiv.ec new file mode 100644 index 0000000000..942f295f48 --- /dev/null +++ b/tests/sym-equiv.ec @@ -0,0 +1,59 @@ +require import AllCore. + +module M = { + proc f(a : int) : int = { + var x; + x <- a + 1; + return x; + } + + proc g(b : int) : int = { + var y, z; + y <- b; + z <- y; + return z; + } +}. + +(* Procedure form: the procedures are exchanged, and the memories of the + pre- and postcondition (including [res]) are swapped. *) +lemma g_f : equiv [M.g ~ M.f : b{1} = a{2} + 1 ==> res{1} = res{2}]. +proof. by proc; auto. qed. + +lemma f_g : equiv [M.f ~ M.g : a{1} + 1 = b{2} ==> res{2} = res{1}]. +proof. by symmetry; conseq g_f. qed. + +lemma f_g_exact : equiv [M.f ~ M.g : b{2} = a{1} + 1 ==> res{2} = res{1}]. +proof. symmetry; exact g_f. qed. + +(* Statement form: the statements, and the types of the memories (here, + different local variables), are exchanged. *) +lemma f_g_stmt : equiv [M.f ~ M.g : a{1} + 1 = b{2} ==> res{1} = res{2}]. +proof. +proc; symmetry. +wp; skip => /> &1 &2. +qed. + +lemma f_g_stmt_locals : equiv [M.f ~ M.g : a{1} + 1 = b{2} ==> res{1} = res{2}]. +proof. +proc; symmetry. +conseq (: b{1} = a{2} + 1 ==> z{1} = x{2}) => //. +by sp; skip. +qed. + +(* Errors: [symmetry] only applies to equiv judgements. *) +lemma hoare_sym : hoare [M.f : a = 1 ==> res = 2]. +proof. +fail symmetry. +proc. +fail symmetry. +by auto. +qed. + +lemma phoare_sym : phoare [M.f : a = 1 ==> res = 2] = 1%r. +proof. +fail symmetry. +proc. +fail symmetry. +by auto. +qed.