def tea_op_unop

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

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/tea.bend as TE

1513def tea_op_unop(o: TE.LcTeaOp, b: L.LcBlock64) -> {b == TE.tea.op(o, TE.tea.unop(o, b)) : L.LcBlock64}:
1514  match o:
1515    case TE.LcTeaY{+s, +ka, +kb}:
1516      match b:
1517        case L.LcBlock64{y, +z}:
1518          %u32_sub_add(y, TE.tea.g(z, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64}
1519          {==}
1520    case TE.LcTeaZ{+s, +ka, +kb}:
1521      match b:
1522        case L.LcBlock64{+y, z}:
1523          %u32_sub_add(z, TE.tea.g(y, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
1524          {==}
1525    case TE.LcXteaY{+c}:
1526      match b:
1527        case L.LcBlock64{y, +z}:
1528          %u32_sub_add(y, TE.xtea.g(z, c)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64}
1529          {==}
1530    case TE.LcXteaZ{+c}:
1531      match b:
1532        case L.LcBlock64{+y, z}:
1533          %u32_sub_add(z, TE.xtea.g(y, c)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
1534          {==}
1535    case TE.LcTeaBswap{}:
1536      match b:
1537        case L.LcBlock64{+y, +z}:
1538          %bswap2(y) : {L.LcBlock64{y, z} == L.LcBlock64{_, L.lc.bswap.bits(L.lc.bswap.bits(z))} : L.LcBlock64}
1539          %bswap2(z) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
1540          {==}