nits

easycrypt.project

@@ -1,4 +1,6 @@
 [general]
 provers = [email protected]
-provers = [email protected]
-provers = [email protected]
+provers = [email protected]
+provers = [email protected]
+
+rdirs = Jasmin:jasmin/eclib

src/ecCircuits.ml

@@ -1104,22 +1104,24 @@ let input_of_variable (env:env) (v: variable) : circuit * cinput =
   {(circ_ident inp) with inps=[]}, inp
 
 
-let pstate_of_memtype ?(pstate = Map.empty) (env: env) (mt: memtype) =
-  let invs = match mt with
-  | Lmt_concrete (Some lmt) -> lmt.lmt_decl 
-    |> List.filter_map (fun ov -> if Option.is_none ov.ov_name then None
-                                  else Some {v_name = Option.get ov.ov_name; v_type=ov.ov_type})
-  | _ -> assert false
-  in
-
-  let inps = List.map (input_of_variable env) invs in
+let pstate_of_variables ?(pstate = Map.empty) (env : env) (vars : variable list) =
+  let inps = List.map (input_of_variable env) vars in
   let inpcs, inps = List.split inps in
-  let inpcs = List.combine inpcs @@ List.map (fun v -> v.v_name) invs in
+  let inpcs = List.combine inpcs @@ List.map (fun v -> v.v_name) vars in
   let pstate = List.fold_left 
     (fun pstate (inp, v) -> Map.add v inp pstate)
     pstate inpcs 
   in pstate, inps
 
+let pstate_of_memtype ?pstate (env: env) (mt : memtype) =
+  let Lmt_concrete lmt = mt in
+  let vars =
+    List.filter_map (function 
+      | { ov_name = Some name; ov_type = ty } ->
+        Some { v_name = name; v_type = ty; }
+      | _ -> None
+    ) (Option.get lmt).lmt_decl in
+  pstate_of_variables ?pstate env vars
 
 let process_instr (hyps: hyps) (mem: memory) ?(cache: cache = Map.empty) (pstate: _) (inst: instr) =
   let env = toenv hyps in
@@ -1133,23 +1135,34 @@ let process_instr (hyps: hyps) (mem: memory) ?(cache: cache = Map.empty) (pstate
       (Printexc.to_string e) in 
       raise @@ CircError err
 
-let insts_equiv (hyps: hyps) ((mem, mt): memenv) ?(pstate: _ = Map.empty) (insts_left: instr list) (insts_right: instr list): bool =
-  let pstate, inps = pstate_of_memtype ~pstate (toenv hyps) mt in
-  let pstate_left = List.fold_left (process_instr hyps mem) pstate insts_left in
-  let pstate_right = List.fold_left (process_instr hyps mem) pstate insts_right in
-
-  (* if (Map.keys pstate_left |> Set.of_enum) != (Map.keys pstate_right |> Set.of_enum) then *)
-    (* begin *)
-    (* Format.eprintf "Left: @."; *)
-    (* Map.iter (fun k _ -> Format.eprintf "%s@." k) pstate_left; *)
-    (* Format.eprintf "Right: @."; *)
-    (* Map.iter (fun k _ -> Format.eprintf "%s@." k) pstate_right; *)
-    (* false *)
-    (* end *)
-  (* else *)
-    Map.foldi (fun var circ bacc -> 
-      let circ = {circ with inps=inps @ circ.inps} in
-      let circ2 = (Map.find var pstate_right) in
-      let circ2 = {circ2 with inps=inps @ circ2.inps} in
-      bacc && (circ_equiv circ circ2 None)) 
-    pstate_left true
+let instrs_equiv
+   (hyps       : hyps         )
+   ((mem, mt)  : memenv       )
+  ?(pstate     : _ = Map.empty)
+   (s1         : instr list   )
+   (s2         : instr list   ) : bool
+=
+  let env = LDecl.toenv hyps in
+
+  let rd, rglobs = EcPV.PV.elements (EcPV.is_read  env (s1 @ s2)) in
+  let wr, wglobs = EcPV.PV.elements (EcPV.is_write env (s1 @ s2)) in
+
+  if not (List.is_empty rglobs && List.is_empty wglobs) then
+    raise (CircError "the statements should not read/write globs");
+
+  if not (List.for_all (EcTypes.is_loc |- fst) (rd @ wr)) then
+    raise (CircError "the statements should not read/write global variables");
+
+  let pstate = List.map (fun (pv, ty) -> { v_name = EcTypes.get_loc pv; v_type = ty; }) wr in
+  let pstate, inputs = pstate_of_variables env pstate in
+
+  let pstate1 = List.fold_left (process_instr hyps mem) pstate s1 in
+  let pstate2 = List.fold_left (process_instr hyps mem) pstate s2 in
+
+  Map.keys pstate |> Enum.for_all (fun var -> 
+    let circ1 = Map.find var pstate1 in
+    let circ1 = { circ1 with inps = inputs @ circ1.inps } in
+    let circ2 = Map.find var pstate2 in
+    let circ2 = { circ2 with inps = inputs @ circ2.inps } in
+    circ_equiv circ1 circ2 None
+  )

src/ecCircuits.mli

@@ -34,5 +34,5 @@ val circ_equiv : ?strict:bool -> circuit -> circuit -> circuit option -> bool
 val circuit_of_form : ?pstate:pstate -> ?cache:cache -> hyps -> form -> circuit
 val pstate_of_memtype : ?pstate:pstate -> env -> memtype -> pstate * cinput list
 val input_of_variable : env -> variable -> circuit * cinput
-val insts_equiv : hyps -> memenv -> ?pstate:pstate -> instr list -> instr list -> bool
+val instrs_equiv : hyps -> memenv -> ?pstate:pstate -> instr list -> instr list -> bool
 val process_instr : hyps -> memory -> ?cache:cache -> pstate -> instr -> (symbol, circuit) Map.t

src/ecEnv.ml

@@ -3428,6 +3428,7 @@ module Theory = struct
           env_atbase  = bind_at_th thpath env.env_atbase cth.cth_items;
           env_ntbase  = bind_nt_th thpath env.env_ntbase cth.cth_items;
           env_redbase = bind_rd_th thpath env.env_redbase cth.cth_items;
+          env_crbds   = bind_cr_th thpath env.env_crbds cth.cth_items;
           env_thenvs  = Mp.set_union env.env_thenvs compiled.compiled; }
 end
 

src/phl/ecPhlRwPrgm.ml

@@ -7,35 +7,45 @@ open EcLowPhlGoal
 (* -------------------------------------------------------------------- *)
 type change_t = pcodepos * int * pstmt
 
-
+(* -------------------------------------------------------------------- *)
 let process_change ((cpos, i, s) : change_t) (tc : tcenv1) =
   let env = FApi.tc1_env tc in
   let hs = EcLowPhlGoal.tc1_as_hoareS tc in
-  let env = EcEnv.Memory.push_active hs.hs_m env in
 
-  let cpos = EcTyping.trans_codepos env cpos in
+  let cpos =
+    let env = EcEnv.Memory.push_active hs.hs_m env in
+    EcTyping.trans_codepos env cpos in
+
   let s =
     let ue = EcProofTyping.unienv_of_hyps (FApi.tc1_hyps tc) in
     let s  = EcTyping.transstmt env ue s in
-    let sb = EcCoreSubst.Tuni.subst (EcUnify.UniEnv.close ue) in
-    (* let sb = { EcTypes.e_subst_id with es_ty = sb } in *)
 
+    assert (EcUnify.UniEnv.closed ue); (* FIXME *)
+
+    let sb = EcCoreSubst.Tuni.subst (EcUnify.UniEnv.close ue) in
     EcCoreSubst.s_subst sb s in
 
   let zp = Zpr.zipper_of_cpos env cpos hs.hs_s in
   let zp =
-    let old, tl = List.split_at i zp.z_tail in
-    let () = assert (EcCircuits.insts_equiv (FApi.tc1_hyps tc) hs.hs_m old s.s_node) in
-    { zp with z_tail = s.s_node @ tl } in
+    let target, tl = List.split_at i zp.z_tail in
 
-  let zp = Zpr.zip zp in
+    begin
+      try
+        if not (EcCircuits.instrs_equiv (FApi.tc1_hyps tc) hs.hs_m target s.s_node) then
+          tc_error !!tc "statements are not circuit-equivalent"
+        with EcCircuits.CircError s ->
+          tc_error !!tc "circuit-equivalence checker error: %s" s
+    end;
+    { zp with z_tail = s.s_node @ tl } in
 
-  let hs = { hs with hs_s = zp } in
+  let hs = { hs with hs_s = Zpr.zip zp } in
 
   FApi.xmutate1 tc `BChange [EcFol.f_hoareS_r hs]
 
+(* -------------------------------------------------------------------- *)
 type idassign_t = pcodepos * pqsymbol
 
+(* -------------------------------------------------------------------- *)
 let process_idassign ((cpos, pv) : idassign_t) (tc : tcenv1) =
   let env = FApi.tc1_env tc in
   let hs = EcLowPhlGoal.tc1_as_hoareS tc in

theories/datatypes/QFABV.ec

@@ -271,7 +271,6 @@ theory BVOperators.
   end BVTruncate.
 
 
-print List.drop.
   (* ------------------------------------------------------------------ *)
   abstract theory BVExtract.
     clone BV as BV1.
@@ -287,8 +286,7 @@ print List.drop.
   end BVExtract.
 
 
-print List. 
-(* ------------------------------------------------------------------ *)
+  (* ------------------------------------------------------------------ *)
   abstract theory BVConcat.
     clone BV as BV1.
     clone BV as BV2.