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.

Author: strub

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.

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

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

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;

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.