def bb16

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/aead.bend:374

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G

374def bb16(+w: Word(128n)) -> {G.block_bytes(w) == [S.nth_byte(G.block_bytes(w), 0n), S.nth_byte(G.block_bytes(w), 1n), S.nth_byte(G.block_bytes(w), 2n), S.nth_byte(G.block_bytes(w), 3n), S.nth_byte(G.block_bytes(w), 4n), S.nth_byte(G.block_bytes(w), 5n), S.nth_byte(G.block_bytes(w), 6n), S.nth_byte(G.block_bytes(w), 7n), S.nth_byte(G.block_bytes(w), 8n), S.nth_byte(G.block_bytes(w), 9n), S.nth_byte(G.block_bytes(w), 10n), S.nth_byte(G.block_bytes(w), 11n), S.nth_byte(G.block_bytes(w), 12n), S.nth_byte(G.block_bytes(w), 13n), S.nth_byte(G.block_bytes(w), 14n), S.nth_byte(G.block_bytes(w), 15n)] : List<&2, U32>}:
375  match w:
376    case WCon{w0, WCon{w1, WCon{w2, WCon{w3, WCon{w4, WCon{w5, WCon{w6, WCon{w7, WCon{w8, WCon{w9, WCon{w10, WCon{w11, WCon{w12, WCon{w13, WCon{w14, WCon{w15, WCon{w16, WCon{w17, WCon{w18, WCon{w19, WCon{w20, WCon{w21, WCon{w22, WCon{w23, WCon{w24, WCon{w25, WCon{w26, WCon{w27, WCon{w28, WCon{w29, WCon{w30, WCon{w31, WCon{w32, WCon{w33, WCon{w34, WCon{w35, WCon{w36, WCon{w37, WCon{w38, WCon{w39, WCon{w40, WCon{w41, WCon{w42, WCon{w43, WCon{w44, WCon{w45, WCon{w46, WCon{w47, WCon{w48, WCon{w49, WCon{w50, WCon{w51, WCon{w52, WCon{w53, WCon{w54, WCon{w55, WCon{w56, WCon{w57, WCon{w58, WCon{w59, WCon{w60, WCon{w61, WCon{w62, WCon{w63, WCon{w64, WCon{w65, WCon{w66, WCon{w67, WCon{w68, WCon{w69, WCon{w70, WCon{w71, WCon{w72, WCon{w73, WCon{w74, WCon{w75, WCon{w76, WCon{w77, WCon{w78, WCon{w79, WCon{w80, WCon{w81, WCon{w82, WCon{w83, WCon{w84, WCon{w85, WCon{w86, WCon{w87, WCon{w88, WCon{w89, WCon{w90, WCon{w91, WCon{w92, WCon{w93, WCon{w94, WCon{w95, WCon{w96, WCon{w97, WCon{w98, WCon{w99, WCon{w100, WCon{w101, WCon{w102, WCon{w103, WCon{w104, WCon{w105, WCon{w106, WCon{w107, WCon{w108, WCon{w109, WCon{w110, WCon{w111, WCon{w112, WCon{w113, WCon{w114, WCon{w115, WCon{w116, WCon{w117, WCon{w118, WCon{w119, WCon{w120, WCon{w121, WCon{w122, WCon{w123, WCon{w124, WCon{w125, WCon{w126, WCon{w127, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}:
377      {==}