def block_xor_ok

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

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/poly.bend as P
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

101def block_xor_ok(+y0: U32, +y1: U32, +y2: U32, +y3: U32, +x0: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32, +x5: U32, +x6: U32, +x7: U32, +x8: U32, +x9: U32, +x10: U32, +x11: U32, +x12: U32, +x13: U32, +x14: U32, +x15: U32) -> {P.coefficients(128n, Word.xor(128n, D.R(I.B{y0, y1, y2, y3}), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]))) == G.string_bits(I.xor_bytes(I.unpack(I.B{y0, y1, y2, y3}), [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])) : List<&2, Bool>}:
102  match y0 y1 y2 y3 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15:
103    case U32{WCon{y0_0, WCon{y0_1, WCon{y0_2, WCon{y0_3, WCon{y0_4, WCon{y0_5, WCon{y0_6, WCon{y0_7, WCon{y0_8, WCon{y0_9, WCon{y0_10, WCon{y0_11, WCon{y0_12, WCon{y0_13, WCon{y0_14, WCon{y0_15, WCon{y0_16, WCon{y0_17, WCon{y0_18, WCon{y0_19, WCon{y0_20, WCon{y0_21, WCon{y0_22, WCon{y0_23, WCon{y0_24, WCon{y0_25, WCon{y0_26, WCon{y0_27, WCon{y0_28, WCon{y0_29, WCon{y0_30, WCon{y0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y1_0, WCon{y1_1, WCon{y1_2, WCon{y1_3, WCon{y1_4, WCon{y1_5, WCon{y1_6, WCon{y1_7, WCon{y1_8, WCon{y1_9, WCon{y1_10, WCon{y1_11, WCon{y1_12, WCon{y1_13, WCon{y1_14, WCon{y1_15, WCon{y1_16, WCon{y1_17, WCon{y1_18, WCon{y1_19, WCon{y1_20, WCon{y1_21, WCon{y1_22, WCon{y1_23, WCon{y1_24, WCon{y1_25, WCon{y1_26, WCon{y1_27, WCon{y1_28, WCon{y1_29, WCon{y1_30, WCon{y1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y2_0, WCon{y2_1, WCon{y2_2, WCon{y2_3, WCon{y2_4, WCon{y2_5, WCon{y2_6, WCon{y2_7, WCon{y2_8, WCon{y2_9, WCon{y2_10, WCon{y2_11, WCon{y2_12, WCon{y2_13, WCon{y2_14, WCon{y2_15, WCon{y2_16, WCon{y2_17, WCon{y2_18, WCon{y2_19, WCon{y2_20, WCon{y2_21, WCon{y2_22, WCon{y2_23, WCon{y2_24, WCon{y2_25, WCon{y2_26, WCon{y2_27, WCon{y2_28, WCon{y2_29, WCon{y2_30, WCon{y2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{y3_0, WCon{y3_1, WCon{y3_2, WCon{y3_3, WCon{y3_4, WCon{y3_5, WCon{y3_6, WCon{y3_7, WCon{y3_8, WCon{y3_9, WCon{y3_10, WCon{y3_11, WCon{y3_12, WCon{y3_13, WCon{y3_14, WCon{y3_15, WCon{y3_16, WCon{y3_17, WCon{y3_18, WCon{y3_19, WCon{y3_20, WCon{y3_21, WCon{y3_22, WCon{y3_23, WCon{y3_24, WCon{y3_25, WCon{y3_26, WCon{y3_27, WCon{y3_28, WCon{y3_29, WCon{y3_30, WCon{y3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x0_0, WCon{x0_1, WCon{x0_2, WCon{x0_3, WCon{x0_4, WCon{x0_5, WCon{x0_6, WCon{x0_7, WCon{x0_8, WCon{x0_9, WCon{x0_10, WCon{x0_11, WCon{x0_12, WCon{x0_13, WCon{x0_14, WCon{x0_15, WCon{x0_16, WCon{x0_17, WCon{x0_18, WCon{x0_19, WCon{x0_20, WCon{x0_21, WCon{x0_22, WCon{x0_23, WCon{x0_24, WCon{x0_25, WCon{x0_26, WCon{x0_27, WCon{x0_28, WCon{x0_29, WCon{x0_30, WCon{x0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x1_0, WCon{x1_1, WCon{x1_2, WCon{x1_3, WCon{x1_4, WCon{x1_5, WCon{x1_6, WCon{x1_7, WCon{x1_8, WCon{x1_9, WCon{x1_10, WCon{x1_11, WCon{x1_12, WCon{x1_13, WCon{x1_14, WCon{x1_15, WCon{x1_16, WCon{x1_17, WCon{x1_18, WCon{x1_19, WCon{x1_20, WCon{x1_21, WCon{x1_22, WCon{x1_23, WCon{x1_24, WCon{x1_25, WCon{x1_26, WCon{x1_27, WCon{x1_28, WCon{x1_29, WCon{x1_30, WCon{x1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x2_0, WCon{x2_1, WCon{x2_2, WCon{x2_3, WCon{x2_4, WCon{x2_5, WCon{x2_6, WCon{x2_7, WCon{x2_8, WCon{x2_9, WCon{x2_10, WCon{x2_11, WCon{x2_12, WCon{x2_13, WCon{x2_14, WCon{x2_15, WCon{x2_16, WCon{x2_17, WCon{x2_18, WCon{x2_19, WCon{x2_20, WCon{x2_21, WCon{x2_22, WCon{x2_23, WCon{x2_24, WCon{x2_25, WCon{x2_26, WCon{x2_27, WCon{x2_28, WCon{x2_29, WCon{x2_30, WCon{x2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x3_0, WCon{x3_1, WCon{x3_2, WCon{x3_3, WCon{x3_4, WCon{x3_5, WCon{x3_6, WCon{x3_7, WCon{x3_8, WCon{x3_9, WCon{x3_10, WCon{x3_11, WCon{x3_12, WCon{x3_13, WCon{x3_14, WCon{x3_15, WCon{x3_16, WCon{x3_17, WCon{x3_18, WCon{x3_19, WCon{x3_20, WCon{x3_21, WCon{x3_22, WCon{x3_23, WCon{x3_24, WCon{x3_25, WCon{x3_26, WCon{x3_27, WCon{x3_28, WCon{x3_29, WCon{x3_30, WCon{x3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x4_0, WCon{x4_1, WCon{x4_2, WCon{x4_3, WCon{x4_4, WCon{x4_5, WCon{x4_6, WCon{x4_7, WCon{x4_8, WCon{x4_9, WCon{x4_10, WCon{x4_11, WCon{x4_12, WCon{x4_13, WCon{x4_14, WCon{x4_15, WCon{x4_16, WCon{x4_17, WCon{x4_18, WCon{x4_19, WCon{x4_20, WCon{x4_21, WCon{x4_22, WCon{x4_23, WCon{x4_24, WCon{x4_25, WCon{x4_26, WCon{x4_27, WCon{x4_28, WCon{x4_29, WCon{x4_30, WCon{x4_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x5_0, WCon{x5_1, WCon{x5_2, WCon{x5_3, WCon{x5_4, WCon{x5_5, WCon{x5_6, WCon{x5_7, WCon{x5_8, WCon{x5_9, WCon{x5_10, WCon{x5_11, WCon{x5_12, WCon{x5_13, WCon{x5_14, WCon{x5_15, WCon{x5_16, WCon{x5_17, WCon{x5_18, WCon{x5_19, WCon{x5_20, WCon{x5_21, WCon{x5_22, WCon{x5_23, WCon{x5_24, WCon{x5_25, WCon{x5_26, WCon{x5_27, WCon{x5_28, WCon{x5_29, WCon{x5_30, WCon{x5_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x6_0, WCon{x6_1, WCon{x6_2, WCon{x6_3, WCon{x6_4, WCon{x6_5, WCon{x6_6, WCon{x6_7, WCon{x6_8, WCon{x6_9, WCon{x6_10, WCon{x6_11, WCon{x6_12, WCon{x6_13, WCon{x6_14, WCon{x6_15, WCon{x6_16, WCon{x6_17, WCon{x6_18, WCon{x6_19, WCon{x6_20, WCon{x6_21, WCon{x6_22, WCon{x6_23, WCon{x6_24, WCon{x6_25, WCon{x6_26, WCon{x6_27, WCon{x6_28, WCon{x6_29, WCon{x6_30, WCon{x6_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x7_0, WCon{x7_1, WCon{x7_2, WCon{x7_3, WCon{x7_4, WCon{x7_5, WCon{x7_6, WCon{x7_7, WCon{x7_8, WCon{x7_9, WCon{x7_10, WCon{x7_11, WCon{x7_12, WCon{x7_13, WCon{x7_14, WCon{x7_15, WCon{x7_16, WCon{x7_17, WCon{x7_18, WCon{x7_19, WCon{x7_20, WCon{x7_21, WCon{x7_22, WCon{x7_23, WCon{x7_24, WCon{x7_25, WCon{x7_26, WCon{x7_27, WCon{x7_28, WCon{x7_29, WCon{x7_30, WCon{x7_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x8_0, WCon{x8_1, WCon{x8_2, WCon{x8_3, WCon{x8_4, WCon{x8_5, WCon{x8_6, WCon{x8_7, WCon{x8_8, WCon{x8_9, WCon{x8_10, WCon{x8_11, WCon{x8_12, WCon{x8_13, WCon{x8_14, WCon{x8_15, WCon{x8_16, WCon{x8_17, WCon{x8_18, WCon{x8_19, WCon{x8_20, WCon{x8_21, WCon{x8_22, WCon{x8_23, WCon{x8_24, WCon{x8_25, WCon{x8_26, WCon{x8_27, WCon{x8_28, WCon{x8_29, WCon{x8_30, WCon{x8_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x9_0, WCon{x9_1, WCon{x9_2, WCon{x9_3, WCon{x9_4, WCon{x9_5, WCon{x9_6, WCon{x9_7, WCon{x9_8, WCon{x9_9, WCon{x9_10, WCon{x9_11, WCon{x9_12, WCon{x9_13, WCon{x9_14, WCon{x9_15, WCon{x9_16, WCon{x9_17, WCon{x9_18, WCon{x9_19, WCon{x9_20, WCon{x9_21, WCon{x9_22, WCon{x9_23, WCon{x9_24, WCon{x9_25, WCon{x9_26, WCon{x9_27, WCon{x9_28, WCon{x9_29, WCon{x9_30, WCon{x9_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x10_0, WCon{x10_1, WCon{x10_2, WCon{x10_3, WCon{x10_4, WCon{x10_5, WCon{x10_6, WCon{x10_7, WCon{x10_8, WCon{x10_9, WCon{x10_10, WCon{x10_11, WCon{x10_12, WCon{x10_13, WCon{x10_14, WCon{x10_15, WCon{x10_16, WCon{x10_17, WCon{x10_18, WCon{x10_19, WCon{x10_20, WCon{x10_21, WCon{x10_22, WCon{x10_23, WCon{x10_24, WCon{x10_25, WCon{x10_26, WCon{x10_27, WCon{x10_28, WCon{x10_29, WCon{x10_30, WCon{x10_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x11_0, WCon{x11_1, WCon{x11_2, WCon{x11_3, WCon{x11_4, WCon{x11_5, WCon{x11_6, WCon{x11_7, WCon{x11_8, WCon{x11_9, WCon{x11_10, WCon{x11_11, WCon{x11_12, WCon{x11_13, WCon{x11_14, WCon{x11_15, WCon{x11_16, WCon{x11_17, WCon{x11_18, WCon{x11_19, WCon{x11_20, WCon{x11_21, WCon{x11_22, WCon{x11_23, WCon{x11_24, WCon{x11_25, WCon{x11_26, WCon{x11_27, WCon{x11_28, WCon{x11_29, WCon{x11_30, WCon{x11_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x12_0, WCon{x12_1, WCon{x12_2, WCon{x12_3, WCon{x12_4, WCon{x12_5, WCon{x12_6, WCon{x12_7, WCon{x12_8, WCon{x12_9, WCon{x12_10, WCon{x12_11, WCon{x12_12, WCon{x12_13, WCon{x12_14, WCon{x12_15, WCon{x12_16, WCon{x12_17, WCon{x12_18, WCon{x12_19, WCon{x12_20, WCon{x12_21, WCon{x12_22, WCon{x12_23, WCon{x12_24, WCon{x12_25, WCon{x12_26, WCon{x12_27, WCon{x12_28, WCon{x12_29, WCon{x12_30, WCon{x12_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x13_0, WCon{x13_1, WCon{x13_2, WCon{x13_3, WCon{x13_4, WCon{x13_5, WCon{x13_6, WCon{x13_7, WCon{x13_8, WCon{x13_9, WCon{x13_10, WCon{x13_11, WCon{x13_12, WCon{x13_13, WCon{x13_14, WCon{x13_15, WCon{x13_16, WCon{x13_17, WCon{x13_18, WCon{x13_19, WCon{x13_20, WCon{x13_21, WCon{x13_22, WCon{x13_23, WCon{x13_24, WCon{x13_25, WCon{x13_26, WCon{x13_27, WCon{x13_28, WCon{x13_29, WCon{x13_30, WCon{x13_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x14_0, WCon{x14_1, WCon{x14_2, WCon{x14_3, WCon{x14_4, WCon{x14_5, WCon{x14_6, WCon{x14_7, WCon{x14_8, WCon{x14_9, WCon{x14_10, WCon{x14_11, WCon{x14_12, WCon{x14_13, WCon{x14_14, WCon{x14_15, WCon{x14_16, WCon{x14_17, WCon{x14_18, WCon{x14_19, WCon{x14_20, WCon{x14_21, WCon{x14_22, WCon{x14_23, WCon{x14_24, WCon{x14_25, WCon{x14_26, WCon{x14_27, WCon{x14_28, WCon{x14_29, WCon{x14_30, WCon{x14_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} U32{WCon{x15_0, WCon{x15_1, WCon{x15_2, WCon{x15_3, WCon{x15_4, WCon{x15_5, WCon{x15_6, WCon{x15_7, WCon{x15_8, WCon{x15_9, WCon{x15_10, WCon{x15_11, WCon{x15_12, WCon{x15_13, WCon{x15_14, WCon{x15_15, WCon{x15_16, WCon{x15_17, WCon{x15_18, WCon{x15_19, WCon{x15_20, WCon{x15_21, WCon{x15_22, WCon{x15_23, WCon{x15_24, WCon{x15_25, WCon{x15_26, WCon{x15_27, WCon{x15_28, WCon{x15_29, WCon{x15_30, WCon{x15_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
104      {==}