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/ecLowPhlGoal.ml

@@ -394,6 +394,14 @@ let s_split env i s =
   try  Pos.split_at_cgap1 env i s
   with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i))
 
+(* Resolve a (symbolic) code gap to its normalized integer index. This is the
+   env-dependent "code resolution" step; splitting a statement at the resulting
+   index ([EcMatching.Position.split_at_nmcgap1]) needs no environment. *)
+let s_split_index env i s =
+  let module Pos = EcMatching.Position in
+  try  Pos.normalize_cgap1 env i s
+  with Pos.InvalidCPos -> raise (InvalidSplit (`Gap i))
+
 (* -------------------------------------------------------------------- *)
 let s_split_i env i s =
   let module Pos = EcMatching.Position in

src/ecParser.mly

@@ -3036,7 +3036,7 @@ direction:
    { Pfun `Code }
 
 | SEQ s=side? pos=s_codegap1_0before COLON p=form_or_double_form f=app_bd_info
-   { Pseq (s, pos, p, f) }
+   { Pseq { seqi_side = s; seqi_at = pos; seqi_mid = p; seqi_bd = f; } }
 
 | WP n=s_codegap1_0before?
    { Pwp n }

src/ecParsetree.ml

@@ -671,8 +671,12 @@ type fun_info = [
 ]
 
 (* -------------------------------------------------------------------- *)
-type seq_info =
-  oside * pcodegap1 doption * pformula doption * p_seq_xt_info
+type seq_info = {
+  seqi_side : oside;                 (* side (prhl only) *)
+  seqi_at   : pcodegap1 doption;     (* split position(s) *)
+  seqi_mid  : pformula doption;      (* intermediate assertion / (pre, post) *)
+  seqi_bd   : p_seq_xt_info;         (* bound information (bdhoare only) *)
+}
 
 (* -------------------------------------------------------------------- *)
 type pcond_info = [

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,94 @@
+# 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 low-level subgoal-builder**
+(`<logic>_<tac>_subgoals : <judgement> -> <node> -> form list`), operating on the
+node's *resolved* parameters (e.g. an integer split index, not a symbolic code
+gap). The checker is then "rerun the builder and compare", which is why recording
+the resolved params in the node is all that recheckability costs. Resolution
+(code positions, typing, …) happens once in the rule, **before** the core, so it
+stays out of the checker's trust boundary — see REFACTORING §7c.
+
+The comparison boilerplate is shared in [`ecPhlRecheck.ml`](ecPhlRecheck.ml):
+`EcPhlRecheck.checker_of name destr build` turns a judgement reader (`pf_as_*`)
+and a builder into a `rule_checker`, and wraps any exception raised while
+rebuilding into a `RecheckFailure`. A checker is then just its registration:
+
+```ocaml
+let () = register_rule_checker (function
+  | R<Logic><Tac> node ->
+      Some (EcPhlRecheck.checker_of "<logic>-<tac>" pf_as_<logic>
+              (fun _hyps j -> <logic>_<tac>_subgoals j node))
+  | _ -> None)
+```
+
+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. The canonical rule `EcHoareSeq.t_hoare_seq`
+  takes a `hoare_seq_rule` record; the legacy `EcPhlSeq.t_hoare_seq` keeps its
+  positional `.mli` and adapts onto it, so existing callers are unchanged.