diff --git a/.github/workflows/charon.yml b/.github/workflows/charon.yml deleted file mode 100644 index bda7df442..000000000 --- a/.github/workflows/charon.yml +++ /dev/null @@ -1,17 +0,0 @@ -on: - pull_request: - workflow_dispatch: - -jobs: - charon: - runs-on: ubuntu-latest - steps: - - uses: DeterminateSystems/nix-installer-action@main - - uses: actions/checkout@v4 - with: - repository: AeneasVerif/charon - - run: | - cd charon - cargo update -p hax-frontend-exporter --precise ${{ github.sha }} - cargo update -p hax-frontend-exporter-options --precise ${{ github.sha }} - - run: nix build -L diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs index a7f1d4e2c..2ec019b8f 100644 --- a/cli/driver/src/driver.rs +++ b/cli/driver/src/driver.rs @@ -1,6 +1,5 @@ #![feature(rustc_private)] #![feature(box_patterns)] -#![feature(concat_idents)] #![feature(trait_alias)] #![allow(unused_imports)] #![allow(unused_variables)] diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 0040f9cbc..2bf0f73f3 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -1086,6 +1086,7 @@ open Phase_utils module TransformToInputLanguage = [%functor_application Phases.Reject.Unsafe(Features.Rust) + |> Phases.Drop_metasized |> Phases.Reject.RawOrMutPointer |> Phases.And_mut_defsite |> Phases.Reconstruct_asserts diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index 867af31b6..f6057deb3 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/engine/backends/coq/ssprove/ssprove_backend.ml @@ -555,6 +555,7 @@ open Phase_utils module TransformToInputLanguage = [%functor_application Phases.Reject.Unsafe(Features.Rust) + |> Phases.Drop_metasized |> Phases.Reject.RawOrMutPointer |> Phases.And_mut_defsite |> Phases.Reconstruct_asserts diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 7e1e49494..dd790222f 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1911,6 +1911,7 @@ module DepGraphR = Dependencies.Make (Features.Rust) module TransformToInputLanguage = [%functor_application Phases.Reject.RawOrMutPointer(Features.Rust) + |> Phases.Drop_metasized |> Phases.Transform_hax_lib_inline |> Phases.Specialize |> Phases.Drop_sized_trait diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 4ec084c1e..d49531cdd 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -887,6 +887,7 @@ module DepGraphR = Dependencies.Make (Features.Rust) module TransformToInputLanguage = [%functor_application Phases.Reject.Unsafe(Features.Rust) + |> Phases.Drop_metasized |> Phases.Reject.RawOrMutPointer |> Phases.Transform_hax_lib_inline |> Phases.Simplify_question_marks diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 821b30d8f..db9297f8b 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -118,6 +118,10 @@ let c_attr (attr : Thir.attribute) : attr option = in let kind = DocComment { kind; body = comment } in Some { kind; span = Span.of_thir span } + | Parsed (AutomaticallyDerived span) -> + (* Restore behavior before PR #1534 *) + let kind = Tool { path = "automatically_derived"; tokens = "" } in + Some { kind; span = Span.of_thir span } | Unparsed { args = Eq { expr = { symbol; _ }; _ }; path = "doc"; span; _ } -> (* Looks for `#[doc = "something"]` *) let kind = DocComment { kind = DCKLine; body = symbol } in @@ -1105,8 +1109,6 @@ end) : EXPR = struct match non_traits with | [] -> TDyn { witness = W.dyn; goals } | _ -> assertion_failure [ span ] "type Dyn with non trait predicate") - | Dynamic (_, _, DynStar) -> - unimplemented ~issue_id:931 [ span ] "type DynStar" | Coroutine _ -> unimplemented ~issue_id:924 [ span ] "Got type `Coroutine`: coroutines are not supported by hax" @@ -1377,7 +1379,7 @@ let is_automatically_derived (attrs : Thir.attribute list) = ~f:(function (* This will break once these attributes get properly parsed. It will then be very easy to parse them correctly *) - | Unparsed { path; _ } -> String.equal path "automatically_derived" + | Parsed (AutomaticallyDerived _) -> true | _ -> false) attrs @@ -1516,7 +1518,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = in (* TODO: things might be unnamed (e.g. constants) *) match (item.kind : Thir.item_kind) with - | Const (_, _, generics, body) -> + | Const (_, generics, _, body) -> mk @@ Fn { @@ -1526,14 +1528,14 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = params = []; safety = Safe; } - | Static (_, _, true, _) -> + | Static (true, _, _, _) -> unimplemented ~issue_id:1343 [ item.span ] "Mutable static items are not supported." - | Static (_, _ty, false, body) -> + | Static (false, _, _ty, body) -> let name = Concrete_ident.of_def_id ~value:true (assert_item_def_id ()) in let generics = { params = []; constraints = [] } in mk (Fn { name; generics; body = c_body body; params = []; safety = Safe }) - | TyAlias (_, ty, generics) -> + | TyAlias (_, generics, ty) -> mk @@ TyAlias { @@ -1552,13 +1554,13 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = params = c_fn_params item.span params; safety = c_header_safety safety; } - | (Enum (_, _, generics, _) | Struct (_, _, generics)) when erased -> + | (Enum (_, generics, _, _) | Struct (_, generics, _)) when erased -> let generics = c_generics generics in let is_struct = match item.kind with Struct _ -> true | _ -> false in let def_id = assert_item_def_id () in let name = Concrete_ident.of_def_id ~value:false def_id in mk @@ Type { name; generics; variants = []; is_struct } - | Enum (_, variants, generics, repr) -> + | Enum (_, generics, variants, repr) -> let def_id = assert_item_def_id () in let generics = c_generics generics in let is_struct = false in @@ -1616,7 +1618,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = mk_one (Type { name; generics; variants; is_struct }) :: discs in if is_primitive then cast_fun :: result else result - | Struct (_, v, generics) -> + | Struct (_, generics, v) -> let generics = c_generics generics in let def_id = assert_item_def_id () in let is_struct = true in @@ -1643,7 +1645,7 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let variants = [ v ] in let name = Concrete_ident.of_def_id ~value:false def_id in mk @@ Type { name; generics; variants; is_struct } - | Trait (No, safety, _, generics, _bounds, items) -> + | Trait (NotConst, No, safety, _, generics, _bounds, items) -> let items = List.filter ~f:(fun { attributes; _ } -> not (should_skip attributes)) @@ -1666,8 +1668,10 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = let items = List.map ~f:c_trait_item items in let safety = csafety safety in mk @@ Trait { name; generics; items; safety } - | Trait (Yes, _, _, _, _, _) -> + | Trait (_, Yes, _, _, _, _, _) -> unimplemented ~issue_id:930 [ item.span ] "Auto trait" + | Trait (Const, _, _, _, _, _, _) -> + unimplemented ~issue_id:930 [ item.span ] "Const trait" | Impl { of_trait = None; generics; items; _ } -> let items = List.filter @@ -1814,7 +1818,9 @@ and c_item_unwrapped ~ident ~type_only (item : Thir.item) : item list = { path = List.map ~f:(fun x -> fst x.ident) segments; is_external = - List.exists ~f:(function Err -> true | _ -> false) res; + List.exists + ~f:(function None | Some Err -> true | _ -> false) + res; (* TODO: this should represent local/external? *) rename; } diff --git a/engine/lib/phases/phase_drop_metasized.ml b/engine/lib/phases/phase_drop_metasized.ml new file mode 100644 index 000000000..5e1ebd77d --- /dev/null +++ b/engine/lib/phases/phase_drop_metasized.ml @@ -0,0 +1,193 @@ +(** This phase gets rid of the MetaSized bound. See + https://github.com/cryspen/hax/pull/1534. *) + +open! Prelude + +module%inlined_contents Make (F : Features.T) = struct + open Ast + module FA = F + module FB = FA + + include + Phase_utils.MakeBase (F) (FB) + (struct + let phase_id = [%auto_phase_name auto] + end) + + module UA = Ast_utils.Make (F) + + module Implem : ImplemT.T = struct + let metadata = metadata + + module S = struct + include Features.SUBTYPE.Id + end + + [%%inline_defs dmutability + dsafety_kind] + + let rec dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr option = + let* kind = dimpl_expr_kind span i.kind in + let* goal = dtrait_goal span i.goal in + Some B.{ kind; goal } + + and dtrait_goal (span : span) (r : A.trait_goal) : B.trait_goal option = + let*? _ = not (Concrete_ident.eq_name Core__marker__MetaSized r.trait) in + Some + B.{ trait = r.trait; args = List.map ~f:(dgeneric_value span) r.args } + + and dimpl_expr_exn message span i = + match dimpl_expr span i with + | None -> Error.assertion_failure span message + | Some impl -> impl + + and dimpl_ident (span : span) (r : A.impl_ident) : B.impl_ident option = + let* goal = dtrait_goal span r.goal in + Some B.{ goal; name = r.name } + + and dty (span : span) (ty : A.ty) : B.ty = + match ty with + | TAssociatedType { impl; item } -> + let impl = + dimpl_expr_exn "MetaSized has no associated type" span impl + in + TAssociatedType { impl; item } + | [%inline_arms "dty.*" - TAssociatedType] -> auto + + and dprojection_predicate (span : span) (r : A.projection_predicate) : + B.projection_predicate = + { + impl = dimpl_expr_exn "MetaSized cannot be projected" span r.impl; + assoc_item = r.assoc_item; + typ = dty span r.typ; + } + + and dimpl_expr_kind (span : span) (i : A.impl_expr_kind) : + B.impl_expr_kind option = + match i with + | Parent { impl; ident } -> + let* impl = dimpl_expr span impl in + let* ident = dimpl_ident span ident in + Some (B.Parent { impl; ident }) + | Projection { impl; item; ident } -> + let impl = dimpl_expr_exn "MetaSized have no projection" span impl in + let* ident = dimpl_ident span ident in + Some (B.Projection { impl; item; ident }) + | ImplApp { impl; args } -> + let* impl = dimpl_expr span impl in + let args = List.filter_map ~f:(dimpl_expr span) args in + Some (B.ImplApp { impl; args }) + | Builtin tr -> + let* tr = dtrait_goal span tr in + Some (B.Builtin tr) + | Concrete tr -> + let* tr = dtrait_goal span tr in + Some (B.Concrete tr) + | [%inline_arms + "dimpl_expr_kind.*" - Parent - Projection - ImplApp - Builtin + - Concrete] -> + map (fun x -> + Some + (let result : B.impl_expr_kind = x in + result)) + + and dexpr' (span : span) (expr : A.expr') : B.expr' = + match expr with + | App { f; args; generic_args; bounds_impls; trait } -> + let dgeneric_values = List.map ~f:(dgeneric_value span) in + App + { + f = dexpr f; + args = List.map ~f:dexpr args; + generic_args = dgeneric_values generic_args; + bounds_impls = List.filter_map ~f:(dimpl_expr span) bounds_impls; + trait = + Option.map + ~f: + (dimpl_expr_exn "MetaSized have no method" span + *** dgeneric_values) + trait; + } + | [%inline_arms "dexpr'.*" - App] -> auto + [@@inline_ands + bindings_of dty - dimpl_expr - dexpr' - dprojection_predicate + - dimpl_expr_kind - dty - dimpl_ident] + + let rec dimpl_item' (span : span) (ii : A.impl_item') : B.impl_item' = + match ii with + | IIType { typ; parent_bounds } -> + IIType + { + typ = dty span typ; + parent_bounds = + List.filter_map + ~f:(fun (impl, ident) -> + let* impl = dimpl_expr span impl in + let* ident = dimpl_ident span ident in + Some (impl, ident)) + parent_bounds; + } + (* | _ -> Obj.magic () *) + | [%inline_arms "dimpl_item'.*" - IIType] -> auto + + and dtrait_item' (span : span) (ti : A.trait_item') : B.trait_item' = + match ti with + | TIType idents -> TIType (List.filter_map ~f:(dimpl_ident span) idents) + | [%inline_arms "dtrait_item'.*" - TIType] -> auto + + and dgeneric_constraint (span : span) + (generic_constraint : A.generic_constraint) : + B.generic_constraint option = + match generic_constraint with + | GCLifetime (lf, witness) -> + Some (B.GCLifetime (lf, S.lifetime span witness)) + | GCType impl_ident -> + let* impl = dimpl_ident span impl_ident in + Some (B.GCType impl) + | GCProjection projection -> + Some (B.GCProjection (dprojection_predicate span projection)) + + and dgenerics (span : span) (g : A.generics) : B.generics = + { + params = List.map ~f:(dgeneric_param span) g.params; + constraints = + List.filter_map ~f:(dgeneric_constraint span) g.constraints; + } + + and ditem' (span : span) (item : A.item') : B.item' = + match item with + | Impl + { + generics; + self_ty; + of_trait = trait_id, trait_generics; + items; + parent_bounds; + safety; + } -> + B.Impl + { + generics = dgenerics span generics; + self_ty = dty span self_ty; + of_trait = + (trait_id, List.map ~f:(dgeneric_value span) trait_generics); + items = List.map ~f:dimpl_item items; + parent_bounds = + List.filter_map + ~f:(fun (impl, ident) -> + let* impl = dimpl_expr span impl in + let* ident = dimpl_ident span ident in + Some (impl, ident)) + parent_bounds; + safety = dsafety_kind span safety; + } + | [%inline_arms "ditem'.*" - Impl] -> auto + [@@inline_ands + "Item.*" - ditem' - dimpl_item' - dtrait_item' - dgeneric_constraint + - dgenerics] + + [%%inline_defs ditems] + end + + include Implem +end +[@@add "subtype.ml"] diff --git a/engine/lib/phases/phase_drop_metasized.mli b/engine/lib/phases/phase_drop_metasized.mli new file mode 100644 index 000000000..01bb072cc --- /dev/null +++ b/engine/lib/phases/phase_drop_metasized.mli @@ -0,0 +1,16 @@ +(** This phase gets rid of the MetaSized bound. See + https://github.com/cryspen/hax/pull/1534. *) + +open! Prelude + +module Make (F : Features.T) : sig + include module type of struct + module FA = F + module FB = FA + module A = Ast.Make (F) + module B = Ast.Make (FB) + module ImplemT = Phase_utils.MakePhaseImplemT (A) (B) + end + + include ImplemT.T +end diff --git a/flake.lock b/flake.lock index 539def0d4..9ce04a43b 100644 --- a/flake.lock +++ b/flake.lock @@ -150,11 +150,11 @@ ] }, "locked": { - "lastModified": 1752720268, - "narHash": "sha256-XCiJdtXIN09Iv0i1gs5ajJ9CVHk537Gy1iG/4nIdpVI=", + "lastModified": 1753066249, + "narHash": "sha256-j2UBrfDRIePGx3532Bbb9UeosNX2F73hfOAHtmACfnM=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "dc221f842e9ddc8c0416beae8d77f2ea356b91ae", + "rev": "0751b65633a1785743ca44fd7c14a633c54c1f91", "type": "github" }, "original": { diff --git a/frontend/exporter/Cargo.toml b/frontend/exporter/Cargo.toml index 35ed4c09a..f19eb4381 100644 --- a/frontend/exporter/Cargo.toml +++ b/frontend/exporter/Cargo.toml @@ -1,10 +1,10 @@ [package] name = "hax-frontend-exporter" +edition = "2024" version.workspace = true authors.workspace = true license.workspace = true homepage.workspace = true -edition.workspace = true repository.workspace = true readme.workspace = true description = "Provides mirrors of the algebraic data types used in the Rust compilers, removing indirections and inlining various pieces of information." diff --git a/frontend/exporter/src/comments.rs b/frontend/exporter/src/comments.rs index 0baecd941..08bfcc102 100644 --- a/frontend/exporter/src/comments.rs +++ b/frontend/exporter/src/comments.rs @@ -21,7 +21,7 @@ pub fn comments_of_file(path: PathBuf) -> std::io::Result> { let mut comments = vec![]; let (mut pos, mut line, mut col) = (0, 0, 0); - for token in rustc_lexer::tokenize(source) { + for token in rustc_lexer::tokenize(source, rustc_lexer::FrontmatterAllowed::Yes) { let len = token.len as usize; let sub = &source[pos..(pos + len)]; let lo = Loc { line, col }; diff --git a/frontend/exporter/src/constant_utils/uneval.rs b/frontend/exporter/src/constant_utils/uneval.rs index 33d18f07d..8f41b2392 100644 --- a/frontend/exporter/src/constant_utils/uneval.rs +++ b/frontend/exporter/src/constant_utils/uneval.rs @@ -154,7 +154,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::Const<'tcx> let span = self.default_span(s.base().tcx); match self.kind() { ty::ConstKind::Param(p) => { - let ty = p.find_ty_from_env(s.param_env()); + let ty = p.find_const_ty_from_env(s.param_env()); let kind = ConstantExprKind::ConstRef { id: p.sinto(s) }; kind.decorate(ty.sinto(s), span.sinto(s)) } @@ -279,7 +279,7 @@ fn op_to_const<'tcx, S: UnderOwnerState<'tcx>>( // Helper for struct-likes. let read_fields = |of: rustc_const_eval::interpret::OpTy<'tcx>, field_count| { (0..field_count).map(move |i| { - let field_op = ecx.project_field(&of, i)?; + let field_op = ecx.project_field(&of, rustc_abi::FieldIdx::from_usize(i))?; op_to_const(s, span, &ecx, field_op) }) }; diff --git a/frontend/exporter/src/lib.rs b/frontend/exporter/src/lib.rs index fe3b58896..ef6af0388 100644 --- a/frontend/exporter/src/lib.rs +++ b/frontend/exporter/src/lib.rs @@ -1,9 +1,8 @@ #![allow(rustdoc::private_intra_doc_links)] -#![cfg_attr(feature = "rustc", feature(concat_idents))] #![cfg_attr(feature = "rustc", feature(if_let_guard))] -#![cfg_attr(feature = "rustc", feature(let_chains))] #![cfg_attr(feature = "rustc", feature(macro_metavar_expr))] #![cfg_attr(feature = "rustc", feature(rustc_private))] +#![cfg_attr(feature = "rustc", feature(sized_hierarchy))] #![cfg_attr(feature = "rustc", feature(trait_alias))] #![cfg_attr(feature = "rustc", feature(type_changing_struct_update))] diff --git a/frontend/exporter/src/sinto.rs b/frontend/exporter/src/sinto.rs index fc58f735f..3e775ceac 100644 --- a/frontend/exporter/src/sinto.rs +++ b/frontend/exporter/src/sinto.rs @@ -1,9 +1,13 @@ -use crate::prelude::{derive_group, JsonSchema}; - +#[cfg(not(feature = "rustc"))] pub trait SInto { fn sinto(&self, s: &S) -> To; } +#[cfg(feature = "rustc")] +pub trait SInto: std::marker::PointeeSized { + fn sinto(&self, s: &S) -> To; +} + #[macro_export] macro_rules! sinto_todo { ($($mod:ident)::+, $type:ident$(<$($lts:lifetime),*$(,)?>)? as $renamed:ident) => { @@ -39,20 +43,6 @@ macro_rules! sinto_as_usize { } } -#[allow(dead_code)] -mod test { - #[derive(Debug)] - pub struct Foo(usize); - impl Foo { - pub fn as_usize(&self) -> usize { - self.0 - } - } -} - -sinto_todo!(test, Foo); -// sinto_as_usize!(test, Foo); - impl, R: SInto> SInto for (L, R) { fn sinto(&self, s: &S) -> (LL, RR) { (self.0.sinto(s), self.1.sinto(s)) diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 453a811ae..2b72db07d 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -677,7 +677,7 @@ pub fn shallow_resolve_trait_ref<'tcx>( use rustc_middle::traits::CodegenObligationError; use rustc_middle::ty::TypeVisitableExt; use rustc_trait_selection::traits::{ - Obligation, ObligationCause, ObligationCtxt, SelectionContext, Unimplemented, + Obligation, ObligationCause, ObligationCtxt, SelectionContext, SelectionError, }; // Do the initial selection for the obligation. This yields the // shallow result we are looking for -- that is, what specific impl. @@ -693,7 +693,7 @@ pub fn shallow_resolve_trait_ref<'tcx>( let selection = match selcx.poly_select(&obligation) { Ok(Some(selection)) => selection, Ok(None) => return Err(CodegenObligationError::Ambiguity), - Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented), + Err(SelectionError::Unimplemented) => return Err(CodegenObligationError::Unimplemented), Err(_) => return Err(CodegenObligationError::Ambiguity), }; diff --git a/frontend/exporter/src/types/attributes.rs b/frontend/exporter/src/types/attributes.rs new file mode 100644 index 000000000..46daa568b --- /dev/null +++ b/frontend/exporter/src/types/attributes.rs @@ -0,0 +1,97 @@ +//! Copies of the types related to attributes. +//! Such types are mostly contained in the crate `rustc_attr_data_structures`. + +use crate::prelude::*; + +/// Reflects [`rustc_attr_data_structures::AttributeKind`] +#[derive(AdtInto)] +#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::AttributeKind, state: S as tcx)] +#[derive_group(Serializers)] +#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] +pub enum AttributeKind { + Align { + align: Align, + span: Span, + }, + AutomaticallyDerived(Span), + Coverage(Span, CoverageStatus), + Deprecation { + deprecation: Deprecation, + span: Span, + }, + DocComment { + style: AttrStyle, + kind: CommentKind, + span: Span, + comment: Symbol, + }, + Ignore { + span: Span, + reason: Option, + }, + Marker(Span), + MayDangle(Span), + MustUse { + span: Span, + reason: Option, + }, + Path(Symbol, Span), + #[todo] + Todo(String), +} + +/// Reflects [`rustc_attr_data_structures::Deprecation`] +#[derive_group(Serializers)] +#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] +#[args(<'tcx, S>, from: rustc_attr_data_structures::Deprecation, state: S as _s)] +pub struct Deprecation { + pub since: DeprecatedSince, + pub note: Option, + pub suggestion: Option, +} + +/// Reflects [`rustc_attr_data_structures::DeprecatedSince`] +#[derive_group(Serializers)] +#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] +#[args(<'tcx, S>, from: rustc_attr_data_structures::DeprecatedSince, state: S as _s)] +pub enum DeprecatedSince { + RustcVersion(RustcVersion), + Future, + NonStandard(Symbol), + Unspecified, + Err, +} + +/// Reflects [`rustc_attr_data_structures::RustcVersion`] +#[derive_group(Serializers)] +#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] +#[args(<'tcx, S>, from: rustc_attr_data_structures::RustcVersion, state: S as _s)] +pub struct RustcVersion { + pub major: u16, + pub minor: u16, + pub patch: u16, +} + +/// Reflects [`rustc_attr_data_structures::CoverageStatus`] +#[derive_group(Serializers)] +#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] +#[args(<'tcx, S>, from: rustc_attr_data_structures::CoverageStatus, state: S as _s)] +pub enum CoverageStatus { + On, + Off, +} + +/// Reflects [`rustc_attr_data_structures::InlineAttr`] +#[derive_group(Serializers)] +#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] +#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::InlineAttr, state: S as _s)] +pub enum InlineAttr { + None, + Hint, + Always, + Never, + Force { + attr_span: Span, + reason: Option, + }, +} diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index c0a10edc5..14196789c 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -21,6 +21,8 @@ use crate::{AdtInto, JsonSchema}; use {rustc_hir as hir, rustc_hir::def_id::DefId as RDefId, rustc_middle::ty}; pub type Symbol = String; +#[cfg(not(feature = "extract_names_mode"))] +pub type ByteSymbol = Vec; #[cfg(all(not(feature = "extract_names_mode"), feature = "rustc"))] impl<'t, S> SInto for rustc_span::symbol::Symbol { @@ -29,6 +31,13 @@ impl<'t, S> SInto for rustc_span::symbol::Symbol { } } +#[cfg(all(not(feature = "extract_names_mode"), feature = "rustc"))] +impl<'t, S> SInto for rustc_span::symbol::ByteSymbol { + fn sinto(&self, _s: &S) -> ByteSymbol { + self.as_byte_str().to_owned() + } +} + /// Reflects [`hir::Safety`] #[cfg_attr(not(feature = "extract_names_mode"), derive(AdtInto, JsonSchema))] #[cfg_attr(not(feature = "extract_names_mode"), args(, from: hir::Safety, state: S as _s))] diff --git a/frontend/exporter/src/types/hir.rs b/frontend/exporter/src/types/hir.rs index e4b5a747b..efa665ea0 100644 --- a/frontend/exporter/src/types/hir.rs +++ b/frontend/exporter/src/types/hir.rs @@ -225,10 +225,10 @@ pub struct Generics { } #[cfg(feature = "rustc")] -impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto> for hir::ImplItemRef { +impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto> for hir::ImplItemId { fn sinto(&self, s: &S) -> ImplItem { let tcx: rustc_middle::ty::TyCtxt = s.base().tcx; - let impl_item = tcx.hir_impl_item(self.id); + let impl_item = tcx.hir_impl_item(*self); let s = with_owner_id(s.base(), (), (), impl_item.owner_id.to_def_id()); impl_item.sinto(&s) } @@ -393,17 +393,6 @@ pub enum ImplItemKind { }, } -/// Reflects [`hir::AssocItemKind`] -#[derive(AdtInto)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: hir::AssocItemKind, state: S as tcx)] -#[derive_group(Serializers)] -#[derive(Clone, Debug, JsonSchema)] -pub enum AssocItemKind { - Const, - Fn { has_self: bool }, - Type, -} - /// Reflects [`hir::Impl`]. #[derive(AdtInto)] #[args(<'tcx, S: UnderOwnerState<'tcx> >, from: hir::Impl<'tcx>, state: S as s)] @@ -535,7 +524,7 @@ pub struct Variant { pub struct UsePath { pub span: Span, #[map(x.iter().map(|res| res.sinto(s)).collect())] - pub res: Vec, + pub res: Vec>, pub segments: Vec, #[value(self.segments.iter().last().and_then(|segment| { match s.base().tcx.hir_node_by_def_id(segment.hir_id.owner.def_id) { @@ -620,8 +609,8 @@ pub struct PathSegment { pub enum ItemKind { ExternCrate(Option, Ident), Use(UsePath, UseKind), - Static(Ident, Ty, Mutability, Body), - Const(Ident, Ty, Generics, Body), + Static(Mutability, Ident, Ty, Body), + Const(Ident, Generics, Ty, Body), #[custom_arm( hir::ItemKind::Fn{ ident, sig, generics, body, .. } => { ItemKind::Fn { @@ -648,6 +637,7 @@ pub enum ItemKind { }, TyAlias( Ident, + Generics, #[map({ let s = &State { base: Base {ty_alias_mode: true, ..s.base()}, @@ -659,21 +649,21 @@ pub enum ItemKind { x.sinto(s) })] Ty, - Generics, ), Enum( Ident, - EnumDef, Generics, + EnumDef, #[value({ let tcx = s.base().tcx; tcx.repr_options_of_def(s.owner_id().expect_local()).sinto(s) })] ReprOptions, ), - Struct(Ident, VariantData, Generics), - Union(Ident, VariantData, Generics), + Struct(Ident, Generics, VariantData), + Union(Ident, Generics, VariantData), Trait( + Constness, IsAuto, Safety, Ident, @@ -741,11 +731,11 @@ impl<'tcx, S: UnderOwnerState<'tcx>, Body: IsBody> SInto> for h } #[cfg(feature = "rustc")] -impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto> for hir::TraitItemRef { +impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto> for hir::TraitItemId { fn sinto(&self, s: &S) -> TraitItem { - let s = with_owner_id(s.base(), (), (), self.id.owner_id.to_def_id()); + let s = with_owner_id(s.base(), (), (), self.owner_id.to_def_id()); let tcx: rustc_middle::ty::TyCtxt = s.base().tcx; - tcx.hir_trait_item(self.id).sinto(&s) + tcx.hir_trait_item(*self).sinto(&s) } } @@ -785,10 +775,10 @@ pub struct ForeignItem { } #[cfg(feature = "rustc")] -impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto> for hir::ForeignItemRef { +impl<'a, S: UnderOwnerState<'a>, Body: IsBody> SInto> for hir::ForeignItemId { fn sinto(&self, s: &S) -> ForeignItem { let tcx: rustc_middle::ty::TyCtxt = s.base().tcx; - tcx.hir_foreign_item(self.id).sinto(s) + tcx.hir_foreign_item(*self).sinto(s) } } @@ -916,7 +906,7 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto> for hir::Item< let name = match self.kind { ExternCrate(_, i) | Use(_, hir::UseKind::Single(i)) - | Static(i, ..) + | Static(_, i, ..) | Const(i, ..) | Fn { ident: i, .. } | Macro(i, ..) @@ -925,7 +915,7 @@ impl<'tcx, S: BaseState<'tcx>, Body: IsBody> SInto> for hir::Item< | Enum(i, ..) | Struct(i, ..) | Union(i, ..) - | Trait(_, _, i, ..) + | Trait(_, _, _, i, ..) | TraitAlias(i, ..) => i.name.to_ident_string(), Use(..) | ForeignMod { .. } | GlobalAsm { .. } | Impl { .. } => String::new(), }; @@ -980,38 +970,6 @@ pub enum Attribute { Parsed(AttributeKind), Unparsed(AttrItem), } - -/// Reflects [`rustc_attr_data_structures::AttributeKind`] -#[derive(AdtInto)] -#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::AttributeKind, state: S as tcx)] -#[derive_group(Serializers)] -#[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -pub enum AttributeKind { - DocComment { - style: AttrStyle, - kind: CommentKind, - span: Span, - comment: Symbol, - }, - #[todo] - Other(String), -} - -/// Reflects [`rustc_attr_data_structures::InlineAttr`] -#[derive_group(Serializers)] -#[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_attr_data_structures::InlineAttr, state: S as _s)] -pub enum InlineAttr { - None, - Hint, - Always, - Never, - Force { - attr_span: Span, - reason: Option, - }, -} - /// Reflects [`rustc_ast::ast::BindingMode`] #[derive(AdtInto)] #[args(, from: rustc_ast::ast::BindingMode, state: S as s)] @@ -1051,8 +1009,8 @@ pub enum StrStyle { #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] pub enum LitKind { Str(Symbol, StrStyle), - ByteStr(Vec, StrStyle), - CStr(Vec, StrStyle), + ByteStr(ByteSymbol, StrStyle), + CStr(ByteSymbol, StrStyle), Byte(u8), Char(char), Int( diff --git a/frontend/exporter/src/types/mod.rs b/frontend/exporter/src/types/mod.rs index e70f2ce3c..7c1787389 100644 --- a/frontend/exporter/src/types/mod.rs +++ b/frontend/exporter/src/types/mod.rs @@ -1,6 +1,4 @@ -// There's a conflict between `mir::ScalarInt`and `todo::ScalarInt` but it doesn't matter. -#![allow(ambiguous_glob_reexports)] - +mod attributes; mod def_id; mod hir; mod mir; @@ -10,6 +8,7 @@ mod span; mod thir; mod ty; +pub use attributes::*; pub use def_id::*; pub use hir::*; pub use mir::*; diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 951150d21..953d4f0fb 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -217,7 +217,7 @@ pub enum FullDefKind { /// `Some` if the item is in the local crate. #[value(s.base().tcx.hir_get_if_local(s.owner_id()).map(|node| { let rustc_hir::Node::Item(item) = node else { unreachable!() }; - let rustc_hir::ItemKind::TyAlias(_, ty, _generics) = &item.kind else { unreachable!() }; + let rustc_hir::ItemKind::TyAlias(_, _generics, ty) = &item.kind else { unreachable!() }; let mut s = State::from_under_owner(s); s.base.ty_alias_mode = true; ty.sinto(&s) @@ -735,7 +735,7 @@ fn get_foreign_mod_children<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> Vec< .expect_foreign_mod() .1 .iter() - .map(|foreign_item_ref| foreign_item_ref.id.owner_id.to_def_id()) + .map(|foreign_item_ref| foreign_item_ref.owner_id.to_def_id()) .collect(), None => vec![], } @@ -981,7 +981,8 @@ fn closure_once_shim<'tcx>( #[cfg(feature = "rustc")] fn drop_glue_shim<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> Option> { - let drop_in_place = tcx.require_lang_item(rustc_hir::LangItem::DropInPlace, None); + let drop_in_place = + tcx.require_lang_item(rustc_hir::LangItem::DropInPlace, rustc_span::DUMMY_SP); if !tcx.generics_of(def_id).is_empty() { // Hack: layout code panics if it can't fully normalize types, which can happen e.g. with a // trait associated type. For now we only translate the glue for monomorphic types. diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index 0438ab5ee..bf71fb173 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -94,22 +94,22 @@ pub struct ExistentialProjection { #[args(, from: ty::DynKind, state: S as _s)] pub enum DynKind { Dyn, - DynStar, } /// Reflects [`ty::BoundTyKind`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind, state: S as s)] pub enum BoundTyKind { Anon, + #[custom_arm(&FROM_TYPE::Param(def_id) => TO_TYPE::Param(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)] Param(DefId, Symbol), } /// Reflects [`ty::BoundTy`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy, state: S as s)] pub struct BoundTy { pub var: BoundVar, pub kind: BoundTyKind, @@ -120,9 +120,11 @@ sinto_as_usize!(rustc_middle::ty, BoundVar); /// Reflects [`ty::BoundRegionKind`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind, state: S as s)] pub enum BoundRegionKind { Anon, + NamedAnon(Symbol), + #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)] Named(DefId, Symbol), ClosureEnv, } @@ -130,7 +132,7 @@ pub enum BoundRegionKind { /// Reflects [`ty::BoundRegion`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion, state: S as s)] pub struct BoundRegion { pub var: BoundVar, pub kind: BoundRegionKind, @@ -370,7 +372,7 @@ impl VariantDef { /// Reflects [`ty::EarlyParamRegion`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::EarlyParamRegion, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::EarlyParamRegion, state: S as s)] pub struct EarlyParamRegion { pub index: u32, pub name: Symbol, @@ -379,7 +381,7 @@ pub struct EarlyParamRegion { /// Reflects [`ty::LateParamRegion`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegion, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegion, state: S as s)] pub struct LateParamRegion { pub scope: DefId, pub kind: LateParamRegionKind, @@ -388,9 +390,11 @@ pub struct LateParamRegion { /// Reflects [`ty::LateParamRegionKind`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegionKind, state: S as gstate)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegionKind, state: S as s)] pub enum LateParamRegionKind { Anon(u32), + NamedAnon(u32, Symbol), + #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)] Named(DefId, Symbol), ClosureEnv, } @@ -544,14 +548,14 @@ impl std::ops::Deref for ItemRef { #[cfg(feature = "rustc")] impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::GenericArg<'tcx> { fn sinto(&self, s: &S) -> GenericArg { - self.unpack().sinto(s) + self.kind().sinto(s) } } #[cfg(feature = "rustc")] impl<'tcx, S: UnderOwnerState<'tcx>> SInto> for ty::GenericArgsRef<'tcx> { fn sinto(&self, s: &S) -> Vec { - self.iter().map(|v| v.unpack().sinto(s)).collect() + self.iter().map(|v| v.kind().sinto(s)).collect() } } @@ -1078,12 +1082,9 @@ pub enum PointerCoercion { ClosureFnPointer(Safety), MutToConstPointer, ArrayToPointer, - DynStar, Unsize, } -sinto_todo!(rustc_middle::ty, ScalarInt); - /// Reflects [`ty::FnSig`] #[derive_group(Serializers)] #[derive(AdtInto, Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] @@ -1169,7 +1170,7 @@ pub enum Term { impl<'tcx, S: UnderOwnerState<'tcx>> SInto for ty::Term<'tcx> { fn sinto(&self, s: &S) -> Term { use ty::TermKind; - match self.unpack() { + match self.kind() { TermKind::Ty(ty) => Term::Ty(ty.sinto(s)), TermKind::Const(c) => Term::Const(c.sinto(s)), } @@ -1228,6 +1229,7 @@ pub enum ClauseKind { WellFormed(Term), ConstEvaluatable(ConstantExpr), HostEffect(HostEffectPredicate), + UnstableFeature(Symbol), } sinto_todo!(rustc_middle::ty, HostEffectPredicate<'tcx>); diff --git a/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v b/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v index 64d56e9e3..3bb96d69c 100644 --- a/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v +++ b/hax-lib/proof-libs/coq/coq/generated-core/src/Core_Iter_Range.v @@ -100,7 +100,7 @@ Instance t_RangeIteratorImpl_158276838 `{v_A : Type} `{t_Sized (v_A)} `{t_Step ( { RangeIteratorImpl_impl_f_Item := v_A; RangeIteratorImpl_impl_f_spec_next := fun (self : t_Range ((v_A)))=> - let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in + let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in (self,hax_temp_output); }. @@ -108,7 +108,7 @@ Instance t_Iterator_416192239 `{v_A : Type} `{t_Sized (v_A)} `{t_Step (v_A)} : t { Iterator_impl_1_f_Item := v_A; Iterator_impl_1_f_next := fun (self : t_Range ((v_A)))=> - let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in + let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in (self,hax_temp_output); Iterator_impl_1_f_size_hint := fun (self : t_Range ((v_A)))=> if diff --git a/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti b/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti index 7c0b405af..7668c3a1f 100644 --- a/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti +++ b/hax-lib/proof-libs/fstar/core/Alloc.Fmt.fsti @@ -3,7 +3,7 @@ open Rust_primitives include Core.Fmt -val impl_2__new_v1 (sz1:usize) (sz2: usize) (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments +val impl_1__new_v1 (sz1:usize) (sz2: usize) (pieces: t_Slice string) (args: Core.Fmt.Rt.t_Argument): t_Arguments val impl_7__write_fmt (fmt: t_Formatter) (args: t_Arguments): t_Result val format (args: t_Arguments): string diff --git a/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti b/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti index f9952dcd2..cab57d432 100644 --- a/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti +++ b/hax-lib/proof-libs/fstar/core/Core.Fmt.Rt.fsti @@ -7,8 +7,8 @@ val impl_1__new_debug (#t:Type0) (x: t): t_Argument val impl_4__new_v1_formatted (#t:Type0) (x: t) : t_Argument val impl_1__new_binary (#t:Type0) (x: t) : t_Argument val impl_1__new_lower_hex (#t:Type0) (x: t) : t_Argument -val impl_2__new_const (#t:Type0) (#u:Type0) (xconst: t) (yconst: u): t_Argument -val impl_2__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0) +val impl_1__new_const (#t:Type0) (#u:Type0) (xconst: t) (yconst: u): t_Argument +val impl_1__new_v1 (#t1:Type0) (#t2:Type0) (#t3:Type0) (#t4:Type0) (x1: t1) (x2: t2) (x3: t3) (x4: t4) : t_Argument val impl__new_display (#t:Type0) (x: t): t_Argument val impl__new_debug (#t:Type0) (x: t): t_Argument diff --git a/rust-toolchain.toml b/rust-toolchain.toml index f290a30ed..5cadcd938 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-05-26" +channel = "nightly-2025-07-20" components = [ "rustc-dev", "llvm-tools-preview" , "rust-analysis" , "rust-src" , "rustfmt" ] diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst index 2421d61b2..b2199312b 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Abort.fst @@ -7,7 +7,7 @@ let might_abort (should_abort: bool) : Prims.unit = if should_abort then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["aborting...\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -15,7 +15,7 @@ let might_abort (should_abort: bool) : Prims.unit = Core.Fmt.t_Arguments) in let _:Prims.unit = () in - Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["panics and aborts"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); @@ -26,7 +26,7 @@ let might_abort (should_abort: bool) : Prims.unit = Rust_primitives.Hax.t_Never) else let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["Don't Panic\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst index 25c0595e5..bf0e5af85 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Assert.fst @@ -4,15 +4,18 @@ open Core open FStar.Mul let might_fail_assert (one_plus_one: u32) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #u32 one_plus_one] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["does 1 + 1 = "; "?\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_display #u32 one_plus_one <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst index 04356340f..964a2565b 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst @@ -6,8 +6,8 @@ open FStar.Mul (* item error backend: (reject_TraitItemDefault) ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" } Last available AST for this item: -#[path()]#[(any(feature = "json"))]#[feature(coverage_attribute)]#[(any(feature = "json", feature = "fstar", feature = "fstar-lax", feature = -"coq"))]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait t_T{fn f_f((self: Self)) -> tuple0{{let _: tuple0 = {std::io::stdio::e_print(core::fmt::rt::impl_2__new_const::(["default\n"]))};{let _: tuple0 = {Tuple0};Tuple0}}}} +#[(any(feature = "json"))]#[feature(coverage_attribute)]#[(any(feature = "json", feature = "fstar", feature = "fstar-lax", feature = +"coq"))]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait t_T{fn f_f((self: Self)) -> tuple0{{let _: tuple0 = {std::io::stdio::e_print(core::fmt::rt::impl_1__new_const::(["default\n"]))};{let _: tuple0 = {Tuple0};Tuple0}}}} Last AST: /** print_rust: pitem: not implemented (item: { Concrete_ident.T.def_id = @@ -74,7 +74,7 @@ let impl: t_T t_S = = fun (self: t_S) -> let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["impl S\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst index 1d226b104..1afbf88e4 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_crate.fst @@ -14,15 +14,18 @@ let used_only_from_bin_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -34,15 +37,18 @@ let used_only_from_this_lib_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -54,15 +60,18 @@ let used_from_bin_crate_and_lib_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -74,17 +83,20 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -96,15 +108,18 @@ let unused_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["unused_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst index 00520c6fd..7d7aa2ce2 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Auxiliary.Used_inline_crate.fst @@ -14,15 +14,18 @@ let used_only_from_bin_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_only_from_bin_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -34,15 +37,18 @@ let used_only_from_this_lib_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_only_from_this_lib_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -54,15 +60,18 @@ let used_from_bin_crate_and_lib_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -74,17 +83,20 @@ let used_with_same_type_from_bin_crate_and_lib_crate_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["used_with_same_type_from_bin_crate_and_lib_crate_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -96,15 +108,18 @@ let unused_generic_function (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Fmt.t_Debug v_T) (arg: v_T) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #v_T arg] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["unused_generic_function with "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #v_T arg <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst index 93864eac0..dc9cacaf3 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Closure_macro.fst @@ -12,7 +12,7 @@ let load_configuration_files (_: Prims.unit) let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["Starting service\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -29,22 +29,19 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String Core.Result.t_Result Alloc.String.t_String Alloc.String.t_String) (fun e -> let e:Alloc.String.t_String = e in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #Alloc.String.t_String e] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let message:Alloc.String.t_String = Core.Hint.must_use #Alloc.String.t_String - (Alloc.Fmt.format (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 1) + (Alloc.Fmt.format (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 1) (mk_usize 1) (let list = ["Error loading configs: "] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #Alloc.String.t_String e - <: - Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) <: @@ -52,21 +49,18 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String in if (Alloc.String.impl_String__len message <: usize) >. mk_usize 0 then + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #Alloc.String.t_String message] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #Alloc.String.t_String message - <: - Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -83,7 +77,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String if (Core.Str.impl_str__len "error" <: usize) >. mk_usize 0 then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["no msg\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -94,7 +88,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit Alloc.String.t_String () else let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["error\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst index f60d96438..2e60b95a5 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Conditions.fst @@ -105,7 +105,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -188,7 +188,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -261,7 +261,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -357,7 +357,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -440,7 +440,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -513,7 +513,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -621,7 +621,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -704,7 +704,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -777,7 +777,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -873,7 +873,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -957,7 +957,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -1030,7 +1030,7 @@ let main (_: Prims.unit) : Prims.unit = else let should_be_reachable:i32 = countdown in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["reached\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst index c8db9b6cf..95ffd8e15 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Drop_trait.fst @@ -13,17 +13,18 @@ let impl: Core.Ops.Drop.t_Drop t_Firework = f_drop = fun (self: t_Firework) -> + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #i32 self.f_strength] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["BOOM times "; "!!!\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [Core.Fmt.Rt.impl__new_display #i32 self.f_strength <: Core.Fmt.Rt.t_Argument] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -37,7 +38,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 = if true then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["Exiting with error...\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst index 069b00db0..00bd52ee1 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Generics.fst @@ -29,17 +29,18 @@ let impl_1 f_drop = fun (self: t_Firework v_T) -> + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #v_T self.f_strength] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["BOOM times "; "!!!\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [Core.Fmt.Rt.impl__new_display #v_T self.f_strength <: Core.Fmt.Rt.t_Argument] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -56,7 +57,7 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 = if true then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["Exiting with error...\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst index 7ca500049..c7d0ce014 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst @@ -8,7 +8,7 @@ let if_not (cond: bool) : Prims.unit = if ~.cond then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cond was false\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -22,7 +22,7 @@ let if_not (cond: bool) : Prims.unit = if ~.cond then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cond was false\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -35,7 +35,7 @@ let if_not (cond: bool) : Prims.unit = if ~.cond then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cond was false\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -46,7 +46,7 @@ let if_not (cond: bool) : Prims.unit = () else let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cond was true\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst index 68c3296a8..96d2ac383 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst @@ -25,11 +25,11 @@ let display : Prims.unit = let _:Prims.unit = Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation" - "{\n for x in (core::iter::traits::collect::f_into_iter(xs)) {\n {\n let _: tuple0 = {\n std::io::stdio::e_print(\n core::fmt::rt::impl_2__new_v1::<\n generic_value!(todo),\n generic_value!(todo),\n >([\"\"], [c..." + "{\n for x in (core::iter::traits::collect::f_into_iter(xs)) {\n {\n let args: [core::fmt::rt::t_Argument; 1] = {\n [core::fmt::rt::impl__new_display::(x)]\n };\n {\n let _: tuple0 = {\n std::io::stdio::e_p..." in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -40,7 +40,7 @@ let display () let error (_: Prims.unit) : Prims.unit = - Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["error"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst index 44e1ff1e3..65091dd0a 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inline_dead.fst @@ -8,17 +8,18 @@ let dead (_: Prims.unit) : u32 = mk_u32 42 let live (v_B: bool) (_: Prims.unit) : u32 = if v_B then dead () else mk_u32 0 let main (_: Prims.unit) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #u32 (live false () <: u32)] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [Core.Fmt.Rt.impl__new_display #u32 (live false () <: u32) <: Core.Fmt.Rt.t_Argument] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst index 2e5ac967c..f6d870fde 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst @@ -14,15 +14,18 @@ let main__t_in_mod__v_IN_MOD_CONST: u32 = mk_u32 1000 let main__in_func (a: u32) : Prims.unit = let b:u32 = mk_u32 1 in let c:u32 = a +! b in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #u32 c] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["c = "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_display #u32 c <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst index c26f2240c..456fe3b9d 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Issue_83601_.fst @@ -44,47 +44,50 @@ let main (_: Prims.unit) : Prims.unit = match baz, (Foo (mk_u32 1) <: t_Foo) <: (t_Foo & t_Foo) with | left_val, right_val -> Hax_lib.v_assert (~.(left_val =. right_val <: bool) <: bool) in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #t_Foo (Foo (mk_u32 1) <: t_Foo)] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [ - Core.Fmt.Rt.impl__new_debug #t_Foo (Foo (mk_u32 1) <: t_Foo) - <: - Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in let _:Prims.unit = () in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #t_Foo bar] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #t_Foo bar <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in let _:Prims.unit = () in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #t_Foo baz] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = [Core.Fmt.Rt.impl__new_debug #t_Foo baz <: Core.Fmt.Rt.t_Argument] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst index 1e5ec879d..be8b66179 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Loops_branches.fst @@ -30,7 +30,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest = in let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) = Core.Fmt.impl_11__write_fmt f - (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cool"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -62,7 +62,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest = let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) = Core.Fmt.impl_11__write_fmt f - (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cool"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -148,7 +148,7 @@ let impl: Core.Fmt.t_Debug t_DebugTest = let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) = Core.Fmt.impl_11__write_fmt f - (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cool"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -254,7 +254,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest = let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) = Core.Fmt.impl_11__write_fmt f - (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cool"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -312,7 +312,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest = in let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) = Core.Fmt.impl_11__write_fmt f - (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cool"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -351,7 +351,7 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest = let tmp0, out:(Core.Fmt.t_Formatter & Core.Result.t_Result Prims.unit Core.Fmt.t_Error) = Core.Fmt.impl_11__write_fmt f - (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["cool"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -411,33 +411,35 @@ let impl_1: Core.Fmt.t_Display t_DisplayTest = let main (_: Prims.unit) : Prims.unit = let debug_test:t_DebugTest = DebugTest <: t_DebugTest in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_debug #t_DebugTest debug_test] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [Core.Fmt.Rt.impl__new_debug #t_DebugTest debug_test <: Core.Fmt.Rt.t_Argument] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in let _:Prims.unit = () in let display_test:t_DisplayTest = DisplayTest <: t_DisplayTest in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #t_DisplayTest display_test] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [Core.Fmt.Rt.impl__new_display #t_DisplayTest display_test <: Core.Fmt.Rt.t_Argument] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst index f225df678..2647d48df 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Macro_in_closure.fst @@ -7,7 +7,7 @@ let v_NO_BLOCK: Prims.unit -> Prims.unit = fun temp_0_ -> let _:Prims.unit = temp_0_ in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["hello\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -20,7 +20,7 @@ let v_WITH_BLOCK: Prims.unit -> Prims.unit = fun temp_0_ -> let _:Prims.unit = temp_0_ in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["hello\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst index 1aa969a36..453968305 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.Nested_fns.fst @@ -7,7 +7,7 @@ let outer_not_covered__inner (is_true: bool) : Prims.unit = if is_true then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called and covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -18,7 +18,7 @@ let outer_not_covered__inner (is_true: bool) : Prims.unit = () else let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["absolutely not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -30,7 +30,7 @@ let outer_not_covered__inner (is_true: bool) : Prims.unit = let outer_not_covered (is_true: bool) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called but not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -45,7 +45,7 @@ let outer__inner_not_covered (is_true: bool) : Prims.unit = if is_true then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called but not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -56,7 +56,7 @@ let outer__inner_not_covered (is_true: bool) : Prims.unit = () else let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["absolutely not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -68,7 +68,7 @@ let outer__inner_not_covered (is_true: bool) : Prims.unit = let outer (is_true: bool) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called and covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -83,7 +83,7 @@ let outer_both_covered__inner (is_true: bool) : Prims.unit = if is_true then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called and covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -94,7 +94,7 @@ let outer_both_covered__inner (is_true: bool) : Prims.unit = () else let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["absolutely not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -106,7 +106,7 @@ let outer_both_covered__inner (is_true: bool) : Prims.unit = let outer_both_covered (is_true: bool) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called and covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst index 2596c888d..dd83efe36 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.No_cov_crate.fst @@ -11,7 +11,7 @@ let _ = let do_not_add_coverage_1_ (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called but not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -23,7 +23,7 @@ let do_not_add_coverage_1_ (_: Prims.unit) : Prims.unit = let do_not_add_coverage_2_ (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called but not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -35,7 +35,7 @@ let do_not_add_coverage_2_ (_: Prims.unit) : Prims.unit = let do_not_add_coverage_not_called (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["not called and not covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -47,7 +47,7 @@ let do_not_add_coverage_not_called (_: Prims.unit) : Prims.unit = let add_coverage_1_ (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called and covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -59,7 +59,7 @@ let add_coverage_1_ (_: Prims.unit) : Prims.unit = let add_coverage_2_ (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["called and covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -71,7 +71,7 @@ let add_coverage_2_ (_: Prims.unit) : Prims.unit = let add_coverage_not_called (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["not called but covered\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst index 8b0241ab1..c8dbe6bf1 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Overflow.fst @@ -8,7 +8,7 @@ let might_overflow (to_add: u32) : u32 = if to_add >. mk_u32 5 then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["this will probably overflow\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -19,27 +19,28 @@ let might_overflow (to_add: u32) : u32 = () in let add_to:u32 = Core.Num.impl_u32__MAX -! mk_u32 5 in + let args:(u32 & u32) = add_to, to_add <: (u32 & u32) in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 2) = + let list = + [Core.Fmt.Rt.impl__new_display #u32 args._1; Core.Fmt.Rt.impl__new_display #u32 args._2] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); + Rust_primitives.Hax.array_of_list 2 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 3) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 3) (mk_usize 2) (let list = ["does "; " + "; " overflow?\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); Rust_primitives.Hax.array_of_list 3 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #u32 add_to <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl__new_display #u32 to_add <: Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); - Rust_primitives.Hax.array_of_list 2 list) + args <: Core.Fmt.t_Arguments) in let _:Prims.unit = () in let result:u32 = to_add +! add_to in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["continuing after overflow check\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -68,17 +69,18 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 = if countdown =. mk_i32 1 then let result:u32 = might_overflow (mk_u32 10) in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #u32 result] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["Result: "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [Core.Fmt.Rt.impl__new_display #u32 result <: Core.Fmt.Rt.t_Argument] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in @@ -88,17 +90,18 @@ let main (_: Prims.unit) : Core.Result.t_Result Prims.unit u8 = if countdown <. mk_i32 5 then let result:u32 = might_overflow (mk_u32 1) in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #u32 result] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = ["Result: "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [Core.Fmt.Rt.impl__new_display #u32 result <: Core.Fmt.Rt.t_Argument] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst index 635c1938a..8778578c1 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Panic_unwind.fst @@ -7,7 +7,7 @@ let might_panic (should_panic: bool) : Prims.unit = if should_panic then let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["panicking...\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -15,7 +15,7 @@ let might_panic (should_panic: bool) : Prims.unit = Core.Fmt.t_Arguments) in let _:Prims.unit = () in - Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["panics"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); @@ -26,7 +26,7 @@ let might_panic (should_panic: bool) : Prims.unit = Rust_primitives.Hax.t_Never) else let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["Don't Panic\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst index d8ec281f8..6f6313509 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Partial_eq.fst @@ -59,30 +59,35 @@ let impl_Version__new (major minor patch: usize) : t_Version = let main (_: Prims.unit) : Prims.unit = let version_3_2_1_:t_Version = impl_Version__new (mk_usize 3) (mk_usize 2) (mk_usize 1) in let version_3_3_0_:t_Version = impl_Version__new (mk_usize 3) (mk_usize 3) (mk_usize 0) in + let args:(t_Version & t_Version & bool) = + version_3_2_1_, + version_3_3_0_, + Core.Cmp.f_lt #t_Version + #t_Version + #FStar.Tactics.Typeclasses.solve + version_3_2_1_ + version_3_3_0_ + <: + (t_Version & t_Version & bool) + in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 3) = + let list = + [ + Core.Fmt.Rt.impl__new_debug #t_Version args._1; + Core.Fmt.Rt.impl__new_debug #t_Version args._2; + Core.Fmt.Rt.impl__new_display #bool args._3 + ] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); + Rust_primitives.Hax.array_of_list 3 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 4) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 4) (mk_usize 3) (let list = [""; " < "; " = "; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 4); Rust_primitives.Hax.array_of_list 4 list) - (let list = - [ - Core.Fmt.Rt.impl__new_debug #t_Version version_3_2_1_ <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl__new_debug #t_Version version_3_3_0_ <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl__new_display #bool - (Core.Cmp.f_lt #t_Version - #t_Version - #FStar.Tactics.Typeclasses.solve - version_3_2_1_ - version_3_3_0_ - <: - bool) - <: - Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); - Rust_primitives.Hax.array_of_list 3 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst index a19adfc3c..c1ad4d15d 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Sort_groups.fst @@ -12,21 +12,18 @@ let _ = let generic_fn (#v_T: Type0) (cond: bool) : Prims.unit = if cond then + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = [Core.Fmt.Rt.impl__new_display #string (Core.Any.type_name #v_T () <: string)] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #string (Core.Any.type_name #v_T () <: string) - <: - Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst index 238db510e..0ceffc9d5 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.Unused_module.fst @@ -5,7 +5,7 @@ open FStar.Mul let never_called_function (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["I am never called\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst index 654c155ce..a54b35f14 100644 --- a/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst +++ b/rustc-coverage-tests/snapshots/fstar/Coverage.Unused_mod.fst @@ -5,7 +5,7 @@ open FStar.Mul let main (_: Prims.unit) : Prims.unit = let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_const (mk_usize 1) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["hello world!\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) diff --git a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap index 0928d26ad..916b17337 100644 --- a/test-harness/src/snapshots/toolchain__dyn into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__dyn into-fstar.snap @@ -54,27 +54,28 @@ let print Alloc.Boxed.t_Box (dyn 1 (fun z -> t_Printable z Alloc.String.t_String)) Alloc.Alloc.t_Global) : Prims.unit = + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 1) = + let list = + [ + Core.Fmt.Rt.impl__new_display #Alloc.String.t_String + (f_stringify #(dyn 1 (fun z -> t_Printable z Alloc.String.t_String)) + #Alloc.String.t_String + #FStar.Tactics.Typeclasses.solve + a + <: + Alloc.String.t_String) + ] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 2) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 2) (mk_usize 1) (let list = [""; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); Rust_primitives.Hax.array_of_list 2 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #Alloc.String.t_String - (f_stringify #(dyn 1 (fun z -> t_Printable z Alloc.String.t_String)) - #Alloc.String.t_String - #FStar.Tactics.Typeclasses.solve - a - <: - Alloc.String.t_String) - <: - Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) + args <: Core.Fmt.t_Arguments) in diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index 6c5a0f5e8..640f68231 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -45,8 +45,7 @@ From Core Require Import Core. (* NotImplementedYet *) -From Literals Require Import hax_lib. -Export hax_lib. + Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_str (("0"%string : string)))) (f_lt (x) (impl_Int__e_unsafe_from_str (("16"%string : string)))) = true} : t_u8 := let _ : t_Int := f_lift ((3 : t_usize)) in @@ -81,7 +80,7 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_s impl_Int__to_u8 (f_add (x) (f_mul (x) (x))). Definition panic_with_msg '(_ : unit) : unit := - never_to_any (panic_fmt (impl_2__new_const ([("with msg"%string : string)]))). + never_to_any (panic_fmt (impl_1__new_const ([("with msg"%string : string)]))). Record Foo_record : Type := { diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index 35a58078c..23fafa1e1 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -72,7 +72,7 @@ let math_integers (x: Hax_lib.Int.t_Int) Hax_lib.Int.impl_Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int) let panic_with_msg (_: Prims.unit) : Prims.unit = - Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_2__new_const (mk_usize + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.Rt.impl_1__new_const (mk_usize 1) (let list = ["with msg"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index cae01d074..cd6dea444 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -33,20 +33,21 @@ open Core open FStar.Mul let debug (label value: u32) : Prims.unit = + let args:(u32 & u32) = label, value <: (u32 & u32) in + let args:t_Array Core.Fmt.Rt.t_Argument (mk_usize 2) = + let list = + [Core.Fmt.Rt.impl__new_display #u32 args._1; Core.Fmt.Rt.impl__new_display #u32 args._2] + in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); + Rust_primitives.Hax.array_of_list 2 list + in let _:Prims.unit = - Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_2__new_v1 (mk_usize 3) + Std.Io.Stdio.e_print (Core.Fmt.Rt.impl_1__new_v1 (mk_usize 3) (mk_usize 2) (let list = ["["; "] a="; "\n"] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); Rust_primitives.Hax.array_of_list 3 list) - (let list = - [ - Core.Fmt.Rt.impl__new_display #u32 label <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl__new_display #u32 value <: Core.Fmt.Rt.t_Argument - ] - in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); - Rust_primitives.Hax.array_of_list 2 list) + args <: Core.Fmt.t_Arguments) in