def valid_of

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/api.bend:19

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as A

19def valid_of(+key: List<&2, U32>, +w: Nat, +h: {List.length(&2, U32, key) == w : Nat}, +v: {A.valid_length(w) == True{} : Bool}) -> {A.valid_length(List.length(&2, U32, key)) == True{} : Bool}:
20  %Equal.sym(Nat, List.length(&2, U32, key), w, h) : {A.valid_length(_) == True{} : Bool}
21  v