def valid_of

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/proof.bend:107

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

107# A key of w bytes, w one of 16, 24, 32, passes the length check.
108def 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}:
109  %Equal.sym(Nat, List.length(&2, U32, key), w, h) : {A.valid_length(_) == True{} : Bool}
110  v