1	import Base
2	import ../../../src/crypto/aes/gcm.bend as I
3	import ../../../spec/crypto/aes/gcm.bend as G
4	import ./gf.bend as GF
5	
6	# The relation between the implementation's GHASH state and the
7	# specification's field elements.
8	
9	# The field element of an implementation block (its 16 bytes, as SP 800-38D
10	# reads them).
11	def R(z: I.Block) -> Word(128n):
12	  G.block(I.unpack(z))
13	
14	# The U32 the implementation reads for a coefficient c.
15	def bit(c: Bool) -> U32:
16	  U32{WCon{c, Word.zero(31n)}}
17	
18	# Algorithm 1 continued from an implementation accumulator (Z, V) over the
19	# coefficients cs.
20	def F(acc: I.Acc, cs: List<&2, Bool>) -> Word(128n):
21	  match acc:
22	    case I.Acc{z, v}:
23	      GF.sa(128n, G.low(), cs, R(z), R(v))
24	
25	# The implementation's steps over a list of coefficients.
26	def steps(cs: List<&2, Bool>, acc: I.Acc) -> I.Acc:
27	  match cs:
28	    case Nil{}:
29	      acc
30	    case c <> r:
31	      steps(r, I.step(bit(c), acc))