def tea_unop_op

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

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

1484def tea_unop_op(o: TE.LcTeaOp, b: L.LcBlock64) -> {b == TE.tea.unop(o, TE.tea.op(o, b)) : L.LcBlock64}:
1485  match o:
1486    case TE.LcTeaY{+s, +ka, +kb}:
1487      match b:
1488        case L.LcBlock64{y, +z}:
1489          %u32_add_sub(y, TE.tea.g(z, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64}
1490          {==}
1491    case TE.LcTeaZ{+s, +ka, +kb}:
1492      match b:
1493        case L.LcBlock64{+y, z}:
1494          %u32_add_sub(z, TE.tea.g(y, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
1495          {==}
1496    case TE.LcXteaY{+c}:
1497      match b:
1498        case L.LcBlock64{y, +z}:
1499          %u32_add_sub(y, TE.xtea.g(z, c)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64}
1500          {==}
1501    case TE.LcXteaZ{+c}:
1502      match b:
1503        case L.LcBlock64{+y, z}:
1504          %u32_add_sub(z, TE.xtea.g(y, c)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
1505          {==}
1506    case TE.LcTeaBswap{}:
1507      match b:
1508        case L.LcBlock64{+y, +z}:
1509          %bswap2(y) : {L.LcBlock64{y, z} == L.LcBlock64{_, L.lc.bswap.bits(L.lc.bswap.bits(z))} : L.LcBlock64}
1510          %bswap2(z) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
1511          {==}