1	# SHA-1 (FIPS 180-4, Secure Hash Standard, 2015, sections 4.1.1, 4.2.1,
2	# 5.1.1, 5.3.1 and 6.1): a 160-bit digest of 64-byte blocks, eighty steps
3	# over a message schedule of eighty words (unrolled by gen/rounds.py).
4	# Big-endian words; the length in bits is padded in big-endian. SHA-1 is
5	# broken for collisions (SHAttered, 2017): it is here for HMAC-SHA-1,
6	# PBKDF2-HMAC-SHA-1 and the formats that require it.
7	#
8	# The hash, as the crypto package's hash interface takes it:
9	#   ~Hs.HsMdState<Hs.HsW5>, ~64n, ~20n, ~HsSha1.init(), ~HsSha1.update,
10	#   ~HsSha1.final, ~HsSha1.digest
11	import Base
12	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
13	import ./hashes.bend as Hs
14	
15	# the functions of section 4.1.1: Ch (steps 0 to 19), Parity (20 to 39 and
16	# 60 to 79), Maj (40 to 59)
17	def hs.sha1.ch(+x: U32, y: U32, z: U32) -> U32:
18	  U32.xor(U32.and(x, y), U32.and(U32.not(x), z))
19	
20	def hs.sha1.parity(x: U32, y: U32, z: U32) -> U32:
21	  U32.xor(U32.xor(x, y), z)
22	
23	def hs.sha1.maj(+x: U32, +y: U32, +z: U32) -> U32:
24	  U32.xor(U32.xor(U32.and(x, y), U32.and(x, z)), U32.and(y, z))
25	
26	# BEGIN GENERATED by gen/rounds.py: sha1
27	def hs.sha1.rounds(x: Hs.HsW16, cv: Hs.HsW5) -> Hs.HsW5:
28	  match x cv:
29	    case Hs.HsW16{+x0, +x1, +x2, +x3, +x4, +x5, +x6, +x7, +x8, +x9, +x10, +x11, +x12, +x13, +x14, +x15} Hs.HsW5{+a0, +b0, +c0, +d0, +e0}:
30	      # steps 0 to 19
31	      +v1 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(a0, 5n), hs.sha1.ch(b0, c0, d0)), e0), 1518500249), x0)
32	      +v2 = Hs.hs.rotl(b0, 30n)
33	      +v3 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v1, 5n), hs.sha1.ch(a0, v2, c0)), d0), 1518500249), x1)
34	      +v4 = Hs.hs.rotl(a0, 30n)
35	      +v5 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v3, 5n), hs.sha1.ch(v1, v4, v2)), c0), 1518500249), x2)
36	      +v6 = Hs.hs.rotl(v1, 30n)
37	      +v7 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v5, 5n), hs.sha1.ch(v3, v6, v4)), v2), 1518500249), x3)
38	      +v8 = Hs.hs.rotl(v3, 30n)
39	      +v9 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v7, 5n), hs.sha1.ch(v5, v8, v6)), v4), 1518500249), x4)
40	      +v10 = Hs.hs.rotl(v5, 30n)
41	      +v11 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v9, 5n), hs.sha1.ch(v7, v10, v8)), v6), 1518500249), x5)
42	      +v12 = Hs.hs.rotl(v7, 30n)
43	      +v13 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v11, 5n), hs.sha1.ch(v9, v12, v10)), v8), 1518500249), x6)
44	      +v14 = Hs.hs.rotl(v9, 30n)
45	      +v15 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v13, 5n), hs.sha1.ch(v11, v14, v12)), v10), 1518500249), x7)
46	      +v16 = Hs.hs.rotl(v11, 30n)
47	      +v17 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v15, 5n), hs.sha1.ch(v13, v16, v14)), v12), 1518500249), x8)
48	      +v18 = Hs.hs.rotl(v13, 30n)
49	      +v19 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v17, 5n), hs.sha1.ch(v15, v18, v16)), v14), 1518500249), x9)
50	      +v20 = Hs.hs.rotl(v15, 30n)
51	      +v21 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v19, 5n), hs.sha1.ch(v17, v20, v18)), v16), 1518500249), x10)
52	      +v22 = Hs.hs.rotl(v17, 30n)
53	      +v23 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v21, 5n), hs.sha1.ch(v19, v22, v20)), v18), 1518500249), x11)
54	      +v24 = Hs.hs.rotl(v19, 30n)
55	      +v25 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v23, 5n), hs.sha1.ch(v21, v24, v22)), v20), 1518500249), x12)
56	      +v26 = Hs.hs.rotl(v21, 30n)
57	      +v27 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v25, 5n), hs.sha1.ch(v23, v26, v24)), v22), 1518500249), x13)
58	      +v28 = Hs.hs.rotl(v23, 30n)
59	      +v29 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v27, 5n), hs.sha1.ch(v25, v28, v26)), v24), 1518500249), x14)
60	      +v30 = Hs.hs.rotl(v25, 30n)
61	      +v31 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v29, 5n), hs.sha1.ch(v27, v30, v28)), v26), 1518500249), x15)
62	      +v32 = Hs.hs.rotl(v27, 30n)
63	      +w16 = Hs.hs.rotl(U32.xor(U32.xor(x13, x8), U32.xor(x2, x0)), 1n)
64	      +v33 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v31, 5n), hs.sha1.ch(v29, v32, v30)), v28), 1518500249), w16)
65	      +v34 = Hs.hs.rotl(v29, 30n)
66	      +w17 = Hs.hs.rotl(U32.xor(U32.xor(x14, x9), U32.xor(x3, x1)), 1n)
67	      +v35 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v33, 5n), hs.sha1.ch(v31, v34, v32)), v30), 1518500249), w17)
68	      +v36 = Hs.hs.rotl(v31, 30n)
69	      +w18 = Hs.hs.rotl(U32.xor(U32.xor(x15, x10), U32.xor(x4, x2)), 1n)
70	      +v37 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v35, 5n), hs.sha1.ch(v33, v36, v34)), v32), 1518500249), w18)
71	      +v38 = Hs.hs.rotl(v33, 30n)
72	      +w19 = Hs.hs.rotl(U32.xor(U32.xor(w16, x11), U32.xor(x5, x3)), 1n)
73	      +v39 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v37, 5n), hs.sha1.ch(v35, v38, v36)), v34), 1518500249), w19)
74	      +v40 = Hs.hs.rotl(v35, 30n)
75	      # steps 20 to 39
76	      +w20 = Hs.hs.rotl(U32.xor(U32.xor(w17, x12), U32.xor(x6, x4)), 1n)
77	      +v41 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v39, 5n), hs.sha1.parity(v37, v40, v38)), v36), 1859775393), w20)
78	      +v42 = Hs.hs.rotl(v37, 30n)
79	      +w21 = Hs.hs.rotl(U32.xor(U32.xor(w18, x13), U32.xor(x7, x5)), 1n)
80	      +v43 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v41, 5n), hs.sha1.parity(v39, v42, v40)), v38), 1859775393), w21)
81	      +v44 = Hs.hs.rotl(v39, 30n)
82	      +w22 = Hs.hs.rotl(U32.xor(U32.xor(w19, x14), U32.xor(x8, x6)), 1n)
83	      +v45 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v43, 5n), hs.sha1.parity(v41, v44, v42)), v40), 1859775393), w22)
84	      +v46 = Hs.hs.rotl(v41, 30n)
85	      +w23 = Hs.hs.rotl(U32.xor(U32.xor(w20, x15), U32.xor(x9, x7)), 1n)
86	      +v47 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v45, 5n), hs.sha1.parity(v43, v46, v44)), v42), 1859775393), w23)
87	      +v48 = Hs.hs.rotl(v43, 30n)
88	      +w24 = Hs.hs.rotl(U32.xor(U32.xor(w21, w16), U32.xor(x10, x8)), 1n)
89	      +v49 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v47, 5n), hs.sha1.parity(v45, v48, v46)), v44), 1859775393), w24)
90	      +v50 = Hs.hs.rotl(v45, 30n)
91	      +w25 = Hs.hs.rotl(U32.xor(U32.xor(w22, w17), U32.xor(x11, x9)), 1n)
92	      +v51 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v49, 5n), hs.sha1.parity(v47, v50, v48)), v46), 1859775393), w25)
93	      +v52 = Hs.hs.rotl(v47, 30n)
94	      +w26 = Hs.hs.rotl(U32.xor(U32.xor(w23, w18), U32.xor(x12, x10)), 1n)
95	      +v53 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v51, 5n), hs.sha1.parity(v49, v52, v50)), v48), 1859775393), w26)
96	      +v54 = Hs.hs.rotl(v49, 30n)
97	      +w27 = Hs.hs.rotl(U32.xor(U32.xor(w24, w19), U32.xor(x13, x11)), 1n)
98	      +v55 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v53, 5n), hs.sha1.parity(v51, v54, v52)), v50), 1859775393), w27)
99	      +v56 = Hs.hs.rotl(v51, 30n)
100	      +w28 = Hs.hs.rotl(U32.xor(U32.xor(w25, w20), U32.xor(x14, x12)), 1n)
101	      +v57 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v55, 5n), hs.sha1.parity(v53, v56, v54)), v52), 1859775393), w28)
102	      +v58 = Hs.hs.rotl(v53, 30n)
103	      +w29 = Hs.hs.rotl(U32.xor(U32.xor(w26, w21), U32.xor(x15, x13)), 1n)
104	      +v59 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v57, 5n), hs.sha1.parity(v55, v58, v56)), v54), 1859775393), w29)
105	      +v60 = Hs.hs.rotl(v55, 30n)
106	      +w30 = Hs.hs.rotl(U32.xor(U32.xor(w27, w22), U32.xor(w16, x14)), 1n)
107	      +v61 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v59, 5n), hs.sha1.parity(v57, v60, v58)), v56), 1859775393), w30)
108	      +v62 = Hs.hs.rotl(v57, 30n)
109	      +w31 = Hs.hs.rotl(U32.xor(U32.xor(w28, w23), U32.xor(w17, x15)), 1n)
110	      +v63 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v61, 5n), hs.sha1.parity(v59, v62, v60)), v58), 1859775393), w31)
111	      +v64 = Hs.hs.rotl(v59, 30n)
112	      +w32 = Hs.hs.rotl(U32.xor(U32.xor(w29, w24), U32.xor(w18, w16)), 1n)
113	      +v65 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v63, 5n), hs.sha1.parity(v61, v64, v62)), v60), 1859775393), w32)
114	      +v66 = Hs.hs.rotl(v61, 30n)
115	      +w33 = Hs.hs.rotl(U32.xor(U32.xor(w30, w25), U32.xor(w19, w17)), 1n)
116	      +v67 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v65, 5n), hs.sha1.parity(v63, v66, v64)), v62), 1859775393), w33)
117	      +v68 = Hs.hs.rotl(v63, 30n)
118	      +w34 = Hs.hs.rotl(U32.xor(U32.xor(w31, w26), U32.xor(w20, w18)), 1n)
119	      +v69 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v67, 5n), hs.sha1.parity(v65, v68, v66)), v64), 1859775393), w34)
120	      +v70 = Hs.hs.rotl(v65, 30n)
121	      +w35 = Hs.hs.rotl(U32.xor(U32.xor(w32, w27), U32.xor(w21, w19)), 1n)
122	      +v71 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v69, 5n), hs.sha1.parity(v67, v70, v68)), v66), 1859775393), w35)
123	      +v72 = Hs.hs.rotl(v67, 30n)
124	      +w36 = Hs.hs.rotl(U32.xor(U32.xor(w33, w28), U32.xor(w22, w20)), 1n)
125	      +v73 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v71, 5n), hs.sha1.parity(v69, v72, v70)), v68), 1859775393), w36)
126	      +v74 = Hs.hs.rotl(v69, 30n)
127	      +w37 = Hs.hs.rotl(U32.xor(U32.xor(w34, w29), U32.xor(w23, w21)), 1n)
128	      +v75 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v73, 5n), hs.sha1.parity(v71, v74, v72)), v70), 1859775393), w37)
129	      +v76 = Hs.hs.rotl(v71, 30n)
130	      +w38 = Hs.hs.rotl(U32.xor(U32.xor(w35, w30), U32.xor(w24, w22)), 1n)
131	      +v77 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v75, 5n), hs.sha1.parity(v73, v76, v74)), v72), 1859775393), w38)
132	      +v78 = Hs.hs.rotl(v73, 30n)
133	      +w39 = Hs.hs.rotl(U32.xor(U32.xor(w36, w31), U32.xor(w25, w23)), 1n)
134	      +v79 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v77, 5n), hs.sha1.parity(v75, v78, v76)), v74), 1859775393), w39)
135	      +v80 = Hs.hs.rotl(v75, 30n)
136	      # steps 40 to 59
137	      +w40 = Hs.hs.rotl(U32.xor(U32.xor(w37, w32), U32.xor(w26, w24)), 1n)
138	      +v81 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v79, 5n), hs.sha1.maj(v77, v80, v78)), v76), 2400959708), w40)
139	      +v82 = Hs.hs.rotl(v77, 30n)
140	      +w41 = Hs.hs.rotl(U32.xor(U32.xor(w38, w33), U32.xor(w27, w25)), 1n)
141	      +v83 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v81, 5n), hs.sha1.maj(v79, v82, v80)), v78), 2400959708), w41)
142	      +v84 = Hs.hs.rotl(v79, 30n)
143	      +w42 = Hs.hs.rotl(U32.xor(U32.xor(w39, w34), U32.xor(w28, w26)), 1n)
144	      +v85 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v83, 5n), hs.sha1.maj(v81, v84, v82)), v80), 2400959708), w42)
145	      +v86 = Hs.hs.rotl(v81, 30n)
146	      +w43 = Hs.hs.rotl(U32.xor(U32.xor(w40, w35), U32.xor(w29, w27)), 1n)
147	      +v87 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v85, 5n), hs.sha1.maj(v83, v86, v84)), v82), 2400959708), w43)
148	      +v88 = Hs.hs.rotl(v83, 30n)
149	      +w44 = Hs.hs.rotl(U32.xor(U32.xor(w41, w36), U32.xor(w30, w28)), 1n)
150	      +v89 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v87, 5n), hs.sha1.maj(v85, v88, v86)), v84), 2400959708), w44)
151	      +v90 = Hs.hs.rotl(v85, 30n)
152	      +w45 = Hs.hs.rotl(U32.xor(U32.xor(w42, w37), U32.xor(w31, w29)), 1n)
153	      +v91 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v89, 5n), hs.sha1.maj(v87, v90, v88)), v86), 2400959708), w45)
154	      +v92 = Hs.hs.rotl(v87, 30n)
155	      +w46 = Hs.hs.rotl(U32.xor(U32.xor(w43, w38), U32.xor(w32, w30)), 1n)
156	      +v93 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v91, 5n), hs.sha1.maj(v89, v92, v90)), v88), 2400959708), w46)
157	      +v94 = Hs.hs.rotl(v89, 30n)
158	      +w47 = Hs.hs.rotl(U32.xor(U32.xor(w44, w39), U32.xor(w33, w31)), 1n)
159	      +v95 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v93, 5n), hs.sha1.maj(v91, v94, v92)), v90), 2400959708), w47)
160	      +v96 = Hs.hs.rotl(v91, 30n)
161	      +w48 = Hs.hs.rotl(U32.xor(U32.xor(w45, w40), U32.xor(w34, w32)), 1n)
162	      +v97 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v95, 5n), hs.sha1.maj(v93, v96, v94)), v92), 2400959708), w48)
163	      +v98 = Hs.hs.rotl(v93, 30n)
164	      +w49 = Hs.hs.rotl(U32.xor(U32.xor(w46, w41), U32.xor(w35, w33)), 1n)
165	      +v99 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v97, 5n), hs.sha1.maj(v95, v98, v96)), v94), 2400959708), w49)
166	      +v100 = Hs.hs.rotl(v95, 30n)
167	      +w50 = Hs.hs.rotl(U32.xor(U32.xor(w47, w42), U32.xor(w36, w34)), 1n)
168	      +v101 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v99, 5n), hs.sha1.maj(v97, v100, v98)), v96), 2400959708), w50)
169	      +v102 = Hs.hs.rotl(v97, 30n)
170	      +w51 = Hs.hs.rotl(U32.xor(U32.xor(w48, w43), U32.xor(w37, w35)), 1n)
171	      +v103 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v101, 5n), hs.sha1.maj(v99, v102, v100)), v98), 2400959708), w51)
172	      +v104 = Hs.hs.rotl(v99, 30n)
173	      +w52 = Hs.hs.rotl(U32.xor(U32.xor(w49, w44), U32.xor(w38, w36)), 1n)
174	      +v105 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v103, 5n), hs.sha1.maj(v101, v104, v102)), v100), 2400959708), w52)
175	      +v106 = Hs.hs.rotl(v101, 30n)
176	      +w53 = Hs.hs.rotl(U32.xor(U32.xor(w50, w45), U32.xor(w39, w37)), 1n)
177	      +v107 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v105, 5n), hs.sha1.maj(v103, v106, v104)), v102), 2400959708), w53)
178	      +v108 = Hs.hs.rotl(v103, 30n)
179	      +w54 = Hs.hs.rotl(U32.xor(U32.xor(w51, w46), U32.xor(w40, w38)), 1n)
180	      +v109 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v107, 5n), hs.sha1.maj(v105, v108, v106)), v104), 2400959708), w54)
181	      +v110 = Hs.hs.rotl(v105, 30n)
182	      +w55 = Hs.hs.rotl(U32.xor(U32.xor(w52, w47), U32.xor(w41, w39)), 1n)
183	      +v111 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v109, 5n), hs.sha1.maj(v107, v110, v108)), v106), 2400959708), w55)
184	      +v112 = Hs.hs.rotl(v107, 30n)
185	      +w56 = Hs.hs.rotl(U32.xor(U32.xor(w53, w48), U32.xor(w42, w40)), 1n)
186	      +v113 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v111, 5n), hs.sha1.maj(v109, v112, v110)), v108), 2400959708), w56)
187	      +v114 = Hs.hs.rotl(v109, 30n)
188	      +w57 = Hs.hs.rotl(U32.xor(U32.xor(w54, w49), U32.xor(w43, w41)), 1n)
189	      +v115 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v113, 5n), hs.sha1.maj(v111, v114, v112)), v110), 2400959708), w57)
190	      +v116 = Hs.hs.rotl(v111, 30n)
191	      +w58 = Hs.hs.rotl(U32.xor(U32.xor(w55, w50), U32.xor(w44, w42)), 1n)
192	      +v117 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v115, 5n), hs.sha1.maj(v113, v116, v114)), v112), 2400959708), w58)
193	      +v118 = Hs.hs.rotl(v113, 30n)
194	      +w59 = Hs.hs.rotl(U32.xor(U32.xor(w56, w51), U32.xor(w45, w43)), 1n)
195	      +v119 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v117, 5n), hs.sha1.maj(v115, v118, v116)), v114), 2400959708), w59)
196	      +v120 = Hs.hs.rotl(v115, 30n)
197	      # steps 60 to 79
198	      +w60 = Hs.hs.rotl(U32.xor(U32.xor(w57, w52), U32.xor(w46, w44)), 1n)
199	      +v121 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v119, 5n), hs.sha1.parity(v117, v120, v118)), v116), 3395469782), w60)
200	      +v122 = Hs.hs.rotl(v117, 30n)
201	      +w61 = Hs.hs.rotl(U32.xor(U32.xor(w58, w53), U32.xor(w47, w45)), 1n)
202	      +v123 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v121, 5n), hs.sha1.parity(v119, v122, v120)), v118), 3395469782), w61)
203	      +v124 = Hs.hs.rotl(v119, 30n)
204	      +w62 = Hs.hs.rotl(U32.xor(U32.xor(w59, w54), U32.xor(w48, w46)), 1n)
205	      +v125 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v123, 5n), hs.sha1.parity(v121, v124, v122)), v120), 3395469782), w62)
206	      +v126 = Hs.hs.rotl(v121, 30n)
207	      +w63 = Hs.hs.rotl(U32.xor(U32.xor(w60, w55), U32.xor(w49, w47)), 1n)
208	      +v127 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v125, 5n), hs.sha1.parity(v123, v126, v124)), v122), 3395469782), w63)
209	      +v128 = Hs.hs.rotl(v123, 30n)
210	      +w64 = Hs.hs.rotl(U32.xor(U32.xor(w61, w56), U32.xor(w50, w48)), 1n)
211	      +v129 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v127, 5n), hs.sha1.parity(v125, v128, v126)), v124), 3395469782), w64)
212	      +v130 = Hs.hs.rotl(v125, 30n)
213	      +w65 = Hs.hs.rotl(U32.xor(U32.xor(w62, w57), U32.xor(w51, w49)), 1n)
214	      +v131 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v129, 5n), hs.sha1.parity(v127, v130, v128)), v126), 3395469782), w65)
215	      +v132 = Hs.hs.rotl(v127, 30n)
216	      +w66 = Hs.hs.rotl(U32.xor(U32.xor(w63, w58), U32.xor(w52, w50)), 1n)
217	      +v133 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v131, 5n), hs.sha1.parity(v129, v132, v130)), v128), 3395469782), w66)
218	      +v134 = Hs.hs.rotl(v129, 30n)
219	      +w67 = Hs.hs.rotl(U32.xor(U32.xor(w64, w59), U32.xor(w53, w51)), 1n)
220	      +v135 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v133, 5n), hs.sha1.parity(v131, v134, v132)), v130), 3395469782), w67)
221	      +v136 = Hs.hs.rotl(v131, 30n)
222	      +w68 = Hs.hs.rotl(U32.xor(U32.xor(w65, w60), U32.xor(w54, w52)), 1n)
223	      +v137 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v135, 5n), hs.sha1.parity(v133, v136, v134)), v132), 3395469782), w68)
224	      +v138 = Hs.hs.rotl(v133, 30n)
225	      +w69 = Hs.hs.rotl(U32.xor(U32.xor(w66, w61), U32.xor(w55, w53)), 1n)
226	      +v139 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v137, 5n), hs.sha1.parity(v135, v138, v136)), v134), 3395469782), w69)
227	      +v140 = Hs.hs.rotl(v135, 30n)
228	      +w70 = Hs.hs.rotl(U32.xor(U32.xor(w67, w62), U32.xor(w56, w54)), 1n)
229	      +v141 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v139, 5n), hs.sha1.parity(v137, v140, v138)), v136), 3395469782), w70)
230	      +v142 = Hs.hs.rotl(v137, 30n)
231	      +w71 = Hs.hs.rotl(U32.xor(U32.xor(w68, w63), U32.xor(w57, w55)), 1n)
232	      +v143 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v141, 5n), hs.sha1.parity(v139, v142, v140)), v138), 3395469782), w71)
233	      +v144 = Hs.hs.rotl(v139, 30n)
234	      +w72 = Hs.hs.rotl(U32.xor(U32.xor(w69, w64), U32.xor(w58, w56)), 1n)
235	      +v145 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v143, 5n), hs.sha1.parity(v141, v144, v142)), v140), 3395469782), w72)
236	      +v146 = Hs.hs.rotl(v141, 30n)
237	      +w73 = Hs.hs.rotl(U32.xor(U32.xor(w70, w65), U32.xor(w59, w57)), 1n)
238	      +v147 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v145, 5n), hs.sha1.parity(v143, v146, v144)), v142), 3395469782), w73)
239	      +v148 = Hs.hs.rotl(v143, 30n)
240	      +w74 = Hs.hs.rotl(U32.xor(U32.xor(w71, w66), U32.xor(w60, w58)), 1n)
241	      +v149 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v147, 5n), hs.sha1.parity(v145, v148, v146)), v144), 3395469782), w74)
242	      +v150 = Hs.hs.rotl(v145, 30n)
243	      +w75 = Hs.hs.rotl(U32.xor(U32.xor(w72, w67), U32.xor(w61, w59)), 1n)
244	      +v151 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v149, 5n), hs.sha1.parity(v147, v150, v148)), v146), 3395469782), w75)
245	      +v152 = Hs.hs.rotl(v147, 30n)
246	      +w76 = Hs.hs.rotl(U32.xor(U32.xor(w73, w68), U32.xor(w62, w60)), 1n)
247	      +v153 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v151, 5n), hs.sha1.parity(v149, v152, v150)), v148), 3395469782), w76)
248	      +v154 = Hs.hs.rotl(v149, 30n)
249	      +w77 = Hs.hs.rotl(U32.xor(U32.xor(w74, w69), U32.xor(w63, w61)), 1n)
250	      +v155 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v153, 5n), hs.sha1.parity(v151, v154, v152)), v150), 3395469782), w77)
251	      +v156 = Hs.hs.rotl(v151, 30n)
252	      +w78 = Hs.hs.rotl(U32.xor(U32.xor(w75, w70), U32.xor(w64, w62)), 1n)
253	      +v157 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v155, 5n), hs.sha1.parity(v153, v156, v154)), v152), 3395469782), w78)
254	      +v158 = Hs.hs.rotl(v153, 30n)
255	      +w79 = Hs.hs.rotl(U32.xor(U32.xor(w76, w71), U32.xor(w65, w63)), 1n)
256	      +v159 = U32.add(U32.add(U32.add(U32.add(Hs.hs.rotl(v157, 5n), hs.sha1.parity(v155, v158, v156)), v154), 3395469782), w79)
257	      +v160 = Hs.hs.rotl(v155, 30n)
258	      Hs.HsW5{U32.add(a0, v159), U32.add(b0, v157), U32.add(c0, v160), U32.add(d0, v158), U32.add(e0, v156)}
259	# END GENERATED: sha1
260	
261	# The chaining value before any block (section 5.3.1)
262	def HsSha1.iv() -> Hs.HsW5:
263	  Hs.HsW5{1732584193, 4023233417, 2562383102, 271733878, 3285377520}
264	
265	# One 64-byte block (a list of another length is read as zero words: the
266	# engine passes only whole blocks)
267	def HsSha1.compress(cv: Hs.HsW5, blk: List<&2, U32>) -> Hs.HsW5:
268	  hs.sha1.rounds(Hs.hs.block.be(blk), cv)
269	
270	def HsSha1.init() -> Hs.HsMdState<Hs.HsW5>:
271	  Hs.HsMd.start(~Hs.HsW5, HsSha1.iv())
272	
273	def HsSha1.update(s: Hs.HsMdState<Hs.HsW5>, o: B.Octets) -> Hs.HsMdState<Hs.HsW5>:
274	  Hs.HsMd.update(~Hs.HsW5, ~HsSha1.compress, ~63, s, o)
275	
276	# the digest of the bytes so far: the padding of section 5.1.1, then the
277	# five words big-endian
278	def HsSha1.final(s: Hs.HsMdState<Hs.HsW5>) -> B.Octets:
279	  Hs.HsMd.final_md(~Hs.HsW5, ~HsSha1.compress, ~63, ~Hs.hs.len.be, ~Hs.HsW5.be, s)
280	
281	# The digest in one call
282	def HsSha1.digest(o: B.Octets) -> B.Octets:
283	  HsSha1.final(HsSha1.update(HsSha1.init(), o))