def CmBlock.dec_enc

bend-osdev-mode-core@0.1.0.0 · mode_core.bend:49

import Base

49# Each block of xs encrypted under k and decrypted again: xs itself for
50# every list exactly where decryption undoes encryption at k, which is how
51# the round-trip laws (LAWS.bend) take that property of the cipher
52def CmBlock.dec_enc(~K: Data, ~enc: K -> CmBlock -> CmBlock, ~dec: K -> CmBlock -> CmBlock, +k: K, xs: List<&2, CmBlock>) -> List<&2, CmBlock>:
53  match xs:
54    case Nil{}:
55      Nil{}
56    case Con{x, t}:
57      Con{dec(k, enc(k, x)), CmBlock.dec_enc(~K, ~enc, ~dec, k, t)}