def c6_unop_op

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1683

import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend as C6

1683def c6_unop_op(o: C6.LcCast6Op, +s: M.CmBlock) -> {s == C6.c6.unop(o, C6.c6.op(o, s)) : M.CmBlock}:
1684  match o:
1685    case C6.LcCast6Op{fwd, +k}:
1686      match fwd:
1687        case True{}:
1688          c6_qq(k, s)
1689        case False{}:
1690          c6_qbq(k, s)

Uses (7)

Used by (1)