PROOF.split_join: def of bend-osdev-aead@0.1.0.0
Import: import bend-osdev-aead@0.1.0.0/PROOF.bend as PROOF
Lines 156-164 of bend-osdev-aead@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&start_line=156&end_line=164

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

# A ciphertext joined with its tag splits back into the two
def 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>}:
  %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>}
  %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>}
  %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>}
  %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>}
  %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>}
  %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>}
  {==}

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_lt_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=nat_sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=olen_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdSplit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=AdTag.split
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aead.bend&name=ad.split.pick
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_drop_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_take_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.drop
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.take
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/crypto.bend&name=CrError