def bb_ok
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash_bits.bend:159
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as GhashBits
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
159def bb_ok(+s: I.Block) -> {G.block_bytes(D.R(s)) == I.unpack(s) : List<&2, U32>}:
160 match s:
161 case I.B{U32{WCon{s0_0, WCon{s0_1, WCon{s0_2, WCon{s0_3, WCon{s0_4, WCon{s0_5, WCon{s0_6, WCon{s0_7, WCon{s0_8, WCon{s0_9, WCon{s0_10, WCon{s0_11, WCon{s0_12, WCon{s0_13, WCon{s0_14, WCon{s0_15, WCon{s0_16, WCon{s0_17, WCon{s0_18, WCon{s0_19, WCon{s0_20, WCon{s0_21, WCon{s0_22, WCon{s0_23, WCon{s0_24, WCon{s0_25, WCon{s0_26, WCon{s0_27, WCon{s0_28, WCon{s0_29, WCon{s0_30, WCon{s0_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s1_0, WCon{s1_1, WCon{s1_2, WCon{s1_3, WCon{s1_4, WCon{s1_5, WCon{s1_6, WCon{s1_7, WCon{s1_8, WCon{s1_9, WCon{s1_10, WCon{s1_11, WCon{s1_12, WCon{s1_13, WCon{s1_14, WCon{s1_15, WCon{s1_16, WCon{s1_17, WCon{s1_18, WCon{s1_19, WCon{s1_20, WCon{s1_21, WCon{s1_22, WCon{s1_23, WCon{s1_24, WCon{s1_25, WCon{s1_26, WCon{s1_27, WCon{s1_28, WCon{s1_29, WCon{s1_30, WCon{s1_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s2_0, WCon{s2_1, WCon{s2_2, WCon{s2_3, WCon{s2_4, WCon{s2_5, WCon{s2_6, WCon{s2_7, WCon{s2_8, WCon{s2_9, WCon{s2_10, WCon{s2_11, WCon{s2_12, WCon{s2_13, WCon{s2_14, WCon{s2_15, WCon{s2_16, WCon{s2_17, WCon{s2_18, WCon{s2_19, WCon{s2_20, WCon{s2_21, WCon{s2_22, WCon{s2_23, WCon{s2_24, WCon{s2_25, WCon{s2_26, WCon{s2_27, WCon{s2_28, WCon{s2_29, WCon{s2_30, WCon{s2_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}, U32{WCon{s3_0, WCon{s3_1, WCon{s3_2, WCon{s3_3, WCon{s3_4, WCon{s3_5, WCon{s3_6, WCon{s3_7, WCon{s3_8, WCon{s3_9, WCon{s3_10, WCon{s3_11, WCon{s3_12, WCon{s3_13, WCon{s3_14, WCon{s3_15, WCon{s3_16, WCon{s3_17, WCon{s3_18, WCon{s3_19, WCon{s3_20, WCon{s3_21, WCon{s3_22, WCon{s3_23, WCon{s3_24, WCon{s3_25, WCon{s3_26, WCon{s3_27, WCon{s3_28, WCon{s3_29, WCon{s3_30, WCon{s3_31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
162 {==}