FStarLang/FStar v2026.11.15

F* v2026.11.15

on GitHub

What's Changed

• FStar.List.Tot.length: extract as a tail-recursive accumulator by @gebner in #4794
• Custard: allow foreign function declarations in generated C headers by @tahina-pro in #4779
• Pulse: expose array-view metadata and empty-mask transport by @tyler-utah in #4786
• Custard: add header-only direct-C extraction with safe CUI reuse by @tahina-pro in #4782
• Pulse: quantify a record witness field by field in inferred postconditions (fixes #4790) by @elefthei in #4793
• Cherry: inline monad bind/return, so continuations are no closures by @gebner in #4787
• Cherry: stable names in the generated C by @gebner in #4800
• Cherry: call let-bound lambdas directly; inline small wrappers by @gebner in #4801
• Add native FStar.BV normalization by @amosr-msft in #4743
• Preserve projector sharing through type ascriptions by @amosr-msft in #4802
• Custard: keep the unit thunk on lambdas whose body erases to () (#4803) by @gebner in #4804
• Pulse: elaborate d.method args as a stateful call (#4805) by @gebner in #4807
• Update karamel submodule to d378c88b by @dzomo in #4810
• Pulse.Lib.ArrayPtr.memcpy: remove unused offsets (fixes #4809) by @gebner in #4811
• Pulse: rename pure model implementations to *-model.fst by @gebner in #4812
• Pulse.Lib.Closure: first-class closures for --codegen C by @gebner in #4813
• Cherry: specialize list higher-order functions on function arguments by @gebner in #4808
• Cherry: tail recursion modulo constructors by @gebner in #4816
• Monomorphize FStar.List.Tot's higher-order functions by @gebner in #4817
• Bump version to 2026.11.01 by @dzomo in #4818
• Cherry: silence -Wfree-nonheap-object in cherry_dec by @gebner in #4819
• Cherry: avoid big-integer arithmetic in SmallInt and Hash by @gebner in #4821
• Custard: default --custard_monomorphize_types to true for C and Cherry by @gebner in #4823
• Remove check world workflow. by @gebner in #4824
• Disable nightly Nix build. by @gebner in #4825
• Custard: test equality at a local let rec's type parameter (fixes #4739) by @gebner in #4822
• CI: switch to Ubuntu 26.04 by @gebner in #4826
• Cherry: update a solely held shared array in place by @gebner in #4827
• CI: avoid duplicate runs on PRs and merge queue by @gebner in #4829
• CI(windows): install opam depexts from pwsh by @gebner in #4831
• Run nightly CI on 24.04 by @gebner in #4832
• Cherry HashTable: clear only the buckets in use by @gebner in #4833
• Custard: leave runtime type parameters free in uniform specializations by @gebner in #4835
• Primops.Base: box primitive_step under Cherry by @gebner in #4837
• Custard: add opt-in function-level C local declaration hoisting by @tahina-pro in #4820
• Cherry: compare strings for SmallInt directly in C by @gebner in #4836
• AVLMap/PSMap/PIMap: monomorphize comparison and callback arguments by @gebner in #4839
• Cherry: reuse shared cells with a single reference by @gebner in #4838
• Ident: box lident under Cherry by @gebner in #4840
• Do not normalize erased spec arguments during extraction by @gebner in #4830
• Custard: --custard_init_locals, zero-initialized C locals by @tahina-pro in #4841
• Custard: raise --custard_max_specializations default to 10000 by @gebner in #4843
• IDE: compare dependency tasks without structural equality on repl_task by @gebner in #4845
• Custard: narrow-float #error only for identifiers, not string literals by @gebner in #4844
• Custard: do not unfold fixpoints when instantiating monomorphized arguments by @gebner in #4842
• Use the Core typechecker as F*'s only VC generator; Rel computes no guards by @nikswamy in #4605
• Custard: keep implementation binder attributes when specializing by @gebner in #4848
• Update karamel submodule to 50b61115 by @dzomo in #4849
• Custard: --custard_line_comments, C line comments in function bodies by @tahina-pro in #4850
• Cherry: avoid two sources of needless allocation by @gebner in #4851
• Fix BvModelAgreesWithZ3 perf regression from #4605; add annotation well-formedness soundness test by @nikswamy in #4853
• Pulse: store rendered context strings in the context, drop WeakMemo by @gebner in #4854
• Core: test the relation with EQUALITY? instead of structural equality by @gebner in #4855
• Cherry: faster SmallInt conversions and Array access by @gebner in #4857
• Syntax: no temporary tuple when hashing Tm_app by @gebner in #4858
• Custard OCaml: cheaper integer patterns by @gebner in #4856
• Eager tcresolve: pin uvars nested in class inputs by @gebner in #4861
• Custard: speed up extraction (164s -> 64s) by @gebner in #4860
• Cherry: force the common case of reference counting inline by @gebner in #4862
• Cherry: undyn takes the dyn owned and moves the payload out by @gebner in #4865
• Cherry: implement FStarC.SmallInt as an Int64.t by @gebner in #4864
• Cherry: peek at borrowed references instead of counting the read value by @gebner in #4866
• Bump version to 2026.11.08 by @dzomo in #4869
• Eager tcresolve: follow chains of uvar bounds when pinning inputs by @gebner in #4870
• Coercions: a closed coercion source type must match by @gebner in #4871
• Cherry: peek through inlined FStarC.Array.get/length by @gebner in #4873
• Interface instances take precedence over implementation-only dependencies by @gebner in #4872
• Cherry: ship mimalloc and link it statically by @gebner in #4875
• Custard: speed up extraction (186 s -> 72 s on the unit-test driver) by @gebner in #4876
• Cherry: FStarC.Util.contains and matches_at in C by @gebner in #4879
• Eager typeclass resolution; remove noinst; overload Pulse |-> for Frac by @gebner in #4859
• Cherry: don't share values stored in global refs until a thread starts by @gebner in #4880
• Do not rely on List.nth raising when out of range by @gebner in #4878
• Cherry: borrow fields of owned boxed values by @gebner in #4881
• Custard C: escape '?' to avoid trigraphs by @gebner in #4877
• Custard: avoid per-call overhead in extraction by @gebner in #4882
• Cfg: look up env-dependent primops lazily by @gebner in #4884
• Env.in_cur_mod: compare namespaces without appending by @gebner in #4885
• Hierarchical modules: IDE / file name fix by @amosr-msft in #4797
• Pulse: library-only logical atomicity with helping and FIFO examples by @nikswamy in #4806
• Pulse join: keep what a generalized binder stands for in each branch by @nikswamy in #4887
• Update karamel submodule to 3384ecaf by @dzomo in #4888
• Core: fix unsound guard caching in args_or_eq (#4890) by @gebner in #4891
• Custard: only unfold-and-rescan type heads that have a definition by @gebner in #4892
• Upgrade github actions to macos 15. by @gebner in #4893
• Normalize: skip normalization in non_info_norm for inductive heads by @gebner in #4894
• Native typeclass resolver with caching by @gebner in #4883
• Syntax.Visit: direct monomorphizable visitor instead of VisitM by @gebner in #4895
• Cherry: hash strings eight bytes at a time by @gebner in #4897
• Cherry: inline definitions that only project a field of their parameter by @gebner in #4898
• Cherry: keep parameters borrowed across tail calls that cannot loop by @gebner in #4896
• Cherry: box the compiler's large state records by @gebner in #4900
• Cherry: box Range.Type.range and HashTable.tbl by @gebner in #4902
• Cherry: --custard_type_stats by @gebner in #4903
• Remove CNoInline and postprocess_for_extraction_with attributes by @gebner in #4904
• Cherry: typing fixes for extracting the ulib tactic plugins by @gebner in #4905
• Custard: pass RegEmb's type arguments in binder order by @gebner in #4906
• Cherry: support the modules the ulib tactic plugins use by @gebner in #4907
• Cherry: persistent cells skip the slow inc/dec call by @gebner in #4910
• Cherry: an unboxed record update moves the fields it keeps by @gebner in #4911
• Cherry: FStarC.List builds results with tail calls modulo constructors by @gebner in #4912
• Cherry: a match on a tuple of variables is a view by @gebner in #4909
• Cherry: free and mark nested cells directly up to a depth budget by @gebner in #4913
• Custard/Cherry: flatten an application of an application by @gebner in #4915
• Bump version to 2026.11.15 by @dzomo in #4920

New Contributors

• @tyler-utah made their first contribution in #4786

Full Changelog: v2026.10.25...v2026.11.15