def round

bend-osdev-crypto@0.1.0.0 · check.bend:163

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr

163# the last 16 bytes of c, and whether d gave the message back
164def round(+m: B.Octets, c: Result<&2, &2, Cr.CrError, B.Octets>, d: Result<&2, &2, Cr.CrError, B.Octets>) -> String:
165  match c d:
166    case Done{+x} Done{y}:
167      ok_if(B.Octets.is_eq(y, m), B.Octets.drop(Nat.sub(B.Octets.len(x), 16n), x))
168    case _ _:
169      "failed"