Repository navigation
encode_value sorts NaN among negative floats #688
Description
Summary
encode_value in src/storage/index.rs (identical on main and v3) writes NaN as 0x7FF8_0000_0000_0000 without the sign transform it applies to every other float. NaN therefore sorts between two negative subnormals, before -0.0 and every positive float. Value::cmp instead orders NaN after +∞.
A Kani harness found it in 1.5 s while prototyping #627:
let a: f64 = kani::any();
kani::assume(!a.is_nan());
assert!(encode_value(&Value::Float(a)) < encode_value(&Value::Float(f64::NAN))); // failsfloat_bits in src/storage/keys.rs on v3 is correct: it maps NaN to 0xFFF8….
Impact
No query results are affected, as far as I can find:
- Every lookup by
encode_valuebytes is an exact match (start..=endwith the samevalue_bytes, e.g.lookup_avet_attr_value). - Every other use is either an equality check (net-assert grouping, pending keys, the log writer) or a sort used only to compare two sets in tests.
Nothing range-scans by value through these bytes. This is not a data-integrity issue.
Proposed fix
Don't change the encoding. On main it is the value_bytes of on-disk v7 index keys, so changing it would reorder AVET keys in existing files. Instead, state the NaN position in encode_value's doc comment on both branches, so that nobody later builds a value range scan on these bytes assuming NaN sorts last.
Spec: docs/superpowers/specs/2026-10-22-kani-storage-encoding-design.md §6 (#627).
🤖 Generated with Claude Code
Activity
docs(spec): narrow the NaN claim's evidence, qualify injectivity (#627)
test(storage): split the NaN position assert so each branch runs (#688)
test(storage): split the NaN position assert so each branch runs (#688)
Merge pull request #704 from project-minigraf/docs/688-nan-encoding-v3
docs(storage): state where encode_value puts NaN (#688)
test(storage): split the NaN position assert so each branch runs (#688)
docs(storage): state where encode_value puts NaN (#688) — backport (#705
adityamukho commentedon Oct 23, 2026
Documented on both branches: v3 in #704, main in #705. The encoding is unchanged, as the spec proposed. Also: NaN's bytes are identical to the encoding of the negative subnormal
f64::from_bits(0x8007_FFFF_FFFF_FFFF), not just next to it. No query can reach this, because NaN can't be stored.