Waes (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Waes)

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

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

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

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

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

val to_matrix : 
  Ssralg.GRing.ComRing.sort ->
  ((((((((((((((Word.word * Word.word) * Word.word) * Word.word) * Word.word)
            * Word.word)
           * Word.word)
          * Word.word)
         * Word.word)
        * Word.word)
       * Word.word)
      * Word.word)
     * Word.word)
    * Word.word)
   * Word.word)
  * Word.word

val to_state : 
  (((((((((((((((Ssralg.GRing.ComRing.sort * Ssralg.GRing.ComRing.sort)
                * Ssralg.GRing.ComRing.sort)
               * Ssralg.GRing.ComRing.sort)
              * Ssralg.GRing.ComRing.sort)
             * Ssralg.GRing.ComRing.sort)
            * Ssralg.GRing.ComRing.sort)
           * Ssralg.GRing.ComRing.sort)
          * Ssralg.GRing.ComRing.sort)
         * Ssralg.GRing.ComRing.sort)
        * Ssralg.GRing.ComRing.sort)
       * Ssralg.GRing.ComRing.sort)
      * Ssralg.GRing.ComRing.sort)
     * Ssralg.GRing.ComRing.sort)
    * Ssralg.GRing.ComRing.sort)
   * Ssralg.GRing.ComRing.sort) ->
  Ssralg.GRing.ComRing.sort

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

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

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

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

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

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

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

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

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

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

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