src/crypto/sha/packed/packed.bend

bend-collections-laws-crypto@1.0.0.0 · 190 lines · 44 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/core.bend as Core
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S
4
5# Packed big-endian words: four bytes per U32. Array<U32> is flat u32 storage in native C.
6def at(a: Array<U32>, i: U32) -> Array<U32> & U32:
7  Array.get(U32,a,i)
8
9def partial(+w: U32, delta: Nat) -> U32:
10  match delta:
11    case 0n: 2147483648
12    case 1n: U32.or(U32.and(w,4278190080),8388608)
13    case 2n: U32.or(U32.and(w,4294901760),32768)
14    case 3n: U32.or(U32.and(w,4294967040),128)
15    case _: w
16
17def pad_choose(c: Cmp, w: U32, delta: Nat) -> U32:
18  match c:
19    case GT{}: 0
20    case EQ{}: 2147483648
21    case LT{}: partial(w,delta)
22
23def pad_word(w: U32, +pos: Nat, +remain: Nat) -> U32:
24  pad_choose(Nat.cmp(pos,remain),w,Nat.sub(remain,pos))
25
26def length_word(short: Bool, w: U32, length: U32) -> U32:
27  match short:
28    case True{}: length
29    case False{}: w
30
31def read16(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
32  (a, w15) = pair
33  (a,Core.fips_compress16(w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,w15,extra,s))
34
35def read15(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
36  (a, w14) = pair
37  read16(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,at(a,U32.inc(index)))
38
39def read14(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
40  (a, w13) = pair
41  read15(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,at(a,U32.inc(index)))
42
43def read13(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
44  (a, w12) = pair
45  read14(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,at(a,U32.inc(index)))
46
47def read12(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
48  (a, w11) = pair
49  read13(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,at(a,U32.inc(index)))
50
51def read11(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
52  (a, w10) = pair
53  read12(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,at(a,U32.inc(index)))
54
55def read10(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
56  (a, w9) = pair
57  read11(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,at(a,U32.inc(index)))
58
59def read9(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
60  (a, w8) = pair
61  read10(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,w8,at(a,U32.inc(index)))
62
63def read8(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
64  (a, w7) = pair
65  read9(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,w7,at(a,U32.inc(index)))
66
67def read7(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
68  (a, w6) = pair
69  read8(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,w6,at(a,U32.inc(index)))
70
71def read6(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
72  (a, w5) = pair
73  read7(extra,U32.inc(index),s,w0,w1,w2,w3,w4,w5,at(a,U32.inc(index)))
74
75def read5(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
76  (a, w4) = pair
77  read6(extra,U32.inc(index),s,w0,w1,w2,w3,w4,at(a,U32.inc(index)))
78
79def read4(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, w2: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
80  (a, w3) = pair
81  read5(extra,U32.inc(index),s,w0,w1,w2,w3,at(a,U32.inc(index)))
82
83def read3(+extra: Nat,+index: U32, s: S.State, w0: U32, w1: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
84  (a, w2) = pair
85  read4(extra,U32.inc(index),s,w0,w1,w2,at(a,U32.inc(index)))
86
87def read2(+extra: Nat,+index: U32, s: S.State, w0: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
88  (a, w1) = pair
89  read3(extra,U32.inc(index),s,w0,w1,at(a,U32.inc(index)))
90
91def read1(+extra: Nat,+index: U32, s: S.State, pair: Array<U32> & U32) -> Array<U32> & S.State:
92  (a, w0) = pair
93  read2(extra,U32.inc(index),s,w0,at(a,U32.inc(index)))
94
95def pad16(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
96  (a, w15) = pair
97  (a,Core.fips_compress16(pad_word(w0,0n,remain),pad_word(w1,4n,remain),pad_word(w2,8n,remain),pad_word(w3,12n,remain),pad_word(w4,16n,remain),pad_word(w5,20n,remain),pad_word(w6,24n,remain),pad_word(w7,28n,remain),pad_word(w8,32n,remain),pad_word(w9,36n,remain),pad_word(w10,40n,remain),pad_word(w11,44n,remain),pad_word(w12,48n,remain),pad_word(w13,52n,remain),length_word(Nat.is_lt(remain,56n),pad_word(w14,56n,remain),Core.len_hi(total)),length_word(Nat.is_lt(remain,56n),pad_word(w15,60n,remain),Core.len_lo(total)),extra,s))
98
99def pad15(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
100  (a, w14) = pair
101  pad16(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,w14,at(a,U32.inc(index)))
102
103def pad14(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
104  (a, w13) = pair
105  pad15(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,w13,at(a,U32.inc(index)))
106
107def pad13(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
108  (a, w12) = pair
109  pad14(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,w12,at(a,U32.inc(index)))
110
111def pad12(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
112  (a, w11) = pair
113  pad13(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,w11,at(a,U32.inc(index)))
114
115def pad11(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
116  (a, w10) = pair
117  pad12(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,w10,at(a,U32.inc(index)))
118
119def pad10(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
120  (a, w9) = pair
121  pad11(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,w9,at(a,U32.inc(index)))
122
123def pad9(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
124  (a, w8) = pair
125  pad10(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,w8,at(a,U32.inc(index)))
126
127def pad8(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
128  (a, w7) = pair
129  pad9(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,w7,at(a,U32.inc(index)))
130
131def pad7(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
132  (a, w6) = pair
133  pad8(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,w6,at(a,U32.inc(index)))
134
135def pad6(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
136  (a, w5) = pair
137  pad7(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,w5,at(a,U32.inc(index)))
138
139def pad5(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, w3: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
140  (a, w4) = pair
141  pad6(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,w4,at(a,U32.inc(index)))
142
143def pad4(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, w2: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
144  (a, w3) = pair
145  pad5(extra,U32.inc(index),s,remain,total,w0,w1,w2,w3,at(a,U32.inc(index)))
146
147def pad3(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, w1: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
148  (a, w2) = pair
149  pad4(extra,U32.inc(index),s,remain,total,w0,w1,w2,at(a,U32.inc(index)))
150
151def pad2(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, w0: U32, pair: Array<U32> & U32) -> Array<U32> & S.State:
152  (a, w1) = pair
153  pad3(extra,U32.inc(index),s,remain,total,w0,w1,at(a,U32.inc(index)))
154
155def pad1(+extra: Nat,+index: U32, s: S.State, +remain: Nat, +total: Nat, pair: Array<U32> & U32) -> Array<U32> & S.State:
156  (a, w0) = pair
157  pad2(extra,U32.inc(index),s,remain,total,w0,at(a,U32.inc(index)))
158
159def final_extra(+extra: Nat,more: Bool, +total: Nat, pair: Array<U32> & S.State) -> Array<U32> & S.State:
160  match more pair:
161    case False{} Tuple{a,s}: (a,s)
162    case True{} Tuple{a,s}:
163      (a,Core.fips_compress16(0,0,0,0,0,0,0,0,0,0,0,0,0,0,Core.len_hi(total),Core.len_lo(total),extra,s))
164
165def blocks(+extra: Nat,n: Nat, +index: U32, +remain: Nat, +total: Nat, pair: Array<U32> & S.State) -> Array<U32> & S.State:
166  match n pair:
167    case 0n Tuple{a,s}:
168      final_extra(extra,Nat.is_ge(remain,56n),total,pad1(extra,index,s,remain,total,at(a,index)))
169    case 1n+p Tuple{a,s}:
170      blocks(extra,p,U32.add(index,16),remain,total,read1(extra,index,s,at(a,index)))
171
172def take_state(pair: Array<U32> & S.State) -> S.State:
173  Pair.snd(Array<U32>,S.State,pair)
174
175# Internal entry; callers must establish length <= 4*array capacity.
176def hash_unchecked(a: Array<U32>, +length: Nat) -> S.State:
177  take_state(blocks(48n,Nat.div(length,64n),0,Nat.mod(length,64n),length,(a,Core.initial())))
178
179def checked(valid: Bool, a: Array<U32>, length: Nat) -> Maybe<&2,S.State>:
180  match valid:
181    case False{}: None{}
182    case True{}: Some{hash_unchecked(a,length)}
183
184def sized(+length: Nat, pair: Array<U32> & U32) -> Maybe<&2,S.State>:
185  (a,capacity) = pair
186  checked(Nat.is_le(length,Nat.mul(4n,U32.to_nat(capacity))),a,length)
187
188# Public bounded API; consumes the input array, without constructing a byte list.
189def hash(a: Array<U32>, length: Nat) -> Maybe<&2,S.State>:
190  sized(length,Array.size(U32,a))