spec/math/u64.bend
bend-collections-laws-containers@1.0.0.0 · 53 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/numeric.bend as N
3import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as U
4
5# Specification of src/math/u64.bend: a U64 denotes the 64-bit word whose
6# low 32 bits are lo and high 32 bits hi (bits below), and each operation is
7# the word operation of spec/lib/numeric.bend: modular addition, two's
8# complement negation, signed order, unsigned and signed quotients by small
9# divisors.
10#
11# function clauses proved in
12# is_zero IsZero.value proofs/math/proof.bend
13# le_signed LeSigned.value (u64_*, via u64/u64.bend
14# add Add.bits, Add.modular and u64/u64div.bend)
15# neg Neg.bits
16# div_small DivSmall.quotient
17# div_small_signed DivSmallSigned.quotient
18
19def bits(a: U.U64) -> Word(64n):
20 match a:
21 case U.U64{lo, hi}:
22 N.pack(lo, hi)
23
24# the quotient of a signed word: rounded toward zero, as the magnitude's
25def signed_quotient(w: Word(64n), neg: Bool, +d: U32) -> Word(64n):
26 match neg:
27 case False{}:
28 N.unsigned_quotient(64n, w, d)
29 case True{}:
30 N.negative_quotient(64n, w, d)
31
32def IsZero.value(+a: U.U64) -> Type:
33 {U.is_zero(a) == N.zero(bits(a)) : Bool}
34
35def LeSigned.value(+a: U.U64, +b: U.U64) -> Type:
36 {U.le_signed(a, b) == N.order(bits(a), bits(b), N.negative(bits(a)), N.negative(bits(b))) : Bool}
37
38def Add.bits(+a: U.U64, +b: U.U64) -> Type:
39 {bits(U.add(a, b)) == Word.add(64n, bits(a), bits(b)) : Word(64n)}
40
41# addition modulo 2^64
42def Add.modular(+a: U.U64, +b: U.U64) -> Type:
43 {bits(U.add(a, b)) == N.from_nat(64n, Nat.add(N.unsigned(64n, bits(a)), N.unsigned(64n, bits(b)))) : Word(64n)}
44
45def Neg.bits(+a: U.U64) -> Type:
46 {bits(U.neg(a)) == Word.inc(64n, Word.not(64n, bits(a))) : Word(64n)}
47
48# divisors 1 .. 2^20 (the limb division stays inside 32 bits)
49def DivSmall.quotient(+a: U.U64, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}) -> Type:
50 {bits(U.div_small(a, d)) == N.unsigned_quotient(64n, bits(a), d) : Word(64n)}
51
52def DivSmallSigned.quotient(+a: U.U64, +d: U32, +hd0: {U32.is_zero(d) == False{} : Bool}, +hle: {U32.is_le(d, 1048576) == True{} : Bool}) -> Type:
53 {bits(U.div_small_signed(a, d)) == signed_quotient(bits(a), N.negative(bits(a)), d) : Word(64n)}