def pack_int

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash_bits.bend:154

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D

154def pack_int(+a0: U32, +a1: U32, +a2: U32, +a3: U32, +a4: U32, +a5: U32, +a6: U32, +a7: U32, +a8: U32, +a9: U32, +a10: U32, +a11: U32, +a12: U32, +a13: U32, +a14: U32, +a15: U32) -> {D.R(I.B{G.int32(a0, a1, a2, a3), G.int32(a4, a5, a6, a7), G.int32(a8, a9, a10, a11), G.int32(a12, a13, a14, a15)}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}:
155  match a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15:
156    case 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{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a4_0, WCon{a4_1, WCon{a4_2, WCon{a4_3, WCon{a4_4, WCon{a4_5, WCon{a4_6, WCon{a4_7, WCon{a4_8, WCon{a4_9, WCon{a4_10, WCon{a4_11, WCon{a4_12, WCon{a4_13, WCon{a4_14, WCon{a4_15, WCon{a4_16, WCon{a4_17, WCon{a4_18, WCon{a4_19, WCon{a4_20, WCon{a4_21, WCon{a4_22, WCon{a4_23, WCon{a4_24, WCon{a4_25, WCon{a4_26, WCon{a4_27, WCon{a4_28, WCon{a4_29, WCon{a4_30, WCon{a4_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a5_0, WCon{a5_1, WCon{a5_2, WCon{a5_3, WCon{a5_4, WCon{a5_5, WCon{a5_6, WCon{a5_7, WCon{a5_8, WCon{a5_9, WCon{a5_10, WCon{a5_11, WCon{a5_12, WCon{a5_13, WCon{a5_14, WCon{a5_15, WCon{a5_16, WCon{a5_17, WCon{a5_18, WCon{a5_19, WCon{a5_20, WCon{a5_21, WCon{a5_22, WCon{a5_23, WCon{a5_24, WCon{a5_25, WCon{a5_26, WCon{a5_27, WCon{a5_28, WCon{a5_29, WCon{a5_30, WCon{a5_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a6_0, WCon{a6_1, WCon{a6_2, WCon{a6_3, WCon{a6_4, WCon{a6_5, WCon{a6_6, WCon{a6_7, WCon{a6_8, WCon{a6_9, WCon{a6_10, WCon{a6_11, WCon{a6_12, WCon{a6_13, WCon{a6_14, WCon{a6_15, WCon{a6_16, WCon{a6_17, WCon{a6_18, WCon{a6_19, WCon{a6_20, WCon{a6_21, WCon{a6_22, WCon{a6_23, WCon{a6_24, WCon{a6_25, WCon{a6_26, WCon{a6_27, WCon{a6_28, WCon{a6_29, WCon{a6_30, WCon{a6_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a7_0, WCon{a7_1, WCon{a7_2, WCon{a7_3, WCon{a7_4, WCon{a7_5, WCon{a7_6, WCon{a7_7, WCon{a7_8, WCon{a7_9, WCon{a7_10, WCon{a7_11, WCon{a7_12, WCon{a7_13, WCon{a7_14, WCon{a7_15, WCon{a7_16, WCon{a7_17, WCon{a7_18, WCon{a7_19, WCon{a7_20, WCon{a7_21, WCon{a7_22, WCon{a7_23, WCon{a7_24, WCon{a7_25, WCon{a7_26, WCon{a7_27, WCon{a7_28, WCon{a7_29, WCon{a7_30, WCon{a7_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a8_0, WCon{a8_1, WCon{a8_2, WCon{a8_3, WCon{a8_4, WCon{a8_5, WCon{a8_6, WCon{a8_7, WCon{a8_8, WCon{a8_9, WCon{a8_10, WCon{a8_11, WCon{a8_12, WCon{a8_13, WCon{a8_14, WCon{a8_15, WCon{a8_16, WCon{a8_17, WCon{a8_18, WCon{a8_19, WCon{a8_20, WCon{a8_21, WCon{a8_22, WCon{a8_23, WCon{a8_24, WCon{a8_25, WCon{a8_26, WCon{a8_27, WCon{a8_28, WCon{a8_29, WCon{a8_30, WCon{a8_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a9_0, WCon{a9_1, WCon{a9_2, WCon{a9_3, WCon{a9_4, WCon{a9_5, WCon{a9_6, WCon{a9_7, WCon{a9_8, WCon{a9_9, WCon{a9_10, WCon{a9_11, WCon{a9_12, WCon{a9_13, WCon{a9_14, WCon{a9_15, WCon{a9_16, WCon{a9_17, WCon{a9_18, WCon{a9_19, WCon{a9_20, WCon{a9_21, WCon{a9_22, WCon{a9_23, WCon{a9_24, WCon{a9_25, WCon{a9_26, WCon{a9_27, WCon{a9_28, WCon{a9_29, WCon{a9_30, WCon{a9_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a10_0, WCon{a10_1, WCon{a10_2, WCon{a10_3, WCon{a10_4, WCon{a10_5, WCon{a10_6, WCon{a10_7, WCon{a10_8, WCon{a10_9, WCon{a10_10, WCon{a10_11, WCon{a10_12, WCon{a10_13, WCon{a10_14, WCon{a10_15, WCon{a10_16, WCon{a10_17, WCon{a10_18, WCon{a10_19, WCon{a10_20, WCon{a10_21, WCon{a10_22, WCon{a10_23, WCon{a10_24, WCon{a10_25, WCon{a10_26, WCon{a10_27, WCon{a10_28, WCon{a10_29, WCon{a10_30, WCon{a10_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a11_0, WCon{a11_1, WCon{a11_2, WCon{a11_3, WCon{a11_4, WCon{a11_5, WCon{a11_6, WCon{a11_7, WCon{a11_8, WCon{a11_9, WCon{a11_10, WCon{a11_11, WCon{a11_12, WCon{a11_13, WCon{a11_14, WCon{a11_15, WCon{a11_16, WCon{a11_17, WCon{a11_18, WCon{a11_19, WCon{a11_20, WCon{a11_21, WCon{a11_22, WCon{a11_23, WCon{a11_24, WCon{a11_25, WCon{a11_26, WCon{a11_27, WCon{a11_28, WCon{a11_29, WCon{a11_30, WCon{a11_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a12_0, WCon{a12_1, WCon{a12_2, WCon{a12_3, WCon{a12_4, WCon{a12_5, WCon{a12_6, WCon{a12_7, WCon{a12_8, WCon{a12_9, WCon{a12_10, WCon{a12_11, WCon{a12_12, WCon{a12_13, WCon{a12_14, WCon{a12_15, WCon{a12_16, WCon{a12_17, WCon{a12_18, WCon{a12_19, WCon{a12_20, WCon{a12_21, WCon{a12_22, WCon{a12_23, WCon{a12_24, WCon{a12_25, WCon{a12_26, WCon{a12_27, WCon{a12_28, WCon{a12_29, WCon{a12_30, WCon{a12_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a13_0, WCon{a13_1, WCon{a13_2, WCon{a13_3, WCon{a13_4, WCon{a13_5, WCon{a13_6, WCon{a13_7, WCon{a13_8, WCon{a13_9, WCon{a13_10, WCon{a13_11, WCon{a13_12, WCon{a13_13, WCon{a13_14, WCon{a13_15, WCon{a13_16, WCon{a13_17, WCon{a13_18, WCon{a13_19, WCon{a13_20, WCon{a13_21, WCon{a13_22, WCon{a13_23, WCon{a13_24, WCon{a13_25, WCon{a13_26, WCon{a13_27, WCon{a13_28, WCon{a13_29, WCon{a13_30, WCon{a13_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a14_0, WCon{a14_1, WCon{a14_2, WCon{a14_3, WCon{a14_4, WCon{a14_5, WCon{a14_6, WCon{a14_7, WCon{a14_8, WCon{a14_9, WCon{a14_10, WCon{a14_11, WCon{a14_12, WCon{a14_13, WCon{a14_14, WCon{a14_15, WCon{a14_16, WCon{a14_17, WCon{a14_18, WCon{a14_19, WCon{a14_20, WCon{a14_21, WCon{a14_22, WCon{a14_23, WCon{a14_24, WCon{a14_25, WCon{a14_26, WCon{a14_27, WCon{a14_28, WCon{a14_29, WCon{a14_30, WCon{a14_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{a15_0, WCon{a15_1, WCon{a15_2, WCon{a15_3, WCon{a15_4, WCon{a15_5, WCon{a15_6, WCon{a15_7, WCon{a15_8, WCon{a15_9, WCon{a15_10, WCon{a15_11, WCon{a15_12, WCon{a15_13, WCon{a15_14, WCon{a15_15, WCon{a15_16, WCon{a15_17, WCon{a15_18, WCon{a15_19, WCon{a15_20, WCon{a15_21, WCon{a15_22, WCon{a15_23, WCon{a15_24, WCon{a15_25, WCon{a15_26, WCon{a15_27, WCon{a15_28, WCon{a15_29, WCon{a15_30, WCon{a15_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
157      {==}