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

src/phl/ecPhlSkip.ml

@@ -1,95 +1,19 @@
 (* -------------------------------------------------------------------- *)
-open EcUtils
-open EcFol
 open EcAst
 
 open EcCoreGoal
 open EcLowPhlGoal
-open EcLowGoal
 
 (* -------------------------------------------------------------------- *)
-module LowInternal = struct
-  (* ------------------------------------------------------------------ *)
-  let t_hoare_skip_r tc =
-    let hs = tc1_as_hoareS tc in
-
-    if not (List.is_empty hs.hs_s.s_node) then
-      tc_error !!tc "instruction list is not empty";
-
-    let post = POE.lower (hs_po hs) in
-    let concl = map_ss_inv2 f_imp (hs_pr hs) post in
-    let concl = EcSubst.f_forall_mems_ss_inv hs.hs_m concl in
-
-    FApi.xmutate1 tc `Skip [concl]
-
-  let t_hoare_skip = FApi.t_low0 "hoare-skip" t_hoare_skip_r
-
-  (* ------------------------------------------------------------------ *)
-  let t_ehoare_skip_r tc =
-    let hs = tc1_as_ehoareS tc in
-
-    if not (List.is_empty hs.ehs_s.s_node) then
-      tc_error !!tc "instruction list is not empty";
-
-    let concl = map_ss_inv2 f_xreal_le (ehs_po hs) (ehs_pr hs) in
-    let concl = EcSubst.f_forall_mems_ss_inv hs.ehs_m concl in
-
-    FApi.xmutate1 tc `Skip [concl]
-
-  let t_ehoare_skip = FApi.t_low0 "ehoare-skip" t_ehoare_skip_r
-
-  (* ------------------------------------------------------------------ *)
-  let t_bdhoare_skip_r_low tc =
-    let bhs = tc1_as_bdhoareS tc in
-
-    if not (List.is_empty bhs.bhs_s.s_node) then
-      tc_error !!tc ~who:"skip" "instruction list is not empty";
-    if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then
-      tc_error !!tc ~who:"skip" "";
-
-    let concl = map_ss_inv2 f_imp (bhs_pr bhs) (bhs_po bhs) in
-    let concl = EcSubst.f_forall_mems_ss_inv bhs.bhs_m concl in
-    let goals =
-      if   f_equal (bhs_bd bhs).inv f_r1
-      then [concl]
-      else [f_eq (bhs_bd bhs).inv f_r1; concl]
-    in
-
-    FApi.xmutate1 tc `Skip goals
-
-  (* ------------------------------------------------------------------ *)
-  let t_bdhoare_skip_r tc =
-    let t_trivial = FApi.t_seqs [t_simplify ~delta:`No; t_split; t_fail] in
-    let bhs = tc1_as_bdhoareS tc in
-    let f_r1: EcAst.ss_inv = {m=fst bhs.bhs_m; inv=f_r1} in
-    let t_conseq  = EcPhlConseq.t_bdHoareS_conseq_bd FHeq f_r1 in
-      FApi.t_internal
-        (FApi.t_seqsub t_conseq
-           [FApi.t_try t_trivial; t_bdhoare_skip_r_low])
-        tc
-
-  let t_bdhoare_skip = FApi.t_low0 "bdhoare-skip" t_bdhoare_skip_r
-
-  (* ------------------------------------------------------------------ *)
-  let t_equiv_skip_r tc =
-    let es = tc1_as_equivS tc in
-
-    if not (List.is_empty es.es_sl.s_node) then
-      tc_error !!tc ~who:"skip" "left instruction list is not empty";
-    if not (List.is_empty es.es_sr.s_node) then
-      tc_error !!tc ~who:"skip" "right instruction list is not empty";
-
-    let concl = map_ts_inv2 f_imp (es_pr es) (es_po es) in
-    let concl = EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr concl in
-    FApi.xmutate1 tc `Skip [concl]
-
-  let t_equiv_skip = FApi.t_low0 "equiv-skip" t_equiv_skip_r
-end
-
-(* -------------------------------------------------------------------- *)
-let t_skip =
-  t_hS_or_bhS_or_eS
-    ~th: LowInternal.t_hoare_skip
-    ~teh: LowInternal.t_ehoare_skip
-    ~tbh:LowInternal.t_bdhoare_skip
-    ~te: LowInternal.t_equiv_skip
+(* The [skip] rules live, one module per logic, in [rules/<logic>/]. This
+   module only keeps the logic-agnostic dispatcher. *)
+let t_skip (tc : tcenv1) =
+  match (FApi.tc1_goal tc).f_node with
+  | FhoareS   _ -> EcHoareSkip.t_hoare_skip tc
+  | FeHoareS  _ -> EcEHoareSkip.t_ehoare_skip tc
+  | FbdHoareS _ -> EcBdHoareSkip.t_bdhoare_skip_full tc
+  | FequivS   _ -> EcEquivSkip.t_equiv_skip tc
+  | _ ->
+      tc_error_noXhl
+        ~kinds:[`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt]
+        !!tc

src/phl/rules/bdhoare/ecBdHoareSkip.ml

@@ -0,0 +1,62 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcFol
+open EcAst
+
+open EcCoreGoal
+open EcLowGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The bdhoare [skip] rule has no parameters. *)
+type EcCoreGoal.rule += RBdHoareSkip
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. Its side conditions (the
+   statement is empty, the comparison is [=] or [>=]) are part of it, so the
+   checker re-validates them. *)
+let bdhoare_skip_subgoals (bhs : bdHoareS) : form list =
+  if not (List.is_empty bhs.bhs_s.s_node) then
+    failwith "bdhoare-skip: the statement is not empty";
+  if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then
+    failwith "bdhoare-skip: the comparison is not = or >=";
+  let concl = map_ss_inv2 f_imp (bhs_pr bhs) (bhs_po bhs) in
+  let concl = EcSubst.f_forall_mems_ss_inv bhs.bhs_m concl in
+  if   f_equal (bhs_bd bhs).inv f_r1
+  then [concl]
+  else [f_eq (bhs_bd bhs).inv f_r1; concl]
+
+(* -------------------------------------------------------------------- *)
+(* Rule (TCB). *)
+let t_bdhoare_skip (tc : tcenv1) =
+  let bhs = tc1_as_bdhoareS tc in
+  if not (List.is_empty bhs.bhs_s.s_node) then
+    tc_error !!tc ~who:"skip" "instruction list is not empty";
+  if bhs.bhs_cmp <> FHeq && bhs.bhs_cmp <> FHge then
+    tc_error !!tc ~who:"skip" "the bound must be compared with = or >=";
+  FApi.xrule1 tc RBdHoareSkip (bdhoare_skip_subgoals bhs)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | RBdHoareSkip ->
+         Some (EcPlRecheck.checker_of "bdhoare-skip" pf_as_bdhoareS
+                 (fun _hyps bhs -> bdhoare_skip_subgoals bhs))
+     | _ -> None)
+
+(* -------------------------------------------------------------------- *)
+(* Derived (no proof-node): first turn the goal into [phoare [...] = 1%r]
+   with the bound-changing consequence, try to close its side condition,
+   then apply the rule.
+
+   TEMPORARY: the bound-changing consequence still comes from the
+   not-yet-migrated [EcPhlConseq]. *)
+let t_bdhoare_skip_full (tc : tcenv1) =
+  let t_trivial = FApi.t_seqs [t_simplify ~delta:`No; t_split; t_fail] in
+  let bhs = tc1_as_bdhoareS tc in
+  let f_r1 : ss_inv = { m = fst bhs.bhs_m; inv = f_r1 } in
+  let t_conseq = EcPhlConseq.t_bdHoareS_conseq_bd FHeq f_r1 in
+  FApi.t_internal
+    (FApi.t_seqsub t_conseq [FApi.t_try t_trivial; t_bdhoare_skip])
+    tc

src/phl/rules/bdhoare/ecBdHoareSkip.mli

@@ -0,0 +1,31 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+(* [t_bdhoare_skip] — empty statement, with [~] the goal's comparison:
+
+     (d = 1%r)      forall &m, P => Q
+     ---------------------------------  ~ is [=] or [>=]
+        phoare [skip : P ==> Q] ~ d
+
+   The premise [d = 1%r] is omitted when [d] is syntactically [1%r].
+   Side conditions: the statement is empty, and [~] is [=] or [>=]
+   (otherwise fails).
+
+   Node: [RBdHoareSkip]. Checker: "bdhoare-skip". *)
+val t_bdhoare_skip : backward
+
+(* ==================================================================== *)
+(* Derived tactics                                                      *)
+
+(* [t_bdhoare_skip_full] — on [phoare [skip : P ==> Q] ~ d]:
+   1. the bound-changing consequence (currently
+      [EcPhlConseq.t_bdHoareS_conseq_bd]) to [phoare [skip : P ==> Q] = 1%r],
+      whose side condition (relating [~ d] to [= 1%r]) is closed when
+      [simplify; split] does, and left open otherwise;
+   2. then [t_bdhoare_skip], whose bound is now syntactically [1%r].
+   Visible goals: [forall &m, P => Q], preceded by the bound side condition
+   if not closed. Emits no node of its own. *)
+val t_bdhoare_skip_full : backward

src/phl/rules/ehoare/ecEHoareSkip.ml

@@ -0,0 +1,37 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcFol
+open EcAst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The ehoare [skip] rule has no parameters. *)
+type EcCoreGoal.rule += REHoareSkip
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. Its side condition (the
+   statement is empty) is part of it, so the checker re-validates it. *)
+let ehoare_skip_subgoals (hs : eHoareS) : form list =
+  if not (List.is_empty hs.ehs_s.s_node) then
+    failwith "ehoare-skip: the statement is not empty";
+  let concl = map_ss_inv2 f_xreal_le (ehs_po hs) (ehs_pr hs) in
+  [EcSubst.f_forall_mems_ss_inv hs.ehs_m concl]
+
+(* -------------------------------------------------------------------- *)
+(* Rule (TCB). *)
+let t_ehoare_skip (tc : tcenv1) =
+  let hs = tc1_as_ehoareS tc in
+  if not (List.is_empty hs.ehs_s.s_node) then
+    tc_error !!tc "instruction list is not empty";
+  FApi.xrule1 tc REHoareSkip (ehoare_skip_subgoals hs)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | REHoareSkip ->
+         Some (EcPlRecheck.checker_of "ehoare-skip" pf_as_ehoareS
+                 (fun _hyps hs -> ehoare_skip_subgoals hs))
+     | _ -> None)

src/phl/rules/ehoare/ecEHoareSkip.mli

@@ -0,0 +1,17 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+(* [t_ehoare_skip] — empty statement:
+
+        forall &m, Q <= P
+     ------------------------
+     ehoare [skip : P ==> Q]
+
+   ([<=] on extended reals.) Side condition: the statement is empty
+   (otherwise fails).
+
+   Node: [REHoareSkip]. Checker: "ehoare-skip". *)
+val t_ehoare_skip : backward

src/phl/rules/equiv/ecEquivSkip.ml

@@ -0,0 +1,41 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcFol
+open EcAst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The equiv [skip] rule has no parameters. *)
+type EcCoreGoal.rule += REquivSkip
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. Its side condition (both
+   statements are empty) is part of it, so the checker re-validates it. *)
+let equiv_skip_subgoals (es : equivS) : form list =
+  if not (List.is_empty es.es_sl.s_node) then
+    failwith "equiv-skip: the left statement is not empty";
+  if not (List.is_empty es.es_sr.s_node) then
+    failwith "equiv-skip: the right statement is not empty";
+  let concl = map_ts_inv2 f_imp (es_pr es) (es_po es) in
+  [EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr concl]
+
+(* -------------------------------------------------------------------- *)
+(* Rule (TCB). *)
+let t_equiv_skip (tc : tcenv1) =
+  let es = tc1_as_equivS tc in
+  if not (List.is_empty es.es_sl.s_node) then
+    tc_error !!tc ~who:"skip" "left instruction list is not empty";
+  if not (List.is_empty es.es_sr.s_node) then
+    tc_error !!tc ~who:"skip" "right instruction list is not empty";
+  FApi.xrule1 tc REquivSkip (equiv_skip_subgoals es)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | REquivSkip ->
+         Some (EcPlRecheck.checker_of "equiv-skip" pf_as_equivS
+                 (fun _hyps es -> equiv_skip_subgoals es))
+     | _ -> None)

src/phl/rules/equiv/ecEquivSkip.mli

@@ -0,0 +1,16 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+(* [t_equiv_skip] — empty statements:
+
+       forall &1 &2, P => Q
+     ---------------------------
+     equiv [skip ~ skip : P ==> Q]
+
+   Side condition: both statements are empty (otherwise fails).
+
+   Node: [REquivSkip]. Checker: "equiv-skip". *)
+val t_equiv_skip : backward

src/phl/rules/hoare/ecHoareSkip.ml

@@ -0,0 +1,38 @@
+(* -------------------------------------------------------------------- *)
+open EcUtils
+open EcFol
+open EcAst
+
+open EcCoreGoal
+open EcLowPhlGoal
+
+(* -------------------------------------------------------------------- *)
+(* The hoare [skip] rule has no parameters. *)
+type EcCoreGoal.rule += RHoareSkip
+
+(* -------------------------------------------------------------------- *)
+(* Pure core shared by the rule and its checker. Its side condition (the
+   statement is empty) is part of it, so the checker re-validates it. *)
+let hoare_skip_subgoals (hs : sHoareS) : form list =
+  if not (List.is_empty hs.hs_s.s_node) then
+    failwith "hoare-skip: the statement is not empty";
+  let post  = POE.lower (hs_po hs) in
+  let concl = map_ss_inv2 f_imp (hs_pr hs) post in
+  [EcSubst.f_forall_mems_ss_inv hs.hs_m concl]
+
+(* -------------------------------------------------------------------- *)
+(* Rule (TCB). *)
+let t_hoare_skip (tc : tcenv1) =
+  let hs = tc1_as_hoareS tc in
+  if not (List.is_empty hs.hs_s.s_node) then
+    tc_error !!tc "instruction list is not empty";
+  FApi.xrule1 tc RHoareSkip (hoare_skip_subgoals hs)
+
+(* -------------------------------------------------------------------- *)
+let () =
+  register_rule_checker
+    (function
+     | RHoareSkip ->
+         Some (EcPlRecheck.checker_of "hoare-skip" pf_as_hoareS
+                 (fun _hyps hs -> hoare_skip_subgoals hs))
+     | _ -> None)

src/phl/rules/hoare/ecHoareSkip.mli

@@ -0,0 +1,17 @@
+(* -------------------------------------------------------------------- *)
+open EcCoreGoal.FApi
+
+(* ==================================================================== *)
+(* Rules (trusted)                                                      *)
+
+(* [t_hoare_skip] — empty statement:
+
+          forall &m, P => Q
+     ---------------------------
+     hoare [skip : P ==> Q | Q_e]
+
+   The exceptional postconditions [Q_e] play no role: [skip] raises nothing.
+   Side condition: the statement is empty (otherwise fails).
+
+   Node: [RHoareSkip]. Checker: "hoare-skip". *)
+val t_hoare_skip : backward