This translation extends 'word_prelude'. Certificate theorem for Sbox: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "Sbox") ((WORD --> WORD) Sbox) Certificate theorem for InvSbox: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "InvSbox") ((WORD --> WORD) InvSbox) Certificate theorem for genSubBytes: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "genSubBytes") (((WORD --> WORD) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) genSubBytes) Certificate theorem for SubBytes: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "SubBytes") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) SubBytes) Certificate theorem for ShiftRows: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "ShiftRows") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) ShiftRows) Certificate theorem for XOR_BLOCK: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "XOR_BLOCK") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) XOR_BLOCK) Certificate theorem for AddRoundKey: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "AddRoundKey") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) AddRoundKey) Certificate theorem for genMixColumns: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "genMixColumns") (((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) genMixColumns) Certificate theorem for xtime: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "xtime") ((WORD --> WORD) xtime) Certificate theorem for **: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "**") ((WORD --> WORD --> WORD) $** ) Certificate theorem for MultCol: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "MultCol") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) MultCol) Certificate theorem for MixColumns: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "MixColumns") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) MixColumns) Certificate theorem for ROTKEYS: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "ROTKEYS") ((PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))) --> PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))))))))))) ROTKEYS) Certificate theorem for RoundTuple: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "RoundTuple") ((PAIR_TYPE NUM (PAIR_TYPE (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))) --> PAIR_TYPE NUM (PAIR_TYPE (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))) RoundTuple) Certificate theorem for Round: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "Round") ((NUM --> PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) Round) Certificate theorem for from_state: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "from_state") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) from_state) Certificate theorem for to_state: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "to_state") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) to_state) Certificate theorem for InvMultCol: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "InvMultCol") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))) InvMultCol) Certificate theorem for InvMixColumns: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "InvMixColumns") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) InvMixColumns) Certificate theorem for InvShiftRows: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "InvShiftRows") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) InvShiftRows) Certificate theorem for InvSubBytes: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "InvSubBytes") ((PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) InvSubBytes) Certificate theorem for InvRoundTuple: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "InvRoundTuple") ((PAIR_TYPE NUM (PAIR_TYPE (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))) --> PAIR_TYPE NUM (PAIR_TYPE (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))))) InvRoundTuple) Certificate theorem for InvRound: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "InvRound") ((NUM --> PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) InvRound) Certificate theorem for AES_FWD: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "AES_FWD") ((PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) AES_FWD) Certificate theorem for AES_BWD: |- DeclAssum example_aes_decls env ⇒ Eval env (Var "AES_BWD") ((PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD)))))))))))))) --> PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD (PAIR_TYPE WORD WORD))))))))))))))) AES_BWD) Definition of declaration list: |- example_aes_decls = [Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])]; Dtype [(["a"],"list", [("Cons",[Tvar "a"; Tapp [Tvar "a"] "list"]); ("Nil",[])])]; Dlet (Pvar "HD") (Fun "x1" (Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")])); Dlet (Pvar "TL") (Fun "x1" (Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v1")])); Dletrec [("APPEND","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "APPEND") (Var "v1")) (Var "v4")])]))]; Dletrec [("REV","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Cons" [Var "v2"; Var "v4"]))]))]; Dlet (Pvar "REVERSE") (Fun "v1" (App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Nil" []))); Dlet (Pvar "FST") (Fun "v3" (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v2")])); Dlet (Pvar "SND") (Fun "v3" (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"],Var "v1")])); Dlet (Pvar "CURRY") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (Var "v1") (Con "Pair" [Var "v2"; Var "v3"]))))); Dlet (Pvar "UNCURRY") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "v1") (App Opapp (Var "FST") (Var "v2"))) (App Opapp (Var "SND") (Var "v2"))))); Dlet (Pvar "o") (Fun "v2" (Fun "v3" (Fun "v1" (App Opapp (Var "v2") (App Opapp (Var "v3") (Var "v1")))))); Dlet (Pvar "I") (Fun "v1" (Var "v1")); Dlet (Pvar "C") (Fun "v3" (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v3") (Var "v1")) (Var "v2"))))); Dlet (Pvar "K") (Fun "v2" (Fun "v1" (Var "v2"))); Dlet (Pvar "S") (Fun "v3" (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v3") (Var "v1")) (App Opapp (Var "v2") (Var "v1")))))); Dlet (Pvar "UPDATE") (Fun "v3" (Fun "v4" (Fun "v2" (Fun "v1" (If (App Equality (Var "v3") (Var "v1")) (Var "v4") (App Opapp (Var "v2") (Var "v1"))))))); Dlet (Pvar "W") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "v2") (Var "v1")) (Var "v1")))); Dtype [([],"one",[("One",[])])]; Dtype [(["a"],"option",[("Some",[Tvar "a"]); ("None",[])])]; Dlet (Pvar "THE") (Fun "x1" (Mat (Var "x1") [(Pcon "None" [],Raise Bind_error); (Pcon "Some" [Pvar "v1"],Var "v1")])); Dlet (Pvar "IS_NONE") (Fun "v2" (Mat (Var "v2") [(Pcon "None" [],Val (Lit (Bool T))); (Pcon "Some" [Pvar "v1"],Val (Lit (Bool F)))])); Dlet (Pvar "IS_SOME") (Fun "v2" (Mat (Var "v2") [(Pcon "None" [],Val (Lit (Bool F))); (Pcon "Some" [Pvar "v1"],Val (Lit (Bool T)))])); Dlet (Pvar "OPTION_MAP") (Fun "v2" (Fun "v3" (Mat (Var "v3") [(Pcon "None" [],Con "None" []); (Pcon "Some" [Pvar "v1"], Con "Some" [App Opapp (Var "v2") (Var "v1")])]))); Dlet (Pvar "OPTION_MAP2") (Fun "v1" (Fun "v2" (Fun "v3" (If (Log And (App Opapp (Var "IS_SOME") (Var "v2")) (App Opapp (Var "IS_SOME") (Var "v3"))) (Con "Some" [App Opapp (App Opapp (Var "v1") (App Opapp (Var "THE") (Var "v2"))) (App Opapp (Var "THE") (Var "v3"))]) (Con "None" []))))); Dtype [(["a"; "b"],"sum",[("Inr",[Tvar "b"]); ("Inl",[Tvar "a"])])]; Dlet (Pvar "ISL") (Fun "v3" (Mat (Var "v3") [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool T))); (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool F)))])); Dlet (Pvar "ISR") (Fun "v3" (Mat (Var "v3") [(Pcon "Inl" [Pvar "v1"],Val (Lit (Bool F))); (Pcon "Inr" [Pvar "v2"],Val (Lit (Bool T)))])); Dlet (Pvar "OUTL") (Fun "x1" (Mat (Var "x1") [(Pcon "Inl" [Pvar "v1"],Var "v1"); (Pcon "Inr" [Pvar "v2"],Raise Bind_error)])); Dlet (Pvar "OUTR") (Fun "x1" (Mat (Var "x1") [(Pcon "Inl" [Pvar "v1"],Raise Bind_error); (Pcon "Inr" [Pvar "v2"],Var "v2")])); Dlet (Pvar "++") (Fun "v3" (Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Inl" [Pvar "v1"], Con "Inl" [App Opapp (Var "v3") (Var "v1")]); (Pcon "Inr" [Pvar "v2"], Con "Inr" [App Opapp (Var "v4") (Var "v2")])])))); Dletrec [("LENGTH_AUX","v3", Fun "v4" (Mat (Var "v3") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1")) (App (Opn Plus) (Var "v4") (Val (Lit (IntLit 1)))))]))]; Dlet (Pvar "LENGTH") (Fun "v1" (App Opapp (App Opapp (Var "LENGTH_AUX") (Var "v1")) (Val (Lit (IntLit 0))))); Dletrec [("MAP","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [App Opapp (Var "v3") (Var "v2"); App Opapp (App Opapp (Var "MAP") (Var "v3")) (Var "v1")])]))]; Dletrec [("FILTER","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Opapp (Var "v3") (Var "v2")) (Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "FILTER") (Var "v3")) (Var "v1")]) (App Opapp (App Opapp (Var "FILTER") (Var "v3")) (Var "v1")))]))]; Dletrec [("FOLDR","v3", Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (App Opapp (Var "FOLDR") (Var "v3")) (Var "v4")) (Var "v1")))])))]; Dletrec [("FOLDL","v3", Fun "v4" (Fun "v5" (Mat (Var "v5") [(Pcon "Nil" [],Var "v4"); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (App Opapp (Var "FOLDL") (Var "v3")) (App Opapp (App Opapp (Var "v3") (Var "v4")) (Var "v2"))) (Var "v1"))])))]; Dletrec [("SUM","v3", Mat (Var "v3") [(Pcon "Nil" [],Val (Lit (IntLit 0))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App (Opn Plus) (Var "v2") (App Opapp (Var "SUM") (Var "v1")))])]; Dletrec [("UNZIP","v3", Mat (Var "v3") [(Pcon "Nil" [],Con "Pair" [Con "Nil" []; Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Pair" [Con "Cons" [App Opapp (Var "FST") (Var "v2"); App Opapp (Var "FST") (App Opapp (Var "UNZIP") (Var "v1"))]; Con "Cons" [App Opapp (Var "SND") (Var "v2"); App Opapp (Var "SND") (App Opapp (Var "UNZIP") (Var "v1"))]])])]; Dletrec [("FLAT","v3", Mat (Var "v3") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "APPEND") (Var "v2")) (App Opapp (Var "FLAT") (Var "v1")))])]; Dletrec [("TAKE","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Con "Nil" []) (Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "TAKE") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (Var "v1")]))]))]; Dletrec [("DROP","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Con "Cons" [Var "v2"; Var "v1"]) (App Opapp (App Opapp (Var "DROP") (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (Var "v1")))]))]; Dletrec [("SNOC","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Con "Cons" [Var "v3"; Con "Nil" []]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Con "Cons" [Var "v2"; App Opapp (App Opapp (Var "SNOC") (Var "v3")) (Var "v1")])]))]; Dletrec [("EVERY","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "EVERY") (Var "v3")) (Var "v1")))]))]; Dletrec [("EXISTS","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log Or (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "EXISTS") (Var "v3")) (Var "v1")))]))]; Dletrec [("GENLIST","v1", Fun "v2" (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0)))) (Con "Nil" []) (App Opapp (App Opapp (Var "SNOC") (App Opapp (Var "v1") (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1)))))) (App Opapp (App Opapp (Var "GENLIST") (Var "v1")) (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1))))))))]; Dlet (Pvar "PAD_RIGHT") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (App Opapp (Var "APPEND") (Var "v3")) (App Opapp (App Opapp (Var "GENLIST") (App Opapp (Var "K") (Var "v1"))) (Let "k" (App (Opn Minus) (Var "v2") (App Opapp (Var "LENGTH") (Var "v3"))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))))); Dlet (Pvar "PAD_LEFT") (Fun "v1" (Fun "v2" (Fun "v3" (App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "GENLIST") (App Opapp (Var "K") (Var "v1"))) (Let "k" (App (Opn Minus) (Var "v2") (App Opapp (Var "LENGTH") (Var "v3"))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (Var "v3"))))); Dletrec [("MEM","v3", Fun "v4" (Mat (Var "v4") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log Or (App Equality (Var "v3") (Var "v2")) (App Opapp (App Opapp (Var "MEM") (Var "v3")) (Var "v1")))]))]; Dletrec [("ALL_DISTINCT","v3", Mat (Var "v3") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Equality (App Opapp (App Opapp (Var "MEM") (Var "v2")) (Var "v1")) (Val (Lit (Bool F)))) (App Opapp (Var "ALL_DISTINCT") (Var "v1")))])]; Dletrec [("isPREFIX","v5", Fun "v6" (Mat (Var "v5") [(Pcon "Nil" [],Val (Lit (Bool T))); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Mat (Var "v6") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Log And (App Equality (Var "v4") (Var "v2")) (App Opapp (App Opapp (Var "isPREFIX") (Var "v3")) (Var "v1")))])]))]; Dletrec [("FRONT","x1", Mat (Var "x1") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v1") (Con "Nil" [])) (Con "Nil" []) (Con "Cons" [Var "v2"; App Opapp (Var "FRONT") (Var "v1")]))])]; Dletrec [("ZIP","x1", Mat (Var "x1") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v8") [(Pcon "Nil" [], Mat (Var "v7") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Raise Bind_error)]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v7") [(Pcon "Nil" [],Raise Bind_error); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Con "Cons" [Con "Pair" [Var "v6"; Var "v4"]; App Opapp (Var "ZIP") (Con "Pair" [Var "v5"; Var "v3"])])])])])]; Dletrec [("EL","v1", Fun "v2" (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0)))) (App Opapp (Var "HD") (Var "v2")) (App Opapp (App Opapp (Var "EL") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (App Opapp (Var "TL") (Var "v2")))))]; Dletrec [("PART","v3", Fun "v4" (Fun "v5" (Fun "v6" (Mat (Var "v4") [(Pcon "Nil" [],Con "Pair" [Var "v5"; Var "v6"]); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], If (App Opapp (Var "v3") (Var "v2")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Con "Cons" [Var "v2"; Var "v5"])) (Var "v6")) (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v3")) (Var "v1")) (Var "v5")) (Con "Cons" [Var "v2"; Var "v6"])))]))))]; Dlet (Pvar "PARTITION") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (App Opapp (Var "PART") (Var "v1")) (Var "v2")) (Con "Nil" [])) (Con "Nil" [])))); Dletrec [("QSORT","v7", Fun "v8" (Mat (Var "v8") [(Pcon "Nil" [],Con "Nil" []); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Let "v3" (App Opapp (App Opapp (Var "PARTITION") (Fun "v4" (App Opapp (App Opapp (Var "v7") (Var "v4")) (Var "v6")))) (Var "v5")) (Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "APPEND") (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v2"))) (Con "Cons" [Var "v6"; Con "Nil" []]))) (App Opapp (App Opapp (Var "QSORT") (Var "v7")) (Var "v1")))]))]))]; Dletrec [("EXP_AUX","v2", Fun "v3" (Fun "v1" (If (App (Opb Leq) (Var "v3") (Val (Lit (IntLit 0)))) (Var "v1") (App Opapp (App Opapp (App Opapp (Var "EXP_AUX") (Var "v2")) (App (Opn Minus) (Var "v3") (Val (Lit (IntLit 1))))) (App (Opn Times) (Var "v2") (Var "v1"))))))]; Dlet (Pvar "EXP") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (App Opapp (Var "EXP_AUX") (Var "v1")) (Var "v2")) (Val (Lit (IntLit 1)))))); Dlet (Pvar "MIN") (Fun "v1" (Fun "v2" (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v1") (Var "v2")))); Dlet (Pvar "MAX") (Fun "v1" (Fun "v2" (If (App (Opb Lt) (Var "v1") (Var "v2")) (Var "v2") (Var "v1")))); Dlet (Pvar "EVEN") (Fun "v1" (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0))))); Dlet (Pvar "ODD") (Fun "v1" (App (Opb Lt) (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))))); Dletrec [("FUNPOW","v1", Fun "v2" (Fun "v3" (If (App (Opb Leq) (Var "v2") (Val (Lit (IntLit 0)))) (Var "v3") (App Opapp (App Opapp (App Opapp (Var "FUNPOW") (Var "v1")) (App (Opn Minus) (Var "v2") (Val (Lit (IntLit 1))))) (App Opapp (Var "v1") (Var "v3"))))))]; Dlet (Pvar "MOD_2EXP") (Fun "v2" (Fun "v1" (App (Opn Modulo) (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2"))))); Dlet (Pvar "DIV_2EXP") (Fun "v2" (Fun "v1" (App (Opn Divide) (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2"))))); Dlet (Pvar "PRE") (Fun "v1" (Let "k" (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))); Dlet (Pvar "ABS_DIFF") (Fun "v2" (Fun "v1" (If (App (Opb Lt) (Var "v2") (Var "v1")) (Let "k" (App (Opn Minus) (Var "v1") (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (Let "k" (App (Opn Minus) (Var "v2") (Var "v1")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))); Dlet (Pvar "DIV2") (Fun "v1" (App (Opn Divide) (Var "v1") (Val (Lit (IntLit 2))))); Dletrec [("string_lt","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Nil" [], Mat (Var "v8") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v2"; Pvar "v1"], Val (Lit (Bool T)))]); (Pcon "Cons" [Pvar "v6"; Pvar "v5"], Mat (Var "v8") [(Pcon "Nil" [],Val (Lit (Bool F))); (Pcon "Cons" [Pvar "v4"; Pvar "v3"], Log Or (App Opapp (Let "m" (Var "v6") (Fun "n" (App (Opb Lt) (Var "m") (Var "n")))) (Var "v4")) (Log And (App Equality (Var "v6") (Var "v4")) (App Opapp (App Opapp (Var "string_lt") (Var "v5")) (Var "v3"))))])]))]; Dlet (Pvar "string_le") (Fun "v1" (Fun "v2" (Log Or (App Equality (Var "v1") (Var "v2")) (App Opapp (App Opapp (Var "string_lt") (Var "v1")) (Var "v2"))))); Dlet (Pvar "string_gt") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "string_lt") (Var "v2")) (Var "v1")))); Dlet (Pvar "string_ge") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "string_le") (Var "v2")) (Var "v1")))); Dlet (Pvar "BITS") (Fun "v1" (Fun "v2" (Fun "v3" (App (Opn Divide) (App (Opn Modulo) (Var "v3") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (App (Opn Plus) (Var "v1") (Val (Lit (IntLit 1)))))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")))))); Dlet (Pvar "BIT") (Fun "v1" (Fun "v2" (App Equality (App (Opn Modulo) (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 1)))))); Dlet (Pvar "SBIT") (Fun "v1" (Fun "v2" (If (Var "v1") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (Val (Lit (IntLit 0)))))); Dtype [(["a"],"ptree", [("Branch", [Tnum; Tnum; Tapp [Tvar "a"] "ptree"; Tapp [Tvar "a"] "ptree"]); ("Leaf",[Tnum; Tvar "a"]); ("Empty",[])])]; Dletrec [("BRANCHING_BIT","v1", Fun "v2" (If (Log Or (App Equality (App Opapp (Var "ODD") (Var "v1")) (App Opapp (Var "EVEN") (Var "v2"))) (App Equality (Var "v1") (Var "v2"))) (Val (Lit (IntLit 0))) (App (Opn Plus) (App Opapp (App Opapp (Var "BRANCHING_BIT") (App Opapp (Var "DIV2") (Var "v1"))) (App Opapp (Var "DIV2") (Var "v2"))) (Val (Lit (IntLit 1))))))]; Dletrec [("PEEK","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Empty" [],Con "None" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v8") (Var "v2")) (Con "Some" [Var "v1"]) (Con "None" [])); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], App Opapp (App Opapp (Var "PEEK") (If (App Opapp (App Opapp (Var "BIT") (Var "v5")) (Var "v8")) (Var "v4") (Var "v3"))) (Var "v8"))]))]; Dlet (Pvar "MOD_2EXP_EQ") (Fun "v3" (Fun "v1" (Fun "v2" (App Equality (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3")) (Var "v1")) (App Opapp (App Opapp (Var "MOD_2EXP") (Var "v3")) (Var "v2")))))); Dlet (Pvar "JOIN") (Fun "v8" (Mat (Var "v8") [(Pcon "Pair" [Pvar "v7"; Pvar "v6"], Mat (Var "v6") [(Pcon "Pair" [Pvar "v5"; Pvar "v4"], Mat (Var "v4") [(Pcon "Pair" [Pvar "v3"; Pvar "v2"], Let "v1" (App Opapp (App Opapp (Var "BRANCHING_BIT") (Var "v7")) (Var "v3")) (If (App Opapp (App Opapp (Var "BIT") (Var "v1")) (Var "v7")) (Con "Branch" [App Opapp (App Opapp (Var "MOD_2EXP") (Var "v1")) (Var "v7"); Var "v1"; Var "v5"; Var "v2"]) (Con "Branch" [App Opapp (App Opapp (Var "MOD_2EXP") (Var "v1")) (Var "v7"); Var "v1"; Var "v2"; Var "v5"])))])])])); Dletrec [("ADD","v13", Fun "v14" (Mat (Var "v13") [(Pcon "Empty" [], Mat (Var "v14") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Leaf" [Var "v2"; Var "v1"])]); (Pcon "Leaf" [Pvar "v6"; Pvar "v5"], Mat (Var "v14") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], If (App Equality (Var "v6") (Var "v4")) (Con "Leaf" [Var "v4"; Var "v3"]) (App Opapp (Var "JOIN") (Con "Pair" [Var "v4"; Con "Pair" [Con "Leaf" [Var "v4"; Var "v3"]; Con "Pair" [Var "v6"; Con "Leaf" [Var "v6"; Var "v5"]]]])))]); (Pcon "Branch" [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"], Mat (Var "v14") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], If (App Opapp (App Opapp (App Opapp (Var "MOD_2EXP_EQ") (Var "v11")) (Var "v8")) (Var "v12")) (If (App Opapp (App Opapp (Var "BIT") (Var "v11")) (Var "v8")) (Con "Branch" [Var "v12"; Var "v11"; App Opapp (App Opapp (Var "ADD") (Var "v10")) (Con "Pair" [Var "v8"; Var "v7"]); Var "v9"]) (Con "Branch" [Var "v12"; Var "v11"; Var "v10"; App Opapp (App Opapp (Var "ADD") (Var "v9")) (Con "Pair" [Var "v8"; Var "v7"])])) (App Opapp (Var "JOIN") (Con "Pair" [Var "v8"; Con "Pair" [Con "Leaf" [Var "v8"; Var "v7"]; Con "Pair" [Var "v12"; Con "Branch" [Var "v12"; Var "v11"; Var "v10"; Var "v9"]]]])))])]))]; Dlet (Pvar "BRANCH") (Fun "v31" (Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v26") [(Pcon "Empty" [], Mat (Var "v25") [(Pcon "Empty" [],Con "Empty" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], Con "Leaf" [Var "v2"; Var "v1"]); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], Con "Branch" [Var "v6"; Var "v5"; Var "v4"; Var "v3"])]); (Pcon "Leaf" [Pvar "v14"; Pvar "v13"], Mat (Var "v25") [(Pcon "Empty" [], Con "Leaf" [Var "v14"; Var "v13"]); (Pcon "Leaf" [Pvar "v8"; Pvar "v7"], Con "Branch" [Var "v30"; Var "v28"; Con "Leaf" [Var "v14"; Var "v13"]; Con "Leaf" [Var "v8"; Var "v7"]]); (Pcon "Branch" [Pvar "v12"; Pvar "v11"; Pvar "v10"; Pvar "v9"], Con "Branch" [Var "v30"; Var "v28"; Con "Leaf" [Var "v14"; Var "v13"]; Con "Branch" [Var "v12"; Var "v11"; Var "v10"; Var "v9"]])]); (Pcon "Branch" [Pvar "v24"; Pvar "v23"; Pvar "v22"; Pvar "v21"], Mat (Var "v25") [(Pcon "Empty" [], Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]); (Pcon "Leaf" [Pvar "v16"; Pvar "v15"], Con "Branch" [Var "v30"; Var "v28"; Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]; Con "Leaf" [Var "v16"; Var "v15"]]); (Pcon "Branch" [Pvar "v20"; Pvar "v19"; Pvar "v18"; Pvar "v17"], Con "Branch" [Var "v30"; Var "v28"; Con "Branch" [Var "v24"; Var "v23"; Var "v22"; Var "v21"]; Con "Branch" [Var "v20"; Var "v19"; Var "v18"; Var "v17"]])])])])])])); Dletrec [("REMOVE","v7", Fun "v8" (Mat (Var "v7") [(Pcon "Empty" [],Con "Empty" []); (Pcon "Leaf" [Pvar "v2"; Pvar "v1"], If (App Equality (Var "v2") (Var "v8")) (Con "Empty" []) (Con "Leaf" [Var "v2"; Var "v1"])); (Pcon "Branch" [Pvar "v6"; Pvar "v5"; Pvar "v4"; Pvar "v3"], If (App Opapp (App Opapp (App Opapp (Var "MOD_2EXP_EQ") (Var "v5")) (Var "v8")) (Var "v6")) (If (App Opapp (App Opapp (Var "BIT") (Var "v5")) (Var "v8")) (App Opapp (Var "BRANCH") (Con "Pair" [Var "v6"; Con "Pair" [Var "v5"; Con "Pair" [App Opapp (App Opapp (Var "REMOVE") (Var "v4")) (Var "v8"); Var "v3"]]])) (App Opapp (Var "BRANCH") (Con "Pair" [Var "v6"; Con "Pair" [Var "v5"; Con "Pair" [Var "v4"; App Opapp (App Opapp (Var "REMOVE") (Var "v3")) (Var "v8")]]]))) (Con "Branch" [Var "v6"; Var "v5"; Var "v4"; Var "v3"]))]))]; Dlet (Pvar "word_add") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_mul") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_add_1") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_mul_1") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_add_2") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Plus) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_mul_2") (Fun "v1" (Fun "v2" (Let "x" (App (Opn Times) (Var "v1") (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dletrec [("BITWISE","v1", Fun "v2" (Fun "v3" (Fun "v4" (If (App (Opb Leq) (Var "v1") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (App (Opn Plus) (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v2")) (Var "v3")) (Var "v4")) (App Opapp (App Opapp (Var "SBIT") (App Opapp (App Opapp (Var "v2") (App Opapp (App Opapp (Var "BIT") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v3"))) (App Opapp (App Opapp (Var "BIT") (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))) (Var "v4")))) (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1))))))))))]; Dlet (Pvar "word_xor") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_xor_1") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 8)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_xor_2") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16)))) (Fun "v2" (Fun "v1" (App Equality (App Equality (Var "v2") (Var "v1")) (Val (Lit (Bool F))))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_or") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (Log Or (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_or_1") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 16)))) (Fun "v2" (Fun "v1" (Log Or (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_and") (Fun "v4" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (App Opapp (Var "BITWISE") (Val (Lit (IntLit 32)))) (Fun "v2" (Fun "v1" (Log And (Var "v2") (Var "v1"))))) (Var "v4")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_lsl") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (Var "v1")))); Dlet (Pvar "word_lsl_1") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul_1") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))) (Var "v1")))); Dlet (Pvar "word_lsl_2") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_mul_2") (Let "x" (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v2")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1")))); Dlet (Pvar "word_lsr") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296))))))); Dlet (Pvar "word_lsr_1") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536))))))); Dlet (Pvar "word_lsr_2") (Fun "v2" (Fun "v1" (Let "x" (App (Opn Divide) (Var "v2") (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Var "v1"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))))); Dlet (Pvar "word_msb") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 31)))) (Var "v1"))); Dlet (Pvar "word_msb_1") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 15)))) (Var "v1"))); Dlet (Pvar "word_msb_2") (Fun "v1" (App Opapp (App Opapp (Var "BIT") (Val (Lit (IntLit 7)))) (Var "v1"))); Dlet (Pvar "word_lsb") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_lsb_1") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_lsb_2") (Fun "v1" (App Equality (App (Opb Leq) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 2)))) (Val (Lit (IntLit 0)))) (Val (Lit (Bool F))))); Dlet (Pvar "word_asr") (Fun "v2" (Fun "v1" (If (App Opapp (Var "word_msb") (Var "v2")) (App Opapp (App Opapp (Var "word_or") (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 4294967296))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 32))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))) (App Opapp (App Opapp (Var "word_lsr") (Var "v2")) (Var "v1"))) (App Opapp (App Opapp (Var "word_lsr") (Var "v2")) (Var "v1"))))); Dlet (Pvar "word_asr_1") (Fun "v2" (Fun "v1" (If (App Opapp (Var "word_msb_1") (Var "v2")) (App Opapp (App Opapp (Var "word_or_1") (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 65536))) (App Opapp (App Opapp (Var "EXP") (Val (Lit (IntLit 2)))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 16))) (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 16))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))) (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2")) (Var "v1"))) (App Opapp (App Opapp (Var "word_lsr_1") (Var "v2")) (Var "v1"))))); Dlet (Pvar "word_sub") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 4294967296))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))))); Dlet (Pvar "word_sub_1") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add_1") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 65536))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 65536)))))))); Dlet (Pvar "word_sub_2") (Fun "v1" (Fun "v2" (App Opapp (App Opapp (Var "word_add_2") (Var "v1")) (Let "x" (Let "k" (App (Opn Minus) (Val (Lit (IntLit 256))) (Var "v2")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k"))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))); Dlet (Pvar "word_bits") (Fun "v1" (Fun "v2" (Fun "v3" (Let "x" (App Opapp (App Opapp (App Opapp (Var "BITS") (App Opapp (App Opapp (Var "MIN") (Var "v1")) (Val (Lit (IntLit 31))))) (Var "v2")) (Var "v3")) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 4294967296)))))))); Dlet (Pvar "word_ror") (Fun "v3" (Fun "v2" (Let "v1" (App (Opn Modulo) (Var "v2") (Val (Lit (IntLit 32)))) (App Opapp (App Opapp (Var "word_or") (App Opapp (App Opapp (App Opapp (Var "word_bits") (Val (Lit (IntLit 31)))) (Var "v1")) (Var "v3"))) (App Opapp (App Opapp (Var "word_lsl") (App Opapp (App Opapp (App Opapp (Var "word_bits") (Let "k" (App (Opn Minus) (Var "v1") (Val (Lit (IntLit 1)))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))) (Val (Lit (IntLit 0)))) (Var "v3"))) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (Var "v1")) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))))); Dlet (Pvar "word_rol") (Fun "v2" (Fun "v1" (App Opapp (App Opapp (Var "word_ror") (Var "v2")) (Let "k" (App (Opn Minus) (Val (Lit (IntLit 32))) (App (Opn Modulo) (Var "v1") (Val (Lit (IntLit 32))))) (If (App (Opb Lt) (Var "k") (Val (Lit (IntLit 0)))) (Val (Lit (IntLit 0))) (Var "k")))))); Dlet (Pvar "Sbox") (Fun "v1" (Let "x" (App Opapp (App Opapp (Var "EL") (Var "v1")) (Con "Cons" [Val (Lit (IntLit 99)); Con "Cons" [Val (Lit (IntLit 124)); Con "Cons" [Val (Lit (IntLit 119)); Con "Cons" [Val (Lit (IntLit 123)); Con "Cons" [Val (Lit (IntLit 242)); Con "Cons" [Val (Lit (IntLit 107)); Con "Cons" [Val (Lit (IntLit 111)); Con "Cons" [Val (Lit (IntLit 197)); Con "Cons" [Val (Lit (IntLit 48)); Con "Cons" [Val (Lit (IntLit 1)); Con "Cons" [Val (Lit (IntLit 103)); Con "Cons" [Val (Lit (IntLit 43)); Con "Cons" [Val (Lit (IntLit 254)); Con "Cons" [Val (Lit (IntLit 215)); Con "Cons" [Val (Lit (IntLit 171)); Con "Cons" [Val (Lit (IntLit 118)); Con "Cons" [Val (Lit (IntLit 202)); Con "Cons" [Val (Lit (IntLit 130)); Con "Cons" [Val (Lit (IntLit 201)); Con "Cons" [Val (Lit (IntLit 125)); Con "Cons" [Val (Lit (IntLit 250)); Con "Cons" [Val (Lit (IntLit 89)); Con "Cons" [Val (Lit (IntLit 71)); Con "Cons" [Val (Lit (IntLit 240)); Con "Cons" [Val (Lit (IntLit 173)); Con "Cons" [Val (Lit (IntLit 212)); Con "Cons" [Val (Lit (IntLit 162)); Con "Cons" [Val (Lit (IntLit 175)); Con "Cons" [Val (Lit (IntLit 156)); Con "Cons" [Val (Lit (IntLit 164)); Con "Cons" [Val (Lit (IntLit 114)); Con "Cons" [Val (Lit (IntLit 192)); Con "Cons" [Val (Lit (IntLit 183)); Con "Cons" [Val (Lit (IntLit 253)); Con "Cons" [Val (Lit (IntLit 147)); Con "Cons" [Val (Lit (IntLit 38)); Con "Cons" [Val (Lit (IntLit 54)); Con "Cons" [Val (Lit (IntLit 63)); Con "Cons" [Val (Lit (IntLit 247)); Con "Cons" [Val (Lit (IntLit 204)); Con "Cons" [Val (Lit (IntLit 52)); Con "Cons" [Val (Lit (IntLit 165)); Con "Cons" [Val (Lit (IntLit 229)); Con "Cons" [Val (Lit (IntLit 241)); Con "Cons" [Val (Lit (IntLit 113)); Con "Cons" [Val (Lit (IntLit 216)); Con "Cons" [Val (Lit (IntLit 49)); Con "Cons" [Val (Lit (IntLit 21)); Con "Cons" [Val (Lit (IntLit 4)); Con "Cons" [Val (Lit (IntLit 199)); Con "Cons" [Val (Lit (IntLit 35)); Con "Cons" [Val (Lit (IntLit 195)); Con "Cons" [Val (Lit (IntLit 24)); Con "Cons" [Val (Lit (IntLit 150)); Con "Cons" [Val (Lit (IntLit 5)); Con "Cons" [Val (Lit (IntLit 154)); Con "Cons" [Val (Lit (IntLit 7)); Con "Cons" [Val (Lit (IntLit 18)); Con "Cons" [Val (Lit (IntLit 128)); Con "Cons" [Val (Lit (IntLit 226)); Con "Cons" [Val (Lit (IntLit 235)); Con "Cons" [Val (Lit (IntLit 39)); Con "Cons" [Val (Lit (IntLit 178)); Con "Cons" [Val (Lit (IntLit 117)); Con "Cons" [Val (Lit (IntLit 9)); Con "Cons" [Val (Lit (IntLit 131)); Con "Cons" [Val (Lit (IntLit 44)); Con "Cons" [Val (Lit (IntLit 26)); Con "Cons" [Val (Lit (IntLit 27)); Con "Cons" [Val (Lit (IntLit 110)); Con "Cons" [Val (Lit (IntLit 90)); Con "Cons" [Val (Lit (IntLit 160)); Con "Cons" [Val (Lit (IntLit 82)); Con "Cons" [Val (Lit (IntLit 59)); Con "Cons" [Val (Lit (IntLit 214)); Con "Cons" [Val (Lit (IntLit 179)); Con "Cons" [Val (Lit (IntLit 41)); Con "Cons" [Val (Lit (IntLit 227)); Con "Cons" [Val (Lit (IntLit 47)); Con "Cons" [Val (Lit (IntLit 132)); Con "Cons" [Val (Lit (IntLit 83)); Con "Cons" [Val (Lit (IntLit 209)); Con "Cons" [Val (Lit (IntLit 0)); Con "Cons" [Val (Lit (IntLit 237)); Con "Cons" [Val (Lit (IntLit 32)); Con "Cons" [Val (Lit (IntLit 252)); Con "Cons" [Val (Lit (IntLit 177)); Con "Cons" [Val (Lit (IntLit 91)); Con "Cons" [Val (Lit (IntLit 106)); Con "Cons" [Val (Lit (IntLit 203)); Con "Cons" [Val (Lit (IntLit 190)); Con "Cons" [Val (Lit (IntLit 57)); Con "Cons" [Val (Lit (IntLit 74)); Con "Cons" [Val (Lit (IntLit 76)); Con "Cons" [Val (Lit (IntLit 88)); Con "Cons" [Val (Lit (IntLit 207)); Con "Cons" [Val (Lit (IntLit 208)); Con "Cons" [Val (Lit (IntLit 239)); Con "Cons" [Val (Lit (IntLit 170)); Con "Cons" [Val (Lit (IntLit 251)); Con "Cons" [Val (Lit (IntLit 67)); Con "Cons" [Val (Lit (IntLit 77)); Con "Cons" [Val (Lit (IntLit 51)); Con "Cons" [Val (Lit (IntLit 133)); Con "Cons" [Val (Lit (IntLit 69)); Con "Cons" [Val (Lit (IntLit 249)); Con "Cons" [Val (Lit (IntLit 2)); Con "Cons" [Val (Lit (IntLit 127)); Con "Cons" [Val (Lit (IntLit 80)); Con "Cons" [Val (Lit (IntLit 60)); Con "Cons" [Val (Lit (IntLit 159)); Con "Cons" [Val (Lit (IntLit 168)); Con "Cons" [Val (Lit (IntLit 81)); Con "Cons" [Val (Lit (IntLit 163)); Con "Cons" [Val (Lit (IntLit 64)); Con "Cons" [Val (Lit (IntLit 143)); Con "Cons" [Val (Lit (IntLit 146)); Con "Cons" [Val (Lit (IntLit 157)); Con "Cons" [Val (Lit (IntLit 56)); Con "Cons" [Val (Lit (IntLit 245)); Con "Cons" [Val (Lit (IntLit 188)); Con "Cons" [Val (Lit (IntLit 182)); Con "Cons" [Val (Lit (IntLit 218)); Con "Cons" [Val (Lit (IntLit 33)); Con "Cons" [Val (Lit (IntLit 16)); Con "Cons" [Val (Lit (IntLit 255)); Con "Cons" [Val (Lit (IntLit 243)); Con "Cons" [Val (Lit (IntLit 210)); Con "Cons" [Val (Lit (IntLit 205)); Con "Cons" [Val (Lit (IntLit 12)); Con "Cons" [Val (Lit (IntLit 19)); Con "Cons" [Val (Lit (IntLit 236)); Con "Cons" [Val (Lit (IntLit 95)); Con "Cons" [Val (Lit (IntLit 151)); Con "Cons" [Val (Lit (IntLit 68)); Con "Cons" [Val (Lit (IntLit 23)); Con "Cons" [Val (Lit (IntLit 196)); Con "Cons" [Val (Lit (IntLit 167)); Con "Cons" [Val (Lit (IntLit 126)); Con "Cons" [Val (Lit (IntLit 61)); Con "Cons" [Val (Lit (IntLit 100)); Con "Cons" [Val (Lit (IntLit 93)); Con "Cons" [Val (Lit (IntLit 25)); Con "Cons" [Val (Lit (IntLit 115)); Con "Cons" [Val (Lit (IntLit 96)); Con "Cons" [Val (Lit (IntLit 129)); Con "Cons" [Val (Lit (IntLit 79)); Con "Cons" [Val (Lit (IntLit 220)); Con "Cons" [Val (Lit (IntLit 34)); Con "Cons" [Val (Lit (IntLit 42)); Con "Cons" [Val (Lit (IntLit 144)); Con "Cons" [Val (Lit (IntLit 136)); Con "Cons" [Val (Lit (IntLit 70)); Con "Cons" [Val (Lit (IntLit 238)); Con "Cons" [Val (Lit (IntLit 184)); Con "Cons" [Val (Lit (IntLit 20)); Con "Cons" [Val (Lit (IntLit 222)); Con "Cons" [Val (Lit (IntLit 94)); Con "Cons" [Val (Lit (IntLit 11)); Con "Cons" [Val (Lit (IntLit 219)); Con "Cons" [Val (Lit (IntLit 224)); Con "Cons" [Val (Lit (IntLit 50)); Con "Cons" [Val (Lit (IntLit 58)); Con "Cons" [Val (Lit (IntLit 10)); Con "Cons" [Val (Lit (IntLit 73)); Con "Cons" [Val (Lit (IntLit 6)); Con "Cons" [Val (Lit (IntLit 36)); Con "Cons" [Val (Lit (IntLit 92)); Con "Cons" [Val (Lit (IntLit 194)); Con "Cons" [Val (Lit (IntLit 211)); Con "Cons" [Val (Lit (IntLit 172)); Con "Cons" [Val (Lit (IntLit 98)); Con "Cons" [Val (Lit (IntLit 145)); Con "Cons" [Val (Lit (IntLit 149)); Con "Cons" [Val (Lit (IntLit 228)); Con "Cons" [Val (Lit (IntLit 121)); Con "Cons" [Val (Lit (IntLit 231)); Con "Cons" [Val (Lit (IntLit 200)); Con "Cons" [Val (Lit (IntLit 55)); Con "Cons" [Val (Lit (IntLit 109)); Con "Cons" [Val (Lit (IntLit 141)); Con "Cons" [Val (Lit (IntLit 213)); Con "Cons" [Val (Lit (IntLit 78)); Con "Cons" [Val (Lit (IntLit 169)); Con "Cons" [Val (Lit (IntLit 108)); Con "Cons" [Val (Lit (IntLit 86)); Con "Cons" [Val (Lit (IntLit 244)); Con "Cons" [Val (Lit (IntLit 234)); Con "Cons" [Val (Lit (IntLit 101)); Con "Cons" [Val (Lit (IntLit 122)); Con "Cons" [Val (Lit (IntLit 174)); Con "Cons" [Val (Lit (IntLit 8)); Con "Cons" [Val (Lit (IntLit 186)); Con "Cons" [Val (Lit (IntLit 120)); Con "Cons" [Val (Lit (IntLit 37)); Con "Cons" [Val (Lit (IntLit 46)); Con "Cons" [Val (Lit (IntLit 28)); Con "Cons" [Val (Lit (IntLit 166)); Con "Cons" [Val (Lit (IntLit 180)); Con "Cons" [Val (Lit (IntLit 198)); Con "Cons" [Val (Lit (IntLit 232)); Con "Cons" [Val (Lit (IntLit 221)); Con "Cons" [Val (Lit (IntLit 116)); Con "Cons" [Val (Lit (IntLit 31)); Con "Cons" [Val (Lit (IntLit 75)); Con "Cons" [Val (Lit (IntLit 189)); Con "Cons" [Val (Lit (IntLit 139)); Con "Cons" [Val (Lit (IntLit 138)); Con "Cons" [Val (Lit (IntLit 112)); Con "Cons" [Val (Lit (IntLit 62)); Con "Cons" [Val (Lit (IntLit 181)); Con "Cons" [Val (Lit (IntLit 102)); Con "Cons" [Val (Lit (IntLit 72)); Con "Cons" [Val (Lit (IntLit 3)); Con "Cons" [Val (Lit (IntLit 246)); Con "Cons" [Val (Lit (IntLit 14)); Con "Cons" [Val (Lit (IntLit 97)); Con "Cons" [Val (Lit (IntLit 53)); Con "Cons" [Val (Lit (IntLit 87)); Con "Cons" [Val (Lit (IntLit 185)); Con "Cons" [Val (Lit (IntLit 134)); Con "Cons" [Val (Lit (IntLit 193)); Con "Cons" [Val (Lit (IntLit 29)); Con "Cons" [Val (Lit (IntLit 158)); Con "Cons" [Val (Lit (IntLit 225)); Con "Cons" [Val (Lit (IntLit 248)); Con "Cons" [Val (Lit (IntLit 152)); Con "Cons" [Val (Lit (IntLit 17)); Con "Cons" [Val (Lit (IntLit 105)); Con "Cons" [Val (Lit (IntLit 217)); Con "Cons" [Val (Lit (IntLit 142)); Con "Cons" [Val (Lit (IntLit 148)); Con "Cons" [Val (Lit (IntLit 155)); Con "Cons" [Val (Lit (IntLit 30)); Con "Cons" [Val (Lit (IntLit 135)); Con "Cons" [Val (Lit (IntLit 233)); Con "Cons" [Val (Lit (IntLit 206)); Con "Cons" [Val (Lit (IntLit 85)); Con "Cons" [Val (Lit (IntLit 40)); Con "Cons" [Val (Lit (IntLit 223)); Con "Cons" [Val (Lit (IntLit 140)); Con "Cons" [Val (Lit (IntLit 161)); Con "Cons" [Val (Lit (IntLit 137)); Con "Cons" [Val (Lit (IntLit 13)); Con "Cons" [Val (Lit (IntLit 191)); Con "Cons" [Val (Lit (IntLit 230)); Con "Cons" [Val (Lit (IntLit 66)); Con "Cons" [Val (Lit (IntLit 104)); Con "Cons" [Val (Lit (IntLit 65)); Con "Cons" [Val (Lit (IntLit 153)); Con "Cons" [Val (Lit (IntLit 45)); Con "Cons" [Val (Lit (IntLit 15)); Con "Cons" [Val (Lit (IntLit 176)); Con "Cons" [Val (Lit (IntLit 84)); Con "Cons" [Val (Lit (IntLit 187)); Con "Cons" [Val (Lit (IntLit 22)); Con "Nil" []]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]])) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))); Dlet (Pvar "InvSbox") (Fun "v1" (Let "x" (App Opapp (App Opapp (Var "EL") (Var "v1")) (Con "Cons" [Val (Lit (IntLit 82)); Con "Cons" [Val (Lit (IntLit 9)); Con "Cons" [Val (Lit (IntLit 106)); Con "Cons" [Val (Lit (IntLit 213)); Con "Cons" [Val (Lit (IntLit 48)); Con "Cons" [Val (Lit (IntLit 54)); Con "Cons" [Val (Lit (IntLit 165)); Con "Cons" [Val (Lit (IntLit 56)); Con "Cons" [Val (Lit (IntLit 191)); Con "Cons" [Val (Lit (IntLit 64)); Con "Cons" [Val (Lit (IntLit 163)); Con "Cons" [Val (Lit (IntLit 158)); Con "Cons" [Val (Lit (IntLit 129)); Con "Cons" [Val (Lit (IntLit 243)); Con "Cons" [Val (Lit (IntLit 215)); Con "Cons" [Val (Lit (IntLit 251)); Con "Cons" [Val (Lit (IntLit 124)); Con "Cons" [Val (Lit (IntLit 227)); Con "Cons" [Val (Lit (IntLit 57)); Con "Cons" [Val (Lit (IntLit 130)); Con "Cons" [Val (Lit (IntLit 155)); Con "Cons" [Val (Lit (IntLit 47)); Con "Cons" [Val (Lit (IntLit 255)); Con "Cons" [Val (Lit (IntLit 135)); Con "Cons" [Val (Lit (IntLit 52)); Con "Cons" [Val (Lit (IntLit 142)); Con "Cons" [Val (Lit (IntLit 67)); Con "Cons" [Val (Lit (IntLit 68)); Con "Cons" [Val (Lit (IntLit 196)); Con "Cons" [Val (Lit (IntLit 222)); Con "Cons" [Val (Lit (IntLit 233)); Con "Cons" [Val (Lit (IntLit 203)); Con "Cons" [Val (Lit (IntLit 84)); Con "Cons" [Val (Lit (IntLit 123)); Con "Cons" [Val (Lit (IntLit 148)); Con "Cons" [Val (Lit (IntLit 50)); Con "Cons" [Val (Lit (IntLit 166)); Con "Cons" [Val (Lit (IntLit 194)); Con "Cons" [Val (Lit (IntLit 35)); Con "Cons" [Val (Lit (IntLit 61)); Con "Cons" [Val (Lit (IntLit 238)); Con "Cons" [Val (Lit (IntLit 76)); Con "Cons" [Val (Lit (IntLit 149)); Con "Cons" [Val (Lit (IntLit 11)); Con "Cons" [Val (Lit (IntLit 66)); Con "Cons" [Val (Lit (IntLit 250)); Con "Cons" [Val (Lit (IntLit 195)); Con "Cons" [Val (Lit (IntLit 78)); Con "Cons" [Val (Lit (IntLit 8)); Con "Cons" [Val (Lit (IntLit 46)); Con "Cons" [Val (Lit (IntLit 161)); Con "Cons" [Val (Lit (IntLit 102)); Con "Cons" [Val (Lit (IntLit 40)); Con "Cons" [Val (Lit (IntLit 217)); Con "Cons" [Val (Lit (IntLit 36)); Con "Cons" [Val (Lit (IntLit 178)); Con "Cons" [Val (Lit (IntLit 118)); Con "Cons" [Val (Lit (IntLit 91)); Con "Cons" [Val (Lit (IntLit 162)); Con "Cons" [Val (Lit (IntLit 73)); Con "Cons" [Val (Lit (IntLit 109)); Con "Cons" [Val (Lit (IntLit 139)); Con "Cons" [Val (Lit (IntLit 209)); Con "Cons" [Val (Lit (IntLit 37)); Con "Cons" [Val (Lit (IntLit 114)); Con "Cons" [Val (Lit (IntLit 248)); Con "Cons" [Val (Lit (IntLit 246)); Con "Cons" [Val (Lit (IntLit 100)); Con "Cons" [Val (Lit (IntLit 134)); Con "Cons" [Val (Lit (IntLit 104)); Con "Cons" [Val (Lit (IntLit 152)); Con "Cons" [Val (Lit (IntLit 22)); Con "Cons" [Val (Lit (IntLit 212)); Con "Cons" [Val (Lit (IntLit 164)); Con "Cons" [Val (Lit (IntLit 92)); Con "Cons" [Val (Lit (IntLit 204)); Con "Cons" [Val (Lit (IntLit 93)); Con "Cons" [Val (Lit (IntLit 101)); Con "Cons" [Val (Lit (IntLit 182)); Con "Cons" [Val (Lit (IntLit 146)); Con "Cons" [Val (Lit (IntLit 108)); Con "Cons" [Val (Lit (IntLit 112)); Con "Cons" [Val (Lit (IntLit 72)); Con "Cons" [Val (Lit (IntLit 80)); Con "Cons" [Val (Lit (IntLit 253)); Con "Cons" [Val (Lit (IntLit 237)); Con "Cons" [Val (Lit (IntLit 185)); Con "Cons" [Val (Lit (IntLit 218)); Con "Cons" [Val (Lit (IntLit 94)); Con "Cons" [Val (Lit (IntLit 21)); Con "Cons" [Val (Lit (IntLit 70)); Con "Cons" [Val (Lit (IntLit 87)); Con "Cons" [Val (Lit (IntLit 167)); Con "Cons" [Val (Lit (IntLit 141)); Con "Cons" [Val (Lit (IntLit 157)); Con "Cons" [Val (Lit (IntLit 132)); Con "Cons" [Val (Lit (IntLit 144)); Con "Cons" [Val (Lit (IntLit 216)); Con "Cons" [Val (Lit (IntLit 171)); Con "Cons" [Val (Lit (IntLit 0)); Con "Cons" [Val (Lit (IntLit 140)); Con "Cons" [Val (Lit (IntLit 188)); Con "Cons" [Val (Lit (IntLit 211)); Con "Cons" [Val (Lit (IntLit 10)); Con "Cons" [Val (Lit (IntLit 247)); Con "Cons" [Val (Lit (IntLit 228)); Con "Cons" [Val (Lit (IntLit 88)); Con "Cons" [Val (Lit (IntLit 5)); Con "Cons" [Val (Lit (IntLit 184)); Con "Cons" [Val (Lit (IntLit 179)); Con "Cons" [Val (Lit (IntLit 69)); Con "Cons" [Val (Lit (IntLit 6)); Con "Cons" [Val (Lit (IntLit 208)); Con "Cons" [Val (Lit (IntLit 44)); Con "Cons" [Val (Lit (IntLit 30)); Con "Cons" [Val (Lit (IntLit 143)); Con "Cons" [Val (Lit (IntLit 202)); Con "Cons" [Val (Lit (IntLit 63)); Con "Cons" [Val (Lit (IntLit 15)); Con "Cons" [Val (Lit (IntLit 2)); Con "Cons" [Val (Lit (IntLit 193)); Con "Cons" [Val (Lit (IntLit 175)); Con "Cons" [Val (Lit (IntLit 189)); Con "Cons" [Val (Lit (IntLit 3)); Con "Cons" [Val (Lit (IntLit 1)); Con "Cons" [Val (Lit (IntLit 19)); Con "Cons" [Val (Lit (IntLit 138)); Con "Cons" [Val (Lit (IntLit 107)); Con "Cons" [Val (Lit (IntLit 58)); Con "Cons" [Val (Lit (IntLit 145)); Con "Cons" [Val (Lit (IntLit 17)); Con "Cons" [Val (Lit (IntLit 65)); Con "Cons" [Val (Lit (IntLit 79)); Con "Cons" [Val (Lit (IntLit 103)); Con "Cons" [Val (Lit (IntLit 220)); Con "Cons" [Val (Lit (IntLit 234)); Con "Cons" [Val (Lit (IntLit 151)); Con "Cons" [Val (Lit (IntLit 242)); Con "Cons" [Val (Lit (IntLit 207)); Con "Cons" [Val (Lit (IntLit 206)); Con "Cons" [Val (Lit (IntLit 240)); Con "Cons" [Val (Lit (IntLit 180)); Con "Cons" [Val (Lit (IntLit 230)); Con "Cons" [Val (Lit (IntLit 115)); Con "Cons" [Val (Lit (IntLit 150)); Con "Cons" [Val (Lit (IntLit 172)); Con "Cons" [Val (Lit (IntLit 116)); Con "Cons" [Val (Lit (IntLit 34)); Con "Cons" [Val (Lit (IntLit 231)); Con "Cons" [Val (Lit (IntLit 173)); Con "Cons" [Val (Lit (IntLit 53)); Con "Cons" [Val (Lit (IntLit 133)); Con "Cons" [Val (Lit (IntLit 226)); Con "Cons" [Val (Lit (IntLit 249)); Con "Cons" [Val (Lit (IntLit 55)); Con "Cons" [Val (Lit (IntLit 232)); Con "Cons" [Val (Lit (IntLit 28)); Con "Cons" [Val (Lit (IntLit 117)); Con "Cons" [Val (Lit (IntLit 223)); Con "Cons" [Val (Lit (IntLit 110)); Con "Cons" [Val (Lit (IntLit 71)); Con "Cons" [Val (Lit (IntLit 241)); Con "Cons" [Val (Lit (IntLit 26)); Con "Cons" [Val (Lit (IntLit 113)); Con "Cons" [Val (Lit (IntLit 29)); Con "Cons" [Val (Lit (IntLit 41)); Con "Cons" [Val (Lit (IntLit 197)); Con "Cons" [Val (Lit (IntLit 137)); Con "Cons" [Val (Lit (IntLit 111)); Con "Cons" [Val (Lit (IntLit 183)); Con "Cons" [Val (Lit (IntLit 98)); Con "Cons" [Val (Lit (IntLit 14)); Con "Cons" [Val (Lit (IntLit 170)); Con "Cons" [Val (Lit (IntLit 24)); Con "Cons" [Val (Lit (IntLit 190)); Con "Cons" [Val (Lit (IntLit 27)); Con "Cons" [Val (Lit (IntLit 252)); Con "Cons" [Val (Lit (IntLit 86)); Con "Cons" [Val (Lit (IntLit 62)); Con "Cons" [Val (Lit (IntLit 75)); Con "Cons" [Val (Lit (IntLit 198)); Con "Cons" [Val (Lit (IntLit 210)); Con "Cons" [Val (Lit (IntLit 121)); Con "Cons" [Val (Lit (IntLit 32)); Con "Cons" [Val (Lit (IntLit 154)); Con "Cons" [Val (Lit (IntLit 219)); Con "Cons" [Val (Lit (IntLit 192)); Con "Cons" [Val (Lit (IntLit 254)); Con "Cons" [Val (Lit (IntLit 120)); Con "Cons" [Val (Lit (IntLit 205)); Con "Cons" [Val (Lit (IntLit 90)); Con "Cons" [Val (Lit (IntLit 244)); Con "Cons" [Val (Lit (IntLit 31)); Con "Cons" [Val (Lit (IntLit 221)); Con "Cons" [Val (Lit (IntLit 168)); Con "Cons" [Val (Lit (IntLit 51)); Con "Cons" [Val (Lit (IntLit 136)); Con "Cons" [Val (Lit (IntLit 7)); Con "Cons" [Val (Lit (IntLit 199)); Con "Cons" [Val (Lit (IntLit 49)); Con "Cons" [Val (Lit (IntLit 177)); Con "Cons" [Val (Lit (IntLit 18)); Con "Cons" [Val (Lit (IntLit 16)); Con "Cons" [Val (Lit (IntLit 89)); Con "Cons" [Val (Lit (IntLit 39)); Con "Cons" [Val (Lit (IntLit 128)); Con "Cons" [Val (Lit (IntLit 236)); Con "Cons" [Val (Lit (IntLit 95)); Con "Cons" [Val (Lit (IntLit 96)); Con "Cons" [Val (Lit (IntLit 81)); Con "Cons" [Val (Lit (IntLit 127)); Con "Cons" [Val (Lit (IntLit 169)); Con "Cons" [Val (Lit (IntLit 25)); Con "Cons" [Val (Lit (IntLit 181)); Con "Cons" [Val (Lit (IntLit 74)); Con "Cons" [Val (Lit (IntLit 13)); Con "Cons" [Val (Lit (IntLit 45)); Con "Cons" [Val (Lit (IntLit 229)); Con "Cons" [Val (Lit (IntLit 122)); Con "Cons" [Val (Lit (IntLit 159)); Con "Cons" [Val (Lit (IntLit 147)); Con "Cons" [Val (Lit (IntLit 201)); Con "Cons" [Val (Lit (IntLit 156)); Con "Cons" [Val (Lit (IntLit 239)); Con "Cons" [Val (Lit (IntLit 160)); Con "Cons" [Val (Lit (IntLit 224)); Con "Cons" [Val (Lit (IntLit 59)); Con "Cons" [Val (Lit (IntLit 77)); Con "Cons" [Val (Lit (IntLit 174)); Con "Cons" [Val (Lit (IntLit 42)); Con "Cons" [Val (Lit (IntLit 245)); Con "Cons" [Val (Lit (IntLit 176)); Con "Cons" [Val (Lit (IntLit 200)); Con "Cons" [Val (Lit (IntLit 235)); Con "Cons" [Val (Lit (IntLit 187)); Con "Cons" [Val (Lit (IntLit 60)); Con "Cons" [Val (Lit (IntLit 131)); Con "Cons" [Val (Lit (IntLit 83)); Con "Cons" [Val (Lit (IntLit 153)); Con "Cons" [Val (Lit (IntLit 97)); Con "Cons" [Val (Lit (IntLit 23)); Con "Cons" [Val (Lit (IntLit 43)); Con "Cons" [Val (Lit (IntLit 4)); Con "Cons" [Val (Lit (IntLit 126)); Con "Cons" [Val (Lit (IntLit 186)); Con "Cons" [Val (Lit (IntLit 119)); Con "Cons" [Val (Lit (IntLit 214)); Con "Cons" [Val (Lit (IntLit 38)); Con "Cons" [Val (Lit (IntLit 225)); Con "Cons" [Val (Lit (IntLit 105)); Con "Cons" [Val (Lit (IntLit 20)); Con "Cons" [Val (Lit (IntLit 99)); Con "Cons" [Val (Lit (IntLit 85)); Con "Cons" [Val (Lit (IntLit 33)); Con "Cons" [Val (Lit (IntLit 12)); Con "Cons" [Val (Lit (IntLit 125)); Con "Nil" []]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]])) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))); Dlet (Pvar "genSubBytes") (Fun "v31" (Fun "v32" (Mat (Var "v32") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Opapp (Var "v31") (Var "v30"); Con "Pair" [App Opapp (Var "v31") (Var "v28"); Con "Pair" [App Opapp (Var "v31") (Var "v26"); Con "Pair" [App Opapp (Var "v31") (Var "v24"); Con "Pair" [App Opapp (Var "v31") (Var "v22"); Con "Pair" [App Opapp (Var "v31") (Var "v20"); Con "Pair" [App Opapp (Var "v31") (Var "v18"); Con "Pair" [App Opapp (Var "v31") (Var "v16"); Con "Pair" [App Opapp (Var "v31") (Var "v14"); Con "Pair" [App Opapp (Var "v31") (Var "v12"); Con "Pair" [App Opapp (Var "v31") (Var "v10"); Con "Pair" [App Opapp (Var "v31") (Var "v8"); Con "Pair" [App Opapp (Var "v31") (Var "v6"); Con "Pair" [App Opapp (Var "v31") (Var "v4"); Con "Pair" [App Opapp (Var "v31") (Var "v2"); App Opapp (Var "v31") (Var "v1")]]]]]]]]]]]]]]])])])])])])])])])])])])])])])]))); Dlet (Pvar "SubBytes") (Fun "v1" (App Opapp (App Opapp (Var "genSubBytes") (Var "Sbox")) (Var "v1"))); Dlet (Pvar "ShiftRows") (Fun "v31" (Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v30"; Con "Pair" [Var "v28"; Con "Pair" [Var "v26"; Con "Pair" [Var "v24"; Con "Pair" [Var "v20"; Con "Pair" [Var "v18"; Con "Pair" [Var "v16"; Con "Pair" [Var "v22"; Con "Pair" [Var "v10"; Con "Pair" [Var "v8"; Con "Pair" [Var "v14"; Con "Pair" [Var "v12"; Con "Pair" [Var "v1"; Con "Pair" [Var "v6"; Con "Pair" [Var "v4"; Var "v2"]]]]]]]]]]]]]]])])])])])])])])])])])])])])])])); Dlet (Pvar "XOR_BLOCK") (Fun "v61" (Fun "v62" (Mat (Var "v61") [(Pcon "Pair" [Pvar "v60"; Pvar "v59"], Mat (Var "v59") [(Pcon "Pair" [Pvar "v58"; Pvar "v57"], Mat (Var "v57") [(Pcon "Pair" [Pvar "v56"; Pvar "v55"], Mat (Var "v55") [(Pcon "Pair" [Pvar "v54"; Pvar "v53"], Mat (Var "v53") [(Pcon "Pair" [Pvar "v52"; Pvar "v51"], Mat (Var "v51") [(Pcon "Pair" [Pvar "v50"; Pvar "v49"], Mat (Var "v49") [(Pcon "Pair" [Pvar "v48"; Pvar "v47"], Mat (Var "v47") [(Pcon "Pair" [Pvar "v46"; Pvar "v45"], Mat (Var "v45") [(Pcon "Pair" [Pvar "v44"; Pvar "v43"], Mat (Var "v43") [(Pcon "Pair" [Pvar "v42"; Pvar "v41"], Mat (Var "v41") [(Pcon "Pair" [Pvar "v40"; Pvar "v39"], Mat (Var "v39") [(Pcon "Pair" [Pvar "v38"; Pvar "v37"], Mat (Var "v37") [(Pcon "Pair" [Pvar "v36"; Pvar "v35"], Mat (Var "v35") [(Pcon "Pair" [Pvar "v34"; Pvar "v33"], Mat (Var "v33") [(Pcon "Pair" [Pvar "v32"; Pvar "v31"], Mat (Var "v62") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v60")) (Var "v30"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v58")) (Var "v28"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v56")) (Var "v26"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v54")) (Var "v24"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v52")) (Var "v22"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v50")) (Var "v20"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v48")) (Var "v18"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v46")) (Var "v16"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v44")) (Var "v14"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v42")) (Var "v12"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v40")) (Var "v10"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v38")) (Var "v8"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v36")) (Var "v6"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v34")) (Var "v4"); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v32")) (Var "v2"); App Opapp (App Opapp (Var "word_xor_1") (Var "v31")) (Var "v1")]]]]]]]]]]]]]]])])])])])])])])])])])])])])])])])])])])])])])])])])])])])])]))); Dlet (Pvar "AddRoundKey") (Fun "v1" (App Opapp (Var "XOR_BLOCK") (Var "v1"))); Dlet (Pvar "genMixColumns") (Fun "v59" (Fun "v60" (Mat (Var "v60") [(Pcon "Pair" [Pvar "v58"; Pvar "v57"], Mat (Var "v57") [(Pcon "Pair" [Pvar "v56"; Pvar "v55"], Mat (Var "v55") [(Pcon "Pair" [Pvar "v54"; Pvar "v53"], Mat (Var "v53") [(Pcon "Pair" [Pvar "v52"; Pvar "v51"], Mat (Var "v51") [(Pcon "Pair" [Pvar "v50"; Pvar "v49"], Mat (Var "v49") [(Pcon "Pair" [Pvar "v48"; Pvar "v47"], Mat (Var "v47") [(Pcon "Pair" [Pvar "v46"; Pvar "v45"], Mat (Var "v45") [(Pcon "Pair" [Pvar "v44"; Pvar "v43"], Mat (Var "v43") [(Pcon "Pair" [Pvar "v42"; Pvar "v41"], Mat (Var "v41") [(Pcon "Pair" [Pvar "v40"; Pvar "v39"], Mat (Var "v39") [(Pcon "Pair" [Pvar "v38"; Pvar "v37"], Mat (Var "v37") [(Pcon "Pair" [Pvar "v36"; Pvar "v35"], Mat (Var "v35") [(Pcon "Pair" [Pvar "v34"; Pvar "v33"], Mat (Var "v33") [(Pcon "Pair" [Pvar "v32"; Pvar "v31"], Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Let "v28" (App Opapp (Var "v59") (Con "Pair" [Var "v58"; Con "Pair" [Var "v50"; Con "Pair" [Var "v42"; Var "v34"]]])) (Mat (Var "v28") [(Pcon "Pair" [Pvar "v27"; Pvar "v26"], Mat (Var "v26") [(Pcon "Pair" [Pvar "v25"; Pvar "v24"], Mat (Var "v24") [(Pcon "Pair" [Pvar "v23"; Pvar "v22"], Let "v21" (App Opapp (Var "v59") (Con "Pair" [Var "v56"; Con "Pair" [Var "v48"; Con "Pair" [Var "v40"; Var "v32"]]])) (Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Let "v14" (App Opapp (Var "v59") (Con "Pair" [Var "v54"; Con "Pair" [Var "v46"; Con "Pair" [Var "v38"; Var "v30"]]])) (Mat (Var "v14") [(Pcon "Pair" [Pvar "v13"; Pvar "v12"], Mat (Var "v12") [(Pcon "Pair" [Pvar "v11"; Pvar "v10"], Mat (Var "v10") [(Pcon "Pair" [Pvar "v9"; Pvar "v8"], Let "v7" (App Opapp (Var "v59") (Con "Pair" [Var "v52"; Con "Pair" [Var "v44"; Con "Pair" [Var "v36"; Var "v29"]]])) (Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v27"; Con "Pair" [Var "v20"; Con "Pair" [Var "v13"; Con "Pair" [Var "v6"; Con "Pair" [Var "v25"; Con "Pair" [Var "v18"; Con "Pair" [Var "v11"; Con "Pair" [Var "v4"; Con "Pair" [Var "v23"; Con "Pair" [Var "v16"; Con "Pair" [Var "v9"; Con "Pair" [Var "v2"; Con "Pair" [Var "v22"; Con "Pair" [Var "v15"; Con "Pair" [Var "v8"; Var "v1"]]]]]]]]]]]]]]])])])]))])])]))])])]))])])]))])])])])])])])])])])])])])])]))); Dlet (Pvar "xtime") (Fun "v1" (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "word_lsl_2") (Var "v1")) (Val (Lit (IntLit 1))))) (If (App Opapp (Var "word_msb_2") (Var "v1")) (Let "x" (Val (Lit (IntLit 27))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))) (Let "x" (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))))); Dletrec [("**","v1", Fun "v2" (If (App Equality (Var "v1") (Let "x" (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Let "x" (Val (Lit (IntLit 0))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256))))) (If (App Opapp (Var "word_lsb_2") (Var "v1")) (App Opapp (App Opapp (Var "word_xor_1") (Var "v2")) (App Opapp (App Opapp (Var "**") (App Opapp (App Opapp (Var "word_lsr_2") (Var "v1")) (Val (Lit (IntLit 1))))) (App Opapp (Var "xtime") (Var "v2")))) (App Opapp (App Opapp (Var "**") (App Opapp (App Opapp (Var "word_lsr_2") (Var "v1")) (Val (Lit (IntLit 1))))) (App Opapp (Var "xtime") (Var "v2"))))))]; Dlet (Pvar "MultCol") (Fun "v7" (Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 2))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v6"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 3))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v4"))) (App Opapp (App Opapp (Var "word_xor_1") (Var "v2")) (Var "v1"))); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v6")) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 2))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v4"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 3))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v2"))) (Var "v1"))); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (Var "v6")) (App Opapp (App Opapp (Var "word_xor_1") (Var "v4")) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 2))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v2"))) (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 3))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1")))); App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 3))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v6"))) (App Opapp (App Opapp (Var "word_xor_1") (Var "v4")) (App Opapp (App Opapp (Var "word_xor_1") (Var "v2")) (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 2))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1"))))]]])])])])); Dlet (Pvar "MixColumns") (Fun "v1" (App Opapp (App Opapp (Var "genMixColumns") (Var "MultCol")) (Var "v1"))); Dlet (Pvar "ROTKEYS") (Fun "v21" (Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v18"; Con "Pair" [Var "v16"; Con "Pair" [Var "v14"; Con "Pair" [Var "v12"; Con "Pair" [Var "v10"; Con "Pair" [Var "v8"; Con "Pair" [Var "v6"; Con "Pair" [Var "v4"; Con "Pair" [Var "v2"; Con "Pair" [Var "v1"; Var "v20"]]]]]]]]]])])])])])])])])])])])); Dletrec [("RoundTuple","v5", Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0)))) (Con "Pair" [Val (Lit (IntLit 0)); Con "Pair" [App Opapp (Var "ROTKEYS") (Var "v2"); App Opapp (App Opapp (Var "AddRoundKey") (App Opapp (Var "FST") (Var "v2"))) (App Opapp (Var "ShiftRows") (App Opapp (Var "SubBytes") (Var "v1")))]]) (App Opapp (Var "RoundTuple") (Con "Pair" [App (Opn Minus) (Var "v4") (Val (Lit (IntLit 1))); Con "Pair" [App Opapp (Var "ROTKEYS") (Var "v2"); App Opapp (App Opapp (Var "AddRoundKey") (App Opapp (Var "FST") (Var "v2"))) (App Opapp (Var "MixColumns") (App Opapp (Var "ShiftRows") (App Opapp (Var "SubBytes") (Var "v1"))))]])))])])]; Dlet (Pvar "Round") (Fun "v2" (Fun "v1" (Fun "v3" (App Opapp (Var "SND") (App Opapp (Var "SND") (App Opapp (Var "RoundTuple") (Con "Pair" [Var "v2"; Con "Pair" [Var "v1"; Var "v3"]]))))))); Dlet (Pvar "from_state") (Fun "v31" (Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v30"; Con "Pair" [Var "v22"; Con "Pair" [Var "v14"; Con "Pair" [Var "v6"; Con "Pair" [Var "v28"; Con "Pair" [Var "v20"; Con "Pair" [Var "v12"; Con "Pair" [Var "v4"; Con "Pair" [Var "v26"; Con "Pair" [Var "v18"; Con "Pair" [Var "v10"; Con "Pair" [Var "v2"; Con "Pair" [Var "v24"; Con "Pair" [Var "v16"; Con "Pair" [Var "v8"; Var "v1"]]]]]]]]]]]]]]])])])])])])])])])])])])])])])])); Dlet (Pvar "to_state") (Fun "v31" (Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v30"; Con "Pair" [Var "v22"; Con "Pair" [Var "v14"; Con "Pair" [Var "v6"; Con "Pair" [Var "v28"; Con "Pair" [Var "v20"; Con "Pair" [Var "v12"; Con "Pair" [Var "v4"; Con "Pair" [Var "v26"; Con "Pair" [Var "v18"; Con "Pair" [Var "v10"; Con "Pair" [Var "v2"; Con "Pair" [Var "v24"; Con "Pair" [Var "v16"; Con "Pair" [Var "v8"; Var "v1"]]]]]]]]]]]]]]])])])])])])])])])])])])])])])])); Dlet (Pvar "InvMultCol") (Fun "v7" (Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 14))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v6"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 11))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v4"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 13))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v2"))) (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 9))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1")))); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 9))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v6"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 14))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v4"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 11))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v2"))) (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 13))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1")))); Con "Pair" [App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 13))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v6"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 9))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v4"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 14))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v2"))) (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 11))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1")))); App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 11))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v6"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 13))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v4"))) (App Opapp (App Opapp (Var "word_xor_1") (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 9))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v2"))) (App Opapp (App Opapp (Var "**") (Let "x" (Val (Lit (IntLit 14))) (App (Opn Modulo) (Var "x") (Val (Lit (IntLit 256)))))) (Var "v1"))))]]])])])])); Dlet (Pvar "InvMixColumns") (Fun "v1" (App Opapp (App Opapp (Var "genMixColumns") (Var "InvMultCol")) (Var "v1"))); Dlet (Pvar "InvShiftRows") (Fun "v31" (Mat (Var "v31") [(Pcon "Pair" [Pvar "v30"; Pvar "v29"], Mat (Var "v29") [(Pcon "Pair" [Pvar "v28"; Pvar "v27"], Mat (Var "v27") [(Pcon "Pair" [Pvar "v26"; Pvar "v25"], Mat (Var "v25") [(Pcon "Pair" [Pvar "v24"; Pvar "v23"], Mat (Var "v23") [(Pcon "Pair" [Pvar "v22"; Pvar "v21"], Mat (Var "v21") [(Pcon "Pair" [Pvar "v20"; Pvar "v19"], Mat (Var "v19") [(Pcon "Pair" [Pvar "v18"; Pvar "v17"], Mat (Var "v17") [(Pcon "Pair" [Pvar "v16"; Pvar "v15"], Mat (Var "v15") [(Pcon "Pair" [Pvar "v14"; Pvar "v13"], Mat (Var "v13") [(Pcon "Pair" [Pvar "v12"; Pvar "v11"], Mat (Var "v11") [(Pcon "Pair" [Pvar "v10"; Pvar "v9"], Mat (Var "v9") [(Pcon "Pair" [Pvar "v8"; Pvar "v7"], Mat (Var "v7") [(Pcon "Pair" [Pvar "v6"; Pvar "v5"], Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], Con "Pair" [Var "v30"; Con "Pair" [Var "v28"; Con "Pair" [Var "v26"; Con "Pair" [Var "v24"; Con "Pair" [Var "v16"; Con "Pair" [Var "v22"; Con "Pair" [Var "v20"; Con "Pair" [Var "v18"; Con "Pair" [Var "v10"; Con "Pair" [Var "v8"; Con "Pair" [Var "v14"; Con "Pair" [Var "v12"; Con "Pair" [Var "v4"; Con "Pair" [Var "v2"; Con "Pair" [Var "v1"; Var "v6"]]]]]]]]]]]]]]])])])])])])])])])])])])])])])])); Dlet (Pvar "InvSubBytes") (Fun "v1" (App Opapp (App Opapp (Var "genSubBytes") (Var "InvSbox")) (Var "v1"))); Dletrec [("InvRoundTuple","v5", Mat (Var "v5") [(Pcon "Pair" [Pvar "v4"; Pvar "v3"], Mat (Var "v3") [(Pcon "Pair" [Pvar "v2"; Pvar "v1"], If (App (Opb Leq) (Var "v4") (Val (Lit (IntLit 0)))) (Con "Pair" [Val (Lit (IntLit 0)); Con "Pair" [App Opapp (Var "ROTKEYS") (Var "v2"); App Opapp (App Opapp (Var "AddRoundKey") (App Opapp (Var "FST") (Var "v2"))) (App Opapp (Var "InvSubBytes") (App Opapp (Var "InvShiftRows") (Var "v1")))]]) (App Opapp (Var "InvRoundTuple") (Con "Pair" [App (Opn Minus) (Var "v4") (Val (Lit (IntLit 1))); Con "Pair" [App Opapp (Var "ROTKEYS") (Var "v2"); App Opapp (Var "InvMixColumns") (App Opapp (App Opapp (Var "AddRoundKey") (App Opapp (Var "FST") (Var "v2"))) (App Opapp (Var "InvSubBytes") (App Opapp (Var "InvShiftRows") (Var "v1"))))]])))])])]; Dlet (Pvar "InvRound") (Fun "v2" (Fun "v1" (Fun "v3" (App Opapp (Var "SND") (App Opapp (Var "SND") (App Opapp (Var "InvRoundTuple") (Con "Pair" [Var "v2"; Con "Pair" [Var "v1"; Var "v3"]]))))))); Dlet (Pvar "AES_FWD") (Fun "v1" (App Opapp (App Opapp (Var "o") (Var "from_state")) (App Opapp (App Opapp (Var "o") (App Opapp (App Opapp (Var "Round") (Val (Lit (IntLit 9)))) (App Opapp (Var "ROTKEYS") (Var "v1")))) (App Opapp (App Opapp (Var "o") (App Opapp (Var "AddRoundKey") (App Opapp (Var "FST") (Var "v1")))) (Var "to_state"))))); Dlet (Pvar "AES_BWD") (Fun "v1" (App Opapp (App Opapp (Var "o") (Var "from_state")) (App Opapp (App Opapp (Var "o") (App Opapp (App Opapp (Var "InvRound") (Val (Lit (IntLit 9)))) (App Opapp (Var "ROTKEYS") (Var "v1")))) (App Opapp (App Opapp (Var "o") (App Opapp (Var "AddRoundKey") (App Opapp (Var "FST") (Var "v1")))) (Var "to_state")))))]