Remove the iterate SMT option

strub · alleystoughton · strub · commit b0c4c726aaad · 2026-05-07T23:20:59.000+02:00
The `iterate` option, when enabled, made `EcSmt.select` retry the SMT
call several times, growing the relevance-selected lemma set on each
attempt. Compile and llm modes hard-coded it to true at startup, which
silently overrode user-specified bounds: a `smt()` call (max=0) would
still ship dozens or hundreds of axioms after one or two retries, and
proofs that should fail were closed by lemmas the user never asked for.
Interactive mode left iteration off, so the same script behaved
differently between batch and REPL.

Drop the option entirely: the parsetree field, the parser keyword, the
CLI flag, the scope/checkmode/prover_infos plumbing, and the iteration
branch in `EcSmt.select`. SMT now always runs a single attempt with the
lemma set the user requested.

Co-Authored-By: Alley Stoughton &lt;alley.stoughton@icloud.com&gt;
diff --git a/examples/MEE-CBC/CBC.eca b/examples/MEE-CBC/CBC.eca
@@ -502,23 +502,24 @@ section Reduce.
            /\ Compute.qs{2} = (DoubleQuery.qs `|` (fset1 (s + nth witness p i))){1}).
       wp; rnd (fun x => x + pi{2}); auto=> /> &1 &2 ge0_iP _ _ lt_i_szp.
       case: (mem DoubleQuery.qs{1} _)=> //=.
-        split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *)
+        split=> [sR _|_]; 1:smt(addbA addbK addbC add0b). (* TODO: instantiate ring structure *)
         split=> [|_ r _]; 1:smt (dBlock_uffu).
         split=> [|_]; 1:smt (dBlock_uffu).
-        split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *)
-        by split=> [|/#]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *)
-      split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *)
+        split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *)
+        by split=> [|/#];
+          split; [congr; congr; smt(addbA addbK addbC add0b) | smt()]. (* TODO: instantiate ring structure *)
+      split=> [sR _ |_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *)
       split=> [|_ r _]; 1:smt (dBlock_uffu).
       split=> [|_]; 1:smt (dBlock_uffu).
-      split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *)
+      split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *)
 split.
       by move=> h; rewrite -addbA Block.subrr Block.addr0 /= /#.
       by move=> h; rewrite -addbA Block.subrr Block.addr0 /= /#.
     wp; rnd (fun x => x + pi{2}).
-    auto=> /> &2 szp_neq_0; split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *)
+    auto=> /> &2 szp_neq_0; split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *)
     split=> [|_ s _]; 1:smt (dBlock_uffu).
     split=> [|_]; 1:smt (dBlock_uffu).
-    split=> [|_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *)
+    split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *)
     smt (size_ge0).
   qed.
 
diff --git a/src/ec.ml b/src/ec.ml
@@ -269,11 +269,6 @@ let main () =
               ["-profile"]
             else [] in
 
-          let iterate =
-            if input.runo_provers.prvo_iterate then
-              ["-iterate"]
-            else [] in
-
           let why3srv =
             input.runo_provers.prvo_why3server
             |> omap (fun server -> ["-server"; server])
@@ -311,7 +306,7 @@ let main () =
           List.flatten [
             maxjobs; timeout; cpufactor; ppwidth;
             provers; quorum ; pragmas  ; checkall;
-            profile; iterate; why3srv  ; why3    ;
+            profile; why3srv  ; why3    ;
             reloc  ; noevict; boot     ; idirs   ;
           ]
         in
@@ -527,7 +522,7 @@ let main () =
             Some [State.{ position = 0; goals = None; messages = [] }]
           else None in
 
-        { prvopts     = {cmpopts.cmpo_provers with prvo_iterate = true}
+        { prvopts     = cmpopts.cmpo_provers
         ; input       = Some name
         ; terminal    = terminal
         ; interactive = false
@@ -556,7 +551,7 @@ let main () =
           lazy (T.from_channel ~name ~progress:`Silent ~lastgoals (open_in name))
         in
 
-        { prvopts     = {llmopts.llmo_provers with prvo_iterate = true}
+        { prvopts     = llmopts.llmo_provers
         ; input       = Some name
         ; terminal    = terminal
         ; interactive = false
@@ -594,7 +589,6 @@ let main () =
           prvo_ppwidth = None;
           prvo_checkall = false;
           prvo_profile = false;
-          prvo_iterate = false;
           prvo_why3server = None; }
         in
 
@@ -742,7 +736,6 @@ let main () =
               EcCommands.cm_provers   = state.prvopts.prvo_provers;
               EcCommands.cm_quorum    = state.prvopts.prvo_quorum;
               EcCommands.cm_profile   = state.prvopts.prvo_profile;
-              EcCommands.cm_iterate   = state.prvopts.prvo_iterate;
             } in
 
             let checkproof = not state.docgen in
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
@@ -846,7 +846,6 @@ type checkmode = {
   cm_provers   : string list option;
   cm_quorum    : int option;
   cm_profile   : bool;
-  cm_iterate   : bool;
 }
 
 let initial ~checkmode ~boot ~checkproof =
@@ -858,7 +857,6 @@ let initial ~checkmode ~boot ~checkproof =
     EcScope.Prover.po_nprovers  = Some checkmode.cm_nprovers;
     EcScope.Prover.po_provers   = (checkmode.cm_provers, []);
     EcScope.Prover.po_quorum    = checkmode.cm_quorum;
-    EcScope.Prover.pl_iterate   = Some (checkmode.cm_iterate);
   } in
 
   let perv    = (None, (mk_loc _dummy EcCoreLib.i_Pervasive, None), Some `Export) in
diff --git a/src/ecCommands.mli b/src/ecCommands.mli
@@ -22,7 +22,6 @@ type checkmode = {
   cm_provers  : string list option;
   cm_quorum   : int option;
   cm_profile  : bool;
-  cm_iterate  : bool;
 }
 
 val initial : checkmode:checkmode -> boot:bool -> checkproof:bool -> EcScope.scope
diff --git a/src/ecOptions.ml b/src/ecOptions.ml
@@ -65,7 +65,6 @@ and prv_options = {
   prvo_ppwidth    : int option;
   prvo_checkall   : bool;
   prvo_profile    : bool;
-  prvo_iterate    : bool;
   prvo_why3server : string option;
 }
 
@@ -410,7 +409,6 @@ let specs = {
       `Spec ("pragmas"    , `String, "Comma-separated list of pragmas");
       `Spec ("pp-width"   , `Int   , "pretty-printing width");
       `Spec ("profile"    , `Flag  , "Collect some profiling informations");
-      `Spec ("iterate"    , `Flag  , "Force to iterate smt call");
       `Spec ("server"     , `String, "Connect to an external Why3 server");
     ]);
 
@@ -535,7 +533,6 @@ let prv_options_of_values ini values =
       end;
       prvo_checkall   = get_flag "check-all" values;
       prvo_profile    = get_flag "profile" values;
-      prvo_iterate    = get_flag "iterate" values;
       prvo_why3server = get_string "why3server" values;
     }
 
diff --git a/src/ecOptions.mli b/src/ecOptions.mli
@@ -61,7 +61,6 @@ and prv_options = {
   prvo_ppwidth    : int option;
   prvo_checkall   : bool;
   prvo_profile    : bool;
-  prvo_iterate    : bool;
   prvo_why3server : string option;
 }
 
diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -152,7 +152,6 @@
 
   type smt = [
     | `ALL
-    | `ITERATE
     | `QUORUM         of int
     | `MAXLEMMAS      of int option
     | `MAXPROVERS     of int
@@ -198,7 +197,6 @@
            "verbose"       ;
            "lazy"          ;
            "full"          ;
-           "iterate"       ;
            "dumpin"        ;
            "selected"      ;
            "debug"         ]
@@ -258,7 +256,6 @@
       | "lazy"           -> `VERSION        (get_as_none s o; `Lazy)
       | "full"           -> `VERSION        (get_as_none s o; `Full)
       | "all"            -> get_as_none s o; (`ALL)
-      | "iterate"        -> get_as_none s o; (`ITERATE)
       | "selected"       -> get_as_none s o; (`SELECTED)
       | "debug"          -> get_as_none s o; (`DEBUG)
       | _                ->  assert false
@@ -274,7 +271,6 @@
       let unwanted = ref None in
       let verbose  = ref None in
       let version  = ref None in
-      let iterate  = ref None in
       let dumpin   = ref None in
       let selected = ref None in
       let debug    = ref None in
@@ -318,7 +314,6 @@
         | `UNWANTEDLEMMAS d -> unwanted := Some d
         | `VERBOSE        v -> verbose  := Some v
         | `VERSION        v -> version  := Some v
-        | `ITERATE          -> iterate  := Some true
         | `PROVER         p -> List.iter add_prover p
         | `DUMPIN         f -> dumpin   := Some f
         | `SELECTED         -> selected := Some true
@@ -340,7 +335,6 @@
         pprov_version   = !version;
         plem_all        = !all;
         plem_max        = !mlemmas;
-        plem_iterate    = !iterate;
         plem_wanted     = !wanted;
         plem_unwanted   = !unwanted;
         plem_dumpin     = !dumpin;
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -890,7 +890,6 @@ type pprover_infos = {
   pprov_version   : [`Lazy | `Full] option;
   plem_all        : bool option;
   plem_max        : int option option;
-  plem_iterate    : bool option;
   plem_wanted     : pdbhint option;
   plem_unwanted   : pdbhint option;
   plem_dumpin     : string located option;
@@ -908,7 +907,6 @@ let empty_pprover = {
   pprov_version   = None;
   plem_all        = None;
   plem_max        = None;
-  plem_iterate    = None;
   plem_wanted     = None;
   plem_unwanted   = None;
   plem_dumpin     = None;
diff --git a/src/ecProvers.ml b/src/ecProvers.ml
@@ -401,7 +401,6 @@ type prover_infos = {
   pr_verbose   : int;
   pr_all       : bool;
   pr_max       : int;
-  pr_iterate   : bool;
   pr_wanted    : hints;
   pr_unwanted  : hints;
   pr_dumpin    : string EcLocation.located option;
@@ -418,7 +417,6 @@ let dft_prover_infos = {
   pr_quorum    = 1;
   pr_verbose   = 0;
   pr_all       = false;
-  pr_iterate   = false;
   pr_max       = 50;
   pr_wanted    = Hints.empty;
   pr_unwanted  = Hints.empty;
diff --git a/src/ecProvers.mli b/src/ecProvers.mli
@@ -49,7 +49,6 @@ type prover_infos = {
   pr_verbose   : int;
   pr_all       : bool;
   pr_max       : int;
-  pr_iterate   : bool;
   pr_wanted    : hints;
   pr_unwanted  : hints;
   pr_dumpin    : string EcLocation.located option;
diff --git a/src/ecScope.ml b/src/ecScope.ml
@@ -641,7 +641,6 @@ module Prover = struct
     po_verbose    : int option;
     pl_all        : bool option;
     pl_max        : int option;
-    pl_iterate    : bool option;
     pl_wanted     : EcProvers.hints option;
     pl_unwanted   : EcProvers.hints option;
     pl_dumpin     : string located option;
@@ -659,7 +658,6 @@ module Prover = struct
     po_verbose   = None;
     pl_all       = None;
     pl_max       = None;
-    pl_iterate   = None;
     pl_wanted    = None;
     pl_unwanted  = None;
     pl_dumpin    = None;
@@ -700,7 +698,6 @@ module Prover = struct
         | None  , None   -> None
         | None  , Some _ -> Some 0
         end;
-      pl_iterate   = ppr.plem_iterate;
       pl_wanted    = omap (process_dbhint env) ppr.plem_wanted;
       pl_unwanted  = omap (process_dbhint env) ppr.plem_unwanted;
       pl_dumpin    = ppr.plem_dumpin;
@@ -720,7 +717,6 @@ module Prover = struct
     let pr_verbose   = max 0 (odfl dft.pr_verbose options.po_verbose) in
     let pr_all       = odfl dft.pr_all options.pl_all in
     let pr_max       = odfl dft.pr_max options.pl_max in
-    let pr_iterate   = odfl dft.pr_iterate options.pl_iterate in
     let pr_wanted    = odfl dft.pr_wanted options.pl_wanted in
     let pr_unwanted  = odfl dft.pr_unwanted options.pl_unwanted in
     let pr_selected  = odfl dft.pr_selected options.pl_selected in
@@ -735,7 +731,7 @@ module Prover = struct
       in List.fold_left do_ar l (snd options.po_provers) in
 
     { pr_maxprocs; pr_provers ; pr_timelimit; pr_cpufactor;
-      pr_verbose ; pr_all     ; pr_max      ; pr_iterate  ;
+      pr_verbose ; pr_all     ; pr_max      ;
       pr_wanted  ; pr_unwanted; pr_selected ; pr_quorum   ;
       pr_dumpin  ;
       gn_debug   ; }
diff --git a/src/ecScope.mli b/src/ecScope.mli
@@ -246,7 +246,6 @@ module Prover : sig
     po_verbose    : int option;
     pl_all        : bool option;
     pl_max        : int option;
-    pl_iterate    : bool option;
     pl_wanted     : EcProvers.hints option;
     pl_unwanted   : EcProvers.hints option;
     pl_dumpin     : string located option;
diff --git a/src/ecSmt.ml b/src/ecSmt.ml
@@ -1644,43 +1644,8 @@ let select env pi hyps concl execute_task =
   else
     let rs = Frequency.f_ops_goal unwanted_ops hyps.h_local concl in
     let ri, other = init_relevant env pi rs in
-    if not pi.P.pr_iterate then begin
-      ignore (relevant_clause ri other);
-      (execute_task ri.toadd = Some true)
-    end else
-      let other, res =
-        if List.is_empty ri.toadd then
-          let other = relevant_clause ri other in
-          other, execute_task ri.toadd
-        else other, execute_task ri.toadd in
-
-      match res with Some res -> res | None ->
-        let rec aux ml other i =
-          if i <= 0 then begin
-            ri.ri_max <- max_int;
-            ri.ri_p   <- 0.;
-            ri.toadd  <- [];
-            let other = relevant_clause ri other in
-            if List.is_empty ri.toadd then
-              (execute_task (List.fst other) = Some true)
-            else
-              match execute_task ri.toadd with
-              | None -> (execute_task (List.fst other) = Some true)
-              | Some res -> res
-          end else begin
-            ri.ri_max <- ml;
-            ri.toadd  <- [];
-            let other = relevant_clause ri other in
-            let ml = min (2*ml+30) max_int in
-            if   List.is_empty ri.toadd
-            then aux ml other (i-1)
-            else
-              match execute_task ri.toadd with
-              | None -> aux ml other (i-1)
-              | Some res -> res
-          end
-
-        in aux pi.P.pr_max other 4
+    ignore (relevant_clause ri other);
+    (execute_task ri.toadd = Some true)
 
 (* -------------------------------------------------------------------- *)
 let cnt = Counter.create ()
diff --git a/theories/datatypes/FMap.ec b/theories/datatypes/FMap.ec
@@ -440,7 +440,7 @@ proof. by rewrite /filter /"_.[_]" filter_valE SmtMap.offunE. qed.
 
 lemma mem_filter (m : ('a,'b) fmap) (p : 'a -> 'b -> bool) x : 
    x \in filter p m <=> x \in m /\ p x (oget m.[x]).
-proof. smt(filterE). qed.
+proof. by smt(filterE fmapP). qed.
 
 lemma get_filter (m : ('a,'b) fmap) (p : 'a -> 'b -> bool) x : 
   x \in filter p m => (filter p m).[x] = m.[x].
@@ -690,7 +690,7 @@ proof. by case _ : (find P m) => // [x /find_some] /#. qed.
 
 lemma find_eq_none (p : 'a -> 'b -> bool) (m : ('a,'b) fmap): 
   (forall x, x \in m => !p x (oget m.[x])) => find p m = None.
-proof. by move=> np; apply contraT => /find_not_none /#. qed.
+proof. by move=> np; apply contraT=> /find_not_none; smt(find_some). qed.
 
 (* -------------------------------------------------------------------- *)
 inductive find_spec (P : 'a -> 'b -> bool) (m : ('a, 'b) fmap) =

Original file line number	Diff line number	Diff line change
`@@ -22,7 +22,6 @@ type checkmode = {`
`22`	`22`	`cm_provers : string list option;`
`23`	`23`	`cm_quorum : int option;`
`24`	`24`	`cm_profile : bool;`
`25`		`- cm_iterate : bool;`
`26`	`25`	`}`
`27`	`26`
`28`	`27`	`val initial : checkmode:checkmode -> boot:bool -> checkproof:bool -> EcScope.scope`
Original file line number	Diff line number	Diff line change
`@@ -61,7 +61,6 @@ and prv_options = {`
`61`	`61`	`prvo_ppwidth : int option;`
`62`	`62`	`prvo_checkall : bool;`
`63`	`63`	`prvo_profile : bool;`
`64`		`- prvo_iterate : bool;`
`65`	`64`	`prvo_why3server : string option;`
`66`	`65`	`}`
`67`	`66`