Binary64 arithmetic

lib/math/binary64.tri provides addition, subtraction, multiplication and division as pure Tree Calculus functions. Each operation rounds to nearest, ties to even, and returns its exception flags explicitly.

The repository workspace registers binary64 and its private providers. The support fixture includes their compiled interfaces and the contract-composition demo, with authenticated source snapshots and build receipts.

For a standalone source workspace, use these filenames with a retained stable compiler:

Repository source	Workspace filename
lib/math/binary64.tri	binary64.tri
lib/math/native.tri	native_math.tri
lib/math/binary64/NAME.tri	binary64_NAME.tri

Import the interface with !import binary64 as F. The portable tool guide describes compiler selection and source compilation. The validation procedure prepares this workspace and compiles a complete example.

Words and working values

A Word is a canonical LSB-first natural-number tree in 0..2^64-1, containing the exact IEEE binary64 bits. Every bit pattern is accepted, including signed zeros, infinities and signaling NaNs. See the natural-number encoding for its tree structure.

A Value is a working value obtained from a successful import or an arithmetic reply. Retain Values between calculations and use Words for storage and interchange. Obtain and inspect Values through the functions below; the internal modules own their representation.

Trusted arithmetic and export require Values produced by this interface. Checks at the Word boundary establish that invariant. As ordinary tricu trees, Values remain structurally inspectable and forgeable; this API contract is not a security barrier.

Interface

Checked boundaries use the standard Result protocol: ok value remainder or err diagnostic remainder.

Function	Result
word? word remainder	Contract accepting the original Word and preserving the remainder.
fromBitsC word remainder	Transforming contract accepting a Value and preserving the remainder.
fromBits word	Checked import: Result Value, empty remainder.
toBits value	Exact export of a trusted Value to Word.
add a b, subtract a b, multiply a b, divide a b	Trusted arithmetic: pair (Value, Flags).
value reply, flags reply	Projections of an arithmetic reply.
clearFlags	Five false flags.
mergeFlags a b	Componentwise OR of two valid flag sets.
invalid f, divideByZero f, overflow f, underflow f, inexact f	Boolean flag projections.
addBits a b, subtractBits a b, multiplyBits a b, divideBits a b	Checked Word operations: Result (Word, Flags).

Use bindResult or matchResult to unwrap checked imports, then use value and flags to consume arithmetic replies. A successful Word operation already contains the exported Word. Merge flags explicitly to accumulate status across operations.

Invalid Word shape or range produces err "binary64 word" remainder. Word operations use an empty remainder and validate left then right. A left failure returns immediately; every accepted pair has both Words checked, including NaN inputs. Imports and exports preserve signaling status and payload bits exactly.

IEEE arithmetic exceptions produce successful value/flag replies. For example, divideBits 0 0 succeeds with a quiet NaN and invalid=true.

Rounding and exceptional values

Each operation produces a binary64 result, including gradual underflow. A sequence uses the rounded result of each preceding operation.

• The leftmost NaN supplies the result sign and payload and is quieted. Either signaling operand raises invalid, including a signaling right operand when the left NaN is already quiet.
• Other invalid operations produce positive 0x7ff8000000000000 and invalid.
• Finite nonzero divided by zero produces signed infinity and divide-by-zero. Infinity divided by zero produces signed infinity with clear flags. Zero/zero and infinity/infinity raise invalid.
• Overflow produces signed infinity and raises overflow plus inexact.
• Underflow uses after-rounding tininess: precision rounding with an unbounded exponent. Inexact tiny results raise underflow, including boundary values stored as minimum normal.
• Exact opposite-sign cancellation produces positive zero. Multiplication and division use XOR signs, including results rounded to zero.

Flags describe their individual operation. Import/export preserves the word as transport data; arithmetic determines quieting and exception flags.

Composition

demos/binary64.tri accepts a pair of Words and computes x*y+x. It uses base.pairOf F.fromBitsC F.fromBitsC to check the pair and produce Values, rounds after multiplication and addition, merges their flags, and exports the final Word. Add lib/base.tri to the workspace as base.tri to compile it.

The implementation contracts describe value invariants and demand. The validation guide covers complete-result checks, independent references and small-workload resource tests.