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

val ch : 
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val maj : 
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val _UU03a3__UU2080_ : Ssralg.GRing.ComRing.sort -> Ssralg.GRing.ComRing.sort

val _UU03a3__UU2081_ : Ssralg.GRing.ComRing.sort -> Ssralg.GRing.ComRing.sort

val _UU03c3__UU2080_ : Ssralg.GRing.ComRing.sort -> Ssralg.GRing.ComRing.sort

val _UU03c3__UU2081_ : Ssralg.GRing.ComRing.sort -> Ssralg.GRing.ComRing.sort

val sha256msg1 : 
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val sha256msg2 : 
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort

val sha256rnds2 : 
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort ->
  Ssralg.GRing.ComRing.sort