def c6_op_unop

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

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

1692def c6_op_unop(o: C6.LcCast6Op, +s: M.CmBlock) -> {s == C6.c6.op(o, C6.c6.unop(o, s)) : M.CmBlock}:
1693  match o:
1694    case C6.LcCast6Op{fwd, +k}:
1695      match fwd:
1696        case True{}:
1697          c6_qbq(k, s)
1698        case False{}:
1699          c6_qq(k, s)

Uses (7)

Used by (1)