~/jendhub

spec/math/w64.bend

bend-collections-laws-crypto@1.0.0.0 · 122 lines · 27 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
4import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
5import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
6
7# Specification of src/math/w64.bend: unsigned 64-bit arithmetic on the
8# two-limb U64 (low limb first). value(a) is the natural number a denotes;
9# every operation is the Nat operation modulo 2^64 (C.low(64n, _): the
10# checker never forms 2^64; spec/lib/common.bend), as in
11# spec/math/u64.bend's word model (the two agree: value(a) is
12# unsigned(64, bits(a))).
13#
14# STATED, TESTED, NOT PROVED: w64.bend is the U64 instance's engine; its
15# clauses are exercised through tools/check_generic.py (every generic
16# function at U64 against Python integers) and tools/check_f64.py (the
17# software binary64's significand arithmetic), not proved.
18#
19#   function          clauses
20#   mul32             Mul32.value
21#   add, add_over     Add.value, AddOver.value
22#   sub               Sub.value
23#   mul, mul_over     Mul.value, MulOver.value
24#   half, odd         Half.value, Odd.value
25#   lt, le, eq,       Lt.value, Le.value, Eq.value, IsZero.value
26#   is_zero
27#   div32, mod32      Div32.quot, Div32.rem, Mod32.value
28#   quot, rem         DivMod.quot, DivMod.rem
29#   mulmod            MulMod.value
30#   isqrt, isqrt32    Isqrt.value, Isqrt32.value
31#   shl, shr,         Shl.value, Shr.value, ShrJam.value
32#   shr_jam
33#   clz               Clz.value
34
35def value(a: W.U64) -> Nat:
36  match a:
37    case W.U64{lo, hi}:
38      Nat.add(U32.to_nat(lo), C.shift(32n, U32.to_nat(hi)))
39
40# the U64 of a value below 2^64
41def of_nat(+n: Nat) -> W.U64:
42  W.U64{U32.from_nat(C.low(32n, n)), U32.from_nat(C.high(32n, n))}
43
44def Mul32.value(+a: U32, +b: U32) -> Type:
45  {value(X.mul32(a, b)) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
46
47def Add.value(+a: W.U64, +b: W.U64) -> Type:
48  {value(X.add(a, b)) == C.low(64n, Nat.add(value(a), value(b))) : Nat}
49
50def AddOver.value(+a: W.U64, +b: W.U64) -> Type:
51  {X.add_over(a, b) == Bool.not(C.fits(64n, Nat.add(value(a), value(b)))) : Bool}
52
53def Sub.value(+a: W.U64, +b: W.U64, +h: {Nat.is_le(value(b), value(a)) == True{} : Bool}) -> Type:
54  {value(X.sub(a, b)) == Nat.sub(value(a), value(b)) : Nat}
55
56def Mul.value(+a: W.U64, +b: W.U64) -> Type:
57  {value(X.mul(a, b)) == C.low(64n, Nat.mul(value(a), value(b))) : Nat}
58
59def MulOver.value(+a: W.U64, +b: W.U64) -> Type:
60  {X.mul_over(a, b) == Bool.not(C.fits(64n, Nat.mul(value(a), value(b)))) : Bool}
61
62def Half.value(+a: W.U64) -> Type:
63  {value(X.half(a)) == Nat.div(value(a), 2n) : Nat}
64
65def Odd.value(+a: W.U64) -> Type:
66  {X.odd(a) == Nat.is_eq(Nat.mod(value(a), 2n), 1n) : Bool}
67
68def Lt.value(+a: W.U64, +b: W.U64) -> Type:
69  {X.lt(a, b) == Nat.is_lt(value(a), value(b)) : Bool}
70
71def Le.value(+a: W.U64, +b: W.U64) -> Type:
72  {X.le(a, b) == Nat.is_le(value(a), value(b)) : Bool}
73
74def Eq.value(+a: W.U64, +b: W.U64) -> Type:
75  {X.eq(a, b) == Nat.is_eq(value(a), value(b)) : Bool}
76
77def IsZero.value(+a: W.U64) -> Type:
78  {X.is_zero(a) == Nat.is_eq(value(a), 0n) : Bool}
79
80def Div32.quot(+a: W.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> Type:
81  {value(X.fst_q(X.div32(a, d))) == Nat.div(value(a), U32.to_nat(d)) : Nat}
82
83def Div32.rem(+a: W.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> Type:
84  {U32.to_nat(X.snd_r(X.div32(a, d))) == Nat.mod(value(a), U32.to_nat(d)) : Nat}
85
86def Mod32.value(+a: W.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}) -> Type:
87  {U32.to_nat(X.mod32(a, d)) == Nat.mod(value(a), U32.to_nat(d)) : Nat}
88
89def DivMod.quot(+a: W.U64, +b: W.U64, +hb: {X.is_zero(b) == False{} : Bool}) -> Type:
90  {value(X.quot(a, b)) == Nat.div(value(a), value(b)) : Nat}
91
92def DivMod.rem(+a: W.U64, +b: W.U64, +hb: {X.is_zero(b) == False{} : Bool}) -> Type:
93  {value(X.rem(a, b)) == Nat.mod(value(a), value(b)) : Nat}
94
95# a, b < m: the product reduced, with no 64-bit overflow on the way
96def MulMod.value(+a: W.U64, +b: W.U64, +m: W.U64, +ha: {Nat.is_lt(value(a), value(m)) == True{} : Bool}, +hb: {Nat.is_lt(value(b), value(m)) == True{} : Bool}) -> Type:
97  {value(X.mulmod(a, b, m)) == Nat.mod(Nat.mul(value(a), value(b)), value(m)) : Nat}
98
99# the integer square root of the proved Nat reference
100def Isqrt.value(+n: W.U64) -> Type:
101  {value(X.isqrt(n)) == M.isqrt(value(n)) : Nat}
102
103def Isqrt32.value(+x: U32) -> Type:
104  {U32.to_nat(X.isqrt32(x)) == M.isqrt(U32.to_nat(x)) : Nat}
105
106def Shl.value(+a: W.U64, +k: Nat, +hk: {Nat.is_lt(k, 64n) == True{} : Bool}) -> Type:
107  {value(X.shl(a, k)) == C.low(64n, C.shift(k, value(a))) : Nat}
108
109def Shr.value(+a: W.U64, +k: Nat) -> Type:
110  {value(X.shr(a, k)) == C.high(k, value(a)) : Nat}
111
112# shifted right, with the shifted-out bits OR-ed into bit 0 (SoftFloat's
113# softfloat_shiftRightJam64); jam(q, r) sets q's bit 0 when r is nonzero
114def jam(+q: Nat, +r: Nat) -> Nat:
115  Nat.add(Nat.mul(2n, Nat.div(q, 2n)), Nat.max(Nat.mod(q, 2n), Nat.min(r, 1n)))
116
117def ShrJam.value(+a: W.U64, +k: Nat) -> Type:
118  {value(X.shr_jam(a, k)) == jam(C.high(k, value(a)), C.low(k, value(a))) : Nat}
119
120# 64 for zero
121def Clz.value(+a: W.U64) -> Type:
122  {X.clz(a) == Nat.sub(64n, M.bit_length(value(a))) : Nat}