Repository navigation
String.order walks both strings once and hands nothing back: a comparison is one tail call per char, 8x on the C lane, and String.eq of two 50000-char strings no longer overflows the JS lane - #1459
Merged
Conversation
…ison is one tail call per char, 8x on the C lane, and String.eq of two 50000-char strings no longer overflows the JS lane String.order was Pair.snd(String.cmp(a, b)): String.cmp hands both strings back, so String.eq and the is_ twins rebuilt every char they read and recursed through String.cmp.fin on the host stack of the JS lane. Now String.order.go(a, b, c) carries the last chars' comparison as a Cmp column after the strings, as Map.has.go carries its test, and each char is one U32.cmp and one tail call. String.cmp stays for the callers that keep the strings (Map's leaves). Measured on Linux x86-64, one thread, 300,000 fresh ~20-char pairs differing at the last char, net of building them: a C String.eq goes from 1.10 us to 0.13 us; List.sort of 20,000 strings by String.is_le from 61 ms to 17 ms; the JS lane 1.5x net. tests/base/string_order.bend pins the order on empty, equal, prefix, first-char and last-char differences and on two 50000-char strings, which on main fail the interpreted and JS lanes with "memory fault (machine stack overflow?)". A reflexivity lemma over String.eq is an induction on the string with U32.cmp's reflexivity, and passes --verdict, as does the test. Repo gate 54/54; tests/base and tests/show unchanged against main on four lanes. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
…chars and lengths
Lorenzobattistela
force-pushed
the
string-order
branch
from
October 14, 2026 13:24
f4caa28 to
7372dfd
Compare
Lorenzobattistela
approved these changes
Oct 14, 2026
Merged
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
String.orderused to bePair.snd(String.cmp(a, b)). That walk wasn't a tail call and rebuilt both strings, so the JS and interpreter lanes overflowed the stack on long strings.String.eqcrashed on two 50,000-char strings.The new
String.order.go(a, b, c)walks both strings once and carries the order so far inc. It returns at the first differing char, or by length when one string is a prefix of the other.String.cmpand the Map ops that use it are unchanged.Pair.snd(String.cmp)on all 116,281 pairs of strings up to length 4 (empty strings, prefixes, chars 0 and 0xFFFFFFFF).tests/base/string_order.bendcovers the edge cases. Two of its cases check that the first difference beats later chars and lengths. It also runs 50,000-char strings, which crash main on interp, bun and node.--verdictALL PROOFS CHECK.