proofs/crypto/aes/ghash.bend

bend-collections-laws-crypto@1.0.0.0 · 150 lines · 10 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as A
4import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as I
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as P
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S
7import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
8import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend as GF
9import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as D
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as B
11
12# Generated by tools/generators/aes/ghash.py.
13
14# The implementation's GHASH (Algorithm 1 on four U32 words, bit by bit)
15# equals SP 800-38D's GHASH over the field GF(2^128), block by block.
16
17# One bit of Algorithm 1: Z += c*V, V = V*x.
18def step_ok(+c: Bool, +z: I.Block, +v: I.Block, +rest: List<&2, Bool>) -> {D.F(I.Acc{z, v}, c <> rest) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}:
19  %B.zstep_ok(c, z, v) : {GF.sa(128n, G.low(), rest, _, P.times_x(128n, G.low(), D.R(v))) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}
20  %B.mulx_ok(v) : {GF.sa(128n, G.low(), rest, D.R(I.add_masked(D.bit(c), z, v)), _) == D.F(I.step(D.bit(c), I.Acc{z, v}), rest) : Word(128n)}
21  {==}
22
23def steps_ok(+cs: List<&2, Bool>, +acc: I.Acc, +rest: List<&2, Bool>) -> {D.F(acc, List.append(&2, Bool, cs, rest)) == D.F(D.steps(cs, acc), rest) : Word(128n)}:
24  match cs:
25    case Nil{}:
26      {==}
27    case c <> r:
28      match acc:
29        case I.Acc{z, v}:
30          Equal.trans(Word(128n), D.F(I.Acc{z, v}, c <> List.append(&2, Bool, r, rest)), D.F(I.step(D.bit(c), I.Acc{z, v}), List.append(&2, Bool, r, rest)), D.F(D.steps(r, I.step(D.bit(c), I.Acc{z, v})), rest),
31            step_ok(c, z, v, List.append(&2, Bool, r, rest)), steps_ok(r, I.step(D.bit(c), I.Acc{z, v}), rest))
32
33def steps_append(+l1: List<&2, Bool>, +l2: List<&2, Bool>, +acc: I.Acc) -> {D.steps(List.append(&2, Bool, l1, l2), acc) == D.steps(l2, D.steps(l1, acc)) : I.Acc}:
34  match l1:
35    case Nil{}:
36      {==}
37    case c <> r:
38      steps_append(r, l2, I.step(D.bit(c), acc))
39
40def mul_bytes_steps(+xs: List<&2, U32>, +acc: I.Acc) -> {I.mul_bytes(xs, acc) == D.steps(G.string_bits(xs), acc) : I.Acc}:
41  match xs:
42    case Nil{}:
43      {==}
44    case x <> rest:
45      %Equal.sym(I.Acc, D.steps(List.append(&2, Bool, G.byte_bits(x), G.string_bits(rest)), acc), D.steps(G.string_bits(rest), D.steps(G.byte_bits(x), acc)), steps_append(G.byte_bits(x), G.string_bits(rest), acc)) : {I.mul_bytes(rest, I.mul_byte(x, acc)) == _ : I.Acc}
46      %B.mul_byte_steps(x, acc) : {I.mul_bytes(rest, I.mul_byte(x, acc)) == D.steps(G.string_bits(rest), _) : I.Acc}
47      mul_bytes_steps(rest, I.mul_byte(x, acc))
48
49def append_nil(+l: List<&2, Bool>) -> {List.append(&2, Bool, l, Nil{}) == l : List<&2, Bool>}:
50  match l:
51    case Nil{}:
52      {==}
53    case c <> r:
54      %append_nil(r) : {c <> List.append(&2, Bool, r, Nil{}) == c <> _ : List<&2, Bool>}
55      {==}
56
57def f_nil(+acc: I.Acc) -> {D.F(acc, Nil{}) == D.R(I.acc_z(acc)) : Word(128n)}:
58  match acc:
59    case I.Acc{z, v}:
60      {==}
61
62# (Y xor X) * H for one 16-byte block.
63def absorb_ok(+h: I.Block, +y: I.Block, +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) -> {D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])) == G.mul(Word.xor(128n, D.R(y), G.block([x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])), D.R(h)) : Word(128n)}:
64  match y:
65    case I.B{y0, y1, y2, y3}:
66      %Equal.sym(Word(128n), G.mul(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])), D.R(h)), GF.sa(128n, G.low(), 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]))), Word.zero(128n), D.R(h)), GF.mul_sa(128n, G.low(), 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])), D.R(h))) : {D.R(I.acc_z(I.mul_bytes(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]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
67      %Equal.sym(List<&2, Bool>, 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])), B.block_xor_ok(y0, y1, y2, y3, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)) : {D.R(I.acc_z(I.mul_bytes(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]), I.Acc{I.zero(), h}))) == GF.sa(128n, G.low(), _, Word.zero(128n), D.R(h)) : Word(128n)}
68      %Equal.cong(List<&2, Bool>, Word(128n), l => D.F(I.Acc{I.zero(), h}, l), List.append(&2, Bool, 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])), Nil{}), 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])), append_nil(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])))) : {D.R(I.acc_z(I.mul_bytes(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]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
69      %Equal.sym(Word(128n), D.F(I.Acc{I.zero(), h}, List.append(&2, Bool, 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])), Nil{})), D.F(D.steps(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])), I.Acc{I.zero(), h}), Nil{}), steps_ok(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])), I.Acc{I.zero(), h}, Nil{})) : {D.R(I.acc_z(I.mul_bytes(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]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
70      %Equal.sym(Word(128n), D.F(D.steps(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])), I.Acc{I.zero(), h}), Nil{}), D.R(I.acc_z(D.steps(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])), I.Acc{I.zero(), h}))), f_nil(D.steps(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])), I.Acc{I.zero(), h}))) : {D.R(I.acc_z(I.mul_bytes(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]), I.Acc{I.zero(), h}))) == _ : Word(128n)}
71      %mul_bytes_steps(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]), I.Acc{I.zero(), h}) : {D.R(I.acc_z(I.mul_bytes(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]), I.Acc{I.zero(), h}))) == D.R(I.acc_z(_)) : Word(128n)}
72      {==}
73
74# GHASH over X || 0^v (then more blocks) is the implementation's GHASH over X.
75def ghash_ok(+h: I.Block, +xs: List<&2, U32>, +rest: List<&2, U32>, +y: I.Block) -> {G.ghash(D.R(h), List.append(&2, U32, G.pad(xs), rest), D.R(y)) == G.ghash(D.R(h), rest, D.R(I.ghash(h, xs, y))) : Word(128n)}:
76  match xs:
77    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> x15 <> xr:
78      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) : {G.ghash(D.R(h), List.append(&2, U32, G.pad(xr), rest), _) == G.ghash(D.R(h), rest, D.R(I.ghash(h, xr, I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15])))) : Word(128n)}
79      ghash_ok(h, xr, rest, I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15]))
80    case Nil{}:
81      {==}
82    case x0 <> Nil{}:
83      %absorb_ok(h, y, x0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
84      {==}
85    case x0 <> x1 <> Nil{}:
86      %absorb_ok(h, y, x0, x1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
87      {==}
88    case x0 <> x1 <> x2 <> Nil{}:
89      %absorb_ok(h, y, x0, x1, x2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
90      {==}
91    case x0 <> x1 <> x2 <> x3 <> Nil{}:
92      %absorb_ok(h, y, x0, x1, x2, x3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
93      {==}
94    case x0 <> x1 <> x2 <> x3 <> x4 <> Nil{}:
95      %absorb_ok(h, y, x0, x1, x2, x3, x4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
96      {==}
97    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> Nil{}:
98      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
99      {==}
100    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> Nil{}:
101      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, 0, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
102      {==}
103    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> Nil{}:
104      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, 0, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, 0, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
105      {==}
106    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> Nil{}:
107      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, 0, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, 0, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
108      {==}
109    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> Nil{}:
110      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, 0, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, 0, 0, 0, 0, 0, 0]))) : Word(128n)}
111      {==}
112    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> Nil{}:
113      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, 0, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, 0, 0, 0, 0, 0]))) : Word(128n)}
114      {==}
115    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> Nil{}:
116      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, 0, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, 0, 0, 0, 0]))) : Word(128n)}
117      {==}
118    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> Nil{}:
119      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, 0, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, 0, 0, 0]))) : Word(128n)}
120      {==}
121    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> Nil{}:
122      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, 0, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, 0, 0]))) : Word(128n)}
123      {==}
124    case x0 <> x1 <> x2 <> x3 <> x4 <> x5 <> x6 <> x7 <> x8 <> x9 <> x10 <> x11 <> x12 <> x13 <> x14 <> Nil{}:
125      %absorb_ok(h, y, x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, 0) : {G.ghash(D.R(h), rest, _) == G.ghash(D.R(h), rest, D.R(I.absorb(h, y, [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, 0]))) : Word(128n)}
126      {==}
127
128# GHASH_H(A || 0^v || C || 0^u || [len(A)]_64 || [len(C)]_64).
129def ghash_all_ok(+h: I.Block, +aad: List<&2, U32>, +c: List<&2, U32>) -> {G.ghash(D.R(h), List.append(&2, U32, G.pad(aad), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c)))), Word.zero(128n)) == D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))) : Word(128n)}:
130  Equal.trans(Word(128n),
131    G.ghash(D.R(h), List.append(&2, U32, G.pad(aad), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c)))), D.R(I.zero())),
132    G.ghash(D.R(h), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), D.R(I.ghash(h, aad, I.zero()))),
133    D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))),
134    ghash_ok(h, aad, List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), I.zero()),
135    Equal.trans(Word(128n),
136      G.ghash(D.R(h), List.append(&2, U32, G.pad(c), List.append(&2, U32, G.len64(aad), G.len64(c))), D.R(I.ghash(h, aad, I.zero()))),
137      G.ghash(D.R(h), List.append(&2, U32, G.len64(aad), G.len64(c)), D.R(I.ghash(h, c, I.ghash(h, aad, I.zero())))),
138      D.R(I.ghash(h, I.lengths(aad, c), I.ghash(h, c, I.ghash(h, aad, I.zero())))),
139      ghash_ok(h, c, List.append(&2, U32, G.len64(aad), G.len64(c)), I.ghash(h, aad, I.zero())),
140      ghash_ok(h, I.lengths(aad, c), Nil{}, I.ghash(h, c, I.ghash(h, aad, I.zero())))))
141
142# The hash subkey: the implementation packs E_K(0^128) into words.
143def pack_ok(+st: T.State) -> {D.R(I.pack(st)) == G.block(S.bytes_of(st)) : Word(128n)}:
144  match st:
145    case T.S{T.W{a0, a1, a2, a3}, T.W{a4, a5, a6, a7}, T.W{a8, a9, a10, a11}, T.W{a12, a13, a14, a15}}:
146      %Equal.sym(U32, I.word(T.W{a0, a1, a2, a3}), G.int32(a0, a1, a2, a3), B.word_ok(a0, a1, a2, a3)) : {D.R(I.B{_, I.word(T.W{a4, a5, a6, a7}), I.word(T.W{a8, a9, a10, a11}), I.word(T.W{a12, a13, a14, a15})}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
147      %Equal.sym(U32, I.word(T.W{a4, a5, a6, a7}), G.int32(a4, a5, a6, a7), B.word_ok(a4, a5, a6, a7)) : {D.R(I.B{G.int32(a0, a1, a2, a3), _, I.word(T.W{a8, a9, a10, a11}), I.word(T.W{a12, a13, a14, a15})}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
148      %Equal.sym(U32, I.word(T.W{a8, a9, a10, a11}), G.int32(a8, a9, a10, a11), B.word_ok(a8, a9, a10, a11)) : {D.R(I.B{G.int32(a0, a1, a2, a3), G.int32(a4, a5, a6, a7), _, I.word(T.W{a12, a13, a14, a15})}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
149      %Equal.sym(U32, I.word(T.W{a12, a13, a14, a15}), G.int32(a12, a13, a14, a15), B.word_ok(a12, a13, a14, a15)) : {D.R(I.B{G.int32(a0, a1, a2, a3), G.int32(a4, a5, a6, a7), G.int32(a8, a9, a10, a11), _}) == G.block([a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15]) : Word(128n)}
150      B.pack_int(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15)