def blk_len

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

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

303# every tag has 16 bytes
304def blk_len(b: R.AdBlk) -> {16n == B.Octets.len(R.AdBlk.to_octets(b)) : Nat}:
305  match b:
306    case R.AdBlk{+w0, +w1, +w2, +w3}:
307      %olen_of(R.AdBlk.to_list(R.AdBlk{w0, w1, w2, w3})) : {16n == _ : Nat}
308      %len_append(B.be32(w0), B.append(B.be32(w1), B.append(B.be32(w2), B.be32(w3)))) : {16n == _ : Nat}
309      %len_append(B.be32(w1), B.append(B.be32(w2), B.be32(w3))) : {16n == Nat.add(B.len(B.be32(w0)), _) : Nat}
310      %len_append(B.be32(w2), B.be32(w3)) : {16n == Nat.add(B.len(B.be32(w0)), Nat.add(B.len(B.be32(w1)), _)) : Nat}
311      %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}
312      %be32_len(w1) : {16n == Nat.add(4n, Nat.add(_, Nat.add(B.len(B.be32(w2)), B.len(B.be32(w3))))) : Nat}
313      %be32_len(w2) : {16n == Nat.add(4n, Nat.add(4n, Nat.add(_, B.len(B.be32(w3))))) : Nat}
314      %be32_len(w3) : {16n == Nat.add(4n, Nat.add(4n, Nat.add(4n, _))) : Nat}
315      {==}