F* v2026.08.30

What's Changed

• Optimize eliminate exists by @gebner in #4448
• Fix quadratic normalization of nested stuck projections by @gebner in #4471
• Print real time info with --query_stats by @mtzguido in #4470
• overload: classify erased by its argument, not as compatible with everything by @mtzguido in #4459
• Unfold inside the scrutinee of a stuck projection by @gebner in #4473
• Update karamel submodule to 9abbb865 by @dzomo in #4489
• Represent real literals as mantissa + exponent by @gebner in #4490
• Pulse: reduce nested projector redexes in Pulse.Simplify by @hei411 in #4492
• Refactor constants by @gebner in #4493
• Mark false_elim irreducible to prevent extraction from diverging (unbounded allocation) by @tahina-pro in #4494
• Upgrade F# extraction to support latest versions. by @kant2002 in #4475
• fix(pulse): correct subtree selection in AVL delete; add pop_min by @elefthei in #4437
• Fix res_summary.sh memory unit handling (KiB/MiB confusion) by @gebner in #4499
• Tactics: unrefine functions being applied by @gebner in #4502
• Introduce --ext freshen, restart Z3 between top-level decls by @gebner in #4501
• Krml: let extraction plugins inject declarations by @gebner in #4504
• Allow typeclass instances with refined types by @gebner in #4503
• Weaken Tot ascriptions when unfolding a definition by @gebner in #4506
• Pulse: --ext pulse:extra_simplify by @gebner in #4507
• Introduce --ext no_krml_private by @gebner in #4500
• Extraction: do not normalize noextract definitions by @mtzguido in #4509
• Set the expected type as a refinement when the expected postcondition is non-trivial by @nikswamy in #4508
• Introduce FStar.Math.Sqrt: square roots of reals by @mtzguido in #4510
• Use an expected postcondition field and propagate it across ascriptions by @nikswamy in #4511
• Bump version to 2026.08.30 by @dzomo in #4514

Full Changelog: v2026.08.23...v2026.08.30