Repository navigation
docs(storage): state where encode_value puts NaN (#688) - #704
Merged
Merged
Conversation
encode_value writes every NaN as 0x7FF8_0000_0000_0000 without the sign transform, so NaN sorts among the negative subnormals and is byte-equal to f64::from_bits(0x8007_FFFF_FFFF_FFFF), while Value::cmp and the v8 keys put it after +inf. The doc comment now says so and a test pins the position; the encoding stays as on v2, where it is v7 on-disk AVET keys. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0169pNQsLcCEn48te9X9WuZW
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0169pNQsLcCEn48te9X9WuZW
This was referenced Oct 23, 2026
adityamukho
added a commit
that referenced
this pull request
Oct 23, 2026
Each PR raised the count from 1,771 to 1,772; merged together they add two. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0169pNQsLcCEn48te9X9WuZW
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.
Doc-only fix for #688 on
v3. Refs #688.encode_valuewrites every NaN as0x03+0x7FF8_0000_0000_0000, without the sign transform. So NaN:-0.0and every positive float (Value::cmpand the v8 keys (keys::float_bits) puts it after+∞);f64::from_bits(0x8007_FFFF_FFFF_FFFF)(about-1.1125e-308). The issue didn't mention this.The encoding stays as it is (spec
2026-10-22-kani-storage-encoding-design.md§6): on v3 the bytes are never stored, but they match v2's v7 AVET keys. Changes:encode_value's doc comment and the inline NaN comment state the real position, and warn against value range scans or NaN/subnormal equality on these bytes.test_encode_value_nan_sorts_among_negative_subnormalspins the bytes, the subnormal twin and the sort position.CLAUDE.md/docs/TEST_COVERAGE.md+1.The equality collision has no visible effect: NaN can't be stored through Datalog (there's no NaN literal, and arithmetic that yields NaN fails). A prepared query that binds
Value::Float(NaN)against a stored-1.1125e-308returns no rows, because the matcher's float comparison rejects NaN.🤖 Generated with Claude Code
https://claude.ai/code/session_0169pNQsLcCEn48te9X9WuZW