law tab_exp_aes

bend-osdev-gf@0.1.1.0 · LAWS.bend:168

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-osdev-gf@0.1.1.0/tables.bend as T

168law tab_exp_aes:
169  for +i: U32
170  for +hi: {Nat.is_lt(U32.to_nat(i), 510n) == True{} : Bool}
171  {T.Gf8Tab.exp(T.Gf8Tab.new(G.Gf8.aes()), i) == (T.Gf8Tab.new(G.Gf8.aes()), G.Gf8.exp(G.Gf8.aes(), U32.to_nat(i))) : T.Gf8Tab & U32}