refactor(pl): symmetry as recheckable per-logic rules

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

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)

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

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.