i64.bend checks

bend-i64: a SIGNED 64-bit integer in pure Bend, two's complement over Word(64n). Source: https://github.com/phenomenon0/bend-i64

The arithmetic is bit-identical to unsigned two's complement — add, sub, mul and the bitwise ops ride the same width-64 Word.* instantiations. The signed layer is interpretation: negation as 0 - x, SIGNED comparison by biasing both operands with the sign bit (x XOR 2^63) before the unsigned compare, and arithmetic right shift that replicates the sign.

The law is machine-checked: add_comm is proved by instantiating Base's own generic inductive lemma Word.add_comm(64n, ...) — and it transfers to the signed reading exactly because addition ignores the sign.

Speed: same as its unsigned twin — every op walks the generic Word(64n) layer (reference-grade on hot loops; bench in the repo README). A native word-64 lowering turns the same semantics into machine-speed ops — merged in the omen fork, proposed upstream. Cold paths today: IDs, deltas, proofs.

Boundaries, stated honestly: - to_nat is valid for 0 <= v <= 2^48-1 (Nat immediate limit); negative values read as their bit pattern and are documented, not converted. - shl.n / shr.s.n are bit-at-a-time folds (n small); O(n). - Division is not implemented yet. - No FFI, no intrinsics, no unsafe; checked on stock Bend 2.0.17.

Note on order: dotted defs (x.y) are defined before their first call — this file keeps that discipline throughout (see tests note in the README).