diff --git a/easycrypt.project b/easycrypt.project index f59238299..daa5ec0f1 100644 --- a/easycrypt.project +++ b/easycrypt.project @@ -1,4 +1,6 @@ [general] provers = Alt-Ergo@2.4 -provers = CVC5@1.0 -provers = Z3@4.12 +provers = CVC4@1.8 +provers = Z3@4.8 + +rdirs = Jasmin:jasmin/eclib diff --git a/src/ecCircuits.ml b/src/ecCircuits.ml index 224bf2eba..7a9807cea 100644 --- a/src/ecCircuits.ml +++ b/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 + ) diff --git a/src/ecCircuits.mli b/src/ecCircuits.mli index 77c911a69..13b2406ba 100644 --- a/src/ecCircuits.mli +++ b/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 diff --git a/src/ecEnv.ml b/src/ecEnv.ml index 3399f35cd..8b116fdc0 100644 --- a/src/ecEnv.ml +++ b/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 diff --git a/src/phl/ecPhlRwPrgm.ml b/src/phl/ecPhlRwPrgm.ml index 4436e4adc..0f8ee2c61 100644 --- a/src/phl/ecPhlRwPrgm.ml +++ b/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 diff --git a/theories/datatypes/QFABV.ec b/theories/datatypes/QFABV.ec index 08fc84660..4fa6e0dcc 100644 --- a/theories/datatypes/QFABV.ec +++ b/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.