refactor(pl): true, zero and exfalso as recheckable per-logic rules

src/phl/ecPhlTAuto.ml

@@ -6,52 +6,28 @@ open EcCoreGoal
 open EcLowPhlGoal
 
 (* -------------------------------------------------------------------- *)
-
-let t_hoare_true_r tc =
-  match (FApi.tc1_goal tc).f_node with
-  | FhoareF hf when POE.forall (f_equal f_true) (hf_po hf).hsi_inv ->
-      FApi.xmutate1 tc `HoareTrue []
-
-  | FhoareS hs when POE.forall (f_equal f_true) (hs_po hs).hsi_inv ->
-      FApi.xmutate1 tc `HoareTrue []
-
-  | _ ->
-    tc_error !!tc
-      "the conclusion is not of the form %s"
-      "hoare[_ : _ ==> true]"
-
-let t_hoare_true = FApi.t_low0 "hoare-true" t_hoare_true_r
+(* The rules closing trivially valid judgements live, one module per rule
+   and logic, in [rules/<logic>/]: [true] (hoare), [zero] (ehoare) and
+   [exfalso] (hoare, bdhoare, equiv). This module only keeps the legacy
+   entry points and the logic-agnostic [exfalso] dispatcher. *)
 
 (* -------------------------------------------------------------------- *)
-let f_xr0 = f_r2xr f_r0
+let t_hoare_true = EcHoareTrue.t_hoare_true
 
-let t_ehoare_zero_r tc =
-  match (FApi.tc1_goal tc).f_node with
-  | FeHoareF hf when f_equal (ehf_po hf).inv f_xr0 ->
-       FApi.xmutate1 tc `eHoareZero []
-
-  | FeHoareS hs when f_equal (ehs_po hs).inv f_xr0 ->
-       FApi.xmutate1 tc `eHoareZero []
-  | _ ->
-    tc_error !!tc
-      "the conclusion is not of the form %s"
-      "ehoare[_ : _ ==> 0%xr]"
-
-let t_ehoare_zero = FApi.t_low0 "hoare-zero" t_ehoare_zero_r
+let t_ehoare_zero = EcEHoareZero.t_ehoare_zero
 
 (* -------------------------------------------------------------------- *)
-let t_core_exfalso_r tc =
-  let pre   = tc1_get_pre tc in
-    if not (f_equal (inv_of_inv pre) f_false) then
-      tc_error !!tc "pre-condition is not `false'";
-    match (FApi.tc1_goal tc).f_node with
-    | FbdHoareS bhs ->
-      FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv bhs.bhs_m 
-        (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs))]
-    | FbdHoareF bhf ->
-      let (me, _) = EcEnv.Fun.hoareF_memenv (bhf.bhf_m) bhf.bhf_f (FApi.tc1_env tc) in
-      FApi.xmutate1 tc `ExFalso [EcSubst.f_forall_mems_ss_inv me 
-        (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf))]
-    | _ -> FApi.xmutate1 tc `ExFalso []
-
-let t_core_exfalso = FApi.t_low0 "core-exfalso" t_core_exfalso_r
+(* An ehoare precondition is an expectation, never [false]: [exfalso] has no
+   ehoare rule, and such goals are rejected by the precondition check. *)
+let t_core_exfalso (tc : tcenv1) =
+  let pre = tc1_get_pre tc in
+  if not (f_equal (inv_of_inv pre) f_false) then
+    tc_error !!tc "pre-condition is not `false'";
+  match (FApi.tc1_goal tc).f_node with
+  | FhoareS   _ -> EcHoareExfalso.t_hoareS_exfalso tc
+  | FhoareF   _ -> EcHoareExfalso.t_hoareF_exfalso tc
+  | FbdHoareS _ -> EcBdHoareExfalso.t_bdhoareS_exfalso tc
+  | FbdHoareF _ -> EcBdHoareExfalso.t_bdhoareF_exfalso tc
+  | FequivS   _ -> EcEquivExfalso.t_equivS_exfalso tc
+  | FequivF   _ -> EcEquivExfalso.t_equivF_exfalso tc
+  | _           -> tc_error !!tc "pre-condition is not `false'"

src/phl/rules/bdhoare/ecBdHoareExfalso.ml

@@ -0,0 +1,57 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+open EcEnv
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The bdhoare [exfalso] rules have no parameters. *)
+type EcCoreGoal.rule +=
+  | RBdHoareSExfalso
+  | RBdHoareFExfalso
+
+(* -------------------------------------------------------------------- *)
+(* Pure cores shared by the rules and their checkers. The side condition
+   (the precondition is syntactically [false]) is part of them, so the
+   checker re-validates it. *)
+let bdhoareS_exfalso_subgoals (bhs : bdHoareS) : form list =
+  if not (f_equal (bhs_pr bhs).inv f_false) then
+    failwith "bdhoareS-exfalso: the precondition is not false";
+  [EcSubst.f_forall_mems_ss_inv bhs.bhs_m
+     (map_ss_inv1 (f_real_le f_r0) (bhs_bd bhs))]
+
+let bdhoareF_exfalso_subgoals (hyps : LDecl.hyps) (bhf : bdHoareF) : form list =
+  if not (f_equal (bhf_pr bhf).inv f_false) then
+    failwith "bdhoareF-exfalso: the precondition is not false";
+  let me, _ = Fun.hoareF_memenv bhf.bhf_m bhf.bhf_f (LDecl.toenv hyps) in
+  [EcSubst.f_forall_mems_ss_inv me
+     (map_ss_inv1 (f_real_le f_r0) (bhf_bd bhf))]
+
+(* -------------------------------------------------------------------- *)
+let not_false tc = tc_error !!tc "pre-condition is not `false'"
+
+(* Rules (TCB). *)
+let t_bdhoareS_exfalso (tc : tcenv1) =
+  let bhs = tc1_as_bdhoareS tc in
+  if not (f_equal (bhs_pr bhs).inv f_false) then not_false tc;
+  FApi.xrule1 tc RBdHoareSExfalso (bdhoareS_exfalso_subgoals bhs)
+
+let t_bdhoareF_exfalso (tc : tcenv1) =
+  let bhf = tc1_as_bdhoareF tc in
+  if not (f_equal (bhf_pr bhf).inv f_false) then not_false tc;
+  FApi.xrule1 tc RBdHoareFExfalso
+    (bdhoareF_exfalso_subgoals (FApi.tc1_hyps tc) bhf)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | RBdHoareSExfalso ->
+         Some (EcPlRecheck.checker_of "bdhoareS-exfalso" pf_as_bdhoareS
+                 (fun _hyps bhs -> bdhoareS_exfalso_subgoals bhs))
+     | RBdHoareFExfalso ->
+         Some (EcPlRecheck.checker_of "bdhoareF-exfalso" pf_as_bdhoareF
+                 (fun hyps bhf -> bdhoareF_exfalso_subgoals hyps bhf))
+     | _ -> None)

src/phl/rules/bdhoare/ecBdHoareExfalso.mli

@@ -0,0 +1,28 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+(* [t_bdhoareS_exfalso] — false precondition, with [~] the goal's
+   comparison:
+
+          forall &m, 0%r <= d
+     -------------------------------
+     phoare [c : false ==> Q] ~ d
+
+   Side condition: the precondition is syntactically [false] (otherwise
+   fails).
+
+   Node: [RBdHoareSExfalso]. Checker: "bdhoareS-exfalso". *)
+val t_bdhoareS_exfalso : backward
+
+(* [t_bdhoareF_exfalso] — same for a procedure (the premise quantifies over
+   the procedure's initial memory):
+
+          forall &m, 0%r <= d
+     -------------------------------
+     phoare [f : false ==> Q] ~ d
+
+   Node: [RBdHoareFExfalso]. Checker: "bdhoareF-exfalso". *)
+val t_bdhoareF_exfalso : backward

src/phl/rules/ehoare/ecEHoareZero.ml

@@ -0,0 +1,63 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The ehoare [zero] rules have no parameters. *)
+type EcCoreGoal.rule +=
+  | REHoareSZero
+  | REHoareFZero
+
+(* -------------------------------------------------------------------- *)
+let f_xr0 = f_r2xr f_r0
+
+(* Pure cores shared by the rules and their checkers: no premise; the side
+   condition (the postcondition is syntactically [0%xr]) is part of them, so
+   the checker re-validates it. *)
+let ehoareS_zero_subgoals (hs : eHoareS) : form list =
+  if not (f_equal (ehs_po hs).inv f_xr0) then
+    failwith "ehoareS-zero: the postcondition is not 0%xr";
+  []
+
+let ehoareF_zero_subgoals (hf : eHoareF) : form list =
+  if not (f_equal (ehf_po hf).inv f_xr0) then
+    failwith "ehoareF-zero: the postcondition is not 0%xr";
+  []
+
+(* -------------------------------------------------------------------- *)
+let not_of_the_form tc =
+  tc_error !!tc "the conclusion is not of the form %s" "ehoare[_ : _ ==> 0%xr]"
+
+(* Rules (TCB). *)
+let t_ehoareS_zero (tc : tcenv1) =
+  let hs = tc1_as_ehoareS tc in
+  if not (f_equal (ehs_po hs).inv f_xr0) then not_of_the_form tc;
+  FApi.xrule1 tc REHoareSZero (ehoareS_zero_subgoals hs)
+
+let t_ehoareF_zero (tc : tcenv1) =
+  let hf = tc1_as_ehoareF tc in
+  if not (f_equal (ehf_po hf).inv f_xr0) then not_of_the_form tc;
+  FApi.xrule1 tc REHoareFZero (ehoareF_zero_subgoals hf)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | REHoareSZero ->
+         Some (EcPlRecheck.checker_of "ehoareS-zero" pf_as_ehoareS
+                 (fun _hyps hs -> ehoareS_zero_subgoals hs))
+     | REHoareFZero ->
+         Some (EcPlRecheck.checker_of "ehoareF-zero" pf_as_ehoareF
+                 (fun _hyps hf -> ehoareF_zero_subgoals hf))
+     | _ -> None)
+
+(* -------------------------------------------------------------------- *)
+(* Dispatcher (no node of its own). *)
+let t_ehoare_zero (tc : tcenv1) =
+  match (FApi.tc1_goal tc).f_node with
+  | FeHoareS _ -> t_ehoareS_zero tc
+  | FeHoareF _ -> t_ehoareF_zero tc
+  | _          -> not_of_the_form tc

src/phl/rules/ehoare/ecEHoareZero.mli

@@ -0,0 +1,31 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+(* [t_ehoareS_zero] — null expectation:
+
+     --------------------------
+     ehoare [c : P ==> 0%xr]
+
+   No premise. Side condition: the postcondition is syntactically [0%xr]
+   (otherwise fails).
+
+   Node: [REHoareSZero]. Checker: "ehoareS-zero". *)
+val t_ehoareS_zero : backward
+
+(* [t_ehoareF_zero] — same for a procedure:
+
+     --------------------------
+     ehoare [f : P ==> 0%xr]
+
+   Node: [REHoareFZero]. Checker: "ehoareF-zero". *)
+val t_ehoareF_zero : backward
+
+(* ==================================================================== *)
+(* Derived tactics                                                      *)
+
+(* [t_ehoare_zero] — [t_ehoareS_zero] or [t_ehoareF_zero], depending on the
+   goal. *)
+val t_ehoare_zero : backward

src/phl/rules/equiv/ecEquivExfalso.ml

@@ -0,0 +1,52 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The equiv [exfalso] rules have no parameters. *)
+type EcCoreGoal.rule +=
+  | REquivSExfalso
+  | REquivFExfalso
+
+(* -------------------------------------------------------------------- *)
+(* Pure cores shared by the rules and their checkers: no premise; the side
+   condition (the precondition is syntactically [false]) is part of them, so
+   the checker re-validates it. *)
+let equivS_exfalso_subgoals (es : equivS) : form list =
+  if not (f_equal (es_pr es).inv f_false) then
+    failwith "equivS-exfalso: the precondition is not false";
+  []
+
+let equivF_exfalso_subgoals (ef : equivF) : form list =
+  if not (f_equal (ef_pr ef).inv f_false) then
+    failwith "equivF-exfalso: the precondition is not false";
+  []
+
+(* -------------------------------------------------------------------- *)
+let not_false tc = tc_error !!tc "pre-condition is not `false'"
+
+(* Rules (TCB). *)
+let t_equivS_exfalso (tc : tcenv1) =
+  let es = tc1_as_equivS tc in
+  if not (f_equal (es_pr es).inv f_false) then not_false tc;
+  FApi.xrule1 tc REquivSExfalso (equivS_exfalso_subgoals es)
+
+let t_equivF_exfalso (tc : tcenv1) =
+  let ef = tc1_as_equivF tc in
+  if not (f_equal (ef_pr ef).inv f_false) then not_false tc;
+  FApi.xrule1 tc REquivFExfalso (equivF_exfalso_subgoals ef)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | REquivSExfalso ->
+         Some (EcPlRecheck.checker_of "equivS-exfalso" pf_as_equivS
+                 (fun _hyps es -> equivS_exfalso_subgoals es))
+     | REquivFExfalso ->
+         Some (EcPlRecheck.checker_of "equivF-exfalso" pf_as_equivF
+                 (fun _hyps ef -> equivF_exfalso_subgoals ef))
+     | _ -> None)

src/phl/rules/equiv/ecEquivExfalso.mli

@@ -0,0 +1,24 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+(* [t_equivS_exfalso] — false precondition:
+
+     ------------------------------
+     equiv [c ~ c' : false ==> Q]
+
+   No premise. Side condition: the precondition is syntactically [false]
+   (otherwise fails).
+
+   Node: [REquivSExfalso]. Checker: "equivS-exfalso". *)
+val t_equivS_exfalso : backward
+
+(* [t_equivF_exfalso] — same for procedures:
+
+     ------------------------------
+     equiv [f ~ f' : false ==> Q]
+
+   Node: [REquivFExfalso]. Checker: "equivF-exfalso". *)
+val t_equivF_exfalso : backward

src/phl/rules/hoare/ecHoareExfalso.ml

@@ -0,0 +1,52 @@
+(* -------------------------------------------------------------------- *)
+open EcFol
+open EcAst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The hoare [exfalso] rules have no parameters. *)
+type EcCoreGoal.rule +=
+  | RHoareSExfalso
+  | RHoareFExfalso
+
+(* -------------------------------------------------------------------- *)
+(* Pure cores shared by the rules and their checkers: no premise; the side
+   condition (the precondition is syntactically [false]) is part of them, so
+   the checker re-validates it. *)
+let hoareS_exfalso_subgoals (hs : sHoareS) : form list =
+  if not (f_equal (hs_pr hs).inv f_false) then
+    failwith "hoareS-exfalso: the precondition is not false";
+  []
+
+let hoareF_exfalso_subgoals (hf : sHoareF) : form list =
+  if not (f_equal (hf_pr hf).inv f_false) then
+    failwith "hoareF-exfalso: the precondition is not false";
+  []
+
+(* -------------------------------------------------------------------- *)
+let not_false tc = tc_error !!tc "pre-condition is not `false'"
+
+(* Rules (TCB). *)
+let t_hoareS_exfalso (tc : tcenv1) =
+  let hs = tc1_as_hoareS tc in
+  if not (f_equal (hs_pr hs).inv f_false) then not_false tc;
+  FApi.xrule1 tc RHoareSExfalso (hoareS_exfalso_subgoals hs)
+
+let t_hoareF_exfalso (tc : tcenv1) =
+  let hf = tc1_as_hoareF tc in
+  if not (f_equal (hf_pr hf).inv f_false) then not_false tc;
+  FApi.xrule1 tc RHoareFExfalso (hoareF_exfalso_subgoals hf)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | RHoareSExfalso ->
+         Some (EcPlRecheck.checker_of "hoareS-exfalso" pf_as_hoareS
+                 (fun _hyps hs -> hoareS_exfalso_subgoals hs))
+     | RHoareFExfalso ->
+         Some (EcPlRecheck.checker_of "hoareF-exfalso" pf_as_hoareF
+                 (fun _hyps hf -> hoareF_exfalso_subgoals hf))
+     | _ -> None)