proofs/lib/lemmas/src/wide.bend

bend-collections-laws-crypto@1.0.0.0 · 131 lines · 25 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend as NM
3
4# All bits are represented explicitly: no Nat holds a full-width integer.
5def zero() -> Word(64n):
6  Word.zero(64n)
7
8def inc(w: Word(64n)) -> Word(64n):
9  Word.inc(64n, w)
10
11def add(a: Word(64n), b: Word(64n)) -> Word(64n):
12  Word.add(64n, a, b)
13
14def neg(w: Word(64n)) -> Word(64n):
15  Word.inc(64n, Word.not(64n, w))
16
17def last(n: Nat, w: Word(n)) -> Bool:
18  match n:
19    case 0n:
20      False{}
21    case 1n+0n:
22      match w:
23        case WCon{b, tail}:
24          b
25    case 1n+1n+p:
26      match w:
27        case WCon{b, tail}:
28          last(1n+p, tail)
29
30def is_zero(n: Nat, w: Word(n)) -> Bool:
31  match n:
32    case 0n:
33      True{}
34    case 1n+p:
35      match w:
36        case WCon{b, tail}:
37          Bool.not(b) && is_zero(p, tail)
38
39def signed_order(a: Word(64n), b: Word(64n), sa: Bool, sb: Bool) -> Bool:
40  match sa sb:
41    case True{} False{}:
42      True{}
43    case False{} True{}:
44      False{}
45    case x y:
46      Cmp.is_le(Word.cmp(64n, a, b))
47
48def le(+a: Word(64n), +b: Word(64n)) -> Bool:
49  signed_order(a, b, last(64n, a), last(64n, b))
50
51def bit_u32(b: Bool) -> U32:
52  match b:
53    case False{}:
54      0
55    case True{}:
56      1
57
58type Division<-n: Nat> is Data:
59  Div{quotient: Word(n), remainder: U32}
60
61def digit_result(p: Nat, q: Word(p), r: U32, subtract: Bool) -> Division<1n+p>:
62  match subtract:
63    case False{}:
64      Div{WCon{False{}, q}, r}
65    case True{}:
66      Div{WCon{True{}, q}, U32.sub(r, 1000000)}
67
68def digit_compare(p: Nat, q: Word(p), +r: U32) -> Division<1n+p>:
69  digit_result(p, q, r, U32.is_ge(r, 1000000))
70
71def digit(p: Nat, b: Bool, prior: Division<p>) -> Division<1n+p>:
72  Div{q, r} = prior
73  digit_compare(p, q, U32.add(U32.mul(r, 2), bit_u32(b)))
74
75# Binary long division, processing the most significant bit first. The partial
76# remainder stays below 1,000,000; the next candidate fits in U32 (<2,000,000).
77def div_million(+n: Nat, w: Word(n)) -> Division<n>:
78  match n:
79    case 0n:
80      Div{WNil{}, 0}
81    case 1n+p:
82      match w:
83        case WCon{b, tail}:
84          digit(p, b, div_million(p, tail))
85
86def quotient(r: Division<64n>) -> Word(64n):
87  Div{q, rem} = r
88  q
89
90def unsigned_milliseconds(w: Word(64n)) -> Word(64n):
91  quotient(div_million(64n, w))
92
93def signed_milliseconds(w: Word(64n), negative: Bool) -> Word(64n):
94  match negative:
95    case False{}:
96      unsigned_milliseconds(w)
97    case True{}:
98      neg(unsigned_milliseconds(neg(w)))
99
100def milliseconds(+w: Word(64n)) -> Word(64n):
101  signed_milliseconds(w, last(64n, w))
102
103# Exact limb boundary used by the host bridge; limbs themselves are primitive U32.
104def join(n: Nat, +m: Nat, a: Word(n), b: Word(m)) -> Word(Nat.add(n, m)):
105  NM.join(n, m, a, b)
106
107type Parts<-n: Nat, -m: Nat> is Data:
108  Split{low: Word(n), high: Word(m)}
109
110def split_cons(-n: Nat, -m: Nat, h: Bool, parts: Parts<n, m>) -> Parts<1n+n, m>:
111  Split{low, high} = parts
112  Split{WCon{h, low}, high}
113
114def split(n: Nat, +m: Nat, w: Word(Nat.add(n, m))) -> Parts<n, m>:
115  match n:
116    case 0n:
117      Split{WNil{}, w}
118    case 1n+p:
119      match w:
120        case WCon{h, tail}:
121          split_cons(p, m, h, split(p, m, tail))
122
123def pack(low: U32, high: U32) -> Word(64n):
124  NM.pack(low, high)
125
126def limbs(parts: Parts<32n, 32n>) -> U32 & U32:
127  Split{lo, hi} = parts
128  (U32{lo}, U32{hi})
129
130def unpack(w: Word(64n)) -> U32 & U32:
131  limbs(split(32n, 32n, w))