Restore the full StringEscapeRoundtrip threshold via total nibble division - #807
Merged
Merged
Conversation
…ision `Bytes.highNibble` and `Bytes.lowNibble` are now `Int.div(value, 16)` and `Int.mod(value, 16)`. A syntactic nonzero literal divisor already types as plain Int and lowers to the Euclidean intrinsics, so the sixteen-branch comparison ladder the nibbles used to avoid the Result path is no longer needed on any backend. The module keeps the same functions and the same smart-constructor gating shape, so the packed-sequence recognizer and the certificate KPI denominator are unchanged. With the ladder gone, `Bytes.byteToHex` unfolds definitionally to `hexDigit (v / 16) + hexDigit (v % 16)`, so the synthesized control-escape lemma closes for the whole octet range in one `simp` instead of enumerating one `by_cases` arm per nibble. The escaped-string roundtrip detector accepts control thresholds 1..=256 again — the `Bytes.fromList` payload range — where it had been narrowed to 1..=32. A new lake-gated proof spec pins the recovered range: a wire format that hex-escapes every octet (threshold 256, terminator and escape introducer above it) certifies universal and sorry-free. The existing threshold-32 laws, including the JSON example, stay green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
1 participant
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.
Bytes.highNibble/Bytes.lowNibblebecomeInt.div(value, 16)/Int.mod(value, 16). The literal-divisor rule types both as plainIntand lowers them to the Euclidean intrinsics, so the sixteen-branch comparison ladder that existed only to avoid theResultpath is gone. Same function count, sameallInRange/fromListgating shape, so the wasm-gc packed-sequence recognizer and the(12 certified, 90 source-level-only)certificate KPI are unchanged.Bytes.byteToHexis now definitionallyhexDigit (v / 16) + hexDigit (v % 16), so the synthesized control-escape lemma closes for any octet in onesimpinstead of aby_casesarm per nibble. The escaped-string roundtrip detector accepts control thresholds1..=256again (theBytes.fromListpayload range), where it had been narrowed to1..=32.New lake-gated spec
lean_proves_full_octet_escape_threshold_when_lake_is_available: a wire format that hex-escapes every octet (threshold 256, terminator/escape introducer above it) certifiesuniversal:true,sorries:0. With the gate put back at 32 the same fixture falls to a caughtsorry.Tests run locally: full
proof_spec(228, includes the JSON example and both existing escape-roundtrip laws),cert_decode_spec,cert_whole_module_guard_iso, the json--certifyKPI test,wasm_gc_packed_sequence,wasm_gc_spec,stdlib_spec(VM + wasm-gc + wasip2),rust_codegen_regressionincl. ignored, bytes/sha256 subsets ofrust_codegen_differential/wasip2_codegen_regression/wasip2_tcp/wasm_gc_codegen_regression,eval_spec,--lib, plus the Dafny backend on the embedded-bytes fixture (38 verified, 0 errors).🤖 Generated with Claude Code