diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index cbbb6e49672d64d652e611af1d86df18ea840e53..b9b62f2b01c2d64874ebe1fc7c2d5ab730284e07 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -474,15 +474,26 @@ sig
   *)
 
   val set_builtin_get :
-    ?force: bool -> Fun.t -> (term list -> tau option -> term -> term) -> unit
+    ?force: bool -> Fun.t -> (term list -> term list -> term) -> unit
   (** [set_builtin_get f rewrite] register a builtin
-      for rewriting [(f a1..an)[k]] into [rewrite (a1..an) k].
-      The type given is the type of (f a1..an).
+      for rewriting [(f a1..an)[k1]..[km]] into [rewrite (a1..an) (k1..km)].
 
       The [force] parameters defaults to [false], when it is [true], if there
       exist another builtin, it is replaced with the new one. Use with care.
 
       @before 22.0-Titanium the optional [force] parameter does not exist
+      @before Frama-C+dev one-dimensional access only
+  *)
+
+  val set_builtin_field :
+    ?force: bool -> Fun.t -> Field.t -> (term list -> term) -> unit
+  (** Register a builtin for simplifying [(f e…).fd] expressions.
+        {b Must} only use recursive comparison for strictly smaller terms.
+
+        The [force] parameters defaults to [false], when it is [true], if there
+        exist another builtin, it is replaced with the new one. Use with care.
+
+        @since Frama-C+dev
   *)
 
   val set_builtin_eq :
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 7d5ec8dacfa9d6e3747f657f62978c865f1070d8..be5a1a97ea5a010eb5cdf358354a0cb7597db42a 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -690,6 +690,7 @@ struct
   (* -------------------------------------------------------------------------- *)
 
   module BUILTIN = Map.Make(Fun)
+  module FIELD = Map.Make(Field)
 
   (* -------------------------------------------------------------------------- *)
   (* --- Cache                                                              --- *)
@@ -732,9 +733,10 @@ struct
     weak : W.t ;
     cache : term C.cache ;
     mutable builtins_fun : (term list -> tau option -> term) BUILTIN.t ;
-    mutable builtins_get : (term list -> tau option -> term -> term) BUILTIN.t ;
+    mutable builtins_get : (term list -> term list -> term) BUILTIN.t ;
     mutable builtins_eq  : (term -> term -> term) BUILTIN.t ;
     mutable builtins_leq : (term -> term -> term) BUILTIN.t ;
+    mutable builtins_fld : (term list -> term) FIELD.t BUILTIN.t ;
   }
 
   let empty () = {
@@ -745,6 +747,7 @@ struct
     builtins_get = BUILTIN.empty ;
     builtins_eq  = BUILTIN.empty ;
     builtins_leq = BUILTIN.empty ;
+    builtins_fld = BUILTIN.empty ;
   }
 
   let state = ref (empty ())
@@ -778,6 +781,7 @@ struct
     st.builtins_get <- BUILTIN.empty ;
     st.builtins_eq  <- BUILTIN.empty ;
     st.builtins_leq <- BUILTIN.empty ;
+    st.builtins_fld <- BUILTIN.empty ;
     let add s c = W.add s.weak c ; s.kid <- max s.kid (succ c.id) in
     Tset.iter (add st) !constants
 
@@ -1028,6 +1032,22 @@ struct
   let set_builtin_map ?force f phi =
     set_builtin' ?force f (fun es tau -> c_fun f (phi es) tau)
 
+  let set_builtin_field ?(force=false) f fd p =
+    begin
+      let fmap =
+        try BUILTIN.find f !state.builtins_fld
+        with Not_found -> FIELD.empty in
+      begin
+        if not force && FIELD.mem fd fmap then
+          let msg = Printf.sprintf
+              "Builtin already registered for '(%s …).%s'"
+              (Fun.debug f) (Field.debug fd) in
+          raise (Failure msg)
+      end ;
+      let fmap = FIELD.add fd p fmap in
+      !state.builtins_fld <- BUILTIN.add f fmap !state.builtins_fld
+    end
+
   (* -------------------------------------------------------------------------- *)
   (* --- Negation                                                           --- *)
   (* -------------------------------------------------------------------------- *)
@@ -2027,9 +2047,15 @@ struct
         | No -> e_get m0 k
         | Maybe -> c_get m k
       end
-    | Fun (g,xs) ->
+    | (Fun _ | Aget _) ->
       begin
-        try (BUILTIN.find g !state.builtins_get) xs m.tau k
+        try
+          let rec getmatrix m0 ks =
+            match m0.repr with
+            | Aget(m0,k) -> getmatrix m0 (k::ks)
+            | Fun(f,es) -> (BUILTIN.find f !state.builtins_get) es (List.rev ks)
+            | _ -> raise Not_found
+          in getmatrix m [k]
         with Not_found -> c_get m k
       end
     | _ -> c_get m k
@@ -2063,6 +2089,11 @@ struct
   let e_getfield m f =
     match m.repr with
     | Rdef gys -> get_field m f gys
+    | Fun(lf,es) ->
+      begin
+        try FIELD.find f (BUILTIN.find lf !state.builtins_fld) es
+        with Not_found -> c_getfield m f
+      end
     | _ -> c_getfield m f
 
   let e_record fxs = c_record fxs
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 898e9209ba48c126c8e7cb0b384abc7066a3a183..ffaa58035207fd130a77ecd550412877bcc76402 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -738,7 +738,7 @@ struct
   let set_builtin_eq f = QZERO.set_builtin_eq f
   let set_builtin_leq f = QZERO.set_builtin_leq f
   let set_builtin_get f = QZERO.set_builtin_get f
-
+  let set_builtin_field f = QZERO.set_builtin_field f
 
   (* -------------------------------------------------------------------------- *)
   (* --- Term Extensions                                                    --- *)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 273b3dd5fde4e2060c0740435bc10874ffc4bff8..abad0dc5df2372e8431329c04e11ad9b3fd85da7 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -387,6 +387,9 @@ sig
 
   val p_call : lfun -> term list -> pred
 
+  val e_lambda : var list -> term -> term
+  val e_apply : term -> term list -> term
+
   val p_forall : var list -> pred -> pred
   val p_exists : var list -> pred -> pred
   val p_bind : binder -> var -> pred -> pred
@@ -553,7 +556,8 @@ sig
       smaller terms. *)
 
   val set_builtin : lfun -> (term list -> term) -> unit
-  val set_builtin_get : lfun -> (term list -> tau option -> term-> term) -> unit
+  val set_builtin_get : lfun -> (term list -> term list -> term) -> unit
+  val set_builtin_field : lfun -> field -> (term list -> term) -> unit
   val set_builtin_1 : lfun -> unop -> unit
   val set_builtin_2 : lfun -> binop -> unit
   val set_builtin_2' : lfun -> (term -> term -> tau option -> term) -> unit
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 74ab9a5ba647851441dc579580eedcfcb6e1ae7a..4180062f721e165382ea790ccf1648c437855cae 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -267,25 +267,28 @@ struct
           let domain = Info.footprint obj loc in
           let result = Info.t_comp c in
           let lfun =
-            Lang.generated_f ~result "Load%a_%s" pp_rid r (Info.comp_id c)
-          in
-          (* Since its a generated it is the unique name given *)
+            Lang.generated_f ~context:true ~result "Load%a_%s"
+              pp_rid r (Info.comp_id c) in
           let xms,chunks,sigma = signature domain in
+          let prms = x :: xms in
           let dfun =
             match c.cfields with
             | None -> Definitions.Logic result
             | Some fields ->
               let def = List.map
                   (fun f ->
-                     cfield ~kind:Info.kind f,
-                     Info.load sigma (object_of f.ftype) (M.field loc f)
+                     let fd = cfield ~kind:Info.kind f in
+                     let ft = object_of f.ftype in
+                     let fv = Info.load sigma ft (M.field loc f) in
+                     let pr = F.e_apply (F.e_lambda prms fv) in
+                     F.set_builtin_field lfun fd pr ;
+                     fd,fv
                   ) fields
-              in
-              Definitions.Function( result , Def , e_record def )
+              in Definitions.Function( result , Def , e_record def )
           in
           Definitions.define_symbol {
             d_lfun = lfun ; d_types = 0 ;
-            d_params = x :: xms ;
+            d_params = prms ;
             d_definition = dfun ;
             d_cluster = cluster () ;
           } ;
@@ -317,21 +320,23 @@ struct
           let domain = Info.footprint obj loc in
           let result = Matrix.cc_tau (Info.t_array a) ds in
           let lfun =
-            Lang.generated_f ~result "Array%a_%s%a"
+            Lang.generated_f ~result ~context:true "Array%a_%s%a"
               pp_rid r (Info.array_id a) Matrix.pp_suffix_id ds in
           let prefix = Lang.Fun.debug lfun in
           let name = prefix ^ "_access" in
-          let xmem,chunks,sigma = signature domain in
+          let xms,chunks,sigma = signature domain in
           let env = Matrix.cc_env ds in
-          let phi = e_fun lfun (v :: env.size_val @ List.map e_var xmem) in
+          let prms = x :: env.size_var @ xms in
+          let phi = e_fun lfun (v :: env.size_val @ List.map e_var xms) in
           let va = List.fold_left e_get phi env.index_val in
           let ofs = e_sum env.index_offset in
           let vm = Info.load sigma obj (M.shift loc obj ofs) in
           let lemma = p_hyps env.index_range (p_equal va vm) in
           let cluster = cluster () in
           Definitions.define_symbol {
-            d_lfun = lfun ; d_types = 0 ;
-            d_params = x :: env.size_var @ xmem ;
+            d_lfun = lfun ;
+            d_types = 0 ;
+            d_params = prms ;
             d_definition = Logic result ;
             d_cluster = cluster ;
           } ;
@@ -343,6 +348,15 @@ struct
             l_lemma = lemma ;
             l_cluster = cluster ;
           } ;
+          let pr = F.e_lambda (prms @ env.index_var) vm in
+          let nk = List.length env.index_var in
+          Lang.F.set_builtin_get lfun
+            (fun es ks ->
+               if List.length ks = nk then
+                 F.e_apply pr (es @ ks)
+               else
+                 raise Not_found
+            ) ;
           if env.length <> None then
             begin
               let ns = List.map F.e_var env.size_var in
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 5db102a4dcf67d0e16f65c803bf4bfe2dc6084ee..062e3f01e3ebd9ee90fcdb40141fbc3975d2f92d 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -302,13 +302,15 @@ let r_havoc = function
    - m[k]     WHEN separated (p,a,k,1)
    - undef[k] WHEN NOT separated (p,a,k,1)
 *)
-let r_get_havoc = function
-  | [undef;m;p;a] ->
-    (fun _ k ->
-       match is_separated [p;a;k;e_one] with
-       | L.Yes -> F.e_get m k
-       | L.No  -> F.e_get undef k
-       | _ -> raise Not_found)
+let r_get_havoc es ks =
+  match es, ks with
+  | [undef;m;p;a],[k] ->
+    begin
+      match is_separated [p;a;k;e_one] with
+      | L.Yes -> F.e_get m k
+      | L.No  -> F.e_get undef k
+      | _ -> raise Not_found
+    end
   | _ -> raise Not_found
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Plang.ml b/src/plugins/wp/Plang.ml
index 4dfc1985af0820bb1d534af628f788c90905a76a..99c4fa10fcedba46c6ee34df24028142dbc20503 100644
--- a/src/plugins/wp/Plang.ml
+++ b/src/plugins/wp/Plang.ml
@@ -239,11 +239,18 @@ class engine =
 
     (* --- Higher Order --- *)
 
-    method pp_apply (_:cmode) (_:term) (_:formatter) (_:term list) =
-      failwith "Qed: higher-order application"
-
-    method pp_lambda (_:formatter) (_: (string * tau) list) =
-      failwith "Qed: lambda abstraction"
+    method pp_apply (_:cmode) e fmt es =
+      fprintf fmt "@[<hov 2>%a" self#pp_atom e ;
+      List.iter (fprintf fmt "@ @@@@ %a" self#pp_atom) es ;
+      fprintf fmt "@]"
+
+    method pp_lambda fmt vs =
+      fprintf fmt "@[<hov 2>fun" ;
+      List.iter
+        (fun (x,t) ->
+           fprintf fmt "@ @[<hov 2>(%a: %a)@]" self#pp_var x self#pp_tau t
+        ) vs ;
+      fprintf fmt "@ ->@]"
 
     (* --- Binders --- *)
 
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index fcdee85cb048bfe531d6875a5b641a0dbea4301d..23e2ff3c367ee55ecf745bf88705e27c063f1505 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -209,7 +209,9 @@ let pp_stats ~shell ~cache fmt s =
        let success = truncate pr.success in
        let print_proofs = success > 0 && total > 1 in
        let print_perfo =
-         pr.time > Rformat.epsilon && (not shell || s.cachemiss > 0) in
+         pr.time > Rformat.epsilon &&
+         (not shell || (not updating && s.cachemiss > 0))
+       in
        if p != Qed || qed_only || print_perfo || print_proofs
        then
          begin
diff --git a/src/plugins/wp/tests/wp_typed/loader.i b/src/plugins/wp/tests/wp_typed/loader.i
new file mode 100644
index 0000000000000000000000000000000000000000..3562e533b74398a09f057689aaf0d9cec9b928e8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/loader.i
@@ -0,0 +1,21 @@
+/* run.config_qualif
+   DONTRUN:
+*/
+
+//@ predicate Obs(integer x);
+
+struct S {
+  int f;
+  int g[4];
+  int m[3][5];
+};
+
+/*@
+  ensures F: Obs( \result.f );
+  ensures G: Obs( \result.g[k] );
+  ensures H: Obs( \result.m[i][j] );
+ */
+struct S load(struct S *x, int k, int i, int j)
+{
+  return *x;
+}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/loader.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/loader.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c8a8532a9214907dedb9214c0e1902678ef6ae64
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/loader.0.res.oracle
@@ -0,0 +1,31 @@
+# frama-c -wp [...]
+[kernel] Parsing loader.i (no preprocessing)
+[kernel] loader.i:5: Warning: 
+  parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function load
+------------------------------------------------------------
+
+Goal Post-condition 'F' in 'load':
+Assume { (* Heap *) Type: region(x.base) <= 0. }
+Prove: P_Obs(Mint_0[shiftfield_F1_S_f(x)]).
+
+------------------------------------------------------------
+
+Goal Post-condition 'G' in 'load':
+Assume { Type: is_sint32(k). (* Heap *) Type: region(x.base) <= 0. }
+Prove: P_Obs(Mint_0[shift_sint32(shiftfield_F1_S_g(x), k)]).
+
+------------------------------------------------------------
+
+Goal Post-condition 'H' in 'load':
+Assume {
+  Type: is_sint32(i) /\ is_sint32(j).
+  (* Heap *)
+  Type: region(x.base) <= 0.
+}
+Prove: P_Obs(Mint_0[shift_sint32(shiftfield_F1_S_m(x), i + (5 * j))]).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/loader.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/loader.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..cf28cba243acb3ec9eefcf0a180b3b30d11f2efe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/loader.1.res.oracle
@@ -0,0 +1,32 @@
+# frama-c -wp -wp-model 'Typed (Ref)' [...]
+[kernel] Parsing loader.i (no preprocessing)
+[kernel] loader.i:5: Warning: 
+  parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function load
+------------------------------------------------------------
+
+Goal Post-condition 'F' in 'load':
+Assume { Type: IsS1_S(load_0). }
+Prove: P_Obs(load_0.F1_S_f).
+
+------------------------------------------------------------
+
+Goal Post-condition 'G' in 'load':
+Assume { Type: IsS1_S(load_0) /\ is_sint32(k). }
+Prove: P_Obs((load_0.F1_S_g)[k]).
+
+------------------------------------------------------------
+
+Goal Post-condition 'H' in 'load':
+Assume { Type: IsS1_S(load_0) /\ is_sint32(i) /\ is_sint32(j). }
+Prove: P_Obs((load_0.F1_S_m)[i][j]).
+
+------------------------------------------------------------
+[wp] loader.i:18: Warning: 
+  Memory model hypotheses for function 'load':
+  /*@ behavior wp_typed_ref:
+        requires \valid(x); */
+  struct S load(struct S *x, int k, int i, int j);
diff --git a/src/plugins/wp/tests/wp_typed/oracle/tuple.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/tuple.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d00a2db178643ef87445e7e159ad092844647956
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/tuple.0.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp [...]
+[kernel] Parsing tuple.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function negate
+------------------------------------------------------------
+
+Goal Post-condition 'P' in 'negate':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'Q' in 'negate':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/tuple.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/tuple.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fdca707fee26ec80739647f00dd1964b1b37251c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle/tuple.1.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp -wp-model 'Typed (Ref)' [...]
+[kernel] Parsing tuple.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function negate
+------------------------------------------------------------
+
+Goal Post-condition 'P' in 'negate':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'Q' in 'negate':
+Prove: true.
+
+------------------------------------------------------------
+[wp] tuple.i:7: Warning: 
+  Memory model hypotheses for function 'negate':
+  /*@ behavior wp_typed_ref:
+        requires \valid(x); */
+  struct S negate(struct S *x);
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/tuple.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/tuple.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..47efc7103a64255a618b492c5507516e9b1ace6c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/tuple.res.oracle
@@ -0,0 +1,13 @@
+# frama-c -wp [...]
+[kernel] Parsing tuple.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 2 goals scheduled
+[wp] [Valid] typed_negate_ensures_P (Qed)
+[wp] [Valid] typed_negate_ensures_Q (Qed)
+[wp] Proved goals:    2 / 2
+  Qed:             2
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  negate                    2        -        2       100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/tuple.i b/src/plugins/wp/tests/wp_typed/tuple.i
new file mode 100644
index 0000000000000000000000000000000000000000..df10a47517ccf4469c83a3c1a4b50744f359afbe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/tuple.i
@@ -0,0 +1,12 @@
+struct S { int p,q; };
+
+/*@
+  ensures P: \result.p == - (x->p);
+  ensures Q: \result.q == x->q;
+*/
+struct S negate(struct S *x)
+{
+  struct S r = *x;
+  r.p = - r.p ;
+  return r;
+}
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index 9f6be07073a925679b0ca1e7c1a162a899d9544d..c1cd19d4c0f58db0c274a19707e3d2dcdd3e415f 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -83,6 +83,7 @@ module MINDEX : Hashtbl.S with type key = model
 val is_defined : unit -> bool
 val on_context : context -> ('a -> 'b) -> 'a -> 'b
 val get_model : unit -> model
+val get_ident : unit -> string
 val get_scope : unit -> scope
 val get_context : unit -> context