Re-sweep after reqproof translator fixes shipped on feat/translator-gap-fixes (HEAD 02a8cb94): char literals (Fix #3), type conversions (Fix #4), package-level const references (Fix #6), multi-lemma per host (Fix #7). Coverage went from 18/18 (100%) to 25/25 (100%). Lemma corpus 11 -> 23 (9 -> 21 PROVED via cached path; 22 PROVED + 1 expected COUNTEREXAMPLE via fresh-translation --coverage path). - 4 new lemmas via Fix #3 (char literals): h2I_decimal_digit, h2I_uppercase_hex, h2I_lowercase_hex, h2I_nondigit_is_badhex. All exercise '0'..'9' / 'A'..'F' / 'a'..'f' on h2I. - Fix #4 (type conversions) is on the same h2I host — its body uses int(c-48) etc., which previously made the host untranslatable. Without Fix #4 the four char-literal lemmas above would translation- error on the host. - 3 new lemmas via Fix #6 (package consts): h2I_nondigit_is_badhex (uses const badHex), isUTF16EncodedRune_const_high_bound (uses const highSurrogateOffset), isUTF16EncodedRune_const_bmp_bound (uses const basicMultilingualPlaneReservedOffset). - 6 additional :lemma directives on existing hosts via Fix #7 (multi-lemma per host): tokenEnd_nonneg, tokenEnd_empty_zero, tokenStart_nonneg, tokenStart_empty_zero, nextToken_signed_disjoint, lastToken_signed_disjoint. Pre-fix the scanner dropped any second :lemma on a host silently. Tried-and-rejected (still blocked by other deferred translator gaps): - combineUTF16Surrogates: Fix #6 resolves the package-const refs in the body, but `<<` shift op is unsupported (separate gap, not one of #1/#2/#5). - findTokenStart: still blocked by #1 (early-return / __early_val scoping bug in switch + return body shape). - unescapeToUTF8: still blocked by #2 (switch). No new production bugs surfaced. The single COUNTEREXAMPLE (deleteCleanupBuggy_prevTok_nonneg_falsifiable) is the existing documented OSS-Fuzz Delete demo from a6c5ed3 — counterexample prevTok=-1, remainedTok=0 matches the documented falsifying witness. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

License #6

Description

Activity

buger commented on Mar 22, 2016

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions