Fine Grained Module Definitions

examples/br93.ec

@@ -83,7 +83,7 @@ import H.Lazy.
 (* BR93 is a module that, given access to an oracle H from type         *)
 (*   `from` to type `rand` (see `print Oracle.`), implements procedures *)
 (*   `keygen`, `enc` and `dec` as follows described below.              *)
-module BR93 (H:Oracle) = {
+module BR93 (H : Oracle) = {
   (* `keygen` simply samples a key pair in `dkeys` *)
   proc keygen() = {
     var kp;
@@ -183,14 +183,14 @@ qed.
 
 (* But we can't do it (yet) for IND-CPA because of the random oracle    *)
 (*             Instead, we define CPA for BR93 with that particular RO. *)
-module type Adv (ARO: POracle)  = {
+module type Adv (ARO : POracle)  = {
   proc a1(p:pkey): (ptxt * ptxt)
   proc a2(c:ctxt): bool
 }.
 
 (* We need to log the random oracle queries made to the adversary       *)
 (*                               in order to express the final theorem. *)
-module Log (H:Oracle) = {
+module Log (H : Oracle) = {
   var qs: rand list
 
   proc init() = {
@@ -251,23 +251,17 @@ declare axiom A_a1_ll (O <: POracle {-A}): islossless O.o => islossless A(O).a1.
 declare axiom A_a2_ll (O <: POracle {-A}): islossless O.o => islossless A(O).a2.
 
 (* Step 1: replace RO call with random sampling                         *)
-local module Game1 = {
-  var r: rand
-
-  proc main() = {
-    var pk, sk, m0, m1, b, h, c, b';
-                Log(LRO).init();
-    (pk,sk)  <$ dkeys;
-    (m0,m1)  <@ A(Log(LRO)).a1(pk);
-    b        <$ {0,1};
-
-    r        <$ drand;
-    h        <$ dptxt;
-    c        <- ((f pk r),h +^ (b?m0:m1));
-
-    b'       <@ A(Log(LRO)).a2(c);
-    return b' = b;
-  }
+local module Game1 = BR93_CPA(A) with {
+  var r : rand
+
+  proc main [
+    (* new local variable to store the sampled ptxt *)
+    var h : ptxt
+    (* inline key generation *)
+    ^ <@ {2} ~ { (pk, sk) <$ dkeys; }
+    (* inline challenge encryption and idealize RO call *)
+    ^ c<@ ~ { r <$ drand; h <$ dptxt; c <- (f pk r, h +^ (b ? m0 : m1)); }
+  ]
 }.
 
 local lemma pr_Game0_Game1 &m:
@@ -327,23 +321,11 @@ by move=> _ rR aL mL aR qsR mR h /h [] ->.
 qed.
 
 (* Step 2: replace h ^ m with h in the challenge encryption            *)
-local module Game2 = {
-  var r: rand
-
-  proc main() = {
-    var pk, sk, m0, m1, b, h, c, b';
-                Log(LRO).init();
-    (pk,sk)  <$ dkeys;
-    (m0,m1)  <@ A(Log(LRO)).a1(pk);
-    b        <$ {0,1};
-
-    r        <$ drand;
-    h        <$ dptxt;
-    c        <- ((f pk r),h);
-
-    b'       <@ A(Log(LRO)).a2(c);
-    return b' = b;
-  }
+local module Game2 = Game1 with {
+  proc main [
+    (* Challenge ciphertext is now produced uniformly at random *)
+    ^ c<- ~ { c <- (f pk r, h); }
+  ]
 }.
 
 local equiv eq_Game1_Game2: Game1.main ~ Game2.main:
@@ -402,12 +384,12 @@ local module OWr (I : Inverter) = {
 
 (* We can easily prove that it is strictly equivalent to OW              *)
 local lemma OW_OWr &m (I <: Inverter {-OWr}):
-  Pr[OW(I).main() @ &m: res]
+    Pr[OW(I).main() @ &m: res]
   = Pr[OWr(I).main() @ &m: res].
 proof. by byequiv=> //=; sim. qed.
 
 local lemma pr_Game2_OW &m:
-  Pr[Game2.main() @ &m: Game2.r \in Log.qs]
+     Pr[Game2.main() @ &m: Game2.r \in Log.qs]
   <= Pr[OW(I(A)).main() @ &m: res].
 proof.
 rewrite (OW_OWr &m (I(A))). (* Note: we proved it forall (abstract) I    *)
@@ -431,7 +413,7 @@ by auto=> /> [pk sk] ->.
 qed.
 
 lemma Reduction &m:
-  Pr[BR93_CPA(A).main() @ &m : res] - 1%r/2%r
+     Pr[BR93_CPA(A).main() @ &m : res] - 1%r/2%r
   <= Pr[OW(I(A)).main() @ &m: res].
 proof.
 smt(pr_Game0_Game1 pr_Game1_Game2 pr_bad_Game1_Game2 pr_Game2 pr_Game2_OW).
@@ -675,4 +657,3 @@ by move=> O O_o_ll; proc; call (A_a2_ll O O_o_ll).
 qed.
 
 end section.
-

src/ecLowPhlGoal.ml

@@ -578,7 +578,7 @@ type 'a zip_t =
 let t_fold f (cenv : code_txenv) (cpos : codepos) (_ : form * form) (state, s) =
   try
     let env = EcEnv.LDecl.toenv (snd cenv) in
-    let (me, f) = Zpr.fold env cenv cpos f state s in
+    let (me, f) = Zpr.fold env cenv cpos (fun _ -> f) state s in
       ((me, f, []) : memenv * _ * form list)
   with Zpr.InvalidCPos -> tc_error (fst cenv) "invalid code position"
 

src/ecMatching.ml

@@ -57,7 +57,10 @@ module Zipper = struct
   module P = EcPath
 
   type ('a, 'state) folder =
-    'a -> 'state -> instr -> 'state * instr list
+    env -> 'a -> 'state -> instr -> 'state * instr list
+
+  type ('a, 'state) folder_tl =
+    env -> 'a -> 'state -> instr -> instr list -> 'state * instr list
 
   type spath_match_ctxt = {
     locals : (EcIdent.t * ty) list;
@@ -71,18 +74,19 @@ module Zipper = struct
   | ZIfThen of expr * spath * stmt
   | ZIfElse of expr * stmt  * spath
   | ZMatch  of expr * spath * spath_match_ctxt
-  
+
   and spath = (instr list * instr list) * ipath
 
   type zipper = {
     z_head : instr list;                (* instructions on my left (rev)       *)
     z_tail : instr list;                (* instructions on my right (me incl.) *)
     z_path : ipath;                     (* path (zipper) leading to me         *)
+    z_env  : env option;
   }
 
   let cpos (i : int) : codepos1 = (0, `ByPos i)
 
-  let zipper hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; }
+  let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; }
 
   let find_by_cp_match
     (env     : EcEnv.env)
@@ -193,19 +197,19 @@ module Zipper = struct
     ((cp1, sub) : codepos1 * codepos_brsel)
     (s          : stmt)
     (zpr        : ipath)
-  : (ipath * stmt) * (codepos1 * codepos_brsel)
+  : (ipath * stmt) * (codepos1 * codepos_brsel) * env
   =
     let (s1, i, s2) = find_by_cpos1 env cp1 s in
-    let zpr =
+    let zpr, env =
       match i.i_node, sub with
       | Swhile (e, sw), `Cond true ->
-          (ZWhile (e, ((s1, s2), zpr)), sw)
+          (ZWhile (e, ((s1, s2), zpr)), sw), env
 
       | Sif (e, ifs1, ifs2), `Cond true ->
-          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1)
+          (ZIfThen (e, ((s1, s2), zpr), ifs2), ifs1), env
 
       | Sif (e, ifs1, ifs2), `Cond false ->
-          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2)
+          (ZIfElse (e, ifs1, ((s1, s2), zpr)), ifs2), env
 
       | Smatch (e, bs), `Match cn ->
           let _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
@@ -216,19 +220,20 @@ module Zipper = struct
             with Not_found -> raise InvalidCPos
           in
           let prebr, (locals, body), postbr = List.pivot_at ix bs in
-          (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body)
+          let env = EcEnv.Var.bind_locals locals env in
+          (ZMatch (e, ((s1, s2), zpr), { locals; prebr; postbr; }), body), env
 
       | _ -> raise InvalidCPos
-    in zpr, ((0, `ByPos (1 + List.length s1)), sub)
+    in zpr, ((0, `ByPos (1 + List.length s1)), sub), env
 
   let zipper_of_cpos_r (env : EcEnv.env) ((nm, cp1) : codepos) (s : stmt) =
-    let (zpr, s), nm =
+    let ((zpr, s), env), nm =
       List.fold_left_map
-        (fun (zpr, s) nm1 -> zipper_at_nm_cpos1 env nm1 s zpr)
-        (ZTop, s) nm in
+        (fun ((zpr, s), env) nm1 -> let zpr, s, env = zipper_at_nm_cpos1 env nm1 s zpr in (zpr, env), s)
+        ((ZTop, s), env) nm in
 
     let s1, i, s2 = find_by_cpos1 env cp1 s in
-    let zpr = zipper s1 (i :: s2) zpr in
+    let zpr = zipper ~env s1 (i :: s2) zpr in
 
     (zpr, (nm, (0, `ByPos (1 + List.length s1))))
 
@@ -274,21 +279,28 @@ module Zipper = struct
     in
       List.rev after
 
-  let fold env cenv cpos f state s =
+  let fold_tl env cenv cpos f state s =
     let zpr = zipper_of_cpos env cpos s in
 
       match zpr.z_tail with
       | []      -> raise InvalidCPos
       | i :: tl -> begin
-          match f cenv state i with
+          match f (odfl env zpr.z_env) cenv state i tl with
           | (state', [i']) when i == i' && state == state' -> (state, s)
-          | (state', si  ) -> (state', zip { zpr with z_tail = si @ tl })
+          | (state', si  ) -> (state', zip { zpr with z_tail = si })
       end
 
+  let fold env cenv cpos f state s =
+    let f e ce st i tl =
+      let state', si = f e ce st i in
+      state', si @ tl
+    in
+    fold_tl env cenv cpos f state s
+
   let map env cpos f s =
     fst_map
       Option.get
-      (fold env () cpos (fun () _ i -> fst_map some (f i)) None s)
+      (fold env () cpos (fun _ () _ i -> fst_map some (f i)) None s)
 end
 
 (* -------------------------------------------------------------------- *)

src/ecMatching.mli

@@ -61,6 +61,7 @@ module Zipper : sig
     z_head : instr list;                (* instructions on my left (rev)       *)
     z_tail : instr list;                (* instructions on my right (me incl.) *)
     z_path : ipath ;                    (* path (zipper) leading to me         *)
+    z_env  : env option;                (* env with local vars from previous instructions *)
   }
 
   exception InvalidCPos
@@ -79,7 +80,7 @@ module Zipper : sig
   val offset_of_position : env -> codepos1 -> stmt -> int
 
   (* [zipper] soft constructor *)
-  val zipper : instr list -> instr list -> ipath -> zipper
+  val zipper : ?env : env -> instr list -> instr list -> ipath -> zipper
 
   (* Return the zipper for the stmt [stmt] at code position [codepos].
    * Raise [InvalidCPos] if [codepos] is not valid for [stmt]. It also
@@ -101,7 +102,8 @@ module Zipper : sig
    *)
   val after : strict:bool -> zipper -> instr list list
 
-  type ('a, 'state) folder = 'a -> 'state -> instr -> 'state * instr list
+  type ('a, 'state) folder = env -> 'a -> 'state -> instr -> 'state * instr list
+  type ('a, 'state) folder_tl = env -> 'a -> 'state -> instr -> instr list -> 'state * instr list
 
   (* [fold env v cpos f state s] create the zipper for [s] at [cpos], and apply
    * [f] to it, along with [v] and the state [state]. [f] must return the
@@ -112,6 +114,9 @@ module Zipper : sig
    *)
   val fold : env -> 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
 
+  (* Same as above but using [folder_tl]. *)
+  val fold_tl : env -> 'a -> codepos -> ('a, 'state) folder_tl -> 'state -> stmt -> 'state * stmt
+
   (* [map cpos env f s] is a special case of [fold] where the state and the
    * out-of-band data are absent
    *)

src/ecParser.mly

@@ -1443,6 +1443,30 @@ mod_item:
 | IMPORT VAR ms=loc(mod_qident)+
     { Pst_import ms }
 
+mod_update_var:
+| v=var_decl { v }
+
+mod_update_fun:
+| PROC x=lident LBRACKET lvs=var_decl* fups=fun_update+ RBRACKET res_up=option(RES TILD e=sexpr {e})
+  { (x, lvs, (List.flatten fups, res_up)) }
+
+update_stmt:
+| PLUS s=brace(stmt){ [Pups_add (s, true)] }
+| MINUS s=brace(stmt){ [Pups_add (s, false)] }
+| TILD s=brace(stmt) { [Pups_del; Pups_add (s, true)] }
+| MINUS { [Pups_del] }
+
+update_cond:
+| PLUS e=sexpr { Pupc_add e }
+| TILD e=sexpr { Pupc_mod e }
+| MINUS bs=branch_select { Pupc_del bs }
+
+fun_update:
+| cp=loc(codepos) sup=update_stmt 
+  { List.map (fun v -> (cp, Pup_stmt v)) sup }
+| cp=loc(codepos) cup=update_cond 
+  { [(cp, Pup_cond cup)] }
+
 (* -------------------------------------------------------------------- *)
 (* Modules                                                              *)
 
@@ -1453,6 +1477,9 @@ mod_body:
 | LBRACE stt=loc(mod_item)* RBRACE
     { Pm_struct stt }
 
+| m=mod_qident WITH LBRACE vs=mod_update_var* fs=mod_update_fun* RBRACE
+  { Pm_update (m, vs, fs) }
+
 mod_def_or_decl:
 | locality=locality MODULE header=mod_header c=mod_cast? EQ ptm_body=loc(mod_body)
   { let ptm_header = match c with None -> header | Some c ->  Pmh_cast(header,c) in