Sha256 (p.jasmin.2026.03.0.doc.jasmin.jasmin.Jasmin.Sha256)

val ch : Word0.word -> Word0.word -> Word0.word -> Word0.word

val maj : Word0.word -> Word0.word -> Word0.word -> Word0.word

val _UU03a3__UU2080_ : Word0.word -> Word0.word

val _UU03a3__UU2081_ : Word0.word -> Word0.word

val _UU03c3__UU2080_ : Word0.word -> Word0.word

val _UU03c3__UU2081_ : Word0.word -> Word0.word

val sha256msg1 : Word0.word -> Word0.word -> Word0.word

val sha256msg2 : Word0.word -> Word0.word -> Word0.word

val sha256rnds2 : Word0.word -> Word0.word -> Word0.word -> Word0.word