diff options
-rw-r--r-- | compiler/AssociatedTypes.ml | 25 | ||||
-rw-r--r-- | compiler/Extract.ml | 6 | ||||
-rw-r--r-- | compiler/ExtractBase.ml | 2 | ||||
-rw-r--r-- | compiler/ExtractTypes.ml | 7 | ||||
-rw-r--r-- | compiler/InterpreterExpressions.ml | 6 | ||||
-rw-r--r-- | compiler/InterpreterStatements.ml | 20 | ||||
-rw-r--r-- | compiler/InterpreterUtils.ml | 2 | ||||
-rw-r--r-- | compiler/Print.ml | 4 | ||||
-rw-r--r-- | compiler/PrintPure.ml | 18 | ||||
-rw-r--r-- | compiler/Pure.ml | 6 | ||||
-rw-r--r-- | compiler/RegionsHierarchy.ml | 2 | ||||
-rw-r--r-- | compiler/SymbolicAst.ml | 3 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 28 | ||||
-rw-r--r-- | compiler/Translate.ml | 2 | ||||
-rw-r--r-- | compiler/TypesUtils.ml | 3 | ||||
-rw-r--r-- | flake.lock | 42 |
16 files changed, 75 insertions, 101 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 054c8169..7b928566 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -51,9 +51,10 @@ let compute_norm_trait_types_from_preds that it would be enough to only visit the field [ty] of the trait type constraint, but for safety we visit all the fields *) assert (trait_type_constraint_no_regions c); - let trait_ty = TTraitType (c.trait_ref, c.generics, c.type_name) in + let { trait_ref; type_name; ty } : trait_type_constraint = c in + let trait_ty = TTraitType (trait_ref, type_name) in let trait_ty_ref = get_ref trait_ty in - let ty_ref = get_ref c.ty in + let ty_ref = get_ref ty in let new_repr = UnionFind.get ty_ref in let merged = UnionFind.union trait_ty_ref ty_ref in (* Not sure the set operation is necessary, but I want to control which @@ -72,9 +73,7 @@ let compute_norm_trait_types_from_preds List.filter_map (fun (k, v) -> match k with - | TTraitType (trait_ref, generics, type_name) -> - assert (generics = empty_generic_args); - Some ({ trait_ref; type_name }, v) + | TTraitType (trait_ref, type_name) -> Some ({ trait_ref; type_name }, v) | _ -> None) rbindings in @@ -225,20 +224,15 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = let inputs = List.map (norm_ctx_normalize_ty ctx) inputs in let output = norm_ctx_normalize_ty ctx output in TArrow (regions, inputs, output) - | TTraitType (trait_ref, generics, type_name) -> ( + | TTraitType (trait_ref, type_name) -> ( log#ldebug (lazy ("norm_ctx_normalize_ty:\n- trait type: " ^ ty_to_string ctx ty ^ "\n- trait_ref: " ^ trait_ref_to_string ctx trait_ref - ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref - ^ "\n- generics:\n" - ^ generic_args_to_string ctx generics)); + ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* Normalize and attempt to project the type from the trait ref *) let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in - let generics = norm_ctx_normalize_generic_args ctx generics in - (* For now, we don't support higher order types *) - assert (generics = empty_generic_args); let ty : ty = match trait_ref.trait_id with | TraitRef { trait_id = TraitImpl impl_id; generics = ref_generics; _ } @@ -284,7 +278,7 @@ let rec norm_ctx_normalize_ty (ctx : norm_ctx) (ty : ty) : ty = ^ "\n- raw trait ref:\n" ^ show_trait_ref trait_ref)); (* We can't project *) assert (trait_instance_id_is_local_clause trait_ref.trait_id); - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) in let tr : trait_type_ref = { trait_ref; type_name } in (* Lookup the representative, if there is *) @@ -484,11 +478,10 @@ and norm_ctx_normalize_trait_decl_ref (ctx : norm_ctx) let norm_ctx_normalize_trait_type_constraint (ctx : norm_ctx) (ttc : trait_type_constraint) : trait_type_constraint = - let { trait_ref; generics; type_name; ty } = ttc in + let { trait_ref; type_name; ty } : trait_type_constraint = ttc in let trait_ref = norm_ctx_normalize_trait_ref ctx trait_ref in - let generics = norm_ctx_normalize_generic_args ctx generics in let ty = norm_ctx_normalize_ty ctx ty in - { trait_ref; generics; type_name; ty } + { trait_ref; type_name; ty } let mk_norm_ctx (ctx : eval_ctx) : norm_ctx = { diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 46f6a1ca..a93ed6e4 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -326,11 +326,8 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) extract_adt_cons ctx fmt inside adt_cons_id qualif.generics args | Proj proj -> extract_field_projector ctx fmt inside app proj qualif.generics args - | TraitConst (trait_ref, generics, const_name) -> - let use_brackets = generics <> empty_generic_args in - if use_brackets then F.pp_print_string fmt "("; + | TraitConst (trait_ref, const_name) -> extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref; - extract_generic_args ctx fmt TypeDeclId.Set.empty generics; let name = ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id const_name ctx @@ -338,7 +335,6 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) let add_brackets (s : string) = if !backend = Coq then "(" ^ s ^ ")" else s in - if use_brackets then F.pp_print_string fmt ")"; F.pp_print_string fmt ("." ^ add_brackets name)) | _ -> (* "Regular" expression *) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 5e97cd21..297a1d22 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1682,7 +1682,7 @@ let ctx_compute_var_basename (ctx : extraction_ctx) (basename : string option) | TLiteral lty -> ( match lty with TBool -> "b" | TChar -> "c" | TInteger _ -> "i") | TArrow _ -> "f" - | TTraitType (_, _, name) -> name_from_type_ident name) + | TTraitType (_, name) -> name_from_type_ident name) (** Generates a type variable basename. *) let ctx_compute_type_var_basename (_ctx : extraction_ctx) (basename : string) : diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 9d4131d2..bbd5fae4 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -528,7 +528,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_rec false ret_ty; if inside then F.pp_print_string fmt ")" - | TTraitType (trait_ref, generics, type_name) -> ( + | TTraitType (trait_ref, type_name) -> ( if !parameterize_trait_types then raise (Failure "Unimplemented") else let type_name = @@ -547,7 +547,6 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) *) match trait_ref.trait_id with | Self -> - assert (generics = empty_generic_args); assert (trait_ref.generics = empty_generic_args); extract_trait_instance_id_with_dot ctx fmt no_params_tys false trait_ref.trait_id; @@ -555,11 +554,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) | _ -> (* HOL4 doesn't have 1st class types *) assert (!backend <> HOL4); - let use_brackets = generics <> empty_generic_args in - if use_brackets then F.pp_print_string fmt "("; extract_trait_ref ctx fmt no_params_tys false trait_ref; - extract_generic_args ctx fmt no_params_tys generics; - if use_brackets then F.pp_print_string fmt ")"; F.pp_print_string fmt ("." ^ add_brackets type_name)) and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 8536b4ab..dc100fe3 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -263,8 +263,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) match cv.value with | CLiteral lit -> cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx - | CTraitConst (trait_ref, generics, const_name) -> ( - assert (generics = empty_generic_args); + | CTraitConst (trait_ref, const_name) -> ( match trait_ref.trait_id with | TraitImpl _ -> (* This shouldn't happen: if we refer to a concrete implementation, we @@ -294,8 +293,7 @@ let eval_operand_no_reorganize (config : config) (op : operand) ( ctx0, None, value_as_symbolic v.value, - SymbolicAst.VaTraitConstValue - (trait_ref, generics, const_name), + SymbolicAst.VaTraitConstValue (trait_ref, const_name), e )))) | CVar vid -> ( let ctx0 = ctx in diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 0cf8b88a..eef9e2c9 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -769,12 +769,8 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) ("trait method call:\n- call: " ^ call_to_string ctx call ^ "\n- method name: " ^ method_name ^ "\n- call.generics:\n" ^ generic_args_to_string ctx func.generics - ^ "\n- trait and method generics:\n" - ^ generic_args_to_string ctx - (Option.get func.trait_and_method_generic_args))); - (* When instantiating, we need to group the generics for the trait ref - and the method *) - let generics = Option.get func.trait_and_method_generic_args in + ^ "\n- trait_ref.trait_decl_ref: " + ^ trait_decl_ref_to_string ctx trait_ref.trait_decl_ref)); (* Lookup the trait method signature - there are several possibilities depending on whethere we call a top-level trait method impl or the method from a local clause *) @@ -794,6 +790,11 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) | Some (_, id) -> (* This is a required method *) let method_def = ctx_lookup_fun_decl ctx id in + (* We have to concatenate the generics for the impl + and the generics for the method *) + let generics = + merge_generic_args trait_ref.generics func.generics + in (* Instantiate *) let tr_self = TraitRef trait_ref in let fid : fun_id = FRegular id in @@ -898,6 +899,12 @@ let eval_transparent_function_call_symbolic_inst (call : call) (ctx : eval_ctx) log#ldebug (lazy ("method:\n" ^ fun_decl_to_string ctx method_def)); (* Instantiate *) + (* When instantiating, we need to group the generics for the + trait ref and the generics for the method *) + let generics = + TypesUtils.merge_generic_args + trait_ref.trait_decl_ref.decl_generics func.generics + in let regions_hierarchy = LlbcAstUtils.FunIdMap.find (FRegular method_id) ctx.fun_ctx.regions_hierarchies @@ -1025,7 +1032,6 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) : { func = FunId (FRegular global.body); generics = TypesUtils.empty_generic_args; - trait_and_method_generic_args = None; } in let call = { func = FnOpRegular func; args = []; dest } in diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 667c5080..243cf67b 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -43,6 +43,8 @@ let fun_sig_to_string = Print.EvalCtx.fun_sig_to_string let inst_fun_sig_to_string = Print.EvalCtx.inst_fun_sig_to_string let ty_to_string = Print.EvalCtx.ty_to_string let generic_args_to_string = Print.EvalCtx.generic_args_to_string +let trait_ref_to_string = Print.EvalCtx.trait_ref_to_string +let trait_decl_ref_to_string = Print.EvalCtx.trait_decl_ref_to_string let fun_id_or_trait_method_ref_to_string = Print.EvalCtx.fun_id_or_trait_method_ref_to_string diff --git a/compiler/Print.ml b/compiler/Print.ml index 0c69bd05..36aa2cb9 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -531,6 +531,10 @@ module EvalCtx = struct let env = eval_ctx_to_fmt_env ctx in trait_ref_to_string env x + let trait_decl_ref_to_string (ctx : eval_ctx) (x : trait_decl_ref) : string = + let env = eval_ctx_to_fmt_env ctx in + trait_decl_ref_to_string env x + let trait_instance_id_to_string (ctx : eval_ctx) (x : trait_instance_id) : string = let env = eval_ctx_to_fmt_env ctx in diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 21ca7f08..a401594d 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -159,14 +159,9 @@ let rec ty_to_string (env : fmt_env) (inside : bool) (ty : ty) : string = ty_to_string env true arg_ty ^ " -> " ^ ty_to_string env false ret_ty in if inside then "(" ^ ty ^ ")" else ty - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = trait_ref_to_string env false trait_ref in - let s = - if generics = empty_generic_args then trait_ref ^ "::" ^ type_name - else - let generics = generic_args_to_string env generics in - "(" ^ trait_ref ^ " " ^ generics ^ ")::" ^ type_name - in + let s = trait_ref ^ "::" ^ type_name in if inside then "(" ^ s ^ ")" else s and generic_args_to_strings (env : fmt_env) (inside : bool) @@ -624,14 +619,9 @@ and app_to_string (env : fmt_env) (inside : bool) (indent : string) let field_s = adt_field_to_string env adt_id field_id in (* Adopting an F*-like syntax *) (ConstStrings.constructor_prefix ^ adt_s ^ "?." ^ field_s, []) - | TraitConst (trait_ref, generics, const_name) -> + | TraitConst (trait_ref, const_name) -> let trait_ref = trait_ref_to_string env true trait_ref in - let generics_s = generic_args_to_string env generics in - let qualif = - if generics <> empty_generic_args then - "(" ^ trait_ref ^ generics_s ^ ")." ^ const_name - else trait_ref ^ "." ^ const_name - in + let qualif = trait_ref ^ "." ^ const_name in (qualif, [])) | _ -> (* "Regular" expression case *) diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 33c23cc3..a735667e 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -283,7 +283,7 @@ type ty = | TVar of type_var_id | TLiteral of literal_type | TArrow of ty * ty - | TTraitType of trait_ref * generic_args * string + | TTraitType of trait_ref * string (** The string is for the name of the associated type *) and trait_ref = { @@ -374,7 +374,6 @@ type generic_params = { type trait_type_constraint = { trait_ref : trait_ref; - generics : generic_args; type_name : trait_item_name; ty : ty; } @@ -599,8 +598,7 @@ type qualif_id = | Global of global_decl_id | AdtCons of adt_cons_id (** A function or ADT constructor identifier *) | Proj of projection (** Field projector *) - | TraitConst of trait_ref * generic_args * string - (** A trait associated constant *) + | TraitConst of trait_ref * string (** A trait associated constant *) [@@deriving show] (** An instantiated qualifier. diff --git a/compiler/RegionsHierarchy.ml b/compiler/RegionsHierarchy.ml index 80b67a54..0b589453 100644 --- a/compiler/RegionsHierarchy.ml +++ b/compiler/RegionsHierarchy.ml @@ -169,7 +169,7 @@ let compute_regions_hierarchy_for_sig (type_decls : type_decl TypeDeclId.Map.t) (* Continue *) explore_ty outer ty | TRawPtr (ty, _) -> explore_ty outer ty - | TTraitType (trait_ref, _generic_args, _) -> + | TTraitType (trait_ref, _) -> (* The trait should reference a clause, and not an implementation (otherwise it should have been normalized) *) assert ( diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 7252a020..79c03e58 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -251,8 +251,7 @@ and value_aggregate = | VaCgValue of const_generic_var_id (** This is used when evaluating a const generic value: in the interpreter, we introduce a fresh symbolic value. *) - | VaTraitConstValue of trait_ref * generic_args * string - (** A trait constant value *) + | VaTraitConstValue of trait_ref * string (** A trait constant value *) [@@deriving show, visitors diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 922f0375..27279327 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -474,10 +474,9 @@ let rec translate_sty (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_sgeneric_args (generics : T.generic_args) : generic_args = @@ -497,11 +496,10 @@ let translate_trait_clause (clause : T.trait_clause) : trait_clause = let translate_strait_type_constraint (ttc : T.trait_type_constraint) : trait_type_constraint = - let { T.trait_ref; generics; type_name; ty } = ttc in + let { T.trait_ref; type_name; ty } = ttc in let trait_ref = translate_strait_ref trait_ref in - let generics = translate_sgeneric_args generics in let ty = translate_sty ty in - { trait_ref; generics; type_name; ty } + { trait_ref; type_name; ty } let translate_predicates (preds : T.predicates) : predicates = let trait_type_constraints = @@ -638,10 +636,9 @@ let rec translate_fwd_ty (type_infos : type_infos) (ty : T.ty) : ty = let ty = translate ty in let generics = { types = [ ty ]; const_generics = []; trait_refs = [] } in TAdt (TAssumed (TRawPtr mut), generics) - | TTraitType (trait_ref, generics, type_name) -> + | TTraitType (trait_ref, type_name) -> let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - TTraitType (trait_ref, generics, type_name) + TTraitType (trait_ref, type_name) | TArrow _ -> raise (Failure "TODO") and translate_fwd_generic_args (type_infos : type_infos) @@ -737,16 +734,14 @@ let rec translate_back_ty (type_infos : type_infos) | TRawPtr _ -> (* TODO: not sure what to do here *) None - | TTraitType (trait_ref, generics, type_name) -> - assert (generics.regions = []); + | TTraitType (trait_ref, type_name) -> assert ( AssociatedTypes.trait_instance_id_is_local_clause trait_ref.trait_id); if inside_mut then - (* Translate the trait ref and the generics as "forward" generics - + (* Translate the trait ref as a "forward" trait ref - we do not want to filter any type *) let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - Some (TTraitType (trait_ref, generics, type_name)) + Some (TTraitType (trait_ref, type_name)) else None | TArrow _ -> raise (Failure "TODO") @@ -2956,11 +2951,10 @@ and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) in { e = StructUpdate su; ty = var.ty } | VaCgValue cg_id -> { e = CVar cg_id; ty = var.ty } - | VaTraitConstValue (trait_ref, generics, const_name) -> + | VaTraitConstValue (trait_ref, const_name) -> let type_infos = ctx.type_ctx.type_infos in let trait_ref = translate_fwd_trait_ref type_infos trait_ref in - let generics = translate_fwd_generic_args type_infos generics in - let qualif_id = TraitConst (trait_ref, generics, const_name) in + let qualif_id = TraitConst (trait_ref, const_name) in let qualif = { id = qualif_id; generics = empty_generic_args } in { e = Qualif qualif; ty = var.ty } in diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 48a3685b..fba1dfb0 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -1086,7 +1086,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) : let exe_dir = Filename.dirname Sys.argv.(0) in let primitives_src_dest = match !Config.backend with - | FStar -> Some ("/backends/fstar/merge/Primitives.fst", "Primitives.fst") + | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst") | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") | Lean -> None | HOL4 -> None diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml index 28db59ec..f5dd7df4 100644 --- a/compiler/TypesUtils.ml +++ b/compiler/TypesUtils.ml @@ -105,9 +105,8 @@ let generic_args_no_regions (x : generic_args) : bool = (** Return [true] if the trait type constraint doesn't contain regions (including erased regions) *) let trait_type_constraint_no_regions (x : trait_type_constraint) : bool = try - let { trait_ref; generics; type_name = _; ty } = x in + let { trait_ref; type_name = _; ty } = x in raise_if_region_ty_visitor#visit_trait_ref () trait_ref; - raise_if_region_ty_visitor#visit_generic_args () generics; raise_if_region_ty_visitor#visit_ty () ty; true with Found -> false @@ -8,11 +8,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1710149523, - "narHash": "sha256-y6ZZvC7y+uIdorsdBEKJG0u02CLsWFf1CTkE8DNWn2o=", + "lastModified": 1710648057, + "narHash": "sha256-Jm5EZsXXIhAhDHAA1jZx4TYPpKREGZBNAUeqpiufbPo=", "owner": "aeneasverif", "repo": "charon", - "rev": "879469900b4baadb85835c5e7da47e6506f6642c", + "rev": "a3ba8b5286ef99584e87035cb965d3cb9c43660c", "type": "github" }, "original": { @@ -131,11 +131,11 @@ "nixpkgs": "nixpkgs_2" }, "locked": { - "lastModified": 1708956704, - "narHash": "sha256-xT0V7oQwR0Zns9g/MvV30ILlAX6tcp92SqWPwej1+sI=", + "lastModified": 1710514291, + "narHash": "sha256-eO3XmWazqfmSm91sQDk0HJNyLpsU5W6BgeftXoJSUl0=", "owner": "fstarlang", "repo": "fstar", - "rev": "a48722f90e14be69b850f093b41fbbdfee7f6eb9", + "rev": "704382c882f3b5b95f7987d3464f97020195319b", "type": "github" }, "original": { @@ -164,11 +164,11 @@ ] }, "locked": { - "lastModified": 1709029146, - "narHash": "sha256-xKqBQ1OdLnyng4Kl3XRU//borVLLet+h15mPQ5g0BEI=", + "lastModified": 1710421079, + "narHash": "sha256-iXmFy2/JmS3khP4V3zIg1P4SROq0sPPuqOxRidJbfqQ=", "owner": "hacl-star", "repo": "hacl-star", - "rev": "59723f7dde13bd7b7eb90491f1385b4e3ee2904f", + "rev": "e5620ceb7c8a4996520d693f597872806dc0a1d3", "type": "github" }, "original": { @@ -194,11 +194,11 @@ ] }, "locked": { - "lastModified": 1709552015, - "narHash": "sha256-zwYbXYRAqKee+OtlWaSX3EhUyD5JLN+xxzcqYxyDnSI=", + "lastModified": 1710638129, + "narHash": "sha256-/SkIjiIg0MROfmYyA8XfWljRC4ehxDuZpE3tDQ07yYc=", "owner": "hacl-star", "repo": "hacl-nix", - "rev": "96a3c4eaaa65beb0ac9e57fc9aa3e9e34aca12f5", + "rev": "cc8c396d454e89c04012cf3b16eb6f64eb455bd6", "type": "github" }, "original": { @@ -223,11 +223,11 @@ ] }, "locked": { - "lastModified": 1709551385, - "narHash": "sha256-aryyJy49PlkZeIMO8Jg0qAUCjtre0r+rvmbH6OhH/sk=", + "lastModified": 1710613474, + "narHash": "sha256-C1y575wlUVaI3AlTMZvMYpie6mSLUmiQDXasaHqKo6o=", "owner": "fstarlang", "repo": "karamel", - "rev": "a1e1b1f2493ac24f8729f17ebedba7c4571f7c97", + "rev": "95968326f0ca1d6f9056347496482d285e6a9f1e", "type": "github" }, "original": { @@ -265,11 +265,11 @@ "nixpkgs": "nixpkgs_4" }, "locked": { - "lastModified": 1710111430, - "narHash": "sha256-TsVeepxSag4OMVWH2UxntI0HHF2Db7hYUpAwhM8XjUQ=", + "lastModified": 1710638987, + "narHash": "sha256-88u7WVtuwQwd4yjUXUJouMBd2W6meLg0C2k9Kv8PuYM=", "owner": "leanprover", "repo": "lean4", - "rev": "32dcc6eb895b58df3d3241a2521963e64995b621", + "rev": "9ee10aa3ebb8e518132873e3d98a13dd7df5e9f7", "type": "github" }, "original": { @@ -318,11 +318,11 @@ "nixpkgs": "nixpkgs_7" }, "locked": { - "lastModified": 1710111430, - "narHash": "sha256-TsVeepxSag4OMVWH2UxntI0HHF2Db7hYUpAwhM8XjUQ=", + "lastModified": 1710638987, + "narHash": "sha256-88u7WVtuwQwd4yjUXUJouMBd2W6meLg0C2k9Kv8PuYM=", "owner": "leanprover", "repo": "lean4", - "rev": "32dcc6eb895b58df3d3241a2521963e64995b621", + "rev": "9ee10aa3ebb8e518132873e3d98a13dd7df5e9f7", "type": "github" }, "original": { |