Try to mark param env as rigid with the next solver

[adwinwhite]

This PR tries to make normalization of param env behave exactly the same as the old solver.

Notably,

• we treat the param env used to normalize param env itself as rigid.
• the normalizes-to term of projection predicate is treated as normalizable rather than rigid.

This fixes some overflow bugs we met in the next solver but unfix some other bugs (existing in the old solver).
See the blessed tests.

r? lcnr

[adwinwhite]

Haven't blessed tests or added comments.

@bors try @rust-timer queue

[adwinwhite]

@bors try cancel

[rust-bors]

Try build cancelled. Cancelled workflows:

• https://github.com/rust-lang/rust/actions/runs/28497483760

[adwinwhite]

@bors try @rust-timer queue

[rust-bors]

☀️ Try build successful (CI)
Build commit: 0abe2a0 (0abe2a0937c875c08c170438a9afec1fecf7de22)
Base parent: 17aa775 (17aa77551e89d5e80d4b506c9a32fc151264b8e4)

[rust-timer]

Finished benchmarking commit (0abe2a0): comparison URL.

Overall result: ❌✅ regressions and improvements - please read:

Benchmarking means the PR may be perf-sensitive. It's automatically marked not fit for rolling up. Overriding is possible but disadvised: it risks changing compiler perf.

Next, please: If you can, justify the regressions found in this try perf run in writing along with @rustbot label: +perf-regression-triaged. If not, fix the regressions and do another perf run. Neutral or positive results will clear the label automatically.

@bors rollup=never
@rustbot label: -S-waiting-on-perf +perf-regression

Instruction count

Our most reliable metric. Used to determine the overall result above. However, even this metric can be noisy.

	mean	range	count
Regressions ❌ (primary)	-	-	0
Regressions ❌ (secondary)	2.2%	[1.2%, 2.8%]	3
Improvements ✅ (primary)	-	-	0
Improvements ✅ (secondary)	-1.3%	[-2.5%, -0.1%]	8
All ❌✅ (primary)	-	-	0

Max RSS (memory usage)

Results (secondary -0.6%)

A less reliable metric. May be of interest, but not used to determine the overall result above.

	mean	range	count
Regressions ❌ (primary)	-	-	0
Regressions ❌ (secondary)	2.8%	[2.8%, 2.8%]	1
Improvements ✅ (primary)	-	-	0
Improvements ✅ (secondary)	-1.8%	[-1.9%, -1.7%]	3
All ❌✅ (primary)	-	-	0

Cycles

Results (secondary -0.7%)

A less reliable metric. May be of interest, but not used to determine the overall result above.

	mean	range	count
Regressions ❌ (primary)	-	-	0
Regressions ❌ (secondary)	3.7%	[3.7%, 3.7%]	1
Improvements ✅ (primary)	-	-	0
Improvements ✅ (secondary)	-2.1%	[-2.2%, -2.0%]	3
All ❌✅ (primary)	-	-	0

Binary size

This perf run didn't have relevant results for this metric.

Bootstrap: 486.291s -> 497.243s (2.25%)
Artifact size: 393.72 MiB -> 393.24 MiB (-0.12%)

[rustbot]

This PR changes a file inside tests/crashes. If a crash was fixed, please move into the corresponding ui subdir and add 'Fixes #' to the PR description to autoclose the issue upon merge.

[adwinwhite]

Unsure which minimization is a valid regression test for ml-kem. Part of it should be covered by tachys. Just add my minimization which is very long?

[lcnr]

hmm, good question :3 I think the largest typenum free minimization to make unknown issues easier to detect + all small mimimizations for the separate issues?

might make sense to just have a list of all the minimization and how they cover each other. You want both all smallest and all largest minimizations :3 minimizations should form a poset