From 1622579fdd5fceb74744a61dedb04a8380a56f77 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Tue, 27 Oct 2026 11:10:48 +0100
Subject: [PATCH] perf(smt): no relevance tables when no lemma is to be
 selected

`smt(lemmas)` without `maxlemmas` sets the maximum number of selected
lemmas to zero: the task holds the given lemmas and nothing else. The
selection still built its relevance tables, scanning the statement of
every axiom of the environment to count the operators, before stopping
on the exhausted maximum; the given lemmas were themselves found by
testing every axiom of the environment against the hints.

When nothing is to be selected the tables are not built, and the given
lemmas come from the hints: a lemma by its path, a theory by a walk of
its items (`Hints.included` lists them). The walk skips the abstract
theories, whose items are not bound in the environment.

On the AVX2 ML-KEM proofs of jasmin-nist, where the environment holds
the Jasmin word and array libraries, the scan cost about 0.13 s per call;
a file with 244 such calls goes from 140 s to 108 s.
---
 src/ecProvers.ml          | 21 +++++++++++++++++++++
 src/ecProvers.mli         |  4 ++++
 src/ecSmt.ml              | 32 ++++++++++++++++++++++++++++++++
 tests/smt-given-lemmas.ec | 25 +++++++++++++++++++++++++
 4 files changed, 82 insertions(+)
 create mode 100644 tests/smt-given-lemmas.ec

diff --git a/src/ecProvers.ml b/src/ecProvers.ml
index 9e2f74e60..41dd1b7e2 100644
--- a/src/ecProvers.ml
+++ b/src/ecProvers.ml
@@ -383,6 +383,27 @@ module Hints = struct
       | None -> assert false
       | Some `Include -> true
       | Some `Exclude -> false
+
+  let included (m : hints) =
+    let rec doit prefix (m : hints) (inherited : hflag) acc =
+      let this =
+        match m.ht_this with
+        | `Inherit -> inherited
+        | #hflag as flag -> flag in
+      let sub x =
+        match prefix with
+        | None   -> EcPath.psymbol x
+        | Some p -> EcPath.pqname p x in
+      match prefix, this with
+      | None  , `Include -> `All :: acc
+      | Some p, `Include -> if inherited = `Include then acc else `Theory p :: acc
+      | _     , `Exclude ->
+          let acc =
+            Msym.fold
+              (fun x flag acc -> if flag = `Include then `Lemma (sub x) :: acc else acc)
+              m.ht_axs acc in
+          Msym.fold (fun x m acc -> doit (Some (sub x)) m this acc) m.ht_sub acc
+    in doit None m `Exclude []
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecProvers.mli b/src/ecProvers.mli
index d5a8572e9..549c86ad7 100644
--- a/src/ecProvers.mli
+++ b/src/ecProvers.mli
@@ -13,6 +13,10 @@ module Hints : sig
   val addm : path -> hflag -> hints -> hints
 
   val mem : path -> hints -> bool
+
+  (* The inclusions of the hints: the lemmas flagged so, the theories
+     flagged so that no included theory contains, or everything. *)
+  val included : hints -> [ `All | `Lemma of path | `Theory of path ] list
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecSmt.ml b/src/ecSmt.ml
index 87435dfc3..f51a52a5b 100644
--- a/src/ecSmt.ml
+++ b/src/ecSmt.ml
@@ -1679,6 +1679,38 @@ let select env pi hyps concl execute_task =
     let init_select p ax =
       ax.ax_smt && not (P.Hints.mem p pi.P.pr_unwanted) in
     (execute_task (EcEnv.Ax.all ~check:init_select env) = Some true)
+  else if pi.P.pr_max <= 0 then
+    (* No lemma is selected beyond the ones given (this is the case of
+       `smt(lemmas)` without `maxlemmas`): the relevance tables, which
+       scan every axiom of the environment, are not built, and the given
+       lemmas are resolved by their path, the given theories walked. The
+       items of abstract theories are not bound in the environment and
+       are skipped, as the scan would have. *)
+    let wanted = pi.P.pr_wanted in
+    let rec of_theory (p : EcPath.path) (cth : EcTheory.ctheory) acc =
+      if cth.EcTheory.cth_mode = `Abstract then acc else
+      List.fold_left (fun acc (item : EcTheory.theory_item) ->
+          match item.ti_item with
+          | EcTheory.Th_axiom (x, ax) ->
+              let p = EcPath.pqname p x in
+              if P.Hints.mem p wanted then (p, ax) :: acc else acc
+          | EcTheory.Th_theory (x, sub) ->
+              of_theory (EcPath.pqname p x) sub acc
+          | _ -> acc)
+        acc cth.cth_items in
+    let toadd =
+      List.fold_left (fun acc h ->
+          match h with
+          | `All ->
+              EcEnv.Ax.all ~check:(fun p _ -> P.Hints.mem p wanted) env @ acc
+          | `Lemma p ->
+              Option.fold ~none:acc ~some:(fun ax -> (p, ax) :: acc)
+                (EcEnv.Ax.by_path_opt p env)
+          | `Theory p ->
+              Option.fold ~none:acc ~some:(fun cth -> of_theory p cth acc)
+                (EcEnv.Theory.by_path_opt ~mode:`All p env))
+        [] (P.Hints.included wanted) in
+    (execute_task toadd = Some true)
   else
     let rs = Frequency.f_ops_goal unwanted_ops hyps.h_local concl in
     let ri, other = init_relevant env pi rs in
diff --git a/tests/smt-given-lemmas.ec b/tests/smt-given-lemmas.ec
new file mode 100644
index 000000000..e01592e18
--- /dev/null
+++ b/tests/smt-given-lemmas.ec
@@ -0,0 +1,25 @@
+(* `smt(lemmas)` without `maxlemmas` sends the given lemmas and nothing
+   else: a lemma by its path, a theory by all its lemmas, including those
+   of its sub-theories. *)
+require import AllCore.
+
+op f : int -> int.
+op g : int -> int.
+
+theory T.
+  axiom fP (x : int) : 0 <= f x.
+
+  theory U.
+    axiom gP (x : int) : f x <= g x.
+  end U.
+
+  abstract theory A.
+    module M = { proc m() : int = { return 0; } }.
+    axiom mP : hoare[M.m : true ==> res = 0].
+  end A.
+end T.
+
+lemma t1 (x : int) : 0 <= f x by smt(T.fP).
+lemma t2 (x : int) : 0 <= g x by smt(T.fP T.U.gP).
+lemma t3 (x : int) : 0 <= g x by smt(@T).
+lemma t4 (x : int) : f x <= g x by smt(@T.U).