PROOF.blk_len: def of bend-osdev-aead@0.1.0.0
Import: import bend-osdev-aead@0.1.0.0/PROOF.bend as PROOF
Lines 303-315 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=303&end_line=315

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-aead@0.1.0.0/aesround.bend as R

# every tag has 16 bytes
def blk_len(b: R.AdBlk) -> {16n == B.Octets.len(R.AdBlk.to_octets(b)) : Nat}:
  match b:
    case R.AdBlk{+w0, +w1, +w2, +w3}:
      %olen_of(R.AdBlk.to_list(R.AdBlk{w0, w1, w2, w3})) : {16n == _ : Nat}
      %len_append(B.be32(w0), B.append(B.be32(w1), B.append(B.be32(w2), B.be32(w3)))) : {16n == _ : Nat}
      %len_append(B.be32(w1), B.append(B.be32(w2), B.be32(w3))) : {16n == Nat.add(B.len(B.be32(w0)), _) : Nat}
      %len_append(B.be32(w2), B.be32(w3)) : {16n == Nat.add(B.len(B.be32(w0)), Nat.add(B.len(B.be32(w1)), _)) : Nat}
      %be32_len(w0) : {16n == Nat.add(_, Nat.add(B.len(B.be32(w1)), Nat.add(B.len(B.be32(w2)), B.len(B.be32(w3))))) : Nat}
      %be32_len(w1) : {16n == Nat.add(4n, Nat.add(_, Nat.add(B.len(B.be32(w2)), B.len(B.be32(w3))))) : Nat}
      %be32_len(w2) : {16n == Nat.add(4n, Nat.add(4n, Nat.add(_, B.len(B.be32(w3))))) : Nat}
      %be32_len(w3) : {16n == Nat.add(4n, Nat.add(4n, Nat.add(4n, _))) : Nat}
      {==}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=be32_len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=len_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/PROOF.bend&name=olen_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aesround.bend&name=AdBlk
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aesround.bend&name=AdBlk.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aesround.bend&name=AdBlk.to_octets
  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=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=be32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=len