summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/lean/Base/Primitives/Base.lean4
-rw-r--r--compiler/AssociatedTypes.ml25
-rw-r--r--compiler/Extract.ml137
-rw-r--r--compiler/ExtractBase.ml2
-rw-r--r--compiler/ExtractTypes.ml7
-rw-r--r--compiler/InterpreterExpressions.ml53
-rw-r--r--compiler/InterpreterStatements.ml52
-rw-r--r--compiler/InterpreterUtils.ml2
-rw-r--r--compiler/Print.ml4
-rw-r--r--compiler/PrintPure.ml18
-rw-r--r--compiler/Pure.ml26
-rw-r--r--compiler/PureTypeCheck.ml4
-rw-r--r--compiler/RegionsHierarchy.ml2
-rw-r--r--compiler/SymbolicAst.ml5
-rw-r--r--compiler/SymbolicToPure.ml75
-rw-r--r--compiler/SynthesizeSymbolic.ml6
-rw-r--r--compiler/Translate.ml3
-rw-r--r--compiler/TypesUtils.ml3
-rw-r--r--flake.lock374
-rw-r--r--flake.nix21
-rw-r--r--tests/coq/misc/Constants.v17
-rw-r--r--tests/coq/traits/Traits.v100
-rw-r--r--tests/fstar/misc/Constants.fst14
-rw-r--r--tests/fstar/traits/Traits.fst77
-rw-r--r--tests/lean/Constants.lean15
-rw-r--r--tests/lean/Traits.lean78
26 files changed, 571 insertions, 553 deletions
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 0b9d9c39..0c64eca1 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -69,7 +69,9 @@ def div? {α: Type u} (r: Result α): Bool :=
def massert (b:Bool) : Result Unit :=
if b then ret () else fail assertionFailure
-def eval_global {α: Type u} (x: Result α) (_: ret? x := by decide): α :=
+macro "prove_eval_global" : tactic => `(tactic| first | apply Eq.refl | decide)
+
+def eval_global {α: Type u} (x: Result α) (_: ret? x := by prove_eval_global) : α :=
match x with
| fail _ | div => by contradiction
| ret x => x
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..aa097a4f 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -185,9 +185,17 @@ let extract_adt_g_value
| _ -> raise (Failure "Inconsistent typed value")
(* Extract globals in the same way as variables *)
-let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
- (id : A.GlobalDeclId.id) : unit =
- F.pp_print_string fmt (ctx_get_global id ctx)
+let extract_global (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
+ (id : A.GlobalDeclId.id) (generics : generic_args) : unit =
+ let use_brackets = inside && generics <> empty_generic_args in
+ F.pp_open_hvbox fmt ctx.indent_incr;
+ if use_brackets then F.pp_print_string fmt "(";
+ (* Extract the global name *)
+ F.pp_print_string fmt (ctx_get_global id ctx);
+ (* Extract the generics *)
+ extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
+ if use_brackets then F.pp_print_string fmt ")";
+ F.pp_close_box fmt ()
(* Filter the generics of a function if it is builtin *)
let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
@@ -321,16 +329,15 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
match qualif.id with
| FunOrOp fun_id ->
extract_function_call ctx fmt inside fun_id qualif.generics args
- | Global global_id -> extract_global ctx fmt global_id
+ | Global global_id ->
+ assert (args = []);
+ extract_global ctx fmt inside global_id qualif.generics
| AdtCons adt_cons_id ->
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 "(";
- extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref;
- extract_generic_args ctx fmt TypeDeclId.Set.empty generics;
+ | TraitConst (trait_ref, const_name) ->
+ extract_trait_ref ctx fmt TypeDeclId.Set.empty true trait_ref;
let name =
ctx_get_trait_const trait_ref.trait_decl_ref.trait_decl_id
const_name ctx
@@ -338,7 +345,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 *)
@@ -1695,7 +1701,9 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
of those declarations. See {!extract_global_decl} for more explanations.
*)
let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
- (kind : decl_kind) (name : string) (ty : ty)
+ (kind : decl_kind) (name : string) (generics : generic_params)
+ (type_params : string list) (cg_params : string list)
+ (trait_clauses : string list) (ty : ty)
(extract_body : (F.formatter -> unit) Option.t) : unit =
let is_opaque = Option.is_none extract_body in
@@ -1712,9 +1720,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_open_hvbox fmt 0;
F.pp_open_hvbox fmt ctx.indent_incr;
- (* Open "QUALIF NAME : TYPE =" box (depth=1) *)
+ (* Open "QUALIF NAME PARAMS : TYPE =" box (depth=1) *)
F.pp_open_hovbox fmt ctx.indent_incr;
- (* Print "QUALIF NAME " *)
+ (* Print "QUALIF NAME PARAMS " *)
(match fun_decl_kind_to_qualif kind with
| Some qualif ->
F.pp_print_string fmt qualif;
@@ -1723,6 +1731,12 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt name;
F.pp_print_space fmt ();
+ (* Extract the generic parameters *)
+ let space = ref true in
+ extract_generic_params ctx fmt TypeDeclId.Set.empty ~space:(Some space)
+ generics type_params cg_params trait_clauses;
+ if not !space then F.pp_print_space fmt ();
+
(* Open ": TYPE =" box (depth=2) *)
F.pp_open_hvbox fmt 0;
(* Print ": " *)
@@ -1779,7 +1793,9 @@ let extract_global_decl_body_gen (ctx : extraction_ctx) (fmt : F.formatter)
but I could not find a better way.
*)
let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
- (name : string) (ty : ty) : unit =
+ (name : string) (generics : generic_params) (ty : ty) : unit =
+ (* TODO: non-empty generics *)
+ assert (generics = empty_generic_params);
(* Open the definition boxe (depth=0) *)
F.pp_open_hvbox fmt ctx.indent_incr;
(* [val ..._def = new_constant ("...",] *)
@@ -1819,58 +1835,94 @@ let extract_global_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
and {!extract_fun_decl}.
*)
let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
- (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
+ (global : global_decl) (body : fun_decl) (interface : bool) : unit =
assert body.is_global_decl_body;
assert (body.signature.inputs = []);
- assert (body.signature.generics = empty_generic_params);
(* Add a break then the name of the corresponding LLBC declaration *)
F.pp_print_break fmt 0 0;
let name =
if !Config.extract_external_name_patterns && not global.is_local then
- Some global.name
+ Some global.llbc_name
else None
in
extract_comment_with_span ctx fmt
- [ "[" ^ name_to_string ctx global.name ^ "]" ]
+ [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
name global.meta.span;
F.pp_print_space fmt ();
let decl_name = ctx_get_global global.def_id ctx in
let body_name =
- ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body), None)) ctx
+ ctx_get_function (FromLlbc (Pure.FunId (FRegular global.body_id), None)) ctx
in
-
let decl_ty, body_ty =
let ty = body.signature.output in
if body.signature.fwd_info.effect_info.can_fail then
(unwrap_result_ty ty, ty)
else (ty, mk_result_ty ty)
in
+ (* Add the type parameters *)
+ let ctx, type_params, cg_params, trait_clauses =
+ ctx_add_generic_params global.llbc_name global.llbc_generics global.generics
+ ctx
+ in
match body.body with
| None ->
(* No body: only generate a [val x_c : u32] declaration *)
let kind = if interface then Declared else Assumed in
if !backend = HOL4 then
- extract_global_decl_hol4_opaque ctx fmt decl_name decl_ty
- else extract_global_decl_body_gen ctx fmt kind decl_name decl_ty None
+ extract_global_decl_hol4_opaque ctx fmt decl_name global.generics
+ decl_ty
+ else
+ extract_global_decl_body_gen ctx fmt kind decl_name global.generics
+ type_params cg_params trait_clauses decl_ty None
| Some body ->
(* There is a body *)
(* Generate: [let x_body : result u32 = Return 3] *)
- extract_global_decl_body_gen ctx fmt SingleNonRec body_name body_ty
+ extract_global_decl_body_gen ctx fmt SingleNonRec body_name
+ global.generics type_params cg_params trait_clauses body_ty
(Some (fun fmt -> extract_texpression ctx fmt false body.body));
F.pp_print_break fmt 0 0;
(* Generate: [let x_c : u32 = eval_global x_body] *)
- extract_global_decl_body_gen ctx fmt SingleNonRec decl_name decl_ty
+ extract_global_decl_body_gen ctx fmt SingleNonRec decl_name
+ global.generics type_params cg_params trait_clauses decl_ty
(Some
(fun fmt ->
- let body =
+ let all_params =
+ List.concat [ type_params; cg_params; trait_clauses ]
+ in
+ let extract_params () =
+ List.iter
+ (fun p ->
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt p)
+ all_params
+ in
+ let use_brackets = all_params <> [] in
+ (* Extract the name *)
+ let before, after =
match !backend with
- | FStar | Lean -> "eval_global " ^ body_name
- | Coq -> body_name ^ "%global"
- | HOL4 -> "get_return_value " ^ body_name
+ | FStar | Lean ->
+ ( (fun () ->
+ F.pp_print_string fmt "eval_global";
+ F.pp_print_space fmt ()),
+ fun () -> () )
+ | Coq ->
+ ((fun () -> ()), fun () -> F.pp_print_string fmt "%global")
+ | HOL4 ->
+ ( (fun () ->
+ F.pp_print_string fmt "get_return_value";
+ F.pp_print_space fmt ()),
+ fun () -> () )
in
- F.pp_print_string fmt body));
+ before ();
+ if use_brackets then F.pp_print_string fmt "(";
+ F.pp_print_string fmt body_name;
+ (* Extract the generic params *)
+ extract_params ();
+ if use_brackets then F.pp_print_string fmt ")";
+ (* *)
+ after ()));
(* Add a break to insert lines between declarations *)
F.pp_print_break fmt 0 0
@@ -2589,18 +2641,39 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
* Extract the items
*)
let trait_decl_id = impl.impl_trait.trait_decl_id in
+ let trait_decl = TraitDeclId.Map.find trait_decl_id ctx.trans_trait_decls in
+ let trait_decl_provided_consts =
+ List.map (fun (_, (_, x)) -> x) trait_decl.consts
+ in
(* The constants *)
List.iter
- (fun (name, (_, id)) ->
+ (fun (provided_id, (name, (_, id))) ->
let item_name = ctx_get_trait_const trait_decl_id name ctx in
+ (* The parameters are not the same depending on whether the constant
+ is a provided constant or not *)
+ let print_params () =
+ if provided_id = Some id then
+ extract_generic_args ctx fmt TypeDeclId.Set.empty
+ impl.impl_trait.decl_generics
+ else
+ let all_params =
+ List.concat [ type_params; cg_params; trait_clauses ]
+ in
+ List.iter
+ (fun p ->
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt p)
+ all_params
+ in
let ty () =
F.pp_print_space fmt ();
- F.pp_print_string fmt (ctx_get_global id ctx)
+ F.pp_print_string fmt (ctx_get_global id ctx);
+ print_params ()
in
extract_trait_impl_item ctx fmt item_name ty)
- impl.consts;
+ (List.combine trait_decl_provided_consts impl.consts);
(* The types *)
List.iter
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..afbf4605 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -1,6 +1,5 @@
open Types
open Values
-open LlbcAst
open Scalars
open Expressions
open Utils
@@ -263,40 +262,24 @@ 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);
- match trait_ref.trait_id with
- | TraitImpl _ ->
- (* This shouldn't happen: if we refer to a concrete implementation, we
- should directly refer to the top-level constant *)
- raise (Failure "Unreachable")
- | _ -> (
- (* We refer to a constant defined in a local clause: simply
- introduce a fresh symbolic value *)
- let ctx0 = ctx in
- (* Lookup the trait declaration to retrieve the type of the symbolic value *)
- let trait_decl =
- ctx_lookup_trait_decl ctx trait_ref.trait_decl_ref.trait_decl_id
- in
- let _, (ty, _) =
- List.find (fun (name, _) -> name = const_name) trait_decl.consts
- in
- (* Introduce a fresh symbolic value *)
- let v = mk_fresh_symbolic_typed_value ty in
- (* Continue the evaluation *)
- let e = cf v ctx in
- (* We have to wrap the generated expression *)
- match e with
- | None -> None
- | Some e ->
- Some
- (SymbolicAst.IntroSymbolic
- ( ctx0,
- None,
- value_as_symbolic v.value,
- SymbolicAst.VaTraitConstValue
- (trait_ref, generics, const_name),
- e ))))
+ | CTraitConst (trait_ref, const_name) -> (
+ let ctx0 = ctx in
+ (* Simply introduce a fresh symbolic value *)
+ let ty = cv.ty in
+ let v = mk_fresh_symbolic_typed_value ty in
+ (* Continue the evaluation *)
+ let e = cf v ctx in
+ (* Wrap the generated expression *)
+ match e with
+ | None -> None
+ | Some e ->
+ Some
+ (SymbolicAst.IntroSymbolic
+ ( ctx0,
+ None,
+ value_as_symbolic v.value,
+ SymbolicAst.VaTraitConstValue (trait_ref, const_name),
+ e )))
| CVar vid -> (
let ctx0 = ctx in
(* In concrete mode: lookup the const generic value.
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 0cf8b88a..95a2956b 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
@@ -942,9 +949,9 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
| Assign (p, rvalue) -> (
(* We handle global assignments separately *)
match rvalue with
- | Global gid ->
+ | Global (gid, generics) ->
(* Evaluate the global *)
- eval_global config p gid cf ctx
+ eval_global config p gid generics cf ctx
| _ ->
(* Evaluate the rvalue *)
let cf_eval_rvalue = eval_rvalue_not_global config rvalue in
@@ -1014,32 +1021,37 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
(* Compose and apply *)
comp cc cf_eval_st cf ctx
-and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) :
- st_cm_fun =
+and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id)
+ (generics : generic_args) : st_cm_fun =
fun cf ctx ->
let global = ctx_lookup_global_decl ctx gid in
match config.mode with
| ConcreteMode ->
- (* Treat the evaluation of the global as a call to the global body (without arguments) *)
- let func =
- {
- func = FunId (FRegular global.body);
- generics = TypesUtils.empty_generic_args;
- trait_and_method_generic_args = None;
- }
- in
+ (* Treat the evaluation of the global as a call to the global body *)
+ let func = { func = FunId (FRegular global.body); generics } in
let call = { func = FnOpRegular func; args = []; dest } in
(eval_transparent_function_call_concrete config global.body call) cf ctx
| SymbolicMode ->
(* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
* defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
assert (ty_no_regions global.ty);
- let sval = mk_fresh_symbolic_value global.ty in
+ (* Instantiate the type *)
+ (* There shouldn't be any reference to Self *)
+ let tr_self : trait_instance_id = UnknownTrait __FUNCTION__ in
+ let generics = Subst.generic_args_erase_regions generics in
+ let { Subst.r_subst = _; ty_subst; cg_subst; tr_subst; tr_self } =
+ Subst.make_subst_from_generics global.generics generics tr_self
+ in
+ let ty =
+ Subst.erase_regions_substitute_types ty_subst cg_subst tr_subst tr_self
+ global.ty
+ in
+ let sval = mk_fresh_symbolic_value ty in
let cc =
assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
in
let e = cc (cf Unit) ctx in
- S.synthesize_global_eval gid sval e
+ S.synthesize_global_eval gid generics sval e
(** Evaluate a switch *)
and eval_switch (config : config) (switch : switch) : st_cm_fun =
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..cf6710aa 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.
@@ -1089,6 +1087,26 @@ type fun_decl = {
}
[@@deriving show]
+type global_decl = {
+ meta : meta;
+ def_id : GlobalDeclId.id;
+ is_local : bool;
+ llbc_name : llbc_name; (** The original LLBC name. *)
+ name : string;
+ (** We use the name only for printing purposes (for debugging):
+ the name used at extraction time will be derived from the
+ llbc_name.
+ *)
+ llbc_generics : Types.generic_params;
+ (** See the comment for [llbc_generics] in fun_decl. *)
+ generics : generic_params;
+ preds : predicates;
+ ty : ty;
+ kind : item_kind;
+ body_id : FunDeclId.id;
+}
+[@@deriving show]
+
type trait_decl = {
def_id : trait_decl_id;
is_local : bool;
diff --git a/compiler/PureTypeCheck.ml b/compiler/PureTypeCheck.ml
index a989fd3b..fc94fa4c 100644
--- a/compiler/PureTypeCheck.ml
+++ b/compiler/PureTypeCheck.ml
@@ -208,7 +208,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
get_adt_field_types ctx.type_decls adt_id variant_id adt_generics
in
List.iter
- (fun (fid, fe) ->
+ (fun ((fid, fe) : _ * texpression) ->
let expected_field_ty = FieldId.nth expected_field_tys fid in
assert (expected_field_ty = fe.ty);
check_texpression ctx fe)
@@ -218,7 +218,7 @@ let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit =
Collections.List.to_cons_nil adt_generics.types
in
List.iter
- (fun (_, fe) ->
+ (fun ((_, fe) : _ * texpression) ->
assert (expected_field_ty = fe.ty);
check_texpression ctx fe)
supd.updates
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..cc74a16b 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -141,7 +141,7 @@ type expression =
The context is the evaluation context from after evaluating the asserted
value. It has the same purpose as for the {!Return} case.
*)
- | EvalGlobal of global_decl_id * symbolic_value * expression
+ | EvalGlobal of global_decl_id * generic_args * symbolic_value * expression
(** Evaluate a global to a fresh symbolic value *)
| Assertion of Contexts.eval_ctx * typed_value * expression
(** An assertion.
@@ -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..58fb6d04 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")
@@ -1895,7 +1890,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
| Panic -> translate_panic ctx
| FunCall (call, e) -> translate_function_call call e ctx
| EndAbstraction (ectx, abs, e) -> translate_end_abstraction ectx abs e ctx
- | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx
+ | EvalGlobal (gid, generics, sv, e) ->
+ translate_global_eval gid generics sv e ctx
| Assertion (ectx, v, e) -> translate_assertion ectx v e ctx
| Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
| IntroSymbolic (ectx, p, sv, v, e) ->
@@ -2667,11 +2663,12 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
(* Create the let-binding *)
mk_let effect_info.can_fail output call next_e)
-and translate_global_eval (gid : A.GlobalDeclId.id) (sval : V.symbolic_value)
- (e : S.expression) (ctx : bs_ctx) : texpression =
+and translate_global_eval (gid : A.GlobalDeclId.id) (generics : T.generic_args)
+ (sval : V.symbolic_value) (e : S.expression) (ctx : bs_ctx) : texpression =
let ctx, var = fresh_var_for_symbolic_value sval ctx in
let decl = A.GlobalDeclId.Map.find gid ctx.global_ctx.llbc_global_decls in
- let global_expr = { id = Global gid; generics = empty_generic_args } in
+ let generics = ctx_translate_fwd_generic_args ctx generics in
+ let global_expr = { id = Global gid; generics } in
(* We use translate_fwd_ty to translate the global type *)
let ty = ctx_translate_fwd_ty ctx decl.ty in
let gval = { e = Qualif global_expr; ty } in
@@ -2956,11 +2953,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
@@ -3844,3 +3840,40 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
required_methods;
provided_methods;
}
+
+let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
+ global_decl =
+ let {
+ A.meta;
+ def_id;
+ is_local;
+ name = llbc_name;
+ generics = llbc_generics;
+ preds;
+ ty;
+ kind;
+ body = body_id;
+ } =
+ decl
+ in
+ let name =
+ Print.Types.name_to_string
+ (Print.Contexts.decls_ctx_to_fmt_env ctx)
+ llbc_name
+ in
+ let generics = translate_generic_params llbc_generics in
+ let preds = translate_predicates preds in
+ let ty = translate_fwd_ty ctx.type_ctx.type_infos ty in
+ {
+ meta;
+ def_id;
+ is_local;
+ llbc_name;
+ name;
+ llbc_generics;
+ generics;
+ preds;
+ ty;
+ kind;
+ body_id;
+ }
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 20bc107e..a42c43ac 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -119,9 +119,9 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
FunCall (call, e))
e
-let synthesize_global_eval (gid : GlobalDeclId.id) (dest : symbolic_value)
- (e : expression option) : expression option =
- Option.map (fun e -> EvalGlobal (gid, dest, e)) e
+let synthesize_global_eval (gid : GlobalDeclId.id) (generics : generic_args)
+ (dest : symbolic_value) (e : expression option) : expression option =
+ Option.map (fun e -> EvalGlobal (gid, generics, dest, e)) e
let synthesize_regular_function_call (fun_id : fun_id_or_trait_method_ref)
(call_id : FunCallId.id) (ctx : Contexts.eval_ctx) (sg : fun_sig)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 48a3685b..9af3c71b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -469,6 +469,7 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
groups are always singletons, so the [extract_global_decl] function
takes care of generating the delimiters.
*)
+ let global = SymbolicToPure.translate_global ctx.trans_ctx global in
Extract.extract_global_decl ctx fmt global body config.interface
(** Utility.
@@ -1086,7 +1087,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
diff --git a/flake.lock b/flake.lock
index db195035..9bbf68bc 100644
--- a/flake.lock
+++ b/flake.lock
@@ -8,11 +8,11 @@
"rust-overlay": "rust-overlay"
},
"locked": {
- "lastModified": 1710149523,
- "narHash": "sha256-y6ZZvC7y+uIdorsdBEKJG0u02CLsWFf1CTkE8DNWn2o=",
+ "lastModified": 1710741599,
+ "narHash": "sha256-/5o81Ifs6OGqNpxMklGCJ6w2CVQrQn+xMaC1VrC8pZE=",
"owner": "aeneasverif",
"repo": "charon",
- "rev": "879469900b4baadb85835c5e7da47e6506f6642c",
+ "rev": "f3faf02ec1dbd6645b816d54be39261dea6970c2",
"type": "github"
},
"original": {
@@ -77,65 +77,17 @@
"type": "indirect"
}
},
- "flake-utils_3": {
- "inputs": {
- "systems": "systems_3"
- },
- "locked": {
- "lastModified": 1710146030,
- "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
- "owner": "numtide",
- "repo": "flake-utils",
- "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
- "type": "github"
- },
- "original": {
- "owner": "numtide",
- "repo": "flake-utils",
- "type": "github"
- }
- },
- "flake-utils_4": {
- "locked": {
- "lastModified": 1656928814,
- "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
- "owner": "numtide",
- "repo": "flake-utils",
- "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
- "type": "github"
- },
- "original": {
- "owner": "numtide",
- "repo": "flake-utils",
- "type": "github"
- }
- },
- "flake-utils_5": {
- "locked": {
- "lastModified": 1656928814,
- "narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
- "owner": "numtide",
- "repo": "flake-utils",
- "rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
- "type": "github"
- },
- "original": {
- "owner": "numtide",
- "repo": "flake-utils",
- "type": "github"
- }
- },
"fstar": {
"inputs": {
"flake-utils": "flake-utils_2",
"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 +116,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 +146,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 +175,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": {
@@ -236,173 +188,6 @@
"type": "github"
}
},
- "lake": {
- "inputs": {
- "flake-utils": "flake-utils_3",
- "lean": "lean",
- "nixpkgs": "nixpkgs_5"
- },
- "locked": {
- "lastModified": 1689377246,
- "narHash": "sha256-UP5Vu5RFPqoRa2tpHaQ7JoX5IY/7BTA9b+MF418oszY=",
- "owner": "leanprover",
- "repo": "lake",
- "rev": "9919b5efc48c71a940635a0bbab00a394ebe53f8",
- "type": "github"
- },
- "original": {
- "owner": "leanprover",
- "ref": "lean4-master",
- "repo": "lake",
- "type": "github"
- }
- },
- "lean": {
- "inputs": {
- "flake-utils": "flake-utils_4",
- "lean4-mode": "lean4-mode",
- "nix": "nix",
- "nixpkgs": "nixpkgs_4"
- },
- "locked": {
- "lastModified": 1710111430,
- "narHash": "sha256-TsVeepxSag4OMVWH2UxntI0HHF2Db7hYUpAwhM8XjUQ=",
- "owner": "leanprover",
- "repo": "lean4",
- "rev": "32dcc6eb895b58df3d3241a2521963e64995b621",
- "type": "github"
- },
- "original": {
- "owner": "leanprover",
- "repo": "lean4",
- "type": "github"
- }
- },
- "lean4-mode": {
- "flake": false,
- "locked": {
- "lastModified": 1676498134,
- "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
- "owner": "leanprover",
- "repo": "lean4-mode",
- "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
- "type": "github"
- },
- "original": {
- "owner": "leanprover",
- "repo": "lean4-mode",
- "type": "github"
- }
- },
- "lean4-mode_2": {
- "flake": false,
- "locked": {
- "lastModified": 1676498134,
- "narHash": "sha256-u3WvyKxOViZG53hkb8wd2/Og6muTecbh+NdflIgVeyk=",
- "owner": "leanprover",
- "repo": "lean4-mode",
- "rev": "2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440",
- "type": "github"
- },
- "original": {
- "owner": "leanprover",
- "repo": "lean4-mode",
- "type": "github"
- }
- },
- "lean_2": {
- "inputs": {
- "flake-utils": "flake-utils_5",
- "lean4-mode": "lean4-mode_2",
- "nix": "nix_2",
- "nixpkgs": "nixpkgs_7"
- },
- "locked": {
- "lastModified": 1710111430,
- "narHash": "sha256-TsVeepxSag4OMVWH2UxntI0HHF2Db7hYUpAwhM8XjUQ=",
- "owner": "leanprover",
- "repo": "lean4",
- "rev": "32dcc6eb895b58df3d3241a2521963e64995b621",
- "type": "github"
- },
- "original": {
- "owner": "leanprover",
- "repo": "lean4",
- "type": "github"
- }
- },
- "lowdown-src": {
- "flake": false,
- "locked": {
- "lastModified": 1633514407,
- "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
- "owner": "kristapsdz",
- "repo": "lowdown",
- "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
- "type": "github"
- },
- "original": {
- "owner": "kristapsdz",
- "repo": "lowdown",
- "type": "github"
- }
- },
- "lowdown-src_2": {
- "flake": false,
- "locked": {
- "lastModified": 1633514407,
- "narHash": "sha256-Dw32tiMjdK9t3ETl5fzGrutQTzh2rufgZV4A/BbxuD4=",
- "owner": "kristapsdz",
- "repo": "lowdown",
- "rev": "d2c2b44ff6c27b936ec27358a2653caaef8f73b8",
- "type": "github"
- },
- "original": {
- "owner": "kristapsdz",
- "repo": "lowdown",
- "type": "github"
- }
- },
- "nix": {
- "inputs": {
- "lowdown-src": "lowdown-src",
- "nixpkgs": "nixpkgs_3",
- "nixpkgs-regression": "nixpkgs-regression"
- },
- "locked": {
- "lastModified": 1657097207,
- "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
- "owner": "NixOS",
- "repo": "nix",
- "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "repo": "nix",
- "type": "github"
- }
- },
- "nix_2": {
- "inputs": {
- "lowdown-src": "lowdown-src_2",
- "nixpkgs": "nixpkgs_6",
- "nixpkgs-regression": "nixpkgs-regression_2"
- },
- "locked": {
- "lastModified": 1657097207,
- "narHash": "sha256-SmeGmjWM3fEed3kQjqIAO8VpGmkC2sL1aPE7kKpK650=",
- "owner": "NixOS",
- "repo": "nix",
- "rev": "f6316b49a0c37172bca87ede6ea8144d7d89832f",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "repo": "nix",
- "type": "github"
- }
- },
"nixpkgs": {
"locked": {
"lastModified": 1701436327,
@@ -418,38 +203,6 @@
"type": "indirect"
}
},
- "nixpkgs-regression": {
- "locked": {
- "lastModified": 1643052045,
- "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
- "type": "github"
- }
- },
- "nixpkgs-regression_2": {
- "locked": {
- "lastModified": 1643052045,
- "narHash": "sha256-uGJ0VXIhWKGXxkeNnq4TvV3CIOkUJ3PAoLZ3HMzNVMw=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "215d4d0fd80ca5163643b03a33fde804a29cc1e2",
- "type": "github"
- }
- },
"nixpkgs_2": {
"locked": {
"lastModified": 1693158576,
@@ -465,86 +218,6 @@
"type": "indirect"
}
},
- "nixpkgs_3": {
- "locked": {
- "lastModified": 1653988320,
- "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "ref": "nixos-22.05-small",
- "repo": "nixpkgs",
- "type": "github"
- }
- },
- "nixpkgs_4": {
- "locked": {
- "lastModified": 1686089707,
- "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "ref": "nixpkgs-unstable",
- "repo": "nixpkgs",
- "type": "github"
- }
- },
- "nixpkgs_5": {
- "locked": {
- "lastModified": 1659914493,
- "narHash": "sha256-lkA5X3VNMKirvA+SUzvEhfA7XquWLci+CGi505YFAIs=",
- "owner": "nixos",
- "repo": "nixpkgs",
- "rev": "022caabb5f2265ad4006c1fa5b1ebe69fb0c3faf",
- "type": "github"
- },
- "original": {
- "owner": "nixos",
- "ref": "nixos-21.05",
- "repo": "nixpkgs",
- "type": "github"
- }
- },
- "nixpkgs_6": {
- "locked": {
- "lastModified": 1653988320,
- "narHash": "sha256-ZaqFFsSDipZ6KVqriwM34T739+KLYJvNmCWzErjAg7c=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "2fa57ed190fd6c7c746319444f34b5917666e5c1",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "ref": "nixos-22.05-small",
- "repo": "nixpkgs",
- "type": "github"
- }
- },
- "nixpkgs_7": {
- "locked": {
- "lastModified": 1686089707,
- "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
- "owner": "NixOS",
- "repo": "nixpkgs",
- "rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
- "type": "github"
- },
- "original": {
- "owner": "NixOS",
- "ref": "nixpkgs-unstable",
- "repo": "nixpkgs",
- "type": "github"
- }
- },
"root": {
"inputs": {
"charon": "charon",
@@ -553,8 +226,6 @@
"flake-utils"
],
"hacl-nix": "hacl-nix",
- "lake": "lake",
- "lean": "lean_2",
"nixpkgs": [
"charon",
"nixpkgs"
@@ -615,21 +286,6 @@
"repo": "default",
"type": "github"
}
- },
- "systems_3": {
- "locked": {
- "lastModified": 1681028828,
- "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
- "owner": "nix-systems",
- "repo": "default",
- "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
- "type": "github"
- },
- "original": {
- "owner": "nix-systems",
- "repo": "default",
- "type": "github"
- }
}
},
"root": "root",
diff --git a/flake.nix b/flake.nix
index cfeb5188..32898765 100644
--- a/flake.nix
+++ b/flake.nix
@@ -8,15 +8,11 @@
flake-utils.follows = "charon/flake-utils";
nixpkgs.follows = "charon/nixpkgs";
hacl-nix.url = "github:hacl-star/hacl-nix";
- lean.url = "github:leanprover/lean4";
- #lake.url = "github:leanprover/lake";
- lake.url = "github:leanprover/lake/lean4-master";
- #lake.flake = false;
};
# Remark: keep the list of outputs in sync with the list of inputs above
# (see above remark)
- outputs = { self, charon, flake-utils, nixpkgs, hacl-nix, lean, lake }:
+ outputs = { self, charon, flake-utils, nixpkgs, hacl-nix }:
flake-utils.lib.eachSystem [ "x86_64-linux" ] (system:
let
pkgs = import nixpkgs { inherit system; };
@@ -126,20 +122,6 @@
# The tests don't generate anything - TODO: actually they do
installPhase = "touch $out";
};
- # Replay the Lean proofs. TODO: doesn't work
- aeneas-verify-lean = pkgs.stdenv.mkDerivation {
- name = "aeneas_verify_lean";
- src = ./tests/lean;
- #LAKE_EXE = lean.packages.${system};
- #buildInputs = [lean.packages.${system}.lake-dev];
- buildInputs = [lean.packages.${system} lake.packages.${system}.cli];
- #buildInputs = [lake.packages.${system}.cli];
- buildPhase= ''
- make prepare-projects
- #make verify -j $NIX_BUILD_CORES
- make verify
- '';
- };
# Replay the HOL4 proofs
#
# Remark: we tried to have two targets, one for ./backends/hol4 and
@@ -174,7 +156,6 @@
inherit aeneas aeneas-tests
aeneas-verify-fstar
aeneas-verify-coq
- aeneas-verify-lean
aeneas-verify-hol4; };
});
}
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v
index 5fa952b4..fcafed53 100644
--- a/tests/coq/misc/Constants.v
+++ b/tests/coq/misc/Constants.v
@@ -158,4 +158,21 @@ Definition s3 : Pair_t u32 u32 := s3_body%global.
Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32.
Definition s4 : Pair_t u32 u32 := s4_body%global.
+(** [constants::V]
+ Source: 'src/constants.rs', lines 86:0-86:31 *)
+Record V_t (T : Type) (N : usize) := mkV_t { v_x : array T N; }.
+
+Arguments mkV_t { _ _ }.
+Arguments v_x { _ _ }.
+
+(** [constants::{constants::V<T, N>#1}::LEN]
+ Source: 'src/constants.rs', lines 91:4-91:24 *)
+Definition v_len_body (T : Type) (N : usize) : result usize := Return N.
+Definition v_len (T : Type) (N : usize) : usize := (v_len_body T N)%global.
+
+(** [constants::use_v]:
+ Source: 'src/constants.rs', lines 94:0-94:42 *)
+Definition use_v (T : Type) (N : usize) : result usize :=
+ Return (v_len T N).
+
End Constants.
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index a9cd7e91..a861c114 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -283,9 +283,12 @@ Definition ToTypetraitsBoolWrapperT (T : Type) (toTypeBoolTInst : ToType_t bool
(** [traits::WithConstTy::LEN2]
Source: 'src/traits.rs', lines 164:4-164:21 *)
-Definition with_const_ty_len2_default_body : result usize := Return 32%usize.
-Definition with_const_ty_len2_default : usize :=
- with_const_ty_len2_default_body%global
+Definition with_const_ty_len2_default_body (Self : Type) (LEN : usize)
+ : result usize :=
+ Return 32%usize
+.
+Definition with_const_ty_len2_default (Self : Type) (LEN : usize) : usize :=
+ (with_const_ty_len2_default_body Self LEN)%global
.
(** Trait declaration: [traits::WithConstTy]
@@ -326,7 +329,7 @@ Definition withConstTyBool32_f
Source: 'src/traits.rs', lines 174:0-174:29 *)
Definition WithConstTyBool32 : WithConstTy_t bool 32%usize := {|
WithConstTy_tWithConstTy_t_LEN1 := with_const_ty_bool32_len1;
- WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_default;
+ WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_default bool 32%usize;
WithConstTy_tWithConstTy_t_V := u8;
WithConstTy_tWithConstTy_t_W := u64;
WithConstTy_tWithConstTy_t_W_clause_0 := ToU64U64;
@@ -613,4 +616,93 @@ Definition test_get_trait
getTraitInst.(GetTrait_t_get_w) x
.
+(** Trait declaration: [traits::Trait]
+ Source: 'src/traits.rs', lines 310:0-310:15 *)
+Record Trait_t (Self : Type) := mkTrait_t { Trait_tTrait_t_LEN : usize; }.
+
+Arguments mkTrait_t { _ }.
+Arguments Trait_tTrait_t_LEN { _ }.
+
+(** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
+ Source: 'src/traits.rs', lines 315:4-315:20 *)
+Definition trait_array_len_body (T : Type) (N : usize) : result usize :=
+ Return N
+.
+Definition trait_array_len (T : Type) (N : usize) : usize :=
+ (trait_array_len_body T N)%global
+.
+
+(** Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}]
+ Source: 'src/traits.rs', lines 314:0-314:40 *)
+Definition TraitArray (T : Type) (N : usize) : Trait_t (array T N) := {|
+ Trait_tTrait_t_LEN := trait_array_len T N;
+|}.
+
+(** [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN]
+ Source: 'src/traits.rs', lines 319:4-319:20 *)
+Definition traittraits_wrapper_len_body (T : Type) (traitInst : Trait_t T)
+ : result usize :=
+ Return 0%usize
+.
+Definition traittraits_wrapper_len (T : Type) (traitInst : Trait_t T)
+ : usize :=
+ (traittraits_wrapper_len_body T traitInst)%global
+.
+
+(** Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}]
+ Source: 'src/traits.rs', lines 318:0-318:35 *)
+Definition TraittraitsWrapper (T : Type) (traitInst : Trait_t T) : Trait_t
+ (Wrapper_t T) := {|
+ Trait_tTrait_t_LEN := traittraits_wrapper_len T traitInst;
+|}.
+
+(** [traits::use_wrapper_len]:
+ Source: 'src/traits.rs', lines 322:0-322:43 *)
+Definition use_wrapper_len (T : Type) (traitInst : Trait_t T) : result usize :=
+ Return (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN)
+.
+
+(** [traits::Foo]
+ Source: 'src/traits.rs', lines 326:0-326:20 *)
+Record Foo_t (T U : Type) := mkFoo_t { foo_x : T; foo_y : U; }.
+
+Arguments mkFoo_t { _ _ }.
+Arguments foo_x { _ _ }.
+Arguments foo_y { _ _ }.
+
+(** [core::result::Result]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+Inductive core_result_Result_t (T E : Type) :=
+| Core_result_Result_Ok : T -> core_result_Result_t T E
+| Core_result_Result_Err : E -> core_result_Result_t T E
+.
+
+Arguments Core_result_Result_Ok { _ _ }.
+Arguments Core_result_Result_Err { _ _ }.
+
+(** [traits::{traits::Foo<T, U>#16}::FOO]
+ Source: 'src/traits.rs', lines 332:4-332:33 *)
+Definition foo_foo_body (T U : Type) (traitInst : Trait_t T)
+ : result (core_result_Result_t T i32) :=
+ Return (Core_result_Result_Err 0%i32)
+.
+Definition foo_foo (T U : Type) (traitInst : Trait_t T)
+ : core_result_Result_t T i32 :=
+ (foo_foo_body T U traitInst)%global
+.
+
+(** [traits::use_foo1]:
+ Source: 'src/traits.rs', lines 335:0-335:48 *)
+Definition use_foo1
+ (T U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) :=
+ Return (foo_foo T U traitInst)
+.
+
+(** [traits::use_foo2]:
+ Source: 'src/traits.rs', lines 339:0-339:48 *)
+Definition use_foo2
+ (T U : Type) (traitInst : Trait_t U) : result (core_result_Result_t U i32) :=
+ Return (foo_foo U T traitInst)
+.
+
End Traits.
diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst
index 66429c80..8d1cf3ce 100644
--- a/tests/fstar/misc/Constants.fst
+++ b/tests/fstar/misc/Constants.fst
@@ -143,3 +143,17 @@ let s3 : pair_t u32 u32 = eval_global s3_body
let s4_body : result (pair_t u32 u32) = mk_pair1 7 8
let s4 : pair_t u32 u32 = eval_global s4_body
+(** [constants::V]
+ Source: 'src/constants.rs', lines 86:0-86:31 *)
+type v_t (t : Type0) (n : usize) = { x : array t n; }
+
+(** [constants::{constants::V<T, N>#1}::LEN]
+ Source: 'src/constants.rs', lines 91:4-91:24 *)
+let v_len_body (t : Type0) (n : usize) : result usize = Return n
+let v_len (t : Type0) (n : usize) : usize = eval_global (v_len_body t n)
+
+(** [constants::use_v]:
+ Source: 'src/constants.rs', lines 94:0-94:42 *)
+let use_v (t : Type0) (n : usize) : result usize =
+ Return (v_len t n)
+
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 466fb482..fba564a5 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -229,9 +229,11 @@ let toTypetraitsBoolWrapperT (t : Type0) (toTypeBoolTInst : toType_t bool t) :
(** [traits::WithConstTy::LEN2]
Source: 'src/traits.rs', lines 164:4-164:21 *)
-let with_const_ty_len2_default_body : result usize = Return 32
-let with_const_ty_len2_default : usize =
- eval_global with_const_ty_len2_default_body
+let with_const_ty_len2_default_body (self : Type0) (len : usize)
+ : result usize =
+ Return 32
+let with_const_ty_len2_default (self : Type0) (len : usize) : usize =
+ eval_global (with_const_ty_len2_default_body self len)
(** Trait declaration: [traits::WithConstTy]
Source: 'src/traits.rs', lines 161:0-161:39 *)
@@ -259,7 +261,7 @@ let withConstTyBool32_f (i : u64) (a : array u8 32) : result u64 =
Source: 'src/traits.rs', lines 174:0-174:29 *)
let withConstTyBool32 : withConstTy_t bool 32 = {
cLEN1 = with_const_ty_bool32_len1;
- cLEN2 = with_const_ty_len2_default;
+ cLEN2 = with_const_ty_len2_default bool 32;
tV = u8;
tW = u64;
tW_clause_0 = toU64U64;
@@ -460,3 +462,70 @@ let test_get_trait
(t : Type0) (getTraitInst : getTrait_t t) (x : t) : result getTraitInst.tW =
getTraitInst.get_w x
+(** Trait declaration: [traits::Trait]
+ Source: 'src/traits.rs', lines 310:0-310:15 *)
+noeq type trait_t (self : Type0) = { cLEN : usize; }
+
+(** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
+ Source: 'src/traits.rs', lines 315:4-315:20 *)
+let trait_array_len_body (t : Type0) (n : usize) : result usize = Return n
+let trait_array_len (t : Type0) (n : usize) : usize =
+ eval_global (trait_array_len_body t n)
+
+(** Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}]
+ Source: 'src/traits.rs', lines 314:0-314:40 *)
+let traitArray (t : Type0) (n : usize) : trait_t (array t n) = {
+ cLEN = trait_array_len t n;
+}
+
+(** [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN]
+ Source: 'src/traits.rs', lines 319:4-319:20 *)
+let traittraits_wrapper_len_body (t : Type0) (traitInst : trait_t t)
+ : result usize =
+ Return 0
+let traittraits_wrapper_len (t : Type0) (traitInst : trait_t t) : usize =
+ eval_global (traittraits_wrapper_len_body t traitInst)
+
+(** Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}]
+ Source: 'src/traits.rs', lines 318:0-318:35 *)
+let traittraitsWrapper (t : Type0) (traitInst : trait_t t) : trait_t (wrapper_t
+ t) = {
+ cLEN = traittraits_wrapper_len t traitInst;
+}
+
+(** [traits::use_wrapper_len]:
+ Source: 'src/traits.rs', lines 322:0-322:43 *)
+let use_wrapper_len (t : Type0) (traitInst : trait_t t) : result usize =
+ Return (traittraitsWrapper t traitInst).cLEN
+
+(** [traits::Foo]
+ Source: 'src/traits.rs', lines 326:0-326:20 *)
+type foo_t (t u : Type0) = { x : t; y : u; }
+
+(** [core::result::Result]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+type core_result_Result_t (t e : Type0) =
+| Core_result_Result_Ok : t -> core_result_Result_t t e
+| Core_result_Result_Err : e -> core_result_Result_t t e
+
+(** [traits::{traits::Foo<T, U>#16}::FOO]
+ Source: 'src/traits.rs', lines 332:4-332:33 *)
+let foo_foo_body (t u : Type0) (traitInst : trait_t t)
+ : result (core_result_Result_t t i32) =
+ Return (Core_result_Result_Err 0)
+let foo_foo (t u : Type0) (traitInst : trait_t t)
+ : core_result_Result_t t i32 =
+ eval_global (foo_foo_body t u traitInst)
+
+(** [traits::use_foo1]:
+ Source: 'src/traits.rs', lines 335:0-335:48 *)
+let use_foo1
+ (t u : Type0) (traitInst : trait_t t) : result (core_result_Result_t t i32) =
+ Return (foo_foo t u traitInst)
+
+(** [traits::use_foo2]:
+ Source: 'src/traits.rs', lines 339:0-339:48 *)
+let use_foo2
+ (t u : Type0) (traitInst : trait_t u) : result (core_result_Result_t u i32) =
+ Return (foo_foo u t traitInst)
+
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 7949a25c..40f590d4 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -149,4 +149,19 @@ def S3 : Pair U32 U32 := eval_global S3_body
def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32
def S4 : Pair U32 U32 := eval_global S4_body
+/- [constants::V]
+ Source: 'src/constants.rs', lines 86:0-86:31 -/
+structure V (T : Type) (N : Usize) where
+ x : Array T N
+
+/- [constants::{constants::V<T, N>#1}::LEN]
+ Source: 'src/constants.rs', lines 91:4-91:24 -/
+def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N
+def V.LEN (T : Type) (N : Usize) : Usize := eval_global (V.LEN_body T N)
+
+/- [constants::use_v]:
+ Source: 'src/constants.rs', lines 94:0-94:42 -/
+def use_v (T : Type) (N : Usize) : Result Usize :=
+ Result.ret (V.LEN T N)
+
end constants
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 26dac252..acddd1a9 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -242,9 +242,10 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
/- [traits::WithConstTy::LEN2]
Source: 'src/traits.rs', lines 164:4-164:21 -/
-def WithConstTy.LEN2_default_body : Result Usize := Result.ret 32#usize
-def WithConstTy.LEN2_default : Usize :=
- eval_global WithConstTy.LEN2_default_body
+def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize :=
+ Result.ret 32#usize
+def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize :=
+ eval_global (WithConstTy.LEN2_default_body Self LEN)
/- Trait declaration: [traits::WithConstTy]
Source: 'src/traits.rs', lines 161:0-161:39 -/
@@ -270,7 +271,7 @@ def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
Source: 'src/traits.rs', lines 174:0-174:29 -/
def WithConstTyBool32 : WithConstTy Bool 32#usize := {
LEN1 := WithConstTyBool32.LEN1
- LEN2 := WithConstTy.LEN2_default
+ LEN2 := WithConstTy.LEN2_default Bool 32#usize
V := U8
W := U64
W_clause_0 := ToU64U64
@@ -467,4 +468,73 @@ def test_get_trait
(T : Type) (GetTraitInst : GetTrait T) (x : T) : Result GetTraitInst.W :=
GetTraitInst.get_w x
+/- Trait declaration: [traits::Trait]
+ Source: 'src/traits.rs', lines 310:0-310:15 -/
+structure Trait (Self : Type) where
+ LEN : Usize
+
+/- [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
+ Source: 'src/traits.rs', lines 315:4-315:20 -/
+def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N
+def TraitArray.LEN (T : Type) (N : Usize) : Usize :=
+ eval_global (TraitArray.LEN_body T N)
+
+/- Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}]
+ Source: 'src/traits.rs', lines 314:0-314:40 -/
+def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := {
+ LEN := TraitArray.LEN T N
+}
+
+/- [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN]
+ Source: 'src/traits.rs', lines 319:4-319:20 -/
+def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T)
+ : Result Usize :=
+ Result.ret 0#usize
+def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize :=
+ eval_global (TraittraitsWrapper.LEN_body T TraitInst)
+
+/- Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}]
+ Source: 'src/traits.rs', lines 318:0-318:35 -/
+def TraittraitsWrapper (T : Type) (TraitInst : Trait T) : Trait (Wrapper T)
+ := {
+ LEN := TraittraitsWrapper.LEN T TraitInst
+}
+
+/- [traits::use_wrapper_len]:
+ Source: 'src/traits.rs', lines 322:0-322:43 -/
+def use_wrapper_len (T : Type) (TraitInst : Trait T) : Result Usize :=
+ Result.ret (TraittraitsWrapper T TraitInst).LEN
+
+/- [traits::Foo]
+ Source: 'src/traits.rs', lines 326:0-326:20 -/
+structure Foo (T U : Type) where
+ x : T
+ y : U
+
+/- [core::result::Result]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 -/
+inductive core.result.Result (T E : Type) :=
+| Ok : T → core.result.Result T E
+| Err : E → core.result.Result T E
+
+/- [traits::{traits::Foo<T, U>#16}::FOO]
+ Source: 'src/traits.rs', lines 332:4-332:33 -/
+def Foo.FOO_body (T U : Type) (TraitInst : Trait T)
+ : Result (core.result.Result T I32) :=
+ Result.ret (core.result.Result.Err 0#i32)
+def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
+ eval_global (Foo.FOO_body T U TraitInst)
+
+/- [traits::use_foo1]:
+ Source: 'src/traits.rs', lines 335:0-335:48 -/
+def use_foo1
+ (T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) :=
+ Result.ret (Foo.FOO T U TraitInst)
+
+/- [traits::use_foo2]:
+ Source: 'src/traits.rs', lines 339:0-339:48 -/
+def use_foo2
+ (T U : Type) (TraitInst : Trait U) : Result (core.result.Result U I32) :=
+ Result.ret (Foo.FOO U T TraitInst)
+
end traits
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-11 02:28:17 +0000