spec/math/u64.bend

bend-collections-laws-crypto@1.0.0.0 · 53 lines · 9 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend as N
3import bend-collections-laws-crypto@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)}