From b0d6df90d69f31e1ff2bc583620972f090428f32 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 7 May 2026 19:23:59 +0200 Subject: [PATCH 1/3] Remove the `iterate` SMT option 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. --- src/ec.ml | 13 +++---------- src/ecCommands.ml | 2 -- src/ecCommands.mli | 1 - src/ecOptions.ml | 3 --- src/ecOptions.mli | 1 - src/ecParser.mly | 6 ------ src/ecParsetree.ml | 2 -- src/ecProvers.ml | 2 -- src/ecProvers.mli | 1 - src/ecScope.ml | 6 +----- src/ecScope.mli | 1 - src/ecSmt.ml | 39 ++------------------------------------- 12 files changed, 6 insertions(+), 71 deletions(-) diff --git a/src/ec.ml b/src/ec.ml index 40a8b39e0d..1a1efc5dd4 100644 --- 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 index 2b08923ea9..e90518ff08 100644 --- 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 index 56440bfa96..7dab0b84b5 100644 --- 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 index d877ccde19..bd21a69aa0 100644 --- 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 index 0feb9f6162..a5c09b11d9 100644 --- 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 index 65cd97b95f..8633c13125 100644 --- 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 index fa83d6e698..9644cfde65 100644 --- 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 index db618f2443..ccb56bbb24 100644 --- 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 index 41481c73ce..d5a8572e93 100644 --- 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 index d0125b46fc..989174512f 100644 --- 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 index f3548a3bd1..953041cc2b 100644 --- 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 index b0230936ae..2e523e770c 100644 --- 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 () From b3ff786a3a926990811fd08e4a1cb71a2d43a4ac Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Thu, 7 May 2026 15:01:12 -0400 Subject: [PATCH 2/3] fixing standarding library failures --- examples/MEE-CBC/CBC.eca | 7 ++++--- theories/datatypes/FMap.ec | 4 ++-- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/examples/MEE-CBC/CBC.eca b/examples/MEE-CBC/CBC.eca index 141b84ed52..f74bac33e1 100644 --- a/examples/MEE-CBC/CBC.eca +++ b/examples/MEE-CBC/CBC.eca @@ -502,12 +502,13 @@ 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 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 *) + by split=> [|/#]; + split; [congr; congr; smt(addbA addbK add0b) | smt()]. (* TODO: instantiate ring structure *) + split=> [sR _ |_]; 1:smt (addbA addbK 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 *) diff --git a/theories/datatypes/FMap.ec b/theories/datatypes/FMap.ec index 77709be247..5057af41f2 100644 --- 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) = From e5ce10123b295f2cd6221dd56a6678e89d2e8303 Mon Sep 17 00:00:00 2001 From: Alley Stoughton Date: Thu, 7 May 2026 15:45:43 -0400 Subject: [PATCH 3/3] trying CBC.eca with more explicit lemmas --- examples/MEE-CBC/CBC.eca | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/examples/MEE-CBC/CBC.eca b/examples/MEE-CBC/CBC.eca index f74bac33e1..919539f18a 100644 --- a/examples/MEE-CBC/CBC.eca +++ b/examples/MEE-CBC/CBC.eca @@ -502,24 +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=> [sR _|_]; 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 *) + split=> [|_]; 1:smt (addbA addbK addbC add0b). (* TODO: instantiate ring structure *) by split=> [|/#]; - split; [congr; congr; smt(addbA addbK add0b) | smt()]. (* TODO: instantiate ring structure *) - split=> [sR _ |_]; 1:smt (addbA addbK add0b). (* TODO: instantiate ring structure *) + 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.