module Data.SHA256Constants import Data.SHA256 import Model.Config -- Part of `sha256RoundConstants`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def sha256RoundConstantsPart1 = (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 36) (byte 6) (byte 153) (byte 214)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 133) (byte 53) (byte 14) (byte 244)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 112) (byte 160) (byte 106) (byte 16)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 22) (byte 193) (byte 164) (byte 25)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 8) (byte 108) (byte 55) (byte 30)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 76) (byte 119) (byte 72) (byte 39)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 181) (byte 188) (byte 176) (byte 52)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 179) (byte 12) (byte 28) (byte 57)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 74) (byte 170) (byte 216) (byte 78)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 79) (byte 202) (byte 156) (byte 91)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 243) (byte 111) (byte 46) (byte 104)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 238) (byte 130) (byte 143) (byte 116)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 111) (byte 99) (byte 165) (byte 120)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 20) (byte 120) (byte 200) (byte 132)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 8) (byte 2) (byte 199) (byte 140)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 250) (byte 255) (byte 190) (byte 144)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 235) (byte 108) (byte 80) (byte 164)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 247) (byte 163) (byte 249) (byte 190)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 242) (byte 120) (byte 113) (byte 198)) (constructor SHA256Schedule SHA256ScheduleEnd)))))))))))))))))))) -- Part of `sha256RoundConstants`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def sha256RoundConstantsPart2 = (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 200) (byte 39) (byte 3) (byte 176)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 199) (byte 127) (byte 89) (byte 191)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 243) (byte 11) (byte 224) (byte 198)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 71) (byte 145) (byte 167) (byte 213)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 81) (byte 99) (byte 202) (byte 6)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 103) (byte 41) (byte 41) (byte 20)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 133) (byte 10) (byte 183) (byte 39)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 56) (byte 33) (byte 27) (byte 46)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 252) (byte 109) (byte 44) (byte 77)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 19) (byte 13) (byte 56) (byte 83)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 84) (byte 115) (byte 10) (byte 101)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 187) (byte 10) (byte 106) (byte 118)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 46) (byte 201) (byte 194) (byte 129)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 133) (byte 44) (byte 114) (byte 146)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 161) (byte 232) (byte 191) (byte 162)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 75) (byte 102) (byte 26) (byte 168)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 112) (byte 139) (byte 75) (byte 194)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 163) (byte 81) (byte 108) (byte 199)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 25) (byte 232) (byte 146) (byte 209)) sha256RoundConstantsPart1))))))))))))))))))) -- Part of `sha256RoundConstants`, lifted out to keep it inside the §28.3 size and -- nesting limits; the parameters are the locals it still needs. def sha256RoundConstantsPart3 = (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 254) (byte 177) (byte 222) (byte 128)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 167) (byte 6) (byte 220) (byte 155)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 116) (byte 241) (byte 155) (byte 193)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 193) (byte 105) (byte 155) (byte 228)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 134) (byte 71) (byte 190) (byte 239)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 198) (byte 157) (byte 193) (byte 15)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 204) (byte 161) (byte 12) (byte 36)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 111) (byte 44) (byte 233) (byte 45)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 170) (byte 132) (byte 116) (byte 74)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 220) (byte 169) (byte 176) (byte 92)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 218) (byte 136) (byte 249) (byte 118)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 82) (byte 81) (byte 62) (byte 152)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 109) (byte 198) (byte 49) (byte 168)) sha256RoundConstantsPart2))))))))))))) def sha256RoundConstants = (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 152) (byte 47) (byte 138) (byte 66)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 145) (byte 68) (byte 55) (byte 113)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 207) (byte 251) (byte 192) (byte 181)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 165) (byte 219) (byte 181) (byte 233)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 91) (byte 194) (byte 86) (byte 57)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 241) (byte 17) (byte 241) (byte 89)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 164) (byte 130) (byte 63) (byte 146)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 213) (byte 94) (byte 28) (byte 171)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 152) (byte 170) (byte 7) (byte 216)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 1) (byte 91) (byte 131) (byte 18)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 190) (byte 133) (byte 49) (byte 36)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 195) (byte 125) (byte 12) (byte 85)) (constructor SHA256Schedule SHA256ScheduleNext (constructor ModelWord32 ModelWord32Value (byte 116) (byte 93) (byte 190) (byte 114)) sha256RoundConstantsPart3))))))))))))) def sha256RoundConstantCount = (byte-to-nat (byte 64))