def aria_blk

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8363

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A

8363# a block read back from its bytes, and the bytes from their block, on the bits
8364def aria_blk(b: M.CmBlock) -> {b == A.aria.to_block(A.aria.of_block(b)) : M.CmBlock}:
8365  match b:
8366    case M.CmBlock{U32{WCon{a0_0, WCon{a0_1, WCon{a0_2, WCon{a0_3, WCon{a0_4, WCon{a0_5, WCon{a0_6, WCon{a0_7, WCon{a0_8, WCon{a0_9, WCon{a0_10, WCon{a0_11, WCon{a0_12, WCon{a0_13, WCon{a0_14, WCon{a0_15, WCon{a0_16, WCon{a0_17, WCon{a0_18, WCon{a0_19, WCon{a0_20, WCon{a0_21, WCon{a0_22, WCon{a0_23, WCon{a0_24, WCon{a0_25, WCon{a0_26, WCon{a0_27, WCon{a0_28, WCon{a0_29, WCon{a0_30, WCon{a0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{a1_0, WCon{a1_1, WCon{a1_2, WCon{a1_3, WCon{a1_4, WCon{a1_5, WCon{a1_6, WCon{a1_7, WCon{a1_8, WCon{a1_9, WCon{a1_10, WCon{a1_11, WCon{a1_12, WCon{a1_13, WCon{a1_14, WCon{a1_15, WCon{a1_16, WCon{a1_17, WCon{a1_18, WCon{a1_19, WCon{a1_20, WCon{a1_21, WCon{a1_22, WCon{a1_23, WCon{a1_24, WCon{a1_25, WCon{a1_26, WCon{a1_27, WCon{a1_28, WCon{a1_29, WCon{a1_30, WCon{a1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{a2_0, WCon{a2_1, WCon{a2_2, WCon{a2_3, WCon{a2_4, WCon{a2_5, WCon{a2_6, WCon{a2_7, WCon{a2_8, WCon{a2_9, WCon{a2_10, WCon{a2_11, WCon{a2_12, WCon{a2_13, WCon{a2_14, WCon{a2_15, WCon{a2_16, WCon{a2_17, WCon{a2_18, WCon{a2_19, WCon{a2_20, WCon{a2_21, WCon{a2_22, WCon{a2_23, WCon{a2_24, WCon{a2_25, WCon{a2_26, WCon{a2_27, WCon{a2_28, WCon{a2_29, WCon{a2_30, WCon{a2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{a3_0, WCon{a3_1, WCon{a3_2, WCon{a3_3, WCon{a3_4, WCon{a3_5, WCon{a3_6, WCon{a3_7, WCon{a3_8, WCon{a3_9, WCon{a3_10, WCon{a3_11, WCon{a3_12, WCon{a3_13, WCon{a3_14, WCon{a3_15, WCon{a3_16, WCon{a3_17, WCon{a3_18, WCon{a3_19, WCon{a3_20, WCon{a3_21, WCon{a3_22, WCon{a3_23, WCon{a3_24, WCon{a3_25, WCon{a3_26, WCon{a3_27, WCon{a3_28, WCon{a3_29, WCon{a3_30, WCon{a3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
8367      {==}