From a8ebfc3947adb052f36775c664e43a8dc7434660 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Mar 2024 01:39:07 +0100 Subject: Make good progress on adding generics to global constants --- compiler/Extract.ml | 107 +++++++++++++++++++++++++++++--------- compiler/InterpreterStatements.ml | 32 +++++++----- compiler/Pure.ml | 20 +++++++ compiler/PureTypeCheck.ml | 4 +- compiler/SymbolicAst.ml | 2 +- compiler/SymbolicToPure.ml | 47 +++++++++++++++-- compiler/SynthesizeSymbolic.ml | 6 +-- compiler/Translate.ml | 1 + 8 files changed, 172 insertions(+), 47 deletions(-) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index a93ed6e4..3c5ea15b 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,7 +329,9 @@ 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 -> @@ -1691,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 @@ -1708,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; @@ -1719,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 ": " *) @@ -1775,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 ("...",] *) @@ -1815,58 +1835,92 @@ 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 = [ 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) + (List.concat 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 @@ -2592,7 +2646,12 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) let item_name = ctx_get_trait_const trait_decl_id name ctx 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); + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + (List.concat [ type_params; cg_params; trait_clauses ]) in extract_trait_impl_item ctx fmt item_name ty) diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index eef9e2c9..95a2956b 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -949,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 @@ -1021,31 +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; - } - 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/Pure.ml b/compiler/Pure.ml index a735667e..cf6710aa 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -1087,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/SymbolicAst.ml b/compiler/SymbolicAst.ml index 79c03e58..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. diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 27279327..58fb6d04 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1890,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) -> @@ -2662,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 @@ -3838,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 fba1dfb0..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. -- cgit v1.2.3 From d281f43fd5dfeab24fe582fd88564f6c1ab7f934 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Mar 2024 01:39:29 +0100 Subject: Regenerate the constants tests and update Primitives/Base.lean --- backends/lean/Base/Primitives/Base.lean | 2 +- tests/coq/misc/Constants.v | 53 ++++++++++++++++++++++----------- tests/fstar/misc/Constants.fst | 50 ++++++++++++++++++++----------- tests/lean/Constants.lean | 51 ++++++++++++++++++++----------- 4 files changed, 101 insertions(+), 55 deletions(-) diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index 0b9d9c39..d2695854 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -69,7 +69,7 @@ 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): α := +def eval_global {α: Type u} (x: Result α) (_: ret? x := by first | apply Eq.refl | decide): α := match x with | fail _ | div => by contradiction | ret x => x diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 5fa952b4..81240847 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -11,17 +11,17 @@ Module Constants. (** [constants::X0] Source: 'src/constants.rs', lines 5:0-5:17 *) Definition x0_body : result u32 := Return 0%u32. -Definition x0 : u32 := x0_body%global. +Definition x0 : u32 := (x0_body)%global. (** [constants::X1] Source: 'src/constants.rs', lines 7:0-7:17 *) Definition x1_body : result u32 := Return core_u32_max. -Definition x1 : u32 := x1_body%global. +Definition x1 : u32 := (x1_body)%global. (** [constants::X2] Source: 'src/constants.rs', lines 10:0-10:17 *) Definition x2_body : result u32 := Return 3%u32. -Definition x2 : u32 := x2_body%global. +Definition x2 : u32 := (x2_body)%global. (** [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 *) @@ -31,7 +31,7 @@ Definition incr (n : u32) : result u32 := (** [constants::X3] Source: 'src/constants.rs', lines 15:0-15:17 *) Definition x3_body : result u32 := incr 32%u32. -Definition x3 : u32 := x3_body%global. +Definition x3 : u32 := (x3_body)%global. (** [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 *) @@ -56,24 +56,24 @@ Definition mk_pair1 (x : u32) (y1 : u32) : result (Pair_t u32 u32) := (** [constants::P0] Source: 'src/constants.rs', lines 31:0-31:24 *) Definition p0_body : result (u32 * u32) := mk_pair0 0%u32 1%u32. -Definition p0 : (u32 * u32) := p0_body%global. +Definition p0 : (u32 * u32) := (p0_body)%global. (** [constants::P1] Source: 'src/constants.rs', lines 32:0-32:28 *) Definition p1_body : result (Pair_t u32 u32) := mk_pair1 0%u32 1%u32. -Definition p1 : Pair_t u32 u32 := p1_body%global. +Definition p1 : Pair_t u32 u32 := (p1_body)%global. (** [constants::P2] Source: 'src/constants.rs', lines 33:0-33:24 *) Definition p2_body : result (u32 * u32) := Return (0%u32, 1%u32). -Definition p2 : (u32 * u32) := p2_body%global. +Definition p2 : (u32 * u32) := (p2_body)%global. (** [constants::P3] Source: 'src/constants.rs', lines 34:0-34:28 *) Definition p3_body : result (Pair_t u32 u32) := Return {| pair_x := 0%u32; pair_y := 1%u32 |} . -Definition p3 : Pair_t u32 u32 := p3_body%global. +Definition p3 : Pair_t u32 u32 := (p3_body)%global. (** [constants::Wrap] Source: 'src/constants.rs', lines 49:0-49:18 *) @@ -91,7 +91,7 @@ Definition wrap_new (T : Type) (value : T) : result (Wrap_t T) := (** [constants::Y] Source: 'src/constants.rs', lines 41:0-41:22 *) Definition y_body : result (Wrap_t i32) := wrap_new i32 2%i32. -Definition y : Wrap_t i32 := y_body%global. +Definition y : Wrap_t i32 := (y_body)%global. (** [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 *) @@ -101,12 +101,12 @@ Definition unwrap_y : result i32 := (** [constants::YVAL] Source: 'src/constants.rs', lines 47:0-47:19 *) Definition yval_body : result i32 := unwrap_y. -Definition yval : i32 := yval_body%global. +Definition yval : i32 := (yval_body)%global. (** [constants::get_z1::Z1] Source: 'src/constants.rs', lines 62:4-62:17 *) Definition get_z1_z1_body : result i32 := Return 3%i32. -Definition get_z1_z1 : i32 := get_z1_z1_body%global. +Definition get_z1_z1 : i32 := (get_z1_z1_body)%global. (** [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 *) @@ -121,17 +121,17 @@ Definition add (a : i32) (b : i32) : result i32 := (** [constants::Q1] Source: 'src/constants.rs', lines 74:0-74:17 *) Definition q1_body : result i32 := Return 5%i32. -Definition q1 : i32 := q1_body%global. +Definition q1 : i32 := (q1_body)%global. (** [constants::Q2] Source: 'src/constants.rs', lines 75:0-75:17 *) Definition q2_body : result i32 := Return q1. -Definition q2 : i32 := q2_body%global. +Definition q2 : i32 := (q2_body)%global. (** [constants::Q3] Source: 'src/constants.rs', lines 76:0-76:17 *) Definition q3_body : result i32 := add q2 3%i32. -Definition q3 : i32 := q3_body%global. +Definition q3 : i32 := (q3_body)%global. (** [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 *) @@ -141,21 +141,38 @@ Definition get_z2 : result i32 := (** [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 *) Definition s1_body : result u32 := Return 6%u32. -Definition s1 : u32 := s1_body%global. +Definition s1 : u32 := (s1_body)%global. (** [constants::S2] Source: 'src/constants.rs', lines 81:0-81:18 *) Definition s2_body : result u32 := incr s1. -Definition s2 : u32 := s2_body%global. +Definition s2 : u32 := (s2_body)%global. (** [constants::S3] Source: 'src/constants.rs', lines 82:0-82:29 *) Definition s3_body : result (Pair_t u32 u32) := Return p3. -Definition s3 : Pair_t u32 u32 := s3_body%global. +Definition s3 : Pair_t u32 u32 := (s3_body)%global. (** [constants::S4] Source: 'src/constants.rs', lines 83:0-83:29 *) Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32. -Definition s4 : Pair_t u32 u32 := s4_body%global. +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#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/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst index 66429c80..3664c7d6 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -8,17 +8,17 @@ open Primitives (** [constants::X0] Source: 'src/constants.rs', lines 5:0-5:17 *) let x0_body : result u32 = Return 0 -let x0 : u32 = eval_global x0_body +let x0 : u32 = eval_global (x0_body) (** [constants::X1] Source: 'src/constants.rs', lines 7:0-7:17 *) let x1_body : result u32 = Return core_u32_max -let x1 : u32 = eval_global x1_body +let x1 : u32 = eval_global (x1_body) (** [constants::X2] Source: 'src/constants.rs', lines 10:0-10:17 *) let x2_body : result u32 = Return 3 -let x2 : u32 = eval_global x2_body +let x2 : u32 = eval_global (x2_body) (** [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 *) @@ -28,7 +28,7 @@ let incr (n : u32) : result u32 = (** [constants::X3] Source: 'src/constants.rs', lines 15:0-15:17 *) let x3_body : result u32 = incr 32 -let x3 : u32 = eval_global x3_body +let x3 : u32 = eval_global (x3_body) (** [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 *) @@ -47,22 +47,22 @@ let mk_pair1 (x : u32) (y1 : u32) : result (pair_t u32 u32) = (** [constants::P0] Source: 'src/constants.rs', lines 31:0-31:24 *) let p0_body : result (u32 & u32) = mk_pair0 0 1 -let p0 : (u32 & u32) = eval_global p0_body +let p0 : (u32 & u32) = eval_global (p0_body) (** [constants::P1] Source: 'src/constants.rs', lines 32:0-32:28 *) let p1_body : result (pair_t u32 u32) = mk_pair1 0 1 -let p1 : pair_t u32 u32 = eval_global p1_body +let p1 : pair_t u32 u32 = eval_global (p1_body) (** [constants::P2] Source: 'src/constants.rs', lines 33:0-33:24 *) let p2_body : result (u32 & u32) = Return (0, 1) -let p2 : (u32 & u32) = eval_global p2_body +let p2 : (u32 & u32) = eval_global (p2_body) (** [constants::P3] Source: 'src/constants.rs', lines 34:0-34:28 *) let p3_body : result (pair_t u32 u32) = Return { x = 0; y = 1 } -let p3 : pair_t u32 u32 = eval_global p3_body +let p3 : pair_t u32 u32 = eval_global (p3_body) (** [constants::Wrap] Source: 'src/constants.rs', lines 49:0-49:18 *) @@ -76,7 +76,7 @@ let wrap_new (t : Type0) (value : t) : result (wrap_t t) = (** [constants::Y] Source: 'src/constants.rs', lines 41:0-41:22 *) let y_body : result (wrap_t i32) = wrap_new i32 2 -let y : wrap_t i32 = eval_global y_body +let y : wrap_t i32 = eval_global (y_body) (** [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 *) @@ -86,12 +86,12 @@ let unwrap_y : result i32 = (** [constants::YVAL] Source: 'src/constants.rs', lines 47:0-47:19 *) let yval_body : result i32 = unwrap_y -let yval : i32 = eval_global yval_body +let yval : i32 = eval_global (yval_body) (** [constants::get_z1::Z1] Source: 'src/constants.rs', lines 62:4-62:17 *) let get_z1_z1_body : result i32 = Return 3 -let get_z1_z1 : i32 = eval_global get_z1_z1_body +let get_z1_z1 : i32 = eval_global (get_z1_z1_body) (** [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 *) @@ -106,17 +106,17 @@ let add (a : i32) (b : i32) : result i32 = (** [constants::Q1] Source: 'src/constants.rs', lines 74:0-74:17 *) let q1_body : result i32 = Return 5 -let q1 : i32 = eval_global q1_body +let q1 : i32 = eval_global (q1_body) (** [constants::Q2] Source: 'src/constants.rs', lines 75:0-75:17 *) let q2_body : result i32 = Return q1 -let q2 : i32 = eval_global q2_body +let q2 : i32 = eval_global (q2_body) (** [constants::Q3] Source: 'src/constants.rs', lines 76:0-76:17 *) let q3_body : result i32 = add q2 3 -let q3 : i32 = eval_global q3_body +let q3 : i32 = eval_global (q3_body) (** [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 *) @@ -126,20 +126,34 @@ let get_z2 : result i32 = (** [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 *) let s1_body : result u32 = Return 6 -let s1 : u32 = eval_global s1_body +let s1 : u32 = eval_global (s1_body) (** [constants::S2] Source: 'src/constants.rs', lines 81:0-81:18 *) let s2_body : result u32 = incr s1 -let s2 : u32 = eval_global s2_body +let s2 : u32 = eval_global (s2_body) (** [constants::S3] Source: 'src/constants.rs', lines 82:0-82:29 *) let s3_body : result (pair_t u32 u32) = Return p3 -let s3 : pair_t u32 u32 = eval_global s3_body +let s3 : pair_t u32 u32 = eval_global (s3_body) (** [constants::S4] Source: 'src/constants.rs', lines 83:0-83:29 *) let s4_body : result (pair_t u32 u32) = mk_pair1 7 8 -let s4 : pair_t u32 u32 = eval_global s4_body +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#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/lean/Constants.lean b/tests/lean/Constants.lean index 7949a25c..3727e393 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -8,17 +8,17 @@ namespace constants /- [constants::X0] Source: 'src/constants.rs', lines 5:0-5:17 -/ def X0_body : Result U32 := Result.ret 0#u32 -def X0 : U32 := eval_global X0_body +def X0 : U32 := eval_global (X0_body) /- [constants::X1] Source: 'src/constants.rs', lines 7:0-7:17 -/ def X1_body : Result U32 := Result.ret core_u32_max -def X1 : U32 := eval_global X1_body +def X1 : U32 := eval_global (X1_body) /- [constants::X2] Source: 'src/constants.rs', lines 10:0-10:17 -/ def X2_body : Result U32 := Result.ret 3#u32 -def X2 : U32 := eval_global X2_body +def X2 : U32 := eval_global (X2_body) /- [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 -/ @@ -28,7 +28,7 @@ def incr (n : U32) : Result U32 := /- [constants::X3] Source: 'src/constants.rs', lines 15:0-15:17 -/ def X3_body : Result U32 := incr 32#u32 -def X3 : U32 := eval_global X3_body +def X3 : U32 := eval_global (X3_body) /- [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 -/ @@ -49,22 +49,22 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) := /- [constants::P0] Source: 'src/constants.rs', lines 31:0-31:24 -/ def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32 -def P0 : (U32 × U32) := eval_global P0_body +def P0 : (U32 × U32) := eval_global (P0_body) /- [constants::P1] Source: 'src/constants.rs', lines 32:0-32:28 -/ def P1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32 -def P1 : Pair U32 U32 := eval_global P1_body +def P1 : Pair U32 U32 := eval_global (P1_body) /- [constants::P2] Source: 'src/constants.rs', lines 33:0-33:24 -/ def P2_body : Result (U32 × U32) := Result.ret (0#u32, 1#u32) -def P2 : (U32 × U32) := eval_global P2_body +def P2 : (U32 × U32) := eval_global (P2_body) /- [constants::P3] Source: 'src/constants.rs', lines 34:0-34:28 -/ def P3_body : Result (Pair U32 U32) := Result.ret { x := 0#u32, y := 1#u32 } -def P3 : Pair U32 U32 := eval_global P3_body +def P3 : Pair U32 U32 := eval_global (P3_body) /- [constants::Wrap] Source: 'src/constants.rs', lines 49:0-49:18 -/ @@ -79,7 +79,7 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) := /- [constants::Y] Source: 'src/constants.rs', lines 41:0-41:22 -/ def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32 -def Y : Wrap I32 := eval_global Y_body +def Y : Wrap I32 := eval_global (Y_body) /- [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 -/ @@ -89,12 +89,12 @@ def unwrap_y : Result I32 := /- [constants::YVAL] Source: 'src/constants.rs', lines 47:0-47:19 -/ def YVAL_body : Result I32 := unwrap_y -def YVAL : I32 := eval_global YVAL_body +def YVAL : I32 := eval_global (YVAL_body) /- [constants::get_z1::Z1] Source: 'src/constants.rs', lines 62:4-62:17 -/ def get_z1.Z1_body : Result I32 := Result.ret 3#i32 -def get_z1.Z1 : I32 := eval_global get_z1.Z1_body +def get_z1.Z1 : I32 := eval_global (get_z1.Z1_body) /- [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 -/ @@ -109,17 +109,17 @@ def add (a : I32) (b : I32) : Result I32 := /- [constants::Q1] Source: 'src/constants.rs', lines 74:0-74:17 -/ def Q1_body : Result I32 := Result.ret 5#i32 -def Q1 : I32 := eval_global Q1_body +def Q1 : I32 := eval_global (Q1_body) /- [constants::Q2] Source: 'src/constants.rs', lines 75:0-75:17 -/ def Q2_body : Result I32 := Result.ret Q1 -def Q2 : I32 := eval_global Q2_body +def Q2 : I32 := eval_global (Q2_body) /- [constants::Q3] Source: 'src/constants.rs', lines 76:0-76:17 -/ def Q3_body : Result I32 := add Q2 3#i32 -def Q3 : I32 := eval_global Q3_body +def Q3 : I32 := eval_global (Q3_body) /- [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 -/ @@ -132,21 +132,36 @@ def get_z2 : Result I32 := /- [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 -/ def S1_body : Result U32 := Result.ret 6#u32 -def S1 : U32 := eval_global S1_body +def S1 : U32 := eval_global (S1_body) /- [constants::S2] Source: 'src/constants.rs', lines 81:0-81:18 -/ def S2_body : Result U32 := incr S1 -def S2 : U32 := eval_global S2_body +def S2 : U32 := eval_global (S2_body) /- [constants::S3] Source: 'src/constants.rs', lines 82:0-82:29 -/ def S3_body : Result (Pair U32 U32) := Result.ret P3 -def S3 : Pair U32 U32 := eval_global S3_body +def S3 : Pair U32 U32 := eval_global (S3_body) /- [constants::S4] Source: 'src/constants.rs', lines 83:0-83:29 -/ def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32 -def S4 : Pair U32 U32 := eval_global S4_body +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#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 -- cgit v1.2.3 From 84066ffa2a0d3d620a7b0776e251052f1876dce9 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Mar 2024 01:52:55 +0100 Subject: Fix the extraction of trait constants --- compiler/Extract.ml | 8 ++++--- compiler/InterpreterExpressions.ml | 49 +++++++++++++------------------------- 2 files changed, 22 insertions(+), 35 deletions(-) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 3c5ea15b..667d269a 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -337,7 +337,7 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | Proj proj -> extract_field_projector ctx fmt inside app proj qualif.generics args | TraitConst (trait_ref, const_name) -> - extract_trait_ref ctx fmt TypeDeclId.Set.empty false trait_ref; + 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 @@ -1888,13 +1888,15 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) global.generics type_params cg_params trait_clauses decl_ty (Some (fun fmt -> - let all_params = [ type_params; cg_params; trait_clauses ] in + 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) - (List.concat all_params) + all_params in let use_brackets = all_params <> [] in (* Extract the name *) diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index dc100fe3..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 @@ -264,37 +263,23 @@ let eval_operand_no_reorganize (config : config) (op : operand) | CLiteral lit -> cf (literal_to_typed_value (ty_as_literal cv.ty) lit) ctx | CTraitConst (trait_ref, const_name) -> ( - 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, const_name), - e )))) + 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. -- cgit v1.2.3 From d0b3cd8a2fb6a55ff910fde4476c0ae4417b810d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Mar 2024 02:05:03 +0100 Subject: Update extract_trait_impl --- compiler/Extract.ml | 30 +++++++++++++++++++++++------- 1 file changed, 23 insertions(+), 7 deletions(-) diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 667d269a..aa097a4f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2641,23 +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); - List.iter - (fun p -> - F.pp_print_space fmt (); - F.pp_print_string fmt p) - (List.concat [ type_params; cg_params; trait_clauses ]) + 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 -- cgit v1.2.3 From 5a1317e51a5854699befb3b470bc346551b1691a Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Mar 2024 02:05:58 +0100 Subject: Regenerate the test files --- tests/coq/misc/Constants.v | 36 +++++++-------- tests/coq/traits/Traits.v | 100 +++++++++++++++++++++++++++++++++++++++-- tests/fstar/misc/Constants.fst | 36 +++++++-------- tests/fstar/traits/Traits.fst | 77 +++++++++++++++++++++++++++++-- tests/lean/Constants.lean | 36 +++++++-------- tests/lean/Traits.lean | 78 ++++++++++++++++++++++++++++++-- 6 files changed, 297 insertions(+), 66 deletions(-) diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 81240847..fcafed53 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -11,17 +11,17 @@ Module Constants. (** [constants::X0] Source: 'src/constants.rs', lines 5:0-5:17 *) Definition x0_body : result u32 := Return 0%u32. -Definition x0 : u32 := (x0_body)%global. +Definition x0 : u32 := x0_body%global. (** [constants::X1] Source: 'src/constants.rs', lines 7:0-7:17 *) Definition x1_body : result u32 := Return core_u32_max. -Definition x1 : u32 := (x1_body)%global. +Definition x1 : u32 := x1_body%global. (** [constants::X2] Source: 'src/constants.rs', lines 10:0-10:17 *) Definition x2_body : result u32 := Return 3%u32. -Definition x2 : u32 := (x2_body)%global. +Definition x2 : u32 := x2_body%global. (** [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 *) @@ -31,7 +31,7 @@ Definition incr (n : u32) : result u32 := (** [constants::X3] Source: 'src/constants.rs', lines 15:0-15:17 *) Definition x3_body : result u32 := incr 32%u32. -Definition x3 : u32 := (x3_body)%global. +Definition x3 : u32 := x3_body%global. (** [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 *) @@ -56,24 +56,24 @@ Definition mk_pair1 (x : u32) (y1 : u32) : result (Pair_t u32 u32) := (** [constants::P0] Source: 'src/constants.rs', lines 31:0-31:24 *) Definition p0_body : result (u32 * u32) := mk_pair0 0%u32 1%u32. -Definition p0 : (u32 * u32) := (p0_body)%global. +Definition p0 : (u32 * u32) := p0_body%global. (** [constants::P1] Source: 'src/constants.rs', lines 32:0-32:28 *) Definition p1_body : result (Pair_t u32 u32) := mk_pair1 0%u32 1%u32. -Definition p1 : Pair_t u32 u32 := (p1_body)%global. +Definition p1 : Pair_t u32 u32 := p1_body%global. (** [constants::P2] Source: 'src/constants.rs', lines 33:0-33:24 *) Definition p2_body : result (u32 * u32) := Return (0%u32, 1%u32). -Definition p2 : (u32 * u32) := (p2_body)%global. +Definition p2 : (u32 * u32) := p2_body%global. (** [constants::P3] Source: 'src/constants.rs', lines 34:0-34:28 *) Definition p3_body : result (Pair_t u32 u32) := Return {| pair_x := 0%u32; pair_y := 1%u32 |} . -Definition p3 : Pair_t u32 u32 := (p3_body)%global. +Definition p3 : Pair_t u32 u32 := p3_body%global. (** [constants::Wrap] Source: 'src/constants.rs', lines 49:0-49:18 *) @@ -91,7 +91,7 @@ Definition wrap_new (T : Type) (value : T) : result (Wrap_t T) := (** [constants::Y] Source: 'src/constants.rs', lines 41:0-41:22 *) Definition y_body : result (Wrap_t i32) := wrap_new i32 2%i32. -Definition y : Wrap_t i32 := (y_body)%global. +Definition y : Wrap_t i32 := y_body%global. (** [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 *) @@ -101,12 +101,12 @@ Definition unwrap_y : result i32 := (** [constants::YVAL] Source: 'src/constants.rs', lines 47:0-47:19 *) Definition yval_body : result i32 := unwrap_y. -Definition yval : i32 := (yval_body)%global. +Definition yval : i32 := yval_body%global. (** [constants::get_z1::Z1] Source: 'src/constants.rs', lines 62:4-62:17 *) Definition get_z1_z1_body : result i32 := Return 3%i32. -Definition get_z1_z1 : i32 := (get_z1_z1_body)%global. +Definition get_z1_z1 : i32 := get_z1_z1_body%global. (** [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 *) @@ -121,17 +121,17 @@ Definition add (a : i32) (b : i32) : result i32 := (** [constants::Q1] Source: 'src/constants.rs', lines 74:0-74:17 *) Definition q1_body : result i32 := Return 5%i32. -Definition q1 : i32 := (q1_body)%global. +Definition q1 : i32 := q1_body%global. (** [constants::Q2] Source: 'src/constants.rs', lines 75:0-75:17 *) Definition q2_body : result i32 := Return q1. -Definition q2 : i32 := (q2_body)%global. +Definition q2 : i32 := q2_body%global. (** [constants::Q3] Source: 'src/constants.rs', lines 76:0-76:17 *) Definition q3_body : result i32 := add q2 3%i32. -Definition q3 : i32 := (q3_body)%global. +Definition q3 : i32 := q3_body%global. (** [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 *) @@ -141,22 +141,22 @@ Definition get_z2 : result i32 := (** [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 *) Definition s1_body : result u32 := Return 6%u32. -Definition s1 : u32 := (s1_body)%global. +Definition s1 : u32 := s1_body%global. (** [constants::S2] Source: 'src/constants.rs', lines 81:0-81:18 *) Definition s2_body : result u32 := incr s1. -Definition s2 : u32 := (s2_body)%global. +Definition s2 : u32 := s2_body%global. (** [constants::S3] Source: 'src/constants.rs', lines 82:0-82:29 *) Definition s3_body : result (Pair_t u32 u32) := Return p3. -Definition s3 : Pair_t u32 u32 := (s3_body)%global. +Definition s3 : Pair_t u32 u32 := s3_body%global. (** [constants::S4] Source: 'src/constants.rs', lines 83:0-83:29 *) Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32. -Definition s4 : Pair_t u32 u32 := (s4_body)%global. +Definition s4 : Pair_t u32 u32 := s4_body%global. (** [constants::V] Source: 'src/constants.rs', lines 86:0-86:31 *) 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)#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)#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)#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)#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#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 3664c7d6..8d1cf3ce 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -8,17 +8,17 @@ open Primitives (** [constants::X0] Source: 'src/constants.rs', lines 5:0-5:17 *) let x0_body : result u32 = Return 0 -let x0 : u32 = eval_global (x0_body) +let x0 : u32 = eval_global x0_body (** [constants::X1] Source: 'src/constants.rs', lines 7:0-7:17 *) let x1_body : result u32 = Return core_u32_max -let x1 : u32 = eval_global (x1_body) +let x1 : u32 = eval_global x1_body (** [constants::X2] Source: 'src/constants.rs', lines 10:0-10:17 *) let x2_body : result u32 = Return 3 -let x2 : u32 = eval_global (x2_body) +let x2 : u32 = eval_global x2_body (** [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 *) @@ -28,7 +28,7 @@ let incr (n : u32) : result u32 = (** [constants::X3] Source: 'src/constants.rs', lines 15:0-15:17 *) let x3_body : result u32 = incr 32 -let x3 : u32 = eval_global (x3_body) +let x3 : u32 = eval_global x3_body (** [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 *) @@ -47,22 +47,22 @@ let mk_pair1 (x : u32) (y1 : u32) : result (pair_t u32 u32) = (** [constants::P0] Source: 'src/constants.rs', lines 31:0-31:24 *) let p0_body : result (u32 & u32) = mk_pair0 0 1 -let p0 : (u32 & u32) = eval_global (p0_body) +let p0 : (u32 & u32) = eval_global p0_body (** [constants::P1] Source: 'src/constants.rs', lines 32:0-32:28 *) let p1_body : result (pair_t u32 u32) = mk_pair1 0 1 -let p1 : pair_t u32 u32 = eval_global (p1_body) +let p1 : pair_t u32 u32 = eval_global p1_body (** [constants::P2] Source: 'src/constants.rs', lines 33:0-33:24 *) let p2_body : result (u32 & u32) = Return (0, 1) -let p2 : (u32 & u32) = eval_global (p2_body) +let p2 : (u32 & u32) = eval_global p2_body (** [constants::P3] Source: 'src/constants.rs', lines 34:0-34:28 *) let p3_body : result (pair_t u32 u32) = Return { x = 0; y = 1 } -let p3 : pair_t u32 u32 = eval_global (p3_body) +let p3 : pair_t u32 u32 = eval_global p3_body (** [constants::Wrap] Source: 'src/constants.rs', lines 49:0-49:18 *) @@ -76,7 +76,7 @@ let wrap_new (t : Type0) (value : t) : result (wrap_t t) = (** [constants::Y] Source: 'src/constants.rs', lines 41:0-41:22 *) let y_body : result (wrap_t i32) = wrap_new i32 2 -let y : wrap_t i32 = eval_global (y_body) +let y : wrap_t i32 = eval_global y_body (** [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 *) @@ -86,12 +86,12 @@ let unwrap_y : result i32 = (** [constants::YVAL] Source: 'src/constants.rs', lines 47:0-47:19 *) let yval_body : result i32 = unwrap_y -let yval : i32 = eval_global (yval_body) +let yval : i32 = eval_global yval_body (** [constants::get_z1::Z1] Source: 'src/constants.rs', lines 62:4-62:17 *) let get_z1_z1_body : result i32 = Return 3 -let get_z1_z1 : i32 = eval_global (get_z1_z1_body) +let get_z1_z1 : i32 = eval_global get_z1_z1_body (** [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 *) @@ -106,17 +106,17 @@ let add (a : i32) (b : i32) : result i32 = (** [constants::Q1] Source: 'src/constants.rs', lines 74:0-74:17 *) let q1_body : result i32 = Return 5 -let q1 : i32 = eval_global (q1_body) +let q1 : i32 = eval_global q1_body (** [constants::Q2] Source: 'src/constants.rs', lines 75:0-75:17 *) let q2_body : result i32 = Return q1 -let q2 : i32 = eval_global (q2_body) +let q2 : i32 = eval_global q2_body (** [constants::Q3] Source: 'src/constants.rs', lines 76:0-76:17 *) let q3_body : result i32 = add q2 3 -let q3 : i32 = eval_global (q3_body) +let q3 : i32 = eval_global q3_body (** [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 *) @@ -126,22 +126,22 @@ let get_z2 : result i32 = (** [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 *) let s1_body : result u32 = Return 6 -let s1 : u32 = eval_global (s1_body) +let s1 : u32 = eval_global s1_body (** [constants::S2] Source: 'src/constants.rs', lines 81:0-81:18 *) let s2_body : result u32 = incr s1 -let s2 : u32 = eval_global (s2_body) +let s2 : u32 = eval_global s2_body (** [constants::S3] Source: 'src/constants.rs', lines 82:0-82:29 *) let s3_body : result (pair_t u32 u32) = Return p3 -let s3 : pair_t u32 u32 = eval_global (s3_body) +let s3 : pair_t u32 u32 = eval_global s3_body (** [constants::S4] Source: 'src/constants.rs', lines 83:0-83:29 *) let s4_body : result (pair_t u32 u32) = mk_pair1 7 8 -let s4 : pair_t u32 u32 = eval_global (s4_body) +let s4 : pair_t u32 u32 = eval_global s4_body (** [constants::V] Source: 'src/constants.rs', lines 86:0-86:31 *) 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)#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)#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)#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)#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#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 3727e393..40f590d4 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -8,17 +8,17 @@ namespace constants /- [constants::X0] Source: 'src/constants.rs', lines 5:0-5:17 -/ def X0_body : Result U32 := Result.ret 0#u32 -def X0 : U32 := eval_global (X0_body) +def X0 : U32 := eval_global X0_body /- [constants::X1] Source: 'src/constants.rs', lines 7:0-7:17 -/ def X1_body : Result U32 := Result.ret core_u32_max -def X1 : U32 := eval_global (X1_body) +def X1 : U32 := eval_global X1_body /- [constants::X2] Source: 'src/constants.rs', lines 10:0-10:17 -/ def X2_body : Result U32 := Result.ret 3#u32 -def X2 : U32 := eval_global (X2_body) +def X2 : U32 := eval_global X2_body /- [constants::incr]: Source: 'src/constants.rs', lines 17:0-17:32 -/ @@ -28,7 +28,7 @@ def incr (n : U32) : Result U32 := /- [constants::X3] Source: 'src/constants.rs', lines 15:0-15:17 -/ def X3_body : Result U32 := incr 32#u32 -def X3 : U32 := eval_global (X3_body) +def X3 : U32 := eval_global X3_body /- [constants::mk_pair0]: Source: 'src/constants.rs', lines 23:0-23:51 -/ @@ -49,22 +49,22 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) := /- [constants::P0] Source: 'src/constants.rs', lines 31:0-31:24 -/ def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32 -def P0 : (U32 × U32) := eval_global (P0_body) +def P0 : (U32 × U32) := eval_global P0_body /- [constants::P1] Source: 'src/constants.rs', lines 32:0-32:28 -/ def P1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32 -def P1 : Pair U32 U32 := eval_global (P1_body) +def P1 : Pair U32 U32 := eval_global P1_body /- [constants::P2] Source: 'src/constants.rs', lines 33:0-33:24 -/ def P2_body : Result (U32 × U32) := Result.ret (0#u32, 1#u32) -def P2 : (U32 × U32) := eval_global (P2_body) +def P2 : (U32 × U32) := eval_global P2_body /- [constants::P3] Source: 'src/constants.rs', lines 34:0-34:28 -/ def P3_body : Result (Pair U32 U32) := Result.ret { x := 0#u32, y := 1#u32 } -def P3 : Pair U32 U32 := eval_global (P3_body) +def P3 : Pair U32 U32 := eval_global P3_body /- [constants::Wrap] Source: 'src/constants.rs', lines 49:0-49:18 -/ @@ -79,7 +79,7 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) := /- [constants::Y] Source: 'src/constants.rs', lines 41:0-41:22 -/ def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32 -def Y : Wrap I32 := eval_global (Y_body) +def Y : Wrap I32 := eval_global Y_body /- [constants::unwrap_y]: Source: 'src/constants.rs', lines 43:0-43:30 -/ @@ -89,12 +89,12 @@ def unwrap_y : Result I32 := /- [constants::YVAL] Source: 'src/constants.rs', lines 47:0-47:19 -/ def YVAL_body : Result I32 := unwrap_y -def YVAL : I32 := eval_global (YVAL_body) +def YVAL : I32 := eval_global YVAL_body /- [constants::get_z1::Z1] Source: 'src/constants.rs', lines 62:4-62:17 -/ def get_z1.Z1_body : Result I32 := Result.ret 3#i32 -def get_z1.Z1 : I32 := eval_global (get_z1.Z1_body) +def get_z1.Z1 : I32 := eval_global get_z1.Z1_body /- [constants::get_z1]: Source: 'src/constants.rs', lines 61:0-61:28 -/ @@ -109,17 +109,17 @@ def add (a : I32) (b : I32) : Result I32 := /- [constants::Q1] Source: 'src/constants.rs', lines 74:0-74:17 -/ def Q1_body : Result I32 := Result.ret 5#i32 -def Q1 : I32 := eval_global (Q1_body) +def Q1 : I32 := eval_global Q1_body /- [constants::Q2] Source: 'src/constants.rs', lines 75:0-75:17 -/ def Q2_body : Result I32 := Result.ret Q1 -def Q2 : I32 := eval_global (Q2_body) +def Q2 : I32 := eval_global Q2_body /- [constants::Q3] Source: 'src/constants.rs', lines 76:0-76:17 -/ def Q3_body : Result I32 := add Q2 3#i32 -def Q3 : I32 := eval_global (Q3_body) +def Q3 : I32 := eval_global Q3_body /- [constants::get_z2]: Source: 'src/constants.rs', lines 70:0-70:28 -/ @@ -132,22 +132,22 @@ def get_z2 : Result I32 := /- [constants::S1] Source: 'src/constants.rs', lines 80:0-80:18 -/ def S1_body : Result U32 := Result.ret 6#u32 -def S1 : U32 := eval_global (S1_body) +def S1 : U32 := eval_global S1_body /- [constants::S2] Source: 'src/constants.rs', lines 81:0-81:18 -/ def S2_body : Result U32 := incr S1 -def S2 : U32 := eval_global (S2_body) +def S2 : U32 := eval_global S2_body /- [constants::S3] Source: 'src/constants.rs', lines 82:0-82:29 -/ def S3_body : Result (Pair U32 U32) := Result.ret P3 -def S3 : Pair U32 U32 := eval_global (S3_body) +def S3 : Pair U32 U32 := eval_global S3_body /- [constants::S4] Source: 'src/constants.rs', lines 83:0-83:29 -/ def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32 -def S4 : Pair U32 U32 := eval_global (S4_body) +def S4 : Pair U32 U32 := eval_global S4_body /- [constants::V] Source: 'src/constants.rs', lines 86:0-86:31 -/ 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)#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)#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)#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)#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#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 -- cgit v1.2.3 From 59bc33b42009ef3a71b43c844f44cd632476e4fe Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Mar 2024 06:59:11 +0100 Subject: Fix a minor issue --- backends/lean/Base/Primitives/Base.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index d2695854..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 first | apply Eq.refl | 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 -- cgit v1.2.3 From 9e230d0c4378b5c992c820cc1f4322896f739095 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 18 Mar 2024 07:01:48 +0100 Subject: Update the flake.nix and the flake.lock --- flake.lock | 350 +------------------------------------------------------------ flake.nix | 21 +--- 2 files changed, 4 insertions(+), 367 deletions(-) diff --git a/flake.lock b/flake.lock index 48273b6a..9bbf68bc 100644 --- a/flake.lock +++ b/flake.lock @@ -8,11 +8,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1710648057, - "narHash": "sha256-Jm5EZsXXIhAhDHAA1jZx4TYPpKREGZBNAUeqpiufbPo=", + "lastModified": 1710741599, + "narHash": "sha256-/5o81Ifs6OGqNpxMklGCJ6w2CVQrQn+xMaC1VrC8pZE=", "owner": "aeneasverif", "repo": "charon", - "rev": "a3ba8b5286ef99584e87035cb965d3cb9c43660c", + "rev": "f3faf02ec1dbd6645b816d54be39261dea6970c2", "type": "github" }, "original": { @@ -77,54 +77,6 @@ "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", @@ -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": 1710638987, - "narHash": "sha256-88u7WVtuwQwd4yjUXUJouMBd2W6meLg0C2k9Kv8PuYM=", - "owner": "leanprover", - "repo": "lean4", - "rev": "9ee10aa3ebb8e518132873e3d98a13dd7df5e9f7", - "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": 1710638987, - "narHash": "sha256-88u7WVtuwQwd4yjUXUJouMBd2W6meLg0C2k9Kv8PuYM=", - "owner": "leanprover", - "repo": "lean4", - "rev": "9ee10aa3ebb8e518132873e3d98a13dd7df5e9f7", - "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; }; }); } -- cgit v1.2.3