phl: reorganize the program logic into a recheckable four-layer structure

src/ecCoreGoal.ml

@@ -125,6 +125,14 @@ type rwproofterm = {
   rpt_lc    : ident option;
 }
 
+(* -------------------------------------------------------------------- *)
+(* An open (extensible) type of recheckable proof-rule nodes. Each tactic
+   that produces a trusted (TCB) judgement extends [rule] with a constructor
+   carrying exactly the parameters needed to recompute its subgoals, and
+   registers a checker (see [register_rule_checker]). The kernel never needs
+   to know the payload types: dispatch is by a registry of partial handlers. *)
+type rule = ..
+
 (* -------------------------------------------------------------------- *)
 type proof = {
   pr_env    : proofenv;
@@ -161,6 +169,10 @@ and validation =
   (* external (hl/phl/prhl/...) proof-node *)
 | VExtern  : 'a * handle list -> validation
 
+  (* recheckable external proof-node: the [rule] carries enough information
+     to recompute (and thus re-validate) the listed subgoals. *)
+| VRule    of rule * handle list
+
 and tcenv1 = {
   tce_penv : proofenv;               (* top-level proof environment *)
   tce_ctxt : tcenv_ctxt;             (* context *)
@@ -528,6 +540,30 @@ module FApi = struct
   let xmutate1_hyps (tc : tcenv1) (vx : 'a) subgoals =
     xmutate_hyps (tcenv_of_tcenv1 tc) vx subgoals
 
+  (* ------------------------------------------------------------------ *)
+  (* Same as [xmutate], but emit a recheckable [VRule] node. [r] must carry
+     the parameters its registered checker needs to recompute [fp]. *)
+  let xrule (tc : tcenv) (r : rule) (fp : form list) =
+    let (tc, hds) = List.map_fold (fun tc fp -> newgoal tc fp) tc fp in
+    close tc (VRule (r, hds))
+
+  (* ------------------------------------------------------------------ *)
+  let xrule1 (tc : tcenv1) (r : rule) (fp : form list) =
+    xrule (tcenv_of_tcenv1 tc) r fp
+
+  (* ------------------------------------------------------------------ *)
+  let xrule_hyps (tc : tcenv) (r : rule) subgoals =
+    let (tc, hds) =
+      List.map_fold
+        (fun tc (hyps, fp) -> newgoal tc ~hyps fp)
+        tc subgoals
+    in
+      close tc (VRule (r, hds))
+
+  (* ------------------------------------------------------------------ *)
+  let xrule1_hyps (tc : tcenv1) (r : rule) subgoals =
+    xrule_hyps (tcenv_of_tcenv1 tc) r subgoals
+
   (* ------------------------------------------------------------------ *)
   let newfact (pe : proofenv) vx hyps concl =
     snd_map (fun x -> x.g_uid) (pf_newgoal pe ~vx:vx hyps concl)
@@ -984,6 +1020,46 @@ let proof_of_tcenv (tc : tcenv) =
 let proofenv_of_proof (pf : proof) =
   pf.pr_env
 
+(* -------------------------------------------------------------------- *)
+(* Rechecking of [VRule] proof-nodes.
+
+   A checker is given the proof environment, the node's (closed) goal and the
+   pregoals of the subgoals the rule produced. It must re-derive what subgoals
+   the rule should yield for that goal and confirm they match what was
+   recorded, raising [RecheckFailure] otherwise. Checkers are registered as
+   partial handlers over the open [rule] type. *)
+exception RecheckFailure of string
+
+type rule_checker = proofenv -> pregoal -> pregoal list -> unit
+
+let rule_checkers : (rule -> rule_checker option) list ref = ref []
+
+let register_rule_checker (f : rule -> rule_checker option) =
+  rule_checkers := f :: !rule_checkers
+
+let find_rule_checker (r : rule) : rule_checker option =
+  let rec aux = function
+    | []      -> None
+    | f :: fs -> (match f r with Some _ as x -> x | None -> aux fs)
+  in aux !rule_checkers
+
+(* Recheck every [VRule] node of [pe]. Nodes whose rule has no registered
+   checker are left untouched (not yet migrated); all other validation kinds
+   are trusted by construction. *)
+let recheck_proofenv (pe : proofenv) =
+  ID.Map.iter (fun _ (g : goal) ->
+    match g.g_validation with
+    | Some (VRule (r, hds)) -> begin
+        match find_rule_checker r with
+        | None     -> ()
+        | Some chk ->
+            let subs =
+              List.map
+                (fun hd -> (FApi.get_goal_by_id hd pe).g_goal) hds in
+            chk pe g.g_goal subs
+      end
+    | _ -> ()) pe.pr_goals
+
 (* -------------------------------------------------------------------- *)
 let start (hyps : LDecl.hyps) (goal : form) =
   let uid = ID.gen () in

src/ecCoreGoal.mli

@@ -146,6 +146,11 @@ type pregoal = {
   g_concl : form;
 }
 
+(* An open (extensible) type of recheckable proof-rule nodes. Each TCB tactic
+   extends [rule] with a constructor carrying the parameters needed to
+   recompute its subgoals, and registers a checker (see below). *)
+type rule = ..
+
 type validation =
 | VSmt                               (* SMT call *)
 | VAdmit                             (* admit *)
@@ -159,6 +164,9 @@ type validation =
   (* external (hl/phl/prhl/...) proof-node *)
 | VExtern  : 'a * handle list -> validation
 
+  (* recheckable external proof-node *)
+| VRule    of rule * handle list
+
 (* -------------------------------------------------------------------- *)
 type location = {
   plc_parent : location option;
@@ -186,6 +194,22 @@ val tcenv_of_proof    : proof  -> tcenv
 val proof_of_tcenv    : tcenv  -> proof
 val proofenv_of_proof : proof  -> proofenv
 
+(* -------------------------------------------------------------------- *)
+(* Rechecking of [VRule] proof-nodes. A [rule_checker] receives the proof
+ * environment, the node's (closed) goal and the pregoals of the subgoals the
+ * rule produced; it must re-derive the expected subgoals and confirm they
+ * match, raising [RecheckFailure] otherwise. Checkers are registered as
+ * partial handlers over the open [rule] type. *)
+exception RecheckFailure of string
+
+type rule_checker = proofenv -> pregoal -> pregoal list -> unit
+
+val register_rule_checker : (rule -> rule_checker option) -> unit
+
+(* Recheck every [VRule] node reachable in this proof environment. Unregistered
+ * rules and non-[VRule] validations are skipped. *)
+val recheck_proofenv : proofenv -> unit
+
 (* Start a new interactive proof in a given local context
  * [LDecl.hyps] for given [form]. Mainly, a [proof] records the set
  * of all goals (closed or not - i.e. a proof-environment) + the list
@@ -289,6 +313,15 @@ module FApi : sig
   val xmutate_hyps  : tcenv  -> 'a -> (LDecl.hyps * form) list -> tcenv
   val xmutate1_hyps : tcenv1 -> 'a -> (LDecl.hyps * form) list -> tcenv
 
+  (* Same as [xmutate], but emit a recheckable [VRule] node. The [rule] must
+   * carry the parameters its registered checker needs to recompute the
+   * subgoals. *)
+  val xrule  : tcenv  -> rule -> form list -> tcenv
+  val xrule1 : tcenv1 -> rule -> form list -> tcenv
+
+  val xrule_hyps  : tcenv  -> rule -> (LDecl.hyps * form) list -> tcenv
+  val xrule1_hyps : tcenv1 -> rule -> (LDecl.hyps * form) list -> tcenv
+
   (* Apply a forward tactic to a backward environment, using the
    * proof-environment of the latter *)
   val bwd1_of_fwd  : forward -> tcenv1 -> tcenv1 * handle

src/ecScope.ml

@@ -1076,7 +1076,9 @@ module Ax = struct
           | PSCheck _ when mode <> `Save -> ()
           | PSCheck pf -> begin
               if not (EcCoreGoal.closed pf) then
-                hierror "cannot save an incomplete proof"
+                hierror "cannot save an incomplete proof";
+              if EcUtils.is_some (Sys.getenv_opt "EC_RECHECK") then
+                EcCoreGoal.recheck_proofenv (EcCoreGoal.proofenv_of_proof pf)
           end
       end; (pac, pct)
     in

src/phl/README.md

@@ -0,0 +1,77 @@
+# Program-logic tactics (`src/phl`)
+
+This directory is being reorganized around a uniform, recheckable structure.
+This note records the target layout and the per-tactic spine. It is being
+applied **one tactic at a time**; until a tactic is migrated it keeps its old
+shape (one `ecPhl<Tactic>.ml` holding every logic).
+
+## The four-layer spine
+
+Every tactic is decomposed into the same layers, so that typing, dispatch and
+the trusted core are separated and each TCB step is re-checkable:
+
+```
+DISPATCH      process_<tactic>        logic-agnostic. Inspects the goal kind and
+   │                                  routes. The ONLY place is_hoareS / f_node
+   │                                  matching belongs. No typing here.
+   ▼
+ELABORATION   process_<logic>_<tac>   the goal kind is known. Type the parse-tree
+   │                                  arguments in that logic's memory and build
+   │                                  the typed rule parameters, then call the rule.
+   ▼
+RULE (TCB)    t_<logic>_<tac>         compute the subgoals from the typed params
+   │                                  and emit a recheckable node carrying THOSE
+   │                                  params: FApi.xrule1 tc (R... params) subgoals.
+   ▼
+CHECKER       check_<logic>_<tac>     read the params back from the node, recompute
+                                      the subgoals via the SAME pure core, and
+                                      confirm they match (is_conv) what was stored.
+```
+
+Key rule: the rule and its checker share one **pure subgoal-builder**
+(`<logic>_<tac>_subgoals : env -> <judgement> -> params -> form list`). The
+checker is then "rerun the builder and compare", which is why recording the
+params in the node is all that recheckability costs.
+
+Derived (non-TCB) tactics that only orchestrate other tactics emit **no** node
+and need **no** checker — rechecking recurses into the rules they expand to.
+
+## Recheckable proof-nodes
+
+The kernel ([`ecCoreGoal`](../ecCoreGoal.mli)) provides:
+
+- `type rule = ..` — an open type. Each migrated tactic adds one constructor,
+  e.g. `type EcCoreGoal.rule += RHoareSeq of codegap1 * ss_inv`.
+- `FApi.xrule1 tc r subgoals` — like `xmutate1` but emits a recheckable
+  `VRule (r, _)` node instead of an opaque `VExtern`.
+- `register_rule_checker : (rule -> rule_checker option) -> unit` — register a
+  partial handler that, for your constructor, returns its checker.
+- `recheck_proofenv` — walks a finished proof and runs every registered checker.
+  It is invoked at `qed` time when the `EC_RECHECK` environment variable is set
+  (see `ecScope.save_r`); unmigrated `VExtern` nodes are skipped.
+
+Run the test suite with `EC_RECHECK=1` to exercise every migrated checker.
+
+## Directory layout
+
+`(include_subdirs unqualified)` in `src/dune` slurps everything under `src/`
+into one flat-namespace library, so subdirectories are purely organizational —
+**module names must stay globally unique** (keep the `Ec<Logic><Tactic>` prefix;
+directories are for humans).
+
+```
+src/phl/
+  rules/        genuine logic rules (different subgoals per logic)
+    hoare/  ehoare/  bdhoare/  equiv/  eager/
+  codetx/       logic-uniform program transforms (wp, sp, inline, swap, rcond, …)
+  bridge/       probabilistic / cross-logic bridges (deno, pr, byequiv, fel, upto)
+  multi/        multi-logic tactics with shared machinery (conseq, trans, sym)
+  ecPhl<Tactic>.ml   legacy, thin dispatchers, not-yet-migrated tactics
+```
+
+## Migrated so far
+
+- **hoare `seq`** — [`rules/hoare/ecHoareSeq.ml`](rules/hoare/ecHoareSeq.ml).
+  The reference example of the full spine + checker. `EcPhlSeq.process_seq`
+  dispatches its `hoareS` arm here; `EcPhlSeq.t_hoare_seq` re-exports the rule
+  so existing callers and the public interface are unchanged.