Repository navigation
docs(storage): state where encode_value puts NaN (#688) — backport - #705
Merged
Merged
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
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). The bytes are v7 on-disk AVET keys, so the encoding stays; the doc comment now says so, the old test comment claiming NaN sorts last is gone, and a test pins the position. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0169pNQsLcCEn48te9X9WuZW
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0169pNQsLcCEn48te9X9WuZW
adityamukho
force-pushed
the
docs/688-nan-encoding
branch
from
October 23, 2026 06:46
4dad28d to
1f07cd4
Compare
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
main, backport of the v3 PR. Refs #688.encode_valuewrites every NaN as0x03+0x7FF8_0000_0000_0000, without the sign transform. So NaN:-0.0and every positive float (Value::cmpputs 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 main these bytes are thevalue_bytesof on-disk 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. The old test comment claiming NaN sorts above all positive floats is removed.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