From 773b750f33db2c4e39bfab15d5eee48a2d775323 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 28 Oct 2026 15:58:53 +0100 Subject: [PATCH] perf(smt): memories as abstract values, local variables as functions of them A memory with local variables was translated as a why3 pair of the tuple of all its locals and an abstract memory, and a local `x{m}` as a projection of the first component. why3's `eliminate_algebraic` then expands the tuple type in every task: for a Jasmin extraction with 162 locals (the `param_k`/`result_k` of the extracted procedures), a single `x{hr}` in a hypothesis adds 162 projection definitions and a 27 000-line inversion axiom, 3.4 MB of SMT-LIB per call, 2 s of printing and parsing for goals the provers close in milliseconds. A memory is now the abstract type `memory` whatever its memtype, and a local variable an uninterpreted function `x : memory -> ty`, created once per name and type (`te_lvar`), as global variables already are (`te_xpath`). The argument variable `arg` is the tuple of the functions of the declared parameters (a single parameter is `arg` itself); `glob M` and `Pr[...]` take the whole memory. `tests/smt-memory-locals.ec` covers locals, `arg` and its projections, a single parameter, `={arg}` in an equiv, and the memories of `Pr` statements. On the Keccak safety proofs of jasmin-nist, a prover call goes from 2.2 s to 0.1 s (47 KB task), the AVX2 file from 140 s to 32 s and the scenario of 49 files from 221 s to 135 s elapsed. `unit` and `stdlib` pass. The loop-body step of PIR_s_uniform in examples/PIR.ec closed by a prover call that found its instances of the restriction lemmas with some prover versions only; two step lemmas (restr_addS_eq, restr_S_eq) now rewrite the goal to a propositional one. --- examples/PIR.ec | 24 ++++++++++- src/ecMemory.ml | 10 +++++ src/ecMemory.mli | 6 +++ src/ecSmt.ml | 81 ++++++++++++++++++++++---------------- tests/smt-memory-locals.ec | 47 ++++++++++++++++++++++ 5 files changed, 131 insertions(+), 37 deletions(-) create mode 100644 tests/smt-memory-locals.ec diff --git a/examples/PIR.ec b/examples/PIR.ec index 3a3caf077c..16e93266d6 100644 --- a/examples/PIR.ec +++ b/examples/PIR.ec @@ -186,6 +186,24 @@ proof. apply fsetP => x;rewrite /restr in_fsetI in_fset0 mem_oflist mem_iota /#. qed. +lemma restr_addS_eq n s x : + 0 <= n => is_restr s n => + (fset1 n `|` s = restr x (n + 1)) = (n \in x /\ s = restr x n). +proof. + move=> Hn Hs; rewrite restrS //; case: (n \in x) => /= _. + + by rewrite (is_restr_Ueq n s (restr x n) Hs (is_restr_restr n x)). + by rewrite fset0U; apply/neqF/is_restr_diff/is_restr_restr. +qed. + +lemma restr_S_eq n s x : + 0 <= n => is_restr s n => + (s = restr x (n + 1)) = (!n \in x /\ s = restr x n). +proof. + move=> Hn Hs; rewrite restrS //; case: (n \in x) => /= _. + + by apply/neqF; rewrite eq_sym; apply/(is_restr_diff n (restr x n) s Hs). + by rewrite fset0U. +qed. + axiom N_pos : 0 <= N. import RField StdOrder.RealOrder. @@ -355,8 +373,10 @@ proof. skip => &m1 &m2 /> H0j HjN Hrs1 Hrs2 Hs Hj; split. + by move=> b _;ring. move=> _ b _;split;1: by ring. - move=> _; rewrite !oflist_cons !restrS //. - smt (is_restr_addS is_restrS is_restr_diff is_restr_Ueq is_restr_restr fset0U). + move=> _; rewrite !oflist_cons !(restr_addS_eq, restr_S_eq) //. + have := is_restr_addS _ _ H0j Hrs1; have := is_restr_addS _ _ H0j Hrs2. + have := is_restrS _ _ H0j Hrs1; have := is_restrS _ _ H0j Hrs2. + smt(). auto; move => &m1 &m2 />. rewrite !restr_0 -set0E /=;smt (is_restr_fset0). qed. diff --git a/src/ecMemory.ml b/src/ecMemory.ml index 64571772ca..b81fd4a72b 100644 --- a/src/ecMemory.ml +++ b/src/ecMemory.ml @@ -220,3 +220,13 @@ let local_type (Lmt_concrete mt) = let has_locals (Lmt_concrete mt) = Option.is_some mt + +let is_arg (x : symbol) (Lmt_concrete mt) = + match mt with + | None -> false + | Some lmt -> lmt.lmt_name = Some x + +let decls (Lmt_concrete mt) = + match mt with + | None -> [] + | Some lmt -> lmt.lmt_decl diff --git a/src/ecMemory.mli b/src/ecMemory.mli index c04c116d76..5a61c44055 100644 --- a/src/ecMemory.mli +++ b/src/ecMemory.mli @@ -69,3 +69,9 @@ val dump_memtype : memtype -> string (* -------------------------------------------------------------------- *) val local_type : memtype -> ty option val has_locals : memtype -> bool + +(* [is_arg x mt]: [x] is the argument variable of [mt] *) +val is_arg : symbol -> memtype -> bool + +(* the declared variables of [mt], in order *) +val decls : memtype -> ovariable list diff --git a/src/ecSmt.ml b/src/ecSmt.ml index f4a167b172..87435dfc30 100644 --- a/src/ecSmt.ml +++ b/src/ecSmt.ml @@ -69,6 +69,15 @@ type kpattern = | KApp of EcPath.path * kpattern list | KProj of kpattern * int +(* -------------------------------------------------------------------- *) +(* Local program variables are translated as uninterpreted functions of + the memory, one per (name, type), like global variables are. *) +module Hlv = Hashtbl.Make(struct + type t = string * WTy.ty + let equal (x1, t1) (x2, t2) = String.equal x1 x2 && WTy.ty_equal t1 t2 + let hash (x, t) = Hashtbl.hash (x, WTy.ty_hash t) +end) + (* -------------------------------------------------------------------- *) type tenv = { (*---*) te_env : EcEnv.env; @@ -82,6 +91,7 @@ type tenv = { mutable te_lam : WTerm.term Mta.t; (*---*) te_gen : WTerm.term Hf.t; (*---*) te_xpath : WTerm.lsymbol Hx.t; (* proc and global var *) + (*---*) te_lvar : WTerm.lsymbol Hlv.t; (* local var *) (*---*) te_absmod : w3absmod Hid.t; (* abstract module *) } @@ -97,6 +107,7 @@ let empty_tenv env task (kwty, kw, kwk) = te_lam = Mta.empty; te_gen = Hf.create 0; te_xpath = Hx.create 0; + te_lvar = Hlv.create 0; te_absmod = Hid.create 0; } @@ -258,9 +269,6 @@ let wproj_tuple genv arg i = let fs = Tuples.proj (n,i) in WTerm.t_app_infer fs [arg] -let wfst genv arg = wproj_tuple genv arg 0 -let wsnd genv arg = wproj_tuple genv arg 1 - (* -------------------------------------------------------------------- *) let trans_tv lenv id = oget (Mid.find_opt id lenv.le_tv) @@ -462,14 +470,6 @@ and trans_tydecl genv (p, tydecl) = List.iter (fun (p, wop) -> Hp.add genv.te_op p wop) opts; ts -(* -------------------------------------------------------------------- *) -let trans_memtype ((genv, _) as env) mt = - match EcMemory.local_type mt with - | None -> ty_mem - | Some ty -> - let ty = trans_ty env ty in - wty_tuple genv [ty; ty_mem] - (* -------------------------------------------------------------------- *) exception CanNotTranslate let trans_binding genv lenv (x, xty) = @@ -478,7 +478,7 @@ let trans_binding genv lenv (x, xty) = | GTty ty -> lenv, trans_ty (genv, lenv) ty | GTmem mt -> - { lenv with le_mt = Mid.add x mt lenv.le_mt }, trans_memtype (genv, lenv) mt + { lenv with le_mt = Mid.add x mt lenv.le_mt }, ty_mem | _ -> raise CanNotTranslate in @@ -850,19 +850,40 @@ and trans_op (genv:tenv) p = try Hp.find genv.te_op p with Not_found -> create_op ~body:true genv p (* -------------------------------------------------------------------- *) +and trans_lvar ((genv, _) as env) (x : string) (ty : ty) (m : WTerm.term) = + let wty = trans_ty env ty in + let ls = + match Hlv.find_opt genv.te_lvar (x, wty) with + | Some ls -> ls + | None -> + let ls = WTerm.create_lsymbol (WIdent.id_fresh x) [ty_mem] (Some wty) in + genv.te_task <- WTask.add_param_decl genv.te_task ls; + Hlv.add genv.te_lvar (x, wty) ls; ls + in + WTerm.t_app_infer ls [m] + and trans_pvar ((genv, lenv) as env) pv ty mem = let pv = NormMp.norm_pvar genv.te_env pv in let mt = get_memtype lenv mem in match pv with | PVloc x -> - let m = trans_mem env ~forglobal:false mem in + let m = trans_mem env mem in begin match EcMemory.lookup x mt with - | Some (_,_,Some i) -> wproj_tuple genv m i - | Some (_,_,None) -> m - | None -> assert false + | Some (v, _, _) when not (EcMemory.is_arg x mt) -> + trans_lvar env x v.v_type m + | Some _ -> + (* the whole argument: the tuple of the declared variables *) + let tr i (ov : ovariable) = + let name = odfl (Printf.sprintf "_arg%d" i) ov.ov_name in + trans_lvar env name ov.ov_type m in + begin match EcMemory.decls mt with + | [ov] -> tr 0 ov + | decls -> wt_tuple genv (List.mapi tr decls) + end + | None -> assert false end | PVglob xp -> - let m = trans_mem env ~forglobal:true mem in + let m = trans_mem env mem in let ls = match Hx.find_opt genv.te_xpath xp with | Some ls -> ls @@ -877,7 +898,7 @@ and trans_pvar ((genv, lenv) as env) pv ty mem = (* -------------------------------------------------------------------- *) and trans_glob ((genv, _) as env) m mem = - let wmem = trans_mem env ~forglobal:true mem in + let wmem = trans_mem env mem in let w3op = match Hid.find_opt genv.te_lc m with | Some w3op -> w3op @@ -895,29 +916,20 @@ and trans_glob ((genv, _) as env) m mem = in apply_wop genv w3op [] [wmem] (* -------------------------------------------------------------------- *) -and trans_mem (genv,lenv) ~forglobal mem = - let wmem = - match Hid.find_opt genv.te_lc mem with - | Some w3op -> apply_wop genv w3op [] [] - | None -> WTerm.t_var (oget (Mid.find_opt mem lenv.le_lv)) in - let mt = get_memtype lenv mem in - let has_locals = EcMemory.has_locals mt in - if forglobal then - if has_locals then wsnd genv wmem - else wmem - else - (assert has_locals; wfst genv wmem) +and trans_mem (genv,lenv) mem = + match Hid.find_opt genv.te_lc mem with + | Some w3op -> apply_wop genv w3op [] [] + | None -> WTerm.t_var (oget (Mid.find_opt mem lenv.le_lv)) (* -------------------------------------------------------------------- *) and trans_pr ((genv,lenv) as env) {pr_mem; pr_fun; pr_args; pr_event} = - let wmem = trans_mem env ~forglobal:true pr_mem in + let wmem = trans_mem env pr_mem in let warg = trans_form_b env pr_args in (* Translate the procedure *) let xp = NormMp.norm_xfun genv.te_env pr_fun in let _, mt = EcEnv.Fun.prF_memenv (EcIdent.create "&dummy") pr_fun genv.te_env in - let mty = trans_memtype env mt in - let tyr = ty_distr mty in + let tyr = ty_distr ty_mem in let ls = let trans () = let tya = oget warg.WTerm.t_ty in @@ -1197,9 +1209,8 @@ let trans_hyp ((genv, lenv) as env) (x, ty) = env | LD_mem mt -> - let wty = trans_memtype env mt in let lenv = { lenv with le_mt = Mid.add x mt lenv.le_mt } in - let wcodom = Some wty in + let wcodom = Some ty_mem in let ls = WTerm.create_lsymbol (preid x) [] wcodom in let w3op = { w3op_fo = `LDecl ls; diff --git a/tests/smt-memory-locals.ec b/tests/smt-memory-locals.ec new file mode 100644 index 0000000000..b8cac226ef --- /dev/null +++ b/tests/smt-memory-locals.ec @@ -0,0 +1,47 @@ +(* smt on goals mentioning program variables: locals, arg, globals, Pr *) +require import AllCore Distr DBool. + +module G = { var g : int }. + +module M = { + proc f (x y : int) : int = { + var z : int; + z <- x + y; + G.g <- z; + return z + 1; + } + proc one (x : int) : int = { return x + 1; } + proc r () : bool = { var b; b <$ {0,1}; return b; } +}. + +(* a local in a hoare post *) +lemma f_hoare : hoare [M.f : 0 <= x /\ 0 <= y ==> 1 <= res /\ 0 <= G.g]. +proof. by proc; wp; skip => &hr; smt(). qed. + +(* the argument variable *) +lemma f_arg : hoare [M.f : arg = (1, 2) ==> res = 4]. +proof. by proc; wp; skip => &hr; smt(). qed. + +lemma f_arg2 : hoare [M.f : arg.`1 = 1 /\ y = 2 ==> res = 4]. +proof. by proc; wp; skip => &hr; smt(). qed. + +(* a single parameter: arg is the parameter *) +lemma one_arg : hoare [M.one : arg = 1 ==> res = 2]. +proof. by proc; wp; skip => &hr; smt(). qed. + +(* equiv with ={arg} and locals of both sides *) +lemma f_equiv : equiv [M.f ~ M.f : ={arg} ==> ={res, G.g}]. +proof. by proc; wp; skip => &1 &2; smt(). qed. + +lemma f_equiv2 : equiv [M.f ~ M.f : x{1} = y{2} /\ y{1} = x{2} ==> ={res}]. +proof. by proc; wp; skip => &1 &2; smt(). qed. + +(* memories in a Pr statement *) +lemma r_pr &m : Pr[M.r() @ &m : res] = 1%r / 2%r. +proof. byphoare => //; proc; rnd; skip => &hr; smt(dbool1E). qed. + +lemma r_pr2 &m1 &m2 : Pr[M.r() @ &m1 : res] = Pr[M.r() @ &m2 : res]. +proof. by rewrite (r_pr &m1) (r_pr &m2). qed. + +lemma r_pr3 &m : G.g{m} = 3 => Pr[M.r() @ &m : res /\ G.g = 3] = 1%r / 2%r. +proof. move=> h; byphoare (_ : G.g = 3 ==> _) => //; proc; rnd; skip => &hr; smt(dbool1E). qed.