diff --git a/Cargo.lock b/Cargo.lock
index c6c2e18397..83ba881617 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -32,9 +32,9 @@ dependencies = [
 
 [[package]]
 name = "anstream"
-version = "0.6.21"
+version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "43d5b281e737544384e969a5ccad3f1cdd24b48086a0fc1b2a5262a26b8f4f4a"
+checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d"
 dependencies = [
  "anstyle",
  "anstyle-parse",
@@ -47,15 +47,15 @@ dependencies = [
 
 [[package]]
 name = "anstyle"
-version = "1.0.13"
+version = "1.0.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5192cca8006f1fd4f7237516f40fa183bb07f8fbdfedaa0036de5ea9b0b45e78"
+checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000"
 
 [[package]]
 name = "anstyle-parse"
-version = "0.2.7"
+version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4e7644824f0aa2c7b9384579234ef10eb7efb6a0deb83f9630a49594dd9c15c2"
+checksum = "52ce7f38b242319f7cabaa6813055467063ecdc9d355bbb4ce0c68908cd8130e"
 dependencies = [
  "utf8parse",
 ]
@@ -66,7 +66,7 @@ version = "1.1.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "40c48f72fd53cd289104fc64099abca73db4166ad86ea0b4341abe65af83dadc"
 dependencies = [
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
@@ -77,7 +77,7 @@ checksum = "291e6a250ff86cd4a820112fb8898808a366d8f9f58ce16d1f538353ad55747d"
 dependencies = [
  "anstyle",
  "once_cell_polyfill",
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
@@ -94,9 +94,9 @@ checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b"
 
 [[package]]
 name = "assert_cmd"
-version = "2.1.2"
+version = "2.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9c5bcfa8749ac45dd12cb11055aeeb6b27a3895560d60d71e3c23bf979e60514"
+checksum = "39bae1d3fa576f7c6519514180a72559268dd7d1fe104070956cb687bc6673bd"
 dependencies = [
  "anstyle",
  "bstr",
@@ -130,9 +130,9 @@ checksum = "5e764a1d40d510daf35e07be9eb06e75770908c27d411ee6c92109c9840eaaf7"
 
 [[package]]
 name = "bitflags"
-version = "2.11.0"
+version = "2.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "843867be96c8daad0d758b57df9392b6d8d271134fce549de6ce169ff98a92af"
+checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3"
 
 [[package]]
 name = "block-buffer"
@@ -188,9 +188,9 @@ dependencies = [
 
 [[package]]
 name = "cargo-platform"
-version = "0.3.2"
+version = "0.3.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "87a0c0e6148f11f01f32650a2ea02d532b2ad4e81d8bd41e6e565b5adc5e6082"
+checksum = "dd0061da739915fae12ea00e16397555ed4371a6bb285431aab930f61b0aa4ba"
 dependencies = [
  "serde",
  "serde_core",
@@ -212,9 +212,9 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.2.56"
+version = "1.2.60"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "aebf35691d1bfb0ac386a69bac2fde4dd276fb618cf8bf4f5318fe285e821bb2"
+checksum = "43c5703da9466b66a946814e1adf53ea2c90f10063b86290cc9eb67ce3478a20"
 dependencies = [
  "find-msvc-tools",
  "jobserver",
@@ -230,9 +230,9 @@ checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
 
 [[package]]
 name = "clap"
-version = "4.5.60"
+version = "4.6.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2797f34da339ce31042b27d23607e051786132987f595b02ba4f6a6dffb7030a"
+checksum = "1ddb117e43bbf7dacf0a4190fef4d345b9bad68dfc649cb349e7d17d28428e51"
 dependencies = [
  "clap_builder",
  "clap_derive",
@@ -240,9 +240,9 @@ dependencies = [
 
 [[package]]
 name = "clap_builder"
-version = "4.5.60"
+version = "4.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "24a241312cea5059b13574bb9b3861cabf758b879c15190b37b6d6fd63ab6876"
+checksum = "714a53001bf66416adb0e2ef5ac857140e7dc3a0c48fb28b2f10762fc4b5069f"
 dependencies = [
  "anstream",
  "anstyle",
@@ -252,9 +252,9 @@ dependencies = [
 
 [[package]]
 name = "clap_derive"
-version = "4.5.55"
+version = "4.6.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a92793da1a46a5f2a02a6f4c46c6496b28c43638adea8306fcb0caa1634f24e5"
+checksum = "f2ce8604710f6733aa641a2b3731eaa1e8b3d9973d5e3565da11800813f997a9"
 dependencies = [
  "heck",
  "proc-macro2",
@@ -264,26 +264,25 @@ dependencies = [
 
 [[package]]
 name = "clap_lex"
-version = "1.0.0"
+version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3a822ea5bc7590f9d40f1ba12c0dc3c2760f3482c6984db1573ad11031420831"
+checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9"
 
 [[package]]
 name = "colorchoice"
-version = "1.0.4"
+version = "1.0.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b05b61dc5112cbb17e4b6cd61790d9845d13888356391624cbe7e41efeac1e75"
+checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570"
 
 [[package]]
 name = "console"
-version = "0.15.11"
+version = "0.16.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "054ccb5b10f9f2cbf51eb355ca1d05c2d279ce1804688d0db74b4733a5aeafd8"
+checksum = "d64e8af5551369d19cf50138de61f1c42074ab970f74e99be916646777f8fc87"
 dependencies = [
  "encode_unicode",
  "libc",
- "once_cell",
- "windows-sys 0.59.0",
+ "windows-sys",
 ]
 
 [[package]]
@@ -460,7 +459,7 @@ dependencies = [
  "libc",
  "option-ext",
  "redox_users",
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
@@ -488,25 +487,19 @@ checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0"
 
 [[package]]
 name = "env_filter"
-version = "1.0.0"
+version = "1.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7a1c3cc8e57274ec99de65301228b537f1e4eedc1b8e0f9411c6caac8ae7308f"
+checksum = "32e90c2accc4b07a8456ea0debdc2e7587bdd890680d71173a15d4ae604f6eef"
 dependencies = [
  "log",
  "regex",
 ]
 
-[[package]]
-name = "env_home"
-version = "0.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c7f84e12ccf0a7ddc17a6c41c93326024c42920d7ee630d04950e6926645c0fe"
-
 [[package]]
 name = "env_logger"
-version = "0.11.9"
+version = "0.11.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b2daee4ea451f429a58296525ddf28b45a3b64f1acf6587e2067437bb11e218d"
+checksum = "0621c04f2196ac3f488dd583365b9c09be011a4ab8b9f37248ffcc8f6198b56a"
 dependencies = [
  "anstream",
  "anstyle",
@@ -528,14 +521,14 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "39cab71617ae0d63f51a36d69f866391735b51691dbda63cf6f96d042b63efeb"
 dependencies = [
  "libc",
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
 name = "fastrand"
-version = "2.3.0"
+version = "2.4.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "37909eebbb50d72f9059c3b6d82c0463f2ff062c9e95845c43a6c9c0355411be"
+checksum = "9f1f227452a390804cdb637b74a86990f2a7d7ba4b7d5693aac9b4dd6defd8d6"
 
 [[package]]
 name = "find-msvc-tools"
@@ -609,19 +602,19 @@ checksum = "899def5c37c4fd7b2664648c28120ecec138e4d395b459e5ca34f9cce2dd77fd"
 dependencies = [
  "cfg-if",
  "libc",
- "r-efi",
+ "r-efi 5.3.0",
  "wasip2",
 ]
 
 [[package]]
 name = "getrandom"
-version = "0.4.1"
+version = "0.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "139ef39800118c7683f2fd3c98c1b23c09ae076556b435f8e9064ae108aaeeec"
+checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555"
 dependencies = [
  "cfg-if",
  "libc",
- "r-efi",
+ "r-efi 6.0.0",
  "wasip2",
  "wasip3",
 ]
@@ -656,9 +649,9 @@ dependencies = [
 
 [[package]]
 name = "hashbrown"
-version = "0.16.1"
+version = "0.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "841d1cc9bed7f9236f321df977030373f4a4163ae1a7dbfe1a51a2c1a51d9100"
+checksum = "4f467dd6dccf739c208452f8014c75c18bb8301b050ad1cfb27153803edb0f51"
 
 [[package]]
 name = "heck"
@@ -674,12 +667,13 @@ checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70"
 
 [[package]]
 name = "icu_collections"
-version = "2.1.1"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4c6b649701667bbe825c3b7e6388cb521c23d88644678e83c0c4d0a621a34b43"
+checksum = "2984d1cd16c883d7935b9e07e44071dca8d917fd52ecc02c04d5fa0b5a3f191c"
 dependencies = [
  "displaydoc",
  "potential_utf",
+ "utf8_iter",
  "yoke",
  "zerofrom",
  "zerovec",
@@ -687,9 +681,9 @@ dependencies = [
 
 [[package]]
 name = "icu_locale_core"
-version = "2.1.1"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "edba7861004dd3714265b4db54a3c390e880ab658fec5f7db895fae2046b5bb6"
+checksum = "92219b62b3e2b4d88ac5119f8904c10f8f61bf7e95b640d25ba3075e6cac2c29"
 dependencies = [
  "displaydoc",
  "litemap",
@@ -700,9 +694,9 @@ dependencies = [
 
 [[package]]
 name = "icu_normalizer"
-version = "2.1.1"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5f6c8828b67bf8908d82127b2054ea1b4427ff0230ee9141c54251934ab1b599"
+checksum = "c56e5ee99d6e3d33bd91c5d85458b6005a22140021cc324cea84dd0e72cff3b4"
 dependencies = [
  "icu_collections",
  "icu_normalizer_data",
@@ -714,15 +708,15 @@ dependencies = [
 
 [[package]]
 name = "icu_normalizer_data"
-version = "2.1.1"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7aedcccd01fc5fe81e6b489c15b247b8b0690feb23304303a9e560f37efc560a"
+checksum = "da3be0ae77ea334f4da67c12f149704f19f81d1adf7c51cf482943e84a2bad38"
 
 [[package]]
 name = "icu_properties"
-version = "2.1.2"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "020bfc02fe870ec3a66d93e677ccca0562506e5872c650f893269e08615d74ec"
+checksum = "bee3b67d0ea5c2cca5003417989af8996f8604e34fb9ddf96208a033901e70de"
 dependencies = [
  "icu_collections",
  "icu_locale_core",
@@ -734,15 +728,15 @@ dependencies = [
 
 [[package]]
 name = "icu_properties_data"
-version = "2.1.2"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "616c294cf8d725c6afcd8f55abc17c56464ef6211f9ed59cccffe534129c77af"
+checksum = "8e2bbb201e0c04f7b4b3e14382af113e17ba4f63e2c9d2ee626b720cbce54a14"
 
 [[package]]
 name = "icu_provider"
-version = "2.1.1"
+version = "2.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "85962cf0ce02e1e0a629cc34e7ca3e373ce20dda4c4d7294bbd0bf1fdb59e614"
+checksum = "139c4cf31c8b5f33d7e199446eff9c1e02decfc2f0eec2c8d71f65befa45b421"
 dependencies = [
  "displaydoc",
  "icu_locale_core",
@@ -782,21 +776,21 @@ dependencies = [
 
 [[package]]
 name = "indexmap"
-version = "2.13.0"
+version = "2.14.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7714e70437a7dc3ac8eb7e6f8df75fd8eb422675fc7678aff7364301092b1017"
+checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
  "equivalent",
- "hashbrown 0.16.1",
+ "hashbrown 0.17.0",
  "serde",
  "serde_core",
 ]
 
 [[package]]
 name = "insta"
-version = "1.46.3"
+version = "1.47.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e82db8c87c7f1ccecb34ce0c24399b8a73081427f3c7c50a5d597925356115e4"
+checksum = "7b4a6248eb93a4401ed2f37dfe8ea592d3cf05b7cf4f8efa867b6895af7e094e"
 dependencies = [
  "console",
  "once_cell",
@@ -821,15 +815,15 @@ dependencies = [
 
 [[package]]
 name = "itoa"
-version = "1.0.17"
+version = "1.0.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "92ecc6618181def0457392ccd0ee51198e065e016d1d527a7ac1b6dc7c1f09d2"
+checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
 
 [[package]]
 name = "jiff"
-version = "0.2.21"
+version = "0.2.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b3e3d65f018c6ae946ab16e80944b97096ed73c35b221d1c478a6c81d8f57940"
+checksum = "1a3546dc96b6d42c5f24902af9e2538e82e39ad350b0c766eb3fbf2d8f3d8359"
 dependencies = [
  "jiff-static",
  "log",
@@ -840,9 +834,9 @@ dependencies = [
 
 [[package]]
 name = "jiff-static"
-version = "0.2.21"
+version = "0.2.23"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a17c2b211d863c7fde02cbea8a3c1a439b98e109286554f2860bdded7ff83818"
+checksum = "2a8c8b344124222efd714b73bb41f8b5120b27a7cc1c75593a6ff768d9d05aa4"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -861,9 +855,9 @@ dependencies = [
 
 [[package]]
 name = "js-sys"
-version = "0.3.90"
+version = "0.3.95"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "14dc6f6450b3f6d4ed5b16327f38fed626d375a886159ca555bd7822c0c3a5a6"
+checksum = "2964e92d1d9dc3364cae4d718d93f227e3abb088e747d92e0395bfdedf1c12ca"
 dependencies = [
  "once_cell",
  "wasm-bindgen",
@@ -883,9 +877,9 @@ checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
 
 [[package]]
 name = "libc"
-version = "0.2.182"
+version = "0.2.185"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6800badb6cb2082ffd7b6a67e6125bb39f18782f793520caee8cb8846be06112"
+checksum = "52ff2c0fe9bc6cb6b14a0592c2ff4fa9ceb83eea9db979b0487cd054946a2b8f"
 
 [[package]]
 name = "libgit2-sys"
@@ -901,19 +895,18 @@ dependencies = [
 
 [[package]]
 name = "libredox"
-version = "0.1.12"
+version = "0.1.16"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3d0b95e02c851351f877147b7deea7b1afb1df71b63aa5f8270716e0c5720616"
+checksum = "e02f3bb43d335493c96bf3fd3a321600bf6bd07ed34bc64118e9293bdffea46c"
 dependencies = [
- "bitflags",
  "libc",
 ]
 
 [[package]]
 name = "libz-sys"
-version = "1.1.24"
+version = "1.1.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4735e9cbde5aac84a5ce588f6b23a90b9b0b528f6c5a8db8a4aff300463a0839"
+checksum = "fc3a226e576f50782b3305c5ccf458698f92798987f551c6a02efe8276721e22"
 dependencies = [
  "cc",
  "libc",
@@ -929,9 +922,9 @@ checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53"
 
 [[package]]
 name = "litemap"
-version = "0.8.1"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6373607a59f0be73a39b6fe456b8192fcc3585f602af20751600e974dd455e77"
+checksum = "92daf443525c4cce67b150400bc2316076100ce0b3686209eb8cf3c31612e6f0"
 
 [[package]]
 name = "lock_api"
@@ -1039,9 +1032,9 @@ dependencies = [
 
 [[package]]
 name = "once_cell"
-version = "1.21.3"
+version = "1.21.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "42f5e15c9953c5e4ccceeb2e7382a716482c34515315f7b03532b8b4e8393d2d"
+checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50"
 
 [[package]]
 name = "once_cell_polyfill"
@@ -1051,12 +1044,12 @@ checksum = "384b8ab6d37215f3c5301a95a4accb5d64aa607f1fcb26a11b5303878451b4fe"
 
 [[package]]
 name = "once_map"
-version = "0.4.23"
+version = "0.4.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "29eefd5038c9eee9e788d90966d6b5578dd3f88363a91edaec117a7ae0adc2d5"
+checksum = "b685c8311c9171d1bd2895222965d25616b2de2cb5819dd3504ed9250df9fecd"
 dependencies = [
  "ahash",
- "hashbrown 0.16.1",
+ "hashbrown 0.17.0",
  "parking_lot",
  "stable_deref_trait",
 ]
@@ -1124,9 +1117,9 @@ dependencies = [
 
 [[package]]
 name = "pkg-config"
-version = "0.3.32"
+version = "0.3.33"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7edddbd0b52d732b21ad9a5fab5c704c14cd949e5e9a1ec5929a24fded1b904c"
+checksum = "19f132c84eca552bf34cab8ec81f1c1dcc229b811638f9d283dceabe58c5569e"
 
 [[package]]
 name = "portable-atomic"
@@ -1136,18 +1129,18 @@ checksum = "c33a9471896f1c69cecef8d20cbe2f7accd12527ce60845ff44c153bb2a21b49"
 
 [[package]]
 name = "portable-atomic-util"
-version = "0.2.5"
+version = "0.2.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7a9db96d7fa8782dd8c15ce32ffe8680bbd1e978a43bf51a34d39483540495f5"
+checksum = "c2a106d1259c23fac8e543272398ae0e3c0b8d33c88ed73d0cc71b0f1d902618"
 dependencies = [
  "portable-atomic",
 ]
 
 [[package]]
 name = "potential_utf"
-version = "0.1.4"
+version = "0.1.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b73949432f5e2a09657003c25bca5e19a0e9c84f8058ca374f49e0ebe605af77"
+checksum = "0103b1cef7ec0cf76490e969665504990193874ea05c85ff9bab8b911d0a0564"
 dependencies = [
  "zerovec",
 ]
@@ -1228,9 +1221,9 @@ dependencies = [
 
 [[package]]
 name = "proptest"
-version = "1.10.0"
+version = "1.11.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "37566cb3fdacef14c0737f9546df7cfeadbfbc9fef10991038bf5015d0c80532"
+checksum = "4b45fcc2344c680f5025fe57779faef368840d0bd1f42f216291f0dc4ace4744"
 dependencies = [
  "bit-set",
  "bit-vec",
@@ -1253,9 +1246,9 @@ checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0"
 
 [[package]]
 name = "quote"
-version = "1.0.44"
+version = "1.0.45"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "21b2ebcf727b7760c461f091f9f0f539b77b8e87f2fd88131e7f1b433b3cece4"
+checksum = "41f2619966050689382d2b44f664f4bc593e129785a36d6ee376ddf37259b924"
 dependencies = [
  "proc-macro2",
 ]
@@ -1266,11 +1259,17 @@ version = "5.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "69cdb34c158ceb288df11e18b4bd39de994f6657d83847bdffdbd7f346754b0f"
 
+[[package]]
+name = "r-efi"
+version = "6.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf"
+
 [[package]]
 name = "rand"
-version = "0.9.2"
+version = "0.9.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6db2770f06117d490610c7488547d543617b21bfa07796d7a12f6f1bd53850d1"
+checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea"
 dependencies = [
  "rand_chacha",
  "rand_core",
@@ -1392,7 +1391,7 @@ dependencies = [
  "errno",
  "libc",
  "linux-raw-sys",
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
@@ -1421,9 +1420,9 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
 
 [[package]]
 name = "semver"
-version = "1.0.27"
+version = "1.0.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d767eb0aabc880b29956c35734170f26ed551a859dbd361d140cdbeca61ab1e2"
+checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
 dependencies = [
  "serde",
  "serde_core",
@@ -1474,9 +1473,9 @@ dependencies = [
 
 [[package]]
 name = "serde_spanned"
-version = "1.0.4"
+version = "1.1.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f8bbf91e5a4d6315eee45e704372590b30e260ee83af6639d64557f51b067776"
+checksum = "6662b5879511e06e8999a8a235d848113e942c9124f211511b16466ee2995f26"
 dependencies = [
  "serde_core",
 ]
@@ -1500,9 +1499,9 @@ checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
 
 [[package]]
 name = "simd-adler32"
-version = "0.3.8"
+version = "0.3.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e320a6c5ad31d271ad523dcf3ad13e2767ad8b1cb8f047f75a8aeaf8da139da2"
+checksum = "703d5c7ef118737c72f1af64ad2f6f8c5e1921f818cdcb97b8fe6fc69bf66214"
 
 [[package]]
 name = "similar"
@@ -1562,15 +1561,15 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.26.0"
+version = "3.27.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "82a72c767771b47409d2345987fda8628641887d5466101319899796367354a0"
+checksum = "32497e9a4c7b38532efcdebeef879707aa9f794296a4f0244f6f69e9bc8574bd"
 dependencies = [
  "fastrand",
- "getrandom 0.4.1",
+ "getrandom 0.4.2",
  "once_cell",
  "rustix",
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
@@ -1610,9 +1609,9 @@ dependencies = [
 
 [[package]]
 name = "tinystr"
-version = "0.8.2"
+version = "0.8.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "42d3e9c45c09de15d06dd8acf5f4e0e399e85927b7f00711024eb7ae10fa4869"
+checksum = "c8323304221c2a851516f22236c5722a72eaa19749016521d6dff0824447d96d"
 dependencies = [
  "displaydoc",
  "zerovec",
@@ -1630,7 +1629,7 @@ dependencies = [
  "toml_datetime",
  "toml_parser",
  "toml_writer",
- "winnow",
+ "winnow 0.7.15",
 ]
 
 [[package]]
@@ -1652,23 +1651,23 @@ dependencies = [
  "toml_datetime",
  "toml_parser",
  "toml_writer",
- "winnow",
+ "winnow 0.7.15",
 ]
 
 [[package]]
 name = "toml_parser"
-version = "1.0.9+spec-1.1.0"
+version = "1.1.2+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "702d4415e08923e7e1ef96cd5727c0dfed80b4d2fa25db9647fe5eb6f7c5a4c4"
+checksum = "a2abe9b86193656635d2411dc43050282ca48aa31c2451210f4202550afb7526"
 dependencies = [
- "winnow",
+ "winnow 1.0.2",
 ]
 
 [[package]]
 name = "toml_writer"
-version = "1.0.6+spec-1.1.0"
+version = "1.1.1+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ab16f14aed21ee8bfd8ec22513f7287cd4a91aa92e44edfe2c17ddd004e92607"
+checksum = "756daf9b1013ebe47a8776667b466417e2d4c5679d441c26230efd9ef78692db"
 
 [[package]]
 name = "typed-arena"
@@ -1684,9 +1683,9 @@ checksum = "8e28f89b80c87b8fb0cf04ab448d5dd0dd0ade2f8891bae878de66a75a28600e"
 
 [[package]]
 name = "typenum"
-version = "1.19.0"
+version = "1.20.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "562d481066bde0658276a35467c4af00bdc6ee726305698a55b86e61d7ad82bb"
+checksum = "40ce102ab67701b8526c123c1bab5cbe42d7040ccfd0f64af1a385808d2f43de"
 
 [[package]]
 name = "unarray"
@@ -1738,11 +1737,11 @@ checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
 [[package]]
 name = "uuid"
-version = "1.21.0"
+version = "1.23.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b672338555252d43fd2240c714dc444b8c6fb0a5c5335e65a07bba7742735ddb"
+checksum = "ddd74a9687298c6858e9b88ec8935ec45d22e8fd5e6394fa1bd4e99a87789c76"
 dependencies = [
- "getrandom 0.4.1",
+ "getrandom 0.4.2",
  "js-sys",
  "wasm-bindgen",
 ]
@@ -1776,11 +1775,11 @@ checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b"
 
 [[package]]
 name = "wasip2"
-version = "1.0.2+wasi-0.2.9"
+version = "1.0.3+wasi-0.2.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9517f9239f02c069db75e65f174b3da828fe5f5b945c4dd26bd25d89c03ebcf5"
+checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6"
 dependencies = [
- "wit-bindgen",
+ "wit-bindgen 0.57.1",
 ]
 
 [[package]]
@@ -1789,14 +1788,14 @@ version = "0.4.0+wasi-0.3.0-rc-2026-01-06"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5"
 dependencies = [
- "wit-bindgen",
+ "wit-bindgen 0.51.0",
 ]
 
 [[package]]
 name = "wasm-bindgen"
-version = "0.2.113"
+version = "0.2.118"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "60722a937f594b7fde9adb894d7c092fc1bb6612897c46368d18e7a20208eff2"
+checksum = "0bf938a0bacb0469e83c1e148908bd7d5a6010354cf4fb73279b7447422e3a89"
 dependencies = [
  "cfg-if",
  "once_cell",
@@ -1807,9 +1806,9 @@ dependencies = [
 
 [[package]]
 name = "wasm-bindgen-macro"
-version = "0.2.113"
+version = "0.2.118"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0fac8c6395094b6b91c4af293f4c79371c163f9a6f56184d2c9a85f5a95f3950"
+checksum = "eeff24f84126c0ec2db7a449f0c2ec963c6a49efe0698c4242929da037ca28ed"
 dependencies = [
  "quote",
  "wasm-bindgen-macro-support",
@@ -1817,9 +1816,9 @@ dependencies = [
 
 [[package]]
 name = "wasm-bindgen-macro-support"
-version = "0.2.113"
+version = "0.2.118"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ab3fabce6159dc20728033842636887e4877688ae94382766e00b180abac9d60"
+checksum = "9d08065faf983b2b80a79fd87d8254c409281cf7de75fc4b773019824196c904"
 dependencies = [
  "bumpalo",
  "proc-macro2",
@@ -1830,9 +1829,9 @@ dependencies = [
 
 [[package]]
 name = "wasm-bindgen-shared"
-version = "0.2.113"
+version = "0.2.118"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "de0e091bdb824da87dc01d967388880d017a0a9bc4f3bdc0d86ee9f9336e3bb5"
+checksum = "5fd04d9e306f1907bd13c6361b5c6bfc7b3b3c095ed3f8a9246390f8dbdee129"
 dependencies = [
  "unicode-ident",
 ]
@@ -1873,13 +1872,11 @@ dependencies = [
 
 [[package]]
 name = "which"
-version = "8.0.0"
+version = "8.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d3fabb953106c3c8eea8306e4393700d7657561cb43122571b172bbfb7c7ba1d"
+checksum = "81995fafaaaf6ae47a7d0cc83c67caf92aeb7e5331650ae6ff856f7c0c60c459"
 dependencies = [
- "env_home",
- "rustix",
- "winsafe",
+ "libc",
 ]
 
 [[package]]
@@ -1917,7 +1914,7 @@ version = "0.1.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22"
 dependencies = [
- "windows-sys 0.61.2",
+ "windows-sys",
 ]
 
 [[package]]
@@ -1926,15 +1923,6 @@ version = "0.2.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f0805222e57f7521d6a62e36fa9163bc891acd422f971defe97d64e70d0a4fe5"
 
-[[package]]
-name = "windows-sys"
-version = "0.59.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b"
-dependencies = [
- "windows-targets",
-]
-
 [[package]]
 name = "windows-sys"
 version = "0.61.2"
@@ -1944,84 +1932,20 @@ dependencies = [
  "windows-link",
 ]
 
-[[package]]
-name = "windows-targets"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
-dependencies = [
- "windows_aarch64_gnullvm",
- "windows_aarch64_msvc",
- "windows_i686_gnu",
- "windows_i686_gnullvm",
- "windows_i686_msvc",
- "windows_x86_64_gnu",
- "windows_x86_64_gnullvm",
- "windows_x86_64_msvc",
-]
-
-[[package]]
-name = "windows_aarch64_gnullvm"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
-
-[[package]]
-name = "windows_aarch64_msvc"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
-
-[[package]]
-name = "windows_i686_gnu"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
-
-[[package]]
-name = "windows_i686_gnullvm"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
-
-[[package]]
-name = "windows_i686_msvc"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
-
-[[package]]
-name = "windows_x86_64_gnu"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
-
-[[package]]
-name = "windows_x86_64_gnullvm"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
-
-[[package]]
-name = "windows_x86_64_msvc"
-version = "0.52.6"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
-
 [[package]]
 name = "winnow"
-version = "0.7.14"
+version = "0.7.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a5364e9d77fcdeeaa6062ced926ee3381faa2ee02d3eb83a5c27a8825540829"
+checksum = "df79d97927682d2fd8adb29682d1140b343be4ac0f08fd68b7765d9c059d3945"
 dependencies = [
  "memchr",
 ]
 
 [[package]]
-name = "winsafe"
-version = "0.0.19"
+name = "winnow"
+version = "1.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d135d17ab770252ad95e9a872d365cf3090e3be864a34ab46f48555993efc904"
+checksum = "2ee1708bef14716a11bae175f579062d4554d95be2c6829f518df847b7b3fdd0"
 
 [[package]]
 name = "wit-bindgen"
@@ -2032,6 +1956,12 @@ dependencies = [
  "wit-bindgen-rust-macro",
 ]
 
+[[package]]
+name = "wit-bindgen"
+version = "0.57.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e"
+
 [[package]]
 name = "wit-bindgen-core"
 version = "0.51.0"
@@ -2113,15 +2043,15 @@ dependencies = [
 
 [[package]]
 name = "writeable"
-version = "0.6.2"
+version = "0.6.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9edde0db4769d2dc68579893f2306b26c6ecfbe0ef499b013d731b7b9247e0b9"
+checksum = "1ffae5123b2d3fc086436f8834ae3ab053a283cfac8fe0a0b8eaae044768a4c4"
 
 [[package]]
 name = "yoke"
-version = "0.8.1"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "72d6e5c6afb84d73944e5cedb052c4680d5657337201555f9f2a16b7406d4954"
+checksum = "abe8c5fda708d9ca3df187cae8bfb9ceda00dd96231bed36e445a1a48e66f9ca"
 dependencies = [
  "stable_deref_trait",
  "yoke-derive",
@@ -2130,9 +2060,9 @@ dependencies = [
 
 [[package]]
 name = "yoke-derive"
-version = "0.8.1"
+version = "0.8.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b659052874eb698efe5b9e8cf382204678a0086ebf46982b79d6ca3182927e5d"
+checksum = "de844c262c8848816172cef550288e7dc6c7b7814b4ee56b3e1553f275f1858e"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -2142,18 +2072,18 @@ dependencies = [
 
 [[package]]
 name = "zerocopy"
-version = "0.8.40"
+version = "0.8.48"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a789c6e490b576db9f7e6b6d661bcc9799f7c0ac8352f56ea20193b2681532e5"
+checksum = "eed437bf9d6692032087e337407a86f04cd8d6a16a37199ed57949d415bd68e9"
 dependencies = [
  "zerocopy-derive",
 ]
 
 [[package]]
 name = "zerocopy-derive"
-version = "0.8.40"
+version = "0.8.48"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f65c489a7071a749c849713807783f70672b28094011623e200cb86dcb835953"
+checksum = "70e3cd084b1788766f53af483dd21f93881ff30d7320490ec3ef7526d203bad4"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -2162,18 +2092,18 @@ dependencies = [
 
 [[package]]
 name = "zerofrom"
-version = "0.1.6"
+version = "0.1.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "50cc42e0333e05660c3587f3bf9d0478688e15d870fab3346451ce7f8c9fbea5"
+checksum = "69faa1f2a1ea75661980b013019ed6687ed0e83d069bc1114e2cc74c6c04c4df"
 dependencies = [
  "zerofrom-derive",
 ]
 
 [[package]]
 name = "zerofrom-derive"
-version = "0.1.6"
+version = "0.1.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d71e5d6e06ab090c67b5e44993ec16b72dcbaabc526db883a360057678b48502"
+checksum = "11532158c46691caf0f2593ea8358fed6bbf68a0315e80aae9bd41fbade684a1"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -2183,9 +2113,9 @@ dependencies = [
 
 [[package]]
 name = "zerotrie"
-version = "0.2.3"
+version = "0.2.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a59c17a5562d507e4b54960e8569ebee33bee890c70aa3fe7b97e85a9fd7851"
+checksum = "0f9152d31db0792fa83f70fb2f83148effb5c1f5b8c7686c3459e361d9bc20bf"
 dependencies = [
  "displaydoc",
  "yoke",
@@ -2194,9 +2124,9 @@ dependencies = [
 
 [[package]]
 name = "zerovec"
-version = "0.11.5"
+version = "0.11.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6c28719294829477f525be0186d13efa9a3c602f7ec202ca9e353d310fb9a002"
+checksum = "90f911cbc359ab6af17377d242225f4d75119aec87ea711a880987b18cd7b239"
 dependencies = [
  "yoke",
  "zerofrom",
@@ -2205,9 +2135,9 @@ dependencies = [
 
 [[package]]
 name = "zerovec-derive"
-version = "0.11.2"
+version = "0.11.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "eadce39539ca5cb3985590102671f2567e659fca9666581ad3411d59207951f3"
+checksum = "625dc425cab0dca6dc3c3319506e6593dcb08a9f387ea3b284dbd52a92c40555"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -2216,9 +2146,9 @@ dependencies = [
 
 [[package]]
 name = "zip"
-version = "8.1.0"
+version = "8.5.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6e499faf5c6b97a0d086f4a8733de6d47aee2252b8127962439d8d4311a73f72"
+checksum = "dcab981e19633ebcf0b001ddd37dd802996098bc1864f90b7c5d970ce76c1d59"
 dependencies = [
  "crc32fast",
  "flate2",
@@ -2230,9 +2160,9 @@ dependencies = [
 
 [[package]]
 name = "zlib-rs"
-version = "0.6.2"
+version = "0.6.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c745c48e1007337ed136dc99df34128b9faa6ed542d80a1c673cf55a6d7236c8"
+checksum = "3be3d40e40a133f9c916ee3f9f4fa2d9d63435b5fbe1bfc6d9dae0aa0ada1513"
 
 [[package]]
 name = "zmij"
diff --git a/creusot-install/src/main.rs b/creusot-install/src/main.rs
index 14583b2cb6..fe2b077c8c 100644
--- a/creusot-install/src/main.rs
+++ b/creusot-install/src/main.rs
@@ -1,4 +1,3 @@
-#![feature(exit_status_error, try_blocks)]
 use anyhow::{Context as _, anyhow, bail};
 use clap::*;
 use creusot_setup::{self as setup, Binary, CreusotPaths, tools_versions_urls::*};
diff --git a/creusot-std/src/ghost.rs b/creusot-std/src/ghost.rs
index d991df162b..c75bb81771 100644
--- a/creusot-std/src/ghost.rs
+++ b/creusot-std/src/ghost.rs
@@ -262,6 +262,9 @@ macro_rules! define_objective {
         /// `Unique<T>` (and therefore `Box<T>`, `Vec<T>`, ...) are therefore objective.
         #[trusted]
         pub auto trait Objective {}
+
+        #[trusted]
+        impl !Objective for NotObjective {}
     };
 }
 
@@ -276,7 +279,3 @@ define_objective! {}
 /// This negative implementation primarily targets `Perm<PermCell<T>>` and
 /// `Perm<*const T>`.
 pub(crate) struct NotObjective {}
-
-#[cfg(creusot)]
-#[trusted]
-impl !Objective for NotObjective {}
diff --git a/creusot-std/src/lib.rs b/creusot-std/src/lib.rs
index 36b4f767fa..50095cdab2 100644
--- a/creusot-std/src/lib.rs
+++ b/creusot-std/src/lib.rs
@@ -47,38 +47,30 @@
 #![cfg_attr(feature = "nightly", allow(incomplete_features, internal_features))]
 #![cfg_attr(
     feature = "nightly",
+    feature(step_trait, allocator_api, unboxed_closures, tuple_trait, edition_panic)
+)]
+#![cfg_attr(
+    creusot,
     feature(
         core_intrinsics,
         const_destruct,
         fn_traits,
-        fmt_internals,
         fmt_arguments_from_str,
         fmt_helpers_for_derive,
-        step_trait,
         try_trait_v2,
-        allocator_api,
-        unboxed_closures,
-        tuple_trait,
         panic_internals,
-        never_type,
         ptr_metadata,
         hint_must_use,
         pointer_is_aligned_to,
-        edition_panic,
-        new_range_api,
         range_bounds_is_empty,
         bound_copied,
-        decl_macro,
         auto_traits,
+        new_range_api_legacy,
         negative_impls,
-        clone_from_ref,
     )
 )]
 #![cfg_attr(all(doc, feature = "nightly"), feature(intra_doc_pointers))]
-#![cfg_attr(
-    all(feature = "nightly", feature = "std"),
-    feature(print_internals, libstd_sys_internals, rt,)
-)]
+#![cfg_attr(all(creusot, feature = "std"), feature(print_internals, libstd_sys_internals, rt,))]
 #![cfg_attr(not(feature = "std"), no_std)]
 
 extern crate alloc;
diff --git a/creusot/src/analysis.rs b/creusot/src/analysis.rs
index 088560ae75..d89f47b0b6 100644
--- a/creusot/src/analysis.rs
+++ b/creusot/src/analysis.rs
@@ -21,7 +21,7 @@ use rustc_index::{Idx as _, bit_set::MixedBitSet};
 use rustc_macros::{TyDecodable, TyEncodable};
 use rustc_middle::{
     mir::{self, BasicBlock, Local, Location, Place, traversal},
-    ty::{self, TyCtxt, TypingEnv},
+    ty::{self, TyCtxt, TypingEnv, Unnormalized},
 };
 use rustc_mir_dataflow::{
     Analysis as _, ResultsCursor,
@@ -275,7 +275,7 @@ impl<'a, 'tcx> HasMoveData<'tcx> for Analysis<'a, 'tcx> {
 fn local_typing_env(tcx: TyCtxt<'_>, def_id: DefId) -> TypingEnv<'_> {
     let param_env = tcx.param_env(def_id);
     let typing_mode = ty::TypingMode::post_borrowck_analysis(tcx, def_id.as_local().unwrap());
-    TypingEnv { typing_mode, param_env }
+    TypingEnv::new(param_env, typing_mode)
 }
 
 impl<'a, 'tcx> Analysis<'a, 'tcx> {
@@ -446,7 +446,7 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
                 continue;
             }
             let ty = pl.ty(&self.body().local_decls, self.tcx());
-            let ty = self.tcx().normalize_erasing_regions(self.typing_env, ty);
+            let ty = self.tcx().normalize_erasing_regions(self.typing_env, Unnormalized::new(ty));
             use TyKind::*;
             match ty.ty.kind() {
                 Adt(adt_def, subst) => {
@@ -517,7 +517,7 @@ impl<'a, 'tcx> Analysis<'a, 'tcx> {
                 | Foreign(_)
                 | Str
                 | RawPtr(_, _)
-                | Alias(_, _)
+                | Alias(_)
                 | Param(_)
                 | Bound(_, _)
                 | Placeholder(_)
@@ -915,7 +915,7 @@ pub(crate) fn run_with_specs<'tcx>(
     let tree = fmir::ScopeTree::build(&body.body, &body_locals.locals);
     let clos_subst = tcx.is_closure_like(def_id).then(|| {
         let loc = body_locals.vars.get_index(1).unwrap();
-        let ty_env = tcx.type_of(def_id).instantiate_identity();
+        let ty_env = tcx.type_of(def_id).instantiate_identity().skip_normalization();
         let TyKind::Closure(_, subst) = ty_env.kind() else { unreachable!() };
         let self_ = Term::var(*loc.0, loc.1.ty);
         let self_ = match subst.as_closure().kind() {
@@ -996,10 +996,8 @@ impl<'tcx> BodyLocals<'tcx> {
                 } else {
                     (Ident::fresh(ctx.crate_name(), &format!("_{}", idx)), LocalKind::Temp)
                 };
-                (
-                    (ident, fmir::LocalDecl { span: d.source_info.span, ty: d.ty, kind }),
-                    (loc, ident),
-                )
+                let ty = ctx.erase_and_anonymize_regions(d.ty);
+                ((ident, fmir::LocalDecl { span: d.source_info.span, ty, kind }), (loc, ident))
             })
             .unzip();
         BodyLocals { vars, locals }
diff --git a/creusot/src/analysis/borrows.rs b/creusot/src/analysis/borrows.rs
index 8c29a3e1d3..a91972a3d7 100644
--- a/creusot/src/analysis/borrows.rs
+++ b/creusot/src/analysis/borrows.rs
@@ -70,8 +70,6 @@ impl<'a, 'mir, 'tcx> Borrows<'a, 'mir, 'tcx> {
 
     /// Kill any borrows that conflict with `place`.
     fn kill_borrows_on_place(&self, trans: &mut impl GenKill<BorrowIndex>, place: Place<'tcx>) {
-        debug!("kill_borrows_on_place: place={:?}", place);
-
         let other_borrows_of_local = self
             .borrow_set
             .local_map()
diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs
index da026fcf99..91ba22b2da 100644
--- a/creusot/src/backend/clone_map.rs
+++ b/creusot/src/backend/clone_map.rs
@@ -20,6 +20,7 @@ use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::ty::{
     GenericArgsRef, List, Ty, TyCtxt, TyKind, TypeFoldable, TypeVisitableExt, TypingEnv,
+    Unnormalized,
 };
 use rustc_span::Span;
 use why3::{
@@ -131,9 +132,11 @@ pub(crate) trait Namer<'tcx> {
         self.dependency(Dependency::PrivateResolve(struct_id, subst)).ident()
     }
 
-    // TODO: get rid of this. It feels like it should be unnecessary
+    /// Ideally we'd like to avoid caring about normalization in the backend,
+    /// but we still need this for normalizing field types after instantiation.
+    /// Also for normalizing RPITs but that seems easier to get rid of if we ever care to.
     fn normalize<T: TypeFoldable<TyCtxt<'tcx>>>(&self, ty: T) -> T {
-        self.tcx().normalize_erasing_regions(self.typing_env(), ty)
+        self.tcx().normalize_erasing_regions(self.typing_env(), Unnormalized::new(ty))
     }
 
     fn import_prelude_module(&self, module: PreMod) {
diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs
index 0509cce461..292c44ced5 100644
--- a/creusot/src/backend/clone_map/elaborator.rs
+++ b/creusot/src/backend/clone_map/elaborator.rs
@@ -31,7 +31,7 @@ use rustc_middle::ty::{
     self, AliasTyKind, Const, GenericArg, GenericArgsRef, TraitRef, Ty, TyCtxt, TyKind, TypingEnv,
 };
 use rustc_span::{DUMMY_SP, Span, Symbol};
-use rustc_type_ir::{ClosureKind, ConstKind, EarlyBinder};
+use rustc_type_ir::{AliasTy, ClosureKind, ConstKind, EarlyBinder};
 use std::{
     assert_matches,
     cell::RefCell,
@@ -119,9 +119,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
 
         let name = names.dependency(dep).ident();
 
-        let mut pre_sig = EarlyBinder::bind(ctx.sig(def_id).clone())
-            .instantiate(ctx.tcx, subst)
-            .normalize(ctx, typing_env);
+        let mut pre_sig = ctx.sig(def_id).clone().instantiate_and_normalize(ctx, subst, typing_env);
 
         if ctx.def_kind(def_id) == DefKind::Closure {
             // Inline the body of closures
@@ -221,9 +219,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
         }
 
         let typing_env = self.typing_env;
-        let pre_sig = EarlyBinder::bind(ctx.sig(def_id).clone())
-            .instantiate(ctx.tcx, subst)
-            .normalize(ctx, typing_env);
+        let pre_sig = ctx.sig(def_id).clone().instantiate_and_normalize(ctx, subst, typing_env);
 
         let bound: Box<[Ident]> = pre_sig.inputs.iter().map(|(ident, _, _)| ident.0).collect();
         let trait_resol = TraitResolved::resolve_item(self.tcx(), typing_env, def_id, subst);
@@ -265,8 +261,9 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
                 let args_tup = Term::var(args_id, subst.type_at(0));
 
                 let res_id = Ident::fresh_local("res").into();
-                let res_ty = ctx.instantiate_bound_regions_with_erased(
-                    ctx.fn_sig(did_f).instantiate(ctx.tcx, subst_f).output(),
+                let res_ty = ctx.normalize_erasing_late_bound_regions(
+                    names.typing_env(),
+                    ctx.fn_sig(did_f).instantiate(ctx.tcx, subst_f).skip_normalization().output(),
                 );
                 let res = Term::var(res_id, res_ty);
 
@@ -330,7 +327,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
             .tcx()
             .layout_of(ty::PseudoCanonicalInput { typing_env: self.typing_env, value: ty })
             .is_err();
-        if size_unknown && self.ctx.is_nonzero_sized(ty) {
+        if size_unknown && self.ctx.is_nonzero_sized(self.typing_env, ty) {
             Some(Decl::Axiom(Axiom {
                 name: Ident::fresh_local(format!("nonzero_{}", name.name().to_string())),
                 rewrite: false,
@@ -373,9 +370,7 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
 
         let mut names = self.namer(dep);
         let name = names.dependency(dep).ident();
-        let mut pre_sig = EarlyBinder::bind(ctx.sig(def_id).clone())
-            .instantiate(ctx.tcx, subst)
-            .normalize(ctx, typing_env);
+        let mut pre_sig = ctx.sig(def_id).clone().instantiate_and_normalize(ctx, subst, typing_env);
         sig_add_type_invariant_spec(ctx, typing_env, names.source_id(), &mut pre_sig, def_id);
         let sig = lower_logic_sig(ctx, &names, name, pre_sig, def_id);
 
@@ -466,10 +461,13 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
                 ty_name: names.ty(ty).to_ident(),
                 ty_params: Box::new([]),
             })],
-            TyKind::Alias(AliasTyKind::Opaque | AliasTyKind::Projection, _) => {
-                let (def_id, subst) = dep.did().unwrap();
+            &TyKind::Alias(AliasTy {
+                kind: AliasTyKind::Opaque { def_id } | AliasTyKind::Projection { def_id },
+                args,
+                ..
+            }) => {
                 vec![Decl::TyDecl(TyDecl::Opaque {
-                    ty_name: names.def_ty(def_id, subst).to_ident(),
+                    ty_name: names.def_ty(def_id, args).to_ident(),
                     ty_params: Box::new([]),
                 })]
             }
@@ -959,10 +957,7 @@ fn post_fndef<'tcx>(
     if is_logic(ctx.tcx, did) {
         return None;
     }
-
-    let mut sig = EarlyBinder::bind(ctx.sig(did).clone())
-        .instantiate(ctx.tcx, subst)
-        .normalize(ctx, names.typing_env());
+    let mut sig = ctx.sig(did).clone().instantiate_and_normalize(ctx, subst, names.typing_env());
     sig_add_type_invariant_spec(ctx, names.typing_env(), names.source_id(), &mut sig, did);
     let mut post = sig.contract.ensures_conj(ctx.tcx);
     post.subst(&HashMap::from([(name::result(), res.kind)]));
@@ -1044,9 +1039,7 @@ fn pre_fndef<'tcx>(
         // precondition if called in a program via a generic.
         return None;
     }
-    let mut sig = EarlyBinder::bind(ctx.sig(did).clone())
-        .instantiate(ctx.tcx, subst)
-        .normalize(ctx, names.typing_env());
+    let mut sig = ctx.sig(did).clone().instantiate_and_normalize(ctx, subst, names.typing_env());
     sig_add_type_invariant_spec(ctx, names.typing_env(), names.source_id(), &mut sig, did);
     let pre = sig.contract.requires_conj(ctx.tcx);
     let pattern = Pattern::tuple(
@@ -1286,7 +1279,7 @@ fn term<'tcx>(
         Intrinsic::MetadataMatches => metadata_matches_term(ctx, names, subst, bound),
         _ => {
             let term = EarlyBinder::bind(ctx.term(def_id).unwrap().rename(bound));
-            Some(normalize(ctx, typing_env, term.instantiate(ctx.tcx, subst)))
+            Some(normalize(ctx, typing_env, term.instantiate(ctx.tcx, subst).skip_normalization()))
         }
     }
 }
diff --git a/creusot/src/backend/closures.rs b/creusot/src/backend/closures.rs
index a3f58ca242..fb515c3358 100644
--- a/creusot/src/backend/closures.rs
+++ b/creusot/src/backend/closures.rs
@@ -25,7 +25,9 @@ fn closure_captures<'tcx>(
     tcx: TyCtxt<'tcx>,
     def_id: LocalDefId,
 ) -> impl Iterator<Item = (FieldIdx, &'tcx CapturedPlace<'tcx>, Ty<'tcx>)> {
-    let TyKind::Closure(_, subst) = tcx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        tcx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     tcx.closure_captures(def_id)
@@ -41,7 +43,9 @@ pub(crate) fn closure_hist_inv<'tcx>(
     self_: Term<'tcx>,
     future: Term<'tcx>,
 ) -> Term<'tcx> {
-    let TyKind::Closure(_, subst) = ctx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        ctx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     let closure_kind = subst.as_closure().kind();
@@ -82,7 +86,9 @@ pub(crate) fn closure_pre<'tcx>(
     args: Term<'tcx>,
 ) -> Term<'tcx> {
     let typing_env = ctx.typing_env(def_id.into());
-    let TyKind::Closure(_, subst) = ctx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        ctx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     let closure_kind = subst.as_closure().kind();
@@ -145,7 +151,9 @@ pub(crate) fn closure_post<'tcx>(
     args: Term<'tcx>,
     result_state: Option<Term<'tcx>>,
 ) -> Term<'tcx> {
-    let TyKind::Closure(_, subst) = ctx.type_of(def_id).instantiate_identity().kind() else {
+    let TyKind::Closure(_, subst) =
+        ctx.type_of(def_id).instantiate_identity().skip_normalization().kind()
+    else {
         unreachable!()
     };
     let closure_kind = subst.as_closure().kind();
diff --git a/creusot/src/backend/dependency.rs b/creusot/src/backend/dependency.rs
index d4cd070956..eced6bb43f 100644
--- a/creusot/src/backend/dependency.rs
+++ b/creusot/src/backend/dependency.rs
@@ -3,7 +3,7 @@ use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_macros::{TypeFoldable, TypeVisitable};
 use rustc_middle::ty::{GenericArgKind, GenericArgsRef, List, Ty, TyCtxt, TyKind};
 use rustc_span::Symbol;
-use rustc_type_ir::AliasTyKind;
+use rustc_type_ir::{AliasTy, AliasTyKind};
 
 use crate::{
     contracts_items::Intrinsic,
@@ -38,9 +38,11 @@ impl<'tcx> Dependency<'tcx> {
             Dependency::Type(t) => match t.kind() {
                 TyKind::Adt(def, substs) => Some((def.did(), substs)),
                 TyKind::Closure(id, substs) => Some((*id, substs)),
-                TyKind::Alias(AliasTyKind::Opaque | AliasTyKind::Projection, aty) => {
-                    Some((aty.def_id, aty.args))
-                }
+                &TyKind::Alias(AliasTy {
+                    kind: AliasTyKind::Opaque { def_id } | AliasTyKind::Projection { def_id },
+                    args,
+                    ..
+                }) => Some((def_id, args)),
                 _ => None,
             },
             _ => None,
@@ -76,7 +78,7 @@ impl<'tcx> Dependency<'tcx> {
                 _ if Intrinsic::SizeOfLogic.is(ctx, did) => {
                     Some(Symbol::intern(&type_string(ctx.tcx, "size_of".into(), subst.type_at(0))))
                 }
-                DefKind::Const | DefKind::AssocConst | DefKind::ConstParam => ctx
+                DefKind::Const { .. } | DefKind::AssocConst { .. } | DefKind::ConstParam => ctx
                     .opt_item_name(did)
                     .map(|name| Symbol::intern(&lowercase_prefix("const_", name.as_str()))),
                 _ => {
@@ -88,7 +90,10 @@ impl<'tcx> Dependency<'tcx> {
                         && let Some(trait_ref) = ctx.impl_opt_trait_ref(parent)
                     {
                         // AssocFn in a trait impl: get the instantiated Self type
-                        first_ty_arg(trait_ref.instantiate(ctx.tcx, subst).args)
+                        // Skip normalization: we are generating names so it doesn't really matter
+                        first_ty_arg(
+                            trait_ref.instantiate(ctx.tcx, subst).skip_normalization().args,
+                        )
                     } else {
                         // AssocFn in a trait or in an inherent impl: Self is the first argument in `subst`
                         // And for plain fn, also display the first type argument in its name.
diff --git a/creusot/src/backend/logic.rs b/creusot/src/backend/logic.rs
index e27961faa2..eebf4c8adc 100644
--- a/creusot/src/backend/logic.rs
+++ b/creusot/src/backend/logic.rs
@@ -23,7 +23,7 @@ mod vcgen;
 
 pub(crate) fn translate_logic(ctx: &Why3Generator, def_id: DefId) -> Option<FileModule> {
     let names = Dependencies::new(ctx, def_id);
-    let pre_sig = ctx.sig(def_id).clone().normalize(ctx, ctx.typing_env(def_id));
+    let pre_sig = ctx.sig(def_id).clone().normalize_contract(ctx, ctx.typing_env(def_id));
 
     let namespace_ty = names.namespace_ty();
 
diff --git a/creusot/src/backend/logic/vcgen.rs b/creusot/src/backend/logic/vcgen.rs
index 138ed93841..6d7188a43b 100644
--- a/creusot/src/backend/logic/vcgen.rs
+++ b/creusot/src/backend/logic/vcgen.rs
@@ -174,7 +174,7 @@ impl<'tcx> VCGen<'_, 'tcx> {
                 }
                 // We pull (id, subst) as a dependency, because it may be useful for the proof
                 let item_name = self.names.item(id, subst);
-                if let TyKind::FnDef(_, _) = self.ctx.type_of(id).instantiate_identity().kind() {
+                if let TyKind::FnDef(_, _) = self.ctx.type_of(id).instantiate_identity().skip_normalization().kind() {
                     k(Exp::unit())
                 } else {
                     k(Exp::Var(item_name))
@@ -195,18 +195,17 @@ impl<'tcx> VCGen<'_, 'tcx> {
             // VC(f As, Q) = VC(A0, |a0| ... VC(An, |an|
             //  pre(f)(a0..an) /\ variant(f)(a0..an) /\ (post(f)(a0..an, F(a0..an)) -> Q(F a0..an))
             // ))
-            TermKind::Call { id, subst, args } => self.build_wp_slice(args, &|args| {
-                let pre_sig = EarlyBinder::bind(self.ctx.sig(*id).clone())
+            &TermKind::Call { id, subst, ref args } => self.build_wp_slice(args, &|args| {
+                let pre_sig = EarlyBinder::bind(self.ctx.sig(id).clone())
                     .instantiate(self.ctx.tcx, subst)
-                    .normalize(self.ctx, self.typing_env);
+                    .skip_normalization().normalize_contract(self.ctx, self.typing_env);
 
-                let variant = if self.ctx.should_check_variant_decreases(self.self_id, *id) {
-                    let subst = self.ctx.normalize_erasing_regions(self.typing_env, *subst);
-                    let subst_id = erased_identity_for_item(self.ctx.tcx, *id);
+                let variant = if self.ctx.should_check_variant_decreases(self.self_id, id) {
+                    let subst_id = erased_identity_for_item(self.ctx.tcx, id);
                     if subst != subst_id {
                         self.ctx.crash_and_error(t.span, "polymorphic recursion is not supported.")
                     }
-                    if self.self_id != *id {
+                    if self.self_id != id {
                         self.ctx
                             .dcx()
                             .struct_span_fatal(
@@ -215,7 +214,7 @@ impl<'tcx> VCGen<'_, 'tcx> {
                             )
                             .with_note(format!(
                                 "calling {} from {}",
-                                self.ctx.def_path_str(*id),
+                                self.ctx.def_path_str(id),
                                 self.ctx.def_path_str(self.self_id)
                             ))
                             .emit();
@@ -234,8 +233,8 @@ impl<'tcx> VCGen<'_, 'tcx> {
                     Exp::mk_true()
                 };
 
-                let mut call = Exp::Var(self.names.item(*id, subst)).app(args.clone());
-                if is_builtin_ascription(self.ctx.tcx, *id) {
+                let mut call = Exp::Var(self.names.item(id, subst)).app(args.clone());
+                if is_builtin_ascription(self.ctx.tcx, id) {
                     call = call.ascribe(self.ty(t.ty, t.span))
                 }
                 let call_subst = pre_sig
@@ -248,7 +247,7 @@ impl<'tcx> VCGen<'_, 'tcx> {
                 let mut contract = lower_contract(self.ctx, self.names, pre_sig.contract);
                 contract.subst(&call_subst);
 
-                let name = self.ctx.item_name(*id);
+                let name = self.ctx.item_name(id);
                 let name = name.as_str();
                 contract
                     .requires_conj(name)
@@ -305,8 +304,7 @@ impl<'tcx> VCGen<'_, 'tcx> {
             }
             // VC((T...), Q) = VC(T[0], |t0| ... VC(T[N], |tn| Q(t0..tn))))
             TermKind::Tuple { fields } => {
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, t.ty);
-                let TyKind::Tuple(args) = ty.kind() else { unreachable!() };
+                let TyKind::Tuple(args) = t.ty.kind() else { unreachable!() };
                 self.build_wp_slice(fields, &|flds| match flds.len() {
                     0 => k(Exp::unit()),
                     1 => k(flds.into_iter().next().unwrap()),
@@ -323,8 +321,7 @@ impl<'tcx> VCGen<'_, 'tcx> {
             }
             // Same as for tuples
             TermKind::Constructor { variant, fields, .. } => {
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, t.ty);
-                let TyKind::Adt(adt, subst) = ty.kind() else { unreachable!() };
+                let TyKind::Adt(adt, subst) = t.ty.kind() else { unreachable!() };
                 self.build_wp_slice(fields, &|fields| {
                     let ctor = constructor(self.names, fields, adt.variant(*variant).def_id, subst);
                     k(ctor)
@@ -377,8 +374,7 @@ impl<'tcx> VCGen<'_, 'tcx> {
             }),
             // VC(A.f, Q) = VC(A, |a| Q(a.f))
             TermKind::Projection { lhs, idx } => {
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, lhs.ty);
-                let field = match ty.kind() {
+                let field = match lhs.ty.kind() {
                     TyKind::Closure(did, substs) => self.names.field(*did, substs, *idx),
                     TyKind::Adt(def, subst) => self.names.field(def.did(), subst, *idx),
                     TyKind::Tuple(tys) if tys.len() == 1 => return self.build_wp(lhs, k),
@@ -391,7 +387,7 @@ impl<'tcx> VCGen<'_, 'tcx> {
             // VC(&mut (*A).f, Q) = VC(A, |a| Q(&mut (*a).f))
             TermKind::Reborrow { inner, projections } => {
                 // FIXME: this does not generate VCs for bounds of indices in ProjectionElem::Index
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, inner.ty);
+                let ty = inner.ty;
                 self.build_wp(inner, &|inner| {
                     self.build_wp_projections(projections, &|projs| {
                         let borrow_id = borrow_generated_id(
diff --git a/creusot/src/backend/program.rs b/creusot/src/backend/program.rs
index dee3995abd..d7d365ab17 100644
--- a/creusot/src/backend/program.rs
+++ b/creusot/src/backend/program.rs
@@ -150,17 +150,12 @@ pub(crate) fn to_why_body<'tcx>(
     let mut body =
         why_body(ctx, names, body_id, None, &args, name::return_(), &mut recursive_calls);
     let (mut sig, variant) = {
-        let typing_env = names.typing_env();
-        let mut pre_sig = sig.clone().normalize(ctx, typing_env);
-        let variant = pre_sig.contract.variant.clone();
-        sig_add_type_invariant_spec(
-            ctx,
-            names.typing_env(),
-            names.source_id(),
-            &mut pre_sig,
-            def_id,
-        );
-        (lower_program_sig(ctx, names, name, pre_sig, def_id, name::return_()), variant)
+        let mut sig = sig.clone();
+        // normalize any RPITs away
+        sig.output = names.normalize(sig.output);
+        let variant = sig.contract.variant.clone();
+        sig_add_type_invariant_spec(ctx, names.typing_env(), names.source_id(), &mut sig, def_id);
+        (lower_program_sig(ctx, names, name, sig, def_id, name::return_()), variant)
     };
 
     let fmir_body = ctx.fmir_body(body_id).clone();
@@ -303,7 +298,10 @@ pub fn why_body<'tcx>(
 ) -> Expr {
     let mut body = ctx.fmir_body(body_id).clone();
     body = if let Some(subst) = subst {
-        ty::EarlyBinder::bind(body).instantiate(ctx.tcx, subst)
+        ctx.tcx.normalize_erasing_regions(
+            names.typing_env(),
+            ty::EarlyBinder::bind(body).instantiate(ctx.tcx, subst),
+        )
     } else {
         body
     };
@@ -1077,13 +1075,8 @@ fn mk_adt_switch<'tcx>(
                 .iter_enumerated()
                 .map(|(ix, field)| {
                     let id: Ident = Ident::fresh_local(format!("x{}", ix.as_usize()));
-                    (
-                        Param::Term(
-                            id,
-                            translate_ty(ctx, names, DUMMY_SP, field.ty(ctx.tcx, subst)),
-                        ),
-                        Exp::var(id),
-                    )
+                    let ty = lower.names.normalize(field.ty(ctx.tcx, subst));
+                    (Param::Term(id, translate_ty(ctx, names, DUMMY_SP, ty)), Exp::var(id))
                 })
                 .unzip();
 
diff --git a/creusot/src/backend/projections.rs b/creusot/src/backend/projections.rs
index f35841fe77..25b29f89a2 100644
--- a/creusot/src/backend/projections.rs
+++ b/creusot/src/backend/projections.rs
@@ -119,9 +119,10 @@ pub(crate) fn projections_to_expr<'tcx, 'a>(
                         .fields
                         .iter()
                         .map(|f| {
+                            let ty = names.normalize(f.ty(names.tcx(), subst));
                             Param::Term(
                                 Ident::fresh_local(format!("r{}", f.name)),
-                                translate_ty(ctx, names, span, f.ty(names.tcx(), subst)),
+                                translate_ty(ctx, names, span, ty),
                             )
                         })
                         .collect();
@@ -404,8 +405,9 @@ pub(crate) fn projections_term<'tcx, 'a, V: Debug>(
     }
 
     let subjty = subject.ty;
-    match state {
+    let term = match state {
         Pat(pat, t) => subject.match_([(pat, t), (Pattern::wildcard(subjty), default.unwrap())]),
         Trm(trm) => trm(subject),
-    }
+    };
+    ctx.erase_and_anonymize_regions(term)
 }
diff --git a/creusot/src/backend/resolve.rs b/creusot/src/backend/resolve.rs
index 7c25261439..23c68a5e0c 100644
--- a/creusot/src/backend/resolve.rs
+++ b/creusot/src/backend/resolve.rs
@@ -2,7 +2,7 @@ use std::collections::HashSet;
 
 use rustc_ast::Mutability;
 use rustc_hir::def_id::DefId;
-use rustc_middle::ty::{GenericArg, Ty, TypingEnv};
+use rustc_middle::ty::{GenericArg, Ty, TypingEnv, Unnormalized};
 use rustc_span::{DUMMY_SP, Span};
 use rustc_type_ir::TyKind;
 
@@ -60,14 +60,18 @@ pub fn is_resolve_trivial<'tcx>(
                     return false;
                 }
                 AdtKind::Box(ty) | AdtKind::Ghost(ty) => stack.push(ty),
-                AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => stack.extend(
-                    def.all_fields()
-                        .map(|f| ctx.normalize_erasing_regions(typing_env, f.ty(ctx.tcx, subst))),
-                ),
+                AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => {
+                    stack.extend(def.all_fields().map(|f| {
+                        ctx.normalize_erasing_regions(
+                            typing_env,
+                            Unnormalized::new(f.ty(ctx.tcx, subst)),
+                        )
+                    }))
+                }
             },
             TyKind::Closure(_, subst) => stack.extend(subst.as_closure().upvar_tys()),
             TyKind::Param(_)
-            | TyKind::Alias(_, _)
+            | TyKind::Alias(_)
             | TyKind::Dynamic(..)
             | TyKind::Ref(_, _, Mutability::Mut) => return false,
             TyKind::Bool
diff --git a/creusot/src/backend/signature.rs b/creusot/src/backend/signature.rs
index 54b6043119..c24fe35b08 100644
--- a/creusot/src/backend/signature.rs
+++ b/creusot/src/backend/signature.rs
@@ -108,7 +108,7 @@ pub(crate) fn lower_logic_sig<'tcx>(
         attrs.push(attr)
     }
 
-    let retty = if names.normalize(pre_sig.output).is_bool() {
+    let retty = if pre_sig.output.is_bool() {
         None
     } else {
         Some(translate_ty(ctx, names, span, pre_sig.output))
diff --git a/creusot/src/backend/term.rs b/creusot/src/backend/term.rs
index c611ac8daa..5336528b67 100644
--- a/creusot/src/backend/term.rs
+++ b/creusot/src/backend/term.rs
@@ -371,10 +371,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             TermKind::Closure { bound, body } => {
                 let binders = bound
                     .iter()
-                    .map(|&(ident, ty)| {
-                        let ty = self.names.normalize(ty);
-                        Binder::typed(ident.0, self.lower_ty(ty))
-                    })
+                    .map(|&(ident, ty)| Binder::typed(ident.0, self.lower_ty(ty)))
                     .collect();
                 let body = self.lower_term(body);
                 Exp::Lam(binders, body.boxed())
@@ -447,15 +444,14 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
     fn lower_pat(&self, pat: &Pattern<'tcx>) -> WPattern {
         match &pat.kind {
             PatternKind::Constructor(variant, fields) => {
-                let ty = self.names.normalize(pat.ty);
-                let (var_did, subst) = match *ty.kind() {
+                let (var_did, subst) = match *pat.ty.kind() {
                     TyKind::Adt(def, subst) => (def.variant(*variant).def_id, subst),
                     TyKind::Closure(did, subst) => (did, subst),
                     _ => unreachable!(),
                 };
                 let flds = fields.iter().map(|(fld, pat)| (*fld, self.lower_pat(pat)));
                 if self.ctx.def_kind(var_did) == DefKind::Variant {
-                    let mut pats: Box<[_]> = ty.ty_adt_def().unwrap().variants()[*variant]
+                    let mut pats: Box<[_]> = pat.ty.ty_adt_def().unwrap().variants()[*variant]
                         .fields
                         .indices()
                         .map(|_| WPattern::Wildcard)
@@ -484,8 +480,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             PatternKind::Tuple(pats) if pats.is_empty() => WPattern::TupleP(Box::new([])),
             PatternKind::Tuple(pats) if pats.len() == 1 => self.lower_pat(&pats[0]),
             PatternKind::Tuple(pats) => {
-                let ty = self.names.normalize(pat.ty);
-                let TyKind::Tuple(tys) = ty.kind() else { unreachable!() };
+                let TyKind::Tuple(tys) = pat.ty.kind() else { unreachable!() };
                 let flds: Box<[_]> = pats
                     .iter()
                     .enumerate()
@@ -496,18 +491,15 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                     .collect();
                 if flds.is_empty() { WPattern::Wildcard } else { WPattern::RecP(flds) }
             }
-            PatternKind::Deref(pointee) => {
-                let ty = self.names.normalize(pat.ty);
-                match ty.kind() {
-                    TyKind::Adt(def, _) if def.is_box() => self.lower_pat(pointee),
-                    TyKind::Ref(_, _, Mutability::Not) => self.lower_pat(pointee),
-                    TyKind::Ref(_, _, Mutability::Mut) => WPattern::RecP(Box::new([(
-                        Name::Global(name::current()),
-                        self.lower_pat(pointee),
-                    )])),
-                    _ => unreachable!(),
-                }
-            }
+            PatternKind::Deref(pointee) => match pat.ty.kind() {
+                TyKind::Adt(def, _) if def.is_box() => self.lower_pat(pointee),
+                TyKind::Ref(_, _, Mutability::Not) => self.lower_pat(pointee),
+                TyKind::Ref(_, _, Mutability::Mut) => WPattern::RecP(Box::new([(
+                    Name::Global(name::current()),
+                    self.lower_pat(pointee),
+                )])),
+                _ => unreachable!(),
+            },
             PatternKind::Or(patterns) => {
                 WPattern::OrP(patterns.iter().map(|p| self.lower_pat(p)).collect())
             }
diff --git a/creusot/src/backend/ty.rs b/creusot/src/backend/ty.rs
index 54c189cafb..ba525a3808 100644
--- a/creusot/src/backend/ty.rs
+++ b/creusot/src/backend/ty.rs
@@ -82,7 +82,6 @@ pub(crate) fn translate_ty<'tcx>(
     span: Span,
     ty: Ty<'tcx>,
 ) -> MlT {
-    let ty = names.normalize(ty);
     match ty.kind() {
         Bool => bool(),
         Char => MlT::qconstructor(names.in_pre(PreMod::Char, "t")),
@@ -133,11 +132,10 @@ pub(crate) fn translate_ty<'tcx>(
         FnPtr(..) => MlT::qconstructor(names.in_pre(PreMod::Opaque, "ptr")),
         Foreign(_) => MlT::qconstructor(names.in_pre(PreMod::Opaque, "foreign")),
         Error(_) => MlT::unit(),
-        Closure(..)
-        | Tuple(_)
-        | Param(_)
-        | Dynamic(_, _)
-        | Alias(AliasTyKind::Opaque | AliasTyKind::Projection, _) => {
+        Closure(..) | Tuple(_) | Param(_) | Dynamic(_, _) => MlT::TConstructor(names.ty(ty)),
+        Alias(t)
+            if matches!(t.kind, AliasTyKind::Opaque { .. } | AliasTyKind::Projection { .. }) =>
+        {
             MlT::TConstructor(names.ty(ty))
         }
         _ => ctx.crash_and_error(span, format!("unsupported type {:?}", ty)),
@@ -249,10 +247,7 @@ pub(crate) fn translate_adtdecl<'tcx>(
                             .fields
                             .iter()
                             .map(|f| {
-                                let ty = ctx.normalize_erasing_regions(
-                                    names.typing_env(),
-                                    f.ty(ctx.tcx, subst),
-                                );
+                                let ty = names.normalize(f.ty(ctx.tcx, subst));
                                 translate_ty(ctx, names, ctx.def_span(f.did), ty)
                             })
                             .collect(),
@@ -272,8 +267,7 @@ pub(crate) fn translate_adtdecl<'tcx>(
                 .iter_enumerated()
                 .filter(|f| f.1.vis.is_accessible_from(names.source_id(), ctx.tcx))
                 .map(|(ix, f)| {
-                    let ty =
-                        ctx.normalize_erasing_regions(names.typing_env(), f.ty(ctx.tcx, subst));
+                    let ty = names.normalize(f.ty(ctx.tcx, subst));
                     FieldDecl {
                         name: names.field(def.did(), subst, ix),
                         ty: translate_ty(ctx, names, ctx.def_span(f.did), ty),
diff --git a/creusot/src/backend/ty_inv.rs b/creusot/src/backend/ty_inv.rs
index 7cd97ef0e4..c4c2e03a6f 100644
--- a/creusot/src/backend/ty_inv.rs
+++ b/creusot/src/backend/ty_inv.rs
@@ -12,7 +12,7 @@ use crate::{
 };
 use rustc_abi::{FieldIdx, VariantIdx};
 use rustc_hir::{def::DefKind, def_id::DefId};
-use rustc_middle::ty::{GenericArg, Ty, TyKind, TypingEnv};
+use rustc_middle::ty::{GenericArg, Ty, TyKind, TypingEnv, Unnormalized};
 use rustc_span::{DUMMY_SP, Span};
 use std::collections::HashSet;
 
@@ -68,14 +68,18 @@ pub(crate) fn is_tyinv_trivial<'tcx>(
                 AdtKind::Struct { partially_opaque: true }
                 | AdtKind::Opaque { always: false }
                 | AdtKind::Empty => return false,
-                AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => stack.extend(
-                    def.all_fields()
-                        .map(|f| ctx.normalize_erasing_regions(typing_env, f.ty(ctx.tcx, subst))),
-                ),
+                AdtKind::Enum | AdtKind::Struct { partially_opaque: false } => {
+                    stack.extend(def.all_fields().map(|f| {
+                        ctx.normalize_erasing_regions(
+                            typing_env,
+                            Unnormalized::new(f.ty(ctx.tcx, subst)),
+                        )
+                    }))
+                }
                 AdtKind::Ghost(_) | AdtKind::Box(_) => unreachable!(),
             },
             TyKind::Closure(_, subst) => stack.extend(subst.as_closure().upvar_tys()),
-            TyKind::Param(_) | TyKind::Alias(_, _) | TyKind::Never => return false,
+            TyKind::Param(_) | TyKind::Alias(_) | TyKind::Never => return false,
             TyKind::Bool
             | TyKind::Char
             | TyKind::Int(_)
@@ -266,7 +270,7 @@ pub(crate) fn inv_call<'tcx>(
     scope_id: DefId,
     term: Term<'tcx>,
 ) -> Option<Term<'tcx>> {
-    let ty = ctx.normalize_erasing_regions(typing_env, term.ty);
+    let ty = ctx.normalize_erasing_regions(typing_env, Unnormalized::new(term.ty));
     if is_tyinv_trivial(&ctx, scope_id, typing_env, ty, term.span) {
         return None;
     }
diff --git a/creusot/src/contracts_items/attributes.rs b/creusot/src/contracts_items/attributes.rs
index 849a03ae24..8ad1d49e55 100644
--- a/creusot/src/contracts_items/attributes.rs
+++ b/creusot/src/contracts_items/attributes.rs
@@ -96,8 +96,8 @@ pub(crate) fn get_builtin(tcx: TyCtxt, def_id: DefId) -> Option<Symbol> {
         tcx.def_kind(def_id),
         DefKind::Fn
             | DefKind::AssocFn
-            | DefKind::AssocConst
-            | DefKind::Const
+            | DefKind::AssocConst { .. }
+            | DefKind::Const { .. }
             | DefKind::Struct
             | DefKind::Enum
             | DefKind::Union
diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs
index 7ac81e1e2b..cf53c4edce 100644
--- a/creusot/src/ctx.rs
+++ b/creusot/src/ctx.rs
@@ -204,7 +204,7 @@ pub(crate) fn gather_params_open_inv(tcx: TyCtxt) -> HashMap<DefId, DenseBitSet<
     struct VisitFns<'tcx, 'a>(
         TyCtxt<'tcx>,
         HashMap<DefId, DenseBitSet<usize>>,
-        &'a ResolverAstLowering,
+        &'a ResolverAstLowering<'tcx>,
     );
     impl<'a> Visitor<'a> for VisitFns<'_, 'a> {
         fn visit_fn(&mut self, fk: FnKind<'a>, _: &AttrVec, _: Span, node: NodeId) {
@@ -476,14 +476,22 @@ impl<'tcx> TranslationCtx<'tcx> {
     }
 
     pub(crate) fn typing_env(&self, def_id: DefId) -> TypingEnv<'tcx> {
-        // FIXME: is it correct to pretend we are doing a non-body analysis?
         let param_env = self.param_env(def_id);
+        self.typing_env_with(def_id, param_env)
+    }
+
+    pub(crate) fn typing_env_with(
+        &self,
+        def_id: DefId,
+        param_env: ParamEnv<'tcx>,
+    ) -> TypingEnv<'tcx> {
+        // FIXME: is it correct to pretend we are doing a non-body analysis?
         let mode = if self.is_mir_available(def_id) && def_id.is_local() {
             TypingMode::post_borrowck_analysis(self.tcx, def_id.as_local().unwrap())
         } else {
             TypingMode::non_body_analysis()
         };
-        TypingEnv { typing_mode: mode, param_env }
+        TypingEnv::new(param_env, mode)
     }
 
     pub(crate) fn has_body(&self, def_id: DefId) -> bool {
@@ -605,9 +613,10 @@ impl<'tcx> TranslationCtx<'tcx> {
                     ItemType::Program
                 }
             }
-            DefKind::AssocConst | DefKind::Const | DefKind::InlineConst | DefKind::ConstParam => {
-                ItemType::Constant
-            }
+            DefKind::AssocConst { .. }
+            | DefKind::Const { .. }
+            | DefKind::InlineConst
+            | DefKind::ConstParam => ItemType::Constant,
             DefKind::Closure => ItemType::Closure,
             DefKind::Struct | DefKind::Enum | DefKind::Union => ItemType::Type,
             DefKind::AssocTy => ItemType::AssocTy,
@@ -643,9 +652,10 @@ impl<'tcx> TranslationCtx<'tcx> {
     }
 
     /// If `true`, the type is definitely non-zero sized. This is a best-effort underapproximation.
-    pub fn is_nonzero_sized(&self, ty: Ty<'tcx>) -> bool {
+    pub fn is_nonzero_sized(&self, typing_env: TypingEnv<'tcx>, ty: Ty<'tcx>) -> bool {
         is_nonzero_sized(
             self.tcx,
+            typing_env,
             &mut self.nonzero_sized_ty.borrow_mut(),
             &mut self.inhabited_ty.borrow_mut(),
             ty,
@@ -675,6 +685,7 @@ pub struct Erasure<'tcx> {
 /// If `true`, the type is definitely non-zero sized. This is a best-effort underapproximation.
 fn is_nonzero_sized<'tcx>(
     tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
     nonzero_sized_cache: &mut HashMap<Ty<'tcx>, bool>,
     inhabited_cache: &mut HashMap<Ty<'tcx>, bool>,
     ty: Ty<'tcx>,
@@ -687,15 +698,23 @@ fn is_nonzero_sized<'tcx>(
         Bool | Char | Int(_) | Uint(_) | Float(_) | Ref(_, _, _) | RawPtr(_, _) => true,
         Adt(def, args) => {
             def.is_box()
-                || is_nonzero_sized_adt(tcx, nonzero_sized_cache, inhabited_cache, def, args)
+                || is_nonzero_sized_adt(
+                    tcx,
+                    typing_env,
+                    nonzero_sized_cache,
+                    inhabited_cache,
+                    def,
+                    args,
+                )
         }
         Tuple(tys) => {
-            tys.iter().any(|ty| is_nonzero_sized(tcx, nonzero_sized_cache, inhabited_cache, ty))
-                && tys.iter().all(|ty| is_inhabited(tcx, inhabited_cache, ty))
+            tys.iter().any(|ty| {
+                is_nonzero_sized(tcx, typing_env, nonzero_sized_cache, inhabited_cache, ty)
+            }) && tys.iter().all(|ty| is_inhabited(tcx, typing_env, inhabited_cache, ty))
         }
         Array(ty, len) => {
             is_nonzero_const(tcx, *len)
-                && is_nonzero_sized(tcx, nonzero_sized_cache, inhabited_cache, *ty)
+                && is_nonzero_sized(tcx, typing_env, nonzero_sized_cache, inhabited_cache, *ty)
         }
         _ => false,
     };
@@ -722,6 +741,7 @@ fn is_nonzero_const<'tcx>(tcx: TyCtxt<'tcx>, len: ty::Const<'tcx>) -> bool {
 /// - there is one inhabited constructor with at least one non-zero sized field.
 fn is_nonzero_sized_adt<'tcx>(
     tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
     nonzero_sized_cache: &mut HashMap<Ty<'tcx>, bool>,
     inhabited_cache: &mut HashMap<Ty<'tcx>, bool>,
     def: &ty::AdtDef<'tcx>,
@@ -736,8 +756,12 @@ fn is_nonzero_sized_adt<'tcx>(
                 variant.fields.iter().all(|field| {
                     is_inhabited(
                         tcx,
+                        typing_env,
                         inhabited_cache,
-                        tcx.type_of(field.did).instantiate(tcx, args),
+                        tcx.normalize_erasing_regions(
+                            typing_env,
+                            tcx.type_of(field.did).instantiate(tcx, args),
+                        ),
                     )
                 })
             })
@@ -747,16 +771,26 @@ fn is_nonzero_sized_adt<'tcx>(
                 variant.fields.iter().any(|field| {
                     is_nonzero_sized(
                         tcx,
+                        typing_env,
                         nonzero_sized_cache,
                         inhabited_cache,
-                        tcx.type_of(field.did).instantiate(tcx, args),
+                        tcx.normalize_erasing_regions(
+                            typing_env,
+                            tcx.type_of(field.did).instantiate(tcx, args),
+                        ),
                     )
                 })
             })
     } else if def.is_union() {
-        def.all_field_tys(tcx)
-            .iter_instantiated(tcx, args)
-            .any(|ty| is_nonzero_sized(tcx, nonzero_sized_cache, inhabited_cache, ty))
+        def.all_field_tys(tcx).iter_instantiated(tcx, args).any(|ty| {
+            is_nonzero_sized(
+                tcx,
+                typing_env,
+                nonzero_sized_cache,
+                inhabited_cache,
+                tcx.normalize_erasing_regions(typing_env, ty),
+            )
+        })
     } else {
         false
     }
@@ -765,13 +799,14 @@ fn is_nonzero_sized_adt<'tcx>(
 /// If `true`, the type is definitely inhabited. This is a best-effort underapproximation.
 fn is_inhabited<'tcx>(
     tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
     inhabited_cache: &mut HashMap<Ty<'tcx>, bool>,
     ty: Ty<'tcx>,
 ) -> bool {
     if let Some(&b) = inhabited_cache.get(&ty) {
         return b;
     }
-    let b = is_inhabited_(tcx, inhabited_cache, &mut Vec::new(), ty);
+    let b = is_inhabited_(tcx, typing_env, inhabited_cache, &mut Vec::new(), ty);
     inhabited_cache.insert(ty, b);
     b
 }
@@ -779,6 +814,7 @@ fn is_inhabited<'tcx>(
 // See `is_inhabited_adt` for the handling of recursive types with `visited`.
 fn is_inhabited_<'tcx>(
     tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
     inhabited_cache: &HashMap<Ty<'tcx>, bool>,
     visited: &mut Vec<ty::AdtDef<'tcx>>,
     ty: Ty<'tcx>,
@@ -786,14 +822,16 @@ fn is_inhabited_<'tcx>(
     use rustc_type_ir::TyKind::*;
     match ty.kind() {
         Bool | Char | Int(_) | Uint(_) | Float(_) | RawPtr(_, _) | Str | Slice(_) => true,
-        Ref(_, ty, _) => is_inhabited_(tcx, inhabited_cache, visited, *ty),
+        Ref(_, ty, _) => is_inhabited_(tcx, typing_env, inhabited_cache, visited, *ty),
         Adt(def, args) if def.is_box() => {
-            is_inhabited_(tcx, inhabited_cache, visited, args.type_at(0))
+            is_inhabited_(tcx, typing_env, inhabited_cache, visited, args.type_at(0))
+        }
+        Adt(def, args) => is_inhabited_adt(tcx, typing_env, inhabited_cache, visited, *def, args),
+        Tuple(tys) => {
+            tys.iter().all(|ty| is_inhabited_(tcx, typing_env, inhabited_cache, visited, ty))
         }
-        Adt(def, args) => is_inhabited_adt(tcx, inhabited_cache, visited, *def, args),
-        Tuple(tys) => tys.iter().all(|ty| is_inhabited_(tcx, inhabited_cache, visited, ty)),
         // [T; 0] is also inhabited but who needs to know that? Make a PR if you do!
-        Array(ty, _) => is_inhabited_(tcx, inhabited_cache, visited, *ty),
+        Array(ty, _) => is_inhabited_(tcx, typing_env, inhabited_cache, visited, *ty),
         _ => false,
     }
 }
@@ -802,6 +840,7 @@ fn is_inhabited_<'tcx>(
 // Since we may return `false` for types which end up being inhabited, we do not modify the cache during this process.
 fn is_inhabited_adt<'tcx>(
     tcx: TyCtxt<'tcx>,
+    typing_env: TypingEnv<'tcx>,
     inhabited_cache: &HashMap<Ty<'tcx>, bool>,
     visited: &mut Vec<ty::AdtDef<'tcx>>,
     def: ty::AdtDef<'tcx>,
@@ -816,17 +855,27 @@ fn is_inhabited_adt<'tcx>(
             variant.fields.iter().all(|field| {
                 is_inhabited_(
                     tcx,
+                    typing_env,
                     inhabited_cache,
                     visited,
-                    tcx.type_of(field.did).instantiate(tcx, args),
+                    tcx.normalize_erasing_regions(
+                        typing_env,
+                        tcx.type_of(field.did).instantiate(tcx, args),
+                    ),
                 )
             })
         })
     } else if def.is_union() {
         use rustc_type_ir::inherent::AdtDef as _;
-        def.all_field_tys(tcx)
-            .iter_instantiated(tcx, args)
-            .any(|ty| is_inhabited_(tcx, inhabited_cache, visited, ty))
+        def.all_field_tys(tcx).iter_instantiated(tcx, args).any(|ty| {
+            is_inhabited_(
+                tcx,
+                typing_env,
+                inhabited_cache,
+                visited,
+                tcx.normalize_erasing_regions(typing_env, ty),
+            )
+        })
     } else {
         false
     };
diff --git a/creusot/src/lib.rs b/creusot/src/lib.rs
index 84d2657bbb..6ccf60abbc 100644
--- a/creusot/src/lib.rs
+++ b/creusot/src/lib.rs
@@ -1,7 +1,6 @@
-#![feature(rustc_private, register_tool)]
+#![feature(rustc_private)]
 #![feature(box_patterns)]
 #![feature(never_type, try_blocks)]
-#![feature(closure_lifetime_binder)]
 #![feature(alloc_slice_into_array)]
 #![feature(iter_intersperse, map_try_insert)]
 
diff --git a/creusot/src/naming.rs b/creusot/src/naming.rs
index 78a153e863..ad95a21732 100644
--- a/creusot/src/naming.rs
+++ b/creusot/src/naming.rs
@@ -1,6 +1,6 @@
 use rustc_ast::Mutability;
 use rustc_hir::def_id::{DefId, LocalDefId};
-use rustc_middle::ty::{self, Ty, TyCtxt};
+use rustc_middle::ty::{self, AliasTy, AliasTyKind, Ty, TyCtxt};
 use rustc_span::Symbol;
 use std::{collections::HashMap, path::PathBuf};
 
@@ -263,7 +263,14 @@ fn type_string_walk(tcx: TyCtxt, prefix: &mut String, ty: Ty) {
                 type_string_walk(tcx, prefix, ty)
             }
         }
-        Alias(_, t) => match tcx.def_key(t.def_id).get_opt_name() {
+        &Alias(AliasTy {
+            kind:
+                AliasTyKind::Projection { def_id }
+                | AliasTyKind::Inherent { def_id }
+                | AliasTyKind::Free { def_id }
+                | AliasTyKind::Opaque { def_id },
+            ..
+        }) => match tcx.def_key(def_id).get_opt_name() {
             None => push_(prefix, "opaque"),
             Some(name) => push_(prefix, &to_alphanumeric(name.as_str())),
         },
diff --git a/creusot/src/translation.rs b/creusot/src/translation.rs
index 06f1987f30..8c1e84e10e 100644
--- a/creusot/src/translation.rs
+++ b/creusot/src/translation.rs
@@ -54,6 +54,7 @@ pub(crate) fn after_analysis<'tcx>(
     params_open_inv: HashMap<DefId, DenseBitSet<usize>>,
 ) -> Result<(), Box<dyn std::error::Error>> {
     let start = Instant::now();
+    silence_unused_features_warnings(tcx);
     let mut ctx = TranslationCtx::new(tcx, opts.clone(), params_open_inv);
     ctx.load_extern_specs();
     ctx.load_erasures();
@@ -107,6 +108,12 @@ pub(crate) fn after_analysis<'tcx>(
     Ok(())
 }
 
+fn silence_unused_features_warnings(tcx: TyCtxt) {
+    let feature = tcx.features();
+    feature.stmt_expr_attributes();
+    feature.proc_macro_hygiene();
+}
+
 pub enum OutputHandle {
     Directory(PathBuf, Vec<Symbol>), // One file per Coma module, second component is a prefix for all files
     File(Box<dyn Write>),            // Monolithic output
diff --git a/creusot/src/translation/constant.rs b/creusot/src/translation/constant.rs
index 1cc05534a3..33d8e321bb 100644
--- a/creusot/src/translation/constant.rs
+++ b/creusot/src/translation/constant.rs
@@ -20,15 +20,17 @@ pub(crate) fn mirconst_to_operand<'tcx>(
     caller_id: DefId,
 ) -> Operand<'tcx> {
     use mir::Const::*;
-    match c.const_ {
+    match ctx.erase_and_anonymize_regions(c.const_) {
         Ty(ty, tyconst) => Operand::term(Term::const_(tyconst, ty, c.span)),
-        Unevaluated(u, ty) if let Some(promoted) = u.promoted => {
-            Operand::promoted(caller_id, promoted, ty)
-        }
-        Unevaluated(u, ty) if matches!(ctx.def_kind(u.def), DefKind::InlineConst) => {
-            Operand::inline_const(u.def, u.args, ty)
+        Unevaluated(u, ty) => {
+            if let Some(promoted) = u.promoted {
+                Operand::promoted(caller_id, promoted, ty)
+            } else if matches!(ctx.def_kind(u.def), DefKind::InlineConst) {
+                Operand::inline_const(u.def, u.args, ty)
+            } else {
+                Operand::term(Term::item(u.def, u.args, ty).span(c.span))
+            }
         }
-        Unevaluated(u, ty) => Operand::term(Term::item(u.def, u.args, ty).span(c.span)),
         Val(const_value, ty) => Operand::term(value_to_term(const_value, ty, ctx, env, c.span)),
     }
 }
@@ -197,7 +199,7 @@ fn try_const_synonym<'tcx>(
     ctx: &TranslationCtx<'tcx>,
     typing_env: TypingEnv<'tcx>,
 ) -> Option<Term<'tcx>> {
-    if !matches!(ctx.def_kind(def_id), rustc_hir::def::DefKind::AssocConst) {
+    if !matches!(ctx.def_kind(def_id), rustc_hir::def::DefKind::AssocConst { .. }) {
         return None;
     }
     let ty::Instance { def, args } =
@@ -210,9 +212,15 @@ fn try_const_synonym<'tcx>(
             Some(Term::const_(c, ty, span))
         }
         ConstKind::Unevaluated(u)
-            if matches!(ctx.def_kind(u.def), DefKind::Const | DefKind::AssocConst) =>
+            if matches!(
+                ctx.def_kind(u.def),
+                DefKind::Const { .. } | DefKind::AssocConst { .. }
+            ) =>
         {
-            let (u, ty) = ty::EarlyBinder::bind((u, ty)).instantiate(ctx.tcx, args);
+            let (u, ty) = ctx.tcx.normalize_erasing_regions(
+                typing_env,
+                ty::EarlyBinder::bind((u, ty)).instantiate(ctx.tcx, args),
+            );
             Some(Term::item(u.def, u.args, ty).span(span))
         }
         _ => None,
diff --git a/creusot/src/translation/external.rs b/creusot/src/translation/external.rs
index b85fd6efed..54e8b1b08e 100644
--- a/creusot/src/translation/external.rs
+++ b/creusot/src/translation/external.rs
@@ -17,10 +17,7 @@ use rustc_hir::{
 use rustc_macros::{TyDecodable, TyEncodable};
 use rustc_middle::{
     thir::{self, Expr, ExprKind, Thir, visit::Visitor},
-    ty::{
-        Clause, EarlyBinder, GenericArgKind, GenericArgsRef, Predicate, Ty, TyCtxt, TyKind,
-        TypingEnv,
-    },
+    ty::{EarlyBinder, GenericArgKind, GenericArgsRef, Predicate, Ty, TyCtxt, TyKind, TypingEnv},
 };
 use rustc_span::Span;
 use rustc_type_ir::ConstKind;
@@ -42,7 +39,10 @@ impl<'tcx> ExternSpec<'tcx> {
         tcx: TyCtxt<'tcx>,
         sub: GenericArgsRef<'tcx>,
     ) -> Vec<Predicate<'tcx>> {
-        EarlyBinder::bind(self.additional_predicates.clone()).instantiate(tcx, sub)
+        // skip normalization: the instantiation should just be a renaming
+        EarlyBinder::bind(self.additional_predicates.clone())
+            .instantiate(tcx, sub)
+            .skip_normalization()
     }
 }
 
@@ -148,7 +148,8 @@ pub(crate) fn extract_extern_specs_from_item<'tcx>(
         .instantiate(ctx.tcx, subst)
         .predicates
         .into_iter()
-        .map(Clause::as_predicate)
+        // skip normalization: the instantiation was only renaming
+        .map(|clause| clause.skip_normalization().as_predicate())
         .collect();
 
     let (inputs, output) = inputs_and_output_from_thir(ctx, def_id, thir);
diff --git a/creusot/src/translation/fmir.rs b/creusot/src/translation/fmir.rs
index 48ad4be77b..c790110efd 100644
--- a/creusot/src/translation/fmir.rs
+++ b/creusot/src/translation/fmir.rs
@@ -45,7 +45,7 @@ impl<'tcx> Place<'tcx> {
             ty = projection_ty(ty, tcx, p);
         }
 
-        ty.ty
+        tcx.erase_and_anonymize_regions(ty.ty)
     }
 
     pub(crate) fn as_symbol(&self) -> Option<Ident> {
@@ -291,6 +291,7 @@ pub enum LocalKind {
 pub struct LocalDecl<'tcx> {
     // Original MIR local
     pub(crate) span: Span,
+    /// This type must be normalized and erased
     pub(crate) ty: Ty<'tcx>,
     #[type_visitable(ignore)]
     #[type_foldable(identity)]
diff --git a/creusot/src/translation/function.rs b/creusot/src/translation/function.rs
index 1eb2236843..e4837ec6f1 100644
--- a/creusot/src/translation/function.rs
+++ b/creusot/src/translation/function.rs
@@ -20,7 +20,7 @@ use rustc_hir::def_id::DefId;
 use rustc_index::bit_set::MixedBitSet;
 use rustc_middle::{
     mir::{self, BasicBlock, Body, Local, Location, Operand, Place, traversal::reverse_postorder},
-    ty::{Ty, TyCtxt, TyKind, TypingEnv},
+    ty::{Ty, TyCtxt, TyKind, TypingEnv, Unnormalized},
 };
 use rustc_span::{DUMMY_SP, Span};
 use std::{assert_matches, collections::HashMap, ops::FnOnce};
@@ -266,7 +266,7 @@ impl<'body, 'tcx> BodyTranslator<'body, 'tcx> {
 
     /// These types cannot contain mutable borrows and thus do not need to be resolved.
     fn skip_resolve_type(&self, ty: Ty<'tcx>) -> bool {
-        let ty = self.ctx.normalize_erasing_regions(self.typing_env(), ty);
+        let ty = self.ctx.normalize_erasing_regions(self.typing_env(), Unnormalized::new(ty));
         self.tcx().type_is_copy_modulo_regions(self.typing_env(), ty)
         // The following is unsound because it does not take into account aliases.
         // It can be made technically sound, but anyway seems much less predictable than "we resolve
diff --git a/creusot/src/translation/function/terminator.rs b/creusot/src/translation/function/terminator.rs
index 3b0916378b..2925987a45 100644
--- a/creusot/src/translation/function/terminator.rs
+++ b/creusot/src/translation/function/terminator.rs
@@ -100,8 +100,8 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                         let known = !matches!(tr_res, TraitResolved::UnknownFound);
                         let (fun_def_id, subst) =
                             tr_res.to_opt(fun_def_id, subst).expect("could not find instance");
-
-                        if self.ctx.sig(fun_def_id).contract.extern_no_spec
+                        let sig = self.ctx.sig(fun_def_id);
+                        if sig.contract.extern_no_spec
                             && let Some(lint_root) =
                                 self.body.source_info(loc).scope.lint_root(&self.body.source_scopes)
                         {
@@ -113,8 +113,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                                 Diagnostics::ContractlessExternalFunction { name, span },
                             );
                         }
-
-                        if self.ctx.sig(fun_def_id).contract.is_requires_false()
+                        if sig.contract.is_requires_false()
                             && !matches!(
                                 self.ctx.intrinsic(fun_def_id),
                                 Intrinsic::GhostDerefMut | Intrinsic::GhostDeref,
@@ -123,9 +122,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                         {
                             target = None
                         } else {
-                            let subst =
-                                self.ctx.normalize_erasing_regions(self.typing_env(), subst);
-
+                            let subst = self.ctx.erase_and_anonymize_regions(subst);
                             self.emit_statement(Statement {
                                 kind: fmir::StatementKind::Call(
                                     self.translate_place(destination, span),
diff --git a/creusot/src/translation/pearlite.rs b/creusot/src/translation/pearlite.rs
index 2ef7af4f36..8989348801 100644
--- a/creusot/src/translation/pearlite.rs
+++ b/creusot/src/translation/pearlite.rs
@@ -7,7 +7,7 @@ use rustc_middle::{
     mir::{Mutability::*, ProjectionElem},
     ty::{
         Const, GenericArgsRef, ParamConst, Ty, TyCtxt, TyKind, TypeFoldable, TypeVisitable,
-        TypingEnv,
+        TypingEnv, Unnormalized,
     },
 };
 use rustc_serialize::{Decodable, Decoder, Encodable, Encoder};
@@ -508,7 +508,7 @@ impl<'tcx> Term<'tcx> {
         subst: GenericArgsRef<'tcx>,
         args: impl IntoIterator<Item = Term<'tcx>>,
     ) -> Self {
-        let ty = tcx.type_of(def_id).instantiate(tcx, subst);
+        let ty = tcx.type_of(def_id).instantiate(tcx, subst).skip_normalization();
         let result = tcx.instantiate_bound_regions_with_erased(ty.fn_sig(tcx).output());
         let args = args.into_iter().collect();
         Term { ty: result, span: DUMMY_SP, kind: TermKind::Call { id: def_id, subst, args } }
@@ -522,7 +522,7 @@ impl<'tcx> Term<'tcx> {
         args: impl IntoIterator<Item = Term<'tcx>>,
     ) -> Self {
         let mut res = Self::call_no_normalize(tcx, def_id, subst, args);
-        res.ty = tcx.normalize_erasing_regions(typing_env, res.ty);
+        res.ty = tcx.normalize_erasing_regions(typing_env, Unnormalized::new(res.ty));
         res
     }
 
diff --git a/creusot/src/translation/pearlite/from_thir.rs b/creusot/src/translation/pearlite/from_thir.rs
index 4f64271f1b..226edacbdd 100644
--- a/creusot/src/translation/pearlite/from_thir.rs
+++ b/creusot/src/translation/pearlite/from_thir.rs
@@ -17,7 +17,7 @@ use rustc_middle::{
         self, AdtExpr, ArmId, Block, ClosureExpr, ExprId, ExprKind, LocalVarId, Pat, PatKind,
         StmtId, StmtKind, Thir,
     },
-    ty::{CapturedPlace, Ty, TyKind, TypingEnv, adjustment::PointerCoercion},
+    ty::{CapturedPlace, Ty, TyKind, adjustment::PointerCoercion},
 };
 use rustc_span::{ErrorGuaranteed, Symbol, sym};
 use std::{
@@ -108,10 +108,7 @@ fn from_thir_with_triggers<'tcx>(
                 PatternKind::Binder(var, _) => var,
                 _ => Ident::fresh_local(format!("__{}", idx)).into(),
             };
-            (
-                ident,
-                ctx.normalize_erasing_regions(TypingEnv::non_body_analysis(ctx.tcx, did), pat.ty),
-            )
+            (ident, pat.ty)
         })
         .collect();
     let body = patterns.into_iter().zip(bound.iter().cloned()).rev().fold(
diff --git a/creusot/src/translation/pearlite/normalize.rs b/creusot/src/translation/pearlite/normalize.rs
index 8cf74a19d2..17626e375d 100644
--- a/creusot/src/translation/pearlite/normalize.rs
+++ b/creusot/src/translation/pearlite/normalize.rs
@@ -10,7 +10,7 @@ use crate::{
     },
 };
 use rustc_hir::def_id::DefId;
-use rustc_middle::ty::{GenericArgsRef, TypingEnv};
+use rustc_middle::ty::{GenericArgsRef, TypingEnv, Unnormalized};
 use rustc_span::sym;
 
 pub(crate) fn normalize<'tcx>(
@@ -19,7 +19,7 @@ pub(crate) fn normalize<'tcx>(
     mut term: Term<'tcx>,
 ) -> Term<'tcx> {
     NormalizeTerm { typing_env, ctx }.visit_mut_term(&mut term);
-    let term = ctx.normalize_erasing_regions(typing_env, term);
+    let term = ctx.normalize_erasing_regions(typing_env, Unnormalized::new(term));
     term
 }
 
diff --git a/creusot/src/translation/specification.rs b/creusot/src/translation/specification.rs
index 39f59bb266..1dac22fba4 100644
--- a/creusot/src/translation/specification.rs
+++ b/creusot/src/translation/specification.rs
@@ -11,7 +11,7 @@ use rustc_hir::{AttrArgs, HirId, Safety, def::DefKind, def_id::DefId};
 use rustc_macros::{TyDecodable, TyEncodable, TypeFoldable, TypeVisitable};
 use rustc_middle::{
     thir::{BodyTy, Pat, PatKind, Thir},
-    ty::{EarlyBinder, GenericArg, GenericArgsRef, Ty, TyCtxt, TyKind, TypingEnv},
+    ty::{EarlyBinder, GenericArg, GenericArgsRef, Ty, TyCtxt, TyKind, TypingEnv, Unnormalized},
 };
 use rustc_span::{DUMMY_SP, Span};
 use rustc_type_ir::ClosureKind;
@@ -221,7 +221,7 @@ pub(crate) fn inherited_extern_spec<'tcx>(
         if ctx.extern_spec(id).is_none() {
             return None;
         }
-        (id, trait_ref.instantiate(ctx.tcx, subst).args)
+        (id, trait_ref.instantiate(ctx.tcx, subst).skip_normalization().args)
     }
 }
 
@@ -232,7 +232,7 @@ pub(crate) fn contract_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> Pr
         None => "closure",
     };
 
-    let (inputs, output) = inputs_and_output(ctx.tcx, def_id);
+    let (inputs, output) = inputs_and_output(ctx, def_id);
     // TODO: handle the "self" argument better
     let raw_inputs =
         if !inputs.is_empty() && inputs[0].0.0 == name::self_() { &inputs[1..] } else { &inputs };
@@ -241,15 +241,24 @@ pub(crate) fn contract_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> Pr
     let mut contract = contract_clauses_of(ctx, def_id)
         .unwrap()
         .get_pre(ctx, fn_name, bound)
-        .instantiate(ctx.tcx, subst);
+        .instantiate(ctx.tcx, subst)
+        .skip_normalization();
 
     if let Some(spec) = ctx.extern_spec(def_id).cloned() {
         // We do NOT normalize the contract here. See below.
         let bound = spec.inputs.iter().map(|(ident, _, _)| ident.0);
-        let contract = spec.contract.get_pre(ctx, fn_name, bound).instantiate(ctx.tcx, spec.subst);
+        let contract = spec
+            .contract
+            .get_pre(ctx, fn_name, bound)
+            .instantiate(ctx.tcx, spec.subst)
+            .skip_normalization();
         PreSignature {
-            inputs: EarlyBinder::bind(spec.inputs).instantiate(ctx.tcx, spec.subst),
-            output: EarlyBinder::bind(spec.output).instantiate(ctx.tcx, spec.subst),
+            inputs: EarlyBinder::bind(spec.inputs)
+                .instantiate(ctx.tcx, spec.subst)
+                .skip_normalization(),
+            output: EarlyBinder::bind(spec.output)
+                .instantiate(ctx.tcx, spec.subst)
+                .skip_normalization(),
             contract,
         }
     } else if contract.is_empty()
@@ -261,10 +270,14 @@ pub(crate) fn contract_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> Pr
         // env for doing this. This is still valid because this contract is going to be substituted
         // and normalized in the caller context (such extern specs are only evaluated in the context
         // of a specific call).
-        let contract = spec.contract.get_pre(ctx, fn_name, bound).instantiate(ctx.tcx, subst);
+        let contract = spec
+            .contract
+            .get_pre(ctx, fn_name, bound)
+            .instantiate(ctx.tcx, subst)
+            .skip_normalization();
         PreSignature {
-            inputs: EarlyBinder::bind(spec.inputs).instantiate(ctx.tcx, subst),
-            output: EarlyBinder::bind(spec.output).instantiate(ctx.tcx, subst),
+            inputs: EarlyBinder::bind(spec.inputs).instantiate(ctx.tcx, subst).skip_normalization(),
+            output: EarlyBinder::bind(spec.output).instantiate(ctx.tcx, subst).skip_normalization(),
             contract,
         }
     } else {
@@ -293,7 +306,7 @@ pub(crate) struct PreSignature<'tcx> {
 }
 
 impl<'tcx> PreSignature<'tcx> {
-    pub(crate) fn normalize(
+    pub(crate) fn normalize_contract(
         mut self,
         ctx: &TranslationCtx<'tcx>,
         typing_env: TypingEnv<'tcx>,
@@ -301,6 +314,20 @@ impl<'tcx> PreSignature<'tcx> {
         self.contract = self.contract.normalize(ctx, typing_env);
         self
     }
+
+    pub(crate) fn instantiate_and_normalize(
+        self,
+        ctx: &TranslationCtx<'tcx>,
+        subst: GenericArgsRef<'tcx>,
+        typing_env: TypingEnv<'tcx>,
+    ) -> Self {
+        let mut sig = EarlyBinder::bind(self).instantiate(ctx.tcx, subst).skip_normalization();
+        sig.contract = sig.contract.normalize(ctx, typing_env);
+        (sig.inputs, sig.output) = ctx
+            .tcx
+            .normalize_erasing_regions(typing_env, Unnormalized::new((sig.inputs, sig.output)));
+        sig
+    }
 }
 
 pub(crate) fn pre_sig_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> PreSignature<'tcx> {
@@ -321,7 +348,7 @@ pub(crate) fn pre_sig_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> Pre
     let mut presig = contract_of(ctx, def_id);
 
     if ctx.def_kind(def_id) == DefKind::Closure {
-        let fn_ty = ctx.type_of(def_id).instantiate_identity();
+        let fn_ty = ctx.type_of(def_id).instantiate_identity().skip_normalization();
         let TyKind::Closure(_, subst) = fn_ty.kind() else { unreachable!() };
 
         let kind = subst.as_closure().kind();
@@ -397,7 +424,7 @@ pub(crate) fn pre_sig_of<'tcx>(ctx: &TranslationCtx<'tcx>, def_id: DefId) -> Pre
         }
     }
 
-    presig
+    ctx.erase_and_anonymize_regions(presig)
 }
 
 pub fn inputs_and_output_from_thir<'tcx>(
@@ -424,11 +451,7 @@ pub fn inputs_and_output_from_thir<'tcx>(
                     None => (Ident::fresh_local(format!("_{ix}")).into(), DUMMY_SP, param.ty),
                 })
                 .collect();
-            let output = ctx.normalize_erasing_regions(
-                rustc_middle::ty::TypingEnv::non_body_analysis(ctx.tcx, def_id),
-                fn_sig.output(),
-            );
-            (inputs, output)
+            (inputs, fn_sig.output())
         }
         BodyTy::GlobalAsm(_) => {
             ctx.crash_and_error(ctx.def_span(def_id), "Inline assembly is not supported")
@@ -438,14 +461,20 @@ pub fn inputs_and_output_from_thir<'tcx>(
 
 /// Normally this information is easier to extract from THIR (using `inputs_and_output_from_thir` above)
 /// but sometimes there is no THIR available (e.g., trait method sigs). Closures also go through this for some reason.
-pub fn inputs_and_output(tcx: TyCtxt, def_id: DefId) -> (Box<[(PIdent, Span, Ty)]>, Ty) {
-    let ty = tcx.type_of(def_id).instantiate_identity();
+pub fn inputs_and_output<'tcx>(
+    tcx: &TranslationCtx<'tcx>,
+    def_id: DefId,
+) -> (Box<[(PIdent, Span, Ty<'tcx>)]>, Ty<'tcx>) {
+    let ty = tcx.type_of(def_id).instantiate_identity().skip_normalization();
     match ty.kind() {
         TyKind::FnDef(..) => {
-            let gen_sig = tcx
-                .instantiate_bound_regions_with_erased(tcx.fn_sig(def_id).instantiate_identity());
-            let sig =
-                tcx.normalize_erasing_regions(TypingEnv::non_body_analysis(tcx, def_id), gen_sig);
+            // Use this typing_env to avoid normalizing RPITs
+            let typing_env = TypingEnv::non_body_analysis(tcx.tcx, def_id);
+            // `fn_sig` does not return normalized types
+            let sig = tcx.normalize_erasing_late_bound_regions(
+                typing_env,
+                tcx.fn_sig(def_id).instantiate_identity().skip_normalization(),
+            );
             let inputs = tcx
                 .fn_arg_idents(def_id)
                 .iter()
@@ -471,7 +500,6 @@ pub fn inputs_and_output(tcx: TyCtxt, def_id: DefId) -> (Box<[(PIdent, Span, Ty)
             let sig = tcx.instantiate_bound_regions_with_erased(
                 tcx.signature_unclosure(subst.as_closure().sig(), Safety::Safe),
             );
-            let sig = tcx.normalize_erasing_regions(TypingEnv::non_body_analysis(tcx, def_id), sig);
             let env_ty = tcx.closure_env_ty(ty, subst.as_closure().kind(), tcx.lifetimes.re_erased);
             let closure_env = (name::self_().into(), tcx.def_span(def_id), env_ty);
             let names = tcx.fn_arg_idents(def_id).iter().cloned();
@@ -493,6 +521,6 @@ pub fn inputs_and_output(tcx: TyCtxt, def_id: DefId) -> (Box<[(PIdent, Span, Ty)
                 .collect();
             (inputs, sig.output())
         }
-        _ => ([].into(), tcx.type_of(def_id).instantiate_identity()),
+        _ => ([].into(), tcx.type_of(def_id).instantiate_identity().skip_normalization()),
     }
 }
diff --git a/creusot/src/translation/traits.rs b/creusot/src/translation/traits.rs
index 5a0c8987df..7a705b4fd3 100644
--- a/creusot/src/translation/traits.rs
+++ b/creusot/src/translation/traits.rs
@@ -19,7 +19,7 @@ use rustc_infer::{
 use rustc_middle::ty::{
     self, Const, ConstKind, EarlyBinder, GenericArgsRef, ParamConst, ParamEnv, ParamEnvAnd,
     ParamTy, Predicate, TraitRef, Ty, TyCtxt, TyKind, TypeFoldable, TypeFolder, TypingEnv,
-    TypingMode,
+    TypingMode, Unnormalized,
 };
 use rustc_span::{DUMMY_SP, ErrorGuaranteed, Span};
 use rustc_trait_selection::{
@@ -60,13 +60,13 @@ impl<'tcx> TranslationCtx<'tcx> {
 
     pub(crate) fn translate_impl(&self, impl_id: DefId) -> Vec<Refinement<'tcx>> {
         assert!(self.impl_opt_trait_id(impl_id).is_some(), "{impl_id:?} is not a trait impl");
-        let trait_ref = self.impl_trait_ref(impl_id).instantiate_identity();
+        let trait_ref = self.impl_trait_ref(impl_id).instantiate_identity().skip_normalization();
 
         let implementor_map = self.tcx.impl_item_implementor_ids(impl_id);
 
         let mut refinements = Vec::new();
         let mut implementor_map =
-            self.with_stable_hashing_context(|hcx| implementor_map.to_sorted(&hcx, true));
+            self.with_stable_hashing_context(|mut hcx| implementor_map.to_sorted(&mut hcx, true));
         implementor_map.sort_by_cached_key(|(trait_item, impl_item)| {
             get_very_stable_hash(&[**trait_item, **impl_item] as &[_], &self.tcx)
         });
@@ -138,7 +138,8 @@ fn logic_refinement_term<'tcx>(
     // Get the contract of the trait version
     let mut trait_sig = EarlyBinder::bind(ctx.sig(trait_item_id).clone())
         .instantiate(ctx.tcx, refn_subst)
-        .normalize(ctx, typing_env);
+        .skip_normalization()
+        .normalize_contract(ctx, typing_env);
 
     let mut impl_sig = ctx.sig(impl_item_id).clone();
 
@@ -241,7 +242,7 @@ impl<'tcx> TraitResolved<'tcx> {
         } else {
             return TraitResolved::NotATraitItem;
         };
-        let trait_ref = tcx.normalize_erasing_regions(typing_env, trait_ref);
+        let trait_ref = tcx.normalize_erasing_regions(typing_env, Unnormalized::new(trait_ref));
 
         let source = tcx.codegen_select_candidate(typing_env.as_query_input(trait_ref));
         if let Err(err) = source {
@@ -506,7 +507,8 @@ impl<'tcx> GraphTraversal<'tcx> {
         Box::new(candidates.filter(|&child| {
             let infcx = self.infcx.fork();
             let args = infcx.fresh_args_for_item(DUMMY_SP, child);
-            let trait_ref_child = self.tcx.impl_trait_ref(child).instantiate(self.tcx, args);
+            let trait_ref_child =
+                self.tcx.impl_trait_ref(child).instantiate(self.tcx, args).skip_normalization();
             infcx
                 .at(&ObligationCause::dummy(), self.param_env)
                 .eq(DefineOpaqueTypes::Yes, trait_ref_child, self.trait_ref)
diff --git a/creusot/src/util.rs b/creusot/src/util.rs
index 6db5371d82..07b01c6e5b 100644
--- a/creusot/src/util.rs
+++ b/creusot/src/util.rs
@@ -138,8 +138,6 @@ fn hashed_symbol(data: DefPathData) -> Option<Symbol> {
         | AnonConst
         | OpaqueTy
         | SyntheticCoroutineBody
-        | LateAnonConst
-        | DesugaredAnonymousLifetime
         | NestedStatic => None,
     }
 }
diff --git a/creusot/src/validate/erasure.rs b/creusot/src/validate/erasure.rs
index 97a1bf77f6..7053e898fe 100644
--- a/creusot/src/validate/erasure.rs
+++ b/creusot/src/validate/erasure.rs
@@ -91,6 +91,7 @@ fn check_erasure<'tcx>(
         ctx.error(left_span, "#[erasure] function must have a body").emit();
         return Err(None);
     }
+    let typing_env = ctx.typing_env(left);
     let left_thir = ctx.thir_body(left_local);
     let left = a_normal_form_or_error(ctx, left_local, left_thir).ok_or_else(|| {
         debug!("{:#?}", left_thir);
@@ -129,8 +130,11 @@ fn check_erasure<'tcx>(
             Cow::Owned(anf)
         }
     };
-    let right = &ty::EarlyBinder::bind(right_anf.into_owned()).instantiate(ctx.tcx, right.def.1);
-    Ok(equate_anf(ctx, left_local, &left, right, level).map_err(|_| None)?)
+    let right = ctx.tcx.normalize_erasing_regions(
+        typing_env,
+        ty::EarlyBinder::bind(right_anf.into_owned()).instantiate(ctx.tcx, right.def.1),
+    );
+    Ok(equate_anf(ctx, left_local, &left, &right, level).map_err(|_| None)?)
 }
 
 /// Equate two ANF bodies.
@@ -862,12 +866,15 @@ impl<'a, 'tcx> AnfBuilder<'a, 'tcx> {
                             });
                     let mut erasure_info = None;
                     if let Some(ctx) = self.ctx {
-                        subst = erase_types(ctx, subst);
+                        subst = erase_types(ctx, self.typing_env, subst);
                         if let Some(erasure) = ctx.erasure(fun_id) {
                             if let Some(erasure) = erasure {
                                 fun_id = erasure.def.0;
-                                subst = ty::EarlyBinder::bind(erasure.def.1)
-                                    .instantiate(self.tcx, subst);
+                                subst = self.tcx.normalize_erasing_regions(
+                                    self.typing_env,
+                                    ty::EarlyBinder::bind(erasure.def.1)
+                                        .instantiate(self.tcx, subst),
+                                );
                                 erasure_info =
                                     Some(ErasureInfo::EraseArgs(erasure.erase_args.clone()));
                             } else {
@@ -1336,24 +1343,34 @@ fn is_erasable(tcx: TyCtxt, thir: &Thir, expr: ExprId) -> bool {
 
 /// Replace function types with their erasure when it exists
 /// (This is very simplistic and experimental)
-fn erase_types<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(ctx: &TranslationCtx<'tcx>, t: T) -> T {
-    struct Eraser<'a, 'tcx>(&'a TranslationCtx<'tcx>);
+fn erase_types<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(
+    ctx: &TranslationCtx<'tcx>,
+    typing_env: ty::TypingEnv<'tcx>,
+    t: T,
+) -> T {
+    struct Eraser<'a, 'tcx> {
+        ctx: &'a TranslationCtx<'tcx>,
+        typing_env: ty::TypingEnv<'tcx>,
+    }
 
     impl<'tcx> ty::TypeFolder<TyCtxt<'tcx>> for Eraser<'_, 'tcx> {
         fn cx(&self) -> TyCtxt<'tcx> {
-            self.0.tcx()
+            self.ctx.tcx()
         }
 
         fn fold_ty(&mut self, t: ty::Ty<'tcx>) -> ty::Ty<'tcx> {
             match t.kind() {
                 &ty::TyKind::FnDef(fun_id, args)
-                    if let Some(Some(erasure)) = self.0.erasure(fun_id) =>
+                    if let Some(Some(erasure)) = self.ctx.erasure(fun_id) =>
                 {
                     let tcx = self.cx();
                     ty::Ty::new_fn_def(
                         tcx,
                         erasure.def.0,
-                        ty::EarlyBinder::bind(erasure.def.1).instantiate(tcx, args),
+                        self.cx().normalize_erasing_regions(
+                            self.typing_env,
+                            ty::EarlyBinder::bind(erasure.def.1).instantiate(tcx, args),
+                        ),
                     )
                 }
                 _ => t,
@@ -1362,7 +1379,7 @@ fn erase_types<'tcx, T: TypeFoldable<TyCtxt<'tcx>>>(ctx: &TranslationCtx<'tcx>,
         }
     }
 
-    t.fold_with(&mut Eraser(ctx))
+    t.fold_with(&mut Eraser { ctx, typing_env })
 }
 
 ////////////////////////////////////////////////////////////////
diff --git a/creusot/src/validate/opacity.rs b/creusot/src/validate/opacity.rs
index 2cfd4fae20..ef7a8e1e07 100644
--- a/creusot/src/validate/opacity.rs
+++ b/creusot/src/validate/opacity.rs
@@ -2,7 +2,7 @@ use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_middle::{
     mir::{PlaceTy, ProjectionElem},
     thir::{self, Thir, visit::Visitor},
-    ty::{self, TyKind, TypingEnv},
+    ty::{self, TyKind},
 };
 use rustc_span::Span;
 
@@ -20,7 +20,6 @@ struct OpacityVisitor<'a, 'tcx> {
     ctx: &'a TranslationCtx<'tcx>,
     opacity: Opacity,
     item: DefId,
-    typing_env: TypingEnv<'tcx>,
 }
 
 impl OpacityVisitor<'_, '_> {
@@ -60,8 +59,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
                 }
             }
             &TermKind::Constructor { variant, .. } => {
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, term.ty);
-                if let Some(adt) = ty.ty_adt_def() {
+                if let Some(adt) = term.ty.ty_adt_def() {
                     if !self.is_visible_enough(adt.did()) {
                         self.error(adt.did(), term.span);
                     }
@@ -73,8 +71,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
                 }
             }
             &TermKind::Projection { idx, ref lhs } => {
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, lhs.ty);
-                if let Some(adt) = ty.ty_adt_def() {
+                if let Some(adt) = lhs.ty.ty_adt_def() {
                     let fdid = adt.non_enum_variant().fields[idx].did;
                     if !self.is_visible_enough(fdid) {
                         self.error(fdid, term.span);
@@ -82,8 +79,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
                 }
             }
             &TermKind::Reborrow { ref projections, ref inner } => {
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, inner.ty);
-                let ty = ty.builtin_deref(false).unwrap();
+                let ty = inner.ty.builtin_deref(false).unwrap();
                 for (elem, place_ty) in
                     iter_projections_ty(self.ctx, projections, &mut PlaceTy::from_ty(ty))
                 {
@@ -112,8 +108,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
     fn visit_pattern(&mut self, pat: &Pattern<'tcx>) {
         match &pat.kind {
             PatternKind::Constructor(variant_idx, patterns) => {
-                let ty = self.ctx.normalize_erasing_regions(self.typing_env, pat.ty);
-                let fields_def = &ty.ty_adt_def().unwrap().variants()[*variant_idx].fields;
+                let fields_def = &pat.ty.ty_adt_def().unwrap().variants()[*variant_idx].fields;
                 for (fld, _) in patterns {
                     let fdid = fields_def[*fld].did;
                     if !self.is_visible_enough(fdid) {
@@ -186,7 +181,6 @@ impl<'thir, 'tcx> Visitor<'thir, 'tcx> for NoOpaqueTypeAccess<'thir, 'tcx> {
 
 /// Validates that a private function is not made visible in a public one which is open.
 pub(crate) fn validate_opacity<'tcx>(ctx: &TranslationCtx<'tcx>, item: DefId) {
-    let typing_env = ctx.typing_env(item);
     let is_logic = is_logic(ctx.tcx, item);
     // Forbid use of opaque type constructors and fields, except in trusted program functions
     if is_logic || !is_trusted(ctx.tcx, item) {
@@ -196,12 +190,12 @@ pub(crate) fn validate_opacity<'tcx>(ctx: &TranslationCtx<'tcx>, item: DefId) {
     }
     if is_logic && !is_opaque(ctx.tcx, item) {
         let Some(ScopedTerm(_, term)) = ctx.term(item) else { return };
-        OpacityVisitor { opacity: *ctx.opacity(item), ctx, item, typing_env }.visit_term(term);
+        OpacityVisitor { opacity: *ctx.opacity(item), ctx, item }.visit_term(term);
     }
     let contract = &ctx.sig(item).contract;
     // We consider variants as private, because we don't support mutual recursion for now
     for term in contract.requires.iter().chain(contract.ensures.iter()).map(|cond| &cond.term) {
         let opacity = Opacity::Transparent(ctx.visibility(item));
-        OpacityVisitor { opacity, ctx, item, typing_env }.visit_term(term);
+        OpacityVisitor { opacity, ctx, item }.visit_term(term);
     }
 }
diff --git a/creusot/src/validate/terminates.rs b/creusot/src/validate/terminates.rs
index e1aa235ed3..d32c785fa2 100644
--- a/creusot/src/validate/terminates.rs
+++ b/creusot/src/validate/terminates.rs
@@ -60,7 +60,7 @@ use rustc_hir::{
     def_id::{DefId, LocalDefId},
 };
 use rustc_index::bit_set::DenseBitSet;
-use rustc_infer::{infer::TyCtxtInferExt as _, traits::ObligationCause};
+use rustc_infer::infer::TyCtxtInferExt as _;
 use rustc_middle::{
     thir::{self, visit::Visitor},
     ty::{
@@ -68,9 +68,7 @@ use rustc_middle::{
     },
 };
 use rustc_span::Span;
-use rustc_trait_selection::traits::{
-    normalize_param_env_or_error, specialization_graph, translate_args,
-};
+use rustc_trait_selection::traits::{specialization_graph, translate_args};
 use std::{collections::HashMap, iter::repeat};
 
 pub(crate) type RecursiveCalls = IndexMap<DefId, IndexSet<DefId>>;
@@ -326,12 +324,14 @@ impl<'tcx> BuildFunctionsGraph<'tcx> {
                 self.visit_specialized_default_function(ctx, impl_ldid, called_id);
             bounds = EarlyBinder::bind(bnds)
                 .instantiate(ctx.tcx, def.1.rebase_onto(ctx.tcx, ctx.parent(def.0), impl_args))
+                .skip_normalization()
         } else {
             let subst_r;
             (called_id, subst_r) = res.to_opt(called_id, subst).unwrap();
             called_node = self.insert_function(GraphNode::Function(called_id));
             bounds = EarlyBinder::bind(ctx.param_env(called_id).caller_bounds())
                 .instantiate(ctx.tcx, subst_r)
+                .skip_normalization()
         }
         self.graph.update_edge(node, called_node, CallKind::Direct(call_span));
 
@@ -426,17 +426,19 @@ impl<'tcx> BuildFunctionsGraph<'tcx> {
         // Before instantiating the bounds, keep only those that are not inherited from the defining
         // impl. After instantiation, they will be implied by the bounds of the inheriting
         // impl.
+        let typing_env_for_bounds = TypingEnv::new(impl_param_env, TypingMode::non_body_analysis());
         let bounds = impl_param_env.caller_bounds().iter().chain(
-            item_bounds
-                .iter()
-                .filter(|b| !defimpl_bounds.contains(b))
-                .map(|b| EarlyBinder::bind(b).instantiate(ctx.tcx, func_impl_args)),
+            item_bounds.iter().filter(|b| !defimpl_bounds.contains(b)).map(|b| {
+                ctx.tcx.normalize_erasing_regions(
+                    typing_env_for_bounds,
+                    EarlyBinder::bind(b).instantiate(ctx.tcx, func_impl_args),
+                )
+            }),
         );
 
         // data for when we call this function
         let param_env = ParamEnv::new(ctx.mk_clauses_from_iter(bounds));
-        let param_env = normalize_param_env_or_error(ctx.tcx, param_env, ObligationCause::dummy());
-        let typing_env = TypingEnv { param_env, ..ctx.typing_env(item_id) };
+        let typing_env = ctx.typing_env_with(item_id, param_env);
 
         let bounds = param_env.caller_bounds();
         self.default_functions_bounds.insert(node, bounds);
@@ -445,8 +447,9 @@ impl<'tcx> BuildFunctionsGraph<'tcx> {
         visitor.visit_term(&ctx.term(item_id).unwrap().1);
         for (called_id, generic_args, call_span) in visitor.results {
             // Instantiate the args for the call with the context we just built up.
-            let actual_args = EarlyBinder::bind(generic_args).instantiate(ctx.tcx, func_impl_args);
-
+            let actual_args = EarlyBinder::bind(generic_args)
+                .instantiate(ctx.tcx, func_impl_args)
+                .skip_normalization();
             self.function_call(ctx, node, typing_env, called_id, actual_args, call_span);
         }
         (node, bounds)
@@ -473,10 +476,11 @@ impl CallGraph {
                 continue;
             }
 
-            if !is_pearlite(ctx.tcx, def_id) && !ctx.sig(def_id).contract.check_terminates {
+            let contract = &ctx.sig(def_id).contract;
+            if !is_pearlite(ctx.tcx, def_id) && !contract.check_terminates {
                 // Only consider functions marked with `terminates`: we already ensured
                 // that a `terminates` functions only calls other `terminates` functions.
-                if let Some(variant) = &ctx.sig(def_id).contract.variant {
+                if let Some(variant) = &contract.variant {
                     ctx.dcx().struct_span_warn(variant.span, "variant will be ignored")
                         .with_span_note(ctx.def_span(def_id), "This function is not a logical function, and is not marked with `#[terminates]`.")
                         .emit();
diff --git a/creusot/src/validate/traits.rs b/creusot/src/validate/traits.rs
index a5545d3a41..cc13256998 100644
--- a/creusot/src/validate/traits.rs
+++ b/creusot/src/validate/traits.rs
@@ -70,7 +70,7 @@ pub(crate) fn validate_impls<'tcx>(ctx: &TranslationCtx<'tcx>) {
         let implementors = ctx.impl_item_implementor_ids(impl_id.to_def_id());
 
         let implementors =
-            ctx.with_stable_hashing_context(|hcx| implementors.to_sorted(&hcx, true));
+            ctx.with_stable_hashing_context(|mut hcx| implementors.to_sorted(&mut hcx, true));
         for (&trait_item, &impl_item) in implementors {
             if !ctx.def_kind(trait_item).is_fn_like() {
                 continue;
diff --git a/creusot/src/very_stable_hash.rs b/creusot/src/very_stable_hash.rs
index ac37935482..a6a77444a2 100644
--- a/creusot/src/very_stable_hash.rs
+++ b/creusot/src/very_stable_hash.rs
@@ -135,8 +135,6 @@ impl<CTX> VeryStableHash<CTX> for DefPathData {
             | AnonConst
             | OpaqueTy
             | SyntheticCoroutineBody
-            | LateAnonConst
-            | DesugaredAnonymousLifetime
             | NestedStatic => {}
             TypeNs(symbol)
             | ValueNs(symbol)
diff --git a/flake.lock b/flake.lock
index 145185b3de..c306bfb3bb 100644
--- a/flake.lock
+++ b/flake.lock
@@ -63,11 +63,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1773216618,
-        "narHash": "sha256-iZlowevS+xKLGOXtZwpIrz3SWe7PtoGUfEeVZNib+WE=",
+        "lastModified": 1776741231,
+        "narHash": "sha256-k9G98qzn+7npROUaks8VqCFm7cFtEG8ulQLBBo5lItg=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "07d7dc6fcc5eae76b4fb0e19d4afd939437bec97",
+        "rev": "02061303f7c4c964f7b4584dabd9e985b4cd442b",
         "type": "github"
       },
       "original": {
diff --git a/rust-toolchain b/rust-toolchain
index d365052d1f..ec3e8f4b4d 100644
--- a/rust-toolchain
+++ b/rust-toolchain
@@ -1,3 +1,3 @@
 [toolchain]
-channel = "nightly-2026-02-27"
+channel = "nightly-2026-04-21"
 components = [ "rustfmt", "rustc-dev", "llvm-tools" ]
diff --git a/tests/creusot-std/creusot-std.coma b/tests/creusot-std/creusot-std.coma
index 48d299abc8..71dce86eff 100644
--- a/tests/creusot-std/creusot-std.coma
+++ b/tests/creusot-std/creusot-std.coma
@@ -107981,9 +107981,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicBool__get_timestamp_mono
   
   use int.Int
   
-  type t_AtomicBool
+  type t_Atomic_bool
   
-  type t_AtomicBool'0 = { f0: t_AtomicBool }
+  type t_AtomicBool = { f0: t_Atomic_bool }
   
   type t_SyncView
   
@@ -107993,13 +107993,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicBool__get_timestamp_mono
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicBool (self: t_AtomicBool'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicBool (self: t_AtomicBool) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicBool'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicBool, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicBool self x <= get_timestamp_AtomicBool self y
         -> get_timestamp_AtomicBool self x <= get_timestamp_AtomicBool self y)
@@ -108011,9 +108011,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicPtr_T__get_timestamp_mon
   
   use int.Int
   
-  type t_AtomicPtr_T
+  type t_Atomic_ptr_T
   
-  type t_AtomicPtr_T'0 = { f0: t_AtomicPtr_T }
+  type t_AtomicPtr_T = { f0: t_Atomic_ptr_T }
   
   type t_SyncView
   
@@ -108023,13 +108023,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicPtr_T__get_timestamp_mon
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicPtr_T (self: t_AtomicPtr_T'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicPtr_T (self: t_AtomicPtr_T) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicPtr_T'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicPtr_T, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicPtr_T self x <= get_timestamp_AtomicPtr_T self y
         -> get_timestamp_AtomicPtr_T self x <= get_timestamp_AtomicPtr_T self y)
@@ -108041,9 +108041,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI8__get_timestamp_monoto
   
   use int.Int
   
-  type t_AtomicI8
+  type t_Atomic_i8
   
-  type t_AtomicI8'0 = { f0: t_AtomicI8 }
+  type t_AtomicI8 = { f0: t_Atomic_i8 }
   
   type t_SyncView
   
@@ -108053,13 +108053,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI8__get_timestamp_monoto
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicI8 (self: t_AtomicI8'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicI8 (self: t_AtomicI8) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicI8'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicI8, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicI8 self x <= get_timestamp_AtomicI8 self y
         -> get_timestamp_AtomicI8 self x <= get_timestamp_AtomicI8 self y)
@@ -108071,9 +108071,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU8__get_timestamp_monoto
   
   use int.Int
   
-  type t_AtomicU8
+  type t_Atomic_u8
   
-  type t_AtomicU8'0 = { f0: t_AtomicU8 }
+  type t_AtomicU8 = { f0: t_Atomic_u8 }
   
   type t_SyncView
   
@@ -108083,13 +108083,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU8__get_timestamp_monoto
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicU8 (self: t_AtomicU8'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicU8 (self: t_AtomicU8) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicU8'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicU8, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicU8 self x <= get_timestamp_AtomicU8 self y
         -> get_timestamp_AtomicU8 self x <= get_timestamp_AtomicU8 self y)
@@ -108101,9 +108101,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI16__get_timestamp_monot
   
   use int.Int
   
-  type t_AtomicI16
+  type t_Atomic_i16
   
-  type t_AtomicI16'0 = { f0: t_AtomicI16 }
+  type t_AtomicI16 = { f0: t_Atomic_i16 }
   
   type t_SyncView
   
@@ -108113,13 +108113,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI16__get_timestamp_monot
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicI16 (self: t_AtomicI16'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicI16 (self: t_AtomicI16) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicI16'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicI16, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicI16 self x <= get_timestamp_AtomicI16 self y
         -> get_timestamp_AtomicI16 self x <= get_timestamp_AtomicI16 self y)
@@ -108131,9 +108131,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU16__get_timestamp_monot
   
   use int.Int
   
-  type t_AtomicU16
+  type t_Atomic_u16
   
-  type t_AtomicU16'0 = { f0: t_AtomicU16 }
+  type t_AtomicU16 = { f0: t_Atomic_u16 }
   
   type t_SyncView
   
@@ -108143,13 +108143,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU16__get_timestamp_monot
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicU16 (self: t_AtomicU16'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicU16 (self: t_AtomicU16) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicU16'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicU16, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicU16 self x <= get_timestamp_AtomicU16 self y
         -> get_timestamp_AtomicU16 self x <= get_timestamp_AtomicU16 self y)
@@ -108161,9 +108161,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI32__get_timestamp_monot
   
   use int.Int
   
-  type t_AtomicI32
+  type t_Atomic_i32
   
-  type t_AtomicI32'0 = { f0: t_AtomicI32 }
+  type t_AtomicI32 = { f0: t_Atomic_i32 }
   
   type t_SyncView
   
@@ -108173,13 +108173,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI32__get_timestamp_monot
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicI32 (self: t_AtomicI32'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicI32 (self: t_AtomicI32) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicI32'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicI32, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicI32 self x <= get_timestamp_AtomicI32 self y
         -> get_timestamp_AtomicI32 self x <= get_timestamp_AtomicI32 self y)
@@ -108191,9 +108191,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU32__get_timestamp_monot
   
   use int.Int
   
-  type t_AtomicU32
+  type t_Atomic_u32
   
-  type t_AtomicU32'0 = { f0: t_AtomicU32 }
+  type t_AtomicU32 = { f0: t_Atomic_u32 }
   
   type t_SyncView
   
@@ -108203,13 +108203,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU32__get_timestamp_monot
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicU32 (self: t_AtomicU32'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicU32 (self: t_AtomicU32) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicU32'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicU32, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicU32 self x <= get_timestamp_AtomicU32 self y
         -> get_timestamp_AtomicU32 self x <= get_timestamp_AtomicU32 self y)
@@ -108221,9 +108221,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI64__get_timestamp_monot
   
   use int.Int
   
-  type t_AtomicI64
+  type t_Atomic_i64
   
-  type t_AtomicI64'0 = { f0: t_AtomicI64 }
+  type t_AtomicI64 = { f0: t_Atomic_i64 }
   
   type t_SyncView
   
@@ -108233,13 +108233,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicI64__get_timestamp_monot
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicI64 (self: t_AtomicI64'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicI64 (self: t_AtomicI64) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicI64'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicI64, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicI64 self x <= get_timestamp_AtomicI64 self y
         -> get_timestamp_AtomicI64 self x <= get_timestamp_AtomicI64 self y)
@@ -108251,9 +108251,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU64__get_timestamp_monot
   
   use int.Int
   
-  type t_AtomicU64
+  type t_Atomic_u64
   
-  type t_AtomicU64'0 = { f0: t_AtomicU64 }
+  type t_AtomicU64 = { f0: t_Atomic_u64 }
   
   type t_SyncView
   
@@ -108263,13 +108263,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicU64__get_timestamp_monot
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicU64 (self: t_AtomicU64'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicU64 (self: t_AtomicU64) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicU64'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicU64, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicU64 self x <= get_timestamp_AtomicU64 self y
         -> get_timestamp_AtomicU64 self x <= get_timestamp_AtomicU64 self y)
@@ -108281,9 +108281,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicIsize__get_timestamp_mon
   
   use int.Int
   
-  type t_AtomicIsize
+  type t_Atomic_isize
   
-  type t_AtomicIsize'0 = { f0: t_AtomicIsize }
+  type t_AtomicIsize = { f0: t_Atomic_isize }
   
   type t_SyncView
   
@@ -108293,13 +108293,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicIsize__get_timestamp_mon
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicIsize (self: t_AtomicIsize'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicIsize (self: t_AtomicIsize) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicIsize'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicIsize, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicIsize self x <= get_timestamp_AtomicIsize self y
         -> get_timestamp_AtomicIsize self x <= get_timestamp_AtomicIsize self y)
@@ -108311,9 +108311,9 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicUsize__get_timestamp_mon
   
   use int.Int
   
-  type t_AtomicUsize
+  type t_Atomic_usize
   
-  type t_AtomicUsize'0 = { f0: t_AtomicUsize }
+  type t_AtomicUsize = { f0: t_Atomic_usize }
   
   type t_SyncView
   
@@ -108323,13 +108323,13 @@ module M_std__sync__atomic__impl_HasTimestamp_for_AtomicUsize__get_timestamp_mon
   
   predicate le_log_SyncView (self: t_SyncView) (o: t_SyncView) = cmp_log_SyncView self o <> Greater
   
-  function get_timestamp_AtomicUsize (self: t_AtomicUsize'0) (_2: t_SyncView) : int
+  function get_timestamp_AtomicUsize (self: t_AtomicUsize) (_2: t_SyncView) : int
   
   meta "compute_max_steps" 1000000
   
   meta "select_lsinst" "all"
   
-  goal refines: forall self: t_AtomicUsize'0, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
+  goal refines: forall self: t_AtomicUsize, x: t_SyncView, y: t_SyncView. le_log_SyncView x y
       -> le_log_SyncView x y
       /\ (forall result: (). get_timestamp_AtomicUsize self x <= get_timestamp_AtomicUsize self y
         -> get_timestamp_AtomicUsize self x <= get_timestamp_AtomicUsize self y)