Skip to content

Extend C-210 to every bytes float writer - #140

Merged
O6lvl4 merged 2 commits into
mainfrom
c210-float-writer-family
Oct 13, 2026
Merged

O6lvl4 merged 2 commits into
mainfrom
c210-float-writer-family

Conversation

@O6lvl4

@O6lvl4 O6lvl4 commented Oct 13, 2026

Copy link
Copy Markdown
Contributor

Implements the owner's ruling on almide/almide#3658 (2026-10-13): C-210 extends to every bytes float writer.

Contract

C-210 named only the appends (append_f64_le/be, append_f32_le/be). Its statement now covers the whole family under one rule: the appends, the in-place sets (set_f64_le/be, set_f32_le/be, set_float32) and the cursor writes (write_f64_be, write_float32). Each writes the canonical NaN on every leg: f64 0x7FF8000000000000, f32 0x7FC00000. The rest of the statement is unchanged.

Fixtures

  • New: spec/wasm_cross/nan_canonical_bytes_set_write.almd. It sends five values through every set and write writer: 0.0/0.0, a from_bits payload NaN (sign set, low payload), a negated NaN, an arithmetic NaN, and 1.5. The 1.5 row shows that non-NaN bits stay raw.
  • Updated: spec/wasm_cross/nan_canonical_bytes_write.almd now matches the implementation's copy. The implementation added the #3647 rows (payload, negated and arithmetic NaN through all four appends) and they had not reached the judge.

Reference evaluator

ref/ wrote raw bits on every float writer, the appends included, so on a payload NaN it disagreed with C-210. Now:

  • all of its float writers (write_bytes_fn for append/set, write_float32, write_f32_le, write_f64_be) take their bits from one helper pair, obs_bits_f64 / obs_bits_f32;
  • it implements bytes.set_float32;
  • write_float32 accepts a Float32 value. It used to abstain with a type mismatch.

On the reference, both NaN fixtures now print the canonical bytes.

Gates (run locally)

All green:

  • check-contracts, check-contract-provenance, check-als-element-coverage, check-als-style, check-als-validation, check-links, check-gate-verification, selftest-conformance, check-runner-coverage, check-ratchet-separation --staged
  • check-ref-kernel, check-ref-totality: 733 evaluated, 18 abstained, ceiling 18
  • cargo fmt --check and cargo clippy -D warnings on ref/

Regenerated: docs/contracts/README.md, docs/contracts/conformance.md.

After this merges, the implementation advances proofs/als-pin.txt, then lands native and wasm canonicalization on its branch fix-3658-float-writer-nan.

O6lvl4 and others added 2 commits October 13, 2026 19:05
…or and implement set_float32

Co-Authored-By: Claude Opus 5.5 (1M context) <[email protected]>
…iters' NaN bits in a fixture

Co-Authored-By: Claude Opus 5.5 (1M context) <[email protected]>
@O6lvl4
O6lvl4 merged commit ec990fe into main Oct 13, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant