def constants

mylsm-lsm-store@0.6.0.1 · src/hub_sha/sha256.bend:17

import Base

17# The core refinement theorem quantifies over every constant table.
18# Instantiate the verified core with the FIPS 180-4 constants.
19def constants() -> List<&2, U32>:
20  [1116352408, 1899447441, 3049323471, 3921009573,
21   961987163, 1508970993, 2453635748, 2870763221,
22   3624381080, 310598401, 607225278, 1426881987,
23   1925078388, 2162078206, 2614888103, 3248222580,
24   3835390401, 4022224774, 264347078, 604807628,
25   770255983, 1249150122, 1555081692, 1996064986,
26   2554220882, 2821834349, 2952996808, 3210313671,
27   3336571891, 3584528711, 113926993, 338241895,
28   666307205, 773529912, 1294757372, 1396182291,
29   1695183700, 1986661051, 2177026350, 2456956037,
30   2730485921, 2820302411, 3259730800, 3345764771,
31   3516065817, 3600352804, 4094571909, 275423344,
32   430227734, 506948616, 659060556, 883997877,
33   958139571, 1322822218, 1537002063, 1747873779,
34   1955562222, 2024104815, 2227730452, 2361852424,
35   2428436474, 2756734187, 3204031479, 3329325298]