def ccmp.ct_refl

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1761

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

1761def ccmp.ct_refl(+xs: List<&2, U32>) -> {M.cm.ct_eq(xs, xs) == True{} : Bool}:
1762  %Equal.sym(U32, M.cm.diff(xs, xs, 0), 0, ccmp.diff_self(xs)) : {U32.is_eq(_, 0) == True{} : Bool}
1763  {==}