diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index 451fc787..9095af72 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -23,9 +23,8 @@ open Ast (** {1 Helpers and type definitions}*) -type vc_return = typed expr * (typed expr, typ) Var.Map.t -(** The return type of VC generators is the VC expression plus the types of any - locally free variable inside that expression. *) +type vc_return = typed expr +(** The return type of VC generators is the VC expression *) type ctx = { current_scope_name : ScopeName.t; @@ -43,31 +42,22 @@ let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) : let conjunction (args : vc_return list) (mark : typed mark) : vc_return = let acc, list = - match args with - | hd :: tl -> hd, tl - | [] -> ((ELit (LBool true), mark), Var.Map.empty), [] + match args with hd :: tl -> hd, tl | [] -> (ELit (LBool true), mark), [] in List.fold_left - (fun (acc, acc_ty) (arg, arg_ty) -> - ( (EApp ((EOp (Binop And), mark), [arg; acc]), mark), - Var.Map.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty - )) + (fun acc arg -> EApp ((EOp (Binop And), mark), [arg; acc]), mark) acc list -let negation ((arg, arg_ty) : vc_return) (mark : typed mark) : vc_return = - (EApp ((EOp (Unop Not), mark), [arg]), mark), arg_ty +let negation (arg : vc_return) (mark : typed mark) : vc_return = + EApp ((EOp (Unop Not), mark), [arg]), mark let disjunction (args : vc_return list) (mark : typed mark) : vc_return = let acc, list = - match args with - | hd :: tl -> hd, tl - | [] -> ((ELit (LBool false), mark), Var.Map.empty), [] + match args with hd :: tl -> hd, tl | [] -> (ELit (LBool false), mark), [] in List.fold_left - (fun ((acc, acc_ty) : vc_return) (arg, arg_ty) -> - ( (EApp ((EOp (Binop Or), mark), [arg; acc]), mark), - Var.Map.union (fun _ _ _ -> failwith "should not happen") acc_ty arg_ty - )) + (fun (acc : vc_return) arg -> + EApp ((EOp (Binop Or), mark), [arg; acc]), mark) acc list (** [half_product \[a1,...,an\] \[b1,...,bm\] returns \[(a1,b1),...(a1,bn),...(an,b1),...(an,bm)\]] *) @@ -131,19 +121,12 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : | EAssert e1 | ErrorOnEmpty e1 -> (generate_vc_must_not_return_empty ctx) e1 - | EAbs (binder, typs) -> + | EAbs (binder, _typs) -> (* Hot take: for a function never to return an empty error when called, it has to do so whatever its input. So we universally quantify over the variable of the function when inspecting the body, resulting in simply traversing through in the code here. *) - let vars, body = Bindlib.unmbind binder in - let vc_body_expr, vc_body_ty = - (generate_vc_must_not_return_empty ctx) body - in - ( vc_body_expr, - snd - @@ List.fold_left - (fun (i, acc) ty -> i + 1, Var.Map.add vars.(i) ty acc) - (0, vc_body_ty) typs ) + let _vars, body = Bindlib.unmbind binder in + (generate_vc_must_not_return_empty ctx) body | EApp (f, args) -> (* We assume here that function calls never return empty error, which implies all functions have been checked never to return empty errors. *) @@ -151,25 +134,18 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : (List.map (generate_vc_must_not_return_empty ctx) (f :: args)) (Marked.get_mark e) | EIfThenElse (e1, e2, e3) -> - let e1_vc, vc_typ1 = generate_vc_must_not_return_empty ctx e1 in - let e2_vc, vc_typ2 = generate_vc_must_not_return_empty ctx e2 in - let e3_vc, vc_typ3 = generate_vc_must_not_return_empty ctx e3 in + let e1_vc = generate_vc_must_not_return_empty ctx e1 in + let e2_vc = generate_vc_must_not_return_empty ctx e2 in + let e3_vc = generate_vc_must_not_return_empty ctx e3 in conjunction - [ - e1_vc, vc_typ1; - ( (EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e), - Var.Map.union - (fun _ _ _ -> failwith "should not happen") - vc_typ2 vc_typ3 ); - ] + [e1_vc; EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e] (Marked.get_mark e) - | ELit LEmptyError -> - Marked.same_mark_as (ELit (LBool false)) e, Var.Map.empty + | ELit LEmptyError -> Marked.same_mark_as (ELit (LBool false)) e | EVar _ (* Per default calculus semantics, you cannot call a function with an argument that evaluates to the empty error. Thus, all variable evaluate to non-empty-error terms. *) | ELit _ | EOp _ -> - Marked.same_mark_as (ELit (LBool true)) e, Var.Map.empty + Marked.same_mark_as (ELit (LBool true)) e | EDefault (exceptions, just, cons) -> (* never returns empty if and only if: - first we look if e1 .. en ejust can return empty; @@ -181,21 +157,20 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : conjunction [ generate_vc_must_not_return_empty ctx just; - (let vc_just_expr, vc_just_ty = + (let vc_just_expr = generate_vc_must_not_return_empty ctx cons in - ( ( EIfThenElse - ( just, - (* Comment from Alain: the justification is not checked for holding an default term. - In such cases, we need to encode the logic of the default terms within - the generation of the verification condition (Z3encoding.translate_expr). - Answer from Denis: Normally, there is a structural invariant from the - surface language to intermediate representation translation preventing - any default terms to appear in justifications.*) - vc_just_expr, - (ELit (LBool false), Marked.get_mark e) ), - Marked.get_mark e ), - vc_just_ty )); + ( EIfThenElse + ( just, + (* Comment from Alain: the justification is not checked for holding an default term. + In such cases, we need to encode the logic of the default terms within + the generation of the verification condition (Z3encoding.translate_expr). + Answer from Denis: Normally, there is a structural invariant from the + surface language to intermediate representation translation preventing + any default terms to appear in justifications.*) + vc_just_expr, + (ELit (LBool false), Marked.get_mark e) ), + Marked.get_mark e )); ] (Marked.get_mark e); ]) @@ -204,11 +179,11 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : out [@@ocamlformat "wrap-comments=false"] -(** [generate_vs_must_not_return_confict e] returns the dcalc boolean expression - [b] such that if [b] is true, then [e] will never return a conflict error. - It also returns a map of all the types of locally free variables inside the - expression. *) -let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr) : +(** [generate_vc_must_not_return_conflict e] returns the dcalc boolean + expression [b] such that if [b] is true, then [e] will never return a + conflict error. It also returns a map of all the types of locally free + variables inside the expression. *) +let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) : vc_return = let out = (* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this @@ -216,46 +191,32 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr) : match Marked.unmark e with | ETuple (args, _) | EArray args -> conjunction - (List.map (generate_vs_must_not_return_confict ctx) args) + (List.map (generate_vc_must_not_return_conflict ctx) args) (Marked.get_mark e) | EMatch (arg, arms, _) -> conjunction - (List.map (generate_vs_must_not_return_confict ctx) (arg :: arms)) + (List.map (generate_vc_must_not_return_conflict ctx) (arg :: arms)) (Marked.get_mark e) | ETupleAccess (e1, _, _, _) | EInj (e1, _, _, _) | EAssert e1 | ErrorOnEmpty e1 -> - generate_vs_must_not_return_confict ctx e1 - | EAbs (binder, typs) -> - let vars, body = Bindlib.unmbind binder in - let vc_body_expr, vc_body_ty = - (generate_vs_must_not_return_confict ctx) body - in - ( vc_body_expr, - List.fold_left - (fun acc (var, ty) -> Var.Map.add var ty acc) - vc_body_ty - (List.map2 (fun x y -> x, y) (Array.to_list vars) typs) ) + generate_vc_must_not_return_conflict ctx e1 + | EAbs (binder, _typs) -> + let _vars, body = Bindlib.unmbind binder in + (generate_vc_must_not_return_conflict ctx) body | EApp (f, args) -> conjunction - (List.map (generate_vs_must_not_return_confict ctx) (f :: args)) + (List.map (generate_vc_must_not_return_conflict ctx) (f :: args)) (Marked.get_mark e) | EIfThenElse (e1, e2, e3) -> - let e1_vc, vc_typ1 = generate_vs_must_not_return_confict ctx e1 in - let e2_vc, vc_typ2 = generate_vs_must_not_return_confict ctx e2 in - let e3_vc, vc_typ3 = generate_vs_must_not_return_confict ctx e3 in + let e1_vc = generate_vc_must_not_return_conflict ctx e1 in + let e2_vc = generate_vc_must_not_return_conflict ctx e2 in + let e3_vc = generate_vc_must_not_return_conflict ctx e3 in conjunction - [ - e1_vc, vc_typ1; - ( (EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e), - Var.Map.union - (fun _ _ _ -> failwith "should not happen") - vc_typ2 vc_typ3 ); - ] + [e1_vc; EIfThenElse (e1, e2_vc, e3_vc), Marked.get_mark e] (Marked.get_mark e) - | EVar _ | ELit _ | EOp _ -> - Marked.same_mark_as (ELit (LBool true)) e, Var.Map.empty + | EVar _ | ELit _ | EOp _ -> Marked.same_mark_as (ELit (LBool true)) e | EDefault (exceptions, just, cons) -> (* never returns conflict if and only if: - neither e1 nor ... nor en nor ejust nor econs return conflict @@ -277,7 +238,7 @@ let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr) : in let others = List.map - (generate_vs_must_not_return_confict ctx) + (generate_vc_must_not_return_conflict ctx) (just :: cons :: exceptions) in let out = conjunction (quadratic :: others) (Marked.get_mark e) in @@ -299,7 +260,6 @@ type verification_condition = { vc_asserts : typed expr; vc_scope : ScopeName.t; vc_variable : typed expr Var.t Marked.pos; - vc_free_vars_typ : (typed expr, typ) Var.Map.t; } let trivial_assert e = Marked.same_mark_as (ELit (LBool true)) e @@ -343,9 +303,7 @@ let rec generate_verification_conditions_scope_body_expr Expr.unbox (Expr.remove_logging_calls scope_let.scope_let_expr) in let e = match_and_ignore_outer_reentrant_default ctx e in - let vc_confl, vc_confl_typs = - generate_vs_must_not_return_confict ctx e - in + let vc_confl = generate_vc_must_not_return_conflict ctx e in let vc_confl = if !Cli.optimize_flag then Bindlib.unbox (Optimizations.optimize_expr ctx.decl vc_confl) @@ -359,10 +317,6 @@ let rec generate_verification_conditions_scope_body_expr (* Placeholder until we add all assertions in scope once * we finished traversing it *) vc_asserts = trivial_assert e; - vc_free_vars_typ = - Var.Map.union - (fun _ _ -> failwith "should not happen") - ctx.scope_variables_typs vc_confl_typs; vc_scope = ctx.current_scope_name; vc_variable = scope_let_var, scope_let.scope_let_pos; }; @@ -371,9 +325,7 @@ let rec generate_verification_conditions_scope_body_expr let vc_list = match scope_let.scope_let_kind with | ScopeVarDefinition -> - let vc_empty, vc_empty_typs = - generate_vc_must_not_return_empty ctx e - in + let vc_empty = generate_vc_must_not_return_empty ctx e in let vc_empty = if !Cli.optimize_flag then Bindlib.unbox (Optimizations.optimize_expr ctx.decl vc_empty) @@ -383,10 +335,6 @@ let rec generate_verification_conditions_scope_body_expr vc_guard = Marked.same_mark_as (Marked.unmark vc_empty) e; vc_kind = NoEmptyError; vc_asserts = trivial_assert e; - vc_free_vars_typ = - Var.Map.union - (fun _ _ -> failwith "should not happen") - ctx.scope_variables_typs vc_empty_typs; vc_scope = ctx.current_scope_name; vc_variable = scope_let_var, scope_let.scope_let_pos; } diff --git a/compiler/verification/conditions.mli b/compiler/verification/conditions.mli index 5d4e1689..4df645be 100644 --- a/compiler/verification/conditions.mli +++ b/compiler/verification/conditions.mli @@ -37,10 +37,6 @@ type verification_condition = { should have type [bool] *) vc_scope : ScopeName.t; vc_variable : typed Dcalc.Ast.expr Var.t Marked.pos; - vc_free_vars_typ : (typed Dcalc.Ast.expr, typ) Var.Map.t; - (** Types of the locally free variables in [vc_guard]. The types of other - free variables linked to scope variables can be obtained with - [Dcalc.Ast.variable_types]. *) } val generate_verification_conditions : diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 6f93feff..cc136565 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -17,14 +17,13 @@ open Utils open Shared_ast -open Dcalc.Ast module type Backend = sig val init_backend : unit -> unit type backend_context - val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding @@ -49,7 +48,7 @@ module type BackendIO = sig type backend_context - val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding diff --git a/compiler/verification/io.mli b/compiler/verification/io.mli index 06bf1853..39573336 100644 --- a/compiler/verification/io.mli +++ b/compiler/verification/io.mli @@ -24,8 +24,7 @@ module type Backend = sig type backend_context - val make_context : - decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding @@ -50,8 +49,7 @@ module type BackendIO = sig type backend_context - val make_context : - decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context + val make_context : decl_ctx -> backend_context type vc_encoding diff --git a/compiler/verification/solver.ml b/compiler/verification/solver.ml index 6f935fa3..81fd1212 100644 --- a/compiler/verification/solver.ml +++ b/compiler/verification/solver.ml @@ -29,7 +29,7 @@ let solve_vc ( vc, try let ctx = - Z3backend.Io.make_context decl_ctx vc.Conditions.vc_free_vars_typ + Z3backend.Io.make_context decl_ctx in let ctx = Z3backend.Io.encode_asserts ctx vc.Conditions.vc_asserts diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml index b911f202..8293b767 100644 --- a/compiler/verification/z3backend.dummy.ml +++ b/compiler/verification/z3backend.dummy.ml @@ -27,7 +27,7 @@ module Io = struct type backend_context = unit - let make_context _ _ = dummy () + let make_context _ = dummy () type vc_encoding = unit diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 908660bb..e7d803e9 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -28,13 +28,10 @@ type context = { ctx_decl : decl_ctx; (* The declaration context from the Catala program, containing information to precisely pretty print Catala expressions *) - ctx_var : (typed expr, typ) Var.Map.t; - (* A map from Catala variables to their types, needed to create Z3 expressions - of the right sort *) ctx_funcdecl : (typed expr, FuncDecl.func_decl) Var.Map.t; (* A map from Catala function names (represented as variables) to Z3 function declarations, used to only define once functions in Z3 queries *) - ctx_z3vars : typed expr Var.t StringMap.t; + ctx_z3vars : (typed expr Var.t * typ) StringMap.t; (* A map from strings, corresponding to Z3 symbol names, to the Catala variable they represent. Used when to pretty-print Z3 models when a counterexample is generated *) @@ -56,13 +53,14 @@ type context = { is an integer which always is greater than 0 *) } (** The context contains all the required information to encode a VC represented - as a Catala term to Z3. The fields [ctx_decl] and [ctx_var] are computed - before starting the translation to Z3, and are thus unmodified throughout - the translation. The [ctx_z3] context is an OCaml abstraction on top of an - underlying C++ imperative implementation, it is therefore only created once. - Unfortunately, the maps [ctx_funcdecl], [ctx_z3vars], and [ctx_z3datatypes] - are computed dynamically during the translation requiring us to pass the - context around in a functional way **) + as a Catala term to Z3. The field [ctx_decl] is computed before starting the + translation to Z3, and are thus unmodified throughout the translation. The + [ctx_z3] context is an OCaml abstraction on top of an underlying C++ + imperative implementation, it is therefore only created once. Unfortunately, + the maps [ctx_funcdecl], [ctx_z3vars], [ctx_z3datatypes], + [ctx_z3matchsubsts], [ctx_z3structs], and [ctx_z3constraints] are computed + dynamically during the translation requiring us to pass the context around + in a functional way **) (** [add_funcdecl] adds the mapping between the Catala variable [v] and the Z3 function declaration [fd] to the context **) @@ -72,10 +70,11 @@ let add_funcdecl (ctx : context) : context = { ctx with ctx_funcdecl = Var.Map.add v fd ctx.ctx_funcdecl } -(** [add_z3var] adds the mapping between [name] and the Catala variable [v] to - the context **) -let add_z3var (name : string) (v : typed expr Var.t) (ctx : context) : context = - { ctx with ctx_z3vars = StringMap.add name v ctx.ctx_z3vars } +(** [add_z3var] adds the mapping between [name] and the Catala variable [v] and + its typ [ty] to the context **) +let add_z3var (name : string) (v : typed expr Var.t) (ty : typ) (ctx : context) + : context = + { ctx with ctx_z3vars = StringMap.add name (v, ty) ctx.ctx_z3vars } (** [add_z3enum] adds the mapping between the Catala enumeration [enum] and the corresponding Z3 datatype [sort] to the context **) @@ -83,8 +82,8 @@ let add_z3enum (enum : EnumName.t) (sort : Sort.sort) (ctx : context) : context = { ctx with ctx_z3datatypes = EnumMap.add enum sort ctx.ctx_z3datatypes } -(** [add_z3var] adds the mapping between temporary variable [v] and the Z3 - expression [e] representing an accessor application to the context **) +(** [add_z3matchsubst] adds the mapping between temporary variable [v] and the + Z3 expression [e] representing an accessor application to the context **) let add_z3matchsubst (v : typed expr Var.t) (e : Expr.expr) (ctx : context) : context = { ctx with ctx_z3matchsubsts = Var.Map.add v e ctx.ctx_z3matchsubsts } @@ -226,11 +225,11 @@ let print_model (ctx : context) (model : Model.model) : string = let symbol_name = Symbol.to_string (FuncDecl.get_name d) in match StringMap.find_opt symbol_name ctx.ctx_z3vars with | None -> () - | Some v -> + | Some (v, ty) -> Format.fprintf fmt "%s %s : %s\n" (Cli.with_style [ANSITerminal.blue] "%s" "-->") (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) - (print_z3model_expr ctx (Var.Map.find v ctx.ctx_var) e)) + (print_z3model_expr ctx ty e)) else (* Declaration d is a function *) match Model.get_func_interp model d with @@ -241,7 +240,7 @@ let print_model (ctx : context) (model : Model.model) : string = (* Print "name : value\n" *) | Some f -> let symbol_name = Symbol.to_string (FuncDecl.get_name d) in - let v = StringMap.find symbol_name ctx.ctx_z3vars in + let v, _ = StringMap.find symbol_name ctx.ctx_z3vars in Format.fprintf fmt "%s %s : %s" (Cli.with_style [ANSITerminal.blue] "%s" "-->") (Cli.with_style [ANSITerminal.yellow] "%s" (Bindlib.name_of v)) @@ -386,24 +385,22 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 d (** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration - corresponding to the variable [v]. If no such function declaration exists - yet, we construct it and add it to the context, thus requiring to return a - new context *) -let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) : + corresponding to the variable [v] and its type [ty]. If no such function + declaration exists yet, we construct it and add it to the context, thus + requiring to return a new context *) +let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) (ty : typ) : context * FuncDecl.func_decl = match Var.Map.find_opt v ctx.ctx_funcdecl with | Some fd -> ctx, fd | None -> ( - (* Retrieves the Catala type of the function [v] *) - let f_ty = Var.Map.find v ctx.ctx_var in - match Marked.unmark f_ty with + match Marked.unmark ty with | TArrow (t1, t2) -> let ctx, z3_t1 = translate_typ ctx (Marked.unmark t1) in let ctx, z3_t2 = translate_typ ctx (Marked.unmark t2) in let name = unique_name v in let fd = FuncDecl.mk_func_decl_s ctx.ctx_z3 name [z3_t1] z3_t2 in let ctx = add_funcdecl v fd ctx in - let ctx = add_z3var name v ctx in + let ctx = add_z3var name v ty ctx in ctx, fd | TAny -> failwith @@ -650,9 +647,9 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = match Var.Map.find_opt v ctx.ctx_z3matchsubsts with | None -> (* We are in the standard case, where this is a true Catala variable *) - let t = Var.Map.find v ctx.ctx_var in + let (Typed { ty = t; _ }) = Marked.get_mark vc in let name = unique_name v in - let ctx = add_z3var name v ctx in + let ctx = add_z3var name v t ctx in let ctx, ty = translate_typ ctx (Marked.unmark t) in let z3_var = Expr.mk_const_s ctx.ctx_z3 name ty in let ctx = @@ -740,7 +737,8 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = match Marked.unmark head with | EOp op -> translate_op ctx op args | EVar v -> - let ctx, fd = find_or_create_funcdecl ctx v in + let (Typed { ty = f_ty; _ }) = Marked.get_mark head in + let ctx, fd = find_or_create_funcdecl ctx v f_ty in (* Fold_right to preserve the order of the arguments: The head argument is appended at the head *) let ctx, z3_args = @@ -820,9 +818,7 @@ module Backend = struct let init_backend () = Cli.debug_print "Running Z3 version %s" Version.to_string - let make_context - (decl_ctx : decl_ctx) - (free_vars_typ : (typed expr, typ) Var.Map.t) : backend_context = + let make_context (decl_ctx : decl_ctx) : backend_context = let cfg = (if !Cli.disable_counterexamples then [] else ["model", "true"]) @ ["proof", "false"] @@ -832,7 +828,6 @@ module Backend = struct { ctx_z3 = z3_ctx; ctx_decl = decl_ctx; - ctx_var = free_vars_typ; ctx_funcdecl = Var.Map.empty; ctx_z3vars = StringMap.empty; ctx_z3datatypes = EnumMap.empty; diff --git a/flake.lock b/flake.lock index 4f2ce58e..43381179 100644 --- a/flake.lock +++ b/flake.lock @@ -17,11 +17,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1667629849, - "narHash": "sha256-P+v+nDOFWicM4wziFK9S/ajF2lc0N2Rg9p6Y35uMoZI=", + "lastModified": 1668087632, + "narHash": "sha256-T/cUx44aYDuLMFfaiVpMdTjL4kpG7bh0VkN6JEM78/E=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "3bacde6273b09a21a8ccfba15586fb165078fb62", + "rev": "5f588eb4a958f1a526ed8da02d6ea1bea0047b9f", "type": "github" }, "original": {