def ghash_ok

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash.bend:74

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

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      {==}