Repository navigation
Re-enable autoharness for the Unicode case conversions #717
Description
#687 removed --include-pattern unicode::unicode_data::conversions::to_ from the autoharness job. After the Unicode tables were regenerated upstream (nightly-2026-09-25), to_lower, to_upper, to_title and to_casefold still verify, but take 53 s, 79 s, 132 s and 589–612 s locally. That exceeds the job's 10m timeout on macOS, and the ubuntu runner died while verifying them under --jobs=3.
To re-enable, either make them cheaper (stubbing or bounding the table lookups) or run them in a job with a longer timeout and fewer parallel jobs.
Activity
feliperodri commentedon Oct 6, 2026
@Tianshu-Huang can you take a look at this?
Tianshu-Huang commentedon Oct 6, 2026
I started with the second option: run the four harnesses alone, one at a time, with a longer timeout. On an aarch64 machine (Apple M4 Pro, 48 GB, #687 head, Kani 1640445da, the same
run-kani.sh --run autoharnessflags CI uses) all four still timed out at 15 min, and the run peaked at 27.7 GB. So a longer timeout alone does not work.Then I looked at why they are slow. It is the loop unwind bound, not the regenerated table. The lookup is a binary search over about 200 entries, which takes 8 rounds. The table is a
static, and CBMC does not treat its length as a constant, so with CI's--default-unwind 1000it unrolls the search 1000 times.Same run with
--default-unwind 16:--default-unwind 1000(what CI uses)--default-unwind 16These are still complete proofs: Kani checks that 16 rounds are enough for every loop, and that check passed. So the first option, stubbing or bounding the lookups, is not needed either. It would weaken the proof for nothing.
Suggested fix, no library change: add a second
run-kani.sh --run autoharnessstep in CI with--harnesskeeps the hand-written harnesses out of that step (--include-patternalone still runs all of them).--jobs=1keeps memory under the ubuntu runner's 16 GB.If this solution looks good to you, I will open the PR.