module Vale.AES.GF128_s
open FStar.Mul