def split_join

bend-osdev-aead@0.1.0.0 · PROOF.bend:156

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
import bend-osdev-aead@0.1.0.0/aead.bend as Ad

156# A ciphertext joined with its tag splits back into the two
157def split_join(+c: B.Octets, +t: B.Octets) -> {Done{Ad.AdSplit{c, t}} == Ad.AdTag.split(B.Octets.len(t), B.Octets.append(c, t)) : Result<&2, &2, Cr.CrError, Ad.AdSplit>}:
158  %olen_append(c, t) : {Done{Ad.AdSplit{c, t}} == Ad.ad.split.pick(Nat.is_lt(_, B.Octets.len(t)), B.Octets.len(t), B.Octets.append(c, t)) : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
159  %nat_lt_add(B.Octets.len(c), B.Octets.len(t)) : {Done{Ad.AdSplit{c, t}} == Ad.ad.split.pick(_, B.Octets.len(t), B.Octets.append(c, t)) : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
160  %olen_append(c, t) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{B.Octets.take(Nat.sub(_, B.Octets.len(t)), B.Octets.append(c, t)), B.Octets.drop(Nat.sub(_, B.Octets.len(t)), B.Octets.append(c, t))}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
161  %nat_sub_add(B.Octets.len(c), B.Octets.len(t)) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{B.Octets.take(_, B.Octets.append(c, t)), B.Octets.drop(_, B.Octets.append(c, t))}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
162  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(c), B.Octets.append(c, t)), c, BL.octets_take_append(c, t)) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{_, B.Octets.drop(B.Octets.len(c), B.Octets.append(c, t))}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
163  %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(c), B.Octets.append(c, t)), t, BL.octets_drop_append(c, t)) : {Done{Ad.AdSplit{c, t}} == Done{Ad.AdSplit{c, _}} : Result<&2, &2, Cr.CrError, Ad.AdSplit>}
164  {==}